/-
Copyright (c) 2014 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module data.nat.cast.basic
! leanprover-community/mathlib commit acebd8d49928f6ed8920e502a6c90674e75bd441
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.CharZero.Defs
import Mathlib.Algebra.GroupWithZero.Commute
import Mathlib.Algebra.Hom.Ring
import Mathlib.Algebra.Order.Group.Abs
import Mathlib.Algebra.Ring.Commute
import Mathlib.Data.Nat.Order.Basic
import Mathlib.Algebra.Group.Opposite

/-!
# Cast of natural numbers (additional theorems)

This file proves additional properties about the *canonical* homomorphism from
the natural numbers into an additive monoid with a one (`Nat.cast`).

## Main declarations

* `castAddMonoidHom`: `cast` bundled as an `AddMonoidHom`.
* `castRingHom`: `cast` bundled as a `RingHom`.
-/

-- Porting note: There are many occasions below where we need `simp [map_zero f]`
-- where `simp [map_zero]` should suffice. (Similarly for `map_one`.)
-- See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20regression.20with.20MonoidHomClass

variable {α: Type ?u.33331
α β: Type ?u.11
β : Type _: Type (?u.6990+1)
Type _}

namespace Nat

/-- `Nat.cast : ℕ → α` as an `AddMonoidHom`. -/
def castAddMonoidHom: (α : Type u_1) → [inst : AddMonoidWithOne α] → ℕ →+ α
castAddMonoidHom (α: Type ?u.14
α : Type _: Type (?u.14+1)
Type _) [AddMonoidWithOne: Type ?u.17 → Type ?u.17
AddMonoidWithOne α: Type ?u.14
α] :
    ℕ: Type
ℕ →+ α: Type ?u.14
α where
  toFun := Nat.cast: {R : Type ?u.566} → [inst : NatCast R] → ℕ → R
Nat.cast
  map_add' := cast_add: ∀ {R : Type ?u.743} [inst : AddMonoidWithOne R] (m n : ℕ), ↑(m + n) = ↑m + ↑n
cast_add
  map_zero' := cast_zero: ∀ {R : Type ?u.725} [inst : AddMonoidWithOne R], ↑0 = 0
cast_zero
#align nat.cast_add_monoid_hom Nat.castAddMonoidHom: (α : Type u_1) → [inst : AddMonoidWithOne α] → ℕ →+ α
Nat.castAddMonoidHom

@[simp]
theorem coe_castAddMonoidHom: ∀ {α : Type u_1} [inst : AddMonoidWithOne α], ↑(castAddMonoidHom α) = Nat.cast
coe_castAddMonoidHom [AddMonoidWithOne: Type ?u.824 → Type ?u.824
AddMonoidWithOne α: Type ?u.818
α] : (castAddMonoidHom: (α : Type ?u.831) → [inst : AddMonoidWithOne α] → ℕ →+ α
castAddMonoidHom α: Type ?u.818
α : ℕ: Type
ℕ → α: Type ?u.818
α) = Nat.cast: {R : Type ?u.1820} → [inst : NatCast R] → ℕ → R
Nat.cast :=
  rfl: ∀ {α : Sort ?u.2066} {a : α}, a = a
rfl
#align nat.coe_cast_add_monoid_hom Nat.coe_castAddMonoidHom: ∀ {α : Type u_1} [inst : AddMonoidWithOne α], ↑(castAddMonoidHom α) = Nat.cast
Nat.coe_castAddMonoidHom

@[simp, norm_cast]
theorem cast_mul: ∀ [inst : NonAssocSemiring α] (m n : ℕ), ↑(m * n) = ↑m * ↑n
cast_mul [NonAssocSemiring: Type ?u.2103 → Type ?u.2103
NonAssocSemiring α: Type ?u.2097
α] (m: ℕ
m n: ℕ
n : ℕ: Type
ℕ) : ((m: ℕ
m * n: ℕ
n : ℕ: Type
ℕ) : α: Type ?u.2097
α) = m: ℕ
m * n: ℕ
n := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n: ℕ

↑(m * n) = ↑m * ↑ninduction n: ℕ
nα: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m: ℕ

zero↑(m * zero) = ↑m * ↑zero
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n✝: ℕ

n_ih✝: ↑(m * n✝) = ↑m * ↑n✝

succ↑(m * succ n✝) = ↑m * ↑(succ n✝) α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n: ℕ

↑(m * n) = ↑m * ↑n<;>α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m: ℕ

zero↑(m * zero) = ↑m * ↑zero
α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n✝: ℕ

n_ih✝: ↑(m * n✝) = ↑m * ↑n✝

succ↑(m * succ n✝) = ↑m * ↑(succ n✝) α: Type u_1

β: Type ?u.2100

inst✝: NonAssocSemiring α

m, n: ℕ

↑(m * n) = ↑m * ↑nsimp [mul_succ: ∀ (n m : ℕ), n * succ m = n * m + n
mul_succ, mul_add: ∀ {R : Type ?u.3816} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
  a * (b + c) = a * b + a * c
mul_add, *]
Goals accomplished! 🐙
#align nat.cast_mul Nat.cast_mul: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (m n : ℕ), ↑(m * n) = ↑m * ↑n
Nat.cast_mul

/-- `Nat.cast : ℕ → α` as a `RingHom` -/
def castRingHom: (α : Type u_1) → [inst : NonAssocSemiring α] → ℕ →+* α
castRingHom (α: Type ?u.4477
α : Type _: Type (?u.4477+1)
Type _) [NonAssocSemiring: Type ?u.4480 → Type ?u.4480
NonAssocSemiring α: Type ?u.4477
α] : ℕ: Type
ℕ →+* α: Type ?u.4477
α :=
  { castAddMonoidHom: (α : Type ?u.4511) → [inst : AddMonoidWithOne α] → ℕ →+ α
castAddMonoidHom α: Type ?u.4477
α with toFun := Nat.cast: {R : Type ?u.4854} → [inst : NatCast R] → ℕ → R
Nat.cast, map_one' := cast_one: ∀ {R : Type ?u.4997} [inst : AddMonoidWithOne R], ↑1 = 1
cast_one, map_mul' := cast_mul: ∀ {α : Type ?u.5014} [inst : NonAssocSemiring α] (m n : ℕ), ↑(m * n) = ↑m * ↑n
cast_mul }
#align nat.cast_ring_hom Nat.castRingHom: (α : Type u_1) → [inst : NonAssocSemiring α] → ℕ →+* α
Nat.castRingHom

@[simp]
theorem coe_castRingHom: ∀ {α : Type u_1} [inst : NonAssocSemiring α], ↑(castRingHom α) = Nat.cast
coe_castRingHom [NonAssocSemiring: Type ?u.5452 → Type ?u.5452
NonAssocSemiring α: Type ?u.5446
α] : (castRingHom: (α : Type ?u.5459) → [inst : NonAssocSemiring α] → ℕ →+* α
castRingHom α: Type ?u.5446
α : ℕ: Type
ℕ → α: Type ?u.5446
α) = Nat.cast: {R : Type ?u.5996} → [inst : NatCast R] → ℕ → R
Nat.cast :=
  rfl: ∀ {α : Sort ?u.6222} {a : α}, a = a
rfl
#align nat.coe_cast_ring_hom Nat.coe_castRingHom: ∀ {α : Type u_1} [inst : NonAssocSemiring α], ↑(castRingHom α) = Nat.cast
Nat.coe_castRingHom

theorem cast_commute: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α), Commute (↑n) x
cast_commute [NonAssocSemiring: Type ?u.6259 → Type ?u.6259
NonAssocSemiring α: Type ?u.6253
α] (n: ℕ
n : ℕ: Type
ℕ) (x: α
x : α: Type ?u.6253
α) : Commute: {S : Type ?u.6266} → [inst : Mul S] → S → S → Prop
Commute (n: ℕ
n : α: Type ?u.6253
α) x: α
x := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

n: ℕ

x: α

Commute (↑n) xinduction n: ℕ
n with
  α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

n: ℕ

x: α

Commute (↑n) x| zero: ℕ
zero => α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

zeroCommute (↑zero) xrw [α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

zeroCommute (↑zero) xNat.cast_zero: ∀ {R : Type ?u.6600} [inst : AddMonoidWithOne R], ↑0 = 0
Nat.cast_zeroα: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

zeroCommute 0 x]α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

zeroCommute 0 x;α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

zeroCommute 0 x α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

zeroCommute (↑zero) xexact Commute.zero_left: ∀ {G₀ : Type ?u.6732} [inst : MulZeroClass G₀] (a : G₀), Commute 0 a
Commute.zero_left x: α
x
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

n: ℕ

x: α

Commute (↑n) x| succ: ℕ → ℕ
succ n: ℕ
n ihn: ?m.6594 n
ihn => α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n: ℕ

ihn: Commute (↑n) x

succCommute (↑(succ n)) xrw [α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n: ℕ

ihn: Commute (↑n) x

succCommute (↑(succ n)) xNat.cast_succ: ∀ {R : Type ?u.6825} [inst : AddMonoidWithOne R] (n : ℕ), ↑(succ n) = ↑n + 1
Nat.cast_succα: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n: ℕ

ihn: Commute (↑n) x

succCommute (↑n + 1) x]α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n: ℕ

ihn: Commute (↑n) x

succCommute (↑n + 1) x;α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n: ℕ

ihn: Commute (↑n) x

succCommute (↑n + 1) x α: Type u_1

β: Type ?u.6256

inst✝: NonAssocSemiring α

x: α

n: ℕ

ihn: Commute (↑n) x

succCommute (↑(succ n)) xexact ihn: ?m.6594 n
ihn.add_left: ∀ {R : Type ?u.6866} [inst : Distrib R] {a b c : R}, Commute a c → Commute b c → Commute (a + b) c
add_left (Commute.one_left: ∀ {M : Type ?u.6958} [inst : MulOneClass M] (a : M), Commute 1 a
Commute.one_left x: α
x)
Goals accomplished! 🐙
#align nat.cast_commute Nat.cast_commute: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α), Commute (↑n) x
Nat.cast_commute

