-- 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 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
this : ↑z * ↑w = 1
⊢ z = 1 ∨ z = -1

Tactic:
norm_cast at this

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
this : z * w = 1
⊢ z = 1 ∨ z = -1

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
ht : t • P.root i ∈ range ⇑P.root
z : ℤ
hz : ↑z * t = 1
s : R
hs : s * t = 1
⊢ s • P.coroot i ∈ range ⇑P.coroot

Tactic:
obtain ⟨j, hj⟩ := ht

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

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
ht : t • P.root i ∈ range ⇑P.root
z : ℤ
hz : ↑z * t = 1
s : R
hs : s * t = 1
⊢ t = 1 ∨ t = -1

Tactic:
replace ht : s • P.coroot i ∈ range P.coroot := by
  obtain ⟨j, hj⟩ := ht
  simpa only [coroot_eq_smul_coroot_iff.mpr hj, smul_smul, hs, one_smul] using mem_range_self j

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
z : ℤ
hz : ↑z * t = 1
s : R
hs : s * t = 1
ht : s • P.coroot i ∈ range ⇑P.coroot
⊢ t = 1 ∨ t = -1

Proof state:
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
this : z * w = 1
⊢ z = 1 ∨ z = -1

Tactic:
rw [Int.mul_eq_one_iff_eq_one_or_neg_one] at this

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
this : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
⊢ z = 1 ∨ z = -1

Proof state:
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
this : z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
⊢ z = 1 ∨ z = -1

Tactic:
tauto

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

Tactic:
left

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

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
ht : t • P.root i ∈ range ⇑P.root
⊢ t = 1 ∨ t = -1

Tactic:
obtain ⟨z, hz⟩ := b.eq_one_or_neg_one_of_mem_support_of_smul_mem_aux i h t ht

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

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

Tactic:
right

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