case w.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
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y
g : RingQuot r →+* T
h : RingHom.comp g (mkRingHom r) = f
x✝ : R
⊢ ↑(RingHom.comp g (mkRingHom r)) x✝ = ↑(RingHom.comp (↑lift { val := f, property := w }) (mkRingHom r)) 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
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y
g : RingQuot r →+* T
h : RingHom.comp g (mkRingHom r) = f
⊢ g = ↑lift { val := f, property := w }
ext
no goals
case w.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
f : R →+* T
r : R → R → Prop
w : ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y
g : RingQuot r →+* T
h : RingHom.comp g (mkRingHom r) = f
x✝ : R
⊢ ↑(RingHom.comp g (mkRingHom r)) x✝ = ↑(RingHom.comp (↑lift { val := f, property := w }) (mkRingHom r)) x✝
simp [h]