awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt_1 : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
⟨hlt.trans this, hpa⟩

Premises used: And.intro, LT.lt.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
hlt_1 : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
a : ℕ
this : nth p k < nth p (k + 1)
hlt : a < nth p k
hpa : p a
⊢ a < nth p (k + 1) ∧ p a

Tactic:
exact ⟨hlt.trans this, hpa⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hf : (setOf p).Finite
k : ℕ
hlt : k + 1 < #(hf.toFinset (s := setOf p))
⊢ {n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
filter_range_nth_eq_insert fun _ => hlt

Premises used: Nat.filter_range_nth_eq_insert
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
k : ℕ
⊢ {n ∈ range (nth p (k + 1)) | p n} = insert (nth p k) ({n ∈ range (nth p k) | p n})

Tactic:
filter_range_nth_eq_insert fun hf => absurd hf hp

Premises used: absurd, Nat.filter_range_nth_eq_insert
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))
⊢ count p (nth p 0) = 0

Tactic:
count_nth_zero _

Premises used: Nat.count_nth_zero
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))
⊢ count p (nth p 0) = 0

Tactic:
exact count_nth_zero _

Premises used: Nat.count_nth_zero
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
ihk : ∀ (hn : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))), count p (nth p k) = k
hn : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
succ : nth p k ∉ {n ∈ range (nth p k) | p n}
⊢ count p (nth p (k + 1)) = k + 1

Tactic:
rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem,
      ← count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]

Premises used: Nat.count_eq_card_filter_range, Finset.card_insert_of_notMem, Nat.lt_of_succ_lt, Nat.filter_range_nth_eq_insert
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
k : ℕ
ihk : ∀ (hn : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))), count p (nth p k) = k
hn : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))
⊢ nth p k ∉ {n ∈ range (nth p k) | p n}

Tactic:
simp
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
zero : ∀ (hn : ∀ (hf : (setOf p).Finite), 0 < #(hf.toFinset (s := setOf p))), count p (nth p 0) = 0
succ :
  ∀ (k : ℕ) (ihk : ∀ (hn : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))), count p (nth p k) = k)
    (hn : ∀ (hf : (setOf p).Finite), k + 1 < #(hf.toFinset (s := setOf p))), count p (nth p (k + 1)) = k + 1
⊢ count p (nth p n) = n

Tactic:
induction n with
  | zero => exact count_nth_zero _
  | succ k ihk =>
    rw [count_eq_card_filter_range, filter_range_nth_eq_insert hn, card_insert_of_notMem,
      ← count_eq_card_filter_range, ihk fun hf => lt_of_succ_lt (hn hf)]
    simp

Premises used: Nat.count_eq_card_filter_range, Finset.card_insert_of_notMem, Nat.zero, Nat.succ, Nat.filter_range_nth_eq_insert, Nat.count_nth_zero
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hp : (setOf p).Finite
hlt : n < #(hp.toFinset (s := setOf p))
⊢ count p (nth p n) = n

Tactic:
count_nth fun _ => hlt

Premises used: Nat.count_nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
n : ℕ
⊢ count p (nth p n) = n

Tactic:
count_nth fun hf => absurd hf hp

Premises used: absurd, Nat.count_nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : Set.Infinite (α := ℕ) {n : ℕ | p n}
⊢ Function.Surjective (count p)

Tactic:
fun n => ⟨nth p n, count_nth_of_infinite h n⟩

Premises used: Exists.intro, Nat.count_nth_of_infinite, Nat.nth, Function.Surjective
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hn : ∀ (hf : (setOf p).Finite), n < #(hf.toFinset (s := setOf p))
rw : (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1
rw₁ : (n + if p (nth p n) then 1 else 0) = n + 1
rw₂ rw₃ : n + 1 = n + 1
⊢ count p (nth p n + 1) = n + 1

Tactic:
rw [count_succ, count_nth hn, if_pos (nth_mem _ hn)]

Premises used: Nat.nth_mem, Nat.count_succ, if_pos, Nat.count_nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
n : ℕ
rw : (count p (nth p n) + if p (nth p n) then 1 else 0) = n + 1
rw₁ : (n + if p (nth p n) then 1 else 0) = n + 1
rw₂ rw₃ : n + 1 = n + 1
⊢ count p (nth p n + 1) = n + 1

Tactic:
rw [count_succ, count_nth_of_infinite hp, if_pos (nth_mem_of_infinite hp _)]

Premises used: Nat.count_succ, if_pos, Nat.nth_mem_of_infinite, Nat.count_nth_of_infinite
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hpn : p n
⊢ nth p (count p n) = n

Tactic:
have : ∀ hf : (setOf p).Finite, count p n < #hf.toFinset := fun hf => count_lt_card hf hpn
  count_injective (nth_mem _ this) hpn (count_nth this)

Premises used: Nat.nth_mem, Nat.count_injective, Nat.count_nth, Nat.count, Nat.count_lt_card
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n k : ℕ
h : k < count p n
⊢ nth p k < n

Tactic:
(count_monotone p).reflect_lt ?_

Premises used: Monotone.reflect_lt, Nat.count_monotone
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n k : ℕ
h : k < count p n
refine : count p (nth p k) < count p n
⊢ nth p k < n

Tactic:
refine (count_monotone p).reflect_lt ?_

Premises used: Monotone.reflect_lt, Nat.count_monotone
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n k : ℕ
h : k < count p n
rwa : ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))
⊢ count p (nth p k) < count p n

