Merge pull request #46 from pitmonticone/golf-proofs

Golf a few proofs

HepLean/SpaceTime/Metric.lean

@@ -85,40 +85,22 @@ lemma η_transpose : η.transpose = η := by
 
 @[simp]
 lemma det_η : η.det = - 1 := by
-  simp only [η_explicit, det_succ_row_zero, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.isValue,
-    of_apply, cons_val', empty_val', cons_val_fin_one, cons_val_zero, submatrix_apply,
-    Fin.succ_zero_eq_one, cons_val_one, head_cons, submatrix_submatrix, Function.comp_apply,
-    Fin.succ_one_eq_two, cons_val_two, tail_cons, det_unique, Fin.default_eq_zero, cons_val_succ,
-    head_fin_const, Fin.sum_univ_succ, Fin.val_zero, pow_zero, one_mul, Fin.zero_succAbove,
-    Finset.univ_unique, Fin.val_succ, Fin.coe_fin_one, zero_add, pow_one, neg_mul,
-    Fin.succ_succAbove_zero, Finset.sum_neg_distrib, Finset.sum_singleton, Fin.succ_succAbove_one,
-    even_two, Even.neg_pow, one_pow, mul_one, mul_neg, neg_neg, mul_zero, neg_zero, add_zero,
-    zero_mul, Finset.sum_const_zero]
+  simp [η_explicit, det_succ_row_zero, Fin.sum_univ_succ]
 
 @[simp]
 lemma η_sq : η * η = 1 := by
   funext μ ν
-  rw [mul_apply, Fin.sum_univ_four]
   fin_cases μ <;> fin_cases ν <;>
-     simp [η_explicit, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one,
-      Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
-      Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
-      vecHead, vecTail, Function.comp_apply]
+     simp [η_explicit, vecHead, vecTail]
 
 lemma η_diag_mul_self (μ : Fin 4) : η μ μ * η μ μ  = 1 := by
-  fin_cases μ
-    <;> simp [η_explicit]
+  fin_cases μ <;> simp [η_explicit]
 
 lemma η_mulVec (x : spaceTime) : η *ᵥ x = ![x 0, -x 1, -x 2, -x 3] := by
-  rw [explicit x]
-  rw [η_explicit]
+  rw [explicit x, η_explicit]
   funext i
-  rw [mulVec, dotProduct, Fin.sum_univ_four]
   fin_cases i <;>
-    simp [Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one, Matrix.cons_val_one,
-      Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
-      Matrix.head_fin_const, Matrix.head_cons, Matrix.vecCons_const, Fin.mk_one, Fin.mk_one,
-      vecHead, vecTail, Function.comp_apply]
+  simp [vecHead, vecTail]
 
 /-- Given a point in spaceTime `x` the linear map `y → x ⬝ᵥ (η *ᵥ y)`. -/
 @[simps!]
@@ -128,7 +110,7 @@ def linearMapForSpaceTime (x : spaceTime) : spaceTime →ₗ[ℝ] ℝ where
     simp only
     rw [mulVec_add, dotProduct_add]
   map_smul' c y := by
-    simp only
+    simp only [RingHom.id_apply, smul_eq_mul]
     rw [mulVec_smul, dotProduct_smul]
     rfl
 
@@ -168,7 +150,7 @@ lemma time_elm_sq_of_ηLin (x : spaceTime) : x 0 ^ 2 = ηLin x x + ‖x.space‖
 
 lemma ηLin_leq_time_sq (x : spaceTime) : ηLin x x ≤ x 0 ^ 2 := by
   rw [time_elm_sq_of_ηLin]
-  apply (le_add_iff_nonneg_right _).mpr $ sq_nonneg ‖x.space‖
+  exact (le_add_iff_nonneg_right _).mpr $ sq_nonneg ‖x.space‖
 
 lemma ηLin_space_inner_product (x y : spaceTime) :
     ηLin x y = x 0 * y 0 - ⟪x.space, y.space⟫_ℝ  := by
@@ -202,18 +184,18 @@ lemma ηLin_stdBasis_apply (μ : Fin 4) (x : spaceTime) : ηLin (stdBasis μ) x
 lemma ηLin_η_stdBasis (μ ν : Fin 4) : ηLin (stdBasis μ) (stdBasis ν) = η μ ν := by
   rw [ηLin_stdBasis_apply]
   by_cases h : μ = ν
