awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
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))) :
      ℝ)

Tactic:
(eq_div_of_mul_eq hb₀ ?_).symm

Premises used: eq_div_of_mul_eq, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
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) : ℝ)
⊢ 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:
refine (eq_div_of_mul_eq hb₀ ?_).symm

Premises used: eq_div_of_mul_eq, Eq.symm
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
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) : ℚ)
⊢ 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
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
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) : ℚ)
e_a₃ e_a₄ :
  Eq (α := ℚ) ((Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) a : 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) : ℚ)

Tactic:
rw [coe_norm_int a, coe_norm_int b, ← map_mul,
    div_mul_cancel₀ _ (RingOfIntegers.coe_ne_zero_iff.mpr hb)]

Premises used: Iff.mpr, div_mul_cancel₀, Algebra.coe_norm_int, map_mul, NumberField.RingOfIntegers.coe_ne_zero_iff
-- Module: Mathlib.NumberTheory.NumberField.ProductFormula
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : K
h_x_nezero : x ≠ 0
⊢ HMul.hMul (α := ℝ) (∏ w : InfinitePlace K, HPow.hPow (α := ℝ) ((w : (a : K) → ℝ) x : ℝ) w.mult)
      (∏ᶠ (w : FinitePlace K), (w : (a : K) → ℝ) x) =
    1

Tactic:
simp [prod_eq_inv_abs_norm, InfinitePlace.prod_eq_abs_norm, h_x_nezero]

Premises used: NumberField.FinitePlace.prod_eq_inv_abs_norm, NumberField.InfinitePlace.prod_eq_abs_norm
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
x : 𝓞 ℚ
simp_rw : (↑x : ℚ) = (↑1 : ℚ) ∨ (↑x : ℚ) = (↑(-1) : ℚ) ↔ (↑x : ℚ) = 1 ∨ (↑x : ℚ) = -1
⊢ IsUnit x ↔ (↑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]

Premises used: Rat.ringOfIntegersEquiv, Function.Injective.eq_iff, RingEquiv.map_eq_one_iff, Subtype.coe_injective, isUnit_map_iff, RingHomClass.toRingHom, RingEquiv.map_eq_neg_one_iff, Int.isUnit_iff, RingEquiv.coe_toRingHom, Iff.symm
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
x : 𝓞 ℚ
⊢ (↑x : ℚ) = (↑1 : ℚ) ∨ (↑x : ℚ) = (↑(-1) : ℚ) ↔ (↑x : ℚ) = 1 ∨ (↑x : ℚ) = -1

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : 𝓞 K
⊢ IsUnit x ↔ IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)

Tactic:
(RingOfIntegers.isUnit_norm ℚ (F := K)).symm

Premises used: Rat, RingOfIntegers.isUnit_norm, Iff.symm
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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 : 𝓞 ℚ)
⊢ IsUnit x ↔ Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x) : ℚ)| 1

Tactic:
convert! (RingOfIntegers.isUnit_norm ℚ (F := K)).symm

Premises used: Rat, RingOfIntegers.isUnit_norm, Iff.symm
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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 : 𝓞 ℚ)
h₂ h₃ :
  IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ) ↔
    IsUnit (M := 𝓞 ℚ) (((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) x : 𝓞 ℚ)
⊢ 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]

Premises used: Rat.RingOfIntegers.isUnit_iff, abs_one, abs_eq_abs
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Function.Injective (β := K) fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)

Tactic:
RingOfIntegers.coe_injective.comp Units.val_injective

Premises used: NumberField.RingOfIntegers.coe_injective, Function.Injective.comp, Units.val_injective
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
u : (𝓞 K)ˣ
⊢ (↑(↑u : 𝓞 K) : K) = (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
x y : (𝓞 K)ˣ
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x * y) : 𝓞 K) =
    HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑y : 𝓞 K) : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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)
rw₁ rw₂ :
  Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K)
    ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) : K)
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) =
    HPow.hPow (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) n

Tactic:
rw [← map_pow, ← val_pow_eq_pow_val]

Premises used: map_pow, Units.val_pow_eq_pow_val
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
n : ℤ
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
⊢ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x ^ n) : 𝓞 K) =
    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) = _

Premises used: Units.coeHom, MonoidHom.comp, HPow.hPow, DFunLike.coe, Units.map
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ (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:
map_zpow _ x n

Premises used: map_zpow
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ (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:
exact map_zpow _ x n

Premises used: map_zpow
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑1 : 𝓞 K) : K) (1 : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Eq (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(-1) : 𝓞 K) : K) (-1 : K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
⊢ Ne (α := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) (0 : K)

Tactic:
Subtype.coe_injective.ne_iff.mpr (_root_.Units.ne_zero x)

Premises used: Iff.mpr, Units.ne_zero, Function.Injective.ne_iff, Subtype.coe_injective
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
u : (𝓞 K)ˣ
⊢ Eq (α := ℂ) ((↑((Units.complexEmbedding φ : (a : (𝓞 K)ˣ) → ℂˣ) u) : ℂ) : ℂ)
    ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K) : ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
⊢ Function.Injective (α := (𝓞 K)ˣ) (β := ℂˣ) (⇑(Units.complexEmbedding φ) : (a : (𝓞 K)ˣ) → ℂˣ)

Tactic:
(map_injective φ.injective).comp (map_injective RingOfIntegers.coe_injective)

Premises used: Units.map_injective, RingHom.injective, NumberField.RingOfIntegers.coe_injective, Function.Injective.comp
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
φ : K →+* ℂ
u v : (𝓞 K)ˣ
⊢ Eq (α := ℂˣ) ((Units.complexEmbedding φ : (a : (𝓞 K)ˣ) → ℂˣ) u : ℂˣ)
      ((Units.complexEmbedding φ : (a : (𝓞 K)ˣ) → ℂˣ) v : ℂˣ) ↔
    u = v

Tactic:
(Units.complexEmbedding_injective φ).eq_iff

Premises used: Function.Injective.eq_iff, NumberField.Units.complexEmbedding_injective
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
rw : Eq (α := ℚ) |(↑(((RingOfIntegers.norm ℚ : 𝓞 K →* 𝓞 ℚ) : (a : 𝓞 K) → 𝓞 ℚ) (↑x : 𝓞 K)) : ℚ)| 1
rw₁ rw₂ : Eq (α := ℚ) 1 1
⊢ Eq (α := ℚ) (|(Algebra.norm ℚ : (a : K) → ℚ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)| : ℚ) (1 : ℚ)

Tactic:
rw [← RingOfIntegers.coe_norm, isUnit_iff_norm.mp x.isUnit]

Premises used: RingOfIntegers.coe_norm, Iff.mp, NumberField.isUnit_iff_norm, Units.isUnit
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ LT.lt (α := ℝ) (0 : ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ)

Tactic:
pos_iff.mpr (coe_ne_zero x)

Premises used: Iff.mpr, NumberField.InfinitePlace.pos_iff, NumberField.Units.coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ Eq (α := ℝ)
    (∑ w : InfinitePlace K,
      (↑w.mult : ℝ) * Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)))
    0

Tactic:
simpa [Units.norm, Real.log_prod, Real.log_pow] using
    congr_arg Real.log (prod_eq_abs_norm (x : K))

Premises used: Units.val, Real.log_prod, Algebra.algebraMap, NumberField.Units.norm, Real.log, congr_arg, Real.log_pow, NumberField.InfinitePlace.prod_eq_abs_norm, NumberField.RingOfIntegers, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
⊢ Nonempty.{u_1 + 1} ↥(torsion K)

Tactic:
One.instNonempty

Premises used: One.instNonempty
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
rw :
  IsOfFinOrder x ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    ∀ (w : InfinitePlace K),
      Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)

Tactic:
rw [eq_iff_eq (x : K) 1, torsion, CommGroup.mem_torsion]

Premises used: Units.val, Algebra.algebraMap, NumberField.Units.torsion, NumberField.InfinitePlace.eq_iff_eq, CommGroup.mem_torsion, OfNat.ofNat, NumberField.RingOfIntegers, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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

Tactic:
⟨fun hx φ ↦ (((φ.comp <| algebraMap (𝓞 K) K).toMonoidHom.comp <|
    Units.coeHom _).isOfFinOrder hx).norm_eq_one, fun h ↦ isOfFinOrder_iff_pow_eq_one.2 ?_⟩

