-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma coroot'_apply_apply_mem_of_mem_span [Module S M] [IsScalarTower S R M] [P.IsValuedIn S]
    {x : M} (hx : x ∈ span S (range P.root)) (i : ι) :
    P.coroot' i x ∈ range (algebraMap S R)

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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
hx : x ∈ span S (range ⇑P.root)
i : ι
⊢ (P.coroot' i) x ∈ range ⇑(algebraMap S R)

Tactic:
rw [show range (algebraMap S R) = LinearMap.range (Algebra.linearMap S R) from rfl]

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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
hx : x ∈ span S (range ⇑P.root)
i : ι
⊢ (P.coroot' i) x ∈ ↑(LinearMap.range (Algebra.linearMap S R))

Proof state:
case smul
ι : 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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x✝ : M
i : ι
t : S
x : M
hx✝ : x ∈ span S (range ⇑P.root)
hx : (P.coroot' i) x ∈ ↑(LinearMap.range (Algebra.linearMap S R))
⊢ (P.coroot' i) (t • x) ∈ ↑(LinearMap.range (Algebra.linearMap S R))

Tactic:
simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx

Result:
no goals

Proof state:
case mem
ι : 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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x✝ : M
i : ι
x : M
hx : x ∈ range ⇑P.root
⊢ (P.coroot' i) x ∈ ↑(LinearMap.range (Algebra.linearMap S R))

Tactic:
obtain ⟨k, rfl⟩ := hx

Result:
case mem.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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
i k : ι
⊢ (P.coroot' i) (P.root k) ∈ ↑(LinearMap.range (Algebra.linearMap S R))

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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
hx : x ∈ span S (range ⇑P.root)
i : ι
⊢ (P.coroot' i) x ∈ ↑(LinearMap.range (Algebra.linearMap S R))

Tactic:
induction hx using Submodule.span_induction with
| mem x hx =>
  obtain ⟨k, rfl⟩ := hx
  simpa using RootPairing.exists_value k i
| zero => simp
| add x y _ _ hx hy => simpa only [map_add] using add_mem hx hy
| smul t x _ hx => simpa only [LinearMap.map_smul_of_tower] using Submodule.smul_mem _ t hx

Result:
no goals

Proof state:
case add
ι : 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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x✝ : M
i : ι
x y : M
hx✝ : x ∈ span S (range ⇑P.root)
hy✝ : y ∈ span S (range ⇑P.root)
hx : (P.coroot' i) x ∈ ↑(LinearMap.range (Algebra.linearMap S R))
hy : (P.coroot' i) y ∈ ↑(LinearMap.range (Algebra.linearMap S R))
⊢ (P.coroot' i) (x + y) ∈ ↑(LinearMap.range (Algebra.linearMap S R))

Tactic:
simpa only [map_add] using add_mem hx hy

Result:
no goals

Proof state:
case mem.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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
i k : ι
⊢ (P.coroot' i) (P.root k) ∈ ↑(LinearMap.range (Algebra.linearMap S R))

Tactic:
simpa using RootPairing.exists_value k i

Result:
no goals

Proof state:
case zero
ι : 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
S : Type u_5
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
inst✝² : Module S M
inst✝¹ : IsScalarTower S R M
inst✝ : P.IsValuedIn S
x : M
i : ι
⊢ (P.coroot' i) 0 ∈ ↑(LinearMap.range (Algebra.linearMap S R))

Tactic:
simp

Result:
no goals