-  rw [stdBasis_apply]
-  subst h
-  simp only [↓reduceIte, mul_one]
-  rw [stdBasis_not_eq, η_off_diagonal h]
-  simp only [mul_zero]
-  exact fun a => h (id a.symm)
+  · rw [stdBasis_apply]
+    subst h
+    simp
+  · rw [stdBasis_not_eq, η_off_diagonal h]
+    simp only [mul_zero]
+    exact fun a ↦ h (id a.symm)
 
 lemma ηLin_mulVec_left (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
     ηLin (Λ *ᵥ x) y = ηLin x ((η * Λᵀ * η) *ᵥ y) := by
-  simp only [ηLin, LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply, mulVec_mulVec]
-  rw [(vecMul_transpose Λ x).symm, ← dotProduct_mulVec, mulVec_mulVec]
-  rw [← mul_assoc, ← mul_assoc, η_sq, one_mul]
+  simp [ηLin, LinearMap.coe_mk, AddHom.coe_mk, linearMapForSpaceTime_apply,
+    mulVec_mulVec, (vecMul_transpose Λ x).symm, ← dotProduct_mulVec, mulVec_mulVec,
+    ← mul_assoc, ← mul_assoc, η_sq, one_mul]
 
 lemma ηLin_mulVec_right (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
     ηLin x (Λ *ᵥ y) = ηLin ((η * Λᵀ * η) *ᵥ x) y := by
@@ -231,14 +213,14 @@ lemma ηLin_matrix_stdBasis' (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
 lemma ηLin_matrix_eq_identity_iff (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
     Λ = 1 ↔ ∀ (x y : spaceTime), ηLin x y = ηLin x (Λ *ᵥ y) := by
   apply Iff.intro
-  intro h
-  subst h
-  simp only [ηLin, one_mulVec, implies_true]
-  intro h
-  funext μ ν
-  have h1 := h (stdBasis μ) (stdBasis ν)
-  rw [ηLin_matrix_stdBasis, ηLin_η_stdBasis] at h1
-  fin_cases μ <;> fin_cases ν <;>
+  · intro h
+    subst h
+    simp only [ηLin, one_mulVec, implies_true]
+  · intro h
+    funext μ ν
+    have h1 := h (stdBasis μ) (stdBasis ν)
+    rw [ηLin_matrix_stdBasis, ηLin_η_stdBasis] at h1
+    fin_cases μ <;> fin_cases ν <;>
     simp_all [η_explicit, Fin.zero_eta, Matrix.cons_val', Matrix.cons_val_fin_one,
       Matrix.cons_val_one,
       Matrix.cons_val_succ', Matrix.cons_val_zero, Matrix.empty_val', Matrix.head_cons,
@@ -248,9 +230,6 @@ lemma ηLin_matrix_eq_identity_iff (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
 /-- The metric as a quadratic form on `spaceTime`. -/
 def quadraticForm : QuadraticForm ℝ spaceTime := ηLin.toQuadraticForm
 
-
-
-
 end spaceTime
 
 end

HepLean/StandardModel/HiggsBoson/Basic.lean

@@ -51,7 +51,7 @@ instance : NormedAddCommGroup (Fin 2 → ℂ) := by
 /-- Given a vector `ℂ²` the constant higgs field with value equal to that
 section. -/
 noncomputable def higgsVec.toField (φ : higgsVec) : higgsField where
-  toFun := fun _ => φ
+  toFun := fun _ ↦ φ
   contMDiff_toFun := by
     intro x
     rw [Bundle.contMDiffAt_section]
@@ -63,7 +63,6 @@ open  Complex Real
 /-- Given a `higgsField`, the corresponding map from `spaceTime` to `higgsVec`. -/
 def toHiggsVec (φ : higgsField) : spaceTime → higgsVec := φ
 
-
 lemma toHiggsVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, higgsVec) φ.toHiggsVec := by
   intro x0
   have h1 := φ.contMDiff x0
@@ -76,29 +75,25 @@ lemma toHiggsVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ
   exact h1
 
 lemma toField_toHiggsVec_apply (φ : higgsField) (x : spaceTime) :
-    (φ.toHiggsVec x).toField x = φ x := by
-  rfl
+    (φ.toHiggsVec x).toField x = φ x := rfl
 
-lemma higgsVecToFin2ℂ_toHiggsVec (φ : higgsField) : higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := by
-  ext x
-  rfl
+lemma higgsVecToFin2ℂ_toHiggsVec (φ : higgsField) :
+    higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl
 
-lemma toVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ := by
-  rw [← φ.higgsVecToFin2ℂ_toHiggsVec]
-  exact Smooth.comp smooth_higgsVecToFin2ℂ (φ.toHiggsVec_smooth)
+lemma toVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ :=
+  smooth_higgsVecToFin2ℂ.comp φ.toHiggsVec_smooth
 
 lemma apply_smooth (φ : higgsField) :
-    ∀ i, Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℂ) (fun (x : spaceTime) => (φ x i)) := by
-  rw [← smooth_pi_space]
-  exact φ.toVec_smooth
+    ∀ i, Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℂ) (fun (x : spaceTime) => (φ x i)) :=
+  (smooth_pi_space).mp (φ.toVec_smooth)
 
 lemma apply_re_smooth (φ : higgsField) (i : Fin 2):
     Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (reCLM ∘ (fun (x : spaceTime) =>  (φ x i))) :=
-  Smooth.comp (ContinuousLinearMap.smooth reCLM) (φ.apply_smooth i)
+  (ContinuousLinearMap.smooth reCLM).comp (φ.apply_smooth i)
 
 lemma apply_im_smooth (φ : higgsField) (i : Fin 2):
     Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (imCLM ∘ (fun (x : spaceTime) =>  (φ x i))) :=
-  Smooth.comp (ContinuousLinearMap.smooth imCLM) (φ.apply_smooth i)
+  (ContinuousLinearMap.smooth imCLM).comp (φ.apply_smooth i)
 
 /-- Given two `higgsField`, the map `spaceTime → ℂ` obtained by taking their inner product. -/
 def innerProd (φ1 φ2 : higgsField) : spaceTime → ℂ := fun x => ⟪φ1 x, φ2 x⟫_ℂ
@@ -115,9 +110,7 @@ lemma toHiggsVec_norm (φ : higgsField) (x : spaceTime) :
 lemma normSq_expand (φ : higgsField)  :
     φ.normSq  = fun x => (conj (φ x 0) * (φ x 0) + conj (φ x 1) * (φ x 1) ).re := by
   funext x
-  simp only [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add]
-  rw [@norm_sq_eq_inner ℂ]
-  simp
+  simp [normSq, add_re, mul_re, conj_re, conj_im, neg_mul, sub_neg_eq_add, @norm_sq_eq_inner ℂ]
 
 lemma normSq_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) φ.normSq := by
   rw [normSq_expand]
@@ -140,10 +133,10 @@ lemma normSq_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ,
   exact φ.apply_im_smooth 1
 
 lemma normSq_nonneg (φ : higgsField) (x : spaceTime) : 0 ≤ φ.normSq x := by
-  simp only [normSq, ge_iff_le, norm_nonneg, pow_nonneg]
+  simp [normSq, ge_iff_le, norm_nonneg, pow_nonneg]
 
 lemma normSq_zero (φ : higgsField) (x : spaceTime) : φ.normSq x = 0 ↔ φ x = 0 := by
-  simp only [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero]
+  simp [normSq, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, pow_eq_zero_iff, norm_eq_zero]
 
 /-- The Higgs potential of the form `- μ² * |φ|² + λ * |φ|⁴`. -/
 @[simp]
@@ -153,10 +146,8 @@ def potential (φ : higgsField) (μSq lambda : ℝ ) (x : spaceTime) :  ℝ :=
 lemma potential_smooth (φ : higgsField) (μSq lambda : ℝ) :
     Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, ℝ) (fun x => φ.potential μSq lambda x) := by
   simp only [potential, normSq, neg_mul]
