refactor: Lint

HepLean/SpaceTime/Basic.lean

@@ -40,6 +40,8 @@ open ComplexConjugate
 /-- The structure of a smooth manifold on spacetime. -/
 def asSmoothManifold : ModelWithCorners ℝ spaceTime spaceTime := 𝓘(ℝ, spaceTime)
 
+instance : ChartedSpace spaceTime spaceTime := chartedSpaceSelf spaceTime
+
 /-- The standard basis for spacetime. -/
 def stdBasis : Basis (Fin 4) ℝ spaceTime := Pi.basisFun ℝ (Fin 4)
 
@@ -73,7 +75,7 @@ lemma stdBasis_3 : stdBasis 3 = ![0, 0, 0, 1] := by
 lemma stdBasis_mulVec (μ ν : Fin 4) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
     (Λ *ᵥ stdBasis μ) ν = Λ ν μ := by
   rw [mulVec, dotProduct, Fintype.sum_eq_single μ, stdBasis_apply]
-  simp
+  simp only [↓reduceIte, mul_one]
   intro x h
   rw [stdBasis_apply, if_neg (Ne.symm h)]
   simp

HepLean/SpaceTime/Metric.lean

@@ -131,9 +131,9 @@ lemma ηLin_η_stdBasis (μ ν : Fin 4) : ηLin (stdBasis μ) (stdBasis ν) = η
   by_cases h : μ = ν
   rw [stdBasis_apply]
   subst h
-  simp
+  simp only [↓reduceIte, mul_one]
   rw [stdBasis_not_eq, η_off_diagonal h]
-  simp
+  simp only [mul_zero]
   exact fun a => h (id a.symm)
 
 lemma ηLin_mulVec_left (x y : spaceTime) (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
@@ -156,7 +156,7 @@ lemma ηLin_matrix_eq_identity_iff (Λ : Matrix (Fin 4) (Fin 4) ℝ) :
   apply Iff.intro
   intro h
   subst h
-  simp
+  simp only [ηLin_apply_apply, one_mulVec, implies_true]
   intro h
   funext μ ν
   have h1 := h (stdBasis μ) (stdBasis ν)