refactor: simp golfing

HepLean/AnomalyCancellation/Basic.lean

@@ -200,7 +200,7 @@ def IsSolution (χ : ACCSystem) (S : χ.Charges) : Prop :=
 instance solsMulAction (χ : ACCSystem) : MulAction ℚ χ.Sols where
   smul a S := ⟨a • S.toQuadSols, by
     erw [(χ.cubicACC).map_smul, S.cubicSol]
-    simp⟩
+    exact Rat.mul_zero (a ^ 3)⟩
   mul_smul a b S := Sols.ext (mul_smul _ _ _)
   one_smul S := Sols.ext (one_smul _ _)
 

HepLean/AnomalyCancellation/PureU1/Even/BasisLinear.lean

@@ -566,9 +566,10 @@ theorem basis_linear_independent : LinearIndependent ℚ (@basis n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change P' f = 0 at h
-  have h1 : (P' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (P' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [P'_val] at h1
   exact P_zero f h1
 
@@ -576,9 +577,10 @@ theorem basis!_linear_independent : LinearIndependent ℚ (@basis! n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change P!' f = 0 at h
-  have h1 : (P!' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (P!' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [P!'_val] at h1
   exact P!_zero f h1
 
@@ -586,9 +588,10 @@ theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n) := by
   apply Fintype.linearIndependent_iff.mpr
   intro f h
   change Pa' f = 0 at h
-  have h1 : (Pa' f).val = 0 := by
-    simp [h]
-    rfl
+  have h1 : (Pa' f).val = 0 :=
+    (AddSemiconjBy.eq_zero_iff (ACCSystemLinear.LinSols.val 0)
+    (congrFun (congrArg HAdd.hAdd (congrArg ACCSystemLinear.LinSols.val (id (Eq.symm h))))
+    (ACCSystemLinear.LinSols.val 0))).mp rfl
   rw [Pa'_P'_P!'] at h1
   change (P' (f ∘ Sum.inl)).val + (P!' (f ∘ Sum.inr)).val = 0 at h1
   rw [P!'_val, P'_val] at h1
@@ -728,7 +731,6 @@ lemma vectorLikeEven_in_span (S : (PureU1 (2 * n.succ)).LinSols)
       rw [ht]
       ring
     rw [h]
-    simp
     rfl
 
 end VectorLikeEvenPlane

HepLean/AnomalyCancellation/PureU1/Permutations.lean

@@ -37,13 +37,8 @@ section Charges
 def chargeMap {n : ℕ} (f : PermGroup n) :
     (PureU1 n).Charges →ₗ[ℚ] (PureU1 n).Charges where
   toFun S := S ∘ f.toFun
-  map_add' S T := by
-    funext i
-    simp
-  map_smul' a S := by
-    funext i
-    simp [HSMul.hSMul]
-    -- rw [show Rat.cast a = a from rfl]
+  map_add' _ _ := rfl
+  map_smul' _ _:= rfl
 
 open PureU1Charges in
 
@@ -51,17 +46,8 @@ open PureU1Charges in
 @[simp]
 def permCharges {n : ℕ} : Representation ℚ (PermGroup n) (PureU1 n).Charges where
   toFun f := chargeMap f⁻¹
-  map_mul' f g := by
-    simp only [PermGroup, mul_inv_rev]
-    apply LinearMap.ext
-    intro S
-    funext i
-    rfl
-  map_one' := by
-    apply LinearMap.ext
-    intro S
-    funext i
-    rfl
+  map_mul' f g := by rfl
+  map_one' := by rfl
 
 lemma accGrav_invariant {n : ℕ} (f : (PermGroup n)) (S : (PureU1 n).Charges) :
     PureU1.accGrav n (permCharges f S) = accGrav n S := by

HepLean/AnomalyCancellation/SM/FamilyMaps.lean

@@ -42,12 +42,8 @@ def chargesMapOfSpeciesMap {n m : ℕ} (f : (SMSpecies n).Charges →ₗ[ℚ] (S
 def speciesFamilyProj {m n : ℕ} (h : n ≤ m) :
     (SMSpecies m).Charges →ₗ[ℚ] (SMSpecies n).Charges where
   toFun S := S ∘ Fin.castLE h
-  map_add' S T := by
-    funext i
-    simp
-  map_smul' a S := by
-    funext i
-    simp [HSMul.hSMul]
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
     --rw [show Rat.cast a = a from rfl]
 
 /-- The projection of the `m`-family charges onto the first `n`-family charges. -/
@@ -77,7 +73,7 @@ def speciesEmbed (m n : ℕ) :
     by_cases hi : i.val < m
     · erw [dif_pos hi, dif_pos hi]
     · erw [dif_neg hi, dif_neg hi]
-      simp
+      exact Eq.symm (Rat.mul_zero a)
 
 /-- The embedding of the `m`-family charges onto the `n`-family charges, with all
 other charges zero. -/
@@ -89,14 +85,9 @@ a universal manor. -/
 @[simps!]
 def speciesFamilyUniversial (n : ℕ) :
     (SMSpecies 1).Charges →ₗ[ℚ] (SMSpecies n).Charges where
-  toFun S _ := S ⟨0, by simp⟩
-  map_add' S T := by
-    funext _
-    simp
-  map_smul' a S := by
-    funext i
-    simp [HSMul.hSMul]
-    --rw [show Rat.cast a = a from rfl]
+  toFun S _ := S ⟨0, Nat.zero_lt_succ 0⟩
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
 
 /-- The embedding of the `1`-family charges into the `n`-family charges in
 a universal manor. -/

HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean

@@ -125,8 +125,7 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
       repeat erw [speciesVal]
       simp only [asCharges, neg_add_rev]
       ring
-    · simp only [toSpecies_apply]
-      rfl
+    · rfl
   right_inv S := by
     simp only [Fin.isValue, toSpecies_apply]
     apply ACCSystemLinear.LinSols.ext

HepLean/Mathematics/LinearMaps.lean

@@ -193,20 +193,15 @@ def mk₃ (f : V × V × V→ ℚ) (map_smul : ∀ a S T L, f (a • S, T, L) =
       rw [swap₁, map_add, swap₁, swap₁ S2 S T])
     (by
       intro L T
-      simp only
-      rw [swap₂])).toLinearMap
+      exact swap₂ S L T)).toLinearMap
   map_add' S1 S2 := by
     apply LinearMap.ext
     intro T
     apply LinearMap.ext
     intro S
-    simp [BiLinearSymm.mk₂, map_add]
-  map_smul' a S := by
-    apply LinearMap.ext
-    intro T
-    apply LinearMap.ext
-    intro L
-    simp [BiLinearSymm.mk₂, map_smul]
+    exact map_add S1 S2 T S
+  map_smul' a S :=
+    LinearMap.ext fun T => LinearMap.ext fun L => map_smul a S T L
   swap₁' := swap₁
   swap₂' := swap₂
 
@@ -248,8 +243,7 @@ lemma map_add₃ (f : TriLinearSymm V) (S T L1 L2 : V) :
 /-- Fixing the second and third input vectors, the resulting linear map. -/
 def toLinear₁ (f : TriLinearSymm V) (T L : V) : V →ₗ[ℚ] ℚ where
   toFun S := f S T L
-  map_add' S1 S2 := by
-    simp only [f.map_add₁]
+  map_add' S1 S2 := map_add₁ f S1 S2 T L
   map_smul' a S := by
     simp only [f.map_smul₁]
     rfl

HepLean/Mathematics/SO3/Basic.lean

@@ -47,13 +47,8 @@ lemma coe_inv (A : SO3) : (A⁻¹).1 = A.1⁻¹:=
 /-- The inclusion of `SO(3)` into `GL (Fin 3) ℝ`. -/
 def toGL : SO(3) →* GL (Fin 3) ℝ where
   toFun A := ⟨A.1, (A⁻¹).1, A.2.2, mul_eq_one_comm.mpr A.2.2⟩
-  map_one' := by
-    simp
-    rfl
-  map_mul' x y := by
-    simp only [_root_.mul_inv_rev, coe_inv]
-    ext
-    rfl
+  map_one' := (GeneralLinearGroup.ext_iff _ 1).mpr fun _=> congrFun rfl
+  map_mul' _ _ := (GeneralLinearGroup.ext_iff _ _).mpr fun _ => congrFun rfl
 
 lemma subtype_val_eq_toGL : (Subtype.val : SO3 → Matrix (Fin 3) (Fin 3) ℝ) =
     Units.val ∘ toGL.toFun :=
@@ -70,14 +65,7 @@ lemma toGL_injective : Function.Injective toGL := by
 def toProd : SO(3) →* (Matrix (Fin 3) (Fin 3) ℝ) × (Matrix (Fin 3) (Fin 3) ℝ)ᵐᵒᵖ :=
   MonoidHom.comp (Units.embedProduct _) toGL
 
-lemma toProd_eq_transpose : toProd A = (A.1, ⟨A.1ᵀ⟩) := by
-  simp only [toProd, Units.embedProduct, coe_units_inv, MulOpposite.op_inv, toGL, coe_inv,
-    MonoidHom.coe_comp, MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply, Prod.mk.injEq,
-    true_and]
-  refine MulOpposite.unop_inj.mp ?_
-  simp only [MulOpposite.unop_inv, MulOpposite.unop_op]
-  rw [← coe_inv]
-  rfl
+lemma toProd_eq_transpose : toProd A = (A.1, ⟨A.1ᵀ⟩) := rfl
 
 lemma toProd_injective : Function.Injective toProd := by
   intro A B h
@@ -131,7 +119,7 @@ lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by
       _ = det A.1 * det (1 - A.1ᵀ) := by rw [← det_mul, mul_sub, mul_one]
       _ = det (1 - A.1ᵀ) := by simp [A.2.1]
       _ = det (1 - A.1ᵀ)ᵀ := by rw [det_transpose]
-      _ = det (1 - A.1) := by simp
+      _ = det (1 - A.1) := rfl
       _ = det (- (A.1 - 1)) := by simp
       _ = (- 1) ^ 3 * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
       _ = - det (A.1 - 1) := by simp [pow_three]
@@ -145,7 +133,7 @@ lemma det_id_minus (A : SO(3)) : det (1 - A.1) = 0 := by
       _ = (- 1) ^ 3 * det (A.1 - 1) := by simp only [det_neg, Fintype.card_fin, neg_mul, one_mul]
       _ = - det (A.1 - 1) := by simp [pow_three]
   rw [h1, det_minus_id]
-  simp only [neg_zero]
+  exact neg_zero
 
 @[simp]
 lemma one_in_spectrum (A : SO(3)) : 1 ∈ spectrum ℝ (A.1) := by