-  exact Smooth.add
-    (Smooth.neg (Smooth.smul smooth_const φ.normSq_smooth))
-    (Smooth.smul (Smooth.smul smooth_const φ.normSq_smooth) φ.normSq_smooth)
-
+  exact (smooth_const.smul φ.normSq_smooth).neg.add
+    ((smooth_const.smul φ.normSq_smooth).smul φ.normSq_smooth)
 
 lemma potential_apply (φ : higgsField) (μSq lambda : ℝ) (x : spaceTime) :
     (φ.potential μSq lambda) x = higgsVec.potential μSq lambda (φ.toHiggsVec x) := by
@@ -171,35 +162,20 @@ lemma isConst_of_higgsVec (φ : higgsVec) : φ.toField.isConst := by
   intro x _
   simp [higgsVec.toField]
 
-lemma isConst_iff_of_higgsVec (Φ : higgsField) : Φ.isConst ↔ ∃ (φ : higgsVec), Φ = φ.toField := by
-  apply Iff.intro
-  intro h
-  use Φ 0
-  ext x y
-  rw [← h x 0]
-  rfl
-  intro h
-  intro x y
-  obtain ⟨φ, hφ⟩ := h
-  subst hφ
-  rfl
+lemma isConst_iff_of_higgsVec (Φ : higgsField) : Φ.isConst ↔ ∃ (φ : higgsVec), Φ = φ.toField :=
+  Iff.intro (fun h ↦ ⟨Φ 0, by ext x y; rw [← h x 0]; rfl⟩) (fun ⟨φ, hφ⟩ x y ↦ by subst hφ; rfl)
 
 lemma normSq_of_higgsVec (φ : higgsVec) : φ.toField.normSq = fun x => (norm φ) ^ 2 := by