theorem cast_comm: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α), ↑n * x = x * ↑n
cast_comm [NonAssocSemiring: Type ?u.6996 → Type ?u.6996
NonAssocSemiring α: Type ?u.6990
α] (n: ℕ
n : ℕ: Type
ℕ) (x: α
x : α: Type ?u.6990
α) : (n: ℕ
n : α: Type ?u.6990
α) * x: α
x = x: α
x * n: ℕ
n :=
  (cast_commute: ∀ {α : Type ?u.7644} [inst : NonAssocSemiring α] (n : ℕ) (x : α), Commute (↑n) x
cast_commute n: ℕ
n x: α
x).eq: ∀ {S : Type ?u.7651} [inst : Mul S] {a b : S}, Commute a b → a * b = b * a
eq
#align nat.cast_comm Nat.cast_comm: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α), ↑n * x = x * ↑n
Nat.cast_comm

theorem commute_cast: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ℕ), Commute x ↑n
commute_cast [NonAssocSemiring: Type ?u.7783 → Type ?u.7783
NonAssocSemiring α: Type ?u.7777
α] (x: α
x : α: Type ?u.7777
α) (n: ℕ
n : ℕ: Type
ℕ) : Commute: {S : Type ?u.7790} → [inst : Mul S] → S → S → Prop
Commute x: α
x n: ℕ
n :=
  (n: ℕ
n.cast_commute: ∀ {α : Type ?u.8103} [inst : NonAssocSemiring α] (n : ℕ) (x : α), Commute (↑n) x
cast_commute x: α
x).symm: ∀ {S : Type ?u.8114} [inst : Mul S] {a b : S}, Commute a b → Commute b a
symm
#align nat.commute_cast Nat.commute_cast: ∀ {α : Type u_1} [inst : NonAssocSemiring α] (x : α) (n : ℕ), Commute x ↑n
Nat.commute_cast

section OrderedSemiring

variable [OrderedSemiring: Type ?u.13765 → Type ?u.13765
OrderedSemiring α: Type ?u.13759
α]

@[mono]
theorem mono_cast: Monotone Nat.cast
mono_cast : Monotone: {α : Type ?u.8256} → {β : Type ?u.8255} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone (Nat.cast: {R : Type ?u.8296} → [inst : NatCast R] → ℕ → R
Nat.cast : ℕ: Type
ℕ → α: Type ?u.8246
α) :=
  monotone_nat_of_le_succ: ∀ {α : Type ?u.8523} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f n ≤ f (n + 1)) → Monotone f
monotone_nat_of_le_succ fun n: ?m.8577
n ↦ by
Goals accomplished! 🐙
    α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n: ℕ

↑n ≤ ↑(n + 1)rw [α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n: ℕ

↑n ≤ ↑(n + 1)Nat.cast_succ: ∀ {R : Type ?u.8680} [inst : AddMonoidWithOne R] (n : ℕ), ↑(succ n) = ↑n + 1
Nat.cast_succα: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n: ℕ

↑n ≤ ↑n + 1]α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n: ℕ

↑n ≤ ↑n + 1;α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n: ℕ

↑n ≤ ↑n + 1 α: Type u_1

β: Type ?u.8249

inst✝: OrderedSemiring α

n: ℕ

↑n ≤ ↑(n + 1)exact le_add_of_nonneg_right: ∀ {α : Type ?u.8894} [inst : AddZeroClass α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 ≤ b → a ≤ a + b
le_add_of_nonneg_right zero_le_one: ∀ {α : Type ?u.9108} [inst : Zero α] [inst_1 : One α] [inst_2 : LE α] [inst_3 : ZeroLEOneClass α], 0 ≤ 1
zero_le_one
Goals accomplished! 🐙
#align nat.mono_cast Nat.mono_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α], Monotone Nat.cast
Nat.mono_cast

@[simp]
theorem cast_nonneg: ∀ {α : Type u_1} [inst : OrderedSemiring α] (n : ℕ), 0 ≤ ↑n
cast_nonneg (n: ℕ
n : ℕ: Type
ℕ) : 0: ?m.9719
0 ≤ (n: ℕ
n : α: Type ?u.9706
α) :=
  @Nat.cast_zero: ∀ {R : Type ?u.10082} [inst : AddMonoidWithOne R], ↑0 = 0
Nat.cast_zero α: Type ?u.9706
α _ ▸ mono_cast: ∀ {α : Type ?u.10225} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast (Nat.zero_le: ∀ (n : ℕ), 0 ≤ n
Nat.zero_le n: ℕ
n)
#align nat.cast_nonneg Nat.cast_nonneg: ∀ {α : Type u_1} [inst : OrderedSemiring α] (n : ℕ), 0 ≤ ↑n
Nat.cast_nonneg

section Nontrivial

variable [Nontrivial: Type ?u.10295 → Prop
Nontrivial α: Type ?u.10286
α]

theorem cast_add_one_pos: ∀ (n : ℕ), 0 < ↑n + 1
cast_add_one_pos (n: ℕ
n : ℕ: Type
ℕ) : 0: ?m.10314
0 < (n: ℕ
n : α: Type ?u.10298
α) + 1: ?m.10445
1 :=
  zero_lt_one: ∀ {α : Type ?u.11032} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
  [inst_4 : NeZero 1], 0 < 1
zero_lt_one.trans_le: ∀ {α : Type ?u.11342} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < c
trans_le <| le_add_of_nonneg_left: ∀ {α : Type ?u.11522} [inst : AddZeroClass α] [inst_1 : LE α]
  [inst_2 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 ≤ b → a ≤ b + a
le_add_of_nonneg_left n: ℕ
n.cast_nonneg: ∀ {α : Type ?u.11728} [inst : OrderedSemiring α] (n : ℕ), 0 ≤ ↑n
cast_nonneg
#align nat.cast_add_one_pos Nat.cast_add_one_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] (n : ℕ), 0 < ↑n + 1
Nat.cast_add_one_pos

@[simp]
theorem cast_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {n : ℕ}, 0 < ↑n ↔ 0 < n
cast_pos {n: ℕ
n : ℕ: Type
ℕ} : (0: ?m.12335
0 : α: Type ?u.12318
α) < n: ℕ
n ↔ 0: ?m.12762
0 < n: ℕ
n := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n: ℕ

0 < ↑n ↔ 0 < ncases n: ℕ
nα: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

zero0 < ↑zero ↔ 0 < zero
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n✝: ℕ

succ0 < ↑(succ n✝) ↔ 0 < succ n✝ α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n: ℕ

0 < ↑n ↔ 0 < n<;>α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

zero0 < ↑zero ↔ 0 < zero
α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n✝: ℕ

succ0 < ↑(succ n✝) ↔ 0 < succ n✝ α: Type u_1

β: Type ?u.12321

inst✝¹: OrderedSemiring α

inst✝: Nontrivial α

n: ℕ

0 < ↑n ↔ 0 < nsimp [cast_add_one_pos: ∀ {α : Type ?u.12848} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] (n : ℕ), 0 < ↑n + 1
cast_add_one_pos]
Goals accomplished! 🐙
#align nat.cast_pos Nat.cast_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] {n : ℕ}, 0 < ↑n ↔ 0 < n
Nat.cast_pos

end Nontrivial

variable [CharZero: (R : Type ?u.15455) → [inst : AddMonoidWithOne R] → Prop
CharZero α: Type ?u.13759
α] {m: ℕ
m n: ℕ
n : ℕ: Type
ℕ}

theorem strictMono_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
strictMono_cast : StrictMono: {α : Type ?u.14076} → {β : Type ?u.14075} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
StrictMono (Nat.cast: {R : Type ?u.14116} → [inst : NatCast R] → ℕ → R
Nat.cast : ℕ: Type
ℕ → α: Type ?u.13917
α) :=
  mono_cast: ∀ {α : Type ?u.14343} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast.strictMono_of_injective: ∀ {α : Type ?u.14352} {β : Type ?u.14351} [inst : Preorder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Injective f → StrictMono f
strictMono_of_injective cast_injective: ∀ {R : Type ?u.14458} [inst : AddMonoidWithOne R] [inst_1 : CharZero R], Function.Injective Nat.cast
cast_injective
#align nat.strict_mono_cast Nat.strictMono_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
Nat.strictMono_cast

/-- `Nat.cast : ℕ → α` as an `OrderEmbedding` -/
@[simps! (config := { fullyApplied := false: Bool
false })]
def castOrderEmbedding: ℕ ↪o α
castOrderEmbedding : ℕ: Type
ℕ ↪o α: Type ?u.14695
α :=
  OrderEmbedding.ofStrictMono: {α : Type ?u.14965} →
  {β : Type ?u.14964} → [inst : LinearOrder α] → [inst_1 : Preorder β] → (f : α → β) → StrictMono f → α ↪o β
OrderEmbedding.ofStrictMono Nat.cast: {R : Type ?u.15095} → [inst : NatCast R] → ℕ → R
Nat.cast Nat.strictMono_cast: ∀ {α : Type ?u.15174} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
Nat.strictMono_cast
#align nat.cast_order_embedding Nat.castOrderEmbedding: {α : Type u_1} → [inst : OrderedSemiring α] → [inst_1 : CharZero α] → ℕ ↪o α
Nat.castOrderEmbedding
#align nat.cast_order_embedding_apply Nat.castOrderEmbedding_apply: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α], ↑castOrderEmbedding = Nat.cast
Nat.castOrderEmbedding_apply

@[simp, norm_cast]
theorem cast_le: ↑m ≤ ↑n ↔ m ≤ n
cast_le : (m: ℕ
m : α: Type ?u.15446
α) ≤ n: ℕ
n ↔ m: ℕ
m ≤ n: ℕ
n :=
  strictMono_cast: ∀ {α : Type ?u.15979} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
strictMono_cast.le_iff_le: ∀ {α : Type ?u.15992} {β : Type ?u.15991} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {a b : α}, f a ≤ f b ↔ a ≤ b
le_iff_le
#align nat.cast_le Nat.cast_le: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
Nat.cast_le

@[simp, norm_cast, mono]
theorem cast_lt: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : ℕ}, ↑m < ↑n ↔ m < n
cast_lt : (m: ℕ
m : α: Type ?u.16299
α) < n: ℕ
n ↔ m: ℕ
m < n: ℕ
n :=
  strictMono_cast: ∀ {α : Type ?u.16832} [inst : OrderedSemiring α] [inst_1 : CharZero α], StrictMono Nat.cast
strictMono_cast.lt_iff_lt: ∀ {α : Type ?u.16845} {β : Type ?u.16844} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ {a b : α}, f a < f b ↔ a < b
lt_iff_lt
#align nat.cast_lt Nat.cast_lt: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : ℕ}, ↑m < ↑n ↔ m < n
Nat.cast_lt

@[simp, norm_cast]
theorem one_lt_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : ℕ}, 1 < ↑n ↔ 1 < n
one_lt_cast : 1: ?m.17312
1 < (n: ℕ
n : α: Type ?u.17152
α) ↔ 1: ?m.17609
1 < n: ℕ
n := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

