awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n)
h₂ : rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < n
⊢ ack (b + 4 + 4) (max n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n)) ≤
    ack (max a b + 9) (m + (n + 1))
have inr : ack (b + HAdd.hAdd (α := ℕ) 4 4) n ≤ ack (max a b + 9) (m + (n + 1))
Tactic: rw [max_eq_left h₂.le, add_assoc]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (max n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n)) ≤
    ack (max a b + 9) (m + (n + 1))
have inr : ack (b + 4 + 4) (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n) ≤
  ack (max a b + 9) (m + (n + 1))
Tactic: rw [max_eq_right h₂]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n) ≤
    ack (max a b + 9) (m + (n + 1))
have inr : ack (b + 4 + 4) (ack (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + (n + 1))
Tactic: apply (ack_strictMono_right _ IH).le.trans
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
IH : rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n)
h₂ : n ≤ rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + (n + 1))
have inr : ack (b + HAdd.hAdd (α := ℕ) 4 4) (ack (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8) (ack (max a b + 8 + 1) (m + n))
Tactic: rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
⊢ rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
have zero : rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) 0 < ack (max a b + 9) (m + 0)
Tactic: induction n with
      | zero => -- The base case is easy.
        apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia
      | succ n IH => -- We get rid of the first `pair`.
        simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
m n : ℕ
zero : rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) 0 < ack (max a b + 9) (m + 0)
⊢ rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
have succ : ∀ (n : ℕ)
  (IH : rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)),
  rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) (n + 1) <
    ack (max a b + 9) (m + (n + 1))
Tactic: induction n with
      | zero => -- The base case is easy.
        apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia
      | succ n IH => -- We get rid of the first `pair`.
        simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (hypothesis)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
⊢ ∃ (m : ℕ),
    ∀ (n : ℕ),
      unpaired (fun (z n : ℕ) ↦ rec (motive := fun (x : ℕ) ↦ ℕ) (f z) (fun (y IH : ℕ) ↦ g (pair z (pair y IH))) n) n <
        ack m n
have this : ∀ {m n : ℕ},
  rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)
Tactic: have :
      ∀ {m n},
        rec (f m) (fun y IH => g <| pair m <| pair y IH) n < ack (max a b + 9) (m + n) := by
      intro m n
      -- We induct on n.
      induction n with
      | zero => -- The base case is easy.
        apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia
      | succ n IH => -- We get rid of the first `pair`.
        simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ ∃ (m : ℕ), ∀ (n : ℕ), f n < ack m n
have zero : ∃ (m : ℕ), ∀ (n : ℕ), (fun (x : ℕ) ↦ (0 : ℕ)) n < ack m n
Tactic: induction hf with
  | zero => exact ⟨0, ack_pos 0⟩
  | succ =>
    refine ⟨1, fun n => ?_⟩
    rw [succ_eq_one_add]
    apply add_lt_ack
  | left =>
    refine ⟨0, fun n => ?_⟩
    rw [ack_zero, Nat.lt_succ_iff]
    exact unpair_left_le n
  | right =>
    refine ⟨0, fun n => ?_⟩
    rw [ack_zero, Nat.lt_succ_iff]
    exact unpair_right_le n
  | @pair f g hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    refine ⟨max a b + 3, fun n => ?_⟩
    calc
      pair (f n) (g n) < (max (f n) (g n) + 1) ^ 2 := pair_lt_max_add_one_sq ..
      _ ≤ (ack (max a b) n + 1) ^ 2 := by rw [max_ack_left]; gcongr; exacts [(ha n).le, (hb n).le]
      _ ≤ ack (max a b + 3) n := ack_add_one_sq_lt_ack_add_three ..
  | comp hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    exact
      ⟨max a b + 2, fun n =>
        (ha _).trans <| (ack_strictMono_right a <| hb n).trans <| ack_ack_lt_ack_max_add_two a b n⟩
  | @prec f g hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    -- We prove this simpler inequality first.
    have :
      ∀ {m n},
        rec (f m) (fun y IH => g <| pair m <| pair y IH) n < ack (max a b + 9) (m + n) := by
      intro m n
      -- We induct on n.
      induction n with
      | zero => -- The base case is easy.
        apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia
      | succ n IH => -- We get rid of the first `pair`.
        simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
    -- The proof is now simple.
    exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : ∃ (m : ℕ), ∀ (n : ℕ), (fun (x : ℕ) ↦ (0 : ℕ)) n < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), f n < ack m n
