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
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf (↑x : (𝓞 K)ˣ) = 0
hc : LE.le (α := ℕ) 0 2
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have linarith : -1 + HSub.hSub (α := ℤ) (↑(orderOf (↑x : (𝓞 K)ˣ)) : ℤ) 0 + (HAdd.hAdd (α := ℤ) 0 1 - (↑(orderOf (↑x : (𝓞 K)ˣ)) : ℤ)) = 0
Tactic: linarith [orderOf_pos_iff.2 ((CommGroup.mem_torsion _ x.1).1 x.2)]
-- 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)
hi : orderOf (↑x : (𝓞 K)ˣ) = 2
hc : LE.le (α := ℕ) 2 2
⊢ (↑x : (𝓞 K)ˣ) = 1 ∨ (↑x : (𝓞 K)ˣ) = -1
have hi₁ : (↑(↑x : (𝓞 K)ˣ) : 𝓞 K) = -1
Tactic: rw [← orderOf_units, CharP.orderOf_eq_two_iff 0 (by decide)] at hi
Cleared hypotheses: hi, 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)
⊢ torsionOrder K = 2
have refine : ∀ (x : ↥(torsion K)),
  Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x →
    Membership.mem (γ := Finset ↥(torsion K))
      {1, Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) sorry} x
Tactic: refine (Finset.card_eq_two.2 ⟨1, ⟨-1, neg_one_mem_torsion⟩,
    by simp [← Subtype.coe_ne_coe], Finset.ext fun x ↦ ⟨fun _ ↦ ?_, fun _ ↦ Finset.mem_univ _⟩⟩)
-- 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)
h_1 : Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x
⊢ Membership.mem (γ := Finset ↥(torsion K))
    {1, Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯} x
have rw : (↑x : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ∨
  (↑x : (𝓞 K)ˣ) =
    (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) sorry) : (𝓞 K)ˣ)
Tactic: rw [Finset.mem_insert, Finset.mem_singleton, ← Subtype.val_inj, ← Subtype.val_inj]
-- 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)
⊢ torsionOrder K = 2
have refine : ∀ (x : ↥(torsion K)),
  Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x →
    Membership.mem (γ := Finset ↥(torsion K))
      {1, Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) sorry} x
Tactic: classical
  refine (Finset.card_eq_two.2 ⟨1, ⟨-1, neg_one_mem_torsion⟩,
    by simp [← Subtype.coe_ne_coe], Finset.ext fun x ↦ ⟨fun _ ↦ ?_, fun _ ↦ Finset.mem_univ _⟩⟩)
  rw [Finset.mem_insert, Finset.mem_singleton, ← Subtype.val_inj, ← Subtype.val_inj]
  exact torsion_eq_one_or_neg_one_of_odd_finrank h x
-- 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)
refine :
  ∀ (x : ↥(torsion K)),
    Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x →
      Membership.mem (γ := Finset ↥(torsion K))
        {1, Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) ⋯} x
⊢ torsionOrder K = 2
have refine₁ : ∀ (x : ↥(torsion K)),
  Membership.mem (γ := Finset ↥(torsion K)) Finset.univ x →
    (↑x : (𝓞 K)ˣ) = (↑1 : (𝓞 K)ˣ) ∨
      (↑x : (𝓞 K)ˣ) =
        (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) (-1) sorry) : (𝓞 K)ˣ)
Tactic: classical
  refine (Finset.card_eq_two.2 ⟨1, ⟨-1, neg_one_mem_torsion⟩,
    by simp [← Subtype.coe_ne_coe], Finset.ext fun x ↦ ⟨fun _ ↦ ?_, fun _ ↦ Finset.mem_univ _⟩⟩)
  rw [Finset.mem_insert, Finset.mem_singleton, ← Subtype.val_inj, ← Subtype.val_inj]
  exact torsion_eq_one_or_neg_one_of_odd_finrank h x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq.{u_1 + 1} (α := logSpace K)
    (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log
          (((↑w : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) 0) : 𝓞 K) : K)))
    0
