awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
pos : (↑x : InfinitePlace K).IsReal → LT.lt (α := ℝ) 0 (↑1 : ℝ)
neg : ¬(↑x : InfinitePlace K).IsReal → LT.lt (α := ℝ) 0 (↑2 : ℝ)
⊢ LT.lt (α := ℝ) 0 (↑(if (↑x : InfinitePlace K).IsReal then 1 else 2) : ℝ)

Tactic:
split_ifs
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
h : (↑x : InfinitePlace K).IsReal
⊢ LT.lt (α := ℝ) 0 (↑1 : ℝ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
h : ¬(↑x : InfinitePlace K).IsReal
⊢ LT.lt (α := ℝ) 0 (↑2 : ℝ)

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
⊢ (↑x : InfinitePlace K) ≠ (↑w : InfinitePlace K)

Tactic:
Subtype.ext_iff.not.mp (ne_of_mem_erase hx)

Premises used: Finset.ne_of_mem_erase, Iff.not, Subtype.ext_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
B : Basis { w : InfinitePlace K // w ≠ w₀ } ℝ ({ w : InfinitePlace K // w ≠ w₀ } → ℝ) :=
  Pi.basisFun ℝ { w : InfinitePlace K // w ≠ w₀ }
v : (w : { w : InfinitePlace K // w ≠ w₀ }) → logSpace K :=
  fun (w : { w : InfinitePlace K // w ≠ w₀ }) ↦
    (logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ)
          (⋯.choose (p := fun (u : (𝓞 K)ˣ) ↦
            ∀ (w_1 : InfinitePlace K),
              w_1 ≠ (↑w : InfinitePlace K) →
                Real.log ((w_1 : (a : K) → ℝ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑u : 𝓞 K) : K)) < 0)) :
        Additive (𝓞 K)ˣ)
w x : { w : InfinitePlace K // w ≠ w₀ }
hx : x ∈ erase univ w
⊢ (↑x : InfinitePlace K) ≠ (↑w : InfinitePlace K)

Tactic:
exact Subtype.ext_iff.not.mp (ne_of_mem_erase hx)

Premises used: Finset.ne_of_mem_erase, Iff.not, Subtype.ext_iff, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ DiscreteTopology.{u_1} ↥(unitLattice K)

Tactic:
discreteTopology_of_isOpen_singleton_zero ?_

Premises used: discreteTopology_of_isOpen_singleton_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : IsOpen (X := ↥(unitLattice K)) {0}
⊢ DiscreteTopology.{u_1} ↥(unitLattice K)

Tactic:
refine discreteTopology_of_isOpen_singleton_zero ?_

Premises used: discreteTopology_of_isOpen_singleton_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ IsOpen (X := ↥(unitLattice K)) {0}

Tactic:
isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_

Premises used: isOpen_singleton_of_finite_mem_nhds, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_1 : Membership.mem (γ := Filter ↥(unitLattice K)) (nhds 0) (Metric.closedBall 0 1)
refine_2 : Set.Finite.{u_1} (α := ↥(unitLattice K)) (Metric.closedBall 0 1)
⊢ IsOpen (X := ↥(unitLattice K)) {0}

Tactic:
refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_

Premises used: isOpen_singleton_of_finite_mem_nhds, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ LT.lt (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Membership.mem (γ := Filter ↥(unitLattice K)) (nhds 0) (Metric.closedBall 0 1)

Tactic:
exact Metric.closedBall_mem_nhds _ (by simp)

Premises used: Metric.closedBall_mem_nhds
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Set.Finite.{u_1} (α := ↥(unitLattice K)) (Metric.closedBall 0 1)

Tactic:
Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)

Premises used: Subtype.val_injective, Set.Finite.of_finite_image, Set.injOn_of_injective
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine_2 :
  Set.Finite.{u_1} (α := logSpace K)
    (Set.image (α := ↥(unitLattice K))
      (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
      (Metric.closedBall 0 1))
⊢ Set.Finite.{u_1} (α := ↥(unitLattice K)) (Metric.closedBall 0 1)

Tactic:
refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)

Premises used: Subtype.val_injective, Set.Finite.of_finite_image, Set.injOn_of_injective
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ ((↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1).Finite

Tactic:
unitLattice_inter_ball_finite K 1

Premises used: NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  Set.image (α := ↥(unitLattice K))
      (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
      (Metric.closedBall 0 1) =
    (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1
⊢ Set.Finite.{u_1} (α := logSpace K)
    (Set.image (α := ↥(unitLattice K))
      (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
      (Metric.closedBall 0 1))

Tactic:
convert! unitLattice_inter_ball_finite K 1

Premises used: NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, OfNat.ofNat
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : logSpace K),
    Membership.mem (γ := Set (logSpace K))
        (Set.image (α := ↥(unitLattice K))
          (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
          (Metric.closedBall 0 1))
        x ↔
      x ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1
⊢ Set.image (α := ↥(unitLattice K))
      (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
      (Metric.closedBall 0 1) =
    (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1

Tactic:
ext x
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : logSpace K
⊢ Membership.mem (γ := Set (logSpace K))
      (Set.image (α := ↥(unitLattice K))
        (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
        (Metric.closedBall 0 1))
      x ↔
    x ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1

Tactic:
⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩

Premises used: _private.0.NumberField.Units.instDiscrete_unitLattice.match_1, Membership.mem, Subtype.mk, And.intro, Iff.intro, Exists.intro, Set.image, Metric.closedBall, OfNat.ofNat, Subtype.val, rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : logSpace K
h :
  Membership.mem (γ := Set (logSpace K))
      (Set.image (α := ↥(unitLattice K))
        (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
        (Metric.closedBall 0 1))
      x →
    x ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1
⊢ Membership.mem (γ := Set (logSpace K))
      (Set.image (α := ↥(unitLattice K))
        (Subtype.val (p := fun (x : logSpace K) ↦ Membership.mem (γ := Submodule ℤ (logSpace K)) (unitLattice K) x))
        (Metric.closedBall 0 1))
      x ↔
    x ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1

Tactic:
refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : ↥(unitLattice K)
hx : Membership.mem (γ := Set ↥(unitLattice K)) (Metric.closedBall 0 1) x
⊢ (↑x : logSpace K) ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1

Tactic:
⟨Subtype.mem x, hx⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro, Subtype.mem
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : ↥(unitLattice K)
hx : Membership.mem (γ := Set ↥(unitLattice K)) (Metric.closedBall 0 1) x
⊢ (↑x : logSpace K) ∈ (↑(unitLattice K) : Set (logSpace K)) ∩ Metric.closedBall 0 1

Tactic:
exact ⟨Subtype.mem x, hx⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
refine : IsOpen (X := ↥(unitLattice K)) {0}
refine_1 : Membership.mem (γ := Filter ↥(unitLattice K)) (nhds 0) (Metric.closedBall 0 1)
refine_2 refine_2₁ : Set.Finite.{u_1} (α := ↥(unitLattice K)) (Metric.closedBall 0 1)
⊢ DiscreteTopology.{u_1} ↥(unitLattice K)

Tactic:
classical
  refine discreteTopology_of_isOpen_singleton_zero ?_
  refine isOpen_singleton_of_finite_mem_nhds 0 (s := Metric.closedBall 0 1) ?_ ?_
  · exact Metric.closedBall_mem_nhds _ (by simp)
  · refine Set.Finite.of_finite_image ?_ (Set.injOn_of_injective Subtype.val_injective)
    convert! unitLattice_inter_ball_finite K 1
    ext x
    refine ⟨?_, fun ⟨hx1, hx2⟩ ↦ ⟨⟨x, hx1⟩, hx2, rfl⟩⟩
    rintro ⟨x, hx, rfl⟩
    exact ⟨Subtype.mem x, hx⟩

Premises used: discreteTopology_of_isOpen_singleton_zero, Metric.closedBall_mem_nhds, Subtype.val_injective, NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite, isOpen_singleton_of_finite_mem_nhds, Set.Finite.of_finite_image, Set.injOn_of_injective, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ finrank.{0, u_1} ℝ (logSpace K) = rank K

Tactic:
simp only [finrank_fintype_fun_eq_card, Fintype.card_subtype_compl,
    Fintype.card_ofSubsingleton, rank]

Premises used: NumberField.Units.rank, Fintype.card_ofSubsingleton, Module.finrank_fintype_fun_eq_card, Fintype.card_subtype_compl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ finrank.{0, u_1} ℝ (logSpace K) = rank K

Tactic:
classical
  simp only [finrank_fintype_fun_eq_card, Fintype.card_subtype_compl,
    Fintype.card_ofSubsingleton, rank]

Premises used: NumberField.Units.rank, Fintype.card_ofSubsingleton, Module.finrank_fintype_fun_eq_card, Fintype.card_subtype_compl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : finrank.{0, u_1} ℤ ↥(unitLattice K) = finrank.{0, u_1} ℝ (logSpace K)
rw₁ rw₂ : finrank.{0, u_1} ℝ (logSpace K) = finrank.{0, u_1} ℝ (logSpace K)
⊢ finrank.{0, u_1} ℤ ↥(unitLattice K) = rank K

Tactic:
rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]

Premises used: NumberField.Units.finrank_eq_rank, Real, ZLattice.rank
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : finrank.{0, u_1} ℤ ↥(unitLattice K) = finrank.{0, u_1} ℝ (logSpace K)
rw₁ rw₂ : finrank.{0, u_1} ℝ (logSpace K) = finrank.{0, u_1} ℝ (logSpace K)
⊢ finrank.{0, u_1} ℤ ↥(unitLattice K) = rank K

Tactic:
classical
  rw [← Units.finrank_eq_rank, ZLattice.rank ℝ]

Premises used: NumberField.Units.finrank_eq_rank, Real, ZLattice.rank
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
h :
  ∀ (x : (𝓞 K)ˣ),
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
      Membership.mem (γ := Subgroup (𝓞 K)ˣ)
        (MonoidHom.ker (M := Multiplicative (logSpace K))
          ((AddMonoidHom.toMultiplicativeRight :
              (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
            (logEmbedding K)))
        x
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (torsion K)
    (MonoidHom.ker (M := Multiplicative (logSpace K))
      ((AddMonoidHom.toMultiplicativeRight :
          (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
        (logEmbedding K)))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
h :
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    Eq (α := Multiplicative (logSpace K))
      ((((AddMonoidHom.toMultiplicativeRight :
                  (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                (logEmbedding K) :
              (𝓞 K)ˣ →* Multiplicative (logSpace K)) :
            (a : (𝓞 K)ˣ) → Multiplicative (logSpace K))
          x :
        Multiplicative (logSpace K))
      (1 : Multiplicative (logSpace K))
h₁ :
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    Eq (α := Multiplicative (logSpace K))
      ((Multiplicative.ofAdd : (a : logSpace K) → Multiplicative (logSpace K))
          ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
              ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
            logSpace K) :
        Multiplicative (logSpace K))
      (1 : Multiplicative (logSpace K))
h₂ :
  Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x ↔
    Eq (α := logSpace K)
      ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
        logSpace K)
      (0 : logSpace K)
h₃ 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) ↔
    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 ↔
    Membership.mem (γ := Subgroup (𝓞 K)ˣ)
      (MonoidHom.ker (M := Multiplicative (logSpace K))
        ((AddMonoidHom.toMultiplicativeRight :
            (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
          (logEmbedding K)))
      x

Tactic:
rw [MonoidHom.mem_ker, AddMonoidHom.toMultiplicativeRight_apply_apply, ofAdd_eq_one,
          ← logEmbedding_eq_zero_iff]

Premises used: AddMonoidHom.toMultiplicativeRight_apply_apply, MonoidHom.mem_ker, NumberField.Units.dirichletUnitTheorem.logEmbedding_eq_zero_iff, ofAdd_eq_one
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ Eq (α := logSpace K)
    ((logEmbeddingQuot K : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K)) (↑x : (𝓞 K)ˣ ⧸ torsion K) :
          Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))) :
      logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)

Tactic:
rfl

Premises used: Quotient.liftOn', Con.liftOn, rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a₁ a₂ : Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
h :
  Eq (α := Multiplicative (logSpace K))
    ((QuotientGroup.kerLift
            ((AddMonoidHom.toMultiplicativeRight :
                (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
              (logEmbedding K)) :
          (a :
              (𝓞 K)ˣ ⧸
                ((AddMonoidHom.toMultiplicativeRight :
                      (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                    (logEmbedding K)).ker) →
            Multiplicative (logSpace K))
        ((QuotientGroup.quotientMulEquivOfEq ⋯ :
              (a : (𝓞 K)ˣ ⧸ torsion K) →
                (𝓞 K)ˣ ⧸
                  ((AddMonoidHom.toMultiplicativeRight :
                        (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                      (logEmbedding K)).ker)
            ((Additive.toMul : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → (𝓞 K)ˣ ⧸ torsion K) a₁) :
          HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ)
            (MonoidHom.ker (M := Multiplicative (logSpace K))
              ((AddMonoidHom.toMultiplicativeRight :
                  (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                (logEmbedding K)))) :
      Multiplicative (logSpace K))
    ((QuotientGroup.kerLift
            ((AddMonoidHom.toMultiplicativeRight :
                (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
              (logEmbedding K)) :
          (a :
              (𝓞 K)ˣ ⧸
                ((AddMonoidHom.toMultiplicativeRight :
                      (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                    (logEmbedding K)).ker) →
            Multiplicative (logSpace K))
        ((QuotientGroup.quotientMulEquivOfEq ⋯ :
              (a : (𝓞 K)ˣ ⧸ torsion K) →
                (𝓞 K)ˣ ⧸
                  ((AddMonoidHom.toMultiplicativeRight :
                        (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                      (logEmbedding K)).ker)
            ((Additive.toMul : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → (𝓞 K)ˣ ⧸ torsion K) a₂) :
          HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ)
            (MonoidHom.ker (M := Multiplicative (logSpace K))
              ((AddMonoidHom.toMultiplicativeRight :
                  (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                (logEmbedding K)))) :
      Multiplicative (logSpace K))
⊢ a₁ = a₂

Tactic:
(EmbeddingLike.apply_eq_iff_eq _).mp <| (QuotientGroup.kerLift_injective _).eq_iff.mp h

Premises used: Function.Injective.eq_iff, EmbeddingLike.apply_eq_iff_eq, QuotientGroup.kerLift_injective, Iff.mp
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a₁ a₂ : Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
h :
  Eq (α := Multiplicative (logSpace K))
    ((QuotientGroup.kerLift
            ((AddMonoidHom.toMultiplicativeRight :
                (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
              (logEmbedding K)) :
          (a :
              (𝓞 K)ˣ ⧸
                ((AddMonoidHom.toMultiplicativeRight :
                      (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                    (logEmbedding K)).ker) →
            Multiplicative (logSpace K))
        ((QuotientGroup.quotientMulEquivOfEq ⋯ :
              (a : (𝓞 K)ˣ ⧸ torsion K) →
                (𝓞 K)ˣ ⧸
                  ((AddMonoidHom.toMultiplicativeRight :
                        (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                      (logEmbedding K)).ker)
            ((Additive.toMul : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → (𝓞 K)ˣ ⧸ torsion K) a₁) :
          HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ)
            (MonoidHom.ker (M := Multiplicative (logSpace K))
              ((AddMonoidHom.toMultiplicativeRight :
                  (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                (logEmbedding K)))) :
      Multiplicative (logSpace K))
    ((QuotientGroup.kerLift
            ((AddMonoidHom.toMultiplicativeRight :
                (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
              (logEmbedding K)) :
          (a :
              (𝓞 K)ˣ ⧸
                ((AddMonoidHom.toMultiplicativeRight :
                      (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                    (logEmbedding K)).ker) →
            Multiplicative (logSpace K))
        ((QuotientGroup.quotientMulEquivOfEq ⋯ :
              (a : (𝓞 K)ˣ ⧸ torsion K) →
                (𝓞 K)ˣ ⧸
                  ((AddMonoidHom.toMultiplicativeRight :
                        (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                      (logEmbedding K)).ker)
            ((Additive.toMul : (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → (𝓞 K)ˣ ⧸ torsion K) a₂) :
          HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ)
            (MonoidHom.ker (M := Multiplicative (logSpace K))
              ((AddMonoidHom.toMultiplicativeRight :
                  (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                (logEmbedding K)))) :
      Multiplicative (logSpace K))
⊢ a₁ = a₂

Tactic:
exact (EmbeddingLike.apply_eq_iff_eq _).mp <| (QuotientGroup.kerLift_injective _).eq_iff.mp h

Premises used: Function.Injective.eq_iff, EmbeddingLike.apply_eq_iff_eq, QuotientGroup.kerLift_injective, Iff.mp