have succ : ∃ (m : ℕ), ∀ (n : ℕ), n.succ < ack m n
Tactic: induction hf with
  | zero => exact ⟨0, ack_pos 0⟩
  | succ =>
    refine ⟨1, fun n => ?_⟩
    rw [succ_eq_one_add]
    apply add_lt_ack
  | left =>
    refine ⟨0, fun n => ?_⟩
    rw [ack_zero, Nat.lt_succ_iff]
    exact unpair_left_le n
  | right =>
    refine ⟨0, fun n => ?_⟩
    rw [ack_zero, Nat.lt_succ_iff]
    exact unpair_right_le n
  | @pair f g hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    refine ⟨max a b + 3, fun n => ?_⟩
    calc
      pair (f n) (g n) < (max (f n) (g n) + 1) ^ 2 := pair_lt_max_add_one_sq ..
      _ ≤ (ack (max a b) n + 1) ^ 2 := by rw [max_ack_left]; gcongr; exacts [(ha n).le, (hb n).le]
      _ ≤ ack (max a b + 3) n := ack_add_one_sq_lt_ack_add_three ..
  | comp hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    exact
      ⟨max a b + 2, fun n =>
        (ha _).trans <| (ack_strictMono_right a <| hb n).trans <| ack_ack_lt_ack_max_add_two a b n⟩
  | @prec f g hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    -- We prove this simpler inequality first.
    have :
      ∀ {m n},
        rec (f m) (fun y IH => g <| pair m <| pair y IH) n < ack (max a b + 9) (m + n) := by
      intro m n
      -- We induct on n.
      induction n with
      | zero => -- The base case is easy.
        apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia
      | succ n IH => -- We get rid of the first `pair`.
        simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
    -- The proof is now simple.
    exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : ∃ (m : ℕ), ∀ (n : ℕ), (fun (x : ℕ) ↦ (0 : ℕ)) n < ack m n
succ : ∃ (m : ℕ), ∀ (n : ℕ), n.succ < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), f n < ack m n
have left : ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).1) n < ack m n
Tactic: induction hf with
  | zero => exact ⟨0, ack_pos 0⟩
  | succ =>
    refine ⟨1, fun n => ?_⟩
    rw [succ_eq_one_add]
    apply add_lt_ack
  | left =>
    refine ⟨0, fun n => ?_⟩
    rw [ack_zero, Nat.lt_succ_iff]
    exact unpair_left_le n
  | right =>
    refine ⟨0, fun n => ?_⟩
    rw [ack_zero, Nat.lt_succ_iff]
    exact unpair_right_le n
  | @pair f g hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    refine ⟨max a b + 3, fun n => ?_⟩
    calc
      pair (f n) (g n) < (max (f n) (g n) + 1) ^ 2 := pair_lt_max_add_one_sq ..
      _ ≤ (ack (max a b) n + 1) ^ 2 := by rw [max_ack_left]; gcongr; exacts [(ha n).le, (hb n).le]
      _ ≤ ack (max a b + 3) n := ack_add_one_sq_lt_ack_add_three ..
  | comp hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    exact
      ⟨max a b + 2, fun n =>
        (ha _).trans <| (ack_strictMono_right a <| hb n).trans <| ack_ack_lt_ack_max_add_two a b n⟩
  | @prec f g hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    -- We prove this simpler inequality first.
    have :
      ∀ {m n},
        rec (f m) (fun y IH => g <| pair m <| pair y IH) n < ack (max a b + 9) (m + n) := by
      intro m n
      -- We induct on n.
      induction n with
      | zero => -- The base case is easy.
        apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia
      | succ n IH => -- We get rid of the first `pair`.
        simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
    -- The proof is now simple.
    exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
