-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem comap_map_eq (f : R →+* S) (s : Subring R) :
    (s.map f).comap f = s ⊔ closure (f ⁻¹' {0})

Proof state:
case a.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
rw [← closure_eq s, ← closure_union, ← add_sub_cancel y x]

Result:
case a.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ closure (↑s ∪ ⇑f ⁻¹' {0})

Proof state:
case a.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ closure (↑s ∪ ⇑f ⁻¹' {0})

Tactic:
exact Subring.add_mem _ (subset_closure <| Or.inl hy) (subset_closure <| Or.inr hxy)

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x : R
hx : x ∈ comap f (map f s)
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
rw [mem_comap, mem_map] at hx

Result:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x : R
hx : ∃ x_1 ∈ s, f x_1 = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Proof state:
case a.hab
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ ⇑f '' (⇑f ⁻¹' {0}) ⊆ ↑(map f s)

Tactic:
exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (s.map f).zero_mem)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : f y = f x
⊢ x - y ∈ ⇑f ⁻¹' {0}

Tactic:
simp [hxy]

Result:
no goals

Proof state:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x : R
hx : ∃ x_1 ∈ s, f x_1 = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
obtain ⟨y, hy, hxy⟩ := hx

Result:
case a.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : f y = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Proof state:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ s ⊔ closure (⇑f ⁻¹' {0}) ≤ comap f (map f s)

Tactic:
rw [← map_le_iff_le_comap, map_sup, f.map_closure]

Result:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (⇑f '' (⇑f ⁻¹' {0})) ≤ map f s

Proof state:
case a.hab
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (⇑f '' (⇑f ⁻¹' {0})) = map f s

Tactic:
rw [sup_eq_left, closure_le]

Result:
case a.hab
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ ⇑f '' (⇑f ⁻¹' {0}) ⊆ ↑(map f s)

Proof state:
case a.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : f y = f x
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]

Result:
case a.intro.intro
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Proof state:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (⇑f '' (⇑f ⁻¹' {0})) ≤ map f s

Tactic:
apply le_of_eq

Result:
case a.hab
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ map f s ⊔ closure (⇑f '' (⇑f ⁻¹' {0})) = map f s

Proof state:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ comap f (map f s) ≤ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
intro x hx

Result:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
x : R
hx : x ∈ comap f (map f s)
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ comap f (map f s) = s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
apply le_antisymm

Result:
case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ comap f (map f s) ≤ s ⊔ closure (⇑f ⁻¹' {0})

case a
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
s : Subring R
⊢ s ⊔ closure (⇑f ⁻¹' {0}) ≤ comap f (map f s)