-- Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean
theorem valuationOfNeZeroToFun_eq (x : Kˣ) :
    (v.valuationOfNeZeroToFun x : ℤₘ₀) = v.valuation K x

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) = (valuation K v) ↑x

Tactic:
rw [show v.valuation K x = _ * _ by rfl]

Result:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2)⁻¹

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      ↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2)⁻¹

Tactic:
rw [Units.val_inv_eq_inv_val]

Result:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      (↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2))⁻¹

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    (if ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 = 0 then 0
      else
        ↑(Multiplicative.ofAdd
            (-↑((Associates.mk v.asIdeal).count
                  (Associates.mk (Ideal.span {((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1})).factors)))) *
      (if (SubmonoidClass.subtype R⁰) ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2 = 0 then 0
        else
          ↑(Multiplicative.ofAdd
              (-↑((Associates.mk v.asIdeal).count
                    (Associates.mk
                        (Ideal.span
                          {(SubmonoidClass.subtype R⁰)
                              ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2})).factors))))⁻¹

Tactic:
simp_rw [IsLocalization.toLocalizationMap_sec, SubmonoidClass.coe_subtype,
  if_neg <| IsLocalization.sec_fst_ne_zero le_rfl x.ne_zero,
  if_neg (nonZeroDivisors.coe_ne_zero _),
  valuationOfNeZeroToFun, ofAdd_sub, ofAdd_neg, div_inv_eq_mul, WithZero.coe_mul,
  WithZero.coe_inv, inv_inv]

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    ↑v.intValuation.toMonoidWithZeroHom ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 *
      (↑((IsUnit.liftRight ((↑v.intValuation.toMonoidWithZeroHom).restrict R⁰) ⋯)
            ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2))⁻¹

Tactic:
change _ = ite _ _ _ * (ite _ _ _)⁻¹

Result:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) =
    (if ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1 = 0 then 0
      else
        ↑(Multiplicative.ofAdd
            (-↑((Associates.mk v.asIdeal).count
                  (Associates.mk (Ideal.span {((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).1})).factors)))) *
      (if (SubmonoidClass.subtype R⁰) ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2 = 0 then 0
        else
          ↑(Multiplicative.ofAdd
              (-↑((Associates.mk v.asIdeal).count
                    (Associates.mk
                        (Ideal.span
                          {(SubmonoidClass.subtype R⁰)
                              ((IsLocalization.toLocalizationMap R⁰ K).sec ↑x).2})).factors))))⁻¹

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ (valuation K v) ↑x = ?m.4404 * ?m.4407

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
x : Kˣ
⊢ ↑(v.valuationOfNeZeroToFun x) = (valuation K v) ↑x

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 le_rfl x.ne_zero,
  if_neg (nonZeroDivisors.coe_ne_zero _),
  valuationOfNeZeroToFun, ofAdd_sub, ofAdd_neg, div_inv_eq_mul, WithZero.coe_mul,
  WithZero.coe_inv, inv_inv]

Result:
no goals