awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS_1 : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this_3 : IsDedekindDomain S := ⋯
s : Finset L
b_1 : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b_1 : (a : ↥s) → L) x : L)
this :
  LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b_1 :
          Basis (↥s) K L) :
      (a : ↥s) → L)
n : ℕ
b :
  Basis.{0, u_1, u_4} (Fin n) R
    ↥(LinearMap.range
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L)))
f : HasQuotient.Quotient S (B := Submodule R S)
    (LinearMap.ker
      ((↑R :
          {S M : Type u_2} →
            {M₂ : Type u_4} →
              [inst : Semiring R] →
                [inst_18 : Semiring S] →
                  [inst_19 : AddCommMonoid M] →
                    [inst_20 : AddCommMonoid M₂] →
                      [inst_21 : Module R M] →
                        [inst_22 : Module R M₂] →
                          [inst_23 : Module S M] →
                            [inst_24 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (Algebra.linearMap S L))) ≃ₗ[R]
  S :=
  Eq.mpr (β := HasQuotient.Quotient S (B := Submodule R S) ⊥ ≃ₗ[R] S) ⋯ (Submodule.quotEquivOfEqBot ⊥ ⋯)
bS : Basis (Fin n) R S := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Algebra.IsIntegral R S

Tactic:
have : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
K : Type u_3
L : Type u_4
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Field K
inst_4 : Field L
inst_5 : Algebra R K
inst_6 : IsFractionRing R K
inst_7 : Algebra K L
inst_8 : FiniteDimensional K L
inst_9 : Algebra.IsSeparable K L
algRL : Algebra R L
inst_10 : IsScalarTower R K L
inst_11 : Algebra R S
inst_12 : Algebra S L
ist : IsScalarTower R S L
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_13 : DecidableEq ι
inst_14 : Fintype ι
bS_1 : Basis ι R S
adm : abv.IsAdmissible
inst_15 : Infinite R
inst_16 : DecidableEq R
inst_17 : IsIntegralClosure S R L
this_1 : DecidableEq L := Classical.decEq L
this_2 : IsFractionRing S L := ⋯
this_3 : IsDedekindDomain S := ⋯
s : Finset L
b_1 : Basis (↥s) K L
hb_int : ∀ (x : ↥s), IsIntegral R (A := L) ((b_1 : (a : ↥s) → L) x : L)
this_4 :
  LinearIndependent.{u_4, u_1, u_4} (ι := ↥s) R (M := L)
    (⇑(LinearMap.BilinForm.dualBasis.{u_4, u_3, u_4} (V := L) (K := K) (ι := ↥s) (Algebra.traceForm K L) ⋯ b_1 :
          Basis (↥s) K L) :
      (a : ↥s) → L)
n : ℕ
b :
  Basis.{0, u_1, u_4} (Fin n) R
    ↥(LinearMap.range
        ((↑R :
            {S M : Type u_2} →
              {M₂ : Type u_4} →
                [inst : Semiring R] →
                  [inst_18 : Semiring S] →
                    [inst_19 : AddCommMonoid M] →
                      [inst_20 : AddCommMonoid M₂] →
                        [inst_21 : Module R M] →
                          [inst_22 : Module R M₂] →
                            [inst_23 : Module S M] →
                              [inst_24 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
          (Algebra.linearMap S L)))
f : HasQuotient.Quotient S (B := Submodule R S)
    (LinearMap.ker
      ((↑R :
          {S M : Type u_2} →
            {M₂ : Type u_4} →
              [inst : Semiring R] →
                [inst_18 : Semiring S] →
                  [inst_19 : AddCommMonoid M] →
                    [inst_20 : AddCommMonoid M₂] →
                      [inst_21 : Module R M] →
                        [inst_22 : Module R M₂] →
                          [inst_23 : Module S M] →
                            [inst_24 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (Algebra.linearMap S L))) ≃ₗ[R]
  S :=
  Eq.mpr (β := HasQuotient.Quotient S (B := Submodule R S) ⊥ ≃ₗ[R] S) ⋯ (Submodule.quotEquivOfEqBot ⊥ ⋯)
bS : Basis (Fin n) R S := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : Algebra.IsIntegral R S
⊢ Fintype (ClassGroup S)

Tactic:
exact fintypeOfAdmissibleOfAlgebraic bS adm

Premises used: ClassGroup.fintypeOfAdmissibleOfAlgebraic
-- Module: Mathlib.NumberTheory.ClassNumber.FunctionField
Goal:
Fq : Type u_1
F : Type u_2
inst : Field Fq
inst_1 : Fintype Fq
inst_2 : Field F
inst_3 : Algebra.{u_1, u_2} Fq[X] F
inst_4 : Algebra.{u_1, u_2} (RatFunc Fq) F
inst_5 : IsScalarTower.{u_1, u_1, u_2} Fq[X] (RatFunc Fq) F
inst_6 : FunctionField Fq F
inst_7 : Algebra.IsSeparable.{u_1, u_2} (RatFunc Fq) F
⊢ classNumber Fq F = 1 ↔ IsPrincipalIdealRing.{u_2} ↥(ringOfIntegers Fq F)

Tactic:
card_classGroup_eq_one_iff

Premises used: Set.Mem, card_classGroup_eq_one_iff, FunctionField.classNumber
-- 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
⊢ IsCyclotomicExtension S A B ↔
    (∀ n ∈ S, n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n) ∧
      Eq.{v + 1} (α := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) ⊤

Tactic:
⟨fun h => ⟨fun _ => h.exists_isPrimitiveRoot, Algebra.eq_top_iff.2 h.adjoin_roots⟩, fun h =>
    ⟨h.1 _, Algebra.eq_top_iff.1 h.2⟩⟩

Premises used: IsCyclotomicExtension.mk, Iff.mpr, IsCyclotomicExtension.exists_isPrimitiveRoot, And.right, And.left, And.intro, Iff.intro, Iff.mp, Algebra.eq_top_iff, IsCyclotomicExtension.adjoin_roots
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
A : Type u
B : Type v
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
⊢ IsCyclotomicExtension {n} A B ↔
    (∃ (r : B), IsPrimitiveRoot r n) ∧ ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | b ^ n = 1}) x

Tactic:
simp [isCyclotomicExtension_iff, NeZero.ne]

Premises used: isCyclotomicExtension_iff, NeZero.ne
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
n : ℕ
inst : NeZero n
S T : Set ℕ
A : Type u
B : Type v
K : Type w
L : Type z
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra A B
inst_4 : Field K
inst_5 : Field L
inst_6 : Algebra K L
h : IsCyclotomicExtension ∅ A B
⊢ Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤

Tactic:
simpa [Algebra.eq_top_iff, isCyclotomicExtension_iff] using h

Premises used: isCyclotomicExtension_iff, Algebra.eq_top_iff
-- 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
⊢ IsCyclotomicExtension S A B = IsCyclotomicExtension (S \ {0}) A B

Tactic:
simp [isCyclotomicExtension_iff, and_assoc]

Premises used: isCyclotomicExtension_iff, and_assoc
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension {1} A B
x : B
⊢ Membership.mem (γ := Subalgebra A B) ⊥ x

Tactic:
simpa [adjoin_singleton_one] using ((isCyclotomicExtension_iff _ _ _).1 h).2 x

Premises used: Algebra.adjoin_singleton_one, And.right, isCyclotomicExtension_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤
⊢ (∀ (n : ℕ), Membership.mem (γ := Set ℕ) {0} n → n ≠ 0 → ∃ (r : B), IsPrimitiveRoot r n) ∧
    Eq.{v + 1} (α := Subalgebra A B)
      (adjoin A {b : B | ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {0} n ∧ n ≠ 0 ∧ b ^ n = 1}) ⊤

Tactic:
simpa
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
rw : IsCyclotomicExtension {0} A B ↔ Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤
⊢ IsCyclotomicExtension {0} A B ↔ Function.Surjective.{u + 1, v + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)

Tactic:
rw [surjective_algebraMap_iff, eq_comm]

Premises used: eq_comm, Algebra.surjective_algebraMap_iff
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
⊢ IsCyclotomicExtension {0} A B ↔ Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤

Tactic:
⟨?_, fun h ↦ singleton_zero_of_bot_eq_top h⟩

Premises used: IsCyclotomicExtension.singleton_zero_of_bot_eq_top, Iff.intro
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
refine : IsCyclotomicExtension {0} A B → Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤
⊢ IsCyclotomicExtension {0} A B ↔ Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤

Tactic:
refine ⟨?_, fun h ↦ singleton_zero_of_bot_eq_top h⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
rw : IsCyclotomicExtension ∅ A B → Subsingleton.{v + 1} (Subalgebra A B)
⊢ IsCyclotomicExtension {0} A B → Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤

Tactic:
rw [eq_self_sdiff_zero, sdiff_self, Set.bot_eq_empty, subsingleton_iff_bot_eq_top]

Premises used: sdiff_self, Set.bot_eq_empty, IsCyclotomicExtension.eq_self_sdiff_zero, subsingleton_iff_bot_eq_top
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
⊢ IsCyclotomicExtension ∅ A B → Subsingleton.{v + 1} (Subalgebra A B)

Tactic:
fun _ ↦ instSubsingleton A B

Premises used: IsCyclotomicExtension.instSubsingleton
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
⊢ IsCyclotomicExtension ∅ A B → Subsingleton.{v + 1} (Subalgebra A B)

Tactic:
exact fun _ ↦ instSubsingleton A B
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
⊢ IsCyclotomicExtension (S ∪ T) A C

Tactic:
⟨fun hn => ?_, fun x => ?_⟩

Premises used: IsCyclotomicExtension.mk
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
refine_1 : ∀ {n : ℕ} (hn : n ∈ S ∪ T) (ha' : n ≠ 0), ∃ (r : C), IsPrimitiveRoot r n
refine_2 : ∀ (x : C), Membership.mem (γ := Subalgebra A C) (adjoin A {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) x
⊢ IsCyclotomicExtension (S ∪ T) A C

Tactic:
refine ⟨fun hn => ?_, fun x => ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
n : ℕ
hn : n ∈ S ∪ T
hn' : n ≠ 0
refine_1 : ∀ (hn : n ∈ S), ∃ (r : C), IsPrimitiveRoot r n
refine_1₁ : ∀ (hn : n ∈ T), ∃ (r : C), IsPrimitiveRoot r n
⊢ ∃ (r : C), IsPrimitiveRoot r n

Tactic:
rcases hn with hn | hn
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
n : ℕ
hn' : n ≠ 0
hn : n ∈ S
refine_1 : ∀ (b : B) (hb : IsPrimitiveRoot b n), ∃ (r : C), IsPrimitiveRoot r n
⊢ ∃ (r : C), IsPrimitiveRoot r n

Tactic:
obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn hn'

Premises used: And.left, isCyclotomicExtension_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
n : ℕ
hn' : n ≠ 0
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b n
⊢ ∃ (r : C), IsPrimitiveRoot r n

Tactic:
⟨algebraMap B C b, ?_⟩

Premises used: Algebra.algebraMap, Exists.intro, DFunLike.coe
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
n : ℕ
hn' : n ≠ 0
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b n
refine_1 : IsPrimitiveRoot.{w} (M := C) ((algebraMap B C : (a : B) → C) b : C) n
⊢ ∃ (r : C), IsPrimitiveRoot r n

Tactic:
refine ⟨algebraMap B C b, ?_⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
n : ℕ
hn' : n ≠ 0
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b n
⊢ IsPrimitiveRoot.{w} (M := C) ((algebraMap B C : (a : B) → C) b : C) n

Tactic:
hb.map_of_injective h

Premises used: IsPrimitiveRoot.map_of_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
n : ℕ
hn' : n ≠ 0
hn : n ∈ S
b : B
hb : IsPrimitiveRoot b n
⊢ IsPrimitiveRoot.{w} (M := C) ((algebraMap B C : (a : B) → C) b : C) n

Tactic:
exact hb.map_of_injective h

Premises used: IsPrimitiveRoot.map_of_injective
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
n : ℕ
hn' : n ≠ 0
hn : n ∈ T
⊢ ∃ (r : C), IsPrimitiveRoot r n

Tactic:
((isCyclotomicExtension_iff _ _ _).1 hT).1 hn hn'

Premises used: And.left, isCyclotomicExtension_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
n : ℕ
hn' : n ≠ 0
hn : n ∈ T
⊢ ∃ (r : C), IsPrimitiveRoot r n

Tactic:
exact ((isCyclotomicExtension_iff _ _ _).1 hT).1 hn hn'

Premises used: And.left, isCyclotomicExtension_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
⊢ Membership.mem (γ := Subalgebra A C) (adjoin A {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) x

Tactic:
adjoin_induction (hx := ((isCyclotomicExtension_iff T B _).1 hT).2 x)
      (fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => ?_)
      (fun x y _ _ hx hy => Subalgebra.add_mem _ hx hy)
      fun x y _ _ hx hy => Subalgebra.mul_mem _ hx hy

Premises used: Algebra.adjoin_induction, And.right, isCyclotomicExtension_iff, Iff.mp
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
refine_2 :
  ∀ (b : B),
    Membership.mem.{w, w} (α := C) (γ := Subalgebra A C) (adjoin A {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1})
      ((algebraMap B C : (a : B) → C) b : C)
⊢ Membership.mem (γ := Subalgebra A C) (adjoin A {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) x

Tactic:
refine adjoin_induction (hx := ((isCyclotomicExtension_iff T B _).1 hT).2 x)
      (fun c ⟨n, hn⟩ => subset_adjoin ⟨n, Or.inr hn.1, hn.2⟩) (fun b => ?_)
      (fun x y _ _ hx hy => Subalgebra.add_mem _ hx hy)
      fun x y _ _ hx hy => Subalgebra.mul_mem _ hx hy
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
⊢ Membership.mem (α := C) (Subalgebra.map f (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) ((f : (a : B) → C) b : C)

Tactic:
have hb : f b ∈ (adjoin A {b : B | ∃ a : ℕ, a ∈ S ∧ a ≠ 0 ∧ b ^ a = 1}).map f :=
      ⟨b, ((isCyclotomicExtension_iff _ _ _).1 hS).2 b, rfl⟩
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb :
  Membership.mem (α := C) (Subalgebra.map f (adjoin A {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1})) ((f : (a : B) → C) b : C)
⊢ Membership.mem.{w, w} (α := C) (γ := Subalgebra A C)
    (adjoin A (image.{v, w} (α := B) (⇑f : (a : B) → C) {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    ((algebraMap B C : (a : B) → C) b : C)

Tactic:
rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb

Premises used: Algebra.adjoin_image, IsScalarTower.toAlgHom_apply
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb :
  Membership.mem.{w, w} (α := C) (γ := Subalgebra A C)
    (adjoin A (image.{v, w} (α := B) (⇑f : (a : B) → C) {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    ((algebraMap B C : (a : B) → C) b : C)
⊢ Membership.mem.{w, w} (α := C) (γ := Subalgebra A C) (adjoin A {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1})
    ((algebraMap B C : (a : B) → C) b : C)

Tactic:
adjoin_mono (fun y hy => ?_) hb

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb :
  Membership.mem.{w, w} (α := C) (γ := Subalgebra A C)
    (adjoin A (image.{v, w} (α := B) (⇑f : (a : B) → C) {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    ((algebraMap B C : (a : B) → C) b : C)
refine_2 :
  ∀ (y : C)
    (hy :
      Membership.mem (γ := Set C) (image.{v, w} (α := B) (⇑f : (a : B) → C) {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) y),
    Membership.mem (γ := Set C) {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} y
⊢ Membership.mem.{w, w} (α := C) (γ := Subalgebra A C) (adjoin A {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1})
    ((algebraMap B C : (a : B) → C) b : C)

Tactic:
refine adjoin_mono (fun y hy => ?_) hb

Premises used: Algebra.adjoin_mono
-- Module: Mathlib.NumberTheory.Cyclotomic.Basic
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
C : Type w
inst_3 : CommRing C
inst_4 : Algebra A C
inst_5 : Algebra B C
inst_6 : IsScalarTower A B C
hS : IsCyclotomicExtension S A B
hT : IsCyclotomicExtension T B C
h : Function.Injective.{v + 1, w + 1} (α := B) (β := C) (⇑(algebraMap B C) : (a : B) → C)
x : C
b : B
f : B →ₐ[A] C := IsScalarTower.toAlgHom A B C
hb :
  Membership.mem.{w, w} (α := C) (γ := Subalgebra A C)
    (adjoin A (image.{v, w} (α := B) (⇑f : (a : B) → C) {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}))
    ((algebraMap B C : (a : B) → C) b : C)
y : C
hy : Membership.mem (γ := Set C) (image.{v, w} (α := B) (⇑f : (a : B) → C) {b : B | ∃ a ∈ S, a ≠ 0 ∧ b ^ a = 1}) y
refine_2 :
  ∀ (b₁ : B) (h₁ : (f : (a : B) → C) b₁ = y) (n : ℕ) (hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1),
    Membership.mem (γ := Set C) {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} y
⊢ Membership.mem (γ := Set C) {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} y

Tactic:
obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy