awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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 : 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)))
⊢ 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
have rw : HasQuotient.Quotient S (B := Submodule R S) ⊥ ≃ₗ[R] S
Tactic: rw [LinearMap.ker_eq_bot.mpr]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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)
⊢ Fintype (ClassGroup S)
have this₁ : Algebra.IsIntegral R S
Tactic: have : Algebra.IsIntegral R S := IsIntegralClosure.isIntegral_algebra R L
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
⊢ IsCyclotomicExtension {0} A B ↔ Function.Surjective.{u + 1, v + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
have rw : IsCyclotomicExtension {0} A B ↔ Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤
Tactic: rw [surjective_algebraMap_iff, eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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) ⊥ ⊤
have refine : IsCyclotomicExtension {0} A B → Eq.{v + 1} (α := Subalgebra A B) ⊥ ⊤
Tactic: refine ⟨?_, fun h ↦ singleton_zero_of_bot_eq_top h⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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) ⊥ ⊤
have rw : IsCyclotomicExtension ∅ A B → Subsingleton.{v + 1} (Subalgebra A B)
Tactic: rw [eq_self_sdiff_zero, sdiff_self, Set.bot_eq_empty, subsingleton_iff_bot_eq_top]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
have refine_1 : ∀ {n : ℕ} (hn : n ∈ S ∪ T) (ha' : n ≠ 0), ∃ (r : C), IsPrimitiveRoot r n
Tactic: refine ⟨fun hn => ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ IsCyclotomicExtension (S ∪ T) A C
have refine_2 : ∀ (x : C), Membership.mem (γ := Subalgebra A C) (adjoin A {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}) x
Tactic: refine ⟨fun hn => ?_, fun x => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ ∃ (r : C), IsPrimitiveRoot r n
have refine_1 : ∀ (hn : n ∈ S), ∃ (r : C), IsPrimitiveRoot r n
Tactic: rcases hn with hn | hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ ∃ (r : C), IsPrimitiveRoot r n
have refine_1₁ : ∀ (hn : n ∈ T), ∃ (r : C), IsPrimitiveRoot r n
Tactic: rcases hn with hn | hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ ∃ (r : C), IsPrimitiveRoot r n
have refine_1 : ∀ (b : B) (hb : IsPrimitiveRoot b n), ∃ (r : C), IsPrimitiveRoot r n
Tactic: obtain ⟨b, hb⟩ := ((isCyclotomicExtension_iff _ _ _).1 hS).1 hn hn'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
have refine_1 : IsPrimitiveRoot.{w} (M := C) ((algebraMap B C : (a : B) → C) b : C) n
Tactic: refine ⟨algebraMap B C b, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
have 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)
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
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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.{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)
have hb : 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⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
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 {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1})
    ((algebraMap B C : (a : B) → C) b : C)
