awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
⊢ fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
have zero : fib (HAdd.hAdd (α := ℕ) 0 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range 0, fib k) 1
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    calc
      fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Basic (goal)
Goal:
n : ℕ
zero : fib (HAdd.hAdd (α := ℕ) 0 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range 0, fib k) 1
⊢ fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1
have succ : ∀ (n : ℕ) (ih : fib (n + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range n, fib k) 1),
  fib (n + 1 + 1) = HAdd.hAdd (α := ℕ) (∑ k ∈ Finset.range (n + 1), fib k) 1
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    calc
      fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (hypothesis)
Goal:
n a : ℕ
l : List ℕ
hl : (a :: l).IsZeckendorfRep
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
⊢ (map fib (a :: l)).sum < fib n
have hl₁ : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
Tactic: simp only [IsZeckendorfRep, cons_append, isChain_iff_pairwise, pairwise_cons] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (hypothesis)
Goal:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
hl : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum < fib n
have this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
Tactic: have : ∀ b, b ∈ head? (l ++ [0]) → b < a - 1 :=
      fun b hb ↦ lt_tsub_iff_right.2 <| hl.1 _ <| mem_of_mem_head? hb
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (hypothesis)
Goal:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
hl : (∀ a' ∈ l ++ [0], a' + 2 ≤ a) ∧ Pairwise (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
⊢ (map fib (a :: l)).sum < fib n
have hl₁ : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
Tactic: simp only [mem_append, mem_singleton, ← isChain_iff_pairwise, or_imp, forall_and, forall_eq,
      zero_add] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib a + (map fib l).sum < fib a + fib (a - 1)
have bc : (map fib l).sum < fib (a - 1)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ fib a + fib (a - 1) ≤ fib n
have rw : fib (a + 1) ≤ fib n
Tactic: rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum < fib n
have fib : fib a + (map fib l).sum < fib a + fib (a - 1)
Tactic: calc
      fib a + (map fib l).sum < fib a + fib (a - 1) := by gcongr; exact sum_fib_lt hl.2 this
      _ ≤ fib n := by
        rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']; exact fib_mono (hn _ rfl)
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n a : ℕ
l : List ℕ
hn : ∀ a_1 ∈ (a :: l ++ [0]).head?, a_1 < n
this : ∀ b ∈ (l ++ [0]).head?, b < a - 1
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
fib : Nat.fib a + (map Nat.fib l).sum < Nat.fib a + Nat.fib (a - 1)
⊢ (map Nat.fib (a :: l)).sum < Nat.fib n
have fib₁ : Nat.fib a + Nat.fib (a - 1) ≤ Nat.fib n
Tactic: calc
      fib a + (map fib l).sum < fib a + fib (a - 1) := by gcongr; exact sum_fib_lt hl.2 this
      _ ≤ fib n := by
        rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']; exact fib_mono (hn _ rfl)
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2
have rw : n < fib (n.greatestFib + 1)
Tactic: rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
    succ_pred, ← fib_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : n < fib (n.greatestFib + 1)
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2
have rw₁ : n.greatestFib ≠ 0
Tactic: rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
    succ_pred, ← fib_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n : ℕ
hn : n ≠ 0
rw : n < fib (n.greatestFib + 1)
rw₁ : n.greatestFib ≠ 0
⊢ (n - fib n.greatestFib).greatestFib ≤ n.greatestFib - 2
have rw₂ : n.greatestFib - 1 ≠ 0
Tactic: rw [← Nat.lt_succ_iff, greatestFib_lt, tsub_lt_iff_right n.fib_greatestFib_le, Nat.sub_succ,
    succ_pred, ← fib_add_one]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
m n : ℕ
h : m = n + 1
⊢ m - fib m.greatestFib < n + 1
have subst_vars : n + 1 - fib (n + 1).greatestFib < n + 1
Tactic: subst_vars
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
m n : ℕ
h : m = n + 1
⊢ m - fib m.greatestFib < namedPattern m n.succ h
have decreasing_by : m - fib m.greatestFib < n + 1
Tactic: decreasing_by simp_wf; subst_vars; apply zeckendorf_aux (zero_lt_succ _)
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
m n : ℕ
h : m = n + 1
decreasing_by decreasing_by₁ : m - fib m.greatestFib < n + 1
⊢ m - fib m.greatestFib < namedPattern m n.succ h
have decreasing_by₂ : n + 1 - fib (n + 1).greatestFib < n + 1
Tactic: decreasing_by simp_wf; subst_vars; apply zeckendorf_aux (zero_lt_succ _)
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n : ℕ
⊢ (n + 1).zeckendorf.IsZeckendorfRep
have rw : IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))
Tactic: rw [zeckendorf_succ, IsZeckendorfRep, List.cons_append]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n : ℕ
⊢ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) ((n + 1).greatestFib :: ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]))
have refine : ∀ (a : ℕ) (ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?), a + 2 ≤ (n + 1).greatestFib
Tactic: refine (isZeckendorfRep_zeckendorf _).cons (fun a ha ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
⊢ a + 2 ≤ (n + 1).greatestFib
have inl : ∀ (h : n + 1 - fib (n + 1).greatestFib = 0), a + 2 ≤ (n + 1).greatestFib
Tactic: obtain h | h := eq_zero_or_pos (n + 1 - fib (greatestFib (n + 1)))
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
inl : ∀ (h : n + 1 - fib (n + 1).greatestFib = 0), a + 2 ≤ (n + 1).greatestFib
⊢ a + 2 ≤ (n + 1).greatestFib
have inr : ∀ (h : n + 1 - fib (n + 1).greatestFib > 0), a + 2 ≤ (n + 1).greatestFib
Tactic: obtain h | h := eq_zero_or_pos (n + 1 - fib (greatestFib (n + 1)))
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (hypothesis)
Goal:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib = 0
⊢ a + 2 ≤ (n + 1).greatestFib
have ha₁ : 0 = a
Tactic: simp only [h, zeckendorf_zero, nil_append, head?_cons, Option.mem_some_iff] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n a : ℕ
h : n + 1 - fib (n + 1).greatestFib = 0
ha : 0 = a
⊢ a + 2 ≤ (n + 1).greatestFib
have inl : HAdd.hAdd (α := ℕ) 0 2 ≤ (n + 1).greatestFib
Tactic: subst ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (hypothesis)
Goal:
n a : ℕ
ha : a ∈ ((n + 1 - fib (n + 1).greatestFib).zeckendorf ++ [0]).head?
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib
have ha₁ : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
Tactic: rw [zeckendorf_of_pos h, cons_append, head?_cons, Option.mem_some_iff] at ha
Cleared hypotheses: ha, h
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n a : ℕ
ha : (n + 1 - fib (n + 1).greatestFib).greatestFib = a
h : n + 1 - fib (n + 1).greatestFib > 0
⊢ a + 2 ≤ (n + 1).greatestFib
have inr : (n + 1 - fib (n + 1).greatestFib).greatestFib + 2 ≤ (n + 1).greatestFib
Tactic: subst a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (hypothesis)
Goal:
a : ℕ
l : List ℕ
hl hl' : (a :: l).IsZeckendorfRep
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l
have hl₁ : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ List.Pairwise (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
Tactic: simp only [IsZeckendorfRep, cons_append, isChain_iff_pairwise, pairwise_cons, mem_append,
      mem_singleton, or_imp, forall_and, forall_eq, zero_add] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (hypothesis)
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ List.Pairwise (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l
have hl₁ : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
Tactic: rw [← isChain_iff_pairwise] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (hypothesis)
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l
have ha : 0 < a
Tactic: have ha : 0 < a := hl.1.2.trans_lt' zero_lt_two
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ (map fib (a :: l)).sum.zeckendorf = a :: l
have suffices : (fib a + (map fib l).sum).greatestFib = a
Tactic: suffices h : greatestFib (fib a + sum (map fib l)) = a by
      simp only [map, List.sum_cons, add_pos_iff, fib_pos.2 ha, true_or, zeckendorf_of_pos, h,
      add_tsub_cancel_left, zeckendorf_sum_fib hl.2]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ (fib a + (map fib l).sum).greatestFib = a
have simp : a ≤ (map fib l).sum + (fib a + 1) ∧
  ∀ ⦃n : ℕ⦄, a < n → n ≤ (map fib l).sum + (fib a + 1) → (map fib l).sum + fib a < fib n
Tactic: simp only [add_comm, add_assoc, greatestFib, findGreatest_eq_iff, ne_eq, ha.ne',
      not_false_eq_true, le_add_iff_nonneg_left, _root_.zero_le, forall_true_left, not_le, true_and]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
⊢ a ≤ (map fib l).sum + (fib a + 1) ∧
    ∀ ⦃n : ℕ⦄, a < n → n ≤ (map fib l).sum + (fib a + 1) → (map fib l).sum + fib a < fib n
have refine : ∀ (n : ℕ) (hn : a < n), n ≤ (map fib l).sum + (fib a + 1) → (map fib l).sum + fib a < fib n
Tactic: refine ⟨le_add_of_le_right <| le_fib_add_one _, fun n hn _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
a : ℕ
l : List ℕ
hl' : (a :: l).IsZeckendorfRep
hl : ((∀ x ∈ l, x + 2 ≤ a) ∧ 2 ≤ a) ∧ IsChain (fun (a b : ℕ) ↦ b + 2 ≤ a) (l ++ [0])
ha : 0 < a
n : ℕ
hn : a < n
h : n ≤ (map fib l).sum + (fib a + 1)
⊢ (map fib l).sum + fib a < fib n
have rw : (map fib (a :: l)).sum < fib n
Tactic: rw [add_comm, ← List.sum_cons, ← map_cons]
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n : ℕ
⊢ (map fib n.zeckendorf).sum = n
have case1 : (map fib (zeckendorf 0)).sum = 0
Tactic: induction n using zeckendorf.induct
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Fib.Zeckendorf (goal)
Goal:
n : ℕ
case1 : (map fib (zeckendorf 0)).sum = 0
⊢ (map fib n.zeckendorf).sum = n
have case2 : ∀ (n : ℕ),
  (map fib (n + 1 - fib (n + 1).greatestFib).zeckendorf).sum = n + 1 - fib (n + 1).greatestFib →
    (map fib n.succ.zeckendorf).sum = n.succ
Tactic: induction n using zeckendorf.induct
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m_1 n_1 k_1 : ℕ
p q : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
n : ℕ
pn : p n
m_2 m : ℕ
IH : ∀ (k : ℕ), n ≤ k + m → Acc (lbp (p := p)) k
k : ℕ
kn : n ≤ k + m.succ
y : ℕ
r : y.lbp (p := p) k
_a : ∀ (k_2 : ℕ), k_2 ≤ k → ¬p k_2
⊢ n ≤ k + 1 + m
have rw : n ≤ k + m + 1
Tactic: rw [Nat.add_right_comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
⊢ Nat.find (p := p) h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n
have mp : Nat.find (p := p) h = m → p m ∧ ∀ (n : ℕ), n < m → ¬p n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
mp : Nat.find (p := p) h = m → p m ∧ ∀ (n : ℕ), n < m → ¬p n
⊢ Nat.find (p := p) h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n
have mpr : (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find (p := p) h = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Find (hypothesis)
Goal:
m : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
hm : p m
hlt : ∀ (n : ℕ), n < m → ¬p n
⊢ Nat.find (p := p) h = m
have this : Nat.find (p := p) h ≤ m
Tactic: have := Nat.find_min' h hm
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
h₁ : ∃ (n : ℕ), p n
h₂ : ∃ (n : ℕ), p (n + 1)
h0 : ¬p 0
⊢ Nat.find (p := p) h₁ = Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1
have refine : ∀ (n : ℕ) (hn : n < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1), ¬p n
Tactic: refine (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
h₁ : ∃ (n : ℕ), p n
h₂ : ∃ (n : ℕ), p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1
⊢ ¬p n
have zero : ∀ (hn : 0 < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1), ¬p 0
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
h₁ : ∃ (n : ℕ), p n
h₂ : ∃ (n : ℕ), p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1
zero : ∀ (hn : 0 < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1), ¬p 0
⊢ ¬p n
have succ : ∀ (n : ℕ) (hn : n + 1 < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1), ¬p (n + 1)
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n = Nat.find (p := p) hₙ
have refine_1 : ∀ (m : ℕ) (hm : m < Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n) (hpm : p m),
  Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n ≤ m
Tactic: refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
refine_1 :
  ∀ (m : ℕ) (hm : m < Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n) (hpm : p m),
    Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n ≤ m
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n = Nat.find (p := p) hₙ
have refine_2 : Nat.find (p := p) hₙ ≤ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n
Tactic: refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Find (hypothesis)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
m : ℕ
hm : m < Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n
hpm : p m
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n ≤ m
have hnm : n ≤ m
Tactic: have hnm : n ≤ m := le_trans hn (find_le hpm)
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
m : ℕ
hm : m < Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n
hpm : p m
hnm : n ≤ m
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n ≤ m
have refine_1 : p (m - n + n)
Tactic: refine Nat.add_le_of_le_sub hnm (find_le ?_)
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
⊢ Nat.find (p := p) hₙ ≤ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n
have refine_2 : Nat.find (p := p) hₙ - n ≤ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ
Tactic: rw [← Nat.sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
⊢ Nat.find (p := p) hₙ - n ≤ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ
have refine_2 : ∀ (m : ℕ) (hm : m < Nat.find (p := p) hₙ - n) (hpm : p (m + n)), Nat.find (p := p) hₙ - n ≤ m
Tactic: refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
m : ℕ
hm : m < Nat.find (p := p) hₙ - n
hpm : p (m + n)
⊢ Nat.find (p := p) hₙ - n ≤ m
have refine_2 : Nat.find (p := p) hₙ ≤ m + n
Tactic: rw [Nat.sub_le_iff_le_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
m : ℕ
⊢ findGreatest P 0 = m ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n
have zero : (m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n) ↔ m = findGreatest P 0
Tactic: rw [eq_comm, Iff.comm]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
m : ℕ
⊢ (m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n) ↔ m = findGreatest P 0
have zero : m = 0 → (¬m = 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n = 0 → ¬P n
Tactic: simp only [Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
have pos : ∀ (hk : P (k + 1)), findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Tactic: by_cases hk : P (k + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
pos : ∀ (hk : P (k + 1)), findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
have neg : ∀ (hk : ¬P (k + 1)), findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Tactic: by_cases hk : P (k + 1)
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
have pos : k + 1 = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Tactic: rw [findGreatest_eq hk]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, 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 ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
have pos : k + 1 = m → m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : P (k + 1)
pos : k + 1 = m → m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
⊢ k + 1 = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
have pos₁ : (m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n) → k + 1 = m
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, 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 + 1
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
⊢ k + 1 = m
have pos : ∀ (hlt : m < k + 1), k + 1 = m
Tactic: rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, 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 + 1
h0 : m ≠ 0 → P m
hm : ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
pos : ∀ (hlt : m < k + 1), k + 1 = m
⊢ k + 1 = m
have pos₁ : ∀ (hle : k + 1 ≤ k + 1) (h0 : k + 1 ≠ 0 → P (k + 1)) (hm : ∀ ⦃n : ℕ⦄, k + 1 < n → n ≤ k + 1 → ¬P n), k + 1 = k + 1
Tactic: rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
Cleared hypotheses: m, hle, h0, hm
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
P : ℕ → Prop
inst : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
have neg : (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) ↔
  m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n
Tactic: rw [findGreatest_of_not hk, ihk]
-- Lean 4 proof step from Mathlib.Data.Nat.Find (goal)
Goal:
m k : ℕ
P : ℕ → Prop
inst : DecidablePred P
⊢ findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
have zero : ∀ {m : ℕ}, findGreatest P 0 = m ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n
Tactic: induction k generalizing m with
  | zero =>
    rw [eq_comm, Iff.comm]
    simp only [Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]
    rintro rfl
    exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by lia⟩
  | succ k ihk =>
    by_cases hk : P (k + 1)
    · rw [findGreatest_eq hk]
      constructor
      · rintro rfl
        exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by lia⟩
      · rintro ⟨hle, h0, hm⟩
        rcases Decidable.lt_or_eq_of_le hle with hlt | rfl
        exacts [(hm hlt (le_refl _) hk).elim, rfl]
    · rw [findGreatest_of_not hk, ihk]
      grind
Cleared hypotheses: m, k