Premises used: Iff.mpr, Units.coeHom, Algebra.algebraMap, MonoidHom.isOfFinOrder, MonoidHom.comp, RingHom.comp, Iff.intro, IsOfFinOrder.norm_eq_one, RingHom.toMonoidHom, NumberField.RingOfIntegers, isOfFinOrder_iff_pow_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
refine :
  ∀
    (h :
      ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 1),
    ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
⊢ IsOfFinOrder x ↔
    ∀ (φ : K →+* ℂ), norm (E := ℂ) ((φ : (a : K) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℂ) = 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 ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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
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
⊢ ∃ (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

Premises used: Units.val, NumberField.RingOfIntegers.isIntegral_coe, Complex, NumberField.Embeddings.pow_eq_one_of_norm_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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 : (↑(↑(x ^ n) : 𝓞 K) : K) = (↑(↑1 : 𝓞 K) : K)
⊢ x ^ n = 1

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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)
huv₄ huv₅ : Eq.{u_1 + 1} (α := K) 1 1
⊢ (↑(↑(x ^ n) : 𝓞 K) : K) = (↑(↑1 : 𝓞 K) : K)

Tactic:
rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]

Premises used: NumberField.Units.coe_pow, NumberField.Units.coe_one, NumberField.RingOfIntegers.coe_eq_algebraMap
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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
⊢ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Tactic:
exact ⟨n, hn, by ext; rw [NumberField.RingOfIntegers.coe_eq_algebraMap, coe_pow, hx,
    NumberField.RingOfIntegers.coe_eq_algebraMap, coe_one]⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : (↑(torsion K) : Set (𝓞 K)ˣ).Finite
⊢ Fintype ↥(torsion K)

Tactic:
refine @Fintype.ofFinite _ (Set.finite_coe_iff.mpr ?_)

Premises used: Fintype.ofFinite
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ (↑(torsion K) : Set (𝓞 K)ˣ).Finite

Tactic:
Set.Finite.of_finite_image ?_ (coe_injective K).injOn

Premises used: Function.Injective.injOn, NumberField.Units.coe_injective, Set.Finite.of_finite_image
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine :
  Set.Finite (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ))
⊢ (↑(torsion K) : Set (𝓞 K)ˣ).Finite

Tactic:
refine Set.Finite.of_finite_image ?_ (coe_injective K).injOn

Premises used: Function.Injective.injOn, NumberField.Units.coe_injective, Set.Finite.of_finite_image
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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)ˣ))

Tactic:
(Embeddings.finite_of_norm_le K ℂ 1).subset
    (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)

Premises used: setOf, Membership.mem, Set.Finite.subset, Int, And, IsIntegral, And.intro, NumberField.Units.instFintypeSubtypeUnitsRingOfIntegersMemSubgroupTorsion.match_1, NumberField.Embeddings.finite_of_norm_le, Complex, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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
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
⊢ Set.Finite (α := K)
    ((fun (x : (𝓞 K)ˣ) ↦ (algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K)) '' (↑(torsion K) : Set (𝓞 K)ˣ))

Tactic:
refine (Embeddings.finite_of_norm_le K ℂ 1).subset
    (fun a ⟨u, ⟨h_tors, h_ua⟩⟩ => ⟨?_, fun φ => ?_⟩)
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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
refine_1 : IsIntegral.{0, u_1} ℤ (A := K) ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u)
⊢ IsIntegral ℤ a

Tactic:
rw [← h_ua]
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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.{0, u_1} ℤ (A := K) ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u)

Tactic:
u.val.prop

Premises used: Units.val, Set.Mem, setOf, RingHom.IsIntegralElem, IsIntegral, Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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.{0, u_1} ℤ (A := K) ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u)

Tactic:
exact u.val.prop

Premises used: Units.val, Subtype.prop
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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 →+* ℂ
refine_2 :
  norm (E := ℂ) ((φ : (a : K) → ℂ) ((fun (x : (𝓞 K)ˣ) ↦ ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) u) : ℂ) ≤
    1
⊢ norm (E := ℂ) ((φ : (a : K) → ℂ) a : ℂ) ≤ 1

Tactic:
rw [← h_ua]