Tactic:
rwa [count_nth]

Premises used: Nat.count_nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n k : ℕ
h : k < count p n
⊢ ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))

Tactic:
fun hf => h.trans_le (count_le_card hf n)

Premises used: Nat.count_le_card, LT.lt.trans_le
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n k : ℕ
h : k < count p n
⊢ ∀ (hf : (setOf p).Finite), k < #(hf.toFinset (s := setOf p))

Tactic:
exact fun hf => h.trans_le (count_le_card hf n)

Premises used: Nat.count_le_card, LT.lt.trans_le
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n k : ℕ
h : n ≤ nth p k
⊢ count p n ≤ k

Tactic:
not_lt.1 fun hlt => h.not_gt <| nth_lt_of_lt_count hlt

Premises used: not_lt, LE.le.not_gt, Iff.mp, Nat.nth_lt_of_lt_count
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
h : ∃ (n : ℕ), p n
n : ℕ
rw : count p n = 0 ↔ n ≤ Nat.find (p := p) h
rw₁ : count p n = 0 ↔ ∀ m < n, ¬p m
rw₂ rw₃ : (∀ m < n, ¬p m) ↔ ∀ m < n, ¬p m
⊢ count p n = 0 ↔ n ≤ nth p 0

Tactic:
rw [nth_zero_of_exists h, le_find_iff h, Nat.count_iff_forall_not]

Premises used: Nat.le_find_iff, Nat.nth_zero_of_exists, Nat.count_iff_forall_not
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i}

Tactic:
(nth_eq_sInf _ _).trans (congr_arg sInf ?_)

Premises used: Nat.nth_eq_sInf, congr_arg, InfSet.sInf, Eq.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
refine : Eq (α := Set ℕ) {x : ℕ | p x ∧ ∀ k < count p n, nth p k < x} {i : ℕ | p i ∧ n ≤ i}
⊢ nth p (count p n) = sInf {i : ℕ | p i ∧ n ≤ i}

Tactic:
refine (nth_eq_sInf _ _).trans (congr_arg sInf ?_)

Premises used: Nat.nth_eq_sInf, congr_arg, InfSet.sInf, Eq.trans
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ Eq (α := Set ℕ) {x : ℕ | p x ∧ ∀ k < count p n, nth p k < x} {i : ℕ | p i ∧ n ≤ i}

Tactic:
Set.ext fun a => and_congr_right fun hpa => ?_

Premises used: Set.ext, and_congr_right
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
refine : ∀ (a : ℕ) (hpa : p a), (∀ k < count p n, nth p k < a) ↔ n ≤ a
⊢ Eq (α := Set ℕ) {x : ℕ | p x ∧ ∀ k < count p n, nth p k < x} {i : ℕ | p i ∧ n ≤ i}

Tactic:
refine Set.ext fun a => and_congr_right fun hpa => ?_

Premises used: Set.ext, and_congr_right
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n a : ℕ
hpa : p a
⊢ (∀ k < count p n, nth p k < a) ↔ n ≤ a

Tactic:
⟨fun h => not_lt.1 fun ha => ?_, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩

Premises used: not_lt, Iff.intro, Iff.mp, Nat.nth_lt_of_lt_count, lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n a : ℕ
hpa : p a
refine : ∀ (h : ∀ k < count p n, nth p k < a) (ha : a < n), False
⊢ (∀ k < count p n, nth p k < a) ↔ n ≤ a

Tactic:
refine ⟨fun h => not_lt.1 fun ha => ?_, fun hn k hk => lt_of_lt_of_le (nth_lt_of_lt_count hk) hn⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
⊢ nth p (count p a) < a

Tactic:
have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha)
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n a : ℕ
hpa : p a
h : ∀ k < count p n, nth p k < a
ha : a < n
hn : nth p (count p a) < a
rwa : ∀ (hn : a < a), False
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hn : False), False
⊢ False

Tactic:
rwa [nth_count hpa, lt_self_iff_false] at hn

Premises used: lt_self_iff_false, Nat.nth_count
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
hpn : ∃ (k : ℕ), p k ∧ n ≤ k
⊢ n ≤ nth p (count p n)

Tactic:
(le_csInf hpn fun _ => And.right).trans (nth_count_eq_sInf p n).ge

Premises used: Eq.ge, le_csInf, And.right, LE.le.trans, Nat.nth_count_eq_sInf
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
n : ℕ
⊢ n ≤ nth p (count p n)

Tactic:
let ⟨m, hp, hn⟩ := hp.exists_gt n
  le_nth_count' ⟨m, hp, hn.le⟩

Premises used: Set.Infinite.exists_gt, LT.lt.le, LE.le, _private.0.Nat.le_nth_count.match_1, And.intro, Nat.count, Exists.intro, Nat.le_nth_count', Nat.nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
a b : ℕ
⊢ count p a ≤ b ↔ a ≤ nth p b

Tactic:
gc_count_nth hp _ _

Premises used: Nat.gc_count_nth
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
inst : DecidablePred p
hp : (setOf p).Infinite
a b : ℕ
⊢ a < count p b ↔ nth p a < b

Tactic:
(gc_count_nth hp).lt_iff_lt

Premises used: Nat.gc_count_nth, GaloisConnection.lt_iff_lt
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
nth_rw : nth p (count p n) = n
nth_rw₁ nth_rw₂ : n = n
⊢ nth p n = n

Tactic:
nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]

Premises used: le_rfl, LT.lt.le, Nat.count_of_forall, Nat.nth_count
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≤ n, p n'
classical : nth p (count p n) = n
classical₁ classical₂ : n = n
⊢ nth p n = n

Tactic:
classical nth_rw 1 [← count_of_forall (hp · ·.le), nth_count (hp n le_rfl)]
-- Module: Mathlib.Data.Nat.Nth
Goal:
n : ℕ
⊢ nth (fun (x : ℕ) ↦ True) n = n

Tactic:
nth_of_forall fun _ _ ↦ trivial

