-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
theorem range_polarization_domRestrict_le_span_coroot :
    LinearMap.range (P.Polarization.domRestrict P.rootSpan) ≤ P.corootSpan

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
⊢ LinearMap.range (P.Polarization.domRestrict P.rootSpan) ≤ P.corootSpan

Tactic:
intro y hy

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
hy : y ∈ LinearMap.range (P.Polarization.domRestrict P.rootSpan)
⊢ y ∈ P.corootSpan

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
x : ↥P.rootSpan
hx : (P.Polarization.domRestrict P.rootSpan) x = y
⊢ y ∈ P.corootSpan

Tactic:
rw [← hx, LinearMap.domRestrict_apply, Polarization_apply]

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
x : ↥P.rootSpan
hx : (P.Polarization.domRestrict P.rootSpan) x = y
⊢ ∑ i : ι, (P.coroot' i) ↑x • P.coroot i ∈ P.corootSpan

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
x : ↥P.rootSpan
hx : (P.Polarization.domRestrict P.rootSpan) x = y
⊢ ∑ i : ι, (fun i => (P.toPerfectPairing ↑x) (P.coroot i)) i • P.coroot i = ∑ i : ι, (P.coroot' i) ↑x • P.coroot i

Tactic:
simp

Result:
no goals

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
x : ↥P.rootSpan
hx : (P.Polarization.domRestrict P.rootSpan) x = y
⊢ ∑ i : ι, (P.coroot' i) ↑x • P.coroot i ∈ P.corootSpan

Tactic:
refine (mem_span_range_iff_exists_fun R).mpr ?_

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
x : ↥P.rootSpan
hx : (P.Polarization.domRestrict P.rootSpan) x = y
⊢ ∃ c, ∑ i : ι, c i • P.coroot i = ∑ i : ι, (P.coroot' i) ↑x • P.coroot i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
hy : y ∈ LinearMap.range (P.Polarization.domRestrict P.rootSpan)
⊢ y ∈ P.corootSpan

Tactic:
obtain ⟨x, hx⟩ := hy

Result:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
x : ↥P.rootSpan
hx : (P.Polarization.domRestrict P.rootSpan) x = y
⊢ y ∈ P.corootSpan

Proof state:
case intro
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
x : ↥P.rootSpan
hx : (P.Polarization.domRestrict P.rootSpan) x = y
⊢ ∃ c, ∑ i : ι, c i • P.coroot i = ∑ i : ι, (P.coroot' i) ↑x • P.coroot i

Tactic:
use fun i => (P.toPerfectPairing x) (P.coroot i)

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
y : N
x : ↥P.rootSpan
hx : (P.Polarization.domRestrict P.rootSpan) x = y
⊢ ∑ i : ι, (fun i => (P.toPerfectPairing ↑x) (P.coroot i)) i • P.coroot i = ∑ i : ι, (P.coroot' i) ↑x • P.coroot i