feat(Lorentz.Vector): mark Vector and CoVector implicit_reducible, add inner_eq_sum

Physlib/Relativity/Tensors/RealTensor/CoVector/Basic.lean

@@ -28,9 +28,13 @@ noncomputable section
 
 namespace Lorentz
 
-/-- Real contravariant Lorentz vector. -/
+/-- Real covariant Lorentz vector. -/
+@[implicit_reducible]
 def CoVector (d : ℕ := 3) := Fin 1 ⊕ Fin d → ℝ
 
+/- As for `Vector`, `CoVector d` is applied directly as a function throughout the library;
+  marking it implicit-reducible lets such applications typecheck at implicit transparency. -/
+
 namespace CoVector
 
 instance {d} : AddCommMonoid (CoVector d) :=
@@ -89,6 +93,7 @@ instance (d : ℕ) : Inner ℝ (CoVector d) where
 
 lemma inner_eq_equivEuclid (d : ℕ) (v w : CoVector d) :
     ⟪v, w⟫_ℝ = ⟪equivEuclid d v, equivEuclid d w⟫_ℝ := rfl
+
 /-- The Euclidean inner product structure on `CoVector`. -/
 instance innerProductSpace (d : ℕ) : InnerProductSpace ℝ (CoVector d) where
   norm_sq_eq_re_inner v := by
@@ -148,14 +153,14 @@ def basis {d : ℕ} : Basis (Fin 1 ⊕ Fin d) ℝ (CoVector d) :=
 lemma basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) :
     basis μ ν = if μ = ν then 1 else 0 := by
   simp [basis]
-  erw [Pi.basisFun_apply, Pi.single_apply]
+  rw [Pi.basisFun_apply, Pi.single_apply]
   congr 1
   exact Lean.Grind.eq_congr' rfl rfl
 
 lemma basis_repr_apply {d : ℕ} (p : CoVector d) (μ : Fin 1 ⊕ Fin d) :
     basis.repr p μ = p μ := by
   simp [basis]
-  erw [Pi.basisFun_repr]
+  rw [Pi.basisFun_repr]
 
 lemma map_apply_eq_basis_mulVec {d : ℕ} (f : CoVector d →ₗ[ℝ] CoVector d) (p : CoVector d) :
     (f p) = (LinearMap.toMatrix basis basis) f *ᵥ p := by

Physlib/Relativity/Tensors/RealTensor/CoVector/Representation.lean

@@ -71,7 +71,6 @@ lemma rep_injective (d : ℕ) (Λ : LorentzGroup d) : Function.Injective (rep Λ
   rw [rep_apply_eq_mulVec, rep_apply_eq_mulVec] at h
   exact Matrix.mulVec_injective_of_isUnit (isUnit_of_invertible _) h
 
-set_option backward.isDefEq.respectTransparency false in
 lemma rep_surjective (d : ℕ) (Λ : LorentzGroup d) : Function.Surjective (rep Λ) := by
   intro v
   use (LorentzGroup.transpose Λ) *ᵥ v

Physlib/Relativity/Tensors/RealTensor/CoVector/Tensorial.lean

@@ -154,7 +154,6 @@ lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : CoV
   · intro t1 t2 h1 h2
     simp only [actionT_add, map_add, h1, h2, apply_add, mul_add, Finset.sum_add_distrib]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : CoVector d) :
     Λ • p = (LorentzGroup.transpose Λ⁻¹).1 *ᵥ p := by
   funext i
@@ -166,18 +165,15 @@ lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : CoVector d) :
 lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : CoVector d) :
     Λ • (p + q) = Λ • p + Λ • q := by simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : CoVector d) :
     Λ • (p - q) = Λ • p - Λ • q := by
   rw [smul_eq_mulVec, smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_sub]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) :
     Λ • (0 : CoVector d) = 0 := by
   rw [smul_eq_mulVec, Matrix.mulVec_zero]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) :
     Λ • (-p) = - (Λ • p) := by
   rw [smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_neg]
@@ -195,7 +191,6 @@ def actionCLM {d : ℕ} (Λ : LorentzGroup d) :
 lemma actionCLM_apply {d : ℕ} (Λ : LorentzGroup d) (p : CoVector d) :
     actionCLM Λ p = Λ • p := rfl
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
     Λ • basis μ = ∑ ν, Λ⁻¹.1 μ ν • basis ν := by
   funext i

Physlib/Relativity/Tensors/RealTensor/Representation/Contraction.lean

