-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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) ⋯)
⊢ 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)
have 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) sorry)
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
Cleared hypotheses: hx