1 < ↑n ↔ 1 < nrw [α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

1 < ↑n ↔ 1 < n← cast_one: ∀ {R : Type ?u.17644} [inst : AddMonoidWithOne R], ↑1 = 1
cast_one,α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑1 < ↑n ↔ 1 < n α: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

1 < ↑n ↔ 1 < ncast_lt: ∀ {α : Type ?u.17812} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : ℕ}, ↑m < ↑n ↔ m < n
cast_ltα: Type u_1

β: Type ?u.17155

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

1 < n ↔ 1 < n]
Goals accomplished! 🐙
#align nat.one_lt_cast Nat.one_lt_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : ℕ}, 1 < ↑n ↔ 1 < n
Nat.one_lt_cast

@[simp, norm_cast]
theorem one_le_cast: 1 ≤ ↑n ↔ 1 ≤ n
one_le_cast : 1: ?m.18162
1 ≤ (n: ℕ
n : α: Type ?u.18002
α) ↔ 1: ?m.18459
1 ≤ n: ℕ
n := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

1 ≤ ↑n ↔ 1 ≤ nrw [α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

1 ≤ ↑n ↔ 1 ≤ n← cast_one: ∀ {R : Type ?u.18494} [inst : AddMonoidWithOne R], ↑1 = 1
cast_one,α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑1 ≤ ↑n ↔ 1 ≤ n α: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

1 ≤ ↑n ↔ 1 ≤ ncast_le: ∀ {α : Type ?u.18662} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
cast_leα: Type u_1

β: Type ?u.18005

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

1 ≤ n ↔ 1 ≤ n]
Goals accomplished! 🐙
#align nat.one_le_cast Nat.one_le_cast: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : ℕ}, 1 ≤ ↑n ↔ 1 ≤ n
Nat.one_le_cast

@[simp, norm_cast]
theorem cast_lt_one: ↑n < 1 ↔ n = 0
cast_lt_one : (n: ℕ
n : α: Type ?u.18852
α) < 1: ?m.19124
1 ↔ n: ℕ
n = 0: ?m.19304
0 := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n < 1 ↔ n = 0rw [α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n < 1 ↔ n = 0← cast_one: ∀ {R : Type ?u.19330} [inst : AddMonoidWithOne R], ↑1 = 1
cast_one,α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n < ↑1 ↔ n = 0 α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n < 1 ↔ n = 0cast_lt: ∀ {α : Type ?u.19498} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : ℕ}, ↑m < ↑n ↔ m < n
cast_lt,α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

n < 1 ↔ n = 0 α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n < 1 ↔ n = 0lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
lt_succ_iff,α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

n ≤ 0 ↔ n = 0 α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n < 1 ↔ n = 0← bot_eq_zero: ∀ {α : Type ?u.19549} [inst : CanonicallyOrderedAddMonoid α], ⊥ = 0
bot_eq_zero,α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

n ≤ ⊥ ↔ n = ⊥ α: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n < 1 ↔ n = 0le_bot_iff: ∀ {α : Type ?u.19579} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, a ≤ ⊥ ↔ a = ⊥
le_bot_iffα: Type u_1

β: Type ?u.18855

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

n = ⊥ ↔ n = ⊥]
Goals accomplished! 🐙
#align nat.cast_lt_one Nat.cast_lt_one: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : ℕ}, ↑n < 1 ↔ n = 0
Nat.cast_lt_one

@[simp, norm_cast]
theorem cast_le_one: ↑n ≤ 1 ↔ n ≤ 1
cast_le_one : (n: ℕ
n : α: Type ?u.19890
α) ≤ 1: ?m.20162
1 ↔ n: ℕ
n ≤ 1: ?m.20342
1 := by
Goals accomplished! 🐙 α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n ≤ 1 ↔ n ≤ 1rw [α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n ≤ 1 ↔ n ≤ 1← cast_one: ∀ {R : Type ?u.20372} [inst : AddMonoidWithOne R], ↑1 = 1
cast_one,α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n ≤ ↑1 ↔ n ≤ 1 α: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

↑n ≤ 1 ↔ n ≤ 1cast_le: ∀ {α : Type ?u.20540} [inst : OrderedSemiring α] [inst_1 : CharZero α] {m n : ℕ}, ↑m ≤ ↑n ↔ m ≤ n
cast_leα: Type u_1

β: Type ?u.19893

inst✝¹: OrderedSemiring α

inst✝: CharZero α

m, n: ℕ

n ≤ 1 ↔ n ≤ 1]
Goals accomplished! 🐙
#align nat.cast_le_one Nat.cast_le_one: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : CharZero α] {n : ℕ}, ↑n ≤ 1 ↔ n ≤ 1
Nat.cast_le_one

end OrderedSemiring

