[GOAL]
x✝¹ x✝ : ℕ
⊢ (fun m n => m * n) (x✝¹ + 1) x✝ = x✝ + (fun m n => m * n) x✝¹ x✝
[PROOFSTEP]
dsimp only
[GOAL]
x✝¹ x✝ : ℕ
⊢ (x✝¹ + 1) * x✝ = x✝ + x✝¹ * x✝
[PROOFSTEP]
rw [Nat.add_comm, Nat.right_distrib, Nat.one_mul]
[GOAL]
m n k : ℕ
p : ℕ → Prop
⊢ (∃ n, p n) → p 0 ∨ ∃ n, p (n + 1)
[PROOFSTEP]
rintro ⟨_ | n, hn⟩
[GOAL]
case intro.zero
m n k : ℕ
p : ℕ → Prop
hn : p zero
⊢ p 0 ∨ ∃ n, p (n + 1)
case intro.succ m n✝ k : ℕ p : ℕ → Prop n : ℕ hn : p (succ n) ⊢ p 0 ∨ ∃ n, p (n + 1)
[PROOFSTEP]
exacts [Or.inl hn, Or.inr ⟨n, hn⟩]
[GOAL]
m✝ n✝ k m n : ℕ
⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
by_cases h1 : m ≤ n
[GOAL]
case pos
m✝ n✝ k m n : ℕ
h1 : m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)
case neg m✝ n✝ k m n : ℕ h1 : ¬m ≤ n ⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
rw [max_eq_right h1, max_eq_right (succ_le_succ h1)]
[GOAL]
case neg
m✝ n✝ k m n : ℕ
h1 : ¬m ≤ n
⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
rw [not_le] at h1 
[GOAL]
case neg
m✝ n✝ k m n : ℕ
h1 : n < m
⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
have h2 := le_of_lt h1
[GOAL]
case neg
m✝ n✝ k m n : ℕ
h1 : n < m
h2 : n ≤ m
⊢ max (succ m) (succ n) = succ (max m n)
[PROOFSTEP]
rw [max_eq_left h2, max_eq_left (succ_le_succ h2)]
[GOAL]
m✝ n✝ k m n : ℕ
⊢ m < n ↔ m + 1 ≤ n
[PROOFSTEP]
rw [succ_le_iff]
[GOAL]
m n k a b : ℕ
⊢ a < 1 + b ↔ a ≤ b
[PROOFSTEP]
simp only [add_comm, lt_succ_iff]
[GOAL]
m n k a b : ℕ
⊢ 1 + a ≤ b ↔ a < b
[PROOFSTEP]
simp only [add_comm, add_one_le_iff]
[GOAL]
m✝ n✝ k✝ m n k : ℕ
n0 : 0 < n
⊢ m / n ≤ k ↔ m ≤ n * k + (n - 1)
[PROOFSTEP]
rw [← lt_succ_iff, div_lt_iff_lt_mul n0, succ_mul, mul_comm]
[GOAL]
m✝ n✝ k✝ m n k : ℕ
n0 : 0 < n
⊢ m < n * k + n ↔ m ≤ n * k + (n - 1)
[PROOFSTEP]
cases n
[GOAL]
case zero
m✝ n k✝ m k : ℕ
n0 : 0 < zero
⊢ m < zero * k + zero ↔ m ≤ zero * k + (zero - 1)
[PROOFSTEP]
cases n0
[GOAL]
case succ
m✝ n k✝ m k n✝ : ℕ
n0 : 0 < succ n✝
⊢ m < succ n✝ * k + succ n✝ ↔ m ≤ succ n✝ * k + (succ n✝ - 1)
[PROOFSTEP]
exact lt_succ_iff
[GOAL]
m n✝ k n : ℕ
x✝² : n + 3 ≠ 0
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
⊢ 2 < n + 3
[PROOFSTEP]
rw [Nat.lt_iff_add_one_le]
[GOAL]
m n✝ k n : ℕ
x✝² : n + 3 ≠ 0
x✝¹ : n + 3 ≠ 1
x✝ : n + 3 ≠ 2
⊢ 2 + 1 ≤ n + 3
[PROOFSTEP]
convert Nat.le_add_left 3 n
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n + 1 → P m) ↔ (∀ (m : ℕ), m < n → P m) ∧ P n
[PROOFSTEP]
simp only [lt_succ_iff, Decidable.le_iff_eq_or_lt, forall_eq_or_imp, and_comm]
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∃ m, m < n + 1 ∧ P m) ↔ (∃ m, m < n ∧ P m) ∨ P n
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (¬∃ m, m < n + 1 ∧ P m) ↔ ¬((∃ m, m < n ∧ P m) ∨ P n)
[PROOFSTEP]
push_neg
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
n : ℕ
⊢ (∀ (m : ℕ), m < n + 1 → ¬P m) ↔ (∀ (m : ℕ), m < n → ¬P m) ∧ ¬P n
[PROOFSTEP]
exact forall_lt_succ
[GOAL]
m n k : ℕ
h : m < n
⊢ n = m + (n - (m + 1)) + 1
[PROOFSTEP]
rw [add_right_comm, add_sub_of_le h]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ n + succ m - 1 = n + m
[PROOFSTEP]
rw [add_succ, succ_sub_one]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ succ n + m - 1 = n + m
[PROOFSTEP]
rw [succ_add, succ_sub_one]
[GOAL]
m✝ n✝ k m n : ℕ
H : m = succ n
⊢ pred m = n
[PROOFSTEP]
simp [H]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ pred n = succ m ↔ n = m + 2
[PROOFSTEP]
cases n
[GOAL]
case zero
m✝ n k m : ℕ
⊢ pred zero = succ m ↔ zero = m + 2
[PROOFSTEP]
constructor
[GOAL]
case succ
m✝ n k m n✝ : ℕ
⊢ pred (succ n✝) = succ m ↔ succ n✝ = m + 2
[PROOFSTEP]
constructor
[GOAL]
case zero.mp
m✝ n k m : ℕ
⊢ pred zero = succ m → zero = m + 2
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case zero.mpr
m✝ n k m : ℕ
⊢ zero = m + 2 → pred zero = succ m
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case succ.mp
m✝ n k m n✝ : ℕ
⊢ pred (succ n✝) = succ m → succ n✝ = m + 2
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case succ.mpr
m✝ n k m n✝ : ℕ
⊢ succ n✝ = m + 2 → pred (succ n✝) = succ m
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case succ.mp.refl
m✝ n k m : ℕ
⊢ succ (succ m) = m + 2
[PROOFSTEP]
rfl
[GOAL]
case succ.mpr.refl
m✝ n k m : ℕ
⊢ pred (succ (Nat.add m 1)) = succ m
[PROOFSTEP]
rfl
[GOAL]
m✝ n✝ k n m : ℕ
⊢ pred n - m = pred (n - m)
[PROOFSTEP]
rw [← Nat.sub_one, Nat.sub_sub, one_add, sub_succ]
[GOAL]
m n✝ k n : ℕ
⊢ pred (1 + n) = n
[PROOFSTEP]
rw [add_comm, add_one, Nat.pred_succ]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ ¬2 * n % 2 = (2 * m + 1) % 2
[PROOFSTEP]
rw [add_comm, add_mul_mod_self_left, mul_mod_right, mod_eq_of_lt]
[GOAL]
m✝ n✝ k n m : ℕ
⊢ ¬0 = 1
[PROOFSTEP]
simp
[GOAL]
m✝ n✝ k n m : ℕ
⊢ 1 < 2
[PROOFSTEP]
simp
[GOAL]
m n k a b : ℕ
ha : 0 < a
this : a * b = a * 1 ↔ b = 1
⊢ a * b = a ↔ b = 1
[PROOFSTEP]
rwa [mul_one] at this 
[GOAL]
m n k a b : ℕ
hb : 0 < b
⊢ a * b = b ↔ a = 1
[PROOFSTEP]
rw [mul_comm, Nat.mul_right_eq_self_iff hb]
[GOAL]
m n✝ k : ℕ
C : ℕ → Sort u
n : ℕ
h : n ≤ n
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h (fun {k} => next) x = x
[PROOFSTEP]
cases n
[GOAL]
case zero
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
h : zero ≤ zero
x : C zero
⊢ leRecOn h (fun {k} => next) x = x
[PROOFSTEP]
unfold leRecOn Eq.recOn
[GOAL]
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ leRecOn h (fun {k} => next) x = x
[PROOFSTEP]
unfold leRecOn Eq.recOn
[GOAL]
case zero
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
h : zero ≤ zero
x : C zero
⊢ (_ : zero = 0) ▸ x = x
[PROOFSTEP]
simp
[GOAL]
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ (Or.by_cases (_ : succ n✝ ≤ n✝ ∨ succ n✝ = succ n✝) (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x))
      fun h => h ▸ x) =
    x
