-- Mathlib/LinearAlgebra/RootSystem/Base.lean
lemma root_mem_span_int (i : ι) :
    P.root i ∈ span ℤ (P.root '' 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
i : ι
this : P.root i ∈ span ℕ (⇑P.root '' b.support) ∨ -P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ (⇑P.root '' b.support)

Tactic:
rw [← span_span_of_tower (R := ℕ)]

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
i : ι
this : P.root i ∈ span ℕ (⇑P.root '' b.support) ∨ -P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' b.support))

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
i : ι
hi : P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' b.support))

Tactic:
exact subset_span hi

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
i : ι
hi : -P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' b.support))

Tactic:
rw [← neg_mem_iff]

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
i : ι
hi : -P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ -P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' 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
i : ι
this : P.root i ∈ span ℕ (⇑P.root '' b.support) ∨ -P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' b.support))

Tactic:
rcases this with hi | hi

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
i : ι
hi : P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' b.support))

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
i : ι
hi : -P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' 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
i : ι
this : P.root i ∈ AddSubmonoid.closure (⇑P.root '' b.support) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ (⇑P.root '' b.support)

Tactic:
simp only [← span_nat_eq_addSubmonoid_closure, mem_toAddSubmonoid] at this

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
i : ι
this : P.root i ∈ span ℕ (⇑P.root '' b.support) ∨ -P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ (⇑P.root '' b.support)

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
i : ι
hi : -P.root i ∈ span ℕ (⇑P.root '' b.support)
⊢ -P.root i ∈ span ℤ ↑(span ℕ (⇑P.root '' b.support))

Tactic:
exact subset_span 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
i : ι
⊢ P.root i ∈ span ℤ (⇑P.root '' b.support)

Tactic:
have := b.root_mem_or_neg_mem 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
i : ι
this : P.root i ∈ AddSubmonoid.closure (⇑P.root '' b.support) ∨ -P.root i ∈ AddSubmonoid.closure (⇑P.root '' b.support)
⊢ P.root i ∈ span ℤ (⇑P.root '' b.support)