/-
Copyright (c) 2014 Floris van Doorn (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro

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

/-!
# Basic operations on the natural numbers

This file contains:
- instances on the natural numbers
- some basic lemmas about natural numbers
- extra recursors:
  * `le_rec_on`, `le_induction`: recursion and induction principles starting at non-zero numbers
  * `decreasing_induction`: recursion growing downwards
  * `le_rec_on'`, `decreasing_induction'`: versions with slightly weaker assumptions
  * `strong_rec'`: recursion based on strong inequalities
- decidability instances on predicates about the natural numbers

Many theorems that used to live in this file have been moved to `Data.Nat.Order`,
so that this file requires fewer imports.
For each section here there is a corresponding section in that file with additional results.
It may be possible to move some of these results here, by tweaking their proofs.


-/


universe u v

namespace Nat

/-! ### instances -/

instance 
nontrivial: Nontrivial ℕ
nontrivial : 
Nontrivial: Type ?u.2 → Prop
Nontrivial 
ℕ: Type
ℕ :=
  ⟨⟨
0: ?m.22
0, 
1: ?m.42
1, 
Nat.zero_ne_one: 0 ≠ 1
Nat.zero_ne_one⟩⟩

instance 
commSemiring: CommSemiring ℕ
commSemiring : 
CommSemiring: Type ?u.55 → Type ?u.55
CommSemiring 
ℕ: Type
ℕ where
  add := 
Nat.add: ℕ → ℕ → ℕ
Nat.add
  add_assoc := 
Nat.add_assoc: ∀ (n m k : ℕ), n + m + k = n + (m + k)
Nat.add_assoc
  zero := 
Nat.zero: ℕ
Nat.zero
  zero_add := 
Nat.zero_add: ∀ (n : ℕ), 0 + n = n
Nat.zero_add
  add_zero := 
Nat.add_zero: ∀ (n : ℕ), n + 0 = n
Nat.add_zero
  add_comm := 
Nat.add_comm: ∀ (n m : ℕ), n + m = m + n
Nat.add_comm
  mul := 
Nat.mul: ℕ → ℕ → ℕ
Nat.mul
  mul_assoc := 
Nat.mul_assoc: ∀ (n m k : ℕ), n * m * k = n * (m * k)
Nat.mul_assoc
  one := 
Nat.succ: ℕ → ℕ
Nat.succ 
Nat.zero: ℕ
Nat.zero
  one_mul := 
Nat.one_mul: ∀ (n : ℕ), 1 * n = n
Nat.one_mul
  mul_one := 
Nat.mul_one: ∀ (n : ℕ), n * 1 = n
Nat.mul_one
  left_distrib := 
Nat.left_distrib: ∀ (n m k : ℕ), n * (m + k) = n * m + n * k
Nat.left_distrib
  right_distrib := 
Nat.right_distrib: ∀ (n m k : ℕ), (n + m) * k = n * k + m * k
Nat.right_distrib
  zero_mul := 
Nat.zero_mul: ∀ (n : ℕ), 0 * n = 0
Nat.zero_mul
  mul_zero := 
Nat.mul_zero: ∀ (n : ℕ), n * 0 = 0
Nat.mul_zero
  mul_comm := 
Nat.mul_comm: ∀ (n m : ℕ), n * m = m * n
Nat.mul_comm
  natCast 
n: ?m.275
n := 
n: ?m.275
n
  natCast_zero := 
rfl: ∀ {α : Sort ?u.279} {a : α}, a = a
rfl
  natCast_succ 
n: ?m.283
n := 
rfl: ∀ {α : Sort ?u.285} {a : α}, a = a
rfl
  nsmul 
m: ?m.111
m 
n: ?m.114
n := 
m: ?m.111
m * 
n: ?m.114
n
  nsmul_zero := 
Nat.zero_mul: ∀ (n : ℕ), 0 * n = 0
Nat.zero_mul
  nsmul_succ 
_: ?m.172
_ 
_: ?m.175
_ := by
Goals accomplished! 🐙 
x✝¹, x✝: ℕ

(fun m n => m * n) (x✝¹ + 1) x✝ = x✝ + (fun m n => m * n) x✝¹ x✝dsimp only
x✝¹, x✝: ℕ

(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝;
x✝¹, x✝: ℕ

(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝ 
x✝¹, x✝: ℕ

(fun m n => m * n) (x✝¹ + 1) x✝ = x✝ + (fun m n => m * n) x✝¹ x✝rw [
x✝¹, x✝: ℕ

(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
Nat.add_comm: ∀ (n m : ℕ), n + m = m + n
Nat.add_comm,
x✝¹, x✝: ℕ

(1 + x✝¹) * x✝ = x✝ + x✝¹ * x✝ 
x✝¹, x✝: ℕ

(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
Nat.right_distrib: ∀ (n m k : ℕ), (n + m) * k = n * k + m * k
Nat.right_distrib,
x✝¹, x✝: ℕ

1 * x✝ + x✝¹ * x✝ = x✝ + x✝¹ * x✝ 
x✝¹, x✝: ℕ

(x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
Nat.one_mul: ∀ (n : ℕ), 1 * n = n
Nat.one_mul
x✝¹, x✝: ℕ

x✝ + x✝¹ * x✝ = x✝ + x✝¹ * x✝]
Goals accomplished! 🐙
  npow 
m: ?m.293
m 
n: ?m.296
n := 
n: ?m.296
n ^ 
m: ?m.293
m
  npow_zero := 
Nat.pow_zero: ∀ (n : ℕ), n ^ 0 = 1
Nat.pow_zero
  npow_succ 
_: ?m.350
_ 
_: ?m.353
_ := 
Nat.pow_succ': ∀ {m n : ℕ}, m ^ succ n = m * m ^ n
Nat.pow_succ'

/-! Extra instances to short-circuit type class resolution and ensure computability -/


instance 
addCommMonoid: AddCommMonoid ℕ
addCommMonoid : 
AddCommMonoid: Type ?u.892 → Type ?u.892
AddCommMonoid 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.894} → [i : α] → α
inferInstance

instance 
addMonoid: AddMonoid ℕ
addMonoid : 
AddMonoid: Type ?u.1154 → Type ?u.1154
AddMonoid 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.1156} → [i : α] → α
inferInstance

instance 
monoid: Monoid ℕ
monoid : 
Monoid: Type ?u.1406 → Type ?u.1406
Monoid 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.1408} → [i : α] → α
inferInstance

instance 
commMonoid: CommMonoid ℕ
commMonoid : 
CommMonoid: Type ?u.1586 → Type ?u.1586
CommMonoid 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.1588} → [i : α] → α
inferInstance

instance 
commSemigroup: CommSemigroup ℕ
commSemigroup : 
CommSemigroup: Type ?u.1721 → Type ?u.1721
CommSemigroup 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.1723} → [i : α] → α
inferInstance

instance 
semigroup: Semigroup ℕ
semigroup : 
Semigroup: Type ?u.1890 → Type ?u.1890
Semigroup 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.1892} → [i : α] → α
inferInstance

instance 
addCommSemigroup: AddCommSemigroup ℕ
addCommSemigroup : 
AddCommSemigroup: Type ?u.2056 → Type ?u.2056
AddCommSemigroup 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.2058} → [i : α] → α
inferInstance

instance 
addSemigroup: AddSemigroup ℕ
addSemigroup : 
AddSemigroup: Type ?u.2156 → Type ?u.2156
AddSemigroup 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.2158} → [i : α] → α
inferInstance

instance 
distrib: Distrib ℕ
distrib : 
Distrib: Type ?u.2244 → Type ?u.2244
Distrib 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.2246} → [i : α] → α
inferInstance

instance 
semiring: Semiring ℕ
semiring : 
Semiring: Type ?u.2414 → Type ?u.2414
Semiring 
ℕ: Type
ℕ :=
  
inferInstance: {α : Sort ?u.2416} → [i : α] → α
inferInstance

protected theorem 
nsmul_eq_mul: ∀ (m n : ℕ), m • n = m * n
nsmul_eq_mul (
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ) : 
m: ℕ
m • 
n: ℕ
n = 
m: ℕ
m * 
n: ℕ
n :=
  
rfl: ∀ {α : Sort ?u.2602} {a : α}, a = a
rfl
#align nat.nsmul_eq_mul 
Nat.nsmul_eq_mul: ∀ (m n : ℕ), m • n = m * n
Nat.nsmul_eq_mul

-- Moved to core
#align nat.eq_of_mul_eq_mul_right 
Nat.eq_of_mul_eq_mul_right: ∀ {n m k : ℕ}, 0 < m → n * m = k * m → n = k
Nat.eq_of_mul_eq_mul_right

instance 
cancelCommMonoidWithZero: CancelCommMonoidWithZero ℕ
cancelCommMonoidWithZero : 
CancelCommMonoidWithZero: Type ?u.2611 → Type ?u.2611
CancelCommMonoidWithZero 
ℕ: Type
ℕ :=
  { (
inferInstance: {α : Sort ?u.2617} → [i : α] → α
inferInstance : 
CommMonoidWithZero: Type ?u.2616 → Type ?u.2616
CommMonoidWithZero 
ℕ: Type
ℕ) with
    mul_left_cancel_of_ne_zero :=
      fun 
h1: ?m.2697
h1 
h2: ?m.2700
h2 => 
Nat.eq_of_mul_eq_mul_left: ∀ {m k n : ℕ}, 0 < n → n * m = n * k → m = k
Nat.eq_of_mul_eq_mul_left (
Nat.pos_of_ne_zero: ∀ {n : ℕ}, n ≠ 0 → 0 < n
Nat.pos_of_ne_zero 
h1: ?m.2697
h1) 
h2: ?m.2700
h2 }
#align nat.cancel_comm_monoid_with_zero 
Nat.cancelCommMonoidWithZero: CancelCommMonoidWithZero ℕ
Nat.cancelCommMonoidWithZero

attribute [simp]
  
Nat.not_lt_zero: ∀ (n : ℕ), ¬n < 0
Nat.not_lt_zero 
Nat.succ_ne_zero: ∀ (n : ℕ), succ n ≠ 0
Nat.succ_ne_zero 
Nat.succ_ne_self: ∀ (n : ℕ), succ n ≠ n
Nat.succ_ne_self 
Nat.zero_ne_one: 0 ≠ 1
Nat.zero_ne_one 
Nat.one_ne_zero: 1 ≠ 0
Nat.one_ne_zero
  -- Nat.zero_ne_bit1 Nat.bit1_ne_zero Nat.bit0_ne_one Nat.one_ne_bit0 Nat.bit0_ne_bit1
  -- Nat.bit1_ne_bit0

variable {
m: ℕ
m 
n: ℕ
n 
k: ℕ
k : 
ℕ: Type
ℕ}

/-!
### Recursion and `forall`/`exists`
-/

-- Porting note:
-- this doesn't work as a simp lemma in Lean 4
-- @[simp]
theorem 
and_forall_succ: ∀ {p : ℕ → Prop}, (p 0 ∧ ∀ (n : ℕ), p (n + 1)) ↔ ∀ (n : ℕ), p n
and_forall_succ {
p: ℕ → Prop
p : 
ℕ: Type
ℕ → 
Prop: Type
Prop} : (
p: ℕ → Prop
p 
0: ?m.2960
0 ∧ ∀ 
n: ?m.2971
n, 
p: ℕ → Prop
p (
n: ?m.2971
n + 
1: ?m.2978
1)) ↔ ∀ 
n: ?m.3033
n, 
p: ℕ → Prop
p 
n: ?m.3033
n :=
  ⟨fun 
