awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i : Fin (d + 1)
j : Fin d
hij : j.succ ≠ 0
succ : IsOrtho B (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V) x
⊢ Function.onFun (IsOrtho B)
    (Fin.cons (α := fun (i : Fin (d + 1)) ↦ V) x
      (Function.comp (β := ↥(Submodule.orthogonalBilin B (K ∙ x)))
        (Subtype.val (p := fun (x_1 : V) ↦ x_1 ∈ Submodule.orthogonalBilin B (K ∙ x)))
        (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))))
    j.succ 0

Tactic:
simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]

Premises used: Fin.cons_succ, Function.onFun, Function.comp_apply, Fin.cons_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i_1 : Fin (d + 1)
i : Fin d
hij : 0 ≠ i.succ
succ : IsOrtho B x (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) i) : V)
⊢ Function.onFun (IsOrtho B)
    (Fin.cons (α := fun (i : Fin (d + 1)) ↦ V) x
      (Function.comp (β := ↥(Submodule.orthogonalBilin B (K ∙ x)))
        (Subtype.val (p := fun (x_1 : V) ↦ x_1 ∈ Submodule.orthogonalBilin B (K ∙ x)))
        (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))))
    0 i.succ

Tactic:
simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]

Premises used: Fin.cons_succ, Function.onFun, Function.comp_apply, Fin.cons_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i_1 : Fin (d + 1)
i j : Fin d
hij : j.succ ≠ i.succ
succ :
  IsOrtho B (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V)
    (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) i) : V)
⊢ Function.onFun (IsOrtho B)
    (Fin.cons (α := fun (i : Fin (d + 1)) ↦ V) x
      (Function.comp (β := ↥(Submodule.orthogonalBilin B (K ∙ x)))
        (Subtype.val (p := fun (x_1 : V) ↦ x_1 ∈ Submodule.orthogonalBilin B (K ∙ x)))
        (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))))
    j.succ i.succ

Tactic:
simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]

Premises used: Fin.cons_succ, Function.onFun, Function.comp_apply, Fin.cons_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i : Fin (d + 1)
hij : Ne (α := Fin (d + 1)) 0 0
⊢ IsOrtho B x x

Tactic:
(hij rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i : Fin (d + 1)
hij : Ne (α := Fin (d + 1)) 0 0
⊢ IsOrtho B x x

Tactic:
exact (hij rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i : Fin (d + 1)
j : Fin d
hij : j.succ ≠ 0
succ :
  Eq (α := K)
    ((RingHom.id K : (a : K) → K)
        ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
            (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V) :
          K) :
      K)
    (0 : K)
⊢ IsOrtho B (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V) x

Tactic:
rw [IsOrtho, ← hB₂.eq]

Premises used: LinearMap.IsOrtho, LinearMap.IsSymm.eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i : Fin (d + 1)
j : Fin d
hij : j.succ ≠ 0
⊢ Eq (α := K)
    ((RingHom.id K : (a : K) → K)
        ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
            (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V) :
          K) :
      K)
    (0 : K)

Tactic:
(v' j).prop _ (Submodule.mem_span_singleton_self x)

Premises used: LinearMap.IsOrtho, Submodule.mem_span_singleton_self, Subtype.prop, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i : Fin (d + 1)
j : Fin d
hij : j.succ ≠ 0
⊢ Eq (α := K)
    ((RingHom.id K : (a : K) → K)
        ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
            (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V) :
          K) :
      K)
    (0 : K)

Tactic:
exact (v' j).prop _ (Submodule.mem_span_singleton_self x)

Premises used: Submodule.mem_span_singleton_self, Subtype.prop, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i_1 : Fin (d + 1)
i : Fin d
hij : 0 ≠ i.succ
⊢ IsOrtho B x (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) i) : V)

Tactic:
(v' i).prop _ (Submodule.mem_span_singleton_self x)

Premises used: Submodule.mem_span_singleton_self, Subtype.prop, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i_1 : Fin (d + 1)
i : Fin d
hij : 0 ≠ i.succ
⊢ IsOrtho B x (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) i) : V)

Tactic:
exact (v' i).prop _ (Submodule.mem_span_singleton_self x)

Premises used: Submodule.mem_span_singleton_self, Subtype.prop, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i_1 : Fin (d + 1)
i j : Fin d
hij : j.succ ≠ i.succ
⊢ IsOrtho B (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V)
    (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) i) : V)

