awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
rw : 0 ∈ s ∨ s = ∅
⊢ sInf s = 0

Tactic:
rw [Nat.sInf_eq_zero]

Premises used: Nat.sInf_eq_zero
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
h₁ : s = ∅
⊢ 0 ∈ s ∨ s = ∅

Tactic:
right
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ s = ∅

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
k : ℕ
h : sInf s = k + 1
⊢ s.Nonempty

Tactic:
nonempty_of_pos_sInf (h.symm ▸ succ_pos k : sInf s > 0)

Premises used: Eq.rec, Nat.nonempty_of_pos_sInf, Nat.succ_pos, Eq.symm
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : s.Nonempty
hs' : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ s = Ici (sInf s)

Tactic:
ext fun n ↦ ⟨fun H ↦ Nat.sInf_le H, fun H ↦ hs' (sInf s) n H (sInf_mem hs)⟩

Premises used: Set.ext, Nat.sInf_mem, Nat.sInf_le, Iff.intro, InfSet.sInf
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
mp : sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s
mpr : k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
constructor
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
mp : k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k
rw : ℕ
rw₁ : sInf s = k + 1
⊢ k + 1 ∈ s ∧ k ∉ s

Tactic:
rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]

Premises used: Nat.nonempty_of_sInf_eq_succ, Set.mem_Ici, Nat.eq_Ici_of_nonempty_of_upward_closed
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k

Tactic:
⟨le_rfl, k.not_succ_le_self⟩

Premises used: le_rfl, And.intro, Nat.not_succ_le_self
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k

Tactic:
exact ⟨le_rfl, k.not_succ_le_self⟩
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ ℕ

Tactic:
exact k
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ sInf s = k + 1

Tactic:
assumption
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
mpr : k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s
⊢ sInf s = k + 1

Tactic:
rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]

Premises used: Nat.sInf_def, Exists.intro, Nat.find_eq_iff
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s

Tactic:
⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

Premises used: Nat.lt_succ_iff, And.intro, Iff.mp
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s

Tactic:
exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
mp : sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s
mpr mpr₁ : k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s

Tactic:
classical
  constructor
  · intro H
    rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
    · exact ⟨le_rfl, k.not_succ_le_self⟩
    · exact k
    · assumption
  · rintro ⟨H, H'⟩
    rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
    exact ⟨H, fun n hnk hns ↦ H' <| hs n k (Nat.lt_succ_iff.mp hnk) hns⟩

Premises used: Nat.nonempty_of_sInf_eq_succ, Set.mem_Ici, Nat.eq_Ici_of_nonempty_of_upward_closed, Nat.find_eq_iff
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ¬BddAbove s
simp :
  (if h : ∃ (n : ℕ), ∀ a ∈ s, a ≤ n then Nat.find (p := fun (n : ℕ) ↦ ∀ a ∈ s, a ≤ n) h else 0) =
    Nat.find (p := fun (n : ℕ) ↦ True) ⋯
⊢ sSup s = sSup ∅

Tactic:
simp only [sSup,
        mem_empty_iff_false, IsEmpty.forall_iff, forall_const, exists_const, dite_true]

Premises used: exists_const, Set.mem_empty_iff_false, forall_const, dite_true, SupSet.sSup, IsEmpty.forall_iff
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ¬BddAbove s
rw : 0 = Nat.find (p := fun (n : ℕ) ↦ True) ⋯
hnc : ¬∃ (n : ℕ), ∀ a ∈ s, a ≤ n
⊢ (if h : ∃ (n : ℕ), ∀ a ∈ s, a ≤ n then Nat.find (p := fun (n : ℕ) ↦ ∀ a ∈ s, a ≤ n) h else 0) =
    Nat.find (p := fun (n : ℕ) ↦ True) ⋯

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ¬BddAbove s
⊢ 0 = Nat.find (p := fun (n : ℕ) ↦ True) ⋯

Tactic:
le_antisymm (zero_le _) (find_le trivial)

Premises used: Nat.zero_le, trivial, Nat.find_le, le_antisymm
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ¬BddAbove s
⊢ 0 = Nat.find (p := fun (n : ℕ) ↦ True) ⋯

