-- Mathlib/LinearAlgebra/RootSystem/Base.lean
lemma sub_nmem_range_root [CharZero R] [Finite ι]
    {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) :
    P.root i - P.root j ∉ range P.root

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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
⊢ ∑ j : ι, f j • P.root j ∈ range ⇑P.root

Tactic:
rwa [hf]

Result:
no goals

Proof state:
case inr.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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
pos : 0 ≤ f
⊢ False

Tactic:
simpa [hij, f] using pos j

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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
⊢ P.root i - P.root j ∉ range ⇑P.root

Tactic:
rcases eq_or_ne j i with rfl | hij

Result:
case 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✝ : Finite ι
j : ι
hj hi : j ∈ b.support
⊢ P.root j - P.root j ∉ range ⇑P.root

case 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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
⊢ P.root i - P.root j ∉ range ⇑P.root

Proof state:
case inr.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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
neg : f ≤ 0
⊢ False

Tactic:
simpa [hij, f] using neg i

Result:
no goals

Proof state:
case 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✝ : Finite ι
j : ι
hj hi : j ∈ b.support
⊢ P.root j - P.root j ∉ range ⇑P.root

Tactic:
simpa only [sub_self, mem_range, not_exists] using fun k ↦ P.ne_zero k

Result:
no goals

Proof state:
case 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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
⊢ P.root i - P.root j ∉ range ⇑P.root

Tactic:
intro contra

Result:
case 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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
⊢ False

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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
⊢ f i • P.root i + f j • P.root j = P.root i - P.root j

Tactic:
simp [f, hij, sub_eq_add_neg]

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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
⊢ i ∉ {j}

Tactic:
aesop

Result:
no goals

Proof state:
case 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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
⊢ P.root i - P.root j ∉ range ⇑P.root

Tactic:
have hf : ∑ k, f k • P.root k = P.root i - P.root j := by
  rw [← Fintype.sum_subset (s := {i, j}) (by aesop), Finset.sum_insert (by aesop),
    Finset.sum_singleton]
  simp [f, hij, sub_eq_add_neg]

Result:
case 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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
⊢ P.root i - P.root j ∉ range ⇑P.root

Proof state:
case 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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
⊢ False

Tactic:
rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg

Result:
case inr.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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
pos : 0 ≤ f
⊢ False

case inr.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✝ : Finite ι
i j : ι
hi : i ∈ b.support
hj : j ∈ b.support
hij : j ≠ i
_i : Fintype ι
f : ι → ℤ := fun k => if k = i then 1 else if k = j then -1 else 0
hf : ∑ k : ι, f k • P.root k = P.root i - P.root j
contra : P.root i - P.root j ∈ range ⇑P.root
neg : f ≤ 0
⊢ False