-  simp only [normSq, higgsVec.toField]
   funext x
-  simp
+  simp [normSq, higgsVec.toField]
 
 lemma potential_of_higgsVec (φ : higgsVec) (μSq lambda : ℝ) :
     φ.toField.potential μSq lambda = fun _ => higgsVec.potential μSq lambda φ := by
   simp [higgsVec.potential]
   unfold potential
   rw [normSq_of_higgsVec]
-  funext x
-  simp only [neg_mul, add_right_inj]
   ring_nf
 
-
-
 end higgsField
 end
 end StandardModel

HepLean/StandardModel/HiggsBoson/TargetSpace.lean

@@ -46,10 +46,8 @@ section higgsVec
 casting vectors. -/
 def higgsVecToFin2ℂ : higgsVec →L[ℝ] (Fin 2 → ℂ) where
   toFun x := x
-  map_add' x y := by
-    simp
-  map_smul' a x := by
-    simp
+  map_add' x y := by simp
+  map_smul' a x := by simp
 
 lemma smooth_higgsVecToFin2ℂ : Smooth 𝓘(ℝ, higgsVec) 𝓘(ℝ, Fin 2 → ℂ) higgsVecToFin2ℂ :=
   ContinuousLinearMap.smooth higgsVecToFin2ℂ
@@ -63,11 +61,10 @@ noncomputable def higgsRepUnitary : gaugeGroup →* unitaryGroup (Fin 2) ℂ whe
   map_mul'  := by
     intro ⟨_, a2, a3⟩ ⟨_, b2, b3⟩
     change repU1 (a3 * b3) *  fundamentalSU2 (a2 * b2) = _
-    rw [repU1.map_mul, fundamentalSU2.map_mul]
-    rw [mul_assoc, mul_assoc, ← mul_assoc (repU1 b3) _ _, repU1_fundamentalSU2_commute]
+    rw [repU1.map_mul, fundamentalSU2.map_mul, mul_assoc, mul_assoc,
+      ← mul_assoc (repU1 b3) _ _, repU1_fundamentalSU2_commute]
     repeat rw [mul_assoc]
-  map_one' := by
-    simp only [Prod.snd_one, _root_.map_one, Prod.fst_one, mul_one]
+  map_one' := by simp
 
 /-- An orthonormal basis of higgsVec. -/
 noncomputable def orthonormBasis : OrthonormalBasis (Fin 2) ℂ higgsVec :=
@@ -87,20 +84,16 @@ lemma matrixToLin_star (g : Matrix (Fin 2) (Fin 2) ℂ) :
 
 lemma matrixToLin_unitary (g : unitaryGroup (Fin 2) ℂ) :
     matrixToLin g ∈ unitary (higgsVec →L[ℂ] higgsVec) := by
