-- Mathlib/RingTheory/Valuation/Quotient.lean
theorem supp_quot {J : Ideal R} (hJ : J ≤ supp v) :
    supp (v.onQuot hJ) = (supp v).map (Ideal.Quotient.mk J)

Proof state:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ (v.onQuot hJ).supp = Ideal.map (Ideal.Quotient.mk J) v.supp

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ (v.onQuot hJ).supp ≤ Ideal.map (Ideal.Quotient.mk J) v.supp

case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ Ideal.map (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp

Proof state:
case a.mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x✝ : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J)) x ∈ (v.onQuot hJ).supp
⊢ Quot.mk (⇑(Submodule.quotientRel J)) x ∈ Ideal.map (Ideal.Quotient.mk J) v.supp

Tactic:
apply Ideal.subset_span

Result:
case a.mk.a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x✝ : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J)) x ∈ (v.onQuot hJ).supp
⊢ Quot.mk (⇑(Submodule.quotientRel J)) x ∈ ⇑(Ideal.Quotient.mk J) '' ↑v.supp

Proof state:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ Ideal.map (Ideal.Quotient.mk J) v.supp ≤ (v.onQuot hJ).supp

Tactic:
rw [Ideal.map_le_iff_le_comap]

Result:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ v.supp ≤ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp

Proof state:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ (v.onQuot hJ).supp ≤ Ideal.map (Ideal.Quotient.mk J) v.supp

Tactic:
rintro ⟨x⟩ hx

Result:
case a.mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x✝ : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J)) x ∈ (v.onQuot hJ).supp
⊢ Quot.mk (⇑(Submodule.quotientRel J)) x ∈ Ideal.map (Ideal.Quotient.mk J) v.supp

Proof state:
case a.mk.a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x✝ : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J)) x ∈ (v.onQuot hJ).supp
⊢ Quot.mk (⇑(Submodule.quotientRel J)) x ∈ ⇑(Ideal.Quotient.mk J) '' ↑v.supp

Tactic:
exact ⟨x, hx, rfl⟩

Result:
no goals

Proof state:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x : R
hx : x ∈ v.supp
⊢ x ∈ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp

Tactic:
exact hx

Result:
no goals

Proof state:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ v.supp ≤ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp

Tactic:
intro x hx

Result:
case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x : R
hx : x ∈ v.supp
⊢ x ∈ Ideal.comap (Ideal.Quotient.mk J) (v.onQuot hJ).supp