-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
a₁ : Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))
_ :
  ∀ ⦃a₂ : Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))⦄,
    Eq (α := logSpace K)
        ((((MonoidHom.toAdditiveLeft :
                    (a : (𝓞 K)ˣ ⧸ torsion K →* Multiplicative (logSpace K)) →
                      Additive ((𝓞 K)ˣ ⧸ torsion K) →+ logSpace K)
                  (MonoidHom.comp
                    (QuotientGroup.kerLift
                      ((AddMonoidHom.toMultiplicativeRight :
                          (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                        (logEmbedding K)))
                    (MulEquiv.toMonoidHom (QuotientGroup.quotientMulEquivOfEq ⋯))) :
                Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)) →+ logSpace K) :
              (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → logSpace K)
            a₁ :
          logSpace K)
        ((((MonoidHom.toAdditiveLeft :
                    (a : (𝓞 K)ˣ ⧸ torsion K →* Multiplicative (logSpace K)) →
                      Additive ((𝓞 K)ˣ ⧸ torsion K) →+ logSpace K)
                  (MonoidHom.comp
                    (QuotientGroup.kerLift
                      ((AddMonoidHom.toMultiplicativeRight :
                          (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                        (logEmbedding K)))
                    (MulEquiv.toMonoidHom (QuotientGroup.quotientMulEquivOfEq ⋯))) :
                Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)) →+ logSpace K) :
              (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → logSpace K)
            a₂ :
          logSpace K) →
      a₁ = a₂
⊢ ∀ ⦃a₂ : Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))⦄,
    Eq (α := logSpace K)
        ((((MonoidHom.toAdditiveLeft :
                    (a : (𝓞 K)ˣ ⧸ torsion K →* Multiplicative (logSpace K)) →
                      Additive ((𝓞 K)ˣ ⧸ torsion K) →+ logSpace K)
                  (MonoidHom.comp
                    (QuotientGroup.kerLift
                      ((AddMonoidHom.toMultiplicativeRight :
                          (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                        (logEmbedding K)))
                    (MulEquiv.toMonoidHom (QuotientGroup.quotientMulEquivOfEq ⋯))) :
                Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)) →+ logSpace K) :
              (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → logSpace K)
            a₁ :
          logSpace K)
        ((((MonoidHom.toAdditiveLeft :
                    (a : (𝓞 K)ˣ ⧸ torsion K →* Multiplicative (logSpace K)) →
                      Additive ((𝓞 K)ˣ ⧸ torsion K) →+ logSpace K)
                  (MonoidHom.comp
                    (QuotientGroup.kerLift
                      ((AddMonoidHom.toMultiplicativeRight :
                          (a : Additive (𝓞 K)ˣ →+ logSpace K) → (𝓞 K)ˣ →* Multiplicative (logSpace K))
                        (logEmbedding K)))
                    (MulEquiv.toMonoidHom (QuotientGroup.quotientMulEquivOfEq ⋯))) :
                Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)) →+ logSpace K) :
              (a : Additive ((𝓞 K)ˣ ⧸ torsion K)) → logSpace K)
            a₂ :
          logSpace K) →
      a₁ = a₂

Tactic:
_