hf : Nat.Primrec f
zero : ∃ (m : ℕ), ∀ (n : ℕ), (fun (x : ℕ) ↦ (0 : ℕ)) n < ack m n
succ : ∃ (m : ℕ), ∀ (n : ℕ), n.succ < ack m n
left : ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).1) n < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), f n < ack m n
have right : ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).2) n < ack m n
Tactic: induction hf with
  | zero => exact ⟨0, ack_pos 0⟩
  | succ =>
    refine ⟨1, fun n => ?_⟩
    rw [succ_eq_one_add]
    apply add_lt_ack
  | left =>
    refine ⟨0, fun n => ?_⟩
    rw [ack_zero, Nat.lt_succ_iff]
    exact unpair_left_le n
  | right =>
    refine ⟨0, fun n => ?_⟩
    rw [ack_zero, Nat.lt_succ_iff]
    exact unpair_right_le n
  | @pair f g hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    refine ⟨max a b + 3, fun n => ?_⟩
    calc
      pair (f n) (g n) < (max (f n) (g n) + 1) ^ 2 := pair_lt_max_add_one_sq ..
      _ ≤ (ack (max a b) n + 1) ^ 2 := by rw [max_ack_left]; gcongr; exacts [(ha n).le, (hb n).le]
      _ ≤ ack (max a b + 3) n := ack_add_one_sq_lt_ack_add_three ..
  | comp hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    exact
      ⟨max a b + 2, fun n =>
        (ha _).trans <| (ack_strictMono_right a <| hb n).trans <| ack_ack_lt_ack_max_add_two a b n⟩
  | @prec f g hf hg IHf IHg =>
    obtain ⟨a, ha⟩ := IHf; obtain ⟨b, hb⟩ := IHg
    -- We prove this simpler inequality first.
    have :
      ∀ {m n},
        rec (f m) (fun y IH => g <| pair m <| pair y IH) n < ack (max a b + 9) (m + n) := by
      intro m n
      -- We induct on n.
      induction n with
      | zero => -- The base case is easy.
        apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
        lia
      | succ n IH => -- We get rid of the first `pair`.
        simp only
        apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
        -- If m is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ m with h₁ | h₁
        · rw [max_eq_left h₁.le]
          gcongr <;> omega
        rw [max_eq_right h₁]
        -- We get rid of the second `pair`.
        apply (ack_pair_lt _ _ _).le.trans
        -- If n is the maximum, we get a very weak inequality.
        rcases lt_or_ge _ n with h₂ | h₂
        · rw [max_eq_left h₂.le, add_assoc]
          exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)
        rw [max_eq_right h₂]
        -- We now use the inductive hypothesis, and some simple algebraic manipulation.
        apply (ack_strictMono_right _ IH).le.trans
        rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]
        exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
    -- The proof is now simple.
    exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
h : Nat.Primrec fun (n : ℕ) ↦ ack n n
⊢ False
have obtain : ∀ (m : ℕ) (hm : ∀ (n : ℕ), ack n n < ack m n), False
Tactic: obtain ⟨m, hm⟩ := exists_lt_ack_of_nat_primrec h
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
⊢ ¬Primrec (β := ℕ) fun (n : ℕ) ↦ ack n n
have rw : ¬Nat.Primrec fun (n : ℕ) ↦ ack n n
Tactic: rw [Primrec.nat_iff]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
⊢ EventuallyEq (β := ℝ) atTop (deriv fun (z : ℝ) ↦ z ^ p * (1 - ε z)) fun (x : ℝ) ↦
    deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 - ε x) x
have h : ∀ (x : ℝ) (hx : 1 < x),
  deriv (fun (z : ℝ) ↦ z ^ p * (1 - ε z)) x =
    deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 - ε x) x
Tactic: filter_upwards [eventually_gt_atTop 1] with x hx
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 1 < x
⊢ deriv (fun (z : ℝ) ↦ z ^ p * (1 - ε z)) x =
    deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 - ε x) x
have h : DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ z ^ p) x
Tactic: rw [deriv_fun_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 1 < x
h : DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ z ^ p) x
⊢ deriv (fun (z : ℝ) ↦ z ^ p * (1 - ε z)) x =
    deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 - ε x) x
have h₁ : DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 - ε z) x
Tactic: rw [deriv_fun_mul]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p : ℝ
⊢ EventuallyEq (β := ℝ) atTop
    (fun (x : ℝ) ↦ deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 - ε x) x) fun (x : ℝ) ↦
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
have h : ∀ (x : ℝ) (hx : 1 < x) (hderiv : deriv (fun (x : ℝ) ↦ 1 - ε x) x = x⁻¹ / HPow.hPow (β := ℕ) (log x) 2),
  deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 - ε x) x =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
Tactic: filter_upwards [eventually_gt_atTop 1, eventually_deriv_one_sub_smoothingFn]
      with x hx hderiv
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 1 < x
hderiv : deriv (fun (x : ℝ) ↦ 1 - ε x) x = x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 - ε x) x =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
have h : deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
Tactic: rw [hderiv, Real.deriv_rpow_const]
-- Lean 4 proof step from Mathlib.Computability.AkraBazzi.AkraBazzi (goal)
Goal:
p x : ℝ
hx : 1 < x
hderiv : deriv (fun (x : ℝ) ↦ 1 - ε x) x = x⁻¹ / HPow.hPow (β := ℕ) (log x) 2
h :
  deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
⊢ deriv (fun (x : ℝ) ↦ x ^ p) x * (1 - ε x) + x ^ p * deriv (fun (x : ℝ) ↦ 1 - ε x) x =
    p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
have h₁ : p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) =
  p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / HPow.hPow (β := ℕ) (log x) 2)
Tactic: rw [hderiv, Real.deriv_rpow_const]