awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
refine_1 :
  ∀ (m : ↥(B.orthogonal (K ∙ x)))
    (hm :
      ∀ (y : ↥(B.orthogonal (K ∙ x))),
        Eq.{u_6 + 1} (α := K)
          ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
                  LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
                (a : ↥(B.orthogonal (K ∙ x))) → K)
              y :
            K)
          (0 : K))
    (n : V), Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)
⊢ Nondegenerate (M := ↥(B.orthogonal (K ∙ x))) (B.restrict (B.orthogonal (K ∙ x)))
have refine_2 : ∀ (m : ↥(B.orthogonal (K ∙ x)))
  (hm :
    ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
      Eq.{u_6 + 1} (α := K)
        ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
                LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
              (a : ↥(B.orthogonal (K ∙ x))) → K)
            m :
          K)
        (0 : K))
  (n : V), Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) n : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
Tactic: refine ⟨fun m hm => Submodule.coe_eq_zero.1 (b₁.1 m fun n ↦ ?_),
    fun m hm => Submodule.coe_eq_zero.1 (b₁.2 m fun n ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (y : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          y :
        K)
      (0 : K)
n : V
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)
have refine_1 : ∀ (y : V) (hy : Membership.mem (γ := Submodule K V) (K ∙ x) y) (z : V) (hz : z ∈ B.orthogonal (K ∙ x)),
  Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) (y + z) : K) (0 : K)
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.1 <| this n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          m :
        K)
      (0 : K)
n : V
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) n : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
have refine_2 : ∀ (y : V) (hy : Membership.mem (γ := Submodule K V) (K ∙ x) y) (z : V) (hz : z ∈ B.orthogonal (K ∙ x)),
  Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (y + z) : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.1 <| this n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (y : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          y :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) (y + z) : K) (0 : K)
have refine_1 : HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) y : K)
    ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) =
  0
Tactic: rw [add_right, b₂ y m <| m.2 y hy, show B m z = 0 from hm ⟨z, hz⟩, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (y : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          y :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
refine_1 :
  HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) y : K)
      ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) =
    0
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) (y + z) : K) (0 : K)
have refine_1₁ : HAdd.hAdd (α := K) (β := K) (0 : K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) = 0
Tactic: rw [add_right, b₂ y m <| m.2 y hy, show B m z = 0 from hm ⟨z, hz⟩, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (y : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          y :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
refine_1 :
  HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) y : K)
      ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) =
    0
refine_1₁ :
  HAdd.hAdd (α := K) (β := K) (0 : K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) = 0
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) (y + z) : K) (0 : K)
have refine_1₂ : HAdd.hAdd (α := K) 0 0 = 0
Tactic: rw [add_right, b₂ y m <| m.2 y hy, show B m z = 0 from hm ⟨z, hz⟩, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (y : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          y :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
refine_1 :
  HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) y : K)
      ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) =
    0
refine_1₁ :
  HAdd.hAdd (α := K) (β := K) (0 : K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) z : K) = 0
refine_1₂ : HAdd.hAdd (α := K) 0 0 = 0
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) (y + z) : K) (0 : K)
have refine_1₃ : Eq.{u_6 + 1} (α := K) 0 0
Tactic: rw [add_right, b₂ y m <| m.2 y hy, show B m z = 0 from hm ⟨z, hz⟩, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          m :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (y + z) : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
have refine_2 : HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) y : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K)
    ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) =
  0
Tactic: rw [add_left, m.2 y hy, show B z m = 0 from hm ⟨z, hz⟩, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          m :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
refine_2 :
  HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) y : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K)
      ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) =
    0
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (y + z) : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
have refine_2₁ : HAdd.hAdd (α := K) (β := K) (0 : K) ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) = 0
Tactic: rw [add_left, m.2 y hy, show B z m = 0 from hm ⟨z, hz⟩, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          m :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
refine_2 :
  HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) y : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K)
      ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) =
    0
refine_2₁ :
  HAdd.hAdd (α := K) (β := K) (0 : K) ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) = 0
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (y + z) : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
have refine_2₂ : HAdd.hAdd (α := K) 0 0 = 0
Tactic: rw [add_left, m.2 y hy, show B z m = 0 from hm ⟨z, hz⟩, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
m : ↥(B.orthogonal (K ∙ x))
hm :
  ∀ (x_1 : ↥(B.orthogonal (K ∙ x))),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) x_1 :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
            (a : ↥(B.orthogonal (K ∙ x))) → K)
          m :
        K)
      (0 : K)