Tactic:
exact le_antisymm (zero_le _) (find_le trivial)

Premises used: Nat.zero_le, Nat.find_le, le_antisymm
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ (n : ℕ), ∀ a ∈ s, a ≤ n

Tactic:
hs

Premises used: Set.Mem, setOf, upperBounds, BddAbove, Set.Nonempty
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ¬BddAbove s
⊢ ¬∃ (n : ℕ), ∀ a ∈ s, a ≤ n

Tactic:
exact hs
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
hs : ¬BddBelow s
⊢ sInf s = sInf ∅

Tactic:
simp at hs
-- Module: Mathlib.Data.Nat.Lattice
Goal:
simp : Nat.find (p := fun (n : ℕ) ↦ True) ⋯ = ⊥
⊢ Eq (α := ℕ) (sSup ∅) ⊥

Tactic:
simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
        not_false_iff, exists_const]

Premises used: Nat.sSup_def, forall_prop_of_false, exists_const, Set.mem_empty_iff_false, forall_const, not_false_iff
-- Module: Mathlib.Data.Nat.Lattice
Goal:
apply : True
⊢ Nat.find (p := fun (n : ℕ) ↦ True) ⋯ = ⊥

Tactic:
apply bot_unique (Nat.find_min' _ _)

Premises used: Nat.find_min', bot_unique
-- Module: Mathlib.Data.Nat.Lattice
Goal:
⊢ True

Tactic:
trivial
-- Module: Mathlib.Data.Nat.Lattice
Goal:
s : Set ℕ
h₁ : s.Nonempty
h₂ : BddAbove s
⊢ sSup s ∈ s

Tactic:
let ⟨k, hk⟩ := h₂
  h₁.csSup_mem ((finite_le_nat k).subset hk)

Premises used: Membership.mem, Set.Nonempty.csSup_mem, Set.Finite.subset, _private.0.Nat.sSup_mem.match_1, SupSet.sSup, Set.finite_le_nat
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
inl : ∀ (h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅), sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
inr :
  ∀ (m : ℕ) (hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m), sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}

Tactic:
obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty

Premises used: setOf, Set.eq_empty_or_nonempty, HAdd.hAdd
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
inl : n = sInf {m : ℕ | p m}
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}

Tactic:
rw [h, Nat.sInf_empty, zero_add]

Premises used: zero_add, Nat.sInf_empty
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
inl : ∀ (hnp : n = sInf {m : ℕ | p m}), n = sInf {m : ℕ | p m}
inl₁ : ∀ (hnp : n < sInf {m : ℕ | p m}), n = sInf {m : ℕ | p m}
⊢ n = sInf {m : ℕ | p m}

Tactic:
obtain hnp | hnp := hn.eq_or_lt

Premises used: LE.le.eq_or_lt
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
hnp : n = sInf {m : ℕ | p m}
⊢ n = sInf {m : ℕ | p m}

Tactic:
hnp
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
hnp : n = sInf {m : ℕ | p m}
⊢ n = sInf {m : ℕ | p m}

Tactic:
exact hnp
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
hnp : n < sInf {m : ℕ | p m}
inl : p (sInf {m : ℕ | p m} - n + n)
⊢ n = sInf {m : ℕ | p m}

Tactic:
suffices hp : p (sInf { m | p m } - n + n) from (h.subset hp).elim
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
hnp : n < sInf {m : ℕ | p m}
inl : p (sInf {m : ℕ | p m})
⊢ p (sInf {m : ℕ | p m} - n + n)

Tactic:
rw [Nat.sub_add_cancel hn]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
hnp : n < sInf {m : ℕ | p m}
⊢ p (sInf {m : ℕ | p m})

Tactic:
csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)

Premises used: Nat.zero_le, csInf_mem, Set.Mem, setOf, Nat.nonempty_of_pos_sInf, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
hnp : n < sInf {m : ℕ | p m}
⊢ p (sInf {m : ℕ | p m})

Tactic:
exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)

