-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : ∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n
x : B
hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
mem :
  ∀ (x : B) (hx : Membership.mem (γ := Set B) {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} x),
    Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
      (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
      (Subtype.mk (p := fun (x : B) ↦
        Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x ⋯)
algebraMap :
  ∀ (x : A),
    Membership.mem.{v, v} (α := ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})) (γ :=
      Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
      (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
      (Subtype.mk (p := fun (x : B) ↦
          Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x)
          ((Algebra.algebraMap A B : (a : A) → B) x) ⋯ :
        ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
add :
  ∀ (x y : B) (hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x)
    (hy : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) y)
    (ihx :
      Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
        (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
        (Subtype.mk (p := fun (x : B) ↦
          Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x hx))
    (ihy :
      Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
        (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
        (Subtype.mk (p := fun (x : B) ↦
          Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) y hy)),
    Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
      (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
      (Subtype.mk (p := fun (x : B) ↦
        Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) (x + y) ⋯)
mul :
  ∀ (x y : B) (hx : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x)
    (hy : Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) y)
    (ihx :
      Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
        (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
        (Subtype.mk (p := fun (x : B) ↦
          Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x hx))
    (ihy :
      Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
        (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
        (Subtype.mk (p := fun (x : B) ↦
          Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) y hy)),
    Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
      (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
      (Subtype.mk (p := fun (x : B) ↦
        Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) (x * y) ⋯)
⊢ Membership.mem (γ := Subalgebra A ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}))
    (adjoin A {b : ↥(adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1})
    (Subtype.mk (p := fun (x : B) ↦
      Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) x hx)

Tactic:
induction hx using adjoin_induction with
    | mem x hx =>
      obtain ⟨n, hn1, hn2, hx⟩ := hx
      exact subset_adjoin ⟨n, hn1, hn2, Subtype.val_injective hx⟩
    | algebraMap x => exact Subalgebra.algebraMap_mem _ x
    | add x y hx hy ihx ihy => exact Subalgebra.add_mem _ ihx ihy
    | mul x y hx hy ihx ihy => exact Subalgebra.mul_mem _ ihx ihy

Premises used: Algebra.algebraMap, Subalgebra.algebraMap_mem