refactor: Lint

2024-11-11 07:22:36 +00:00 · 2024-11-11 07:22:36 +00:00 · 081955c993
commit 081955c993
parent a8243f4e79
6 changed files with 35 additions and 34 deletions
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/Lemmas.lean
@ -53,12 +53,11 @@ lemma accGrav_Q_neq_zero {S : (SMNoGrav 1).Sols} (hQ : Q S.val (0 : Fin 1) ≠ 0
  have hE := E_zero_iff_Q_zero.mpr.mt hQ
  let S' := linearParametersQENeqZero.bijection.symm ⟨S.1.1, And.intro hQ hE⟩
  have hC := cubeSol S
-  have FLTThree := fermatLastTheoremFor_iff_rat.mp fermatLastTheoremThree
  have hS' := congrArg (fun S => S.val.val)
    (linearParametersQENeqZero.bijection.right_inv ⟨S.1.1, And.intro hQ hE⟩)
  change _ = S.val at hS'
  rw [← hS'] at hC ⊢
-  exact S'.grav_of_cubic hC FLTThree
+  exact S'.grav_of_cubic hC

 /-- Any solution to the ACCs without gravity satisfies the gravitational ACC. -/
 theorem accGravSatisfied {S : (SMNoGrav 1).Sols} :
--- a/HepLean/Lorentz/PauliMatrices/AsTensor.lean
+++ b/HepLean/Lorentz/PauliMatrices/AsTensor.lean
@ -130,14 +130,14 @@ def asConsTensor : 𝟙_ (Rep ℂ SL(2,ℂ)) ⟶ complexContr ⊗ leftHanded ⊗
      map_sum, map_tmul]
    symm
    calc _ = ∑ x, ((complexContr.ρ M) (complexContrBasis x) ⊗ₜ[ℂ]
-      leftRightToMatrix.symm (SL2C.toLinearMapSelfAdjointMatrix M (σSA x))) := by
+      leftRightToMatrix.symm (SL2C.toSelfAdjointMap M (σSA x))) := by
          refine Finset.sum_congr rfl (fun x _ => ?_)
          rw [← leftRightToMatrix_ρ_symm_selfAdjoint]
          rfl
      _ = ∑ x, ((∑ i, (SL2C.toLorentzGroup M).1 i x • (complexContrBasis i)) ⊗ₜ[ℂ]
          ∑ j, leftRightToMatrix.symm ((SL2C.toLorentzGroup M⁻¹).1 x j • (σSA j))) := by
          refine Finset.sum_congr rfl (fun x _ => ?_)
-          rw [SL2CRep_ρ_basis, toSelfAdjointMap_σSA]
+          rw [SL2CRep_ρ_basis, SL2C.toSelfAdjointMap_σSA]
          simp only [Action.instMonoidalCategory_tensorObj_V, SL2C.toLorentzGroup_apply_coe,
            Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero, Fin.isValue,
            Finset.sum_singleton, map_inv, lorentzGroupIsGroup_inv, AddSubgroup.coe_add,
--- a/HepLean/Lorentz/RealVector/Modules.lean
+++ b/HepLean/Lorentz/RealVector/Modules.lean
@ -278,11 +278,9 @@ lemma toSelfAdjoint_symm_basis (i : Fin 1 ⊕ Fin 3) :
 ## Topology
 -/

-
 instance : TopologicalSpace (ContrMod d) := TopologicalSpace.induced
  ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)

-
 lemma toFin1dℝEquiv_isInducing : IsInducing (@ContrMod.toFin1dℝEquiv d) := by
  exact { eq_induced := rfl }

--- a/HepLean/Lorentz/RealVector/NormOne.lean
+++ b/HepLean/Lorentz/RealVector/NormOne.lean
@ -22,7 +22,7 @@ variable {d : ℕ}
 /-- The set of Lorentz vectors with norm 1. -/
 def NormOne (d : ℕ) : Set (Contr d) := fun v => ⟪v, v⟫ₘ = (1 : ℝ)

