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

refactor: more multiple-goals

Browse source
This commit is contained in:
jstoobysmith 2024-08-20 15:27:45 -04:00
parent 01f9f7da8b
commit b9479c904d
4 changed files with 166 additions and 180 deletions
Download patch file Download diff file Expand all files Collapse all files

235
HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
View file

@ -179,36 +179,36 @@ lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
simp [basisAsCharges]
simp [δ₁, δ₂]
split
rename_i h1
rw [Fin.ext_iff] at h1
simp_all
rw [Fin.ext_iff] at h
simp_all
split
rename_i h1 h2
simp_all
rw [Fin.ext_iff] at h2
simp at h2
omega
rfl
· rename_i h1
rw [Fin.ext_iff] at h1
simp_all
rw [Fin.ext_iff] at h
simp_all
· split
· rename_i h1 h2
simp_all
rw [Fin.ext_iff] at h2
simp at h2
omega
· rfl
lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (δ!₁ j) = 0 := by
simp [basis!AsCharges]
simp [δ!₁, δ!₂]
split
rename_i h1
rw [Fin.ext_iff] at h1
simp_all
rw [Fin.ext_iff] at h
simp_all
split
rename_i h1 h2
simp_all
rw [Fin.ext_iff] at h2
simp at h2
omega
rfl
· rename_i h1
rw [Fin.ext_iff] at h1
simp_all
rw [Fin.ext_iff] at h
simp_all
· split
· rename_i h1 h2
simp_all
rw [Fin.ext_iff] at h2
simp at h2
omega
rfl
lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ₁ k) (h2 : j ≠ δ₂ k) :
basisAsCharges k j = 0 := by
@ -245,8 +245,8 @@ lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
all_goals rename_i h1 h2
all_goals rw [Fin.ext_iff] at h1 h2
all_goals simp_all
subst h1
exact Fin.elim0 i
· subst h1
exact Fin.elim0 i
all_goals rename_i h3
all_goals rw [Fin.ext_iff] at h3
all_goals simp_all
@ -269,26 +269,26 @@ lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ
lemma basis_on_δ₃ (j : Fin n) : basisAsCharges j δ₃ = 0 := by
simp [basisAsCharges]
split <;> rename_i h
rw [Fin.ext_iff] at h
simp [δ₃, δ₁] at h
omega
split <;> rename_i h2
rw [Fin.ext_iff] at h2
simp [δ₃, δ₂] at h2
omega
rfl
· rw [Fin.ext_iff] at h
simp [δ₃, δ₁] at h
omega
· split <;> rename_i h2
· rw [Fin.ext_iff] at h2
simp [δ₃, δ₂] at h2
omega
· rfl
lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
simp [basis!AsCharges]
split <;> rename_i h
rw [Fin.ext_iff] at h
simp [δ!₃, δ!₁] at h
omega
split <;> rename_i h2
rw [Fin.ext_iff] at h2
simp [δ!₃, δ!₂] at h2
omega
rfl
· rw [Fin.ext_iff] at h
simp [δ!₃, δ!₁] at h
omega
· split <;> rename_i h2
· rw [Fin.ext_iff] at h2
simp [δ!₃, δ!₂] at h2
omega
· rfl
lemma basis_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0 := by
rw [accGrav]
@ -338,16 +338,16 @@ lemma swap!_as_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n)
funext i
rw [← hS, FamilyPermutations_anomalyFreeLinear_apply]
by_cases hi : i = δ!₁ j
subst hi
simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
by_cases hi2 : i = δ!₂ j
subst hi2
simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd]
simp [HSMul.hSMul]
rw [basis!_on_other hi hi2]
change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
simp
· subst hi
simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
· by_cases hi2 : i = δ!₂ j
· subst hi2
simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd]
· simp [HSMul.hSMul]
rw [basis!_on_other hi hi2]
change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
simp
/-- A point in the span of the first part of the basis as a charge. -/
def P (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basisAsCharges i
@ -362,45 +362,45 @@ lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by
rw [P, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
rw [basis_on_δ₁_self]
simp only [mul_one]
intro k _ hkj
rw [basis_on_δ₁_other hkj]
simp only [mul_zero]
simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
· rw [basis_on_δ₁_self]
simp only [mul_one]
· intro k _ hkj
rw [basis_on_δ₁_other hkj]
simp only [mul_zero]
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
rw [basis!_on_δ!₁_self]
simp only [mul_one]
intro k _ hkj
rw [basis!_on_δ!₁_other hkj]
simp only [mul_zero]
simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
· rw [basis!_on_δ!₁_self]
simp only [mul_one]
· intro k _ hkj
rw [basis!_on_δ!₁_other hkj]
simp only [mul_zero]
· simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
rw [P, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
rw [basis_on_δ₂_self]
simp only [mul_neg, mul_one]
intro k _ hkj
rw [basis_on_δ₂_other hkj]
simp only [mul_zero]
simp
· rw [basis_on_δ₂_self]
simp only [mul_neg, mul_one]
· intro k _ hkj
rw [basis_on_δ₂_other hkj]
simp only [mul_zero]
· simp
lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
rw [basis!_on_δ!₂_self]
simp only [mul_neg, mul_one]
intro k _ hkj
rw [basis!_on_δ!₂_other hkj]
simp only [mul_zero]
simp
· rw [basis!_on_δ!₂_self]
simp only [mul_neg, mul_one]
· intro k _ hkj
rw [basis!_on_δ!₂_other hkj]
simp only [mul_zero]
· simp
lemma P_δ₃ (f : Fin n → ℚ) : P f (δ₃) = 0 := by
rw [P, sum_of_charges]
@ -476,12 +476,12 @@ lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
rw [sum_δ!, basis!_on_δ!₃]
simp only [mul_zero, Function.comp_apply, zero_add]
rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
rw [← δ₂_δ!₂, P_δ₂]
ring
intro k _ hkj
erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
simp only [mul_zero, add_zero]
simp
· rw [← δ₂_δ!₂, P_δ₂]
ring
· intro k _ hkj
erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
simp only [mul_zero, add_zero]
· simp
lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
intro i
@ -584,29 +584,27 @@ theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by
have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1
have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1
intro i
simp_all
simp_all only [succ_eq_add_one, Function.comp_apply]
cases i
simp_all
simp_all
· simp_all
· simp_all
lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔ f = f' := by
apply Iff.intro
intro h
funext i
rw [Pa', Pa'] at h
have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basisa i = 0 := by
simp only [add_smul, neg_smul]
rw [Finset.sum_add_distrib]
rw [h]
rw [← Finset.sum_add_distrib]
simp
have h2 : ∀ i, (f i + (- f' i)) = 0 := by
exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n)
(fun i => f i + -f' i) h1
have h2i := h2 i
linarith
intro h
rw [h]
refine Iff.intro (fun h => ?_) (fun h => ?_)
· funext i
rw [Pa', Pa'] at h
have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basisa i = 0 := by
simp only [add_smul, neg_smul]
rw [Finset.sum_add_distrib]
rw [h]
rw [← Finset.sum_add_distrib]
simp
have h2 : ∀ i, (f i + (- f' i)) = 0 := by
exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n)
(fun i => f i + -f' i) h1
have h2i := h2 i
linarith
· rw [h]
/-! TODO: Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`. -/
/-- A helper function for what follows. -/
@ -617,28 +615,23 @@ def join (g f : Fin n → ℚ) : Fin n ⊕ Fin n → ℚ := fun i =>
lemma join_ext (g g' : Fin n → ℚ) (f f' : Fin n → ℚ) :
join g f = join g' f' ↔ g = g' ∧ f = f' := by
apply Iff.intro
intro h
apply And.intro
funext i
exact congr_fun h (Sum.inl i)
funext i
exact congr_fun h (Sum.inr i)
intro h
rw [h.left, h.right]
refine Iff.intro (fun h => ?_) (fun h => ?_)
· apply And.intro
· funext i
exact congr_fun h (Sum.inl i)
· funext i
exact congr_fun h (Sum.inr i)
· rw [h.left, h.right]
lemma join_Pa (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
Pa' (join g f) = Pa' (join g' f') ↔ Pa g f = Pa g' f' := by
apply Iff.intro
intro h
rw [Pa'_eq] at h
rw [join_ext] at h
rw [h.left, h.right]
intro h
apply ACCSystemLinear.LinSols.ext
rw [Pa'_P'_P!', Pa'_P'_P!']
simp [P'_val, P!'_val]
exact h
refine Iff.intro (fun h => ?_) (fun h => ?_)
· rw [Pa'_eq, join_ext] at h
rw [h.left, h.right]
· apply ACCSystemLinear.LinSols.ext
rw [Pa'_P'_P!', Pa'_P'_P!']
simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val]
exact h
lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := by

14
HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
View file

@ -114,8 +114,8 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
exact ne_or_eq _ _
cases h1 <;> rename_i h1
exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
· exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
· exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
∃ g f a, S = parameterization g f a := by
@ -127,11 +127,11 @@ theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
change S.val = _ • (_ • P g + _• P! f)
rw [anomalyFree_param _ _ hS]
rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel, one_smul]
exact hS
have h := h g f hS
rw [anomalyFree_param _ _ hS] at h
simp at h
exact h
· exact hS
· have h := h g f hS
rw [anomalyFree_param _ _ hS] at h
simp at h
exact h
lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
(h : SpecialCase S) :

78
HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
View file

@ -107,10 +107,10 @@ lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
rw [h1] at hc
simp at hc
cases' hc with hc hc
have h2 := (add_eq_zero_iff' (by nlinarith) (sq_nonneg S.Y)).mp hc
simp at h2
exact h2.1
exact hc
· have h2 := (add_eq_zero_iff' (by nlinarith) (sq_nonneg S.Y)).mp hc
simp at h2
exact h2.1
· exact hc
/-- The bijection between the type of linear parameters and `(SMNoGrav 1).LinSols`. -/
def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
@ -120,13 +120,13 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
SMCharges.E S.val (0 : Fin 1)⟩
left_inv S := by
apply linearParameters.ext
rfl
simp only [Fin.isValue]
repeat erw [speciesVal]
simp only [asCharges, neg_add_rev]
ring
simp only [toSpecies_apply]
rfl
· rfl
· simp only [Fin.isValue]
repeat erw [speciesVal]
simp only [asCharges, neg_add_rev]
ring
· simp only [toSpecies_apply]
rfl
right_inv S := by
simp only [Fin.isValue, toSpecies_apply]
apply ACCSystemLinear.LinSols.ext
@ -239,25 +239,25 @@ def bijectionLinearParameters :
have hvw := S.hvw
have hQ := S.hx
apply linearParametersQENeqZero.ext
rfl
field_simp
ring
simp only [tolinearParametersQNeqZero_w, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
toLinearParameters_coe_E']
field_simp
ring
· rfl
· field_simp
ring
· simp only [tolinearParametersQNeqZero_w, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
toLinearParameters_coe_E']
field_simp
ring
right_inv S := by
apply Subtype.ext
have hQ := S.2.1
have hE := S.2.2
apply linearParameters.ext
rfl
field_simp
ring_nf
field_simp [hQ, hE]
field_simp
ring_nf
field_simp [hQ, hE]
· rfl
· field_simp
ring_nf
field_simp [hQ, hE]
· field_simp
ring_nf
field_simp [hQ, hE]
/-- The bijection between `linearParametersQENeqZero` and `LinSols` with `Q` and `E` non-zero. -/
def bijection : linearParametersQENeqZero ≃
@ -332,23 +332,21 @@ lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val
(S.v = -1 ∧ S.w = 0) ∨ (S.v = 0 ∧ S.w = -1) := by
have h' := cubic_v_or_w_zero S h FLTThree
cases' h' with hx hx
simp [hx]
exact cubic_v_zero S h hx
simp [hx]
exact cube_w_zero S h hx
· simp [hx]
exact cubic_v_zero S h hx
· simp [hx]
exact cube_w_zero S h hx
lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔ S.v + S.w = -1 := by
erw [linearParameters.grav]
have hvw := S.hvw
have hQ := S.hx
field_simp
apply Iff.intro
intro h
apply (mul_right_inj' hQ).mp
linear_combination -1 * h / 6
intro h
rw [h]
exact Eq.symm (mul_neg_one (6 * S.x))
refine Iff.intro (fun h => ?_) (fun h => ?_)
· apply (mul_right_inj' hQ).mp
linear_combination -1 * h / 6
· rw [h]
exact Eq.symm (mul_neg_one (6 * S.x))
lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
(FLTThree : FermatLastTheoremWith ℚ 3) :
@ -356,10 +354,10 @@ lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1
rw [grav]
have h' := cube_w_v S h FLTThree
cases' h' with h h
rw [h.1, h.2]
exact Rat.add_zero (-1)
rw [h.1, h.2]
exact Rat.zero_add (-1)
· rw [h.1, h.2]
exact Rat.add_zero (-1)
· rw [h.1, h.2]
exact Rat.zero_add (-1)
end linearParametersQENeqZero

19
HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean
View file

@ -115,9 +115,7 @@ lemma all_dual_eq_getDual?_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l
lemma some_eq_getDual?_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.withUniqueDual) :
l.AreDualInSelf i j ↔ some j = l.getDual? i := by
apply Iff.intro
exact fun h' => all_dual_eq_getDual?_of_mem_withUniqueDual l i h j h'
intro h'
refine Iff.intro (fun h' => all_dual_eq_getDual?_of_mem_withUniqueDual l i h j h') (fun h' => ?_)
have hj : j = (l.getDual? i).get (mem_withUniqueDual_isSome l i h) :=
Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h')))
subst hj
@ -128,8 +126,8 @@ lemma eq_getDual?_get_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.wi
l.AreDualInSelf i j ↔ j = (l.getDual? i).get (mem_withUniqueDual_isSome l i h) := by
rw [l.some_eq_getDual?_of_withUniqueDual_iff i j h]
refine Iff.intro (fun h' => ?_) (fun h' => ?_)
exact Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h')))
simp [h']
· exact Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h')))
· simp [h']
lemma eq_of_areDualInSelf_withUniqueDual {j k : Fin l.length} (i : l.withUniqueDual)
(hj : l.AreDualInSelf i j) (hk : l.AreDualInSelf i k) : j = k := by
@ -198,9 +196,7 @@ lemma all_dual_eq_of_withUniqueDualInOther (i : Fin l.length)
lemma some_eq_getDualInOther?_of_withUniqueDualInOther_iff (i : Fin l.length) (j : Fin l2.length)
(h : i ∈ l.withUniqueDualInOther l2) :
l.AreDualInOther l2 i j ↔ some j = l.getDualInOther? l2 i := by
apply Iff.intro
exact fun h' => l.all_dual_eq_of_withUniqueDualInOther l2 i h j h'
intro h'
refine Iff.intro (fun h' => l.all_dual_eq_of_withUniqueDualInOther l2 i h j h') (fun h' => ?_)
have hj : j = (l.getDualInOther? l2 i).get (mem_withUniqueDualInOther_isSome l l2 i h) :=
Eq.symm (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h')))
subst hj
@ -213,8 +209,8 @@ lemma eq_getDualInOther?_get_of_withUniqueDualInOther_iff (i : Fin l.length) (j
(mem_withUniqueDualInOther_isSome l l2 i h) := by
rw [l.some_eq_getDualInOther?_of_withUniqueDualInOther_iff l2 i j h]
refine Iff.intro (fun h' => ?_) (fun h' => ?_)
exact Eq.symm (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h')))
simp [h']
· exact (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h'))).symm
· simp [h']
@[simp, nolint simpNF]
lemma getDualInOther?_get_getDualInOther?_get_of_withUniqueDualInOther
@ -284,8 +280,7 @@ lemma getDualInOther?_get_of_mem_withUniqueInOther_mem (i : Fin l.length)
simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
getDualInOther?_getDualInOther?_get_isSome, true_and]
apply And.intro
exact getDual?_of_getDualInOther?_of_mem_withUniqueInOther_eq_none l l2 i h
apply And.intro (getDual?_of_getDualInOther?_of_mem_withUniqueInOther_eq_none l l2 i h)
intro j hj
simp only [h, getDualInOther?_getDualInOther?_get_of_withUniqueDualInOther, Option.some.injEq]
by_contra hn