/-- A version of `Nat.cast_sub` that works for `ℝ≥0` and `ℚ≥0`. Note that this proof doesn't work
for `ℕ∞` and `ℝ≥0∞`, so we use type-specific lemmas for these types. -/
@[simp, norm_cast]
theorem cast_tsub: ∀ {α : Type u_1} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
  [inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (m n : ℕ), ↑(m - n) = ↑m - ↑n
cast_tsub [CanonicallyOrderedCommSemiring: Type ?u.20733 → Type ?u.20733
CanonicallyOrderedCommSemiring α: Type ?u.20727
α] [Sub: Type ?u.20736 → Type ?u.20736
Sub α: Type ?u.20727
α] [OrderedSub: (α : Type ?u.20739) → [inst : LE α] → [inst : Add α] → [inst : Sub α] → Prop
OrderedSub α: Type ?u.20727
α]
    [ContravariantClass: (M : Type ?u.21006) → (N : Type ?u.21005) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass α: Type ?u.20727
α α: Type ?u.20727
α (· + ·): α → α → α
(· + ·) (· ≤ ·): α → α → Prop
(· ≤ ·)] (m: ℕ
m n: ℕ
n : ℕ: Type
ℕ) : ↑(m: ℕ
m - n: ℕ
n) = (m: ℕ
m - n: ℕ
n : α: Type ?u.20727
α) := by
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

↑(m - n) = ↑m - ↑ncases' le_total: ∀ {α : Type ?u.21653} [inst : LinearOrder α] (a b : α), a ≤ b ∨ b ≤ a
le_total m: ℕ
m n: ℕ
n with h: ?m.21686
h h: ?m.21687
hα: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑(m - n) = ↑m - ↑n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: n ≤ m

inr↑(m - n) = ↑m - ↑n
  α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

↑(m - n) = ↑m - ↑n·α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑(m - n) = ↑m - ↑n α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑(m - n) = ↑m - ↑n
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: n ≤ m

inr↑(m - n) = ↑m - ↑nrw [α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑(m - n) = ↑m - ↑ntsub_eq_zero_of_le: ∀ {α : Type ?u.21729} [inst : CanonicallyOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
  a ≤ b → a - b = 0
tsub_eq_zero_of_le h: ?m.21686
h,α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑0 = ↑m - ↑n α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑(m - n) = ↑m - ↑ncast_zero: ∀ {R : Type ?u.21772} [inst : AddMonoidWithOne R], ↑0 = 0
cast_zero,α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl0 = ↑m - ↑n α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑(m - n) = ↑m - ↑ntsub_eq_zero_of_le: ∀ {α : Type ?u.21955} [inst : CanonicallyOrderedAddMonoid α] [inst_1 : Sub α] [inst_2 : OrderedSub α] {a b : α},
  a ≤ b → a - b = 0
tsub_eq_zero_of_leα: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl0 = 0
α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑m ≤ ↑n]α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑m ≤ ↑n
    α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: m ≤ n

inl↑(m - n) = ↑m - ↑nexact mono_cast: ∀ {α : Type ?u.22049} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast h: ?m.21686
h
Goals accomplished! 🐙
  α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

↑(m - n) = ↑m - ↑n·α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: n ≤ m

inr↑(m - n) = ↑m - ↑n α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: n ≤ m

inr↑(m - n) = ↑m - ↑nrcases le_iff_exists_add': ∀ {α : Type ?u.22087} [inst : CanonicallyOrderedAddMonoid α] {a b : α}, a ≤ b ↔ ∃ c, b = c + a
le_iff_exists_add'.mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp h: ?m.21687
h with ⟨m, rfl⟩: ∃ c, m = c + n
⟨m: ℕ
m⟨m, rfl⟩: ∃ c, m = c + n
, rfl: m✝ = m + n
rfl⟨m, rfl⟩: ∃ c, m = c + n
⟩α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

n, m: ℕ

h: n ≤ m + n

inr.intro↑(m + n - n) = ↑(m + n) - ↑n
    α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

m, n: ℕ

h: n ≤ m

inr↑(m - n) = ↑m - ↑nrw [α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

n, m: ℕ

h: n ≤ m + n

inr.intro↑(m + n - n) = ↑(m + n) - ↑nadd_tsub_cancel_right: ∀ {α : Type ?u.22157} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a + b - b = a
add_tsub_cancel_right,α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

n, m: ℕ

h: n ≤ m + n

inr.intro↑m = ↑(m + n) - ↑n α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

n, m: ℕ

h: n ≤ m + n

inr.intro↑(m + n - n) = ↑(m + n) - ↑ncast_add: ∀ {R : Type ?u.22479} [inst : AddMonoidWithOne R] (m n : ℕ), ↑(m + n) = ↑m + ↑n
cast_add,α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

n, m: ℕ

h: n ≤ m + n

inr.intro↑m = ↑m + ↑n - ↑n α: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

n, m: ℕ

h: n ≤ m + n

inr.intro↑(m + n - n) = ↑(m + n) - ↑nadd_tsub_cancel_right: ∀ {α : Type ?u.22524} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (a b : α), a + b - b = a
add_tsub_cancel_rightα: Type u_1

β: Type ?u.20730

inst✝³: CanonicallyOrderedCommSemiring α

inst✝²: Sub α

inst✝¹: OrderedSub α

inst✝: ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

n, m: ℕ

h: n ≤ m + n

inr.intro↑m = ↑m]
Goals accomplished! 🐙
#align nat.cast_tsub Nat.cast_tsub: ∀ {α : Type u_1} [inst : CanonicallyOrderedCommSemiring α] [inst_1 : Sub α] [inst_2 : OrderedSub α]
  [inst_3 : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] (m n : ℕ), ↑(m - n) = ↑m - ↑n
Nat.cast_tsub

@[simp, norm_cast]
theorem cast_min: ∀ [inst : LinearOrderedSemiring α] {a b : ℕ}, ↑(min a b) = min ↑a ↑b
cast_min [LinearOrderedSemiring: Type ?u.23104 → Type ?u.23104
LinearOrderedSemiring α: Type ?u.23098
α] {a: ℕ
a b: ℕ
b : ℕ: Type
ℕ} : ((min: {α : Type ?u.23114} → [self : Min α] → α → α → α
min a: ℕ
a b: ℕ
b : ℕ: Type
ℕ) : α: Type ?u.23098
α) = min: {α : Type ?u.23206} → [self : Min α] → α → α → α
min (a: ℕ
a : α: Type ?u.23098
α) b: ℕ
b :=
  (@mono_cast: ∀ {α : Type ?u.23344} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast α: Type ?u.23098
α _).map_min: ∀ {α : Type ?u.23402} {β : Type ?u.23401} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
  Monotone f → f (min a b) = min (f a) (f b)
map_min
#align nat.cast_min Nat.cast_min: ∀ {α : Type u_1} [inst : LinearOrderedSemiring α] {a b : ℕ}, ↑(min a b) = min ↑a ↑b
Nat.cast_min

@[simp, norm_cast]
theorem cast_max: ∀ {α : Type u_1} [inst : LinearOrderedSemiring α] {a b : ℕ}, ↑(max a b) = max ↑a ↑b
cast_max [LinearOrderedSemiring: Type ?u.23628 → Type ?u.23628
LinearOrderedSemiring α: Type ?u.23622
α] {a: ℕ
a b: ℕ
b : ℕ: Type
ℕ} : ((max: {α : Type ?u.23638} → [self : Max α] → α → α → α
max a: ℕ
a b: ℕ
b : ℕ: Type
ℕ) : α: Type ?u.23622
α) = max: {α : Type ?u.23730} → [self : Max α] → α → α → α
max (a: ℕ
a : α: Type ?u.23622
α) b: ℕ
b :=
  (@mono_cast: ∀ {α : Type ?u.23868} [inst : OrderedSemiring α], Monotone Nat.cast
mono_cast α: Type ?u.23622
α _).map_max: ∀ {α : Type ?u.23926} {β : Type ?u.23925} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
  Monotone f → f (max a b) = max (f a) (f b)
map_max
#align nat.cast_max Nat.cast_max: ∀ {α : Type u_1} [inst : LinearOrderedSemiring α] {a b : ℕ}, ↑(max a b) = max ↑a ↑b
Nat.cast_max

@[simp, norm_cast]
theorem abs_cast: ∀ [inst : LinearOrderedRing α] (a : ℕ), abs ↑a = ↑a
abs_cast [LinearOrderedRing: Type ?u.24152 → Type ?u.24152
LinearOrderedRing α: Type ?u.24146
α] (a: ℕ
a : ℕ: Type
ℕ) : |(a: ℕ
a : α: Type ?u.24146
α)| = a: ℕ
a :=
  abs_of_nonneg: ∀ {α : Type ?u.24423} [inst : AddGroup α] [inst_1 : LinearOrder α]
  [inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a : α}, 0 ≤ a → abs a = a
abs_of_nonneg (cast_nonneg: ∀ {α : Type ?u.24616} [inst : OrderedSemiring α] (n : ℕ), 0 ≤ ↑n
cast_nonneg a: ℕ
a)
#align nat.abs_cast Nat.abs_cast: ∀ {α : Type u_1} [inst : LinearOrderedRing α] (a : ℕ), abs ↑a = ↑a
Nat.abs_cast

theorem coe_nat_dvd: ∀ [inst : Semiring α] {m n : ℕ}, m ∣ n → ↑m ∣ ↑n
coe_nat_dvd [Semiring: Type ?u.24846 → Type ?u.24846
Semiring α: Type ?u.24840
α] {m: ℕ
m n: ℕ
n : ℕ: Type
ℕ} (h: m ∣ n
h : m: ℕ
m ∣ n: ℕ
n) : (m: ℕ
m : α: Type ?u.24840
α) ∣ (n: ℕ
n : α: Type ?u.24840
α) :=
  map_dvd: ∀ {M : Type ?u.25078} {N : Type ?u.25079} [inst : Monoid M] [inst_1 : Monoid N] {F : Type ?u.25077}
  [inst_2 : MulHomClass F M N] (f : F) {a b : M}, a ∣ b → ↑f a ∣ ↑f b
map_dvd (Nat.castRingHom: (α : Type ?u.25086) → [inst : NonAssocSemiring α] → ℕ →+* α
Nat.castRingHom α: Type ?u.24840
α) h: m ∣ n
h
#align nat.coe_nat_dvd Nat.coe_nat_dvd: ∀ {α : Type u_1} [inst : Semiring α] {m n : ℕ}, m ∣ n → ↑m ∣ ↑n
Nat.coe_nat_dvd

alias coe_nat_dvd: ∀ {α : Type u_1} [inst : Semiring α] {m n : ℕ}, m ∣ n → ↑m ∣ ↑n
coe_nat_dvd ← _root_.Dvd.dvd.natCast: ∀ {α : Type u_1} [inst : Semiring α] {m n : ℕ}, m ∣ n → ↑m ∣ ↑n
_root_.Dvd.dvd.natCast

end Nat

instance: ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst : CharZero α], Nontrivial α
instance [AddMonoidWithOne: Type ?u.25690 → Type ?u.25690
AddMonoidWithOne α: Type ?u.25684
α] [CharZero: (R : Type ?u.25693) → [inst : AddMonoidWithOne R] → Prop
CharZero α: Type ?u.25684
α] : Nontrivial: Type ?u.25702 → Prop
Nontrivial α: Type ?u.25684
α where exists_pair_ne :=
  ⟨1: ?m.25722
1, 0: ?m.25927
0, (Nat.cast_one: ∀ {R : Type ?u.26344} [inst : AddMonoidWithOne R], ↑1 = 1
Nat.cast_one (R := α: Type ?u.25684
α) ▸ Nat.cast_ne_zero: ∀ {R : Type ?u.26349} [inst : AddMonoidWithOne R] [inst_1 : CharZero R] {n : ℕ}, ↑n ≠ 0 ↔ n ≠ 0
Nat.cast_ne_zero.2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 (by
Goals accomplished! 🐙 α: Type ?u.25684

β: Type ?u.25687

inst✝¹: AddMonoidWithOne α

inst✝: CharZero α

1 ≠ 0decide
Goals accomplished! 🐙))⟩

section AddMonoidHomClass

variable {A: Type ?u.33337
A B: Type ?u.26449
B F: Type ?u.35455
F : Type _: Type (?u.35452+1)
Type _} [AddMonoidWithOne: Type ?u.35458 → Type ?u.35458
AddMonoidWithOne B: Type ?u.26449
B]

theorem ext_nat': ∀ {A : Type u_1} {F : Type u_2} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F ℕ A] (f g : F), ↑f 1 = ↑g 1 → f = g
ext_nat' [AddMonoid: Type ?u.26476 → Type ?u.26476
AddMonoid A: Type ?u.26464
A] [AddMonoidHomClass: Type ?u.26481 →
  (M : outParam (Type ?u.26480)) →
    (N : outParam (Type ?u.26479)) →
      [inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.26481?u.26480)?u.26479)
AddMonoidHomClass F: Type ?u.26470
F ℕ: Type
ℕ A: Type ?u.26464
A] (f: F
f g: F
g : F: Type ?u.26470
F) (h: ↑f 1 = ↑g 1
h : f: F
f 1: ?m.27487
1 = g: F
g 1: ?m.28454
1) : f: F
f = g: F
g :=
  FunLike.ext: ∀ {F : Sort ?u.28469} {α : Sort ?u.28470} {β : α → Sort ?u.28468} [i : FunLike F α β] (f g : F),
  (∀ (x : α), ↑f x = ↑g x) → f = g
FunLike.ext f: F
f g: F
g <| by
Goals accomplished! 🐙
    α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

∀ (x : ℕ), ↑f x = ↑g xintro n: ℕ
nα: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

n: ℕ

↑f n = ↑g n
    α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

∀ (x : ℕ), ↑f x = ↑g xinduction n: ℕ
n with
    α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

n: ℕ

↑f n = ↑g n| zero: ℕ
zero => α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