h: ?m.3055
h 
n: ?m.3058
n => 
Nat.casesOn: ∀ {motive : ℕ → Sort ?u.3060} (t : ℕ), motive zero → (∀ (n : ℕ), motive (succ n)) → motive t
Nat.casesOn 
n: ?m.3058
n 
h: ?m.3055
h.
1: ∀ {a b : Prop}, a ∧ b → a
1 
h: ?m.3055
h.
2: ∀ {a b : Prop}, a ∧ b → b
2, fun 
h: ?m.3086
h => ⟨
h: ?m.3086
h 
_: ℕ
_, fun 
_: ?m.3100
_ => 
h: ?m.3086
h 
_: ℕ
_⟩⟩
#align nat.and_forall_succ 
Nat.and_forall_succ: ∀ {p : ℕ → Prop}, (p 0 ∧ ∀ (n : ℕ), p (n + 1)) ↔ ∀ (n : ℕ), p n
Nat.and_forall_succ

-- Porting note:
-- this doesn't work as a simp lemma in Lean 4
-- @[simp]
theorem 
or_exists_succ: ∀ {p : ℕ → Prop}, (p 0 ∨ ∃ n, p (n + 1)) ↔ ∃ n, p n
or_exists_succ {
p: ℕ → Prop
p : 
ℕ: Type
ℕ → 
Prop: Type
Prop} : (
p: ℕ → Prop
p 
0: ?m.3136
0 ∨ ∃ 
n: ?m.3149
n, 
p: ℕ → Prop
p (
n: ?m.3149
n + 
1: ?m.3155
1)) ↔ ∃ 
n: ?m.3213
n, 
p: ℕ → Prop
p 
n: ?m.3213
n :=
  ⟨fun 
h: ?m.3234
h => 
h: ?m.3234
h.
elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
elim (fun 
h0: ?m.3248
h0 => ⟨
0: ?m.3263
0, 
h0: ?m.3248
h0⟩) fun ⟨
n: ℕ
n, 
hn: p (n + 1)
hn⟩ => ⟨
n: ℕ
n + 
1: ?m.3310
1, 
hn: p (n + 1)
hn⟩, by
Goals accomplished! 🐙
    
m, n, k: ℕ

p: ℕ → Prop

(∃ n, p n) → p 0 ∨ ∃ n, p (n + 1)rintro 
⟨_ | n, hn⟩: ∃ n, p n
⟨
_ | n: ℕ
_ | 
n: ℕ
n
⟨_ | n, hn⟩: ∃ n, p n
, 
hn: unknown free variable '_uniq.3446'
hn
⟨_ | n, hn⟩: ∃ n, p n
⟩
m, n, k: ℕ

p: ℕ → Prop

hn: p zero

intro.zero
p 0 ∨ ∃ n, p (n + 1)
m, n✝, k: ℕ

p: ℕ → Prop

n: ℕ

hn: p (succ n)

intro.succ
p 0 ∨ ∃ n, p (n + 1)
    
m, n, k: ℕ

p: ℕ → Prop

(∃ n, p n) → p 0 ∨ ∃ n, p (n + 1)exacts[
Or.inl: ∀ {a b : Prop}, a → a ∨ b
Or.inl 
hn: p zero
hn, 
Or.inr: ∀ {a b : Prop}, b → a ∨ b
Or.inr ⟨
n: ℕ
n, 
hn: p (succ n)
hn⟩]
Goals accomplished! 🐙⟩
#align nat.or_exists_succ 
Nat.or_exists_succ: ∀ {p : ℕ → Prop}, (p 0 ∨ ∃ n, p (n + 1)) ↔ ∃ n, p n
Nat.or_exists_succ

/-! ### `succ` -/


theorem 
_root_.LT.lt.nat_succ_le: ∀ {n m : ℕ}, n < m → succ n ≤ m
_root_.LT.lt.nat_succ_le {
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ} (
h: n < m
h : 
n: ℕ
n < 
m: ℕ
m) : 
succ: ℕ → ℕ
succ 
n: ℕ
n ≤ 
m: ℕ
m :=
  
succ_le_of_lt: ∀ {n m : ℕ}, n < m → succ n ≤ m
succ_le_of_lt 
h: n < m
h
#align has_lt.lt.nat_succ_le 
LT.lt.nat_succ_le: ∀ {n m : ℕ}, n < m → succ n ≤ m
LT.lt.nat_succ_le

-- Moved to Std
#align nat.succ_eq_one_add 
Nat.succ_eq_one_add: ∀ (n : ℕ), succ n = 1 + n
Nat.succ_eq_one_add

theorem 
eq_of_lt_succ_of_not_lt: ∀ {a b : ℕ}, a < b + 1 → ¬a < b → a = b
eq_of_lt_succ_of_not_lt {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} (
h1: a < b + 1
h1 : 
a: ℕ
a < 
b: ℕ
b + 
1: ?m.3569
1) (
h2: ¬a < b
h2 : ¬
a: ℕ
a < 
b: ℕ
b) : 
a: ℕ
a = 
b: ℕ
b :=
  have 
h3: a ≤ b
h3 : 
a: ℕ
a ≤ 
b: ℕ
b := 
le_of_lt_succ: ∀ {m n : ℕ}, m < succ n → m ≤ n
le_of_lt_succ 
h1: a < b + 1
h1
  
Or.elim: ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
Or.elim (
eq_or_lt_of_not_lt: ∀ {α : Type ?u.3667} [inst : LinearOrder α] {a b : α}, ¬a < b → a = b ∨ b < a
eq_or_lt_of_not_lt 
h2: ¬a < b
h2) (fun 
h: ?m.3690
h => 
h: ?m.3690
h) fun 
h: ?m.3695
h => 
absurd: ∀ {a : Prop} {b : Sort ?u.3697}, a → ¬a → b
absurd 
h: ?m.3695
h (
not_lt_of_ge: ∀ {α : Type ?u.3700} [inst : Preorder α] {a b : α}, a ≥ b → ¬a < b
not_lt_of_ge 
h3: a ≤ b
h3)
#align nat.eq_of_lt_succ_of_not_lt 
Nat.eq_of_lt_succ_of_not_lt: ∀ {a b : ℕ}, a < b + 1 → ¬a < b → a = b
Nat.eq_of_lt_succ_of_not_lt

theorem 
eq_of_le_of_lt_succ: ∀ {n m : ℕ}, n ≤ m → m < n + 1 → m = n
eq_of_le_of_lt_succ {
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ} (
h₁: n ≤ m
h₁ : 
n: ℕ
n ≤ 
m: ℕ
m) (
h₂: m < n + 1
h₂ : 
m: ℕ
m < 
n: ℕ
n + 
1: ?m.3770
1) : 
m: ℕ
m = 
n: ℕ
n :=
  
Nat.le_antisymm: ∀ {n m : ℕ}, n ≤ m → m ≤ n → n = m
Nat.le_antisymm (
le_of_succ_le_succ: ∀ {n m : ℕ}, succ n ≤ succ m → n ≤ m
le_of_succ_le_succ 
h₂: m < n + 1
h₂) 
h₁: n ≤ m
h₁
#align nat.eq_of_le_of_lt_succ 
Nat.eq_of_le_of_lt_succ: ∀ {n m : ℕ}, n ≤ m → m < n + 1 → m = n
Nat.eq_of_le_of_lt_succ

-- Moved to Std
#align nat.one_add 
Nat.one_add: ∀ (n : ℕ), 1 + n = succ n
Nat.one_add

@[simp]
theorem 
succ_pos': ∀ {n : ℕ}, 0 < succ n
succ_pos' {
n: ℕ
n : 
ℕ: Type
ℕ} : 
0: ?m.3872
0 < 
succ: ℕ → ℕ
succ 
n: ℕ
n :=
  
succ_pos: ∀ (n : ℕ), 0 < succ n
succ_pos 
n: ℕ
n
#align nat.succ_pos' 
Nat.succ_pos': ∀ {n : ℕ}, 0 < succ n
Nat.succ_pos'

-- Moved to Std
#align nat.succ_inj' 
Nat.succ_inj': ∀ {n m : ℕ}, succ n = succ m ↔ n = m
Nat.succ_inj'

theorem 
succ_injective: Function.Injective succ
succ_injective : 
Function.Injective: {α : Sort ?u.3928} → {β : Sort ?u.3927} → (α → β) → Prop
Function.Injective 
Nat.succ: ℕ → ℕ
Nat.succ := fun 
_: ?m.3936
_ 
_: ?m.3939
_ => 
succ.inj: ∀ {n n_1 : ℕ}, succ n = succ n_1 → n = n_1
succ.inj
#align nat.succ_injective 
Nat.succ_injective: Function.Injective succ
Nat.succ_injective

theorem 
succ_ne_succ: ∀ {n m : ℕ}, succ n ≠ succ m ↔ n ≠ m
succ_ne_succ {
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ} : 
succ: ℕ → ℕ
succ 
n: ℕ
n ≠ 
succ: ℕ → ℕ
succ 
m: ℕ
m ↔ 
n: ℕ
n ≠ 
m: ℕ
m :=
  
succ_injective: Function.Injective succ
succ_injective.
ne_iff: ∀ {α : Sort ?u.3971} {β : Sort ?u.3972} {f : α → β}, Function.Injective f → ∀ {x y : α}, f x ≠ f y ↔ x ≠ y
ne_iff
#align nat.succ_ne_succ 
Nat.succ_ne_succ: ∀ {n m : ℕ}, succ n ≠ succ m ↔ n ≠ m
Nat.succ_ne_succ

-- Porting note: no longer a simp lemma, as simp can prove this
theorem 
succ_succ_ne_one: ∀ (n : ℕ), succ (succ n) ≠ 1
succ_succ_ne_one (
n: ℕ
n : 
ℕ: Type
ℕ) : 
n: ℕ
n.
succ: ℕ → ℕ
succ.
succ: ℕ → ℕ
succ ≠ 
1: ?m.4009
1 :=
  
succ_ne_succ: ∀ {n m : ℕ}, succ n ≠ succ m ↔ n ≠ m
succ_ne_succ.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr 
n: ℕ
n.
succ_ne_zero: ∀ (n : ℕ), succ n ≠ 0
succ_ne_zero
#align nat.succ_succ_ne_one 
Nat.succ_succ_ne_one: ∀ (n : ℕ), succ (succ n) ≠ 1
Nat.succ_succ_ne_one

@[simp]
theorem 
one_lt_succ_succ: ∀ (n : ℕ), 1 < succ (succ n)
one_lt_succ_succ (
n: ℕ
n : 
ℕ: Type
ℕ) : 
1: ?m.4064
1 < 
n: ℕ
n.
succ: ℕ → ℕ
succ.
succ: ℕ → ℕ
succ :=
  
succ_lt_succ: ∀ {n m : ℕ}, n < m → succ n < succ m
succ_lt_succ <| 
succ_pos: ∀ (n : ℕ), 0 < succ n
succ_pos 
n: ℕ
n
#align nat.one_lt_succ_succ 
Nat.one_lt_succ_succ: ∀ (n : ℕ), 1 < succ (succ n)
Nat.one_lt_succ_succ

-- Porting note: Nat.succ_le_succ_iff is in Std

