-- Mathlib/LinearAlgebra/RootSystem/Base.lean
lemma exists_root_eq_sum_int (i : ι) :
    ∃ f : ι → ℤ, (0 ≤ f ∨ f ≤ 0) ∧ P.root i = ∑ j, f j • P.root j

Proof state:
case intro.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 : ι
f : ι → ℕ
hf : P.root i = -∑ j : ι, f j • P.root j
⊢ ∃ f, (0 ≤ f ∨ f ≤ 0) ∧ P.root i = ∑ j : ι, f j • P.root j

Tactic:
exact ⟨- Nat.cast ∘ f, Or.inr fun _ ↦ by simp, by simp [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 : ι
f : ι → ℕ
hf : P.root i = ∑ j : ι, f j • P.root j
x✝ : ι
⊢ 0 x✝ ≤ (Nat.cast ∘ f) x✝

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 : ι
f : ι → ℕ
hf : P.root i = ∑ j : ι, f j • P.root j
⊢ P.root i = ∑ j : ι, (Nat.cast ∘ f) j • P.root j

Tactic:
simp [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 : ι
⊢ ∃ f, (0 ≤ f ∨ f ≤ 0) ∧ P.root i = ∑ j : ι, f j • P.root j

Tactic:
obtain ⟨f, hf | hf⟩ := b.exists_root_eq_sum_nat_or_neg i

Result:
case intro.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 : ι
f : ι → ℕ
hf : P.root i = ∑ j : ι, f j • P.root j
⊢ ∃ f, (0 ≤ f ∨ f ≤ 0) ∧ P.root i = ∑ j : ι, f j • P.root j

case intro.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 : ι
f : ι → ℕ
hf : P.root i = -∑ j : ι, f j • P.root j
⊢ ∃ f, (0 ≤ f ∨ f ≤ 0) ∧ P.root i = ∑ j : ι, f j • P.root j

Proof state:
case intro.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 : ι
f : ι → ℕ
hf : P.root i = ∑ j : ι, f j • P.root j
⊢ ∃ f, (0 ≤ f ∨ f ≤ 0) ∧ P.root i = ∑ j : ι, f j • P.root j

Tactic:
exact ⟨  Nat.cast ∘ f, Or.inl fun _ ↦ by simp, by simp [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 : ι
f : ι → ℕ
hf : P.root i = -∑ j : ι, f j • P.root j
x✝ : ι
⊢ (-Nat.cast ∘ f) x✝ ≤ 0 x✝

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 : ι
f : ι → ℕ
hf : P.root i = -∑ j : ι, f j • P.root j
⊢ P.root i = ∑ j : ι, (-Nat.cast ∘ f) j • P.root j

Tactic:
simp [hf]

Result:
no goals