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

Merge pull request #141 from HEPLean/Metaprogramming

Browse source 
refactor: change some simp to simp?
This commit is contained in:
Joseph Tooby-Smith 2024-09-04 09:24:47 -04:00 • committed by GitHub
commit 994bb9acf9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
10 changed files with 223 additions and 170 deletions
Download patch file Download diff file Expand all files Collapse all files

76
HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean
View file

@ -62,7 +62,7 @@ lemma ext_δ (S T : Fin (2 * n.succ) → ℚ) (h1 : ∀ i, S (δ₁ i) = T (δ
· let j : Fin n.succ := ⟨i - n.succ, by omega⟩
have h2 := h2 j
have h3 : δ₂ j = i := by
simp [δ₂, Fin.ext_iff]
simp only [succ_eq_add_one, δ₂, Fin.ext_iff, Fin.coe_cast, Fin.coe_natAdd]
omega
rw [h3] at h2
exact h2
@ -170,24 +170,24 @@ lemma basis_on_δ₁_other {k j : Fin n.succ} (h : k ≠ j) :
· rename_i h1 h2
simp_all
rw [Fin.ext_iff] at h2
simp at h2
simp only [Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd] at h2
omega
· rfl
lemma basis_on_other {k : Fin n.succ} {j : Fin (2 * n.succ)} (h1 : j ≠ δ₁ k) (h2 : j ≠ δ₂ k) :
basisAsCharges k j = 0 := by
simp [basisAsCharges]
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges]
simp_all only [ne_eq, ↓reduceIte]
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n.succ)} (h1 : j ≠ δ!₁ k) (h2 : j ≠ δ!₂ k) :
basis!AsCharges k j = 0 := by
simp [basis!AsCharges]
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
simp_all only [ne_eq, ↓reduceIte]
lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
basis!AsCharges k (δ!₁ j) = 0 := by
simp [basis!AsCharges]
simp [δ!₁, δ!₂]
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
simp only [δ!₁, succ_eq_add_one, δ!₂]
split
· rename_i h1
rw [Fin.ext_iff] at h1
@ -198,13 +198,13 @@ lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
· rename_i h1 h2
simp_all
rw [Fin.ext_iff] at h2
simp at h2
simp only [Fin.coe_cast, Fin.coe_natAdd, Fin.coe_castAdd, add_right_inj] at h2
omega
· rfl
lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) :
basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by
simp [basisAsCharges, δ₂, δ₁]
simp only [basisAsCharges, succ_eq_add_one, PureU1_numberCharges, δ₂, δ₁]
split <;> split
any_goals split
any_goals rfl
@ -222,7 +222,7 @@ lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n.succ) :
lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by
simp [basis!AsCharges, δ!₂, δ!₁]
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges, δ!₂, δ!₁]
split <;> split
any_goals split
any_goals split
@ -252,7 +252,7 @@ lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ
rfl
lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
simp [basis!AsCharges]
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
split<;> rename_i h
· simp only [δ!₃, succ_eq_add_one, Fin.isValue, δ!₁, Fin.ext_iff, Fin.coe_cast, Fin.coe_castAdd,
Fin.coe_fin_one, Fin.coe_natAdd] at h
@ -264,14 +264,16 @@ lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
· rfl
lemma basis!_on_δ!₄ (j : Fin n) : basis!AsCharges j δ!₄ = 0 := by
simp [basis!AsCharges]
simp only [basis!AsCharges, succ_eq_add_one, PureU1_numberCharges]
split <;> rename_i h
· rw [Fin.ext_iff] at h
simp [δ!₄, δ!₁] at h
simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.coe_fin_one,
add_zero, δ!₁, Fin.coe_castAdd, add_right_inj] at h
omega
· split <;> rename_i h2
· rw [Fin.ext_iff] at h2
simp [δ!₄, δ!₂] at h2
simp only [succ_eq_add_one, δ!₄, Fin.isValue, Fin.coe_cast, Fin.coe_natAdd, Fin.coe_fin_one,
add_zero, δ!₂, Fin.coe_castAdd, add_right_inj] at h2
omega
· rfl
@ -292,7 +294,7 @@ lemma basis_accCube (j : Fin n.succ) :
rw [accCube_explicit, sum_δ₁_δ₂]
apply Finset.sum_eq_zero
intro i _
simp [basis_δ₂_eq_minus_δ₁]
simp only [succ_eq_add_one, Function.comp_apply, basis_δ₂_eq_minus_δ₁]
ring
lemma basis!_accCube (j : Fin n) :
@ -303,7 +305,7 @@ lemma basis!_accCube (j : Fin n) :
zero_add]
apply Finset.sum_eq_zero
intro i _
simp [basis!_δ!₂_eq_minus_δ!₁]
simp only [basis!_δ!₂_eq_minus_δ!₁]
ring
/-- The first part of the basis as `LinSols`. -/
@ -311,7 +313,7 @@ lemma basis!_accCube (j : Fin n) :
def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols :=
⟨basisAsCharges j, by
intro i
simp at i
simp only [succ_eq_add_one, PureU1_numberLinear] at i
match i with
| 0 =>
exact basis_linearACC j⟩
@ -321,7 +323,7 @@ def basis (j : Fin n.succ) : (PureU1 (2 * n.succ)).LinSols :=
def basis! (j : Fin n) : (PureU1 (2 * n.succ)).LinSols :=
⟨basis!AsCharges j, by
intro i
simp at i
simp only [succ_eq_add_one, PureU1_numberLinear] at i
match i with
| 0 =>
exact basis!_linearACC j⟩
@ -344,7 +346,8 @@ lemma swap!_as_add {S S' : (PureU1 (2 * n.succ)).LinSols} (j : Fin n)
simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
· by_cases hi2 : i = δ!₂ j
· simp [HSMul.hSMul, hi2, basis!_on_δ!₂_self, pairSwap_inv_snd]
· simp [HSMul.hSMul]
· simp only [succ_eq_add_one, Equiv.invFun_as_coe, HSMul.hSMul,
ACCSystemCharges.chargesAddCommMonoid_add, ACCSystemCharges.chargesModule_smul]
rw [basis!_on_other hi hi2]
change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
@ -361,7 +364,7 @@ def Pa (f : Fin n.succ → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n.succ)).Char
lemma P_δ₁ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₁ j) = f j := by
rw [P, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₁_self]
exact Rat.mul_one (f j)
@ -372,7 +375,7 @@ lemma P_δ₁ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₁ j) = f j :=
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₁_self]
exact Rat.mul_one (f j)
@ -389,7 +392,7 @@ lemma Pa_δ!₁ (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (j : Fin n) :
lemma P_δ₂ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₂ j) = - f j := by
rw [P, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
simp only [succ_eq_add_one, HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· simp only [basis_on_δ₂_self, mul_neg, mul_one]
· intro k _ hkj
@ -398,7 +401,7 @@ lemma P_δ₂ (f : Fin n.succ → ℚ) (j : Fin n.succ) : P f (δ₂ j) = - f j
lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₂_self]
exact mul_neg_one (f j)
@ -449,7 +452,7 @@ lemma P_accCube (f : Fin n.succ → ℚ) : accCube (2 * n.succ) (P f) = 0 := by
rw [accCube_explicit, sum_δ₁_δ₂]
apply Finset.sum_eq_zero
intro i _
simp [P_δ₁, P_δ₂]
simp only [succ_eq_add_one, Function.comp_apply, P_δ₁, P_δ₂]
ring
lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by
@ -458,17 +461,18 @@ lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n.succ) (P! f) = 0 := by
zero_add]
apply Finset.sum_eq_zero
intro i _
simp [P!_δ!₁, P!_δ!₂]
simp only [P!_δ!₁, P!_δ!₂]
ring
lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
accCubeTriLinSymm (P g) (P g) (basis!AsCharges j)
= g (j.succ) ^ 2 - g (j.castSucc) ^ 2 := by
simp [accCubeTriLinSymm]
simp only [succ_eq_add_one, accCubeTriLinSymm, PureU1Charges_numberCharges,
TriLinearSymm.mk₃_toFun_apply_apply]
rw [sum_δ!₁_δ!₂, basis!_on_δ!₃, basis!_on_δ!₄]
simp only [mul_zero, add_zero, Function.comp_apply, zero_add]
rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
· simp [δ!₁_δ₁, δ!₂_δ₂]
· simp only [δ!₁_δ₁, mul_one, δ!₂_δ₂, mul_neg]
rw [P_δ₁, P_δ₂]
ring
· intro k _ hkj
@ -479,11 +483,12 @@ lemma P_P_P!_accCube (g : Fin n.succ → ℚ) (j : Fin n) :
lemma P_P!_P!_accCube (g : Fin n → ℚ) (j : Fin n.succ) :
accCubeTriLinSymm (P! g) (P! g) (basisAsCharges j)
= (P! g (δ₁ j))^2 - (P! g (δ₂ j))^2 := by
simp [accCubeTriLinSymm]
simp only [succ_eq_add_one, accCubeTriLinSymm, PureU1Charges_numberCharges,
TriLinearSymm.mk₃_toFun_apply_apply]
rw [sum_δ₁_δ₂]
simp only [Function.comp_apply]
rw [Finset.sum_eq_single j, basis_on_δ₁_self, basis_on_δ₂_self]
· simp [δ!₁_δ₁, δ!₂_δ₂]
· simp only [mul_one, mul_neg]
ring
· intro k _ hkj
erw [basis_on_δ₁_other hkj.symm, basis_on_δ₂_other hkj.symm]
@ -517,10 +522,10 @@ lemma Pa_zero (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
have h1 := Pa_δ!₁ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
have h2 := Pa_δ!₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
rw [h] at h1 h2
simp at h1 h2
simp only [Fin.succ_mk, succ_eq_add_one, Fin.castSucc_mk] at h1 h2
erw [hi2] at h2
change 0 = _ at h2
simp at h2
simp only [neg_zero, zero_sub, zero_eq_neg] at h2
rw [h2] at h1
exact self_eq_add_left.mp h1
exact hinduc i.val i.prop
@ -529,7 +534,7 @@ lemma Pa_zero! (f : Fin n.succ → ℚ) (g : Fin n → ℚ) (h : Pa f g = 0) :
∀ i, g i = 0 := by
have hf := Pa_zero f g h
rw [Pa, P] at h
simp [hf] at h
simp only [succ_eq_add_one, hf, zero_smul, sum_const_zero, zero_add] at h
exact P!_zero g h
/-- A point in the span of the first part of the basis. -/
@ -547,13 +552,13 @@ lemma Pa'_P'_P!' (f : (Fin n.succ) ⊕ (Fin n) → ℚ) :
exact Fintype.sum_sum_type _
lemma P'_val (f : Fin n.succ → ℚ) : (P' f).val = P f := by
simp [P', P]
simp only [succ_eq_add_one, P', P]
funext i
rw [sum_of_anomaly_free_linear, sum_of_charges]
rfl
lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by
simp [P!', P!]
simp only [succ_eq_add_one, P!', P!]
funext i
rw [sum_of_anomaly_free_linear, sum_of_charges]
rfl
@ -660,12 +665,13 @@ lemma span_basis (S : (PureU1 (2 * n.succ)).LinSols) :
∃ (g : Fin n.succ → ℚ) (f : Fin n → ℚ), S.val = P g + P! f := by
have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S)
obtain ⟨f, hf⟩ := h
simp [basisaAsBasis] at hf
simp only [succ_eq_add_one, basisaAsBasis, coe_basisOfLinearIndependentOfCardEqFinrank,
Fintype.sum_sum_type] at hf
change P' _ + P!' _ = S at hf
use f ∘ Sum.inl
use f ∘ Sum.inr
rw [← hf]
simp [P'_val, P!'_val]
simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val]
rfl
lemma P!_in_span (f : Fin n → ℚ) : P! f ∈ Submodule.span ℚ (Set.range basis!AsCharges) := by

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

@ -81,7 +81,7 @@ lemma δa₁_δ!₃ : @δa₁ n = δ!₃ := by
lemma δa₂_δ₁ (j : Fin n) : δa₂ j = δ₁ j.succ := by
rw [Fin.ext_iff]
simp [δa₂, δ₁]
simp only [succ_eq_add_one, δa₂, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, δ₁, Fin.val_succ]
exact Nat.add_comm 1 ↑j
lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by
@ -90,7 +90,8 @@ lemma δa₂_δ!₁ (j : Fin n) : δa₂ j = δ!₁ j.castSucc := by
lemma δa₃_δ₃ : @δa₃ n = δ₃ := by
rw [Fin.ext_iff]
simp [δa₃, δ₃]
simp only [succ_eq_add_one, δa₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd,
Fin.coe_fin_one, add_zero, δ₃]
exact Nat.add_comm 1 n
lemma δa₃_δ!₁ : δa₃ = δ!₁ (Fin.last n) := by
@ -98,7 +99,7 @@ lemma δa₃_δ!₁ : δa₃ = δ!₁ (Fin.last n) := by
lemma δa₄_δ₂ (j : Fin n.succ) : δa₄ j = δ₂ j := by
rw [Fin.ext_iff]
simp [δa₄, δ₂]
simp only [succ_eq_add_one, δa₄, Fin.coe_cast, Fin.coe_natAdd, δ₂, add_left_inj]
exact Nat.add_comm 1 n
lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = δ!₂ j := by
@ -107,7 +108,7 @@ lemma δa₄_δ!₂ (j : Fin n.succ) : δa₄ j = δ!₂ j := by
lemma δ₂_δ!₂ (j : Fin n) : δ₂ j = δ!₂ j := by
rw [Fin.ext_iff]
simp [δ₂, δ!₂]
simp only [δ₂, Fin.coe_cast, Fin.coe_natAdd, δ!₂, add_left_inj]
exact Nat.add_comm n 1
lemma sum_δ (S : Fin (2 * n + 1) → ℚ) :
@ -171,8 +172,8 @@ lemma basis!_on_δ!₁_self (j : Fin n) : basis!AsCharges j (δ!₁ j) = 1 := by
lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
basisAsCharges k (δ₁ j) = 0 := by
simp [basisAsCharges]
simp [δ₁, δ₂]
simp only [basisAsCharges, PureU1_numberCharges]
simp only [δ₁, δ₂]
split
· rename_i h1
rw [Fin.ext_iff] at h1
@ -183,14 +184,14 @@ lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
· rename_i h1 h2
simp_all
rw [Fin.ext_iff] at h2
simp at h2
simp only [Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd] 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 [δ!₁, δ!₂]
simp only [basis!AsCharges, PureU1_numberCharges]
simp only [δ!₁, δ!₂]
split
· rename_i h1
rw [Fin.ext_iff] at h1
@ -201,23 +202,23 @@ lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
· rename_i h1 h2
simp_all
rw [Fin.ext_iff] at h2
simp at h2
simp only [Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd] 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
simp [basisAsCharges]
simp only [basisAsCharges, PureU1_numberCharges]
simp_all only [ne_eq, ↓reduceIte]
lemma basis!_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ!₁ k) (h2 : j ≠ δ!₂ k) :
basis!AsCharges k j = 0 := by
simp [basis!AsCharges]
simp only [basis!AsCharges, PureU1_numberCharges]
simp_all only [ne_eq, ↓reduceIte]
lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n) :
basisAsCharges j (δ₂ i) = - basisAsCharges j (δ₁ i) := by
simp [basisAsCharges, δ₂, δ₁]
simp only [basisAsCharges, PureU1_numberCharges, δ₂, δ₁]
split <;> split
any_goals split
any_goals split
@ -232,7 +233,7 @@ lemma basis_δ₂_eq_minus_δ₁ (j i : Fin n) :
lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
basis!AsCharges j (δ!₂ i) = - basis!AsCharges j (δ!₁ i) := by
simp [basis!AsCharges, δ!₂, δ!₁]
simp only [basis!AsCharges, PureU1_numberCharges, δ!₂, δ!₁]
split <;> split
any_goals split
any_goals split
@ -262,26 +263,30 @@ lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ
rfl
lemma basis_on_δ₃ (j : Fin n) : basisAsCharges j δ₃ = 0 := by
simp [basisAsCharges]
simp only [basisAsCharges, PureU1_numberCharges]
split <;> rename_i h
· rw [Fin.ext_iff] at h
simp [δ₃, δ₁] at h
simp only [δ₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, Fin.coe_fin_one,
add_zero, δ₁] at h
omega
· split <;> rename_i h2
· rw [Fin.ext_iff] at h2
simp [δ₃, δ₂] at h2
simp only [δ₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_natAdd, Fin.coe_fin_one,
add_zero, δ₂] at h2
omega
· rfl
lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
simp [basis!AsCharges]
simp only [basis!AsCharges, PureU1_numberCharges]
split <;> rename_i h
· rw [Fin.ext_iff] at h
simp [δ!₃, δ!₁] at h
simp only [δ!₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_fin_one, δ!₁,
Fin.coe_natAdd] at h
omega
· split <;> rename_i h2
· rw [Fin.ext_iff] at h2
simp [δ!₃, δ!₂] at h2
simp only [δ!₃, Fin.isValue, Fin.coe_cast, Fin.coe_castAdd, Fin.coe_fin_one, δ!₂,
Fin.coe_natAdd] at h2
omega
· rfl
@ -302,7 +307,7 @@ lemma basis!_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basis!AsCharges j) =
def basis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols :=
⟨basisAsCharges j, by
intro i
simp at i
simp only [PureU1_numberLinear] at i
match i with
| 0 =>
exact basis_linearACC j⟩
@ -312,7 +317,7 @@ def basis (j : Fin n) : (PureU1 (2 * n + 1)).LinSols :=
def basis! (j : Fin n) : (PureU1 (2 * n + 1)).LinSols :=
⟨basis!AsCharges j, by
intro i
simp at i
simp only [PureU1_numberLinear] at i
match i with
| 0 =>
exact basis!_linearACC j⟩
@ -338,7 +343,8 @@ lemma swap!_as_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n)
· by_cases hi2 : i = δ!₂ j
· subst hi2
simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd]
· simp [HSMul.hSMul]
· simp only [Equiv.invFun_as_coe, HSMul.hSMul, ACCSystemCharges.chargesAddCommMonoid_add,
ACCSystemCharges.chargesModule_smul]
rw [basis!_on_other hi hi2]
change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
@ -355,7 +361,7 @@ def Pa (f : Fin n → ℚ) (g : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges :=
lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by
rw [P, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₁_self]
exact Rat.mul_one (f j)
@ -366,7 +372,7 @@ lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by
lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₁_self]
exact Rat.mul_one (f j)
@ -377,7 +383,7 @@ lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
rw [P, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis_on_δ₂_self]
exact mul_neg_one (f j)
@ -388,7 +394,7 @@ lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
rw [P!, sum_of_charges]
simp [HSMul.hSMul, SMul.smul]
simp only [HSMul.hSMul, SMul.smul]
rw [Finset.sum_eq_single j]
· rw [basis!_on_δ!₂_self]
exact mul_neg_one (f j)
@ -461,13 +467,13 @@ lemma P!_accCube (f : Fin n → ℚ) : accCube (2 * n +1) (P! f) = 0 := by
simp only [ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, Function.comp_apply, zero_add]
apply Finset.sum_eq_zero
intro i _
simp [P!_δ!₁, P!_δ!₂]
simp only [P!_δ!₁, P!_δ!₂]
ring
lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
accCubeTriLinSymm (P g) (P g) (basis!AsCharges j)
= (P g (δ!₁ j))^2 - (g j)^2 := by
simp [accCubeTriLinSymm]
simp only [accCubeTriLinSymm, PureU1Charges_numberCharges, TriLinearSymm.mk₃_toFun_apply_apply]
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]
@ -495,7 +501,7 @@ lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
have h₃ := Pa_δa₁ f g
rw [h] at h₃
change 0 = _ at h₃
simp at h₃
simp only at h₃
intro i
have hinduc (iv : ℕ) (hiv : iv < n.succ) : f ⟨iv, hiv⟩ = 0 := by
induction iv
@ -506,7 +512,7 @@ lemma Pa_zero (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
have h1 := Pa_δa₄ f g ⟨iv, hivi⟩
rw [h, hi2] at h1
change 0 = _ at h1
simp at h1
simp only [neg_zero, succ_eq_add_one, zero_sub, zero_eq_neg] at h1
have h2 := Pa_δa₂ f g ⟨iv, succ_lt_succ_iff.mp hiv⟩
simp [h, h1] at h2
exact h2.symm
@ -516,7 +522,7 @@ lemma Pa_zero! (f g : Fin n.succ → ℚ) (h : Pa f g = 0) :
∀ i, g i = 0 := by
have hf := Pa_zero f g h
rw [Pa, P] at h
simp [hf] at h
simp only [succ_eq_add_one, hf, zero_smul, sum_const_zero, zero_add] at h
exact P!_zero g h
/-- A point in the span of the first part of the basis. -/
@ -534,13 +540,13 @@ lemma Pa'_P'_P!' (f : (Fin n) ⊕ (Fin n) → ℚ) :
exact Fintype.sum_sum_type _
lemma P'_val (f : Fin n → ℚ) : (P' f).val = P f := by
simp [P', P]
simp only [P', P]
funext i
rw [sum_of_anomaly_free_linear, sum_of_charges]
rfl
lemma P!'_val (f : Fin n → ℚ) : (P!' f).val = P! f := by
simp [P!', P!]
simp only [P!', P!]
funext i
rw [sum_of_anomaly_free_linear, sum_of_charges]
rfl
@ -652,12 +658,13 @@ lemma span_basis (S : (PureU1 (2 * n.succ + 1)).LinSols) :
∃ (g f : Fin n.succ → ℚ), S.val = P g + P! f := by
have h := (mem_span_range_iff_exists_fun ℚ).mp (Basis.mem_span basisaAsBasis S)
obtain ⟨f, hf⟩ := h
simp [basisaAsBasis] at hf
simp only [succ_eq_add_one, basisaAsBasis, coe_basisOfLinearIndependentOfCardEqFinrank,
Fintype.sum_sum_type] at hf
change P' _ + P!' _ = S at hf
use f ∘ Sum.inl
use f ∘ Sum.inr
rw [← hf]
simp [P'_val, P!'_val]
simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val]
rfl
lemma span_basis_swap! {S : (PureU1 (2 * n.succ + 1)).LinSols} (j : Fin n.succ)

66
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
View file

@ -474,7 +474,9 @@ lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
use 0, 0, δ₁₃, 0, 0, - δ₁₃
have hb := exp_ne_zero (I * δ₁₃)
simp [standParam, standParamAsMatrix, h, phaseShift, exp_neg]
simp only [standParam, standParamAsMatrix, ofReal_cos, ofReal_sin, neg_mul, exp_neg, h,
ofReal_zero, mul_zero, zero_mul, sub_zero, zero_sub, phaseShift, phaseShiftMatrix, exp_zero,
mul_one, Submonoid.mk_mul_mk, ofReal_neg, mul_neg, Subtype.mk.injEq]
funext i j
fin_cases i <;> fin_cases j <;>
simp [mul_apply, Fin.sum_univ_three, mul_apply, Fin.sum_univ_three]
@ -494,7 +496,7 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
↑√(VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2)) = ofReal (VAbs 0 0 ⟦V⟧ ^ 2 + VAbs 0 1 ⟦V⟧ ^ 2) := by
rw [Real.mul_self_sqrt]
apply add_nonneg (sq_nonneg _) (sq_nonneg _)
simp at h1
simp only [Fin.isValue, _root_.map_mul, ofReal_eq_coe, map_add, map_pow] at h1
have hx := Vabs_sq_add_neq_zero hb
refine eq_rows V ?_ ?_ hV.2.2.2.2
· funext i
@ -504,10 +506,16 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
cons_val_fin_one, cons_val_one, head_cons, cons_val_two, tail_cons]
rw [hV.1, VudAbs_eq_C₁₂_mul_C₁₃ ⟦V⟧]
simp [C₁₂, C₁₃]
· simp [uRow, standParam, standParamAsMatrix]
· simp only [uRow, Fin.isValue, Fin.mk_one, cons_val_one, head_cons, standParam,
standParamAsMatrix, ofReal_cos, ofReal_sin, ofReal_neg, mul_neg, neg_mul, neg_neg, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd,
tail_cons]
rw [hV.2.1, VusAbs_eq_S₁₂_mul_C₁₃ ⟦V⟧, ← S₁₂_eq_sin_θ₁₂ ⟦V⟧, C₁₃]
simp only [ofReal_mul, ofReal_sin, ofReal_cos]
· simp [uRow, standParam, standParamAsMatrix]
· simp only [uRow, Fin.isValue, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one,
Nat.reduceAdd, tail_cons, head_cons, standParam, standParamAsMatrix, ofReal_cos, ofReal_sin,
ofReal_neg, mul_neg, neg_mul, neg_neg, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
cons_val_one]
nth_rewrite 1 [← abs_mul_exp_arg_mul_I (V.1 0 2)]
rw [show Complex.abs (V.1 0 2) = VubAbs ⟦V⟧ from rfl]
rw [VubAbs_eq_S₁₃, ← S₁₃_eq_sin_θ₁₃ ⟦V⟧]
@ -526,10 +534,13 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
C₂₃_of_Vub_neq_one hb', S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃]
field_simp
rw [h1]
simp [sq]
simp only [Fin.isValue, sq]
field_simp
ring_nf
· simp [cRow, standParam, standParamAsMatrix]
· simp only [cRow, Fin.isValue, Fin.mk_one, cons_val_one, head_cons, standParam,
standParamAsMatrix, ofReal_cos, ofReal_sin, ofReal_neg, mul_neg, neg_mul, neg_neg, cons_val',
cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, Nat.succ_eq_add_one, Nat.reduceAdd,
tail_cons]
rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₂₃_eq_ℂcos_θ₂₃ ⟦V⟧, S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧,
S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧]
rw [C₁₂_eq_Vud_div_sqrt hb', C₂₃_of_Vub_neq_one hb', S₁₂, S₁₃, S₂₃_of_Vub_neq_one hb']
@ -550,26 +561,38 @@ lemma eq_standParam_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0
lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
V = standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
have h1 : VubAbs ⟦V⟧ = 1 := by
simp [VAbs]
simp only [VubAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk]
rw [hV.2.2.2.1]
exact AbsoluteValue.map_one Complex.abs
refine eq_rows V ?_ ?_ hV.2.2.2.2.1
· funext i
fin_cases i
· simp [uRow, standParam, standParamAsMatrix]
· simp only [uRow, Fin.isValue, Fin.zero_eta, cons_val_zero, standParam, standParamAsMatrix,
ofReal_cos, ofReal_sin, ofReal_zero, mul_zero, exp_zero, mul_one, neg_mul, cons_val',
empty_val', cons_val_fin_one, cons_val_one, head_cons, cons_val_two, Nat.succ_eq_add_one,
Nat.reduceAdd, tail_cons]
rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.1]
exact Eq.symm (mul_eq_zero_of_right (cos ↑(θ₁₂ ⟦V⟧)) rfl)
· simp [uRow, standParam, standParamAsMatrix]
· simp only [uRow, Fin.isValue, Fin.mk_one, cons_val_one, head_cons, standParam,
standParamAsMatrix, ofReal_cos, ofReal_sin, ofReal_zero, mul_zero, exp_zero, mul_one, neg_mul,
cons_val', cons_val_zero, empty_val', cons_val_fin_one, cons_val_two, Nat.succ_eq_add_one,
Nat.reduceAdd, tail_cons]
rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.1]
exact Eq.symm (mul_eq_zero_of_right (sin ↑(θ₁₂ ⟦V⟧)) rfl)
· simp [uRow, standParam, standParamAsMatrix]
· simp only [uRow, Fin.isValue, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one,
Nat.reduceAdd, tail_cons, head_cons, standParam, standParamAsMatrix, ofReal_cos, ofReal_sin,
ofReal_zero, mul_zero, exp_zero, mul_one, neg_mul, cons_val', cons_val_zero, empty_val',
cons_val_fin_one, cons_val_one]
rw [S₁₃_eq_ℂsin_θ₁₃ ⟦V⟧, S₁₃]
simp [VAbs]
simp only [Fin.isValue, VubAbs, VAbs, VAbs', Quotient.lift_mk]
rw [hV.2.2.2.1]
simp only [_root_.map_one, ofReal_one]
· funext i
fin_cases i
· simp [cRow, standParam, standParamAsMatrix]
· simp only [cRow, Fin.isValue, Fin.zero_eta, cons_val_zero, standParam, standParamAsMatrix,
ofReal_cos, ofReal_sin, ofReal_zero, mul_zero, exp_zero, mul_one, neg_mul, cons_val',
empty_val', cons_val_fin_one, cons_val_one, head_cons, cons_val_two, Nat.succ_eq_add_one,
Nat.reduceAdd, tail_cons]
rw [S₂₃_eq_ℂsin_θ₂₃ ⟦V⟧, S₂₃_of_Vub_eq_one h1]
rw [S₁₂_eq_ℂsin_θ₁₂ ⟦V⟧, S₁₂_of_Vub_one h1]
rw [C₁₂_eq_ℂcos_θ₁₂ ⟦V⟧, C₁₂_of_Vub_one h1]
@ -585,9 +608,12 @@ lemma eq_standParam_of_ubOnePhaseCond {V : CKMMatrix} (hV : ubOnePhaseCond V) :
simp only [Fin.isValue, ofReal_one, one_mul, ofReal_zero, mul_one, VcdAbs, zero_mul, sub_zero]
have h3 : (Real.cos (θ₂₃ ⟦V⟧) : ℂ) = √(1 - S₂₃ ⟦V⟧ ^ 2) := by
rw [θ₂₃, Real.cos_arcsin]
simp at h3
simp only [ofReal_cos] at h3
rw [h3, S₂₃_of_Vub_eq_one h1, hV.2.2.2.2.2.2]
· simp [cRow, standParam, standParamAsMatrix]
· simp only [cRow, Fin.isValue, Fin.reduceFinMk, cons_val_two, Nat.succ_eq_add_one,
Nat.reduceAdd, tail_cons, head_cons, standParam, standParamAsMatrix, ofReal_cos, ofReal_sin,
ofReal_zero, mul_zero, exp_zero, mul_one, neg_mul, cons_val', cons_val_zero, empty_val',
cons_val_fin_one, cons_val_one]
rw [C₁₃_eq_ℂcos_θ₁₃ ⟦V⟧, C₁₃_of_Vub_eq_one h1, hV.2.2.1]
exact Eq.symm (mul_eq_zero_of_right (sin ↑(θ₂₃ ⟦V⟧)) rfl)
@ -598,12 +624,12 @@ theorem exists_δ₁₃ (V : CKMMatrix) :
by_cases ha : [V]ud ≠ 0 ∨ [V]us ≠ 0
· have haU : [U]ud ≠ 0 ∨ [U]us ≠ 0 := by -- should be much simplier
by_contra hn
simp [not_or] at hn
simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at hn
have hna : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ =0 := by
simp [VAbs]
simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero, VusAbs]
exact hn
rw [hUV] at hna
simp [VAbs] at hna
simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero, VusAbs] at hna
simp_all
have hU' := eq_standParam_of_fstRowThdColRealCond haU hU.2
rw [hU'] at hU
@ -611,10 +637,10 @@ theorem exists_δ₁₃ (V : CKMMatrix) :
rw [← hUV]
exact hU.1
· have haU : ¬ ([U]ud ≠ 0 ∨ [U]us ≠ 0) := by -- should be much simplier
simp [not_or] at ha
simp only [Fin.isValue, ne_eq, not_or, Decidable.not_not] at ha
have h1 : VudAbs ⟦U⟧ = 0 ∧ VusAbs ⟦U⟧ = 0 := by
rw [hUV]
simp [VAbs]
simp only [VudAbs, VAbs, VAbs', Fin.isValue, Quotient.lift_mk, map_eq_zero, VusAbs]
exact ha
simpa [not_or, VAbs] using h1
have ⟨U2, hU2⟩ := ubOnePhaseCond_hold_up_to_equiv_of_ub_one haU hU.2
@ -636,7 +662,7 @@ theorem eq_standardParameterization_δ₃ (V : CKMMatrix) :
← hSV, δ₁₃, Invariant.mulExpδ₁₃])
rw [h2] at hδ₃
exact hδ₃
· simp at h
· simp only [ne_eq, Decidable.not_not] at h
have h1 : δ₁₃ ⟦V⟧ = 0 := by
rw [hSV, δ₁₃, h]
exact arg_zero

