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

Tactic:
simpa using this (-f) (by convert hk'; simp) (by simpa only [support_neg'])

Result:
no goals

Proof state:
case h.e'_5
ι : 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)
⊢ ∑ j : ι, (-f) j • P.root j = -∑ j : ι, f 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 : 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
⊢ i ∈ b.support

Tactic:
exact hf₀ hi

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

Tactic:
obtain ⟨c, hc⟩ := 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 : ∑ 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

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) = f' i
i : ι
hi : i ∉ b.support
⊢ i ∉ Function.support f

Tactic:
contrapose! hi

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
c : ↑b.support → ℕ
hc : ∀ (i : ↑b.support), ↑(c i) = f' i
i : ι
hi : i ∈ Function.support f
⊢ i ∈ b.support

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

Tactic:
have _i : Fintype b.support := Fintype.ofFinite b.support

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

Tactic:
replace hf : ∑ j, f' j • P.root j ∈ AddSubmonoid.closure (P.root '' b.support) := by
  suffices ∑ j, f' j • P.root j = ∑ j, f j • P.root j by rwa [this]
  rw [← Fintype.sum_subset (s := b.support.toFinset) (by aesop), ← Finset.sum_set_coe]

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 : ∑ j : ↑b.support, f' j • P.root ↑j ∈ AddSubmonoid.closure (⇑P.root '' b.support)
⊢ 0 ≤ f

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

Tactic:
right

Result:
case intro.inr.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)
⊢ f ≤ 0