awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (hypothesis)
Goal:
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ m ∉ s
have x : s = ∅ ∨ s.Nonempty
Tactic: cases eq_empty_or_nonempty s with
  | inl h => subst h; apply notMem_empty
  | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (hypothesis)
Goal:
s : Set ℕ
m : ℕ
hm : m < sInf s
⊢ m ∉ s
have x : s = ∅ ∨ s.Nonempty
Tactic: classical
  cases eq_empty_or_nonempty s with
  | inl h => subst h; apply notMem_empty
  | inr h => rw [Nat.sInf_def h] at hm; exact Nat.find_min h hm
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m
have rw : Nat.find (p := fun (n : ℕ) ↦ n ∈ s) sorry ≤ m
Tactic: rw [Nat.sInf_def ⟨m, hm⟩]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
m : ℕ
hm : m ∈ s
⊢ sInf s ≤ m
have rw : Nat.find (p := fun (n : ℕ) ↦ n ∈ s) sorry ≤ m
Tactic: classical
  rw [Nat.sInf_def ⟨m, hm⟩]
  exact Nat.find_min' ⟨m, hm⟩ hm
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
h : 0 < sInf s
⊢ s.Nonempty
have by_contra : ∀ (contra : ¬s.Nonempty), False
Tactic: by_contra contra
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (hypothesis)
Goal:
s : Set ℕ
h : 0 < sInf s
contra : ¬s.Nonempty
⊢ False
have contra₁ : s = ∅
Tactic: rw [Set.not_nonempty_iff_eq_empty] at contra
Cleared hypotheses: contra
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (hypothesis)
Goal:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
⊢ False
have h' : sInf s ≠ 0
Tactic: have h' : sInf s ≠ 0 := ne_of_gt h
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ False
have apply : sInf s = 0
Tactic: apply h'
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
h : 0 < sInf s
contra : s = ∅
h' : sInf s ≠ 0
⊢ sInf s = 0
have rw : 0 ∈ s ∨ s = ∅
Tactic: rw [Nat.sInf_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
have mp : sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
mp : sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
have mpr : k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : sInf s = k + 1
⊢ k + 1 ∈ s ∧ k ∉ s
have mp : k + 1 ≤ k + 1 ∧ ¬k + 1 ≤ k
Tactic: rw [eq_Ici_of_nonempty_of_upward_closed (nonempty_of_sInf_eq_succ _) hs, H, mem_Ici, mem_Ici]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
H : k + 1 ∈ s
H' : k ∉ s
⊢ sInf s = k + 1
have mpr : k + 1 ∈ s ∧ ∀ n < k + 1, n ∉ s
Tactic: rw [sInf_def (⟨_, H⟩ : s.Nonempty), find_eq_iff]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
have mp : 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⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
k : ℕ
mp : sInf s = k + 1 → k + 1 ∈ s ∧ k ∉ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
have mpr : k + 1 ∈ s ∧ k ∉ s → sInf s = k + 1
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⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ¬BddAbove s
⊢ sSup s = sSup ∅
have 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) sorry
Tactic: simp only [sSup,
        mem_empty_iff_false, IsEmpty.forall_iff, forall_const, exists_const, dite_true]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ¬BddAbove s
⊢ (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) ⋯
have rw : 0 = Nat.find (p := fun (n : ℕ) ↦ True) sorry
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
s : Set ℕ
hs : ¬BddAbove s
rw : 0 = Nat.find (p := fun (n : ℕ) ↦ True) ⋯
⊢ (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) ⋯
have hnc : ¬∃ (n : ℕ), ∀ a ∈ s, a ≤ n
Tactic: rw [dif_neg]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
⊢ Eq (α := ℕ) (sSup ∅) ⊥
have simp : Nat.find (p := fun (n : ℕ) ↦ True) sorry = ⊥
Tactic: simp only [sSup_def, Set.mem_empty_iff_false, forall_const, forall_prop_of_false,
        not_false_iff, exists_const]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
⊢ Nat.find (p := fun (n : ℕ) ↦ True) ⋯ = ⊥
have apply : True
Tactic: apply bot_unique (Nat.find_min' _ _)
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
have inl : ∀ (h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅), sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
Tactic: obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
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}
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
have inr : ∀ (m : ℕ) (hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m), sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
Tactic: obtain h | ⟨m, hm⟩ := { m | p (m + n) }.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
have inl : n = sInf {m : ℕ | p m}
Tactic: rw [h, Nat.sInf_empty, zero_add]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅
⊢ n = sInf {m : ℕ | p m}
have inl : ∀ (hnp : n = sInf {m : ℕ | p m}), n = sInf {m : ℕ | p m}
Tactic: obtain hnp | hnp := hn.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
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}
⊢ n = sInf {m : ℕ | p m}
have inl₁ : ∀ (hnp : n < sInf {m : ℕ | p m}), n = sInf {m : ℕ | p m}
Tactic: obtain hnp | hnp := hn.eq_or_lt
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
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}
have inl : p (sInf {m : ℕ | p m} - n + n)
Tactic: suffices hp : p (sInf { m | p m } - n + n) from (h.subset hp).elim
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
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} - n + n)
have inl : p (sInf {m : ℕ | p m})
Tactic: rw [Nat.sub_add_cancel hn]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (hypothesis)
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} m
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
have hp : ∃ (n : ℕ), Membership.mem (γ := Set ℕ) {m : ℕ | p m} n
Tactic: have hp : ∃ n, n ∈ { m | p m } := ⟨_, hm⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
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
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
have inr : Nat.find (p := fun (n_1 : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} n_1) sorry + n =
  Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p m} n) hp
