-- Module: Mathlib.RingTheory.DedekindDomain.AdicValuation
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDedekindDomain R
K : Type u_2
inst_2 : Field K
inst_3 : Algebra R K
inst_4 : IsFractionRing R K
v : HeightOneSpectrum R
x : K
hv :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : R
d : ↥v.asIdeal.primeCompl
hnd : HMul.hMul (β := K) x ((algebraMap R K : (a : R) → K) n : K) = (algebraMap R K : (a : R) → K) (↑d : R)
inr :
  (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (↑d : R) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
inr₁ :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (↑(↑d : R) : K) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
inr₂ :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (↑(↑d : R) : K) ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) (↑n : K) :
        WithZero (Multiplicative ℤ))
inr₃ :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (↑(↑d : R) : K) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (x * (↑n : K)) :
      WithZero (Multiplicative ℤ))
inr₄ inr₅ :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (↑(↑d : R) : K) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (↑(↑d : R) : K) :
      WithZero (Multiplicative ℤ))
⊢ 1 ≤
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ)) x :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))

Tactic:
rw [← (v.intValuation_eq_one_iff_mem_primeCompl d).mpr d.prop,
      ← valuation_of_algebraMap (K := K), ← valuation_of_algebraMap (K := K), ← map_mul, hnd]

Premises used: Iff.mpr, IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff_mem_primeCompl, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, map_mul, Subtype.prop, Subtype.val