refactor: Some golfing

HepLean/AnomalyCancellation/SMNu/PlusU1/BMinusL.lean

@@ -67,7 +67,7 @@ lemma on_quadBiLin (S : (PlusU1 n).Charges) :
 
 lemma on_quadBiLin_AFL (S : (PlusU1 n).LinSols) : quadBiLin (BL n).val S.val = 0 := by
   rw [on_quadBiLin, YYsol S, SU2Sol S, SU3Sol S]
-  simp
+  rfl
 
 lemma add_AFL_quad (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accQuad (a • S.val + b • (BL n).val) = a ^ 2 * accQuad S.val := by
@@ -100,7 +100,7 @@ lemma on_cubeTriLin (S : (PlusU1 n).Charges) :
 lemma on_cubeTriLin_AFL (S : (PlusU1 n).LinSols) :
     cubeTriLin (BL n).val (BL n).val S.val = 0 := by
   rw [on_cubeTriLin, gravSol S, SU3Sol S]
-  simp
+  rfl
 
 lemma add_AFL_cube (S : (PlusU1 n).LinSols) (a b : ℚ) :
     accCube (a • S.val + b • (BL n).val) =

HepLean/Mathematics/Fin.lean

@@ -237,10 +237,6 @@ lemma finExtractOne_symm_inr_apply {n : ℕ} (i : Fin n.succ) (x : Fin n) :
 @[simp]
 lemma finExtractOne_symm_inl_apply {n : ℕ} (i : Fin n.succ) :
     (finExtractOne i).symm (Sum.inl 0) = i := by
-  simp only [Nat.succ_eq_add_one, finExtractOne, Fin.isValue, Equiv.symm_trans_apply, finCongr_symm,
-    Equiv.symm_symm, Equiv.sumCongr_symm, Equiv.refl_symm, Equiv.sumCongr_apply, Equiv.coe_refl,
-    Sum.map_inl, id_eq, Equiv.sumAssoc_symm_apply_inl, Equiv.sumComm_symm, Equiv.sumComm_apply,
-    Sum.swap_inl, finSumFinEquiv_apply_right, finSumFinEquiv_apply_left, finCongr_apply]
   rfl
 
 /-- Given an equivalence `Fin n.succ.succ ≃ Fin n.succ.succ`, and an `i : Fin n.succ.succ`,

HepLean/Mathematics/PiTensorProduct.lean

@@ -269,7 +269,6 @@ lemma elimPureTensor_update_right (p : (i : ι1) → s1 i) (q : (i : ι2) → s2
   funext x
   match x with
   | Sum.inl x =>
-    simp only [Sum.elim_inl, ne_eq, reduceCtorEq, not_false_eq_true, Function.update_noteq]
     rfl
   | Sum.inr x =>
     change Function.update q y r x = _
@@ -277,7 +276,7 @@ lemma elimPureTensor_update_right (p : (i : ι1) → s1 i) (q : (i : ι2) → s2
     split_ifs
     · rename_i h
       subst h
-      simp_all only
+      rfl
     · rfl
 
 @[simp]
@@ -295,7 +294,6 @@ lemma elimPureTensor_update_left (p : (i : ι1) → s1 i) (q : (i : ι2) → s2
       rfl
     · rfl
   | Sum.inr y =>
-    simp only [Sum.elim_inr, ne_eq, reduceCtorEq, not_false_eq_true, Function.update_noteq]
     rfl
 
 end

HepLean/Tensors/OverColor/Basic.lean

@@ -152,8 +152,7 @@ instance (C : Type) : MonoidalCategoryStruct (OverColor C) where
       simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
       rfl,
     inv_hom_id := by
-      apply CategoryTheory.Iso.ext
-      erw [CategoryTheory.Iso.trans_hom]}
+      rfl}
   rightUnitor X := {
     hom := Over.isoMk (Equiv.sumEmpty X.left Empty).toIso
     inv := (Over.isoMk (Equiv.sumEmpty X.left Empty).toIso).symm
@@ -163,8 +162,7 @@ instance (C : Type) : MonoidalCategoryStruct (OverColor C) where
       simp only [Functor.id_obj, Over.mk_left, Over.mk_hom, Iso.symm_hom, Iso.hom_inv_id]
       rfl,
     inv_hom_id := by
-      apply CategoryTheory.Iso.ext
-      erw [CategoryTheory.Iso.trans_hom]}
+      rfl}
 
 instance (C : Type) : MonoidalCategory (OverColor C) where
     tensorHom_def f g := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => rfl

HepLean/Tensors/OverColor/Functors.lean

@@ -27,13 +27,9 @@ def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D)
     | Sum.inl x => rfl
     | Sum.inr x => rfl)
   μ_natural_left X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl x => rfl
