-- 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:
ι : 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 • P.root ↑i = ∑ j : ↑b.support, f' j • P.root ↑j
i : ↑b.support
⊢ ∑ i : ↑b.support, (Int.ofNat ∘ c) i • P.root ↑i = ∑ i : ↑b.support, f' i • P.root ↑i

Tactic:
simpa

Result:
no goals

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 • P.root ↑i = ∑ j : ↑b.support, f' j • P.root ↑j
⊢ 0 ≤ f

Tactic:
replace hc (i : b.support) : c i = f' i := Fintype.linearIndependent_iffₛ.mp
  (b.linInd_root.restrict_scalars' ℤ) (Int.ofNat ∘ c) f' (by simpa) 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
⊢ 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₀ : 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)
⊢ Function.support (-f) ⊆ b.support

Tactic:
simpa only [support_neg']

Result:
no goals

Proof state:
case neg
ι : 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 ∉ Function.support f
⊢ 0 i ≤ f i

Tactic:
aesop

Result:
no goals

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
i : ι
⊢ 0 i ≤ f i

Tactic:
by_cases hi : i ∈ b.support

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 i ≤ f i

case neg
ι : 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

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
⊢ 0 ≤ f

Tactic:
let f' : b.support → ℤ := fun i ↦ f i

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
⊢ 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
this :
  ∀ (f : ι → ℤ),
    ∑ j : ι, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' b.support) → Function.support f ⊆ b.support → 0 ≤ f
⊢ 0 ≤ f ∨ f ≤ 0

Tactic:
obtain ⟨k, hk⟩ := hf

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₀ : 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
⊢ 0 ≤ f ∨ f ≤ 0