-- Lean 4 proof step from Mathlib.RingTheory.DedekindDomain.SelmerGroup (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type v
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Rˣ
erw :
  Eq (α := Multiplicative (ZMod n))
    (((MonoidHom.comp
              (MulEquiv.toMonoidHom
                ((AddEquiv.toMultiplicative :
                    (a : ℤ ⧸ AddSubgroup.zmultiples (↑n : ℤ) ≃+ ZMod n) →
                      Multiplicative (ℤ ⧸ AddSubgroup.zmultiples (↑n : ℤ)) ≃* Multiplicative (ZMod n))
                  (Int.quotientZMultiplesNatEquivZMod n)))
              (QuotientGroup.map (MonoidHom.range (G := Kˣ) (powMonoidHom n))
                ((AddSubgroup.toSubgroup : (a : AddSubgroup ℤ) → Subgroup (Multiplicative ℤ))
                  (AddSubgroup.zmultiples (↑n : ℤ)))
                v.valuationOfNeZero ⋯) :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x) :
          Kˣ ⧸ (powMonoidHom n).range) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
⊢ Eq (α := Multiplicative (ZMod n))
    (((v.valuationOfNeZeroMod n :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              Multiplicative (ZMod n)) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ZMod n))
        (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x) :
          Kˣ ⧸ (powMonoidHom n).range) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have erw₁ : Eq (α := Multiplicative (ZMod n))
  ((MulEquiv.toMonoidHom
          ((AddEquiv.toMultiplicative :
              (a : ℤ ⧸ AddSubgroup.zmultiples (↑n : ℤ) ≃+ ZMod n) →
                Multiplicative (ℤ ⧸ AddSubgroup.zmultiples (↑n : ℤ)) ≃* Multiplicative (ZMod n))
            (Int.quotientZMultiplesNatEquivZMod n)) :
        (a : Multiplicative (ℤ ⧸ AddSubgroup.zmultiples (↑n : ℤ))) → Multiplicative (ZMod n))
      (((QuotientGroup.map (MonoidHom.range (G := Kˣ) (powMonoidHom n))
              ((AddSubgroup.toSubgroup : (a : AddSubgroup ℤ) → Subgroup (Multiplicative ℤ))
                (AddSubgroup.zmultiples (↑n : ℤ)))
              v.valuationOfNeZero sorry :
            HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) →*
              HasQuotient.Quotient (Multiplicative ℤ) (B := Subgroup (Multiplicative ℤ))
                ((AddSubgroup.toSubgroup : (a : AddSubgroup ℤ) → Subgroup (Multiplicative ℤ))
                    (AddSubgroup.zmultiples (↑n : ℤ)) :
                  Subgroup (Multiplicative ℤ))) :
          (a : Kˣ ⧸ (powMonoidHom n).range) → Multiplicative (ℤ ⧸ AddSubgroup.zmultiples (↑n : ℤ)))
        (↑(((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x) :
          Kˣ ⧸ (powMonoidHom n).range)) :
    Multiplicative (ZMod n))
  (1 : Multiplicative (ZMod n))
Tactic: erw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk',
    QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)),
    valuation_of_unit_eq, QuotientGroup.mk_one, map_one]