-- Module: Mathlib.RingTheory.DedekindDomain.SelmerGroup
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 ℤ))
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)))))) :
                ℤ)))⁻¹
⊢ (↑(v.valuationOfNeZeroToFun x) : WithZero (Multiplicative ℤ)) =
    ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑x : K)

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]

Premises used: WithZero.exp_add, IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun, Units.val_inv_eq_inv_val, sub_eq_add_neg, Units.ne_zero, SubmonoidClass.coe_subtype, IsLocalization.toLocalizationMap_sec, nonZeroDivisors.coe_ne_zero, WithZero.exp, IsLocalization.sec_fst_ne_zero, if_neg, WithZero.exp_neg, ite