awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Fintype ↥(torsion K)
have refine : (↑(torsion K) : Set (𝓞 K)ˣ).Finite
Tactic: refine @Fintype.ofFinite _ (Set.finite_coe_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (↑(torsion K) : Set (𝓞 K)ˣ).Finite
have refine : Set.Finite (α := K)
  ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ))
Tactic: refine Set.Finite.of_finite_image ?_ (coe_injective K).injOn
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Set.Finite (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ))
have refine_1 : ∀ (a : K),
  Membership.mem (γ := Set K)
      ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ)) a →
    ∀ (u : (𝓞 K)ˣ) (h_tors : u ∈ (↑(torsion K) : Set (𝓞 K)ˣ))
      (h_ua : (fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u = a), IsIntegral ℤ a
Tactic: refine (Embeddings.finite_of_norm_le K ℂ 1).subset
    (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 :
  ∀ (a : K),
    Membership.mem (γ := Set K)
        ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ)) a →
      ∀ (u : (𝓞 K)ˣ) (h_tors : u ∈ (↑(torsion K) : Set (𝓞 K)ˣ))
        (h_ua : (fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u = a), IsIntegral ℤ a
⊢ Set.Finite (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ))
have refine_2 : ∀ (a : K),
  Membership.mem (γ := Set K)
      ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ)) a →
    ∀ (u : (𝓞 K)ˣ) (h_tors : u ∈ (↑(torsion K) : Set (𝓞 K)ˣ))
      (h_ua : (fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u = a) (φ : K →+* ℂ),
      norm (E := ℂ) ((φ : (a : K) → ℂ) a : ℂ) ≤ 1
Tactic: refine (Embeddings.finite_of_norm_le K ℂ 1).subset
    (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
h :
  Membership.mem (γ := Set K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ)) a
u : (𝓞 K)ˣ
h_tors : u ∈ (↑(torsion K) : Set (𝓞 K)ˣ)
h_ua : (fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u = a
⊢ IsIntegral ℤ a
have refine_1 : IsIntegral.{0, u_1} ℤ (A := K) ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u)
Tactic: rw [← h_ua]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a : K
h :
  Membership.mem (γ := Set K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ)) a
