awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hc :
  ¬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 =
      0
⊢ False

Tactic:
(ne_of_lt (hp ((B x) y • x - (B x) x • y) hc)).symm <|
      (apply_smul_sub_smul_sub_eq B x y).symm ▸ (mul_eq_zero_of_right ((B x) x)
      (sub_eq_zero_of_eq he.symm))

Premises used: HSub.hSub, mul_eq_zero_of_right, Eq.rec, sub_eq_zero_of_eq, Ne.symm, HSMul.hSMul, Eq.symm, ne_of_lt, DFunLike.coe, 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hc :
  ¬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 =
      0
⊢ False

Tactic:
exact (ne_of_lt (hp ((B x) y • x - (B x) x • y) hc)).symm <|
      (apply_smul_sub_smul_sub_eq B x y).symm ▸ (mul_eq_zero_of_right ((B x) x)
      (sub_eq_zero_of_eq he.symm))

Premises used: HSub.hSub, Ne.symm, HSMul.hSMul, ne_of_lt, 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
⊢ 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 =
    0

Tactic:
have hz : (B x y) • x - (B x x) • y = 0 := by
    by_contra hc
    exact (ne_of_lt (hp ((B x) y • x - (B x) x • y) hc)).symm <|
      (apply_smul_sub_smul_sub_eq B x y).symm ▸ (mul_eq_zero_of_right ((B x) x)
      (sub_eq_zero_of_eq he.symm))
-- 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hz :
  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 =
    0
by_contra : ∀ (hL : LinearIndependent R ![x, y]), False
⊢ ¬LinearIndependent R ![x, y]

Tactic:
by_contra hL
-- 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hz :
  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 =
    0
hL : LinearIndependent R ![x, y]
pos : ∀ (hx : x = 0), False
neg : ∀ (hx : ¬x = 0), False
⊢ False

Tactic:
by_cases hx : x = 0
-- 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hz :
  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 =
    0
hL : LinearIndependent R ![x, y]
hx : x = 0
⊢ False

Tactic:
simpa [hx] using LinearIndependent.ne_zero 0 hL

Premises used: LinearIndependent.ne_zero, OfNat.ofNat
-- 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hz :
  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 =
    0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
⊢ 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 -
      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 =
    0

Tactic:
have h := sub_eq_zero.mpr (sub_eq_zero.mp hz).symm
-- 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hz :
  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 =
    0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
h :
  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 -
      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 =
    0
⊢ 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 =
    0

Tactic:
rw [sub_eq_add_neg, ← neg_smul, add_comm] at h

Premises used: neg_smul, sub_eq_add_neg, add_comm
-- 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hz :
  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 =
    0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
h :
  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 =
    0
⊢ False

Tactic:
(Ne.symm (ne_of_lt (hp x hx))) (LinearIndependent.eq_zero_of_pair hL h).2

Premises used: Ne.symm, And.right, LinearIndependent.eq_zero_of_pair, ne_of_lt
-- 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
hp : ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
x y : M
he :
  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)
hz :
  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 =
    0
hL : LinearIndependent R ![x, y]
hx : ¬x = 0
h :
  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 =
    0
⊢ False

Tactic:
exact (Ne.symm (ne_of_lt (hp x hx))) (LinearIndependent.eq_zero_of_pair hL h).2

Premises used: Ne.symm, And.right, LinearIndependent.eq_zero_of_pair, ne_of_lt
-- 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)
hB : IsSymm B
x : M
h : Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)

Tactic:
simp [h]
-- 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)
hB : IsSymm B
x : M
refine :
  ∀ (h : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)),
    Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ↔
    Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- 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)
hB : IsSymm B
x : M
h : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
h₁ :
  ∀ (y : M),
    Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) ((0 : (a : M) → R) y : R)
⊢ Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R)

Tactic:
ext 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)
hB : IsSymm B
x : M
h : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
y : M
⊢ HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 ≤
    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:
have := B.apply_sq_le_of_symm hs hB 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)
hB : IsSymm B
x : M
h : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
y : M
this :
  HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 ≤
    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)