@@ -40,7 +40,6 @@ TODO "In a similar way to `Vector.contract` and `CoVector.contract`,
   we want to define metrics and units as intertwining maps of representations.
   This should copy (and eventually replace) the definitions e.g. `./Units/Pre.lean`."
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The intertwining map defining the contraction of a contravariant Lorentz vector with a
   covariant Lorentz vector. -/
 def Vector.contract : (Vector.rep.tprod CoVector.rep).IntertwiningMap
@@ -61,7 +60,6 @@ def Vector.contract : (Vector.rep.tprod CoVector.rep).IntertwiningMap
         vecMul_transpose, mulVec_mulVec, LorentzGroup.coe_inv, inv_mul_of_invertible Λ.1]
       rfl
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The intertwining map defining the contraction of a covariant Lorentz vector with a
   contravariant Lorentz vector. -/
 def CoVector.contract : (CoVector.rep.tprod Vector.rep).IntertwiningMap
@@ -94,19 +92,15 @@ lemma Vector.contract_tmul (φ : Vector d) (ψ : CoVector d) :
 lemma CoVector.contract_tmul (φ : CoVector d) (ψ : Vector d) :
     CoVector.contract (φ ⊗ₜ ψ) = ∑ i, φ i * ψ i := rfl
 
-set_option backward.isDefEq.respectTransparency false in
 lemma Vector.contract_basis_left (μ : Fin 1 ⊕ Fin d) (ψ : CoVector d) :
     Vector.contract (basis μ ⊗ₜ ψ) = ψ μ := by simp [Vector.contract_tmul, basis_apply]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma CoVector.contract_basis_left (μ : Fin 1 ⊕ Fin d) (φ : Vector d) :
     CoVector.contract (basis μ ⊗ₜ φ) = φ μ := by simp [CoVector.contract_tmul, basis_apply]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma Vector.contract_basis_right (φ : Vector d) (μ : Fin 1 ⊕ Fin d) :
     Vector.contract (φ ⊗ₜ basis μ) = φ μ := by simp [Vector.contract_tmul, basis_apply]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma CoVector.contract_basis_right (ψ : CoVector d) (μ : Fin 1 ⊕ Fin d) :
     CoVector.contract (ψ ⊗ₜ basis μ) = ψ μ := by simp [CoVector.contract_tmul, basis_apply]
 

Physlib/Relativity/Tensors/RealTensor/Vector/Basic.lean

@@ -29,8 +29,14 @@ noncomputable section
 namespace Lorentz
 
 /-- Real contravariant Lorentz vector. -/
+@[implicit_reducible]
 def Vector (d : ℕ := 3) := Fin 1 ⊕ Fin d → ℝ
 
+/- `Vector d` is applied directly as a function throughout the library. Marking it
+  implicit-reducible lets such applications typecheck at implicit transparency, so that
+  `rw` and `simp` can match patterns containing them (see the Lean 4.33 release notes on
+  `backward.isDefEq.respectTransparency.types`). -/
+
 namespace Vector
 
 instance {d} : AddCommMonoid (Vector d) :=
@@ -116,6 +122,11 @@ instance innerProductSpace (d : ℕ) : InnerProductSpace ℝ (Vector d) where
     simp only [inner_eq_equivEuclid, map_smul]
     exact InnerProductSpace.smul_left (equivEuclid d x) (equivEuclid d y) r
 
+/-- The inner product on `Vector d` as a sum over components. -/
+lemma inner_eq_sum {d : ℕ} (v w : Vector d) : ⟪v, w⟫_ℝ = ∑ μ, v μ * w μ := by
+  rw [inner_eq_equivEuclid, PiLp.inner_apply]
+  simp [mul_comm]
+
 /-- The instance of a `ChartedSpace` on `Vector d`. -/
 instance : ChartedSpace (Vector d) (Vector d) := chartedSpaceSelf (Vector d)
 
@@ -278,14 +289,14 @@ def basis {d : ℕ} : Basis (Fin 1 ⊕ Fin d) ℝ (Vector d) :=
 lemma basis_apply {d : ℕ} (μ ν : Fin 1 ⊕ Fin d) :
     basis μ ν = if μ = ν then 1 else 0 := by
   simp [basis]
-  erw [Pi.basisFun_apply, Pi.single_apply]
+  rw [Pi.basisFun_apply, Pi.single_apply]
   congr 1
   exact Lean.Grind.eq_congr' rfl rfl
 
 lemma basis_repr_apply {d : ℕ} (p : Vector d) (μ : Fin 1 ⊕ Fin d) :
     basis.repr p μ = p μ := by
   simp [basis]