have simp : Eq.{u_1 + 1} (α := logSpace K) (fun (w : { w : InfinitePlace K // ¬w = w₀ }) ↦ 0) 0
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x x_1 : Additive (𝓞 K)ˣ
⊢ (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log
          (((↑w : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
                (↑((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) (x + x_1)) : 𝓞 K) :
              K))) =
    HAdd.hAdd (α := logSpace K)
      (fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
        (↑(↑w : InfinitePlace K).mult : ℝ) *
          Real.log
            (((↑w : InfinitePlace K) : (a : K) → ℝ)
              ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x) : 𝓞 K) :
                K)))
      fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log
          (((↑w : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x_1) : 𝓞 K) : K))
have simp : (fun (w : { w : InfinitePlace K // ¬w = w₀ }) ↦
    (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log
          (((↑w : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x) : 𝓞 K) : K)) +
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log
          (((↑w : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x_1) : 𝓞 K) :
              K))) =
  HAdd.hAdd (α := logSpace K)
    (fun (w : { w : InfinitePlace K // ¬w = w₀ }) ↦
      (↑(↑w : InfinitePlace K).mult : ℝ) *
        Real.log
          (((↑w : InfinitePlace K) : (a : K) → ℝ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x) : 𝓞 K) : K)))
    fun (w : { w : InfinitePlace K // ¬w = w₀ }) ↦
    (↑(↑w : InfinitePlace K).mult : ℝ) *
      Real.log
        (((↑w : InfinitePlace K) : (a : K) → ℝ)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑((Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) x_1) : 𝓞 K) : K))
Tactic: simp [Real.log_mul, mul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ ∑ w : { w : InfinitePlace K // w ≠ w₀ },
      (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w =
    -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
      Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))
have h : Eq (α := ℝ)
  (∑ w : InfinitePlace K,
    (↑w.mult : ℝ) * Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)))
  0
Tactic: have h := sum_mult_mul_log x
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  Eq (α := ℝ)
    (∑ w : InfinitePlace K,
      (↑w.mult : ℝ) * Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)))
    0
⊢ ∑ w : { w : InfinitePlace K // w ≠ w₀ },
      (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w =
    -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
      Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))
have h₁ : ∑ i : { i : InfinitePlace K // i ≠ w₀ },
    (↑(↑i : InfinitePlace K).mult : ℝ) *
      Real.log (((↑i : InfinitePlace K) : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
  -(↑(mult.{u_1} (K := K) w₀) : ℝ) * Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))
Tactic: rw [Fintype.sum_eq_add_sum_subtype_ne _ w₀, add_comm, add_eq_zero_iff_eq_neg, ← neg_mul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ (↑w.mult : ℝ) * Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) = 0 ↔
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have rw : ¬Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (-1 : ℝ)
Tactic: rw [mul_eq_zero, or_iff_right, Real.log_eq_zero, or_iff_right, or_iff_left]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
rw : ¬Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (-1 : ℝ)
⊢ (↑w.mult : ℝ) * Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) = 0 ↔
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have rw₁ : ¬Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (0 : ℝ)
Tactic: rw [mul_eq_zero, or_iff_right, Real.log_eq_zero, or_iff_right, or_iff_left]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
rw : ¬Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (-1 : ℝ)
rw₁ : ¬Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (0 : ℝ)
⊢ (↑w.mult : ℝ) * Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) = 0 ↔
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have rw₂ : ¬Eq (α := ℝ) (↑w.mult : ℝ) 0
Tactic: rw [mul_eq_zero, or_iff_right, Real.log_eq_zero, or_iff_right, or_iff_left]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (-1 : ℝ)
have linarith : Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (-1 : ℝ) →
  -1 +
        HSub.hSub (α := ℝ) (β := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ)
          (-1 : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) (0 : ℝ)
        ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) =
    0
Tactic: linarith [(apply_nonneg _ _ : 0 ≤ w x)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ Eq (α := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K)
      (0 : logSpace K) ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x
have rw : Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K) ↔
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
Tactic: rw [mem_torsion]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ Eq (α := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K)
      (0 : logSpace K) ↔
    ∀ (w : InfinitePlace K),
      Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have refine_1 : ∀
  (h :
    Eq (α := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K)
      (0 : logSpace K))
  (w : InfinitePlace K),
  Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
