-- 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:
V : Type u
K : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hK : Invertible 2
B : BilinForm K V
hB₂ : IsSymm B
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
suffices ∀ d, finrank K V = d → ∃ v : Basis (Fin d) K V, B.IsOrthoᵢ v by exact this _ rfl

Result:
V : Type u
K : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hK : Invertible 2
B : BilinForm K V
hB₂ : IsSymm B
⊢ ∀ (d : ℕ), finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v

Proof state:
V : Type u
K : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
hK : Invertible 2
B : BilinForm K V
hB₂ : IsSymm B
this : ∀ (d : ℕ), finrank K V = d → ∃ v, IsOrthoᵢ B ⇑v
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
exact this _ rfl

Result:
no goals

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
b : Basis (Fin (d + 1)) K V
⊢ ∃ v, IsOrthoᵢ 0 ⇑v

Tactic:
exact ⟨b, fun i j _ => rfl⟩

Result:
no goals

Proof state:
case 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'
y : V
c : K
hz : c • x ∈ Submodule.span K {x}
⊢ IsOrtho B (c • x) (y + (-(B x) y / (B x) x) • x)

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]

Result:
no goals

Proof state:
case zero
K : Type v
inst✝³ : Field K
hK : Invertible 2
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 = 0
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
exact ⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩

Result:
no goals

Proof state:
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'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
⊢ IsOrthoᵢ B ⇑b

Tactic:
rw [Basis.coe_mkFinCons]

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'
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
⊢ IsOrthoᵢ B (Fin.cons x (Subtype.val ∘ ⇑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
hd : finrank K V = d + 1
this : Nontrivial V
hB₁ : B ≠ 0
x : V
hx : ¬IsOrtho B x x
⊢ ∃ v, IsOrthoᵢ B ⇑v

Tactic:
rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
  finrank_span_singleton (ne_zero_of_map hx)] at hd

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
⊢ ∃ v, IsOrthoᵢ B ⇑v