-- 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:
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

Tactic:
exact ⟨Pi.single j 1, by simp [Pi.single_apply]⟩

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 : ι
this : ∀ m ∈ AddSubmonoid.closure (⇑P.root '' b.support), ∃ f, m = ∑ 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:
rcases b.root_mem_or_neg_mem i with hi | hi

Result:
case inl
ι : 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, P.root i = ∑ j : ι, f j • P.root j ∨ -P.root i = ∑ j : ι, f j • P.root j

case inr
ι : 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, P.root i = ∑ j : ι, f j • P.root j ∨ -P.root i = ∑ j : ι, f j • P.root j

Proof state:
case inl
ι : 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, P.root i = ∑ j : ι, f j • P.root j ∨ -P.root i = ∑ j : ι, f j • P.root j

Tactic:
obtain ⟨f, hf⟩ := this _ hi

Result:
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

Proof state:
case refine_2
ι : 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
⊢ ∃ f, x✝ + y✝ = ∑ j : ι, f j • P.root j

Tactic:
exact ⟨f + g, by simp [hf, hg, add_smul, Finset.sum_add_distrib]⟩

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)
⊢ ∃ f, m = ∑ j : ι, f j • P.root j

Tactic:
refine AddSubmonoid.closure_induction ?_ ⟨0, by simp⟩ ?_ hm

Result:
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

case refine_2
ι : 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),
    x ∈ AddSubmonoid.closure (⇑P.root '' b.support) →
      y ∈ AddSubmonoid.closure (⇑P.root '' b.support) →
        (∃ f, x = ∑ j : ι, f j • P.root j) → (∃ f, y = ∑ j : ι, f j • P.root j) → ∃ f, x + y = ∑ j : ι, f j • P.root j

Proof state:
case inr
ι : 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, P.root i = ∑ j : ι, f j • P.root j ∨ -P.root i = ∑ j : ι, f j • P.root j

Tactic:
obtain ⟨f, hf⟩ := this _ hi

Result:
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

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 : ι
⊢ ∃ f, P.root i = ∑ j : ι, f j • P.root j ∨ P.root i = -∑ j : ι, f j • P.root j

Tactic:
simp_rw [← neg_eq_iff_eq_neg]

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 : ι
⊢ ∃ f, P.root i = ∑ j : ι, f j • P.root j ∨ -P.root i = ∑ j : ι, f j • P.root j

Proof state:
case refine_2
ι : 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),
    x ∈ AddSubmonoid.closure (⇑P.root '' b.support) →
      y ∈ AddSubmonoid.closure (⇑P.root '' b.support) →
        (∃ f, x = ∑ j : ι, f j • P.root j) → (∃ f, y = ∑ j : ι, f j • P.root j) → ∃ f, x + y = ∑ j : ι, f j • P.root j

Tactic:
intro _ _ _ _ ⟨f, hf⟩ ⟨g, hg⟩

Result:
case refine_2
ι : 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
⊢ ∃ f, x✝ + y✝ = ∑ j : ι, f j • P.root j