[GOAL]
m n k l : ℕ
⊢ 1 < 0 ↔ 0 ≠ 0 ∧ 0 ≠ 1
[PROOFSTEP]
decide
[GOAL]
m n k l : ℕ
⊢ 1 < 1 ↔ 1 ≠ 0 ∧ 1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
m n✝ k l n : ℕ
⊢ 1 < n + 2 ↔ n + 2 ≠ 0 ∧ n + 2 ≠ 1
[PROOFSTEP]
simp
[GOAL]
m n k l : ℕ
⊢ 0 = m * n ↔ m = 0 ∨ n = 0
[PROOFSTEP]
rw [eq_comm, Nat.mul_eq_zero]
[GOAL]
m n k l : ℕ
⊢ m + n = max m n ↔ m = 0 ∨ n = 0
[PROOFSTEP]
rw [← min_eq_zero_iff]
[GOAL]
m n k l : ℕ
⊢ m + n = max m n ↔ min m n = 0
[PROOFSTEP]
cases' le_total m n with H H
[GOAL]
case inl
m n k l : ℕ
H : m ≤ n
⊢ m + n = max m n ↔ min m n = 0
[PROOFSTEP]
simp [H]
[GOAL]
case inr
m n k l : ℕ
H : n ≤ m
⊢ m + n = max m n ↔ min m n = 0
[PROOFSTEP]
simp [H]
[GOAL]
m n k l : ℕ
⊢ m + n = min m n ↔ m = 0 ∧ n = 0
[PROOFSTEP]
rw [← max_eq_zero_iff]
[GOAL]
m n k l : ℕ
⊢ m + n = min m n ↔ max m n = 0
[PROOFSTEP]
cases' le_total m n with H H
[GOAL]
case inl
m n k l : ℕ
H : m ≤ n
⊢ m + n = min m n ↔ max m n = 0
[PROOFSTEP]
simp [H]
[GOAL]
case inr
m n k l : ℕ
H : n ≤ m
⊢ m + n = min m n ↔ max m n = 0
[PROOFSTEP]
simp [H]
[GOAL]
m n k l : ℕ
H : m * n = 1
⊢ n * ?m.12220 H = 1
[PROOFSTEP]
rwa [mul_comm]
[GOAL]
m n k l : ℕ
⊢ 2 ≤ 0 ↔ 0 ≠ 0 ∧ 0 ≠ 1
[PROOFSTEP]
simp
[GOAL]
m n k l : ℕ
⊢ 2 ≤ 1 ↔ 1 ≠ 0 ∧ 1 ≠ 1
[PROOFSTEP]
simp
[GOAL]
m n✝ k l n : ℕ
⊢ 2 ≤ n + 2 ↔ n + 2 ≠ 0 ∧ n + 2 ≠ 1
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ k l m n : ℕ
⊢ 0 < m + n → 0 < m ∨ 0 < n
[PROOFSTEP]
intro h
[GOAL]
m✝ n✝ k l m n : ℕ
h : 0 < m + n
⊢ 0 < m ∨ 0 < n
[PROOFSTEP]
cases' m with m
[GOAL]
case zero
m n✝ k l n : ℕ
h : 0 < zero + n
⊢ 0 < zero ∨ 0 < n
[PROOFSTEP]
simp [zero_add] at h 
[GOAL]
case zero
m n✝ k l n : ℕ
h : 0 < n
⊢ 0 < zero ∨ 0 < n
[PROOFSTEP]
exact Or.inr h
[GOAL]
case succ
m✝ n✝ k l n m : ℕ
h : 0 < succ m + n
⊢ 0 < succ m ∨ 0 < n
[PROOFSTEP]
exact Or.inl (succ_pos _)
[GOAL]
m✝ n✝ k l m n : ℕ
⊢ 0 < m ∨ 0 < n → 0 < m + n
[PROOFSTEP]
intro h
[GOAL]
m✝ n✝ k l m n : ℕ
h : 0 < m ∨ 0 < n
⊢ 0 < m + n
[PROOFSTEP]
cases' h with mpos npos
[GOAL]
case inl
m✝ n✝ k l m n : ℕ
mpos : 0 < m
⊢ 0 < m + n
[PROOFSTEP]
apply add_pos_left mpos
[GOAL]
case inr
m✝ n✝ k l m n : ℕ
npos : 0 < n
⊢ 0 < m + n
[PROOFSTEP]
apply add_pos_right _ npos
[GOAL]
m n k l : ℕ
⊢ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
m k l : ℕ
⊢ m + zero = 1 ↔ m = 0 ∧ zero = 1 ∨ m = 1 ∧ zero = 0
[PROOFSTEP]
simp [succ_eq_add_one, ← add_assoc, succ_inj']
[GOAL]
case succ
m k l n✝ : ℕ
⊢ m + succ n✝ = 1 ↔ m = 0 ∧ succ n✝ = 1 ∨ m = 1 ∧ succ n✝ = 0
[PROOFSTEP]
simp [succ_eq_add_one, ← add_assoc, succ_inj']
[GOAL]
m n k l : ℕ
⊢ m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
m k l : ℕ
⊢ m + zero = 2 ↔ m = 0 ∧ zero = 2 ∨ m = 1 ∧ zero = 1 ∨ m = 2 ∧ zero = 0
[PROOFSTEP]
simp [(succ_ne_zero 1).symm, (show 2 = Nat.succ 1 from rfl), succ_eq_add_one, ← add_assoc, succ_inj', add_eq_one_iff]
[GOAL]
case succ
m k l n✝ : ℕ
⊢ m + succ n✝ = 2 ↔ m = 0 ∧ succ n✝ = 2 ∨ m = 1 ∧ succ n✝ = 1 ∨ m = 2 ∧ succ n✝ = 0
[PROOFSTEP]
simp [(succ_ne_zero 1).symm, (show 2 = Nat.succ 1 from rfl), succ_eq_add_one, ← add_assoc, succ_inj', add_eq_one_iff]
[GOAL]
m n k l : ℕ
⊢ m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
m k l : ℕ
⊢ m + zero = 3 ↔ m = 0 ∧ zero = 3 ∨ m = 1 ∧ zero = 2 ∨ m = 2 ∧ zero = 1 ∨ m = 3 ∧ zero = 0
[PROOFSTEP]
simp [(succ_ne_zero 1).symm, succ_eq_add_one, (show 3 = Nat.succ 2 from rfl), ← add_assoc, succ_inj', add_eq_two_iff]
[GOAL]
case succ
m k l n✝ : ℕ
⊢ m + succ n✝ = 3 ↔ m = 0 ∧ succ n✝ = 3 ∨ m = 1 ∧ succ n✝ = 2 ∨ m = 2 ∧ succ n✝ = 1 ∨ m = 3 ∧ succ n✝ = 0
[PROOFSTEP]
simp [(succ_ne_zero 1).symm, succ_eq_add_one, (show 3 = Nat.succ 2 from rfl), ← add_assoc, succ_inj', add_eq_two_iff]
[GOAL]
m n k l : ℕ
⊢ n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1
[PROOFSTEP]
rw [le_add_one_iff, and_or_left, ← le_antisymm_iff, eq_comm, and_iff_right_of_imp]
[GOAL]
m n k l : ℕ
⊢ m = n + 1 → n ≤ m
[PROOFSTEP]
rintro rfl
[GOAL]
n k l : ℕ
⊢ n ≤ n + 1
[PROOFSTEP]
exact n.le_succ
[GOAL]
m n k l : ℕ
hab : m < n
hcd : k < l
⊢ m + k + 1 < n + l
[PROOFSTEP]
rw [add_assoc]
[GOAL]
m n k l : ℕ
hab : m < n
hcd : k < l
⊢ m + (k + 1) < n + l
[PROOFSTEP]
exact add_lt_add_of_lt_of_le hab (Nat.succ_le_iff.2 hcd)
[GOAL]
m n k l : ℕ
⊢ m ≤ succ n → pred m ≤ n
[PROOFSTEP]
cases m
[GOAL]
case zero
n k l : ℕ
⊢ zero ≤ succ n → pred zero ≤ n
[PROOFSTEP]
exact fun _ => zero_le n
[GOAL]
case succ
n k l n✝ : ℕ
⊢ succ n✝ ≤ succ n → pred (succ n✝) ≤ n
[PROOFSTEP]
exact le_of_succ_le_succ
[GOAL]
m n k l : ℕ
⊢ OrderedSub ℕ
[PROOFSTEP]
constructor
[GOAL]
case tsub_le_iff_right
m n k l : ℕ
⊢ ∀ (a b c : ℕ), a - b ≤ c ↔ a ≤ c + b
[PROOFSTEP]
intro m n k
[GOAL]
case tsub_le_iff_right
m✝ n✝ k✝ l m n k : ℕ
⊢ m - n ≤ k ↔ m ≤ k + n
[PROOFSTEP]
induction' n with n ih generalizing k
[GOAL]
case tsub_le_iff_right.zero
m✝ n k✝¹ l m k✝ k : ℕ
⊢ m - zero ≤ k ↔ m ≤ k + zero
[PROOFSTEP]
simp
[GOAL]
case tsub_le_iff_right.succ
m✝ n✝ k✝¹ l m k✝ n : ℕ
ih : ∀ (k : ℕ), m - n ≤ k ↔ m ≤ k + n
k : ℕ
⊢ m - succ n ≤ k ↔ m ≤ k + succ n
[PROOFSTEP]
simp only [sub_succ, pred_le_iff, ih, succ_add, add_succ]
[GOAL]
m n k l : ℕ
h : k + l = m + n - 1
⊢ m ≤ k ∨ n ≤ l
[PROOFSTEP]
cases' le_or_lt m k with h' h' <;> [left; right]
[GOAL]
m n k l : ℕ
h : k + l = m + n - 1
⊢ m ≤ k ∨ n ≤ l
[PROOFSTEP]
cases' le_or_lt m k with h' h'
[GOAL]
case inl
m n k l : ℕ
h : k + l = m + n - 1
h' : m ≤ k
⊢ m ≤ k ∨ n ≤ l
[PROOFSTEP]
left
[GOAL]
case inr
m n k l : ℕ
h : k + l = m + n - 1
h' : k < m
⊢ m ≤ k ∨ n ≤ l
[PROOFSTEP]
right
[GOAL]
case inl.h
m n k l : ℕ
h : k + l = m + n - 1
h' : m ≤ k
⊢ m ≤ k
[PROOFSTEP]
exact h'
[GOAL]
case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : k < m
⊢ n ≤ l
[PROOFSTEP]
replace h' := add_lt_add_right h' l
[GOAL]
case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : k + l < m + l
⊢ n ≤ l
[PROOFSTEP]
rw [h] at h' 
[GOAL]
case inr.h
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
⊢ n ≤ l
[PROOFSTEP]
cases' n.eq_zero_or_pos with hn hn
[GOAL]
case inr.h.inl
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n = 0
⊢ n ≤ l
[PROOFSTEP]
rw [hn]
[GOAL]
case inr.h.inl
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n = 0
⊢ 0 ≤ l
[PROOFSTEP]
exact zero_le l
[GOAL]
case inr.h.inr
m n k l : ℕ
h : k + l = m + n - 1
h' : m + n - 1 < m + l
hn : n > 0
⊢ n ≤ l
[PROOFSTEP]
rw [n.add_sub_assoc (Nat.succ_le_of_lt hn), add_lt_add_iff_left] at h' 
[GOAL]
case inr.h.inr
m n k l : ℕ
h : k + l = m + n - 1
h' : n - succ 0 < l
hn : n > 0
⊢ n ≤ l
[PROOFSTEP]
exact Nat.le_of_pred_lt h'
[GOAL]
m n✝ k l n : ℕ
⊢ n + 1 ≤ (n + 1) * (n + 1)
[PROOFSTEP]
simp
[GOAL]
m n k l : ℕ
h : 0 < n
⊢ m ≤ n * m
[PROOFSTEP]
conv =>
  lhs
  rw [← one_mul m]
[GOAL]
m n k l : ℕ
h : 0 < n
| m ≤ n * m
[PROOFSTEP]
  lhs
  rw [← one_mul m]
[GOAL]
m n k l : ℕ
h : 0 < n
| m ≤ n * m
[PROOFSTEP]
  lhs
  rw [← one_mul m]
[GOAL]
m n k l : ℕ
h : 0 < n
| m ≤ n * m
[PROOFSTEP]
lhs
[GOAL]
m n k l : ℕ
h : 0 < n
| m
[PROOFSTEP]
rw [← one_mul m]
[GOAL]
m n k l : ℕ
h : 0 < n
⊢ 1 * m ≤ n * m
[PROOFSTEP]
exact mul_le_mul_of_nonneg_right h.nat_succ_le (zero_le _)
[GOAL]
m n k l : ℕ
h : 0 < n
⊢ m ≤ m * n
[PROOFSTEP]
conv =>
  lhs
  rw [← mul_one m]
[GOAL]
m n k l : ℕ
h : 0 < n
| m ≤ m * n
[PROOFSTEP]
  lhs
  rw [← mul_one m]
[GOAL]
m n k l : ℕ
h : 0 < n
| m ≤ m * n
[PROOFSTEP]
  lhs
  rw [← mul_one m]
[GOAL]
m n k l : ℕ
h : 0 < n
| m ≤ m * n
[PROOFSTEP]
lhs
[GOAL]
m n k l : ℕ
h : 0 < n
| m
[PROOFSTEP]
rw [← mul_one m]
[GOAL]
m n k l : ℕ
h : 0 < n
⊢ m * 1 ≤ m * n
[PROOFSTEP]
exact mul_le_mul_of_nonneg_left h.nat_succ_le (zero_le _)
[GOAL]
m n✝ k l n i : ℕ
hi : i ≠ 0
⊢ n ≤ i + (n - 1)
[PROOFSTEP]
refine le_trans ?_ add_tsub_le_assoc
[GOAL]
m n✝ k l n i : ℕ
hi : i ≠ 0
⊢ n ≤ i + n - 1
[PROOFSTEP]
simp [add_comm, Nat.add_sub_assoc, one_le_iff_ne_zero.2 hi]
[GOAL]
m n k l : ℕ
hm : m ≠ 0
hn : n ≠ 0
⊢ m + n - 1 ≤ m * n
[PROOFSTEP]
cases m
[GOAL]
case zero
n k l : ℕ
hn : n ≠ 0
hm : zero ≠ 0
⊢ zero + n - 1 ≤ zero * n
[PROOFSTEP]
cases hm rfl
[GOAL]
case succ
n k l : ℕ
hn : n ≠ 0
n✝ : ℕ
hm : succ n✝ ≠ 0
⊢ succ n✝ + n - 1 ≤ succ n✝ * n
[PROOFSTEP]
rw [succ_add, succ_sub_one, succ_mul]
[GOAL]
case succ
n k l : ℕ
hn : n ≠ 0
n✝ : ℕ
hm : succ n✝ ≠ 0
⊢ n✝ + n ≤ n✝ * n + n
[PROOFSTEP]
exact add_le_add_right (le_mul_of_one_le_right' $ succ_le_iff.2 $ pos_iff_ne_zero.2 hn) _
[GOAL]
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) (b + 1)
[PROOFSTEP]
apply hd _ _ ((add_lt_add_iff_right _).1 h)
[GOAL]
case a
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P (a + 1) b
[PROOFSTEP]
have this : a + 1 = b ∨ a + 1 < b := by rwa [← le_iff_eq_or_lt, ← Nat.lt_succ_iff]
[GOAL]
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ a + 1 = b ∨ a + 1 < b
[PROOFSTEP]
rwa [← le_iff_eq_or_lt, ← Nat.lt_succ_iff]
[GOAL]
case a
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
this : a + 1 = b ∨ a + 1 < b
⊢ P (a + 1) b
[PROOFSTEP]
have wf : (a + 1) + b < (a + 1) + (b + 1) := by simp
[GOAL]
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
this : a + 1 = b ∨ a + 1 < b
⊢ a + 1 + b < a + 1 + (b + 1)
[PROOFSTEP]
simp
[GOAL]
case a
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
this : a + 1 = b ∨ a + 1 < b
wf : a + 1 + b < a + 1 + (b + 1)
⊢ P (a + 1) b
[PROOFSTEP]
rcases this with (rfl | h)
[GOAL]
case a.inl
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a : ℕ
h : a + 1 < a + 1 + 1
wf : a + 1 + (a + 1) < a + 1 + (a + 1 + 1)
⊢ P (a + 1) (a + 1)
[PROOFSTEP]
exact ha _
[GOAL]
case a.inr
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h✝ : a + 1 < b + 1
wf : a + 1 + b < a + 1 + (b + 1)
h : a + 1 < b
⊢ P (a + 1) b
[PROOFSTEP]
apply diag_induction P ha hb hd (a + 1) b h
[GOAL]
case a
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ P a (b + 1)
[PROOFSTEP]
have _ : a + (b + 1) < (a + 1) + (b + 1) := by simp
[GOAL]
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
⊢ a + (b + 1) < a + 1 + (b + 1)
[PROOFSTEP]
simp
[GOAL]
case a
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
x✝ : a + (b + 1) < a + 1 + (b + 1)
⊢ P a (b + 1)
[PROOFSTEP]
apply diag_induction P ha hb hd a (b + 1)
[GOAL]
case a
m n k l : ℕ
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
a b : ℕ
h : a + 1 < b + 1
x✝ : a + (b + 1) < a + 1 + (b + 1)
⊢ a < b + 1
[PROOFSTEP]
apply lt_of_le_of_lt (Nat.le_succ _) h
[GOAL]
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
_x✝ : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1
a✝² :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y _x✝ →
      P y.1 y.2.1
x✝⁴ : ℕ
x✝³ : (x : ℕ) ×' x✝⁴ < x
a✝¹ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := x✝⁴, snd := x✝³ } →
      P y.1 y.2.1
x✝² : ℕ
x✝¹ : x✝⁴ < x✝²
a✝ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := x✝⁴, snd := { fst := x✝², snd := x✝¹ } } →
      P y.1 y.2.1
a b : ℕ
h✝ : a + 1 < b + 1
x✝ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := succ a, snd := { fst := succ b, snd := h✝ } } →
      P y.1 y.2.1
this : a + 1 = b ∨ a + 1 < b
wf : a + 1 + b < a + 1 + (b + 1)
h : a + 1 < b
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
    { fst := a + 1, snd := { fst := b, snd := h } } { fst := succ a, snd := { fst := succ b, snd := h✝ } }
[PROOFSTEP]
{assumption
}
[GOAL]
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
_x✝ : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1
a✝² :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y _x✝ →
      P y.1 y.2.1
x✝⁴ : ℕ
x✝³ : (x : ℕ) ×' x✝⁴ < x
a✝¹ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := x✝⁴, snd := x✝³ } →
      P y.1 y.2.1
x✝² : ℕ
x✝¹ : x✝⁴ < x✝²
a✝ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := x✝⁴, snd := { fst := x✝², snd := x✝¹ } } →
      P y.1 y.2.1
a b : ℕ
h✝ : a + 1 < b + 1
x✝ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := succ a, snd := { fst := succ b, snd := h✝ } } →
      P y.1 y.2.1
