-- 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 (α := 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)
⊢ 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))

Tactic:
simp_rw [MonoidHom.toAdditiveLeft_apply_apply, MonoidHom.coe_comp, MulEquiv.coe_toMonoidHom,
    Function.comp_apply, EmbeddingLike.apply_eq_iff_eq] at h

Premises used: MonoidHom.coe_comp, MonoidHom.toAdditiveLeft_apply_apply, MulEquiv.coe_toMonoidHom, EmbeddingLike.apply_eq_iff_eq, Function.comp_apply