theorem 
max_succ_succ: ∀ {m n : ℕ}, max (succ m) (succ n) = succ (max m n)
max_succ_succ {
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ} : 
max: {α : Type ?u.4149} → [self : Max α] → α → α → α
max (
succ: ℕ → ℕ
succ 
m: ℕ
m) (
succ: ℕ → ℕ
succ 
n: ℕ
n) = 
succ: ℕ → ℕ
succ (
max: {α : Type ?u.4155} → [self : Max α] → α → α → α
max 
m: ℕ
m 
n: ℕ
n) := by
Goals accomplished! 🐙
  
m✝, n✝, k, m, n: ℕ

max (succ m) (succ n) = succ (max m n)by_cases 
h1: ?m.4189
h1 : 
m: ℕ
m ≤ 
n: ℕ
n
m✝, n✝, k, m, n: ℕ

h1: m ≤ n

pos
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)
  
m✝, n✝, k, m, n: ℕ

max (succ m) (succ n) = succ (max m n)rw [
m✝, n✝, k, m, n: ℕ

h1: m ≤ n

pos
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)
max_eq_right: ∀ {α : Type ?u.4203} [inst : LinearOrder α] {a b : α}, a ≤ b → max a b = b
max_eq_right 
h1: ?m.4189
h1,
m✝, n✝, k, m, n: ℕ

h1: m ≤ n

pos
max (succ m) (succ n) = succ n
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n) 
m✝, n✝, k, m, n: ℕ

h1: m ≤ n

pos
max (succ m) (succ n) = succ (max m n)
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)
max_eq_right: ∀ {α : Type ?u.4220} [inst : LinearOrder α] {a b : α}, a ≤ b → max a b = b
max_eq_right (
succ_le_succ: ∀ {n m : ℕ}, n ≤ m → succ n ≤ succ m
succ_le_succ 
h1: ?m.4189
h1)
m✝, n✝, k, m, n: ℕ

h1: m ≤ n

pos
succ n = succ n
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)]
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)
  
m✝, n✝, k, m, n: ℕ

max (succ m) (succ n) = succ (max m n)·
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n) 
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)rw [
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)
not_le: ∀ {α : Type ?u.4242} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_le
m✝, n✝, k, m, n: ℕ

h1: n < m

neg
max (succ m) (succ n) = succ (max m n)]
m✝, n✝, k, m, n: ℕ

h1: n < m

neg
max (succ m) (succ n) = succ (max m n) at 
h1: ?m.4196
h1
m✝, n✝, k, m, n: ℕ

h1: n < m

neg
max (succ m) (succ n) = succ (max m n)
    
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)have 
h2: ?m.4299
h2 := 
le_of_lt: ∀ {α : Type ?u.4300} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_lt 
h1: n < m
h1
m✝, n✝, k, m, n: ℕ

h1: n < m

h2: n ≤ m

neg
max (succ m) (succ n) = succ (max m n)
    
m✝, n✝, k, m, n: ℕ

h1: ¬m ≤ n

neg
max (succ m) (succ n) = succ (max m n)rw [
m✝, n✝, k, m, n: ℕ

h1: n < m

h2: n ≤ m

neg
max (succ m) (succ n) = succ (max m n)
max_eq_left: ∀ {α : Type ?u.4338} [inst : LinearOrder α] {a b : α}, b ≤ a → max a b = a
max_eq_left 
h2: ?m.4299
h2,
m✝, n✝, k, m, n: ℕ

h1: n < m

h2: n ≤ m

neg
max (succ m) (succ n) = succ m 
m✝, n✝, k, m, n: ℕ

h1: n < m

h2: n ≤ m

neg
max (succ m) (succ n) = succ (max m n)
max_eq_left: ∀ {α : Type ?u.4350} [inst : LinearOrder α] {a b : α}, b ≤ a → max a b = a
max_eq_left (
succ_le_succ: ∀ {n m : ℕ}, n ≤ m → succ n ≤ succ m
succ_le_succ 
h2: ?m.4299
h2)
m✝, n✝, k, m, n: ℕ

h1: n < m

h2: n ≤ m

neg
succ m = succ m]
Goals accomplished! 🐙
#align nat.max_succ_succ 
Nat.max_succ_succ: ∀ {m n : ℕ}, max (succ m) (succ n) = succ (max m n)
Nat.max_succ_succ

theorem 
not_succ_lt_self: ∀ {n : ℕ}, ¬succ n < n
not_succ_lt_self {
n: ℕ
n : 
ℕ: Type
ℕ} : ¬
succ: ℕ → ℕ
succ 
n: ℕ
n < 
n: ℕ
n :=
  
not_lt_of_ge: ∀ {α : Type ?u.4396} [inst : Preorder α] {a b : α}, a ≥ b → ¬a < b
not_lt_of_ge (
Nat.le_succ: ∀ (n : ℕ), n ≤ succ n
Nat.le_succ 
_: ℕ
_)
#align nat.not_succ_lt_self 
Nat.not_succ_lt_self: ∀ {n : ℕ}, ¬succ n < n
Nat.not_succ_lt_self

theorem 
lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
lt_succ_iff {
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ} : 
m: ℕ
m < 
succ: ℕ → ℕ
succ 
n: ℕ
n ↔ 
m: ℕ
m ≤ 
n: ℕ
n :=
  ⟨
le_of_lt_succ: ∀ {m n : ℕ}, m < succ n → m ≤ n
le_of_lt_succ, 
lt_succ_of_le: ∀ {n m : ℕ}, n ≤ m → n < succ m
lt_succ_of_le⟩
#align nat.lt_succ_iff 
Nat.lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
Nat.lt_succ_iff

theorem 
succ_le_iff: ∀ {m n : ℕ}, succ m ≤ n ↔ m < n
succ_le_iff {
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ} : 
succ: ℕ → ℕ
succ 
m: ℕ
m ≤ 
n: ℕ
n ↔ 
m: ℕ
m < 
n: ℕ
n :=
  ⟨
lt_of_succ_le: ∀ {n m : ℕ}, succ n ≤ m → n < m
lt_of_succ_le, 
succ_le_of_lt: ∀ {n m : ℕ}, n < m → succ n ≤ m
succ_le_of_lt⟩
#align nat.succ_le_iff 
Nat.succ_le_iff: ∀ {m n : ℕ}, succ m ≤ n ↔ m < n
Nat.succ_le_iff

theorem 
lt_iff_add_one_le: ∀ {m n : ℕ}, m < n ↔ m + 1 ≤ n
lt_iff_add_one_le {
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ} : 
m: ℕ
m < 
n: ℕ
n ↔ 
m: ℕ
m + 
1: ?m.4569
1 ≤ 
n: ℕ
n := by
Goals accomplished! 🐙 
m✝, n✝, k, m, n: ℕ

m < n ↔ m + 1 ≤ nrw [
m✝, n✝, k, m, n: ℕ

m < n ↔ m + 1 ≤ n
succ_le_iff: ∀ {m n : ℕ}, succ m ≤ n ↔ m < n
succ_le_iff
m✝, n✝, k, m, n: ℕ

m < n ↔ m < n]
Goals accomplished! 🐙
#align nat.lt_iff_add_one_le 
Nat.lt_iff_add_one_le: ∀ {m n : ℕ}, m < n ↔ m + 1 ≤ n
Nat.lt_iff_add_one_le

-- Just a restatement of `Nat.lt_succ_iff` using `+1`.
theorem 
lt_add_one_iff: ∀ {a b : ℕ}, a < b + 1 ↔ a ≤ b
lt_add_one_iff {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} : 
a: ℕ
a < 
b: ℕ
b + 
1: ?m.4678
1 ↔ 
a: ℕ
a ≤ 
b: ℕ
b :=
  
lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
lt_succ_iff
#align nat.lt_add_one_iff 
Nat.lt_add_one_iff: ∀ {a b : ℕ}, a < b + 1 ↔ a ≤ b
Nat.lt_add_one_iff

-- A flipped version of `lt_add_one_iff`.
theorem 
lt_one_add_iff: ∀ {a b : ℕ}, a < 1 + b ↔ a ≤ b
lt_one_add_iff {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} : 
a: ℕ
a < 
1: ?m.4780
1 + 
b: ℕ
b ↔ 
a: ℕ
a ≤ 
b: ℕ
b := by
Goals accomplished! 🐙 
m, n, k, a, b: ℕ

a < 1 + b ↔ a ≤ bsimp only [
add_comm: ∀ {G : Type ?u.4867} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm, 
lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
lt_succ_iff]
Goals accomplished! 🐙
#align nat.lt_one_add_iff 
Nat.lt_one_add_iff: ∀ {a b : ℕ}, a < 1 + b ↔ a ≤ b
Nat.lt_one_add_iff

-- This is true reflexively, by the definition of `≤` on ℕ,
-- but it's still useful to have, to convince Lean to change the syntactic type.
theorem 
add_one_le_iff: ∀ {a b : ℕ}, a + 1 ≤ b ↔ a < b
add_one_le_iff {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} : 
a: ℕ
a + 
1: ?m.5016
1 ≤ 
b: ℕ
b ↔ 
a: ℕ
a < 
b: ℕ
b :=
  
Iff.refl: ∀ (a : Prop), a ↔ a
Iff.refl 
_: Prop
_
#align nat.add_one_le_iff 
Nat.add_one_le_iff: ∀ {a b : ℕ}, a + 1 ≤ b ↔ a < b
Nat.add_one_le_iff

theorem 
one_add_le_iff: ∀ {a b : ℕ}, 1 + a ≤ b ↔ a < b
one_add_le_iff {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} : 
1: ?m.5118
1 + 
a: ℕ
a ≤ 
b: ℕ
b ↔ 
a: ℕ
a < 
b: ℕ
b := by
Goals accomplished! 🐙 
m, n, k, a, b: ℕ

1 + a ≤ b ↔ a < bsimp only [
add_comm: ∀ {G : Type ?u.5210} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm, 
add_one_le_iff: ∀ {a b : ℕ}, a + 1 ≤ b ↔ a < b
add_one_le_iff]
Goals accomplished! 🐙
#align nat.one_add_le_iff 
Nat.one_add_le_iff: ∀ {a b : ℕ}, 1 + a ≤ b ↔ a < b
Nat.one_add_le_iff

theorem 
of_le_succ: ∀ {n m : ℕ}, n ≤ succ m → n ≤ m ∨ n = succ m
of_le_succ {
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ} (
H: n ≤ succ m
H : 
n: ℕ
n ≤ 
m: ℕ
m.
succ: ℕ → ℕ
succ) : 
n: ℕ
n ≤ 
m: ℕ
m ∨ 
n: ℕ
n = 
m: ℕ
m.
succ: ℕ → ℕ
succ :=
  
H: n ≤ succ m
H.
lt_or_eq_dec: ∀ {α : Type ?u.5377} [inst : PartialOrder α] [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] {a b : α},
  a ≤ b → a < b ∨ a = b
lt_or_eq_dec.
imp: ∀ {a c b d : Prop}, (a → c) → (b → d) → a ∨ b → c ∨ d
imp 
le_of_lt_succ: ∀ {m n : ℕ}, m < succ n → m ≤ n
le_of_lt_succ 
id: ∀ {α : Sort ?u.5449}, α → α
id
#align nat.of_le_succ 
Nat.of_le_succ: ∀ {n m : ℕ}, n ≤ succ m → n ≤ m ∨ n = succ m
Nat.of_le_succ