-noncomputable  section
+noncomputable section

 namespace NormOne

@ -68,7 +68,7 @@ lemma _root_.LorentzGroup.inl_inl_mul (Λ Λ' : LorentzGroup d) : (Λ * Λ').1 (
    ⟪(LorentzGroup.toNormOne (LorentzGroup.transpose Λ)).1,
      (Contr d).ρ LorentzGroup.parity (LorentzGroup.toNormOne Λ').1⟫ₘ := by
  rw [contrContrContractField.right_parity]
-  simp  only [Fin.isValue, lorentzGroupIsGroup_mul_coe, Matrix.mul_apply, Fintype.sum_sum_type,
+  simp only [Fin.isValue, lorentzGroupIsGroup_mul_coe, Matrix.mul_apply, Fintype.sum_sum_type,
    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton,
    LorentzGroup.transpose, PiLp.inner_apply, Function.comp_apply,
    RCLike.inner_apply, conj_trivial]
@ -80,7 +80,7 @@ lemma _root_.LorentzGroup.inl_inl_mul (Λ Λ' : LorentzGroup d) : (Λ * Λ').1 (
    rw [LorentzGroup.toNormOne_inr, LorentzGroup.toNormOne_inr]
    rfl

-lemma inl_sq : v.val.val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace v.val‖ ^ 2  := by
+lemma inl_sq : v.val.val (Sum.inl 0) ^ 2 = 1 + ‖ContrMod.toSpace v.val‖ ^ 2 := by
  rw [contrContrContractField.inl_sq_eq, v.2]
  congr
  rw [← real_inner_self_eq_norm_sq]
@ -99,14 +99,14 @@ lemma inl_le_neg_one_or_one_le_inl : v.val.val (Sum.inl 0) ≤ -1 ∨ 1 ≤ v.va

 lemma norm_space_le_abs_inl : ‖v.1.toSpace‖ < |v.val.val (Sum.inl 0)| := by
  rw [(abs_norm _).symm, ← @sq_lt_sq, inl_sq]
-  change  ‖ContrMod.toSpace v.val‖ ^ 2 < 1 + ‖ContrMod.toSpace v.val‖ ^ 2
+  change ‖ContrMod.toSpace v.val‖ ^ 2 < 1 + ‖ContrMod.toSpace v.val‖ ^ 2
  exact lt_one_add (‖(v.1).toSpace‖ ^ 2)

 lemma norm_space_leq_abs_inl : ‖v.1.toSpace‖ ≤ |v.val.val (Sum.inl 0)| :=
  le_of_lt (norm_space_le_abs_inl v)

 lemma inl_abs_sub_space_norm :
-    0 ≤ |v.val.val (Sum.inl 0)| * |w.val.val (Sum.inl 0)| - ‖v.1.toSpace‖  * ‖w.1.toSpace‖ := by
+    0 ≤ |v.val.val (Sum.inl 0)| * |w.val.val (Sum.inl 0)| - ‖v.1.toSpace‖ * ‖w.1.toSpace‖ := by
  apply sub_nonneg.mpr
  apply mul_le_mul (norm_space_leq_abs_inl v) (norm_space_leq_abs_inl w) ?_ ?_
  · exact norm_nonneg _
@ -148,7 +148,6 @@ lemma mem_iff_parity_mem : v ∈ FuturePointing d ↔ ⟨(Contr d).ρ LorentzGro
  change _ ↔ 0 < (minkowskiMatrix.mulVec v.val.val) (Sum.inl 0)
  simp only [Fin.isValue, minkowskiMatrix.mulVec_inl_0]

-
 lemma not_mem_iff_inl_le_zero : v ∉ FuturePointing d ↔ v.val.val (Sum.inl 0) ≤ 0 := by
  rw [mem_iff]
  simp
@ -173,7 +172,7 @@ lemma not_mem_iff_neg : v ∉ FuturePointing d ↔ neg v ∈ FuturePointing d :=

 variable (f f' : FuturePointing d)

-lemma inl_nonneg : 0 ≤ f.val.val.val (Sum.inl 0):= le_of_lt f.2
+lemma inl_nonneg : 0 ≤ f.val.val.val (Sum.inl 0) := le_of_lt f.2

 lemma abs_inl : |f.val.val.val (Sum.inl 0)| = f.val.val.val (Sum.inl 0) :=
  abs_of_nonneg (inl_nonneg f)
@ -231,7 +230,6 @@ namespace FuturePointing
 ## Topology
 -/

-
 /-- The `FuturePointing d` which has all space components zero. -/
@[simps!]
 noncomputable def timeVecNormOneFuture : FuturePointing d := ⟨⟨ContrMod.stdBasis (Sum.inl 0), by
--- a/HepLean/Lorentz/SL2C/Basic.lean
+++ b/HepLean/Lorentz/SL2C/Basic.lean
@ -83,7 +83,7 @@ lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) :
    (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +
      (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re)) • PauliMatrix.σSAL (Sum.inr 0)
    + ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im
-      - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) •  PauliMatrix.σSAL (Sum.inr 1)
+      - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re)) • PauliMatrix.σSAL (Sum.inr 1)
    + ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) •
      PauliMatrix.σSAL (Sum.inr 2) := by
  simp only [toSelfAdjointMap, PauliMatrix.σSAL, Fin.isValue, Basis.coe_mk, PauliMatrix.σSAL',
@ -97,34 +97,43 @@ lemma toSelfAdjointMap_apply_σSAL_inl (M : SL(2, ℂ)) :
  conv => lhs; erw [← eta_fin_two 1, mul_one]
  conv => lhs; lhs; rw [eta_fin_two M.1]
  conv => lhs; rhs; rw [eta_fin_two M.1ᴴ]
-  simp
+  simp only [Fin.isValue, conjTranspose_apply, RCLike.star_def, cons_mul, Nat.succ_eq_add_one,
+    Nat.reduceAdd, vecMul_cons, head_cons, smul_cons, smul_eq_mul, smul_empty, tail_cons,
+    empty_vecMul, add_zero, add_cons, empty_add_empty, empty_mul, Equiv.symm_apply_apply,
+    EmbeddingLike.apply_eq_iff_eq]
  rw [mul_conj', mul_conj', mul_conj', mul_conj']
  ext x y
  match x, y with
  | 0, 0 =>
-    simp
+    simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_zero, empty_val', cons_val_fin_one]
    ring_nf
  | 0, 1 =>
-    simp
+    simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_one, head_cons, empty_val',
+      cons_val_fin_one, cons_val_zero]
    ring_nf
    rw [← re_add_im (M.1 0 0), ← re_add_im (M.1 0 1), ← re_add_im (M.1 1 0), ← re_add_im (M.1 1 1)]
