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
s : A → A → Prop
this : Function.Surjective fun x => { toQuot := Quot.mk (Rel s) x }
⊢ Function.Surjective ↑(mkAlgHom S s)

case this
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
s : A → A → Prop
⊢ Function.Surjective fun x => { toQuot := Quot.mk (Rel 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
s : A → A → Prop
⊢ Function.Surjective ↑(mkAlgHom S s)
suffices : Function.Surjective fun x ↦ (⟨.mk (Rel s) x⟩ : RingQuot s)
case this.mk.mk
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
s : A → A → Prop
toQuot✝ : Quot (Rel s)
a : A
⊢ ∃ a_1, (fun x => { toQuot := Quot.mk (Rel s) x }) a_1 = { toQuot := Quot.mk (Rel s) a }
case this
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
s : A → A → Prop
⊢ Function.Surjective fun x => { toQuot := Quot.mk (Rel s) x }
rintro ⟨⟨a⟩⟩
no goals
case this.mk.mk
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
s : A → A → Prop
toQuot✝ : Quot (Rel s)
a : A
⊢ ∃ a_1, (fun x => { toQuot := Quot.mk (Rel s) x }) a_1 = { toQuot := Quot.mk (Rel s) a }
use a
no goals
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
s : A → A → Prop
this : Function.Surjective fun x => { toQuot := Quot.mk (Rel s) x }
⊢ Function.Surjective ↑(mkAlgHom S s)
simpa  [mkAlgHom_def, mkRingHom_def]