-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
@[simp]
lemma orthogonal_rootSpan_eq :
    P.RootForm.orthogonal P.rootSpan = LinearMap.ker P.RootForm

Proof state:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
u : M
hu : u ∈ P.rootSpan
v : M
hv : P.RootForm v = 0
⊢ (P.RootForm (u + v)) x = 0

Tactic:
simp [hx _ hu, hv]

Result:
no goals

Proof state:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
u : M
hu : u ∈ P.rootSpan
v : M
hv : v ∈ LinearMap.ker P.RootForm
⊢ (P.RootForm (u + v)) x = 0

Tactic:
simp only [LinearMap.mem_ker] at hv

Result:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
u : M
hu : u ∈ P.rootSpan
v : M
hv : P.RootForm v = 0
⊢ (P.RootForm (u + v)) x = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x y : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
⊢ ∃ u ∈ P.rootSpan, ∃ v ∈ LinearMap.ker P.RootForm, u + v = y

Tactic:
rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x y : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
⊢ y ∈ ⊤

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x y : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
⊢ (P.RootForm y) x = 0

Tactic:
obtain ⟨u, hu, v, hv, rfl⟩ : ∃ᵉ (u ∈ P.rootSpan) (v ∈ LinearMap.ker P.RootForm), u + v = y := by
  rw [← Submodule.mem_sup, P.isCompl_rootSpan_ker_rootForm.sup_eq_top]; exact Submodule.mem_top

Result:
case intro.intro.intro.intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
u : M
hu : u ∈ P.rootSpan
v : M
hv : v ∈ LinearMap.ker P.RootForm
⊢ (P.RootForm (u + v)) x = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x : M
hx : x ∈ P.RootForm.orthogonal P.rootSpan
y : M
⊢ P.RootForm.IsOrtho y x

Tactic:
simp only [LinearMap.BilinForm.mem_orthogonal_iff, LinearMap.BilinForm.IsOrtho] at hx ⊢

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x y : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
⊢ (P.RootForm y) x = 0

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ P.RootForm.orthogonal P.rootSpan ≤ P.RootForm.orthogonal ⊤

Tactic:
rintro x hx y -

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x : M
hx : x ∈ P.RootForm.orthogonal P.rootSpan
y : M
⊢ P.RootForm.IsOrtho y x

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x✝ : M
⊢ x✝ ∈ P.RootForm.orthogonal ⊤ → x✝ ∈ P.RootForm.orthogonal P.rootSpan

Tactic:
aesop

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ P.RootForm.orthogonal P.rootSpan = LinearMap.ker P.RootForm

Tactic:
rw [← LinearMap.BilinForm.orthogonal_top_eq_ker P.rootForm_symmetric.isRefl]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ P.RootForm.orthogonal P.rootSpan = P.RootForm.orthogonal ⊤

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ P.RootForm.orthogonal P.rootSpan = P.RootForm.orthogonal ⊤

Tactic:
refine le_antisymm ?_ (by intro; aesop)

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ P.RootForm.orthogonal P.rootSpan ≤ P.RootForm.orthogonal ⊤

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ P.RootForm.orthogonal ⊤ ≤ P.RootForm.orthogonal P.rootSpan

Tactic:
intro

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x✝ : M
⊢ x✝ ∈ P.RootForm.orthogonal ⊤ → x✝ ∈ P.RootForm.orthogonal P.rootSpan

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Field R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
x y : M
hx : ∀ n ∈ P.rootSpan, (P.RootForm n) x = 0
⊢ y ∈ ⊤

Tactic:
exact Submodule.mem_top

Result:
no goals