-    simp [- re_add_im]
+    simp only [Fin.isValue, map_add, conj_ofReal, _root_.map_mul, conj_I, mul_neg, add_re,
+      ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self, add_zero, add_im,
+      mul_im, zero_add]
    ring_nf
-    simp
+    simp only [Fin.isValue, I_sq, mul_neg, mul_one, neg_mul, neg_neg, one_mul, sub_neg_eq_add]
    ring
  | 1, 0 =>
-    simp
+    simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_zero, empty_val', cons_val_fin_one,
+      cons_val_one, head_fin_const]
    ring_nf
    rw [← re_add_im (M.1 0 0), ← re_add_im (M.1 0 1), ← re_add_im (M.1 1 0), ← re_add_im (M.1 1 1)]
-    simp [- re_add_im]
+    simp only [Fin.isValue, map_add, conj_ofReal, _root_.map_mul, conj_I, mul_neg, add_re,
+      ofReal_re, mul_re, I_re, mul_zero, ofReal_im, I_im, mul_one, sub_self, add_zero, add_im,
+      mul_im, zero_add]
    ring_nf
-    simp
+    simp only [Fin.isValue, I_sq, mul_neg, mul_one, neg_mul, neg_neg, one_mul, sub_neg_eq_add]
    ring
  | 1, 1 =>