theorem 
succ_lt_succ_iff: ∀ {m n : ℕ}, succ m < succ n ↔ m < n
succ_lt_succ_iff {
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ} : 
succ: ℕ → ℕ
succ 
m: ℕ
m < 
succ: ℕ → ℕ
succ 
n: ℕ
n ↔ 
m: ℕ
m < 
n: ℕ
n :=
  ⟨
lt_of_succ_lt_succ: ∀ {n m : ℕ}, succ n < succ m → n < m
lt_of_succ_lt_succ, 
succ_lt_succ: ∀ {n m : ℕ}, n < m → succ n < succ m
succ_lt_succ⟩
#align nat.succ_lt_succ_iff 
Nat.succ_lt_succ_iff: ∀ {m n : ℕ}, succ m < succ n ↔ m < n
Nat.succ_lt_succ_iff

theorem 
div_le_iff_le_mul_add_pred: ∀ {m n k : ℕ}, 0 < n → (m / n ≤ k ↔ m ≤ n * k + (n - 1))
div_le_iff_le_mul_add_pred {
m: ℕ
m 
n: ℕ
n 
k: ℕ
k : 
ℕ: Type
ℕ} (
n0: 0 < n
n0 : 
0: ?m.5521
0 < 
n: ℕ
n) : 
m: ℕ
m / 
n: ℕ
n ≤ 
k: ℕ
k ↔ 
m: ℕ
m ≤ 
n: ℕ
n * 
k: ℕ
k + (
n: ℕ
n - 
1: ?m.5613
1) := by
Goals accomplished! 🐙
  
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n ≤ k ↔ m ≤ n * k + (n - 1)rw [
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n ≤ k ↔ m ≤ n * k + (n - 1)← 
lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
lt_succ_iff,
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n < succ k ↔ m ≤ n * k + (n - 1) 
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n ≤ k ↔ m ≤ n * k + (n - 1)
div_lt_iff_lt_mul: ∀ {k x y : ℕ}, 0 < k → (x / k < y ↔ x < y * k)
div_lt_iff_lt_mul 
n0: 0 < n
n0,
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m < succ k * n ↔ m ≤ n * k + (n - 1) 
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n ≤ k ↔ m ≤ n * k + (n - 1)
succ_mul: ∀ (n m : ℕ), succ n * m = n * m + m
succ_mul,
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m < k * n + n ↔ m ≤ n * k + (n - 1) 
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n ≤ k ↔ m ≤ n * k + (n - 1)
mul_comm: ∀ {G : Type ?u.5800} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m < n * k + n ↔ m ≤ n * k + (n - 1)]
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m < n * k + n ↔ m ≤ n * k + (n - 1)
  
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n ≤ k ↔ m ≤ n * k + (n - 1)cases 
n: ℕ
n
m✝, n, k✝, m, k: ℕ

n0: 0 < zero

zero
m < zero * k + zero ↔ m ≤ zero * k + (zero - 1)
m✝, n, k✝, m, k, n✝: ℕ

n0: 0 < succ n✝

succ
m < succ n✝ * k + succ n✝ ↔ m ≤ succ n✝ * k + (succ n✝ - 1)
  
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n ≤ k ↔ m ≤ n * k + (n - 1)·
m✝, n, k✝, m, k: ℕ

n0: 0 < zero

zero
m < zero * k + zero ↔ m ≤ zero * k + (zero - 1) 
m✝, n, k✝, m, k: ℕ

n0: 0 < zero

zero
m < zero * k + zero ↔ m ≤ zero * k + (zero - 1)
m✝, n, k✝, m, k, n✝: ℕ

n0: 0 < succ n✝

succ
m < succ n✝ * k + succ n✝ ↔ m ≤ succ n✝ * k + (succ n✝ - 1)cases 
n0: 0 < zero
n0
Goals accomplished! 🐙

  
m✝, n✝, k✝, m, n, k: ℕ

n0: 0 < n

m / n ≤ k ↔ m ≤ n * k + (n - 1)exact 
lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
lt_succ_iff
Goals accomplished! 🐙
#align nat.div_le_iff_le_mul_add_pred 
Nat.div_le_iff_le_mul_add_pred: ∀ {m n k : ℕ}, 0 < n → (m / n ≤ k ↔ m ≤ n * k + (n - 1))
Nat.div_le_iff_le_mul_add_pred

theorem 
two_lt_of_ne: ∀ {n : ℕ}, n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n
two_lt_of_ne : ∀ {
n: ?m.6021
n}, 
n: ?m.6021
n ≠ 
0: ?m.6028
0 → 
n: ?m.6021
n ≠ 
1: ?m.6044
1 → 
n: ?m.6021
n ≠ 
2: ?m.6057
2 → 
2: ?m.6067
2 < 
n: ?m.6021
n
  | 
0: ℕ
0, 
h: 0 ≠ 0
h, _, _ => (
h: 0 ≠ 0
h 
rfl: ∀ {α : Sort ?u.6259} {a : α}, a = a
rfl).
elim: ∀ {C : Sort ?u.6265}, False → C
elim
  | 
1: ℕ
1, _, 
h: 1 ≠ 1
h, _ => (
h: 1 ≠ 1
h 
rfl: ∀ {α : Sort ?u.6299} {a : α}, a = a
rfl).
elim: ∀ {C : Sort ?u.6302}, False → C
elim
  | 
2: ℕ
2, _, _, 
h: 2 ≠ 2
h => (
h: 2 ≠ 2
h 
rfl: ∀ {α : Sort ?u.6336} {a : α}, a = a
rfl).
elim: ∀ {C : Sort ?u.6339}, False → C
elim
  -- Porting note: was `by decide`
  | 
n: ℕ
n + 3, _, _, _ => by
Goals accomplished! 🐙 
m, n✝, k, n: ℕ

x✝²: n + 3 ≠ 0

x✝¹: n + 3 ≠ 1

x✝: n + 3 ≠ 2

2 < n + 3rw [
m, n✝, k, n: ℕ

x✝²: n + 3 ≠ 0

x✝¹: n + 3 ≠ 1

x✝: n + 3 ≠ 2

2 < n + 3
Nat.lt_iff_add_one_le: ∀ {m n : ℕ}, m < n ↔ m + 1 ≤ n
Nat.lt_iff_add_one_le
m, n✝, k, n: ℕ

x✝²: n + 3 ≠ 0

x✝¹: n + 3 ≠ 1

x✝: n + 3 ≠ 2

2 + 1 ≤ n + 3]
m, n✝, k, n: ℕ

x✝²: n + 3 ≠ 0

x✝¹: n + 3 ≠ 1

x✝: n + 3 ≠ 2

2 + 1 ≤ n + 3;
m, n✝, k, n: ℕ

x✝²: n + 3 ≠ 0

x✝¹: n + 3 ≠ 1

x✝: n + 3 ≠ 2

2 + 1 ≤ n + 3 
m, n✝, k, n: ℕ

x✝²: n + 3 ≠ 0

x✝¹: n + 3 ≠ 1

x✝: n + 3 ≠ 2

2 < n + 3convert 
Nat.le_add_left: ∀ (n m : ℕ), n ≤ m + n
Nat.le_add_left 
3: ?m.6835
3 
n: ℕ
n
Goals accomplished! 🐙
#align nat.two_lt_of_ne 
Nat.two_lt_of_ne: ∀ {n : ℕ}, n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n
Nat.two_lt_of_ne

theorem 
forall_lt_succ: ∀ {P : ℕ → Prop} {n : ℕ}, (∀ (m : ℕ), m < n + 1 → P m) ↔ (∀ (m : ℕ), m < n → P m) ∧ P n
forall_lt_succ {
P: ℕ → Prop
P : 
ℕ: Type
ℕ → 
Prop: Type
Prop} {
n: ℕ
n : 
ℕ: Type
ℕ} : (∀ 
m: ?m.6925
m < 
n: ℕ
n + 
1: ?m.6934
1, 
P: ℕ → Prop
P 
m: ?m.6925
m) ↔ (∀ 
m: ?m.7003
m < 
n: ℕ
n, 
P: ℕ → Prop
P 
m: ?m.7003
m) ∧ 
P: ℕ → Prop
P 
n: ℕ
n := by
Goals accomplished! 🐙
  
m, n✝, k: ℕ

P: ℕ → Prop

n: ℕ

(∀ (m : ℕ), m < n + 1 → P m) ↔ (∀ (m : ℕ), m < n → P m) ∧ P nsimp only [
lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
lt_succ_iff, 
Decidable.le_iff_eq_or_lt: ∀ {α : Type ?u.7042} [inst : PartialOrder α] [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] {a b : α},
  a ≤ b ↔ a = b ∨ a < b
Decidable.le_iff_eq_or_lt, 
forall_eq_or_imp: ∀ {α : Sort ?u.7069} {p q : α → Prop} {a' : α}, (∀ (a : α), a = a' ∨ q a → p a) ↔ p a' ∧ ∀ (a : α), q a → p a
forall_eq_or_imp, 
and_comm: ∀ {a b : Prop}, a ∧ b ↔ b ∧ a
and_comm]
Goals accomplished! 🐙
#align nat.forall_lt_succ 
Nat.forall_lt_succ: ∀ {P : ℕ → Prop} {n : ℕ}, (∀ (m : ℕ), m < n + 1 → P m) ↔ (∀ (m : ℕ), m < n → P m) ∧ P n
Nat.forall_lt_succ

