awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
hi : i ∉ vi.support
⊢ Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)

Tactic:
replace hi : vi i = 0 := Finsupp.notMem_support_iff.mp hi
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
vi : n →₀ R
i : n
hB :
  Eq.{u_22 + 1} (α := M₁)
    (∑ x ∈ vi.support,
      HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) x : R) : R)
        ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) x) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
          M₁))
    0
hi : Eq.{u_20 + 1} (α := R) ((vi : (a : n) → R) i : R) (0 : R)
h₁ :
  HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) 0 : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
h₂ :
  HSMul.hSMul.{u_20, u_22, u_22} (α := R) (β := M₁) 0
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0
h₃ h₄ : Eq.{u_22 + 1} (α := M₁) 0 0
⊢ HSMul.hSMul (α := R) (β := M₁) ((RingHom.id R : (a : R) → R) ((vi : (a : n) → R) i : R) : R)
      ((((B : (a : M) → M →ₗ[R] M₁) ((v : (a : n) → M) i) : M →ₗ[R] M₁) : (a : M) → M₁) ((v : (a : n) → M) i : M) :
        M₁) =
    0

Tactic:
rw [hi, RingHom.id_apply, zero_smul]

Premises used: RingHom.id_apply, zero_smul
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
⊢ IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)

Tactic:
rw [isOrthoᵢ_flip] at hO

Premises used: LinearMap.isOrthoᵢ_flip
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
hO₁ : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
⊢ ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
rw [isOrthoᵢ_flip] at hO

Premises used: LinearMap.isOrthoᵢ_flip
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
rw : B.flip.SeparatingLeft
⊢ B.SeparatingRight

Tactic:
rw [← flip_separatingLeft]

Premises used: LinearMap.flip_separatingLeft
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
⊢ B.flip.SeparatingLeft

Tactic:
IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO fun i ↦ ?_

Premises used: LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
refine : ∀ (i : n), ¬B.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
⊢ B.flip.SeparatingLeft

Tactic:
refine IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO fun i ↦ ?_

Premises used: LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
i : n
rw : ¬B.flip.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
⊢ ¬B.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
rw [isOrtho_flip]

Premises used: LinearMap.isOrtho_flip
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
i : n
⊢ ¬B.flip.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
h i

Premises used: LinearMap.mk₂'ₛₗ, LinearMap.flip
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B.flip (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
i : n
⊢ ¬B.flip.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)

Tactic:
exact h i
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : Module R M
inst_4 : Module R M₁
inst_5 : IsDomain R
inst_6 : IsTorsionFree R M₁
B : M →ₗ[R] M →ₗ[R] M₁
v : Basis n R M
hO : IsOrthoᵢ.{u_20, u_20, u_22, u_21, u_19} (n := n) B (⇑v : (a : n) → M)
h : ∀ (i : n), ¬B.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
⊢ B.Nondegenerate

Tactic:
⟨IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO h,
    IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self v hO h⟩

Premises used: And.intro, LinearMap.IsOrthoᵢ.separatingRight_iff_not_isOrtho_basis_self, LinearMap.IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self, LinearMap.Nondegenerate
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : LinearMap.BilinForm R M
x y : M
simp :
  HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) -
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)) -
      (HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) -
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R))) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)) -
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
⊢ (((B : (a : M) → M →ₗ[R] R)
            (HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) x -
              HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
                y) :
          M →ₗ[R] R) :
        (a : M) → R)
      (HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) x -
        HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) y) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) -
        HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))

Tactic:
simp only [map_sub, map_smul, sub_apply, smul_apply, smul_eq_mul, mul_sub,
    mul_comm (B x y) (B x x), mul_left_comm (B x y) (B x x)]

Premises used: map_sub, mul_sub, LinearMap.smul_apply, mul_left_comm, mul_comm, LinearMap.sub_apply, smul_eq_mul, DFunLike.coe, map_smul
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : LinearMap.BilinForm R M
x y : M
⊢ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) -
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)) -
      (HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)) -
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R))) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)) -
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x_1 y_1 x y : M
rw :
  LE.le.{u_1} (α := R) (0 : R)
    ((((B : (a : M) → M →ₗ[R] R)
              (HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
                  x -
                HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
                  y) :
            M →ₗ[R] R) :
          (a : M) → R)
        (HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) x -
          HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) y) :
      R)
⊢ 0 ≤
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) -
        HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
          ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))

Tactic:
rw [← apply_smul_sub_smul_sub_eq B x y]

Premises used: LinearMap.BilinForm.apply_smul_sub_smul_sub_eq
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x_1 y_1 x y : M
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((((B : (a : M) → M →ₗ[R] R)
              (HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
                  x -
                HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
                  y) :
            M →ₗ[R] R) :
          (a : M) → R)
        (HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) x -
          HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) y) :
      R)

Tactic:
hs (B x y • x - B x x • y)

Premises used: HSub.hSub, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x_1 y_1 x y : M
⊢ LE.le.{u_1} (α := R) (0 : R)
    ((((B : (a : M) → M →ₗ[R] R)
              (HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
                  x -
                HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
                  y) :
            M →ₗ[R] R) :
          (a : M) → R)
        (HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) x -
          HSMul.hSMul.{u_1, u_5, u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) y) :
      R)

Tactic:
exact hs (B x y • x - B x x • y)

Premises used: HSub.hSub, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
⊢ ∀ (x y : M),
    0 ≤
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) -
          HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))

Tactic:
have aux (x y : M) : 0 ≤ (B x x) * ((B x x) * (B y y) - (B x y) * (B y x)) := by
    rw [← apply_smul_sub_smul_sub_eq B x y]
    exact hs (B x y • x - B x x • y)
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
aux :
  ∀ (x y : M),
    0 ≤
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) -
          HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
inl :
  ∀ (hx : LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) ≤
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)
inr :
  ∀ (hx : LE.le.{u_1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)),
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) ≤
      HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
rcases lt_or_ge 0 (B x x) with hx | hx

Premises used: lt_or_ge, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
aux :
  ∀ (x y : M),
    0 ≤
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) -
          HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
hx : LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux x y) hx

Premises used: nonneg_of_mul_nonneg_right, Iff.mp, sub_nonneg
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
aux :
  ∀ (x y : M),
    0 ≤
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) -
          HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
hx : LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) ≤
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
exact sub_nonneg.mp <| nonneg_of_mul_nonneg_right (aux x y) hx

Premises used: nonneg_of_mul_nonneg_right, Iff.mp, sub_nonneg
-- Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic
Goal:
R : Type u_1
M : Type u_5
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), LE.le.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
aux :
  ∀ (x y : M),
    0 ≤
      HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
        (HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) -
          HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
            ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R))
hx : LE.le.{u_1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)

Tactic:
replace hx : B x x = 0 := le_antisymm hx (hs x)