-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem comap_map_eq (f : A →ₐ[R] B) (S : Subalgebra R A) :
    (S.map f).comap f = S ⊔ Algebra.adjoin R (f ⁻¹' {0})

Proof state:
case a.hab
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ ⇑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:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : x ∈ comap f (map f S)
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
rw [mem_comap, mem_map] at hx

Result:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : ∃ x_1 ∈ S, f x_1 = f x
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : f y = f x
⊢ x - y ∈ ⇑f ⁻¹' {0}

Tactic:
simp [hxy]

Result:
no goals

Proof state:
case a.hab
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ adjoin R (⇑f '' (⇑f ⁻¹' {0})) = map f S

Tactic:
rw [sup_eq_left, Algebra.adjoin_le_iff]

Result:
case a.hab
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ ⇑f '' (⇑f ⁻¹' {0}) ⊆ ↑(map f S)

Proof state:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ comap f (map f S) ≤ S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
intro x hx

Result:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : x ∈ comap f (map f S)
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

Proof state:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ adjoin R (⇑f '' (⇑f ⁻¹' {0})) ≤ map f S

Tactic:
apply le_of_eq

Result:
case a.hab
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ adjoin R (⇑f '' (⇑f ⁻¹' {0})) = map f S

Proof state:
case a.intro.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ adjoin R (↑S ∪ ⇑f ⁻¹' {0})

Tactic:
exact Subalgebra.add_mem _
  (Algebra.subset_adjoin <| Or.inl hy) (Algebra.subset_adjoin <| Or.inr hxy)

Result:
no goals

Proof state:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ S ⊔ adjoin R (⇑f ⁻¹' {0}) ≤ comap f (map f S)

Tactic:
rw [← map_le, Algebra.map_sup, f.map_adjoin]

Result:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ adjoin R (⇑f '' (⇑f ⁻¹' {0})) ≤ map f S

Proof state:
case a.intro.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
rw [← Algebra.adjoin_eq S, ← Algebra.adjoin_union, ← add_sub_cancel y x]

Result:
case a.intro.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ adjoin R (↑S ∪ ⇑f ⁻¹' {0})

Proof state:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x : A
hx : ∃ x_1 ∈ S, f x_1 = f x
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

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

Result:
case a.intro.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : f y = f x
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

Proof state:
case a.intro.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : f y = f x
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

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

Result:
case a.intro.intro
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ comap f (map f S) = S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
apply le_antisymm

Result:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ comap f (map f S) ≤ S ⊔ adjoin R (⇑f ⁻¹' {0})

case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ S ⊔ adjoin R (⇑f ⁻¹' {0}) ≤ comap f (map f S)