zero↑f Nat.zero = ↑g Nat.zerosimp_rw [α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

zero↑f Nat.zero = ↑g Nat.zeroNat.zero_eq: Nat.zero = 0
Nat.zero_eq,α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

zero↑f 0 = ↑g 0 α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

zero↑f Nat.zero = ↑g Nat.zeromap_zero: ∀ {M : Type ?u.29561} {N : Type ?u.29562} {F : Type ?u.29560} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero f: F
f,α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

zero0 = ↑g 0 α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

zero↑f Nat.zero = ↑g Nat.zeromap_zero: ∀ {M : Type ?u.30305} {N : Type ?u.30306} {F : Type ?u.30304} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero g: F
g
Goals accomplished! 🐙]
Goals accomplished! 🐙
    α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

n: ℕ

↑f n = ↑g n| succ: ℕ → ℕ
succ n: ℕ
n ihn: ?m.29434 n
ihn =>
      α: Type ?u.26458

β: Type ?u.26461

A: Type u_1

B: Type ?u.26467

F: Type u_2

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoid A

inst✝: AddMonoidHomClass F ℕ A

f, g: F

h: ↑f 1 = ↑g 1

n: ℕ

ihn: ↑f n = ↑g n

succ↑f (Nat.succ n) = ↑g (Nat.succ n)simp [Nat.succ_eq_add_one: ∀ (n : ℕ), Nat.succ n = n + 1
Nat.succ_eq_add_one, h: ↑f 1 = ↑g 1
h, ihn: ?m.29434 n
ihn]
Goals accomplished! 🐙
#align ext_nat' ext_nat': ∀ {A : Type u_1} {F : Type u_2} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F ℕ A] (f g : F), ↑f 1 = ↑g 1 → f = g
ext_nat'

@[ext]
theorem AddMonoidHom.ext_nat: ∀ [inst : AddMonoid A] {f g : ℕ →+ A}, ↑f 1 = ↑g 1 → f = g
AddMonoidHom.ext_nat [AddMonoid: Type ?u.33349 → Type ?u.33349
AddMonoid A: Type ?u.33337
A] {f: ℕ →+ A
f g: ℕ →+ A
g : ℕ: Type
ℕ →+ A: Type ?u.33337
A} : f: ℕ →+ A
f 1: ?m.34371
1 = g: ℕ →+ A
g 1: ?m.35344
1 → f: ℕ →+ A
f = g: ℕ →+ A
g :=
  ext_nat': ∀ {A : Type ?u.35355} {F : Type ?u.35356} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F ℕ A] (f g : F),
  ↑f 1 = ↑g 1 → f = g
ext_nat' f: ℕ →+ A
f g: ℕ →+ A
g
#align add_monoid_hom.ext_nat AddMonoidHom.ext_nat: ∀ {A : Type u_1} [inst : AddMonoid A] {f g : ℕ →+ A}, ↑f 1 = ↑g 1 → f = g
AddMonoidHom.ext_nat

variable [AddMonoidWithOne: Type ?u.40894 → Type ?u.40894
AddMonoidWithOne A: Type ?u.35470
A]

-- these versions are primed so that the `RingHomClass` versions aren't
theorem eq_natCast': ∀ [inst : AddMonoidHomClass F ℕ A] (f : F), ↑f 1 = 1 → ∀ (n : ℕ), ↑f n = ↑n
eq_natCast' [AddMonoidHomClass: Type ?u.35487 →
  (M : outParam (Type ?u.35486)) →
    (N : outParam (Type ?u.35485)) →
      [inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.35487?u.35486)?u.35485)
AddMonoidHomClass F: Type ?u.35476
F ℕ: Type
ℕ A: Type ?u.35470
A] (f: F
f : F: Type ?u.35476
F) (h1: ↑f 1 = 1
h1 : f: F
f 1: ?m.36497
1 = 1: ?m.36508
1) : ∀ n: ℕ
n : ℕ: Type
ℕ, f: F
f n: ℕ
n = n: ℕ
n
  | 0: ℕ
0 => by
Goals accomplished! 🐙 α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

↑f 0 = ↑0simp [map_zero: ∀ {M : Type ?u.38371} {N : Type ?u.38372} {F : Type ?u.38370} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero f: F
f]
Goals accomplished! 🐙
  | n: ℕ
n + 1 => by
Goals accomplished! 🐙 α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑f (n + 1) = ↑(n + 1)rw [α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑f (n + 1) = ↑(n + 1)map_add: ∀ {M : Type ?u.40180} {N : Type ?u.40181} {F : Type ?u.40179} [inst : Add M] [inst_1 : Add N]
  [inst_2 : AddHomClass F M N] (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y
map_add,α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑f n + ↑f 1 = ↑(n + 1) α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑f (n + 1) = ↑(n + 1)h1: ↑f 1 = 1
h1,α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑f n + 1 = ↑(n + 1) α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑f (n + 1) = ↑(n + 1)eq_natCast': ∀ [inst : AddMonoidHomClass F ℕ A] (f : F), ↑f 1 = 1 → ∀ (n : ℕ), ↑f n = ↑n
eq_natCast' f: F
f h1: ↑f 1 = 1
h1 n: ℕ
n,α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑n + 1 = ↑(n + 1) α: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑f (n + 1) = ↑(n + 1)Nat.cast_add_one: ∀ {R : Type ?u.40735} [inst : AddMonoidWithOne R] (n : ℕ), ↑(n + 1) = ↑n + 1
Nat.cast_add_oneα: Type ?u.35464

β: Type ?u.35467

A: Type u_2

B: Type ?u.35473

F: Type u_1

inst✝²: AddMonoidWithOne B

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F ℕ A

f: F

h1: ↑f 1 = 1

n: ℕ

↑n + 1 = ↑n + 1]
Goals accomplished! 🐙
#align eq_nat_cast' eq_natCast': ∀ {A : Type u_2} {F : Type u_1} [inst : AddMonoidWithOne A] [inst_1 : AddMonoidHomClass F ℕ A] (f : F),
  ↑f 1 = 1 → ∀ (n : ℕ), ↑f n = ↑n
eq_natCast'

theorem map_natCast': ∀ {B : Type u_3} {F : Type u_2} [inst : AddMonoidWithOne B] {A : Type u_1} [inst_1 : AddMonoidWithOne A]
  [inst_2 : AddMonoidHomClass F A B] (f : F), ↑f 1 = 1 → ∀ (n : ℕ), ↑f ↑n = ↑n
map_natCast' {A: Type u_1
A} [AddMonoidWithOne: Type ?u.40900 → Type ?u.40900
AddMonoidWithOne A: ?m.40897
A] [AddMonoidHomClass: Type ?u.40905 →
  (M : outParam (Type ?u.40904)) →
    (N : outParam (Type ?u.40903)) →
      [inst : AddZeroClass M] → [inst : AddZeroClass N] → Type (max(max?u.40905?u.40904)?u.40903)
AddMonoidHomClass F: Type ?u.40888
F A: ?m.40897
A B: Type ?u.40885
B] (f: F
f : F: Type ?u.40888
F) (h: ↑f 1 = 1
h : f: F
f 1: ?m.41921
1 = 1: ?m.42117
1) :
    ∀ n: ℕ
n : ℕ: Type
ℕ, f: F
f n: ℕ
n = n: ℕ
n
  | 0: ℕ
0 => by
Goals accomplished! 🐙 α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

↑f ↑0 = ↑0simp [map_zero: ∀ {M : Type ?u.44154} {N : Type ?u.44155} {F : Type ?u.44153} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero f: F
f]
Goals accomplished! 🐙
  | n: ℕ
n + 1 => by
Goals accomplished! 🐙
    α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑(n + 1) = ↑(n + 1)rw [α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑(n + 1) = ↑(n + 1)Nat.cast_add: ∀ {R : Type ?u.47021} [inst : AddMonoidWithOne R] (m n : ℕ), ↑(m + n) = ↑m + ↑n
Nat.cast_add,α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f (↑n + ↑1) = ↑(n + 1) α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑(n + 1) = ↑(n + 1)map_add: ∀ {M : Type ?u.47057} {N : Type ?u.47058} {F : Type ?u.47056} [inst : Add M] [inst_1 : Add N]
  [inst_2 : AddHomClass F M N] (f : F) (x y : M), ↑f (x + y) = ↑f x + ↑f y
map_add,α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑n + ↑f ↑1 = ↑(n + 1) α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑(n + 1) = ↑(n + 1)Nat.cast_add: ∀ {R : Type ?u.47728} [inst : AddMonoidWithOne R] (m n : ℕ), ↑(m + n) = ↑m + ↑n
Nat.cast_add,α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑n + ↑f ↑1 = ↑n + ↑1 α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑(n + 1) = ↑(n + 1)map_natCast': ∀ {A : Type u_1} [inst : AddMonoidWithOne A] [inst_1 : AddMonoidHomClass F A B] (f : F),
  ↑f 1 = 1 → ∀ (n : ℕ), ↑f ↑n = ↑n
map_natCast' f: F
f h: ↑f 1 = 1
h n: ℕ
n,α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑n + ↑f ↑1 = ↑n + ↑1 α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑(n + 1) = ↑(n + 1)Nat.cast_one: ∀ {R : Type ?u.47895} [inst : AddMonoidWithOne R], ↑1 = 1
Nat.cast_one,α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑n + ↑f 1 = ↑n + ↑1 α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑(n + 1) = ↑(n + 1)h: ↑f 1 = 1
h,α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑n + 1 = ↑n + ↑1 α: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑f ↑(n + 1) = ↑(n + 1)Nat.cast_one: ∀ {R : Type ?u.47933} [inst : AddMonoidWithOne R], ↑1 = 1
Nat.cast_oneα: Type ?u.40876

β: Type ?u.40879

A✝: Type ?u.40882

B: Type u_3

F: Type u_2

inst✝³: AddMonoidWithOne B

inst✝²: AddMonoidWithOne A✝

A: Type u_1

inst✝¹: AddMonoidWithOne A

inst✝: AddMonoidHomClass F A B

f: F

h: ↑f 1 = 1

n: ℕ

↑n + 1 = ↑n + 1]
Goals accomplished! 🐙
#align map_nat_cast' map_natCast': ∀ {B : Type u_3} {F : Type u_2} [inst : AddMonoidWithOne B] {A : Type u_1} [inst_1 : AddMonoidWithOne A]
  [inst_2 : AddMonoidHomClass F A B] (f : F), ↑f 1 = 1 → ∀ (n : ℕ), ↑f ↑n = ↑n
