-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
lemma ker_rootForm_eq_dualAnnihilator :
    LinearMap.ker P.RootForm = P.corootSpan.dualAnnihilator.map P.toDualLeft.symm

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
⊢ LinearMap.ker P.RootForm = Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator

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

Tactic:
have aux0 := 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
aux0 : finrank R ↥P.corootSpan + finrank R ↥P.corootSpan.dualAnnihilator = finrank R N
⊢ finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥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
_iM : IsReflexive R M
_iN : IsReflexive R N
this : finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R ↥(Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator) = finrank R ↥(LinearMap.ker P.RootForm)

Tactic:
rw [this]

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
this : finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R ↥(Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator) = finrank R ↥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
_iM : IsReflexive R M
_iN : IsReflexive R N
⊢ LinearMap.ker P.RootForm = Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator

Tactic:
suffices finrank R (LinearMap.ker P.RootForm) = finrank R P.corootSpan.dualAnnihilator by
  refine (Submodule.eq_of_le_of_finrank_eq P.corootSpan_dualAnnihilator_le_ker_rootForm ?_).symm
  rw [this]
  apply LinearEquiv.finrank_map_eq

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 ↥(LinearMap.ker P.RootForm) = finrank R ↥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
_iM : IsReflexive R M
⊢ LinearMap.ker P.RootForm = Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator

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
⊢ LinearMap.ker P.RootForm = 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
_iM : IsReflexive R M
_iN : IsReflexive R N
this : finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator
⊢ LinearMap.ker P.RootForm = Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator

Tactic:
refine (Submodule.eq_of_le_of_finrank_eq P.corootSpan_dualAnnihilator_le_ker_rootForm ?_).symm

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
this : finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R ↥(Submodule.map P.toDualLeft.symm 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
aux0 : finrank R ↥P.corootSpan + finrank R ↥P.corootSpan.dualAnnihilator = finrank R N
aux1 : finrank R ↥P.rootSpan + finrank R ↥(LinearMap.ker P.RootForm) = finrank R M
⊢ finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator

Tactic:
rw [← P.finrank_corootSpan_eq, P.toPerfectPairing.finrank_eq] at aux1

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
aux0 : finrank R ↥P.corootSpan + finrank R ↥P.corootSpan.dualAnnihilator = finrank R N
aux1 : finrank R ↥P.corootSpan + finrank R ↥(LinearMap.ker P.RootForm) = finrank R N
⊢ finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥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
_iM : IsReflexive R M
_iN : IsReflexive R N
this : finrank R ↥(LinearMap.ker P.RootForm) = finrank R ↥P.corootSpan.dualAnnihilator
⊢ finrank R ↥(Submodule.map P.toDualLeft.symm P.corootSpan.dualAnnihilator) = finrank R ↥P.corootSpan.dualAnnihilator

Tactic:
apply LinearEquiv.finrank_map_eq

Result:
no goals