-- Mathlib/LinearAlgebra/RootSystem/Base.lean
lemma exists_root_eq_sum_nat_or_neg (i : ι) :
    ∃ f : ι → ℕ, P.root i = ∑ j, f j • P.root j ∨ P.root i = - ∑ j, f j • P.root j

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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
⊢ ∀ m ∈ AddSubmonoid.closure (⇑P.root '' b.support), ∃ f, m = ∑ j : ι, f j • P.root j

Tactic:
intro m hm

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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' b.support)
⊢ ∃ f, m = ∑ j : ι, f j • P.root j

Proof state:
case inl.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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
this : ∀ m ∈ AddSubmonoid.closure (⇑P.root '' b.support), ∃ f, m = ∑ j : ι, f j • P.root j
hi : P.root i ∈ AddSubmonoid.closure (⇑P.root '' b.support)
f : ι → ℕ
hf : P.root i = ∑ j : ι, f j • P.root j
⊢ ∃ f, P.root i = ∑ j : ι, f j • P.root j ∨ -P.root i = ∑ j : ι, f j • P.root j

Tactic:
exact ⟨f, Or.inl hf⟩

Result:
no goals

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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' b.support)
⊢ 0 = ∑ j : ι, 0 j • P.root j

Tactic:
simp

Result:
no goals

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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' b.support)
j : ι
hj : j ∈ b.support
⊢ P.root j = ∑ j_1 : ι, Pi.single j 1 j_1 • P.root j_1

Tactic:
simp [Pi.single_apply]

Result:
no goals

Proof state:
case refine_1
ι : 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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' b.support)
⊢ ∀ x ∈ ⇑P.root '' b.support, ∃ f, x = ∑ j : ι, f j • P.root j

Tactic:
rintro - ⟨j, hj, rfl⟩

Result:
case refine_1.intro.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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' b.support)
j : ι
hj : j ∈ b.support
⊢ ∃ f, P.root j = ∑ j : ι, f j • P.root j

Proof state:
case inr.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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
this : ∀ m ∈ AddSubmonoid.closure (⇑P.root '' b.support), ∃ f, m = ∑ j : ι, f j • P.root j
hi : -P.root i ∈ AddSubmonoid.closure (⇑P.root '' b.support)
f : ι → ℕ
hf : -P.root i = ∑ j : ι, f j • P.root j
⊢ ∃ f, P.root i = ∑ j : ι, f j • P.root j ∨ -P.root i = ∑ j : ι, f j • P.root j

Tactic:
exact ⟨f, Or.inr hf⟩

Result:
no goals

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 : RootSystem ι R M N
b : P.Base
inst✝ : Fintype ι
i : ι
m : M
hm : m ∈ AddSubmonoid.closure (⇑P.root '' b.support)
x✝ y✝ : M
hx✝ : x✝ ∈ AddSubmonoid.closure (⇑P.root '' b.support)
hy✝ : y✝ ∈ AddSubmonoid.closure (⇑P.root '' b.support)
f : ι → ℕ
hf : x✝ = ∑ j : ι, f j • P.root j
g : ι → ℕ
hg : y✝ = ∑ j : ι, g j • P.root j
⊢ x✝ + y✝ = ∑ j : ι, (f + g) j • P.root j

Tactic:
simp [hf, hg, add_smul, Finset.sum_add_distrib]

Result:
no goals