awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst_3 : (↑w : AbsoluteValue L ℝ).LiesOver (↑v : AbsoluteValue K ℝ)
⊢ Eq (α := RingHom.{u_1, u_2} (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥) w.Completion)
    (RingHom.comp (algebraMap v.Completion w.Completion) (RingEquiv.toRingHom (RingEquiv.quotientBot v.Completion)))
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.quotientBot w.Completion))
      (algebraMap (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
        (HasQuotient.Quotient w.Completion (B := Ideal w.Completion) ⊥)))
have h : ∀ (x : v.Completion),
  Eq.{u_2 + 1} (α := w.Completion)
    ((@RingHom.comp _ (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥) _ _ Semiring.toNonAssocSemiring _
            (RingHom.comp (algebraMap v.Completion w.Completion)
              (RingEquiv.toRingHom (RingEquiv.quotientBot v.Completion)))
            (Ideal.Quotient.mk ⊥) :
          (a : v.Completion) → w.Completion)
        x :
      w.Completion)
    ((RingHom.comp (β := HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
            (RingHom.comp (RingEquiv.toRingHom (RingEquiv.quotientBot w.Completion))
              (algebraMap (HasQuotient.Quotient v.Completion (B := Ideal v.Completion) ⊥)
                (HasQuotient.Quotient w.Completion (B := Ideal w.Completion) ⊥)))
            (Ideal.Quotient.mk ⊥) :
          (a : v.Completion) → w.Completion)
        x :
      w.Completion)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Completion.Ramification (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
v : InfinitePlace K
inst_3 : NumberField K
inst_4 : NumberField L
⊢ ∑ w ∈ toFinset (placesOver L v), v.inertiaDeg w = Module.finrank K L
have rw : ∑ x ∈ toFinset (unramifiedPlacesOver L v), 1 +
    HSMul.hSMul (β := ℕ) (card (α := InfinitePlace L) (toFinset (ramifiedPlacesOver L v))) 2 =
  Module.finrank K L
Tactic: rw [← union_ramifiedPlacesOver_unramifiedPlacesOver L v, toFinset_union,
    sum_union (Set.disjoint_toFinset.2 <| disjoint_ramifiedPlacesOver_unramifiedPlacesOver L v),
    sum_congr rfl (fun _ h ↦ inertiaDeg_eq_two (by simpa using h)),
    sum_congr rfl (fun _ h ↦ inertiaDeg_eq_one (by simpa using h)), sum_const, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hk : p ^ (k + 1) ≠ 2
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ (k + 1)) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ k * ((p - 1) * (k + 1) - 1))
have rw : Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
    (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
      (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
    (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
Tactic: rw [← discr_prime_pow_ne_two hζ (cyclotomic.irreducible_rat (NeZero.pos _)) hk]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ p
hodd : p ≠ 2
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    HPow.hPow (α := ℚ) (-1) ((p - 1) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p - 2)
have rw : Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
    (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
      (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
    (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
Tactic: rw [← discr_odd_prime hζ (cyclotomic.irreducible_rat hp.out.pos) hodd]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    HPow.hPow (α := ℚ) (-1) (φ (p ^ k) / 2) * HPow.hPow (α := ℚ) (↑p : ℚ) (p ^ (k - 1) * ((p - 1) * k - 1))
have rw : Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
    (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
      (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
    (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K)
Tactic: rw [← discr_prime_pow hζ (cyclotomic.irreducible_rat (NeZero.pos _))]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
inst_2 : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ ∃ (u : ℤˣ) (n : ℕ),
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
        (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
          (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
      (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
have rw : ∃ (u : ℤˣ) (n : ℕ),
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.powerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.powerBasis ℚ hζ)) : (a : Fin (IsPrimitiveRoot.powerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
Tactic: rw [hζ.discr_zeta_eq_discr_zeta_sub_one.symm]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K
have refine_1 : ∀ (x : K) (h : IsIntegral ℤ x), Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
Tactic: refine ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
refine_1 : ∀ (x : K) (h : IsIntegral ℤ x), Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
⊢ IsIntegralClosure ↥ℤ[ζ] ℤ K
have refine_2 : ∀ (x : K), (∃ (y : ↥ℤ[ζ]), (algebraMap (↥ℤ[ζ]) K : (a : ↥ℤ[ζ]) → K) y = x) → IsIntegral ℤ x
Tactic: refine ⟨Subtype.val_injective, @fun x => ⟨fun h => ⟨⟨x, ?_⟩, rfl⟩, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have hint : IsIntegral ℤ B.gen
Tactic: have hint : IsIntegral ℤ B.gen := (hζ.isIntegral (NeZero.pos _)).sub isIntegral_one
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have H : Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
  (Algebra.discr (ι := Fin B.dim) ℚ (B := K) (⇑B.basis : (a : Fin B.dim) → K) • x)
Tactic: have H := discr_mul_isIntegral_mem_adjoin ℚ hint h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (Algebra.discr (ι := Fin B.dim) ℚ (B := K) (⇑B.basis : (a : Fin B.dim) → K) • x)
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have refine_1 : ∀ (u : ℤˣ) (n : ℕ)
  (hun :
    Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
        (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
          (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
      (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n),
  Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
Tactic: obtain ⟨u, n, hun⟩ := discr_prime_pow_eq_unit_mul_pow' hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (Algebra.discr (ι := Fin B.dim) ℚ (B := K) (⇑B.basis : (a : Fin B.dim) → K) • x)
u : ℤˣ
n : ℕ
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have H₁ : Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)
Tactic: rw [hun] at H
Cleared hypotheses: H, hun
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
u : ℤˣ
n : ℕ
H : Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have H₁ : Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (u.inv • ((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)
Tactic: replace H := Subalgebra.smul_mem _ H u.inv
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
u : ℤˣ
n : ℕ
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H : Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (u.inv • ((↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n) • x)
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have H₁ : Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
Tactic: rw [← smul_assoc, ← smul_mul_assoc, Units.inv_eq_val_inv, zsmul_eq_mul, ← Int.cast_mul,
    Units.inv_mul, Int.cast_one, one_mul, smul_def, map_pow] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
u : ℤˣ
n : ℕ
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have refine_1 : ∀ [hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K] (hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)),
  let B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ;
  ∀ (hint : IsIntegral ℤ B.gen)
    (hun :
      Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
          (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
            (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
        (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n)
    (H :
      Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
        (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)),
    Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
Tactic: cases k
Cleared hypotheses: k, hcycl, hζ, B, hint, this, hun, H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p k : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
x : K
h : IsIntegral ℤ x
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
u : ℤˣ
n : ℕ
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
refine_1 :
  ∀ [hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K] (hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)),
    let B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ;
    ∀ (hint : IsIntegral ℤ B.gen)
      (hun :
        Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
            (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
              (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
          (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n)
      (H :
        Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
          (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)),
      Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have refine_1₁ : ∀ (n_1 : ℕ) [hcycl : IsCyclotomicExtension {p ^ (n_1 + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (n_1 + 1))),
  let B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ;
  ∀ (hint : IsIntegral ℤ B.gen)
    (hun :
      Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
          (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
            (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
        (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n)
    (H :
      Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
        (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)),
    Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
Tactic: cases k
Cleared hypotheses: k, hcycl, hζ, B, hint, this, hun, H
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have this₁ : IsCyclotomicExtension {1} ℚ K
Tactic: haveI : IsCyclotomicExtension {1} ℚ K := by simpa using hcycl
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this_1 : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
this : IsCyclotomicExtension {1} ℚ K
⊢ Membership.mem (γ := Subalgebra ℚ K) ⊥ x
have rw : Membership.mem (γ := Subalgebra ℚ K) ⊤ x
Tactic: rw [singleton_one ℚ K]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this_1 : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
this : IsCyclotomicExtension {1} ℚ K
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have this₁ : Membership.mem (γ := Subalgebra ℚ K) ⊥ x
Tactic: have : x ∈ (⊥ : Subalgebra ℚ K) := by
      rw [singleton_one ℚ K]
      exact mem_top
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (goal)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
x : K
h : IsIntegral ℤ x
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this_1 : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen] (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n * x)
this_2 : IsCyclotomicExtension {1} ℚ K
this : Membership.mem (γ := Subalgebra ℚ K) ⊥ x
⊢ Membership.mem (γ := Subalgebra ℤ K) ℤ[ζ] x
have refine_1 : ∀ (y : ℚ) (h : IsIntegral ℤ (A := K) ((algebraMap ℚ K : (a : ℚ) → K) y : K))
  (H :
    Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
      (HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n)
        ((algebraMap ℚ K : (a : ℚ) → K) y : K)))
  (this : Membership.mem (α := K) (γ := Subalgebra ℚ K) ⊥ ((algebraMap ℚ K : (a : ℚ) → K) y : K)),
  Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)
Tactic: obtain ⟨y, rfl⟩ := mem_bot.1 this
Cleared hypotheses: x, h, H, this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Cyclotomic.Basic (hypothesis)
Goal:
p : ℕ
K : Type u
inst : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst_1 : CharZero K
u : ℤˣ
n : ℕ
hcycl : IsCyclotomicExtension {HPow.hPow (β := ℕ) p 0} ℚ K
hζ : IsPrimitiveRoot ζ (HPow.hPow (β := ℕ) p 0)
B : PowerBasis ℚ K := IsPrimitiveRoot.subOnePowerBasis ℚ hζ
hint : IsIntegral ℤ B.gen
this_1 : FiniteDimensional ℚ K := ⋯
hun :
  Algebra.discr (ι := Fin (PowerBasis.dim (IsPrimitiveRoot.subOnePowerBasis ℚ hζ))) ℚ (B := K)
      (⇑(PowerBasis.basis (IsPrimitiveRoot.subOnePowerBasis ℚ hζ)) :
        (a : Fin (IsPrimitiveRoot.subOnePowerBasis ℚ hζ).dim) → K) =
    (↑(↑u : ℤ) : ℚ) * HPow.hPow (α := ℚ) (↑p : ℚ) n
this_2 : IsCyclotomicExtension {1} ℚ K
y : ℚ
h : IsIntegral ℤ (A := K) ((algebraMap ℚ K : (a : ℚ) → K) y : K)
H :
  Membership.mem (γ := Subalgebra ℤ K) ℤ[B.gen]
    (HMul.hMul (β := K) (HPow.hPow (α := K) ((algebraMap ℚ K : (a : ℚ) → K) (↑p : ℚ) : K) n)
      ((algebraMap ℚ K : (a : ℚ) → K) y : K))
this : Membership.mem (α := K) (γ := Subalgebra ℚ K) ⊥ ((algebraMap ℚ K : (a : ℚ) → K) y : K)
⊢ Membership.mem (α := K) (γ := Subalgebra ℤ K) ℤ[ζ] ((algebraMap ℚ K : (a : ℚ) → K) y : K)
have h₁ : IsIntegral ℤ y
Tactic: replace h := (isIntegral_algebraMap_iff (algebraMap ℚ K).injective).1 h
Cleared hypotheses: h