theorem 
exists_lt_succ: ∀ {P : ℕ → Prop} {n : ℕ}, (∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P n
exists_lt_succ {
P: ℕ → Prop
P : 
ℕ: Type
ℕ → 
Prop: Type
Prop} {
n: ℕ
n : 
ℕ: Type
ℕ} : (∃ 
m: ?m.7394
m < 
n: ℕ
n + 
1: ?m.7401
1, 
P: ℕ → Prop
P 
m: ?m.7394
m) ↔ (∃ 
m: ?m.7471
m < 
n: ℕ
n, 
P: ℕ → Prop
P 
m: ?m.7471
m) ∨ 
P: ℕ → Prop
P 
n: ℕ
n := by
Goals accomplished! 🐙
  
m, n✝, k: ℕ

P: ℕ → Prop

n: ℕ

(∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P nrw [
m, n✝, k: ℕ

P: ℕ → Prop

n: ℕ

(∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P n← 
not_iff_not: ∀ {a b : Prop}, (¬a ↔ ¬b) ↔ (a ↔ b)
not_iff_not
m, n✝, k: ℕ

P: ℕ → Prop

n: ℕ

(¬∃ m, m < n + 1 ∧ P m) ↔ ¬((∃ m, m < n ∧ P m) ∨ P n)]
m, n✝, k: ℕ

P: ℕ → Prop

n: ℕ

(¬∃ m, m < n + 1 ∧ P m) ↔ ¬((∃ m, m < n ∧ P m) ∨ P n)
  
m, n✝, k: ℕ

P: ℕ → Prop

n: ℕ

(∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P npush_neg
m, n✝, k: ℕ

P: ℕ → Prop

n: ℕ

(∀ (m : ℕ), m < n + 1 → ¬P m) ↔ (∀ (m : ℕ), m < n → ¬P m) ∧ ¬P n
  
m, n✝, k: ℕ

P: ℕ → Prop

n: ℕ

(∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P nexact 
forall_lt_succ: ∀ {P : ℕ → Prop} {n : ℕ}, (∀ (m : ℕ), m < n + 1 → P m) ↔ (∀ (m : ℕ), m < n → P m) ∧ P n
forall_lt_succ
Goals accomplished! 🐙
#align nat.exists_lt_succ 
Nat.exists_lt_succ: ∀ {P : ℕ → Prop} {n : ℕ}, (∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P n
Nat.exists_lt_succ

/-! ### `add` -/

-- Sometimes a bare `Nat.add` or similar appears as a consequence of unfolding
-- during pattern matching. These lemmas package them back up as typeclass
-- mediated operations.
@[simp]
theorem 
add_def: ∀ {a b : ℕ}, Nat.add a b = a + b
add_def {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} : 
Nat.add: ℕ → ℕ → ℕ
Nat.add 
a: ℕ
a 
b: ℕ
b = 
a: ℕ
a + 
b: ℕ
b :=
  
rfl: ∀ {α : Sort ?u.7695} {a : α}, a = a
rfl
#align nat.add_def 
Nat.add_def: ∀ {a b : ℕ}, Nat.add a b = a + b
Nat.add_def

@[simp]
theorem 
mul_def: ∀ {a b : ℕ}, Nat.mul a b = a * b
mul_def {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} : 
Nat.mul: ℕ → ℕ → ℕ
Nat.mul 
a: ℕ
a 
b: ℕ
b = 
a: ℕ
a * 
b: ℕ
b :=
  
rfl: ∀ {α : Sort ?u.7771} {a : α}, a = a
rfl
#align nat.mul_def 
Nat.mul_def: ∀ {a b : ℕ}, Nat.mul a b = a * b
Nat.mul_def

theorem 
exists_eq_add_of_le: m ≤ n → ∃ k, n = m + k
exists_eq_add_of_le (
h: m ≤ n
h : 
m: ℕ
m ≤ 
n: ℕ
n) : ∃ 
k: ℕ
k : 
ℕ: Type
ℕ, 
n: ℕ
n = 
m: ℕ
m + 
k: ℕ
k :=
  ⟨
n: ℕ
n - 
m: ℕ
m, (
add_sub_of_le: ∀ {a b : ℕ}, a ≤ b → a + (b - a) = b
add_sub_of_le 
h: m ≤ n
h).
symm: ∀ {α : Sort ?u.7908} {a b : α}, a = b → b = a
symm⟩
#align nat.exists_eq_add_of_le 
Nat.exists_eq_add_of_le: ∀ {m n : ℕ}, m ≤ n → ∃ k, n = m + k
Nat.exists_eq_add_of_le

theorem 
exists_eq_add_of_le': m ≤ n → ∃ k, n = k + m
exists_eq_add_of_le' (
h: m ≤ n
h : 
m: ℕ
m ≤ 
n: ℕ
n) : ∃ 
k: ℕ
k : 
ℕ: Type
ℕ, 
n: ℕ
n = 
k: ℕ
k + 
m: ℕ
m :=
  ⟨
n: ℕ
n - 
m: ℕ
m, (
Nat.sub_add_cancel: ∀ {n m : ℕ}, m ≤ n → n - m + m = n
Nat.sub_add_cancel 
h: m ≤ n
h).
symm: ∀ {α : Sort ?u.8046} {a b : α}, a = b → b = a
symm⟩
#align nat.exists_eq_add_of_le' 
Nat.exists_eq_add_of_le': ∀ {m n : ℕ}, m ≤ n → ∃ k, n = k + m
Nat.exists_eq_add_of_le'

theorem 
exists_eq_add_of_lt: ∀ {m n : ℕ}, m < n → ∃ k, n = m + k + 1
exists_eq_add_of_lt (
h: m < n
h : 
m: ℕ
m < 
n: ℕ
n) : ∃ 
k: ℕ
k : 
ℕ: Type
ℕ, 
n: ℕ
n = 
m: ℕ
m + 
k: ℕ
k + 
1: ?m.8088
1 :=
  ⟨
n: ℕ
n - (
m: ℕ
m + 
1: ?m.8193
1), by
Goals accomplished! 🐙 
m, n, k: ℕ

h: m < n

n = m + (n - (m + 1)) + 1rw [
m, n, k: ℕ

h: m < n

n = m + (n - (m + 1)) + 1
add_right_comm: ∀ {G : Type ?u.8271} [inst : AddCommSemigroup G] (a b c : G), a + b + c = a + c + b
add_right_comm,
m, n, k: ℕ

h: m < n

n = m + 1 + (n - (m + 1)) 
m, n, k: ℕ

h: m < n

n = m + (n - (m + 1)) + 1
add_sub_of_le: ∀ {a b : ℕ}, a ≤ b → a + (b - a) = b
add_sub_of_le 
h: m < n
h
m, n, k: ℕ

h: m < n

n = n]
Goals accomplished! 🐙⟩
#align nat.exists_eq_add_of_lt 
Nat.exists_eq_add_of_lt: ∀ {m n : ℕ}, m < n → ∃ k, n = m + k + 1
Nat.exists_eq_add_of_lt

/-! ### `pred` -/

@[simp]
theorem 
add_succ_sub_one: ∀ (n m : ℕ), n + succ m - 1 = n + m
add_succ_sub_one (
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ) : 
n: ℕ
n + 
succ: ℕ → ℕ
succ 
m: ℕ
m - 
1: ?m.8348
1 = 
n: ℕ
n + 
m: ℕ
m := by
Goals accomplished! 🐙 
m✝, n✝, k, n, m: ℕ

n + succ m - 1 = n + mrw [
m✝, n✝, k, n, m: ℕ

n + succ m - 1 = n + m
add_succ: ∀ (n m : ℕ), n + succ m = succ (n + m)
add_succ,
m✝, n✝, k, n, m: ℕ

succ (n + m) - 1 = n + m 
m✝, n✝, k, n, m: ℕ

n + succ m - 1 = n + m
succ_sub_one: ∀ (n : ℕ), succ n - 1 = n
succ_sub_one
m✝, n✝, k, n, m: ℕ

n + m = n + m]
Goals accomplished! 🐙
#align nat.add_succ_sub_one 
Nat.add_succ_sub_one: ∀ (n m : ℕ), n + succ m - 1 = n + m
Nat.add_succ_sub_one

@[simp]
theorem 
succ_add_sub_one: ∀ (n m : ℕ), succ n + m - 1 = n + m
succ_add_sub_one (
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ) : 
succ: ℕ → ℕ
succ 
n: ℕ
n + 
m: ℕ
m - 
1: ?m.8550
1 = 
n: ℕ
n + 
m: ℕ
m := by
Goals accomplished! 🐙 
m✝, n✝, k, n, m: ℕ

succ n + m - 1 = n + mrw [
m✝, n✝, k, n, m: ℕ

succ n + m - 1 = n + m
succ_add: ∀ (n m : ℕ), succ n + m = succ (n + m)
succ_add,
m✝, n✝, k, n, m: ℕ

succ (n + m) - 1 = n + m 
m✝, n✝, k, n, m: ℕ

succ n + m - 1 = n + m
succ_sub_one: ∀ (n : ℕ), succ n - 1 = n
succ_sub_one
m✝, n✝, k, n, m: ℕ

n + m = n + m]
Goals accomplished! 🐙
#align nat.succ_add_sub_one 
Nat.succ_add_sub_one: ∀ (n m : ℕ), succ n + m - 1 = n + m
Nat.succ_add_sub_one

theorem 
pred_eq_sub_one: ∀ (n : ℕ), pred n = n - 1
pred_eq_sub_one (
n: ℕ
n : 
ℕ: Type
ℕ) : 
pred: ℕ → ℕ
pred 
n: ℕ
n = 
n: ℕ
n - 
1: ?m.8747
1 :=
  
rfl: ∀ {α : Sort ?u.8810} {a : α}, a = a
rfl
#align nat.pred_eq_sub_one 
Nat.pred_eq_sub_one: ∀ (n : ℕ), pred n = n - 1
Nat.pred_eq_sub_one

theorem 
pred_eq_of_eq_succ: ∀ {m n : ℕ}, m = succ n → pred m = n
pred_eq_of_eq_succ {
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ} (
H: m = succ n
H : 
m: ℕ
m = 
n: ℕ
n.
succ: ℕ → ℕ
succ) : 
m: ℕ
m.
pred: ℕ → ℕ
pred = 
n: ℕ
n := by
Goals accomplished! 🐙 
m✝, n✝, k, m, n: ℕ

H: m = succ n

pred m = nsimp [
H: m = succ n
H]
Goals accomplished! 🐙
#align nat.pred_eq_of_eq_succ 
Nat.pred_eq_of_eq_succ: ∀ {m n : ℕ}, m = succ n → pred m = n
Nat.pred_eq_of_eq_succ

@[simp]
theorem 
pred_eq_succ_iff: ∀ {n m : ℕ}, pred n = succ m ↔ n = m + 2
pred_eq_succ_iff {
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ} : 
pred: ℕ → ℕ
pred 
n: ℕ
n = 
succ: ℕ → ℕ
succ 
m: ℕ
m ↔ 
n: ℕ
n = 
m: ℕ
m + 
2: ?m.8954
2 := by
Goals accomplished! 🐙
  
m✝, n✝, k, n, m: ℕ

pred n = succ m ↔ n = m + 2cases 
n: ℕ
n
m✝, n, k, m: ℕ

zero
pred zero = succ m ↔ zero = m + 2
m✝, n, k, m, n✝: ℕ

succ
pred (succ n✝) = succ m ↔ succ n✝ = m + 2 
m✝, n✝, k, n, m: ℕ

pred n = succ m ↔ n = m + 2<;>
m✝, n, k, m: ℕ

zero
pred zero = succ m ↔ zero = m + 2
m✝, n, k, m, n✝: ℕ

succ
pred (succ n✝) = succ m ↔ succ n✝ = m + 2 
m✝, n✝, k, n, m: ℕ

pred n = succ m ↔ n = m + 2constructor
m✝, n, k, m, n✝: ℕ

succ.mp
pred (succ n✝) = succ m → succ n✝ = m + 2
m✝, n, k, m, n✝: ℕ

succ.mpr
succ n✝ = m + 2 → pred (succ n✝) = succ m 
m✝, n✝, k, n, m: ℕ

pred n = succ m ↔ n = m + 2<;>
m✝, n, k, m: ℕ

zero.mp
pred zero = succ m → zero = m + 2
m✝, n, k, m: ℕ

zero.mpr
zero = m + 2 → pred zero = succ m
m✝, n, k, m, n✝: ℕ

succ.mp
pred (succ n✝) = succ m → succ n✝ = m + 2
m✝, n, k, m, n✝: ℕ

succ.mpr
succ n✝ = m + 2 → pred (succ n✝) = succ m 
m✝, n✝, k, n, m: ℕ

pred n = succ m ↔ n = m + 2rintro 
⟨⟩: ?b
⟨⟩
Goals accomplished! 🐙 
m✝, n✝, k, n, m: ℕ

pred n = succ m ↔ n = m + 2<;>
m✝, n, k, m: ℕ

succ.mp.refl
succ (succ m) = m + 2
m✝, n, k, m: ℕ

succ.mpr.refl
pred (succ (Nat.add m 1)) = succ m 
m✝, n✝, k, n, m: ℕ

pred n = succ m ↔ n = m + 2rfl
Goals accomplished! 🐙
#align nat.pred_eq_succ_iff 
Nat.pred_eq_succ_iff: ∀ {n m : ℕ}, pred n = succ m ↔ n = m + 2
Nat.pred_eq_succ_iff

theorem 
pred_sub: ∀ (n m : ℕ), pred n - m = pred (n - m)
pred_sub (
n: ℕ
n 
m: ℕ
m : 
ℕ: Type
ℕ) : 
pred: ℕ → ℕ
pred 
n: ℕ
n - 
m: ℕ
m = 
pred: ℕ → ℕ
pred (
n: ℕ
n - 
m: ℕ
m) := by
Goals accomplished! 🐙
  
m✝, n✝, k, n, m: ℕ

pred n - m = pred (n - m)rw [
m✝, n✝, k, n, m: ℕ

pred n - m = pred (n - m)← 
Nat.sub_one: ∀ (n : ℕ), n - 1 = pred n
Nat.sub_one,
m✝, n✝, k, n, m: ℕ

n - 1 - m = pred (n - m) 
m✝, n✝, k, n, m: ℕ

pred n - m = pred (n - m)
Nat.sub_sub: ∀ (n m k : ℕ), n - m - k = n - (m + k)
Nat.sub_sub,
m✝, n✝, k, n, m: ℕ

n - (1 + m) = pred (n - m) 
m✝, n✝, k, n, m: ℕ

pred n - m = pred (n - m)
one_add: ∀ (n : ℕ), 1 + n = succ n
one_add,
m✝, n✝, k, n, m: ℕ

n - succ m = pred (n - m) 
m✝, n✝, k, n, m: ℕ

pred n - m = pred (n - m)
sub_succ: ∀ (n m : ℕ), n - succ m = pred (n - m)
sub_succ
m✝, n✝, k, n, m: ℕ

pred (n - m) = pred (n - m)]
Goals accomplished! 🐙
#align nat.pred_sub 
Nat.pred_sub: ∀ (n m : ℕ), pred n - m = pred (n - m)
Nat.pred_sub

-- Moved to Std
#align nat.le_pred_of_lt 
Nat.le_pred_of_lt: ∀ {m n : ℕ}, m < n → m ≤ n - 1
Nat.le_pred_of_lt

theorem 
le_of_pred_lt: ∀ {m n : ℕ}, pred m < n → m ≤ n
le_of_pred_lt {
m: ℕ
m 
n: ℕ
n : 
ℕ: Type
ℕ} : 
pred: ℕ → ℕ
pred 
m: ℕ
m < 
n: ℕ
n → 
m: ℕ
m ≤ 
n: ℕ
n :=
  match 
m: ℕ
m with
  | 
0: ℕ
0 => 
le_of_lt: ∀ {α : Type ?u.9620} [inst : Preorder α] {a b : α}, a < b → a ≤ b
le_of_lt
  | 
_: ℕ
_ + 1 => 
id: ∀ {α : Sort ?u.9749}, α → α
id
#align nat.le_of_pred_lt 
Nat.le_of_pred_lt: ∀ {m n : ℕ}, pred m < n → m ≤ n
Nat.le_of_pred_lt

/-- This ensures that `simp` succeeds on `pred (n + 1) = n`. -/
@[simp]
theorem 
pred_one_add: ∀ (n : ℕ), pred (1 + n) = n
pred_one_add (
n: ℕ
n : 
ℕ: Type
ℕ) : 
pred: ℕ → ℕ
pred (
1: ?m.9843
1 + 
n: ℕ
n) = 
n: ℕ
n := by
Goals accomplished! 🐙 
m, n✝, k, n: ℕ

pred (1 + n) = nrw [
m, n✝, k, n: ℕ

pred (1 + n) = n
add_comm: ∀ {G : Type ?u.9909} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm,
m, n✝, k, n: ℕ

pred (n + 1) = n 
m, n✝, k, n: ℕ

pred (1 + n) = n
add_one: ∀ (n : ℕ), n + 1 = succ n
add_one,
m, n✝, k, n: ℕ

pred (succ n) = n 
m, n✝, k, n: ℕ

pred (1 + n) = n
Nat.pred_succ: ∀ (n : ℕ), pred (succ n) = n
Nat.pred_succ
m, n✝, k, n: ℕ

n = n]
Goals accomplished! 🐙
#align nat.pred_one_add 
Nat.pred_one_add: ∀ (n : ℕ), pred (1 + n) = n
Nat.pred_one_add

/-! ### `mul` -/


theorem 
two_mul_ne_two_mul_add_one: ∀ {n m : ℕ}, 2 * n ≠ 2 * m + 1
two_mul_ne_two_mul_add_one {
n: ?m.9988
n 
m: ?m.9991
m} : 
2: ?m.10000
2 * 
n: ?m.9988
n ≠ 
2: ?m.10033
2 * 
m: ?m.9991
m + 
1: ?m.10043
1 :=
  
mt: ∀ {a b : Prop}, (a → b) → ¬b → ¬a
mt (
congr_arg: ∀ {α : Sort ?u.10389} {β : Sort ?u.10388} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg 
(· % 2): ℕ → ℕ
(· % 2))
    (by
Goals accomplished! 🐙 
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = (2 * m + 1) % 2rw [
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = (2 * m + 1) % 2
add_comm: ∀ {G : Type ?u.10510} [inst : AddCommSemigroup G] (a b : G), a + b = b + a
add_comm,
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = (1 + 2 * m) % 2 
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = (2 * m + 1) % 2
add_mul_mod_self_left: ∀ (x y z : ℕ), (x + y * z) % y = x % y
add_mul_mod_self_left,
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = 1 % 2 
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = (2 * m + 1) % 2
mul_mod_right: ∀ (m n : ℕ), m * n % m = 0
mul_mod_right,
m✝, n✝, k, n, m: ℕ

¬0 = 1 % 2 
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = (2 * m + 1) % 2
mod_eq_of_lt: ∀ {a b : ℕ}, a < b → a % b = a
mod_eq_of_lt
m✝, n✝, k, n, m: ℕ

¬0 = 1
m✝, n✝, k, n, m: ℕ

1 < 2]
m✝, n✝, k, n, m: ℕ

¬0 = 1
m✝, n✝, k, n, m: ℕ

1 < 2 
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = (2 * m + 1) % 2<;>
m✝, n✝, k, n, m: ℕ

¬0 = 1
m✝, n✝, k, n, m: ℕ

1 < 2 
m✝, n✝, k, n, m: ℕ

¬2 * n % 2 = (2 * m + 1) % 2simp
Goals accomplished! 🐙)
#align nat.two_mul_ne_two_mul_add_one 
Nat.two_mul_ne_two_mul_add_one: ∀ {n m : ℕ}, 2 * n ≠ 2 * m + 1
Nat.two_mul_ne_two_mul_add_one

theorem 
mul_ne_mul_left: ∀ {a b c : ℕ}, 0 < a → (b * a ≠ c * a ↔ b ≠ c)
mul_ne_mul_left {
a: ℕ
a 
b: ℕ
b 
c: ℕ
c : 
ℕ: Type
ℕ} (
ha: 0 < a
ha : 
0: ?m.10686
0 < 
a: ℕ
a) : 
b: ℕ
b * 
a: ℕ
a ≠ 
c: ℕ
c * 
a: ℕ
a ↔ 
b: ℕ
b ≠ 
c: ℕ
c :=
  (
mul_left_injective₀: ∀ {M₀ : Type ?u.10803} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : IsRightCancelMulZero M₀] {b : M₀},
  b ≠ 0 → Function.Injective fun a => a * b
mul_left_injective₀ 
ha: 0 < a
ha.
ne': ∀ {α : Type ?u.10809} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne').
ne_iff: ∀ {α : Sort ?u.10931} {β : Sort ?u.10932} {f : α → β}, Function.Injective f → ∀ {x y : α}, f x ≠ f y ↔ x ≠ y
ne_iff
#align nat.mul_ne_mul_left 
Nat.mul_ne_mul_left: ∀ {a b c : ℕ}, 0 < a → (b * a ≠ c * a ↔ b ≠ c)
Nat.mul_ne_mul_left

theorem 
mul_ne_mul_right: ∀ {a b c : ℕ}, 0 < a → (a * b ≠ a * c ↔ b ≠ c)
mul_ne_mul_right {
a: ℕ
a 
b: ℕ
b 
c: ℕ
c : 
ℕ: Type
ℕ} (
ha: 0 < a
ha : 
0: ?m.10978
0 < 
a: ℕ
a) : 
a: ℕ
a * 
b: ℕ
b ≠ 
a: ℕ
a * 
c: ℕ
c ↔ 
b: ℕ
b ≠ 
c: ℕ
c :=
  (
mul_right_injective₀: ∀ {M₀ : Type ?u.11095} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : IsLeftCancelMulZero M₀] {a : M₀},
  a ≠ 0 → Function.Injective ((fun x x_1 => x * x_1) a)
mul_right_injective₀ 
ha: 0 < a
ha.
ne': ∀ {α : Type ?u.11101} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne').
ne_iff: ∀ {α : Sort ?u.11190} {β : Sort ?u.11191} {f : α → β}, Function.Injective f → ∀ {x y : α}, f x ≠ f y ↔ x ≠ y
ne_iff
#align nat.mul_ne_mul_right 
Nat.mul_ne_mul_right: ∀ {a b c : ℕ}, 0 < a → (a * b ≠ a * c ↔ b ≠ c)
Nat.mul_ne_mul_right

theorem 
mul_right_eq_self_iff: ∀ {a b : ℕ}, 0 < a → (a * b = a ↔ b = 1)
mul_right_eq_self_iff {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} (
ha: 0 < a
ha : 
0: ?m.11237
0 < 
a: ℕ
a) : 
a: ℕ
a * 
b: ℕ
b = 
a: ℕ
a ↔ 
b: ℕ
b = 
1: ?m.11322
1 :=
  suffices 
a: ℕ
a * 
b: ℕ
b = 
a: ℕ
a * 
1: ?m.11355
1 ↔ 
b: ℕ
b = 
1: ?m.11421
1 by rwa [
m, n, k, a, b: ℕ

ha: 0 < a

this: a * b = a * 1 ↔ b = 1

a * b = a ↔ b = 1
mul_one: ∀ {M : Type ?u.11510} [inst : MulOneClass M] (a : M), a * 1 = a
mul_one
m, n, k, a, b: ℕ

ha: 0 < a

this: a * b = a ↔ b = 1

a * b = a ↔ b = 1]
m, n, k, a, b: ℕ

ha: 0 < a

this: a * b = a ↔ b = 1

a * b = a ↔ b = 1 at 
this: a * b = a * 1 ↔ b = 1
this
Goals accomplished! 🐙
  
mul_right_inj': ∀ {M₀ : Type ?u.11437} [inst : CancelMonoidWithZero M₀] {a b c : M₀}, a ≠ 0 → (a * b = a * c ↔ b = c)
mul_right_inj' 
ha: 0 < a
ha.
ne': ∀ {α : Type ?u.11474} [inst : Preorder α] {x y : α}, x < y → y ≠ x
ne'
#align nat.mul_right_eq_self_iff 
Nat.mul_right_eq_self_iff: ∀ {a b : ℕ}, 0 < a → (a * b = a ↔ b = 1)
Nat.mul_right_eq_self_iff

theorem 
mul_left_eq_self_iff: ∀ {a b : ℕ}, 0 < b → (a * b = b ↔ a = 1)
mul_left_eq_self_iff {
a: ℕ
a 
b: ℕ
b : 
ℕ: Type
ℕ} (
hb: 0 < b
hb : 
0: ?m.11619
0 < 
b: ℕ
b) : 
a: ℕ
a * 
b: ℕ
b = 
b: ℕ
b ↔ 
a: ℕ
a = 
1: ?m.11704
1 := by
Goals accomplished! 🐙
  
m, n, k, a, b: ℕ

hb: 0 < b

a * b = b ↔ a = 1rw [
m, n, k, a, b: ℕ

hb: 0 < b

a * b = b ↔ a = 1
mul_comm: ∀ {G : Type ?u.11730} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm,
m, n, k, a, b: ℕ

hb: 0 < b

b * a = b ↔ a = 1 
m, n, k, a, b: ℕ

hb: 0 < b

a * b = b ↔ a = 1
Nat.mul_right_eq_self_iff: ∀ {a b : ℕ}, 0 < a → (a * b = a ↔ b = 1)
Nat.mul_right_eq_self_iff 
hb: 0 < b
hb
m, n, k, a, b: ℕ

hb: 0 < b

a = 1 ↔ a = 1]
Goals accomplished! 🐙
#align nat.mul_left_eq_self_iff 
Nat.mul_left_eq_self_iff: ∀ {a b : ℕ}, 0 < b → (a * b = b ↔ a = 1)
Nat.mul_left_eq_self_iff

theorem 
lt_succ_iff_lt_or_eq: ∀ {n i : ℕ}, n < succ i ↔ n < i ∨ n = i
lt_succ_iff_lt_or_eq {
n: ℕ
n 
i: ℕ
i : 
ℕ: Type
ℕ} : 
n: ℕ
n < 
i: ℕ
i.
succ: ℕ → ℕ
succ ↔ 
n: ℕ
n < 
i: ℕ
i ∨ 
n: ℕ
n = 
i: ℕ
i :=
  
lt_succ_iff: ∀ {m n : ℕ}, m < succ n ↔ m ≤ n
lt_succ_iff.
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans 
Decidable.le_iff_lt_or_eq: ∀ {α : Type ?u.11834} [inst : PartialOrder α] [inst_1 : DecidableRel fun x x_1 => x ≤ x_1] {a b : α},
  a ≤ b ↔ a < b ∨ a = b
Decidable.le_iff_lt_or_eq
#align nat.lt_succ_iff_lt_or_eq 
Nat.lt_succ_iff_lt_or_eq: ∀ {n i : ℕ}, n < succ i ↔ n < i ∨ n = i
Nat.lt_succ_iff_lt_or_eq

/-!
### Recursion and induction principles

This section is here due to dependencies -- the lemmas here require some of the lemmas
proved above, and some of the results in later sections depend on the definitions in this section.
-/

-- Porting note: The type ascriptions of these two theorems need to be changed,
-- as mathport wrote a lambda that wasn't there in mathlib3, that prevents `simp` applying them.

@[simp]
theorem 
rec_zero: ∀ {C : ℕ → Sort u} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)), rec h0 h 0 = h0
rec_zero {
C: ℕ → Sort u
C : 
ℕ: Type
ℕ → 
Sort u: Type u
Sort
Sort u: Type u
 u} (
h0: C 0
h0 : 
C: ℕ → Sort u
C 
0: ?m.11942
0) (
h: (n : ℕ) → C n → C (n + 1)
h : ∀ 
n: ?m.11955
n, 
C: ℕ → Sort u
C 
n: ?m.11955
n → 
C: ℕ → Sort u
C (
n: ?m.11955
n + 
1: ?m.11964
1)) :
    
Nat.rec: {motive : ℕ → Sort ?u.12061} → motive zero → ((n : ℕ) → motive n → motive (succ n)) → (t : ℕ) → motive t
Nat.rec 
h0: C 0
h0 
h: (n : ℕ) → C n → C (n + 1)
h 
0: ?m.12081
0 = 
h0: C 0
h0 :=
  
rfl: ∀ {α : Sort ?u.12119} {a : α}, a = a
rfl
#align nat.rec_zero 
Nat.rec_zero: ∀ {C : ℕ → Sort u} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)), rec h0 h 0 = h0
Nat.rec_zero

