-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem finite_of_singleton [IsDomain B] [h : IsCyclotomicExtension {n} A B] :
    Module.Finite A B

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ (Subalgebra.toSubmodule (adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1})).FG

Tactic:
refine fg_adjoin_of_finite ?_ fun b hb => ?_

Result:
case refine_1
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}.Finite

case refine_2
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
b : B
hb : b ∈ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
⊢ IsIntegral A b

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
b : B
hb : b ^ ↑n = 1
⊢ eval₂ (algebraMap A B) b (X ^ ↑n - 1) = 0

Tactic:
simp [hb]

Result:
no goals

Proof state:
case refine_1
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}.Finite

Tactic:
simp only [mem_singleton_iff, exists_eq_left]

Result:
case refine_1
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ {b | b ^ ↑n = 1}.Finite

Proof state:
case refine_1
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ {b | b ^ ↑n = 1}.Finite

Tactic:
have : {b : B | b ^ (n : ℕ) = 1} = (nthRoots n (1 : B)).toFinset :=
  Set.ext fun x => ⟨fun h => by simpa using h, fun h => by simpa using h⟩

Result:
case refine_1
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | b ^ ↑n = 1} = ↑(nthRoots (↑n) 1).toFinset
⊢ {b | b ^ ↑n = 1}.Finite

Proof state:
case refine_1
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | b ^ ↑n = 1} = ↑(nthRoots (↑n) 1).toFinset
⊢ (↑(nthRoots (↑n) 1).toFinset).Finite

Tactic:
exact (nthRoots (↑n) 1).toFinset.finite_toSet

Result:
no goals

Proof state:
case refine_2
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
b : B
hb : b ∈ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
⊢ IsIntegral A b

Tactic:
simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq] at hb

Result:
case refine_2
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
b : B
hb : b ^ ↑n = 1
⊢ IsIntegral A b

Proof state:
case refine_1
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | b ^ ↑n = 1} = ↑(nthRoots (↑n) 1).toFinset
⊢ {b | b ^ ↑n = 1}.Finite

Tactic:
rw [this]

Result:
case refine_1
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
this : {b | b ^ ↑n = 1} = ↑(nthRoots (↑n) 1).toFinset
⊢ (↑(nthRoots (↑n) 1).toFinset).Finite

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h✝ : IsCyclotomicExtension {n} A B
x : B
h : x ∈ ↑(nthRoots (↑n) 1).toFinset
⊢ x ∈ {b | b ^ ↑n = 1}

Tactic:
simpa using h

Result:
no goals

Proof state:
case refine_2
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
b : B
hb : b ^ ↑n = 1
⊢ IsIntegral A b

Tactic:
exact ⟨X ^ (n : ℕ) - 1, ⟨monic_X_pow_sub_C _ n.pos.ne.symm, by simp [hb]⟩⟩

Result:
no goals

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ Module.Finite A B

Tactic:
rw [Module.finite_def, ← top_toSubmodule, ← ((iff_adjoin_eq_top _ _ _).1 h).2]

Result:
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h : IsCyclotomicExtension {n} A B
⊢ (Subalgebra.toSubmodule (adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1})).FG

Proof state:
n : ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h✝ : IsCyclotomicExtension {n} A B
x : B
h : x ∈ {b | b ^ ↑n = 1}
⊢ x ∈ ↑(nthRoots (↑n) 1).toFinset

Tactic:
simpa using h

Result:
no goals