awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
hy : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : 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)
have inr : Eq.{u_1 + 1} (α := 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: suffices B x y = - B y x by simpa [this, hx, hy] using mul_self_nonneg (B y x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
hy : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ Eq.{u_1 + 1} (α := 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)
have inr : HAdd.hAdd (α := 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) =
  0
Tactic: rw [eq_neg_iff_add_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
hy : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ HAdd.hAdd (α := 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) =
    0
have inr : HAdd.hAdd (α := 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) ≤
  0
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
hy : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
inr :
  HAdd.hAdd (α := 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) ≤
    0
⊢ HAdd.hAdd (α := 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) =
    0
have inr₁ : 0 ≤
  HAdd.hAdd (α := 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: apply le_antisymm
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 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) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have rw : 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) (β := 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 [sq, ← hB.eq, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 y : M
rw :
  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) (β := 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)
⊢ 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) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have rw₁ : HMul.hMul (α := R) (β := R)
    ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
    ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R) =
  HMul.hMul (α := R) (β := R)
    ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: rw [sq, ← hB.eq, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 y : M
rw :
  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) (β := 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)
rw₁ :
  HMul.hMul (α := R) (β := R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R) =
    HMul.hMul (α := R) (β := R)
      ((RingHom.id R : (a : R) → R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R) : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ 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) y : R)
      ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
have rw₂ : HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : 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) y : M →ₗ[R] R) : (a : M) → R) x : R)
    ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: rw [sq, ← hB.eq, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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 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)
have rw : 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: rw [show (B x y) ^ 2 = (B x y) * (B y x) by rw [sq, ← hB.eq, RingHom.id_apply]]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
have by_contra : ∀
  (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: by_contra hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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)
⊢ ¬LinearIndependent R ![x, y]
have 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
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))
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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]
⊢ False
have pos : ∀ (hx : x = 0), False
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ False
have neg : ∀ (hx : ¬x = 0), False
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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
have 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
Tactic: have h := sub_eq_zero.mpr (sub_eq_zero.mp hz).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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
⊢ False
have 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
Tactic: rw [sub_eq_add_neg, ← neg_smul, add_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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) ↔
    Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R)
have 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)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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)
⊢ Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) (0 : M →ₗ[R] R)
have 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)
Tactic: ext y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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
⊢ 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)
have 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)
Tactic: have := B.apply_sq_le_of_symm hs hB x y
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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)
⊢ 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)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ 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)
have 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)
Tactic: rw [B.nondegenerate_iff hs hB]