case mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
r✝ : R ⧸ J
x : R
⊢ ↑(onQuot (comap (Ideal.Quotient.mk J) v) (_ : J ≤ supp (comap (Ideal.Quotient.mk J) v))) (Quot.mk Setoid.r x) =
    ↑v (Quot.mk Setoid.r x)
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ ∀ (r : R ⧸ J), ↑(onQuot (comap (Ideal.Quotient.mk J) v) (_ : J ≤ supp (comap (Ideal.Quotient.mk J) v))) r = ↑v r
rintro ⟨x⟩
no goals
case mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
r✝ : R ⧸ J
x : R
⊢ ↑(onQuot (comap (Ideal.Quotient.mk J) v) (_ : J ≤ supp (comap (Ideal.Quotient.mk J) v))) (Quot.mk Setoid.r x) =
    ↑v (Quot.mk Setoid.r x)
rfl