Numerous additions

Physicslib4.lean

@@ -54,6 +54,7 @@ import Physicslib4.GNS.UnitaryRepresentation
 import Physicslib4.Operators.Conjugation
 import Physicslib4.Operators.LpDiagonal
 import Physicslib4.Spacetime.Basic
+import Physicslib4.Spacetime.CausalComplement
 import Physicslib4.Spacetime.CausalStructure
 import Physicslib4.Spacetime.Causality
 import Physicslib4.Spacetime.Curves

Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean

@@ -5,6 +5,7 @@ Authors: Lean Community
 -/
 import Physicslib4.AQFT.HaagKastler.EinsteinCausality
 import Physicslib4.GNS.Irreducibility
+import Physicslib4.Spacetime.CausalComplement
 
 /-!
 # Local von Neumann algebras and spacelike commutation
@@ -89,12 +90,12 @@ theorem eq_zero_of_commute_of_cyclic {S : Set (H →L[ℂ] H)} {Ω : H}
   have hzero : Set.EqOn (⇑R) (fun _ => (0 : H)) ((fun T => T Ω) '' S) := by
     rintro _ ⟨T, hT, rfl⟩
     change R (T Ω) = 0
-    rw [← ContinuousLinearMap.mul_apply, hcomm T hT, ContinuousLinearMap.mul_apply, hRΩ,
+    rw [← mul_apply_eq_comp, hcomm T hT, mul_apply_eq_comp, hRΩ,
       map_zero]
   have hRx : (⇑R) = fun _ => (0 : H) :=
     Continuous.ext_on hcyc R.continuous continuous_const hzero
   exact ContinuousLinearMap.ext fun x =>
-    (congrFun hRx x).trans (ContinuousLinearMap.zero_apply x).symm
+    (congrFun hRx x).trans (zero_apply x).symm
 
 /-- **Statistical independence (Schlieder property), Minkowski spacetime.** If `Ω`
 is cyclic for the local observables of `B₁` - in Minkowski spacetime this
@@ -150,6 +151,21 @@ theorem localVonNeumannAlgebra_le_commutant
   simp only [coe_localVonNeumannAlgebra, VonNeumannAlgebra.coe_commutant]
   exact N.localVonNeumann_subset_centralizer π hB₁ hB₂ hs
 
+/-- **Additive-free locality (Minkowski).** A bounded region lying in the spacelike
+complement of `B` has its local algebra inside the commutant of `R(B)`: for basis
+sets `B' ⊆ B^⊥`, `R(B') ≤ R(B)'`. This repackages microcausality through the
+spacelike complement, keeping strictly to bounded (diamond) regions — no algebra is
+attached to the unbounded complement. -/
+theorem localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement
+    (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B B' : Set StandardMinkowskiSpacetime.Carrier⦄
+    (hB : IsAlexandrovBasisSet B) (hB' : IsAlexandrovBasisSet B')
+    (hsub : B' ⊆ Spacetime.spacelikeComplement StandardMinkowskiSpacetime
+      standardMinkowskiTimeOrientation B) :
+    N.localVonNeumannAlgebra π B' ≤ (N.localVonNeumannAlgebra π B).commutant :=
+  N.localVonNeumannAlgebra_le_commutant π hB' hB
+    ((Spacetime.subset_spacelikeComplement_iff _ _).mp hsub)
+
 /-- **Isotony, bundled (Minkowski).** `B₁ ⊆ B₂ ⟹ R(B₁) ≤ R(B₂)` as von Neumann
 algebras. -/
 theorem localVonNeumannAlgebra_mono

Physicslib4/AQFT/HaagKastler/Net.lean

@@ -269,7 +269,7 @@ the empty-region normalisation being the identity isomorphism. -/
 noncomputable def trivialLocalNet : LocalNet where
   algebra := fun _ => ℂ
   instCStarAlgebra := fun _ => inferInstance
-  emptyEquivComplex := StarAlgEquiv.refl
+  emptyEquivComplex := StarAlgEquiv.refl ℂ ℂ
 
 /-- A concrete Alexandrov-basis set of standard Minkowski spacetime
 (`I⁺(0) ∩ I⁻(0)`), used as a witness that basis sets exist. -/
@@ -310,7 +310,7 @@ theorem trivialLocalNet_quasilocalCompleteness :
 
 theorem trivialLocalNet_lorentzCovariance :
     LorentzCovariance trivialLocalNet := by
-  refine ⟨fun _ _ => StarAlgEquiv.refl, fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ,
+  refine ⟨fun _ _ => StarAlgEquiv.refl ℂ ℂ, fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ,
     ?_, ?_, ?_, ?_⟩
   · intro B₁ B₂ hB₁ hB₂ h a b hh; exact hh
   · intro _ _; rfl

Physicslib4/AQFT/HaagKastler/QuasilocalAction.lean

@@ -84,7 +84,6 @@ theorem QuasilocalLift.unique {Q : QuasilocalAlgebra N.U}
   intro x hx
   simp only [Set.mem_iUnion, Set.mem_range] at hx
   obtain ⟨B, hB, a, rfl⟩ := hx
-  change l₁.β (Q.ι B a) = l₂.β (Q.ι B a)
   rw [l₁.intertwines hB a, l₂.intertwines hB a]
 
 /-- The type of lifts of a fixed `L` is a subsingleton: a lift is determined by

Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean

@@ -402,8 +402,8 @@ inhabiting `QuasilocalLift`. -/
 noncomputable def quasilocalLift (hcov : IsCovariant N Q)
     (L : InhomogeneousLorentzGroup) : N.QuasilocalLift Q L where
   β := StarAlgEquiv.ofStarAlgHom (extendHom hcov L) (extendHom hcov L⁻¹)
-        (fun x => DFunLike.congr_fun (extendHom_inv_comp hcov L) x)
-        (fun x => DFunLike.congr_fun (extendHom_comp_inv hcov L) x)
+        (extendHom_inv_comp hcov L)
+        (extendHom_comp_inv hcov L)
   intertwines := by
     intro B hB a
     rw [StarAlgEquiv.ofStarAlgHom_apply]
@@ -476,7 +476,8 @@ theorem action_ι (C : CovariantQuasilocalAlgebra) (L : InhomogeneousLorentzGrou
 theorem action_apply (C : CovariantQuasilocalAlgebra)
     (L : InhomogeneousLorentzGroup) (x : C.quasilocal.carrier) :
     C.action L x = extendHom C.covariant L x :=
-  StarAlgEquiv.ofStarAlgHom_apply _ _ _ _ x
+  StarAlgEquiv.ofStarAlgHom_apply (extendHom C.covariant L) (extendHom C.covariant L⁻¹)
+    (extendHom_inv_comp C.covariant L) (extendHom_comp_inv C.covariant L) x
 
 /-- **The action is trivial at the identity:** `β_1 = id`. -/
 theorem action_one_apply (C : CovariantQuasilocalAlgebra)
@@ -495,7 +496,7 @@ theorem action_mul_apply (C : CovariantQuasilocalAlgebra)
 
 /-- The covariance action sends the identity to the identity automorphism. -/
 theorem action_one (C : CovariantQuasilocalAlgebra) :
-    C.action 1 = StarAlgEquiv.refl := by
+    C.action 1 = StarAlgEquiv.refl ℂ C.quasilocal.carrier := by
   ext x; rw [action_one_apply]; rfl
 
 /-- The covariance action is multiplicative: `β_{L'·L} = β_L` followed by

Physicslib4/AQFT/HaagKastlerCurved/Concrete.lean

@@ -5,8 +5,10 @@ Authors: Lean Community
 -/
 import Physicslib4.AQFT.HaagKastlerCurved.Spacetime
 import Physicslib4.AQFT.HaagKastlerCurved.Net
+import Physicslib4.AQFT.HaagKastlerCurved.LocalVonNeumann
 import Physicslib4.Spacetime.LorentzianSpacetime
 import Physicslib4.Spacetime.Isometry
+import Physicslib4.Spacetime.CausalComplement
 
 /-!
 # Bridging a concrete spacetime to the abstract Haag-Kastler interface
@@ -35,9 +37,16 @@ spacetime:
 * `Isom` is `Physicslib4.Spacetime.Isometry` of the underlying
   spacetime, with its `Group` and `MulAction` instances.
 
-The same deferred refinements noted on `Spacetime.Isometry` apply here:
-the isometry group is the full metric-preserving group (its
-identity-component restriction is not yet captured) and its bundled
+This bridge instantiates `Isom` with the *full* metric-preserving
+isometry group. The identity-component restriction of Axiom 5
+("isometries connected to the identity") is captured by the sibling
+bridge `toAbstractIdentityComponent`
+(`Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean`), which uses
+`Spacetime.Isometry.orientedIdentityComponent` (the topological
+`connectedComponentOfOne` intersected with future-orientation
+preservation); this full-group bridge is retained for the axioms that
+hold under the whole isometry group (e.g. microcausality). One deferred
+refinement noted on `Spacetime.Isometry` still applies: the bundled
 differential is not yet tied to the manifold derivative.
 -/
 
@@ -96,6 +105,26 @@ theorem commute_of_spacelike_mono_geometric
     (fun _ _ _ _ hh₁ hh₂ hh => L.isCompletelySpacelike_mono hh₁ hh₂ hh)
     hB₁' hB₂' hB hs hsub₁ hsub₂ h₁ h₂ a b
 
+/-- **Additive-free locality over a concrete spacetime.** The geometric
+specialisation of the curved additive-free locality: for a Haag-Kastler net over a
+concrete Lorentzian spacetime `L`, a bounded region `B₁` lying in the spacelike
+complement of `B₂` (both inside a common containing basis set `B`) has its local von
+Neumann algebra inside the commutant of `R(B₂)`. The Galois bridge
+`subset_spacelikeComplement_iff` discharges the spacelike hypothesis; no algebra is
+attached to the unbounded complement. -/
+theorem localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement_geometric
+    {L : Spacetime.LorentzianSpacetime} (N : HaagKastlerNet L.toAbstract)
+    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+    {B : Set L.toAbstract.Carrier} (hB : L.toAbstract.IsBasisSet B)
+    (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
+    ⦃B₁ B₂ : Set L.toAbstract.Carrier⦄
+    (hB₁ : L.toAbstract.IsBasisSet B₁) (hB₂ : L.toAbstract.IsBasisSet B₂)
+    (hsub : B₁ ⊆ L.spacelikeComplement B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) :
+    N.localVonNeumannAlgebra π hB₁ hB h₁
+      ≤ (N.localVonNeumannAlgebra π hB₂ hB h₂).commutant :=
+  N.localVonNeumannAlgebra_le_commutant hB π hB₁ hB₂
+    (L.subset_spacelikeComplement_iff.mp hsub) h₁ h₂
+
 end AQFT.HaagKastlerCurved.HaagKastlerNet
 
 end Physicslib4

Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean

@@ -107,12 +107,12 @@ theorem eq_zero_of_commute_of_cyclic {S : Set (H →L[ℂ] H)} {Ω : H}
   have hzero : Set.EqOn (⇑R) (fun _ => (0 : H)) ((fun T => T Ω) '' S) := by
     rintro _ ⟨T, hT, rfl⟩
     change R (T Ω) = 0
-    rw [← ContinuousLinearMap.mul_apply, hcomm T hT, ContinuousLinearMap.mul_apply, hRΩ,
+    rw [← mul_apply_eq_comp, hcomm T hT, mul_apply_eq_comp, hRΩ,
       map_zero]
   have hRx : (⇑R) = fun _ => (0 : H) :=
     Continuous.ext_on hcyc R.continuous continuous_const hzero
   exact ContinuousLinearMap.ext fun x =>
-    (congrFun hRx x).trans (ContinuousLinearMap.zero_apply x).symm
+    (congrFun hRx x).trans (zero_apply x).symm
 
 /-- **Statistical independence (Schlieder property) for spacelike curved regions.**
 If `Ω` is cyclic for the local observables of `B₁` - the role supplied in

Physicslib4/AQFT/HaagKastlerCurved/Net.lean

@@ -276,7 +276,7 @@ identity isomorphism. -/
 noncomputable def trivialLocalNet (M : LorentzianSpacetime) : LocalNet M where
   algebra := fun _ => ℂ
   instCStarAlgebra := fun _ => inferInstance
-  emptyEquivComplex := StarAlgEquiv.refl
+  emptyEquivComplex := StarAlgEquiv.refl ℂ ℂ
 
 theorem trivialLocalNet_isotony (M : LorentzianSpacetime) :
     Isotony (trivialLocalNet M) :=
@@ -295,7 +295,7 @@ theorem trivialLocalNet_localAlgebra (M : LorentzianSpacetime) :
 
 theorem trivialLocalNet_isometricCovariance (M : LorentzianSpacetime) :
     IsometricCovariance (trivialLocalNet M) := by
-  refine ⟨fun _ _ => StarAlgEquiv.refl, fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ,
+  refine ⟨fun _ _ => StarAlgEquiv.refl ℂ ℂ, fun _ _ _ _ _ => StarAlgHom.id ℂ ℂ,
     ?_, ?_, ?_, ?_⟩
   · intro _ _ _ _ h _ _ hh; exact hh
   · intro _ _; rfl

Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean

@@ -59,11 +59,11 @@ variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
 /-- Transport a local algebra along an equality of regions. -/
 noncomputable def algCongr {B₁ B₂ : Set M.Carrier} (h : B₁ = B₂) :
     N.algebra B₁ ≃⋆ₐ[ℂ] N.algebra B₂ := by
-  subst h; exact StarAlgEquiv.refl
+  subst h; exact StarAlgEquiv.refl ℂ (N.algebra B₁)
 
 theorem algCongr_apply {B₁ B₂ : Set M.Carrier} (h : B₁ = B₂) (a : N.algebra B₁) :
     N.algCongr h a = cast (congrArg N.algebra h) a := by
-  subst h; rfl
+  subst h; simp [algCongr]
 
 /-- **Stabilizer automorphism.** For an isometry `φ` fixing the region `B`
 (`φ·B = B`), the covariance equivalence `covEquiv φ B` lands back in `𝔘(B)` and

Physicslib4/Analysis/HorizontalLineRemovable.lean

@@ -156,7 +156,7 @@ theorem rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line (f : ℂ 
     intro z hz
     rw [Complex.mem_reProdIm] at hz
     obtain ⟨hre, him⟩ := hz
-    refine Set.mem_diff_of_mem (Complex.mem_reProdIm.mpr ⟨Set.Ioo_subset_Icc_self hre, ?_⟩) ?_
+    refine Set.mem_sdiff_of_mem (Complex.mem_reProdIm.mpr ⟨Set.Ioo_subset_Icc_self hre, ?_⟩) ?_
     · exact Set.mem_Icc.mpr ⟨him.1.le, him.2.le.trans hℓd⟩
     · simp only [Set.mem_setOf_eq]; exact ne_of_lt him.2
   -- The upper piece `[a,b] × [ℓ,d]`: holomorphic interior has `im > ℓ`.
@@ -167,7 +167,7 @@ theorem rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line (f : ℂ 
     intro z hz
     rw [Complex.mem_reProdIm] at hz
     obtain ⟨hre, him⟩ := hz
-    refine Set.mem_diff_of_mem (Complex.mem_reProdIm.mpr ⟨Set.Ioo_subset_Icc_self hre, ?_⟩) ?_
+    refine Set.mem_sdiff_of_mem (Complex.mem_reProdIm.mpr ⟨Set.Ioo_subset_Icc_self hre, ?_⟩) ?_
     · exact Set.mem_Icc.mpr ⟨hcℓ.trans him.1.le, him.2.le⟩
     · simp only [Set.mem_setOf_eq]; exact (ne_of_lt him.1).symm
   rw [hlow, hupp, add_zero]
@@ -225,7 +225,7 @@ theorem rectIntegralReal_eq_zero_of_subset {U : Set ℂ} (ℓ : ℝ)
       · -- `c ≤ ℓ ≤ d`: straddling vanishing
         refine rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line f a b c d ℓ
           hab hcℓ hℓd hcont (hd.mono (fun z hz => ?_))
-        refine Set.mem_diff_of_mem (hsub ?_) hz.2
+        refine Set.mem_sdiff_of_mem (hsub ?_) hz.2
         rw [Complex.mem_reProdIm, Set.uIcc_of_le hab, Set.uIcc_of_le hcd]
         exact Complex.mem_reProdIm.mp hz.1
       · -- `d < ℓ`: line above the rectangle, plain Cauchy-Goursat
@@ -234,14 +234,14 @@ theorem rectIntegralReal_eq_zero_of_subset {U : Set ℂ} (ℓ : ℝ)
         rw [min_eq_left hab, max_eq_right hab, min_eq_left hcd, max_eq_right hcd]
         intro z hz
         rw [Complex.mem_reProdIm] at hz
-        exact Set.mem_diff_of_mem (hsub (hmem_open z hz.1 hz.2)) (ne_of_lt (hz.2.2.trans_le hdℓ))
+        exact Set.mem_sdiff_of_mem (hsub (hmem_open z hz.1 hz.2)) (ne_of_lt (hz.2.2.trans_le hdℓ))
     · -- `ℓ < c`: line below the rectangle, plain Cauchy-Goursat
       refine rectIntegralReal_eq_zero_of_continuousOn_of_differentiableOn f a b c d
         hcont (hd.mono ?_)
       rw [min_eq_left hab, max_eq_right hab, min_eq_left hcd, max_eq_right hcd]
       intro z hz
       rw [Complex.mem_reProdIm] at hz
-      exact Set.mem_diff_of_mem (hsub (hmem_open z hz.1 hz.2))
+      exact Set.mem_sdiff_of_mem (hsub (hmem_open z hz.1 hz.2))
         (ne_of_lt (lt_of_le_of_lt hℓc hz.2.1)).symm
   rcases le_total a b with hab | hab <;> rcases le_total c d with hcd | hcd
   · exact ordered a b c d hab hcd hsub
@@ -316,7 +316,7 @@ theorem frontier_setOf_im_lt (c : ℝ) :
       = closure {z : ℂ | z.im < c} \ interior {z : ℂ | z.im < c} from rfl,
     closure_setOf_im_lt, (isOpen_setOf_im_lt c).interior_eq]
   ext z
-  simp only [Set.mem_diff, Set.mem_setOf_eq, not_lt]
+  simp only [Set.mem_sdiff, Set.mem_setOf_eq, not_lt]
   exact ⟨fun ⟨h1, h2⟩ => le_antisymm h1 h2, fun h => ⟨h.le, h.ge⟩⟩
 
 /-- **Holomorphic gluing across a horizontal line (Schwarz-reflection form).**

Physicslib4/GNS/Amplification.lean

@@ -60,10 +60,10 @@ theorem not_isIrreducible_directSum {j k : ι} (hjk : j ≠ k)
     exact norm_ne_zero_iff.mpr hw
   have e1 := DFunLike.congr_fun hc (lp.single 2 j v)
   have e2 := DFunLike.congr_fun hc (lp.single 2 k w)
-  simp only [summandProj_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply,
+  simp only [summandProj_apply, smul_apply, one_apply_eq_self,
     lp.single_apply_self] at e1
   simp only [summandProj_apply, lp.single_apply_ne 2 k w hjk, lp.single_zero,
-    ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply] at e2
+    smul_apply, one_apply_eq_self] at e2
   have hc1 : c = 1 := by
     have h0 : (1 - c) • lp.single 2 j v = 0 := by rw [sub_smul, one_smul, ← e1, sub_self]
     rcases smul_eq_zero.mp h0 with h | h

Physicslib4/GNS/Basic.lean

@@ -66,7 +66,7 @@ variable {A}
 
 noncomputable instance : FunLike (State A) A ℂ where
   coe ω := ω.toContinuousLinearMap
-  coe_injective' := by
+  coe_injective := by
     intro ω₁ ω₂ h
     cases ω₁
     cases ω₂

Physicslib4/GNS/Construction.lean

@@ -195,12 +195,12 @@ theorem gns_unique {A : Type*} [CStarAlgebra A] (ω : State A)
       U Ω₁ = Ω₂ ∧ ∀ (a : A) (x : H₁), U (π₁ a x) = π₂ a (U x) := by
   let e₁ : A →ₗ[ℂ] H₁ :=
     { toFun := fun a => π₁ a Ω₁
-      map_add' := fun a b => by simp [map_add, ContinuousLinearMap.add_apply]
-      map_smul' := fun c a => by simp [map_smul, ContinuousLinearMap.smul_apply] }
+      map_add' := fun a b => by simp [map_add, add_apply]
+      map_smul' := fun c a => by simp [map_smul, smul_apply] }
   let e₂ : A →ₗ[ℂ] H₂ :=
     { toFun := fun a => π₂ a Ω₂
-      map_add' := fun a b => by simp [map_add, ContinuousLinearMap.add_apply]
-      map_smul' := fun c a => by simp [map_smul, ContinuousLinearMap.smul_apply] }
+      map_add' := fun a b => by simp [map_add, add_apply]
+      map_smul' := fun c a => by simp [map_smul, smul_apply] }
   have hdense₁ : DenseRange e₁ := hcyc₁
   have hdense₂ : DenseRange e₂ := hcyc₂
   have hinner_eq : ∀ a b : A, ⟪e₁ a, e₁ b⟫_ℂ = ⟪e₂ a, e₂ b⟫_ℂ := by
@@ -209,11 +209,11 @@ theorem gns_unique {A : Type*} [CStarAlgebra A] (ω : State A)
     have h1 : ⟪π₁ a Ω₁, π₁ b Ω₁⟫_ℂ = ⟪Ω₁, π₁ (star a * b) Ω₁⟫_ℂ := by
       rw [← ContinuousLinearMap.adjoint_inner_right,
           ← ContinuousLinearMap.star_eq_adjoint, ← map_star]
-      rw [map_mul, ContinuousLinearMap.mul_apply]
+      rw [map_mul, mul_apply_eq_comp]
     have h2 : ⟪π₂ a Ω₂, π₂ b Ω₂⟫_ℂ = ⟪Ω₂, π₂ (star a * b) Ω₂⟫_ℂ := by
       rw [← ContinuousLinearMap.adjoint_inner_right,
           ← ContinuousLinearMap.star_eq_adjoint, ← map_star]
-      rw [map_mul, ContinuousLinearMap.mul_apply]
+      rw [map_mul, mul_apply_eq_comp]
     rw [h1, h2, ← hrep₁, ← hrep₂]
   have hnorm : ∀ a : A, ‖e₂ a‖ = ‖e₁ a‖ := by
     intro a

Physicslib4/GNS/DirectSum.lean

@@ -64,7 +64,7 @@ noncomputable def directSum : A →⋆ₐ[ℂ] (lp H 2 →L[ℂ] lp H 2) where
   toFun := directSumFun π
   map_one' := by refine lpDiag_ext fun x i => ?_; simp [map_one]
   map_mul' a b := by
-    refine lpDiag_ext fun x i => ?_; simp [map_mul, ContinuousLinearMap.mul_apply]
+    refine lpDiag_ext fun x i => ?_; simp [map_mul, mul_apply_eq_comp]
   map_zero' := by
     refine lpDiag_ext fun x i => ?_
     change π i 0 (x i) = (0 : lp H 2) i
@@ -75,8 +75,8 @@ noncomputable def directSum : A →⋆ₐ[ℂ] (lp H 2 →L[ℂ] lp H 2) where
     rw [map_add (π i) a b]; rfl
   commutes' r := by
     refine lpDiag_ext fun x i => ?_
-    simp [Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.smul_apply,
-      ContinuousLinearMap.one_apply, lp.coeFn_smul]
+    simp [Algebra.algebraMap_eq_smul_one, smul_apply,
+      one_apply_eq_self, lp.coeFn_smul]
   map_star' a := by
     simp only [directSumFun]
     rw [lpDiag_star]
@@ -118,7 +118,7 @@ theorem summandProj_mem_commutant (j : ι) :
   rw [Set.mem_centralizer_iff]
   rintro _ ⟨a, rfl⟩
   refine lpDiag_ext fun x i => ?_
-  simp only [ContinuousLinearMap.mul_apply, directSum_apply, directSumFun_apply_coe,
+  simp only [mul_apply_eq_comp, directSum_apply, directSumFun_apply_coe,
     summandProj_apply, lp.single_apply]
   rcases eq_or_ne i j with h | h
   · subst h; simp