7
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Basic.lean
View file

@ -238,14 +238,17 @@ lemma append_val {l l2 : IndexList X} : (l ++ l2).val = l.val ++ l2.val := by
@[simp]
lemma idMap_append_inl {l l2 : IndexList X} (i : Fin l.length) :
(l ++ l2).idMap (appendEquiv (Sum.inl i)) = l.idMap i := by
simp [appendEquiv, idMap]
simp only [idMap, append_val, appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_left,
List.get_eq_getElem]
rw [List.getElem_append_left]
rfl
@[simp]
lemma idMap_append_inr {l l2 : IndexList X} (i : Fin l2.length) :
(l ++ l2).idMap (appendEquiv (Sum.inr i)) = l2.idMap i := by
simp [appendEquiv, idMap, IndexList.length]
simp only [idMap, append_val, length, appendEquiv, Equiv.trans_apply, finSumFinEquiv_apply_right,
RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, List.get_eq_getElem, Fin.coe_cast,
Fin.coe_natAdd]
rw [List.getElem_append_right]
· simp only [Nat.add_sub_cancel_left]
· omega

53
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Color.lean
View file

@ -28,7 +28,7 @@ def dual : Index 𝓒.Color := ⟨𝓒.τ I.toColor, I.id⟩
@[simp]
lemma dual_dual : I.dual.dual = I := by
simp [dual, toColor, id]
simp only [dual, toColor, id]
rw [𝓒.τ_involutive]
rfl
@ -53,11 +53,12 @@ lemma countColorQuot_eq_filter_id_countP (I : Index 𝓒.Color) :
l.countColorQuot I =
(l.val.filter (fun J => I.id = J.id)).countP
(fun J => I.toColor = J.toColor ∨ I.toColor = 𝓒.τ (J.toColor)) := by
simp [countColorQuot]
simp only [countColorQuot, Bool.decide_or]
rw [List.countP_filter]
apply List.countP_congr
intro I' _
simp [Index.eq_iff_color_eq_and_id_eq]
simp only [Index.eq_iff_color_eq_and_id_eq, Bool.decide_and, Index.dual_color, Index.dual_id,
Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, Bool.decide_or]
apply Iff.intro
· intro a_1
cases a_1 with
@ -158,7 +159,7 @@ def countSelf (I : Index 𝓒.Color) : ℕ := l.val.countP (fun J => I = J)
lemma countSelf_eq_filter_id_countP : l.countSelf I =
(l.val.filter (fun J => I.id = J.id)).countP (fun J => I.toColor = J.toColor) := by
simp [countSelf]
rw [countSelf]
rw [List.countP_filter]
apply List.countP_congr
intro I' _
@ -167,7 +168,7 @@ lemma countSelf_eq_filter_id_countP : l.countSelf I =
lemma countSelf_eq_filter_color_countP :
l.countSelf I =
(l.val.filter (fun J => I.toColor = J.toColor)).countP (fun J => I.id = J.id) := by
simp [countSelf]
simp only [countSelf]
rw [List.countP_filter]
apply List.countP_congr
intro I' _
@ -253,11 +254,12 @@ lemma countDual_eq_countSelf_Dual (I : Index 𝓒.Color) : l.countDual I = l.cou
lemma countDual_eq_filter_id_countP : l.countDual I =
(l.val.filter (fun J => I.id = J.id)).countP (fun J => I.toColor = 𝓒.τ (J.toColor)) := by
simp [countDual]
simp only [countDual]
rw [List.countP_filter]
apply List.countP_congr
intro I' _
simp [Index.eq_iff_color_eq_and_id_eq, Index.dual, Index.toColor, Index.id]
simp only [Index.dual, Index.toColor, Index.id, Index.eq_iff_color_eq_and_id_eq, Bool.decide_and,
Bool.and_eq_true, decide_eq_true_eq, and_congr_left_iff]
intro _
refine Iff.intro (fun h => ?_) (fun h => ?_)
· rw [← h]
@ -292,9 +294,10 @@ lemma countSelf_eq_countDual_iff_of_isSome (hl : l.OnlyUniqueDuals)
rcases l.filter_id_of_countId_eq_two hi1 with hf | hf
all_goals
erw [hf]
simp [List.countP, List.countP.go]
simp only [List.countP, List.countP.go, List.get_eq_getElem, decide_True, zero_add,
Nat.reduceAdd, cond_true]
by_cases hn : l.colorMap i = 𝓒.τ (l.colorMap ((l.getDual? i).get hi))
· simp [hn]
· simp only [hn, true_or, iff_true]
have hn' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑((l.getDual? i).get hi)].toColor)
= true := by simpa [colorMap] using hn
erw [hn']
@ -302,34 +305,34 @@ lemma countSelf_eq_countDual_iff_of_isSome (hl : l.OnlyUniqueDuals)
have hτ : l.colorMap ((l.getDual? i).get hi) = 𝓒.τ (l.colorMap i) := by
rw [hn]
exact (𝓒.τ_involutive _).symm
simp [colorMap] at hτ
simp only [colorMap, List.get_eq_getElem] at hτ
erw [hτ]
· have hn' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑((l.getDual? i).get hi)].toColor) =
false := by simpa [colorMap] using hn
erw [hn']
simp [hn]
simp only [cond_false, hn, false_or]
by_cases hm : l.colorMap i = 𝓒.τ (l.colorMap i)
· trans True
· simp
· simp only [iff_true]
have hm' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑i].toColor) = true := by simpa using hm
erw [hm']
simp only [cond_true]
have hm'' : decide (l.val[↑i].toColor = l.val[↑((l.getDual? i).get hi)].toColor)
= false := by
simp only [Fin.getElem_fin, decide_eq_false_iff_not]
simp [colorMap] at hm
simp only [colorMap, List.get_eq_getElem] at hm
erw [hm]
by_contra hn'
have hn'' : l.colorMap i = 𝓒.τ (l.colorMap ((l.getDual? i).get hi)) := by
simp [colorMap]
simp only [colorMap, List.get_eq_getElem]
rw [← hn']
exact (𝓒.τ_involutive _).symm
exact hn hn''
erw [hm'']
rfl
· exact true_iff_iff.mpr hm
· simp [hm]
simp [colorMap] at hm
· simp only [hm, iff_false, ne_eq]
simp only [colorMap, List.get_eq_getElem] at hm
have hm' : decide (l.val[↑i].toColor = 𝓒.τ l.val[↑i].toColor) = false := by simpa using hm
erw [hm']
simp only [cond_false, ne_eq]
@ -357,13 +360,13 @@ lemma iff_withDual :
(l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i := by
refine Iff.intro (fun h i => ?_) (fun h => ?_)
· have h' := congrFun h i
simp at h'
simp only [Function.comp_apply] at h'
rw [show l.getDual? i = some ((l.getDual? i).get (l.withDual_isSome i)) by simp] at h'
have h'' : (Option.guard (fun i => (l.getDual? i).isSome = true) ↑i) = i := by
apply Option.guard_eq_some.mpr
simp [l.withDual_isSome i]
rw [h'', Option.map_some', Option.map_some'] at h'
simp at h'
simp only [Function.comp_apply, Option.some.injEq] at h'
rw [h']
exact 𝓒.τ_involutive (l.colorMap i)
· funext i
@ -376,10 +379,11 @@ lemma iff_withDual :
rw [Option.eq_some_of_isSome hi, Option.map_some']
simp only [Option.some.injEq]
have hii := h ⟨i, (mem_withDual_iff_isSome l i).mpr hi⟩
simp at hii
simp only at hii
rw [← hii]
exact (𝓒.τ_involutive _).symm
· simp [Option.guard, hi]
· simp only [Function.comp_apply, Option.guard, hi, Bool.false_eq_true, ↓reduceIte,
Option.map_none', Option.map_eq_none']
exact Option.not_isSome_iff_eq_none.mp hi
omit [DecidableEq 𝓒.Color] in
@ -462,7 +466,7 @@ lemma mem_iff_dual_mem (hl : l.OnlyUniqueDuals) (hc : l.ColorCond) (I : Index
have hc' := (hc I.dual h hIdd).2
rw [← countSelf_neq_zero] at h ⊢
rw [countDual_eq_countSelf_Dual] at hc'
simp at hc'
simp only [Index.dual_dual] at hc'
exact Ne.symm (ne_of_ne_of_eq (id (Ne.symm h)) hc')
lemma iff_countColorCond (hl : l.OnlyUniqueDuals) :
@ -498,12 +502,13 @@ lemma inl (hl : (l ++ l2).OnlyUniqueDuals) (h : ColorCond (l ++ l2)) : ColorCond
have hI2' : l2.countId I = 0 := by
rw [OnlyUniqueDuals.iff_countId_leq_two'] at hl
have hlI := hl I
simp at hlI
simp only [countId_append] at hlI
omega
have hI' := h I (by
simp only [countSelf_append, ne_eq, add_eq_zero, not_and, hI1, false_implies])
(by simp_all)
simp at hI'
simp only [countColorCond, countColorQuot_append, countId_append, countSelf_append,
countDual_append] at hI'
rw [l2.countColorQuot_of_countId_zero hI2', l2.countSelf_of_countId_zero hI2',
l2.countDual_of_countId_zero hI2', hI2'] at hI'
exact hI'
@ -542,7 +547,7 @@ lemma contrIndexList_left (hl : (l ++ l2).OnlyUniqueDuals) (h1 : (l ++ l2).Color
have h2 := (countId_eq_two_ofcontrIndexList_left_of_OnlyUniqueDuals l l2 hl I hI2)
have hI1' := h1 I (by simp_all; omega) h2
have hIdEq : l.contrIndexList.countId I = l.countId I := by
simp at h2 hI2
simp only [countId_append] at h2 hI2
omega
simp only [countColorCond, countColorQuot_append, countId_append, countSelf_append,
countDual_append]

32
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Contraction.lean
View file

@ -89,20 +89,22 @@ lemma contrIndexList_length : l.contrIndexList.length = l.withoutDual.card := by
@[simp]
lemma contrIndexList_idMap (i : Fin l.contrIndexList.length) : l.contrIndexList.idMap i
= l.idMap (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 := by
simp [contrIndexList_eq_contrIndexList', idMap]
simp only [idMap, List.get_eq_getElem, contrIndexList_eq_contrIndexList', contrIndexList',
List.getElem_ofFn, Function.comp_apply]
rfl
@[simp]
lemma contrIndexList_colorMap (i : Fin l.contrIndexList.length) : l.contrIndexList.colorMap i
= l.colorMap (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1 := by
simp [contrIndexList_eq_contrIndexList', colorMap]
simp only [colorMap, List.get_eq_getElem, contrIndexList_eq_contrIndexList', contrIndexList',
List.getElem_ofFn, Function.comp_apply]
rfl
lemma contrIndexList_areDualInSelf (i j : Fin l.contrIndexList.length) :
l.contrIndexList.AreDualInSelf i j ↔
l.AreDualInSelf (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)).1
(l.withoutDualEquiv (Fin.cast l.contrIndexList_length j)).1 := by
simp [AreDualInSelf]
simp only [AreDualInSelf, ne_eq, contrIndexList_idMap, and_congr_left_iff]
intro _
trans ¬ (l.withoutDualEquiv (Fin.cast l.contrIndexList_length i)) =
(l.withoutDualEquiv (Fin.cast l.contrIndexList_length j))
@ -151,10 +153,11 @@ lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList
rw [contrIndexList_length, h1]
simp only [Finset.card_univ, Fintype.card_fin, List.get_eq_getElem, true_and]
intro n h1' h2
simp [contrIndexList_eq_contrIndexList']
simp only [contrIndexList_eq_contrIndexList', contrIndexList', List.getElem_ofFn,
Function.comp_apply, List.get_eq_getElem]
congr
simp [withoutDualEquiv]
simp [h1]
simp only [withoutDualEquiv, RelIso.coe_fn_toEquiv, Finset.coe_orderIsoOfFin_apply]
simp only [h1]
rw [(Finset.orderEmbOfFin_unique' _
(fun x => Finset.mem_univ ((Fin.castOrderIso _).toOrderEmbedding x))).symm]
· exact Eq.symm (Nat.add_zero n)
@ -167,15 +170,15 @@ lemma contrIndexList_contrIndexList : l.contrIndexList.contrIndexList = l.contrI
@[simp]
lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) :
l.contrIndexList.getDualInOther? l.contrIndexList i = some i := by
simp [getDualInOther?]
simp only [getDualInOther?]
rw [@Fin.find_eq_some_iff]
simp [AreDualInOther]
simp only [AreDualInOther, contrIndexList_idMap, true_and]
intro j hj
have h1 : i = j := by
by_contra hn
have h : l.contrIndexList.AreDualInSelf i j := by
simp only [AreDualInSelf]
simp [hj]
simp only [ne_eq, contrIndexList_idMap, hj, and_true]
exact hn
exact (contrIndexList_areDualInSelf_false l i j).mp h
exact Fin.ge_of_eq (id (Eq.symm h1))
@ -184,7 +187,7 @@ lemma cons_contrIndexList_of_countId_eq_zero {I : Index X}
(h : l.countId I = 0) :
(l.cons I).contrIndexList = l.contrIndexList.cons I := by
apply ext
simp [contrIndexList, countId]
simp only [contrIndexList, countId, cons_val]
rw [List.filter_cons_of_pos]
· apply congrArg
apply List.filter_congr
@ -233,7 +236,7 @@ lemma mem_contrIndexList_filter {I : Index X} (h : I ∈ l.contrIndexList.val) :
rw [List.length_eq_one] at h1
obtain ⟨J, hJ⟩ := h1
rw [hJ] at h2
simp at h2
simp only [List.mem_singleton] at h2
subst h2
exact hJ
@ -279,14 +282,14 @@ lemma countId_contrIndexList_eq_one_iff_countId_eq_one (I : Index X) :
l.contrIndexList.countId I = 1 ↔ l.countId I = 1 := by
refine Iff.intro (fun h => ?_) (fun h => ?_)
· obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l.contrIndexList I (ne_zero_of_eq_one h)
simp [contrIndexList] at hI1
simp only [contrIndexList, List.mem_filter, decide_eq_true_eq] at hI1
rw [countId_congr l hI2]
exact hI1.2
· obtain ⟨I', hI1, hI2⟩ := countId_neq_zero_mem l I (ne_zero_of_eq_one h)
rw [countId_congr l hI2] at h
rw [countId_congr _ hI2]
refine mem_contrIndexList_countId_contrIndexList l ?_
simp [contrIndexList]
simp only [contrIndexList, List.mem_filter, decide_eq_true_eq]
exact ⟨hI1, h⟩
lemma countId_contrIndexList_le_countId (I : Index X) :
@ -318,7 +321,8 @@ lemma filter_id_contrIndexList_eq_of_countId_contrIndexList (I : Index X)
lemma contrIndexList_append_eq_filter : (l ++ l2).contrIndexList.val =
l.contrIndexList.val.filter (fun I => l2.countId I = 0) ++
l2.contrIndexList.val.filter (fun I => l.countId I = 0) := by
simp [contrIndexList]
simp only [contrIndexList, countId_append, append_val, List.filter_append, List.filter_filter,
decide_eq_true_eq, Bool.decide_and]
congr 1
· apply List.filter_congr
intro I hI

4
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/CountId.lean
View file

@ -132,7 +132,7 @@ lemma filter_finRange (i : Fin l.length) :
have h3 : (List.filter (fun j => i = j) (List.finRange l.length)).length = 1 := by
rw [← List.countP_eq_length_filter]
trans List.count i (List.finRange l.length)
· simp [List.count]
· rw [List.count]
apply List.countP_congr (fun j _ => ?_)
simp only [decide_eq_true_eq, beq_iff_eq]
exact eq_comm
@ -317,7 +317,7 @@ lemma mem_withUniqueDual_of_countId_eq_two (i : Fin l.length)
have hj : j ∈ List.filter (fun j => decide (l.AreDualInSelf i j)) (List.finRange l.length) := by
simpa using hj
rw [ha] at hj
simp at hj
simp only [List.mem_singleton] at hj
subst hj
have ht : (l.getDual? i).get ((mem_withDual_iff_isSome l i).mp hw) ∈
(List.finRange l.length).filter (fun j => decide (l.AreDualInSelf i j)) := by

22
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Duals.lean
View file

@ -157,12 +157,12 @@ lemma not_mem_withDual_iff_isNone (i : Fin l.length) :
Option.isNone_iff_eq_none]
lemma mem_withDual_iff_exists : i ∈ l.withDual ↔ ∃ j, l.AreDualInSelf i j := by
simp [withDual, Finset.mem_filter, Finset.mem_univ, getDual?]
simp only [withDual, getDual?, Finset.mem_filter, Finset.mem_univ, true_and]
exact Fin.isSome_find_iff
lemma mem_withInDualOther_iff_exists :
i ∈ l.withDualInOther l2 ↔ ∃ (j : Fin l2.length), l.AreDualInOther l2 i j := by
simp [withDualInOther, Finset.mem_filter, Finset.mem_univ, getDualInOther?]
simp only [withDualInOther, getDualInOther?, Finset.mem_filter, Finset.mem_univ, true_and]
exact Fin.isSome_find_iff
lemma withDual_disjoint_withoutDual : Disjoint l.withDual l.withoutDual := by
@ -183,7 +183,7 @@ lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ :=
intro i
by_cases h : (l.getDual? i).isSome
· simp [withDual, Finset.mem_filter, Finset.mem_univ, h]
· simp at h
· simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at h
simp [withoutDual, Finset.mem_filter, Finset.mem_univ, h]
lemma mem_withUniqueDual_of_mem_withUniqueDualLt (i : Fin l.length) (h : i ∈ l.withUniqueDualLT) :
@ -308,7 +308,7 @@ lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) :
by_cases hik' : i = k'
· exact Fin.ge_of_eq (id (Eq.symm hik'))
· have hik'' : l.AreDualInSelf i k' := by
simp [AreDualInSelf, hik']
simp only [AreDualInSelf, ne_eq, hik', not_false_eq_true, true_and]
simp_all [AreDualInSelf]
have hk'' := hk.2 k' hik''
exact (lt_of_lt_of_le hik hk'').le
@ -329,14 +329,14 @@ lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) :
· subst hik'
exact Lean.Omega.Fin.le_of_not_lt hik
· have hik'' : l.AreDualInSelf i k' := by
simp [AreDualInSelf, hik']
simp_all [AreDualInSelf]
simp only [AreDualInSelf, ne_eq, hik', not_false_eq_true, true_and]
simp_all only [AreDualInSelf, ne_eq, and_imp, not_lt, not_le]
exact hk.2 k' hik''
@[simp]
lemma getDual?_neq_self (i : Fin l.length) : ¬ l.getDual? i = some i := by
intro h
simp [getDual?] at h
simp only [getDual?] at h
rw [Fin.find_eq_some_iff] at h
simp [AreDualInSelf] at h
@ -356,7 +356,7 @@ lemma getDual?_get_id (i : Fin l.length) (h : (l.getDual? i).isSome) :
have h1 : l.getDual? i = some ((l.getDual? i).get h) := Option.eq_some_of_isSome h
nth_rewrite 1 [getDual?] at h1
rw [Fin.find_eq_some_iff] at h1
simp [AreDualInSelf] at h1
simp only [AreDualInSelf, ne_eq, and_imp] at h1
exact h1.1.2.symm
@[simp]
@ -392,7 +392,7 @@ lemma getDualInOther?_id (i : Fin l.length) (h : (l.getDualInOther? l2 i).isSome
Option.eq_some_of_isSome h
nth_rewrite 1 [getDualInOther?] at h1
rw [Fin.find_eq_some_iff] at h1
simp [AreDualInOther] at h1
simp only [AreDualInOther] at h1
exact h1.1.symm
@[simp]
@ -415,7 +415,7 @@ lemma getDualInOther?_getDualInOther?_get_isSome (i : Fin l.length)
@[simp]
lemma getDualInOther?_self_isSome (i : Fin l.length) :
(l.getDualInOther? l i).isSome := by
simp [getDualInOther?]
simp only [getDualInOther?]
rw [@Fin.isSome_find_iff]
exact ⟨i, rfl⟩
@ -425,7 +425,7 @@ lemma getDualInOther?_getDualInOther?_get_self (i : Fin l.length) :
some ((l.getDualInOther? l i).get (getDualInOther?_self_isSome l i)) := by
nth_rewrite 1 [getDualInOther?]
rw [Fin.find_eq_some_iff]
simp [AreDualInOther]
simp only [AreDualInOther, getDualInOther?_id, true_and]
intro j hj
have h1 := Option.eq_some_of_isSome (getDualInOther?_self_isSome l i)
nth_rewrite 1 [getDualInOther?] at h1

4
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Equivs.lean
View file

@ -94,7 +94,7 @@ lemma getDual?_getDualEquiv (i : l.withUniqueDual) : l.getDual? (l.getDualEquiv
have h1 := (Equiv.apply_symm_apply l.getDualEquiv i).symm
nth_rewrite 2 [h1]
nth_rewrite 2 [getDualEquiv]
simp
simp only [Equiv.coe_fn_mk, Option.some_get]
rfl
/-- An equivalence from `l.withUniqueDualInOther l2 ` to
@ -140,7 +140,7 @@ omit [IndexNotation X] [Fintype X] in
lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ := by
apply Equiv.ext
intro x
simp [getDualInOtherEquiv]
simp only [getDualInOtherEquiv, Equiv.coe_fn_mk, Equiv.refl_apply]
apply Subtype.eq
simp only
have hx2 := x.2

50
HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexList/Normalize.lean
View file

@ -184,7 +184,7 @@ lemma findIdx?_on_finRange_eq_findIdx {n : ℕ} (p : Fin n → Prop) [DecidableP
rw [@Fin.find_eq_some_iff] at hi ⊢
simp_all only [Function.comp_apply, Fin.succ_pred, true_and]
exact fun j hj => (Fin.pred_le_iff hn).mpr (hi.2 j.succ hj)
· simp at hs
· simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at hs
rw [hs]
simp only [Nat.succ_eq_add_one, Option.map_eq_none']
rw [@Fin.find_eq_none_iff] at hs ⊢
@ -229,7 +229,8 @@ lemma idList_getDualInOther? : l.idList =
rw [idList, idListFin_getDualInOther?]
lemma mem_idList_of_mem {I : Index X} (hI : I ∈ l.val) : I.id ∈ l.idList := by
simp [idList_getDualInOther?]
simp only [idList_getDualInOther?, List.mem_map, List.mem_filter, List.mem_finRange,
decide_eq_true_eq, true_and]
have hI : l.val.indexOf I < l.val.length := List.indexOf_lt_length.mpr hI
have hI' : I = l.val.get ⟨l.val.indexOf I, hI⟩ := Eq.symm (List.indexOf_get hI)
rw [hI']
@ -257,7 +258,7 @@ lemma idList_indexOf_get (i : Fin l.length) :
l.idList.indexOf (l.idMap i) = l.idListFin.indexOf ((l.getDualInOther? l i).get
(getDualInOther?_self_isSome l i)) := by
rw [idList]
simp [idListFin_getDualInOther?]
simp only [idListFin_getDualInOther?]
rw [← indexOf_map' l.idMap (fun i => (l.getDualInOther? l i).get
(getDualInOther?_self_isSome l i))]
· intro i _ j
@ -271,7 +272,7 @@ lemma idList_indexOf_get (i : Fin l.length) :
· exact congrArg l.idMap h
· exact getDualInOther?_id l l j (getDualInOther?_self_isSome l j)
· intro i hi
simp at hi
simp only [List.mem_filter, List.mem_finRange, decide_eq_true_eq, true_and] at hi
exact Option.get_of_mem (getDualInOther?_self_isSome l i) hi
· exact fun i => Eq.symm (getDualInOther?_id l l i (getDualInOther?_self_isSome l i))
@ -343,9 +344,9 @@ lemma areDualInSelf_of (h : GetDualCast l l2) (i j : Fin l.length) (hA : l.AreDu
have h1 : ((l2.getDual? (Fin.cast h.1 j)).get ((getDual?_isSome_iff h j).mp hn))
= ((l2.getDual? (Fin.cast h.1 i)).get ((getDual?_isSome_iff h i).mp hni)) := by
simpa [Fin.ext_iff] using h1'
simp [AreDualInSelf]
simp only [AreDualInSelf, ne_eq]
apply And.intro
· simp [AreDualInSelf] at hA
· simp only [AreDualInSelf, ne_eq] at hA
simpa [Fin.ext_iff] using hA.1
trans l2.idMap ((l2.getDual? (Fin.cast h.1 j)).get ((getDual?_isSome_iff h j).mp hn))
· trans l2.idMap ((l2.getDual? (Fin.cast h.1 i)).get ((getDual?_isSome_iff h i).mp hni))
@ -367,7 +368,7 @@ lemma idMap_eq_of (h : GetDualCast l l2) (i j : Fin l.length) (hm : l.idMap i =
by_cases h1 : i = j
· exact congrArg l2.idMap (congrArg (Fin.cast h.left) h1)
have h1' : l.AreDualInSelf i j := by
simp [AreDualInSelf]
simp only [AreDualInSelf, ne_eq]
exact ⟨h1, hm⟩
rw [h.areDualInSelf_iff] at h1'
simpa using h1'.2
@ -390,10 +391,10 @@ lemma iff_idMap_eq : GetDualCast l l2 ↔
simp only [Function.comp_apply]
by_cases h1 : (l.getDual? i).isSome
· have h1' : (l2.getDual? (Fin.cast h.1 i)).isSome := by
simp [getDual?, Fin.isSome_find_iff] at h1 ⊢
simp only [getDual?, Fin.isSome_find_iff] at h1 ⊢
obtain ⟨j, hj⟩ := h1
use (Fin.cast h.1 j)
simp [AreDualInSelf] at hj ⊢
simp only [AreDualInSelf, ne_eq] at hj ⊢
rw [← h.2]
simpa [Fin.ext_iff] using hj
have h2 := Option.eq_some_of_isSome h1'
@ -402,26 +403,26 @@ lemma iff_idMap_eq : GetDualCast l l2 ↔
rw [Fin.find_eq_some_iff] at h2 ⊢
apply And.intro
· apply And.intro
· simp [AreDualInSelf] at h2
· simp only [AreDualInSelf, ne_eq, getDual?_get_id, and_true, and_imp] at h2
simpa [Fin.ext_iff] using h2.1
· rw [h.2 h.1]
simp
· intro j hj
apply h2.2 (Fin.cast h.1 j)
simp [AreDualInSelf] at hj ⊢
simp only [AreDualInSelf, ne_eq] at hj ⊢
apply And.intro
· simpa [Fin.ext_iff] using hj.1
· rw [← h.2]
simpa using hj.2
· simp at h1
· simp only [Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at h1
rw [h1]
symm
refine Option.map_eq_none'.mpr ?_
rw [getDual?, Fin.find_eq_none_iff] at h1 ⊢
simp [AreDualInSelf]
simp only [AreDualInSelf, ne_eq, not_and]
intro j hij
have h1j := h1 (Fin.cast h.1.symm j)
simp [AreDualInSelf] at h1j
simp only [AreDualInSelf, ne_eq, not_and] at h1j
rw [h.2 h.1] at h1j
apply h1j
exact ne_of_apply_ne (Fin.cast h') hij
@ -447,12 +448,12 @@ lemma getDualInOther?_get (h : GetDualCast l l2) (i : Fin l.length) :
have h1 := Option.eq_some_of_isSome (getDualInOther?_self_isSome l2 (Fin.cast h.left i))
erw [Fin.find_eq_some_iff] at h1
apply And.intro
· simp [AreDualInOther]
· simp only [AreDualInOther]
rw [idMap_eq_iff h]
simp
· intro j hj
apply h1.2 (Fin.cast h.1 j)
simp [AreDualInOther]
simp only [AreDualInOther]
exact (idMap_eq_iff h i j).mp hj
lemma countId_cast (h : GetDualCast l l2) (i : Fin l.length) :
@ -478,11 +479,12 @@ lemma idListFin_cast (h : GetDualCast l l2) :
rw [h1]
rw [List.filter_map]
have h1 : Fin.cast h.1 ∘ Fin.cast h.1.symm = id := rfl
simp [h1]
simp only [List.map_map, h1, List.map_id]
rw [idListFin_getDualInOther?]
apply List.filter_congr
intro i _
simp [getDualInOther?, Fin.find_eq_some_iff, AreDualInOther]
simp only [getDualInOther?, AreDualInOther, Fin.find_eq_some_iff, true_and, Function.comp_apply,
decide_eq_decide]
refine Iff.intro (fun h' j hj => ?_) (fun h' j hj => ?_)
· simpa using h' (Fin.cast h.1.symm j) (by rw [h.idMap_eq_iff]; exact hj)
· simpa using h' (Fin.cast h.1 j) (by rw [h.symm.idMap_eq_iff]; exact hj)
@ -518,7 +520,7 @@ lemma normalize_eq_map :
have hl : l.val = List.map l.val.get (List.finRange l.length) := by
simp [length]
rw [hl]
simp [normalize]
simp only [normalize, List.map_map]
exact List.ofFn_eq_map
omit [DecidableEq X] in
@ -548,13 +550,13 @@ lemma normalize_countId (i : Fin l.normalize.length) :
l.normalize.countId l.normalize.val[Fin.val i] =
l.countId (l.val.get ⟨i, by simpa using i.2⟩) := by
rw [countId, countId]
simp [l.normalize_eq_map, Index.id]
simp only [Index.id, l.normalize_eq_map, List.getElem_map, List.countP_map, List.get_eq_getElem]
apply List.countP_congr
intro J hJ
simp only [Function.comp_apply, decide_eq_true_eq]
trans List.indexOf (l.val.get ⟨i, by simpa using i.2⟩).id l.idList = List.indexOf J.id l.idList
· rfl
· simp
· simp only [List.get_eq_getElem]
rw [idList_indexOf_mem]
· rfl
· exact List.getElem_mem l.val _ _
@ -564,13 +566,13 @@ lemma normalize_countId (i : Fin l.normalize.length) :
lemma normalize_countId' (i : Fin l.length) (hi : i.1 < l.normalize.length) :
l.normalize.countId (l.normalize.val[Fin.val i]) = l.countId (l.val.get i) := by
rw [countId, countId]
simp [l.normalize_eq_map, Index.id]
simp only [Index.id, l.normalize_eq_map, List.getElem_map, List.countP_map, List.get_eq_getElem]
apply List.countP_congr
intro J hJ
simp only [Function.comp_apply, decide_eq_true_eq]
trans List.indexOf (l.val.get i).id l.idList = List.indexOf J.id l.idList
· rfl
· simp
· simp only [List.get_eq_getElem]
rw [idList_indexOf_mem]
· rfl
· exact List.getElem_mem l.val _ _
@ -689,7 +691,7 @@ lemma normalize_colorMap_eq_of_eq_colorMap (h : l.length = l2.length)
(hc : l.colorMap = l2.colorMap ∘ Fin.cast h) :
l.normalize.colorMap = l2.normalize.colorMap ∘
Fin.cast (normalize_length_eq_of_eq_length l l2 h) := by
simp [hc]
simp only [normalize_colorMap, hc]
rfl
/-!