-- 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
⊢ ∑ k : ι, f k • P.root k = P.root i - P.root j

Tactic:
rw [← Fintype.sum_subset (s := {i, j}) (by aesop), Finset.sum_insert (by aesop),
  Finset.sum_singleton]

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

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_1 : ι), f i_1 • P.root i_1 ≠ 0 → i_1 ∈ {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
⊢ P.root i - P.root j ∉ range ⇑P.root

Tactic:
have _i : Fintype ι := Fintype.ofFinite ι

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 ι
⊢ 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 ι
⊢ P.root i - P.root j ∉ range ⇑P.root

Tactic:
let f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0

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
⊢ 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
⊢ Function.support f ⊆ b.support

Tactic:
aesop

Result:
no goals