Merge pull request #382 from HEPLean/Web

feat: Fix free_simps

PhysLean/Relativity/Lorentz/Group/Basic.lean

@@ -126,19 +126,9 @@ instance (M : LorentzGroup d) : Invertible M.1 where
     rw [← coe_inv]
     exact (mem_iff_self_mul_dual.mp M.2)
 
-lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := by
-  trans Subtype.val (Λ⁻¹ * Λ)
-  · rw [← coe_inv]
-    rfl
-  · rw [inv_mul_cancel Λ]
-    rfl
+lemma subtype_inv_mul : (Subtype.val Λ)⁻¹ * (Subtype.val Λ) = 1 := inv_mul_of_invertible _
 
-lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := by
-  trans Subtype.val (Λ * Λ⁻¹)
-  · rw [← coe_inv]
-    rfl
-  · rw [mul_inv_cancel Λ]
-    rfl
+lemma subtype_mul_inv : (Subtype.val Λ) * (Subtype.val Λ)⁻¹ = 1 := mul_inv_of_invertible _
 
 @[simp]
 lemma mul_minkowskiMatrix_mul_transpose :
@@ -180,12 +170,7 @@ lemma transpose_inv : (transpose Λ)⁻¹ = transpose Λ⁻¹ := by
 lemma comm_minkowskiMatrix : Λ.1 * minkowskiMatrix = minkowskiMatrix * (transpose Λ⁻¹).1 := by
   conv_rhs => rw [← @mul_minkowskiMatrix_mul_transpose d Λ]
   rw [← transpose_inv, coe_inv, transpose_val]
-  rw [mul_assoc]
-  have h1 : ((Λ.1)ᵀ * (Λ.1)ᵀ⁻¹) = 1 := by
-    rw [← transpose_val]
-    simp only [subtype_mul_inv]
-  rw [h1]
-  simp
+  exact Eq.symm (mul_inv_cancel_right_of_invertible _ _)
 
 lemma minkowskiMatrix_comm : minkowskiMatrix * Λ.1 = (transpose Λ⁻¹).1 * minkowskiMatrix := by
   conv_rhs => rw [← @transpose_mul_minkowskiMatrix_mul_self d Λ]

PhysLean/Relativity/Tensors/OverColor/Iso.lean

@@ -123,18 +123,10 @@ def fin2Iso {c : Fin 2 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1] := by
 
 /-- The isomorphism splitting a `mk c` for `c : Fin 3 → C` into the tensor product of
   a `Fin 1 → C` map `![c 0]` and a `Fin 2 → C` map `![c 1, c 2]`. -/
-def fin3Iso {c : Fin 3 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1, c 2] := by
-  let e1 : Fin 3 ≃ Fin 1 ⊕ Fin 2 := (finSumFinEquiv (n := 2)).symm
-  apply (equivToIso e1).trans
-  apply (mkSum _).trans
-  refine tensorIso (mkIso ?_) (mkIso ?_)
-  · funext x
-    fin_cases x
-    rfl
-  · funext x
-    fin_cases x
-    rfl
-    rfl
+def fin3Iso {c : Fin 3 → C} : mk c ≅ mk ![c 0] ⊗ mk ![c 1, c 2] :=
+  (equivToIso (finSumFinEquiv (n := 2)).symm).trans <|
+  (mkSum _).trans <|
+  tensorIso (mkIso (List.ofFn_inj.mp rfl)) (mkIso (List.ofFn_inj.mp rfl))
 
 /-- The isomorphism splitting a `mk ![c1, c2, c3]` into the tensor product of
   a `Fin 1 → C` map `fun _ => c1` and a `Fin 2 → C` map `![c 1, c 2]`. -/

PhysLean/Relativity/Tensors/OverColor/Lift.lean

@@ -261,21 +261,8 @@ lemma μ_tmul_tprod_mk {X Y : Type} {cX : X → C} {cY : Y → C}
     (μ F (OverColor.mk cX) (OverColor.mk cY)).hom.hom
     (PiTensorProduct.tprod k p ⊗ₜ[k] PiTensorProduct.tprod k q)
     = (PiTensorProduct.tprod k) fun i =>