Tactic: rw [Nat.sInf_def ⟨m, hm⟩, Nat.sInf_def hp]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (hypothesis)
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
⊢ 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
have hn₁ : n ≤ Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {m : ℕ | p m} n) hp
Tactic: rw [Nat.sInf_def hp] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
hn : n ≤ sInf {m : ℕ | p m}
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
have inl : ∀ (h : Eq (α := Set ℕ) {m : ℕ | p (m + n)} ∅), 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
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
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}
⊢ sInf {m : ℕ | p (m + n)} + n = sInf {m : ℕ | p m}
have inr : ∀ (m : ℕ) (hm : Membership.mem (γ := Set ℕ) {m : ℕ | p (m + n)} 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
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
h₁ : n ≤ sInf {m : ℕ | p (m - n)}
⊢ sInf {m : ℕ | p m} + n = sInf {m : ℕ | p (m - n)}
have h₂ : ∀ (x : ℕ), x = x + n - n
Tactic: convert! sInf_add h₁
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
⊢ sInf {m : ℕ | p m} + n = sInf {m : ℕ | p (m - n)}
have suffices : 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]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
⊢ n ≤ sInf {m : ℕ | p (m - n)}
have obtain : ∀ (m : ℕ) (hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m), n ≤ sInf {m : ℕ | p (m - n)}
Tactic: obtain ⟨m, hm⟩ := nonempty_of_pos_sInf h
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
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)}
have refine_1 : Membership.mem (γ := Set ℕ) {m : ℕ | p (m - n)} (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)
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
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)
⊢ n ≤ sInf {m : ℕ | p (m - n)}
have refine_2 : ∀ (b : ℕ) (hb : Membership.mem (γ := Set ℕ) {m : ℕ | p (m - n)} b) (hbn : b < n),
  Membership.mem (γ := Set ℕ) {m : ℕ | p m} (b - 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)
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m
⊢ Membership.mem (γ := Set ℕ) {m : ℕ | p (m - n)} (m + n)
have refine_1 : p (m + n - n)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
n : ℕ
p : ℕ → Prop
h : LT.lt (α := ℕ) 0 (sInf {m : ℕ | p m})
m : ℕ
hm : Membership.mem (γ := Set ℕ) {m : ℕ | p m} m
⊢ p (m + n - n)
have refine_1 : p m
Tactic: rwa [Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ (k : ℕ), ⨆ (_ : k < n + 1), u k = (⨆ (k : ℕ), ⨆ (_ : k < n), u k) ⊔ u n
have simp_rw : ⨆ (k : ℕ), ⨆ (_ : k ≤ n), u k = (⨆ (k : ℕ), ⨆ (_ : k < n), u k) ⊔ u n
Tactic: simp_rw [Nat.lt_add_one_iff, biSup_le_eq_sup]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ (k : ℕ), ⨆ (_ : k < n + 1), u k = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k < n), u (k + 1)
have rw : (⨆ (_ : 0 < n + 1), u 0) ⊔ ⨆ (i : ℕ), ⨆ (_ : i + 1 < n + 1), u (i + 1) = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k < n), u (k + 1)
Tactic: rw [← sup_iSup_nat_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ n + 1), u k = (⨆ (k : ℕ), ⨆ (_ : k ≤ n), u k) ⊔ u (n + 1)
have simp_rw : ⨆ (k : ℕ), ⨆ (_ : k < (n + 1).succ), u k = (⨆ (k : ℕ), ⨆ (_ : k < n.succ), u k) ⊔ u (n + 1)
Tactic: simp_rw [← Nat.lt_succ_iff, iSup_lt_succ]
-- Lean 4 proof step from Mathlib.Data.Nat.Lattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ⨆ (k : ℕ), ⨆ (_ : k ≤ n + 1), u k = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k ≤ n), u (k + 1)
have simp_rw : ⨆ (k : ℕ), ⨆ (_ : k < (n + 1).succ), u k = u 0 ⊔ ⨆ (k : ℕ), ⨆ (_ : k < n.succ), u (k + 1)
Tactic: simp_rw [← Nat.lt_succ_iff, iSup_lt_succ']
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
hb : b ≤ 1
n : ℕ
⊢ log b n = 0
have rw : (if b ≤ 1 then 0 else (log.go n b n).snd) = 0
Tactic: rw [log, if_pos hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b : ℕ
hb : b ≤ 1
n : ℕ
rw : (if b ≤ 1 then 0 else (log.go n b n).snd) = 0
⊢ log b n = 0
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [log, if_pos hb]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : n < b
h : ¬b ≤ 1
⊢ (log.go n b n).snd = 0
have case2 : ∀ (hb : 0 < b), Eq (α := ℕ) (Prod.snd (α := ℕ) (0, 0)) 0
Tactic: fun_cases log.go with grind
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : n < b
h : ¬b ≤ 1
case2 : ∀ (hb : 0 < b), Eq (α := ℕ) (Prod.snd (α := ℕ) (0, 0)) 0
⊢ (log.go n b n).snd = 0
have case2₁ : ∀ (fuel : ℕ) (hb : fuel.succ < b), fuel.succ < b → Eq (α := ℕ) (Prod.snd (fuel.succ, 0)) 0
Tactic: fun_cases log.go with grind
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ (log.go n b n).snd = 0
have 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
Tactic: fun_cases log.go with grind
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
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
⊢ (log.go n b n).snd = 0
have 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
Tactic: fun_cases log.go with grind
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : n < b
⊢ log b n = 0
have case1 : b ≤ 1 → Eq (α := ℕ) 0 0
Tactic: fun_cases log with
  | case1 => rfl
  | case2 => fun_cases log.go with grind
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
b n : ℕ
hb : n < b
case1 : b ≤ 1 → Eq (α := ℕ) 0 0
⊢ log b n = 0
have case2 : ¬b ≤ 1 → (log.go n b n).snd = 0
Tactic: fun_cases log with
  | case1 => rfl
  | case2 => fun_cases log.go with grind
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
⊢ n < (b * b) ^ fuel
have hfuel₀ : fuel ≠ 0
Tactic: obtain hfuel₀ : fuel ≠ 0 := by rintro rfl; simp [Nat.not_lt_of_le hbn] at hfuel
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n b fuel : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hbn : b ≤ n
hfuel₀ : fuel ≠ 0
⊢ n < (b * b) ^ fuel
have rw : n < b ^ (2 * fuel)
Tactic: rw [← Nat.pow_two, ← Nat.pow_mul]
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)
have ih₁ : (go n (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
Tactic: rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
ih₁ : (go n (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)
have ih₂ : (b * b) ^ (go n (b * b) fuel).snd ≤ n
Tactic: rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
ih₁ : (go n (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
ih₂ : (b * b) ^ (go n (b * b) fuel).snd ≤ n
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)
have ih₃ : n < (b * b) ^ ((go n (b * b) fuel).snd + 1)
Tactic: rcases ih (Nat.one_mul 1 ▸ Nat.mul_lt_mul_of_lt_of_lt hb hb) (go_aux hb hfuel hnb)
        with ⟨ih₁, ih₂, ih₃⟩
-- Lean 4 proof step from Mathlib.Data.Nat.Log (goal)
Goal:
n : ℕ
hn : n ≠ 0
fuel : ℕ
ih :
  ∀ {b : ℕ} (hb : 1 < b) (hfuel : n < b ^ fuel),
    (go n b fuel).fst = n / b ^ (go n b fuel).snd ∧ b ^ (go n b fuel).snd ≤ n ∧ n < b ^ ((go n b fuel).snd + 1)
b : ℕ
hb : 1 < b
hfuel : n < b ^ (fuel + 1)
hnb : n ≥ b
ih₁ : (go n (b * b) fuel).fst = n / (b * b) ^ (go n (b * b) fuel).snd
ih₂ : (b * b) ^ (go n (b * b) fuel).snd ≤ n
ih₃ : n < (b * b) ^ ((go n (b * b) fuel).snd + 1)
⊢ (go n b (fuel + 1)).fst = n / b ^ (go n b (fuel + 1)).snd ∧
    b ^ (go n b (fuel + 1)).snd ≤ n ∧ n < b ^ ((go n b (fuel + 1)).snd + 1)
have succ : ∀ (ih₁ : (go n (HPow.hPow (β := ℕ) b 2) fuel).fst = n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd))
  (ih₂ : b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd) ≤ n)
  (ih₃ : n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 2)),
  (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
        else
          (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
            2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).fst =
      n /
        b ^
          (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
            else
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd ∧
    b ^
          (if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
            else
              (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd ≤
        n ∧
      n <
        b ^
          ((if n < b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1) then
                (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd), 2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd)
              else
                (n / b ^ (2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1),
                  2 * (go n (HPow.hPow (β := ℕ) b 2) fuel).snd + 1)).snd +
            1)
Tactic: simp_all only [go, if_neg (Nat.not_lt_of_le hnb), ← Nat.pow_two, ← Nat.pow_mul,
        Nat.div_lt_iff_lt_mul, Nat.pow_pos (Nat.zero_lt_of_lt hb), Nat.div_div_eq_div_mul,
        ← Nat.pow_add_one, ← Nat.pow_add_one', Nat.mul_add_one]
Cleared hypotheses: ih₁, ih₂, ih₃