case w.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
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y
g : RingQuot s →ₐ[S] B
h : AlgHom.comp g (mkAlgHom S s) = f
x✝ : A
⊢ ↑(AlgHom.comp g (mkAlgHom S s)) x✝ = ↑(AlgHom.comp (↑(liftAlgHom S) { val := f, property := w }) (mkAlgHom S s)) 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
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y
g : RingQuot s →ₐ[S] B
h : AlgHom.comp g (mkAlgHom S s) = f
⊢ g = ↑(liftAlgHom S) { val := f, property := w }
ext
no goals
case w.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
f : A →ₐ[S] B
s : A → A → Prop
w : ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y
g : RingQuot s →ₐ[S] B
h : AlgHom.comp g (mkAlgHom S s) = f
x✝ : A
⊢ ↑(AlgHom.comp g (mkAlgHom S s)) x✝ = ↑(AlgHom.comp (↑(liftAlgHom S) { val := f, property := w }) (mkAlgHom S s)) x✝
simp [h]