awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
n : ℕ
inst_2 : NeZero n
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) n
⊢ Function.Injective (α := ↥(rootsOfUnity n (𝓞 K))) (β := (𝓞 K ⧸ I)ˣ)
    (⇑(I.rootsOfUnityMapQuot n) : (a : ↥(rootsOfUnity n (𝓞 K))) → (𝓞 K ⧸ I)ˣ)
have refine : ∀ (x : ↥(rootsOfUnity n (𝓞 K))) (ζ : (𝓞 K)ˣ) (hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) ζ)
  (h :
    Eq (α := (𝓞 K ⧸ I)ˣ)
      ((I.rootsOfUnityMapQuot n : (a : ↥(rootsOfUnity n (𝓞 K))) → (𝓞 K ⧸ I)ˣ)
          (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ) :
        (𝓞 K ⧸ I)ˣ)
      (1 : (𝓞 K ⧸ I)ˣ)),
  Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ = 1
Tactic: refine (injective_iff_map_eq_one _).mpr fun ⟨ζ, hζ⟩ h ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
n : ℕ
inst_2 : NeZero n
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) n
x : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) ζ
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.rootsOfUnityMapQuot n : (a : ↥(rootsOfUnity n (𝓞 K))) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ) :
      (𝓞 K ⧸ I)ˣ)
    (1 : (𝓞 K ⧸ I)ˣ)
⊢ Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ = 1
have obtain : ∀ (t : ℕ) (ht₀ : t ≠ 0) (ht : t ∣ n) (hζ_1 : IsPrimitiveRoot ζ t),
  Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ = 1
Tactic: obtain ⟨t, ht₀, ht, hζ⟩ := isPrimitiveRoot_of_mem_rootsOfUnity hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
n : ℕ
inst_2 : NeZero n
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) n
x : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) ζ
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.rootsOfUnityMapQuot n : (a : ↥(rootsOfUnity n (𝓞 K))) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ_1) :
      (𝓞 K ⧸ I)ˣ)
    (1 : (𝓞 K ⧸ I)ˣ)
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
⊢ Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ_1 = 1
have suffices : ¬2 ≤ t
Tactic: suffices ¬ (2 ≤ t) by
    simpa [show t = 1 by grind] using hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
n : ℕ
inst_2 : NeZero n
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) n
x : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) ζ
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.rootsOfUnityMapQuot n : (a : ↥(rootsOfUnity n (𝓞 K))) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ_1) :
      (𝓞 K ⧸ I)ˣ)
    (1 : (𝓞 K ⧸ I)ˣ)
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := (↑(↑ζ : 𝓞 K) : K)
⊢ False
have hμ : IsPrimitiveRoot μ t
Tactic: have hμ : IsPrimitiveRoot μ t :=
    (IsPrimitiveRoot.coe_units_iff.mpr hζ).map_of_injective RingOfIntegers.coe_injective
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
n : ℕ
inst_2 : NeZero n
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) n
x : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) ζ
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.rootsOfUnityMapQuot n : (a : ↥(rootsOfUnity n (𝓞 K))) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) x) ζ hζ_1) :
      (𝓞 K ⧸ I)ˣ)
    (1 : (𝓞 K ⧸ I)ˣ)
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := (↑(↑ζ : 𝓞 K) : K)
hμ : IsPrimitiveRoot μ t
⊢ False
have rw : ∀ (h : Eq (α := 𝓞 K ⧸ I) ((Quotient.mk I : (a : 𝓞 K) → 𝓞 K ⧸ I) (↑ζ : 𝓞 K) : 𝓞 K ⧸ I) (1 : 𝓞 K ⧸ I)) (t : ℕ)
  (ht₀ : t ≠ 0) (ht : t ∣ n) (hζ : IsPrimitiveRoot ζ t) (ht' : 2 ≤ t),
  let μ := (↑(↑ζ : 𝓞 K) : K);
  ∀ (hμ : IsPrimitiveRoot μ t), False
Tactic: rw [Units.ext_iff, rootsOfUnityMapQuot_apply, Units.val_one] at h
Cleared hypotheses: h, t, ht₀, ht, hζ, ht', μ, hμ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
n : ℕ
inst_2 : NeZero n
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) n
x : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity n (𝓞 K)) ζ
h : Eq (α := 𝓞 K ⧸ I) ((Quotient.mk I : (a : 𝓞 K) → 𝓞 K ⧸ I) (↑ζ : 𝓞 K) : 𝓞 K ⧸ I) (1 : 𝓞 K ⧸ I)
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
ht' : 2 ≤ t
μ : K := (↑(↑ζ : 𝓞 K) : K)
hμ : IsPrimitiveRoot μ t
⊢ False
have refine : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) t
Tactic: refine hμ.not_coprime_norm_of_mk_eq_one hI₁ ht' h ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
n : ℕ
inst_2 : NeZero n
ζ : 𝓞 K
hζ : IsPrimitiveRoot ζ n
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) n
⊢ IsPrimitiveRoot (M := 𝓞 K ⧸ I) ((Ideal.Quotient.mk I : (a : 𝓞 K) → 𝓞 K ⧸ I) ζ : 𝓞 K ⧸ I) n
have h : IsPrimitiveRoot hζ.toRootsOfUnity n
Tactic: have h : IsPrimitiveRoot hζ.toRootsOfUnity n :=
    IsPrimitiveRoot.coe_submonoidClass_iff.mp <| IsPrimitiveRoot.coe_units_iff.mp hζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) (torsionOrder K)