@[simp]
theorem 
rec_add_one: ∀ {C : ℕ → Sort u} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) (n : ℕ), rec h0 h (n + 1) = h n (rec h0 h n)
rec_add_one {
C: ℕ → Sort u
C : 
ℕ: Type
ℕ → 
Sort u: Type u
Sort
Sort u: Type u
 u} (
h0: C 0
h0 : 
C: ℕ → Sort u
C 
0: ?m.12160
0) (
h: (n : ℕ) → C n → C (n + 1)
h : ∀ 
n: ?m.12173
n, 
C: ℕ → Sort u
C 
n: ?m.12173
n → 
C: ℕ → Sort u
C (
n: ?m.12173
n + 
1: ?m.12182
1)) (
n: ℕ
n : 
ℕ: Type
ℕ) :
    
Nat.rec: {motive : ℕ → Sort ?u.12340} → motive zero → ((n : ℕ) → motive n → motive (succ n)) → (t : ℕ) → motive t
Nat.rec 
h0: C 0
h0 
h: (n : ℕ) → C n → C (n + 1)
h (
n: ℕ
n + 
1: ?m.12363
1) = 
h: (n : ℕ) → C n → C (n + 1)
h 
n: ℕ
n (
Nat.rec: {motive : ℕ → Sort ?u.12267} → motive zero → ((n : ℕ) → motive n → motive (succ n)) → (t : ℕ) → motive t
Nat.rec 
h0: C 0
h0 
h: (n : ℕ) → C n → C (n + 1)
h 
n: ℕ
n) :=
  
