-- Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
lemma coxeterWeightIn_mem_set_of_isCrystallographic :
    P.coxeterWeightIn ℤ i j ∈ ({0, 1, 2, 3, 4} : Set ℤ)

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

Tactic:
have : P.coxeterWeightIn ℤ i j ≤ 4 := P.coxeterWeightIn_le_four ℤ i j

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : P.coxeterWeightIn ℤ i j ≤ 4
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : ↑n ≤ 4
⊢ ↑n = 0 ∨ ↑n = 1 ∨ ↑n = 2 ∨ ↑n = 3 ∨ ↑n = 4

Tactic:
norm_cast at this ⊢

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : n ≤ 4
⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : n ≤ 4
⊢ n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4

Tactic:
omega

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

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

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this : Fintype ι
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this : Fintype ι
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

Tactic:
obtain ⟨n, hcn⟩ : ∃ n : ℕ, P.coxeterWeightIn ℤ i j = n := by
  have : 0 ≤ P.coxeterWeightIn ℤ i j := by
    simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i j
  obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le this
  exact ⟨n, by simp [← P.algebraMap_coxeterWeightIn ℤ, hn]⟩

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
⊢ ∃ n, P.coxeterWeightIn ℤ i j = ↑n

Tactic:
obtain ⟨n, hn⟩ := Int.eq_ofNat_of_zero_le this

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
n : ℕ
hn : P.coxeterWeightIn ℤ i j = ↑n
⊢ ∃ n, P.coxeterWeightIn ℤ i j = ↑n

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this : Fintype ι
⊢ 0 ≤ P.coxeterWeightIn ℤ i j

Tactic:
simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i 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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
n : ℕ
hn : P.coxeterWeightIn ℤ i j = ↑n
⊢ P.coxeterWeightIn ℤ i j = ↑n

Tactic:
simp [← P.algebraMap_coxeterWeightIn ℤ, hn]

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this : Fintype ι
⊢ ∃ n, P.coxeterWeightIn ℤ i j = ↑n

Tactic:
have : 0 ≤ P.coxeterWeightIn ℤ i j := by
  simpa only [P.algebraMap_coxeterWeightIn] using P.coxeterWeight_nonneg (P.posRootForm ℤ) i j

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
⊢ ∃ n, P.coxeterWeightIn ℤ i j = ↑n

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : P.coxeterWeightIn ℤ i j ≤ 4
⊢ P.coxeterWeightIn ℤ i j ∈ {0, 1, 2, 3, 4}

Tactic:
simp only [hcn, mem_insert_iff, mem_singleton_iff] at this ⊢

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
n : ℕ
hcn : P.coxeterWeightIn ℤ i j = ↑n
this : ↑n ≤ 4
⊢ ↑n = 0 ∨ ↑n = 1 ∨ ↑n = 2 ∨ ↑n = 3 ∨ ↑n = 4

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
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : P.IsCrystallographic
i j : ι
this✝ : Fintype ι
this : 0 ≤ P.coxeterWeightIn ℤ i j
n : ℕ
hn : P.coxeterWeightIn ℤ i j = ↑n
⊢ ∃ n, P.coxeterWeightIn ℤ i j = ↑n

Tactic:
exact ⟨n, by simp [← P.algebraMap_coxeterWeightIn ℤ, hn]⟩

Result:
no goals