-- Mathlib/LinearAlgebra/RootSystem/Base.lean
lemma pos_or_neg_of_sum_smul_root_mem [CharZero R] [Fintype ι] (f : ι → ℤ)
    (hf : ∑ j, f j • P.root j ∈ range P.root) (hf₀ : f.support ⊆ b.support) :
    0 ≤ f ∨ f ≤ 0

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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
c : ↑b.support → ℕ
hc : ∀ (i : ↑b.support), ↑(c i) = f' i
⊢ 0 ≤ f

Tactic:
intro i

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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
c : ↑b.support → ℕ
hc : ∀ (i : ↑b.support), ↑(c i) = f' i
i : ι
⊢ 0 i ≤ f i

Proof state:
case pos
ι : 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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
c : ↑b.support → ℕ
hc : ∀ (i : ↑b.support), ↑(c i) = f' i
i : ι
hi : i ∈ b.support
⊢ 0 i ≤ f i

Tactic:
change 0 ≤ f' ⟨i, hi⟩

Result:
case pos
ι : 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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
c : ↑b.support → ℕ
hc : ∀ (i : ↑b.support), ↑(c i) = f' i
i : ι
hi : i ∈ b.support
⊢ 0 ≤ f' ⟨i, hi⟩

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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf✝ : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
hf : ∑ j : ↑b.support, f' j • P.root ↑j ∈ AddSubmonoid.closure (⇑P.root '' b.support)
⊢ 0 ≤ f

Tactic:
rw [← span_nat_eq_addSubmonoid_closure, mem_toAddSubmonoid,
  Fintype.mem_span_image_iff_exists_fun] at hf

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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf✝ : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
hf : ∃ c, ∑ i : ↑b.support, c i • P.root ↑i = ∑ j : ↑b.support, f' j • P.root ↑j
⊢ 0 ≤ f

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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf✝ : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf : ∑ j : ι, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' b.support)
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
⊢ ∑ j : ↑b.support, f' j • P.root ↑j = ∑ j : ι, f j • P.root j

Tactic:
rw [← Fintype.sum_subset (s := b.support.toFinset) (by aesop), ← Finset.sum_set_coe]

Result:
no goals

Proof state:
case intro.inl.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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f : ι → ℤ
hf₀ : Function.support f ⊆ b.support
this :
  ∀ (f : ι → ℤ),
    ∑ j : ι, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' b.support) → Function.support f ⊆ b.support → 0 ≤ f
k : ι
hk : P.root k = ∑ j : ι, f j • P.root j
hk' : ∑ j : ι, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' b.support)
⊢ 0 ≤ f

Tactic:
exact this f hk' 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 : RootPairing ι R M N
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf✝ : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf : ∑ j : ι, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' b.support)
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
⊢ ∑ j : ↑b.support, f' j • P.root ↑j ∈ AddSubmonoid.closure (⇑P.root '' b.support)

Tactic:
suffices ∑ j, f' j • P.root j = ∑ j, f j • P.root j by rwa [this]

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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf✝ : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf : ∑ j : ι, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' b.support)
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
⊢ ∑ j : ↑b.support, f' j • P.root ↑j = ∑ j : ι, f j • P.root j

Proof state:
case pos
ι : 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
b : P.Base
inst✝¹ : CharZero R
inst✝ : Fintype ι
f✝ : ι → ℤ
hf : ∑ j : ι, f✝ j • P.root j ∈ range ⇑P.root
hf₀✝ : Function.support f✝ ⊆ b.support
f : ι → ℤ
hf₀ : Function.support f ⊆ b.support
_i : Fintype ↑b.support
f' : ↑b.support → ℤ := fun i => f ↑i
c : ↑b.support → ℕ
hc : ∀ (i : ↑b.support), ↑(c i) = f' i
i : ι
hi : i ∈ b.support
⊢ 0 ≤ f' ⟨i, hi⟩

Tactic:
simp [← hc]

Result:
no goals