Premises used: Nat.zero_le, csInf_mem, Nat.nonempty_of_pos_sInf, LE.le.trans_lt
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m
⊢ ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {m : ℕ | p m} n

Tactic:
have hp : ∃ n, n ∈ { m | p m } := ⟨_, hm⟩
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m
hp : ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {m : ℕ | p m} n
inr :
  Nat.find (p := fun (n_1 : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} n_1) ⋯ + n =
    Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p m} n) hp
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}

Tactic:
rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]

Premises used: Nat.sInf_def, Exists.intro
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m
hp : ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {m : ℕ | p m} n
⊢ n ≤ Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p m} n) hp

Tactic:
rw [Nat.sInf_def hp] at hn

Premises used: Nat.sInf_def
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m
hp : ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {m : ℕ | p m} n
hn : n ≤ Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p m} n) hp
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} n_1) ⋯ + n =
    Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p m} n) hp

Tactic:
find_add hn

Premises used: Set.Mem, setOf, Nat.find_add
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m
hp : ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {m : ℕ | p m} n
hn : n ≤ Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p m} n) hp
⊢ Nat.find (p := fun (n_1 : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} n_1) ⋯ + n =
    Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p m} n) hp

Tactic:
exact find_add hn

Premises used: Nat.find_add
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
inl : ∀ (h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅), sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
inr inr₁ :
  ∀ (m : ℕ) (hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m), sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}

Tactic:
classical
  obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty
  · rw [h, Nat.sInf_empty, zero_add]
    obtain hnp | hnp := hn.eq_or_lt
    · exact hnp
    suffices hp : p (sInf { m | p m } - n + n) from (h.subset hp).elim
    rw [Nat.sub_add_cancel hn]
    exact csInf_mem (nonempty_of_pos_sInf <| n.zero_le.trans_lt hnp)
  · have hp : ∃ n, n ∈ { m | p m } := ⟨_, hm⟩
    rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]
    rw [Nat.sInf_def hp] at hn
    exact find_add hn

Premises used: LE.le.eq_or_lt, setOf, zero_add, Set.eq_empty_or_nonempty, Nat.find_add, Nat.sub_add_cancel, HAdd.hAdd, Nat.sInf_empty
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
h₁ : n ≤ sInf {m : ℕ | p (m - n)}
⊢ sInf {m : ℕ | p (m + n - n)} + n = sInf {m : ℕ | p (m - n)}

Tactic:
sInf_add h₁

Premises used: Nat.sInf_add
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
h₁ : n ≤ sInf {m : ℕ | p (m - n)}
h₂ : ∀ (x : ℕ), x = x + n - n
⊢ sInf {m : ℕ | p m} + n = sInf {m : ℕ | p (m - n)}

Tactic:
convert! sInf_add h₁

Premises used: Nat.sInf_add
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
h₁ : n ≤ sInf {m : ℕ | p (m - n)}
x : ℕ
⊢ x = x + n - n

