awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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
⊢ 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₃ : c •
    HAdd.hAdd (α := 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)
          (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]
-- 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)))
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)
have succ : IsOrthoᵢ (n := Fin (d + 1)) B (⇑b : (a : Fin (d + 1)) → V)
Tactic: refine ⟨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
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' ⋯ ⋯
⊢ IsOrthoᵢ (n := Fin (d + 1)) B (⇑b : (a : Fin (d + 1)) → V)
have 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)))))
Tactic: rw [Basis.coe_mkFinCons]
-- 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)))
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
have 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
Tactic: refine Fin.cases ?_ (fun i => ?_) i
-- 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)))
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
⊢ 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
have 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
Tactic: refine Fin.cases ?_ (fun i => ?_) i
-- 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)))
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
have 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
Tactic: refine Fin.cases ?_ (fun j => ?_) j
-- 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)))
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
⊢ 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
have 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
Tactic: refine Fin.cases ?_ (fun j => ?_) j
-- 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)))
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
have 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
Tactic: refine Fin.cases ?_ (fun j => ?_) j
-- 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)))
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
⊢ 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
have 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
Tactic: refine Fin.cases ?_ (fun j => ?_) j
-- 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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i : Fin (d + 1)
hij : 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
have succ : IsOrtho B x x
Tactic: simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]
-- 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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i : Fin (d + 1)
j : Fin d
hij : 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
have succ : IsOrtho B (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V) x
Tactic: simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]
-- 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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j i_1 : Fin (d + 1)
i : Fin d
hij : 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
have succ : IsOrtho B x (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) i) : V)
Tactic: simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]