this : a + 1 = b ∨ a + 1 < b
wf : a + 1 + b < a + 1 + (b + 1)
h : a + 1 < b
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
    { fst := a + 1, snd := { fst := b, snd := h } } { fst := succ a, snd := { fst := succ b, snd := h✝ } }
[PROOFSTEP]
assumption
[GOAL]
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
_x✝ : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1
a✝³ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y _x✝ →
      P y.1 y.2.1
x✝⁵ : ℕ
x✝⁴ : (x : ℕ) ×' x✝⁵ < x
a✝² :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := x✝⁵, snd := x✝⁴ } →
      P y.1 y.2.1
x✝³ : ℕ
x✝² : x✝⁵ < x✝³
a✝¹ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := x✝⁵, snd := { fst := x✝³, snd := x✝² } } →
      P y.1 y.2.1
a b : ℕ
h : a + 1 < b + 1
x✝¹ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := succ a, snd := { fst := succ b, snd := h } } →
      P y.1 y.2.1
x✝ : a + (b + 1) < a + 1 + (b + 1)
a✝ : a < b + 1
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
    { fst := a, snd := { fst := b + 1, snd := a✝ } } { fst := succ a, snd := { fst := succ b, snd := h } }
[PROOFSTEP]
{assumption
}
[GOAL]
P : ℕ → ℕ → Prop
ha : ∀ (a : ℕ), P (a + 1) (a + 1)
hb : ∀ (b : ℕ), P 0 (b + 1)
hd : ∀ (a b : ℕ), a < b → P (a + 1) b → P a (b + 1) → P (a + 1) (b + 1)
_x✝ : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1
a✝³ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y _x✝ →
      P y.1 y.2.1