Tactic:
simp_rw [Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
suffices : n ≤ sInf {m : ℕ | p (m - n)}
⊢ sInf {m : ℕ | p m} + n = sInf {m : ℕ | p (m - n)}

Tactic:
suffices h₁ : n ≤ sInf {m | p (m - n)} by
    convert! sInf_add h₁
    simp_rw [Nat.add_sub_cancel_right]
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
obtain : ∀ (m : ℕ) (hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m), n ≤ sInf {m : ℕ | p (m - n)}
⊢ n ≤ sInf {m : ℕ | p (m - n)}

Tactic:
obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h

Premises used: Nat.nonempty_of_pos_sInf
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m
⊢ n ≤ sInf {m : ℕ | p (m - n)}

Tactic:
le_csInf ⟨m + n, ?_⟩ fun b hb ↦
      le_of_not_gt fun hbn ↦
        ne_of_mem_of_not_mem ?_ (notMem_of_lt_sInf h) (Nat.sub_eq_zero_of_le hbn.le)

Premises used: Nat.notMem_of_lt_sInf, le_csInf, le_of_not_gt, LT.lt.le, ne_of_mem_of_not_mem, HAdd.hAdd, Exists.intro, Nat.sub_eq_zero_of_le
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m
refine_1 : Membership.mem (γ := Set ℕ) {m : ℕ | p (m - n)} (m + n)
refine_2 :
  ∀ (b : ℕ) (hb : Membership.mem (γ := Set ℕ) {m : ℕ | p (m - n)} b) (hbn : b < n),
    Membership.mem (γ := Set ℕ) {m : ℕ | p m} (b - n)
⊢ n ≤ sInf {m : ℕ | p (m - n)}

Tactic:
refine
    le_csInf ⟨m + n, ?_⟩ fun b hb ↦
      le_of_not_gt fun hbn ↦
        ne_of_mem_of_not_mem ?_ (notMem_of_lt_sInf h) (Nat.sub_eq_zero_of_le hbn.le)

Premises used: Nat.notMem_of_lt_sInf, le_csInf, le_of_not_gt, LT.lt.le, ne_of_mem_of_not_mem, HAdd.hAdd, Exists.intro, Nat.sub_eq_zero_of_le
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m
refine_1 : p (m + n - n)
⊢ Membership.mem (γ := Set ℕ) {m : ℕ | p (m - n)} (m + n)

Tactic:
dsimp
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m
refine_1 refine_1₁ refine_1₂ refine_1₃ : p m
⊢ p (m + n - n)

Tactic:
rwa [Nat.add_sub_cancel_right]

Premises used: Nat.add_sub_cancel_right
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m
b : ℕ
hb : Membership.mem (γ := Set ℕ) {m : ℕ | p (m - n)} b
hbn : b < n
⊢ Membership.mem (γ := Set ℕ) {m : ℕ | p m} (b - n)

Tactic:
hb

Premises used: Set.Mem, setOf
-- Module: Mathlib.Data.Nat.Lattice
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m
b : ℕ
hb : Membership.mem (γ := Set ℕ) {m : ℕ | p (m - n)} b
hbn : b < n
⊢ Membership.mem (γ := Set ℕ) {m : ℕ | p m} (b - n)

Tactic:
exact hb
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
simp_rw : ⨆ (k : ℕ), ⨆ (_ : k ≤ n), u k = (⨆ (k : ℕ), ⨆ (_ : k < n), u k) ⊔ u n
⊢ ⨆ (k : ℕ), ⨆ (_ : k < n + 1), u k = (⨆ (k : ℕ), ⨆ (_ : k < n), u k) ⊔ u n

Tactic:
simp_rw [Nat.lt_add_one_iff, biSup_le_eq_sup]

Premises used: biSup_le_eq_sup, Nat.lt_add_one_iff
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
rw : (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ (i : ℕ), ⨆ (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k < n), u (k + 1)
⊢ ⨆ (k : ℕ), ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k < n), u (k + 1)

Tactic:
rw [← sup_iSup_nat_succ]

Premises used: sup_iSup_nat_succ
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ (i : ℕ), ⨆ (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k < n), u (k + 1)

Tactic:
simp
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨅ (k : ℕ), ⨅ (_ : k < n + 1), u k = (⨅ (k : ℕ), ⨅ (_ : k < n), u k) ⊓ u n

Tactic:
@iSup_lt_succ αᵒᵈ _ _ _

Premises used: iInf, Nat.iSup_lt_succ, OrderDual
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨅ (k : ℕ), ⨅ (_ : k < n + 1), u k = u 0 ⊓ ⨅ (k : ℕ), ⨅ (_ : k < n), u (k + 1)

Tactic:
@iSup_lt_succ' αᵒᵈ _ _ _

Premises used: Nat.iSup_lt_succ', iInf, OrderDual
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
simp_rw : ⨆ (k : ℕ), ⨆ (_ : k < (n + 1).succ), u k = (⨆ (k : ℕ), ⨆ (_ : k < n.succ), u k) ⊔ u (n + 1)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ n + 1), u k = (⨆ (k : ℕ), ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)

Tactic:
simp_rw [← Nat.lt_succ_iff, iSup_lt_succ]

Premises used: Nat.lt_succ_iff, Nat.iSup_lt_succ
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
simp_rw : ⨆ (k : ℕ), ⨆ (_ : k < (n + 1).succ), u k = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k < n.succ), u (k + 1)
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), u (k + 1)

