-- 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))
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 ⋯ :
              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))
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 ⋯ :
              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 : ℤ)))
          ((QuotientGroup.mk' (MonoidHom.range (G := Kˣ) (powMonoidHom n)) : (a : Kˣ) → Kˣ ⧸ (powMonoidHom n).range)
            (((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x))) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
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))
        (↑(((v.valuationOfNeZero : Kˣ →* Multiplicative ℤ) : (a : Kˣ) → Multiplicative ℤ)
              (((Units.map (↑(algebraMap R K) : R →* K) : MonoidHom.{u, v} Rˣ Kˣ) : (a : Rˣ) → Kˣ) x)) :
          Multiplicative ℤ ⧸
            (AddSubgroup.toSubgroup : (a : AddSubgroup ℤ) → Subgroup (Multiplicative ℤ))
              (AddSubgroup.zmultiples (↑n : ℤ))) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
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))
        (↑1 :
          Multiplicative ℤ ⧸
            (AddSubgroup.toSubgroup : (a : AddSubgroup ℤ) → Subgroup (Multiplicative ℤ))
              (AddSubgroup.zmultiples (↑n : ℤ))) :
      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))
    1)
  1
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]