x✝⁵ : ℕ
x✝⁴ : (x : ℕ) ×' x✝⁵ < x
a✝² :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := x✝⁵, snd := x✝⁴ } →
      P y.1 y.2.1
x✝³ : ℕ
x✝² : x✝⁵ < x✝³
a✝¹ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := x✝⁵, snd := { fst := x✝³, snd := x✝² } } →
      P y.1 y.2.1
a b : ℕ
h : a + 1 < b + 1
x✝¹ :
  ∀ (y : (x : ℕ) ×' (x_1 : ℕ) ×' x < x_1),
    (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
        y { fst := succ a, snd := { fst := succ b, snd := h } } →
      P y.1 y.2.1
x✝ : a + (b + 1) < a + 1 + (b + 1)
a✝ : a < b + 1
⊢ (invImage (fun a => PSigma.casesOn a fun a snd => PSigma.casesOn snd fun b snd => a + b) instWellFoundedRelation).1
    { fst := a, snd := { fst := b + 1, snd := a✝ } } { fst := succ a, snd := { fst := succ b, snd := h } }
[PROOFSTEP]
assumption
[GOAL]
m n k l : ℕ
h : m ≤ k * n
k0 : k = 0
⊢ m / k ≤ n
[PROOFSTEP]
rw [k0, Nat.div_zero]
[GOAL]
m n k l : ℕ
h : m ≤ k * n
k0 : k = 0
⊢ 0 ≤ n
[PROOFSTEP]
apply zero_le
[GOAL]
m✝ n✝ k l m n : ℕ
n0 : n = 0
⊢ m / n ≤ m
[PROOFSTEP]
rw [n0, Nat.div_zero]
[GOAL]
m✝ n✝ k l m n : ℕ
n0 : n = 0
⊢ 0 ≤ m
[PROOFSTEP]
apply zero_le
[GOAL]
m n k l : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ n * m ≤ m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m n k l : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ m * n ≤ m
[PROOFSTEP]
exact (Nat.le_div_iff_mul_le' (lt_of_lt_of_le (by decide) hn)).1 h
[GOAL]
m n k l : ℕ
hn : 2 ≤ n
h : m ≤ m / n
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
hm0 : m = 0
⊢ m / k * n / m ≤ n / k
[PROOFSTEP]
simp [hm0]
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
hm0 : ¬m = 0
⊢ m / k * n ≤ n * m / k
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
hm0 : ¬m = 0
⊢ n * (m / k) ≤ n * m / k
[PROOFSTEP]
exact mul_div_le_mul_div_assoc _ _ _
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
hm0 : ¬m = 0
⊢ n * m / k / m = n / k
[PROOFSTEP]
{rw [Nat.div_div_eq_div_mul, mul_comm n, mul_comm k, Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero hm0)]
}
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
hm0 : ¬m = 0
⊢ n * m / k / m = n / k
[PROOFSTEP]
rw [Nat.div_div_eq_div_mul, mul_comm n, mul_comm k, Nat.mul_div_mul_left _ _ (Nat.pos_of_ne_zero hm0)]
[GOAL]
m n k l : ℕ
hmk : k ∣ m
hnl : l ∣ n
⊢ m * n / (k * l) = m / k * (n / l)
[PROOFSTEP]
rcases k.eq_zero_or_pos with (rfl | hk0)
[GOAL]
case inl
m n l : ℕ
hnl : l ∣ n
hmk : 0 ∣ m
⊢ m * n / (0 * l) = m / 0 * (n / l)
[PROOFSTEP]
simp
[GOAL]
case inr
m n k l : ℕ
hmk : k ∣ m
hnl : l ∣ n
hk0 : k > 0
⊢ m * n / (k * l) = m / k * (n / l)
[PROOFSTEP]
rcases l.eq_zero_or_pos with (rfl | hl0)
[GOAL]
case inr.inl
m n k : ℕ
hmk : k ∣ m
hk0 : k > 0
hnl : 0 ∣ n
⊢ m * n / (k * 0) = m / k * (n / 0)
[PROOFSTEP]
simp
[GOAL]
case inr.inr
m n k l : ℕ
hmk : k ∣ m
hnl : l ∣ n
hk0 : k > 0
hl0 : l > 0
⊢ m * n / (k * l) = m / k * (n / l)
[PROOFSTEP]
obtain ⟨_, rfl⟩ := hmk
[GOAL]
case inr.inr.intro
n k l : ℕ
hnl : l ∣ n
hk0 : k > 0
hl0 : l > 0
w✝ : ℕ
⊢ k * w✝ * n / (k * l) = k * w✝ / k * (n / l)
[PROOFSTEP]
obtain ⟨_, rfl⟩ := hnl
[GOAL]
case inr.inr.intro.intro
k l : ℕ
hk0 : k > 0
hl0 : l > 0
w✝¹ w✝ : ℕ
⊢ k * w✝¹ * (l * w✝) / (k * l) = k * w✝¹ / k * (l * w✝ / l)
[PROOFSTEP]
rw [mul_mul_mul_comm, Nat.mul_div_cancel_left _ hk0, Nat.mul_div_cancel_left _ hl0,
  Nat.mul_div_cancel_left _ (mul_pos hk0 hl0)]
[GOAL]
m n k l a b : ℕ
h : a / 2 < a - b
⊢ b ≤ a / 2
[PROOFSTEP]
rw [Nat.le_div_iff_mul_le two_pos]
[GOAL]
m n k l a b : ℕ
h : a / 2 < a - b
⊢ b * 2 ≤ a
[PROOFSTEP]
rw [Nat.div_lt_iff_lt_mul two_pos, Nat.mul_sub_right_distrib, lt_tsub_iff_right, mul_two a] at h 
[GOAL]
m n k l a b : ℕ
h✝ : a < a * 2 - b * 2
h : a + b * 2 < a + a
⊢ b * 2 ≤ a
[PROOFSTEP]
exact le_of_lt (Nat.lt_of_add_lt_add_left h)
[GOAL]
m n k l a b : ℕ
h : a - b ≤ a / 2
⊢ a / 2 ≤ b
[PROOFSTEP]
rw [Nat.le_div_iff_mul_le two_pos, Nat.mul_sub_right_distrib, tsub_le_iff_right, mul_two, add_le_add_iff_left] at h 
[GOAL]
m n k l a b : ℕ
h✝ : a * 2 - b * 2 ≤ a
h : a ≤ b * 2
⊢ a / 2 ≤ b
[PROOFSTEP]
rw [← Nat.mul_div_left b two_pos]
[GOAL]
m n k l a b : ℕ
h✝ : a * 2 - b * 2 ≤ a
h : a ≤ b * 2
⊢ a / 2 ≤ b * 2 / 2
[PROOFSTEP]
exact Nat.div_le_div_right h
[GOAL]
m n k l : ℕ
hn : n % 2 = 1
⊢ 2 * (n / 2) = n - 1
[PROOFSTEP]
conv =>
  rhs
  rw [← Nat.mod_add_div n 2, hn, @add_tsub_cancel_left]
[GOAL]
m n k l : ℕ
hn : n % 2 = 1
| 2 * (n / 2) = n - 1
[PROOFSTEP]
  rhs
  rw [← Nat.mod_add_div n 2, hn, @add_tsub_cancel_left]
[GOAL]
m n k l : ℕ
hn : n % 2 = 1
| 2 * (n / 2) = n - 1
[PROOFSTEP]
  rhs
  rw [← Nat.mod_add_div n 2, hn, @add_tsub_cancel_left]
[GOAL]
m n k l : ℕ
hn : n % 2 = 1
| 2 * (n / 2) = n - 1
[PROOFSTEP]
rhs
[GOAL]
m n k l : ℕ
hn : n % 2 = 1
| n - 1
[PROOFSTEP]
rw [← Nat.mod_add_div n 2, hn, @add_tsub_cancel_left]
[GOAL]
m n k l : ℕ
h : n ∣ m
hm : m ≠ 0
⊢ m / (m / n) = n
[PROOFSTEP]
rcases h with ⟨_, rfl⟩
[GOAL]
case intro
n k l w✝ : ℕ
hm : n * w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n
[PROOFSTEP]
rw [mul_ne_zero_iff] at hm 
[GOAL]
case intro
n k l w✝ : ℕ
hm : n ≠ 0 ∧ w✝ ≠ 0
⊢ n * w✝ / (n * w✝ / n) = n
[PROOFSTEP]
rw [mul_div_right _ (Nat.pos_of_ne_zero hm.1), mul_div_left _ (Nat.pos_of_ne_zero hm.2)]
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
⊢ m % (n * k) / n = m / n % k
[PROOFSTEP]
rcases Nat.eq_zero_or_pos n with (rfl | hn)
[GOAL]
case inl
m✝ n k✝ l m k : ℕ
⊢ m % (0 * k) / 0 = m / 0 % k
case inr m✝ n✝ k✝ l m n k : ℕ hn : n > 0 ⊢ m % (n * k) / n = m / n % k
[PROOFSTEP]
simp [mod_zero]
[GOAL]
case inr
m✝ n✝ k✝ l m n k : ℕ
hn : n > 0
⊢ m % (n * k) / n = m / n % k
[PROOFSTEP]
rcases Nat.eq_zero_or_pos k with (rfl | hk)
[GOAL]
case inr.inl
m✝ n✝ k l m n : ℕ
hn : n > 0
⊢ m % (n * 0) / n = m / n % 0
case inr.inr m✝ n✝ k✝ l m n k : ℕ hn : n > 0 hk : k > 0 ⊢ m % (n * k) / n = m / n % k
[PROOFSTEP]
simp [mod_zero]
[GOAL]
case inr.inr
m✝ n✝ k✝ l m n k : ℕ
hn : n > 0
hk : k > 0
⊢ m % (n * k) / n = m / n % k
[PROOFSTEP]
conv_rhs => rw [← mod_add_div m (n * k)]
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
hn : n > 0
hk : k > 0
| m / n % k
[PROOFSTEP]
rw [← mod_add_div m (n * k)]
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
hn : n > 0
hk : k > 0
| m / n % k
[PROOFSTEP]
rw [← mod_add_div m (n * k)]
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
hn : n > 0
hk : k > 0
| m / n % k
[PROOFSTEP]
rw [← mod_add_div m (n * k)]
[GOAL]
case inr.inr
m✝ n✝ k✝ l m n k : ℕ
hn : n > 0
hk : k > 0
⊢ m % (n * k) / n = (m % (n * k) + n * k * (m / (n * k))) / n % k
[PROOFSTEP]
rw [mul_assoc, add_mul_div_left _ _ hn, add_mul_mod_self_left,
  mod_eq_of_lt (Nat.div_lt_of_lt_mul (mod_lt _ (mul_pos hn hk)))]
[GOAL]
m✝ n✝ k✝ l m n k : ℕ
⊢ m % (k * n) / n = m / n % k
[PROOFSTEP]
rw [mul_comm k, mod_mul_right_div_self]
[GOAL]
m n k l : ℕ
h1 : 0 < n
h2 : n < m
⊢ ¬m ∣ n
[PROOFSTEP]
rintro ⟨k, rfl⟩
[GOAL]
case intro
m k✝ l k : ℕ
h1 : 0 < m * k
h2 : m * k < m
⊢ False
[PROOFSTEP]
rcases Nat.eq_zero_or_pos k with (rfl | hk)
[GOAL]
case intro.inl
m k l : ℕ
h1 : 0 < m * 0
h2 : m * 0 < m
⊢ False
[PROOFSTEP]
exact lt_irrefl 0 h1
[GOAL]
case intro.inr
m k✝ l k : ℕ
h1 : 0 < m * k
h2 : m * k < m
hk : k > 0
⊢ False
[PROOFSTEP]
exact not_lt.2 (le_mul_of_pos_right hk) h2
[GOAL]
m n k l : ℕ
h : m % k = n % k
⊢ (m - n) % k = 0
[PROOFSTEP]
rw [← Nat.mod_add_div m k, ← Nat.mod_add_div n k, ← h, tsub_add_eq_tsub_tsub, @add_tsub_cancel_left, ← mul_tsub k,
  Nat.mul_mod_right]
[GOAL]
m n k l : ℕ
⊢ (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k
[PROOFSTEP]
cases k
[GOAL]
case zero
m n l : ℕ
⊢ (m + n) % zero = if zero ≤ m % zero + n % zero then m % zero + n % zero - zero else m % zero + n % zero
case succ
m n l n✝ : ℕ
⊢ (m + n) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
[PROOFSTEP]
simp [mod_zero]
[GOAL]
case succ
m n l n✝ : ℕ
⊢ (m + n) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
[PROOFSTEP]
rw [Nat.add_mod]
[GOAL]
case succ
m n l n✝ : ℕ
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ =
    if succ n✝ ≤ m % succ n✝ + n % succ n✝ then m % succ n✝ + n % succ n✝ - succ n✝ else m % succ n✝ + n % succ n✝
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
m n l n✝ : ℕ
h : succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ = m % succ n✝ + n % succ n✝ - succ n✝
[PROOFSTEP]
rw [Nat.mod_eq_sub_mod h, Nat.mod_eq_of_lt]
[GOAL]
case pos
m n l n✝ : ℕ
h : succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ m % succ n✝ + n % succ n✝ - succ n✝ < succ n✝
[PROOFSTEP]
exact (tsub_lt_iff_right h).mpr (Nat.add_lt_add (m.mod_lt (zero_lt_succ _)) (n.mod_lt (zero_lt_succ _)))
[GOAL]
case neg
m n l n✝ : ℕ
h : ¬succ n✝ ≤ m % succ n✝ + n % succ n✝
⊢ (m % succ n✝ + n % succ n✝) % succ n✝ = m % succ n✝ + n % succ n✝
[PROOFSTEP]
exact Nat.mod_eq_of_lt (lt_of_not_ge h)
[GOAL]
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : n = 0
⊢ m / n * (k / l) = m * k / (n * l)
[PROOFSTEP]
simp [hn]
[GOAL]
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this : 0 < n
hl : l = 0
⊢ m / n * (k / l) = m * k / (n * l)
[PROOFSTEP]
simp [hl]
[GOAL]
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this : 0 < n
hl : ¬l = 0
⊢ m / n * (k / l) = m * k / (n * l)
[PROOFSTEP]
have : 0 < l := Nat.pos_of_ne_zero hl
[GOAL]
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi1 : ∃ x, m = n * x
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
⊢ m / n * (k / l) = m * k / (n * l)
[PROOFSTEP]
cases' exi1 with x hx
[GOAL]
case intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
exi2 : ∃ y, k = l * y
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
⊢ m / n * (k / l) = m * k / (n * l)
[PROOFSTEP]
cases' exi2 with y hy
[GOAL]
case intro.intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ m / n * (k / l) = m * k / (n * l)
[PROOFSTEP]
rw [hx, hy, Nat.mul_div_cancel_left, Nat.mul_div_cancel_left]
[GOAL]
case intro.intro
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ x * y = n * x * (l * y) / (n * l)
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
[PROOFSTEP]
apply Eq.symm
[GOAL]
case intro.intro.h
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) / (n * l) = x * y
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
[PROOFSTEP]
apply Nat.div_eq_of_eq_mul_left
[GOAL]
case intro.intro.h.H1
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n * l
case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
[PROOFSTEP]
apply mul_pos
[GOAL]
case intro.intro.h.H1.ha
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
case intro.intro.h.H1.hb
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l
case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
[PROOFSTEP]
repeat'
  assumption
    -- Porting note: this line was `cc` in Lean3
[GOAL]
case intro.intro.h.H1.ha
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
[PROOFSTEP]
assumption
  -- Porting note: this line was `cc` in Lean3
[GOAL]
case intro.intro.h.H1.hb
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l
[PROOFSTEP]
assumption
  -- Porting note: this line was `cc` in Lean3
[GOAL]
case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)
[PROOFSTEP]
assumption
  -- Porting note: this line was `cc` in Lean3