Tactic:
simp_rw [← Nat.lt_succ_iff, iSup_lt_succ']

Premises used: Nat.iSup_lt_succ', Nat.lt_succ_iff
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨅ (k : ℕ), ⨅ (_ : k ≤ n + 1), u k = (⨅ (k : ℕ), ⨅ (_ : k ≤ n), u k) ⊓ u (n + 1)

Tactic:
@iSup_le_succ αᵒᵈ _ _ _

Premises used: iInf, OrderDual, Nat.iSup_le_succ
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨅ (k : ℕ), ⨅ (_ : k ≤ n + 1), u k = u 0 ⊓ ⨅ (k : ℕ), ⨅ (_ : k ≤ n), u (k + 1)

Tactic:
@iSup_le_succ' αᵒᵈ _ _ _

Premises used: iInf, OrderDual, Nat.iSup_le_succ'
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), u k = (⋃ (k : ℕ), ⋃ (_ : k < n), u k) ∪ u n

Tactic:
Nat.iSup_lt_succ u n

Premises used: Nat.iSup_lt_succ, Set.iUnion
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ ⋃ (k : ℕ), ⋃ (_ : k < n + 1), u k = u 0 ∪ ⋃ (k : ℕ), ⋃ (_ : k < n), u (k + 1)

Tactic:
Nat.iSup_lt_succ' u n

Premises used: Nat.iSup_lt_succ', Set.iUnion
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ ⋂ (k : ℕ), ⋂ (_ : k < n + 1), u k = (⋂ (k : ℕ), ⋂ (_ : k < n), u k) ∩ u n

Tactic:
Nat.iInf_lt_succ u n

Premises used: Set.iInter, Nat.iInf_lt_succ
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ ⋂ (k : ℕ), ⋂ (_ : k < n + 1), u k = u 0 ∩ ⋂ (k : ℕ), ⋂ (_ : k < n), u (k + 1)

Tactic:
Nat.iInf_lt_succ' u n

Premises used: Nat.iInf_lt_succ', Set.iInter
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ ⋃ (k : ℕ), ⋃ (_ : k ≤ n + 1), u k = (⋃ (k : ℕ), ⋃ (_ : k ≤ n), u k) ∪ u (n + 1)

Tactic:
Nat.iSup_le_succ u n

Premises used: Set.iUnion, Nat.iSup_le_succ
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ ⋃ (k : ℕ), ⋃ (_ : k ≤ n + 1), u k = u 0 ∪ ⋃ (k : ℕ), ⋃ (_ : k ≤ n), u (k + 1)

Tactic:
Nat.iSup_le_succ' u n

Premises used: Nat.iSup_le_succ', Set.iUnion
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ ⋂ (k : ℕ), ⋂ (_ : k ≤ n + 1), u k = (⋂ (k : ℕ), ⋂ (_ : k ≤ n), u k) ∩ u (n + 1)

Tactic:
Nat.iInf_le_succ u n

Premises used: Set.iInter, Nat.iInf_le_succ
-- Module: Mathlib.Data.Nat.Lattice
Goal:
α : Type u_1
u : ℕ → Set α
n : ℕ
⊢ ⋂ (k : ℕ), ⋂ (_ : k ≤ n + 1), u k = u 0 ∩ ⋂ (k : ℕ), ⋂ (_ : k ≤ n), u (k + 1)

Tactic:
Nat.iInf_le_succ' u n

Premises used: Nat.iInf_le_succ', Set.iInter
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
hb : b ≤ 1
n : ℕ
rw : (if b ≤ 1 then 0 else (log.go n b n).snd) = 0
rw₁ rw₂ : Eq (α := ℕ) 0 0
⊢ log b n = 0

Tactic:
rw [log, if_pos hb]

Premises used: if_pos, Nat.log
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : n < b
h : b ≤ 1
⊢ Eq (α := ℕ) 0 0

