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)))
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
this_1 :
  ∀ (x_1 : V), Membership.mem (γ := Submodule K V) (K ∙ x) x_1 → x_1 ∈ Submodule.orthogonalBilin B (K ∙ x) → x_1 = 0
this : c • x = 0
⊢ c = 0

Tactic:
exact (smul_eq_zero.1 this).resolve_right fun h => hx <| h.symm ▸ map_zero _

Premises used: Eq.rec, map_zero, Iff.mp, Or.resolve_right, OfNat.ofNat, Eq.symm, DFunLike.coe, smul_eq_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)))
y : V
⊢ ∃ (c : K), y + c • x ∈ Submodule.orthogonalBilin B (K ∙ x)

Tactic:
⟨-B x y / B x x, fun z hz => ?_⟩

Premises used: HDiv.hDiv, Exists.intro, DFunLike.coe, Neg.neg
-- 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)))
y : V
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)
⊢ ∃ (c : K), y + c • x ∈ Submodule.orthogonalBilin B (K ∙ x)

Tactic:
refine ⟨-B x y / B x x, fun z hz => ?_⟩
-- 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)))
y z : V
hz : Membership.mem (γ := Submodule K V) (K ∙ x) z
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)
⊢ 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:
obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz

Premises used: Submodule.mem_span_singleton, Iff.mp, 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' ⋯ ⋯
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)

Tactic:
⟨b, ?_⟩

Premises used: Exists.intro
-- 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' ⋯ ⋯
succ : IsOrthoᵢ (n := Fin (d + 1)) B (⇑b : (a : Fin (d + 1)) → V)
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)

Tactic:
refine ⟨b, ?_⟩
-- 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' ⋯ ⋯
succ :
  IsOrthoᵢ (n := Fin (d + 1)) 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)))))
⊢ IsOrthoᵢ (n := Fin (d + 1)) B (⇑b : (a : Fin (d + 1)) → V)

Tactic:
rw [Basis.coe_mkFinCons]

Premises used: Module.Basis.coe_mkFinCons
-- 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)
⊢ j ≠ i →
    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 i

Tactic:
Fin.cases ?_ (fun i => ?_) i

Premises used: Fin.cases
-- 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)
succ :
  j ≠ 0 →
    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 0
succ₁ :
  ∀ (i : Fin d),
    j ≠ i.succ →
      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 i.succ
⊢ j ≠ i →
    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 i

Tactic:
refine Fin.cases ?_ (fun i => ?_) i
-- 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)
⊢ j ≠ 0 →
    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 0

Tactic:
Fin.cases ?_ (fun j => ?_) j

Premises used: Fin.cases
-- 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)
succ :
  Ne (α := Fin (d + 1)) 0 0 →
    Function.onFun (α := Fin (d + 1)) (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 0
succ₁ :
  ∀ (j : Fin d),
    j.succ ≠ 0 →
      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
⊢ j ≠ 0 →
    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 0

Tactic:
refine Fin.cases ?_ (fun j => ?_) j
-- 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
⊢ j ≠ i.succ →
    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 i.succ

Tactic:
Fin.cases ?_ (fun j => ?_) j

Premises used: Fin.cases
-- 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
succ :
  0 ≠ i.succ →
    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
succ₁ :
  ∀ (j : Fin d),
    j.succ ≠ i.succ →
      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
⊢ j ≠ i.succ →
    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 i.succ

Tactic:
refine Fin.cases ?_ (fun j => ?_) j
-- 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
succ : IsOrtho B x x
⊢ Function.onFun (α := Fin (d + 1)) (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 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