Premises used: trivial, Nat.nth_of_forall
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
n' : ℕ
hn' : n' ∈ setOf p
contrapose! : ∀ (hp : n' ∉ (↑(range n) : Set ℕ)), ∃ n' ≥ n, p n'
⊢ n' ∈ (↑(range n) : Set ℕ)

Tactic:
contrapose! hp
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ setOf p
hp : n' ∉ (↑(range n) : Set ℕ)
⊢ n' ≥ n

Tactic:
simpa using hp
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n n' : ℕ
hn' : n' ∈ setOf p
hp : n' ∉ (↑(range n) : Set ℕ)
⊢ ∃ n' ≥ n, p n'

Tactic:
exact ⟨n', by simpa using hp, Set.mem_setOf.mp hn'⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
⊢ setOf p ⊆ (↑(range n) : Set ℕ)

Tactic:
have : setOf p ⊆ Finset.range n := by
    intro n' hn'
    contrapose! hp
    exact ⟨n', by simpa using hp, Set.mem_setOf.mp hn'⟩
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ (↑(range n) : Set ℕ)
rw : #(⋯.toFinset (s := setOf p)) ≤ n
⊢ nth p n = 0

Tactic:
rw [nth_of_card_le ((finite_toSet _).subset this)]

Premises used: Nat.nth_of_card_le, Set.Finite.subset, Finset.finite_toSet
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ (↑(range n) : Set ℕ)
⊢ #(⋯.toFinset (s := setOf p)) ≤ n

Tactic:
(Finset.card_le_card ?_).trans_eq (Finset.card_range n)

Premises used: LE.le.trans_eq, Finset.card_le_card, Finset.card_range
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ (↑(range n) : Set ℕ)
refine : ⋯.toFinset (s := setOf p) ⊆ range n
⊢ #(⋯.toFinset (s := setOf p)) ≤ n

Tactic:
refine (Finset.card_le_card ?_).trans_eq (Finset.card_range n)

Premises used: LE.le.trans_eq, Finset.card_le_card, Finset.card_range
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ (↑(range n) : Set ℕ)
⊢ ⋯.toFinset (s := setOf p) ⊆ range n

Tactic:
Set.Finite.toFinset_subset.mpr this

Premises used: Iff.mpr, Set.Finite.toFinset_subset
-- Module: Mathlib.Data.Nat.Nth
Goal:
p : ℕ → Prop
n : ℕ
hp : ∀ n' ≥ n, ¬p n'
this : setOf p ⊆ (↑(range n) : Set ℕ)
⊢ ⋯.toFinset (s := setOf p) ⊆ range n

Tactic:
exact Set.Finite.toFinset_subset.mpr this

Premises used: Iff.mpr, Set.Finite.toFinset_subset
-- Module: Mathlib.Data.Nat.Nth
Goal:
n : ℕ
⊢ nth (fun (x : ℕ) ↦ False) n = 0

Tactic:
nth_of_forall_not fun _ _ ↦ id

Premises used: Nat.nth_of_forall_not, id
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
s : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ s
h : Nonempty (↑s : Type)
⊢ (↑⊥ : ℕ) = Nat.find (p := fun (x : ℕ) ↦ x ∈ s) ⋯

Tactic:
rfl

Premises used: Nat.find, rfl
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
⊢ Membership.mem (γ := Set ℕ) Set.univ 0 ∧
    ∀ (k : ℕ), Membership.mem (γ := Set ℕ) Set.univ k → Membership.mem (γ := Set ℕ) Set.univ (k + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
⊢ p k

Tactic:
have hk : p k := Nat.find_spec H
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
this : 0 < k
rwa rwa₁ rwa₂ rwa₃ : p k
⊢ p (k - 1 + 1)

Tactic:
rwa [Nat.sub_add_cancel this]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
suffices : 0 < k
⊢ ∃ (n : ℕ), ¬p n ∧ p (n + 1)

Tactic:
suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
by_contra! : ∀ (contra : k ≤ 0), False
⊢ 0 < k

Tactic:
by_contra! contra
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
contra : k ≤ 0
⊢ k = 0

Tactic:
rw [le_zero_eq] at contra

Premises used: Nat.le_zero_eq
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
contra : k = 0
⊢ False

Tactic:
H' (contra ▸ hk)

Premises used: Eq.rec
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
k : ℕ := Nat.find (p := p) H
hk : p k
contra : k = 0
⊢ False

Tactic:
exact H' (contra ▸ hk)

Premises used: Eq.rec
-- Module: Mathlib.Data.Nat.Order.Lemmas
Goal:
p : ℕ → Prop
H' : ¬p 0
H : ∃ (n : ℕ), p n
let let₁ let₂ : ∃ (n : ℕ), ¬p n ∧ p (n + 1)
let₃ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k), ∃ (n : ℕ), ¬p n ∧ p (n + 1)
let₄ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k), 0 < k
let₅ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k) (contra : k ≤ 0), False
let₆ :
  let k := Nat.find (p := p) H;
  ∀ (hk : p k) (contra : k = 0), False
⊢ ∃ (n : ℕ), ¬p n ∧ p (n + 1)

Tactic:
classical
  let k := Nat.find H
  have hk : p k := Nat.find_spec H
  suffices 0 < k from
    ⟨k - 1, Nat.find_min H <| Nat.pred_lt this.ne', by rwa [Nat.sub_add_cancel this]⟩
  by_contra! contra
  rw [le_zero_eq] at contra
  exact H' (contra ▸ hk)

Premises used: Nat.le_zero_eq
-- Module: Mathlib.Data.Nat.PSub
Goal:
⊢ ppred 0 = none

Tactic:
rfl

Premises used: Nat.ppred, rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
⊢ n.succ.ppred = some n

Tactic:
rfl

Premises used: Nat.ppred, rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
m : ℕ
⊢ m.psub 0 = some m

Tactic:
rfl

Premises used: Nat.psub, rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
⊢ m.psub n.succ = m.psub n >>= ppred