u : (𝓞 K)ˣ
h_tors : u ∈ (↑(torsion K) : Set (𝓞 K)ˣ)
h_ua : (fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u = a
φ : K →+* ℂ
⊢ norm (E := ℂ) ((φ : (a : K) → ℂ) a : ℂ) ≤ 1
have refine_2 : norm (E := ℂ) ((φ : (a : K) → ℂ) ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u) : ℂ) ≤ 1
Tactic: rw [← h_ua]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ = 1
⊢ ζ ^ (↑k : ℕ) = 1
have rw : HPow.hPow (α := (𝓞 K)ˣ) 1 (↑k : ℕ) = 1
Tactic: rw [h, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ = 1
rw : HPow.hPow (α := (𝓞 K)ˣ) 1 (↑k : ℕ) = 1
⊢ ζ ^ (↑k : ℕ) = 1
have rw₁ : Eq.{u_1 + 1} (α := (𝓞 K)ˣ) 1 1
Tactic: rw [h, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
⊢ ζ ^ (↑k : ℕ) = 1 ↔ ζ = 1
have refine : ∀ (h : ζ ^ (↑k : ℕ) = 1), ζ = 1
Tactic: refine ⟨fun h => ?_, fun h => by rw [h, one_pow]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ ζ = 1
have refine_1 : orderOf ζ ∣ (↑k : ℕ)
Tactic: refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
refine_1 : orderOf ζ ∣ (↑k : ℕ)
⊢ ζ = 1
have refine_2 : orderOf ζ ∣ torsionOrder K
Tactic: refine orderOf_eq_one_iff.mp (Nat.eq_one_of_dvd_coprimes hc ?_ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
have rw : ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1
Tactic: rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
⊢ orderOf ζ ∣ torsionOrder K
have hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
Tactic: have hζ : ζ ∈ torsion K := by
      rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
      exact ⟨k, k.prop, h⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
k : ℕ+
hc : (↑k : ℕ).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ (↑k : ℕ) = 1
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ orderOf ζ ∣ torsionOrder K
have refine_2 : orderOf (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ hζ) ∣ torsionOrder K
Tactic: rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) (torsion K)
have h : ∀ (ζ : (𝓞 K)ˣ),
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (rootsOfUnity (torsionOrder K) (𝓞 K)) ζ ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
Tactic: ext ζ
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
⊢ ζ ^ torsionOrder K = 1 ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ
have h : ∀ (h : ζ ^ torsionOrder K = 1), Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
h : ∀ (h : ζ ^ torsionOrder K = 1), Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ
⊢ ζ ^ torsionOrder K = 1 ↔ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ
have h₁ : ∀ (h : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ), ζ ^ torsionOrder K = 1
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (CommGroup.torsion (𝓞 K)ˣ) ζ
have h₁ : ∃ (n : ℕ), 0 < n ∧ ζ ^ n = 1
Tactic: rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) = rootsOfUnity (torsionOrder K) ℂ
have hle : Subgroup.map (Units.complexEmbedding φ) (torsion K) ≤ rootsOfUnity (torsionOrder K) ℂ
Tactic: apply Subgroup.eq_of_le_of_card_ge
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
hle : Subgroup.map (Units.complexEmbedding φ) (torsion K) ≤ rootsOfUnity (torsionOrder K) ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) = rootsOfUnity (torsionOrder K) ℂ
have hcard : Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
Tactic: apply Subgroup.eq_of_le_of_card_ge
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
⊢ Subgroup.map (Units.complexEmbedding φ) (torsion K) ≤ rootsOfUnity (torsionOrder K) ℂ
have hle : Subgroup.map (Units.complexEmbedding φ) (rootsOfUnity (torsionOrder K) (𝓞 K)) ≤ rootsOfUnity (torsionOrder K) ℂ
Tactic: rw [← rootsOfUnity_eq_torsion]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  MulEquiv.toEquiv (MulEquiv.symm (Subgroup.equivMapOfInjective (torsion K) (Units.complexEmbedding φ) ⋯))
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
have hcard : Fintype.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
Tactic: rw [Nat.card_eq_fintype_card, Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder,
      Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  MulEquiv.toEquiv (MulEquiv.symm (Subgroup.equivMapOfInjective (torsion K) (Units.complexEmbedding φ) ⋯))
hcard :
  Fintype.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
have hcard₁ : torsionOrder K ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
Tactic: rw [Nat.card_eq_fintype_card, Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder,
      Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  MulEquiv.toEquiv (MulEquiv.symm (Subgroup.equivMapOfInjective (torsion K) (Units.complexEmbedding φ) ⋯))
hcard :
  Fintype.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
hcard₁ : torsionOrder K ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
have hcard₂ : torsionOrder K ≤ Nat.card.{u_1} ↥(torsion K)
Tactic: rw [Nat.card_eq_fintype_card, Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder,
      Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  MulEquiv.toEquiv (MulEquiv.symm (Subgroup.equivMapOfInjective (torsion K) (Units.complexEmbedding φ) ⋯))
hcard :
  Fintype.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
hcard₁ : torsionOrder K ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
hcard₂ : torsionOrder K ≤ Nat.card.{u_1} ↥(torsion K)
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
have hcard₃ : Fintype.card.{u_1} ↥(torsion K) ≤ Nat.card.{u_1} ↥(torsion K)
Tactic: rw [Nat.card_eq_fintype_card, Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder,
      Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  MulEquiv.toEquiv (MulEquiv.symm (Subgroup.equivMapOfInjective (torsion K) (Units.complexEmbedding φ) ⋯))
hcard :
  Fintype.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
hcard₁ : torsionOrder K ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
hcard₂ : torsionOrder K ≤ Nat.card.{u_1} ↥(torsion K)
hcard₃ : Fintype.card.{u_1} ↥(torsion K) ≤ Nat.card.{u_1} ↥(torsion K)
⊢ Nat.card ↥(rootsOfUnity (torsionOrder K) ℂ) ≤ Nat.card ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K))
have hcard₄ : Fintype.card.{u_1} ↥(torsion K) ≤ Fintype.card.{u_1} ↥(torsion K)
Tactic: rw [Nat.card_eq_fintype_card, Complex.card_rootsOfUnity, Nat.card_congr e, torsionOrder,
      Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
this :
  orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
⊢ Even (torsionOrder K)
have rw : orderOf.{u_1} (G := ↥(torsion K))
    (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) sorry) ∣
  torsionOrder K
Tactic: rw [even_iff_two_dvd, ← this]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Even (torsionOrder K)
have suffices : orderOf.{u_1} (G := ↥(torsion K))
    (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) sorry) =
  2
Tactic: suffices orderOf (⟨-1, neg_one_mem_torsion⟩ : torsion K) = 2 by
    rw [even_iff_two_dvd, ← this]
    exact orderOf_dvd_card
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
have rw : orderOf.{u_1} (G := (𝓞 K)ˣ)
    (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) sorry) : (𝓞 K)ˣ) =
  2
