-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S : Set ℕ
K : Type w
L : Type z
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsCyclotomicExtension S K L
i : L ≃ₐ[K] ↥(IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
f : AlgebraicClosure K →ₐ[K] AlgebraicClosure K
y : AlgebraicClosure K
hy :
  Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y
right :
  ∀ (x : AlgebraicClosure K)
    (hx : Membership.mem (γ := Set (AlgebraicClosure K)) {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1} x),
    Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
      (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)
right₁ :
  ∀ (x : K),
    Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
      (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K)
          ((algebraMap K (AlgebraicClosure K) : (a : K) → AlgebraicClosure K) x) :
        AlgebraicClosure K)
right₂ :
  ∀ (x y : AlgebraicClosure K)
    (hx :
      Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x)
    (hy :
      Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y)
    (ihx :
      Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
        ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K))
    (ihy :
      Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
        ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K)),
    Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
      (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) (x + y) : AlgebraicClosure K)
right₃ :
  ∀ (x y : AlgebraicClosure K)
    (hx :
      Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x)
    (hy :
      Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) y)
    (ihx :
      Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
        ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K))
    (ihy :
      Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
        ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K)),
    Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
      (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) (x * y) : AlgebraicClosure K)
right₄ :
  ∀ (x : AlgebraicClosure K)
    (hx :
      Membership.mem (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1}) x)
    (ihx :
      Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
        (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
        ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x : AlgebraicClosure K)),
    Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
      (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
      ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) x⁻¹ : AlgebraicClosure K)
⊢ Membership.mem (α := AlgebraicClosure K) (γ := IntermediateField K (AlgebraicClosure K))
    (IntermediateField.adjoin K {x : AlgebraicClosure K | ∃ n ∈ S, n ≠ 0 ∧ x ^ n = 1})
    ((f : (a : AlgebraicClosure K) → AlgebraicClosure K) y : AlgebraicClosure K)

Tactic:
induction hy using IntermediateField.adjoin_induction with
  | mem x hx =>
    obtain ⟨n, hn, h1, h2⟩ := hx
    apply IntermediateField.subset_adjoin
    use n, hn, h1
    rw [← map_pow, ← map_one f, h2]
  | algebraMap x =>
    convert! IntermediateField.algebraMap_mem _ x
    exact AlgHom.commutes _ x
  | add x y hx hy ihx ihy =>
    rw [map_add]
    exact add_mem ihx ihy
  | mul x y hx hy ihx ihy =>
    rw [map_mul]
    exact mul_mem ihx ihy
  | inv x hx ihx =>
    rw [map_inv₀]
    exact inv_mem ihx

Premises used: Algebra.algebraMap, map_inv₀, map_add, map_pow, IntermediateField.subset_adjoin, map_mul, map_one