DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor: Replace tactics with rfl if allowed.

Browse source
This commit is contained in:
jstoobysmith 2024-09-03 15:16:06 -04:00
parent 064a5ebbfe
commit d62d59ace2
26 changed files with 82 additions and 123 deletions
Download patch file Download diff file Expand all files Collapse all files

7
HepLean/AnomalyCancellation/PureU1/Odd/LineInCubic.lean
View file

@ -111,12 +111,7 @@ lemma P_P_P!_accCube' {S : (PureU1 (2 * n.succ.succ + 1)).LinSols}
simp at h2
have h5 : f 1 = S.val (δa₂ 0) + S.val δa₁ + S.val (δa₄ 0) := by
linear_combination -(1 * h1) - 1 * h4 - 1 * h2
rw [h5]
rw [δa₄_δ!₂]
have h0 : (δa₂ (0 : Fin n.succ)) = δ!₁ 0 := by
rw [δa₂_δ!₁]
exact ht
rw [h0, δa₁_δ!₃]
rw [h5, δa₄_δ!₂, show (δa₂ (0 : Fin n.succ)) = δ!₁ 0 from rfl, δa₁_δ!₃]
ring
lemma lineInCubicPerm_last_cond {S : (PureU1 (2 * n.succ.succ+1)).LinSols}