-- Mathlib/RingTheory/Ideal/Over.lean
theorem comap_eq_of_scalar_tower_quotient [Algebra R S] [Algebra (R ⧸ p) (S ⧸ P)]
    [IsScalarTower R (R ⧸ p) (S ⧸ P)] (h : Function.Injective (algebraMap (R ⧸ p) (S ⧸ P))) :
    comap (algebraMap R S) P = p

Proof state:
case h.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Tactic:
intro hx

Result:
case h.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Proof state:
case h.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Tactic:
exact (injective_iff_map_eq_zero (algebraMap (R ⧸ p) (S ⧸ P))).mp h _ hx

Result:
no goals

Proof state:
case h.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Tactic:
rw [hx, RingHom.map_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Proof state:
case h.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Tactic:
intro hx

Result:
case h.mpr
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Tactic:
constructor

Result:
case h.mp
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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
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

Proof state:
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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

Tactic:
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]

Result:
case h
R : Type u_1
inst✝⁴ : CommRing R
S : Type u_2
inst✝³ : CommRing 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