-- Mathlib/LinearAlgebra/RootSystem/Base.lean
lemma eq_one_or_neg_one_of_mem_support_of_smul_mem [Finite ι] [CharZero R]
    [NoZeroSMulDivisors ℤ M] [NoZeroSMulDivisors ℤ N]
    (i : ι) (h : i ∈ b.support) (t : R) (ht : t • P.root i ∈ range P.root) :
    t = 1 ∨ t = - 1

Proof state:
case 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t s : R
hs : s * t = 1
ht : s • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * s = 1
hz : ↑1 * t = 1
this : ↑1 * ↑w = 1
⊢ t = 1

Tactic:
simpa using hz

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
s : R
hs : s * t = 1
ht : s • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * s = 1
this✝ : ↑z * ↑w = 1
this : z = 1 ∨ z = -1
⊢ t = 1 ∨ t = -1

Tactic:
rcases this with rfl | rfl

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t s : R
hs : s * t = 1
ht : s • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * s = 1
hz : ↑1 * t = 1
this : ↑1 * ↑w = 1
⊢ t = 1 ∨ t = -1

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t s : R
hs : s * t = 1
ht : s • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * s = 1
hz : ↑(-1) * t = 1
this : ↑(-1) * ↑w = 1
⊢ t = 1 ∨ t = -1

Proof state:
case intro.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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
s : R
hs : s * t = 1
ht : s • P.coroot i ∈ range ⇑P.coroot
⊢ t = 1 ∨ t = -1

Tactic:
obtain ⟨w, hw⟩ := b.flip.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h s ht

Result:
case intro.intro.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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
s : R
hs : s * t = 1
ht : s • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * s = 1
⊢ t = 1 ∨ t = -1

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
z : ℤ
hz : ↑z * t = 1
s : R
hs : s * t = 1
j : ι
hj : P.root j = t • P.root i
⊢ s • P.coroot i ∈ range ⇑P.coroot

Tactic:
simpa only [coroot_eq_smul_coroot_iff.mpr hj, smul_smul, hs, one_smul] using mem_range_self j

Result:
no goals

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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
ht : t • P.root i ∈ range ⇑P.root
z : ℤ
hz : ↑z * t = 1
⊢ t = 1 ∨ t = -1

Tactic:
obtain ⟨s, hs⟩ := IsUnit.exists_left_inv <| isUnit_of_mul_eq_one_right _ t hz

Result:
case intro.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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t : R
ht : t • P.root i ∈ range ⇑P.root
z : ℤ
hz : ↑z * t = 1
s : R
hs : s * t = 1
⊢ t = 1 ∨ t = -1

Proof state:
case 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✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : NoZeroSMulDivisors ℤ M
inst✝ : NoZeroSMulDivisors ℤ N
i : ι
h : i ∈ b.support
t s : R
hs : s * t = 1
ht : s • P.coroot i ∈ range ⇑P.coroot
w : ℤ
hw : ↑w * s = 1
hz : ↑(-1) * t = 1
this : ↑(-1) * ↑w = 1
⊢ t = -1

Tactic:
simpa [neg_eq_iff_eq_neg] using hz

Result:
no goals