-- Mathlib/LinearAlgebra/RootSystem/Finite/Nondegenerate.lean
@[simp]
lemma finrank_rootSpan_map_polarization_eq_finrank_corootSpan :
    finrank R (P.rootSpan.map P.Polarization) = finrank R P.corootSpan

Proof state:
case 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan
c : ι → R
hc : ∑ i : ι, c i • P.coroot i = x✝
⊢ (∏ i : ι, (P.RootForm (P.root i)) (P.root i)) • x✝ ∈ LinearMap.range (P.Polarization.domRestrict P.rootSpan)

Tactic:
rw [← hc, Finset.smul_sum]

Result:
case 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan
c : ι → R
hc : ∑ i : ι, c i • P.coroot i = x✝
⊢ ∑ x : ι, (∏ i : ι, (P.RootForm (P.root i)) (P.root i)) • c x • P.coroot x ∈
    LinearMap.range (P.Polarization.domRestrict P.rootSpan)

Proof state:
case 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan
c : ι → R
hc : ∑ i : ι, c i • P.coroot i = x✝
⊢ ∑ x : ι, (∏ i : ι, (P.RootForm (P.root i)) (P.root i)) • c x • P.coroot x ∈
    LinearMap.range (P.Polarization.domRestrict P.rootSpan)

Tactic:
simp_rw [smul_smul, mul_comm, ← smul_smul]

Result:
case 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan
c : ι → R
hc : ∑ i : ι, c i • P.coroot i = x✝
⊢ ∑ x : ι, c x • (∏ i : ι, (P.RootForm (P.root i)) (P.root i)) • P.coroot x ∈
    LinearMap.range (P.Polarization.domRestrict 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ finrank R ↥P.corootSpan ≤ finrank R ↥(LinearMap.range (P.Polarization.domRestrict P.rootSpan))

Tactic:
have : 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
⊢ finrank R ↥P.corootSpan ≤ finrank R ↥(LinearMap.range (P.Polarization.domRestrict 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ finrank R ↥(Submodule.map P.Polarization P.rootSpan) = finrank R ↥P.corootSpan

Tactic:
rw [← LinearMap.range_domRestrict]

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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ finrank R ↥(LinearMap.range (P.Polarization.domRestrict P.rootSpan)) = finrank R ↥P.corootSpan

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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
⊢ finrank R ↥P.corootSpan ≤ finrank R ↥(LinearMap.range (P.Polarization.domRestrict P.rootSpan))

Tactic:
have h_ne : ∏ i, P.RootForm (P.root i) (P.root i) ≠ 0 :=
  Finset.prod_ne_zero_iff.mpr fun i _ ↦ IsAnisotropic.rootForm_root_ne_zero i

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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
⊢ finrank R ↥P.corootSpan ≤ finrank R ↥(LinearMap.range (P.Polarization.domRestrict 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan
⊢ (∏ i : ι, (P.RootForm (P.root i)) (P.root i)) • x✝ ∈ LinearMap.range (P.Polarization.domRestrict P.rootSpan)

Tactic:
obtain ⟨c, hc⟩ := (mem_span_range_iff_exists_fun R).mp hx

Result:
case 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan
c : ι → R
hc : ∑ i : ι, c i • P.coroot i = x✝
⊢ (∏ i : ι, (P.RootForm (P.root i)) (P.root i)) • x✝ ∈ LinearMap.range (P.Polarization.domRestrict 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ finrank R ↥(LinearMap.range (P.Polarization.domRestrict P.rootSpan)) = finrank R ↥P.corootSpan

Tactic:
apply (Submodule.finrank_mono P.range_polarization_domRestrict_le_span_coroot).antisymm

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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
⊢ finrank R ↥P.corootSpan ≤ finrank R ↥(LinearMap.range (P.Polarization.domRestrict P.rootSpan))

Proof state:
case 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✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Module R M
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : P.IsAnisotropic
this : IsReflexive R N
h_ne : ∏ i : ι, (P.RootForm (P.root i)) (P.root i) ≠ 0
x✝ : N
hx : x✝ ∈ P.corootSpan
c : ι → R
hc : ∑ i : ι, c i • P.coroot i = x✝
⊢ ∑ x : ι, c x • (∏ i : ι, (P.RootForm (P.root i)) (P.root i)) • P.coroot x ∈
    LinearMap.range (P.Polarization.domRestrict P.rootSpan)

Tactic:
exact Submodule.sum_smul_mem (LinearMap.range (P.Polarization.domRestrict P.rootSpan)) c
  (fun c _ ↦ prod_rootForm_smul_coroot_mem_range_domRestrict P c)

Result:
no goals