x : (𝓞 K)ˣ
hx : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x
⊢ ∀ ⦃a₂ : ↥(torsion K)⦄,
    Eq (α := (𝓞 K ⧸ I)ˣ)
        ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
            (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx) :
          (𝓞 K ⧸ I)ˣ)
        ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ) a₂ : (𝓞 K ⧸ I)ˣ) →
      Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx = a₂
have this : ∀ (y : (𝓞 K)ˣ) (hy : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) y),
  Eq (α := (𝓞 K ⧸ I)ˣ)
      ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
          (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx) :
        (𝓞 K ⧸ I)ˣ)
      ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
          (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy) :
        (𝓞 K ⧸ I)ˣ) →
    Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx =
      Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy
Tactic: ⟨y, hy⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) (torsionOrder K)
x : (𝓞 K)ˣ
hx : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x
y : (𝓞 K)ˣ
hy : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) y
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx) :
      (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy) :
      (𝓞 K ⧸ I)ˣ)
⊢ Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx =
    Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy
have rw : ∀ (hx_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) x) (y : (𝓞 K)ˣ)
  (hy : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) y)
  (hy_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) y)
  (h :
    Eq (α := (𝓞 K ⧸ I)ˣ)
      ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
          (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx) :
        (𝓞 K ⧸ I)ˣ)
      ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
          (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy) :
        (𝓞 K ⧸ I)ˣ)),
  Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx =
    Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy
Tactic: rw [← rootsOfUnity_eq_torsion] at hx hy
Cleared hypotheses: y, hy, h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
I : Ideal (𝓞 K)
inst_1 : NumberField K
hI₁ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I : ℕ) (1 : ℕ)
hI₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) I) (torsionOrder K)
x : (𝓞 K)ˣ
hx_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x
hx : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) x
y : (𝓞 K)ˣ
hy_1 : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) y
hy : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) y
h :
  Eq (α := (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx_1) :
      (𝓞 K ⧸ I)ˣ)
    ((I.torsionMapQuot : (a : ↥(torsion K)) → (𝓞 K ⧸ I)ˣ)
        (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy_1) :
      (𝓞 K ⧸ I)ˣ)
⊢ Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) x hx_1 =
    Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) y hy_1
have rw : Subtype.mk (p := Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K))) x hx =
  Subtype.mk (p := Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K))) y hy
Tactic: rw [Subtype.mk_eq_mk, ← Subtype.mk_eq_mk (h := hx) (h' := hy)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
⊢ torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
have this : P.IsMaximal
Tactic: have : P.IsMaximal := Ring.DimensionLEOne.maximalOfPrime hP₀ hP₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
this : P.IsMaximal
x : Field (𝓞 K ⧸ P) := Quotient.field P
⊢ torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
have hP₃ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
Tactic: have hP₃ : absNorm P ≠ 1 := absNorm_eq_one_iff.not.mpr <| IsPrime.ne_top hP₁
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
this : P.IsMaximal
x : Field (𝓞 K ⧸ P) := Quotient.field P
hP₃ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
⊢ torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
have h : Nat.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P)ˣ
Tactic: have h := Subgroup.card_dvd_of_injective _ (torsionMapQuot_injective hP₃ hP₂)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
this : P.IsMaximal
x : Field (𝓞 K ⧸ P) := Quotient.field P
hP₃ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
h : Nat.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P)ˣ
⊢ torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
have rwa : ∀ (h : Fintype.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P)ˣ),
  torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