Tactic: rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one,
    ringChar.eq_zero, if_neg (by decide)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  orderOf.{u_1} (G := (𝓞 K)ˣ)
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) =
    2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
have rw₁ : orderOf.{u_1} (G := 𝓞 K)
    (↑(↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) sorry) : (𝓞 K)ˣ) :
      𝓞 K) =
  2
Tactic: rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one,
    ringChar.eq_zero, if_neg (by decide)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  orderOf.{u_1} (G := (𝓞 K)ˣ)
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) =
    2
rw₁ :
  orderOf.{u_1} (G := 𝓞 K)
      (↑(↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) :
        𝓞 K) =
    2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
have rw₂ : orderOf.{u_1} (G := 𝓞 K) (-(↑1 : 𝓞 K)) = 2
Tactic: rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one,
    ringChar.eq_zero, if_neg (by decide)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  orderOf.{u_1} (G := (𝓞 K)ˣ)
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) =
    2
rw₁ :
  orderOf.{u_1} (G := 𝓞 K)
      (↑(↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) :
        𝓞 K) =
    2
rw₂ : orderOf.{u_1} (G := 𝓞 K) (-(↑1 : 𝓞 K)) = 2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
have rw₃ : orderOf.{u_1} (G := 𝓞 K) (-1) = 2
Tactic: rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one,
    ringChar.eq_zero, if_neg (by decide)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  orderOf.{u_1} (G := (𝓞 K)ˣ)
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) =
    2
rw₁ :
  orderOf.{u_1} (G := 𝓞 K)
      (↑(↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) :
        𝓞 K) =
    2
rw₂ : orderOf.{u_1} (G := 𝓞 K) (-(↑1 : 𝓞 K)) = 2
rw₃ : orderOf.{u_1} (G := 𝓞 K) (-1) = 2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
have rw₄ : Eq (α := ℕ) (if ringChar.{u_1} (𝓞 K) = 2 then 1 else 2) 2
Tactic: rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one,
    ringChar.eq_zero, if_neg (by decide)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  orderOf.{u_1} (G := (𝓞 K)ˣ)
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) =
    2
rw₁ :
  orderOf.{u_1} (G := 𝓞 K)
      (↑(↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) :
        𝓞 K) =
    2
