awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ 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
have h₃ : Eq.{u_22 + 1} (α := M₁) 0 0
Tactic: rw [hi, RingHom.id_apply, zero_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (hypothesis)
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.SeparatingRight
have hO₁ : 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
Cleared hypotheses: hO, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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.SeparatingRight
have rw : B.flip.SeparatingLeft
Tactic: rw [← flip_separatingLeft]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
have refine : ∀ (i : n), ¬B.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
Tactic: refine IsOrthoᵢ.separatingLeft_of_not_isOrtho_basis_self v hO fun i ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
have rw : ¬B.flip.flip.IsOrtho ((v : (a : n) → M) i) ((v : (a : n) → M) i)
Tactic: rw [isOrtho_flip]
-- Lean 4 proof step from Mathlib.LinearAlgebra.SesquilinearForm.Basic (goal)
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
⊢ (((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))
have 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))
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)]
-- 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_1 y_1 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))
have 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)
Tactic: rw [← apply_smul_sub_smul_sub_eq B 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)
x y : M
⊢ 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 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))
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)
-- 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))
⊢ 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 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)
Tactic: rcases lt_or_ge 0 (B x x) with hx | hx
-- 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))
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)
⊢ 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 : ∀ (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)
Tactic: rcases lt_or_ge 0 (B x x) with hx | hx
-- 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)
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)
⊢ 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 hx₁ : 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)
Cleared hypotheses: hx
-- 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)
⊢ 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 : ∀ (hy : LT.lt.{u_1} (α := R) (0 : 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 y y) with hy | hy
-- 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)
inr :
  ∀ (hy : LT.lt.{u_1} (α := R) (0 : 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)
⊢ 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₁ : ∀ (hy : LE.le.{u_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)
Tactic: rcases lt_or_ge 0 (B y y) with hy | hy
-- 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 : LT.lt.{u_1} (α := R) (0 : 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)
have inr : 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) x : M →ₗ[R] R) : (a : M) → R) y : R) ≤
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
Tactic: rw [mul_comm (B x y), mul_comm (B x x)]
-- 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)
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 : LE.le.{u_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 hy₁ : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) y : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
Tactic: replace hy : B y y = 0 := le_antisymm hy (hs y)
Cleared hypotheses: hy