-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem algebraMap_quotient_injective {R} [CommRing R] {I : Ideal A} [I.IsTwoSided] [Algebra R A] :
    Function.Injective (algebraMap (R ⧸ I.comap (algebraMap R A)) (A ⧸ I))

Proof state:
case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : (algebraMap R A) a - (algebraMap R A) b ∈ I
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b

Tactic:
rw [← RingHom.map_sub] at hab

Result:
case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : (algebraMap R A) (a - b) ∈ I
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b

Proof state:
case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : (algebraMap R A) (a - b) ∈ I
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b

Tactic:
exact Quotient.eq.mpr hab

Result:
no goals

Proof state:
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
⊢ Injective ⇑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))

Tactic:
rintro ⟨a⟩ ⟨b⟩ hab

Result:
case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab :
  (algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))
      (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a) =
    (algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))
      (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b)
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b

Proof state:
case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab :
  (algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))
      (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a) =
    (algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))
      (Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b)
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b

Tactic:
replace hab := Quotient.eq.mp hab

Result:
case mk.mk
A : Type u_3
inst✝³ : Ring A
R : Type u_5
inst✝² : CommRing R
I : Ideal A
inst✝¹ : I.IsTwoSided
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
hab : (algebraMap R A) a - (algebraMap R A) b ∈ I
⊢ Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) a =
    Quot.mk (⇑(Submodule.quotientRel (comap (algebraMap R A) I))) b