awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Find
Goal:
m_1 n_1 k : ℕ
p q : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
m : ℕ
IH :
  (y : ℕ) → y.lbp (p := p) m → (fun (k : ℕ) ↦ (∀ (n : ℕ), n < k → ¬p n) → { n : ℕ // p n ∧ ∀ (m : ℕ), m < n → ¬p m }) y
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p m

Tactic:
pm
-- Module: Mathlib.Data.Nat.Find
Goal:
m_1 n_1 k : ℕ
p q : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
m : ℕ
IH :
  (y : ℕ) → y.lbp (p := p) m → (fun (k : ℕ) ↦ (∀ (n : ℕ), n < k → ¬p n) → { n : ℕ // p n ∧ ∀ (m : ℕ), m < n → ¬p m }) y
al : ∀ (n : ℕ), n < m → ¬p n
pm : ¬p m
n : ℕ
h : n ≤ m
e : n = m
⊢ ¬p m

Tactic:
exact pm
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
⊢ p (Nat.find (p := p) H)

Tactic:
(Nat.findX H).2.left

Premises used: And.left, Nat.find, Nat.findX, Subtype.property
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
⊢ ∀ {m : ℕ}, m < Nat.find (p := p) H → ¬p m

Tactic:
@(Nat.findX H).2.right

Premises used: And.right, Nat.find, Nat.findX, Subtype.property
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
H : ∃ (n : ℕ), p n
m : ℕ
h : p m
⊢ Nat.find (p := p) H ≤ m

Tactic:
Nat.le_of_not_gt fun l => Nat.find_min H l h

Premises used: Nat.find_min, Nat.le_of_not_gt
-- Module: Mathlib.Data.Nat.Find
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
mpr : (p m ∧ ∀ (n : ℕ), n < m → ¬p n) → Nat.find (p := p) h = m
⊢ Nat.find (p := p) h = m ↔ p m ∧ ∀ (n : ℕ), n < m → ¬p n

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
⊢ Nat.find (p := p) h = m → p m ∧ ∀ (n : ℕ), n < m → ¬p n

Tactic:
grind [Nat.find_min]

Premises used: Nat.find_min
-- Module: Mathlib.Data.Nat.Find
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

Tactic:
have := Nat.find_min' h hm
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
hm : p m
hlt : ∀ (n : ℕ), n < m → ¬p n
this : Nat.find (p := p) h ≤ m
⊢ Nat.find (p := p) h = m

Tactic:
grind
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
n : ℕ
⊢ Nat.find (p := p) h < n ↔ ∃ (m : ℕ), m < n ∧ p m

Tactic:
⟨fun h2 ↦ ⟨Nat.find h, h2, Nat.find_spec h⟩,
    fun ⟨_, hmn, hm⟩ ↦ Nat.lt_of_le_of_lt (Nat.find_min' h hm) hmn⟩

Premises used: Nat.lt_of_le_of_lt, Nat.find_min', _private.0.Nat.find_lt_iff.match_1, And.intro, LT.lt, Iff.intro, Nat.find, Exists.intro, Nat.find_spec
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
n : ℕ
⊢ Nat.find (p := p) h ≤ n ↔ ∃ (m : ℕ), m ≤ n ∧ p m

Tactic:
simp only [← Nat.lt_succ_iff, find_lt_iff]

Premises used: Nat.find_lt_iff, Nat.lt_succ_iff
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
n : ℕ
⊢ n ≤ Nat.find (p := p) h ↔ ∀ (m : ℕ), m < n → ¬p m

Tactic:
simp only [← not_lt, find_lt_iff, not_exists, not_and]

Premises used: Nat.find_lt_iff, not_exists, not_lt, not_and
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
n : ℕ
⊢ n < Nat.find (p := p) h ↔ ∀ (m : ℕ), m ≤ n → ¬p m

Tactic:
simp only [← succ_le_iff, le_find_iff, succ_le_succ_iff]

Premises used: Nat.le_find_iff, Nat.succ_le_succ_iff, Nat.succ_le_iff
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
⊢ Nat.find (p := p) h = 0 ↔ p 0

Tactic:
simp [find_eq_iff]

Premises used: Nat.find_eq_iff
-- Module: Mathlib.Data.Nat.Find
Goal:
p q : ℕ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
x : ℕ
hx : q x
hpq : ∀ (n : ℕ), n ≤ x → q n → p n
⊢ Nat.find (p := p) ⋯ ≤ Nat.find (p := q) ⋯

Tactic:
Nat.find_min' _ (hpq _ (Nat.find_min' _ hx) (Nat.find_spec ⟨x, hx⟩))

Premises used: Nat.find_min', Exists.intro, Nat.find_spec
-- Module: Mathlib.Data.Nat.Find
Goal:
p q : ℕ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
h : ∀ (n : ℕ), q n → p n
hp : ∃ (n : ℕ), p n
hq : ∃ (n : ℕ), q n
⊢ Nat.find (p := p) hp ≤ Nat.find (p := q) hq

Tactic:
let ⟨_, hq⟩ := hq; find_mono_of_le hq fun _ _ ↦ h _

Premises used: Nat.find_mono_of_le, _private.0.Nat.wf_lbp.match_2, LE.le, Nat.find
-- Module: Mathlib.Data.Nat.Find
Goal:
p q : ℕ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
x : ℕ
hx : p x
hpq : ∀ (n : ℕ), n ≤ x → (p n ↔ q n)
⊢ Nat.find (p := p) ⋯ = Nat.find (p := q) ⋯

Tactic:
le_antisymm (find_mono_of_le (hpq _ le_rfl |>.1 hx) fun _ h ↦ (hpq _ h).mpr)
    (find_mono_of_le hx fun _ h ↦ (hpq _ h).mp)

Premises used: Iff.mpr, le_rfl, Nat.find_mono_of_le, le_antisymm, Iff.mp
-- Module: Mathlib.Data.Nat.Find
Goal:
p q : ℕ → Prop
inst : DecidablePred p
inst_1 : DecidablePred q
hp : ∃ (n : ℕ), p n
hq : ∃ (n : ℕ), q n
hpq : ∀ {n : ℕ}, p n ↔ q n
⊢ Nat.find (p := p) hp = Nat.find (p := q) hq

Tactic:
let ⟨_, hp⟩ := hp; find_congr hp fun _ _ ↦ hpq

Premises used: _private.0.Nat.wf_lbp.match_2, Nat.find, Nat.find_congr, Eq
-- Module: Mathlib.Data.Nat.Find
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
hn : p n
⊢ Nat.find (p := p) h ≤ n

Tactic:
(Nat.find_le_iff _ _).2 ⟨n, le_refl _, hn⟩

Premises used: Iff.mpr, le_refl, Nat.find_le_iff, And.intro, Exists.intro
-- Module: Mathlib.Data.Nat.Find
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

Tactic:
(find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Nat.find_eq_iff, Nat.find_spec
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h₁ : ∃ (n : ℕ), p n
h₂ : ∃ (n : ℕ), p (n + 1)
h0 : ¬p 0
refine : ∀ (n : ℕ) (hn : n < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1), ¬p n
⊢ Nat.find (p := p) h₁ = Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1

Tactic:
refine (find_eq_iff _).2 ⟨Nat.find_spec h₂, fun n hn ↦ ?_⟩

Premises used: Iff.mpr, And.intro, Nat.find_eq_iff, Nat.find_spec
-- Module: Mathlib.Data.Nat.Find
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
succ : ∀ (n : ℕ) (hn : n + 1 < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1), ¬p (n + 1)
⊢ ¬p n

Tactic:
cases n
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h₁ : ∃ (n : ℕ), p n
h₂ : ∃ (n : ℕ), p (n + 1)
h0 : ¬p 0
hn : 0 < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1
⊢ ¬p 0

Tactic:
h0
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h₁ : ∃ (n : ℕ), p n
h₂ : ∃ (n : ℕ), p (n + 1)
h0 : ¬p 0
n : ℕ
hn : n + 1 < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1
⊢ ¬p (n + 1)

Tactic:
@Nat.find_min (fun n ↦ p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)

Premises used: Nat.succ_lt_succ_iff, Nat.find_min, Iff.mp
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h₁ : ∃ (n : ℕ), p n
h₂ : ∃ (n : ℕ), p (n + 1)
h0 : ¬p 0
hn : 0 < Nat.find (p := fun (n : ℕ) ↦ p (n + 1)) h₂ + 1
⊢ ¬p 0

Tactic:
exacts [h0, @Nat.find_min (fun n ↦ p (n + 1)) _ h₂ _ (succ_lt_succ_iff.1 hn)]
-- Module: Mathlib.Data.Nat.Find
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
⊢ 0 < Nat.find (p := p) h ↔ ¬p 0

Tactic:
Nat.pos_iff_ne_zero.trans (Nat.find_eq_zero _).not

Premises used: Nat.pos_iff_ne_zero, Iff.not, Nat.find_eq_zero, Iff.trans
-- Module: Mathlib.Data.Nat.Find
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ₙ

Tactic:
le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_

Premises used: Iff.mpr, Nat.le_find_iff, le_antisymm, Nat.not_le
-- Module: Mathlib.Data.Nat.Find
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
refine_2 : Nat.find (p := p) hₙ ≤ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n = Nat.find (p := p) hₙ

Tactic:
refine le_antisymm ((le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_) ?_

Premises used: Iff.mpr, Nat.le_find_iff, le_antisymm, Nat.not_le
-- Module: Mathlib.Data.Nat.Find
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
⊢ n ≤ m

Tactic:
have hnm : n ≤ m := le_trans hn (find_le hpm)
-- Module: Mathlib.Data.Nat.Find
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

Tactic:
Nat.add_le_of_le_sub hnm (find_le ?_)

Premises used: Nat.find_le, Nat.add_le_of_le_sub
-- Module: Mathlib.Data.Nat.Find
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
refine_1 : p (m - n + n)
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n ≤ m

Tactic:
refine Nat.add_le_of_le_sub hnm (find_le ?_)

Premises used: Nat.find_le, Nat.add_le_of_le_sub
-- Module: Mathlib.Data.Nat.Find
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
refine_1 refine_1₁ refine_1₂ refine_1₃ : p m
⊢ p (m - n + n)

Tactic:
rwa [Nat.sub_add_cancel hnm]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Data.Nat.Find
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
refine_2 : Nat.find (p := p) hₙ - n ≤ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ
⊢ Nat.find (p := p) hₙ ≤ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ + n

Tactic:
rw [← Nat.sub_le_iff_le_add]

Premises used: Nat.sub_le_iff_le_add
-- Module: Mathlib.Data.Nat.Find
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ₘ

Tactic:
(le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_

Premises used: Iff.mpr, Nat.le_find_iff, Nat.not_le
-- Module: Mathlib.Data.Nat.Find
Goal:
n : ℕ
p : ℕ → Prop
inst : DecidablePred p
hₘ : ∃ (m : ℕ), p (m + n)
hₙ : ∃ (n : ℕ), p n
hn : n ≤ Nat.find (p := p) hₙ
refine_2 : ∀ (m : ℕ) (hm : m < Nat.find (p := p) hₙ - n) (hpm : p (m + n)), Nat.find (p := p) hₙ - n ≤ m
⊢ Nat.find (p := p) hₙ - n ≤ Nat.find (p := fun (n_1 : ℕ) ↦ p (n_1 + n)) hₘ

Tactic:
refine (le_find_iff _ _).2 fun m hm hpm => Nat.not_le.2 hm ?_

Premises used: Iff.mpr, Nat.le_find_iff, Nat.not_le
-- Module: Mathlib.Data.Nat.Find
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)
refine_2 : Nat.find (p := p) hₙ ≤ m + n
⊢ Nat.find (p := p) hₙ - n ≤ m

Tactic:
rw [Nat.sub_le_iff_le_add]

Premises used: Nat.sub_le_iff_le_add
-- Module: Mathlib.Data.Nat.Find
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ₙ ≤ m + n

Tactic:
find_le hpm

Premises used: Nat.find_le
-- Module: Mathlib.Data.Nat.Find
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ₙ ≤ m + n

Tactic:
exact find_le hpm

Premises used: Nat.find_le
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
⊢ findGreatest P 0 = 0

Tactic:
(rfl)

Premises used: Nat.findGreatest, rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
⊢ findGreatest P (n + 1) = if P (n + 1) then n + 1 else findGreatest P n

Tactic:
(rfl)

Premises used: Nat.findGreatest, rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
h : P (n + 1)
⊢ findGreatest P (n + 1) = n + 1

Tactic:
simp [Nat.findGreatest, h]

Premises used: Nat.findGreatest
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) = findGreatest P n

Tactic:
simp [Nat.findGreatest, h]

Premises used: Nat.findGreatest
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m : ℕ
zero : (m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n) ↔ m = findGreatest P 0
⊢ findGreatest P 0 = m ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n

Tactic:
rw [eq_comm, Iff.comm]

Premises used: eq_comm, Iff.comm
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m : ℕ
zero : m = 0 → (¬m = 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n = 0 → ¬P n
⊢ (m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n) ↔ m = findGreatest P 0

Tactic:
simp only [Nat.le_zero, ne_eq, findGreatest_zero, and_iff_left_iff_imp]

Premises used: Nat.findGreatest_zero, Nat.le_zero, ne_eq, and_iff_left_iff_imp
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hlt : 0 < n
heq : n = 0
⊢ ¬P n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
⊢ (¬Eq (α := ℕ) 0 0 → P 0) ∧ ∀ ⦃n : ℕ⦄, 0 < n → n = 0 → ¬P n

Tactic:
exact ⟨fun h ↦ (h rfl).elim, fun n hlt heq ↦ by lia⟩
-- Module: Mathlib.Data.Nat.Find
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
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
⊢ 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)

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Data.Nat.Find
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
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
rw [findGreatest_eq hk]

Premises used: Nat.findGreatest_eq
-- Module: Mathlib.Data.Nat.Find
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
pos₁ : (m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n) → k + 1 = m
⊢ k + 1 = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Find
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
hk : P (k + 1)
n : ℕ
hlt : k + 1 < n
hle : n ≤ k + 1
⊢ ¬P n

Tactic:
lia
-- Module: Mathlib.Data.Nat.Find
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
hk : P (k + 1)
⊢ k + 1 ≤ k + 1 ∧ (k + 1 ≠ 0 → P (k + 1)) ∧ ∀ ⦃n : ℕ⦄, k + 1 < n → n ≤ k + 1 → ¬P n

Tactic:
exact ⟨le_refl _, fun _ ↦ hk, fun n hlt hle ↦ by lia⟩
-- Module: Mathlib.Data.Nat.Find
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
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
⊢ k + 1 = m

Tactic:
rcases Decidable.lt_or_eq_of_le hle with hlt | rfl

Premises used: Decidable.lt_or_eq_of_le, rfl
-- Module: Mathlib.Data.Nat.Find
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
hlt : m < k + 1
⊢ k + 1 = m

Tactic:
(hm hlt (le_refl _) hk).elim

Premises used: le_refl, False.elim
-- Module: Mathlib.Data.Nat.Find
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
hk : P (k + 1)
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:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Nat.Find
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
hlt : m < k + 1
⊢ k + 1 = m

Tactic:
exacts [(hm hlt (le_refl _) hk).elim, rfl]

Premises used: le_refl, False.elim, rfl
-- Module: Mathlib.Data.Nat.Find
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)
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
⊢ findGreatest P (k + 1) = m ↔ m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
rw [findGreatest_of_not hk, ihk]

Premises used: Nat.findGreatest_of_not
-- Module: Mathlib.Data.Nat.Find
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)
⊢ (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:
grind
-- Module: Mathlib.Data.Nat.Find
Goal:
m k : ℕ
P : ℕ → Prop
inst : DecidablePred P
zero : ∀ {m : ℕ}, findGreatest P 0 = m ↔ m ≤ 0 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ 0 → ¬P n
succ :
  ∀ (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
⊢ findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬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

Premises used: Nat.findGreatest_zero, Nat.le_zero, eq_comm, ne_eq, HAdd.hAdd, Nat.zero, Iff.comm, OfNat.ofNat, Nat.succ, and_iff_left_iff_imp, rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
k : ℕ
P : ℕ → Prop
inst : DecidablePred P
⊢ findGreatest P k = 0 ↔ ∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n

Tactic:
simp [findGreatest_eq_iff]

Premises used: Nat.findGreatest_eq_iff
-- Module: Mathlib.Data.Nat.Find
Goal:
k : ℕ
P : ℕ → Prop
inst : DecidablePred P
rw : (¬∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n) ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n
⊢ 0 < findGreatest P k ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n

Tactic:
rw [Nat.pos_iff_ne_zero, Ne, findGreatest_eq_zero_iff]

Premises used: Nat.pos_iff_ne_zero, Ne, Nat.findGreatest_eq_zero_iff
-- Module: Mathlib.Data.Nat.Find
Goal:
k : ℕ
P : ℕ → Prop
inst : DecidablePred P
push : (Exists fun ⦃n : ℕ⦄ ↦ 0 < n ∧ n ≤ k ∧ P n) ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n
⊢ (¬∀ ⦃n : ℕ⦄, 0 < n → n ≤ k → ¬P n) ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Data.Nat.Find
Goal:
k : ℕ
P : ℕ → Prop
inst : DecidablePred P
⊢ (Exists fun ⦃n : ℕ⦄ ↦ 0 < n ∧ n ≤ k ∧ P n) ↔ ∃ (n : ℕ), 0 < n ∧ n ≤ k ∧ P n

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
pos : ∀ (h : findGreatest P n = 0), P (findGreatest P n)
neg : ∀ (h : ¬findGreatest P n = 0), P (findGreatest P n)
⊢ P (findGreatest P n)

Tactic:
by_cases h : Nat.findGreatest P n = 0

Premises used: Nat.findGreatest
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : findGreatest P n = 0
pos : ∀ (hmb : 0 ≤ n) (hm : P 0), P (findGreatest P n)
pos₁ : ∀ (n_1 : ℕ) (hmb : n_1 + 1 ≤ n) (hm : P (n_1 + 1)), P (findGreatest P n)
⊢ P (findGreatest P n)

Tactic:
cases m
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
h : findGreatest P n = 0
hmb : 0 ≤ n
hm pos pos₁ pos₂ pos₃ : P 0
⊢ P (findGreatest P n)

Tactic:
rwa [h]
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n_1 : ℕ
hmb : n_1 + 1 ≤ n
hm : P (n_1 + 1)
⊢ P (findGreatest P n)

Tactic:
((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim

Premises used: False.elim, Nat.zero_lt_succ, Nat.findGreatest_eq_zero_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
h : findGreatest P n = 0
n_1 : ℕ
hmb : n_1 + 1 ≤ n
hm : P (n_1 + 1)
⊢ P (findGreatest P n)

Tactic:
exact ((findGreatest_eq_zero_iff.1 h) (zero_lt_succ _) hmb hm).elim

Premises used: False.elim, Nat.zero_lt_succ, Nat.findGreatest_eq_zero_iff, Iff.mp
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
(findGreatest_eq_iff.1 rfl).2.1 h

Premises used: And.right, And.left, Iff.mp, Nat.findGreatest_eq_iff, rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
h : ¬findGreatest P n = 0
⊢ P (findGreatest P n)

Tactic:
exact (findGreatest_eq_iff.1 rfl).2.1 h

Premises used: And.right, And.left, Iff.mp, Nat.findGreatest_eq_iff, rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
⊢ findGreatest P n ≤ n

Tactic:
(findGreatest_eq_iff.1 rfl).1

Premises used: And.left, Iff.mp, Nat.findGreatest_eq_iff, rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
m : ℕ
P : ℕ → Prop
inst : DecidablePred P
n : ℕ
hmb : m ≤ n
hm : P m
⊢ m ≤ findGreatest P n

Tactic:
le_of_not_gt fun hlt => (findGreatest_eq_iff.1 rfl).2.2 hlt hmb hm

Premises used: le_of_not_gt, And.right, Iff.mp, Nat.findGreatest_eq_iff, rfl
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n : ℕ
⊢ findGreatest P m ≤ findGreatest P m

Tactic:
simp
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n m_1 : ℕ
hmk : m.le m_1
ih : findGreatest P m ≤ findGreatest P m_1
pos : P (m_1 + 1) → findGreatest P m ≤ m_1 + 1
neg : ¬P (m_1 + 1) → findGreatest P m ≤ findGreatest P m_1
⊢ findGreatest P m ≤ if P (m_1 + 1) then m_1 + 1 else findGreatest P m_1

Tactic:
split_ifs
-- Module: Mathlib.Data.Nat.Find
Goal:
P : ℕ → Prop
inst : DecidablePred P
m n m_1 : ℕ
hmk : m.le m_1
ih : findGreatest P m ≤ findGreatest P m_1
h : P (m_1 + 1)
⊢ findGreatest P m ≤ m_1 + 1

Tactic:
le_trans ih <| le_trans (findGreatest_le _) (le_succ _)

Premises used: Nat.le_succ, Nat.findGreatest_le, le_trans