case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
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 Setoid.r a) =
    ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I)) (Quot.mk Setoid.r b)
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
⊢ Function.Injective ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I))
rintro ⟨a⟩ ⟨b⟩ hab
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
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 Setoid.r a = Quot.mk Setoid.r b
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
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 Setoid.r a) =
    ↑(algebraMap (R ⧸ comap (algebraMap R A) I) (A ⧸ I)) (Quot.mk Setoid.r b)
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
replace hab := Quotient.eq.mp hab
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
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
this : NonAssocRing R := Ring.toNonAssocRing
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
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 Setoid.r a = Quot.mk Setoid.r b
letI : NonAssocRing R := Ring.toNonAssocRing
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
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
this✝ : NonAssocRing R := Ring.toNonAssocRing
this : NonAssocRing A := Ring.toNonAssocRing
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
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
this : NonAssocRing R := Ring.toNonAssocRing
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
letI : NonAssocRing A := Ring.toNonAssocRing
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
this✝ : NonAssocRing R := Ring.toNonAssocRing
this : NonAssocRing A := Ring.toNonAssocRing
hab : ↑(algebraMap R A) (a - b) ∈ I
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
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
this✝ : NonAssocRing R := Ring.toNonAssocRing
this : NonAssocRing A := Ring.toNonAssocRing
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
rw [← RingHom.map_sub] at hab
no goals
case mk.mk
R : Type u
S : Type v
F : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
R₁ : Type ?u.1618416
R₂ : Type ?u.1618419
A : Type u_1
B : Type ?u.1618425
inst✝⁷ : CommSemiring R₁
inst✝⁶ : CommSemiring R₂
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R₁ A
inst✝² : Algebra R₂ A
inst✝¹ : Algebra R₁ B
I : Ideal A
inst✝ : Algebra R A
a₁✝ : R ⧸ comap (algebraMap R A) I
a : R
a₂✝ : R ⧸ comap (algebraMap R A) I
b : R
this✝ : NonAssocRing R := Ring.toNonAssocRing
this : NonAssocRing A := Ring.toNonAssocRing
hab : ↑(algebraMap R A) (a - b) ∈ I
⊢ Quot.mk Setoid.r a = Quot.mk Setoid.r b
exact Quotient.eq.mpr hab