[GOAL]
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < l
[PROOFSTEP]
assumption
  -- Porting note: this line was `cc` in Lean3
[GOAL]
case intro.intro.H
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ 0 < n
[PROOFSTEP]
assumption
  -- Porting note: this line was `cc` in Lean3
[GOAL]
case intro.intro.h.H2
m n k l : ℕ
hmn : n ∣ m
hkl : l ∣ k
hn : ¬n = 0
this✝ : 0 < n
hl : ¬l = 0
this : 0 < l
x : ℕ
hx : m = n * x
y : ℕ
hy : k = l * y
⊢ n * x * (l * y) = x * y * (n * l)
[PROOFSTEP]
simp only [mul_comm, mul_left_comm, mul_assoc]
[GOAL]
m n k l : ℕ
⊢ m / n = m ↔ m = 0 ∨ n = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
m n k l : ℕ
⊢ m / n = m → m = 0 ∨ n = 1
[PROOFSTEP]
intro
[GOAL]
case mp
m n k l : ℕ
a✝ : m / n = m
⊢ m = 0 ∨ n = 1
[PROOFSTEP]
match n with
| 0 => simp_all
| 1 =>
  right
  rfl
| n + 2 =>
  left
  have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)
  refine eq_zero_of_le_half ?_
  simp_all