-    simp
+    simp only [Fin.isValue, norm_eq_abs, cons_val', cons_val_one, head_cons, empty_val',
+      cons_val_fin_one, head_fin_const]
    ring_nf

-
 /-- The monoid homomorphisms from `SL(2, ℂ)` to matrices indexed by `Fin 1 ⊕ Fin 3`
  formed by the action `M A Mᴴ`. -/
 def toMatrix : SL(2, ℂ) →* Matrix (Fin 1 ⊕ Fin 3) (Fin 1 ⊕ Fin 3) ℝ where
@ -216,15 +225,15 @@ lemma toLorentzGroup_fst_col (M : SL(2, ℂ)) :
    (fun μ => (toLorentzGroup M).1 μ (Sum.inl 0)) = fun μ =>
      match μ with
      | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)
-      | Sum.inr 0 =>  (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +
+      | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +
        (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re))
      | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im
        - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re))
      | Sum.inr 2 => ((- ‖M.1 0 0‖ ^ 2 - ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2) := by
-  let k :  Fin 1 ⊕ Fin 3 → ℝ := fun μ =>
+  let k : Fin 1 ⊕ Fin 3 → ℝ := fun μ =>
    match μ with
    | Sum.inl 0 => ((‖M.1 0 0‖ ^ 2 + ‖M.1 0 1‖ ^ 2 + ‖M.1 1 0‖ ^ 2 + ‖M.1 1 1‖ ^ 2) / 2)
-    | Sum.inr 0 =>  (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +
+    | Sum.inr 0 => (- ((M.1 0 1).re * (M.1 1 1).re + (M.1 0 1).im * (M.1 1 1).im +
      (M.1 0 0).im * (M.1 1 0).im + (M.1 0 0).re * (M.1 1 0).re))
    | Sum.inr 1 => ((- (M.1 0 0).re * (M.1 1 0).im + ↑(M.1 1 0).re * (M.1 0 0).im
      - (M.1 0 1).re * (M.1 1 1).im + (M.1 0 1).im * (M.1 1 1).re))
--- a/HepLean/Lorentz/Weyl/Two.lean
+++ b/HepLean/Lorentz/Weyl/Two.lean
@ -718,12 +718,10 @@ open Lorentz
 lemma altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
    (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :
    TensorProduct.map (altLeftHanded.ρ M) (altRightHanded.ρ M) (altLeftAltRightToMatrix.symm v) =
-    altLeftAltRightToMatrix.symm
-    (SL2C.toLinearMapSelfAdjointMatrix (M.transpose⁻¹) ⟨v, hv⟩) := by
+    altLeftAltRightToMatrix.symm (SL2C.toSelfAdjointMap (M.transpose⁻¹) ⟨v, hv⟩) := by
  rw [altLeftAltRightToMatrix_ρ_symm]
  apply congrArg
-  simp only [MonoidHom.coe_mk, OneHom.coe_mk,
-    SL2C.toLinearMapSelfAdjointMatrix_apply_coe, SpecialLinearGroup.coe_inv,
+  simp only [SL2C.toSelfAdjointMap_apply_coe, SpecialLinearGroup.coe_inv,
    SpecialLinearGroup.coe_transpose]
  congr
  · rw [SL2C.inverse_coe]
@ -737,8 +735,7 @@ lemma altLeftAltRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2)
 lemma leftRightToMatrix_ρ_symm_selfAdjoint (v : Matrix (Fin 2) (Fin 2) ℂ)
    (hv : IsSelfAdjoint v) (M : SL(2,ℂ)) :
    TensorProduct.map (leftHanded.ρ M) (rightHanded.ρ M) (leftRightToMatrix.symm v) =
-    leftRightToMatrix.symm
-    (SL2C.toLinearMapSelfAdjointMatrix M ⟨v, hv⟩) := by
+    leftRightToMatrix.symm (SL2C.toSelfAdjointMap M ⟨v, hv⟩) := by
  rw [leftRightToMatrix_ρ_symm]
  rfl