y : V
hy : Membership.mem (γ := Submodule K V) (K ∙ x) y
z : V
hz : z ∈ B.orthogonal (K ∙ x)
refine_2 :
  HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) y : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K)
      ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) =
    0
refine_2₁ :
  HAdd.hAdd (α := K) (β := K) (0 : K) ((((B : (a : V) → V →ₗ[K] K) z : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) = 0
refine_2₂ : HAdd.hAdd (α := K) 0 0 = 0
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (y + z) : V →ₗ[K] K) : (a : V) → K) (↑m : V) : K) (0 : K)
have refine_2₃ : Eq.{u_6 + 1} (α := K) 0 0
Tactic: rw [add_left, m.2 y hy, show B z m = 0 from hm ⟨z, hz⟩, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
h_1 : B.IsSymm
h :
  ∀ (x y : M),
    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)
⊢ (flipHom : (a : BilinForm R M) → BilinForm R M) B = B
have H : ∀ (x y : M),
  Eq.{u_1 + 1} (α := R)
    ((((((flipHom : (a : BilinForm R M) → BilinForm R M) B : BilinForm R M) : (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)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
h : (flipHom : (a : BilinForm R M) → BilinForm R M) B = B
x y : M
⊢ 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 rw : Eq.{u_1 + 1} (α := R)
  ((((((flipHom : (a : BilinForm R M) → BilinForm R M) B : BilinForm R M) : (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 [← flip_apply, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
h : (flipHom : (a : BilinForm R M) → BilinForm R M) B = B
x y : M
rw :
  Eq.{u_1 + 1} (α := R)
    ((((((flipHom : (a : BilinForm R M) → BilinForm R M) B : BilinForm R M) : (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)
⊢ 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 rw₁ : Eq.{u_1 + 1} (α := 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 [← flip_apply, h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HSub.hSub (β := R)
        (HSub.hSub (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) (x + y) : M →ₗ[R] R) : (a : M) → R) (x + y) : 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) /
      2
have simp : (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
  HSub.hSub (β := R)
      (HSub.hSub (β := R)
        (HAdd.hAdd (α := 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) x : 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) y : 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) /
    2
Tactic: simp only [map_add, LinearMap.add_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HSub.hSub (β := R)
        (HSub.hSub (β := R)
          (HAdd.hAdd (α := 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) x : 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) y : 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) /
      2
have rw : (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
  HSub.hSub (β := R)
      (HSub.hSub (β := R)
        (HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
            ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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) y : 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) /
    2
Tactic: rw [hB.eq y x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HSub.hSub (β := R)
        (HSub.hSub (β := R)
          (HAdd.hAdd (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
              ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : 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) y : 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) /
      2
have ring_nf : (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (2⁻¹ : R) * 2
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (2⁻¹ : R) * 2
have rw : (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
  HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (HMul.hMul (α := R) 2⁻¹ 2)
Tactic: rw [mul_assoc, inv_mul_cancel₀ two_ne_zero, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
rw :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (HMul.hMul (α := R) 2⁻¹ 2)
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (2⁻¹ : R) * 2
have rw₁ : (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
  HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (1 : R)
Tactic: rw [mul_assoc, inv_mul_cancel₀ two_ne_zero, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B : BilinForm R M
x y : M
hB : B.IsSymm
rw :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (HMul.hMul (α := R) 2⁻¹ 2)
rw₁ :
  (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (1 : R)
⊢ (((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y =
    HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (2⁻¹ : R) * 2
have rw₂ : Eq.{u_8 + 1} (α := 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)
Tactic: rw [mul_assoc, inv_mul_cancel₀ two_ne_zero, mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Properties (goal)
Goal:
M : Type u_2
inst : AddCommMonoid M
R : Type u_8
inst_1 : Field R
inst_2 : NeZero.{u_8} (R := R) 2
inst_3 : Module R M
B C : BilinForm R M
hB : B.IsSymm
hC : C.IsSymm
h :
  ∀ (x : M),
    Eq.{u_8 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((((C : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
⊢ B = C
have H : ∀ (x y : M),
  Eq.{u_8 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
    ((((C : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
Tactic: ext x y