-    discreteSumEquiv' F i (PhysLean.PiTensorProduct.elimPureTensor p q i) := by
-  let q' : (i : (OverColor.mk cY).left) → (F.obj <| Discrete.mk ((OverColor.mk cY).hom i)) := q
-  let p' : (i : (OverColor.mk cX).left) → (F.obj <| Discrete.mk ((OverColor.mk cX).hom i)) := p
-  have h1 := μModEquiv_tmul_tprod F p' q'
-  simp only [Action.instMonoidalCategory_tensorObj_V, Equivalence.symm_inverse,
-    Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
-    objObj'_V_carrier, mk_hom, Functor.id_obj, instMonoidalCategoryStruct_tensorObj_hom] at h1
-  erw [h1]
-  simp only [objObj'_V_carrier, instMonoidalCategoryStruct_tensorObj_left,
-    instMonoidalCategoryStruct_tensorObj_hom, mk_hom, p', q']
-  apply congrArg
-  funext i
-  match i with
-  | Sum.inl i => rfl
-  | Sum.inr i => rfl
+    discreteSumEquiv' F i (PhysLean.PiTensorProduct.elimPureTensor p q i) :=
+  μModEquiv_tmul_tprod F _ _
 
 lemma μ_natural_left {X Y : OverColor C} (f : X ⟶ Y) (Z : OverColor C) :
     MonoidalCategory.whiskerRight (objMap' F f) (objObj' F Z) ≫ (μ F Y Z).hom =

PhysLean/Relativity/Tensors/Tree/Basic.lean

@@ -493,14 +493,8 @@ lemma perm_tensorBasis_repr_apply {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m
     simp only [OverColor.mk_hom, Basis.repr_self, pb]
     rw [Finsupp.single_apply, Finsupp.single_apply]
     congr 1
-    simp only [eq_iff_iff, pb]
-    apply Iff.intro
-    · intro h
-      rw [← h]
-      simp only [Equiv.apply_symm_apply, pb]
-    · intro h
-      rw [h]
-      simp
+    exact eq_iff_iff.mpr <| Equiv.symm_apply_eq
+      (TensorBasis.congr (OverColor.Hom.toEquiv σ) (OverColor.Hom.toEquiv_comp_apply σ))
   · simp only [OverColor.mk_hom, map_zero, Finsupp.coe_zero, Pi.zero_apply, pb]
   · intro x y hx hy
     simp_all [pb]

PhysLean/Relativity/Tensors/Tree/NodeIdentities/Basic.lean

@@ -334,9 +334,7 @@ lemma perm_action {n m : ℕ} {c : Fin n → S.C} {c1 : Fin m → S.C}
     (σ : (OverColor.mk c) ⟶ (OverColor.mk c1)) (g : S.G) (t : TensorTree S c) :
     (perm σ (action g t)).tensor = (action g (perm σ t)).tensor := by
   simp only [perm_tensor, action_tensor]
-  change (ModuleCat.ofHom ((S.F.obj (OverColor.mk c)).ρ g) ≫ (S.F.map σ).hom) t.tensor = _
-  erw [(S.F.map σ).comm g]
-  rfl
+  exact Rep.hom_comm_apply (S.F.map σ) g t.tensor
 
 /-- An `action` node can be moved through a `neg` node. -/
 lemma neg_action {n : ℕ} {c : Fin n → S.C} (g : S.G) (t : TensorTree S c) :

scripts/MetaPrograms/free_simps.lean

@@ -64,7 +64,7 @@ unsafe def processAllFiles : IO Unit := do
   let tasks := files.map fun f =>
     ((IO.asTask $ IO.Process.run
     {cmd := "lake", args := #["exe", "free_simps", f.toString]}), f)
-  tasks.toList.enum.forM fun (n, (t, path)) => do
+  tasks.toList.zipIdx.forM fun ((t, path), n) => do
     let tn ← IO.wait (← t)
     match tn with
     | .ok x =>
@@ -87,7 +87,7 @@ unsafe def processFileArray (files : Array FilePath) : IO Unit := do
   let tasks := files.map fun f =>
     ((IO.asTask $ IO.Process.run
     {cmd := "lake", args := #["exe", "free_simps","-file", f.toString]}), f)
-  tasks.toList.enum.forM fun (n, (t, path)) => do
+  tasks.toList.zipIdx.forM fun ((t, path), n) => do
     let tn ← IO.wait (← t)
     match tn with
     | .ok x =>