map_natCast'

end AddMonoidHomClass

section MonoidWithZeroHomClass

variable {A: Type ?u.48254
A F: Type ?u.48257
F : Type _: Type (?u.48242+1)
Type _} [MulZeroOneClass: Type ?u.48245 → Type ?u.48245
MulZeroOneClass A: Type ?u.48239
A]

/-- If two `MonoidWithZeroHom`s agree on the positive naturals they are equal. -/
theorem ext_nat'': ∀ [inst : MonoidWithZeroHomClass F ℕ A] (f g : F), (∀ {n : ℕ}, 0 < n → ↑f n = ↑g n) → f = g
ext_nat'' [MonoidWithZeroHomClass: Type ?u.48265 →
  (M : outParam (Type ?u.48264)) →
    (N : outParam (Type ?u.48263)) →
      [inst : MulZeroOneClass M] → [inst : MulZeroOneClass N] → Type (max(max?u.48265?u.48264)?u.48263)
MonoidWithZeroHomClass F: Type ?u.48257
F ℕ: Type
ℕ A: Type ?u.48254
A] (f: F
f g: F
g : F: Type ?u.48257
F) (h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
h_pos : ∀ {n: ℕ
n : ℕ: Type
ℕ}, 0: ?m.48305
0 < n: ℕ
n → f: F
f n: ℕ
n = g: F
g n: ℕ
n) :
    f: F
f = g: F
g := by
Goals accomplished! 🐙
  α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

f = gapply FunLike.ext: ∀ {F : Sort ?u.49797} {α : Sort ?u.49798} {β : α → Sort ?u.49796} [i : FunLike F α β] (f g : F),
  (∀ (x : α), ↑f x = ↑g x) → f = g
FunLike.extα: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

h∀ (x : ℕ), ↑f x = ↑g x
  α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

f = grintro (_ | n): ?α
(_ | n: ?α
_ | n: ℕ
n(_ | n): ?α
)α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

h.zero↑f Nat.zero = ↑g Nat.zero
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

n: ℕ

h.succ↑f (Nat.succ n) = ↑g (Nat.succ n)
  α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

f = g·α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

h.zero↑f Nat.zero = ↑g Nat.zero α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

h.zero↑f Nat.zero = ↑g Nat.zero
α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

n: ℕ

h.succ↑f (Nat.succ n) = ↑g (Nat.succ n)simp [map_zero: ∀ {M : Type ?u.50537} {N : Type ?u.50538} {F : Type ?u.50536} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero f: F
f, map_zero: ∀ {M : Type ?u.50930} {N : Type ?u.50931} {F : Type ?u.50929} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero g: F
g]
Goals accomplished! 🐙
  α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

f = g·α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

n: ℕ

h.succ↑f (Nat.succ n) = ↑g (Nat.succ n) α: Type ?u.48248

β: Type ?u.48251

A: Type u_2

F: Type u_1

inst✝¹: MulZeroOneClass A

inst✝: MonoidWithZeroHomClass F ℕ A

f, g: F

h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n

n: ℕ

h.succ↑f (Nat.succ n) = ↑g (Nat.succ n)exact h_pos: ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
h_pos n: ℕ
n.succ_pos: ∀ (n : ℕ), 0 < Nat.succ n
succ_pos
Goals accomplished! 🐙
#align ext_nat'' ext_nat'': ∀ {A : Type u_2} {F : Type u_1} [inst : MulZeroOneClass A] [inst_1 : MonoidWithZeroHomClass F ℕ A] (f g : F),
  (∀ {n : ℕ}, 0 < n → ↑f n = ↑g n) → f = g
ext_nat''

@[ext]
theorem MonoidWithZeroHom.ext_nat: ∀ {f g : ℕ →*₀ A}, (∀ {n : ℕ}, 0 < n → ↑f n = ↑g n) → f = g
MonoidWithZeroHom.ext_nat {f: ℕ →*₀ A
f g: ℕ →*₀ A
g : ℕ: Type
ℕ →*₀ A: Type ?u.51912
A} : (∀ {n: ℕ
n : ℕ: Type
ℕ}, 0: ?m.51965
0 < n: ℕ
n → f: ℕ →*₀ A
f n: ℕ
n = g: ℕ →*₀ A
g n: ℕ
n) → f: ℕ →*₀ A
f = g: ℕ →*₀ A
g :=
  ext_nat'': ∀ {A : Type ?u.53467} {F : Type ?u.53466} [inst : MulZeroOneClass A] [inst_1 : MonoidWithZeroHomClass F ℕ A] (f g : F),
  (∀ {n : ℕ}, 0 < n → ↑f n = ↑g n) → f = g
ext_nat'' f: ℕ →*₀ A
f g: ℕ →*₀ A
g
#align monoid_with_zero_hom.ext_nat MonoidWithZeroHom.ext_nat: ∀ {A : Type u_1} [inst : MulZeroOneClass A] {f g : ℕ →*₀ A}, (∀ {n : ℕ}, 0 < n → ↑f n = ↑g n) → f = g
MonoidWithZeroHom.ext_nat

end MonoidWithZeroHomClass

section RingHomClass

variable {R: Type ?u.53572
R S: Type ?u.53575
S F: Type ?u.57182
F : Type _: Type (?u.57179+1)
Type _} [NonAssocSemiring: Type ?u.59361 → Type ?u.59361
NonAssocSemiring R: Type ?u.53572
R] [NonAssocSemiring: Type ?u.55176 → Type ?u.55176
NonAssocSemiring S: Type ?u.53554
S]

@[simp]
theorem eq_natCast: ∀ {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : RingHomClass F ℕ R] (f : F) (n : ℕ), ↑f n = ↑n
eq_natCast [RingHomClass: Type ?u.53589 →
  (α : outParam (Type ?u.53588)) →
    (β : outParam (Type ?u.53587)) →
      [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.53589?u.53588)?u.53587)
RingHomClass F: Type ?u.53578
F ℕ: Type
ℕ R: Type ?u.53572
R] (f: F
f : F: Type ?u.53578
F) : ∀ n: ?m.53616
n, f: F
f n: ?m.53616
n = n: ?m.53616
n :=
  eq_natCast': ∀ {A : Type ?u.54584} {F : Type ?u.54583} [inst : AddMonoidWithOne A] [inst_1 : AddMonoidHomClass F ℕ A] (f : F),
  ↑f 1 = 1 → ∀ (n : ℕ), ↑f n = ↑n
eq_natCast' f: F
f <| map_one: ∀ {M : Type ?u.54761} {N : Type ?u.54762} {F : Type ?u.54760} [inst : One M] [inst_1 : One N]
  [inst_2 : OneHomClass F M N] (f : F), ↑f 1 = 1
map_one f: F
f
#align eq_nat_cast eq_natCast: ∀ {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : RingHomClass F ℕ R] (f : F) (n : ℕ), ↑f n = ↑n
eq_natCast

@[simp]
theorem map_natCast: ∀ {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast [RingHomClass: Type ?u.55181 →
  (α : outParam (Type ?u.55180)) →
    (β : outParam (Type ?u.55179)) →
      [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.55181?u.55180)?u.55179)
RingHomClass F: Type ?u.55170
F R: Type ?u.55164
R S: Type ?u.55167
S] (f: F
f : F: Type ?u.55170
F) : ∀ n: ℕ
n : ℕ: Type
ℕ, f: F
f (n: ℕ
n : R: Type ?u.55164
R) = n: ℕ
n :=
  map_natCast': ∀ {B : Type ?u.56359} {F : Type ?u.56358} [inst : AddMonoidWithOne B] {A : Type ?u.56357} [inst_1 : AddMonoidWithOne A]
  [inst_2 : AddMonoidHomClass F A B] (f : F), ↑f 1 = 1 → ∀ (n : ℕ), ↑f ↑n = ↑n
map_natCast' f: F
f <| map_one: ∀ {M : Type ?u.56634} {N : Type ?u.56635} {F : Type ?u.56633} [inst : One M] [inst_1 : One N]
  [inst_2 : OneHomClass F M N] (f : F), ↑f 1 = 1
map_one f: F
f
#align map_nat_cast map_natCast: ∀ {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast

--Porting note: new theorem
@[simp]
theorem map_ofNat: ∀ {R : Type u_2} {S : Type u_3} {F : Type u_1} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ) [inst_3 : Nat.AtLeastTwo n], ↑f (OfNat.ofNat n) = OfNat.ofNat n
map_ofNat [RingHomClass: Type ?u.57193 →
  (α : outParam (Type ?u.57192)) →
    (β : outParam (Type ?u.57191)) →
      [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.57193?u.57192)?u.57191)
RingHomClass F: Type ?u.57182
F R: Type ?u.57176
R S: Type ?u.57179
S] (f: F
f : F: Type ?u.57182
F)  (n: ℕ
n : ℕ: Type
ℕ) [Nat.AtLeastTwo: ℕ → Prop
Nat.AtLeastTwo n: ℕ
n] :
    (f: F
f (OfNat.ofNat: {α : Type ?u.57735} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat n: ℕ
n) : S: Type ?u.57179
S) = OfNat.ofNat: {α : Type ?u.57908} → (x : ℕ) → [self : OfNat α x] → α
OfNat.ofNat n: ℕ
n :=
  map_natCast: ∀ {R : Type ?u.58143} {S : Type ?u.58144} {F : Type ?u.58142} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast f: F
f n: ℕ
n

theorem ext_nat: ∀ [inst : RingHomClass F ℕ R] (f g : F), f = g
ext_nat [RingHomClass: Type ?u.58259 →
  (α : outParam (Type ?u.58258)) →
    (β : outParam (Type ?u.58257)) →
      [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.58259?u.58258)?u.58257)
