-- 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 ℤ))
γ : (WithZero (Multiplicative ℤ))ˣ
n d : R
hd_1 : d ∈ v.asIdeal.primeCompl
hd :
  Eq (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hnd :
  HMul.hMul (β := K) x
      ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) : K) =
    (algebraMap R K : (a : R) → K) n
hd' :
  LE.le (α := WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) n : WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) d : WithZero (Multiplicative ℤ))
a : R
hval : (v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) < (↑γ : WithZero (Multiplicative ℤ))
h :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (↑(n - a * d) : K) :
      WithZero (Multiplicative ℤ))
h₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        ((algebraMap R K : (a : R) → K) (n - a * d)) :
      WithZero (Multiplicative ℤ))
h₂ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) (β := K) ((algebraMap R K : (a : R) → K) n : K)
          ((algebraMap R K : (a : R) → K) (a * d) : K)) :
      WithZero (Multiplicative ℤ))
h₃ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) n : K)
          (HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) d : K))) :
      WithZero (Multiplicative ℤ))
h₄ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HMul.hMul (β := K) x
            ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) :
              K) -
          HMul.hMul (α := K) (β := K) ((algebraMap R K : (a : R) → K) a : K) ((algebraMap R K : (a : R) → K) d : K)) :
      WithZero (Multiplicative ℤ))
h₅ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HMul.hMul (β := K) (HSub.hSub (β := K) x ((algebraMap R K : (a : R) → K) a : K))
          ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) :
            K)) :
      WithZero (Multiplicative ℤ))
h₆ :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (HSub.hSub (β := K) x ((algebraMap R K : (a : R) → K) a : K)) :
        WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          ((algebraMap R K : (a : R) → K) (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R)) :
        WithZero (Multiplicative ℤ))
h₇ :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (HSub.hSub (β := K) x ((algebraMap R K : (a : R) → K) a : K)) :
        WithZero (Multiplicative ℤ))
      ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ))
          (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ v.asIdeal.primeCompl) d hd_1) : R) :
        WithZero (Multiplicative ℤ))
h₈ :
  ((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
      (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) =
    HMul.hMul (α := WithZero (Multiplicative ℤ)) (β := WithZero (Multiplicative ℤ))
      (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
          (HSub.hSub (β := K) x ((algebraMap R K : (a : R) → K) a : K)) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))
h₉ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K) x ((algebraMap R K : (a : R) → K) a : K)) :
      WithZero (Multiplicative ℤ))
h₁₀ h₁₁ :
  Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K) x ((algebraMap R K : (a : R) → K) a : K)) :
      WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (β := K) x ((algebraMap R K : (a : R) → K) a : K)) :
      WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((valuation K v : Valuation K (WithZero (Multiplicative ℤ))) : (a : K) → WithZero (Multiplicative ℤ))
        (HSub.hSub (α := K) ((algebraMap R K : (a : R) → K) a : K) x) :
      WithZero (Multiplicative ℤ))
    ((v.intValuation : (a : R) → WithZero (Multiplicative ℤ)) (n - a * d) : WithZero (Multiplicative ℤ))

Tactic:
rw [← valuation_of_algebraMap (K := K), Algebra.cast, map_sub _ n, map_mul, ← hnd, ← sub_mul,
    map_mul, valuation_of_algebraMap, hd, mul_one, Valuation.map_sub_swap]

Premises used: Algebra.cast, IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap, map_sub, Valuation.map_sub_swap, sub_mul, map_mul, mul_one