-- 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ˣ
simp_rw :
  (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if Eq.{u + 1} (α := R) (IsLocalization.sec R⁰ (↑x : K)).1 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ (↑x : K)).1})))) :
              ℤ)))
      (if Eq (α := R) ((SubmonoidClass.subtype R⁰ : (a : ↥R⁰) → R) (IsLocalization.sec R⁰ (↑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) (IsLocalization.sec R⁰ (↑x : K)).2 : R)))))) :
                ℤ)))⁻¹
simp_rw₁ :
  (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (if Eq.{u + 1} (α := R) (IsLocalization.sec R⁰ (↑x : K)).1 0 then 0
      else
        exp
          (-(↑(Associates.count (Associates.mk v.asIdeal)
                  (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ (↑x : K)).1})))) :
              ℤ)))
      (if Eq.{u + 1} (α := R) (↑(IsLocalization.sec R⁰ (↑x : K)).2 : R) 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal)
                    (Associates.factors (Associates.mk (Ideal.span {(↑(IsLocalization.sec R⁰ (↑x : K)).2 : R)})))) :
                ℤ)))⁻¹
simp_rw₂ :
  (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    HMul.hMul (α := WithZero (Multiplicative ℤ))
      (exp
        (-(↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ (↑x : K)).1})))) :
            ℤ)))
      (if Eq.{u + 1} (α := R) (↑(IsLocalization.sec R⁰ (↑x : K)).2 : R) 0 then 0
        else
          exp
            (-(↑(Associates.count (Associates.mk v.asIdeal)
                    (Associates.factors (Associates.mk (Ideal.span {(↑(IsLocalization.sec R⁰ (↑x : K)).2 : R)})))) :
                ℤ)))⁻¹
⊢ (↑(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)))))) :
                ℤ)))⁻¹
have simp_rw₃ : (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
  HMul.hMul (α := WithZero (Multiplicative ℤ))
    (exp
      (-(↑(Associates.count (Associates.mk v.asIdeal)
              (Associates.factors (Associates.mk (Ideal.span {(IsLocalization.sec R⁰ (↑x : K)).1})))) :
          ℤ)))
    (exp
        (-(↑(Associates.count (Associates.mk v.asIdeal)
                (Associates.factors (Associates.mk (Ideal.span {(↑(IsLocalization.sec R⁰ (↑x : K)).2 : R)})))) :
            ℤ)))⁻¹
Tactic: 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]