-- 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_1 : HeightOneSpectrum R
S S' : Set (HeightOneSpectrum R)
n : ℕ
a b : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))
hx :
  Membership.mem (γ := Set (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    {x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) |
      ∀ v ∉ S,
        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))
              x :
            Multiplicative (ZMod n))
          (1 : Multiplicative (ZMod n))}
    a
hy :
  Membership.mem (γ := Set (HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n))))
    {x : HasQuotient.Quotient Kˣ (B := Subgroup Kˣ) (MonoidHom.range (G := Kˣ) (powMonoidHom n)) |
      ∀ v ∉ S,
        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))
              x :
            Multiplicative (ZMod n))
          (1 : Multiplicative (ZMod n))}
    b
v : HeightOneSpectrum R
hv : v ∉ S
rw :
  HMul.hMul (α := Multiplicative (ZMod n)) (β := 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))
          a :
        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))
          b :
        Multiplicative (ZMod n)) =
    1
rw₁ :
  HMul.hMul (α := Multiplicative (ZMod n)) (β := Multiplicative (ZMod n)) (1 : 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))
          b :
        Multiplicative (ZMod n)) =
    1
rw₂ : HMul.hMul (α := Multiplicative (ZMod n)) 1 1 = 1
⊢ 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))
        (a * b) :
      Multiplicative (ZMod n))
    (1 : Multiplicative (ZMod n))
have rw₃ : Eq (α := Multiplicative (ZMod n)) 1 1
Tactic: rw [map_mul, hx v hv, hy v hv, one_mul]