Bump to version: v4.34.0

Physlib/ClassicalMechanics/DampedHarmonicOscillator/Solution.lean

@@ -534,7 +534,7 @@ lemma equationOfMotion_unique (x y : Time → EuclideanSpace ℝ (Fin 1))
     (v := fun _ p => S.phaseVectorField p) (s := fun _ => Set.univ) (t₀ := (0 : ℝ))
     (f := fun τ : ℝ => (x (Time.toRealCLE.symm τ), ∂ₜ x (Time.toRealCLE.symm τ)))
     (g := fun τ : ℝ => (y (Time.toRealCLE.symm τ), ∂ₜ y (Time.toRealCLE.symm τ)))
-    (fun _ => S.phaseVectorField.lipschitz.lipschitzOnWith)
+    (fun _ => S.phaseVectorField.lipschitzWith.lipschitzOnWith)
     (fun τ => ⟨S.phaseCurve_hasDerivAt x hx hEOMx τ, Set.mem_univ _⟩)
     (fun τ => ⟨S.phaseCurve_hasDerivAt y hy hEOMy τ, Set.mem_univ _⟩)
     hIC

Physlib/CondensedMatter/Thermoelectric/Basic.lean

@@ -5,7 +5,7 @@ Authors: Giuseppe Barbalinardo
 -/
 module
 
-public import Mathlib.Data.Real.Basic
+public import Mathlib.Basic.Real.Basic
 public import Mathlib.Tactic.Ring
 public import Mathlib.Tactic.Positivity
 /-!

Physlib/CondensedMatter/TightBindingChain/Basic.lean

@@ -246,7 +246,7 @@ lemma hamiltonian_apply_localizedState (n : Fin T.N) :
   simp only [hamiltonian, LinearMap.sub_apply, LinearMap.smul_apply, LinearMap.coe_sum,
     Finset.sum_apply, LinearMap.add_apply, smul_add, Finset.sum_add_distrib,
     localizedComp_apply_localizedState, ← eq_sub_iff_add_eq, Finset.sum_ite_eq', Finset.mem_univ,
-    if_true]
+    ite_true]
   module
 
 /-!

Physlib/Electromagnetism/Distributional/Basic.lean