⊢ HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 ≤ 0

Tactic:
simp only [h, zero_mul] at this

Premises used: MulZeroClass.zero_mul
-- 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)
hB : IsSymm B
x : M
h : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
y : M
this : HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 ≤ 0
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) ((0 : (a : M) → R) y : R)

Tactic:
eq_zero_of_pow_eq_zero <| le_antisymm this (sq_nonneg (B x y))

Premises used: le_antisymm, sq_nonneg, eq_zero_of_pow_eq_zero, 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)
hB : IsSymm B
x : M
h : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
y : M
this : HPow.hPow (α := R) (β := ℕ) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) 2 ≤ 0
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) ((0 : (a : M) → R) y : R)

Tactic:
exact eq_zero_of_pow_eq_zero <| le_antisymm this (sq_nonneg (B x y))

Premises used: le_antisymm, sq_nonneg, eq_zero_of_pow_eq_zero, 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)
hB : IsSymm B
simp_rw :
  (∀ (x : M), Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R) → x = 0) ↔
    ∀ (x : M), Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R) ↔ x = 0
⊢ Nondegenerate B ↔
    ∀ (x : M), Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ↔ x = 0

Tactic:
simp_rw [hB.isRefl.nondegenerate_iff_separatingLeft, separatingLeft_iff_ker_eq_bot,
    Submodule.eq_bot_iff, B.apply_apply_same_eq_zero_iff hs hB, mem_ker]

Premises used: LinearMap.BilinForm.apply_apply_same_eq_zero_iff, LinearMap.mem_ker, LinearMap.IsSymm.isRefl, Submodule.eq_bot_iff, LinearMap.separatingLeft_iff_ker_eq_bot, LinearMap.IsRefl.nondegenerate_iff_separatingLeft
-- 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)
hB : IsSymm B
x : M
⊢ Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R) → x = 0 ↔
    (Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R) ↔ x = 0)

Tactic:
aesop
-- 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)
hB : IsSymm B
⊢ (∀ (x : M), Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R) → x = 0) ↔
    ∀ (x : M), Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R) ↔ x = 0

Tactic:
exact forall_congr' fun x ↦ by aesop

Premises used: forall_congr'
-- 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)
hB : IsSymm B
rw :
  (∀ (x : M), Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ↔ x = 0) ↔
    ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ Nondegenerate B ↔
    ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
rw [B.nondegenerate_iff hs hB]

Premises used: LinearMap.BilinForm.nondegenerate_iff
-- 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)
hB : IsSymm B
contrapose! :
  (∃ (x : M),
      Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ∧ x ≠ 0 ∨
        Ne.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ∧ x = 0) ↔
    ∃ (x : M), x ≠ 0 ∧ LE.le.{u_1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
⊢ (∀ (x : M), Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ↔ x = 0) ↔
    ∀ (x : M), x ≠ 0 → LT.lt.{u_1} (α := R) (0 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)

Tactic:
contrapose!
-- 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)
hB : IsSymm B
x : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ∧ x ≠ 0 ∨
      Ne.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ∧ x = 0 →
    x ≠ 0 ∧ LE.le.{u_1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)

Tactic:
aesop
-- 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)
hB : IsSymm B
⊢ (∃ (x : M),
      Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ∧ x ≠ 0 ∨
        Ne.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R) ∧ x = 0) ↔
    ∃ (x : M), x ≠ 0 ∧ LE.le.{u_1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)

Tactic:
exact exists_congr fun x ↦ ⟨by aesop, fun ⟨h₀, h⟩ ↦ Or.inl ⟨le_antisymm h (hs x), h₀⟩⟩

Premises used: exists_congr, Iff.intro
-- 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)
hB : IsSymm B
W : Submodule R M
⊢ (domRestrict₁₂ B W W).Nondegenerate ↔ Disjoint W (ker B)

Tactic:
⟨disjoint_ker_of_nondegenerate_restrict, fun hW ↦ ?_⟩

Premises used: LinearMap.disjoint_ker_of_nondegenerate_restrict, Iff.intro