case H
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
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : AlgHom.comp f (mkAlgHom S s) = AlgHom.comp g (mkAlgHom S s)
x : RingQuot s
⊢ ↑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
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : AlgHom.comp f (mkAlgHom S s) = AlgHom.comp g (mkAlgHom S s)
⊢ f = g
ext x
case H.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
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : AlgHom.comp f (mkAlgHom S s) = AlgHom.comp g (mkAlgHom S s)
x : A
⊢ ↑f (↑(mkAlgHom S s) x) = ↑g (↑(mkAlgHom S s) x)
case H
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
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : AlgHom.comp f (mkAlgHom S s) = AlgHom.comp g (mkAlgHom S s)
x : RingQuot s
⊢ ↑f x = ↑g x
rcases mkAlgHom_surjective S s x with ⟨x, rfl⟩
no goals
case H.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
B : Type u₄
inst✝¹ : Semiring B
inst✝ : Algebra S B
s : A → A → Prop
f g : RingQuot s →ₐ[S] B
w : AlgHom.comp f (mkAlgHom S s) = AlgHom.comp g (mkAlgHom S s)
x : A
⊢ ↑f (↑(mkAlgHom S s) x) = ↑g (↑(mkAlgHom S s) x)
exact AlgHom.congr_fun w x