awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Units.Basic
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
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) ⋯) : (𝓞 K)ˣ)
⊢ torsionOrder K = 2

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

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_singleton, Subtype.val_inj, Finset.ext, Finset.mem_insert, Finset.card_eq_two, And.intro, Iff.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
simp : Eq.{u_1 + 1} (α := logSpace K) (fun (w : { w : InfinitePlace K // ¬w = w₀ }) ↦ 0) 0
⊢ 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

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₀ }) ↦ 0) 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x x_1 : Additive (𝓞 K)ˣ
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))
⊢ (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))

Tactic:
simp [Real.log_mul, mul_add]

Premises used: mul_add, Real.log_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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) : 𝓞 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:
rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 =
    (↑(↑w : InfinitePlace K).mult : ℝ) *
      Real.log (((↑w : InfinitePlace K) : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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:
have h := sum_mult_mul_log x
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
⊢ ∑ 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

Premises used: Fintype.sum_eq_add_sum_subtype_ne, add_eq_zero_iff_eq_neg, add_comm, NumberField.Units.dirichletUnitTheorem.w₀, neg_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
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))
⊢ ∑ 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))

Tactic:
simpa [logEmbedding_component] using h

Premises used: NumberField.Units.dirichletUnitTheorem.logEmbedding_component
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℝ)
rw₂ : ¬Eq (α := ℝ) (↑w.mult : ℝ) 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 : ℝ)

Tactic:
rw [mul_eq_zero, or_iff_right, Real.log_eq_zero, or_iff_right, or_iff_left]

Premises used: Real.log_eq_zero, mul_eq_zero, or_iff_right, or_iff_left
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
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
⊢ ¬Eq (α := ℝ) ((w : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K) : ℝ) (-1 : ℝ)

Tactic:
linarith [(apply_nonneg _ _ : 0 ≤ w x)]

Premises used: NonnegHomClass.apply_nonneg
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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) : ℝ) (0 : ℝ)

Tactic:
(Units.pos_at_place _ _).ne'

Premises used: NumberField.Units.pos_at_place, LT.lt.ne'
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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) : ℝ) (0 : ℝ)

Tactic:
exact (Units.pos_at_place _ _).ne'

Premises used: NumberField.Units.pos_at_place, LT.lt.ne'
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬Eq (α := ℝ) (↑w.mult : ℝ) 0

Tactic:
mult_coe_ne_zero

Premises used: NumberField.InfinitePlace.mult_coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
x : (𝓞 K)ˣ
w : InfinitePlace K
⊢ ¬Eq (α := ℝ) (↑w.mult : ℝ) 0

Tactic:
exact mult_coe_ne_zero

Premises used: NumberField.InfinitePlace.mult_coe_ne_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
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 : ℝ)
⊢ 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

Tactic:
rw [mem_torsion]

Premises used: NumberField.Units.mem_torsion
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℝ)

Tactic:
⟨fun h w ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℝ)
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)
⊢ 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 ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℝ)
neg :
  ∀ (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 : ℝ)

Tactic:
by_cases hw : w = w₀

Premises used: NumberField.Units.dirichletUnitTheorem.w₀
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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
⊢ (↑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

Premises used: neg_eq_zero, neg_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : (↑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 : ℝ)

Tactic:
mult_log_place_eq_zero.mp this

Premises used: NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : (↑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 : ℝ)

Tactic:
exact mult_log_place_eq_zero.mp this

Premises used: NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₀
pos :
  -(↑(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 : ℝ)

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
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₀
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
⊢ -(↑(mult.{u_1} (K := K) w₀) : ℝ) *
      Real.log ((w₀ : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑x : 𝓞 K) : K)) =
    0

Tactic:
rw [← sum_logEmbedding_component, sum_eq_zero]

Premises used: Finset.sum_eq_zero, NumberField.Units.dirichletUnitTheorem.sum_logEmbedding_component
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₀
⊢ ∀ (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:
fun w _ ↦ congrFun h w

Premises used: congrFun
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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₀
⊢ ∀ (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:
exact fun w _ ↦ congrFun h w

Premises used: congrFun
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℝ)

Tactic:
mult_log_place_eq_zero.mp (congrFun h ⟨w, hw⟩)

Premises used: NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, Subtype.mk, congrFun, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℝ)

Tactic:
exact mult_log_place_eq_zero.mp (congrFun h ⟨w, hw⟩)

Premises used: NumberField.Units.dirichletUnitTheorem.mult_log_place_eq_zero, Subtype.mk, congrFun, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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 : ℝ)
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)
⊢ 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:
ext w
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
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)
refine_2₄ refine_2₅ : Eq (α := ℝ) 0 0
⊢ Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) w)
    (0 w)

Tactic:
rw [logEmbedding_component, h w.val, Real.log_one, mul_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, Real.log_one, MulZeroClass.mul_zero, NumberField.Units.dirichletUnitTheorem.logEmbedding_component, Subtype.val
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
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
⊢ Eq (α := AddSubgroup (Additive (𝓞 K)ˣ)) (AddMonoidHom.ker (M := logSpace K) (logEmbedding K))
    ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ)) (torsion K))

Tactic:
ext x