Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Amelia Livingston, Jireh Loreaux
Ported by: Winston Yin

! This file was ported from Lean 3 source module algebra.hom.ring
! leanprover-community/mathlib commit cf9386b56953fb40904843af98b7a80757bbe7f9
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.GroupWithZero.InjSurj
import Mathlib.Algebra.Ring.Basic
import Mathlib.Algebra.Divisibility.Basic
import Mathlib.Data.Pi.Algebra
import Mathlib.Algebra.Hom.Units
import Mathlib.Data.Set.Image

/-!
# Homomorphisms of semirings and rings

This file defines bundled homomorphisms of (non-unital) semirings and rings. As with monoid and
groups, we use the same structure `RingHom a β`, a.k.a. `α →+* β`, for both types of homomorphisms.

## Main definitions

* `NonUnitalRingHom`: Non-unital (semi)ring homomorphisms. Additive monoid homomorphism which
preserve multiplication.
* `RingHom`: (Semi)ring homomorphisms. Monoid homomorphisms which are also additive monoid
homomorphism.

## Notations

* `→ₙ+*`: Non-unital (semi)ring homs
* `→+*`: (Semi)ring homs

## Implementation notes

* There's a coercion from bundled homs to fun, and the canonical notation is to
use the bundled hom as a function via this coercion.

* There is no `SemiringHom` -- the idea is that `RingHom` is used.
The constructor for a `RingHom` between semirings needs a proof of `map_zero`,
`map_one` and `map_add` as well as `map_mul`; a separate constructor
`RingHom.mk'` will construct ring homs between rings from monoid homs given
only a proof that addition is preserved.

## Tags

`RingHom`, `SemiringHom`
-/

open Function

variable {F: Type ?u.52022F α: Type ?u.5α β: Type ?u.52028β γ: Type ?u.11γ : Type _: Type (?u.19512+1)Type _}

/-- Bundled non-unital semiring homomorphisms `α →ₙ+* β`; use this for bundled non-unital ring
homomorphisms too.

When possible, instead of parametrizing results over `(f : α →ₙ+* β)`,
you should parametrize over `(F : Type _) [NonUnitalRingHomClass F α β] (f : F)`.

When you extend this structure, make sure to extend `NonUnitalRingHomClass`. -/
structure NonUnitalRingHom: {α : Type u_1} →
{β : Type u_2} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
(toMulHom : α →ₙ* β) →
MulHom.toFun toMulHom 0 = 0 →
(∀ (x y : α), MulHom.toFun toMulHom (x + y) = MulHom.toFun toMulHom x + MulHom.toFun toMulHom y) →
NonUnitalRingHom α βNonUnitalRingHom (α: Type ?u.26α β: Type ?u.29β : Type _: Type (?u.26+1)Type _) [NonUnitalNonAssocSemiring: Type ?u.32 → Type ?u.32NonUnitalNonAssocSemiring α: Type ?u.26α]
[NonUnitalNonAssocSemiring: Type ?u.35 → Type ?u.35NonUnitalNonAssocSemiring β: Type ?u.29β] extends α: Type ?u.26α →ₙ* β: Type ?u.29β, α: Type ?u.26α →+ β: Type ?u.29β
#align non_unital_ring_hom NonUnitalRingHom: (α : Type u_1) →
(β : Type u_2) → [inst : NonUnitalNonAssocSemiring α] → [inst : NonUnitalNonAssocSemiring β] → Type (maxu_1u_2)NonUnitalRingHom

/-- `α →ₙ+* β` denotes the type of non-unital ring homomorphisms from `α` to `β`. -/
infixr:25 " →ₙ+* " => NonUnitalRingHom: (α : Type u_1) →
(β : Type u_2) → [inst : NonUnitalNonAssocSemiring α] → [inst : NonUnitalNonAssocSemiring β] → Type (maxu_1u_2)NonUnitalRingHom

/-- Reinterpret a non-unital ring homomorphism `f : α →ₙ+* β` as a semigroup
homomorphism `α →ₙ* β`. The `simp`-normal form is `(f : α →ₙ* β)`. -/
add_decl_doc NonUnitalRingHom.toMulHom: {α : Type u_1} →
{β : Type u_2} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →ₙ* βNonUnitalRingHom.toMulHom
#align non_unital_ring_hom.to_mul_hom NonUnitalRingHom.toMulHom: {α : Type u_1} →
{β : Type u_2} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →ₙ* βNonUnitalRingHom.toMulHom

/-- Reinterpret a non-unital ring homomorphism `f : α →ₙ+* β` as an additive
monoid homomorphism `α →+ β`. The `simp`-normal form is `(f : α →+ β)`. -/
{β : Type u_2} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →+ βNonUnitalRingHom.toAddMonoidHom
{β : Type u_2} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →+ βNonUnitalRingHom.toAddMonoidHom

section NonUnitalRingHomClass

/-- `NonUnitalRingHomClass F α β` states that `F` is a type of non-unital (semi)ring
homomorphisms. You should extend this class when you extend `NonUnitalRingHom`. -/
class NonUnitalRingHomClass: {F : Type u_1} →
{α : outParam (Type u_2)} →
{β : outParam (Type u_3)} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[toMulHomClass : MulHomClass F α β] →
(∀ (f : F) (x y : α), ↑f (x + y) = ↑f x + ↑f y) → (∀ (f : F), ↑f 0 = 0) → NonUnitalRingHomClass F α βNonUnitalRingHomClass (F: Type ?u.9159F : Type _: Type (?u.9159+1)Type _) (α: outParam (Type ?u.9163)α β: outParam (Type ?u.9167)β : outParam: Sort ?u.9162 → Sort ?u.9162outParam (Type _: Type (?u.9163+1)Type _)) [NonUnitalNonAssocSemiring: Type ?u.9170 → Type ?u.9170NonUnitalNonAssocSemiring α: outParam (Type ?u.9163)α]
[NonUnitalNonAssocSemiring: Type ?u.9173 → Type ?u.9173NonUnitalNonAssocSemiring β: outParam (Type ?u.9167)β] extends MulHomClass: Type ?u.9180 →
(M : outParam (Type ?u.9179)) →
(N : outParam (Type ?u.9178)) → [inst : Mul M] → [inst : Mul N] → Type (max(max?u.9180?u.9179)?u.9178)MulHomClass F: Type ?u.9159F α: outParam (Type ?u.9163)α β: outParam (Type ?u.9167)β, AddMonoidHomClass: Type ?u.9291 →
(M : outParam (Type ?u.9290)) →
(N : outParam (Type ?u.9289)) →
[inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.9291?u.9290)?u.9289)AddMonoidHomClass F: Type ?u.9159F α: outParam (Type ?u.9163)α β: outParam (Type ?u.9167)β
#align non_unital_ring_hom_class NonUnitalRingHomClass: Type u_1 →
(α : outParam (Type u_2)) →
(β : outParam (Type u_3)) →
[inst : NonUnitalNonAssocSemiring α] → [inst : NonUnitalNonAssocSemiring β] → Type (max(maxu_1u_2)u_3)NonUnitalRingHomClass

variable [NonUnitalNonAssocSemiring: Type ?u.9885 → Type ?u.9885NonUnitalNonAssocSemiring α: Type ?u.9913α] [NonUnitalNonAssocSemiring: Type ?u.9925 → Type ?u.9925NonUnitalNonAssocSemiring β: Type ?u.9879β] [NonUnitalRingHomClass: Type ?u.9893 →
(α : outParam (Type ?u.9892)) →
(β : outParam (Type ?u.9891)) →
[inst : NonUnitalNonAssocSemiring α] →
[inst : NonUnitalNonAssocSemiring β] → Type (max(max?u.9893?u.9892)?u.9891)NonUnitalRingHomClass F: Type ?u.9873F α: Type ?u.11282α β: Type ?u.11285β]