Tactic:
rfl

Premises used: Nat.psub, rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
zero : pred 0 = (ppred 0).getD 0
succ : ∀ (n : ℕ), (n + 1).pred = (n + 1).ppred.getD 0
⊢ n.pred = n.ppred.getD 0

Tactic:
cases n
-- Module: Mathlib.Data.Nat.PSub
Goal:
⊢ pred 0 = (ppred 0).getD 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
⊢ (n + 1).pred = (n + 1).ppred.getD 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
rw : ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0
⊢ (m - n).ppred.getD 0 = (m.psub (n + 1)).getD 0

Tactic:
rw [sub_eq_psub m n, psub]

Premises used: Nat.psub
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
none : (ppred (Option.getD Option.none 0)).getD 0 = (Option.none >>= ppred).getD 0
some : ∀ (val : ℕ), ((Option.some val).getD 0).ppred.getD 0 = (Option.some val >>= ppred).getD 0
⊢ ((m.psub n).getD 0).ppred.getD 0 = (m.psub n >>= ppred).getD 0

Tactic:
cases psub m n

Premises used: Nat.psub
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
⊢ (ppred (Option.getD none 0)).getD 0 = (none >>= ppred).getD 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n val : ℕ
⊢ ((some val).getD 0).ppred.getD 0 = (some val >>= ppred).getD 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
m : ℕ
mp : ppred 0 = some m → m.succ = 0
mpr : m.succ = 0 → ppred 0 = some m
⊢ ppred 0 = some m ↔ m.succ = 0

Tactic:
constructor
-- Module: Mathlib.Data.Nat.PSub
Goal:
m : ℕ
h : ppred 0 = some m
⊢ m.succ = 0

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.PSub
Goal:
m : ℕ
h : m.succ = 0
⊢ ppred 0 = some m

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
mp : (n + 1).ppred = some m → m.succ = n + 1
mpr : m.succ = n + 1 → (n + 1).ppred = some m
⊢ (n + 1).ppred = some m ↔ m.succ = n + 1

Tactic:
constructor
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
h : (n + 1).ppred = some m
⊢ n = m

Tactic:
injection h
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
h : m.succ = n + 1
⊢ m = n

Tactic:
injection h
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
val_eq : n = m
mp : n.succ = n + 1
⊢ m.succ = n + 1

Tactic:
subst m
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
n_eq : m = n
mpr : (n + 1).ppred = some n
⊢ (n + 1).ppred = some m

Tactic:
subst m
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
⊢ n.succ = n + 1

Tactic:
rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
⊢ (n + 1).ppred = some n

Tactic:
rfl
-- Module: Mathlib.Data.Nat.PSub
Goal:
⊢ ppred 0 = none ↔ Eq (α := ℕ) 0 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
mp : (n + 1).ppred = none → n + 1 = 0
mpr : n + 1 = 0 → (n + 1).ppred = none
⊢ (n + 1).ppred = none ↔ n + 1 = 0

Tactic:
constructor
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
h : (n + 1).ppred = none
⊢ n + 1 = 0

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
h : n + 1 = 0
⊢ (n + 1).ppred = none