Tactic: rwa [Nat.card_eq_fintype_card, Nat.card_units] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Ideal.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
P : Ideal (𝓞 K)
hP₀ : P ≠ ⊥
hP₁ : P.IsPrime
hP₂ : Nat.Coprime ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P) (torsionOrder K)
this : P.IsMaximal
x : Field (𝓞 K ⧸ P) := Quotient.field P
hP₃ : Ne (α := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
h : Nat.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P)ˣ
rwa :
  ∀ (h : Fintype.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P)ˣ),
    torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
⊢ torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
have rwa₁ : ∀ (h : Fintype.card.{u_1} ↥(torsion K) ∣ Nat.card.{u_1} (𝓞 K ⧸ P) - 1),
  torsionOrder K ∣ HSub.hSub (α := ℕ) (β := ℕ) ((absNorm : (a : Ideal (𝓞 K)) → ℕ) P : ℕ) (1 : ℕ)
Tactic: rwa [Nat.card_eq_fintype_card, Nat.card_units] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (goal)
Goal:
K : Type u_1
inst : Field K
x : K
⊢ Eq (α := mixedEmbedding.mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x : mixedEmbedding.mixedSpace K)
    ((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
        ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x) :
      mixedEmbedding.mixedSpace K)
have fst : ∀ (v : { w : InfinitePlace K // w.IsReal }),
  Eq (α := ℝ) (((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x).1 v)
    (((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
          ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x)).1
      v)
Tactic: ext v
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (goal)
Goal:
K : Type u_1
inst : Field K
x : K
fst :
  ∀ (v : { w : InfinitePlace K // w.IsReal }),
    Eq (α := ℝ) (((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x).1 v)
      (((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
            ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x)).1
        v)
⊢ Eq (α := mixedEmbedding.mixedSpace K)
    ((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x : mixedEmbedding.mixedSpace K)
    ((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
        ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x) :
      mixedEmbedding.mixedSpace K)
have snd : ∀ (v : { w : InfinitePlace K // w.IsComplex }),
  Eq (α := ℂ) (((mixedEmbedding K : (a : K) → mixedEmbedding.mixedSpace K) x).2 v)
    (((ringEquiv_mixedSpace K : (a : InfiniteAdeleRing K) → mixedEmbedding.mixedSpace K)
          ((algebraMap K (InfiniteAdeleRing K) : (a : K) → InfiniteAdeleRing K) x)).2
      v)
Tactic: ext v
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfiniteAdeleRing K
hx : ¬IsUnit x
⊢ ‖x‖ = 0
have hx₁ : ∃ (x_1 : InfinitePlace K), ¬IsUnit (x x_1)
Tactic: rw [Pi.isUnit_iff, not_forall] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfiniteAdeleRing (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : InfiniteAdeleRing K
hx : ∃ (x_1 : InfinitePlace K), ¬IsUnit (x x_1)
⊢ ‖x‖ = 0
have obtain : ∀ (v : InfinitePlace K) (hv : ¬IsUnit (x v)), ‖x‖ = 0
Tactic: obtain ⟨v, hv⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ mk (ComplexEmbedding.conjugate φ) = mk φ
have refine : ∀ (x : K), Eq (α := ℝ) ((mk (ComplexEmbedding.conjugate φ) : (a : K) → ℝ) x : ℝ) ((mk φ : (a : K) → ℝ) x : ℝ)
Tactic: refine DFunLike.ext _ _ (fun x => ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
⊢ Eq (α := ℝ) ((mk (ComplexEmbedding.conjugate φ) : (a : K) → ℝ) x : ℝ) ((mk φ : (a : K) → ℝ) x : ℝ)
have rw : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = (mk φ : (a : K) → ℝ) x
Tactic: rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.norm_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
rw : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = (mk φ : (a : K) → ℝ) x
⊢ Eq (α := ℝ) ((mk (ComplexEmbedding.conjugate φ) : (a : K) → ℝ) x : ℝ) ((mk φ : (a : K) → ℝ) x : ℝ)
have rw₁ : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
Tactic: rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.norm_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
rw : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = (mk φ : (a : K) → ℝ) x
rw₁ : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
⊢ Eq (α := ℝ) ((mk (ComplexEmbedding.conjugate φ) : (a : K) → ℝ) x : ℝ) ((mk φ : (a : K) → ℝ) x : ℝ)
have rw₂ : norm (E := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
Tactic: rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.norm_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
x : K
rw : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = (mk φ : (a : K) → ℝ) x
rw₁ : norm (E := ℂ) ((ComplexEmbedding.conjugate φ : (a : K) → ℂ) x : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
rw₂ :
  norm (E := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : K) → ℂ) x : ℂ) : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
⊢ Eq (α := ℝ) ((mk (ComplexEmbedding.conjugate φ) : (a : K) → ℝ) x : ℝ) ((mk φ : (a : K) → ℝ) x : ℝ)
have rw₃ : norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ) = norm (E := ℂ) ((φ : (a : K) → ℂ) x : ℂ)
Tactic: rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.norm_conj]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
w : InfinitePlace K
x : K
⊢ norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) = (w : (a : K) → ℝ) x
have nth_rewrite : norm (E := ℂ) ((w.embedding : (a : K) → ℂ) x : ℂ) = (mk w.embedding : (a : K) → ℝ) x
Tactic: nth_rewrite 2 [← mk_embedding w]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
⊢ v₁ = v₂
have rw : mk v₁.embedding = v₂
Tactic: rw [← mk_embedding v₁, h, mk_conjugate_eq, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
rw : mk v₁.embedding = v₂
⊢ v₁ = v₂
have rw₁ : mk (ComplexEmbedding.conjugate v₂.embedding) = v₂
Tactic: rw [← mk_embedding v₁, h, mk_conjugate_eq, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
rw : mk v₁.embedding = v₂
rw₁ : mk (ComplexEmbedding.conjugate v₂.embedding) = v₂
⊢ v₁ = v₂
have rw₂ : mk v₂.embedding = v₂
Tactic: rw [← mk_embedding v₁, h, mk_conjugate_eq, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
rw : mk v₁.embedding = v₂
rw₁ : mk (ComplexEmbedding.conjugate v₂.embedding) = v₂
rw₂ : mk v₂.embedding = v₂
⊢ v₁ = v₂
have rw₃ : v₂ = v₂
Tactic: rw [← mk_embedding v₁, h, mk_conjugate_eq, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
have rw : φ = (mk φ).embedding ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
Tactic: rw [@eq_comm _ _ φ, @eq_comm _ _ (ComplexEmbedding.conjugate φ), ← mk_eq_iff, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
rw : φ = (mk φ).embedding ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
⊢ (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
have rw₁ : φ = (mk φ).embedding ∨ ComplexEmbedding.conjugate φ = (mk φ).embedding
Tactic: rw [@eq_comm _ _ φ, @eq_comm _ _ (ComplexEmbedding.conjugate φ), ← mk_eq_iff, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
rw : φ = (mk φ).embedding ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
rw₁ : φ = (mk φ).embedding ∨ ComplexEmbedding.conjugate φ = (mk φ).embedding
⊢ (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
have rw₂ : mk φ = mk (mk φ).embedding
Tactic: rw [@eq_comm _ _ φ, @eq_comm _ _ (ComplexEmbedding.conjugate φ), ← mk_eq_iff, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (goal)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
rw : φ = (mk φ).embedding ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
rw₁ : φ = (mk φ).embedding ∨ ComplexEmbedding.conjugate φ = (mk φ).embedding
rw₂ : mk φ = mk (mk φ).embedding
⊢ (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
have rw₃ : mk φ = mk φ
Tactic: rw [@eq_comm _ _ φ, @eq_comm _ _ (ComplexEmbedding.conjugate φ), ← mk_eq_iff, mk_embedding]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.InfinitePlace.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ (mk φ).embedding = φ
have this : (mk φ).embedding = φ ∨ (mk φ).embedding = ComplexEmbedding.conjugate φ
Tactic: have := embedding_mk_eq φ