chore(LinearAlgebra/SesquilinearForm): deprecate IsOrtho and associated lemmas (leanprover-community#37381)

Next steps in cleaning up bilinearity and orthogonality:

- deprecate `IsOrtho` and accompanying trivial lemmas (this also allows to shorten the proofs in `orthogonalBilin`).
- deprecate `ortho_smul_right` and `ortho_smul_left` since now provable from simp.
- remove uses of deprecated definitions.
- replace `IsOrtho` in undergrad.yaml by `iIsOrtho`.

See discussion at [#mathlib4 > Reorganizing bilinearity and orthogonality?](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Reorganizing.20bilinearity.20and.20orthogonality.3F/with/582426197)

Due to too agressive simplification I had to remove simp from
- `QuadraticMap.associated_apply`
- `QuadraticMap.isOrtho_polarBilin`

Co-authored-by: Martin Winter <martin.winter.math@gmail.com>
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: 2 people

Mathlib/Algebra/Lie/InvariantForm.lean

@@ -74,7 +74,7 @@ def orthogonal (hΦ_inv : Φ.lieInvariant L) (N : LieSubmodule R L M) : LieSubmo
   __ := Φ.orthogonal N
   lie_mem {x y} := by
     suffices (∀ n ∈ N, Φ n y = 0) → ∀ n ∈ N, Φ n ⁅x, y⁆ = 0 by
-      simpa only [LinearMap.BilinForm.isOrtho_def, -- and some default simp lemmas
+      simpa only [
         AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, Submodule.mem_toAddSubmonoid,
         LinearMap.BilinForm.mem_orthogonal_iff, LieSubmodule.mem_toSubmodule]
     intro H a ha
@@ -89,7 +89,7 @@ lemma orthogonal_toSubmodule (N : LieSubmodule R L M) :
 
 lemma mem_orthogonal (N : LieSubmodule R L M) (y : M) :
     y ∈ orthogonal Φ hΦ_inv N ↔ ∀ x ∈ N, Φ x y = 0 := by
-  simp [orthogonal, LinearMap.BilinForm.isOrtho_def, LinearMap.BilinForm.mem_orthogonal_iff]
+  simp [orthogonal, LinearMap.BilinForm.mem_orthogonal_iff]
 
 variable [LieAlgebra R L]
 
@@ -202,7 +202,7 @@ theorem isSemisimple_of_nondegenerate : IsSemisimple K L := by
   intro J hJ hJI
   rw [← lie_eq_self_of_isAtom_of_nonabelian J hJ (hL J hJ), lieIdeal_oper_eq_span, lieSpan_le]
   rintro _ ⟨x, y, rfl⟩
-  simp only [orthogonal_carrier, LinearMap.IsOrtho, Set.mem_setOf_eq]
+  simp only [orthogonal_carrier, Set.mem_setOf_eq]
   intro z hz
   rw [← neg_eq_zero, ← hΦ_inv]
   suffices ⁅(x : L), z⁆ = 0 by simp only [this, map_zero, LinearMap.zero_apply]

Mathlib/Algebra/Lie/TraceForm.lean

@@ -404,7 +404,7 @@ noncomputable def killingCompl : LieIdeal R L :=
 lemma coe_killingCompl_top :
     killingCompl R L ⊤ = LinearMap.ker (killingForm R L) := by
   ext x
-  simp [LinearMap.ext_iff, LinearMap.BilinForm.IsOrtho, LieModule.traceForm_comm R L L x]
+  simp [LinearMap.ext_iff, LieModule.traceForm_comm R L L x]
 
 lemma restrict_killingForm :
     (killingForm R L).restrict I = LieModule.traceForm R I L :=

Mathlib/Algebra/Lie/Weights/Killing.lean

@@ -524,7 +524,7 @@ lemma traceForm_eq_zero_of_mem_ker_of_mem_span_coroot {α : Weight K H L} {x y :
     refine le_antisymm (fun x hx ↦ ?_) (fun x hx y hy ↦ ?_)
     · simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx
       specialize hx (coroot α) (Submodule.mem_span_singleton_self _)
-      simp only [LinearMap.BilinForm.isOrtho_def, traceForm_coroot, smul_eq_mul, nsmul_eq_mul,
+      simp only [traceForm_coroot, smul_eq_mul, nsmul_eq_mul,
         Nat.cast_ofNat, mul_eq_zero, OfNat.ofNat_ne_zero, inv_eq_zero, false_or] at hx
       simpa using hx.resolve_left (root_apply_cartanEquivDual_symm_ne_zero hα)
     · have := traceForm_eq_zero_of_mem_ker_of_mem_span_coroot hx hy

Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

@@ -50,32 +50,47 @@ namespace BilinForm
 
 /-- The proposition that two elements of a bilinear form space are orthogonal. For orthogonality
 of an indexed set of elements, use `BilinForm.iIsOrtho`. -/
+@[deprecated "Use `B x y = 0`." (since := "2026-03-30")]
 def IsOrtho (B : BilinForm R M) (x y : M) : Prop :=
   B x y = 0
 
+set_option linter.deprecated false in
+@[deprecated "`BilinMap.IsOrtho` has been deprecated" (since := "2026-03-30")]
 theorem isOrtho_def {B : BilinForm R M} {x y : M} : B.IsOrtho x y ↔ B x y = 0 :=
   Iff.rfl
 
+set_option linter.deprecated false in
+@[deprecated "`BilinMap.IsOrtho` has been deprecated" (since := "2026-03-30")]
 theorem isOrtho_zero_left (x : M) : IsOrtho B (0 : M) x := LinearMap.isOrtho_zero_left B x
 
+set_option linter.deprecated false in
+@[deprecated "`BilinMap.IsOrtho` has been deprecated" (since := "2026-03-30")]
 theorem isOrtho_zero_right (x : M) : IsOrtho B x (0 : M) :=
   zero_right x
 
-theorem ne_zero_of_not_isOrtho_self {B : BilinForm K V} (x : V) (hx₁ : ¬B.IsOrtho x x) : x ≠ 0 :=
-  fun hx₂ => hx₁ (hx₂.symm ▸ isOrtho_zero_left _)
+theorem ne_zero_of_not_isOrtho_self {B : BilinForm K V} (x : V) (hx₁ : B x x ≠ 0) : x ≠ 0 := by
+  by_contra; simp [this] at hx₁
 
-theorem IsRefl.ortho_comm (H : B.IsRefl) {x y : M} : IsOrtho B x y ↔ IsOrtho B y x :=
+theorem IsRefl.eq_iff (H : B.IsRefl) {x y : M} : B x y = 0 ↔ B y x = 0 :=
   ⟨eq_zero H, eq_zero H⟩
 
-theorem IsAlt.ortho_comm (H : B₁.IsAlt) {x y : M₁} : IsOrtho B₁ x y ↔ IsOrtho B₁ y x :=
-  LinearMap.IsAlt.ortho_comm H
+@[deprecated (since := "2026-03-31")]
+alias IsRefl.ortho_comm := IsRefl.eq_iff
 
-theorem IsSymm.ortho_comm (H : B.IsSymm) {x y : M} : IsOrtho B x y ↔ IsOrtho B y x :=
-  LinearMap.IsSymm.ortho_comm (isSymm_iff.1 H)
+theorem IsAlt.eq_iff (H : B₁.IsAlt) {x y : M₁} : B₁ x y = 0 ↔ B₁ y x = 0 :=
+  LinearMap.IsAlt.eq_iff H
+
+@[deprecated (since := "2026-03-31")]
+alias IsAlt.ortho_comm := IsAlt.eq_iff
+
+theorem IsSymm.eq_iff (H : B.IsSymm) {x y : M} : B x y = 0 ↔ B y x = 0 :=
+  LinearMap.IsSymm.eq_iff (isSymm_iff.1 H)
+
+@[deprecated (since := "2026-03-31")]
+alias IsSymm.ortho_comm := IsSymm.eq_iff
 
 /-- A set of vectors `v` is orthogonal with respect to some bilinear form `B` if and only
-if for all `i ≠ j`, `B (v i) (v j) = 0`. For orthogonality between two elements, use
-`BilinForm.IsOrtho` -/
+if for all `i ≠ j`, `B (v i) (v j) = 0`. -/
 def iIsOrtho {n : Type w} (B : BilinForm R M) (v : n → M) : Prop :=
   B.IsOrthoᵢ v
 
@@ -88,15 +103,17 @@ section
 variable {R₄ M₄ : Type*} [CommRing R₄] [IsDomain R₄]
 variable [AddCommGroup M₄] [Module R₄ M₄] {G : BilinForm R₄ M₄}
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "`BilinMap.IsOrtho` has been deprecated" (since := "2026-03-30")]
 theorem isOrtho_smul_left {x y : M₄} {a : R₄} (ha : a ≠ 0) :
     IsOrtho G (a • x) y ↔ IsOrtho G x y := by
   dsimp only [IsOrtho]
   rw [map_smul]
   simp only [LinearMap.smul_apply, smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]
   exact fun a ↦ (ha a).elim
 
-@[simp]
+set_option linter.deprecated false in
+@[deprecated "`BilinMap.IsOrtho` has been deprecated" (since := "2026-03-30")]
 theorem isOrtho_smul_right {x y : M₄} {a : R₄} (ha : a ≠ 0) :
     IsOrtho G x (a • y) ↔ IsOrtho G x y := by
   dsimp only [IsOrtho]
@@ -107,7 +124,7 @@ theorem isOrtho_smul_right {x y : M₄} {a : R₄} (ha : a ≠ 0) :
 /-- A set of orthogonal vectors `v` with respect to some bilinear form `B` is linearly independent
   if for all `i`, `B (v i) (v i) ≠ 0`. -/
 theorem linearIndependent_of_iIsOrtho {n : Type w} {B : BilinForm K V} {v : n → V}
-    (hv₁ : B.iIsOrtho v) (hv₂ : ∀ i, ¬B.IsOrtho (v i) (v i)) : LinearIndependent K v := by
+    (hv₁ : B.iIsOrtho v) (hv₂ : ∀ i, B (v i) (v i) ≠ 0) : LinearIndependent K v := by
   classical
     rw [linearIndependent_iff']
     intro s w hs i hi
@@ -136,10 +153,10 @@ variable {N L : Submodule R M}
 
 @[simp]
 theorem mem_orthogonal_iff {N : Submodule R M} {m : M} :
-    m ∈ B.orthogonal N ↔ ∀ n ∈ N, IsOrtho B n m :=
+    m ∈ B.orthogonal N ↔ ∀ n ∈ N, B n m = 0 :=
   Iff.rfl
 
-@[simp] lemma orthogonal_bot : B.orthogonal ⊥ = ⊤ := by ext; simp [IsOrtho]
+@[simp] lemma orthogonal_bot : B.orthogonal ⊥ = ⊤ := by ext; simp
 
 theorem orthogonal_le (h : N ≤ L) : B.orthogonal L ≤ B.orthogonal N := fun _ hn l hl => hn l (h hl)
 
@@ -148,14 +165,14 @@ theorem le_orthogonal_orthogonal (b : B.IsRefl) : N ≤ B.orthogonal (B.orthogon
 
 lemma orthogonal_top_eq_ker (hB : B.IsRefl) :
     B.orthogonal ⊤ = LinearMap.ker B := by
-  ext; simp [LinearMap.BilinForm.IsOrtho, LinearMap.ext_iff, hB.eq_iff]
+  ext; simp [LinearMap.ext_iff, hB.eq_iff]
 
 lemma orthogonal_top_eq_bot (hB : B.Nondegenerate) :
     B.orthogonal ⊤ = ⊥ :=
   (Submodule.eq_bot_iff _).mpr fun x hx ↦ hB.2 x (by simpa using! hx)
 
 -- ↓ This lemma only applies in fields as we require `a * b = 0 → a = 0 ∨ b = 0`
-theorem span_singleton_inf_orthogonal_eq_bot {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :
+theorem span_singleton_inf_orthogonal_eq_bot {B : BilinForm K V} {x : V} (hx : B x x ≠ 0) :
     K ∙ x ⊓ B.orthogonal (K ∙ x) = ⊥ :=
   LinearMap.span_singleton_inf_orthogonal_eq_bot B _ hx
 
@@ -164,13 +181,13 @@ theorem orthogonal_span_singleton_eq_toLin_ker {B : BilinForm K V} (x : V) :
     B.orthogonal (K ∙ x) = LinearMap.ker (LinearMap.BilinForm.toLinHomAux₁ B x) :=
   LinearMap.orthogonal_span_singleton_eq_to_lin_ker ..
 
-theorem span_singleton_sup_orthogonal_eq_top {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :
+theorem span_singleton_sup_orthogonal_eq_top {B : BilinForm K V} {x : V} (hx : B x x ≠ 0) :
     K ∙ x ⊔ B.orthogonal (K ∙ x) = ⊤ :=
   LinearMap.span_singleton_sup_orthogonal_eq_top hx
 
 /-- Given a bilinear form `B` and some `x` such that `B x x ≠ 0`, the span of the singleton of `x`
   is complement to its orthogonal complement. -/
-theorem isCompl_span_singleton_orthogonal {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :
+theorem isCompl_span_singleton_orthogonal {B : BilinForm K V} {x : V} (hx : B x x ≠ 0) :
     IsCompl (K ∙ x) (B.orthogonal <| K ∙ x) :=
   LinearMap.isCompl_span_singleton_orthogonal hx
 
@@ -189,14 +206,14 @@ theorem nondegenerate_restrict_of_disjoint_orthogonal (B : BilinForm R₁ M₁)
 elements. -/
 theorem iIsOrtho.not_isOrtho_basis_self_of_nondegenerate {n : Type w} [Nontrivial R]
     {B : BilinForm R M} {v : Basis n R M} (h : B.iIsOrtho v) (hB : B.Nondegenerate) (i : n) :
-    ¬B.IsOrtho (v i) (v i) :=
+    B (v i) (v i) ≠ 0 :=
   h.not_isOrtho_basis_self_of_separatingLeft hB.1 i
 
 /-- Given an orthogonal basis with respect to a bilinear form, the bilinear form is nondegenerate
 iff the basis has no elements which are self-orthogonal. -/
 theorem iIsOrtho.nondegenerate_iff_not_isOrtho_basis_self {n : Type w} [IsDomain R]
     (B : BilinForm R M) (v : Basis n R M) (hO : B.iIsOrtho v) :
-    B.Nondegenerate ↔ ∀ i, ¬B.IsOrtho (v i) (v i) :=
+    B.Nondegenerate ↔ ∀ i, B (v i) (v i) ≠ 0 :=
   ⟨hO.not_isOrtho_basis_self_of_nondegenerate, hO.nondegenerate_of_not_isOrtho_basis_self _⟩
 
 section
@@ -351,7 +368,7 @@ on the whole space. -/
 /-- The restriction of a reflexive, non-degenerate bilinear form on the orthogonal complement of
 the span of a singleton is also non-degenerate. -/
 theorem restrict_nondegenerate_orthogonal_spanSingleton (B : BilinForm K V) (b₁ : B.Nondegenerate)
-    (b₂ : B.IsRefl) {x : V} (hx : ¬B.IsOrtho x x) :
+    (b₂ : B.IsRefl) {x : V} (hx : B x x ≠ 0) :
     Nondegenerate <| B.restrict <| B.orthogonal (K ∙ x) := by
   have (n : V) : n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x) :=
     (span_singleton_sup_orthogonal_eq_top hx).symm ▸ Submodule.mem_top

Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

@@ -901,16 +901,14 @@ def associatedHom : QuadraticMap R M N →ₗ[S] (BilinMap R M N) where
 
 variable (Q : QuadraticMap R M N)
 
-@[simp]
 theorem associated_apply (x y : M) :
-    associatedHom S Q x y = ⅟(2 : Module.End R N) • (Q (x + y) - Q x - Q y) :=
-  rfl
+    associatedHom S Q x y = ⅟(2 : Module.End R N) • (Q (x + y) - Q x - Q y) := rfl
 
 set_option backward.defeqAttrib.useBackward true in
 /-- Twice the associated bilinear map of `Q` is the same as the polar of `Q`. -/
 @[simp] theorem two_nsmul_associated : 2 • associatedHom S Q = Q.polarBilin := by
   ext
-  dsimp
+  dsimp [associated_apply]
   rw [← LinearMap.smul_apply, nsmul_eq_mul, Nat.cast_ofNat, mul_invOf_self', Module.End.one_apply,
     polar]
 
@@ -1065,9 +1063,9 @@ alias ⟨IsOrtho.symm, _⟩ := isOrtho_comm
 
 theorem _root_.LinearMap.BilinForm.toQuadraticMap_isOrtho [IsCancelAdd R]
     [NoZeroDivisors R] [CharZero R] {B : BilinMap R M R} {x y : M} (h : B.IsSymm) :
-    B.toQuadraticMap.IsOrtho x y ↔ B.IsOrtho x y := by
+    B.toQuadraticMap.IsOrtho x y ↔ B x y = 0 := by
   letI : AddCancelMonoid R := { ‹IsCancelAdd R›, (inferInstance : AddCommMonoid R) with }
-  simp_rw [isOrtho_def, LinearMap.isOrtho_def, B.toQuadraticMap_apply, map_add,
+  simp_rw [isOrtho_def, B.toQuadraticMap_apply, map_add,
     LinearMap.add_apply, add_comm _ (B y y), add_add_add_comm _ _ (B y y), add_comm (B y y)]
   rw [add_eq_left (a := B x x + B y y), ← h.eq, RingHom.id_apply, add_self_eq_zero]
 
@@ -1077,18 +1075,16 @@ section CommRing
 variable [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
   {Q : QuadraticMap R M N}
 
-@[simp]
-theorem isOrtho_polarBilin {x y : M} : Q.polarBilin.IsOrtho x y ↔ IsOrtho Q x y := by
-  simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]
+theorem isOrtho_polarBilin {x y : M} : Q.polarBilin x y = 0 ↔ IsOrtho Q x y := by
+  simp_rw [isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]
 
 theorem IsOrtho.polar_eq_zero {x y : M} (h : IsOrtho Q x y) : polar Q x y = 0 :=
   isOrtho_polarBilin.mpr h
 
 @[simp]
 theorem associated_isOrtho [Invertible (2 : R)] {x y : M} :
-    Q.associated.IsOrtho x y ↔ Q.IsOrtho x y := by
-  simp_rw [isOrtho_def, LinearMap.isOrtho_def, associated_apply, invOf_smul_eq_iff,
-    smul_zero, sub_sub, sub_eq_zero]
+    Q.associated x y = 0 ↔ Q.IsOrtho x y := by
+  simp_rw [isOrtho_def, associated_apply, invOf_smul_eq_iff, smul_zero, sub_sub, sub_eq_zero]
 
 end CommRing
 
@@ -1366,7 +1362,7 @@ variable [CommRing R] [AddCommGroup M] [Module R M]
 on a module `M` over a ring `R` with invertible `2`, i.e. there exists some
 `x : M` such that `B x x ≠ 0`. -/
 theorem exists_bilinForm_self_ne_zero [htwo : Invertible (2 : R)] {B : BilinForm R M}
-    (hB₁ : B ≠ 0) (hB₂ : B.IsSymm) : ∃ x, ¬B.IsOrtho x x := by
+    (hB₁ : B ≠ 0) (hB₂ : B.IsSymm) : ∃ x, B x x ≠ 0 := by
   lift B to QuadraticForm R M using hB₂ with Q
   obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁
   exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩
@@ -1410,15 +1406,15 @@ theorem exists_orthogonal_basis [hK : Invertible (2 : K)] {B : LinearMap.BilinFo
         intro y
         refine ⟨-B x y / B x x, fun z hz => ?_⟩
         obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
-        rw [IsOrtho, map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul,
+        rw [map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul,
           div_mul_cancel₀ _ hx, add_neg_cancel, mul_zero])
   refine ⟨b, ?_⟩
   rw [Basis.coe_mkFinCons]
   intro j i
   refine Fin.cases ?_ (fun i => ?_) i <;> refine Fin.cases ?_ (fun j => ?_) j <;> intro hij <;>
     simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]
   · exact (hij rfl).elim
-  · rw [IsOrtho, ← hB₂.eq]
+  · rw [← hB₂.eq]
     exact (v' j).prop _ (Submodule.mem_span_singleton_self x)
   · exact (v' i).prop _ (Submodule.mem_span_singleton_self x)
   · exact hv₁ (ne_of_apply_ne _ hij)

Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

@@ -171,7 +171,7 @@ theorem equivalent_weightedSumSquares_units_of_nondegenerate' (Q : QuadraticForm
     ∃ w : Fin (Module.finrank K V) → Kˣ, Equivalent Q (weightedSumSquares K w) := by
   obtain ⟨v, hv₁⟩ := exists_orthogonal_basis (associated_isSymm K Q)
   have hv₂ := hv₁.not_isOrtho_basis_self_of_separatingLeft hQ
-  simp_rw [LinearMap.IsOrtho, associated_eq_self_apply] at hv₂
+  simp_rw [associated_eq_self_apply] at hv₂
   exact ⟨fun i => Units.mk0 _ (hv₂ i), ⟨Q.isometryEquivWeightedSumSquares v hv₁⟩⟩
 
 variable {ι S R : Type*}

Mathlib/LinearAlgebra/QuadraticForm/Radical.lean

@@ -138,7 +138,7 @@ the radical of a quadratic map is the kernel of its associated bilinear map. -/
 lemma radical_eq_ker_associated : Q.radical = (QuadraticMap.associated Q).ker := by
   rw [radical_eq_ker_polarBilin]
   ext m
-  simp [LinearMap.ext_iff, QuadraticMap.polar, -smul_eq_mul, invOf_smul_eq_iff]
+  simp [associated_apply, LinearMap.ext_iff, QuadraticMap.polar, invOf_smul_eq_iff]
 
 /--
 If `2` is invertible in the coefficient ring,

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean

@@ -110,8 +110,10 @@ protected abbrev tmul (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂
 theorem associated_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :
     (Q₁.tmul Q₂).associated = BilinForm.tmul Q₁.associated Q₂.associated := by
   rw [BilinForm.tmul, BilinForm.tensorDistrib, LinearMap.comp_apply, ← BilinMap.tmul,
-    ← QuadraticMap.associated_tmul Q₁ Q₂]
-  aesop
+    ← QuadraticMap.associated_tmul Q₁ Q₂, LinearEquiv.coe_coe, LinearEquiv.congrRight₂_apply]
+  ext : 6
+  simp [associated_apply]
+  rfl
 
 set_option backward.isDefEq.respectTransparency false in
 theorem polarBilin_tmul [Invertible (2 : A)] (Q₁ : QuadraticForm A M₁) (Q₂ : QuadraticForm R M₂) :

Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean

@@ -47,7 +47,7 @@ theorem tmul_comp_tensorMap
   have h₃ : Q₃ = Q₄.comp g.toLinearMap := QuadraticMap.ext fun x => (g.map_app x).symm
   refine (QuadraticMap.associated_rightInverse R).injective ?_
   ext m₁ m₃ m₁' m₃'
-  simp [-associated_apply, h₁, h₃, associated_tmul]
+  simp [h₁, h₃, associated_tmul]
 
 @[simp]
 theorem tmul_tensorMap_apply
@@ -156,8 +156,7 @@ theorem comp_tensorRId_eq (Q₁ : QuadraticForm R M₁) :
     Q₁.comp (TensorProduct.rid R M₁) = Q₁.tmul (sq (R := R)) := by
   refine (QuadraticMap.associated_rightInverse R).injective ?_
   ext m₁ m₁'
-  simp only [associated_tmul, QuadraticMap.associated_comp]
-  simp [-associated_apply, one_mul]
+  simp [associated_tmul, QuadraticMap.associated_comp, one_mul]
 
 @[simp]
 theorem tmul_tensorRId_apply

Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean

@@ -328,11 +328,11 @@ lemma orthogonal_rootSpan_eq :
   rw [← LinearMap.BilinForm.orthogonal_top_eq_ker P.rootForm_symmetric.isRefl]
   refine le_antisymm ?_ (by intro; simp_all)
   rintro x hx y -
-  simp only [LinearMap.BilinForm.mem_orthogonal_iff, LinearMap.BilinForm.IsOrtho] at hx ⊢
+  simp only [LinearMap.BilinForm.mem_orthogonal_iff] at hx ⊢
   obtain ⟨u, hu, v, hv, rfl⟩ : ∃ᵉ (u ∈ P.rootSpan R) (v ∈ LinearMap.ker P.RootForm), u + v = y := by
     rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]; exact Submodule.mem_top
   simp only [LinearMap.mem_ker] at hv
-  simp [LinearMap.IsOrtho, hx _ hu, hv]
+  simp [hx _ hu, hv]
 
 @[simp]
 lemma orthogonal_corootSpan_eq :