awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
⊢ Eq (α := ℝ)
    (∏ᶠ (w : FinitePlace K),
      (w : (a : K) → ℝ)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)))
    (↑|(Algebra.norm ℚ : (a : K) → ℚ)
              (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))|⁻¹ :
      ℝ)
have simp_rw : HDiv.hDiv (α := ℝ) |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ)|⁻¹ |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ)|⁻¹ =
  |(↑((Algebra.norm ℚ : (a : K) → ℚ)
            (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
        ℝ)|⁻¹
Tactic: simp_rw [map_div₀, Rat.cast_inv, Rat.cast_abs,
    finprod_div_distrib (hasFiniteMulSupport_int ha) (hasFiniteMulSupport_int hb),
    prod_eq_inv_abs_norm_int ha, prod_eq_inv_abs_norm_int hb]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
⊢ HDiv.hDiv (α := ℝ) |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ)|⁻¹ |(↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ)|⁻¹ =
    |(↑((Algebra.norm ℚ : (a : K) → ℚ)
              (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
                ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
          ℝ)|⁻¹
have rw : |HDiv.hDiv (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ)| =
  |(↑((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
      ℝ)|
Tactic: rw [← inv_eq_iff_eq_inv, inv_inv_div_inv, ← abs_div]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
⊢ |HDiv.hDiv (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ)| =
    |(↑((Algebra.norm ℚ : (a : K) → ℚ)
            (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
        ℝ)|
have e_a : HDiv.hDiv (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) =
  (↑((Algebra.norm ℚ : (a : K) → ℚ)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
    ℝ)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
⊢ HDiv.hDiv (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) =
    (↑((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
      ℝ)
have hb₀ : Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0
Tactic: have hb₀ : ((Algebra.norm ℤ) b : ℝ) ≠ 0 := by simp [hb]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0
⊢ HDiv.hDiv (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) =
    (↑((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
      ℝ)
have e_a : HMul.hMul (α := ℝ)
    (↑((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
      ℝ)
    (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) =
  (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ)
Tactic: refine (eq_div_of_mul_eq hb₀ ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0
⊢ HMul.hMul (α := ℝ)
      (↑((Algebra.norm ℚ : (a : K) → ℚ)
            (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K))) :
        ℝ)
      (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) =
    (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℝ)
have e_a : HMul.hMul (α := ℚ) (β := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
      ℚ)
    ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
  (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℚ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0
⊢ HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
    (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℚ)
have e_a : HMul.hMul (α := ℚ) (β := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
      ℚ)
    ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
  (Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)
Tactic: rw [coe_norm_int a, coe_norm_int b, ← map_mul,
    div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0
e_a :
  HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
    (Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)
⊢ HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
    (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℚ)
have e_a₁ : HMul.hMul (α := ℚ) (β := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
      ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ) (↑b : K) : ℚ) =
  (Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)
Tactic: rw [coe_norm_int a, coe_norm_int b, ← map_mul,
    div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0
e_a :
  HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
    (Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)
e_a₁ :
  HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ) (↑b : K) : ℚ) =
    (Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)
⊢ HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
    (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℚ)
have e_a₂ : Eq (α := ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ)
      (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) *
        (↑b : K)) :
    ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ) (↑a : K) : ℚ)
Tactic: rw [coe_norm_int a, coe_norm_int b, ← map_mul,
    div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.ProductFormula (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a b : 𝓞 K
h_x_nezero :
  HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) ≠
    0
hb : b ≠ 0
ha : a ≠ 0
hb₀ : Ne (α := ℝ) (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℝ) 0
e_a :
  HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
    (Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)
e_a₁ :
  HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ) (↑b : K) : ℚ) =
    (Algebra.norm ℚ : (a : K) → ℚ) (↑a : K)
e_a₂ :
  Eq (α := ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ)
        (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K) *
          (↑b : K)) :
      ℚ)
    ((Algebra.norm ℚ : (a : K) → ℚ) (↑a : K) : ℚ)
⊢ HMul.hMul (α := ℚ) (β := ℚ)
      ((Algebra.norm ℚ : (a : K) → ℚ)
          (HDiv.hDiv (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) b : K)) :
        ℚ)
      ((↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) b) : ℚ) : ℚ) =
    (↑((Algebra.norm ℤ : (a : 𝓞 K) → ℤ) a) : ℚ)
have e_a₃ : Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : K) : ℚ)
  ((Algebra.norm ℚ : (a : K) → ℚ) (↑a : K) : ℚ)
Tactic: rw [coe_norm_int a, coe_norm_int b, ← map_mul,
    div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
x : 𝓞 ℚ
⊢ IsUnit x ↔ (↑x : ℚ) = 1 ∨ (↑x : ℚ) = -1
have simp_rw : (↑x : ℚ) = (↑1 : ℚ) ∨ (↑x : ℚ) = (↑(-1) : ℚ) ↔ (↑x : ℚ) = 1 ∨ (↑x : ℚ) = -1
Tactic: simp_rw [(isUnit_map_iff (Rat.ringOfIntegersEquiv : 𝓞 ℚ →+* ℤ) x).symm, Int.isUnit_iff,
    RingEquiv.coe_toRingHom, RingEquiv.map_eq_one_iff, RingEquiv.map_eq_neg_one_iff, ←
    Subtype.coe_injective.eq_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
⊢ IsUnit x ↔ Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| 1
have h : Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| 1 ↔
  IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
Tactic: convert! (RingOfIntegers.isUnit_norm ℚ (F := K)).symm
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
⊢ Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| 1 ↔
    IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
have h : Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| |1| ↔
  IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
Tactic: rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h :
  Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| |1| ↔
    IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
⊢ Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| 1 ↔
    IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
have h₁ : Eq (α := ℚ) (↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ) 1 ∨
    Eq (α := ℚ) (↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ) (-1) ↔
  IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
Tactic: rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
h :
  Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| |1| ↔
    IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
h₁ :
  Eq (α := ℚ) (↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ) 1 ∨
      Eq (α := ℚ) (↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ) (-1) ↔
    IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
⊢ Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| 1 ↔
    IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
have h₂ : IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ) ↔
  IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
Tactic: rw [← abs_one, abs_eq_abs, ← Rat.RingOfIntegers.isUnit_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
n : ℕ
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) =
    HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n
have rw : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K)
  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((↑x : 𝓞 K) ^ n) : K)
Tactic: rw [← map_pow, ← val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
n : ℕ
rw :
  Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((↑x : 𝓞 K) ^ n) : K)
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) =
    HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n
have rw₁ : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K)
  ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K)
