-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem _root_.IsPrimitiveRoot.adjoin_isCyclotomicExtension {ζ : B} {n : ℕ+}
    (h : IsPrimitiveRoot ζ n) : IsCyclotomicExtension {n} A (adjoin A ({ζ} : Set B)) :=
  { exists_prim_root := fun hi => by
      rw [Set.mem_singleton_iff] at hi
      refine ⟨⟨ζ, subset_adjoin <| Set.mem_singleton ζ⟩, ?_⟩
      rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk, hi]
    adjoin_roots := fun ⟨x, hx⟩ => by
      refine
        adjoin_induction
          (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
          (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
      · rw [Set.mem_singleton_iff] at hb
        refine subset_adjoin ?_
        simp only [mem_singleton_iff, exists_eq_left, mem_setOf_eq, hb]
        rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]
        exact ((IsPrimitiveRoot.iff_def ζ n).1 h).1
      · exact Subalgebra.algebraMap_mem _ _
      · exact Subalgebra.add_mem _ hb₁ hb₂
      · exact Subalgebra.mul_mem _ hb₁ hb₂ }

Proof state:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ⟨ζ, ⋯⟩ ^ ↑n = 1

Tactic:
rw [← Subalgebra.coe_eq_one, Subalgebra.coe_pow, Subtype.coe_mk]

Result:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ζ ^ ↑n = 1

Proof state:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ζ ^ ↑n = 1

Tactic:
exact ((IsPrimitiveRoot.iff_def ζ n).1 h).1

Result:
no goals

Proof state:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb : b ∈ {ζ}
⊢ ⟨b, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
rw [Set.mem_singleton_iff] at hb

Result:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ⟨b, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
n✝ : ℕ+
hi : n✝ ∈ {n}
⊢ ∃ r, IsPrimitiveRoot r ↑n✝

Tactic:
rw [Set.mem_singleton_iff] at hi

Result:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
n✝ : ℕ+
hi : n✝ = n
⊢ ∃ r, IsPrimitiveRoot r ↑n✝

Proof state:
case refine_2
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
a : A
⊢ ⟨(algebraMap A B) a, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
exact Subalgebra.algebraMap_mem _ _

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
n✝ : ℕ+
hi : n✝ = n
⊢ IsPrimitiveRoot ⟨ζ, ⋯⟩ ↑n✝

Tactic:
rwa [← IsPrimitiveRoot.coe_submonoidClass_iff, Subtype.coe_mk, hi]

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
n✝ : ℕ+
hi : n✝ = n
⊢ ∃ r, IsPrimitiveRoot r ↑n✝

Tactic:
refine ⟨⟨ζ, subset_adjoin <| Set.mem_singleton ζ⟩, ?_⟩

Result:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
n✝ : ℕ+
hi : n✝ = n
⊢ IsPrimitiveRoot ⟨ζ, ⋯⟩ ↑n✝

Proof state:
case refine_3
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝² : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b₁ b₂ : B
x✝¹ : b₁ ∈ adjoin A {ζ}
x✝ : b₂ ∈ adjoin A {ζ}
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
⊢ ⟨b₁ + b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
exact Subalgebra.add_mem _ hb₁ hb₂

Result:
no goals

Proof state:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ⟨b, ⋯⟩ ∈ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

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

Result:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ⟨ζ, ⋯⟩ ^ ↑n = 1

Proof state:
case refine_4
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝² : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b₁ b₂ : B
x✝¹ : b₁ ∈ adjoin A {ζ}
x✝ : b₂ ∈ adjoin A {ζ}
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
⊢ ⟨b₁ * b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
exact Subalgebra.mul_mem _ hb₁ hb₂

Result:
no goals

Proof state:
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
⊢ ⟨x, hx⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
refine
  adjoin_induction
    (hx := hx) (fun b hb => ?_) (fun a => ?_) (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)
    (fun b₁ b₂ _ _ hb₁ hb₂ => ?_)

Result:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb : b ∈ {ζ}
⊢ ⟨b, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

case refine_2
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
a : A
⊢ ⟨(algebraMap A B) a, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

case refine_3
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝² : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b₁ b₂ : B
x✝¹ : b₁ ∈ adjoin A {ζ}
x✝ : b₂ ∈ adjoin A {ζ}
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
⊢ ⟨b₁ + b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

case refine_4
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝² : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b₁ b₂ : B
x✝¹ : b₁ ∈ adjoin A {ζ}
x✝ : b₂ ∈ adjoin A {ζ}
hb₁ : ⟨b₁, x✝¹⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
hb₂ : ⟨b₂, x✝⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
⊢ ⟨b₁ * b₂, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Proof state:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ⟨b, ⋯⟩ ∈ adjoin A {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
refine subset_adjoin ?_

Result:
case refine_1
A : Type u
B : Type v
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
ζ : B
n : ℕ+
h : IsPrimitiveRoot ζ ↑n
x✝ : ↥(adjoin A {ζ})
x : B
hx : x ∈ adjoin A {ζ}
b : B
hb✝ : b ∈ {ζ}
hb : b = ζ
⊢ ⟨b, ⋯⟩ ∈ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}