rw₂ : orderOf.{u_1} (G := 𝓞 K) (-(↑1 : 𝓞 K)) = 2
rw₃ : orderOf.{u_1} (G := 𝓞 K) (-1) = 2
rw₄ : Eq (α := ℕ) (if ringChar.{u_1} (𝓞 K) = 2 then 1 else 2) 2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
have rw₅ : Eq (α := ℕ) (if Eq (α := ℕ) 0 2 then 1 else 2) 2
Tactic: rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one,
    ringChar.eq_zero, if_neg (by decide)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  orderOf.{u_1} (G := (𝓞 K)ˣ)
      (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) =
    2
rw₁ :
  orderOf.{u_1} (G := 𝓞 K)
      (↑(↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) : (𝓞 K)ˣ) :
        𝓞 K) =
    2
rw₂ : orderOf.{u_1} (G := 𝓞 K) (-(↑1 : 𝓞 K)) = 2
rw₃ : orderOf.{u_1} (G := 𝓞 K) (-1) = 2
rw₄ : Eq (α := ℕ) (if ringChar.{u_1} (𝓞 K) = 2 then 1 else 2) 2
rw₅ : Eq (α := ℕ) (if Eq (α := ℕ) 0 2 then 1 else 2) 2
⊢ orderOf.{u_1} (G := ↥(torsion K))
      (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯) =
    2
have rw₆ : Eq (α := ℕ) 2 2
Tactic: rw [← Subgroup.orderOf_coe, ← orderOf_units, Units.val_neg, val_one, orderOf_neg_one,
    ringChar.eq_zero, if_neg (by decide)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have pos : ∀ (hc : 2 < orderOf (↑x : (𝓞 K)ˣ)), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
Tactic: by_cases! hc : 2 < orderOf (x : (𝓞 K)ˣ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
pos : ∀ (hc : 2 < orderOf (↑x : (𝓞 K)ˣ)), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have neg : ∀ (hc : orderOf (↑x : (𝓞 K)ˣ) ≤ 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
Tactic: by_cases! hc : 2 < orderOf (x : (𝓞 K)ˣ)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : 2 < orderOf (↑x : (𝓞 K)ˣ)
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have hc₁ : 2 < orderOf (↑(↑(↑x : (𝓞 K)ˣ) : 𝓞 K) : K)
Tactic: rw [← orderOf_units, ← orderOf_submonoid] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : 2 < orderOf (↑(↑(↑x : (𝓞 K)ˣ) : 𝓞 K) : K)
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have linarith : -1 + HSub.hSub (α := ℤ) (↑(nrRealPlaces K) : ℤ) 0 + (HAdd.hAdd (α := ℤ) 0 1 - (↑(nrRealPlaces K) : ℤ)) = 0
Tactic: linarith [IsPrimitiveRoot.nrRealPlaces_eq_zero_of_two_lt hc (IsPrimitiveRoot.orderOf (x.1 : K)),
        NumberField.InfinitePlace.nrRealPlaces_pos_of_odd_finrank h]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : orderOf (↑x : (𝓞 K)ˣ) ≤ 2
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have neg : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 0) (hc : LE.le (α := ℕ) 0 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
Tactic: interval_cases hi : orderOf (x : (𝓞 K)ˣ)
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : orderOf (↑x : (𝓞 K)ˣ) ≤ 2
neg : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 0) (hc : LE.le (α := ℕ) 0 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have neg₁ : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 1) (hc : LE.le (α := ℕ) 1 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
Tactic: interval_cases hi : orderOf (x : (𝓞 K)ˣ)
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : orderOf (↑x : (𝓞 K)ˣ) ≤ 2
neg : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 0) (hc : LE.le (α := ℕ) 0 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
neg₁ : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 1) (hc : LE.le (α := ℕ) 1 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have neg₂ : ∀ (hi : orderOf (↑x : (𝓞 K)ˣ) = 2) (hc : LE.le (α := ℕ) 2 2), (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
Tactic: interval_cases hi : orderOf (x : (𝓞 K)ˣ)
Cleared hypotheses: hc