rfl: ∀ {α : Sort ?u.12429} {a : α}, a = a
rfl
#align nat.rec_add_one 
Nat.rec_add_one: ∀ {C : ℕ → Sort u} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) (n : ℕ), rec h0 h (n + 1) = h n (rec h0 h n)
Nat.rec_add_one

/-- Recursion starting at a non-zero number: given a map `C k → C (k+1)` for each `k`,
there is a map from `C n` to each `C m`, `n ≤ m`. For a version where the assumption is only made
when `k ≥ n`, see `leRecOn`. -/
@[elab_as_elim]
def 
leRecOn: {C : ℕ → Sort u} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn {
C: ℕ → Sort u
C : 
ℕ: Type
ℕ → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
n: ℕ
n : 
ℕ: Type
ℕ} : ∀ {
m: ℕ
m : 
ℕ: Type
ℕ}, 
n: ℕ
n ≤ 
m: ℕ
m → (∀ {
k: ?m.12508
k}, 
C: ℕ → Sort u
C 
k: ?m.12508
k → 
C: ℕ → Sort u
C (
k: ?m.12508
k + 
1: ?m.12517
1)) → 
C: ℕ → Sort u
C 
n: ℕ
n → 
C: ℕ → Sort u
C 
m: ℕ
m
  | 
0: ℕ
0, 
H: n ≤ 0
H, _, 
x: C n
x => 
Eq.recOn: {α : Sort ?u.12643} →
  {a : α} →
    {motive : (a_1 : α) → a = a_1 → Sort ?u.12644} → {a_1 : α} → (t : a = a_1) → motive a (_ : a = a) → motive a_1 t
Eq.recOn (
Nat.eq_zero_of_le_zero: ∀ {n : ℕ}, n ≤ 0 → n = 0
Nat.eq_zero_of_le_zero 
H: n ≤ 0
H) 
x: C n
x
  | 
m: ℕ
m + 1, 
H: n ≤ m + 1
H, 
next: {k : ℕ} → C k → C (k + 1)
next, 
x: C n
x =>
    
Or.by_cases: {p q : Prop} → [inst : Decidable p] → {α : Sort ?u.12773} → p ∨ q → (p → α) → (q → α) → α
Or.by_cases (
of_le_succ: ∀ {n m : ℕ}, n ≤ succ m → n ≤ m ∨ n = succ m
of_le_succ 
H: n ≤ m + 1
H) (fun 
h: n ≤ m
h : 
n: ℕ
n ≤ 
m: ℕ
m => 
next: {k : ℕ} → C k → C (k + 1)
next <| 
leRecOn: {C : ℕ → Sort u} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn 
h: n ≤ m
h (@
next: {k : ℕ} → C k → C (k + 1)
next) 
x: C n
x)
      fun 
h: n = m + 1
h : 
n: ℕ
n = 
m: ℕ
m + 
1: ?m.12884
1 => 
Eq.recOn: {α : Sort ?u.12922} →
  {a : α} →
    {motive : (a_1 : α) → a = a_1 → Sort ?u.12923} → {a_1 : α} → (t : a = a_1) → motive a (_ : a = a) → motive a_1 t
Eq.recOn 
h: n = m + 1
h 
x: C n
x
#align nat.le_rec_on 
Nat.leRecOn: {C : ℕ → Sort u} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
Nat.leRecOn

theorem 
leRecOn_self: ∀ {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n} {next : {k : ℕ} → C k → C (k + 1)} (x : C n), leRecOn h (fun {k} => next) x = x
leRecOn_self {
C: ℕ → Sort u
C : 
ℕ: Type
ℕ → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
n: ?m.13782
n} {
h: n ≤ n
h : 
n: ?m.13782
n ≤ 
n: ?m.13782
n} {
next: {k : ℕ} → C k → C (k + 1)
next : ∀ {
k: ?m.13826
k}, 
C: ℕ → Sort u
C 
k: ?m.13826
k → 
C: ℕ → Sort u
C (
k: ?m.13826
k + 
1: ?m.13835
1)} (
x: C n
x : 
C: ℕ → Sort u
C 
n: ?m.13782
n) :
    (
leRecOn: {C : ℕ → Sort ?u.13905} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn 
h: n ≤ n
h 
next: {k : ℕ} → C k → C (k + 1)
next 
x: C n
x : 
C: ℕ → Sort u
C 
n: ?m.13782
n) = 
x: C n
x := by
Goals accomplished! 🐙
  
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h (fun {k} => next) x = xcases 
n: ℕ
n
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

h: zero ≤ zero

x: C zero

zero
leRecOn h (fun {k} => next) x = x
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
leRecOn h (fun {k} => next) x = x 
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h (fun {k} => next) x = x<;>
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

h: zero ≤ zero

x: C zero

zero
leRecOn h (fun {k} => next) x = x
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
leRecOn h (fun {k} => next) x = x 
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h (fun {k} => next) x = xunfold 
leRecOn: {C : ℕ → Sort u} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn 
Eq.recOn: {α : Sort u_1} →
  {a : α} → {motive : (a_1 : α) → a = a_1 → Sort u} → {a_1 : α} → (t : a = a_1) → motive a (_ : a = a) → motive a_1 t
Eq.recOn
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
(Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
    fun h => h ▸ x) =   x
  
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h (fun {k} => next) x = x·
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

h: zero ≤ zero

x: C zero

zero
(_ : zero = 0) ▸ x = x 
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

h: zero ≤ zero

x: C zero

zero
(_ : zero = 0) ▸ x = x
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
(Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
    fun h => h ▸ x) =   xsimp
