awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
V : Type u
K : Type v
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
hK : Invertible (α := K) 2
B : BilinForm K V
hB₂ : IsSymm B
⊢ ∃ (v : Basis (Fin (finrank K V)) K V), IsOrthoᵢ (n := Fin (finrank K V)) B (⇑v : (a : Fin (finrank K V)) → V)
have suffices : ∀ (d : ℕ), finrank K V = d → ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
Tactic: suffices ∀ d, finrank K V = d → ∃ v : Basis (Fin d) K V, B.IsOrthoᵢ v by exact this _ rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
have succ : ∀ (hB₂ : IsSymm.{v, u} (R := K) (M := V) (I := RingHom.id K) 0),
  ∃ (v : Basis (Fin (d + 1)) K V),
    IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
      RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)
Tactic: obtain rfl | hB₁ := eq_or_ne B 0
Cleared hypotheses: B, hB₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
succ :
  ∀ (hB₂ : IsSymm.{v, u} (R := K) (M := V) (I := RingHom.id K) 0),
    ∃ (v : Basis (Fin (d + 1)) K V),
      IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
        RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
have succ₁ : ∀ (hB₁ : B ≠ 0), ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
Tactic: obtain rfl | hB₁ := eq_or_ne B 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm.{v, u} (R := K) (M := V) (I := RingHom.id K) 0
b : Basis (Fin (finrank K V)) K V := finBasis K V
⊢ ∃ (v : Basis (Fin (d + 1)) K V),
    IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
      RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)
have succ : ∀ (b : Basis (Fin (d + 1)) K V),
  ∃ (v : Basis (Fin (d + 1)) K V),
    IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
      RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)
Tactic: rw [hd] at b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
hB₁ : B ≠ 0
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
have succ : ∀ (x : V) (hx : ¬IsOrtho B x x),
  ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
Tactic: obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (hypothesis)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
hB₁ : B ≠ 0
x : V
hx : ¬IsOrtho B x x
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
have hd₁ : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
Tactic: rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
    finrank_span_singleton (ne_zero_of_map hx)] at hd
Cleared hypotheses: hd, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
have succ : ∀ (v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x)))
  (hv₁ :
    IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
      (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
      (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))),
  ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
Tactic: obtain ⟨v', hv₁⟩ := ih (hB₂.domRestrict _ : B'.IsSymm) (Nat.succ.inj hd)
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (hypothesis)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : y ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : c • x + y = 0
⊢ c = 0
have hc₁ : -(c • x) = y
Tactic: rw [add_eq_zero_iff_neg_eq] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (hypothesis)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : y ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
⊢ c = 0
have hy₁ : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
Tactic: rw [← hc, Submodule.neg_mem_iff] at hy
Cleared hypotheses: hy, hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (hypothesis)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
⊢ c = 0
have this : Disjoint (K ∙ x) (Submodule.orthogonalBilin B (K ∙ x))
Tactic: have := (isCompl_span_singleton_orthogonal hx).disjoint
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (hypothesis)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
this : Disjoint (K ∙ x) (Submodule.orthogonalBilin B (K ∙ x))
⊢ c = 0
have this₁ : ∀ (x_1 : V), Membership.mem (γ := Submodule K V) (K ∙ x) x_1 → x_1 ∈ Submodule.orthogonalBilin B (K ∙ x) → x_1 = 0
Tactic: rw [Submodule.disjoint_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (hypothesis)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
this :
  ∀ (x_1 : V), Membership.mem (γ := Submodule K V) (K ∙ x) x_1 → x_1 ∈ Submodule.orthogonalBilin B (K ∙ x) → x_1 = 0
⊢ c = 0
have this₁ : c • x = 0
Tactic: have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
y : V
⊢ ∃ (c : K), y + c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
have refine : ∀ (z : V) (hz : Membership.mem (γ := Submodule K V) (K ∙ x) z),
  IsOrtho B z
    (y +
      HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
        x)
Tactic: refine ⟨-B x y / B x x, fun z hz => ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
y z : V
hz : Membership.mem (γ := Submodule K V) (K ∙ x) z
⊢ IsOrtho B z
    (y +
      HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
        x)
have obtain : ∀ (c : K) (hz : Membership.mem (γ := Submodule K V) (K ∙ x) (c • x)),
  IsOrtho B (c • x)
    (y +
      HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
        x)
Tactic: obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
y : V
c : K
hz : Membership.mem (γ := Submodule K V) (K ∙ x) (c • x)
⊢ IsOrtho B (c • x)
    (y +
      HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
        x)
have rw : Eq.{v + 1} (α := K)
  ((((B : (a : V) → V →ₗ[K] K) (c • x) : V →ₗ[K] K) : (a : V) → K)
      (y +
        HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
            ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
          x) :
    K)
  (0 : K)
Tactic: rw [IsOrtho, map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul,
          div_mul_cancel₀ _ hx, add_neg_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
y : V
c : K
hz : Membership.mem (γ := Submodule K V) (K ∙ x) (c • x)
rw :
  Eq.{v + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) (c • x) : V →ₗ[K] K) : (a : V) → K)
        (y +
          HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
              ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
            x) :
      K)
    (0 : K)
⊢ IsOrtho B (c • x)
    (y +
      HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
        x)
have rw₁ : Eq.{v + 1} (α := K)
  ((HSMul.hSMul (β := V →ₗ[K] K) c ((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
      (y +
        HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
            ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
          x) :
    K)
  (0 : K)
Tactic: rw [IsOrtho, map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul,
          div_mul_cancel₀ _ hx, add_neg_cancel, mul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
y : V
c : K
hz : Membership.mem (γ := Submodule K V) (K ∙ x) (c • x)
rw :
  Eq.{v + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) (c • x) : V →ₗ[K] K) : (a : V) → K)
        (y +
          HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
              ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
            x) :
      K)
    (0 : K)
rw₁ :
  Eq.{v + 1} (α := K)
    ((HSMul.hSMul (β := V →ₗ[K] K) c ((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
        (y +
          HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
              ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
            x) :
      K)
    (0 : K)
⊢ IsOrtho B (c • x)
    (y +
      HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
        x)
have rw₂ : HSMul.hSMul (β := K) c
    ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
        (y +
          HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
              ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
            x) :
      K) =
  0
Tactic: rw [IsOrtho, map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul,
          div_mul_cancel₀ _ hx, add_neg_cancel, mul_zero]