-    | Sum.inr x => rfl
+    rfl
   μ_natural_right X Y := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
-    match x with
-    | Sum.inl x => rfl
-    | Sum.inr x => rfl
+    rfl
   associativity X Y Z := CategoryTheory.Iso.ext <| Over.OverMorphism.ext <| funext fun x => by
     match x with
     | Sum.inl (Sum.inl x) => rfl
@@ -51,9 +47,7 @@ def map {C D : Type} (f : C → D) : MonoidalFunctor (OverColor C) (OverColor D)
 /-- The tensor product on `OverColor C` as a monoidal functor. -/
 def tensor (C : Type) : MonoidalFunctor (OverColor C × OverColor C) (OverColor C) where
   toFunctor := MonoidalCategory.tensor (OverColor C)
-  ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso (by
-    ext x
-    exact Empty.elim x)
+  ε := Over.isoMk (Equiv.sumEmpty Empty Empty).symm.toIso rfl
   μ X Y := Over.isoMk (Equiv.sumSumSumComm X.1.left X.2.left Y.1.left Y.2.left).toIso (by
     ext x
     match x with

HepLean/Tensors/Tree/Basic.lean

@@ -180,14 +180,14 @@ lemma contrFin1Fin1_hom_hom_tprod {n : ℕ} (c : Fin n.succ.succ → S.C)
   change ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).hom _ = _
   trans ((Action.forget _ _).mapIso (S.contrFin1Fin1 c i j h)).toLinearEquiv
     (PiTensorProduct.tprod S.k x)
-  · congr
+  · rfl
   erw [← LinearEquiv.eq_symm_apply]
   erw [contrFin1Fin1_inv_tmul]
   congr
   funext i
   match i with
   | Sum.inl 0 =>
-    simp
+    rfl
   | Sum.inr 0 =>
     simp only [Nat.succ_eq_add_one, Fin.isValue, mk_hom, Function.comp_apply,
       Discrete.functor_obj_eq_as]
@@ -217,9 +217,7 @@ lemma contrIso_hom_hom {n : ℕ} {c1 : Fin n.succ.succ → S.C}
     (OverColor.mk ((c1 ∘ ⇑(HepLean.Fin.finExtractTwo i j).symm) ∘ Sum.inr))).inv.hom ≫
     ((S.contrFin1Fin1 c1 i j h).hom.hom ⊗
     (S.F.map (mkIso (contrIso.proof_1 S c1 i j)).hom).hom) := by
-  rw [contrIso]
-  simp [Nat.succ_eq_add_one, Action.instMonoidalCategory_tensorObj_V, Action.comp_hom,
-    extractOne_homToEquiv, Action.instMonoidalCategory_tensorHom_hom]
+  rfl
 
 /-- `contrMap` is a function that takes a natural number `n`, a function `c` from
 `Fin n.succ.succ` to `S.C`, an index `i` of type `Fin n.succ.succ`, an index `j` of type

HepLean/Tensors/Tree/NodeIdentities/PermContr.lean

@@ -146,7 +146,6 @@ lemma contrIso_comm_aux_3 {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
       ((HepLean.Fin.finExtractOnePerm ((Hom.toEquiv σ).symm i) (Hom.toEquiv σ)).symm j))).hom) ≫
       (S.F.map (extractTwo i j σ)) := by
     rw [← Functor.map_comp, ← Functor.map_comp]
-    apply congrArg
     rfl
   exact congrArg (λ f => Action.Hom.hom f) h1
 
@@ -234,8 +233,7 @@ lemma contrMap_naturality {n : ℕ} {c c1 : Fin n.succ.succ → S.C}
   erw [CategoryTheory.Category.id_comp, CategoryTheory.Category.comp_id]
   erw [CategoryTheory.Category.comp_id]
   rw [S.contr.naturality]
-  simp only [Nat.succ_eq_add_one, extractOne_homToEquiv, Monoidal.tensorUnit_obj,
-    Monoidal.tensorUnit_map, Category.comp_id]
+  rfl
 
 end
 end TensorStruct