Tactic: refine ⟨fun h w ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
refine_1 :
  ∀
    (h :
      Eq (α := logSpace K)
        ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
            ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
          logSpace K)
        (0 : logSpace K))
    (w : InfinitePlace K),
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
⊢ Eq (α := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K)
      (0 : logSpace K) ↔
    ∀ (w : InfinitePlace K),
      Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have refine_2 : ∀
  (h :
    ∀ (w : InfinitePlace K),
      Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)),
  Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
Tactic: refine ⟨fun h w ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
w : InfinitePlace K
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have pos : ∀ (hw : w = w₀), Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
Tactic: by_cases hw : w = w₀
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
w : InfinitePlace K
pos : ∀ (hw : w = w₀), Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have neg : ∀ (hw : ¬w = w₀), Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
Tactic: by_cases hw : w = w₀
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
w : InfinitePlace K
hw : w = w₀
this :
  -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
      Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
    0
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have this₁ : (↑w.mult : ℝ) * Real.log ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) = 0
Tactic: rw [neg_mul, neg_eq_zero, ← hw] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
w : InfinitePlace K
hw : w = w₀
⊢ Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
have pos : -(↑(mult.{u_1} (K := K) w₀) : ℝ) * Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
  0
Tactic: suffices -mult w₀ * Real.log (w₀ (x : K)) = 0 by
        rw [neg_mul, neg_eq_zero, ← hw] at this
        exact mult_log_place_eq_zero.mp this
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
w : InfinitePlace K
hw : w = w₀
⊢ -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
      Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
    0
have pos : ∀ (x_1 : { w : InfinitePlace K // w ≠ w₀ }),
  Membership.mem (γ := Finset { w : InfinitePlace K // w ≠ w₀ }) univ x_1 →
    Eq (α := ℝ)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) x_1)
      0
Tactic: rw [← sum_logEmbedding_component, sum_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
⊢ Eq (α := logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)
    (0 : logSpace K)
have refine_2 : ∀ (w : { w : InfinitePlace K // w ≠ w₀ }),
  Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w)
    (0 w)
Tactic: ext w
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
⊢ Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w)
    (0 w)
have refine_2 : (↑(↑w : InfinitePlace K).mult : ℝ) *
    Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
  0 w
Tactic: rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
refine_2 :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
    0 w
⊢ Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w)
    (0 w)
have refine_2₁ : (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log 1 = 0 w
Tactic: rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
refine_2 :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
    0 w
refine_2₁ : (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log 1 = 0 w
⊢ Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w)
    (0 w)
have refine_2₂ : HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) 0 = 0 w
Tactic: rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
refine_2 :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
    0 w
refine_2₁ : (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log 1 = 0 w
refine_2₂ : HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) 0 = 0 w
⊢ Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w)
    (0 w)
have refine_2₃ : Eq (α := ℝ) 0 (0 w)
Tactic: rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  ∀ (w : InfinitePlace K),
    Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (1 : ℝ)
w : { w : InfinitePlace K // w ≠ w₀ }
refine_2 :
  (↑(↑w : InfinitePlace K).mult : ℝ) *
      Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
    0 w
refine_2₁ : (↑(↑w : InfinitePlace K).mult : ℝ) * Real.log 1 = 0 w
refine_2₂ : HMul.hMul (α := ℝ) (↑(↑w : InfinitePlace K).mult : ℝ) 0 = 0 w
refine_2₃ : Eq (α := ℝ) 0 (0 w)
⊢ Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w)
    (0 w)
have refine_2₄ : Eq (α := ℝ) 0 0
Tactic: rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Eq (α := AddSubgroup (Additive (𝓞 K)ˣ)) (AddMonoidHom.ker (M := logSpace K) (logEmbedding K))
    ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K))
have h : ∀ (x : Additive (𝓞 K)ˣ),
  Membership.mem (γ := AddSubgroup (Additive (𝓞 K)ˣ)) (AddMonoidHom.ker (M := logSpace K) (logEmbedding K)) x ↔
    Membership.mem (γ := AddSubgroup (Additive (𝓞 K)ˣ))
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K) :
        AddSubgroup (Additive (𝓞 K)ˣ))
      x
Tactic: ext x