[PROOFSTEP]
unfold Or.by_cases
[GOAL]
case succ
m n k : ℕ
C : ℕ → Sort u
next : {k : ℕ} → C k → C (k + 1)
n✝ : ℕ
h : succ n✝ ≤ succ n✝
x : C (succ n✝)
⊢ (if hp : succ n✝ ≤ n✝ then (fun h => (fun {k} => next) (leRecOn h (fun {k} => next) x)) hp
    else (fun h => h ▸ x) (_ : succ n✝ = succ n✝)) =
    x
[PROOFSTEP]
rw [dif_neg (Nat.not_succ_le_self _)]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h2 next x = next (leRecOn h1 next x)
[PROOFSTEP]
conv =>
  lhs
  rw [leRecOn, Or.by_cases, dif_pos h1]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
| leRecOn h2 next x = next (leRecOn h1 next x)
[PROOFSTEP]
  lhs
  rw [leRecOn, Or.by_cases, dif_pos h1]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
| leRecOn h2 next x = next (leRecOn h1 next x)
[PROOFSTEP]
  lhs
  rw [leRecOn, Or.by_cases, dif_pos h1]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
| leRecOn h2 next x = next (leRecOn h1 next x)
[PROOFSTEP]
lhs
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n ≤ m + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
| leRecOn h2 next x
[PROOFSTEP]
rw [leRecOn, Or.by_cases, dif_pos h1]
[GOAL]
m n✝ k : ℕ
C : ℕ → Sort u
n : ℕ
h : n ≤ n + 1
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h (fun {k} => next) x = next x
[PROOFSTEP]
rw [leRecOn_succ (le_refl n), leRecOn_self]
[GOAL]
m✝ n✝ k✝ : ℕ
C : ℕ → Sort u
n m k : ℕ
hnm : n ≤ m
hmk : m ≤ k
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)
[PROOFSTEP]
induction' hmk with k hmk ih
[GOAL]
case refl
m✝ n✝ k✝ : ℕ
C : ℕ → Sort u
n m k : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn (_ : n ≤ m) next x = leRecOn (_ : Nat.le m m) next (leRecOn hnm next x)
[PROOFSTEP]
rw [leRecOn_self]
[GOAL]
case step
m✝ n✝ k✝¹ : ℕ
C : ℕ → Sort u
n m k✝ : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
x : C n
k : ℕ
hmk : Nat.le m k
ih : leRecOn (_ : n ≤ k) next x = leRecOn hmk next (leRecOn hnm next x)
⊢ leRecOn (_ : n ≤ succ k) next x = leRecOn (_ : Nat.le m (succ k)) next (leRecOn hnm next x)
[PROOFSTEP]
rw [leRecOn_succ (le_trans hnm hmk), ih, leRecOn_succ]
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
h1 : n ≤ m
h2 : n + 1 ≤ m
next : {k : ℕ} → C k → C (k + 1)
x : C n
⊢ leRecOn h2 (fun {k} => next) (next x) = leRecOn h1 (fun {k} => next) x
[PROOFSTEP]
rw [Subsingleton.elim h1 (le_trans (le_succ n) h2), leRecOn_trans (le_succ n) h2, leRecOn_succ']
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
⊢ Function.Injective (leRecOn hnm fun {k} => next)
[PROOFSTEP]
induction' hnm with m hnm ih
[GOAL]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
⊢ Function.Injective (leRecOn (_ : Nat.le n n) fun {k} => next)
[PROOFSTEP]
intro x y H
[GOAL]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
x y : C n
H : leRecOn (_ : Nat.le n n) (fun {k} => next) x = leRecOn (_ : Nat.le n n) (fun {k} => next) y
⊢ x = y
[PROOFSTEP]
rwa [leRecOn_self, leRecOn_self] at H 
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
⊢ Function.Injective (leRecOn (_ : Nat.le n (succ m)) fun {k} => next)
[PROOFSTEP]
intro x y H
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
x y : C n
H : leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) x = leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) y
⊢ x = y
[PROOFSTEP]
rw [leRecOn_succ hnm, leRecOn_succ hnm] at H 
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Injective next
m : ℕ
hnm : Nat.le n m
ih : Function.Injective (leRecOn hnm fun {k} => next)
x y : C n
H : next (leRecOn hnm (fun {k} => next) x) = next (leRecOn hnm (fun {k} => next) y)
⊢ x = y
[PROOFSTEP]
exact ih (Hnext _ H)
[GOAL]
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
hnm : n ≤ m
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
⊢ Function.Surjective (leRecOn hnm fun {k} => next)
[PROOFSTEP]
induction' hnm with m hnm ih
[GOAL]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
⊢ Function.Surjective (leRecOn (_ : Nat.le n n) fun {k} => next)
[PROOFSTEP]
intro x
[GOAL]
case refl
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
x : C n
⊢ ∃ a, leRecOn (_ : Nat.le n n) (fun {k} => next) a = x
[PROOFSTEP]
use x
[GOAL]
case h
m✝ n✝ k : ℕ
C : ℕ → Sort u
n m : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
x : C n
⊢ leRecOn (_ : Nat.le n n) (fun {k} => next) x = x
[PROOFSTEP]
rw [leRecOn_self]
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
⊢ Function.Surjective (leRecOn (_ : Nat.le n (succ m)) fun {k} => next)
[PROOFSTEP]
intro x
[GOAL]
case step
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C (succ m)
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = x
[PROOFSTEP]
rcases Hnext _ x with ⟨w, rfl⟩
[GOAL]
case step.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
w : C m
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = next w
[PROOFSTEP]
rcases ih w with ⟨x, rfl⟩
[GOAL]
case step.intro.intro
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ ∃ a, leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) a = next (leRecOn hnm (fun {k} => next) x)
[PROOFSTEP]
use x
[GOAL]
case h
m✝¹ n✝ k : ℕ
C : ℕ → Sort u
n m✝ : ℕ
next : {k : ℕ} → C k → C (k + 1)
Hnext : ∀ (n : ℕ), Function.Surjective next
m : ℕ
hnm : Nat.le n m
ih : Function.Surjective (leRecOn hnm fun {k} => next)
x : C n
⊢ leRecOn (_ : Nat.le n (succ m)) (fun {k} => next) x = next (leRecOn hnm (fun {k} => next) x)
[PROOFSTEP]
rw [leRecOn_succ]
[GOAL]
m n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n
n : ℕ
⊢ strongRecOn' n h = h n fun m x => strongRecOn' m h
[PROOFSTEP]
simp only [strongRecOn']
[GOAL]
m n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n
n : ℕ
⊢ Nat.strongRec' h n = h n fun m x => Nat.strongRec' h m
[PROOFSTEP]
rw [Nat.strongRec']
[GOAL]
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ ∀ (n : ℕ) (hn : m ≤ n), P n hn
[PROOFSTEP]
apply Nat.le.rec
[GOAL]
case refl
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ P m (_ : Nat.le m m)
[PROOFSTEP]
exact base
[GOAL]
case step
m✝ n k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
⊢ ∀ {m_1 : ℕ} (a : Nat.le m m_1), P m_1 a → P (Nat.succ m_1) (_ : Nat.le m (Nat.succ m_1))
[PROOFSTEP]
intros n hn
[GOAL]
case step
m✝ n✝ k m : ℕ
P : (n : ℕ) → m ≤ n → Prop
base : P m (_ : m ≤ m)
succ : ∀ (n : ℕ) (hn : m ≤ n), P n hn → P (n + 1) (_ : m ≤ n + 1)
n : ℕ
hn : Nat.le m n
⊢ P n hn → P (Nat.succ n) (_ : Nat.le m (Nat.succ n))
[PROOFSTEP]
apply succ n hn
[GOAL]
m n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
n : ℕ
nn : n ≤ n
hP : P n
⊢ decreasingInduction h nn hP = hP
[PROOFSTEP]
dsimp only [decreasingInduction]
[GOAL]
m n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
n : ℕ
nn : n ≤ n
hP : P n
⊢ leRecOn nn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) hP = hP
[PROOFSTEP]
rw [leRecOn_self]
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
mn : m ≤ n
msn : m ≤ n + 1
hP : P (n + 1)
⊢ decreasingInduction h msn hP = decreasingInduction h mn (h n hP)
[PROOFSTEP]
dsimp only [decreasingInduction]
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
mn : m ≤ n
msn : m ≤ n + 1
hP : P (n + 1)
⊢ leRecOn msn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) hP =
    leRecOn mn (fun {k} ih hsk => ih (h k hsk)) (fun h => h) (h n hP)
