case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ x ∈ comap (algebraMap R S) P ↔ x ∈ p
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
⊢ comap (algebraMap R S) P = p
ext x
case h.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ ↑(algebraMap (R ⧸ p) (S ⧸ P)) (↑(Quotient.mk p) x) = 0 → ↑(Quotient.mk p) x = 0

case h.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ ↑(Quotient.mk p) x = 0 → ↑(algebraMap (R ⧸ p) (S ⧸ P)) (↑(Quotient.mk p) x) = 0
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ x ∈ comap (algebraMap R S) P ↔ x ∈ p
constructor <;>
  rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← Quotient.eq_zero_iff_mem, Quotient.mk_algebraMap,
    IsScalarTower.algebraMap_apply R (R ⧸ p) (S ⧸ P), Quotient.algebraMap_eq]
case h.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
hx : ↑(algebraMap (R ⧸ p) (S ⧸ P)) (↑(Quotient.mk p) x) = 0
⊢ ↑(Quotient.mk p) x = 0
case h.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ ↑(algebraMap (R ⧸ p) (S ⧸ P)) (↑(Quotient.mk p) x) = 0 → ↑(Quotient.mk p) x = 0
intro hx
no goals
case h.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
hx : ↑(algebraMap (R ⧸ p) (S ⧸ P)) (↑(Quotient.mk p) x) = 0
⊢ ↑(Quotient.mk p) x = 0
exact (injective_iff_map_eq_zero (algebraMap (R ⧸ p) (S ⧸ P))).mp h _ hx
case h.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
hx : ↑(Quotient.mk p) x = 0
⊢ ↑(algebraMap (R ⧸ p) (S ⧸ P)) (↑(Quotient.mk p) x) = 0
case h.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
⊢ ↑(Quotient.mk p) x = 0 → ↑(algebraMap (R ⧸ p) (S ⧸ P)) (↑(Quotient.mk p) x) = 0
intro hx
no goals
case h.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing S
f : R →+* S
I J : Ideal S
p : Ideal R
P : Ideal S
inst✝² : Algebra R S
inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)
inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)
h : Function.Injective ↑(algebraMap (R ⧸ p) (S ⧸ P))
x : R
hx : ↑(Quotient.mk p) x = 0
⊢ ↑(algebraMap (R ⧸ p) (S ⧸ P)) (↑(Quotient.mk p) x) = 0
rw [hx, RingHom.map_zero]