RingHomClass F: Type ?u.58248
F ℕ: Type
ℕ R: Type ?u.58242
R] (f: F
f g: F
g : F: Type ?u.58248
F) : f: F
f = g: F
g :=
  ext_nat': ∀ {A : Type ?u.58293} {F : Type ?u.58294} [inst : AddMonoid A] [inst_1 : AddMonoidHomClass F ℕ A] (f g : F),
  ↑f 1 = ↑g 1 → f = g
ext_nat' f: F
f g: F
g <| by
Goals accomplished! 🐙 α: Type ?u.58236

β: Type ?u.58239

R: Type u_2

S: Type ?u.58245

F: Type u_1

inst✝²: NonAssocSemiring R

inst✝¹: NonAssocSemiring S

inst✝: RingHomClass F ℕ R

f, g: F

↑f 1 = ↑g 1simp only [map_one: ∀ {M : Type ?u.58495} {N : Type ?u.58496} {F : Type ?u.58494} [inst : One M] [inst_1 : One N]
  [inst_2 : OneHomClass F M N] (f : F), ↑f 1 = 1
map_one f: F
f, map_one: ∀ {M : Type ?u.58872} {N : Type ?u.58873} {F : Type ?u.58871} [inst : One M] [inst_1 : One N]
  [inst_2 : OneHomClass F M N] (f : F), ↑f 1 = 1
map_one g: F
g]
Goals accomplished! 🐙
#align ext_nat ext_nat: ∀ {R : Type u_2} {F : Type u_1} [inst : NonAssocSemiring R] [inst : RingHomClass F ℕ R] (f g : F), f = g
ext_nat

theorem NeZero.nat_of_injective: ∀ {n : ℕ} [h : NeZero ↑n] [inst : RingHomClass F R S] {f : F}, Function.Injective ↑f → NeZero ↑n
NeZero.nat_of_injective {n: ℕ
n : ℕ: Type
ℕ} [h: NeZero ↑n
h : NeZero: {R : Type ?u.59369} → [inst : Zero R] → R → Prop
NeZero (n: ℕ
n : R: Type ?u.59352
R)] [RingHomClass: Type ?u.59786 →
  (α : outParam (Type ?u.59785)) →
    (β : outParam (Type ?u.59784)) →
      [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.59786?u.59785)?u.59784)
RingHomClass F: Type ?u.59358
F R: Type ?u.59352
R S: Type ?u.59355
S] {f: F
f : F: Type ?u.59358
F}
    (hf: Function.Injective ↑f
hf : Function.Injective: {α : Sort ?u.59802} → {β : Sort ?u.59801} → (α → β) → Prop
Function.Injective f: F
f) : NeZero: {R : Type ?u.60327} → [inst : Zero R] → R → Prop
NeZero (n: ℕ
n : S: Type ?u.59355
S) :=
  ⟨fun h: ?m.60790
h ↦ NeZero.natCast_ne: ∀ (n : ℕ) (R : Type ?u.60792) [inst : AddMonoidWithOne R] [h : NeZero ↑n], ↑n ≠ 0
NeZero.natCast_ne n: ℕ
n R: Type ?u.59352
R <| hf: Function.Injective ↑f
hf <| by
Goals accomplished! 🐙 α: Type ?u.59346

β: Type ?u.59349

R: Type u_1

S: Type u_3

F: Type u_2

inst✝²: NonAssocSemiring R

inst✝¹: NonAssocSemiring S

n: ℕ

h✝: NeZero ↑n

inst✝: RingHomClass F R S

f: F

hf: Function.Injective ↑f

h: ↑n = 0

↑f ↑n = ↑f 0simpa only [map_natCast: ∀ {R : Type ?u.61136} {S : Type ?u.61137} {F : Type ?u.61135} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast, map_zero: ∀ {M : Type ?u.61168} {N : Type ?u.61169} {F : Type ?u.61167} [inst : Zero M] [inst_1 : Zero N]
  [inst_2 : ZeroHomClass F M N] (f : F), ↑f 0 = 0
map_zero f: F
f]
Goals accomplished! 🐙 ⟩
#align ne_zero.nat_of_injective NeZero.nat_of_injective: ∀ {R : Type u_1} {S : Type u_3} {F : Type u_2} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {n : ℕ}
  [h : NeZero ↑n] [inst_2 : RingHomClass F R S] {f : F}, Function.Injective ↑f → NeZero ↑n
NeZero.nat_of_injective

theorem NeZero.nat_of_neZero: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {F : Type u_3} [inst_2 : RingHomClass F R S],
  F → ∀ {n : ℕ} [hn : NeZero ↑n], NeZero ↑n
NeZero.nat_of_neZero {R: Type u_1
R S: ?m.61830
S} [Semiring: Type ?u.61833 → Type ?u.61833
Semiring R: ?m.61827
R] [Semiring: Type ?u.61836 → Type ?u.61836
Semiring S: ?m.61830
S] {F: ?m.61839
F} [RingHomClass: Type ?u.61844 →
  (α : outParam (Type ?u.61843)) →
    (β : outParam (Type ?u.61842)) →
      [inst : NonAssocSemiring α] → [inst : NonAssocSemiring β] → Type (max(max?u.61844?u.61843)?u.61842)
RingHomClass F: ?m.61839
F R: ?m.61827
R S: ?m.61830
S] (f: F
f : F: ?m.61839
F)
    {n: ℕ
n : ℕ: Type
ℕ} [hn: NeZero ↑n
hn : NeZero: {R : Type ?u.61881} → [inst : Zero R] → R → Prop
NeZero (n: ℕ
n : S: ?m.61830
S)] : NeZero: {R : Type ?u.62079} → [inst : Zero R] → R → Prop
NeZero (n: ℕ
n : R: ?m.61827
R) :=
  .of_map: ∀ {F : Type ?u.62287} {R : Type ?u.62285} {M : Type ?u.62286} [inst : Zero R] [inst_1 : Zero M]
  [inst_2 : ZeroHomClass F R M] (f : F) {r : R} [neZero : NeZero (↑f r)], NeZero r
.of_map (f := f: F
f) (neZero := by
Goals accomplished! 🐙 α: Type ?u.61806

β: Type ?u.61809

R✝: Type ?u.61812

S✝: Type ?u.61815

F✝: Type ?u.61818

inst✝⁴: NonAssocSemiring R✝

inst✝³: NonAssocSemiring S✝

R: Type u_1

S: Type u_2

inst✝²: Semiring R

inst✝¹: Semiring S

F: Type u_3

inst✝: RingHomClass F R S

f: F

n: ℕ

hn: NeZero ↑n

NeZero (↑f ↑n)simp only [map_natCast: ∀ {R : Type ?u.62715} {S : Type ?u.62716} {F : Type ?u.62714} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : RingHomClass F R S] (f : F) (n : ℕ), ↑f ↑n = ↑n
map_natCast, hn: NeZero ↑n
hn]
Goals accomplished! 🐙)
#align ne_zero.nat_of_ne_zero NeZero.nat_of_neZero: ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] {F : Type u_3} [inst_2 : RingHomClass F R S],
  F → ∀ {n : ℕ} [hn : NeZero ↑n], NeZero ↑n
NeZero.nat_of_neZero

end RingHomClass

namespace RingHom

/-- This is primed to match `eq_intCast'`. -/
theorem eq_natCast': ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : ℕ →+* R), f = Nat.castRingHom R
eq_natCast' {R: ?m.62990
R} [NonAssocSemiring: Type ?u.62993 → Type ?u.62993
NonAssocSemiring R: ?m.62990
R] (f: ℕ →+* R
f : ℕ: Type
ℕ →+* R: ?m.62990
R) : f: ℕ →+* R
f = Nat.castRingHom: (α : Type ?u.63021) → [inst : NonAssocSemiring α] → ℕ →+* α
Nat.castRingHom R: ?m.62990
R :=
  RingHom.ext: ∀ {α : Type ?u.63032} {β : Type ?u.63033} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄,
  (∀ (x_2 : α), ↑f x_2 = ↑g x_2) → f = g
RingHom.ext <| eq_natCast: ∀ {R : Type ?u.63049} {F : Type ?u.63048} [inst : NonAssocSemiring R] [inst_1 : RingHomClass F ℕ R] (f : F) (n : ℕ),
  ↑f n = ↑n
eq_natCast f: ℕ →+* R
f
#align ring_hom.eq_nat_cast' RingHom.eq_natCast': ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : ℕ →+* R), f = Nat.castRingHom R
RingHom.eq_natCast'

end RingHom

@[simp, norm_cast]
theorem Nat.cast_id: ∀ (n : ℕ), ↑n = n
Nat.cast_id (n: ℕ
n : ℕ: Type
ℕ) : n: ℕ
n.cast: {R : Type ?u.63109} → [inst : NatCast R] → ℕ → R
cast = n: ℕ
n :=
  rfl: ∀ {α : Sort ?u.63154} {a : α}, a = a
rfl
#align nat.cast_id Nat.cast_id: ∀ (n : ℕ), ↑n = n
Nat.cast_id

@[simp]
theorem Nat.castRingHom_nat: castRingHom ℕ = RingHom.id ℕ
Nat.castRingHom_nat : Nat.castRingHom: (α : Type ?u.63190) → [inst : NonAssocSemiring α] → ℕ →+* α
Nat.castRingHom ℕ: Type
ℕ = RingHom.id: (α : Type ?u.63206) → [inst : NonAssocSemiring α] → α →+* α
RingHom.id ℕ: Type
ℕ :=
  rfl: ∀ {α : Sort ?u.63214} {a : α}, a = a
rfl
#align nat.cast_ring_hom_nat Nat.castRingHom_nat: Nat.castRingHom ℕ = RingHom.id ℕ
Nat.castRingHom_nat

/-- We don't use `RingHomClass` here, since that might cause type-class slowdown for
`Subsingleton`-/
instance Nat.uniqueRingHom: {R : Type u_1} → [inst : NonAssocSemiring R] → Unique (ℕ →+* R)
Nat.uniqueRingHom {R: Type ?u.63256
R : Type _: Type (?u.63256+1)
Type _} [NonAssocSemiring: Type ?u.63259 → Type ?u.63259
NonAssocSemiring R: Type ?u.63256
R] : Unique: Sort ?u.63262 → Sort (max1?u.63262)
Unique (ℕ: Type
ℕ →+* R: Type ?u.63256
R) where
  default := Nat.castRingHom: (α : Type ?u.63295) → [inst : NonAssocSemiring α] → ℕ →+* α
