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

Tactic:
replace hi : i ∉ f.support := by contrapose! hi; exact hf₀ hi

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

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

Tactic:
rcases b.root_mem_or_neg_mem k with hk' | hk' <;> rw [hk] at hk'

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

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

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

Tactic:
intro f hf 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 : ∑ j : ι, f j • P.root j ∈ AddSubmonoid.closure (⇑P.root '' b.support)
hf₀ : Function.support f ⊆ 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
⊢ ∀ (i : ι), f i • P.root i ≠ 0 → i ∈ b.support.toFinset

Tactic:
aesop

Result:
no goals

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

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

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

Tactic:
convert hk'

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

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

Tactic:
rwa [this]

Result:
no goals