-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.Units.DirichletTheorem (hypothesis)
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 (α := 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₂
have 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 sorry :
            (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 sorry :
            (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))
Tactic: simp_rw [MonoidHom.toAdditiveLeft_apply_apply, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom,
    Function.comp_apply, EmbeddingLike.apply_eq_iff_eq] at h
Cleared hypotheses: h