Nat.castRingHom R: Type ?u.63256
R
  uniq := RingHom.eq_natCast': ∀ {R : Type ?u.63304} [inst : NonAssocSemiring R] (f : ℕ →+* R), f = castRingHom R
RingHom.eq_natCast'

namespace Pi

variable {π: α → Type ?u.64938
π : α: Type ?u.63375
α → Type _: Type (?u.63364+1)
Type _} [∀ a: ?m.63368
a, NatCast: Type ?u.63371 → Type ?u.63371
NatCast (π: α → Type ?u.63364
π a: ?m.63368
a)]

/- Porting note: manually wrote this instance.
Was `by refine_struct { .. } <;> pi_instance_derive_field` -/
instance natCast: NatCast ((a : α) → π a)
natCast : NatCast: Type ?u.63394 → Type ?u.63394
NatCast (∀ a: ?m.63396
a, π: α → Type ?u.63383
π a: ?m.63396
a) := { natCast := fun n: ?m.63407
n _: ?m.63410
_ ↦ n: ?m.63407
n }

theorem nat_apply: ∀ {α : Type u_2} {π : α → Type u_1} [inst : (a : α) → NatCast (π a)] (n : ℕ) (a : α), ↑n a = ↑n
nat_apply (n: ℕ
n : ℕ: Type
ℕ) (a: α
a : α: Type ?u.63536
α) : (n: ℕ
n : ∀ a: ?m.63562
a, π: α → Type ?u.63544
π a: ?m.63562
a) a: α
a = n: ℕ
n :=
  rfl: ∀ {α : Sort ?u.64910} {a : α}, a = a
rfl
#align pi.nat_apply Pi.nat_apply: ∀ {α : Type u_2} {π : α → Type u_1} [inst : (a : α) → NatCast (π a)] (n : ℕ) (a : α), ↑n a = ↑n
Pi.nat_apply

@[simp]
theorem coe_nat: ∀ {α : Type u_1} {π : α → Type u_2} [inst : (a : α) → NatCast (π a)] (n : ℕ), ↑n = fun x => ↑n
coe_nat (n: ℕ
n : ℕ: Type
ℕ) : (n: ℕ
n : ∀ a: ?m.64954
a, π: α → Type ?u.64938
π a: ?m.64954
a) = fun _: ?m.66225
_ ↦ ↑n: ℕ
n :=
  rfl: ∀ {α : Sort ?u.66316} {a : α}, a = a
rfl
#align pi.coe_nat Pi.coe_nat: ∀ {α : Type u_1} {π : α → Type u_2} [inst : (a : α) → NatCast (π a)] (n : ℕ), ↑n = fun x => ↑n
Pi.coe_nat

end Pi

theorem Sum.elim_natCast_natCast: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : NatCast γ] (n : ℕ), Sum.elim ↑n ↑n = ↑n
Sum.elim_natCast_natCast {α: Type ?u.66355
α β: Type ?u.66358
β γ: Type ?u.66361
γ : Type _: Type (?u.66355+1)
Type _} [NatCast: Type ?u.66364 → Type ?u.66364
NatCast γ: Type ?u.66361
γ] (n: ℕ
n : ℕ: Type
ℕ) :
    Sum.elim: {α : Type ?u.66372} → {β : Type ?u.66371} → {γ : Sort ?u.66370} → (α → γ) → (β → γ) → α ⊕ β → γ
Sum.elim (n: ℕ
n : α: Type ?u.66355
α → γ: Type ?u.66361
γ) (n: ℕ
n : β: Type ?u.66358
β → γ: Type ?u.66361
γ) = n: ℕ
n :=
  @Sum.elim_lam_const_lam_const: ∀ {α : Type ?u.70246} {β : Type ?u.70245} {γ : Type ?u.70247} (c : γ), (Sum.elim (fun x => c) fun x => c) = fun x => c
Sum.elim_lam_const_lam_const α: Type u_1
α β: Type u_2
β γ: Type u_3
γ n: ℕ
n
#align sum.elim_nat_cast_nat_cast Sum.elim_natCast_natCast: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : NatCast γ] (n : ℕ), Sum.elim ↑n ↑n = ↑n
Sum.elim_natCast_natCast

/-! ### Order dual -/


open OrderDual

instance: {α : Type u_1} → [h : NatCast α] → NatCast αᵒᵈ
instance [h: NatCast α
h : NatCast: Type ?u.70320 → Type ?u.70320
NatCast α: Type ?u.70314
α] : NatCast: Type ?u.70323 → Type ?u.70323
NatCast α: Type ?u.70314
αᵒᵈ :=
  h: NatCast α
h

instance: {α : Type u_1} → [h : AddMonoidWithOne α] → AddMonoidWithOne αᵒᵈ
instance [h: AddMonoidWithOne α
h : AddMonoidWithOne: Type ?u.70364 → Type ?u.70364
AddMonoidWithOne α: Type ?u.70358
α] : AddMonoidWithOne: Type ?u.70367 → Type ?u.70367
AddMonoidWithOne α: Type ?u.70358
αᵒᵈ :=
  h: AddMonoidWithOne α
h

instance: {α : Type u_1} → [h : AddCommMonoidWithOne α] → AddCommMonoidWithOne αᵒᵈ
instance [h: AddCommMonoidWithOne α
h : AddCommMonoidWithOne: Type ?u.70408 → Type ?u.70408
AddCommMonoidWithOne α: Type ?u.70402
α] : AddCommMonoidWithOne: Type ?u.70411 → Type ?u.70411
AddCommMonoidWithOne α: Type ?u.70402
αᵒᵈ :=
  h: AddCommMonoidWithOne α
h

@[simp]
theorem toDual_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ℕ), ↑toDual ↑n = ↑n
toDual_natCast [NatCast: Type ?u.70452 → Type ?u.70452
NatCast α: Type ?u.70446
α] (n: ℕ
n : ℕ: Type
ℕ) : toDual: {α : Type ?u.70458} → α ≃ αᵒᵈ
toDual (n: ℕ
n : α: Type ?u.70446
α) = n: ℕ
n :=
  rfl: ∀ {α : Sort ?u.70683} {a : α}, a = a
rfl
#align to_dual_nat_cast toDual_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ℕ), ↑toDual ↑n = ↑n
toDual_natCast

@[simp]
theorem ofDual_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ℕ), ↑(↑ofDual n) = ↑n
ofDual_natCast [NatCast: Type ?u.70725 → Type ?u.70725
NatCast α: Type ?u.70719
α] (n: ℕ
n : ℕ: Type
ℕ) : (ofDual: {α : Type ?u.70732} → αᵒᵈ ≃ α
ofDual n: ℕ
n : α: Type ?u.70719
α) = n: ℕ
n :=
  rfl: ∀ {α : Sort ?u.70933} {a : α}, a = a
rfl
#align of_dual_nat_cast ofDual_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ℕ), ↑(↑ofDual n) = ↑n
ofDual_natCast

/-! ### Lexicographic order -/


instance: {α : Type u_1} → [h : NatCast α] → NatCast (Lex α)
instance [h: NatCast α
h : NatCast: Type ?u.70975 → Type ?u.70975
NatCast α: Type ?u.70969
α] : NatCast: Type ?u.70978 → Type ?u.70978
NatCast (Lex: Type ?u.70979 → Type ?u.70979
Lex α: Type ?u.70969
α) :=
  h: NatCast α
h

instance: {α : Type u_1} → [h : AddMonoidWithOne α] → AddMonoidWithOne (Lex α)
instance [h: AddMonoidWithOne α
h : AddMonoidWithOne: Type ?u.71019 → Type ?u.71019
AddMonoidWithOne α: Type ?u.71013
α] : AddMonoidWithOne: Type ?u.71022 → Type ?u.71022
AddMonoidWithOne (Lex: Type ?u.71023 → Type ?u.71023
Lex α: Type ?u.71013
α) :=
  h: AddMonoidWithOne α
h

instance: {α : Type u_1} → [h : AddCommMonoidWithOne α] → AddCommMonoidWithOne (Lex α)
instance [h: AddCommMonoidWithOne α
h : AddCommMonoidWithOne: Type ?u.71063 → Type ?u.71063
AddCommMonoidWithOne α: Type ?u.71057
α] : AddCommMonoidWithOne: Type ?u.71066 → Type ?u.71066
AddCommMonoidWithOne (Lex: Type ?u.71067 → Type ?u.71067
Lex α: Type ?u.71057
α) :=
  h: AddCommMonoidWithOne α
h

@[simp]
theorem toLex_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ℕ), ↑toLex ↑n = ↑n
toLex_natCast [NatCast: Type ?u.71107 → Type ?u.71107
NatCast α: Type ?u.71101
α] (n: ℕ
n : ℕ: Type
ℕ) : toLex: {α : Type ?u.71113} → α ≃ Lex α
toLex (n: ℕ
n : α: Type ?u.71101
α) = n: ℕ
n :=
  rfl: ∀ {α : Sort ?u.71338} {a : α}, a = a
rfl
#align to_lex_nat_cast toLex_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ℕ), ↑toLex ↑n = ↑n
toLex_natCast

@[simp]
theorem ofLex_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ℕ), ↑(↑ofLex n) = ↑n
ofLex_natCast [NatCast: Type ?u.71380 → Type ?u.71380
NatCast α: Type ?u.71374
α] (n: ℕ
n : ℕ: Type
ℕ) : (ofLex: {α : Type ?u.71387} → Lex α ≃ α
ofLex n: ℕ
n : α: Type ?u.71374
α) = n: ℕ
n :=
  rfl: ∀ {α : Sort ?u.71588} {a : α}, a = a
rfl
#align of_lex_nat_cast ofLex_natCast: ∀ {α : Type u_1} [inst : NatCast α] (n : ℕ), ↑(↑ofLex n) = ↑n
ofLex_natCast