Tactic: rw [← map_pow, ← val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) =
    HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n
have change : (MonoidHom.comp (coeHom K) (map (↑(algebraMap (𝓞 K) K) : 𝓞 K →* K)) : (a : (𝓞 K)ˣ) → K) (x ^ n) =
  HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n
Tactic: change ((Units.coeHom K).comp (map (algebraMap (𝓞 K) K))) (x ^ n) = _
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ Eq (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)| : ℚ) (1 : ℚ)
have rw : Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) (↑x : 𝓞 K)) : ℚ)| 1
Tactic: rw [← RingOfIntegers.coe_norm, isUnit_iff_norm.mp x.isUnit]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
rw : Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) (↑x : 𝓞 K)) : ℚ)| 1
⊢ Eq (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)| : ℚ) (1 : ℚ)
have rw₁ : Eq (α := ℚ) 1 1
Tactic: rw [← RingOfIntegers.coe_norm, isUnit_iff_norm.mp x.isUnit]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    ∀ (w : InfinitePlace K),
      Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have rw : IsOfFinOrder x ↔
  ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
Tactic: rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ IsOfFinOrder x ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
have refine : ∀
  (h :
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1),
  ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
Tactic: refine ⟨fun hx φ ↦ (((φ.comp <| algebraMap (𝓞 K) K).toMonoidHom.comp <|
    Units.coeHom _).isOfFinOrder hx).norm_eq_one, fun h ↦ isOfFinOrder_iff_pow_eq_one.2 ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
⊢ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
have obtain : ∀ (n : ℕ) (hn : 0 < n) (hx : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = 1),
  ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
Tactic: obtain ⟨n, hn, hx⟩ := Embeddings.pow_eq_one_of_norm_eq_one K ℂ x.val.isIntegral_coe h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
n : ℕ
hn : 0 < n
hx : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = 1
⊢ x ^ n = 1
have huv : (↑(↑(x ^ n) : 𝓞 K) : K) = (↑(↑1 : 𝓞 K) : 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
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
n : ℕ
hn : 0 < n
hx : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = 1
⊢ (↑(↑(x ^ n) : 𝓞 K) : K) = (↑(↑1 : 𝓞 K) : K)
have huv : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K) ((↑(↑1 : 𝓞 K) : K) : K)
Tactic: rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
n : ℕ
hn : 0 < n
hx : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = 1
huv : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K) ((↑(↑1 : 𝓞 K) : K) : K)
⊢ (↑(↑(x ^ n) : 𝓞 K) : K) = (↑(↑1 : 𝓞 K) : K)
have huv₁ : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = (↑(↑1 : 𝓞 K) : K)
Tactic: rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
n : ℕ
hn : 0 < n
hx : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = 1
huv : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K) ((↑(↑1 : 𝓞 K) : K) : K)
huv₁ : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = (↑(↑1 : 𝓞 K) : K)
⊢ (↑(↑(x ^ n) : 𝓞 K) : K) = (↑(↑1 : 𝓞 K) : K)
have huv₂ : Eq.{u_1 + 1} (α := K) 1 (↑(↑1 : 𝓞 K) : K)
Tactic: rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
n : ℕ
hn : 0 < n
hx : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = 1
huv : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K) ((↑(↑1 : 𝓞 K) : K) : K)
huv₁ : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = (↑(↑1 : 𝓞 K) : K)
huv₂ : Eq.{u_1 + 1} (α := K) 1 (↑(↑1 : 𝓞 K) : K)
⊢ (↑(↑(x ^ n) : 𝓞 K) : K) = (↑(↑1 : 𝓞 K) : K)
have huv₃ : Eq (α := K) (1 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑1 : 𝓞 K) : K)
Tactic: rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.Basic (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h : ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
n : ℕ
hn : 0 < n
hx : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = 1
huv : Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K) ((↑(↑1 : 𝓞 K) : K) : K)
huv₁ : HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n = (↑(↑1 : 𝓞 K) : K)
huv₂ : Eq.{u_1 + 1} (α := K) 1 (↑(↑1 : 𝓞 K) : K)
huv₃ : Eq (α := K) (1 : K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑1 : 𝓞 K) : K)
⊢ (↑(↑(x ^ n) : 𝓞 K) : K) = (↑(↑1 : 𝓞 K) : K)
have huv₄ : Eq.{u_1 + 1} (α := K) 1 1
Tactic: rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]