Tactic:
hv₁ (ne_of_apply_ne _ hij)

Premises used: LinearMap.domRestrict₂, LinearMap.IsOrtho, ne_of_apply_ne, LinearMap.domRestrict₁₂
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i_1 : Fin (d + 1)
i j : Fin d
hij : j.succ ≠ i.succ
⊢ IsOrtho B (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V)
    (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) i) : V)

Tactic:
exact hv₁ (ne_of_apply_ne _ hij)

Premises used: ne_of_apply_ne
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
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
d : ℕ
hd : finrank K V = d
zero :
  ∀ {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 = 0), ∃ (v : Basis (Fin 0) K V), IsOrthoᵢ (n := Fin 0) B (⇑v : (a : Fin 0) → V)
succ :
  ∀ (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_4 : AddCommGroup V] [inst_5 : Module K V] [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)
⊢ ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)

Tactic:
induction d generalizing V with
  | zero => exact ⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩
  | succ d ih =>
  -- either the bilinear form is trivial or we can pick a non-null `x`
  obtain rfl | hB₁ := eq_or_ne B 0
  · let b := Module.finBasis K V
    rw [hd] at b
    exact ⟨b, fun i j _ => rfl⟩
  obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂
  rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
    finrank_span_singleton (ne_zero_of_map hx)] at hd
  let B' := B.domRestrict₁₂ ((K ∙ x).orthogonalBilin B) ((K ∙ x).orthogonalBilin B)
  obtain ⟨v', hv₁⟩ := ih (hB₂.domRestrict _ : B'.IsSymm) (Nat.succ.inj hd)
  -- concatenate `x` with the basis obtained by induction
  let b :=
    Basis.mkFinCons x v'
      (by
        rintro c y hy hc
        rw [add_eq_zero_iff_neg_eq] at hc
        rw [← hc, Submodule.neg_mem_iff] at hy
        have := (isCompl_span_singleton_orthogonal hx).disjoint
        rw [Submodule.disjoint_def] at this
        have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy
        exact (smul_eq_zero.1 this).resolve_right fun h => hx <| h.symm ▸ map_zero _)
      (by
        intro y
        refine ⟨-B x y / B x x, fun z hz => ?_⟩
        obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
        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])
  refine ⟨b, ?_⟩
  rw [Basis.coe_mkFinCons]
  intro j i
  refine Fin.cases ?_ (fun i => ?_) i <;> refine Fin.cases ?_ (fun j => ?_) j <;> intro hij <;>
    simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]
  · exact (hij rfl).elim
  · rw [IsOrtho, ← hB₂.eq]
    exact (v' j).prop _ (Submodule.mem_span_singleton_self x)
  · exact (v' i).prop _ (Submodule.mem_span_singleton_self x)
  · exact hv₁ (ne_of_apply_ne _ hij)

Premises used: Fin.cons_succ, Function.onFun, LinearMap.IsOrtho, LinearMap.IsSymm.eq, eq_or_ne, Function.comp_apply, Module.Basis.coe_mkFinCons, OfNat.ofNat, rfl, Fin.cons_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_8
inst_5 : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
rw :
  Eq.{u_5 + 1} (α := N) ((Q.basisRepr v : (a : ι → R) → N) w : N)
    ((Q : (a : M) → N) ((v.equivFun.symm : (a : ι → R) → M) w : M) : N)
⊢ Eq.{u_5 + 1} (α := N) ((Q.basisRepr v : (a : ι → R) → N) w : N)
    ((Q : (a : M) → N) (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) : N)

Tactic:
rw [← v.equivFun_symm_apply]

Premises used: Module.Basis.equivFun_symm_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_8
inst_5 : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
⊢ Eq.{u_5 + 1} (α := N) ((Q.basisRepr v : (a : ι → R) → N) w : N)
    ((Q : (a : M) → N) ((v.equivFun.symm : (a : ι → R) → M) w : M) : N)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
S : Type u_1
R : Type u_3
inst : CommSemiring R
ι : Type u_8
inst_1 : Fintype ι
inst_2 : Monoid S
inst_3 : DistribMulAction S R
inst_4 : SMulCommClass S R R
w : ι → S
v : ι → R
⊢ Eq.{u_3 + 1} (α := R) ((weightedSumSquares R w : (a : ι → R) → R) v : R) (∑ i : ι, w i • (v i * v i) : R)

Tactic:
QuadraticMap.sum_apply _ _ _

Premises used: QuadraticMap.sum_apply