-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
lemma isCompl_rootSpan_ker_rootForm :
    IsCompl P.rootSpan (LinearMap.ker P.RootForm)

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
_iM : IsReflexive R M
_iN : IsReflexive R N
aux : finrank R M = finrank R ↥P.rootSpan + finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R M ≤ finrank R ↥P.rootSpan + finrank R ↥(LinearMap.ker P.RootForm)

Tactic:
rw [aux, add_le_add_iff_left]

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
_iM : IsReflexive R M
_iN : IsReflexive R N
aux : finrank R M = finrank R ↥P.rootSpan + finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R ↥P.corootSpan.dualAnnihilator ≤ finrank R ↥(LinearMap.ker P.RootForm)

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
_iM : IsReflexive R M
_iN : IsReflexive R N
⊢ IsCompl P.rootSpan (LinearMap.ker P.RootForm)

Tactic:
refine (Submodule.isCompl_iff_disjoint _ _ ?_).mpr P.disjoint_rootSpan_ker_rootForm

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
_iM : IsReflexive R M
_iN : IsReflexive R N
⊢ finrank R M ≤ finrank R ↥P.rootSpan + finrank R ↥(LinearMap.ker P.RootForm)

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
_iM : IsReflexive R M
_iN : IsReflexive R N
aux : finrank R M = finrank R ↥P.rootSpan + finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R ↥P.corootSpan.dualAnnihilator ≤ finrank R ↥(LinearMap.ker P.RootForm)

Tactic:
convert Submodule.finrank_mono P.corootSpan_dualAnnihilator_le_ker_rootForm

Result:
case h.e'_3
ι : 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
_iM : IsReflexive R M
_iN : IsReflexive R N
aux : finrank R M = finrank R ↥P.rootSpan + finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R ↥P.corootSpan.dualAnnihilator = finrank R ↥(Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator)

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
⊢ IsCompl P.rootSpan (LinearMap.ker P.RootForm)

Tactic:
have _iM : IsReflexive R M := PerfectPairing.reflexive_left P.toPerfectPairing

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
_iM : IsReflexive R M
⊢ IsCompl P.rootSpan (LinearMap.ker P.RootForm)

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
_iM : IsReflexive R M
⊢ IsCompl P.rootSpan (LinearMap.ker P.RootForm)

Tactic:
have _iN : IsReflexive R N := PerfectPairing.reflexive_right P.toPerfectPairing

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
_iM : IsReflexive R M
_iN : IsReflexive R N
⊢ IsCompl P.rootSpan (LinearMap.ker P.RootForm)

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
_iM : IsReflexive R M
_iN : IsReflexive R N
⊢ finrank R M ≤ finrank R ↥P.rootSpan + finrank R ↥(LinearMap.ker P.RootForm)

Tactic:
have aux : finrank R M = finrank R P.rootSpan + finrank R P.corootSpan.dualAnnihilator := by
  rw [P.toPerfectPairing.finrank_eq, ← P.finrank_corootSpan_eq,
    Subspace.finrank_add_finrank_dualAnnihilator_eq P.corootSpan]

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
_iM : IsReflexive R M
_iN : IsReflexive R N
aux : finrank R M = finrank R ↥P.rootSpan + finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R M ≤ finrank R ↥P.rootSpan + finrank R ↥(LinearMap.ker P.RootForm)

Proof state:
case h.e'_3
ι : 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
_iM : IsReflexive R M
_iN : IsReflexive R N
aux : finrank R M = finrank R ↥P.rootSpan + finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R ↥P.corootSpan.dualAnnihilator = finrank R ↥(Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator)

Tactic:
exact (LinearEquiv.finrank_map_eq _ _).symm

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
_iM : IsReflexive R M
_iN : IsReflexive R N
⊢ finrank R M = finrank R ↥P.rootSpan + finrank R ↥P.corootSpan.dualAnnihilator

Tactic:
rw [P.toPerfectPairing.finrank_eq, ← P.finrank_corootSpan_eq,
  Subspace.finrank_add_finrank_dualAnnihilator_eq P.corootSpan]

Result:
no goals