[PROOFSTEP]
rw [leRecOn_succ]
[GOAL]
m✝ n k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m : ℕ
msm : m ≤ m + 1
hP : P (m + 1)
⊢ decreasingInduction h msm hP = h m hP
[PROOFSTEP]
dsimp only [decreasingInduction]
[GOAL]
m✝ n k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m : ℕ
msm : m ≤ m + 1
hP : P (m + 1)
⊢ leRecOn msm (fun {k} ih hsk => ih (h k hsk)) (fun h => h) hP = h m hP
[PROOFSTEP]
rw [leRecOn_succ']
[GOAL]
m✝ n✝ k✝ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k : ℕ
mn : m ≤ n
nk : n ≤ k
hP : P k
⊢ decreasingInduction h (_ : m ≤ k) hP = decreasingInduction h mn (decreasingInduction h nk hP)
[PROOFSTEP]
induction' nk with k nk ih
[GOAL]
case refl
m✝ n✝ k✝ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k : ℕ
mn : m ≤ n
hP✝ : P k
hP : P n
⊢ decreasingInduction h (_ : m ≤ n) hP = decreasingInduction h mn (decreasingInduction h (_ : Nat.le n n) hP)
[PROOFSTEP]
rw [decreasingInduction_self]
[GOAL]
case step
m✝ n✝ k✝¹ : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n k✝ : ℕ
mn : m ≤ n
hP✝ : P k✝
k : ℕ
nk : Nat.le n k
ih : ∀ (hP : P k), decreasingInduction h (_ : m ≤ k) hP = decreasingInduction h mn (decreasingInduction h nk hP)
hP : P (succ k)
⊢ decreasingInduction h (_ : m ≤ succ k) hP =
    decreasingInduction h mn (decreasingInduction h (_ : Nat.le n (succ k)) hP)
[PROOFSTEP]
rw [decreasingInduction_succ h (le_trans mn nk), ih, decreasingInduction_succ]
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
smn : m + 1 ≤ n
mn : m ≤ n
hP : P n
⊢ decreasingInduction h mn hP = h m (decreasingInduction h smn hP)
[PROOFSTEP]
rw [Subsingleton.elim mn (le_trans (le_succ m) smn), decreasingInduction_trans, decreasingInduction_succ']
[GOAL]
case msm
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
h : (n : ℕ) → P (n + 1) → P n
m n : ℕ
smn : m + 1 ≤ n
mn : m ≤ n
hP : P n
⊢ m ≤ m + 1
[PROOFSTEP]
apply Nat.le_succ
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
h : (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
mn : m ≤ n
hP : P n
⊢ P m
[PROOFSTEP]
revert h hP
[GOAL]
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
mn : m ≤ n
⊢ ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → P n → P m
[PROOFSTEP]
refine' leRecOn' mn _ _
[GOAL]
case refine'_1
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
mn : m ≤ n
⊢ ⦃k : ℕ⦄ →
    m ≤ k →
      (((k_1 : ℕ) → k_1 < k → m ≤ k_1 → P (k_1 + 1) → P k_1) → P k → P m) →
        ((k_1 : ℕ) → k_1 < k + 1 → m ≤ k_1 → P (k_1 + 1) → P k_1) → P (k + 1) → P m
[PROOFSTEP]
intro n mn ih h hP
[GOAL]
case refine'_1
m✝ n✝¹ k : ℕ
P : ℕ → Sort u_1
m n✝ : ℕ
mn✝ : m ≤ n✝
n : ℕ
mn : m ≤ n
ih : ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → P n → P m
h : (k : ℕ) → k < n + 1 → m ≤ k → P (k + 1) → P k
hP : P (n + 1)
⊢ P m
[PROOFSTEP]
apply ih
[GOAL]
case refine'_1.h
m✝ n✝¹ k : ℕ
P : ℕ → Sort u_1
m n✝ : ℕ
mn✝ : m ≤ n✝
n : ℕ
mn : m ≤ n
ih : ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → P n → P m
h : (k : ℕ) → k < n + 1 → m ≤ k → P (k + 1) → P k
hP : P (n + 1)
⊢ (k : ℕ) → k < n → m ≤ k → P (k + 1) → P k
[PROOFSTEP]
exact fun k hk => h k (Nat.lt.step hk)
[GOAL]
case refine'_1.hP
m✝ n✝¹ k : ℕ
P : ℕ → Sort u_1
m n✝ : ℕ
mn✝ : m ≤ n✝
n : ℕ
mn : m ≤ n
ih : ((k : ℕ) → k < n → m ≤ k → P (k + 1) → P k) → P n → P m
h : (k : ℕ) → k < n + 1 → m ≤ k → P (k + 1) → P k
hP : P (n + 1)
⊢ P n
[PROOFSTEP]
exact h n (lt_succ_self n) mn hP
[GOAL]
case refine'_2
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
mn : m ≤ n
⊢ ((k : ℕ) → k < m → m ≤ k → P (k + 1) → P k) → P m → P m
[PROOFSTEP]
intro _ hP
[GOAL]
case refine'_2
m✝ n✝ k : ℕ
P : ℕ → Sort u_1
m n : ℕ
mn : m ≤ n
h✝ : (k : ℕ) → k < m → m ≤ k → P (k + 1) → P k
hP : P m
⊢ P m
[PROOFSTEP]
exact hP
[GOAL]
m n k a b : ℕ
hb : 0 < b
⊢ 1 ≤ a / b ↔ b ≤ a
[PROOFSTEP]
rw [le_div_iff_mul_le hb, one_mul]
[GOAL]
m✝ n✝ k✝ n m : ℕ
h : n ≤ m
k : ℕ
k0 : k = 0
⊢ n / k ≤ m / k
[PROOFSTEP]
simp [k0]
[GOAL]
m n k a b : ℕ
hba : b ≤ a
hb : 0 < b
h : a / b = 0
⊢ a = a % b
[PROOFSTEP]
simpa [h] using (mod_add_div a b).symm
[GOAL]
m n k a b c : ℕ
hc0 : c = 0
⊢ a * (b / c) ≤ a * b / c
[PROOFSTEP]
simp [hc0]
[GOAL]
m n k a b c : ℕ
hc0 : ¬c = 0
⊢ a * (b / c) * c ≤ a * b
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
m n k a b c : ℕ
hc0 : ¬c = 0
⊢ a * (b / c * c) ≤ a * b
[PROOFSTEP]
exact Nat.mul_le_mul_left _ (Nat.div_mul_le_self _ _)
[GOAL]
m n k a b c : ℕ
H1 : b ∣ a
H2 : a / b = c
⊢ a = b * c
[PROOFSTEP]
rw [← H2, Nat.mul_div_cancel' H1]
[GOAL]
m n k a b c : ℕ
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = c * b
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m n k a b c : ℕ
H : 0 < b
H' : b ∣ a
⊢ a / b = c ↔ a = b * c
[PROOFSTEP]
exact Nat.div_eq_iff_eq_mul_right H H'
[GOAL]
m n k a b c : ℕ
H1 : b ∣ a
H2 : a / b = c
⊢ a = c * b
[PROOFSTEP]
rw [mul_comm, Nat.eq_mul_of_div_eq_right H1 H2]
[GOAL]
m n k a b : ℕ
Hd : a ∣ b
⊢ a * (b / a) = b
[PROOFSTEP]
rw [mul_comm, Nat.div_mul_cancel Hd]
[GOAL]
m n k a b : ℕ
hb : 0 < b
⊢ a < a / b * b + b
[PROOFSTEP]
rw [← Nat.succ_mul, ← Nat.div_lt_iff_lt_mul hb]
[GOAL]
m n k a b : ℕ
hb : 0 < b
⊢ a / b < succ (a / b)
[PROOFSTEP]
exact Nat.lt_succ_self _
[GOAL]
m n k a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
⊢ a / d = b / d ↔ a = b
[PROOFSTEP]
refine ⟨fun h => ?_, congr_arg fun n => n / d⟩
[GOAL]
m n k a b d : ℕ
hda : d ∣ a
hdb : d ∣ b
h : a / d = b / d
⊢ a = b
[PROOFSTEP]
rw [← Nat.mul_div_cancel' hda, ← Nat.mul_div_cancel' hdb, h]
[GOAL]
m n k a b : ℕ
h : b ≠ 0
⊢ a % b = a ↔ a < b
[PROOFSTEP]
cases b
[GOAL]
case zero
m n k a : ℕ
h : zero ≠ 0
⊢ a % zero = a ↔ a < zero
case succ m n k a n✝ : ℕ h : succ n✝ ≠ 0 ⊢ a % succ n✝ = a ↔ a < succ n✝
[PROOFSTEP]
contradiction
[GOAL]
case succ
m n k a n✝ : ℕ
h : succ n✝ ≠ 0
⊢ a % succ n✝ = a ↔ a < succ n✝
[PROOFSTEP]
exact ⟨fun h => h.ge.trans_lt (mod_lt _ (succ_pos _)), mod_eq_of_lt⟩
[GOAL]
m✝ n k✝ m k : ℕ
⊢ m % k + m / k * k = m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m✝ n k✝ m k : ℕ
⊢ m % k + k * (m / k) = m
[PROOFSTEP]
exact mod_add_div _ _
[GOAL]
m✝ n k✝ m k : ℕ
⊢ m / k * k + m % k = m
[PROOFSTEP]
rw [mul_comm]
[GOAL]
m✝ n k✝ m k : ℕ
⊢ k * (m / k) + m % k = m
[PROOFSTEP]
exact div_add_mod _ _
[GOAL]
m✝ n✝ k✝ n k m d : ℕ
h : 0 < k
x✝ : m + k * d = n ∧ m < k
h₁ : m + k * d = n
h₂ : m < k
⊢ (m + k * d) / k = d ∧ (m + k * d) % k = m
[PROOFSTEP]
rw [add_mul_div_left _ _ h, add_mul_mod_self_left]
[GOAL]
m✝ n✝ k✝ n k m d : ℕ
h : 0 < k
x✝ : m + k * d = n ∧ m < k
h₁ : m + k * d = n
h₂ : m < k
⊢ m / k + d = d ∧ m % k = m
[PROOFSTEP]
simp [div_eq_of_lt, mod_eq_of_lt, h₂]
[GOAL]
m n k a b c : ℕ
ha : 0 < a
d : ℕ
⊢ a * c = a * b * d ↔ c = b * d
[PROOFSTEP]
rw [mul_assoc, mul_right_inj' ha.ne']
[GOAL]
m n k a b c : ℕ
hc : 0 < c
d : ℕ
⊢ b * c = a * c * d ↔ b = a * d
[PROOFSTEP]
rw [mul_right_comm, mul_left_inj' hc.ne']
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
⊢ n % k % m = n % m
[PROOFSTEP]
conv =>
  rhs
  rw [← mod_add_div n k]
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
| n % k % m = n % m
[PROOFSTEP]
  rhs
  rw [← mod_add_div n k]
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
| n % k % m = n % m
[PROOFSTEP]
  rhs
  rw [← mod_add_div n k]
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
| n % k % m = n % m
[PROOFSTEP]
rhs
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
| n % m
[PROOFSTEP]
rw [← mod_add_div n k]
[GOAL]
m✝ n✝ k✝ n m k : ℕ
h : m ∣ k
⊢ n % k % m = (n % k + k * (n / k)) % m
[PROOFSTEP]
rcases h with ⟨t, rfl⟩
[GOAL]
case intro
m✝ n✝ k n m t : ℕ
⊢ n % (m * t) % m = (n % (m * t) + m * t * (n / (m * t))) % m
[PROOFSTEP]
rw [mul_assoc, add_mul_mod_self_left]
[GOAL]
m✝ n✝ k✝ m n k i : ℕ
H : m % n = k % n
⊢ (m + i) % n = (k + i) % n
[PROOFSTEP]
rw [← mod_add_mod, ← mod_add_mod k, H]
[GOAL]
m✝ n✝ k✝ m n k i : ℕ
H : m % n = k % n
⊢ (i + m) % n = (i + k) % n
[PROOFSTEP]
rw [add_comm, add_mod_eq_add_mod_right _ H, add_comm]
[GOAL]
m n k a b c : ℕ
hab : c ∣ b
h : a ∣ b / c
h1 : ∃ d, b / c = a * d
d : ℕ
hd : b / c = a * d
h3 : b = a * d * c
⊢ b = c * a * d
[PROOFSTEP]
rwa [mul_comm, ← mul_assoc] at h3 
[GOAL]
m n k a b : ℕ
w : a ∣ b
h : b / a = 1
⊢ a = b
[PROOFSTEP]
rw [← Nat.div_mul_cancel w, h, one_mul]
[GOAL]
m n k a b : ℕ
w : a ∣ b
h : b / a = 0
⊢ b = 0
[PROOFSTEP]
rw [← Nat.div_mul_cancel w, h, zero_mul]
[GOAL]
m✝ n✝ k m n : ℕ
n0 : 0 < n
⊢ m < n * (m / n + 1)
[PROOFSTEP]
rw [mul_comm, ← Nat.div_lt_iff_lt_mul' n0]
[GOAL]
m✝ n✝ k m n : ℕ
n0 : 0 < n
⊢ m / n < m / n + 1
[PROOFSTEP]
exact lt_succ_self _
[GOAL]
m n k a b c : ℕ
⊢ (a * b + c) % b = c % b
[PROOFSTEP]
simp [Nat.add_mod]
[GOAL]
m n k a b c : ℕ
h : c < b
⊢ (a * b + c) % b = c
[PROOFSTEP]
rw [Nat.mul_add_mod, Nat.mod_eq_of_lt h]
[GOAL]
m n✝ k n : ℕ
⊢ pred n = n ↔ n = 0
[PROOFSTEP]
cases n
[GOAL]
case zero
m n k : ℕ
⊢ pred zero = zero ↔ zero = 0
[PROOFSTEP]
simp [(Nat.succ_ne_self _).symm]
[GOAL]
case succ
m n k n✝ : ℕ
⊢ pred (succ n✝) = succ n✝ ↔ succ n✝ = 0
[PROOFSTEP]
simp [(Nat.succ_ne_self _).symm]
[GOAL]
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ Nat.find h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n
[PROOFSTEP]
constructor
[GOAL]
case mp
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ Nat.find h = m → p m ∧ ∀ (n : ℕ), n < m → ¬p n
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ p (Nat.find h) ∧ ∀ (n : ℕ), n < Nat.find h → ¬p n
[PROOFSTEP]
exact ⟨Nat.find_spec h, fun _ => Nat.find_min h⟩
[GOAL]
case mpr
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find h = m
[PROOFSTEP]
rintro ⟨hm, hlt⟩
[GOAL]
case mpr.intro
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
hm : p m
hlt : ∀ (n : ℕ), n < m → ¬p n
⊢ Nat.find h = m
[PROOFSTEP]
exact le_antisymm (Nat.find_min' h hm) (not_lt.1 <| imp_not_comm.1 (hlt _) <| Nat.find_spec h)
[GOAL]
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ
⊢ Nat.find h ≤ n ↔ ∃ m, m ≤ n ∧ p m
[PROOFSTEP]
simp only [exists_prop, ← lt_succ_iff, find_lt_iff]
[GOAL]
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ
⊢ n ≤ Nat.find h ↔ ∀ (m : ℕ), m < n → ¬p m
[PROOFSTEP]
simp_rw [← not_lt, find_lt_iff, not_exists, not_and]
[GOAL]
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
n : ℕ
⊢ n < Nat.find h ↔ ∀ (m : ℕ), m ≤ n → ¬p m
[PROOFSTEP]
simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]
[GOAL]
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∃ n, p n
⊢ Nat.find h = 0 ↔ p 0
[PROOFSTEP]
simp [find_eq_iff]
[GOAL]
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
⊢ Nat.find h₁ = Nat.find h₂ + 1
[PROOFSTEP]
refine' (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn => _⟩
[GOAL]
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n < Nat.find h₂ + 1
⊢ ¬p n
[PROOFSTEP]
cases' n with n
[GOAL]
case zero
m n k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
hn : zero < Nat.find h₂ + 1
⊢ ¬p zero
case succ
m n✝ k : ℕ
p q : ℕ → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h₁ : ∃ n, p n
h₂ : ∃ n, p (n + 1)
h0 : ¬p 0
n : ℕ
hn : succ n < Nat.find h₂ + 1
⊢ ¬p (succ n)
[PROOFSTEP]
exacts [h0, @Nat.find_min (fun n => p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)]
[GOAL]
m n✝ k : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
b n : ℕ
h : P (n + 1)
⊢ Nat.findGreatest P (n + 1) = n + 1
[PROOFSTEP]
simp [Nat.findGreatest, h]
[GOAL]
m n k : ℕ
P Q : ℕ → Prop
inst✝ : DecidablePred P
b : ℕ
h : ¬P (b + 1)
⊢ Nat.findGreatest P (b + 1) = Nat.findGreatest P b
[PROOFSTEP]
simp [Nat.findGreatest, h]
[GOAL]
m n✝ k : ℕ
P : (k : ℕ) → k < 0 → Prop
x✝ : (n : ℕ) → (h : n < 0) → Decidable (P n h)
n : ℕ
h : n < 0
⊢ P n h
[PROOFSTEP]
cases h
[GOAL]
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
cases' decidableBallLT n fun k h => P k (lt_succ_of_lt h) with h h
[GOAL]
case isFalse
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ¬∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
refine' isFalse (mt _ h)
[GOAL]
case isFalse
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ¬∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
⊢ (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h) → ∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
[PROOFSTEP]
intro hn k h
[GOAL]
case isFalse
m n✝ k✝ n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h✝ : ¬∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
hn : ∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h
k : ℕ
h : k < n
⊢ P k (_ : k < succ n)
[PROOFSTEP]
apply hn
[GOAL]
case isTrue
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
by_cases p : P n (lt_succ_self n)
[GOAL]
case pos
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
p : P n (_ : n < succ n)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
exact
  isTrue fun k h' =>
    (le_of_lt_succ h').lt_or_eq_dec.elim (h _) fun e =>
      match k, e, h' with
      | _, rfl, _ => p
[GOAL]
case neg
m n✝ k n : ℕ
P : (k : ℕ) → k < n + 1 → Prop
H : (n_1 : ℕ) → (h : n_1 < n + 1) → Decidable (P n_1 h)
h : ∀ (n_1 : ℕ) (h : n_1 < n), P n_1 (_ : n_1 < succ n)
p : ¬P n (_ : n < succ n)
⊢ Decidable (∀ (n_1 : ℕ) (h : n_1 < n + 1), P n_1 h)
[PROOFSTEP]
exact isFalse (mt (fun hn => hn _ _) p)
[GOAL]
m n k : ℕ
P : ℕ → Prop
h : DecidablePred P
⊢ ¬(fun n => ∃ m, m < n ∧ P m) 0
[PROOFSTEP]
simp
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
h : DecidablePred P
n : ℕ
⊢ (fun n_1 => ∃ m, m < n_1 ∧ ?m.69545 n m) n ∨ P n ↔ (fun n => ∃ m, m < n ∧ P m) (n + 1)
[PROOFSTEP]
simp only [lt_succ_iff_lt_or_eq, or_and_right, exists_or, exists_eq_left]
[GOAL]
m n✝ k : ℕ
P : ℕ → Prop
h : DecidablePred P
n : ℕ
⊢ (∃ m, m < n ∧ ?m.69545 n m) ∨ P n ↔ (∃ x, x < n ∧ P x) ∨ P n
[PROOFSTEP]
apply Iff.refl
