-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem exists_orthogonal_basis [hK : Invertible (2 : K)] {B : LinearMap.BilinForm K V}
    (hB₂ : B.IsSymm) : ∃ v : Basis (Fin (finrank K V)) K V, B.IsOrthoᵢ v

Proof state:
case succ.inr
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
this : Nontrivial V
hB₁ : B ≠ 0
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂

Result:
case succ.inr.intro
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
this : Nontrivial V
hB₁ : B ≠ 0
x : V
hx : ¬IsOrtho B x x
⊢ ∃ v, IsOrthoᵢ B ⇑v

Proof state:
case succ.inr.intro
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
this : Nontrivial V
hB₁ : B ≠ 0
x : V
hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K :=
  domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
obtain ⟨v', hv₁⟩ := ih (hB₂.domRestrict _ : B'.IsSymm) (Nat.succ.inj hd)

Result:
case succ.inr.intro.intro
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
this : Nontrivial V
hB₁ : B ≠ 0
x : V
hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K :=
  domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)
v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)
hv₁ :
  (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'
⊢ ∃ v, IsOrthoᵢ B ⇑v

Proof state:
case succ.inl
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hd : finrank K V = d + 1
this : Nontrivial V
hB₂ : IsSymm 0
⊢ ∃ v, IsOrthoᵢ 0 ⇑v

Tactic:
let b := Module.finBasis K V

Result:
case succ.inl
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hd : finrank K V = d + 1
this : Nontrivial V
hB₂ : IsSymm 0
b : Basis (Fin (finrank K V)) K V := finBasis K V
⊢ ∃ v, IsOrthoᵢ 0 ⇑v

Proof state:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
this : Nontrivial V
hB₁ : B ≠ 0
x : V
hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K :=
  domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)
v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)
hv₁ :
  (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'
⊢ ∀ (z : V), ∃ c, z + c • x ∈ (Submodule.span K {x}).orthogonalBilin B

Tactic:
intro y

Result:
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
this : Nontrivial V
hB₁ : B ≠ 0
x : V
hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K :=
  domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)
v' : Basis (Fin d) K ↥((Submodule.span K {x}).orthogonalBilin B)
hv₁ :
  (domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)).IsOrthoᵢ ⇑v'
y : V
⊢ ∃ c, y + c • x ∈ (Submodule.span K {x}).orthogonalBilin B

Proof state:
case succ.inr.intro
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
this : Nontrivial V
hB₁ : B ≠ 0
x : V
hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1
hx : ¬IsOrtho B x x
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
let B' :=  B.domRestrict₁₂ (Submodule.orthogonalBilin (K ∙ x) B )
  (Submodule.orthogonalBilin (K ∙ x) B )

Result:
case succ.inr.intro
K : Type v
inst✝³ : Field K
hK : Invertible 2
d : ℕ
ih :
  ∀ {V : Type u} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] {B : BilinForm K V},
    IsSymm B → finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
V : Type u
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
this : Nontrivial V
hB₁ : B ≠ 0
x : V
hd : finrank K ↥((Submodule.span K {x}).orthogonalBilin B) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] ↥((Submodule.span K {x}).orthogonalBilin B) →ₗ[K] K :=
  domRestrict₁₂ B ((Submodule.span K {x}).orthogonalBilin B) ((Submodule.span K {x}).orthogonalBilin B)
⊢ ∃ v, IsOrthoᵢ B ⇑v