From 1c9d66ee19f1a2ec829f9057bdc3ae166f1e2a6c Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Thu, 15 Aug 2024 10:53:30 -0400 Subject: [PATCH] refactor: Lint --- .../LorentzTensor/IndexNotation/AreDual.lean | 13 ++--- .../LorentzTensor/IndexNotation/Basic.lean | 2 - .../LorentzTensor/IndexNotation/Color.lean | 39 +++++-------- .../IndexNotation/Contraction.lean | 32 +++++------ .../LorentzTensor/IndexNotation/GetDual.lean | 20 +++---- .../IndexNotation/IndexString.lean | 2 +- .../IndexNotation/OnlyUniqueDuals.lean | 20 +++---- .../IndexNotation/Relations.lean | 7 +-- .../IndexNotation/TensorIndex.lean | 15 ++--- .../LorentzTensor/IndexNotation/WithDual.lean | 4 -- .../IndexNotation/WithUniqueDual.lean | 57 +++++++------------ .../LorentzTensor/Real/IndexNotation.lean | 6 +- 12 files changed, 79 insertions(+), 138 deletions(-) diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/AreDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/AreDual.lean index 6cd928a..1e68771 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/AreDual.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/AreDual.lean @@ -12,13 +12,11 @@ import HepLean.SpaceTime.LorentzTensor.IndexNotation.Basic namespace IndexNotation - namespace IndexList variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable (l l2 l3 : IndexList X) - /-! ## Are dual indices @@ -30,7 +28,7 @@ def AreDualInSelf (i j : Fin l.length) : Prop := i ≠ j ∧ l.idMap i = l.idMap j /-- Two indices in different `IndexLists` are dual to one another if they have the same `id`. -/ -def AreDualInOther (i : Fin l.length) (j : Fin l2.length) : +def AreDualInOther (i : Fin l.length) (j : Fin l2.length) : Prop := l.idMap i = l2.idMap j namespace AreDualInSelf @@ -74,12 +72,11 @@ lemma append_inr_inl (l l2 : IndexList X) (i : Fin l2.length) (j : Fin l.length) end AreDualInSelf - namespace AreDualInOther variable {l l2 l3 : IndexList X} {i : Fin l.length} {j : Fin l2.length} -instance {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) : +instance {l : IndexList X} {l2 : IndexList X} (i : Fin l.length) (j : Fin l2.length) : Decidable (l.AreDualInOther l2 i j) := (l.idMap i).decEq (l2.idMap j) @[symm] @@ -93,17 +90,17 @@ lemma append_of_inl (i : Fin l.length) (j : Fin l3.length) : simp [AreDualInOther] @[simp] -lemma append_of_inr (i : Fin l2.length) (j : Fin l3.length) : +lemma append_of_inr (i : Fin l2.length) (j : Fin l3.length) : (l ++ l2).AreDualInOther l3 (appendEquiv (Sum.inr i)) j ↔ l2.AreDualInOther l3 i j := by simp [AreDualInOther] @[simp] -lemma of_append_inl (i : Fin l.length) (j : Fin l2.length) : +lemma of_append_inl (i : Fin l.length) (j : Fin l2.length) : l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inl j)) ↔ l.AreDualInOther l2 i j := by simp [AreDualInOther] @[simp] -lemma of_append_inr (i : Fin l.length) (j : Fin l3.length) : +lemma of_append_inr (i : Fin l.length) (j : Fin l3.length) : l.AreDualInOther (l2 ++ l3) i (appendEquiv (Sum.inr j)) ↔ l.AreDualInOther l3 i j := by simp [AreDualInOther] diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean index a45f97f..4fbad2e 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Basic.lean @@ -243,7 +243,6 @@ instance : Fintype l.toPosSet where def toPosFinset (l : IndexList X) : Finset (Fin l.length × Index X) := l.toPosSet.toFinset - /-- The construction of a list of indices from a map from `Fin n` to `Index X`. -/ def fromFinMap {n : ℕ} (f : Fin n → Index X) : IndexList X where @@ -368,7 +367,6 @@ lemma colorMap_sumELim (l1 l2 : IndexList X) : | Sum.inl i => simp | Sum.inr i => simp - end append end IndexList diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean index feb77cf..36f75c3 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Color.lean @@ -20,7 +20,6 @@ a Tensor Color structure. namespace IndexNotation - namespace IndexList variable {𝓒 : TensorColor} @@ -55,7 +54,7 @@ lemma iff_withDual : · have h'' : (Option.guard (fun i => (l.getDual? i).isSome = true) ↑i) = i := by apply Option.guard_eq_some.mpr simp only [true_and] - exact hi + exact hi simp only [Function.comp_apply, h'', Option.map_some'] rw [show l.getDual? ↑i = some ((l.getDual? i).get hi) by simp] rw [Option.map_some'] @@ -140,10 +139,10 @@ lemma symm (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond ( colorMap_append_inr, true_implies, getDual?_append_inr_getDualInOther?_isSome, colorMap_append_inl] -lemma inr (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) : +lemma inr (hu : (l ++ l2).withUniqueDual = (l ++ l2).withDual) (h : ColorCond (l ++ l2)) : ColorCond l2 := inl (symm hu h) -lemma triple_right (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) +lemma triple_right (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) (h : ColorCond (l ++ l2 ++ l3)) : ColorCond (l2 ++ l3) := by have h1 := assoc h rw [append_assoc] at hu @@ -158,8 +157,7 @@ lemma triple_drop_mid (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).wit rw [append_withDual_eq_withUniqueDual_symm, append_assoc] at hu exact append_withDual_eq_withUniqueDual_inr _ _ hu - -lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) +lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) (h : ColorCond (l ++ l2 ++ l3)) : ColorCond (l2 ++ l ++ l3) := by have hC := h @@ -222,7 +220,7 @@ lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) simp only [mem_withDual_iff_isSome, mem_withInDualOther_iff_isSome, getDualInOther?_isSome_of_append_iff, not_or, Bool.not_eq_true, Option.not_isSome, Option.isNone_iff_eq_none] at hn - by_cases hk' : (l3.getDual? k).isSome + by_cases hk' : (l3.getDual? k).isSome · simp_all only [mem_withDual_iff_isSome, true_iff, Option.isNone_iff_eq_none, getDualInOther?_eq_none_of_append_iff, and_self, getDual?_inr_getDualInOther?_isNone_getDual?_isSome, Option.get_some, colorMap_append_inr] @@ -256,8 +254,8 @@ lemma swap (hu : (l ++ l2 ++ l3).withUniqueDual = (l ++ l2 ++ l3).withDual) /-- A bool which is true for an index list if and only if every index and its' dual, when it exists, have dual colors. -/ def bool (l : IndexList 𝓒.Color) : Bool := - if (∀ (i : l.withDual), 𝓒.τ - (l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i) then + if (∀ (i : l.withDual), 𝓒.τ + (l.colorMap ((l.getDual? i).get (l.withDual_isSome i))) = l.colorMap i) then true else false @@ -268,11 +266,8 @@ lemma iff_bool : l.ColorCond ↔ bool l := by end ColorCond - - end IndexList - variable (𝓒 : TensorColor) variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] @@ -284,7 +279,7 @@ variable [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color `['ᵘ¹', 'ᵤ₁', 'ᵤ₁']` cannot. -/ structure ColorIndexList (𝓒 : TensorColor) [IndexNotation 𝓒.Color] extends IndexList 𝓒.Color where /-- The condition that for index with a dual, that dual is the unique other index with - an identical `id`. -/ + an identical `id`. -/ unique_duals : toIndexList.withDual = toIndexList.withUniqueDual /-- The condition that for an index with a dual, that dual has dual color to the index. -/ dual_color : IndexList.ColorCond toIndexList @@ -305,7 +300,7 @@ def empty : ColorIndexList 𝓒 where dual_color := rfl /-- The colorMap of a `ColorIndexList` as a `𝓒.ColorMap`. - This is to be compared with `colorMap` which is a map `Fin l.length → 𝓒.Color`. -/ + This is to be compared with `colorMap` which is a map `Fin l.length → 𝓒.Color`. -/ def colorMap' : 𝓒.ColorMap (Fin l.length) := l.colorMap @@ -317,14 +312,13 @@ lemma ext {l l' : ColorIndexList 𝓒} (h : l.val = l'.val) : l = l' := by apply IndexList.ext exact h - /-! TODO: `orderEmbOfFin_univ` should be replaced with a mathlib lemma if possible. -/ -lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m): +lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m) : Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (by simp [h]: Finset.univ.card = m) = (Fin.castOrderIso h.symm).toOrderEmbedding := by symm have h1 : (Fin.castOrderIso h.symm).toFun = - ( Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) + (Finset.orderEmbOfFin (Finset.univ : Finset (Fin n)) (by simp [h]: Finset.univ.card = m)).toFun := by apply Finset.orderEmbOfFin_unique intro x @@ -332,7 +326,6 @@ lemma orderEmbOfFin_univ (n m : ℕ) (h : n = m): exact fun ⦃a b⦄ a => a exact Eq.symm (Fin.orderEmbedding_eq (congrArg Set.range (id (Eq.symm h1)))) - /-! ## Contracting an `ColorIndexList` @@ -388,7 +381,6 @@ lemma contr_areDualInSelf (i j : Fin l.contr.length) : l.contr.AreDualInSelf i j ↔ False := by simp [contr] - /-! ## Contract equiv @@ -397,7 +389,7 @@ lemma contr_areDualInSelf (i j : Fin l.contr.length) : /-- An equivalence splitting the indices of `l` into a sum type of those indices and their duals (with choice determined by the ordering on `Fin`), - and those indices without duals. + and those indices without duals. This equivalence is used to contract the indices of tensors. -/ def contrEquiv : (l.withUniqueDualLT ⊕ l.withUniqueDualLT) ⊕ Fin l.contr.length ≃ Fin l.length := @@ -464,7 +456,7 @@ lemma contrEquiv_on_withDual_empty (i : Fin l.contr.length) (h : l.withDual = -/ -/-- The condition on the `ColorIndexList`s `l` and `l2` so that on appending they form +/-- The condition on the `ColorIndexList`s `l` and `l2` so that on appending they form a `ColorIndexList`. -/ def AppendCond : Prop := (l.toIndexList ++ l2.toIndexList).withUniqueDual = (l.toIndexList ++ l2.toIndexList).withDual @@ -541,13 +533,13 @@ lemma appendCond_of_eq (h1 : l.withUniqueDual = l.withDual) /-- A boolean which is true for two index lists `l` and `l2` if on appending they can form a `ColorIndexList`. -/ def bool (l l2 : IndexList 𝓒.Color) : Bool := - if ¬ (l ++ l2).withUniqueDual = (l ++ l2).withDual then + if ¬ (l ++ l2).withUniqueDual = (l ++ l2).withDual then false else ColorCond.bool (l ++ l2) lemma bool_iff (l l2 : IndexList 𝓒.Color) : - bool l l2 ↔ (l ++ l2).withUniqueDual = (l ++ l2).withDual ∧ ColorCond.bool (l ++ l2) := by + bool l l2 ↔ (l ++ l2).withUniqueDual = (l ++ l2).withDual ∧ ColorCond.bool (l ++ l2) := by simp [bool] lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndexList l2.toIndexList := by @@ -558,7 +550,6 @@ lemma iff_bool (l l2 : ColorIndexList 𝓒) : AppendCond l l2 ↔ bool l.toIndex end AppendCond - end ColorIndexList end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean index 57d9db8..14e7e99 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Contraction.lean @@ -14,7 +14,6 @@ import Mathlib.Data.Finset.Sort namespace IndexNotation - namespace IndexList variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] @@ -53,10 +52,10 @@ lemma withDual_union_withoutDual : l.withDual ∪ l.withoutDual = Finset.univ := /-- An equivalence from `Fin l.withoutDual.card` to `l.withoutDual` determined by the order on `l.withoutDual` inherted from `Fin`. -/ -def withoutDualEquiv : Fin l.withoutDual.card ≃ l.withoutDual := +def withoutDualEquiv : Fin l.withoutDual.card ≃ l.withoutDual := (Finset.orderIsoOfFin l.withoutDual (by rfl)).toEquiv -/-- An equivalence splitting the indices of an index list `l` into those indices +/-- An equivalence splitting the indices of an index list `l` into those indices which have a dual in `l` and those which do not have a dual in `l`. -/ def dualEquiv : l.withDual ⊕ Fin l.withoutDual.card ≃ Fin l.length := (Equiv.sumCongr (Equiv.refl _) l.withoutDualEquiv).trans <| @@ -131,10 +130,10 @@ lemma contrIndexList_areDualInSelf_false (i j : Fin l.contrIndexList.length) : @[simp] lemma contrIndexList_of_withDual_empty (h : l.withDual = ∅) : l.contrIndexList = l := by have h1 := l.withDual_union_withoutDual - rw [h , Finset.empty_union] at h1 + rw [h, Finset.empty_union] at h1 apply ext rw [@List.ext_get_iff] - change l.contrIndexList.length = l.length ∧ _ + change l.contrIndexList.length = l.length ∧ _ rw [contrIndexList_length, h1] simp only [Finset.card_univ, Fintype.card_fin, List.get_eq_getElem, true_and] intro n h1' h2 @@ -152,7 +151,7 @@ lemma contrIndexList_contrIndexList : l.contrIndexList.contrIndexList = l.contrI simp @[simp] -lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) : +lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) : l.contrIndexList.getDualInOther? l.contrIndexList i = some i := by simp [getDualInOther?] rw [@Fin.find_eq_some_iff] @@ -160,14 +159,13 @@ lemma contrIndexList_getDualInOther?_self (i : Fin l.contrIndexList.length) : intro j hj have h1 : i = j := by by_contra hn - have h : l.contrIndexList.AreDualInSelf i j := by + have h : l.contrIndexList.AreDualInSelf i j := by simp only [AreDualInSelf] simp [hj] exact hn exact (contrIndexList_areDualInSelf_false l i j).mp h exact Fin.ge_of_eq (id (Eq.symm h1)) - /-! ## Splitting withUniqueDual @@ -231,7 +229,7 @@ lemma option_not_lt (i j : Option (Fin l.length)) : i < j → i ≠ j → ¬ j < exact Fin.lt_asymm h /-! TODO: Replace with a mathlib lemma. -/ -lemma lt_option_of_not (i j : Option (Fin l.length)) : ¬ j < i → i ≠ j → i < j := by +lemma lt_option_of_not (i j : Option (Fin l.length)) : ¬ j < i → i ≠ j → i < j := by match i, j with | none, none => exact fun a b => a (a (a (b rfl))) @@ -243,7 +241,7 @@ lemma lt_option_of_not (i j : Option (Fin l.length)) : ¬ j < i → i ≠ j → intro h h' simp_all change ¬ j < i at h - change i < j + change i < j omega /-- The equivalence between `l.withUniqueDualLT` and `l.withUniqueDualGT` obtained by @@ -273,16 +271,14 @@ def withUniqueDualLTEquivGT : l.withUniqueDualLT ≃ l.withUniqueDualGT where withUniqueDualLTToWithUniqueDual]) /-- An equivalence from `l.withUniqueDualLT ⊕ l.withUniqueDualLT` to `l.withUniqueDual`. - The first `l.withUniqueDualLT` are taken to themselves, whilst the second copy are + The first `l.withUniqueDualLT` are taken to themselves, whilst the second copy are taken to their dual. -/ def withUniqueLTGTEquiv : l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUniqueDual := by - apply (Equiv.sumCongr (Equiv.refl _ ) l.withUniqueDualLTEquivGT).trans + apply (Equiv.sumCongr (Equiv.refl _) l.withUniqueDualLTEquivGT).trans apply (Equiv.Finset.union _ _ l.withUniqueDualLT_disjoint_withUniqueDualGT).trans apply (Equiv.subtypeEquivRight (by simp only [l.withUniqueDualLT_union_withUniqueDualGT, implies_true])) - - /-! ## withUniqueDualInOther equal univ @@ -292,7 +288,7 @@ def withUniqueLTGTEquiv : l.withUniqueDualLT ⊕ l.withUniqueDualLT ≃ l.withUn /-! TODO: There is probably a better place for this section. -/ lemma withUniqueDualInOther_eq_univ_fst_withDual_empty - (h : l.withUniqueDualInOther l2 = Finset.univ) : l.withDual = ∅ := by + (h : l.withUniqueDualInOther l2 = Finset.univ) : l.withDual = ∅ := by rw [@Finset.eq_empty_iff_forall_not_mem] intro x have hx : x ∈ l.withUniqueDualInOther l2 := by @@ -316,7 +312,7 @@ lemma withUniqueDualInOther_eq_univ_symm (hl : l.length = l2.length) let S' : Finset (Fin l2.length) := Finset.map ⟨Subtype.val, Subtype.val_injective⟩ (Equiv.finsetCongr - (l.getDualInOtherEquiv l2) Finset.univ ) + (l.getDualInOtherEquiv l2) Finset.univ) have hSCard : S'.card = l2.length := by rw [Finset.card_map] simp only [Finset.univ_eq_attach, Equiv.finsetCongr_apply, Finset.card_map, Finset.card_attach] @@ -325,7 +321,7 @@ lemma withUniqueDualInOther_eq_univ_symm (hl : l.length = l2.length) have hsCardUn : S'.card = (@Finset.univ (Fin l2.length)).card := by rw [hSCard] exact Eq.symm (Finset.card_fin l2.length) - have hS'Eq : S' = (l2.withUniqueDualInOther l) := by + have hS'Eq : S' = (l2.withUniqueDualInOther l) := by rw [@Finset.ext_iff] intro a simp only [S'] @@ -378,7 +374,7 @@ lemma withUniqueDualInOther_eq_univ_trans (h : l.withUniqueDualInOther l2 = Fins use (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 simp only [AreDualInOther, getDualInOther?_id] intro j hj - have hj' : j = (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by + have hj' : j = (l2.getDualInOther? l3 ((l.getDualInOther? l2 i).get hi.2.1)).get hi2.2.1 := by rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] simpa only [AreDualInOther, getDualInOther?_id] using hj rw [h'] diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean index e78a7b5..673418c 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/GetDual.lean @@ -16,13 +16,11 @@ We define the functions `getDual?` and `getDualInOther?` which return the namespace IndexNotation - namespace IndexList variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable (l l2 : IndexList X) - /-! ## The getDual? Function @@ -30,17 +28,15 @@ variable (l l2 : IndexList X) -/ /-- Given an `i`, if a dual exists in the same list, - outputs the first such dual, otherwise outputs `none`. -/ + outputs the first such dual, otherwise outputs `none`. -/ def getDual? (i : Fin l.length) : Option (Fin l.length) := Fin.find (fun j => l.AreDualInSelf i j) - /-- Given an `i`, if a dual exists in the other list, - outputs the first such dual, otherwise outputs `none`. -/ + outputs the first such dual, otherwise outputs `none`. -/ def getDualInOther? (i : Fin l.length) : Option (Fin l2.length) := Fin.find (fun j => l.AreDualInOther l2 i j) - /-! ## Basic properties of getDual? @@ -65,7 +61,7 @@ lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) : intro k' hk' by_cases hik' : i = k' · exact Fin.ge_of_eq (id (Eq.symm hik')) - · have hik'' : l.AreDualInSelf i k' := by + · have hik'' : l.AreDualInSelf i k' := by simp [AreDualInSelf, hik'] simp_all [AreDualInSelf] have hk'' := hk.2 k' hik'' @@ -86,7 +82,7 @@ lemma getDual?_of_areDualInSelf (h : l.AreDualInSelf i j) : by_cases hik' : i = k' subst hik' exact Lean.Omega.Fin.le_of_not_lt hik - have hik'' : l.AreDualInSelf i k' := by + have hik'' : l.AreDualInSelf i k' := by simp [AreDualInSelf, hik'] simp_all [AreDualInSelf] exact hk.2 k' hik'' @@ -124,7 +120,7 @@ lemma getDual?_get_areDualInSelf (i : Fin l.length) (h : (l.getDual? i).isSome) @[simp] lemma getDual?_areDualInSelf_get (i : Fin l.length) (h : (l.getDual? i).isSome) : - l.AreDualInSelf i ((l.getDual? i).get h):= + l.AreDualInSelf i ((l.getDual? i).get h) := AreDualInSelf.symm (getDual?_get_areDualInSelf l i h) @[simp] @@ -206,7 +202,7 @@ lemma getDual?_isSome_append_inl_iff (i : Fin l.length) : @[simp] lemma getDual?_isSome_append_inr_iff (i : Fin l2.length) : ((l ++ l2).getDual? (appendEquiv (Sum.inr i))).isSome ↔ - (l2.getDual? i).isSome ∨ (l2.getDualInOther? l i).isSome := by + (l2.getDual? i).isSome ∨ (l2.getDualInOther? l i).isSome := by rw [getDual?_isSome_iff_exists, getDual?_isSome_iff_exists, getDualInOther?_isSome_iff_exists] refine Iff.intro (fun h => ?_) (fun h => ?_) · obtain ⟨j, hj⟩ := h @@ -245,7 +241,7 @@ lemma getDual?_eq_none_append_inl_iff (i : Fin l.length) : exact h1 h @[simp] -lemma getDual?_eq_none_append_inr_iff (i : Fin l2.length) : +lemma getDual?_eq_none_append_inr_iff (i : Fin l2.length) : (l ++ l2).getDual? (appendEquiv (Sum.inr i)) = none ↔ (l2.getDual? i = none ∧ l2.getDualInOther? l i = none) := by apply Iff.intro @@ -290,7 +286,7 @@ lemma getDual?_append_inl_of_getDual?_isSome (i : Fin l.length) (h : (l.getDual? lemma getDual?_inl_of_getDual?_isNone_getDualInOther?_isSome (i : Fin l.length) (hi : (l.getDual? i).isNone) (h : (l.getDualInOther? l2 i).isSome) : (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some - (appendEquiv (Sum.inr ((l.getDualInOther? l2 i).get h))) := by + (appendEquiv (Sum.inr ((l.getDualInOther? l2 i).get h))) := by rw [getDual?, Fin.find_eq_some_iff, AreDualInSelf.append_inl_inr] apply And.intro (getDualInOther?_areDualInOther_get l l2 i h) intro j hj diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean index 0c57cd4..e6484e7 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/IndexString.lean @@ -268,7 +268,7 @@ noncomputable def fromIndexString (T : 𝓣.Tensor cn) (s : String) (hn : n = (toIndexList' s hs).length) (hD : (toIndexList' s hs).withDual = (toIndexList' s hs).withUniqueDual) (hC : IndexList.ColorCond (toIndexList' s hs)) - (hd : TensorColor.ColorMap.DualMap (toIndexList' s hs).colorMap + (hd : TensorColor.ColorMap.DualMap (toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) : 𝓣.TensorIndex := TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD, hC⟩ hn hd diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean index f719d99..6cac050 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/OnlyUniqueDuals.lean @@ -18,7 +18,6 @@ namespace IndexList variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable (l l2 l3 : IndexList X) - /-! ## withDual equal to withUniqueDual @@ -56,7 +55,7 @@ lemma withUnqiueDual_eq_withDual_iff : by_cases hi : i ∈ l.withDual · have hii : i ∈ l.withUniqueDual := by simp_all only - change (l.getDual? i).bind l.getDual? = _ + change (l.getDual? i).bind l.getDual? = _ simp [hii] symm rw [Option.guard_eq_some] @@ -79,8 +78,8 @@ lemma withUnqiueDual_eq_withDual_iff : rw [hi] at hj' rw [h i] at hj' have hi : Option.guard (fun i => i ∈ l.withDual) ↑i = some i := by - apply Option.guard_eq_some.mpr - simp + apply Option.guard_eq_some.mpr + simp rw [hi] at hj' simp at hj' have hj'' := Option.guard_eq_some.mp hj'.symm @@ -129,7 +128,7 @@ lemma withUnqiueDual_eq_withDual_of_empty (h : l.withDual = ∅) : intro x by_contra hx have x' : l.withDual := ⟨x, l.mem_withDual_of_withUniqueDual ⟨x, hx⟩⟩ - have hx' := x'.2 + have hx' := x'.2 simp [h] at hx' /-! @@ -140,7 +139,7 @@ lemma withUnqiueDual_eq_withDual_of_empty (h : l.withDual = ∅) : lemma withUniqueDualInOther_eq_withDualInOther_append_of_symm' (h : (l ++ l2).withUniqueDualInOther l3 = (l ++ l2).withDualInOther l3) : - (l2 ++ l).withUniqueDualInOther l3 = (l2 ++ l).withDualInOther l3 := by + (l2 ++ l).withUniqueDualInOther l3 = (l2 ++ l).withDualInOther l3 := by rw [Finset.ext_iff] at h ⊢ intro j obtain ⟨k, hk⟩ := appendEquiv.surjective j @@ -179,20 +178,18 @@ lemma withUniqueDualInOther_eq_withDualInOther_of_append_symm : exact l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l2 l3 exact l.withUniqueDualInOther_eq_withDualInOther_of_append_symm' l3 l2 - /-! ## withDual equal to withUniqueDual append conditions -/ - lemma append_withDual_eq_withUniqueDual_iff : (l ++ l2).withUniqueDual = (l ++ l2).withDual ↔ ((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2) = l.withDual ∪ l.withDualInOther l2 ∧ (l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l - = l2.withDual ∪ l2.withDualInOther l := by + = l2.withDual ∪ l2.withDualInOther l := by rw [append_withUniqueDual_disjSum, withDual_append_eq_disjSum] simp only [Equiv.finsetCongr_apply, Finset.map_inj] have h (s s' : Finset (Fin l.length)) (t t' : Finset (Fin l2.length)) : @@ -227,7 +224,7 @@ lemma append_withDual_eq_withUniqueDual_inr (h : (l ++ l2).withUniqueDual = (l + @[simp] lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl - (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : + (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : l.withUniqueDualInOther l2 = l.withDualInOther l2 := by rw [Finset.ext_iff] intro i @@ -242,7 +239,7 @@ lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl @[simp] lemma append_withDual_eq_withUniqueDual_withUniqueDualInOther_inr - (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : + (h : (l ++ l2).withUniqueDual = (l ++ l2).withDual) : l2.withUniqueDualInOther l = l2.withDualInOther l := by rw [append_withDual_eq_withUniqueDual_symm] at h exact append_withDual_eq_withUniqueDual_withUniqueDualInOther_inl l2 l h @@ -292,7 +289,6 @@ lemma append_withDual_eq_withUniqueDual_swap : rw [withUniqueDualInOther_eq_withDualInOther_of_append_symm] rw [withUniqueDualInOther_eq_withDualInOther_append_of_symm] - end IndexList end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean index 5d2aa9c..b1f44bf 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/Relations.lean @@ -18,7 +18,6 @@ a Tensor Color structure. namespace IndexNotation - namespace ColorIndexList variable {𝓒 : TensorColor} [IndexNotation 𝓒.Color] [Fintype 𝓒.Color] [DecidableEq 𝓒.Color] @@ -59,11 +58,10 @@ def ContrPerm : Prop := l'.contr.colorMap' ∘ Subtype.val ∘ (l.contr.getDualInOtherEquiv l'.contr) = l.contr.colorMap' ∘ Subtype.val -namespace ContrPerm +namespace ContrPerm variable {l l' l2 l3 : ColorIndexList 𝓒} - @[symm] lemma symm (h : ContrPerm l l') : ContrPerm l' l := by rw [ContrPerm] at h ⊢ @@ -148,7 +146,6 @@ lemma contrPermEquiv_colorMap_iso' {l l' : ColorIndexList 𝓒} (h : ContrPerm l rw [ColorMap.MapIso.symm'] exact contrPermEquiv_colorMap_iso h - @[simp] lemma contrPermEquiv_refl : contrPermEquiv (@ContrPerm.refl 𝓒 _ l) = Equiv.refl _ := by simp [contrPermEquiv, ContrPerm.refl] @@ -185,7 +182,7 @@ lemma contrPermEquiv_self_contr {l : ColorIndexList 𝓒} : symm rw [← eq_getDualInOther?_get_of_withUniqueDualInOther_iff] simp only [AreDualInOther, contr_contr_idMap, Fin.cast_trans, Fin.cast_eq_self] - have h1 : ContrPerm l l.contr := by simp + have h1 : ContrPerm l l.contr := by simp rw [h1.2.1] simp diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean index 44d1661..d91b5f7 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/TensorIndex.lean @@ -74,7 +74,6 @@ lemma ext {T₁ T₂ : 𝓣.TensorIndex} (hi : T₁.toColorIndexList = T₂.toCo subst hi simp_all - lemma index_eq_of_eq {T₁ T₂ : 𝓣.TensorIndex} (h : T₁ = T₂) : T₁.toColorIndexList = T₂.toColorIndexList := by cases h @@ -134,7 +133,7 @@ lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) : simp only [PiTensorProduct.tprodCoeff_eq_smul_tprod, LinearMapClass.map_smul, mapIso_tprod, id_eq, eq_mpr_eq_cast, OrderIso.toEquiv_symm, RelIso.coe_fn_toEquiv] apply congrArg - have hEm : IsEmpty { x // x ∈ i.withUniqueDualLT } := by + have hEm : IsEmpty { x // x ∈ i.withUniqueDualLT } := by rw [Finset.isEmpty_coe_sort] rw [Finset.eq_empty_iff_forall_not_mem] intro x hx @@ -158,7 +157,7 @@ lemma contr_of_withDual_empty (T : 𝓣.TensorIndex) (h : T.withDual = ∅) : @[simp] lemma contr_contr (T : 𝓣.TensorIndex) : T.contr.contr = T.contr := - T.contr.contr_of_withDual_empty (by simp [contr, ColorIndexList.contr]) + T.contr.contr_of_withDual_empty (by simp [contr, ColorIndexList.contr]) @[simp] lemma contr_toColorIndexList (T : 𝓣.TensorIndex) : @@ -197,8 +196,6 @@ lemma smul_contr (r : R) (T : 𝓣.TensorIndex) : (r • T).contr = r • T.cont -/ - - /-- An (equivalence) relation on two `TensorIndex`. The point in this equivalence relation is that certain things (like the permutation of indices, the contraction of indices, or rising or lowering indices) can be placed @@ -320,10 +317,8 @@ lemma rel_left {T₁ T₁' T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' lemma rel_right {T₁ T₂ T₂' : 𝓣.TensorIndex} (h : AddCond T₁ T₂) (h' : T₂ ≈ T₂') : AddCond T₁ T₂' := h.trans h'.1 - end AddCond - /-- The equivalence between indices after contraction given a `AddCond`. -/ @[simp] def addCondEquiv {T₁ T₂ : 𝓣.TensorIndex} (h : AddCond T₁ T₂) : @@ -405,7 +400,7 @@ lemma smul_add (r : R) (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : simp only [smul_index, contr_toColorIndexList, Fin.castOrderIso_refl, OrderIso.refl_toEquiv, mapIso_refl, smul_tensor, map_smul, LinearEquiv.refl_apply] -lemma add_withDual_empty (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : +lemma add_withDual_empty (T₁ T₂ : 𝓣.TensorIndex) (h : AddCond T₁ T₂) : (T₁ +[h] T₂).withDual = ∅ := by simp [contr] change T₂.toColorIndexList.contr.withDual = ∅ @@ -463,7 +458,7 @@ lemma add_rel_right {T₁ T₂ T₂' : 𝓣.TensorIndex} (h : AddCond T₁ T₂) open AddCond in lemma add_assoc' {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₂ T₃} (h : AddCond T₁ (T₂ +[h'] T₃)) : T₁ +[h] (T₂ +[h'] T₃) = T₁ +[h'.of_add_right h] T₂ +[h'.add_left_of_add_right h] T₃ := by - refine ext ?_ ?_ + refine ext ?_ ?_ simp only [add_toColorIndexList, ColorIndexList.contr_contr] simp only [add_toColorIndexList, add_tensor, contr_toColorIndexList, addCondEquiv, contr_add_tensor, map_add, mapIso_mapIso] @@ -486,7 +481,6 @@ lemma add_assoc {T₁ T₂ T₃ : 𝓣.TensorIndex} {h' : AddCond T₁ T₂} (h -/ - /-- The condition on two `TensorIndex` which is true if and only if their `ColorIndexList`s are related by the condition `AppendCond`. That is, they can be appended to form a `ColorIndexList`. -/ @@ -515,7 +509,6 @@ lemma prod_toColorIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T lemma prod_toIndexList (T₁ T₂ : 𝓣.TensorIndex) (h : ProdCond T₁ T₂) : (prod T₁ T₂ h).toIndexList = T₁.toIndexList ++ T₂.toIndexList := rfl - end TensorIndex end end TensorStructure diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithDual.lean index a6355d2..1e8433f 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithDual.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithDual.lean @@ -13,10 +13,8 @@ We define the finite sets of indices in an index list which have a dual -/ - namespace IndexNotation - namespace IndexList variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] @@ -65,7 +63,6 @@ lemma mem_withDual_iff_exists : i ∈ l.withDual ↔ ∃ j, l.AreDualInSelf i j -/ - @[simp] lemma mem_withInDualOther_iff_isSome (i : Fin l.length) : i ∈ l.withDualInOther l2 ↔ (l.getDualInOther? l2 i).isSome := by @@ -114,7 +111,6 @@ lemma append_withDualInOther_eq : | Sum.inr k => simp - lemma withDualInOther_append_eq : l.withDualInOther (l2 ++ l3) = l.withDualInOther l2 ∪ l.withDualInOther l3 := by ext i diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean index 8b8148d..7f581d5 100644 --- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean +++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean @@ -15,13 +15,11 @@ Finite sets of indices with a unique dual. namespace IndexNotation - namespace IndexList variable {X : Type} [IndexNotation X] [Fintype X] [DecidableEq X] variable (l l2 l3 : IndexList X) - /-! ## Unique duals @@ -37,7 +35,7 @@ def withUniqueDual : Finset (Fin l.length) := list. -/ def withUniqueDualInOther : Finset (Fin l.length) := Finset.filter (fun i => i ∉ l.withDual ∧ i ∈ l.withDualInOther l2 - ∧ (∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther? l2 i)) Finset.univ + ∧ (∀ j, l.AreDualInOther l2 i j → j = l.getDualInOther? l2 i)) Finset.univ /-! @@ -61,8 +59,6 @@ lemma mem_withDual_of_withUniqueDual (i : l.withUniqueDual) : i.1 ∈ l.withDual := mem_withDual_of_mem_withUniqueDual l (↑i) i.2 - - /-! ## Basic properties of withUniqueDualInOther @@ -128,7 +124,7 @@ lemma getDual?_get_getDual?_get_of_withUniqueDual (i : Fin l.length) (h : i ∈ (l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h))).get (l.getDual?_getDual?_get_isSome i (mem_withUniqueDual_isSome l i h)) = i := by by_contra hn - have h' : l.AreDualInSelf i ((l.getDual? ((l.getDual? i).get + have h' : l.AreDualInSelf i ((l.getDual? ((l.getDual? i).get (mem_withUniqueDual_isSome l i h))).get ( getDual?_getDual?_get_isSome l i (mem_withUniqueDual_isSome l i h))) := by simp [AreDualInSelf, hn] @@ -168,7 +164,6 @@ lemma getDual?_get_of_mem_withUnique_mem (i : Fin l.length) (h : i ∈ l.withUni subst h1 exact Eq.symm (getDual?_getDual?_get_of_withUniqueDual l i h) - /-! ## Properties of getDualInOther? and withUniqueDualInOther @@ -188,7 +183,7 @@ lemma some_eq_getDualInOther?_of_withUniqueDualInOther_iff (i : Fin l.length) (j exact fun h' => l.all_dual_eq_of_withUniqueDualInOther l2 i h j h' intro 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'))) + Eq.symm (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h'))) subst hj exact getDualInOther?_areDualInOther_get l l2 i (mem_withUniqueDualInOther_isSome l l2 i h) @@ -210,10 +205,10 @@ lemma getDualInOther?_get_getDualInOther?_get_of_withUniqueDualInOther (l.getDualInOther?_getDualInOther?_get_isSome l2 i (mem_withUniqueDualInOther_isSome l l2 i h)) = i := by by_contra hn - have h' : l.AreDualInSelf i ((l2.getDualInOther? l ((l.getDualInOther? l2 i).get + have h' : l.AreDualInSelf i ((l2.getDualInOther? l ((l.getDualInOther? l2 i).get (mem_withUniqueDualInOther_isSome l l2 i h))).get (l.getDualInOther?_getDualInOther?_get_isSome l2 i - (mem_withUniqueDualInOther_isSome l l2 i h))):= by + (mem_withUniqueDualInOther_isSome l l2 i h))) := by simp [AreDualInSelf, hn] exact fun a => hn (id (Eq.symm a)) have h1 := l.not_mem_withDual_of_withUniqueDualInOther l2 ⟨i, h⟩ @@ -285,17 +280,12 @@ lemma getDualInOther?_get_of_mem_withUniqueInOther_mem (i : Fin l.length) rw [Fin.find_eq_none_iff] at h simp_all only - - @[simp] lemma getDualInOther?_self_of_mem_withUniqueInOther (i : Fin l.length) (h : i ∈ l.withUniqueDualInOther l) : l.getDualInOther? l i = some i := by rw [all_dual_eq_of_withUniqueDualInOther l l i h i rfl] - - - /-! ## Properties of getDual?, withUniqueDual and append @@ -319,7 +309,6 @@ lemma append_inl_not_mem_withDual_of_withDualInOther (i : Fin l.length) simp only [getDual?_isSome_append_inl_iff] at ht simp_all - lemma append_inr_not_mem_withDual_of_withDualInOther (i : Fin l2.length) (h : appendEquiv (Sum.inr i) ∈ (l ++ l2).withUniqueDual) : i ∈ l2.withDual ↔ ¬ i ∈ l2.withDualInOther l := by @@ -337,7 +326,6 @@ lemma append_inr_not_mem_withDual_of_withDualInOther (i : Fin l2.length) simp only [getDual?_isSome_append_inr_iff] at ht simp_all - lemma getDual?_append_symm_of_withUniqueDual_of_inl (i : Fin l.length) (k : Fin l2.length) (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) : (l ++ l2).getDual? (appendEquiv (Sum.inl i)) = some (appendEquiv (Sum.inr k)) @@ -394,10 +382,10 @@ lemma mem_withUniqueDual_append_symm (i : Fin l.length) : implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, getDual?_areDualInSelf_get] | Sum.inr k => - have hk' := h' (appendEquiv (Sum.inl k)) + have hk' := h' (appendEquiv (Sum.inl k)) simp only [AreDualInSelf.append_inl_inl] at hk' simp only [AreDualInSelf.append_inr_inr] at hj - refine ((l.getDual?_append_symm_of_withUniqueDual_of_inl' l2 _ _ ?_).mp (hk' hj).symm).symm + refine ((l.getDual?_append_symm_of_withUniqueDual_of_inl' l2 _ _ ?_).mp (hk' hj).symm).symm simp_all only [AreDualInSelf.append_inl_inl, imp_self, withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inl_iff, implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, @@ -415,30 +403,30 @@ lemma mem_withUniqueDual_append_symm (i : Fin l.length) : implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, getDual?_areDualInSelf_get] | Sum.inr k => - have hk' := h' (appendEquiv (Sum.inl k)) + have hk' := h' (appendEquiv (Sum.inl k)) simp only [AreDualInSelf.append_inr_inl] at hk' simp only [AreDualInSelf.append_inl_inr] at hj - refine ((l2.getDual?_append_symm_of_withUniqueDual_of_inr l _ _ ?_).mp (hk' hj).symm).symm + refine ((l2.getDual?_append_symm_of_withUniqueDual_of_inr l _ _ ?_).mp (hk' hj).symm).symm simp_all only [AreDualInSelf.append_inr_inl, imp_self, withUniqueDual, mem_withDual_iff_isSome, Finset.mem_filter, Finset.mem_univ, getDual?_isSome_append_inr_iff, implies_true, and_self, mem_withUniqueDual_isSome, eq_getDual?_get_of_withUniqueDual_iff, getDual?_areDualInSelf_get] @[simp] -lemma not_mem_withDualInOther_of_inl_mem_withUniqueDual (i : Fin l.length) +lemma not_mem_withDualInOther_of_inl_mem_withUniqueDual (i : Fin l.length) (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hs : i ∈ l.withUniqueDual) : ¬ i ∈ l.withUniqueDualInOther l2 := by have hn := l.append_inl_not_mem_withDual_of_withDualInOther l2 i h simp_all by_contra ho - have ho' : (l.getDualInOther? l2 i).isSome := by + have ho' : (l.getDualInOther? l2 i).isSome := by exact mem_withUniqueDualInOther_isSome l l2 i ho simp_all [Option.isSome_none, Bool.false_eq_true] @[simp] lemma not_mem_withUniqueDual_of_inl_mem_withUnqieuDual (i : Fin l.length) (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hi : i ∈ l.withUniqueDualInOther l2) : - ¬ i ∈ l.withUniqueDual := by + ¬ i ∈ l.withUniqueDual := by by_contra hs simp_all only [not_mem_withDualInOther_of_inl_mem_withUniqueDual] @@ -457,7 +445,7 @@ lemma mem_withUniqueDual_of_inl (i : Fin l.length) simp_all @[simp] -lemma mem_withUniqueDualInOther_of_inl_withDualInOther (i : Fin l.length) +lemma mem_withUniqueDualInOther_of_inl_withDualInOther (i : Fin l.length) (h : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDual) (hi : (l.getDualInOther? l2 i).isSome) : i ∈ l.withUniqueDualInOther l2 := by simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome, @@ -644,7 +632,7 @@ lemma append_withUniqueDual : (l ++ l2).withUniqueDual = lemma append_withUniqueDual_disjSum : (l ++ l2).withUniqueDual = Equiv.finsetCongr appendEquiv (((l.withUniqueDual ∩ (l.withDualInOther l2)ᶜ) ∪ l.withUniqueDualInOther l2).disjSum - ((l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l)) := by + ((l2.withUniqueDual ∩ (l2.withDualInOther l)ᶜ) ∪ l2.withUniqueDualInOther l)) := by rw [← Equiv.symm_apply_eq] simp only [Equiv.finsetCongr_symm, append_withUniqueDual, Equiv.finsetCongr_apply] rw [Finset.map_union] @@ -660,8 +648,6 @@ lemma append_withUniqueDual_disjSum : (l ++ l2).withUniqueDual = -/ - - lemma mem_append_withUniqueDualInOther_symm (i : Fin l.length) : appendEquiv (Sum.inl i) ∈ (l ++ l2).withUniqueDualInOther l3 ↔ appendEquiv (Sum.inr i) ∈ (l2 ++ l).withUniqueDualInOther l3 := by @@ -729,24 +715,23 @@ lemma withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd (i : Fin l.leng lemma getDualInOther?_append_symm_of_withUniqueDual_of_inl (i : Fin l.length) (k : Fin l2.length) (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) : l.getDualInOther? (l2 ++ l3) i = some (appendEquiv (Sum.inl k)) - ↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inr k)) := by + ↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inr k)) := by have h := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h by_cases hs : (l.getDualInOther? l2 i).isSome - <;> by_cases ho : (l.getDualInOther? l3 i).isSome + <;> by_cases ho : (l.getDualInOther? l3 i).isSome <;> simp_all [hs] lemma getDualInOther?_append_symm_of_withUniqueDual_of_inr (i : Fin l.length) (k : Fin l3.length) (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) : l.getDualInOther? (l2 ++ l3) i = some (appendEquiv (Sum.inr k)) - ↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inl k)) := by + ↔ l.getDualInOther? (l3 ++ l2) i = some (appendEquiv (Sum.inl k)) := by have h := l.withUniqueDualInOther_append_isSome_fst_iff_not_isSome_snd l2 l3 i h by_cases hs : (l.getDualInOther? l2 i).isSome - <;> by_cases ho : (l.getDualInOther? l3 i).isSome + <;> by_cases ho : (l.getDualInOther? l3 i).isSome <;> simp_all [hs] - lemma mem_withUniqueDualInOther_symm' (i : Fin l.length) - (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)): + (h : i ∈ l.withUniqueDualInOther (l2 ++ l3)) : i ∈ l.withUniqueDualInOther (l3 ++ l2) := by have h' := h simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, @@ -759,7 +744,7 @@ lemma mem_withUniqueDualInOther_symm' (i : Fin l.length) by_cases h1 : (l.getDualInOther? l2 i).isSome <;> by_cases h2 : (l.getDualInOther? l3 i).isSome · simp only [h1, h2, not_true_eq_false, imp_false] at hc - rw [← @Option.not_isSome_iff_eq_none] at hc + rw [← @Option.not_isSome_iff_eq_none] at hc simp [h2] at hc · simp only [h1, or_true, true_and] intro j @@ -803,7 +788,6 @@ lemma mem_withUniqueDualInOther_symm (i : Fin l.length) : i ∈ l.withUniqueDualInOther (l2 ++ l3) ↔ i ∈ l.withUniqueDualInOther (l3 ++ l2) := Iff.intro (l.mem_withUniqueDualInOther_symm' l2 l3 i) (l.mem_withUniqueDualInOther_symm' l3 l2 i) - /-! ## The equivalence defined by getDual? @@ -847,7 +831,6 @@ lemma getDualInOtherEquiv_self_refl : l.getDualInOtherEquiv l = Equiv.refl _ := intro x simp [getDualInOtherEquiv] - end IndexList end IndexNotation diff --git a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean index 513ea0f..b83034d 100644 --- a/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean +++ b/HepLean/SpaceTime/LorentzTensor/Real/IndexNotation.lean @@ -85,11 +85,10 @@ noncomputable def fromIndexStringColor {cn : Fin n → realTensorColor.Color} (hd : TensorColor.ColorMap.DualMap.boolFin (toIndexList' s hs).colorMap (cn ∘ Fin.cast hn.symm)) : (realLorentzTensor d).TensorIndex := - TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD, + TensorStructure.TensorIndex.mkDualMap T ⟨(toIndexList' s hs), hD, IndexList.ColorCond.iff_bool.mpr hC⟩ hn (TensorColor.ColorMap.DualMap.boolFin_DualMap hd) - /-- A tactic used to prove `boolFin` for real Lornetz tensors. -/ macro "dualMapTactic" : tactic => `(tactic| { @@ -114,10 +113,9 @@ macro "prodTactic" : tactic => /-- The product of Real Lorentz tensors. Conditions on indices are checked automatically. -/ notation:10 T "⊗ᵀ" S:11 => TensorIndex.prod T S (by prodTactic) - /-- An example showing the allowed constructions. -/ example (T : (realLorentzTensor d).Tensor ![ColorType.up, ColorType.down]) : True := by - let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ⁴ᵤ₃" + let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ⁴ᵤ₃" let _ := T|"ᵤ₁ᵤ₂" ⊗ᵀ T|"ᵘ³ᵤ₄" ⊗ᵀ T|"ᵘ¹ᵘ²" ⊗ᵀ T|"ᵘ⁴ᵤ₃" exact trivial