[GOAL]
m n k l : ℕ
a✝ : m / 0 = m
⊢ m = 0 ∨ 0 = 1
[PROOFSTEP]
simp_all
[GOAL]
m n k l : ℕ
a✝ : m / 1 = m
⊢ m = 0 ∨ 1 = 1
[PROOFSTEP]
right
[GOAL]
case h
m n k l : ℕ
a✝ : m / 1 = m
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ m = 0 ∨ n + 2 = 1
[PROOFSTEP]
left
[GOAL]
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ m = 0
[PROOFSTEP]
have : m / (n + 2) ≤ m / 2 := div_le_div_left (by simp) (by decide)
[GOAL]
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ 2 ≤ n + 2
[PROOFSTEP]
simp
[GOAL]
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m = 0
[PROOFSTEP]
refine eq_zero_of_le_half ?_
[GOAL]
case h
m n✝ k l n : ℕ
a✝ : m / (n + 2) = m
this : m / (n + 2) ≤ m / 2
⊢ m ≤ m / 2
[PROOFSTEP]
simp_all
[GOAL]
case mpr
m n k l : ℕ
⊢ m = 0 ∨ n = 1 → m / n = m
[PROOFSTEP]
rintro (rfl | rfl)
[GOAL]
case mpr.inl
n k l : ℕ
⊢ 0 / n = 0
[PROOFSTEP]
simp
[GOAL]
case mpr.inr
m k l : ℕ
⊢ m / 1 = m
[PROOFSTEP]
simp
[GOAL]
m n k l : ℕ
⊢ m / n = (m - m % n) / n
[PROOFSTEP]
by_cases n0 : n = 0
[GOAL]
case pos
m n k l : ℕ
n0 : n = 0
⊢ m / n = (m - m % n) / n
[PROOFSTEP]
rw [n0, Nat.div_zero, Nat.div_zero]
[GOAL]
case neg
m n k l : ℕ
n0 : ¬n = 0
⊢ m / n = (m - m % n) / n
[PROOFSTEP]
have : m - m % n = n * (m / n) := by rw [tsub_eq_iff_eq_add_of_le (Nat.mod_le _ _), add_comm, mod_add_div]
[GOAL]
m n k l : ℕ
n0 : ¬n = 0
⊢ m - m % n = n * (m / n)
[PROOFSTEP]
rw [tsub_eq_iff_eq_add_of_le (Nat.mod_le _ _), add_comm, mod_add_div]
[GOAL]
case neg
m n k l : ℕ
n0 : ¬n = 0
this : m - m % n = n * (m / n)
⊢ m / n = (m - m % n) / n
[PROOFSTEP]
rw [this, mul_div_right _ (Nat.pos_of_ne_zero n0)]
[GOAL]
m n k l : ℕ
h1 : n * k < m
h2 : m < n * (k + 1)
⊢ ¬n ∣ m
[PROOFSTEP]
rintro ⟨d, rfl⟩
[GOAL]
case intro
n k l d : ℕ
h1 : n * k < n * d
h2 : n * d < n * (k + 1)
⊢ False
[PROOFSTEP]
exact Monotone.ne_of_lt_of_lt_nat (Covariant.monotone_of_const n) k h1 h2 d rfl
[GOAL]
m n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ 0 < Nat.find h ↔ ¬p 0
[PROOFSTEP]
rw [pos_iff_ne_zero, Ne, Nat.find_eq_zero]
[GOAL]
m n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₘ + n = Nat.find hₙ
[PROOFSTEP]
refine ((le_find_iff _ _).2 fun m hm hpm => hm.not_le ?_).antisymm ?_
[GOAL]
case refine_1
m✝ n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₘ + n
hpm : p m
⊢ Nat.find hₘ + n ≤ m
[PROOFSTEP]
have hnm : n ≤ m := hn.trans (find_le hpm)
[GOAL]
case refine_1
m✝ n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₘ + n
hpm : p m
hnm : n ≤ m
⊢ Nat.find hₘ + n ≤ m
[PROOFSTEP]
refine add_le_of_le_tsub_right_of_le hnm (find_le ?_)
[GOAL]
case refine_1
m✝ n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₘ + n
hpm : p m
hnm : n ≤ m
⊢ p (m - n + n)
[PROOFSTEP]
rwa [tsub_add_cancel_of_le hnm]
[GOAL]
case refine_2
m n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ ≤ Nat.find hₘ + n
[PROOFSTEP]
rw [← tsub_le_iff_right]
[GOAL]
case refine_2
m n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
⊢ Nat.find hₙ - n ≤ Nat.find hₘ
[PROOFSTEP]
refine (le_find_iff _ _).2 fun m hm hpm => hm.not_le ?_
[GOAL]
case refine_2
m✝ n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₙ - n
hpm : p (m + n)
⊢ Nat.find hₙ - n ≤ m
[PROOFSTEP]
rw [tsub_le_iff_right]
[GOAL]
case refine_2
m✝ n k l : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
hₘ : ∃ m, p (m + n)
hₙ : ∃ n, p n
hn : n ≤ Nat.find hₙ
m : ℕ
hm : m < Nat.find hₙ - n
hpm : p (m + n)
⊢ Nat.find hₙ ≤ m + n
[PROOFSTEP]
exact find_le hpm
[GOAL]
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
⊢ Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
[PROOFSTEP]
induction' k with k ihk generalizing m
[GOAL]
case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ Nat.findGreatest P zero = m ↔ m ≤ zero ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ zero → ¬P n
[PROOFSTEP]
rw [eq_comm, Iff.comm]
[GOAL]
case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ (m ≤ zero ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ zero → ¬P n) ↔ m = Nat.findGreatest P zero
[PROOFSTEP]
simp only [zero_eq, nonpos_iff_eq_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
[GOAL]
case zero
m✝ n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
m : ℕ
⊢ m = 0 → (¬m = 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n = 0 → ¬P n
[PROOFSTEP]
rintro rfl
[GOAL]
case zero
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
⊢ (¬0 = 0 → P 0) ∧ ∀ ⦃n : ℕ⦄, 0 < n → n = 0 → ¬P n
[PROOFSTEP]
exact ⟨fun h => (h rfl).elim, fun n hlt heq => (hlt.ne heq.symm).elim⟩
[GOAL]
case succ
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
[PROOFSTEP]
by_cases hk : P (k + 1)
[GOAL]
case pos
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
[PROOFSTEP]
rw [findGreatest_eq hk]
[GOAL]
case pos
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
[PROOFSTEP]
constructor
[GOAL]
case pos.mp
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ k + 1 = m → m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
[PROOFSTEP]
rintro rfl
[GOAL]
case pos.mp
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
⊢ k + 1 ≤ succ k ∧ (k + 1 ≠ 0 → P (k + 1)) ∧ ∀ ⦃n : ℕ⦄, k + 1 < n → n ≤ succ k → ¬P n
[PROOFSTEP]
exact ⟨le_rfl, fun _ => hk, fun n hlt hle => (hlt.not_le hle).elim⟩
[GOAL]
case pos.mpr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ (m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n) → k + 1 = m
[PROOFSTEP]
rintro ⟨hle, h0, hm⟩
[GOAL]
case pos.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ succ k
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ k + 1 = m
[PROOFSTEP]
rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt)
[GOAL]
case pos.mpr.intro.intro.inl
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : P (k + 1)
hle : succ k ≤ succ k
h0 : succ k ≠ 0 → P (succ k)
hm : ∀ ⦃n : ℕ⦄, succ k < n → n ≤ succ k → ¬P n
⊢ k + 1 = succ k
case pos.mpr.intro.intro.inr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
hle : m ≤ succ k
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
hlt : m < succ k
⊢ k + 1 = m
[PROOFSTEP]
exacts [rfl, (hm hlt le_rfl hk).elim]
[GOAL]
case neg
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ Nat.findGreatest P (succ k) = m ↔ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
[PROOFSTEP]
rw [findGreatest_of_not hk, ihk]
[GOAL]
case neg
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) ↔
    m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