Goals accomplished! 🐙
  
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h (fun {k} => next) x = x·
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
(Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
    fun h => h ▸ x) =   x 
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
(Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
    fun h => h ▸ x) =   xunfold 
Or.by_cases: {p q : Prop} → [inst : Decidable p] → {α : Sort u} → p ∨ q → (p → α) → (q → α) → α
Or.by_cases
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
(if hp : succ n✝ ≤ n✝ then (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) hp
  else (fun h => h ▸ x) (_ : succ n✝ = succ n✝)) =   x
    
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
(Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
    fun h => h ▸ x) =   xrw [
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
(if hp : succ n✝ ≤ n✝ then (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) hp
  else (fun h => h ▸ x) (_ : succ n✝ = succ n✝)) =   x
dif_neg: ∀ {c : Prop} {h : Decidable c} (hnc : ¬c) {α : Sort ?u.15860} {t : c → α} {e : ¬c → α}, dite c t e = e hnc
dif_neg (
Nat.not_succ_le_self: ∀ (n : ℕ), ¬succ n ≤ n
Nat.not_succ_le_self 
_: ℕ
_)
m, n, k: ℕ

C: ℕ → Sort u

next: {k : ℕ} → C k → C (k + 1)

n✝: ℕ

h: succ n✝ ≤ succ n✝

x: C (succ n✝)

succ
(fun h => h ▸ x) (_ : succ n✝ = succ n✝) = x]
Goals accomplished! 🐙
#align nat.le_rec_on_self 
Nat.leRecOn_self: ∀ {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n} {next : {k : ℕ} → C k → C (k + 1)} (x : C n), leRecOn h (fun {k} => next) x = x
Nat.leRecOn_self

theorem 
leRecOn_succ: ∀ {C : ℕ → Sort u} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  leRecOn h2 next x = next (leRecOn h1 next x)
leRecOn_succ {
C: ℕ → Sort u
C : 
ℕ: Type
ℕ → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
n: ?m.15988
n 
m: ℕ
m} (
h1: n ≤ m
h1 : 
n: ?m.15988
n ≤ 
m: ?m.15991
m) {
h2: n ≤ m + 1
h2 : 
n: ?m.15988
n ≤ 
m: ?m.15991
m + 
1: ?m.16039
1} {
next: ?m.16117
next} (
x: C n
x : 
C: ℕ → Sort u
C 
n: ?m.15988
n) :
    (
leRecOn: {C : ℕ → Sort ?u.16188} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn 
h2: n ≤ m + 1
h2 (@
next: ?m.16117
next) 
x: C n
x : 
C: ℕ → Sort u
C (
m: ?m.15991
m + 
1: ?m.16128
1)) = 
next: ?m.16117
next (
leRecOn: {C : ℕ → Sort ?u.16236} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn 
h1: n ≤ m
h1 (@
next: ?m.16117
next) 
x: C n
x : 
C: ℕ → Sort u
C 
m: ?m.15991
m) := by
Goals accomplished! 🐙
  
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h2 next x = next (leRecOn h1 next x)conv =>
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

next (leRecOn h1 next x)
    
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h2 next x = next (leRecOn h1 next x)lhs
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h2 next x
    
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h2 next x = next (leRecOn h1 next x)rw [
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h2 next x
leRecOn: {C : ℕ → Sort ?u.16353} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn,
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

Or.by_cases (_ : n ≤ m ∨ n = succ m) (fun h => next (leRecOn h next x)) fun h => Eq.recOn h x 
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h2 next x
Or.by_cases: {p q : Prop} → [inst : Decidable p] → {α : Sort ?u.16582} → p ∨ q → (p → α) → (q → α) → α
Or.by_cases,
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

if hp : n ≤ m then next (leRecOn hp next x) else Eq.recOn (_ : n = succ m) x 
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h2 next x
dif_pos: ∀ {c : Prop} {h : Decidable c} (hc : c) {α : Sort ?u.16583} {t : c → α} {e : ¬c → α}, dite c t e = t hc
dif_pos 
h1: n ≤ m
h1
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

next (leRecOn h1 next x)]
m✝, n✝, k: ℕ

C: ℕ → Sort u

n, m: ℕ

h1: n ≤ m

h2: n ≤ m + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

next (leRecOn h1 next x)
#align nat.le_rec_on_succ 
Nat.leRecOn_succ: ∀ {C : ℕ → Sort u} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  leRecOn h2 next x = next (leRecOn h1 next x)
Nat.leRecOn_succ

theorem 
leRecOn_succ': ∀ {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  leRecOn h (fun {k} => next) x = next x
leRecOn_succ' {
C: ℕ → Sort u
C : 
ℕ: Type
ℕ → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
n: ?m.16660
n} {
h: n ≤ n + 1
h : 
n: ?m.16660
n ≤ 
n: ?m.16660
n + 
1: ?m.16668
1} {
next: {k : ℕ} → C k → C (k + 1)
next : ∀ {
k: ?m.16747
k}, 
C: ℕ → Sort u
C 
k: ?m.16747
k → 
C: ℕ → Sort u
C (
k: ?m.16747
k + 
1: ?m.16756
1)}
    (
x: C n
x : 
C: ℕ → Sort u
C 
n: ?m.16660
n) :
    (
leRecOn: {C : ℕ → Sort ?u.16882} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn 
h: n ≤ n + 1
h 
next: {k : ℕ} → C k → C (k + 1)
next 
x: C n
x : 
C: ℕ → Sort u
C (
n: ?m.16660
n + 
1: ?m.16838
1)) = 
next: {k : ℕ} → C k → C (k + 1)
next 
x: C n
x := by
Goals accomplished! 🐙 
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h (fun {k} => next) x = next xrw [
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h (fun {k} => next) x = next x
leRecOn_succ: ∀ {C : ℕ → Sort ?u.16957} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  leRecOn h2 next x = next (leRecOn h1 next x)
leRecOn_succ (
le_refl: ∀ {α : Type ?u.16961} [inst : Preorder α] (a : α), a ≤ a
le_refl 
n: ℕ
n),
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

next (leRecOn (_ : n ≤ n) (fun {k} => next) x) = next x 
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn h (fun {k} => next) x = next x
leRecOn_self: ∀ {C : ℕ → Sort ?u.17001} {n : ℕ} {h : n ≤ n} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  leRecOn h (fun {k} => next) x = x
leRecOn_self
m, n✝, k: ℕ

C: ℕ → Sort u

n: ℕ

h: n ≤ n + 1

next: {k : ℕ} → C k → C (k + 1)

x: C n

next x = next x]
Goals accomplished! 🐙
#align nat.le_rec_on_succ' 
Nat.leRecOn_succ': ∀ {C : ℕ → Sort u} {n : ℕ} {h : n ≤ n + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  leRecOn h (fun {k} => next) x = next x
Nat.leRecOn_succ'

theorem 
leRecOn_trans: ∀ {C : ℕ → Sort u} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)
leRecOn_trans {
C: ℕ → Sort u
C : 
ℕ: Type
ℕ → 
Sort u: Type u
Sort
Sort u: Type u
 u} {
n: ?m.17052
n 
m: ?m.17055
m 
k: ℕ
k} (
hnm: n ≤ m
hnm : 
n: ?m.17052
n ≤ 
m: ?m.17055
m) (
hmk: m ≤ k
hmk : 
m: ?m.17055
m ≤ 
k: ?m.17058
k) {
next: ?m.17141
next} (
x: C n
x : 
C: ℕ → Sort u
C 
n: ?m.17052
n) :
    (
leRecOn: {C : ℕ → Sort ?u.17148} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn (
le_trans: ∀ {α : Type ?u.17173} [inst : Preorder α] {a b c : α}, a ≤ b → b ≤ c → a ≤ c
le_trans 
hnm: n ≤ m
hnm 
hmk: m ≤ k
hmk) (@
next: ?m.17141
next) 
x: C n
x : 
C: ℕ → Sort u
C 
k: ?m.17058
k) = 
leRecOn: {C : ℕ → Sort ?u.17251} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn 
hmk: m ≤ k
hmk (@
next: ?m.17141
next) (
leRecOn: {C : ℕ → Sort ?u.17280} → {n m : ℕ} → n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C m
leRecOn 
hnm: n ≤ m
hnm (@
next: ?m.17141
next) 
x: C n
x) := by
Goals accomplished! 🐙
  
m✝, n✝, k✝: ℕ

C: ℕ → Sort u

n, m, k: ℕ

hnm: n ≤ m

hmk: m ≤ k

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)induction' 
hmk: m ≤ k
hmk with 
k: ℕ
k 
hmk: Nat.le ?m.17340 k
hmk 
ih: ?m.17341 k hmk
ih
m✝, n✝, k✝: ℕ

C: ℕ → Sort u

n, m, k: ℕ

hnm: n ≤ m

next: {k : ℕ} → C k → C (k + 1)

x: C n

refl
leRecOn (_ : n ≤ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
m✝, n✝, k✝¹: ℕ

C: ℕ → Sort u

n, m, k✝: ℕ

hnm: n ≤ m

next: {k : ℕ} → C k → C (k + 1)

x: C n

k: ℕ

hmk: Nat.le m k

ih: leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)

step
leRecOn (_ : n ≤ succ k) next x = leRecOn (_ : Nat.le m (succ k)) next (leRecOn hnm next x)
  
m✝, n✝, k✝: ℕ

C: ℕ → Sort u

n, m, k: ℕ

hnm: n ≤ m

hmk: m ≤ k

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)·
m✝, n✝, k✝: ℕ

C: ℕ → Sort u

n, m, k: ℕ

hnm: n ≤ m

next: {k : ℕ} → C k → C (k + 1)

x: C n

refl
leRecOn (_ : n ≤ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x) 
m✝, n✝, k✝: ℕ

C: ℕ → Sort u

n, m, k: ℕ

hnm: n ≤ m

next: {k : ℕ} → C k → C (k + 1)

x: C n

refl
leRecOn (_ : n ≤ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
m✝, n✝, k✝¹: ℕ

C: ℕ → Sort u

n, m, k✝: ℕ

hnm: n ≤ m

next: {k : ℕ} → C k → C (k + 1)

x: C n

k: ℕ

hmk: Nat.le m k

ih: leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)

step
leRecOn (_ : n ≤ succ k) next x = leRecOn (_ : Nat.le m (succ k)) next (leRecOn hnm next x)rw [
m✝, n✝, k✝: ℕ

C: ℕ → Sort u

n, m, k: ℕ

hnm: n ≤ m

next: {k : ℕ} → C k → C (k + 1)

x: C n

refl
leRecOn (_ : n ≤ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
leRecOn_self: ∀ {C : ℕ → Sort ?u.17355} {n : ℕ} {h : n ≤ n} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  leRecOn h (fun {k} => next) x = x
leRecOn_self
m✝, n✝, k✝: ℕ

C: ℕ → Sort u

n, m, k: ℕ

hnm: n ≤ m

next: {k : ℕ} → C k → C (k + 1)

x: C n

refl
leRecOn (_ : n ≤ m) next x = leRecOn hnm next x]
Goals accomplished! 🐙

  
m✝, n✝, k✝: ℕ

C: ℕ → Sort u

n, m, k: ℕ

hnm: n ≤ m

hmk: m ≤ k

next: {k : ℕ} → C k → C (k + 1)

x: C n

leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)rw [
m✝, n✝, k✝¹: ℕ

C: ℕ → Sort u

n, m, k✝: ℕ

hnm: n