[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


[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
m n : ℕ
⊢ ↑(m * n) = ↑m * ↑n
[PROOFSTEP]
induction n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
m : ℕ
⊢ ↑(m * zero) = ↑m * ↑zero
[PROOFSTEP]
simp [mul_succ, mul_add, *]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
m n✝ : ℕ
n_ih✝ : ↑(m * n✝) = ↑m * ↑n✝
⊢ ↑(m * succ n✝) = ↑m * ↑(succ n✝)
[PROOFSTEP]
simp [mul_succ, mul_add, *]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x
[PROOFSTEP]
induction n with
| zero => rw [Nat.cast_zero]; exact Commute.zero_left x
| succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x
[PROOFSTEP]
induction n with
| zero => rw [Nat.cast_zero]; exact Commute.zero_left x
| succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
⊢ Commute (↑zero) x
[PROOFSTEP]

| zero => rw [Nat.cast_zero]; exact Commute.zero_left x
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
⊢ Commute (↑zero) x
[PROOFSTEP]
rw [Nat.cast_zero]
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x
[PROOFSTEP]
exact Commute.zero_left x
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑(succ n)) x
[PROOFSTEP]

| succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑(succ n)) x
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x
[PROOFSTEP]
exact ihn.add_left (Commute.one_left x)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : AddCommMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑(n + 1)
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : AddCommMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝ : ZeroLEOneClass α
n : ℕ
⊢ ↑n ≤ ↑n + 1
[PROOFSTEP]
exact le_add_of_nonneg_right zero_le_one
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 0 < ↑n ↔ 0 < n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ 0 < ↑zero ↔ 0 < zero
[PROOFSTEP]
simp [cast_add_one_pos]
  -- without this more specific version Lean often chokes
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n✝ : ℕ
⊢ 0 < ↑(succ n✝) ↔ 0 < succ n✝
[PROOFSTEP]
simp [cast_add_one_pos]
  -- without this more specific version Lean often chokes
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
m n : ℕ
⊢ 1 < ↑n ↔ 1 < n
[PROOFSTEP]
rw [← cast_one, cast_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
m n : ℕ
⊢ 1 ≤ ↑n ↔ 1 ≤ n
[PROOFSTEP]
rw [← cast_one, cast_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
m n : ℕ
⊢ ↑n < 1 ↔ n = 0
[PROOFSTEP]
rw [← cast_one, cast_lt, lt_succ_iff, ← bot_eq_zero, le_bot_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : AddCommMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
inst✝¹ : ZeroLEOneClass α
inst✝ : CharZero α
m n : ℕ
⊢ ↑n ≤ 1 ↔ n ≤ 1
[PROOFSTEP]
rw [← cast_one, cast_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : ℕ
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
cases' le_total m n with h h
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : ℕ
h : m ≤ n
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
rw [tsub_eq_zero_of_le h, cast_zero, tsub_eq_zero_of_le]
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : ℕ
h : m ≤ n
⊢ ↑m ≤ ↑n
[PROOFSTEP]
exact mono_cast h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
m n : ℕ
h : n ≤ m
⊢ ↑(m - n) = ↑m - ↑n
[PROOFSTEP]
rcases le_iff_exists_add'.mp h with ⟨m, rfl⟩
[GOAL]
case inr.intro
α : Type u_1
β : Type u_2
inst✝³ : CanonicallyOrderedCommSemiring α
inst✝² : Sub α
inst✝¹ : OrderedSub α
inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
n m : ℕ
h : n ≤ m + n
⊢ ↑(m + n - n) = ↑(m + n) - ↑n
[PROOFSTEP]
rw [add_tsub_cancel_right, cast_add, add_tsub_cancel_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : CharZero α
⊢ 1 ≠ 0
[PROOFSTEP]
decide
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
⊢ ∀ (x : ℕ), ↑f x = ↑g x
[PROOFSTEP]
intro n
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
⊢ ↑f n = ↑g n
[PROOFSTEP]
induction n with
| zero => simp_rw [Nat.zero_eq, map_zero f, map_zero g]
| succ n ihn => simp [Nat.succ_eq_add_one, h, ihn]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
⊢ ↑f n = ↑g n
[PROOFSTEP]
induction n with
| zero => simp_rw [Nat.zero_eq, map_zero f, map_zero g]
| succ n ihn => simp [Nat.succ_eq_add_one, h, ihn]
[GOAL]
case zero
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
⊢ ↑f Nat.zero = ↑g Nat.zero
[PROOFSTEP]

| zero => simp_rw [Nat.zero_eq, map_zero f, map_zero g]
[GOAL]
case zero
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
⊢ ↑f Nat.zero = ↑g Nat.zero
[PROOFSTEP]
simp_rw [Nat.zero_eq, map_zero f, map_zero g]
[GOAL]
case succ
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
ihn : ↑f n = ↑g n
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
[PROOFSTEP]

| succ n ihn => simp [Nat.succ_eq_add_one, h, ihn]
[GOAL]
case succ
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoid A
inst✝ : AddMonoidHomClass F ℕ A
f g : F
h : ↑f 1 = ↑g 1
n : ℕ
ihn : ↑f n = ↑g n
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
[PROOFSTEP]
simp [Nat.succ_eq_add_one, h, ihn]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : ↑f 1 = 1
⊢ ↑f 0 = ↑0
[PROOFSTEP]
simp [map_zero f]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
B : Type u_4
F : Type u_5
inst✝² : AddMonoidWithOne B
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F ℕ A
f : F
h1 : ↑f 1 = 1
n : ℕ
⊢ ↑f (n + 1) = ↑(n + 1)
[PROOFSTEP]
rw [map_add, h1, eq_natCast' f h1 n, Nat.cast_add_one]
[GOAL]
α : Type u_1
β : Type u_2
A✝ : Type u_3
B : Type u_4
F : Type u_5
inst✝³ : AddMonoidWithOne B
inst✝² : AddMonoidWithOne A✝
A : Type u_6
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F A B
f : F
h : ↑f 1 = 1
⊢ ↑f ↑0 = ↑0
[PROOFSTEP]
simp [map_zero f]
[GOAL]
α : Type u_1
β : Type u_2
A✝ : Type u_3
B : Type u_4
F : Type u_5
inst✝³ : AddMonoidWithOne B
inst✝² : AddMonoidWithOne A✝
A : Type u_6
inst✝¹ : AddMonoidWithOne A
inst✝ : AddMonoidHomClass F A B
f : F
h : ↑f 1 = 1
n : ℕ
⊢ ↑f ↑(n + 1) = ↑(n + 1)
[PROOFSTEP]
rw [Nat.cast_add, map_add, Nat.cast_add, map_natCast' f h n, Nat.cast_one, h, Nat.cast_one]
[GOAL]
α : Type u_1
β : Type u_2
A : Type u_3
F : Type u_4
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ f = g
[PROOFSTEP]
apply FunLike.ext
[GOAL]
case h
α : Type u_1
β : Type u_2
A : Type u_3
F : Type u_4
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ ∀ (x : ℕ), ↑f x = ↑g x
[PROOFSTEP]
rintro (_ | n)
[GOAL]
case h.zero
α : Type u_1
β : Type u_2
A : Type u_3
F : Type u_4
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
⊢ ↑f Nat.zero = ↑g Nat.zero
[PROOFSTEP]
simp [map_zero f, map_zero g]
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
A : Type u_3
F : Type u_4
inst✝¹ : MulZeroOneClass A
inst✝ : MonoidWithZeroHomClass F ℕ A
f g : F
h_pos : ∀ {n : ℕ}, 0 < n → ↑f n = ↑g n
n : ℕ
⊢ ↑f (Nat.succ n) = ↑g (Nat.succ n)
[PROOFSTEP]
exact h_pos n.succ_pos
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
inst✝ : RingHomClass F ℕ R
f g : F
⊢ ↑f 1 = ↑g 1
[PROOFSTEP]
simp only [map_one f, map_one g]
[GOAL]
α : Type u_1
β : Type u_2
R : Type u_3
S : Type u_4
F : Type u_5
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
n : ℕ
h✝ : NeZero ↑n
inst✝ : RingHomClass F R S
f : F
hf : Function.Injective ↑f
h : ↑n = 0
⊢ ↑f ↑n = ↑f 0
[PROOFSTEP]
simpa only [map_natCast, map_zero f]
[GOAL]
α : Type u_1
β : Type u_2
R✝ : Type u_3
S✝ : Type u_4
F✝ : Type u_5
inst✝⁴ : NonAssocSemiring R✝
inst✝³ : NonAssocSemiring S✝
R : Type u_6
S : Type u_7
inst✝² : Semiring R
inst✝¹ : Semiring S
F : Type u_8
inst✝ : RingHomClass F R S
f : F
n : ℕ
hn : NeZero ↑n
⊢ NeZero (↑f ↑n)
[PROOFSTEP]
simp only [map_natCast, hn]


[GOAL]
p a b k : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
⊢ p ∣ choose (a + b) a
[PROOFSTEP]
have h₁ : p ∣ (a + b)! := hp.dvd_factorial.2 h
[GOAL]
p a b k : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : p ∣ (a + b)!
⊢ p ∣ choose (a + b) a
[PROOFSTEP]
rw [← add_choose_mul_factorial_mul_factorial, ← choose_symm_add, hp.dvd_mul, hp.dvd_mul, hp.dvd_factorial,
  hp.dvd_factorial] at h₁
[GOAL]
p a b k : ℕ
hp : Prime p
hap : a < p
hbp : b < p
h : p ≤ a + b
h₁ : (p ∣ choose (a + b) a ∨ p ≤ a) ∨ p ≤ b
⊢ p ∣ choose (a + b) a
[PROOFSTEP]
exact (h₁.resolve_right hbp.not_le).resolve_right hap.not_le


[GOAL]
r n : ℕ
⊢ choose (2 * n) (2 * n / 2) = choose (2 * n) n
[PROOFSTEP]
rw [Nat.mul_div_cancel_left n zero_lt_two]
[GOAL]
n : ℕ
⊢ choose (2 * n + 2) (n + 1) * (n + 1) = choose (2 * n + 1) n * (2 * n + 2)
[PROOFSTEP]
rw [choose_succ_right_eq, choose_mul_succ_eq]
[GOAL]
n : ℕ
⊢ choose (2 * n + 1) n * (2 * n + 2) = 2 * (choose (2 * n + 1) n * (n + 1))
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ 2 * (choose (2 * n + 1) n * (n + 1)) = 2 * (choose (2 * n + 1) n * (2 * n + 1 - n))
[PROOFSTEP]
rw [two_mul n, add_assoc, Nat.add_sub_cancel_left]
[GOAL]
n : ℕ
⊢ 2 * (choose (2 * n + 1) n * (2 * n + 1 - n)) = 2 * (choose (2 * n) n * (2 * n + 1))
[PROOFSTEP]
rw [choose_mul_succ_eq]
[GOAL]
n : ℕ
⊢ 2 * (choose (2 * n) n * (2 * n + 1)) = 2 * (2 * n + 1) * choose (2 * n) n
[PROOFSTEP]
rw [mul_assoc, mul_comm (2 * n + 1)]
[GOAL]
n : ℕ
n_big : 4 ≤ n
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n IH
[GOAL]
case h
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
rcases lt_trichotomy n 4 with (hn | rfl | hn)
[GOAL]
case h.inl
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
clear IH
[GOAL]
case h.inl
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
n_big : 4 ≤ n
hn : n < 4
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
exact False.elim ((not_lt.2 n_big) hn)
[GOAL]
case h.inr.inl
n : ℕ
n_big✝ : 4 ≤ n
IH : ∀ (m : ℕ), m < 4 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ 4
⊢ 4 ^ 4 < 4 * centralBinom 4
[PROOFSTEP]
norm_num [centralBinom, choose]
[GOAL]
case h.inr.inr
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n
hn : 4 < n
⊢ 4 ^ n < n * centralBinom n
[PROOFSTEP]
obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := Nat.exists_eq_succ_of_ne_zero (Nat.not_eq_zero_of_lt hn)
[GOAL]
case h.inr.inr.intro
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 ^ (n + 1) < (n + 1) * centralBinom (n + 1)
[PROOFSTEP]
calc
  4 ^ (n + 1) < 4 * (n * centralBinom n) :=
    lt_of_eq_of_lt (pow_succ'' n 4) $
      (mul_lt_mul_left <| zero_lt_four' ℕ).mpr (IH n n.lt_succ_self (Nat.le_of_lt_succ hn))
  _ ≤ 2 * (2 * n + 1) * centralBinom n := by rw [← mul_assoc]; linarith
  _ = (n + 1) * centralBinom (n + 1) := (succ_mul_centralBinom_succ n).symm
[GOAL]
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * (n * centralBinom n) ≤ 2 * (2 * n + 1) * centralBinom n
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
n✝ : ℕ
n_big✝ : 4 ≤ n✝
n : ℕ
IH : ∀ (m : ℕ), m < n + 1 → 4 ≤ m → 4 ^ m < m * centralBinom m
n_big : 4 ≤ n + 1
hn : 4 < n + 1
⊢ 4 * n * centralBinom n ≤ 2 * (2 * n + 1) * centralBinom n
[PROOFSTEP]
linarith
[GOAL]
x✝ : 0 < 1
⊢ 4 ^ 1 ≤ 2 * 1 * centralBinom 1
[PROOFSTEP]
norm_num [centralBinom, choose]
[GOAL]
x✝ : 0 < 2
⊢ 4 ^ 2 ≤ 2 * 2 * centralBinom 2
[PROOFSTEP]
norm_num [centralBinom, choose]
[GOAL]
x✝ : 0 < 3
⊢ 4 ^ 3 ≤ 2 * 3 * centralBinom 3
[PROOFSTEP]
norm_num [centralBinom, choose]
[GOAL]
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * centralBinom (n + 4) ≤ 2 * (n + 4) * centralBinom (n + 4)
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
n : ℕ
x✝ : 0 < n + 4
⊢ (n + 4) * centralBinom (n + 4) ≤ 2 * ((n + 4) * centralBinom (n + 4))
[PROOFSTEP]
refine' le_mul_of_pos_left zero_lt_two
[GOAL]
n : ℕ
⊢ 2 ∣ centralBinom (n + 1)
[PROOFSTEP]
use(n + 1 + n).choose n
[GOAL]
case h
n : ℕ
⊢ centralBinom (n + 1) = 2 * choose (n + 1 + n) n
[PROOFSTEP]
rw [centralBinom_eq_two_mul_choose, two_mul, ← add_assoc, choose_succ_succ' (n + 1 + n) n, choose_symm_add, ← two_mul]
[GOAL]
n : ℕ
h : 0 < n
⊢ 2 ∣ centralBinom n
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos h]
[GOAL]
n : ℕ
h : 0 < n
⊢ 2 ∣ centralBinom (succ (pred n))
[PROOFSTEP]
exact two_dvd_centralBinom_succ n.pred
[GOAL]
n : ℕ
⊢ n + 1 ∣ centralBinom n
[PROOFSTEP]
have h_s : (n + 1).coprime (2 * n + 1) :=
  by
  rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
  exact coprime_one_left n
[GOAL]
n : ℕ
⊢ coprime (n + 1) (2 * n + 1)
[PROOFSTEP]
rw [two_mul, add_assoc, coprime_add_self_right, coprime_self_add_left]
[GOAL]
n : ℕ
⊢ coprime 1 n
[PROOFSTEP]
exact coprime_one_left n
[GOAL]
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ n + 1 ∣ centralBinom n
[PROOFSTEP]
apply h_s.dvd_of_dvd_mul_left
[GOAL]
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ n + 1 ∣ (2 * n + 1) * centralBinom n
[PROOFSTEP]
apply Nat.dvd_of_mul_dvd_mul_left zero_lt_two
[GOAL]
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ 2 * (n + 1) ∣ 2 * ((2 * n + 1) * centralBinom n)
[PROOFSTEP]
rw [← mul_assoc, ← succ_mul_centralBinom_succ, mul_comm]
[GOAL]
n : ℕ
h_s : coprime (n + 1) (2 * n + 1)
⊢ (n + 1) * 2 ∣ (n + 1) * centralBinom (n + 1)
[PROOFSTEP]
exact mul_dvd_mul_left _ (two_dvd_centralBinom_succ n)


[GOAL]
p n k : ℕ
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
by_cases h : (choose n k).factorization p = 0
[GOAL]
case pos
p n k : ℕ
h : ↑(factorization (choose n k)) p = 0
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
simp [h]
[GOAL]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
have hp : p.Prime := Not.imp_symm (choose n k).factorization_eq_zero_of_non_prime h
[GOAL]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
have hkn : k ≤ n := by
  refine' le_of_not_lt fun hnk => h _
  simp [choose_eq_zero_of_lt hnk]
[GOAL]
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
⊢ k ≤ n
[PROOFSTEP]
refine' le_of_not_lt fun hnk => h _
[GOAL]
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
simp [choose_eq_zero_of_lt hnk]
[GOAL]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ ↑(factorization (choose n k)) p ≤ log p n
[PROOFSTEP]
rw [factorization_def _ hp, @padicValNat_def _ ⟨hp⟩ _ (choose_pos hkn)]
[GOAL]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ Part.get (multiplicity p (choose n k)) (_ : multiplicity.Finite p (choose n k)) ≤ log p n
[PROOFSTEP]
simp only [hp.multiplicity_choose hkn (lt_add_one _), PartENat.get_natCast]
[GOAL]
case neg
p n k : ℕ
h : ¬↑(factorization (choose n k)) p = 0
hp : Prime p
hkn : k ≤ n
⊢ Finset.card (Finset.filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Finset.Ico 1 (log p n + 1))) ≤ log p n
[PROOFSTEP]
refine (Finset.card_filter_le _ _).trans (le_of_eq (Nat.card_Ico _ _))
[GOAL]
p n k : ℕ
p_large : n < p ^ 2
⊢ ↑(factorization (choose n k)) p ≤ 1
[PROOFSTEP]
apply factorization_choose_le_log.trans
[GOAL]
p n k : ℕ
p_large : n < p ^ 2
⊢ log p n ≤ 1
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn0)
[GOAL]
case inl
p k : ℕ
p_large : 0 < p ^ 2
⊢ log p 0 ≤ 1
[PROOFSTEP]
simp
[GOAL]
case inr
p n k : ℕ
p_large : n < p ^ 2
hn0 : n ≠ 0
⊢ log p n ≤ 1
[PROOFSTEP]
exact lt_succ_iff.1 (log_lt_of_lt_pow hn0 p_large)
[GOAL]
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
cases' em' p.Prime with hp hp
[GOAL]
case inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : ¬Prime p
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
exact factorization_eq_zero_of_non_prime (choose n k) hp
[GOAL]
case inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
cases' lt_or_le n k with hnk hkn
[GOAL]
case inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
simp [choose_eq_zero_of_lt hnk]
[GOAL]
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
rw [factorization_def _ hp, @padicValNat_def _ ⟨hp⟩ _ (choose_pos hkn)]
[GOAL]
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ Part.get (multiplicity p (choose n k)) (_ : multiplicity.Finite p (choose n k)) = 0
[PROOFSTEP]
simp only [hp.multiplicity_choose hkn (lt_add_one _), PartENat.get_natCast, Finset.card_eq_zero,
  Finset.filter_eq_empty_iff, not_le]
[GOAL]
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
⊢ ∀ (x : ℕ), x ∈ Finset.Ico 1 (log p n + 1) → k % p ^ x + (n - k) % p ^ x < p ^ x
[PROOFSTEP]
intro i hi
[GOAL]
case inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi : i ∈ Finset.Ico 1 (log p n + 1)
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
[PROOFSTEP]
rcases eq_or_lt_of_le (Finset.mem_Ico.mp hi).1 with (rfl | hi)
[GOAL]
case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi : 1 ∈ Finset.Ico 1 (log p n + 1)
⊢ k % p ^ 1 + (n - k) % p ^ 1 < p ^ 1
[PROOFSTEP]
rw [pow_one, ← add_lt_add_iff_left (2 * p), ← succ_mul, two_mul, add_add_add_comm]
[GOAL]
case inr.inr.inl
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi : 1 ∈ Finset.Ico 1 (log p n + 1)
⊢ p + k % p + (p + (n - k) % p) < succ 2 * p
[PROOFSTEP]
exact
  lt_of_le_of_lt
    (add_le_add (add_le_add_right (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk)) (k % p))
      (add_le_add_right (le_mul_of_one_le_right' ((one_le_div_iff hp.pos).mpr hk')) ((n - k) % p)))
    (by rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn])
[GOAL]
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
hi : 1 ∈ Finset.Ico 1 (log p n + 1)
⊢ p * (k / p) + k % p + (p * ((n - k) / p) + (n - k) % p) < succ 2 * p
[PROOFSTEP]
rwa [div_add_mod, div_add_mod, add_tsub_cancel_of_le hkn]
[GOAL]
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
[PROOFSTEP]
replace hn : n < p ^ i
[GOAL]
case hn
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
⊢ n < p ^ i
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
hn : n < p ^ i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
[PROOFSTEP]
have : 3 ≤ p := lt_of_le_of_ne hp.two_le hp'.symm
[GOAL]
case hn
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hn : n < 3 * p
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
this : 3 ≤ p
⊢ n < p ^ i
[PROOFSTEP]
calc
  n < 3 * p := hn
  _ ≤ p * p := (mul_le_mul_right' this p)
  _ = p ^ 2 := (sq p).symm
  _ ≤ p ^ i := pow_le_pow hp.one_lt.le hi
[GOAL]
case inr.inr.inr
p n k : ℕ
hp' : p ≠ 2
hk : p ≤ k
hk' : p ≤ n - k
hp : Prime p
hkn : k ≤ n
i : ℕ
hi✝ : i ∈ Finset.Ico 1 (log p n + 1)
hi : 1 < i
hn : n < p ^ i
⊢ k % p ^ i + (n - k) % p ^ i < p ^ i
[PROOFSTEP]
rwa [mod_eq_of_lt (lt_of_le_of_lt hkn hn), mod_eq_of_lt (lt_of_le_of_lt tsub_le_self hn), add_tsub_cancel_of_le hkn]
[GOAL]
p n k : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ ↑(factorization (centralBinom n)) p = 0
[PROOFSTEP]
refine' factorization_choose_of_lt_three_mul _ p_le_n (p_le_n.trans _) big
[GOAL]
case refine'_1
p n k : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ p ≠ 2
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
n k : ℕ
n_big : 2 < n
p_le_n : 2 ≤ n
big : 2 * n < 3 * 2
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
p n k : ℕ
n_big : 2 < n
p_le_n : p ≤ n
big : 2 * n < 3 * p
⊢ n ≤ 2 * n - n
[PROOFSTEP]
rw [two_mul, add_tsub_cancel_left]
[GOAL]
p n k : ℕ
h : n < p
⊢ ↑(factorization n !) p = 0
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
p n k : ℕ
h✝ : n < p
h : zero < p
⊢ ↑(factorization zero !) p = 0
[PROOFSTEP]
simp
[GOAL]
case succ
p n✝ k : ℕ
h✝ : n✝ < p
n : ℕ
hn : n < p → ↑(factorization n !) p = 0
h : succ n < p
⊢ ↑(factorization (succ n)!) p = 0
[PROOFSTEP]
rw [factorial_succ, factorization_mul n.succ_ne_zero n.factorial_ne_zero, Finsupp.coe_add, Pi.add_apply,
  hn (lt_of_succ_lt h), add_zero, factorization_eq_zero_of_lt h]
[GOAL]
p n k : ℕ
h : n < p
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
by_cases hnk : n < k
[GOAL]
case pos
p n k : ℕ
h : n < p
hnk : n < k
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
simp [choose_eq_zero_of_lt hnk]
[GOAL]
case neg
p n k : ℕ
h : n < p
hnk : ¬n < k
⊢ ↑(factorization (choose n k)) p = 0
[PROOFSTEP]
rw [choose_eq_factorial_div_factorial (le_of_not_lt hnk),
  factorization_div (factorial_mul_factorial_dvd_factorial (le_of_not_lt hnk)), Finsupp.coe_tsub, Pi.sub_apply,
  factorization_factorial_eq_zero_of_lt h, zero_tsub]
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
[PROOFSTEP]
conv =>
  -- Porting note: was `nth_rw_rhs`
  rhs
  rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
| ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
[PROOFSTEP]
  rhs
  rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
| ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
[PROOFSTEP]
  rhs
  rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
| ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p = choose n k
[PROOFSTEP]
rhs
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
| choose n k
[PROOFSTEP]
rw [← factorization_prod_pow_eq_self (choose_pos hkn).ne']
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p =
    Finsupp.prod (factorization (choose n k)) fun x x_1 => x ^ x_1
[PROOFSTEP]
rw [eq_comm]
[GOAL]
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ (Finsupp.prod (factorization (choose n k)) fun x x_1 => x ^ x_1) =
    ∏ p in Finset.range (n + 1), p ^ ↑(factorization (choose n k)) p
[PROOFSTEP]
apply Finset.prod_subset
[GOAL]
case h
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ (factorization (choose n k)).support ⊆ Finset.range (n + 1)
[PROOFSTEP]
intro p hp
[GOAL]
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (factorization (choose n k)).support
⊢ p ∈ Finset.range (n + 1)
[PROOFSTEP]
rw [Finset.mem_range]
[GOAL]
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : p ∈ (factorization (choose n k)).support
⊢ p < n + 1
[PROOFSTEP]
contrapose! hp
[GOAL]
case h
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
hp : n + 1 ≤ p
⊢ ¬p ∈ (factorization (choose n k)).support
[PROOFSTEP]
rw [Finsupp.mem_support_iff, Classical.not_not, factorization_choose_eq_zero_of_lt hp]
[GOAL]
case hf
p n✝ k✝ n k : ℕ
hkn : k ≤ n
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      ¬x ∈ (factorization (choose n k)).support → (fun x x_1 => x ^ x_1) x (↑(factorization (choose n k)) x) = 1
[PROOFSTEP]
intro p _ h2
[GOAL]
case hf
p✝ n✝ k✝ n k : ℕ
hkn : k ≤ n
p : ℕ
a✝ : p ∈ Finset.range (n + 1)
h2 : ¬p ∈ (factorization (choose n k)).support
⊢ (fun x x_1 => x ^ x_1) p (↑(factorization (choose n k)) p) = 1
[PROOFSTEP]
simp [Classical.not_not.1 (mt Finsupp.mem_support_iff.2 h2)]
[GOAL]
p n✝ k n : ℕ
⊢ ∏ p in Finset.range (2 * n + 1), p ^ ↑(factorization (centralBinom n)) p = centralBinom n
[PROOFSTEP]
apply prod_pow_factorization_choose
[GOAL]
case hkn
p n✝ k n : ℕ
⊢ n ≤ 2 * n
[PROOFSTEP]
linarith


[GOAL]
m✝ n✝ m n : ℕ
h : m ≤ n
⊢ m ! ∣ n !
[PROOFSTEP]
induction' n with n IH
[GOAL]
case zero
m✝ n✝ m n : ℕ
h✝ : m ≤ n
h : m ≤ zero
⊢ m ! ∣ zero !
[PROOFSTEP]
simp [Nat.eq_zero_of_le_zero h]
[GOAL]
case succ
m✝ n✝¹ m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
IH : m ≤ n → m ! ∣ n !
h : m ≤ succ n
⊢ m ! ∣ (succ n)!
[PROOFSTEP]
obtain rfl | hl := h.eq_or_lt
[GOAL]
case succ.inl
m n✝¹ n✝ n : ℕ
h✝ : succ n ≤ n✝
IH : succ n ≤ n → (succ n)! ∣ n !
h : succ n ≤ succ n
⊢ (succ n)! ∣ (succ n)!
[PROOFSTEP]
simp
[GOAL]
case succ.inr
m✝ n✝¹ m n✝ : ℕ
h✝ : m ≤ n✝
n : ℕ
IH : m ≤ n → m ! ∣ n !
h : m ≤ succ n
hl : m < succ n
⊢ m ! ∣ (succ n)!
[PROOFSTEP]
exact (IH (le_of_lt_succ hl)).mul_left _
[GOAL]
m✝ n m : ℕ
⊢ m ! * succ m ^ 0 ≤ (m + 0)!
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ m n : ℕ
⊢ m ! * succ m ^ (n + 1) ≤ (m + (n + 1))!
[PROOFSTEP]
rw [← add_assoc, ← Nat.succ_eq_add_one (m + n), Nat.factorial_succ, pow_succ', mul_comm (_ + 1), mul_comm (succ m), ←
  mul_assoc]
[GOAL]
m✝ n✝ m n : ℕ
⊢ m ! * succ m ^ n * succ m ≤ (m + n)! * (m + n + 1)
[PROOFSTEP]
exact
  mul_le_mul factorial_mul_pow_le_factorial (Nat.succ_le_succ (Nat.le_add_right _ _)) (Nat.zero_le _) (Nat.zero_le _)
[GOAL]
m n : ℕ
hn : 0 < n
⊢ n ! < m ! ↔ n < m
[PROOFSTEP]
refine' ⟨fun h => not_le.mp fun hmn => not_le_of_lt h (factorial_le hmn), fun h => _⟩
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
⊢ n ! < m !
[PROOFSTEP]
have : ∀ {n}, 0 < n → n ! < n.succ ! := by
  intro k hk
  rw [factorial_succ, succ_mul, lt_add_iff_pos_left]
  exact mul_pos hk k.factorial_pos
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
⊢ ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
[PROOFSTEP]
intro k hk
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ k ! < (succ k)!
[PROOFSTEP]
rw [factorial_succ, succ_mul, lt_add_iff_pos_left]
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
k : ℕ
hk : 0 < k
⊢ 0 < k * k !
[PROOFSTEP]
exact mul_pos hk k.factorial_pos
[GOAL]
m n : ℕ
hn : 0 < n
h : n < m
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
⊢ n ! < m !
[PROOFSTEP]
induction' h with k hnk ih generalizing hn
[GOAL]
case refl
m n : ℕ
hn✝ : 0 < n
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
hn : 0 < n
⊢ n ! < (succ n)!
[PROOFSTEP]
exact this hn
[GOAL]
case step
m n : ℕ
hn✝ : 0 < n
this : ∀ {n : ℕ}, 0 < n → n ! < (succ n)!
k : ℕ
hnk : Nat.le (succ n) k
ih : 0 < n → n ! < k !
hn : 0 < n
⊢ n ! < (succ k)!
[PROOFSTEP]
exact (ih hn).trans (this <| hn.trans <| lt_of_succ_le hnk)
[GOAL]
m n : ℕ
⊢ n ! = 1 ↔ n ≤ 1
[PROOFSTEP]
apply Iff.intro
[GOAL]
case mp
m n : ℕ
⊢ n ! = 1 → n ≤ 1
[PROOFSTEP]
intro
[GOAL]
case mpr
m n : ℕ
⊢ n ≤ 1 → n ! = 1
[PROOFSTEP]
intro
[GOAL]
case mp
m n : ℕ
a✝ : n ! = 1
⊢ n ≤ 1
[PROOFSTEP]
rw [← not_lt, ← one_lt_factorial, ‹n ! = 1›]
[GOAL]
case mp
m n : ℕ
a✝ : n ! = 1
⊢ ¬1 < 1
[PROOFSTEP]
apply lt_irrefl
[GOAL]
case mpr
m n : ℕ
a✝ : n ≤ 1
⊢ n ! = 1
[PROOFSTEP]
cases ‹n ≤ 1›
[GOAL]
case mpr.refl
m : ℕ
⊢ 1! = 1
[PROOFSTEP]
rfl
[GOAL]
case mpr.step
m n : ℕ
a✝ : Nat.le n 0
⊢ n ! = 1
[PROOFSTEP]
cases ‹n ≤ 0›
[GOAL]
case mpr.step.refl
m : ℕ
⊢ 0! = 1
[PROOFSTEP]
rfl
[GOAL]
m n : ℕ
hn : 1 < n !
⊢ n ! = m ! ↔ n = m
[PROOFSTEP]
refine' ⟨fun h => _, congr_arg _⟩
[GOAL]
m n : ℕ
hn : 1 < n !
h : n ! = m !
⊢ n = m
[PROOFSTEP]
obtain hnm | rfl | hnm := lt_trichotomy n m
[GOAL]
case inl
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : n < m
⊢ n = m
[PROOFSTEP]
rw [← factorial_lt <| pos_of_gt <| one_lt_factorial.mp hn, h] at hnm
[GOAL]
case inl
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m ! < m !
⊢ n = m
[PROOFSTEP]
cases lt_irrefl _ hnm
[GOAL]
case inr.inl
n : ℕ
hn : 1 < n !
h : n ! = n !
⊢ n = n
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
m n : ℕ
hn : 1 < n !
h : n ! = m !
hnm : m < n
⊢ n = m
[PROOFSTEP]
rw [h, one_lt_factorial] at hn
[GOAL]
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m < n
⊢ n = m
[PROOFSTEP]
rw [← factorial_lt (lt_trans one_pos hn), h] at hnm
[GOAL]
case inr.inr
m n : ℕ
hn : 1 < m
h : n ! = m !
hnm : m ! < m !
⊢ n = m
[PROOFSTEP]
cases lt_irrefl _ hnm
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
⊢ n < n !
[PROOFSTEP]
have : 0 < n := (by decide : 0 < 2).trans (succ_le_iff.mp hi)
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
this : 0 < n
⊢ n < n !
[PROOFSTEP]
have : 1 < pred n := le_pred_of_lt (succ_le_iff.mp hi)
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
this✝ : 0 < n
this : 1 < pred n
⊢ n < n !
[PROOFSTEP]
rw [← succ_pred_eq_of_pos ‹0 < n›, factorial_succ]
[GOAL]
m n✝ n : ℕ
hi : 3 ≤ n
this✝ : 0 < n
this : 1 < pred n
⊢ succ (pred n) < (pred n + 1) * (pred n)!
[PROOFSTEP]
exact lt_mul_of_one_lt_right (pred n).succ_pos ((‹1 < pred n›).trans_le (self_le_factorial _))
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
[PROOFSTEP]
rw [← Nat.succ_eq_add_one (i + _), factorial_succ (i + _), add_mul, one_mul]
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
[PROOFSTEP]
have : i ≤ i + n := le.intro rfl
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ i + (n + 1)! < (i + n) * (i + n)! + (i + n)!
[PROOFSTEP]
exact
  add_lt_add_of_lt_of_le
    (this.trans_lt
      ((lt_mul_iff_one_lt_right ((by decide : 0 < 2).trans_le (hi.trans this))).mpr
        (lt_iff_le_and_ne.mpr
          ⟨(i + n).factorial_pos, fun g =>
            Nat.not_succ_le_self 1 ((hi.trans this).trans (factorial_eq_one.mp g.symm))⟩)))
    (factorial_le ((le_of_eq (add_comm n 1)).trans ((add_le_add_iff_right n).mpr ((by decide : 1 ≤ 2).trans hi))))
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
this : i ≤ i + n
⊢ 1 ≤ 2
[PROOFSTEP]
decide
[GOAL]
m n✝ i n : ℕ
hi : 2 ≤ i
hn : 1 ≤ n
⊢ i + n ! < (i + n)!
[PROOFSTEP]
cases hn
[GOAL]
case refl
m n i : ℕ
hi : 2 ≤ i
⊢ i + 1! < (i + 1)!
[PROOFSTEP]
rw [factorial_one]
[GOAL]
case refl
m n i : ℕ
hi : 2 ≤ i
⊢ i + 1 < (i + 1)!
[PROOFSTEP]
exact lt_factorial_self (succ_le_succ hi)
[GOAL]
case step
m n i : ℕ
hi : 2 ≤ i
m✝ : ℕ
a✝ : Nat.le 1 m✝
⊢ i + (succ m✝)! < (i + succ m✝)!
[PROOFSTEP]
exact add_factorial_succ_lt_factorial_add_succ _ hi
[GOAL]
m n✝ i n : ℕ
⊢ i + (n + 1)! ≤ (i + (n + 1))!
[PROOFSTEP]
cases (le_or_lt (2 : ℕ) i)
[GOAL]
case inl
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + (n + 1))!
[PROOFSTEP]
rw [← add_assoc]
[GOAL]
case inl
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! ≤ (i + n + 1)!
[PROOFSTEP]
apply Nat.le_of_lt
[GOAL]
case inl.h
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ i + (n + 1)! < (i + n + 1)!
[PROOFSTEP]
apply add_factorial_succ_lt_factorial_add_succ
[GOAL]
case inl.h.hi
m n✝ i n : ℕ
h✝ : 2 ≤ i
⊢ 2 ≤ i
[PROOFSTEP]
assumption
[GOAL]
case inr
m n✝ i n : ℕ
h✝ : i < 2
⊢ i + (n + 1)! ≤ (i + (n + 1))!
[PROOFSTEP]
match i with
| 0 => simp
|
1 =>
  rw [← add_assoc, ← Nat.succ_eq_add_one (1 + n), factorial_succ (1 + n), add_mul, one_mul, add_comm 1 n,
    add_le_add_iff_right]
  apply one_le_mul
  · apply Nat.le_add_left
  · apply factorial_pos
| succ (succ n) => contradiction
[GOAL]
m n✝ i n : ℕ
h✝ : 0 < 2
⊢ 0 + (n + 1)! ≤ (0 + (n + 1))!
[PROOFSTEP]
simp
[GOAL]
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 + (n + 1)! ≤ (1 + (n + 1))!
[PROOFSTEP]
rw [← add_assoc, ← Nat.succ_eq_add_one (1 + n), factorial_succ (1 + n), add_mul, one_mul, add_comm 1 n,
  add_le_add_iff_right]
[GOAL]
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1) * (n + 1)!
[PROOFSTEP]
apply one_le_mul
[GOAL]
case ha
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ n + 1
[PROOFSTEP]
apply Nat.le_add_left
[GOAL]
case hb
m n✝ i n : ℕ
h✝ : 1 < 2
⊢ 1 ≤ (n + 1)!
[PROOFSTEP]
apply factorial_pos
[GOAL]
m n✝¹ i n✝ n : ℕ
h✝ : succ (succ n) < 2
⊢ succ (succ n) + (n✝ + 1)! ≤ (succ (succ n) + (n✝ + 1))!
[PROOFSTEP]
contradiction
[GOAL]
m n✝ i n : ℕ
n1 : 1 ≤ n
⊢ i + n ! ≤ (i + n)!
[PROOFSTEP]
cases' n1 with h
[GOAL]
case refl
m n i : ℕ
⊢ i + 1! ≤ (i + 1)!
[PROOFSTEP]
exact self_le_factorial _
[GOAL]
case step
m n i h : ℕ
a✝ : Nat.le 1 h
⊢ i + (succ h)! ≤ (i + succ h)!
[PROOFSTEP]
exact add_factorial_succ_le_factorial_add_succ i h
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
⊢ n ! * n ^ (m - n) ≤ m !
[PROOFSTEP]
suffices n ! * (n + 1) ^ (m - n) ≤ m ! from by
  apply LE.le.trans _ this
  apply mul_le_mul_left
  apply pow_le_pow_of_le_left (le_succ n)
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * (n + 1) ^ (m - n) ≤ m !
⊢ n ! * n ^ (m - n) ≤ m !
[PROOFSTEP]
apply LE.le.trans _ this
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * (n + 1) ^ (m - n) ≤ m !
⊢ n ! * n ^ (m - n) ≤ n ! * (n + 1) ^ (m - n)
[PROOFSTEP]
apply mul_le_mul_left
[GOAL]
case h
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * (n + 1) ^ (m - n) ≤ m !
⊢ n ^ (m - n) ≤ (n + 1) ^ (m - n)
[PROOFSTEP]
apply pow_le_pow_of_le_left (le_succ n)
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
⊢ n ! * (n + 1) ^ (m - n) ≤ m !
[PROOFSTEP]
have := @Nat.factorial_mul_pow_le_factorial n (m - n)
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * succ n ^ (m - n) ≤ (n + (m - n))!
⊢ n ! * (n + 1) ^ (m - n) ≤ m !
[PROOFSTEP]
simp [hnm] at this
[GOAL]
m✝ n✝ n m : ℕ
hnm : n ≤ m
this : n ! * succ n ^ (m - n) ≤ m !
⊢ n ! * (n + 1) ^ (m - n) ≤ m !
[PROOFSTEP]
exact this
[GOAL]
k : ℕ
⊢ ascFactorial 0 k = k !
[PROOFSTEP]
induction' k with t ht
[GOAL]
case zero
⊢ ascFactorial 0 zero = zero !
[PROOFSTEP]
rfl
[GOAL]
case succ
t : ℕ
ht : ascFactorial 0 t = t !
⊢ ascFactorial 0 (succ t) = (succ t)!
[PROOFSTEP]
rw [ascFactorial, ht, zero_add, Nat.factorial_succ]
[GOAL]
n : ℕ
⊢ (n + 1) * ascFactorial (succ n) 0 = (n + 0 + 1) * ascFactorial n 0
[PROOFSTEP]
rw [add_zero, ascFactorial_zero, ascFactorial_zero]
[GOAL]
n k : ℕ
⊢ (n + 1) * ascFactorial (succ n) (k + 1) = (n + (k + 1) + 1) * ascFactorial n (k + 1)
[PROOFSTEP]
rw [ascFactorial, mul_left_comm, succ_ascFactorial n k, ascFactorial, succ_add, ← add_assoc, succ_eq_add_one]
[GOAL]
n : ℕ
⊢ n ! * ascFactorial n 0 = (n + 0)!
[PROOFSTEP]
rw [ascFactorial, add_zero, mul_one]
[GOAL]
n k : ℕ
⊢ n ! * ascFactorial n (k + 1) = (n + (k + 1))!
[PROOFSTEP]
rw [ascFactorial_succ, mul_left_comm, factorial_mul_ascFactorial n k, ← add_assoc, ← Nat.succ_eq_add_one (n + k),
  factorial]
[GOAL]
n k : ℕ
⊢ ascFactorial n k = (n + k)! / n !
[PROOFSTEP]
apply mul_left_cancel₀ n.factorial_ne_zero
[GOAL]
n k : ℕ
⊢ n ! * ascFactorial n k = n ! * ((n + k)! / n !)
[PROOFSTEP]
rw [factorial_mul_ascFactorial]
[GOAL]
n k : ℕ
⊢ (n + k)! = n ! * ((n + k)! / n !)
[PROOFSTEP]
exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| le.intro rfl).symm
[GOAL]
n k : ℕ
h : k < n
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
[PROOFSTEP]
let t := n - k.succ
[GOAL]
n k : ℕ
h : k < n
t : ℕ := n - succ k
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
[PROOFSTEP]
let ht : t = n - k.succ := rfl
[GOAL]
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
[PROOFSTEP]
suffices h' : n - k = t.succ
[GOAL]
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
h' : n - k = succ t
⊢ (n - k) * ascFactorial (n - k) k = ascFactorial (n - (k + 1)) (k + 1)
[PROOFSTEP]
rw [← ht, h', succ_ascFactorial, ascFactorial_succ]
[GOAL]
case h'
n k : ℕ
h : k < n
t : ℕ := n - succ k
ht : t = n - succ k := rfl
⊢ n - k = succ t
[PROOFSTEP]
rw [ht, succ_eq_add_one, ← tsub_tsub_assoc (succ_le_of_lt h) (succ_pos _), succ_sub_one]
[GOAL]
n : ℕ
⊢ (n + 1) ^ 0 ≤ ascFactorial n 0
[PROOFSTEP]
rw [ascFactorial_zero, pow_zero]
[GOAL]
n k : ℕ
⊢ (n + 1) ^ (k + 1) ≤ ascFactorial n (k + 1)
[PROOFSTEP]
rw [pow_succ, mul_comm]
[GOAL]
n k : ℕ
⊢ (n + 1) * (n + 1) ^ k ≤ ascFactorial n (k + 1)
[PROOFSTEP]
exact Nat.mul_le_mul (Nat.add_le_add_right le_self_add _) (pow_succ_le_ascFactorial _ k)
[GOAL]
n k : ℕ
⊢ (n + 1) ^ (k + 2) < ascFactorial n (k + 2)
[PROOFSTEP]
rw [pow_succ, ascFactorial, mul_comm]
[GOAL]
n k : ℕ
⊢ (n + 1) * (n + 1) ^ (k + 1) < (n + (k + 1) + 1) * ascFactorial n (k + 1)
[PROOFSTEP]
exact
  Nat.mul_lt_mul (Nat.add_lt_add_right (Nat.lt_add_of_pos_right succ_pos') 1) (pow_succ_le_ascFactorial n _)
    (pow_pos succ_pos' _)
[GOAL]
n : ℕ
⊢ 2 ≤ 0 → (n + 1) ^ 0 < ascFactorial n 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
⊢ 2 ≤ 1 → (n + 1) ^ 1 < ascFactorial n 1
[PROOFSTEP]
intro
[GOAL]
n : ℕ
a✝ : 2 ≤ 1
⊢ (n + 1) ^ 1 < ascFactorial n 1
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
⊢ ascFactorial n 0 ≤ (n + 0) ^ 0
[PROOFSTEP]
rw [ascFactorial_zero, pow_zero]
[GOAL]
n k : ℕ
⊢ ascFactorial n (k + 1) ≤ (n + (k + 1)) ^ (k + 1)
[PROOFSTEP]
rw [ascFactorial_succ, pow_succ, ← add_assoc, ← Nat.succ_eq_add_one (n + k), mul_comm _ (succ (n + k))]
[GOAL]
n k : ℕ
⊢ succ (n + k) * ascFactorial n k ≤ succ (n + k) * succ (n + k) ^ k
[PROOFSTEP]
exact Nat.mul_le_mul_of_nonneg_left ((ascFactorial_le_pow_add _ k).trans (Nat.pow_le_pow_of_le_left (le_succ _) _))
[GOAL]
n : ℕ
⊢ 2 ≤ 0 → ascFactorial n 0 < (n + 0) ^ 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
⊢ 2 ≤ 1 → ascFactorial n 1 < (n + 1) ^ 1
[PROOFSTEP]
intro
[GOAL]
n : ℕ
a✝ : 2 ≤ 1
⊢ ascFactorial n 1 < (n + 1) ^ 1
[PROOFSTEP]
contradiction
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ ascFactorial n (k + 2) < (n + (k + 2)) ^ (k + 2)
[PROOFSTEP]
rw [ascFactorial_succ, pow_succ]
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1) + 1) * ascFactorial n (k + 1) < (n + (k + 2)) ^ (k + 1) * (n + (k + 2))
[PROOFSTEP]
rw [add_assoc n (k + 1) 1, mul_comm <| (n + (k + 2)) ^ (k + 1)]
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
⊢ (n + (k + 1 + 1)) * ascFactorial n (k + 1) < (n + (k + 2)) * (n + (k + 2)) ^ (k + 1)
[PROOFSTEP]
refine'
  Nat.mul_lt_mul' le_rfl ((ascFactorial_le_pow_add n _).trans_lt (pow_lt_pow_of_lt_left (lt_add_one _) (succ_pos _)))
    (succ_pos _)
[GOAL]
k : ℕ
⊢ descFactorial 0 (succ k) = 0
[PROOFSTEP]
rw [descFactorial_succ, zero_tsub, zero_mul]
[GOAL]
n : ℕ
⊢ descFactorial n 1 = n
[PROOFSTEP]
rw [descFactorial_succ, descFactorial_zero, mul_one, tsub_zero]
[GOAL]
n : ℕ
⊢ descFactorial (n + 1) (0 + 1) = (n + 1) * descFactorial n 0
[PROOFSTEP]
rw [descFactorial_zero, descFactorial_one, mul_one]
[GOAL]
n k : ℕ
⊢ descFactorial (n + 1) (succ k + 1) = (n + 1) * descFactorial n (succ k)
[PROOFSTEP]
rw [descFactorial_succ, succ_descFactorial_succ _ k, descFactorial_succ, succ_sub_succ, mul_left_comm]
[GOAL]
n : ℕ
⊢ (n + 1 - 0) * descFactorial (n + 1) 0 = (n + 1) * descFactorial n 0
[PROOFSTEP]
rw [tsub_zero, descFactorial_zero, descFactorial_zero]
[GOAL]
n k : ℕ
⊢ (n + 1 - (k + 1)) * descFactorial (n + 1) (k + 1) = (n + 1) * descFactorial n (k + 1)
[PROOFSTEP]
rw [descFactorial, succ_descFactorial _ k, descFactorial_succ, succ_sub_succ, mul_left_comm]
[GOAL]
⊢ descFactorial 0 0 = 0!
[PROOFSTEP]
rw [descFactorial_zero, factorial_zero]
[GOAL]
n : ℕ
⊢ descFactorial (succ n) (succ n) = (succ n)!
[PROOFSTEP]
rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]
[GOAL]
n : ℕ
⊢ descFactorial n 0 = 0 ↔ n < 0
[PROOFSTEP]
simp only [descFactorial_zero, Nat.one_ne_zero, Nat.not_lt_zero]
[GOAL]
n k : ℕ
⊢ descFactorial n (succ k) = 0 ↔ n < succ k
[PROOFSTEP]
rw [descFactorial_succ, mul_eq_zero, descFactorial_eq_zero_iff_lt, lt_succ_iff, tsub_eq_zero_iff_le, lt_iff_le_and_ne,
  or_iff_left_iff_imp, and_imp]
[GOAL]
n k : ℕ
⊢ n ≤ k → n ≠ k → n ≤ k
[PROOFSTEP]
exact fun h _ => h
[GOAL]
n : ℕ
⊢ descFactorial (n + 0) 0 = ascFactorial n 0
[PROOFSTEP]
rw [ascFactorial_zero, descFactorial_zero]
[GOAL]
n k : ℕ
⊢ descFactorial (n + succ k) (succ k) = ascFactorial n (succ k)
[PROOFSTEP]
rw [Nat.add_succ, Nat.succ_eq_add_one, Nat.succ_eq_add_one, succ_descFactorial_succ, ascFactorial_succ,
  add_descFactorial_eq_ascFactorial _ k]
[GOAL]
n : ℕ
x✝ : 0 ≤ n
⊢ (n - 0)! * descFactorial n 0 = n !
[PROOFSTEP]
rw [descFactorial_zero, mul_one, tsub_zero]
[GOAL]
k : ℕ
h : succ k ≤ 0
⊢ (0 - succ k)! * descFactorial 0 (succ k) = 0!
[PROOFSTEP]
exfalso
[GOAL]
case h
k : ℕ
h : succ k ≤ 0
⊢ False
[PROOFSTEP]
exact not_succ_le_zero k h
[GOAL]
n k : ℕ
h : succ k ≤ succ n
⊢ (succ n - succ k)! * descFactorial (succ n) (succ k) = (succ n)!
[PROOFSTEP]
rw [succ_descFactorial_succ, succ_sub_succ, ← mul_assoc, mul_comm (n - k)!, mul_assoc,
  factorial_mul_descFactorial (Nat.succ_le_succ_iff.1 h), factorial_succ]
[GOAL]
n k : ℕ
h : k ≤ n
⊢ descFactorial n k = n ! / (n - k)!
[PROOFSTEP]
apply mul_left_cancel₀ (factorial_ne_zero (n - k))
[GOAL]
n k : ℕ
h : k ≤ n
⊢ (n - k)! * descFactorial n k = (n - k)! * (n ! / (n - k)!)
[PROOFSTEP]
rw [factorial_mul_descFactorial h]
[GOAL]
n k : ℕ
h : k ≤ n
⊢ n ! = (n - k)! * (n ! / (n - k)!)
[PROOFSTEP]
exact (Nat.mul_div_cancel' <| factorial_dvd_factorial <| Nat.sub_le n k).symm
[GOAL]
n : ℕ
⊢ (n + 1 - 0) ^ 0 ≤ descFactorial n 0
[PROOFSTEP]
rw [descFactorial_zero, pow_zero]
[GOAL]
n k : ℕ
⊢ (n + 1 - (k + 1)) ^ (k + 1) ≤ descFactorial n (k + 1)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ, succ_sub_succ, mul_comm]
[GOAL]
n k : ℕ
⊢ (n - k) * (n - k) ^ k ≤ (n - k) * descFactorial n k
[PROOFSTEP]
apply Nat.mul_le_mul_of_nonneg_left
[GOAL]
case h₁
n k : ℕ
⊢ (n - k) ^ k ≤ descFactorial n k
[PROOFSTEP]
exact (le_trans (Nat.pow_le_pow_of_le_left (tsub_le_tsub_right (le_succ _) _) k) (pow_sub_le_descFactorial n k))
[GOAL]
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) ^ (0 + 2) < descFactorial n (0 + 2)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ, pow_one, descFactorial_one]
[GOAL]
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n
[PROOFSTEP]
exact Nat.mul_lt_mul_of_pos_left (tsub_lt_self (lt_of_lt_of_le zero_lt_two h) zero_lt_one) (tsub_pos_of_lt h)
[GOAL]
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < descFactorial n (k + 1 + 2)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ, mul_comm]
[GOAL]
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * descFactorial n (k + 2)
[PROOFSTEP]
apply Nat.mul_lt_mul_of_pos_left
[GOAL]
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
refine' ((Nat.pow_le_pow_of_le_left (tsub_le_tsub_right (le_succ n) _) _).trans_lt _)
[GOAL]
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (succ n - (k + 1 + 1)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
rw [succ_sub_succ]
[GOAL]
case h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
exact pow_sub_lt_descFactorial' ((le_succ _).trans h)
[GOAL]
case hk
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ n - (k + 1 + 1) > 0
[PROOFSTEP]
apply tsub_pos_of_lt
[GOAL]
case hk.h
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ k + 1 + 1 < n
[PROOFSTEP]
apply h
[GOAL]
n : ℕ
⊢ 2 ≤ 0 → 0 ≤ n → (n + 1 - 0) ^ 0 < descFactorial n 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
⊢ 2 ≤ 1 → 1 ≤ n → (n + 1 - 1) ^ 1 < descFactorial n 1
[PROOFSTEP]
intro
[GOAL]
n : ℕ
a✝ : 2 ≤ 1
⊢ 1 ≤ n → (n + 1 - 1) ^ 1 < descFactorial n 1
[PROOFSTEP]
contradiction
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n + 1 - (k + 2)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
rw [succ_sub_succ]
[GOAL]
n k : ℕ
x✝ : 2 ≤ k + 2
h : k + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < descFactorial n (k + 2)
[PROOFSTEP]
exact pow_sub_lt_descFactorial' h
[GOAL]
n : ℕ
⊢ descFactorial n 0 ≤ n ^ 0
[PROOFSTEP]
rw [descFactorial_zero, pow_zero]
[GOAL]
n k : ℕ
⊢ descFactorial n (k + 1) ≤ n ^ (k + 1)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ, mul_comm _ n]
[GOAL]
n k : ℕ
⊢ (n - k) * descFactorial n k ≤ n * n ^ k
[PROOFSTEP]
exact Nat.mul_le_mul (Nat.sub_le _ _) (descFactorial_le_pow _ k)
[GOAL]
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ 0 → descFactorial n 0 < n ^ 0
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
n : ℕ
hn : 1 ≤ n
⊢ 2 ≤ 1 → descFactorial n 1 < n ^ 1
[PROOFSTEP]
intro
[GOAL]
n : ℕ
hn : 1 ≤ n
a✝ : 2 ≤ 1
⊢ descFactorial n 1 < n ^ 1
[PROOFSTEP]
contradiction
[GOAL]
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ descFactorial n (k + 2) < n ^ (k + 2)
[PROOFSTEP]
rw [descFactorial_succ, pow_succ', mul_comm, mul_comm n]
[GOAL]
n : ℕ
hn : 1 ≤ n
k : ℕ
x✝ : 2 ≤ k + 2
⊢ descFactorial n (k + 1) * (n - (k + 1)) < n ^ (k + 1) * n
[PROOFSTEP]
exact Nat.mul_lt_mul' (descFactorial_le_pow _ _) (tsub_lt_self hn k.zero_lt_succ) (pow_pos (Nat.lt_of_succ_le hn) _)


[GOAL]
ι : Type u_1
x : ℕ
s : ι → ℕ
t : Finset ι
⊢ (fun y => coprime y x) 1
[PROOFSTEP]
simp
[GOAL]
ι : Type u_1
x : ℕ
s : ι → ℕ
t : Finset ι
⊢ (fun y => coprime x y) 1
[PROOFSTEP]
simp


[GOAL]
n : ℕ
⊢ (n + 1)‼ = (n + 1) * (n - 1)‼
[PROOFSTEP]
cases n
[GOAL]
case zero
⊢ (zero + 1)‼ = (zero + 1) * (zero - 1)‼
[PROOFSTEP]
rfl
[GOAL]
case succ
n✝ : ℕ
⊢ (succ n✝ + 1)‼ = (succ n✝ + 1) * (succ n✝ - 1)‼
[PROOFSTEP]
rfl
[GOAL]
k : ℕ
⊢ (k + 1 + 1)! = (k + 1 + 1)‼ * (k + 1)‼
[PROOFSTEP]
rw [doubleFactorial_add_two, factorial, factorial_eq_mul_doubleFactorial _, mul_comm _ k‼, mul_assoc]
[GOAL]
n : ℕ
⊢ (2 * (n + 1))‼ = 2 ^ (n + 1) * (n + 1)!
[PROOFSTEP]
rw [mul_add, mul_one, doubleFactorial_add_two, factorial, pow_succ, doubleFactorial_two_mul _, succ_eq_add_one]
[GOAL]
n : ℕ
⊢ (2 * n + 2) * (2 ^ n * n !) = 2 ^ n * 2 * ((n + 1) * n !)
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ (2 * (n + 1))‼ = ∏ i in Finset.range (n + 1), 2 * (i + 1)
[PROOFSTEP]
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_even _, mul_comm (2 * n)‼, (by ring : 2 * (n + 1) = 2 * n + 2)]
[GOAL]
n : ℕ
⊢ 2 * (n + 1) = 2 * n + 2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ (2 * n + 2)‼ = (2 * n + 2) * (2 * n)‼
[PROOFSTEP]
rfl
[GOAL]
n : ℕ
⊢ (2 * (n + 1) + 1)‼ = ∏ i in Finset.range (n + 1), (2 * (i + 1) + 1)
[PROOFSTEP]
rw [Finset.prod_range_succ, ← doubleFactorial_eq_prod_odd _, mul_comm (2 * n + 1)‼,
  (by ring : 2 * (n + 1) + 1 = 2 * n + 1 + 2)]
[GOAL]
n : ℕ
⊢ 2 * (n + 1) + 1 = 2 * n + 1 + 2
[PROOFSTEP]
ring
[GOAL]
n : ℕ
⊢ (2 * n + 1 + 2)‼ = (2 * n + 1 + 2) * (2 * n + 1)‼
[PROOFSTEP]
rfl