-- Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
Goal:
n : ℕ
K : Type u
inst : Field K
inst_1 : CharZero K
hn : NeZero n
hK : IsCyclotomicExtension {n} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ n
this : NumberField K
zero :
  ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero (R := ℕ) 0] [hK : IsCyclotomicExtension {0} ℚ K]
    {ζ : K} (hζ : IsPrimitiveRoot ζ 0) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
prime_pow :
  ∀ (p k : ℕ) (hp : Nat.Prime p) {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero (p ^ k)]
    [hK : IsCyclotomicExtension {p ^ k} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ k)) (this : NumberField K),
    Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
coprime :
  ∀ (n₁ n₂ : ℕ) (hn₁ : 1 < n₁) (hn₂ : 1 < n₂) (h : n₁.Coprime n₂)
    (hK₁ :
      ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₁] [hK : IsCyclotomicExtension {n₁} ℚ K]
        {ζ : K} (hζ : IsPrimitiveRoot ζ n₁) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤)
    (hK₂ :
      ∀ {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero n₂] [hK : IsCyclotomicExtension {n₂} ℚ K]
        {ζ : K} (hζ : IsPrimitiveRoot ζ n₂) (this : NumberField K), Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤)
    {K : Type u} [inst : Field K] [inst_2 : CharZero K] [hn : NeZero (n₁ * n₂)]
    [hK : IsCyclotomicExtension {n₁ * n₂} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (n₁ * n₂)) (this : NumberField K),
    Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤
⊢ Eq (α := Subalgebra ℤ (𝓞 K)) ℤ[hζ.toInteger] ⊤

Tactic:
induction n using Nat.recOnPrimeCoprime generalizing K hn with
  | zero => exact (neZero_zero_iff_false.mp hn).elim
  | prime_pow p k hp =>
    have : Fact (p.Prime) := ⟨hp⟩
    rw [← hζ.integralPowerBasisOfPrimePow.adjoin_gen_eq_top, hζ.integralPowerBasisOfPrimePow_gen]
  | coprime n₁ n₂ hn₁ hn₂ h hK₁ hK₂ =>
    have : NeZero n₁ := NeZero.of_gt hn₁
    have : NeZero n₂ := NeZero.of_gt hn₂
    have hζ₁ := hζ.pow (NeZero.pos _) (a := n₂) (b := n₁) (by rw [mul_comm])
    have := hζ₁.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₁ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₂)) n₁ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₁
    replace hK₁ := @hK₁ ℚ⟮ζ ^ n₂⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₁ (of_intermediateField _)
    have hζ₂ := hζ.pow (NeZero.pos _) (a := n₁) (b := n₂) rfl
    have := hζ₂.intermediateField_adjoin_isCyclotomicExtension ℚ
    replace hζ₂ : IsPrimitiveRoot (AdjoinSimple.gen ℚ (ζ ^ n₁)) n₂ :=
      IsPrimitiveRoot.coe_submonoidClass_iff.mp hζ₂
    replace hK₂ := @hK₂ ℚ⟮ζ ^ n₁⟯ _ _ _ _ (AdjoinSimple.gen _ _) hζ₂ (of_intermediateField _)
    have h_top : ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯ = ⊤ := by
      have : IsCyclotomicExtension {n₁ * n₂} ℚ (⊤ : IntermediateField ℚ K) :=
          hK.equiv _ _ _ topEquiv.symm
      have : IsCyclotomicExtension {n₁ * n₂} ℚ ↥(ℚ⟮ζ ^ n₂⟯ ⊔ ℚ⟮ζ ^ n₁⟯) := by
        rw [← Nat.Coprime.lcm_eq_mul h]
        exact isCyclotomicExtension_lcm_sup ℚ K n₁ n₂ ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯
      exact isCyclotomicExtension_eq {n₁ * n₂} ℚ K _ _
    exact adjoin_singleton_eq_top_aux K ℚ⟮ζ ^ n₂⟯ ℚ⟮ζ ^ n₁⟯ hζ₁ hK₁ hζ₂ hK₂ h h_top hζ

Premises used: IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, False.elim, IsPrimitiveRoot.integralPowerBasisOfPrimePow, PowerBasis.adjoin_gen_eq_top, neZero_zero_iff_false, Iff.mp, IsPrimitiveRoot.zero