/-
Copyright (c) 2019 Amelia Livingston. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.52022
F 
α: 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.32
NonUnitalNonAssocSemiring 
α: Type ?u.26
α]
  [
NonUnitalNonAssocSemiring: Type ?u.35 → Type ?u.35
NonUnitalNonAssocSemiring 
β: 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 : α →+ β)`. -/
add_decl_doc 
NonUnitalRingHom.toAddMonoidHom: {α : Type u_1} →
  {β : Type u_2} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →+ β
NonUnitalRingHom.toAddMonoidHom
#align non_unital_ring_hom.to_add_monoid_hom 
NonUnitalRingHom.toAddMonoidHom: {α : Type u_1} →
  {β : 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.9159
F : 
Type _: Type (?u.9159+1)
Type _) (
α: outParam (Type ?u.9163)
α 
β: outParam (Type ?u.9167)
β : 
outParam: Sort ?u.9162 → Sort ?u.9162
outParam (
Type _: Type (?u.9163+1)
Type _)) [
NonUnitalNonAssocSemiring: Type ?u.9170 → Type ?u.9170
NonUnitalNonAssocSemiring 
α: outParam (Type ?u.9163)
α]
  [
NonUnitalNonAssocSemiring: Type ?u.9173 → Type ?u.9173
NonUnitalNonAssocSemiring 
β: 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.9159
F 
α: 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.9159
F 
α: 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.9885
NonUnitalNonAssocSemiring 
α: Type ?u.9913
α] [
NonUnitalNonAssocSemiring: Type ?u.9925 → Type ?u.9925
NonUnitalNonAssocSemiring 
β: 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.9873
F 
α: 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: F
f : 
F: Type ?u.9910
F) : 
α: Type ?u.9913
α →ₙ+* 
β: Type ?u.9916
β :=
{ (f : α →ₙ* β), (f : α →+ β) with }: ?m.10672 →ₙ+* ?m.10673
{ (
f: F
f
{ (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
f
{ (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.10673
with
{ (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.11279
F (
α: 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.13426
NonUnitalNonAssocSemiring 
α: Type ?u.11507
α] [
NonUnitalNonAssocSemiring: Type ?u.11501 → Type ?u.11501
NonUnitalNonAssocSemiring 
β: 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.11680
f := 
f: ?m.11680
f.
toFun: {M : Type ?u.11693} → {N : Type ?u.11692} → [inst : Mul M] → [inst_1 : Mul N] → (M →ₙ* N) → M → N
toFun
  coe_injective' 
f: ?m.11709
f 
g: ?m.11712
g 
h: ?m.11715
h := by
Goals accomplished! 🐙
    
F: Type ?u.11504

α: Type ?u.11507

β: Type ?u.11510

γ: Type ?u.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

f, g: α →ₙ+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcases 
f: α →ₙ+* β
f
F: Type ?u.11504

α: Type ?u.11507

β: Type ?u.11510

γ: Type ?u.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

g: α →ₙ+* β

toMulHom✝: α →ₙ* β

map_zero'✝: MulHom.toFun toMulHom✝ 0 = 0

map_add'✝: ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y

h: (fun f => f.toFun) { toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = (fun f => f.toFun) g

mk
{ toMulHom := toMulHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
    
F: Type ?u.11504

α: Type ?u.11507

β: Type ?u.11510

γ: Type ?u.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

f, g: α →ₙ+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcases 
g: α →ₙ+* β
g
F: Type ?u.11504

α: Type ?u.11507

β: Type ?u.11510

γ: Type ?u.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

toMulHom✝¹: α →ₙ* β

map_zero'✝¹: MulHom.toFun toMulHom✝¹ 0 = 0

map_add'✝¹: ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y

toMulHom✝: α →ₙ* β

map_zero'✝: MulHom.toFun toMulHom✝ 0 = 0

map_add'✝: ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y

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'✝ }

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.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

f, g: α →ₙ+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcongr
F: Type ?u.11504

α: Type ?u.11507

β: Type ?u.11510

γ: Type ?u.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

toMulHom✝¹: α →ₙ* β

map_zero'✝¹: MulHom.toFun toMulHom✝¹ 0 = 0

map_add'✝¹: ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y

toMulHom✝: α →ₙ* β

map_zero'✝: MulHom.toFun toMulHom✝ 0 = 0

map_add'✝: ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y

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'✝ }

mk.mk.e_toMulHom
toMulHom✝¹ = toMulHom✝
    
F: Type ?u.11504

α: Type ?u.11507

β: Type ?u.11510

γ: Type ?u.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

f, g: α →ₙ+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gapply 
FunLike.coe_injective': ∀ {F : Sort ?u.12131} {α : outParam (Sort ?u.12130)} {β : outParam (α → Sort ?u.12129)} [self : FunLike F α β],
  Injective FunLike.coe
FunLike.coe_injective'
F: Type ?u.11504

α: Type ?u.11507

β: Type ?u.11510

γ: Type ?u.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

toMulHom✝¹: α →ₙ* β

map_zero'✝¹: MulHom.toFun toMulHom✝¹ 0 = 0

map_add'✝¹: ∀ (x y : α), MulHom.toFun toMulHom✝¹ (x + y) = MulHom.toFun toMulHom✝¹ x + MulHom.toFun toMulHom✝¹ y

toMulHom✝: α →ₙ* β

map_zero'✝: MulHom.toFun toMulHom✝ 0 = 0

map_add'✝: ∀ (x y : α), MulHom.toFun toMulHom✝ (x + y) = MulHom.toFun toMulHom✝ x + MulHom.toFun toMulHom✝ y

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'✝ }

mk.mk.e_toMulHom.a
↑toMulHom✝¹ = ↑toMulHom✝
    
F: Type ?u.11504

α: Type ?u.11507

β: Type ?u.11510

γ: Type ?u.11513

inst✝¹: NonUnitalNonAssocSemiring α

inst✝: NonUnitalNonAssocSemiring β

f, g: α →ₙ+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = 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'✝ }
h
Goals 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 y
NonUnitalRingHom.map_add'
  map_zero := 
NonUnitalRingHom.map_zero': ∀ {α : Type ?u.11797} {β : Type ?u.11796} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (self : α →ₙ+* β), MulHom.toFun self.toMulHom 0 = 0
NonUnitalRingHom.map_zero'
  map_mul 
f: ?m.11728
f := 
f: ?m.11728
f.
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 y
map_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 = ↑f
coe_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 = a
rfl
#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 = ↑f
NonUnitalRingHom.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 y
h₁ 
h₂: ?m.13439
h₂ 
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
h₃) :
    ((⟨⟨
f: α → β
f, 
h₁: ?m.13436
h₁⟩, 
h₂: ?m.13439
h₂, 
h₃: ?m.13442
h₃⟩ : 
α: Type ?u.13417
α →ₙ+* 
β: Type ?u.13420
β) : 
α: Type ?u.13417
α →ₙ* 
β: Type ?u.13420
β) = ⟨
f: α → β
f, 
h₁: ?m.13436
h₁⟩ :=
  
rfl: ∀ {α : Sort ?u.13856} {a : α}, a = a
rfl
#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) = ↑f
coe_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 = a
rfl
#align non_unital_ring_hom.coe_to_add_monoid_hom 
NonUnitalRingHom.coe_toAddMonoidHom: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β), ↑(toAddMonoidHom f) = ↑f
NonUnitalRingHom.coe_toAddMonoidHom

@[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 y
h₁ 
h₂: ?m.15067
h₂ 
h₃: ?m.15070
h₃) :
    ((⟨⟨
f: α → β
f, 
h₁: ?m.15064
h₁⟩, 
h₂: ?m.15067
h₂, 
h₃: ?m.15070
h₃⟩ : 
α: Type ?u.15045
α →ₙ+* 
β: Type ?u.15048
β) : 
α: Type ?u.15045
α →+ 
β: Type ?u.15048
β) = ⟨⟨
f: α → β
f, 
h₂: ?m.15067
h₂⟩, 
h₃: ?m.15070
h₃⟩ :=
  
rfl: ∀ {α : Sort ?u.16183} {a : α}, a = a
rfl
#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' = ↑f
h : 
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 →ₙ* N
copy
{ 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' = ↑f
h
{ 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 →+ N
copy
{ 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' = ↑f
h
{ 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.17337
with
{ 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' = ↑f
h : 
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' = ↑f
h) = 
f': α → β
f' :=
  
rfl: ∀ {α : Sort ?u.18525} {a : α}, a = a
rfl
#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 = f
copy_eq (
f: α →ₙ+* β
f : 
α: Type ?u.18581
α →ₙ+* 
β: Type ?u.18584
β) (
f': α → β
f' : 
α: Type ?u.18581
α → 
β: Type ?u.18584
β) (
h: f' = ↑f
h : 
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' = ↑f
h = 
f: α →ₙ+* β
f :=
  
FunLike.ext': ∀ {F : Sort ?u.19140} {α : Sort ?u.19138} {β : α → Sort ?u.19139} [i : FunLike F α β] {f g : F}, ↑f = ↑g → f = g
FunLike.ext' 
h: f' = ↑f
h
#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 = f
NonUnitalRingHom.copy_eq

end coe

section

variable [
NonUnitalNonAssocSemiring: Type ?u.20784 → Type ?u.20784
NonUnitalNonAssocSemiring 
α: Type ?u.19451
α] [
NonUnitalNonAssocSemiring: Type ?u.19463 → Type ?u.19463
NonUnitalNonAssocSemiring 
β: 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 = g
ext ⦃
f: α →ₙ+* β
f 
g: α →ₙ+* β
g : 
α: Type ?u.19509
α →ₙ+* 
β: Type ?u.19512
β⦄ : (∀ 
x: ?m.19572
x, 
f: α →ₙ+* β
f 
x: ?m.19572
x = 
g: α →ₙ+* β
g 
x: ?m.19572
x) → 
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 = g
FunLike.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 = g
NonUnitalRingHom.ext

theorem 
ext_iff: ∀ {f g : α →ₙ+* β}, f = g ↔ ∀ (x : α), ↑f x = ↑g x
ext_iff {
f: α →ₙ+* β
f 
g: α →ₙ+* β
g : 
α: Type ?u.20149
α →ₙ+* 
β: Type ?u.20152
β} : 
f: α →ₙ+* β
f = 
g: α →ₙ+* β
g ↔ ∀ 
x: ?m.20217
x, 
f: α →ₙ+* β
f 
x: ?m.20217
x = 
g: α →ₙ+* β
g 
x: ?m.20217
x :=
  
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 x
FunLike.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 x
NonUnitalRingHom.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₃ } = f
mk_coe (
f: α →ₙ+* β
f : 
α: Type ?u.20775
α →ₙ+* 
β: Type ?u.20778
β) (
h₁: ∀ (x y : α), ↑f (x * y) = ↑f x * ↑f y
h₁ 
h₂: MulHom.toFun { toFun := ↑f, map_mul' := h₁ } 0 = 0
h₂ 
h₃: ?m.20836
h₃) : 
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 →ₙ* N
MulHom.mk 
f: α →ₙ+* β
f 
h₁: ?m.20830
h₁) 
h₂: ?m.20833
h₂ 
h₃: ?m.20836
h₃ = 
f: α →ₙ+* β
f :=
  
ext: ∀ {α : Type ?u.21202} {β : Type ?u.21203} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  ⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = g
ext fun 
_: ?m.21230
_ => 
rfl: ∀ {α : Sort ?u.21232} {a : α}, a = a
rfl
#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₃ } = f
NonUnitalRingHom.mk_coe

theorem 
coe_addMonoidHom_injective: Injective fun f => ↑f
coe_addMonoidHom_injective : 
Injective: {α : Sort ?u.21353} → {β : Sort ?u.21352} → (α → β) → Prop
Injective fun 
f: α →ₙ+* β
f : 
α: Type ?u.21315
α →ₙ+* 
β: Type ?u.21318
β => (
f: α →ₙ+* β
f : 
α: Type ?u.21315
α →+ 
β: Type ?u.21318
β) :=
  fun 
_: ?m.21923
_ 
_: ?m.21926
_ 
h: ?m.21929
h => 
ext: ∀ {α : Type ?u.21931} {β : Type ?u.21932} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  ⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = g
ext <| 
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 x
FunLike.congr_fun (F := 
α: Type ?u.21315
α →+ 
β: Type ?u.21318
β) 
h: ?m.21929
h
#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 β],
  Injective fun f => ↑f
NonUnitalRingHom.coe_addMonoidHom_injective

set_option linter.deprecated false in
theorem 
coe_mulHom_injective: Injective fun f => ↑f
coe_mulHom_injective : 
Injective: {α : Sort ?u.22940} → {β : Sort ?u.22939} → (α → β) → Prop
Injective fun 
f: α →ₙ+* β
f : 
α: Type ?u.22902
α →ₙ+* 
β: Type ?u.22905
β => (
f: α →ₙ+* β
f : 
α: Type ?u.22902
α →ₙ* 
β: Type ?u.22905
β) := fun 
_: ?m.23211
_ 
_: ?m.23214
_ 
h: ?m.23217
h =>
  
ext: ∀ {α : Type ?u.23219} {β : Type ?u.23220} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  ⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = g
ext <| 
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 x
MulHom.congr_fun 
h: ?m.23217
h
#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 => ↑f
NonUnitalRingHom.coe_mulHom_injective

end

variable [
NonUnitalNonAssocSemiring: Type ?u.29984 → Type ?u.29984
NonUnitalNonAssocSemiring 
α: Type ?u.23437
α] [
NonUnitalNonAssocSemiring: Type ?u.29236 → Type ?u.29236
NonUnitalNonAssocSemiring 
β: 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.23473
NonUnitalNonAssocSemiring 
α: Type ?u.23470
α] : 
α: Type ?u.23470
α →ₙ+* 
α: Type ?u.23470
α := by
Goals accomplished! 🐙
  
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

α →ₙ+* αrefine' { toFun := 
id: {α : Sort ?u.23562} → α → α
id.. }
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

refine'_1
∀ (x y : α), id (x * y) = id x * id y
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

refine'_2
MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } 0 = 0
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: 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.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

α →ₙ+* α<;>
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

refine'_1
∀ (x y : α), id (x * y) = id x * id y
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

refine'_2
MulHom.toFun { toFun := id, map_mul' := ?refine'_1 } 0 = 0
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: 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.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

α →ₙ+* αintros
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

refine'_2
MulHom.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.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

α →ₙ+* α<;>
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

x✝, y✝: α

refine'_1
id (x✝ * y✝) = id x✝ * id y✝
F: Type ?u.23452

α✝: Type ?u.23455

β: Type ?u.23458

γ: Type ?u.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

refine'_2
MulHom.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.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

x✝, y✝: α

refine'_3
MulHom.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.23461

inst✝²: NonUnitalNonAssocSemiring α✝

inst✝¹: NonUnitalNonAssocSemiring β

α: Type ?u.23470

inst✝: NonUnitalNonAssocSemiring α

α →ₙ+* αrfl
Goals 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.23649
Zero (
α: Type ?u.23634
α →ₙ+* 
β: Type ?u.23637
β) :=
  ⟨{ toFun := 
0: ?m.23789
0, map_mul' := fun 
_: ?m.23981
_ 
_: ?m.23984
_ => (
mul_zero: ∀ {M₀ : Type ?u.23986} [self : MulZeroClass M₀] (a : M₀), a * 0 = 0
mul_zero (
0: ?m.23991
0 : 
β: Type ?u.23637
β)).
symm: ∀ {α : Sort ?u.24127} {a b : α}, a = b → b = a
symm, map_zero' := 
rfl: ∀ {α : Sort ?u.24149} {a : α}, a = a
rfl,
      map_add' := fun 
_: ?m.24154
_ 
_: ?m.24157
_ => (
add_zero: ∀ {M : Type ?u.24159} [inst : AddZeroClass M] (a : M), a + 0 = a
add_zero (
0: ?m.24164
0 : 
β: Type ?u.23637
β)).
symm: ∀ {α : Sort ?u.24346} {a b : α}, a = b → b = a
symm }⟩

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.24540
0⟩

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

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

@[simp]
theorem 
id_apply: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x : α), ↑(NonUnitalRingHom.id α) x = x
id_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 = a
rfl
#align non_unital_ring_hom.id_apply 
NonUnitalRingHom.id_apply: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x : α), ↑(NonUnitalRingHom.id α) x = x
NonUnitalRingHom.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 →+ M
AddMonoidHom.id 
α: Type ?u.26193
α :=
  
rfl: ∀ {α : Sort ?u.26552} {a : α}, a = a
rfl
#align non_unital_ring_hom.coe_add_monoid_hom_id 
NonUnitalRingHom.coe_addMonoidHom_id: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], ↑(NonUnitalRingHom.id α) = AddMonoidHom.id α
NonUnitalRingHom.coe_addMonoidHom_id

@[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 →ₙ* M
MulHom.id 
α: Type ?u.26599
α :=
  
rfl: ∀ {α : Sort ?u.26810} {a : α}, a = a
rfl
#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.33500
NonUnitalNonAssocSemiring 
γ: 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 →ₙ* P
comp
{ 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 →+ P
comp
{ 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.27765
with
{ 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.28260
NonUnitalNonAssocSemiring 
δ: ?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 = a
rfl
#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 ∘ ↑f
coe_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 = a
rfl
#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 ∘ ↑f
NonUnitalRingHom.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 = a
rfl
#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) },
      map_add' :=
        (_ :
          ∀ (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 ↑f
coe_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} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        (toZeroHom : ZeroHom M N) →
          (∀ (x y : M), ZeroHom.toFun toZeroHom (x + y) = ZeroHom.toFun toZeroHom x + ZeroHom.toFun toZeroHom y) →
            M →+ N
AddMonoidHom.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 = 0
map_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 y
map_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 →+ P
comp 
f: α →ₙ+* β
f :=
  
rfl: ∀ {α : Sort ?u.32007} {a : α}, a = a
rfl
#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) },
      map_add' :=
        (_ :
          ∀ (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 ↑f
NonUnitalRingHom.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 ↑f
coe_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 →ₙ* N
MulHom.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 y
map_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 →ₙ* P
comp 
f: α →ₙ+* β
f :=
  
rfl: ∀ {α : Sort ?u.33390} {a : α}, a = a
rfl
#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 ↑f
NonUnitalRingHom.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 = 0
comp_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.33585
0 : 
α: Type ?u.33485
α →ₙ+* 
β: Type ?u.33488
β) = 
0: ?m.33627
0 := by
Goals accomplished! 🐙
  
F: Type ?u.33482

α: Type u_3

β: Type u_1

γ: Type u_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

comp g 0 = 0ext
F: Type ?u.33482

α: Type u_3

β: Type u_1

γ: Type u_2

inst✝²: 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_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

comp g 0 = 0simp
Goals 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 = 0
NonUnitalRingHom.comp_zero

@[simp]
theorem 
zero_comp: ∀ (f : α →ₙ+* β), comp 0 f = 0
zero_comp (
f: α →ₙ+* β
f : 
α: Type ?u.34959
α →ₙ+* 
β: Type ?u.34962
β) : (
0: ?m.35038
0 : 
β: 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.35105
0 := by
Goals accomplished! 🐙
  
F: Type ?u.34956

α: Type u_1

β: Type u_2

γ: Type u_3

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g: β →ₙ+* γ

f✝, f: α →ₙ+* β

comp 0 f = 0ext
F: Type ?u.34956

α: Type u_1

β: Type u_2

γ: Type u_3

inst✝²: 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_3

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g: β →ₙ+* γ

f✝, f: α →ₙ+* β

comp 0 f = 0rfl
Goals 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 = 0
NonUnitalRingHom.zero_comp

@[simp]
theorem 
comp_id: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β), comp f (NonUnitalRingHom.id α) = f
comp_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 = g
ext fun 
_: ?m.35389
_ => 
rfl: ∀ {α : Sort ?u.35391} {a : α}, a = a
rfl
#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 α) = f
NonUnitalRingHom.comp_id

@[simp]
theorem 
id_comp: ∀ {α : Type u_1} {β : Type u_2} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β), comp (NonUnitalRingHom.id β) f = f
id_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 = g
ext fun 
_: ?m.35572
_ => 
rfl: ∀ {α : Sort ?u.35574} {a : α}, a = a
rfl
#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 = f
NonUnitalRingHom.id_comp

instance: {α : Type u_1} → [inst : NonUnitalNonAssocSemiring α] → MonoidWithZero (α →ₙ+* α)
instance : 
MonoidWithZero: Type ?u.35673 → Type ?u.35673
MonoidWithZero (
α: 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 α) = f
comp_id
  one_mul := 
id_comp: ∀ {α : Type ?u.35792} {β : Type ?u.35793} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  (f : α →ₙ+* β), comp (NonUnitalRingHom.id β) f = f
id_comp
  mul_assoc 
f: ?m.35732
f 
g: ?m.35735
g 
h: ?m.35738
h := 
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.35837
0
  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 = 0
comp_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 = 0
zero_comp

theorem 
one_def: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], 1 = NonUnitalRingHom.id α
one_def : (
1: ?m.36166
1 : 
α: Type ?u.36105
α →ₙ+* 
α: Type ?u.36105
α) = 
NonUnitalRingHom.id: (α : Type ?u.36355) → [inst : NonUnitalNonAssocSemiring α] → α →ₙ+* α
NonUnitalRingHom.id 
α: Type ?u.36105
α :=
  
rfl: ∀ {α : Sort ?u.36359} {a : α}, a = a
rfl
#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 = id
coe_one : ⇑(
1: ?m.36432
1 : 
α: Type ?u.36371
α →ₙ+* 
α: Type ?u.36371
α) = 
id: {α : Sort ?u.36789} → α → α
id :=
  
rfl: ∀ {α : Sort ?u.36835} {a : α}, a = a
rfl
#align non_unital_ring_hom.coe_one 
NonUnitalRingHom.coe_one: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α], ↑1 = id
NonUnitalRingHom.coe_one

theorem 
mul_def: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), f * g = comp f g
mul_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 = a
rfl
#align non_unital_ring_hom.mul_def 
NonUnitalRingHom.mul_def: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), f * g = comp f g
NonUnitalRingHom.mul_def

@[simp]
theorem 
coe_mul: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), ↑(f * g) = ↑f ∘ ↑g
coe_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 = a
rfl
#align non_unital_ring_hom.coe_mul 
NonUnitalRingHom.coe_mul: ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), ↑(f * g) = ↑f ∘ ↑g
NonUnitalRingHom.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 ↑f
hf : 
Surjective: {α : Sort ?u.38232} → {β : Sort ?u.38231} → (α → β) → Prop
Surjective 
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.38498
h => 
ext: ∀ {α : Type ?u.38500} {β : Type ?u.38501} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  ⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = g
ext <| 
hf: Surjective ↑f
hf.
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 → a
2 (
ext_iff: ∀ {α : Type ?u.38546} {β : Type ?u.38547} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  {f g : α →ₙ+* β}, f = g ↔ ∀ (x : α), ↑f x = ↑g x
ext_iff.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
h: ?m.38498
h), fun 
h: ?m.38628
h => 
h: ?m.38628
h ▸ 
rfl: ∀ {α : Sort ?u.38635} {a : α}, a = a
rfl⟩
#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 ↑g
hg : 
Injective: {α : Sort ?u.38769} → {β : Sort ?u.38768} → (α → β) → Prop
Injective 
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.39033
h => 
ext: ∀ {α : Type ?u.39035} {β : Type ?u.39036} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
  ⦃f g : α →ₙ+* β⦄, (∀ (x : α), ↑f x = ↑g x) → f = g
ext fun 
x: ?m.39063
x => 
hg: Injective ↑g
hg <| by
Goals accomplished! 🐙 
F: Type ?u.38681

α: Type u_3

β: Type u_1

γ: Type u_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

f₁, f₂: α →ₙ+* β

hg: Injective ↑g

h: 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_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

f₁, f₂: α →ₙ+* β

hg: Injective ↑g

h: 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_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

f₁, f₂: α →ₙ+* β

hg: Injective ↑g

h: 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_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

f₁, f₂: α →ₙ+* β

hg: Injective ↑g

h: 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_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

f₁, f₂: α →ₙ+* β

hg: Injective ↑g

h: 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_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

f₁, f₂: α →ₙ+* β

hg: Injective ↑g

h: 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_apply
F: Type ?u.38681

α: Type u_3

β: Type u_1

γ: Type u_2

inst✝²: NonUnitalNonAssocSemiring α

inst✝¹: NonUnitalNonAssocSemiring β

inst✝: NonUnitalNonAssocSemiring γ

g✝: β →ₙ+* γ

f: α →ₙ+* β

g: β →ₙ+* γ

f₁, f₂: α →ₙ+* β

hg: Injective ↑g

h: comp g f₁ = comp g f₂

x: α

↑g (↑f₂ x) = ↑g (↑f₂ x)]
Goals accomplished! 🐙, fun 
h: ?m.39088
h => 
h: ?m.39088
h ▸ 
rfl: ∀ {α : Sort ?u.39090} {a : α}, a = a
rfl⟩
#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.39413
NonAssocSemiring 
α: Type ?u.39407
α] [
NonAssocSemiring: Type ?u.39416 → Type ?u.39416
NonAssocSemiring 
β: 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
`MonoidWithZeroHomClass` already extends `MonoidHomClass`. -/
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.48337
F : 
Type _: Type (?u.48337+1)
Type _) (
α: outParam (Type ?u.48341)
α 
β: outParam (Type ?u.48345)
β : 
outParam: Sort ?u.48344 → Sort ?u.48344
outParam (
Type _: Type (?u.48341+1)
Type _)) [
NonAssocSemiring: Type ?u.48348 → Type ?u.48348
NonAssocSemiring 
α: outParam (Type ?u.48341)
α]
  [
NonAssocSemiring: Type ?u.48351 → Type ?u.48351
NonAssocSemiring 
β: 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.48337
F 
α: 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.48337
F 
α: 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.48337
F 
α: 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.48865
NonAssocSemiring 
α: Type ?u.48856
α] [
NonAssocSemiring: Type ?u.48868 → Type ?u.48868
NonAssocSemiring 
β: 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.48853
F 
α: Type ?u.48856
α 
β: Type ?u.48859
β]
    (
f: F
f : 
F: Type ?u.48853
F) (
a: α
a : 
α: Type ?u.48856
α) : (
f: F
f (
bit1: {α : Type ?u.49270} → [inst : One α] → [inst : Add α] → α → α
bit1 
a: α
a) : 
β: Type ?u.48859
β) = 
bit1: {α : Type ?u.49413} → [inst : One α] → [inst : Add α] → α → α
bit1 (
f: F
f 
a: α
a) := by
Goals accomplished! 🐙 
F: Type u_3

α: Type u_1

β: Type u_2

γ: Type ?u.48862

inst✝²: NonAssocSemiring α

inst✝¹: NonAssocSemiring β

inst✝: RingHomClass F α β

f: F

a: α

↑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.52034
NonAssocSemiring 
α: Type ?u.51067
α} {
_: NonAssocSemiring β
_ : 
NonAssocSemiring: Type ?u.51044 → Type ?u.51044
NonAssocSemiring 
β: 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.51029
F 
α: 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: F
f : 
F: Type ?u.51064
F) : 
α: Type ?u.51067
α →+* 
β: Type ?u.51070
β :=
{ (f : α →* β), (f : α →+ β) with }: ?m.51535 →+* ?m.51536
{ (
f: F
f
{ (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
f
{ (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.51536
with
{ (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.52022
F (
α: 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.52209
F 
α: 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.52363
with
{ ‹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.52651
NonAssocSemiring 
α: Type ?u.59553
α} {
_: NonAssocSemiring β
_ : 
NonAssocSemiring: Type ?u.57375 → Type ?u.57375
NonAssocSemiring 
β: 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.52890
f := 
f: ?m.52890
f.
toFun: {M : Type ?u.52913} → {N : Type ?u.52912} → [inst : One M] → [inst_1 : One N] → OneHom M N → M → N
toFun
  coe_injective' 
f: ?m.53017
f 
g: ?m.53020
g 
h: ?m.53023
h := by
Goals accomplished! 🐙
    
F: Type ?u.52657

α: Type ?u.52660

β: Type ?u.52663

γ: Type ?u.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

f, g: α →+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcases 
f: α →+* β
f
F: Type ?u.52657

α: Type ?u.52660

β: Type ?u.52663

γ: Type ?u.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

g: α →+* β

toMonoidHom✝: α →* β

map_zero'✝: OneHom.toFun (↑toMonoidHom✝) 0 = 0

map_add'✝: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y

h: (fun f => f.toFun) { toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } =   (fun f => f.toFun) g

mk
{ toMonoidHom := toMonoidHom✝, map_zero' := map_zero'✝, map_add' := map_add'✝ } = g
    
F: Type ?u.52657

α: Type ?u.52660

β: Type ?u.52663

γ: Type ?u.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

f, g: α →+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcases 
g: α →+* β
g
F: Type ?u.52657

α: Type ?u.52660

β: Type ?u.52663

γ: Type ?u.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

toMonoidHom✝¹: α →* β

map_zero'✝¹: OneHom.toFun (↑toMonoidHom✝¹) 0 = 0

map_add'✝¹: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y

toMonoidHom✝: α →* β

map_zero'✝: OneHom.toFun (↑toMonoidHom✝) 0 = 0

map_add'✝: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y

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'✝ }

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.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

f, g: α →+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gcongr
F: Type ?u.52657

α: Type ?u.52660

β: Type ?u.52663

γ: Type ?u.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

toMonoidHom✝¹: α →* β

map_zero'✝¹: OneHom.toFun (↑toMonoidHom✝¹) 0 = 0

map_add'✝¹: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y

toMonoidHom✝: α →* β

map_zero'✝: OneHom.toFun (↑toMonoidHom✝) 0 = 0

map_add'✝: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y

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'✝ }

mk.mk.e_toMonoidHom
toMonoidHom✝¹ = toMonoidHom✝
    
F: Type ?u.52657

α: Type ?u.52660

β: Type ?u.52663

γ: Type ?u.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

f, g: α →+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = gapply 
FunLike.coe_injective': ∀ {F : Sort ?u.53458} {α : outParam (Sort ?u.53457)} {β : outParam (α → Sort ?u.53456)} [self : FunLike F α β],
  Injective FunLike.coe
FunLike.coe_injective'
F: Type ?u.52657

α: Type ?u.52660

β: Type ?u.52663

γ: Type ?u.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

toMonoidHom✝¹: α →* β

map_zero'✝¹: OneHom.toFun (↑toMonoidHom✝¹) 0 = 0

map_add'✝¹: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝¹) (x + y) = OneHom.toFun (↑toMonoidHom✝¹) x + OneHom.toFun (↑toMonoidHom✝¹) y

toMonoidHom✝: α →* β

map_zero'✝: OneHom.toFun (↑toMonoidHom✝) 0 = 0

map_add'✝: ∀ (x y : α), OneHom.toFun (↑toMonoidHom✝) (x + y) = OneHom.toFun (↑toMonoidHom✝) x + OneHom.toFun (↑toMonoidHom✝) y

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'✝ }

mk.mk.e_toMonoidHom.a
↑toMonoidHom✝¹ = ↑toMonoidHom✝
    
F: Type ?u.52657

α: Type ?u.52660

β: Type ?u.52663

γ: Type ?u.52666

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

f, g: α →+* β

h: (fun f => f.toFun) f = (fun f => f.toFun) g

f = 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'✝ }
h
Goals 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) y
RingHom.map_add'
  map_zero := 
RingHom.map_zero': ∀ {α : Type ?u.53126} {β : Type ?u.53125} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (self : α →+* β),
  OneHom.toFun (↑self.toMonoidHom) 0 = 0
RingHom.map_zero'
  map_mul 
f: ?m.53036
f := 
f: ?m.53036
f.
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) y
map_mul'
  map_one 
f: ?m.53072
f := 
f: ?m.53072
f.
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 = 1
map_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 = ↑f
toFun_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 → N
toFun = 
f: α →+* β
f :=
  
rfl: ∀ {α : Sort ?u.55889} {a : α}, a = a
rfl
#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 = ↑f
RingHom.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₂ } = ↑f
coe_mk (
f: α →* β
f : 
α: Type ?u.55906
α →* 
β: Type ?u.55909
β) (
h₁: OneHom.toFun (↑f) 0 = 0
h₁ 
h₂: ?m.55966
h₂) : ((⟨
f: α →* β
f, 
h₁: ?m.55963
h₁, 
h₂: ?m.55966
h₂⟩ : 
α: Type ?u.55906
α →+* 
β: Type ?u.55909
β) : 
α: Type ?u.55906
α → 
β: Type ?u.55909
β) = 
f: α →* β
f :=
  
rfl: ∀ {α : Sort ?u.57305} {a : α}, a = a
rfl
#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₂ } = ↑f
RingHom.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 = ↑f
coe_coe {
F: Type u_1
F : 
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.57378
F 
α: Type ?u.57363
α 
β: Type ?u.57366
β] (
f: F
f : 
F: Type ?u.57378
F) : ((
f: F
f : 
α: Type ?u.57363
α →+* 
β: Type ?u.57366
β) : 
α: Type ?u.57363
α → 
β: Type ?u.57366
β) = 
f: F
f :=
  
rfl: ∀ {α : Sort ?u.58682} {a : α}, a = a
rfl
#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 = ↑f
RingHom.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 = ↑f
toMonoidHom_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 = a
rfl
#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 = ↑f
RingHom.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) = ↑f
toMonoidWithZeroHom_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 := by
Goals accomplished! 🐙
  
F: Type ?u.59550

α: Type u_1

β: Type u_2

γ: Type ?u.59559

x✝¹: NonAssocSemiring α

x✝: NonAssocSemiring β

f: α →+* β

↑(toMonoidWithZeroHom f) = ↑frfl
Goals 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) = ↑f
RingHom.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₂ } = f
coe_monoidHom_mk (
f: α →* β
f : 
α: Type ?u.60952
α →* 
β: Type ?u.60955
β) (
h₁: OneHom.toFun (↑f) 0 = 0
h₁ 
h₂: ?m.61012
h₂) : ((⟨
f: α →* β
f, 
h₁: ?m.61009
h₁, 
h₂: ?m.61012
h₂⟩ : 
α: Type ?u.60952
α →+* 
β: Type ?u.60955
β) : 
α: Type ?u.60952
α →* 
β: Type ?u.60955
β) = 
f: α →* β
f :=
  
rfl: ∀ {α : Sort ?u.61222} {a : α}, a = a
rfl
#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₂ } = f
RingHom.coe_monoidHom_mk

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

@[simp]
theorem 
toAddMonoidHom_eq_coe: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), toAddMonoidHom f = ↑f
toAddMonoidHom_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 = a
rfl
#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 = ↑f
RingHom.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.61644
h₁ 
h₂: ?m.61647
h₂ 
h₃: OneHom.toFun (↑{ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0
h₃ 
h₄: ?m.61653
h₄) :
    ((⟨⟨⟨
f: α → β
f, 
h₁: ?m.61644
h₁⟩, 
h₂: ?m.61647
h₂⟩, 
h₃: ?m.61650
h₃, 
h₄: ?m.61653
h₄⟩ : 
α: Type ?u.61625
α →+* 
β: Type ?u.61628
β) : 
α: Type ?u.61625
α →+ 
β: Type ?u.61628
β) = ⟨⟨
f: α → β
f, 
h₃: ?m.61650
h₃⟩, 
h₄: ?m.61653
h₄⟩ :=
  
rfl: ∀ {α : Sort ?u.62482} {a : α}, a = a
rfl
#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' = ↑f
h : 
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 →* N
copy
{ 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' = ↑f
h
{ 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 →+ N
copy
{ 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' = ↑f
h
{ 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.63657
with
{ 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' = ↑f
h : 
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' = ↑f
h) = 
f': α → β
f' :=
  
rfl: ∀ {α : Sort ?u.65593} {a : α}, a = a
rfl
#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 = f
copy_eq (
f: α →+* β
f : 
α: Type ?u.65649
α →+* 
β: Type ?u.65652
β) (
f': α → β
f' : 
α: Type ?u.65649
α → 
β: Type ?u.65652
β) (
h: f' = ↑f
h : 
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' = ↑f
h = 
f: α →+* β
f :=
  
FunLike.ext': ∀ {F : Sort ?u.66548} {α : Sort ?u.66546} {β : α → Sort ?u.66547} [i : FunLike F α β] {f g : F}, ↑f = ↑g → f = g
FunLike.ext' 
h: f' = ↑f
h
#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 = f
RingHom.copy_eq

end coe

section

variable {
_: NonAssocSemiring α
_ : 
NonAssocSemiring: Type ?u.75665 → Type ?u.75665
NonAssocSemiring 
α: Type ?u.67192
α} {
_: NonAssocSemiring β
_ : 
NonAssocSemiring: Type ?u.69477 → Type ?u.69477
NonAssocSemiring 
β: 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_2
congr_fun {
f: α →+* β
f 
g: α →+* β
g : 
α: Type ?u.67230
α →+* 
β: Type ?u.67233
β} (
h: f = g
h : 
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 x
FunLike.congr_fun 
h: f = g
h 
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_2
RingHom.congr_fun

theorem 
congr_arg: ∀ (f : α →+* β) {x y : α}, x = y → ↑f x = ↑f y
congr_arg (
f: α →+* β
f : 
α: Type ?u.68346
α →+* 
β: Type ?u.68349
β) {
x: α
x 
y: α
y : 
α: Type ?u.68346
α} (
h: x = y
h : 
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 y
FunLike.congr_arg 
f: α →+* β
f 
h: x = y
h
#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 y
RingHom.congr_arg

theorem 
coe_inj: ∀ ⦃f g : α →+* β⦄, ↑f = ↑g → f = g
coe_inj ⦃
f: α →+* β
f 
g: α →+* β
g : 
α: Type ?u.69465
α →+* 
β: Type ?u.69468
β⦄ (
h: ↑f = ↑g
h : (
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 => ↑f
FunLike.coe_injective 
h: ↑f = ↑g
h
#align ring_hom.coe_inj 
RingHom.coe_inj: ∀ {α : Type u_1} {β : Type u_2} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, ↑f = ↑g → f = g
RingHom.coe_inj

@[ext]
theorem 
ext: ∀ {α :