-  rw [@unitary.mem_iff, ← matrixToLin_star, ← matrixToLin.map_mul, ← matrixToLin.map_mul]
-  rw [mem_unitaryGroup_iff.mp g.prop, mem_unitaryGroup_iff'.mp g.prop, matrixToLin.map_one]
+  rw [@unitary.mem_iff, ← matrixToLin_star, ← matrixToLin.map_mul, ← matrixToLin.map_mul,
+    mem_unitaryGroup_iff.mp g.prop, mem_unitaryGroup_iff'.mp g.prop, matrixToLin.map_one]
   simp
 
 /-- The natural homomorphism from unitary `2×2` complex matrices to unitary transformations
 of `higgsVec`. -/
 noncomputable def unitaryToLin : unitaryGroup (Fin 2) ℂ →* unitary (higgsVec →L[ℂ] higgsVec) where
   toFun g := ⟨matrixToLin g, matrixToLin_unitary g⟩
-  map_mul' g h := by
-    ext
-    simp
-  map_one' := by
-    ext
-    simp
+  map_mul' g h := by simp
+  map_one' := by simp
 
 /-- The inclusion of unitary transformations on `higgsVec` into all linear transformations. -/
 @[simps!]
@@ -114,8 +107,7 @@ def rep : Representation ℂ gaugeGroup higgsVec :=
 
 lemma higgsRepUnitary_mul (g : gaugeGroup) (φ : higgsVec) :
     (higgsRepUnitary g).1 *ᵥ φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) := by
-  simp only [higgsRepUnitary_apply_coe]
-  exact smul_mulVec_assoc (g.2.2 ^ 3) (g.2.1.1) φ
+  simp [higgsRepUnitary_apply_coe, smul_mulVec_assoc]
 
 lemma rep_apply (g : gaugeGroup) (φ : higgsVec) : rep g φ = g.2.2 ^ 3 • (g.2.1.1 *ᵥ φ) :=
   higgsRepUnitary_mul g φ
@@ -133,13 +125,11 @@ def potential (φ : higgsVec) : ℝ := - μSq  * ‖φ‖ ^ 2 + λ * ‖φ‖ ^
 
 lemma potential_invariant (φ : higgsVec)  (g : gaugeGroup) :
     potential μSq (λ) (rep g φ) = potential μSq (λ) φ := by
-  simp only [potential, neg_mul]
-  rw [norm_invariant]
+  simp only [potential, neg_mul, norm_invariant]
 
 lemma potential_as_quad (φ : higgsVec) :
     λ  * ‖φ‖ ^ 2 * ‖φ‖ ^ 2 + (- μSq ) * ‖φ‖ ^ 2 + (- potential μSq (λ) φ) = 0 := by
-  simp [potential]
-  ring
+  simp [potential]; ring
 
 end potentialDefn
 section potentialProp
@@ -161,11 +151,9 @@ lemma zero_le_potential_discrim  (φ : higgsVec) :
     0 ≤ discrim (λ) (- μSq ) (- potential μSq (λ) φ) := by
   have h1 := potential_as_quad μSq (λ) φ
   rw [quadratic_eq_zero_iff_discrim_eq_sq] at h1
-  rw [h1]
-  exact sq_nonneg (2 * (lambda ) * ‖φ‖ ^ 2 + -μSq)
-  simp only [ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
-  exact ne_of_gt hLam
-
+  · simp only [h1, ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
+    exact sq_nonneg (2 * lambda * ‖φ‖ ^ 2 + -μSq)
+  · exact ne_of_gt hLam
 
 lemma potential_eq_zero_sol (φ : higgsVec)
     (hV : potential μSq (λ) φ = 0) : φ = 0 ∨ ‖φ‖ ^ 2 = μSq / λ := by
@@ -209,19 +197,14 @@ lemma potential_bounded_below (φ : higgsVec) :
 
 lemma potential_bounded_below_of_μSq_nonpos  {μSq : ℝ}
     (hμSq : μSq ≤ 0) (φ : higgsVec) : 0 ≤ potential μSq (λ) φ := by
-  simp only [potential, neg_mul, add_zero]
   refine add_nonneg ?_ (potential_snd_term_nonneg hLam φ)
-  field_simp
-  rw [@mul_nonpos_iff]
-  simp_all only [ge_iff_le, norm_nonneg, pow_nonneg, and_self, or_true]
-
+  field_simp [mul_nonpos_iff]
+  simp_all [ge_iff_le, norm_nonneg, pow_nonneg, and_self, or_true]
 
 lemma potential_eq_bound_discrim_zero (φ : higgsVec)
     (hV : potential μSq (λ) φ = - μSq ^ 2 / (4  * λ)) :
     discrim (λ) (- μSq) (- potential μSq (λ) φ) = 0 := by
-  simp [discrim, hV]
-  field_simp
-  ring
+  field_simp [discrim, hV]
 
 lemma potential_eq_bound_higgsVec_sq (φ : higgsVec)
     (hV : potential μSq (λ) φ = - μSq ^ 2 / (4  * (λ))) :
@@ -229,81 +212,60 @@ lemma potential_eq_bound_higgsVec_sq (φ : higgsVec)
   have h1 := potential_as_quad μSq (λ) φ
   rw [quadratic_eq_zero_iff_of_discrim_eq_zero _
     (potential_eq_bound_discrim_zero μSq hLam φ hV)] at h1
-  rw [h1]
-  field_simp
-  ring_nf
-  simp only [ne_eq, div_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
+  simp_rw [h1, neg_neg]
   exact ne_of_gt hLam
 
 lemma potential_eq_bound_iff (φ : higgsVec) :
-    potential μSq (λ) φ = - μSq ^ 2 / (4  * (λ)) ↔ ‖φ‖ ^ 2 = μSq / (2 * (λ)) := by
-  apply Iff.intro
-  · intro h
-    exact potential_eq_bound_higgsVec_sq μSq hLam φ h
-  · intro h
-    have hv : ‖φ‖  ^ 4 = ‖φ‖ ^ 2 * ‖φ‖ ^ 2 := by
-      ring_nf
-    field_simp [potential, hv, h]
-    ring
+    potential μSq (λ) φ = - μSq ^ 2 / (4  * (λ)) ↔ ‖φ‖ ^ 2 = μSq / (2 * (λ)) :=
+  Iff.intro (potential_eq_bound_higgsVec_sq μSq hLam φ)
+    (fun h ↦ by
+      have hv : ‖φ‖ ^ 4 = ‖φ‖ ^ 2 * ‖φ‖ ^ 2 := by ring_nf
+      field_simp [potential, hv, h]
+      ring_nf)
 
 lemma potential_eq_bound_iff_of_μSq_nonpos  {μSq : ℝ}
-    (hμSq : μSq ≤ 0) (φ : higgsVec) : potential μSq (λ) φ = 0 ↔ φ = 0 := by
-  apply Iff.intro
-  · intro h
-    exact potential_eq_zero_sol_of_μSq_nonpos μSq hLam hμSq φ h
-  · intro h
-    simp [potential, h]
+    (hμSq : μSq ≤ 0) (φ : higgsVec) : potential μSq (λ) φ = 0 ↔ φ = 0 :=
+  Iff.intro (fun h ↦ potential_eq_zero_sol_of_μSq_nonpos μSq hLam hμSq φ h)
+  (fun h ↦ by simp [potential, h])
 
-lemma potential_eq_bound_IsMinOn  (φ : higgsVec)
+lemma potential_eq_bound_IsMinOn (φ : higgsVec)
     (hv : potential μSq lambda φ = - μSq ^ 2 / (4  * lambda)) :
     IsMinOn (potential μSq lambda) Set.univ φ := by
-  rw [isMinOn_univ_iff]
-  intro x
-  rw [hv]
-  exact potential_bounded_below μSq hLam x
+  rw [isMinOn_univ_iff, hv]
+  exact fun x ↦ potential_bounded_below μSq hLam x
 
 lemma potential_eq_bound_IsMinOn_of_μSq_nonpos  {μSq : ℝ}
     (hμSq : μSq ≤ 0) (φ : higgsVec) (hv : potential μSq lambda φ = 0) :
     IsMinOn (potential μSq lambda) Set.univ φ := by
-  rw [isMinOn_univ_iff]
-  intro x
-  rw [hv]
-  exact potential_bounded_below_of_μSq_nonpos hLam hμSq x
+  rw [isMinOn_univ_iff, hv]
+  exact fun x ↦ potential_bounded_below_of_μSq_nonpos hLam hμSq x
 
 lemma potential_bound_reached_of_μSq_nonneg  {μSq : ℝ} (hμSq : 0 ≤ μSq) :
     ∃ (φ : higgsVec), potential μSq lambda φ = - μSq ^ 2 / (4  * lambda) := by
   use ![√(μSq/(2 * lambda)), 0]
   refine (potential_eq_bound_iff μSq hLam _).mpr ?_
-  simp [@PiLp.norm_sq_eq_of_L2, Fin.sum_univ_two]
+  simp [PiLp.norm_sq_eq_of_L2]
   field_simp [mul_pow]
 
 lemma IsMinOn_potential_iff_of_μSq_nonneg  {μSq : ℝ} (hμSq : 0 ≤ μSq) :
     IsMinOn (potential μSq lambda) Set.univ φ ↔ ‖φ‖ ^ 2 = μSq /(2 * lambda) := by
-  apply Iff.intro
+  apply Iff.intro <;> rw [← potential_eq_bound_iff μSq hLam φ]
   · intro h
     obtain ⟨φm, hφ⟩ := potential_bound_reached_of_μSq_nonneg hLam hμSq
     have hm := isMinOn_univ_iff.mp h φm
     rw [hφ] at hm
-    have h1 := potential_bounded_below μSq hLam φ
-    rw [← potential_eq_bound_iff μSq hLam φ]
-    exact (Real.partialOrder.le_antisymm _ _ h1 hm).symm
-  · intro h
-    rw [← potential_eq_bound_iff μSq hLam φ] at h
-    exact potential_eq_bound_IsMinOn μSq hLam φ h
-
+    exact (Real.partialOrder.le_antisymm _ _ (potential_bounded_below μSq hLam φ) hm).symm
+  · exact potential_eq_bound_IsMinOn μSq hLam φ
 
 lemma IsMinOn_potential_iff_of_μSq_nonpos {μSq : ℝ} (hμSq : μSq ≤ 0) :
     IsMinOn (potential μSq lambda) Set.univ φ ↔ φ = 0 := by
-  apply Iff.intro
+  apply Iff.intro <;> rw [← potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ]
   · intro h
     have h0 := isMinOn_univ_iff.mp h 0
-    rw [(potential_eq_bound_iff_of_μSq_nonpos hLam hμSq 0).mpr (by rfl)] at h0
     have h1 := potential_bounded_below_of_μSq_nonpos hLam hμSq φ
-    rw [← (potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ)]
+    rw [(potential_eq_bound_iff_of_μSq_nonpos hLam hμSq 0).mpr (by rfl)] at h0
     exact (Real.partialOrder.le_antisymm _ _ h1 h0).symm
-  · intro h
-    rw [← potential_eq_bound_iff_of_μSq_nonpos hLam hμSq φ] at h
-    exact potential_eq_bound_IsMinOn_of_μSq_nonpos hLam hμSq φ h
+  · exact potential_eq_bound_IsMinOn_of_μSq_nonpos hLam hμSq φ
 
 end potentialProp
 /-- Given a Higgs vector, a rotation matrix which puts the first component of the
@@ -314,40 +276,31 @@ def rotateMatrix (φ : higgsVec) : Matrix (Fin 2) (Fin 2) ℂ :=
 lemma rotateMatrix_star (φ : higgsVec) :
     star φ.rotateMatrix =
     ![![conj (φ 1) /‖φ‖ ,  φ 0 /‖φ‖], ![- conj (φ 0) / ‖φ‖ , φ 1 / ‖φ‖] ] := by
-  simp [star]
-  rw [rotateMatrix, conjTranspose]
+  simp_rw [star, rotateMatrix, conjTranspose]
   ext i j
   fin_cases i <;> fin_cases j <;> simp [conj_ofReal]
 
-
 lemma rotateMatrix_det {φ : higgsVec} (hφ : φ ≠ 0) : (rotateMatrix φ).det = 1 := by
-  simp [rotateMatrix, det_fin_two]
   have h1 : (‖φ‖ : ℂ)  ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
-  field_simp
+  field_simp [rotateMatrix, det_fin_two]
   rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
-  simp only [PiLp.inner_apply, Complex.inner,  neg_mul, sub_neg_eq_add,
+  simp [PiLp.inner_apply, Complex.inner,  neg_mul, sub_neg_eq_add,
     Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
-  rfl
 
 lemma rotateMatrix_unitary {φ : higgsVec} (hφ : φ ≠ 0) :
     (rotateMatrix φ) ∈ unitaryGroup (Fin 2) ℂ := by
   rw [mem_unitaryGroup_iff', rotateMatrix_star, rotateMatrix]
   erw [mul_fin_two, one_fin_two]
   have : (‖φ‖ : ℂ)  ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
-  congr
-  field_simp
   ext i j
   fin_cases i <;> fin_cases j <;> field_simp
-  · rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
-    simp only [PiLp.inner_apply, Complex.inner,  neg_mul, sub_neg_eq_add,
+  <;> rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
+  · simp [PiLp.inner_apply, Complex.inner,  neg_mul, sub_neg_eq_add,
       Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm, add_comm]
-    rfl
   · ring_nf
   · ring_nf
-  · rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
-    simp only [PiLp.inner_apply, Complex.inner,  neg_mul, sub_neg_eq_add,
+  · simp [PiLp.inner_apply, Complex.inner,  neg_mul, sub_neg_eq_add,
       Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
-    rfl
 
 lemma rotateMatrix_specialUnitary {φ : higgsVec} (hφ : φ ≠ 0) :
     (rotateMatrix φ) ∈ specialUnitaryGroup (Fin 2) ℂ :=
@@ -361,19 +314,22 @@ def rotateGuageGroup {φ : higgsVec} (hφ : φ ≠ 0) : gaugeGroup :=
 lemma rotateGuageGroup_apply {φ : higgsVec} (hφ : φ ≠ 0) :
     rep (rotateGuageGroup hφ) φ = ![0, ofReal ‖φ‖] := by
   rw [rep_apply]
-  simp [rotateGuageGroup, rotateMatrix]
+  simp only [rotateGuageGroup, rotateMatrix, one_pow, one_smul,
+     Nat.succ_eq_add_one, Nat.reduceAdd, ofReal_eq_coe]
   ext i
   fin_cases i
-  simp [mulVec, vecHead, vecTail]
-  ring_nf
-  simp only [Fin.mk_one, Fin.isValue, cons_val_one, head_cons]
-  simp [mulVec, vecHead, vecTail]
-  have : (‖φ‖ : ℂ)  ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
-  field_simp
-  rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
-  simp only [PiLp.inner_apply, Complex.inner,  neg_mul, sub_neg_eq_add,
+  · simp only [mulVec, Fin.zero_eta, Fin.isValue, cons_val', empty_val', cons_val_fin_one,
+    cons_val_zero, cons_dotProduct, vecHead, vecTail, Nat.succ_eq_add_one, Nat.reduceAdd,
+    Function.comp_apply, Fin.succ_zero_eq_one, dotProduct_empty, add_zero]
+    ring_nf
+  · simp only [Fin.mk_one, Fin.isValue, cons_val_one, head_cons, mulVec, Fin.isValue,
+    cons_val', empty_val', cons_val_fin_one, vecHead, cons_dotProduct, vecTail, Nat.succ_eq_add_one,
+    Nat.reduceAdd, Function.comp_apply, Fin.succ_zero_eq_one, dotProduct_empty, add_zero]
+    have : (‖φ‖ : ℂ)  ≠ 0 := ofReal_inj.mp.mt (norm_ne_zero_iff.mpr hφ)
+    field_simp
+    rw [← ofReal_mul, ← sq, ← @real_inner_self_eq_norm_sq]
+    simp [PiLp.inner_apply, Complex.inner,  neg_mul, sub_neg_eq_add,
       Fin.sum_univ_two, ofReal_add, ofReal_mul, mul_conj, mul_comm]
-  rfl
 
 theorem rotate_fst_zero_snd_real (φ : higgsVec) :
     ∃ (g : gaugeGroup), rep g φ = ![0, ofReal ‖φ‖] := by