-- 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
x : Kˣ
rw rw₁ rw₂ :
  (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)) :
            (a : R) → WithZero (Multiplicative ℤ))
          (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).1 :
        WithZero (Multiplicative ℤ))
      ((↑(((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)).restrict R⁰) ⋯ :
                    ↥(R⁰ : Submonoid R) →* (WithZero (Multiplicative ℤ))ˣ) :
                  (a : ↥R⁰) → (WithZero (Multiplicative ℤ))ˣ)
                (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K)
                    (↑x : K)).2)⁻¹ :
          WithZero (Multiplicative ℤ)) :
        WithZero (Multiplicative ℤ))
rw₃ :
  (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)) :
            (a : R) → WithZero (Multiplicative ℤ))
          (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).1 :
        WithZero (Multiplicative ℤ))
      ((↑(((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom : R →* WithZero (Multiplicative ℤ)).restrict R⁰) ⋯ :
                    ↥(R⁰ : Submonoid R) →* (WithZero (Multiplicative ℤ))ˣ) :
                  (a : ↥R⁰) → (WithZero (Multiplicative ℤ))ˣ)
                (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K)
                    (↑x : K)).2) :
            WithZero (Multiplicative ℤ))⁻¹ :
        WithZero (Multiplicative ℤ))
⊢ (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑x : K)
have rw₄ : (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
  HMul.hMul (α := WithZero (Multiplicative ℤ))
    (if
        Eq.{u + 1} (α := R)
          (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).1
          0 then
      0
    else
      exp
        (-(↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors
                  (Associates.mk
                    (Ideal.span
                      {(Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K)
                            (↑x : K)).1})))) :
            ℤ)))
    (if
          Eq (α := R)
            ((SubmonoidClass.subtype R⁰ : (a : ↥R⁰) → R)
                (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰) (IsLocalization.toLocalizationMap R⁰ K)
                    (↑x : K)).2 :
              R)
            (0 : R) then
        0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors
                    (Associates.mk
                      (Ideal.span
                        (singleton (α := R)
                          ((SubmonoidClass.subtype R⁰ : (a : ↥R⁰) → R)
                              (Submonoid.LocalizationMap.sec.{u, v} (M := R) (S := R⁰)
                                  (IsLocalization.toLocalizationMap R⁰ K) (↑x : K)).2 :
                            R)))))) :
              ℤ)))⁻¹
Tactic: classical
  rw [show v.valuation K x = _ * _ by rfl]
  rw [Units.val_inv_eq_inv_val]
  change _ = ite _ _ _ * (ite _ _ _)⁻¹
  simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
    if_neg <| IsLocalization.sec_fst_ne_zero x.ne_zero,
    if_neg (nonZeroDivisors.coe_ne_zero _),
    ← exp_neg, ← exp_add, valuationOfNeZeroToFun, ← sub_eq_add_neg, exp]