From 748188f81ae09a591e72af6a29354fbf35a70f07 Mon Sep 17 00:00:00 2001
From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com>
Date: Thu, 23 Jan 2025 01:15:49 +0100
Subject: [PATCH] Update LineInCubic.lean

---
 HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
index ac9e7bd..9921211 100644
--- a/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Even/LineInCubic.lean
@@ -136,7 +136,7 @@ lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ)).LinSols}
   rw [P_P_P!_accCube' g f hfg] at h1
   simp only [Nat.succ_eq_add_one, neg_add_rev, mul_eq_zero] at h1
   cases h1 <;> rename_i h1
-  · apply Or.inl
+  · left
     linear_combination h1
   · cases h1 <;> rename_i h1
     · refine Or.inr (Or.inl ?_)