-  erw [Pi.basisFun_repr]
+  rw [Pi.basisFun_repr]
 
 lemma map_apply_eq_basis_mulVec {d : ℕ} (f : Vector d →ₗ[ℝ] Vector d) (p : Vector d) :
     (f p) = (LinearMap.toMatrix basis basis) f *ᵥ p := by
@@ -431,19 +442,13 @@ def asSmoothManifold (d : ℕ) : ModelWithCorners ℝ (Vector d) (Vector d) := 
 -/
 open InnerProductSpace
 
-set_option backward.isDefEq.respectTransparency false in
 lemma basis_inner {d : ℕ} (μ : Fin 1 ⊕ Fin d) (p : Lorentz.Vector d) :
     ⟪Lorentz.Vector.basis μ, p⟫_ℝ = p μ := by
-  simp [inner_eq_equivEuclid]
-  rw [PiLp.inner_apply]
-  simp [-Fintype.sum_sum_type]
+  simp [inner_eq_sum]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma inner_basis {d : ℕ} (p : Lorentz.Vector d) (μ : Fin 1 ⊕ Fin d) :
     ⟪p, Lorentz.Vector.basis μ⟫_ℝ = p μ := by
-  simp [inner_eq_equivEuclid]
-  rw [PiLp.inner_apply]
-  simp [-Fintype.sum_sum_type]
+  simp [inner_eq_sum]
 
 end Vector
 

Physlib/Relativity/Tensors/RealTensor/Vector/Representation.lean

@@ -60,7 +60,6 @@ lemma rep_toMatrix (d : ℕ) (Λ : LorentzGroup d) :
 lemma rep_injective (d : ℕ) (Λ : LorentzGroup d) : Function.Injective (rep Λ) :=
   fun _ _ h => Matrix.mulVec_injective_of_isUnit (isUnit_of_invertible Λ.1) h
 
-set_option backward.isDefEq.respectTransparency false in
 lemma rep_surjective (d : ℕ) (Λ : LorentzGroup d) : Function.Surjective (rep Λ) :=
   fun v => ⟨Λ⁻¹ *ᵥ v, by simp [rep_apply_eq_mulVec]⟩
 

Physlib/Relativity/Tensors/RealTensor/Vector/Tensorial.lean

@@ -151,7 +151,6 @@ lemma smul_eq_sum {d : ℕ} (i : Fin 1 ⊕ Fin d) (Λ : LorentzGroup d) (p : Vec
   · intro t1 t2 h1 h2
     simp only [actionT_add, map_add, apply_add, h1, h2, mul_add, Finset.sum_add_distrib]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : Vector d) :
     Λ • p = Λ.1 *ᵥ p := by
   funext i
@@ -162,18 +161,15 @@ lemma smul_eq_mulVec {d} (Λ : LorentzGroup d) (p : Vector d) :
 lemma smul_add {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) :
     Λ • (p + q) = Λ • p + Λ • q := by simp
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma smul_sub {d : ℕ} (Λ : LorentzGroup d) (p q : Vector d) :
     Λ • (p - q) = Λ • p - Λ • q := by
   rw [smul_eq_mulVec, smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_sub]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_zero {d : ℕ} (Λ : LorentzGroup d) :
     Λ • (0 : Vector d) = 0 := by
   rw [smul_eq_mulVec, Matrix.mulVec_zero]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_neg {d : ℕ} (Λ : LorentzGroup d) (p : Vector d) :
     Λ • (-p) = - (Λ • p) := by
   rw [smul_eq_mulVec, smul_eq_mulVec, Matrix.mulVec_neg]
@@ -183,7 +179,6 @@ lemma neg_smul {d} (Λ : LorentzGroup d) (p : Vector d) :
   funext i
   simp [smul_eq_sum, neg_apply]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma _root_.LorentzGroup.eq_of_action_vector_eq {d : ℕ}
     {Λ Λ' : LorentzGroup d} (h : ∀ p : Vector d, Λ • p = Λ' • p) :
     Λ = Λ' := by
@@ -221,7 +216,6 @@ lemma actionCLM_surjective {d : ℕ} (Λ : LorentzGroup d) :
   use (actionCLM Λ⁻¹) x1
   simp [actionCLM_apply]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma smul_basis {d : ℕ} (Λ : LorentzGroup d) (μ : Fin 1 ⊕ Fin d) :
     Λ • basis μ = ∑ ν, Λ.1 ν μ • basis ν := by
   funext i