[PROOFSTEP]
constructor
[GOAL]
case neg.mp
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) →
    m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
[PROOFSTEP]
rintro ⟨hle, hP, hm⟩
[GOAL]
case neg.mp.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
⊢ m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
[PROOFSTEP]
refine ⟨hle.trans k.le_succ, hP, fun n hlt hle => ?_⟩
[GOAL]
case neg.mp.intro.intro
m✝ n✝ k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
n : ℕ
hlt : m < n
hle : n ≤ succ k
⊢ ¬P n
[PROOFSTEP]
rcases Decidable.eq_or_lt_of_le hle with (rfl | hlt')
[GOAL]
case neg.mp.intro.intro.inl
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hlt : m < succ k
hle : succ k ≤ succ k
⊢ ¬P (succ k)
case neg.mp.intro.intro.inr
m✝ n✝ k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle✝ : m ≤ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
n : ℕ
hlt : m < n
hle : n ≤ succ k
hlt' : n < succ k
⊢ ¬P n
[PROOFSTEP]
exacts [hk, hm hlt <| lt_succ_iff.1 hlt']
[GOAL]
case neg.mpr
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ succ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n) →
    m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
[PROOFSTEP]
rintro ⟨hle, hP, hm⟩
[GOAL]
case neg.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ succ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
[PROOFSTEP]
refine ⟨lt_succ_iff.1 (hle.lt_of_ne ?_), hP, fun n hlt hle => hm hlt (hle.trans k.le_succ)⟩
[GOAL]
case neg.mpr.intro.intro
m✝ n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
hle : m ≤ succ k
hP : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ succ k → ¬P n
⊢ m ≠ succ k
[PROOFSTEP]
rintro rfl
[GOAL]
case neg.mpr.intro.intro
m n k✝ l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, Nat.findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
hk : ¬P (k + 1)
hle : succ k ≤ succ k
hP : succ k ≠ 0 → P (succ k)
hm : ∀ ⦃n : ℕ⦄, succ k < n → n ≤ succ k → ¬P n
⊢ False
[PROOFSTEP]
exact hk (hP k.succ_ne_zero)
[GOAL]
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
⊢ Nat.findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n
[PROOFSTEP]
simp [findGreatest_eq_iff]
[GOAL]
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
hmb : m ≤ n
hm : P m
⊢ P (Nat.findGreatest P n)
[PROOFSTEP]
by_cases h : Nat.findGreatest P n = 0
[GOAL]
case pos
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
hmb : m ≤ n
hm : P m
h : Nat.findGreatest P n = 0
⊢ P (Nat.findGreatest P n)
[PROOFSTEP]
cases m
[GOAL]
case pos.zero
n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
h : Nat.findGreatest P n = 0
hmb : zero ≤ n
hm : P zero
⊢ P (Nat.findGreatest P n)
[PROOFSTEP]
rwa [h]
[GOAL]
case pos.succ
n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
h : Nat.findGreatest P n = 0
n✝ : ℕ
hmb : succ n✝ ≤ n
hm : P (succ n✝)
⊢ P (Nat.findGreatest P n)
[PROOFSTEP]
exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim
[GOAL]
case neg
m n k l : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
hmb : m ≤ n
hm : P m
h : ¬Nat.findGreatest P n = 0
⊢ P (Nat.findGreatest P n)
[PROOFSTEP]
exact (findGreatest_eq_iff.1 rfl).2.1 h
[GOAL]
m n k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ Monotone (Nat.findGreatest P)
[PROOFSTEP]
refine monotone_nat_of_le_succ fun n => ?_
[GOAL]
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ Nat.findGreatest P n ≤ Nat.findGreatest P (n + 1)
[PROOFSTEP]
rw [findGreatest_succ]
[GOAL]
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
⊢ Nat.findGreatest P n ≤ if P (n + 1) then n + 1 else Nat.findGreatest P n
[PROOFSTEP]
split_ifs
[GOAL]
case pos
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h✝ : P (n + 1)
⊢ Nat.findGreatest P n ≤ n + 1
[PROOFSTEP]
exact (findGreatest_le n).trans (le_succ _)
[GOAL]
case neg
m n✝ k l : ℕ
P✝ Q : ℕ → Prop
inst✝¹ : DecidablePred P✝
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h✝ : ¬P (n + 1)
⊢ Nat.findGreatest P n ≤ Nat.findGreatest P n
[PROOFSTEP]
rfl
[GOAL]
m n k l : ℕ
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : P ≤ Q
⊢ Nat.findGreatest P ≤ Nat.findGreatest Q
[PROOFSTEP]
intro n
[GOAL]
m n✝ k l : ℕ
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : P ≤ Q
n : ℕ
⊢ Nat.findGreatest P n ≤ Nat.findGreatest Q n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
m n k l : ℕ
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : P ≤ Q
⊢ Nat.findGreatest P zero ≤ Nat.findGreatest Q zero
[PROOFSTEP]
rfl
[GOAL]
case succ
m n✝ k l : ℕ
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : P ≤ Q
n : ℕ
hn : Nat.findGreatest P n ≤ Nat.findGreatest Q n
⊢ Nat.findGreatest P (succ n) ≤ Nat.findGreatest Q (succ n)
[PROOFSTEP]
by_cases h : P (n + 1)
[GOAL]
case pos
m n✝ k l : ℕ
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : P ≤ Q
n : ℕ
hn : Nat.findGreatest P n ≤ Nat.findGreatest Q n
h : P (n + 1)
⊢ Nat.findGreatest P (succ n) ≤ Nat.findGreatest Q (succ n)
[PROOFSTEP]
rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]
[GOAL]
case neg
m n✝ k l : ℕ
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : P ≤ Q
n : ℕ
hn : Nat.findGreatest P n ≤ Nat.findGreatest Q n
h : ¬P (n + 1)
⊢ Nat.findGreatest P (succ n) ≤ Nat.findGreatest Q (succ n)
[PROOFSTEP]
rw [findGreatest_of_not h]
[GOAL]
case neg
m n✝ k l : ℕ
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : P ≤ Q
n : ℕ
hn : Nat.findGreatest P n ≤ Nat.findGreatest Q n
h : ¬P (n + 1)
⊢ Nat.findGreatest P n ≤ Nat.findGreatest Q (succ n)
[PROOFSTEP]
exact hn.trans (Nat.findGreatest_mono_right _ <| le_succ _)
[GOAL]
m n k l : ℕ
h : bit0 m ≤ bit1 n
⊢ m ≤ n
[PROOFSTEP]
rwa [← Nat.lt_succ_iff, n.bit1_eq_succ_bit0, ← n.bit0_succ_eq, bit0_lt_bit0, Nat.lt_succ_iff] at h 
[GOAL]
m n k l : ℕ
h : bit1 m ≤ bit0 n
⊢ m < n
[PROOFSTEP]
rwa [m.bit1_eq_succ_bit0, succ_le_iff, bit0_lt_bit0] at h 
[GOAL]
m n k l lo hi : ℕ
P : ℕ → Prop
H : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
⊢ P x
[PROOFSTEP]
have := al (x - lo) ((tsub_lt_tsub_iff_right hl).mpr hh)
[GOAL]
m n k l lo hi : ℕ
P : ℕ → Prop
H : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
this : P (lo + (x - lo))
⊢ P x
[PROOFSTEP]
rwa [add_tsub_cancel_of_le hl] at this 
