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

Tactic:
obtain rfl | hB₁ := eq_or_ne B 0

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

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

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 (Fin.cons x (Subtype.val ∘ ⇑v'))

Tactic:
intro j i

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' ⋯ ⋯
j i : Fin (d + 1)
⊢ j ≠ i → Function.onFun (IsOrtho B) (Fin.cons x (Subtype.val ∘ ⇑v')) j i

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'
c : K
y : V
hy : c • x ∈ (Submodule.span K {x}).orthogonalBilin B
hc : -(c • x) = y
this✝ : ∀ x_1 ∈ Submodule.span K {x}, x_1 ∈ (Submodule.span K {x}).orthogonalBilin B → 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 _

Result:
no goals

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'
⊢ ∀ (c : K), ∀ x_1 ∈ (Submodule.span K {x}).orthogonalBilin B, c • x + x_1 = 0 → c = 0

Tactic:
rintro c y hy hc

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'
c : K
y : V
hy : y ∈ (Submodule.span K {x}).orthogonalBilin B
hc : c • x + y = 0
⊢ c = 0

Proof state:
case succ.inr.intro.intro.refine_2.refine_2
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' ⋯ ⋯
j✝ i✝ : Fin (d + 1)
i j : Fin d
hij : j.succ ≠ i.succ
⊢ IsOrtho B ↑(v' j) ↑(v' i)

Tactic:
exact hv₁ (ne_of_apply_ne _ hij)

Result:
no goals