Tactic:
contradiction
-- Module: Mathlib.Data.Nat.PSub
Goal:
m k : ℕ
⊢ m.psub 0 = some k ↔ k + 0 = m

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n k : ℕ
apply : (∃ (a : ℕ), m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m
⊢ m.psub (n + 1) = some k ↔ k + (n + 1) = m

Tactic:
apply Option.bind_eq_some_iff.trans

Premises used: Iff.trans, Option.bind_eq_some_iff
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n k : ℕ
simp : (∃ (a : ℕ), a + n = m ∧ k.succ = a) ↔ k + (n + 1) = m
⊢ (∃ (a : ℕ), m.psub n = some a ∧ a.ppred = some k) ↔ k + (n + 1) = m

Tactic:
simp only [psub_eq_some, ppred_eq_some]

Premises used: Nat.ppred_eq_some
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n k : ℕ
⊢ (∃ (a : ℕ), a + n = m ∧ k.succ = a) ↔ k + (n + 1) = m

Tactic:
simp [add_comm, add_left_comm]

Premises used: add_left_comm, add_comm
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
none : ∀ (s : m.psub n = Option.none), Eq (α := Option ℕ) Option.none Option.none ↔ m < n
some : ∀ (val : ℕ) (s : m.psub n = Option.some val), Option.some val = Option.none ↔ m < n
⊢ m.psub n = Option.none ↔ m < n

Tactic:
rcases s : psub m n

Premises used: Nat.psub
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
s : m.psub n = Option.none
none : m < n
⊢ Eq (α := Option ℕ) Option.none Option.none ↔ m < n

Tactic:
simp only [true_iff]

Premises used: true_iff
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
s : m.psub n = none
⊢ m < n

Tactic:
lt_of_not_ge fun h => ?_

Premises used: lt_of_not_ge
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
s : m.psub n = Option.none
none : ∀ (h : n ≤ m), False
⊢ m < n

Tactic:
refine lt_of_not_ge fun h => ?_

Premises used: lt_of_not_ge
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
s : m.psub n = Option.none
h : n ≤ m
none : ∀ (k : ℕ) (e : n + k = m), False
⊢ False

Tactic:
obtain ⟨k, e⟩ := le.dest h

Premises used: Nat.le.dest
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
s : m.psub n = none
h : n ≤ m
k : ℕ
e : n + k = m
⊢ False

Tactic:
injection s.symm.trans (psub_eq_some.2 <| (add_comm _ _).trans e)

Premises used: Iff.mpr, Nat.psub_eq_some, add_comm, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n val : ℕ
s : m.psub n = some val
⊢ some val = none ↔ m < n

Tactic:
grind [psub_eq_some]

Premises used: Nat.psub_eq_some
-- Module: Mathlib.Data.Nat.PSub
Goal:
n : ℕ
h : 0 < n
⊢ n.ppred = some n.pred

Tactic:
ppred_eq_some.2 <| succ_pred_eq_of_pos h

Premises used: Iff.mpr, Nat.succ_pred_eq_of_pos, Nat.ppred_eq_some
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
h : n ≤ m
⊢ m.psub n = some (m - n)

Tactic:
psub_eq_some.2 <| Nat.sub_add_cancel h

Premises used: Iff.mpr, Nat.psub_eq_some, Nat.sub_add_cancel
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
⊢ m.psub (n + 0) = do
    let __do_lift ← m.psub n
    __do_lift.psub 0

Tactic:
simp
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n_1 n : ℕ
ih :
  m.psub (n_1 + n) = do
    let __do_lift ← m.psub n_1
    __do_lift.psub n
⊢ m.psub (n_1 + (n + 1)) = do
    let __do_lift ← m.psub n_1
    __do_lift.psub (n + 1)

Tactic:
simp only [ih, add_succ, psub_succ, bind_assoc]

Premises used: Nat.psub_succ, LawfulMonad.bind_assoc, Nat.add_succ
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n k : ℕ
zero :
  m.psub (n + 0) = do
    let __do_lift ← m.psub n
    __do_lift.psub 0
succ :
  ∀ (n_1 : ℕ)
    (ih :
      m.psub (n + n_1) = do
        let __do_lift ← m.psub n
        __do_lift.psub n_1),
    m.psub (n + (n_1 + 1)) = do
      let __do_lift ← m.psub n
      __do_lift.psub (n_1 + 1)
⊢ m.psub (n + k) = do
    let __do_lift ← m.psub n
    __do_lift.psub k

Tactic:
induction k with
    | zero => simp
    | succ n ih => simp only [ih, add_succ, psub_succ, bind_assoc]

Premises used: Nat.psub_succ, LawfulMonad.bind_assoc, Nat.add_succ, Nat.zero, Nat.succ
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
pos : ∀ (h : n ≤ m), some (m - n) = m.psub n
neg : ∀ (h : ¬n ≤ m), none = m.psub n
⊢ (if n ≤ m then some (m - n) else none) = m.psub n

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
h : n ≤ m
⊢ some (m - n) = m.psub n

Tactic:
(psub_eq_sub h).symm

Premises used: Nat.psub_eq_sub, Eq.symm
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
h : n ≤ m
⊢ some (m - n) = m.psub n

Tactic:
exact (psub_eq_sub h).symm

Premises used: Nat.psub_eq_sub, Eq.symm
-- Module: Mathlib.Data.Nat.PSub
Goal:
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n

Tactic:
(psub_eq_none.2 (not_le.1 h)).symm

Premises used: not_le, Iff.mpr, Nat.psub_eq_none, Iff.mp, Eq.symm