@@ -189,8 +189,7 @@ lemma toTensor_distTensorDeriv_basis_repr_apply {d} (A : DistElectromagneticPote
     distDeriv (b 0) A ε (b 1) := by
   rw [Tensorial.basis_toTensor_apply]
   rw [Tensorial.basis_map_prod]
-  simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
-    Equiv.symm_symm, Fin.isValue]
+  simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Fin.isValue]
   rw [Lorentz.Vector.tensor_basis_map_eq_basis_reindex,
     Lorentz.CoVector.tensor_basis_map_eq_basis_reindex]
   have hb : (((Lorentz.CoVector.basis (d := d)).reindex
@@ -203,7 +202,8 @@ lemma toTensor_distTensorDeriv_basis_repr_apply {d} (A : DistElectromagneticPote
     | ⟨i, j⟩ =>
     simp
   rw [hb]
-  rw [Module.Basis.repr_reindex_apply, distTensorDeriv_basis_repr_apply]
+  rw [Finsupp.equivMapDomain_apply, Module.Basis.repr_reindex_apply,
+    distTensorDeriv_basis_repr_apply]
   rfl
 
 end DistElectromagneticPotential

Physlib/Electromagnetism/Distributional/Dynamics/KineticTerm.lean

@@ -197,8 +197,7 @@ lemma gradKineticTerm_eq_distTensorDeriv {d} {𝓕 : FreeSpace}
       (fun | 0 => μ | 1 => ν)
   · generalize (distDeriv μ (A.fieldStrength) ε) = t at *
     rw [Tensorial.basis_toTensor_apply, Tensorial.basis_map_prod]
-    simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
-      Equiv.symm_symm]
+    simp only [Basis.repr_reindex]
     rw [Lorentz.Vector.tensor_basis_map_eq_basis_reindex]
     have hb : (((Lorentz.Vector.basis (d := d)).reindex
         Lorentz.Vector.indexEquiv.symm).tensorProduct
@@ -207,7 +206,7 @@ lemma gradKineticTerm_eq_distTensorDeriv {d} {𝓕 : FreeSpace}
         (Lorentz.Vector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm) := by
       ext ⟨i, j⟩
       simp
-    rw [hb, Module.Basis.repr_reindex_apply]
+    rw [hb, Finsupp.equivMapDomain_apply, Module.Basis.repr_reindex_apply]
     rfl
   apply congr
   · simp

Physlib/Electromagnetism/Distributional/FieldStrength.lean

@@ -131,8 +131,7 @@ lemma fieldStrengthAux_tensor_basis_eq_basis {d} (A : DistElectromagneticPotenti
       (b 0, b 1) := by
   rw [Tensorial.basis_toTensor_apply]
   rw [Tensorial.basis_map_prod]
-  simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
-    Equiv.symm_symm, Fin.isValue]
+  simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Fin.isValue]
   rw [Lorentz.Vector.tensor_basis_map_eq_basis_reindex]
   have hb : (((Lorentz.Vector.basis (d := d)).reindex Lorentz.Vector.indexEquiv.symm).tensorProduct
           (Lorentz.Vector.basis.reindex Lorentz.Vector.indexEquiv.symm)) =
@@ -143,7 +142,7 @@ lemma fieldStrengthAux_tensor_basis_eq_basis {d} (A : DistElectromagneticPotenti
         | ⟨i, j⟩ =>
         simp
   rw [hb]
-  rw [Module.Basis.repr_reindex_apply]
+  rw [Finsupp.equivMapDomain_apply, Module.Basis.repr_reindex_apply]
   congr 1
 
 lemma fieldStrengthAux_basis_repr_apply {d} {μν : (Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)}

Physlib/Electromagnetism/Kinematics/EMPotential.lean

@@ -643,8 +643,7 @@ lemma toTensor_deriv_basis_repr_apply {d} (A : ElectromagneticPotential d)
     (Tensor.basis _).repr (Tensorial.toTensor (deriv A x)) b =
     ∂_ (b 0) A x (b 1) := by
   rw [Tensorial.basis_toTensor_apply, Tensorial.basis_map_prod]
-  simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
-    Equiv.symm_symm, Fin.isValue]
+  simp only [Nat.reduceSucc, Nat.reduceAdd, Basis.repr_reindex, Fin.isValue]
   rw [Lorentz.Vector.tensor_basis_map_eq_basis_reindex,
     Lorentz.CoVector.tensor_basis_map_eq_basis_reindex]
   have hb : (((Lorentz.CoVector.basis (d := d)).reindex
@@ -654,7 +653,7 @@ lemma toTensor_deriv_basis_repr_apply {d} (A : ElectromagneticPotential d)
       (Lorentz.CoVector.indexEquiv.symm.prodCongr Lorentz.Vector.indexEquiv.symm) := by
     ext ⟨i, j⟩
     simp
-  rw [hb, Module.Basis.repr_reindex_apply, deriv_basis_repr_apply]
+  rw [hb, Finsupp.equivMapDomain_apply, Module.Basis.repr_reindex_apply, deriv_basis_repr_apply]
   rfl
 
 /-!

Physlib/Electromagnetism/Kinematics/FieldStrength.lean

@@ -160,7 +160,7 @@ lemma toFieldStrength_eq_sum_basis {d} {A : ElectromagneticPotential d}
         Vector.basis_eq_map_tensor_basis,
     toFieldStrength_eq_sub_tensorDeriv hA, ← deriv_eq_tensorDeriv _ hA, map_sub, Basis.repr_reindex,
     Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply, LinearEquiv.apply_symm_apply,
-    Finsupp.coe_sub, Pi.sub_apply, Finsupp.mapDomain_equiv_apply, permT_basis_repr_symm_apply,
+    Finsupp.coe_sub, Pi.sub_apply, Finsupp.equivMapDomain_apply, permT_basis_repr_symm_apply,
     Function.comp_apply, contrT_basis_repr_apply_eq_fin, prodT_basis_repr_apply,
     contrMetric_repr_apply_eq_minkowskiMatrix,
     prod_tensor_basis_eq_map_reindex CoVector.basis_eq_map_tensor_basis
@@ -367,8 +367,7 @@ lemma toFieldStrength_eval_equivariant {d} (A : ElectromagneticPotential d)
   simp only [Vector.toField_eval_eval_eq_tensorProduct_repr]
   rw [toFieldStrength_equivariant A Λ hf x]
   generalize A.toFieldStrength (Λ⁻¹ • x) = F
-  induction F using TensorProduct.induction_on with
-  | zero => simp
+  induction F using TensorProduct.inductionOn with
   | tmul v w =>
     rw [Tensorial.smul_prod]
     simp only [Basis.tensorProduct_repr_tmul_apply, Lorentz.Vector.basis_repr_apply, smul_eq_mul]

Physlib/Electromagnetism/Kinematics/GaugeTransformation.lean

@@ -378,7 +378,7 @@ lemma toFieldStrength_eval_bareGradient_inl_inr {d : ℕ} (i : Fin d)
   simp_rw [hfderiv]
   simp only [_root_.add_apply, FunLike.coe_smul,
     Pi.smul_apply, Lorentz.Vector.coordCLM_apply, smul_eq_mul, Lorentz.Vector.basis_apply]
-  simp only [mul_ite, mul_one, mul_zero, ite_add, zero_add, if_true]
+  simp only [mul_ite, mul_one, mul_zero, ite_add, zero_add, ite_true]
   simp only [minkowskiMatrix.inl_0_inl_0, minkowskiMatrix.inr_i_inr_i]
   simp only [reduceCtorEq, ↓reduceIte, add_zero]
   simp only [Lorentz.Vector.fderiv_coord, Lorentz.Vector.coordCLM_apply,

Physlib/Mathematics/Calculus/Wirtinger/Coordinate.lean

@@ -270,7 +270,7 @@ coordinate-difference rule `dWirtingerCoord_coordDiff` and the conjugate-coordin
   funext u
   rw [dWirtingerCoord_apply I, fderiv_coordProj, fderiv_coordProj]
   by_cases h : I = J
-  · subst h; rw [Pi.single_eq_same, Pi.single_eq_same, if_pos rfl, Complex.I_mul_I]; ring
+  · subst h; rw [Pi.single_eq_same, Pi.single_eq_same, ite_eq_left rfl, Complex.I_mul_I]; ring
   · simp [h]
 
 /-- Pointwise additivity of the holomorphic coordinate derivative at `u`:

Physlib/Mathematics/CrossProduct.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Analysis.Calculus.ContDiff.Operations
 public import Mathlib.Data.Matrix.Mul
-public import Mathlib.Data.Real.Basic
+public import Mathlib.Basic.Real.Basic
 public import Mathlib.LinearAlgebra.CrossProduct
 /-!
 

Physlib/Mathematics/CrossProductMatrix.lean

@@ -6,7 +6,7 @@ Authors: Giuseppe Sorge
 module
 
 public import Mathlib.Data.Matrix.Mul
-public import Mathlib.Data.Real.Basic
+public import Mathlib.Basic.Real.Basic
 public import Mathlib.LinearAlgebra.CrossProduct
 public import Mathlib.LinearAlgebra.Matrix.Notation
 /-!

Physlib/Mathematics/DataStructures/Matrix/LieTrace.lean

@@ -60,9 +60,9 @@ lemma matrix_tsum_apply
     have h := Pi.summable.1 hf
     exact h i
   have h₁ : ((∑' n, f n) : Matrix m m 𝕂) i = (∑' n, (f n) i) := by
-    exact tsum_apply hf
+    exact Pi.tsum_apply hf
   have h₂ : ((∑' n, (f n) i) : m → 𝕂) j = (∑' n, (f n) i j) := by
-    exact tsum_apply h_row_summable
+    exact Pi.tsum_apply h_row_summable
   rw [h₁, h₂]
 
 variable [Fintype m] [LinearOrder m]

Physlib/Mathematics/Distribution/Basic.lean

@@ -476,8 +476,10 @@ private lemma lipschitzWith_integral_of_le {μ ρ : Measure E} (hμρ : μ ≤ 
         MeasureTheory.norm_integral_le_lintegral_norm (μ := μ) (fun x => f x - g x)
     _ ≤ (eLpNorm (fun x => f x - g x) 1 ρ).toReal := by
       refine ENNReal.toReal_mono hfg_top ?_
-      simpa [eLpNorm_one_eq_lintegral_enorm] using
-        eLpNorm_mono_measure (p := (1 : ℝ≥0∞)) (fun x => f x - g x) hμρ
+      have hfg_meas : AEStronglyMeasurable (fun x => f x - g x) μ :=
+        (hfμ.sub hgμ).aestronglyMeasurable
+      rw [← eLpNorm_one_eq_lintegral_enorm hfg_meas]
+      exact eLpNorm_mono_measure (p := (1 : ℝ≥0∞)) (fun x => f x - g x) hμρ
     _ = ‖f - g‖ := by rw [Lp.norm_def, eLpNorm_congr_ae hfg_ae]
 
 private lemma integral_boundedContinuous_eq_of_forall_schwartz_integral_eq

Physlib/Mathematics/Fin.lean

@@ -114,7 +114,7 @@ lemma finExtractOne_symm_inr {n : ℕ} (i : Fin n.succ) :
     · rfl
     rename_i hn
     simp_all only [Nat.succ_eq_add_one, not_lt, Fin.le_def, Fin.val_castSucc, Fin.val_succ,
-      left_eq_add, one_ne_zero]
+      left_eq_add]
     omega
   · generalize_proofs hp
     have h1 : (finSumFinEquiv.symm (Fin.cast hp x)) =

Physlib/Mathematics/Fin/Involutions.lean

@@ -64,12 +64,12 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
         by_cases hja : j = a
         · subst hja
           simp
-        · rw [Function.update_apply, if_neg hja]
+        · rw [Function.update_apply, ite_eq_right hja]
           simp only [Function.comp_apply, Fin.cons_succ]
           have hf2 := f.2.2 hs
           change f.1.1 a = a at hf2
           have hjf1 : f.1.1 j ≠ a := fun hn => hja (by rw [← f.1.2 j, hn, hf2])
-          rw [Function.update_apply, if_neg hjf1]
+          rw [Function.update_apply, ite_eq_right hjf1]
           simp only [Function.comp_apply, Fin.succ_inj]
           rw [f.1.2]
     · simp only [succ_eq_add_one, hs, Bool.false_eq_true, ↓reduceDIte]
@@ -85,7 +85,7 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
     | ⟨f, hf⟩ =>
     have hpred (j : Fin n) (hj : f j.succ ≠ 0) :
         (↑(if h : f j.succ = 0 then j else (f j.succ).pred h) + 1 : ℕ) = ↑(f j.succ) := by
-      rw [dif_neg hj, Fin.val_pred]
+      rw [dite_eq_right hj, Fin.val_pred]
       have hv : (f j.succ).val ≠ 0 := fun h => hj (Fin.ext (by simpa using h))
       omega
     simp only [succ_eq_add_one, Option.isSome_dite', Option.get_dite', Fin.succ_pred,
@@ -99,13 +99,13 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
       · subst hj
         simp only [Fin.cons_succ, Function.comp_apply, Fin.val_succ]
         refine hpred j fun hj => Fin.succ_ne_zero j (hf.injective (hj.trans h0.symm))
-    · rw [if_neg h0]
+    · rw [ite_eq_right h0]
       by_cases hf' : i = f 0
       · subst hf'
         simp only [Function.update_self, Fin.val_zero]
         rw [hf]
         simp
-      · rw [Function.update_apply, if_neg hf']
+      · rw [Function.update_apply, ite_eq_right hf']
         rcases Fin.eq_zero_or_eq_succ i with hi | ⟨j, hj⟩
         · subst hi
           simp
@@ -125,10 +125,10 @@ def involutionCons (n : ℕ) : {f : Fin n.succ → Fin n.succ // Function.Involu
           exact Eq.symm (Fin.val_eq_of_eq (hf0 hs))
         · simp only [ne_eq, Fin.succ_inj, hi, not_false_eq_true, Function.update_of_ne,
           Fin.cons_succ, Function.comp_apply, Fin.pred_succ, dite_eq_ite]
-          rw [if_neg (Fin.succ_ne_zero (f i))]
+          rw [ite_eq_right (Fin.succ_ne_zero (f i))]
       · simp only [hs, Bool.false_eq_true, ↓reduceDIte, Fin.cons_succ, Function.comp_apply,
         Fin.pred_succ, dite_eq_ite]
-        rw [if_neg (Fin.succ_ne_zero (f i))]
+        rw [ite_eq_right (Fin.succ_ne_zero (f i))]
     · simp only [Nat.succ_eq_add_one, Option.dite_none_left_eq_some, Option.some.injEq]
       by_cases hs : f0.isSome
       · simp only [hs, ↓reduceDIte]
@@ -193,7 +193,7 @@ lemma involutionAddEquiv_none_image_zero {n : ℕ} :
   by_contra hf0
   simp only [Fin.zero_eta] at hf0
   simp only [succ_eq_add_one, involutionCons, Equiv.coe_fn_mk, involutionAddEquiv,
-    Option.isSome_some, Option.get_some, Option.isSome_none, dif_neg hf0] at h
+    Option.isSome_some, Option.get_some, Option.isSome_none, dite_eq_right hf0] at h
   exact absurd h (Option.some_ne_none _)
 
 lemma involutionAddEquiv_cast {n : ℕ} {f1 f2 : {f : Fin n → Fin n // Function.Involutive f}}

Physlib/Mathematics/KroneckerDelta/Basic.lean

@@ -58,9 +58,9 @@ def kroneckerDelta (i j : α) : ℕ := if i = j then 1 else 0
 notation "δ[" i "," j "]" => kroneckerDelta i j
 
 @[simp]
-lemma eq_one_of_same (i : α) : δ[i,i] = 1 := if_pos rfl
+lemma eq_one_of_same (i : α) : δ[i,i] = 1 := ite_eq_left rfl
 
-lemma eq_zero_of_ne {i j : α} (h : i ≠ j) : δ[i,j] = 0 := if_neg h
+lemma eq_zero_of_ne {i j : α} (h : i ≠ j) : δ[i,j] = 0 := ite_eq_right h
 
 @[simp]
 lemma eq_of_coe {p : α → Prop} (i j : Subtype p) : δ[(i : α),j] = δ[i,j] := by

Physlib/Mathematics/LinearPMap.lean

@@ -357,25 +357,31 @@ end Monoid
 
 section Inverses
 
+/-- The kernel of `f.toFun` is trivial exactly when the kernel of `f` is. -/
+lemma toFun_ker_eq_bot_iff {f : E →ₗ.[R] F} : f.toFun.ker = ⊥ ↔ f.ker = ⊥ := by
+  rw [LinearMap.ker_eq_bot', LinearPMap.ker_eq_bot']
+  rfl
+
 variable {f : E →ₗ.[R] F} (h_ker : f.toFun.ker = ⊥)
 include h_ker
 
 lemma inverse_ker : f.inverse.toFun.ker = ⊥ := by
   refine LinearMap.ker_eq_bot'.mpr fun ⟨y, hy⟩ hy' ↦ ?_
   obtain ⟨x, hx⟩ := inverse_domain (f := f) ▸ hy
-  simp_all [inverse_apply_eq (x := x) (y := ⟨y, hy⟩) h_ker hx]
+  simp_all [inverse_apply_eq (x := x) (y := ⟨y, hy⟩) (toFun_ker_eq_bot_iff.mp h_ker) hx]
 
 lemma inverse_inverse : f.inverse.inverse = f := by
   ext x hx hx'
-  · rw [inverse_domain, inverse_range h_ker]
+  · rw [inverse_domain, inverse_range (toFun_ker_eq_bot_iff.mp h_ker)]
   · refine inverse_apply_eq (y := ⟨x, hx⟩) (x := ⟨f ⟨x, hx'⟩, by simp [inverse_domain]⟩) ?_ ?_
-    · exact inverse_ker h_ker
-    · exact inverse_apply_eq (y := ⟨f ⟨x, hx'⟩, by simp [inverse_domain]⟩) (x := ⟨x, hx'⟩) h_ker rfl
+    · exact toFun_ker_eq_bot_iff.mp (inverse_ker h_ker)
+    · exact inverse_apply_eq (y := ⟨f ⟨x, hx'⟩, by simp [inverse_domain]⟩) (x := ⟨x, hx'⟩)
+        (toFun_ker_eq_bot_iff.mp h_ker) rfl
 
 lemma inverse_compRestricted_eq : f.inverse ∘ᵣ f = domRestrict 1 f.domain := by
   ext x hx hx'
-  · simp [mem_compRestricted_domain_iff, inverse_domain, ← toFun_eq_coe]
-  · exact inverse_apply_eq (x := ⟨x, hx.2⟩) h_ker rfl
+  · simp [mem_compRestricted_domain_iff, inverse_domain, ← toFun_eq_coe, -coe_toFun_eq_coe]
+  · exact inverse_apply_eq (x := ⟨x, hx.2⟩) (toFun_ker_eq_bot_iff.mp h_ker) rfl
 
 lemma compRestricted_inverse_eq : f ∘ᵣ f.inverse = domRestrict 1 f.inverse.domain := by
   nth_rw 1 [← inverse_inverse h_ker]

Physlib/Mathematics/List.lean

@@ -287,7 +287,7 @@ lemma orderedInsert_eraseIdx_orderedInsertPos_le {I : Type} (le1 : I → I → P
         omega
       rw [hn]
       simp only [List.eraseIdx_cons_succ, List.cons.injEq, true_and]
-      rw [dropWile_eraseIdx, if_pos]
+      rw [dropWile_eraseIdx, ite_eq_left]
       · rw [orderedInsertPos] at hi
         omega
       · exact hr
@@ -467,7 +467,7 @@ lemma orderedInsert_eq_insertIdx_orderedInsertPos {I : Type} (le1 : I → I →
   apply List.ext_get
   · simp only [List.orderedInsert_length]
     rw [List.length_insertIdx]
-    exact (if_pos (Nat.le_of_succ_le_succ (orderedInsertPos_lt_length le1 r r0))).symm
+    exact (ite_eq_left (Nat.le_of_succ_le_succ (orderedInsertPos_lt_length le1 r r0))).symm
   intro n h1 h2
   obtain ⟨n', hn'⟩ := (orderedInsertEquiv le1 r r0).surjective ⟨n, h1⟩
   rw [← hn']
@@ -730,7 +730,7 @@ lemma mem_take_finrange : (n m : ℕ) → (a : Fin n) → a ∈ List.take m (Lis
     simp [List.finRange_succ]
   | n +1, m + 1, ⟨i + 1, h⟩ => by
     simp only [List.finRange_succ, List.take_succ_cons, List.mem_cons, Fin.ext_iff, Fin.val_zero,
-      AddLeftCancelMonoid.add_eq_zero, one_ne_zero, and_false, false_or, add_lt_add_iff_right]
+      Nat.add_eq_zero_iff, one_ne_zero, and_false, false_or, add_lt_add_iff_right]
     rw [← List.map_take, @List.mem_map]
     apply Iff.intro
     · intro h

Physlib/Mathematics/List/InsertionSort.lean

@@ -102,7 +102,7 @@ lemma orderedInsert_commute {α : Type} (r : α → α → Prop) [DecidableRel r
     simp only [List.orderedInsert]
     by_cases h : r a c
     · simp only [h, ↓reduceIte, List.orderedInsert.eq_2, hrb]
-      rw [if_pos (IsTrans.trans (r := r) _ _ _ hrb h)]
+      rw [ite_eq_left (IsTrans.trans (r := r) _ _ _ hrb h)]
       simp only [List.orderedInsert, hr, ↓reduceIte, h]
     · simp only [h, ↓reduceIte, List.orderedInsert.eq_2]
       by_cases hbc : r b c

Physlib/Mathematics/SO3/Basic.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.LinearAlgebra.Eigenspace.Basic
 public import Mathlib.Analysis.InnerProductSpace.PiL2
+public import Mathlib.Topology.Algebra.Group.Units
 /-!
 # The group SO(3)
 
@@ -109,7 +110,7 @@ lemma toGL_embedding : IsEmbedding toGL.toFun where
 /-- The instance of a topological group on `SO(3)`, defined through the embedding of `SO(3)`
   into `GL(n)`. -/
 instance : IsTopologicalGroup SO(3) :=
-  IsInducing.topologicalGroup toGL toGL_embedding.toIsInducing
+  IsInducing.isTopologicalGroup toGL toGL_embedding.toIsInducing
 
 /-- The determinant of an `SO(3)` matrix minus the identity is equal to zero. -/
 lemma det_minus_id (A : SO(3)) : det (A.1 - 1) = 0 := by

Physlib/Mathematics/SchurTriangulation.lean

@@ -167,11 +167,11 @@ protected noncomputable def SchurTriangulationAux.of
           | ⟨true, i⟩ => show bE ⟨true, i⟩ = bV i from
             show (int.collectedBasis fun b => (B b).toBasis).toOrthonormalBasis _ ⟨true, i⟩ = bV i
             by simp only [Basis.coe_toOrthonormalBasis, DirectSum.IsInternal.collectedBasis_coe,
-              cond_true, OrthonormalBasis.coe_toBasis, B, V, W]
+              Bool.cond_true, OrthonormalBasis.coe_toBasis, B, V, W]
           | ⟨false, j⟩ => show bE ⟨false, j⟩ = bW j from
             show (int.collectedBasis fun b => (B b).toBasis).toOrthonormalBasis _ ⟨false, j⟩ = bW j
             by simp only [Basis.coe_toOrthonormalBasis, DirectSum.IsInternal.collectedBasis_coe,
-              cond_false, OrthonormalBasis.coe_toBasis, B, V, W]
+              Bool.cond_false, OrthonormalBasis.coe_toBasis, B, V, W]
         have hf {bi i' bj j'} (hi : e i = ⟨bi, i'⟩) (hj : e j = ⟨bj, j'⟩) :=
           calc toMatrixOrthonormal basis f i j
             _ = toMatrixOrthonormal bE f (e i) (e j) := by

Physlib/Particles/BeyondTheStandardModel/RHN/AnomalyCancellation/FamilyMaps.lean

@@ -69,16 +69,16 @@ def speciesEmbed (m n : ℕ) :
     funext i
     simp only [ACCSystemCharges.chargesAddCommMonoid_add]
     by_cases hi : i.val < m
-    · rw [dif_pos hi, dif_pos hi, dif_pos hi]
-    · rw [dif_neg hi, dif_neg hi, dif_neg hi]
+    · rw [dite_eq_left hi, dite_eq_left hi, dite_eq_left hi]
+    · rw [dite_eq_right hi, dite_eq_right hi, dite_eq_right hi]
       with_unfolding_all rfl
   map_smul' a S := by
     funext i
     simp only [HSMul.hSMul, ACCSystemCharges.chargesModule_smul,
       eq_ratCast, Rat.cast_eq_id, id_eq]
     by_cases hi : i.val < m
-    · rw [dif_pos hi, dif_pos hi]
-    · rw [dif_neg hi, dif_neg hi]
+    · rw [dite_eq_left hi, dite_eq_left hi]
+    · rw [dite_eq_right hi, dite_eq_right hi]
       exact Eq.symm (Rat.mul_zero a)
 
 /-- The embedding of the `m`-family charges onto the `n`-family charges, with all