no goals
K : Type ?u.4018726
F : Type ?u.4018729
R : Type u_2
inst✝⁵ : DivisionRing K
Γ₀ : Type u_3
Γ'₀ : Type ?u.4018741
Γ''₀ : Type ?u.4018744
inst✝⁴ : LinearOrderedCommMonoidWithZero Γ''₀
inst✝³ : CommRing R
inst✝² : LinearOrderedCommMonoidWithZero Γ₀
inst✝¹ : LinearOrderedCommMonoidWithZero Γ'₀
v : Valuation R Γ₀
S : Type u_1
inst✝ : CommRing S
f : S →+* R
x : S
⊢ x ∈ supp (comap f v) ↔ x ∈ Ideal.comap f (supp v)
rw [mem_supp_iff, Ideal.mem_comap, mem_supp_iff, comap_apply]