Upgrade to Lean and Mathlib v4.34.1

Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean

@@ -212,7 +212,7 @@ theorem intertwiner_ι (N : HaagKastlerNet) (Q : QuasilocalAlgebra N.U N.isotony
       ∃ a' : N.U.algebra B', Q.ι hB' a' = Q.ι hB a :=
     ⟨B, hB, a, rfl⟩
   unfold intertwiner
-  rw [dif_pos h₀]
+  rw [dite_eq_left h₀]
   exact ι_covEquiv_congr N Q L h₀.choose_spec.1 hB h₀.choose_spec.2.choose a
     h₀.choose_spec.2.choose_spec
 

Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean

@@ -179,7 +179,7 @@ theorem quasilocalObservables_eq {U : LocalNet} {i : Isotony U} (Q : QuasilocalA
     quasilocalObservables Q π
       = (selfAdjoint (H →L[ℂ] H) : Set (H →L[ℂ] H)) ∩ Set.range π := by
   ext T
-  simp only [quasilocalObservables, Set.mem_setOf_eq, isQuasilocalObservable_iff,
+  simp only [quasilocalObservables, Set.mem_ofPred_eq, isQuasilocalObservable_iff,
     Set.mem_inter_iff, SetLike.mem_coe, selfAdjoint.mem_iff, isSelfAdjoint_iff]
 
 section ObservablesSet

Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean

@@ -210,7 +210,7 @@ theorem localObservables_eq {U : LocalNet M} {B : Set M.Carrier} {H : Type}
     localObservables π
       = (selfAdjoint (H →L[ℂ] H) : Set (H →L[ℂ] H)) ∩ Set.range π := by
   ext T
-  simp only [localObservables, Set.mem_setOf_eq, isLocalObservable_iff,
+  simp only [localObservables, Set.mem_ofPred_eq, isLocalObservable_iff,
     Set.mem_inter_iff, SetLike.mem_coe, selfAdjoint.mem_iff, isSelfAdjoint_iff]
 
 section ObservablesSet

Physicslib4/Analysis/CStarDenseExtend.lean

@@ -41,7 +41,7 @@ theorem exists_starAlgHom_extend_of_dense
     ∃ F : A →⋆ₐ[ℂ] B, Continuous F ∧ ∀ x : S, F (x : A) = f x := by
   have hue : IsUniformInducing ((↑) : S → A) := isUniformInducing_val (S : Set A)
   have hdr : DenseRange ((↑) : S → A) := by
-    simpa only [DenseRange, Subtype.range_coe_subtype, SetLike.setOf_mem_eq] using hS
+    simpa only [DenseRange, Subtype.range_coe_subtype, SetLike.setOfPred_mem_eq] using hS
   set F₀ : A → B := (hue.isDenseInducing hdr).extend (f : S → B) with hF₀def
   have hcont : Continuous F₀ :=
     (uniformContinuous_uniformly_extend hue hdr hf).continuous

Physicslib4/Analysis/HorizontalLineRemovable.lean

@@ -158,7 +158,7 @@ theorem rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line (f : ℂ 
     obtain ⟨hre, him⟩ := hz
     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
+    · simp only [Set.mem_ofPred_eq]; exact ne_of_lt him.2
   -- The upper piece `[a,b] × [ℓ,d]`: holomorphic interior has `im > ℓ`.
   have hupp : rectIntegralReal f a b ℓ d = 0 := by
     refine rectIntegralReal_eq_zero_of_continuousOn_of_differentiableOn f a b ℓ d
@@ -169,7 +169,7 @@ theorem rectIntegralReal_eq_zero_of_continuousOn_off_horizontal_line (f : ℂ 
     obtain ⟨hre, him⟩ := hz
     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
+    · simp only [Set.mem_ofPred_eq]; exact (ne_of_lt him.1).symm
   rw [hlow, hupp, add_zero]
 
 /-- Swapping the real bounds negates the rectangle contour integral. -/
@@ -286,7 +286,7 @@ theorem isOpen_setOf_im_lt (c : ℝ) : IsOpen {z : ℂ | z.im < c} :=
 theorem closure_setOf_im_lt (c : ℝ) :
     closure {z : ℂ | z.im < c} = {z : ℂ | z.im ≤ c} := by
   apply Set.Subset.antisymm
-  · exact closure_minimal (Set.setOf_subset_setOf.mpr fun z h => le_of_lt h)
+  · exact closure_minimal (Set.ofPred_subset_ofPred.mpr fun z h => le_of_lt h)
       (isClosed_le Complex.continuous_im continuous_const)
   · intro z hz
     rw [Metric.mem_closure_iff]
@@ -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_sdiff, Set.mem_setOf_eq, not_lt]
+  simp only [Set.mem_sdiff, Set.mem_ofPred_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).**
@@ -342,28 +342,28 @@ theorem differentiableOn_if_of_eqOn_horizontal_line [CompleteSpace E] {U : Set 
   have hcont : ContinuousOn (fun z => if z.im < ℓ then g z else h z) U := by
     apply ContinuousOn.if
     · intro z hz
-      rw [Set.mem_inter_iff, frontier_setOf_im_lt, Set.mem_setOf_eq] at hz
+      rw [Set.mem_inter_iff, frontier_setOf_im_lt, Set.mem_ofPred_eq] at hz
       exact hglue z hz.1 hz.2
     · rw [closure_setOf_im_lt]; exact hgc
     · rw [closure_setOf_not_im_lt]; exact hhc
   have hdiff : DifferentiableOn ℂ (fun z => if z.im < ℓ then g z else h z)
       (U \ {z : ℂ | z.im = ℓ}) := by
     intro z hz
     obtain ⟨hzU, hzne⟩ := hz
-    rw [Set.mem_setOf_eq] at hzne
+    rw [Set.mem_ofPred_eq] at hzne
     rcases lt_or_gt_of_ne hzne with hlt | hgt
     · have hopen : IsOpen (U ∩ {w : ℂ | w.im < ℓ}) := hU.inter (isOpen_setOf_im_lt ℓ)
       have hgat : DifferentiableAt ℂ g z := hgd.differentiableAt (hopen.mem_nhds ⟨hzU, hlt⟩)
       have heq : (fun z => if z.im < ℓ then g z else h z) =ᶠ[nhds z] g := by
         filter_upwards [(isOpen_setOf_im_lt ℓ).mem_nhds hlt] with w hw
-        simp only [if_pos hw]
+        simp only [ite_eq_left hw]
       exact (heq.differentiableAt_iff.mpr hgat).differentiableWithinAt
     · have hopen : IsOpen (U ∩ {w : ℂ | ℓ < w.im}) :=
         hU.inter (isOpen_lt continuous_const Complex.continuous_im)
       have hhat : DifferentiableAt ℂ h z := hhd.differentiableAt (hopen.mem_nhds ⟨hzU, hgt⟩)
       have heq : (fun z => if z.im < ℓ then g z else h z) =ᶠ[nhds z] h := by
         filter_upwards [(isOpen_lt continuous_const Complex.continuous_im).mem_nhds hgt] with w hw
-        simp only [if_neg (not_lt.mpr (le_of_lt hw))]
+        simp only [ite_eq_right (not_lt.mpr (le_of_lt hw))]
       exact (heq.differentiableAt_iff.mpr hhat).differentiableWithinAt
   exact differentiableOn_of_continuousOn_off_horizontal_line hU ℓ _ hcont hdiff
 

Physicslib4/Analysis/StripPeriodicExtension.lean

@@ -161,16 +161,16 @@ theorem pext_differentiableAt_online (hβ : 0 < β)
   have hHeq : ∀ w ∈ B, pext β F w = if w.im < c then g w else h w := by
     intro w hwB
     by_cases hwc : w.im < c
-    · rw [if_pos hwc]; simp only [pext, pshift, hfloor_lo w hwB hwc, hgdef]
-    · rw [if_neg hwc]; rw [not_lt] at hwc
+    · rw [ite_eq_left hwc]; simp only [pext, pshift, hfloor_lo w hwB hwc, hgdef]
+    · rw [ite_eq_right hwc]; rw [not_lt] at hwc
       simp only [pext, pshift, hfloor_hi w hwB hwc, hhdef]
   -- continuity of the glued model on the ball
   have hcont' : ContinuousOn (pext β F) B := by
     have hif : ContinuousOn (fun w => if w.im < c then g w else h w) B := by
       apply ContinuousOn.if
       · -- agreement on the line `Im = c`
         intro w hw
-        rw [Set.mem_inter_iff, frontier_setOf_im_lt, Set.mem_setOf_eq] at hw
+        rw [Set.mem_inter_iff, frontier_setOf_im_lt, Set.mem_ofPred_eq] at hw
         obtain ⟨_, hwc⟩ := hw
         have e1 : w - ((n₀ - 1 : ℤ) : ℂ) * ((β : ℂ) * Complex.I)
             = (↑w.re : ℂ) + (↑β : ℂ) * Complex.I := by
@@ -199,9 +199,9 @@ theorem pext_differentiableAt_online (hβ : 0 < β)
             (B ∩ {w : ℂ | w.im ≤ c}) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β} := by
           intro w hw
           obtain ⟨hwB, hwle⟩ := hw
-          rw [Set.mem_setOf_eq] at hwle
+          rw [Set.mem_ofPred_eq] at hwle
           have hb := hbound w hwB; rw [abs_lt, hz₀im] at hb
-          rw [Set.mem_setOf_eq, sub_intMul_im]
+          rw [Set.mem_ofPred_eq, sub_intMul_im]
           push_cast
           have e : ((n₀ : ℝ) - 1) * β = (n₀ : ℝ) * β - β := by ring
           rw [hc] at hwle
@@ -217,9 +217,9 @@ theorem pext_differentiableAt_online (hβ : 0 < β)
             (B ∩ {w : ℂ | c ≤ w.im}) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ β} := by
           intro w hw
           obtain ⟨hwB, hwge⟩ := hw
-          rw [Set.mem_setOf_eq] at hwge
+          rw [Set.mem_ofPred_eq] at hwge
           have hb := hbound w hwB; rw [abs_lt, hz₀im] at hb
-          rw [Set.mem_setOf_eq, sub_intMul_im]
+          rw [Set.mem_ofPred_eq, sub_intMul_im]
           rw [hc] at hwge
           refine ⟨by linarith [hwge], ?_⟩
           have e : ((n₀ : ℝ) + 1) * β = (n₀ : ℝ) * β + β := by ring
@@ -231,7 +231,7 @@ theorem pext_differentiableAt_online (hβ : 0 < β)
     intro w hw
     refine (pext_differentiableAt_offline hβ hdiff ?_).differentiableWithinAt
     obtain ⟨hwB, hwne⟩ := hw
-    rw [Set.mem_setOf_eq] at hwne
+    rw [Set.mem_ofPred_eq] at hwne
     rw [pshift_im]
     have hb := hbound w hwB; rw [abs_lt, hz₀im] at hb
     rcases lt_or_gt_of_ne hwne with hlt | hgt

Physicslib4/GNS/Construction.lean

@@ -86,6 +86,7 @@ theorem gns_construction.{u} {A : Type u} [CStarAlgebra A] (ω : State A) :
             ContinuousLinearMap.completion_apply_coe,
             PositiveLinearMap.leftMulMapPreGNS_apply,
             PositiveLinearMap.ofPreGNS, PositiveLinearMap.toPreGNS]
+      exact congrArg _ (congrArg _ (mul_one _))
     rw [show (Set.range fun a : A => f.gnsStarAlgHom a
               ((f.toPreGNS 1 : f.PreGNS) : f.GNS))
             = Set.range (fun a : A => ((f.toPreGNS a : f.PreGNS) : f.GNS)) by
@@ -112,6 +113,7 @@ theorem gns_construction.{u} {A : Type u} [CStarAlgebra A] (ω : State A) :
             ContinuousLinearMap.completion_apply_coe,
             PositiveLinearMap.leftMulMapPreGNS_apply,
             PositiveLinearMap.ofPreGNS, PositiveLinearMap.toPreGNS]
+      exact congrArg _ (congrArg _ (mul_one _))
     rw [hkey, UniformSpace.Completion.inner_coe,
         PositiveLinearMap.preGNS_inner_def]
     change (ω a : ℂ) = f (star (f.ofPreGNS (f.toPreGNS 1)) * f.ofPreGNS (f.toPreGNS a))
@@ -131,6 +133,7 @@ theorem gns_construction.{u} {A : Type u} [CStarAlgebra A] (ω : State A) :
             ContinuousLinearMap.completion_apply_coe,
             PositiveLinearMap.leftMulMapPreGNS_apply,
             PositiveLinearMap.ofPreGNS, PositiveLinearMap.toPreGNS]
+      exact congrArg _ (congrArg _ (mul_one _))
     have happ : f.gnsStarAlgHom (a - b) ((f.toPreGNS 1 : f.PreGNS) : f.GNS) = 0 := by
       rw [hsub]; rfl
     rw [hkey] at happ

Physicslib4/GNS/DirectSum.lean

@@ -43,7 +43,9 @@ noncomputable def lpEvalCLM (j : ι) : lp H 2 →L[ℂ] H j :=
       map_add' := fun _ _ => rfl
       map_smul' := fun _ _ => rfl }
     1
-    (fun x => by simpa using lp.norm_apply_le_norm (p := 2) (by norm_num) x j)
+    (fun x => by
+      rw [one_mul]
+      exact lp.norm_apply_le_norm (p := 2) (by norm_num) x j)
 
 omit [DecidableEq ι] [∀ (i : ι), CompleteSpace (H i)] in
 @[simp] theorem lpEvalCLM_apply (j : ι) (x : lp H 2) : lpEvalCLM j x = x j := rfl

Physicslib4/GNS/Irreducibility.lean

@@ -342,7 +342,7 @@ theorem center_gnsVonNeumann_eq_of_isIrreducible {π : A →⋆ₐ[ℂ] (H →L[
     gnsVonNeumann π ∩ Set.centralizer (gnsVonNeumann π)
       = {T : H →L[ℂ] H | ∃ c : ℂ, T = c • 1} := by
   ext T
-  simp only [Set.mem_inter_iff, Set.mem_setOf_eq]
+  simp only [Set.mem_inter_iff, Set.mem_ofPred_eq]
   constructor
   · rintro ⟨_, hT'⟩
     rw [gnsVonNeumann, Set.centralizer_centralizer_centralizer] at hT'

Physicslib4/GNS/PureStateExists.lean

@@ -66,7 +66,7 @@ theorem isClosed_complex_nonneg : IsClosed {z : ℂ | (0 : ℂ) ≤ z} := by
   have hset : {z : ℂ | (0 : ℂ) ≤ z}
       = (Complex.re ⁻¹' Set.Ici 0) ∩ (Complex.im ⁻¹' {0}) := by
     ext z
-    simp only [Set.mem_setOf_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_Ici,
+    simp only [Set.mem_ofPred_eq, Set.mem_inter_iff, Set.mem_preimage, Set.mem_Ici,
       Set.mem_singleton_iff, Complex.le_def, Complex.zero_re, Complex.zero_im]
     tauto
   rw [hset]
@@ -75,7 +75,7 @@ theorem isClosed_complex_nonneg : IsClosed {z : ℂ | (0 : ℂ) ≤ z} := by
 
 theorem isClosed_weakStateSet : IsClosed (weakStateSet : Set (WeakDual ℂ A)) := by
   have h1 : IsClosed {φ : WeakDual ℂ A | ∀ a : A, (0 : ℂ) ≤ φ (star a * a)} := by
-    rw [Set.setOf_forall]
+    rw [Set.ofPred_forall]
     exact isClosed_iInter fun a =>
       isClosed_complex_nonneg.preimage (WeakDual.eval_continuous (star a * a))
   have h2 : IsClosed {φ : WeakDual ℂ A | φ 1 = 1} :=

Physicslib4/GNS/UnitaryEquiv.lean

@@ -137,7 +137,7 @@ theorem conjMulEquiv_image_scalar (U : H₁ ≃ₗᵢ[ℂ] H₂) :
     rw [conjMulEquiv_apply, conjCLM_apply]
     simp [map_smul]
   ext S
-  simp only [scalarOperators, Set.mem_image, Set.mem_setOf_eq]
+  simp only [scalarOperators, Set.mem_image, Set.mem_ofPred_eq]
   constructor
   · rintro ⟨_, ⟨c, rfl⟩, rfl⟩
     exact ⟨c, hfix c⟩

Physicslib4/Operators/Conjugation.lean

@@ -155,7 +155,7 @@ theorem lieConj_image_scalarOperators (Uop : H ≃ₗᵢ[ℂ] H) :
     rw [lieConj_apply]
     simp
   ext T
-  simp only [scalarOperators, Set.mem_image, Set.mem_setOf_eq]
+  simp only [scalarOperators, Set.mem_image, Set.mem_ofPred_eq]
   constructor
   · rintro ⟨_, ⟨c, rfl⟩, rfl⟩
     exact ⟨c, hfix c⟩

Physicslib4/Spacetime/CausalComplement.lean

@@ -66,11 +66,11 @@ theorem spacelikeComplement_isCausallyConvex (B : Set M.Carrier) :
   have hp_pb : IsSpacelikeRelated M t p b := hp p (by simp) b hb
   have hr_rb : IsSpacelikeRelated M t r b := hr r (by simp) b hb
   unfold IsSpacelikeRelated at hp_pb hr_rb
-  simp only [Set.mem_union, causalFuture, causalPast, Set.mem_setOf_eq, not_or] at hp_pb hr_rb
+  simp only [Set.mem_union, causalFuture, causalPast, Set.mem_ofPred_eq, not_or] at hp_pb hr_rb
   rcases hp_pb with ⟨hpb_not, hbp_not⟩
   rcases hr_rb with ⟨hrb_not, hbr_not⟩
   unfold IsSpacelikeRelated
-  simp only [Set.mem_union, causalFuture, causalPast, Set.mem_setOf_eq, not_or]
+  simp only [Set.mem_union, causalFuture, causalPast, Set.mem_ofPred_eq, not_or]
   constructor
   · intro hqb
     apply hpb_not

Physicslib4/Spacetime/Causality.lean

@@ -331,7 +331,7 @@ theorem causallyPrecedes_antisymm (t : M.TimeOrientation)
 theorem isSpacelikeRelated_comm (t : M.TimeOrientation) {p₁ p₂ : M.Carrier} :
     M.IsSpacelikeRelated t p₁ p₂ ↔ M.IsSpacelikeRelated t p₂ p₁ := by
   unfold IsSpacelikeRelated
-  simp only [Set.mem_union, causalFuture, causalPast, Set.mem_setOf_eq, not_or]
+  simp only [Set.mem_union, causalFuture, causalPast, Set.mem_ofPred_eq, not_or]
   tauto
 
 /-- Complete spacelike separation is symmetric in its two regions. -/
@@ -612,7 +612,7 @@ Alexandrov basis set iff `U = I^+(p) ∩ I^-(q)` for some `p, q`. -/
 theorem mem_alexandrovBasis_iff_eq_chronologicalDiamond (t : M.TimeOrientation)
     {U : Set M.Carrier} :
     U ∈ alexandrovBasis M t ↔ ∃ p q : M.Carrier, U = chronologicalDiamond M t p q := by
-  simp only [alexandrovBasis, chronologicalDiamond, Set.mem_setOf_eq]
+  simp only [alexandrovBasis, chronologicalDiamond, Set.mem_ofPred_eq]
 
 /-! ### Causal convexity -/
 

Physicslib4/Spacetime/Curves.lean

@@ -182,8 +182,9 @@ theorem SmoothPath.mfderivWithin_comp_reparam {M : Spacetime} (μ : M.SmoothPath
   change mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model μ.toFun μ.parameterSpace (φ s)
       (mfderivWithin (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) φ u s (1 : ℝ))
     = derivWithin φ u s • μ.tangent (φ s)
-  rw [SmoothPath.tangent_def, ← ContinuousLinearMap.map_smul]
-  congr 1
+  rw [SmoothPath.tangent_def]
+  refine (congrArg _ ?_).trans ((mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model μ.toFun
+    μ.parameterSpace (φ s)).map_smul _ _)
   rw [mfderivWithin_eq_fderivWithin]
   change (fderivWithin ℝ φ u s) 1 = (derivWithin φ u s : ℝ) • (1 : ℝ)
   rw [smul_eq_mul, mul_one]

Physicslib4/Spacetime/LorentzCausality.lean

@@ -64,7 +64,7 @@ theorem isSpacelikeRelated_congr (t : M.TimeOrientation)
     (p₁ p₂ : M.Carrier) :
     IsSpacelikeRelated M t (g p₁) (g p₂) ↔ IsSpacelikeRelated M t p₁ p₂ := by
   simp only [IsSpacelikeRelated, Set.mem_union, causalFuture, causalPast,
-    Set.mem_setOf_eq, not_or, hg]
+    Set.mem_ofPred_eq, not_or, hg]
 
 /-- **Complete spacelikeness is invariant under taking images by a
 precedence-preserving map.** If `g` preserves causal precedence in both
@@ -428,12 +428,12 @@ theorem isAlexandrovBasisSet_smul (g : InhomogeneousLorentzGroup)
     {B : Set StandardMinkowskiSpacetime.Carrier}
     (hB : IsAlexandrovBasisSet B) :
     IsAlexandrovBasisSet (g • B) := by
-  simp only [IsAlexandrovBasisSet, Spacetime.alexandrovBasis, Set.mem_setOf_eq] at hB ⊢
+  simp only [IsAlexandrovBasisSet, Spacetime.alexandrovBasis, Set.mem_ofPred_eq] at hB ⊢
   obtain ⟨p, q, rfl⟩ := hB
   refine ⟨g • p, g • q, ?_⟩
   ext y
   simp only [Set.mem_smul_set, Set.mem_inter_iff, chronologicalFuture, chronologicalPast,
-    Set.mem_setOf_eq]
+    Set.mem_ofPred_eq]
   constructor
   · rintro ⟨x, ⟨hxF, hxP⟩, rfl⟩
     exact ⟨(chronologicallyPrecedes_smul_iff g p x).mpr hxF,

Physicslib4/Spacetime/Minkowski.lean

@@ -1349,7 +1349,7 @@ theorem chronologicalFuture_standardMinkowski_subset (p : SpacetimeModel) :
       ⊆ minkowskiForwardCone p := by
   intro q hq
   unfold Spacetime.chronologicalFuture at hq
-  simp only [Set.mem_setOf_eq, Spacetime.ChronologicallyPrecedes, Spacetime.IsTrip] at hq
+  simp only [Set.mem_ofPred_eq, Spacetime.ChronologicallyPrecedes, Spacetime.IsTrip] at hq
   induction hq with
   | single h =>
       exact segmentPrecedes_mem_minkowskiForwardCone h
@@ -1453,8 +1453,15 @@ theorem euclidean_le_alexandrov_standardMinkowski :
           standardMinkowskiTimeOrientation := by
   apply le_generateFrom
   rintro s ⟨p, q, rfl⟩
-  rw [chronologicalFuture_standardMinkowski, chronologicalPast_standardMinkowski]
-  exact (isOpen_minkowskiForwardCone p).inter (isOpen_minkowskiBackwardCone q)
+  have h := (isOpen_minkowskiForwardCone p).inter (isOpen_minkowskiBackwardCone q)
+  have e : Spacetime.chronologicalFuture StandardMinkowskiSpacetime
+        standardMinkowskiTimeOrientation p ∩
+      Spacetime.chronologicalPast StandardMinkowskiSpacetime
+        standardMinkowskiTimeOrientation q =
+      minkowskiForwardCone p ∩ minkowskiBackwardCone q :=
+    congrArg₂ (· ∩ ·) (chronologicalFuture_standardMinkowski p)
+      (chronologicalPast_standardMinkowski q)
+  exact e ▸ h
 
 /-- *Hard direction of the Alexandrov-vs-Euclidean topology comparison.*
 Every Euclidean-open subset of standard Minkowski spacetime is open in the
@@ -1466,7 +1473,7 @@ theorem alexandrov_le_euclidean_standardMinkowski :
     Spacetime.alexandrovTopology StandardMinkowskiSpacetime
         standardMinkowskiTimeOrientation
       ≤ (inferInstance : TopologicalSpace SpacetimeModel) := by
-  rw [TopologicalSpace.le_def]
+  refine (TopologicalSpace.le_def (α := SpacetimeModel)).mpr ?_
   -- `StandardMinkowskiSpacetime.Carrier` is definitionally `SpacetimeModel`,
   -- so we may transport everything to the underlying Euclidean model.
   change ∀ U : Set SpacetimeModel, IsOpen U →

Physicslib4/Spacetime/MinkowskiDilation.lean

@@ -67,7 +67,7 @@ theorem minkowskiForwardCone_smul (lam : ℝ) (hlam : 0 < lam) (p q : SpacetimeM
 theorem minkowskiBackwardCone_smul (lam : ℝ) (hlam : 0 < lam) (p q : SpacetimeModel) :
     lam • p ∈ minkowskiBackwardCone (lam • q) ↔ p ∈ minkowskiBackwardCone q := by
   rw [minkowskiBackwardCone_eq, minkowskiBackwardCone_eq q]
-  simp only [Set.mem_setOf_eq]
+  simp only [Set.mem_ofPred_eq]
   exact minkowskiForwardCone_smul lam hlam p q
 
 /-- **A positive dilation is a causal automorphism: it preserves the Alexandrov basis.**
@@ -80,7 +80,7 @@ theorem alexandrovBasis_image_smul (lam : ℝ) (hlam : 0 < lam)
       standardMinkowskiTimeOrientation) :
     (fun x => lam • x) '' B ∈ Spacetime.alexandrovBasis StandardMinkowskiSpacetime
       standardMinkowskiTimeOrientation := by
-  simp only [Spacetime.alexandrovBasis, Set.mem_setOf_eq] at hB ⊢
+  simp only [Spacetime.alexandrovBasis, Set.mem_ofPred_eq] at hB ⊢
   obtain ⟨p, q, rfl⟩ := hB
   refine ⟨lam • p, lam • q, ?_⟩
   ext y