[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
q : R ⧸ J
a b : R
h : Setoid.r a b
⊢ ↑v a = ↑v (b + -(-a + b))
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ J ≤ supp (comap (Ideal.Quotient.mk J) v)
[PROOFSTEP]
rw [comap_supp, ← Ideal.map_le_iff_le_comap]
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v✝ : Valuation R Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ Ideal.map (Ideal.Quotient.mk J) J ≤ supp v
[PROOFSTEP]
simp
[GOAL]
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
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
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)
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
⊢ supp (onQuot v hJ) = Ideal.map (Ideal.Quotient.mk J) (supp v)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
⊢ supp (onQuot v hJ) ≤ Ideal.map (Ideal.Quotient.mk J) (supp v)
[PROOFSTEP]
rintro ⟨x⟩ hx
[GOAL]
case a.mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
x✝ : R ⧸ J
x : R
hx : Quot.mk Setoid.r x ∈ supp (onQuot v hJ)
⊢ Quot.mk Setoid.r x ∈ Ideal.map (Ideal.Quotient.mk J) (supp v)
[PROOFSTEP]
apply Ideal.subset_span
[GOAL]
case a.mk.a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
x✝ : R ⧸ J
x : R
hx : Quot.mk Setoid.r x ∈ supp (onQuot v hJ)
⊢ Quot.mk Setoid.r x ∈ ↑(Ideal.Quotient.mk J) '' ↑(supp v)
[PROOFSTEP]
exact ⟨x, hx, rfl⟩
[GOAL]
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
⊢ Ideal.map (Ideal.Quotient.mk J) (supp v) ≤ supp (onQuot v hJ)
[PROOFSTEP]
rw [Ideal.map_le_iff_le_comap]
[GOAL]
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
⊢ supp v ≤ Ideal.comap (Ideal.Quotient.mk J) (supp (onQuot v hJ))
[PROOFSTEP]
intro x hx
[GOAL]
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ supp v
x : R
hx : x ∈ supp v
⊢ x ∈ Ideal.comap (Ideal.Quotient.mk J) (supp (onQuot v hJ))
[PROOFSTEP]
exact hx
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ supp (onQuot v (_ : supp v ≤ supp v)) = 0
[PROOFSTEP]
rw [supp_quot]
[GOAL]
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
⊢ Ideal.map (Ideal.Quotient.mk (supp v)) (supp v) = 0
[PROOFSTEP]
exact Ideal.map_quotient_self _