Tactic:
rfl
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
h : ¬b ≤ 1
hb : 0 < b
⊢ Eq (α := ℕ) (Prod.snd (α := ℕ) (0, 0)) 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
h : ¬b ≤ 1
fuel : ℕ
hb h_1 : fuel.succ < b
⊢ Eq (α := ℕ) (Prod.snd (fuel.succ, 0)) 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
h : ¬b ≤ 1
fuel q e : ℕ
h_1 : q < b
hb : fuel.succ < b
h_2 : ¬fuel.succ < b
h_3 : log.go fuel.succ (b * b) fuel = (q, e)
⊢ (q, 2 * e).snd = 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b : ℕ
h : ¬b ≤ 1
fuel q e : ℕ
h_1 : ¬q < b
hb : fuel.succ < b
h_2 : ¬fuel.succ < b
h_3 : log.go fuel.succ (b * b) fuel = (q, e)
⊢ (q / b, 2 * e + 1).snd = 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : n < b
h : ¬b ≤ 1
case2 : ∀ (hb : 0 < b), Eq (α := ℕ) (Prod.snd (α := ℕ) (0, 0)) 0
case2₁ : ∀ (fuel : ℕ) (hb : fuel.succ < b), fuel.succ < b → Eq (α := ℕ) (Prod.snd (fuel.succ, 0)) 0
case2₂ :
  ∀ (fuel q e : ℕ),
    q < b → ∀ (hb : fuel.succ < b), ¬fuel.succ < b → log.go fuel.succ (b * b) fuel = (q, e) → (q, 2 * e).snd = 0
case2₃ :
  ∀ (fuel q e : ℕ),
    ¬q < b →
      ∀ (hb : fuel.succ < b), ¬fuel.succ < b → log.go fuel.succ (b * b) fuel = (q, e) → (q / b, 2 * e + 1).snd = 0
⊢ (log.go n b n).snd = 0

Tactic:
fun_cases log.go with grind

Premises used: Nat.log.go
-- Module: Mathlib.Data.Nat.Log
Goal:
b n : ℕ
hb : n < b
case1 : b ≤ 1 → Eq (α := ℕ) 0 0
case2 : ¬b ≤ 1 → (log.go n b n).snd = 0
⊢ log b n = 0

Tactic:
fun_cases log with
  | case1 => rfl
  | case2 => fun_cases log.go with grind

Premises used: Nat.log, Nat.log.go
-- Module: Mathlib.Data.Nat.Log
Goal:
n b : ℕ
hb : 1 < b
hbn : b ≤ n
hfuel : n < b ^ HAdd.hAdd (α := ℕ) 0 1
⊢ False

Tactic:
simp [Nat.not_lt_of_le hbn] at hfuel

Premises used: Nat.not_lt_of_le
-- Module: Mathlib.Data.Nat.Log
Goal:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
⊢ fuel ≠ 0

Tactic:
obtain hfuel₀ : fuel ≠ 0 := by rintro rfl; simp [Nat.not_lt_of_le hbn] at hfuel
-- Module: Mathlib.Data.Nat.Log
Goal:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
rw : n < b ^ (2 * fuel)
⊢ n < (b * b) ^ fuel

Tactic:
rw [← Nat.pow_two, ← Nat.pow_mul]

Premises used: Nat.pow_mul, Nat.pow_two
-- Module: Mathlib.Data.Nat.Log
Goal:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ b > 0

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ fuel + 1 ≤ 2 * fuel

Tactic:
grind
-- Module: Mathlib.Data.Nat.Log
Goal:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ n < b ^ (2 * fuel)

Tactic:
exact Nat.lt_of_lt_of_le hfuel <| Nat.pow_le_pow_right (by grind) (by grind)

Premises used: Nat.pow_le_pow_right, Nat.lt_of_lt_of_le
-- Module: Mathlib.Data.Nat.Log
Goal:
n : ℕ
hn : n ≠ 0
b : ℕ
hb : 1 < b
hfuel : n < HPow.hPow (β := ℕ) b 0
⊢ (go n b 0).fst = n / b ^ (go n b 0).snd ∧ b ^ (go n b 0).snd ≤ n ∧ n < b ^ ((go n b 0).snd + 1)

Tactic:
simp_all