have 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)
Tactic: rw [IsScalarTower.toAlgHom_apply, ← adjoin_image] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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)
have 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
Tactic: refine adjoin_mono (fun y hy => ?_) hb
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
⊢ Membership.mem (γ := Set C) {b : C | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1} y
have 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
Tactic: obtain ⟨b₁, ⟨⟨n, hn⟩, h₁⟩⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
b₁ : B
h₁ : (f : (a : B) → C) b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
⊢ y ^ n = 1
have rw : HPow.hPow (α := C) ((f : (a : B) → C) b₁ : C) n = 1
Tactic: rw [← h₁, ← map_pow, hn.2.2, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
b₁ : B
h₁ : (f : (a : B) → C) b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
rw : HPow.hPow (α := C) ((f : (a : B) → C) b₁ : C) n = 1
⊢ y ^ n = 1
have rw₁ : Eq.{w + 1} (α := C) ((f : (a : B) → C) (b₁ ^ n) : C) (1 : C)
Tactic: rw [← h₁, ← map_pow, hn.2.2, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
b₁ : B
h₁ : (f : (a : B) → C) b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
rw : HPow.hPow (α := C) ((f : (a : B) → C) b₁ : C) n = 1
rw₁ : Eq.{w + 1} (α := C) ((f : (a : B) → C) (b₁ ^ n) : C) (1 : C)
⊢ y ^ n = 1
have rw₂ : Eq.{w + 1} (α := C) ((f : (a : B) → C) 1 : C) (1 : C)
Tactic: rw [← h₁, ← map_pow, hn.2.2, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
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
b₁ : B
h₁ : (f : (a : B) → C) b₁ = y
n : ℕ
hn : n ∈ S ∧ n ≠ 0 ∧ b₁ ^ n = 1
rw : HPow.hPow (α := C) ((f : (a : B) → C) b₁ : C) n = 1
rw₁ : Eq.{w + 1} (α := C) ((f : (a : B) → C) (b₁ ^ n) : C) (1 : C)
rw₂ : Eq.{w + 1} (α := C) ((f : (a : B) → C) 1 : C) (1 : C)
⊢ y ^ n = 1
have rw₃ : Eq.{w + 1} (α := C) 1 1
Tactic: rw [← h₁, ← map_pow, hn.2.2, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
⊢ IsCyclotomicExtension S A B ↔ S ⊆ {0, 1}
have this : Subsingleton.{v + 1} (Subalgebra A B)
Tactic: have : Subsingleton (Subalgebra A B) := inferInstance
-- 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
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
⊢ IsCyclotomicExtension S A B ↔ S ⊆ {0, 1}
have refine_1 : IsCyclotomicExtension S A B →
  ∀ (hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n),
    (∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) → S ⊆ {0, 1}
Tactic: refine ⟨fun ⟨hprim, _⟩ ↦ ?_, fun hS ↦ ?_⟩
-- 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
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
refine_1 :
  IsCyclotomicExtension S A B →
    ∀ (hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n),
      (∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x) → S ⊆ {0, 1}
⊢ IsCyclotomicExtension S A B ↔ S ⊆ {0, 1}
have refine_2 : ∀ (hS : S ⊆ {0, 1}), IsCyclotomicExtension S A B
Tactic: refine ⟨fun ⟨hprim, _⟩ ↦ ?_, fun hS ↦ ?_⟩
-- 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
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
h : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n
adjoin_roots : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
⊢ S ⊆ {0, 1}
have refine_1 : ∀ (s : ℕ) (hs : s ∈ S) (hs' : ¬s = 0), s = 1
Tactic: refine subset_pair_iff.mpr fun s hs ↦ or_iff_not_imp_left.mpr fun hs' ↦ ?_
-- 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
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
h : IsCyclotomicExtension S A B
hprim : ∀ {n : ℕ} (ha : n ∈ S) (ha' : n ≠ 0), ∃ (r : B), IsPrimitiveRoot r n
adjoin_roots : ∀ (x : B), Membership.mem (γ := Subalgebra A B) (adjoin A {b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1}) x
s : ℕ
hs : s ∈ S
hs' : ¬s = 0
⊢ s = 1
have refine_1 : ∀ (ζ : B) (hζ : IsPrimitiveRoot ζ s), s = 1
Tactic: obtain ⟨ζ, hζ⟩ := hprim hs hs'
-- 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
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
hS : S ⊆ {0, 1}
⊢ IsCyclotomicExtension S A B
have refine_2 : ∀ {s : ℕ} (hs : s ∈ S) (hs' : s ≠ 0), ∃ (r : B), IsPrimitiveRoot r s
Tactic: refine ⟨fun {s} hs hs' ↦ ?_, fun x ↦ by convert! (mem_top (R := A) : x ∈ ⊤)⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (hypothesis)
Goal:
S : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
inst_3 : Subsingleton B
this : Subsingleton.{v + 1} (Subalgebra A B)
hS : S ⊆ {0, 1}
s : ℕ
hs : s ∈ S
hs' : s ≠ 0
⊢ ∃ (r : B), IsPrimitiveRoot r s
have this₁ : s = 1
Tactic: have : s = 1 := (subset_pair_iff.mp hS s hs).resolve_left hs'
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
⊢ Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
have refine_1 : LE.le.{v} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
  ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Cyclotomic.Basic (goal)
Goal:
S T : Set ℕ
A : Type u
B : Type v
inst : CommRing A
inst_1 : CommRing B
inst_2 : Algebra A B
h : IsCyclotomicExtension (S ∪ T) A B
refine_1 :
  LE.le.{v} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
⊢ Eq.{v + 1} (α := Set B) {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
    ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
have refine_2 : LE.le.{v} (α := Set B) ({b : B | ∃ n ∈ S, n ≠ 0 ∧ b ^ n = 1} ∪ {b : B | ∃ n ∈ T, n ≠ 0 ∧ b ^ n = 1})
  {b : B | ∃ n ∈ S ∪ T, n ≠ 0 ∧ b ^ n = 1}
Tactic: refine le_antisymm ?_ ?_