case a
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : RingHom.comp f (mkRingHom r) = RingHom.comp g (mkRingHom r)
x : RingQuot r
⊢ ↑f x = ↑g x
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : RingHom.comp f (mkRingHom r) = RingHom.comp g (mkRingHom r)
⊢ f = g
ext x
case a.intro
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : RingHom.comp f (mkRingHom r) = RingHom.comp g (mkRingHom r)
x : R
⊢ ↑f (↑(mkRingHom r) x) = ↑g (↑(mkRingHom r) x)
case a
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : RingHom.comp f (mkRingHom r) = RingHom.comp g (mkRingHom r)
x : RingQuot r
⊢ ↑f x = ↑g x
rcases mkRingHom_surjective r x with ⟨x, rfl⟩
no goals
case a.intro
R : Type u₁
inst✝⁴ : Semiring R
S : Type u₂
inst✝³ : CommSemiring S
A : Type u₃
inst✝² : Semiring A
inst✝¹ : Algebra S A
r✝ : R → R → Prop
T : Type u₄
inst✝ : Semiring T
r : R → R → Prop
f g : RingQuot r →+* T
w : RingHom.comp f (mkRingHom r) = RingHom.comp g (mkRingHom r)
x : R
⊢ ↑f (↑(mkRingHom r) x) = ↑g (↑(mkRingHom r) x)
exact (RingHom.congr_fun w x : _)