/-- Turn an element of a type `F` satisfying `NonUnitalRingHomClass F α β` into an actual
`NonUnitalRingHom`. This is declared as the default coercion from `F` to `α →ₙ+* β`. -/
@[coe]
def NonUnitalRingHomClass.toNonUnitalRingHom: {F : Type u_1} →
{α : Type u_2} →
{β : Type u_3} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] → [inst_2 : NonUnitalRingHomClass F α β] → F → α →ₙ+* βNonUnitalRingHomClass.toNonUnitalRingHom (f: Ff : F: Type ?u.9910F) : α: Type ?u.9913α →ₙ+* β: Type ?u.9916β :=
{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673{ (f: Ff{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673 : α: Type ?u.9913α{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673 →ₙ* β: Type ?u.9916β{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673), (f: Ff{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673 : α: Type ?u.9913α{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673 →+ β: Type ?u.9916β{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673) { (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673with{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673 }

/-- Any type satisfying `NonUnitalRingHomClass` can be cast into `NonUnitalRingHom` via
`NonUnitalRingHomClass.toNonUnitalRingHom`. -/
instance: {F : Type u_1} →
{α : Type u_2} →
{β : Type u_3} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] → [inst_2 : NonUnitalRingHomClass F α β] → CoeTC F (α →ₙ+* β)instance : CoeTC: Sort ?u.11317 → Sort ?u.11316 → Sort (max(max1?u.11317)?u.11316)CoeTC F: Type ?u.11279F (α: Type ?u.11282α →ₙ+* β: Type ?u.11285β) :=
⟨NonUnitalRingHomClass.toNonUnitalRingHom: {F : Type ?u.11346} →
{α : Type ?u.11345} →
{β : Type ?u.11344} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] → [inst_2 : NonUnitalRingHomClass F α β] → F → α →ₙ+* βNonUnitalRingHomClass.toNonUnitalRingHom⟩

end NonUnitalRingHomClass

namespace NonUnitalRingHom

section coe

variable [NonUnitalNonAssocSemiring: Type ?u.13426 → Type ?u.13426NonUnitalNonAssocSemiring α: Type ?u.11507α] [NonUnitalNonAssocSemiring: Type ?u.11501 → Type ?u.11501NonUnitalNonAssocSemiring β: Type ?u.13939β]

instance: {α : Type u_1} →
{β : Type u_2} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → NonUnitalRingHomClass (α →ₙ+* β) α βinstance : NonUnitalRingHomClass: Type ?u.11524 →
(α : outParam (Type ?u.11523)) →
(β : outParam (Type ?u.11522)) →
[inst : NonUnitalNonAssocSemiring α] →
[inst : NonUnitalNonAssocSemiring β] → Type (max(max?u.11524?u.11523)?u.11522)NonUnitalRingHomClass (α: Type ?u.11507α →ₙ+* β: Type ?u.11510β) α: Type ?u.11507α β: Type ?u.11510β where
coe f: ?m.11680f := f: ?m.11680f.toFun: {M : Type ?u.11693} → {N : Type ?u.11692} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → M → NtoFun
coe_injective' f: ?m.11709f g: ?m.11712g h: ?m.11715h := byGoals accomplished! 🐙
F: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βf, g: α →ₙ+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gcases f: α →ₙ+* βfF: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βg: α →ₙ+* βtoMulHom✝: α →ₙ* βmap_zero'✝: MulHom.toFun toMulHom✝ 0 = 0map_add'✝: ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ yh: (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = (fun f => f.toFun) gmk{ toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
F: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βf, g: α →ₙ+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gcases g: α →ₙ+* βgF: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βtoMulHom✝¹: α →ₙ* βmap_zero'✝¹: MulHom.toFun toMulHom✝¹ 0 = 0map_add'✝¹: ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ ytoMulHom✝: α →ₙ* βmap_zero'✝: MulHom.toFun toMulHom✝ 0 = 0map_add'✝: ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ yh: (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }mk.mk{ toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
F: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βf, g: α →ₙ+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gcongrF: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βtoMulHom✝¹: α →ₙ* βmap_zero'✝¹: MulHom.toFun toMulHom✝¹ 0 = 0map_add'✝¹: ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ ytoMulHom✝: α →ₙ* βmap_zero'✝: MulHom.toFun toMulHom✝ 0 = 0map_add'✝: ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ yh: (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }mk.mk.e_toMulHomtoMulHom✝¹ = toMulHom✝
F: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βf, g: α →ₙ+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gapply FunLike.coe_injective': ∀ {F : Sort ?u.12131} {α : outParam (Sort ?u.12130)} {β : outParam (α → Sort ?u.12129)} [self : FunLike F α β],
Injective FunLike.coeFunLike.coe_injective'F: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βtoMulHom✝¹: α →ₙ* βmap_zero'✝¹: MulHom.toFun toMulHom✝¹ 0 = 0map_add'✝¹: ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ ytoMulHom✝: α →ₙ* βmap_zero'✝: MulHom.toFun toMulHom✝ 0 = 0map_add'✝: ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ yh: (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }mk.mk.e_toMulHom.a↑toMulHom✝¹ = ↑toMulHom✝
F: Type ?u.11504α: Type ?u.11507β: Type ?u.11510γ: Type ?u.11513inst✝¹: NonUnitalNonAssocSemiring αinst✝: NonUnitalNonAssocSemiring βf, g: α →ₙ+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gexact h: (fun f => f.toFun) { toMulHom := toMulHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }hGoals accomplished! 🐙
map_add := NonUnitalRingHom.map_add': ∀ {α : Type ?u.11764} {β : Type ?u.11763} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(self : α →ₙ+* β) (x y : α),
MulHom.toFun self.toMulHom (x + y) = MulHom.toFun self.toMulHom x + MulHom.toFun self.toMulHom yNonUnitalRingHom.map_add'
map_zero := NonUnitalRingHom.map_zero': ∀ {α : Type ?u.11797} {β : Type ?u.11796} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(self : α →ₙ+* β), MulHom.toFun self.toMulHom 0 = 0NonUnitalRingHom.map_zero'
map_mul f: ?m.11728f := f: ?m.11728f.map_mul': ∀ {M : Type ?u.11737} {N : Type ?u.11736} [inst : Mul M] [inst_1 : Mul N] (self : M →ₙ* N) (x y : M),
MulHom.toFun self (x * y) = MulHom.toFun self x * MulHom.toFun self ymap_mul'

-- Porting note:
-- These helper instances are unhelpful in Lean 4, so omitting:
-- /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
-- directly. -/
-- instance : CoeFun (α →ₙ+* β) fun _ => α → β :=
--   ⟨fun f => f.toFun⟩

-- Porting note: removed due to new `coe` in Lean4
#noalign non_unital_ring_hom.to_fun_eq_coe
#noalign non_unital_ring_hom.coe_mk
#noalign non_unital_ring_hom.coe_coe

initialize_simps_projections NonUnitalRingHom: (α : Type u_1) →
(β : Type u_2) → [inst : NonUnitalNonAssocSemiring α] → [inst : NonUnitalNonAssocSemiring β] → Type (maxu_1u_2)NonUnitalRingHom (toFun: (α : Type u_1) →
(β : Type u_2) → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α → βtoFun → apply: (α : Type u_1) →
(β : Type u_2) → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α → βapply)

@[simp]
theorem coe_toMulHom: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β), ↑f.toMulHom = ↑fcoe_toMulHom (f: α →ₙ+* βf : α: Type ?u.12679α →ₙ+* β: Type ?u.12682β) : ⇑f: α →ₙ+* βf.toMulHom: {α : Type ?u.12714} →
{β : Type ?u.12713} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →ₙ* βtoMulHom = f: α →ₙ+* βf :=
rfl: ∀ {α : Sort ?u.13376} {a : α}, a = arfl
#align non_unital_ring_hom.coe_to_mul_hom NonUnitalRingHom.coe_toMulHom: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β), ↑f.toMulHom = ↑fNonUnitalRingHom.coe_toMulHom

@[simp]
theorem coe_mulHom_mk: ∀ {α : Type u_2} {β : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (f : α → β)
(h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : MulHom.toFun { toFun := f, map_mul' := h₁ } 0 = 0)
(h₃ :
∀ (x y : α),
MulHom.toFun { toFun := f, map_mul' := h₁ } (x + y) =         MulHom.toFun { toFun := f, map_mul' := h₁ } x + MulHom.toFun { toFun := f, map_mul' := h₁ } y),
↑{ toMulHom := { toFun := f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_mul' := h₁ }coe_mulHom_mk (f: α → βf : α: Type ?u.13417α → β: Type ?u.13420β) (h₁: ∀ (x y : α), f (x * y) = f x * f yh₁ h₂: ?m.13439h₂ h₃: ∀ (x y : α),
MulHom.toFun { toFun := f, map_mul' := h₁ } (x + y) =     MulHom.toFun { toFun := f, map_mul' := h₁ } x + MulHom.toFun { toFun := f, map_mul' := h₁ } yh₃) :
((⟨⟨f: α → βf, h₁: ?m.13436h₁⟩, h₂: ?m.13439h₂, h₃: ?m.13442h₃⟩ : α: Type ?u.13417α →ₙ+* β: Type ?u.13420β) : α: Type ?u.13417α →ₙ* β: Type ?u.13420β) = ⟨f: α → βf, h₁: ?m.13436h₁⟩ :=
rfl: ∀ {α : Sort ?u.13856} {a : α}, a = arfl
#align non_unital_ring_hom.coe_mul_hom_mk NonUnitalRingHom.coe_mulHom_mk: ∀ {α : Type u_2} {β : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (f : α → β)
(h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : MulHom.toFun { toFun := f, map_mul' := h₁ } 0 = 0)
(h₃ :
∀ (x y : α),
MulHom.toFun { toFun := f, map_mul' := h₁ } (x + y) =         MulHom.toFun { toFun := f, map_mul' := h₁ } x + MulHom.toFun { toFun := f, map_mul' := h₁ } y),
↑{ toMulHom := { toFun := f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_mul' := h₁ }NonUnitalRingHom.coe_mulHom_mk

theorem coe_toAddMonoidHom: ∀ (f : α →ₙ+* β), ↑(toAddMonoidHom f) = ↑fcoe_toAddMonoidHom (f: α →ₙ+* βf : α: Type ?u.13936α →ₙ+* β: Type ?u.13939β) : ⇑f: α →ₙ+* βf.toAddMonoidHom: {α : Type ?u.13971} →
{β : Type ?u.13970} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →+ βtoAddMonoidHom = f: α →ₙ+* βf := rfl: ∀ {α : Sort ?u.15025} {a : α}, a = arfl
#align non_unital_ring_hom.coe_to_add_monoid_hom NonUnitalRingHom.coe_toAddMonoidHom: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]

@[simp]
theorem coe_addMonoidHom_mk: ∀ {α : Type u_2} {β : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (f : α → β)
(h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : MulHom.toFun { toFun := f, map_mul' := h₁ } 0 = 0)
(h₃ :
∀ (x y : α),
MulHom.toFun { toFun := f, map_mul' := h₁ } (x + y) =         MulHom.toFun { toFun := f, map_mul' := h₁ } x + MulHom.toFun { toFun := f, map_mul' := h₁ } y),
↑{ toMulHom := { toFun := f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } =     { toZeroHom := { toFun := f, map_zero' := h₂ }, map_add' := h₃ }coe_addMonoidHom_mk (f: α → βf : α: Type ?u.15045α → β: Type ?u.15048β) (h₁: ∀ (x y : α), f (x * y) = f x * f yh₁ h₂: ?m.15067h₂ h₃: ?m.15070h₃) :
((⟨⟨f: α → βf, h₁: ?m.15064h₁⟩, h₂: ?m.15067h₂, h₃: ?m.15070h₃⟩ : α: Type ?u.15045α →ₙ+* β: Type ?u.15048β) : α: Type ?u.15045α →+ β: Type ?u.15048β) = ⟨⟨f: α → βf, h₂: ?m.15067h₂⟩, h₃: ?m.15070h₃⟩ :=
rfl: ∀ {α : Sort ?u.16183} {a : α}, a = arfl
#align non_unital_ring_hom.coe_add_monoid_hom_mk NonUnitalRingHom.coe_addMonoidHom_mk: ∀ {α : Type u_2} {β : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (f : α → β)
(h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : MulHom.toFun { toFun := f, map_mul' := h₁ } 0 = 0)
(h₃ :
∀ (x y : α),
MulHom.toFun { toFun := f, map_mul' := h₁ } (x + y) =         MulHom.toFun { toFun := f, map_mul' := h₁ } x + MulHom.toFun { toFun := f, map_mul' := h₁ } y),
↑{ toMulHom := { toFun := f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } =     { toZeroHom := { toFun := f, map_zero' := h₂ }, map_add' := h₃ }NonUnitalRingHom.coe_addMonoidHom_mk

/-- Copy of a `RingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
protected def copy: {α : Type u_1} →
{β : Type u_2} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] → (f : α →ₙ+* β) → (f' : α → β) → f' = ↑f → α →ₙ+* βcopy (f: α →ₙ+* βf : α: Type ?u.16269α →ₙ+* β: Type ?u.16272β) (f': α → βf' : α: Type ?u.16269α → β: Type ?u.16272β) (h: f' = ↑fh : f': α → βf' = f: α →ₙ+* βf) : α: Type ?u.16269α →ₙ+* β: Type ?u.16272β :=
{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337{ f: α →ₙ+* βf{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337.toMulHom: {α : Type ?u.16812} →
{β : Type ?u.16811} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →ₙ* βtoMulHom{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337.copy: {M : Type ?u.16818} →
{N : Type ?u.16817} → [inst : Mul M] → [inst_1 : Mul N] → (f : M →ₙ* N) → (f' : M → N) → f' = ↑f → M →ₙ* Ncopy{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337 f': α → βf'{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337 h: f' = ↑fh{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337, f: α →ₙ+* βf{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337.toAddMonoidHom: {α : Type ?u.16936} →
{β : Type ?u.16935} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →+ βtoAddMonoidHom{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337.copy: {M : Type ?u.16942} →
{N : Type ?u.16941} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (f : M →+ N) → (f' : M → N) → f' = ↑f → M →+ Ncopy{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337 f': α → βf'{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337 h: f' = ↑fh{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337 { f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337with{ f.toMulHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.17336 →ₙ+* ?m.17337 }
#align non_unital_ring_hom.copy NonUnitalRingHom.copy: {α : Type u_1} →
{β : Type u_2} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] → (f : α →ₙ+* β) → (f' : α → β) → f' = ↑f → α →ₙ+* βNonUnitalRingHom.copy

@[simp]
theorem coe_copy: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β) (f' : α → β) (h : f' = ↑f), ↑(NonUnitalRingHom.copy f f' h) = f'coe_copy (f: α →ₙ+* βf : α: Type ?u.17800α →ₙ+* β: Type ?u.17803β) (f': α → βf' : α: Type ?u.17800α → β: Type ?u.17803β) (h: f' = ↑fh : f': α → βf' = f: α →ₙ+* βf) : ⇑(f: α →ₙ+* βf.copy: {α : Type ?u.18334} →
{β : Type ?u.18333} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] → (f : α →ₙ+* β) → (f' : α → β) → f' = ↑f → α →ₙ+* βcopy f': α → βf' h: f' = ↑fh) = f': α → βf' :=
rfl: ∀ {α : Sort ?u.18525} {a : α}, a = arfl
#align non_unital_ring_hom.coe_copy NonUnitalRingHom.coe_copy: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β) (f' : α → β) (h : f' = ↑f), ↑(NonUnitalRingHom.copy f f' h) = f'NonUnitalRingHom.coe_copy

theorem copy_eq: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β) (f' : α → β) (h : f' = ↑f), NonUnitalRingHom.copy f f' h = fcopy_eq (f: α →ₙ+* βf : α: Type ?u.18581α →ₙ+* β: Type ?u.18584β) (f': α → βf' : α: Type ?u.18581α → β: Type ?u.18584β) (h: f' = ↑fh : f': α → βf' = f: α →ₙ+* βf) : f: α →ₙ+* βf.copy: {α : Type ?u.19115} →
{β : Type ?u.19114} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] → (f : α →ₙ+* β) → (f' : α → β) → f' = ↑f → α →ₙ+* βcopy f': α → βf' h: f' = ↑fh = f: α →ₙ+* βf :=
FunLike.ext': ∀ {F : Sort ?u.19140} {α : Sort ?u.19138} {β : α → Sort ?u.19139} [i : FunLike F α β] {f g : F}, ↑f = ↑g → f = gFunLike.ext' h: f' = ↑fh
#align non_unital_ring_hom.copy_eq NonUnitalRingHom.copy_eq: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β) (f' : α → β) (h : f' = ↑f), NonUnitalRingHom.copy f f' h = fNonUnitalRingHom.copy_eq

end coe

section

variable [NonUnitalNonAssocSemiring: Type ?u.20784 → Type ?u.20784NonUnitalNonAssocSemiring α: Type ?u.19451α] [NonUnitalNonAssocSemiring: Type ?u.19463 → Type ?u.19463NonUnitalNonAssocSemiring β: Type ?u.19454β]
variable (f: α →ₙ+* βf : α: Type ?u.21315α →ₙ+* β: Type ?u.20778β) {x: αx y: αy : α: Type ?u.19469α}

@[ext]
theorem ext: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext ⦃f: α →ₙ+* βf g: α →ₙ+* βg : α: Type ?u.19509α →ₙ+* β: Type ?u.19512β⦄ : (∀ x: ?m.19572x, f: α →ₙ+* βf x: ?m.19572x = g: α →ₙ+* βg x: ?m.19572x) → f: α →ₙ+* βf = g: α →ₙ+* βg :=
FunLike.ext: ∀ {F : Sort ?u.19936} {α : Sort ?u.19937} {β : α → Sort ?u.19935} [i : FunLike F α β] (f g : F),
(∀ (x : α), ↑f x = ↑g x) → f = gFunLike.ext _: ?m.19938_ _: ?m.19938_
#align non_unital_ring_hom.ext NonUnitalRingHom.ext: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gNonUnitalRingHom.ext

theorem ext_iff: ∀ {f g : α →ₙ+* β}, f = g ↔ ∀ (x : α), ↑f x = ↑g xext_iff {f: α →ₙ+* βf g: α →ₙ+* βg : α: Type ?u.20149α →ₙ+* β: Type ?u.20152β} : f: α →ₙ+* βf = g: α →ₙ+* βg ↔ ∀ x: ?m.20217x, f: α →ₙ+* βf x: ?m.20217x = g: α →ₙ+* βg x: ?m.20217x :=
FunLike.ext_iff: ∀ {F : Sort ?u.20574} {α : Sort ?u.20576} {β : α → Sort ?u.20575} [i : FunLike F α β] {f g : F},
f = g ↔ ∀ (x : α), ↑f x = ↑g xFunLike.ext_iff
#align non_unital_ring_hom.ext_iff NonUnitalRingHom.ext_iff: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
{f g : α →ₙ+* β}, f = g ↔ ∀ (x : α), ↑f x = ↑g xNonUnitalRingHom.ext_iff

@[simp]
theorem mk_coe: ∀ (f : α →ₙ+* β) (h₁ : ∀ (x y : α), ↑f (x * y) = ↑f x * ↑f y) (h₂ : MulHom.toFun { toFun := ↑f, map_mul' := h₁ } 0 = 0)
(h₃ :
∀ (x y : α),
MulHom.toFun { toFun := ↑f, map_mul' := h₁ } (x + y) =         MulHom.toFun { toFun := ↑f, map_mul' := h₁ } x + MulHom.toFun { toFun := ↑f, map_mul' := h₁ } y),
{ toMulHom := { toFun := ↑f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = fmk_coe (f: α →ₙ+* βf : α: Type ?u.20775α →ₙ+* β: Type ?u.20778β) (h₁: ∀ (x y : α), ↑f (x * y) = ↑f x * ↑f yh₁ h₂: MulHom.toFun { toFun := ↑f, map_mul' := h₁ } 0 = 0h₂ h₃: ?m.20836h₃) : NonUnitalRingHom.mk: {α : Type ?u.20841} →
{β : Type ?u.20840} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
(toMulHom : α →ₙ* β) →
MulHom.toFun toMulHom 0 = 0 →
(∀ (x y : α), MulHom.toFun toMulHom (x + y) = MulHom.toFun toMulHom x + MulHom.toFun toMulHom y) → α →ₙ+* βNonUnitalRingHom.mk (MulHom.mk: {M : Type ?u.20847} →
{N : Type ?u.20846} →
[inst : Mul M] → [inst_1 : Mul N] → (toFun : M → N) → (∀ (x y : M), toFun (x * y) = toFun x * toFun y) → M →ₙ* NMulHom.mk f: α →ₙ+* βf h₁: ?m.20830h₁) h₂: ?m.20833h₂ h₃: ?m.20836h₃ = f: α →ₙ+* βf :=
ext: ∀ {α : Type ?u.21202} {β : Type ?u.21203} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext fun _: ?m.21230_ => rfl: ∀ {α : Sort ?u.21232} {a : α}, a = arfl
#align non_unital_ring_hom.mk_coe NonUnitalRingHom.mk_coe: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β) (h₁ : ∀ (x y : α), ↑f (x * y) = ↑f x * ↑f y) (h₂ : MulHom.toFun { toFun := ↑f, map_mul' := h₁ } 0 = 0)
(h₃ :
∀ (x y : α),
MulHom.toFun { toFun := ↑f, map_mul' := h₁ } (x + y) =         MulHom.toFun { toFun := ↑f, map_mul' := h₁ } x + MulHom.toFun { toFun := ↑f, map_mul' := h₁ } y),
{ toMulHom := { toFun := ↑f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = fNonUnitalRingHom.mk_coe

theorem coe_addMonoidHom_injective: Injective fun f => ↑fcoe_addMonoidHom_injective : Injective: {α : Sort ?u.21353} → {β : Sort ?u.21352} → (α → β) → PropInjective fun f: α →ₙ+* βf : α: Type ?u.21315α →ₙ+* β: Type ?u.21318β => (f: α →ₙ+* βf : α: Type ?u.21315α →+ β: Type ?u.21318β) :=
fun _: ?m.21923_ _: ?m.21926_ h: ?m.21929h => ext: ∀ {α : Type ?u.21931} {β : Type ?u.21932} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext <| FunLike.congr_fun: ∀ {F : Sort ?u.21958} {α : Sort ?u.21960} {β : α → Sort ?u.21959} [i : FunLike F α β] {f g : F},
f = g → ∀ (x : α), ↑f x = ↑g xFunLike.congr_fun (F := α: Type ?u.21315α →+ β: Type ?u.21318β) h: ?m.21929h
#align non_unital_ring_hom.coe_add_monoid_hom_injective NonUnitalRingHom.coe_addMonoidHom_injective: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β],

set_option linter.deprecated false in
theorem coe_mulHom_injective: Injective fun f => ↑fcoe_mulHom_injective : Injective: {α : Sort ?u.22940} → {β : Sort ?u.22939} → (α → β) → PropInjective fun f: α →ₙ+* βf : α: Type ?u.22902α →ₙ+* β: Type ?u.22905β => (f: α →ₙ+* βf : α: Type ?u.22902α →ₙ* β: Type ?u.22905β) := fun _: ?m.23211_ _: ?m.23214_ h: ?m.23217h =>
ext: ∀ {α : Type ?u.23219} {β : Type ?u.23220} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext <| MulHom.congr_fun: ∀ {M : Type ?u.23246} {N : Type ?u.23247} [inst : Mul M] [inst_1 : Mul N] {f g : M →ₙ* N},
f = g → ∀ (x : M), ↑f x = ↑g xMulHom.congr_fun h: ?m.23217h
#align non_unital_ring_hom.coe_mul_hom_injective NonUnitalRingHom.coe_mulHom_injective: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β],
Injective fun f => ↑fNonUnitalRingHom.coe_mulHom_injective

end

variable [NonUnitalNonAssocSemiring: Type ?u.29984 → Type ?u.29984NonUnitalNonAssocSemiring α: Type ?u.23437α] [NonUnitalNonAssocSemiring: Type ?u.29236 → Type ?u.29236NonUnitalNonAssocSemiring β: Type ?u.23440β]

/-- The identity non-unital ring homomorphism from a non-unital semiring to itself. -/
protected def id: (α : Type u_1) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αid (α: Type ?u.23470α : Type _: Type (?u.23470+1)Type _) [NonUnitalNonAssocSemiring: Type ?u.23473 → Type ?u.23473NonUnitalNonAssocSemiring α: Type ?u.23470α] : α: Type ?u.23470α →ₙ+* α: Type ?u.23470α := byGoals accomplished! 🐙
F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αα →ₙ+* αrefine' { toFun := id: {α : Sort ?u.23562} → α → αid.. }F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αrefine'_1∀ (x y : α), id (x * y) = id x * id yF: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αrefine'_2MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } 0 = 0F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αrefine'_3∀ (x y : α),
MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } (x + y) =     MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } x + MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } y F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αα →ₙ+* α<;>F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αrefine'_1∀ (x y : α), id (x * y) = id x * id yF: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αrefine'_2MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } 0 = 0F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αrefine'_3∀ (x y : α),
MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } (x + y) =     MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } x + MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } y F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αα →ₙ+* αintrosF: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αrefine'_2MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } 0 = 0 F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αα →ₙ+* α<;>F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αx✝, y✝: αrefine'_1id (x✝ * y✝) = id x✝ * id y✝F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αrefine'_2MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } 0 = 0F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αx✝, y✝: αrefine'_3MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } (x✝ + y✝) =   MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } x✝ +     MulHom.toFun { toFun := id, map_mul' := (_ : ∀ (x y : α), id (x * y) = id x * id y) } y✝ F: Type ?u.23452α✝: Type ?u.23455β: Type ?u.23458γ: Type ?u.23461inst✝²: NonUnitalNonAssocSemiring α✝inst✝¹: NonUnitalNonAssocSemiring βα: Type ?u.23470inst✝: NonUnitalNonAssocSemiring αα →ₙ+* αrflGoals accomplished! 🐙
#align non_unital_ring_hom.id NonUnitalRingHom.id: (α : Type u_1) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αNonUnitalRingHom.id

instance: {α : Type u_1} →
{β : Type u_2} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → Zero (α →ₙ+* β)instance : Zero: Type ?u.23649 → Type ?u.23649Zero (α: Type ?u.23634α →ₙ+* β: Type ?u.23637β) :=
⟨{ toFun := 0: ?m.237890, map_mul' := fun _: ?m.23981_ _: ?m.23984_ => (mul_zero: ∀ {M₀ : Type ?u.23986} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0mul_zero (0: ?m.239910 : β: Type ?u.23637β)).symm: ∀ {α : Sort ?u.24127} {a b : α}, a = b → b = asymm, map_zero' := rfl: ∀ {α : Sort ?u.24149} {a : α}, a = arfl,
map_add' := fun _: ?m.24154_ _: ?m.24157_ => (add_zero: ∀ {M : Type ?u.24159} [inst : AddZeroClass M] (a : M), a + 0 = aadd_zero (0: ?m.241640 : β: Type ?u.23637β)).symm: ∀ {α : Sort ?u.24346} {a b : α}, a = b → b = asymm }⟩

instance: {α : Type u_1} →
{β : Type u_2} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → Inhabited (α →ₙ+* β)instance : Inhabited: Sort ?u.24516 → Sort (max1?u.24516)Inhabited (α: Type ?u.24501α →ₙ+* β: Type ?u.24504β) :=
⟨0: ?m.245400⟩

@[simp]
theorem coe_zero: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β], ↑0 = 0coe_zero : ⇑(0: ?m.247030 : α: Type ?u.24669α →ₙ+* β: Type ?u.24672β) = 0: ?m.249240 :=
rfl: ∀ {α : Sort ?u.25384} {a : α}, a = arfl
#align non_unital_ring_hom.coe_zero NonUnitalRingHom.coe_zero: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β], ↑0 = 0NonUnitalRingHom.coe_zero

@[simp]
theorem zero_apply: ∀ {α : Type u_2} {β : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (x : α),
↑0 x = 0zero_apply (x: αx : α: Type ?u.25429α) : (0: ?m.254650 : α: Type ?u.25429α →ₙ+* β: Type ?u.25432β) x: αx = 0: ?m.256860 :=
rfl: ∀ {α : Sort ?u.25906} {a : α}, a = arfl
#align non_unital_ring_hom.zero_apply NonUnitalRingHom.zero_apply: ∀ {α : Type u_2} {β : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β] (x : α),
↑0 x = 0NonUnitalRingHom.zero_apply

@[simp]
theorem id_apply: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x : α), ↑(NonUnitalRingHom.id α) x = xid_apply (x: αx : α: Type ?u.25950α) : NonUnitalRingHom.id: (α : Type ?u.25968) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αNonUnitalRingHom.id α: Type ?u.25950α x: αx = x: αx :=
rfl: ∀ {α : Sort ?u.26157} {a : α}, a = arfl
#align non_unital_ring_hom.id_apply NonUnitalRingHom.id_apply: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x : α), ↑(NonUnitalRingHom.id α) x = xNonUnitalRingHom.id_apply

@[simp]
theorem coe_addMonoidHom_id: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], ↑(NonUnitalRingHom.id α) = AddMonoidHom.id αcoe_addMonoidHom_id : (NonUnitalRingHom.id: (α : Type ?u.26413) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αNonUnitalRingHom.id α: Type ?u.26193α : α: Type ?u.26193α →+ α: Type ?u.26193α) = AddMonoidHom.id: (M : Type ?u.26548) → [inst : AddZeroClass M] → M →+ MAddMonoidHom.id α: Type ?u.26193α :=
rfl: ∀ {α : Sort ?u.26552} {a : α}, a = arfl

@[simp]
theorem coe_mulHom_id: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], ↑(NonUnitalRingHom.id α) = MulHom.id αcoe_mulHom_id : (NonUnitalRingHom.id: (α : Type ?u.26670) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αNonUnitalRingHom.id α: Type ?u.26599α : α: Type ?u.26599α →ₙ* α: Type ?u.26599α) = MulHom.id: (M : Type ?u.26806) → [inst : Mul M] → M →ₙ* MMulHom.id α: Type ?u.26599α :=
rfl: ∀ {α : Sort ?u.26810} {a : α}, a = arfl
#align non_unital_ring_hom.coe_mul_hom_id NonUnitalRingHom.coe_mulHom_id: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], ↑(NonUnitalRingHom.id α) = MulHom.id αNonUnitalRingHom.coe_mulHom_id

variable [NonUnitalNonAssocSemiring: Type ?u.33500 → Type ?u.33500NonUnitalNonAssocSemiring γ: Type ?u.26857γ]

/-- Composition of non-unital ring homomorphisms is a non-unital ring homomorphism. -/
def comp: (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp (g: β →ₙ+* γg : β: Type ?u.26875β →ₙ+* γ: Type ?u.26878γ) (f: α →ₙ+* βf : α: Type ?u.26872α →ₙ+* β: Type ?u.26875β) : α: Type ?u.26872α →ₙ+* γ: Type ?u.26878γ :=
{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765{ g: β →ₙ+* γg{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765.toMulHom: {α : Type ?u.26930} →
{β : Type ?u.26929} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →ₙ* βtoMulHom{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765.comp: {M : Type ?u.26941} →
{N : Type ?u.26940} →
{P : Type ?u.26939} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* Pcomp{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765 f: α →ₙ+* βf{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765.toMulHom: {α : Type ?u.27075} →
{β : Type ?u.27074} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →ₙ* βtoMulHom{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765, g: β →ₙ+* γg{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765.toAddMonoidHom: {α : Type ?u.27148} →
{β : Type ?u.27147} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →+ βtoAddMonoidHom{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765.comp: {M : Type ?u.27155} →
{N : Type ?u.27154} →
{P : Type ?u.27153} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ Pcomp{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765 f: α →ₙ+* βf{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765.toAddMonoidHom: {α : Type ?u.27553} →
{β : Type ?u.27552} →
[inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →+ βtoAddMonoidHom{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765 { g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765with{ g.toMulHom.comp f.toMulHom, g.toAddMonoidHom.comp f.toAddMonoidHom with }: ?m.27764 →ₙ+* ?m.27765 }
#align non_unital_ring_hom.comp NonUnitalRingHom.comp: {α : Type u_1} →
{β : Type u_2} →
{γ : Type u_3} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γNonUnitalRingHom.comp

/-- Composition of non-unital ring homomorphisms is associative. -/
theorem comp_assoc: ∀ {δ : Type u_1} {x : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ),
comp (comp h g) f = comp h (comp g f)comp_assoc {δ: ?m.28257δ} {_: NonUnitalNonAssocSemiring δ_ : NonUnitalNonAssocSemiring: Type ?u.28260 → Type ?u.28260NonUnitalNonAssocSemiring δ: ?m.28257δ} (f: α →ₙ+* βf : α: Type ?u.28239α →ₙ+* β: Type ?u.28242β) (g: β →ₙ+* γg : β: Type ?u.28242β →ₙ+* γ: Type ?u.28245γ)
(h: γ →ₙ+* δh : γ: Type ?u.28245γ →ₙ+* δ: ?m.28257δ) : (h: γ →ₙ+* δh.comp: {α : Type ?u.28307} →
{β : Type ?u.28306} →
{γ : Type ?u.28305} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp g: β →ₙ+* γg).comp: {α : Type ?u.28336} →
{β : Type ?u.28335} →
{γ : Type ?u.28334} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf = h: γ →ₙ+* δh.comp: {α : Type ?u.28365} →
{β : Type ?u.28364} →
{γ : Type ?u.28363} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp (g: β →ₙ+* γg.comp: {α : Type ?u.28382} →
{β : Type ?u.28381} →
{γ : Type ?u.28380} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf) :=
rfl: ∀ {α : Sort ?u.28426} {a : α}, a = arfl
#align non_unital_ring_hom.comp_assoc NonUnitalRingHom.comp_assoc: ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {δ : Type u_1}
{x : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ), comp (comp h g) f = comp h (comp g f)NonUnitalRingHom.comp_assoc

@[simp]
theorem coe_comp: ∀ (g : β →ₙ+* γ) (f : α →ₙ+* β), ↑(comp g f) = ↑g ∘ ↑fcoe_comp (g: β →ₙ+* γg : β: Type ?u.28511β →ₙ+* γ: Type ?u.28514γ) (f: α →ₙ+* βf : α: Type ?u.28508α →ₙ+* β: Type ?u.28511β) : ⇑(g: β →ₙ+* γg.comp: {α : Type ?u.28559} →
{β : Type ?u.28558} →
{γ : Type ?u.28557} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf) = g: β →ₙ+* γg ∘ f: α →ₙ+* βf :=
rfl: ∀ {α : Sort ?u.29159} {a : α}, a = arfl
#align non_unital_ring_hom.coe_comp NonUnitalRingHom.coe_comp: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β),
↑(comp g f) = ↑g ∘ ↑fNonUnitalRingHom.coe_comp

@[simp]
theorem comp_apply: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α),
↑(comp g f) x = ↑g (↑f x)comp_apply (g: β →ₙ+* γg : β: Type ?u.29227β →ₙ+* γ: Type ?u.29230γ) (f: α →ₙ+* βf : α: Type ?u.29224α →ₙ+* β: Type ?u.29227β) (x: αx : α: Type ?u.29224α) : g: β →ₙ+* γg.comp: {α : Type ?u.29277} →
{β : Type ?u.29276} →
{γ : Type ?u.29275} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf x: αx = g: β →ₙ+* γg (f: α →ₙ+* βf x: αx) :=
rfl: ∀ {α : Sort ?u.29863} {a : α}, a = arfl
#align non_unital_ring_hom.comp_apply NonUnitalRingHom.comp_apply: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α),
↑(comp g f) x = ↑g (↑f x)NonUnitalRingHom.comp_apply
variable (g: β →ₙ+* γg : β: Type ?u.29927β →ₙ+* γ: Type ?u.29930γ) (f: α →ₙ+* βf : α: Type ?u.29924α →ₙ+* β: Type ?u.29978β)

@[simp]
theorem coe_comp_addMonoidHom: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β),
{ toZeroHom := { toFun := ↑g ∘ ↑f, map_zero' := (_ : MulHom.toFun (comp g f).toMulHom 0 = 0) },
(_ :
∀ (x y : α),
MulHom.toFun (comp g f).toMulHom (x + y) =               MulHom.toFun (comp g f).toMulHom x + MulHom.toFun (comp g f).toMulHom y) } =     AddMonoidHom.comp ↑g ↑fcoe_comp_addMonoidHom (g: β →ₙ+* γg : β: Type ?u.29978β →ₙ+* γ: Type ?u.29981γ) (f: α →ₙ+* βf : α: Type ?u.29975α →ₙ+* β: Type ?u.29978β) :
AddMonoidHom.mk: {M : Type ?u.30055} →
{N : Type ?u.30054} →
(toZeroHom : ZeroHom M N) →
(∀ (x y : M), ZeroHom.toFun toZeroHom (x + y) = ZeroHom.toFun toZeroHom x + ZeroHom.toFun toZeroHom y) →
M →+ NAddMonoidHom.mk ⟨g: β →ₙ+* γg ∘ f: α →ₙ+* βf, (g: β →ₙ+* γg.comp: {α : Type ?u.30527} →
{β : Type ?u.30526} →
{γ : Type ?u.30525} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf).map_zero': ∀ {α : Type ?u.30547} {β : Type ?u.30546} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(self : α →ₙ+* β), MulHom.toFun self.toMulHom 0 = 0map_zero'⟩ (g: β →ₙ+* γg.comp: {α : Type ?u.31262} →
{β : Type ?u.31261} →
{γ : Type ?u.31260} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf).map_add': ∀ {α : Type ?u.31282} {β : Type ?u.31281} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(self : α →ₙ+* β) (x y : α),
MulHom.toFun self.toMulHom (x + y) = MulHom.toFun self.toMulHom x + MulHom.toFun self.toMulHom ymap_add' = (g: β →ₙ+* γg : β: Type ?u.29978β →+ γ: Type ?u.29981γ).comp: {M : Type ?u.31627} →
{N : Type ?u.31626} →
{P : Type ?u.31625} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [inst_2 : AddZeroClass P] → (N →+ P) → (M →+ N) → M →+ Pcomp f: α →ₙ+* βf :=
rfl: ∀ {α : Sort ?u.32007} {a : α}, a = arfl
#align non_unital_ring_hom.coe_comp_add_monoid_hom NonUnitalRingHom.coe_comp_addMonoidHom: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β),
{ toZeroHom := { toFun := ↑g ∘ ↑f, map_zero' := (_ : MulHom.toFun (comp g f).toMulHom 0 = 0) },
(_ :
∀ (x y : α),
MulHom.toFun (comp g f).toMulHom (x + y) =               MulHom.toFun (comp g f).toMulHom x + MulHom.toFun (comp g f).toMulHom y) } =     AddMonoidHom.comp ↑g ↑fNonUnitalRingHom.coe_comp_addMonoidHom

@[simp]
theorem coe_comp_mulHom: ∀ (g : β →ₙ+* γ) (f : α →ₙ+* β),
{ toFun := ↑g ∘ ↑f,
map_mul' :=
(_ :
∀ (x y : α),
MulHom.toFun (comp g f).toMulHom (x * y) =               MulHom.toFun (comp g f).toMulHom x * MulHom.toFun (comp g f).toMulHom y) } =     MulHom.comp ↑g ↑fcoe_comp_mulHom (g: β →ₙ+* γg : β: Type ?u.32117β →ₙ+* γ: Type ?u.32120γ) (f: α →ₙ+* βf : α: Type ?u.32114α →ₙ+* β: Type ?u.32117β) :
MulHom.mk: {M : Type ?u.32194} →
{N : Type ?u.32193} →
[inst : Mul M] → [inst_1 : Mul N] → (toFun : M → N) → (∀ (x y : M), toFun (x * y) = toFun x * toFun y) → M →ₙ* NMulHom.mk (g: β →ₙ+* γg ∘ f: α →ₙ+* βf) (g: β →ₙ+* γg.comp: {α : Type ?u.32592} →
{β : Type ?u.32591} →
{γ : Type ?u.32590} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf).map_mul': ∀ {M : Type ?u.32622} {N : Type ?u.32621} [inst : Mul M] [inst_1 : Mul N] (self : M →ₙ* N) (x y : M),
MulHom.toFun self (x * y) = MulHom.toFun self x * MulHom.toFun self ymap_mul' = (g: β →ₙ+* γg : β: Type ?u.32117β →ₙ* γ: Type ?u.32120γ).comp: {M : Type ?u.32951} →
{N : Type ?u.32950} →
{P : Type ?u.32949} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → (N →ₙ* P) → (M →ₙ* N) → M →ₙ* Pcomp f: α →ₙ+* βf :=
rfl: ∀ {α : Sort ?u.33390} {a : α}, a = arfl
#align non_unital_ring_hom.coe_comp_mul_hom NonUnitalRingHom.coe_comp_mulHom: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β),
{ toFun := ↑g ∘ ↑f,
map_mul' :=
(_ :
∀ (x y : α),
MulHom.toFun (comp g f).toMulHom (x * y) =               MulHom.toFun (comp g f).toMulHom x * MulHom.toFun (comp g f).toMulHom y) } =     MulHom.comp ↑g ↑fNonUnitalRingHom.coe_comp_mulHom

@[simp]
theorem comp_zero: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ), comp g 0 = 0comp_zero (g: β →ₙ+* γg : β: Type ?u.33488β →ₙ+* γ: Type ?u.33491γ) : g: β →ₙ+* γg.comp: {α : Type ?u.33554} →
{β : Type ?u.33553} →
{γ : Type ?u.33552} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp (0: ?m.335850 : α: Type ?u.33485α →ₙ+* β: Type ?u.33488β) = 0: ?m.336270 := byGoals accomplished! 🐙
F: Type ?u.33482α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γcomp g 0 = 0extF: Type ?u.33482α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γx✝: αa↑(comp g 0) x✝ = ↑0 x✝
F: Type ?u.33482α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γcomp g 0 = 0simpGoals accomplished! 🐙
#align non_unital_ring_hom.comp_zero NonUnitalRingHom.comp_zero: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ), comp g 0 = 0NonUnitalRingHom.comp_zero

@[simp]
theorem zero_comp: ∀ (f : α →ₙ+* β), comp 0 f = 0zero_comp (f: α →ₙ+* βf : α: Type ?u.34959α →ₙ+* β: Type ?u.34962β) : (0: ?m.350380 : β: Type ?u.34962β →ₙ+* γ: Type ?u.34965γ).comp: {α : Type ?u.35081} →
{β : Type ?u.35080} →
{γ : Type ?u.35079} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf = 0: ?m.351050 := byGoals accomplished! 🐙
F: Type ?u.34956α: Type u_1β: Type u_2γ: Type u_3inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg: β →ₙ+* γf✝, f: α →ₙ+* βcomp 0 f = 0extF: Type ?u.34956α: Type u_1β: Type u_2γ: Type u_3inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg: β →ₙ+* γf✝, f: α →ₙ+* βx✝: αa↑(comp 0 f) x✝ = ↑0 x✝
F: Type ?u.34956α: Type u_1β: Type u_2γ: Type u_3inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg: β →ₙ+* γf✝, f: α →ₙ+* βcomp 0 f = 0rflGoals accomplished! 🐙
#align non_unital_ring_hom.zero_comp NonUnitalRingHom.zero_comp: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (f : α →ₙ+* β), comp 0 f = 0NonUnitalRingHom.zero_comp

@[simp]
theorem comp_id: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β), comp f (NonUnitalRingHom.id α) = fcomp_id (f: α →ₙ+* βf : α: Type ?u.35260α →ₙ+* β: Type ?u.35263β) : f: α →ₙ+* βf.comp: {α : Type ?u.35329} →
{β : Type ?u.35328} →
{γ : Type ?u.35327} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp (NonUnitalRingHom.id: (α : Type ?u.35348) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αNonUnitalRingHom.id α: Type ?u.35260α) = f: α →ₙ+* βf :=
ext: ∀ {α : Type ?u.35361} {β : Type ?u.35362} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext fun _: ?m.35389_ => rfl: ∀ {α : Sort ?u.35391} {a : α}, a = arfl
#align non_unital_ring_hom.comp_id NonUnitalRingHom.comp_id: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β), comp f (NonUnitalRingHom.id α) = fNonUnitalRingHom.comp_id

@[simp]
theorem id_comp: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β), comp (NonUnitalRingHom.id β) f = fid_comp (f: α →ₙ+* βf : α: Type ?u.35443α →ₙ+* β: Type ?u.35446β) : (NonUnitalRingHom.id: (α : Type ?u.35510) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αNonUnitalRingHom.id β: Type ?u.35446β).comp: {α : Type ?u.35514} →
{β : Type ?u.35513} →
{γ : Type ?u.35512} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf = f: α →ₙ+* βf :=
ext: ∀ {α : Type ?u.35544} {β : Type ?u.35545} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext fun _: ?m.35572_ => rfl: ∀ {α : Sort ?u.35574} {a : α}, a = arfl
#align non_unital_ring_hom.id_comp NonUnitalRingHom.id_comp: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β), comp (NonUnitalRingHom.id β) f = fNonUnitalRingHom.id_comp

instance: {α : Type u_1} → [inst : NonUnitalNonAssocSemiring α] → MonoidWithZero (α →ₙ+* α)instance : MonoidWithZero: Type ?u.35673 → Type ?u.35673MonoidWithZero (α: Type ?u.35625α →ₙ+* α: Type ?u.35625α) where
one := NonUnitalRingHom.id: (α : Type ?u.35790) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αNonUnitalRingHom.id α: Type ?u.35625α
mul := comp: {α : Type ?u.35699} →
{β : Type ?u.35698} →
{γ : Type ?u.35697} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp
mul_one := comp_id: ∀ {α : Type ?u.35811} {β : Type ?u.35812} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β), comp f (NonUnitalRingHom.id α) = fcomp_id
one_mul := id_comp: ∀ {α : Type ?u.35792} {β : Type ?u.35793} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(f : α →ₙ+* β), comp (NonUnitalRingHom.id β) f = fid_comp
mul_assoc f: ?m.35732f g: ?m.35735g h: ?m.35738h := comp_assoc: ∀ {α : Type ?u.35741} {β : Type ?u.35742} {γ : Type ?u.35743} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {δ : Type ?u.35740}
{x : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ), comp (comp h g) f = comp h (comp g f)comp_assoc _: ?m.35744 →ₙ+* ?m.35745_ _: ?m.35745 →ₙ+* ?m.35746_ _: ?m.35746 →ₙ+* ?m.35750_
zero := 0: ?m.358370
mul_zero := comp_zero: ∀ {α : Type ?u.35900} {β : Type ?u.35898} {γ : Type ?u.35899} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ), comp g 0 = 0comp_zero
zero_mul := zero_comp: ∀ {α : Type ?u.35871} {β : Type ?u.35872} {γ : Type ?u.35873} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (f : α →ₙ+* β), comp 0 f = 0zero_comp

theorem one_def: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], 1 = NonUnitalRingHom.id αone_def : (1: ?m.361661 : α: Type ?u.36105α →ₙ+* α: Type ?u.36105α) = NonUnitalRingHom.id: (α : Type ?u.36355) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* αNonUnitalRingHom.id α: Type ?u.36105α :=
rfl: ∀ {α : Sort ?u.36359} {a : α}, a = arfl
#align non_unital_ring_hom.one_def NonUnitalRingHom.one_def: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], 1 = NonUnitalRingHom.id αNonUnitalRingHom.one_def

@[simp]
theorem coe_one: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], ↑1 = idcoe_one : ⇑(1: ?m.364321 : α: Type ?u.36371α →ₙ+* α: Type ?u.36371α) = id: {α : Sort ?u.36789} → α → αid :=
rfl: ∀ {α : Sort ?u.36835} {a : α}, a = arfl
#align non_unital_ring_hom.coe_one NonUnitalRingHom.coe_one: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], ↑1 = idNonUnitalRingHom.coe_one

theorem mul_def: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), f * g = comp f gmul_def (f: α →ₙ+* αf g: α →ₙ+* αg : α: Type ?u.36873α →ₙ+* α: Type ?u.36873α) : f: α →ₙ+* αf * g: α →ₙ+* αg = f: α →ₙ+* αf.comp: {α : Type ?u.36945} →
{β : Type ?u.36944} →
{γ : Type ?u.36943} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp g: α →ₙ+* αg :=
rfl: ∀ {α : Sort ?u.37236} {a : α}, a = arfl
#align non_unital_ring_hom.mul_def NonUnitalRingHom.mul_def: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), f * g = comp f gNonUnitalRingHom.mul_def

@[simp]
theorem coe_mul: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), ↑(f * g) = ↑f ∘ ↑gcoe_mul (f: α →ₙ+* αf g: α →ₙ+* αg : α: Type ?u.37250α →ₙ+* α: Type ?u.37250α) : ⇑(f: α →ₙ+* αf * g: α →ₙ+* αg) = f: α →ₙ+* αf ∘ g: α →ₙ+* αg :=
rfl: ∀ {α : Sort ?u.38099} {a : α}, a = arfl
#align non_unital_ring_hom.coe_mul NonUnitalRingHom.coe_mul: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), ↑(f * g) = ↑f ∘ ↑gNonUnitalRingHom.coe_mul

theorem cancel_right: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β},
Surjective ↑f → (comp g₁ f = comp g₂ f ↔ g₁ = g₂)cancel_right {g₁: β →ₙ+* γg₁ g₂: β →ₙ+* γg₂ : β: Type ?u.38150β →ₙ+* γ: Type ?u.38153γ} {f: α →ₙ+* βf : α: Type ?u.38147α →ₙ+* β: Type ?u.38150β} (hf: Surjective ↑fhf : Surjective: {α : Sort ?u.38232} → {β : Sort ?u.38231} → (α → β) → PropSurjective f: α →ₙ+* βf) :
g₁: β →ₙ+* γg₁.comp: {α : Type ?u.38432} →
{β : Type ?u.38431} →
{γ : Type ?u.38430} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf = g₂: β →ₙ+* γg₂.comp: {α : Type ?u.38457} →
{β : Type ?u.38456} →
{γ : Type ?u.38455} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f: α →ₙ+* βf ↔ g₁: β →ₙ+* γg₁ = g₂: β →ₙ+* γg₂ :=
⟨fun h: ?m.38498h => ext: ∀ {α : Type ?u.38500} {β : Type ?u.38501} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext <| hf: Surjective ↑fhf.forall: ∀ {α : Sort ?u.38527} {β : Sort ?u.38528} {f : α → β},
Surjective f → ∀ {p : β → Prop}, (∀ (y : β), p y) ↔ ∀ (x : α), p (f x)forall.2: ∀ {a b : Prop}, (a ↔ b) → b → a2 (ext_iff: ∀ {α : Type ?u.38546} {β : Type ?u.38547} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
{f g : α →ₙ+* β}, f = g ↔ ∀ (x : α), ↑f x = ↑g xext_iff.1: ∀ {a b : Prop}, (a ↔ b) → a → b1 h: ?m.38498h), fun h: ?m.38628h => h: ?m.38628h ▸ rfl: ∀ {α : Sort ?u.38635} {a : α}, a = arfl⟩
#align non_unital_ring_hom.cancel_right NonUnitalRingHom.cancel_right: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {g₁ g₂ : β →ₙ+* γ} {f : α →ₙ+* β},
Surjective ↑f → (comp g₁ f = comp g₂ f ↔ g₁ = g₂)NonUnitalRingHom.cancel_right

theorem cancel_left: ∀ {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β}, Injective ↑g → (comp g f₁ = comp g f₂ ↔ f₁ = f₂)cancel_left {g: β →ₙ+* γg : β: Type ?u.38687β →ₙ+* γ: Type ?u.38690γ} {f₁: α →ₙ+* βf₁ f₂: α →ₙ+* βf₂ : α: Type ?u.38684α →ₙ+* β: Type ?u.38687β} (hg: Injective ↑ghg : Injective: {α : Sort ?u.38769} → {β : Sort ?u.38768} → (α → β) → PropInjective g: β →ₙ+* γg) :
g: β →ₙ+* γg.comp: {α : Type ?u.38968} →
{β : Type ?u.38967} →
{γ : Type ?u.38966} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f₁: α →ₙ+* βf₁ = g: β →ₙ+* γg.comp: {α : Type ?u.38993} →
{β : Type ?u.38992} →
{γ : Type ?u.38991} →
[inst : NonUnitalNonAssocSemiring α] →
[inst_1 : NonUnitalNonAssocSemiring β] →
[inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γcomp f₂: α →ₙ+* βf₂ ↔ f₁: α →ₙ+* βf₁ = f₂: α →ₙ+* βf₂ :=
⟨fun h: ?m.39033h => ext: ∀ {α : Type ?u.39035} {β : Type ?u.39036} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = gext fun x: ?m.39063x => hg: Injective ↑ghg <| byGoals accomplished! 🐙 F: Type ?u.38681α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γf₁, f₂: α →ₙ+* βhg: Injective ↑gh: comp g f₁ = comp g f₂x: α↑g (↑f₁ x) = ↑g (↑f₂ x)rw [F: Type ?u.38681α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γf₁, f₂: α →ₙ+* βhg: Injective ↑gh: comp g f₁ = comp g f₂x: α↑g (↑f₁ x) = ↑g (↑f₂ x)← comp_apply: ∀ {α : Type ?u.39113} {β : Type ?u.39111} {γ : Type ?u.39112} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α),
↑(comp g f) x = ↑g (↑f x)comp_apply,F: Type ?u.38681α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γf₁, f₂: α →ₙ+* βhg: Injective ↑gh: comp g f₁ = comp g f₂x: α↑(comp g f₁) x = ↑g (↑f₂ x) F: Type ?u.38681α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γf₁, f₂: α →ₙ+* βhg: Injective ↑gh: comp g f₁ = comp g f₂x: α↑g (↑f₁ x) = ↑g (↑f₂ x)h: comp g f₁ = comp g f₂h,F: Type ?u.38681α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γf₁, f₂: α →ₙ+* βhg: Injective ↑gh: comp g f₁ = comp g f₂x: α↑(comp g f₂) x = ↑g (↑f₂ x) F: Type ?u.38681α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γf₁, f₂: α →ₙ+* βhg: Injective ↑gh: comp g f₁ = comp g f₂x: α↑g (↑f₁ x) = ↑g (↑f₂ x)comp_apply: ∀ {α : Type ?u.39277} {β : Type ?u.39275} {γ : Type ?u.39276} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α),
↑(comp g f) x = ↑g (↑f x)comp_applyF: Type ?u.38681α: Type u_3β: Type u_1γ: Type u_2inst✝²: NonUnitalNonAssocSemiring αinst✝¹: NonUnitalNonAssocSemiring βinst✝: NonUnitalNonAssocSemiring γg✝: β →ₙ+* γf: α →ₙ+* βg: β →ₙ+* γf₁, f₂: α →ₙ+* βhg: Injective ↑gh: comp g f₁ = comp g f₂x: α↑g (↑f₂ x) = ↑g (↑f₂ x)]Goals accomplished! 🐙, fun h: ?m.39088h => h: ?m.39088h ▸ rfl: ∀ {α : Sort ?u.39090} {a : α}, a = arfl⟩
#align non_unital_ring_hom.cancel_left NonUnitalRingHom.cancel_left: ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β},
Injective ↑g → (comp g f₁ = comp g f₂ ↔ f₁ = f₂)NonUnitalRingHom.cancel_left

end NonUnitalRingHom

/-- Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both `MonoidHom` and `MonoidWithZeroHom` in order to put the fields in a
sensible order, even though `MonoidWithZeroHom` already extends `MonoidHom`. -/
structure RingHom: {α : Type u_1} →
{β : Type u_2} →
[inst : NonAssocSemiring α] →
[inst_1 : NonAssocSemiring β] →
(toMonoidHom : α →* β) →
OneHom.toFun (↑toMonoidHom) 0 = 0 →
(∀ (x y : α),
OneHom.toFun (↑toMonoidHom) (x + y) = OneHom.toFun (↑toMonoidHom) x + OneHom.toFun (↑toMonoidHom) y) →
RingHom α βRingHom (α: Type ?u.39407α : Type _: Type (?u.39407+1)Type _) (β: Type ?u.39410β : Type _: Type (?u.39410+1)Type _) [NonAssocSemiring: Type ?u.39413 → Type ?u.39413NonAssocSemiring α: Type ?u.39407α] [NonAssocSemiring: Type ?u.39416 → Type ?u.39416NonAssocSemiring β: Type ?u.39410β] extends
α: Type ?u.39407α →* β: Type ?u.39410β, α: Type ?u.39407α →+ β: Type ?u.39410β, α: Type ?u.39407α →ₙ+* β: Type ?u.39410β, α: Type ?u.39407α →*₀ β: Type ?u.39410β
#align ring_hom RingHom: (α : Type u_1) → (β : Type u_2) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (maxu_1u_2)RingHom

/-- `α →+* β` denotes the type of ring homomorphisms from `α` to `β`. -/
infixr:25 " →+* " => RingHom: (α : Type u_1) → (β : Type u_2) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (maxu_1u_2)RingHom

/-- Reinterpret a ring homomorphism `f : α →+* β` as a monoid with zero homomorphism `α →*₀ β`.
The `simp`-normal form is `(f : α →*₀ β)`. -/
add_decl_doc RingHom.toMonoidWithZeroHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →*₀ βRingHom.toMonoidWithZeroHom
#align ring_hom.to_monoid_with_zero_hom RingHom.toMonoidWithZeroHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →*₀ βRingHom.toMonoidWithZeroHom

/-- Reinterpret a ring homomorphism `f : α →+* β` as a monoid homomorphism `α →* β`.
The `simp`-normal form is `(f : α →* β)`. -/
add_decl_doc RingHom.toMonoidHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* βRingHom.toMonoidHom
#align ring_hom.to_monoid_hom RingHom.toMonoidHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* βRingHom.toMonoidHom

/-- Reinterpret a ring homomorphism `f : α →+* β` as an additive monoid homomorphism `α →+ β`.
The `simp`-normal form is `(f : α →+ β)`. -/
add_decl_doc RingHom.toAddMonoidHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ βRingHom.toAddMonoidHom
#align ring_hom.to_add_monoid_hom RingHom.toAddMonoidHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ βRingHom.toAddMonoidHom

/-- Reinterpret a ring homomorphism `f : α →+* β` as a non-unital ring homomorphism `α →ₙ+* β`. The
`simp`-normal form is `(f : α →ₙ+* β)`. -/
add_decl_doc RingHom.toNonUnitalRingHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →ₙ+* βRingHom.toNonUnitalRingHom
#align ring_hom.to_non_unital_ring_hom RingHom.toNonUnitalRingHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →ₙ+* βRingHom.toNonUnitalRingHom

section RingHomClass

/-- `RingHomClass F α β` states that `F` is a type of (semi)ring homomorphisms.
You should extend this class when you extend `RingHom`.

This extends from both `MonoidHomClass` and `MonoidWithZeroHomClass` in
order to put the fields in a sensible order, even though
class RingHomClass: Type u_1 →
(α : outParam (Type u_2)) →
(β : outParam (Type u_3)) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(maxu_1u_2)u_3)RingHomClass (F: Type ?u.48337F : Type _: Type (?u.48337+1)Type _) (α: outParam (Type ?u.48341)α β: outParam (Type ?u.48345)β : outParam: Sort ?u.48344 → Sort ?u.48344outParam (Type _: Type (?u.48341+1)Type _)) [NonAssocSemiring: Type ?u.48348 → Type ?u.48348NonAssocSemiring α: outParam (Type ?u.48341)α]
[NonAssocSemiring: Type ?u.48351 → Type ?u.48351NonAssocSemiring β: outParam (Type ?u.48345)β] extends MonoidHomClass: Type ?u.48358 →
(M : outParam (Type ?u.48357)) →
(N : outParam (Type ?u.48356)) →
[inst : MulOneClass M] → [inst : MulOneClass N] → Type (max(max?u.48358?u.48357)?u.48356)MonoidHomClass F: Type ?u.48337F α: outParam (Type ?u.48341)α β: outParam (Type ?u.48345)β, AddMonoidHomClass: Type ?u.48407 →
(M : outParam (Type ?u.48406)) →
(N : outParam (Type ?u.48405)) →
[inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.48407?u.48406)?u.48405)AddMonoidHomClass F: Type ?u.48337F α: outParam (Type ?u.48341)α β: outParam (Type ?u.48345)β,
MonoidWithZeroHomClass: Type ?u.48551 →
(M : outParam (Type ?u.48550)) →
(N : outParam (Type ?u.48549)) →
[inst : MulZeroOneClass M] → [inst : MulZeroOneClass N] → Type (max(max?u.48551?u.48550)?u.48549)MonoidWithZeroHomClass F: Type ?u.48337F α: outParam (Type ?u.48341)α β: outParam (Type ?u.48345)β
#align ring_hom_class RingHomClass: Type u_1 →
(α : outParam (Type u_2)) →
(β : outParam (Type u_3)) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(maxu_1u_2)u_3)RingHomClass

set_option linter.deprecated false in
/-- Ring homomorphisms preserve `bit1`. -/
@[simp] lemma map_bit1: ∀ {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β]
[inst_2 : RingHomClass F α β] (f : F) (a : α), ↑f (bit1 a) = bit1 (↑f a)map_bit1 [NonAssocSemiring: Type ?u.48865 → Type ?u.48865NonAssocSemiring α: Type ?u.48856α] [NonAssocSemiring: Type ?u.48868 → Type ?u.48868NonAssocSemiring β: Type ?u.48859β] [RingHomClass: Type ?u.48873 →
(α : outParam (Type ?u.48872)) →
(β : outParam (Type ?u.48871)) →
[inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.48873?u.48872)?u.48871)RingHomClass F: Type ?u.48853F α: Type ?u.48856α β: Type ?u.48859β]
(f: Ff : F: Type ?u.48853F) (a: αa : α: Type ?u.48856α) : (f: Ff (bit1: {α : Type ?u.49270} → [inst : One α] → [inst : Add α] → α → αbit1 a: αa) : β: Type ?u.48859β) = bit1: {α : Type ?u.49413} → [inst : One α] → [inst : Add α] → α → αbit1 (f: Ff a: αa) := byGoals accomplished! 🐙 F: Type u_3α: Type u_1β: Type u_2γ: Type ?u.48862inst✝²: NonAssocSemiring αinst✝¹: NonAssocSemiring βinst✝: RingHomClass F α βf: Fa: α↑f (bit1 a) = bit1 (↑f a)simp [bit1: {α : Type ?u.49915} → [inst : One α] → [inst : Add α] → α → αbit1]Goals accomplished! 🐙
#align map_bit1 map_bit1: ∀ {F : Type u_3} {α : Type u_1} {β : Type u_2} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β]
[inst_2 : RingHomClass F α β] (f : F) (a : α), ↑f (bit1 a) = bit1 (↑f a)map_bit1

-- Porting note: marked `{}` rather than `[]` to prevent dangerous instances
variable {_: NonAssocSemiring α_ : NonAssocSemiring: Type ?u.52034 → Type ?u.52034NonAssocSemiring α: Type ?u.51067α} {_: NonAssocSemiring β_ : NonAssocSemiring: Type ?u.51044 → Type ?u.51044NonAssocSemiring β: Type ?u.51035β} [RingHomClass: Type ?u.51049 →
(α : outParam (Type ?u.51048)) →
(β : outParam (Type ?u.51047)) →
[inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.51049?u.51048)?u.51047)RingHomClass F: Type ?u.51029F α: Type ?u.52025α β: Type ?u.52028β]

/-- Turn an element of a type `F` satisfying `RingHomClass F α β` into an actual
`RingHom`. This is declared as the default coercion from `F` to `α →+* β`. -/
@[coe]
def RingHomClass.toRingHom: F → α →+* βRingHomClass.toRingHom (f: Ff : F: Type ?u.51064F) : α: Type ?u.51067α →+* β: Type ?u.51070β :=
{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536{ (f: Ff{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536 : α: Type ?u.51067α{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536 →* β: Type ?u.51070β{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536), (f: Ff{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536 : α: Type ?u.51067α{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536 →+ β: Type ?u.51070β{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536) { (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536with{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536 }

/-- Any type satisfying `RingHomClass` can be cast into `RingHom` via `RingHomClass.toRingHom`. -/
instance: {F : Type u_1} →
{α : Type u_2} →
{β : Type u_3} →
{x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [inst : RingHomClass F α β] → CoeTC F (α →+* β)instance : CoeTC: Sort ?u.52058 → Sort ?u.52057 → Sort (max(max1?u.52058)?u.52057)CoeTC F: Type ?u.52022F (α: Type ?u.52025α →+* β: Type ?u.52028β) :=
⟨RingHomClass.toRingHom: {F : Type ?u.52085} →
{α : Type ?u.52084} →
{β : Type ?u.52083} →
{x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [inst : RingHomClass F α β] → F → α →+* βRingHomClass.toRingHom⟩

instance (priority := 100) RingHomClass.toNonUnitalRingHomClass: NonUnitalRingHomClass F α βRingHomClass.toNonUnitalRingHomClass : NonUnitalRingHomClass: Type ?u.52246 →
(α : outParam (Type ?u.52245)) →
(β : outParam (Type ?u.52244)) →
[inst : NonUnitalNonAssocSemiring α] →
[inst : NonUnitalNonAssocSemiring β] → Type (max(max?u.52246?u.52245)?u.52244)NonUnitalRingHomClass F: Type ?u.52209F α: Type ?u.52212α β: Type ?u.52215β :=
{ ‹RingHomClass F α β› with }: NonUnitalRingHomClass ?m.52361 ?m.52362 ?m.52363{ ‹RingHomClass F α β› { ‹RingHomClass F α β› with }: NonUnitalRingHomClass ?m.52361 ?m.52362 ?m.52363with{ ‹RingHomClass F α β› with }: NonUnitalRingHomClass ?m.52361 ?m.52362 ?m.52363 }
#align ring_hom_class.to_non_unital_ring_hom_class RingHomClass.toNonUnitalRingHomClass: {F : Type u_1} →
{α : Type u_2} →
{β : Type u_3} →
{x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [inst : RingHomClass F α β] → NonUnitalRingHomClass F α βRingHomClass.toNonUnitalRingHomClass

end RingHomClass

namespace RingHom

section coe

/-!
Throughout this section, some `Semiring` arguments are specified with `{}` instead of `[]`.
See note [implicit instance arguments].
-/

variable {_: NonAssocSemiring α_ : NonAssocSemiring: Type ?u.52651 → Type ?u.52651NonAssocSemiring α: Type ?u.59553α} {_: NonAssocSemiring β_ : NonAssocSemiring: Type ?u.57375 → Type ?u.57375NonAssocSemiring β: Type ?u.52645β}

instance: {α : Type u_1} → {β : Type u_2} → {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → RingHomClass (α →+* β) α βinstance : RingHomClass: Type ?u.52677 →
(α : outParam (Type ?u.52676)) →
(β : outParam (Type ?u.52675)) →
[inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.52677?u.52676)?u.52675)RingHomClass (α: Type ?u.52660α →+* β: Type ?u.52663β) α: Type ?u.52660α β: Type ?u.52663β where
coe f: ?m.52890f := f: ?m.52890f.toFun: {M : Type ?u.52913} → {N : Type ?u.52912} → [inst : One M] → [inst_1 : One N] → OneHom M N → M → NtoFun
coe_injective' f: ?m.53017f g: ?m.53020g h: ?m.53023h := byGoals accomplished! 🐙
F: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βf, g: α →+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gcases f: α →+* βfF: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βg: α →+* βtoMonoidHom✝: α →* βmap_zero'✝: OneHom.toFun (↑toMonoidHom✝) 0 = 0map_add'✝: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) yh: (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } =   (fun f => f.toFun) gmk{ toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
F: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βf, g: α →+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gcases g: α →+* βgF: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βtoMonoidHom✝¹: α →* βmap_zero'✝¹: OneHom.toFun (↑toMonoidHom✝¹) 0 = 0map_add'✝¹: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) ytoMonoidHom✝: α →* βmap_zero'✝: OneHom.toFun (↑toMonoidHom✝) 0 = 0map_add'✝: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) yh: (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }mk.mk{ toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }
F: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βf, g: α →+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gcongrF: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βtoMonoidHom✝¹: α →* βmap_zero'✝¹: OneHom.toFun (↑toMonoidHom✝¹) 0 = 0map_add'✝¹: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) ytoMonoidHom✝: α →* βmap_zero'✝: OneHom.toFun (↑toMonoidHom✝) 0 = 0map_add'✝: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) yh: (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }mk.mk.e_toMonoidHomtoMonoidHom✝¹ = toMonoidHom✝
F: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βf, g: α →+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gapply FunLike.coe_injective': ∀ {F : Sort ?u.53458} {α : outParam (Sort ?u.53457)} {β : outParam (α → Sort ?u.53456)} [self : FunLike F α β],
Injective FunLike.coeFunLike.coe_injective'F: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βtoMonoidHom✝¹: α →* βmap_zero'✝¹: OneHom.toFun (↑toMonoidHom✝¹) 0 = 0map_add'✝¹: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) ytoMonoidHom✝: α →* βmap_zero'✝: OneHom.toFun (↑toMonoidHom✝) 0 = 0map_add'✝: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) yh: (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }mk.mk.e_toMonoidHom.a↑toMonoidHom✝¹ = ↑toMonoidHom✝
F: Type ?u.52657α: Type ?u.52660β: Type ?u.52663γ: Type ?u.52666x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βf, g: α →+* βh: (fun f => f.toFun) f = (fun f => f.toFun) gf = gexact h: (fun f => f.toFun) { toMonoidHom := toMonoidHom✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ } =   (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }hGoals accomplished! 🐙
map_add := RingHom.map_add': ∀ {α : Type ?u.53095} {β : Type ?u.53094} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (self : α →+* β)
(x y : α),
OneHom.toFun (↑self.toMonoidHom) (x + y) = OneHom.toFun (↑self.toMonoidHom) x + OneHom.toFun (↑self.toMonoidHom) yRingHom.map_add'
map_zero := RingHom.map_zero': ∀ {α : Type ?u.53126} {β : Type ?u.53125} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (self : α →+* β),
OneHom.toFun (↑self.toMonoidHom) 0 = 0RingHom.map_zero'
map_mul f: ?m.53036f := f: ?m.53036f.map_mul': ∀ {M : Type ?u.53045} {N : Type ?u.53044} [inst : MulOneClass M] [inst_1 : MulOneClass N] (self : M →* N) (x y : M),
OneHom.toFun (↑self) (x * y) = OneHom.toFun (↑self) x * OneHom.toFun (↑self) ymap_mul'
map_one f: ?m.53072f := f: ?m.53072f.map_one': ∀ {M : Type ?u.53087} {N : Type ?u.53086} [inst : One M] [inst_1 : One N] (self : OneHom M N), OneHom.toFun self 1 = 1map_one'

-- Porting note:
-- These helper instances are unhelpful in Lean 4, so omitting:
-- /-- Helper instance for when there's too many metavariables to apply `fun_like.has_coe_to_fun`
-- directly.
-- -/
-- instance : CoeFun (α →+* β) fun _ => α → β :=
--   ⟨RingHom.toFun⟩

initialize_simps_projections RingHom: (α : Type u_1) → (β : Type u_2) → [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (maxu_1u_2)RingHom (toFun: (α : Type u_1) → (β : Type u_2) → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α → βtoFun → apply: (α : Type u_1) → (β : Type u_2) → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α → βapply)

-- Porting note: is this lemma still needed in Lean4?
-- Porting note: because `f.toFun` really means `f.toMonoidHom.toOneHom.toFun` and
-- `toMonoidHom_eq_coe` wants to simplify `f.toMonoidHom` to `(↑f : M →* N)`, this can't
-- be a simp lemma anymore
-- @[simp]
theorem toFun_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f.toFun = ↑ftoFun_eq_coe (f: α →+* βf : α: Type ?u.54869α →+* β: Type ?u.54872β) : f: α →+* βf.toFun: {M : Type ?u.54954} → {N : Type ?u.54953} → [inst : One M] → [inst_1 : One N] → OneHom M N → M → NtoFun = f: α →+* βf :=
rfl: ∀ {α : Sort ?u.55889} {a : α}, a = arfl
#align ring_hom.to_fun_eq_coe RingHom.toFun_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f.toFun = ↑fRingHom.toFun_eq_coe

@[simp]
theorem coe_mk: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β)
(h₁ : OneHom.toFun (↑f) 0 = 0)
(h₂ : ∀ (x_2 y : α), OneHom.toFun (↑f) (x_2 + y) = OneHom.toFun (↑f) x_2 + OneHom.toFun (↑f) y),
↑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = ↑fcoe_mk (f: α →* βf : α: Type ?u.55906α →* β: Type ?u.55909β) (h₁: OneHom.toFun (↑f) 0 = 0h₁ h₂: ?m.55966h₂) : ((⟨f: α →* βf, h₁: ?m.55963h₁, h₂: ?m.55966h₂⟩ : α: Type ?u.55906α →+* β: Type ?u.55909β) : α: Type ?u.55906α → β: Type ?u.55909β) = f: α →* βf :=
rfl: ∀ {α : Sort ?u.57305} {a : α}, a = arfl
#align ring_hom.coe_mk RingHom.coe_mk: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β)
(h₁ : OneHom.toFun (↑f) 0 = 0)
(h₂ : ∀ (x_2 y : α), OneHom.toFun (↑f) (x_2 + y) = OneHom.toFun (↑f) x_2 + OneHom.toFun (↑f) y),
↑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = ↑fRingHom.coe_mk

@[simp]
theorem coe_coe: ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_1}
[inst : RingHomClass F α β] (f : F), ↑↑f = ↑fcoe_coe {F: Type u_1F : Type _: Type (?u.57378+1)Type _} [RingHomClass: Type ?u.57383 →
(α : outParam (Type ?u.57382)) →
(β : outParam (Type ?u.57381)) →
[inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.57383?u.57382)?u.57381)RingHomClass F: Type ?u.57378F α: Type ?u.57363α β: Type ?u.57366β] (f: Ff : F: Type ?u.57378F) : ((f: Ff : α: Type ?u.57363α →+* β: Type ?u.57366β) : α: Type ?u.57363α → β: Type ?u.57366β) = f: Ff :=
rfl: ∀ {α : Sort ?u.58682} {a : α}, a = arfl
#align ring_hom.coe_coe RingHom.coe_coe: ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_1}
[inst : RingHomClass F α β] (f : F), ↑↑f = ↑fRingHom.coe_coe

attribute [coe] RingHom.toMonoidHom: {α : Type u_1} → {β : Type u_2} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* βRingHom.toMonoidHom

instance coeToMonoidHom: Coe (α →+* β) (α →* β)coeToMonoidHom : Coe: semiOutParam (Sort ?u.58891) → Sort ?u.58890 → Sort (max(max1?u.58891)?u.58890)Coe (α: Type ?u.58875α →+* β: Type ?u.58878β) (α: Type ?u.58875α →* β: Type ?u.58878β) :=
⟨RingHom.toMonoidHom: {α : Type ?u.58953} →
{β : Type ?u.58952} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* βRingHom.toMonoidHom⟩
#align ring_hom.has_coe_monoid_hom RingHom.coeToMonoidHom: {α : Type u_1} → {β : Type u_2} → {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → Coe (α →+* β) (α →* β)RingHom.coeToMonoidHom

-- Porting note: `dsimp only` can prove this
#noalign ring_hom.coe_monoid_hom

@[simp]
theorem toMonoidHom_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f = ↑ftoMonoidHom_eq_coe (f: α →+* βf : α: Type ?u.59246α →+* β: Type ?u.59249β) : f: α →+* βf.toMonoidHom: {α : Type ?u.59279} →
{β : Type ?u.59278} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →* βtoMonoidHom = f: α →+* βf :=
rfl: ∀ {α : Sort ?u.59528} {a : α}, a = arfl
#align ring_hom.to_monoid_hom_eq_coe RingHom.toMonoidHom_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), ↑f = ↑fRingHom.toMonoidHom_eq_coe

-- Porting note: this can't be a simp lemma anymore
-- @[simp]
theorem toMonoidWithZeroHom_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
↑(toMonoidWithZeroHom f) = ↑ftoMonoidWithZeroHom_eq_coe (f: α →+* βf : α: Type ?u.59553α →+* β: Type ?u.59556β) : (f: α →+* βf.toMonoidWithZeroHom: {α : Type ?u.59589} →
{β : Type ?u.59588} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →*₀ βtoMonoidWithZeroHom : α: Type ?u.59553α → β: Type ?u.59556β) = f: α →+* βf := byGoals accomplished! 🐙
F: Type ?u.59550α: Type u_1β: Type u_2γ: Type ?u.59559x✝¹: NonAssocSemiring αx✝: NonAssocSemiring βf: α →+* β↑(toMonoidWithZeroHom f) = ↑frflGoals accomplished! 🐙
#align ring_hom.to_monoid_with_zero_hom_eq_coe RingHom.toMonoidWithZeroHom_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
↑(toMonoidWithZeroHom f) = ↑fRingHom.toMonoidWithZeroHom_eq_coe

@[simp]
theorem coe_monoidHom_mk: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β)
(h₁ : OneHom.toFun (↑f) 0 = 0)
(h₂ : ∀ (x_2 y : α), OneHom.toFun (↑f) (x_2 + y) = OneHom.toFun (↑f) x_2 + OneHom.toFun (↑f) y),
↑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = fcoe_monoidHom_mk (f: α →* βf : α: Type ?u.60952α →* β: Type ?u.60955β) (h₁: OneHom.toFun (↑f) 0 = 0h₁ h₂: ?m.61012h₂) : ((⟨f: α →* βf, h₁: ?m.61009h₁, h₂: ?m.61012h₂⟩ : α: Type ?u.60952α →+* β: Type ?u.60955β) : α: Type ?u.60952α →* β: Type ?u.60955β) = f: α →* βf :=
rfl: ∀ {α : Sort ?u.61222} {a : α}, a = arfl
#align ring_hom.coe_monoid_hom_mk RingHom.coe_monoidHom_mk: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β)
(h₁ : OneHom.toFun (↑f) 0 = 0)
(h₂ : ∀ (x_2 y : α), OneHom.toFun (↑f) (x_2 + y) = OneHom.toFun (↑f) x_2 + OneHom.toFun (↑f) y),
↑{ toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = fRingHom.coe_monoidHom_mk

-- Porting note: `dsimp only` can prove this

@[simp]
theorem toAddMonoidHom_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), toAddMonoidHom f = ↑ftoAddMonoidHom_eq_coe (f: α →+* βf : α: Type ?u.61275α →+* β: Type ?u.61278β) : f: α →+* βf.toAddMonoidHom: {α : Type ?u.61308} →
{β : Type ?u.61307} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ βtoAddMonoidHom = f: α →+* βf :=
rfl: ∀ {α : Sort ?u.61570} {a : α}, a = arfl
#align ring_hom.to_add_monoid_hom_eq_coe RingHom.toAddMonoidHom_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), toAddMonoidHom f = ↑fRingHom.toAddMonoidHom_eq_coe

@[simp]
theorem coe_addMonoidHom_mk: ∀ {α : Type u_2} {β : Type u_1} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α → β) (h₁ : f 1 = 1)
(h₂ :
∀ (x_2 y : α),
OneHom.toFun { toFun := f, map_one' := h₁ } (x_2 * y) =         OneHom.toFun { toFun := f, map_one' := h₁ } x_2 * OneHom.toFun { toFun := f, map_one' := h₁ } y)
(h₃ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0)
(h₄ :
∀ (x_2 y : α),
OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) (x_2 + y) =         OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) x_2 +           OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) y),
↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ } =     { toZeroHom := { toFun := f, map_zero' := h₃ }, map_add' := h₄ }coe_addMonoidHom_mk (f: α → βf : α: Type ?u.61625α → β: Type ?u.61628β) (h₁: ?m.61644h₁ h₂: ?m.61647h₂ h₃: OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0h₃ h₄: ?m.61653h₄) :
((⟨⟨⟨f: α → βf, h₁: ?m.61644h₁⟩, h₂: ?m.61647h₂⟩, h₃: ?m.61650h₃, h₄: ?m.61653h₄⟩ : α: Type ?u.61625α →+* β: Type ?u.61628β) : α: Type ?u.61625α →+ β: Type ?u.61628β) = ⟨⟨f: α → βf, h₃: ?m.61650h₃⟩, h₄: ?m.61653h₄⟩ :=
rfl: ∀ {α : Sort ?u.62482} {a : α}, a = arfl
#align ring_hom.coe_add_monoid_hom_mk RingHom.coe_addMonoidHom_mk: ∀ {α : Type u_2} {β : Type u_1} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α → β) (h₁ : f 1 = 1)
(h₂ :
∀ (x_2 y : α),
OneHom.toFun { toFun := f, map_one' := h₁ } (x_2 * y) =         OneHom.toFun { toFun := f, map_one' := h₁ } x_2 * OneHom.toFun { toFun := f, map_one' := h₁ } y)
(h₃ : OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0)
(h₄ :
∀ (x_2 y : α),
OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) (x_2 + y) =         OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) x_2 +           OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) y),
↑{ toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ } =     { toZeroHom := { toFun := f, map_zero' := h₃ }, map_add' := h₄ }RingHom.coe_addMonoidHom_mk

/-- Copy of a `RingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
def copy: {α : Type u_1} →
{β : Type u_2} →
{x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → (f : α →+* β) → (f' : α → β) → f' = ↑f → α →+* βcopy (f: α →+* βf : α: Type ?u.62577α →+* β: Type ?u.62580β) (f': α → βf' : α: Type ?u.62577α → β: Type ?u.62580β) (h: f' = ↑fh : f': α → βf' = f: α →+* βf) : α: Type ?u.62577α →+* β: Type ?u.62580β :=
{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657{ f: α →+* βf{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657.toMonoidWithZeroHom: {α : Type ?u.63460} →
{β : Type ?u.63459} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →*₀ βtoMonoidWithZeroHom{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657.copy: {M : Type ?u.63466} →
{N : Type ?u.63465} →
[inst : MulZeroOneClass M] → [inst_1 : MulZeroOneClass N] → (f : M →*₀ N) → (f' : M → N) → f' = ↑f → M →* Ncopy{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657 f': α → βf'{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657 h: f' = ↑fh{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657, f: α →+* βf{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657.toAddMonoidHom: {α : Type ?u.63514} →
{β : Type ?u.63513} → [inst : NonAssocSemiring α] → [inst_1 : NonAssocSemiring β] → (α →+* β) → α →+ βtoAddMonoidHom{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657.copy: {M : Type ?u.63520} →
{N : Type ?u.63519} →
[inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → (f : M →+ N) → (f' : M → N) → f' = ↑f → M →+ Ncopy{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657 f': α → βf'{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657 h: f' = ↑fh{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657 { f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657with{ f.toMonoidWithZeroHom.copy f' h, f.toAddMonoidHom.copy f' h with }: ?m.63656 →+* ?m.63657 }
#align ring_hom.copy RingHom.copy: {α : Type u_1} →
{β : Type u_2} →
{x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → (f : α →+* β) → (f' : α → β) → f' = ↑f → α →+* βRingHom.copy

@[simp]
theorem coe_copy: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β)
(h : f' = ↑f), ↑(copy f f' h) = f'coe_copy (f: α →+* βf : α: Type ?u.64358α →+* β: Type ?u.64361β) (f': α → βf' : α: Type ?u.64358α → β: Type ?u.64361β) (h: f' = ↑fh : f': α → βf' = f: α →+* βf) : ⇑(f: α →+* βf.copy: {α : Type ?u.65232} →
{β : Type ?u.65231} →
{x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → (f : α →+* β) → (f' : α → β) → f' = ↑f → α →+* βcopy f': α → βf' h: f' = ↑fh) = f': α → βf' :=
rfl: ∀ {α : Sort ?u.65593} {a : α}, a = arfl
#align ring_hom.coe_copy RingHom.coe_copy: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β)
(h : f' = ↑f), ↑(copy f f' h) = f'RingHom.coe_copy

theorem copy_eq: ∀ (f : α →+* β) (f' : α → β) (h : f' = ↑f), copy f f' h = fcopy_eq (f: α →+* βf : α: Type ?u.65649α →+* β: Type ?u.65652β) (f': α → βf' : α: Type ?u.65649α → β: Type ?u.65652β) (h: f' = ↑fh : f': α → βf' = f: α →+* βf) : f: α →+* βf.copy: {α : Type ?u.66523} →
{β : Type ?u.66522} →
{x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → (f : α →+* β) → (f' : α → β) → f' = ↑f → α →+* βcopy f': α → βf' h: f' = ↑fh = f: α →+* βf :=
FunLike.ext': ∀ {F : Sort ?u.66548} {α : Sort ?u.66546} {β : α → Sort ?u.66547} [i : FunLike F α β] {f g : F}, ↑f = ↑g → f = gFunLike.ext' h: f' = ↑fh
#align ring_hom.copy_eq RingHom.copy_eq: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : α → β)
(h : f' = ↑f), copy f f' h = fRingHom.copy_eq

end coe

section

variable {_: NonAssocSemiring α_ : NonAssocSemiring: Type ?u.75665 → Type ?u.75665NonAssocSemiring α: Type ?u.67192α} {_: NonAssocSemiring β_ : NonAssocSemiring: Type ?u.69477 → Type ?u.69477NonAssocSemiring β: Type ?u.67233β} (f: α →+* βf : α: Type ?u.67230α →+* β: Type ?u.67233β) {x: αx y: αy : α: Type ?u.91221α}

theorem congr_fun: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β},
f = g → ∀ (x_2 : α), ↑f x_2 = ↑g x_2congr_fun {f: α →+* βf g: α →+* βg : α: Type ?u.67230α →+* β: Type ?u.67233β} (h: f = gh : f: α →+* βf = g: α →+* βg) (x: αx : α: Type ?u.67230α) : f: α →+* βf x: αx = g: α →+* βg x: αx :=
FunLike.congr_fun: ∀ {F : Sort ?u.67994} {α : Sort ?u.67996} {β : α → Sort ?u.67995} [i : FunLike F α β] {f g : F},
f = g → ∀ (x : α), ↑f x = ↑g xFunLike.congr_fun h: f = gh x: αx
#align ring_hom.congr_fun RingHom.congr_fun: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β},
f = g → ∀ (x_2 : α), ↑f x_2 = ↑g x_2RingHom.congr_fun

theorem congr_arg: ∀ (f : α →+* β) {x y : α}, x = y → ↑f x = ↑f ycongr_arg (f: α →+* βf : α: Type ?u.68346α →+* β: Type ?u.68349β) {x: αx y: αy : α: Type ?u.68346α} (h: x = yh : x: αx = y: αy) : f: α →+* βf x: αx = f: α →+* βf y: αy :=
FunLike.congr_arg: ∀ {F : Sort ?u.69108} {α : Sort ?u.69106} {β : Sort ?u.69107} [i : FunLike F α fun x => β] (f : F) {x y : α},
x = y → ↑f x = ↑f yFunLike.congr_arg f: α →+* βf h: x = yh
#align ring_hom.congr_arg RingHom.congr_arg: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) {x_2 y : α},
x_2 = y → ↑f x_2 = ↑f yRingHom.congr_arg

theorem coe_inj: ∀ ⦃f g : α →+* β⦄, ↑f = ↑g → f = gcoe_inj ⦃f: α →+* βf g: α →+* βg : α: Type ?u.69465α →+* β: Type ?u.69468β⦄ (h: ↑f = ↑gh : (f: α →+* βf : α: Type ?u.69465α → β: Type ?u.69468β) = g: α →+* βg) : f: α →+* βf = g: α →+* βg :=
FunLike.coe_injective: ∀ {F : Sort ?u.70728} {α : Sort ?u.70729} {β : α → Sort ?u.70730} [i : FunLike F α β], Injective fun f => ↑fFunLike.coe_injective h: ↑f = ↑gh
#align ring_hom.coe_inj RingHom.coe_inj: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, ↑f = ↑g → f = gRingHom.coe_inj

@[ext]
theorem ext: ∀ {α : ```