awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
⊢ 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)
have bc : LE.le (α := ℕ) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
bc : LE.le (α := ℕ) 1 2
⊢ 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)
have bc₁ : 3 ≤ n + 3
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
⊢ HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)
have calc : HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3
Tactic: calc 2 * 3
      _ ≤ 2 * 2 ^ 3 := by simp
      _ ≤ 2 * 2 ^ (n + 3) := by gcongr <;> lia
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
calc : HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3
⊢ HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)
have calc₁ : 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)
Tactic: calc 2 * 3
      _ ≤ 2 * 2 ^ 3 := by simp
      _ ≤ 2 * 2 ^ (n + 3) := by gcongr <;> lia
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
⊢ ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
have zero : ack 3 0 = HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 3) - 3
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    rw [ack_succ_succ, IH, ack_two, Nat.succ_add, Nat.pow_succ 2 (n + 3), mul_comm _ 2,
        Nat.mul_sub_left_distrib, ← Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right]
    calc 2 * 3
      _ ≤ 2 * 2 ^ 3 := by simp
      _ ≤ 2 * 2 ^ (n + 3) := by gcongr <;> lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
zero : ack 3 0 = HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 3) - 3
⊢ ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
have succ : ∀ (n : ℕ) (IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3), ack 3 (n + 1) = HPow.hPow (α := ℕ) 2 (n + 1 + 3) - 3
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    rw [ack_succ_succ, IH, ack_two, Nat.succ_add, Nat.pow_succ 2 (n + 3), mul_comm _ 2,
        Nat.mul_sub_left_distrib, ← Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right]
    calc 2 * 3
      _ ≤ 2 * 2 ^ 3 := by simp
      _ ≤ 2 * 2 ^ (n + 3) := by gcongr <;> lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m : ℕ
⊢ 0 < ack (m + 1) 0
have rw : 0 < ack m 1
Tactic: rw [ack_succ_zero]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
⊢ 0 < ack (m + 1) (n + 1)
have rw : 0 < ack m (ack (m + 1) n)
Tactic: rw [ack_succ_succ]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m : ℕ
⊢ 1 < ack (m + 1 + 1) 0
have rw : 1 < ack (m + 1) 1
Tactic: rw [ack_succ_zero]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
⊢ 1 < ack (m + 1 + 1) (n + 1)
have rw : 1 < ack (m + 1) (ack (m + 1 + 1) n)
Tactic: rw [ack_succ_succ]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
_h : 0 < n + 1
⊢ ack (m + 1) 0 < ack (m + 1) (n + 1)
have rw : ack m 1 < ack m (ack (m + 1) n)
Tactic: rw [ack_succ_zero, ack_succ_succ]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)
have rw : ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
Tactic: rw [ack_succ_succ, ack_succ_succ]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
have apply : n₁ < n₂
Tactic: apply ack_strictMono_right _ (ack_strictMono_right _ _)
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
⊢ n₁ < n₂
have rwa : ∀ (h : n₁ < n₂), n₁ < n₂
Tactic: rwa [add_lt_add_iff_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
h : 0 < m + 1
⊢ ack 0 (n + 1) < ack (m + 1) (n + 1)
have rw : n + 1 + 1 < ack m (ack (m + 1) n)
Tactic: rw [ack_zero, ack_succ_succ]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
h : 0 < m + 1
⊢ m + (m + 1 + n + 1) ≤ m + ack (m + 1) n
have bc : m + 1 + n + 1 ≤ ack (m + 1) n
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 < ack m (ack (m + 1) n)
have n₁ : n + 1 + 1 ≤ m + (m + 1 + n + 1)
Tactic: calc
      n + 1 + 1 ≤ m + (m + 1 + n + 1) := by lia
      _ ≤ m + ack (m + 1) n := by gcongr; exact add_add_one_le_ack ..
      _ < ack m (ack (m + 1) n) := add_lt_ack ..
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
h : 0 < m + 1
n₁ : n + 1 + 1 ≤ m + (m + 1 + n + 1)
⊢ n + 1 + 1 < ack m (ack (m + 1) n)
have n₂ : m + (m + 1 + n + 1) ≤ m + ack (m + 1) n
Tactic: calc
      n + 1 + 1 ≤ m + (m + 1 + n + 1) := by lia
      _ ≤ m + ack (m + 1) n := by gcongr; exact add_add_one_le_ack ..
      _ < ack m (ack (m + 1) n) := add_lt_ack ..
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) (n + 1) < ack (m₂ + 1) (n + 1)
have rw : ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
Tactic: rw [ack_succ_succ, ack_succ_succ]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
⊢ ack m (n + 1) ≤ ack (m + 1) n
have zero : ack m (HAdd.hAdd (α := ℕ) 0 1) ≤ ack (m + 1) 0
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
zero : ack m (HAdd.hAdd (α := ℕ) 0 1) ≤ ack (m + 1) 0
⊢ ack m (n + 1) ≤ ack (m + 1) n
have succ : ∀ (n : ℕ), ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)
Tactic: rcases n with - | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)
have succ : ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)
Tactic: rw [ack_succ_succ]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
⊢ ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)
have apply : n + 1 + 1 ≤ m + 1 + n + 1
Tactic: apply ack_mono_right m (le_trans _ <| add_add_one_le_ack _ n)
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
k : ℕ
h : HPow.hPow (β := ℕ) k 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1) - 3
⊢ HPow.hPow (β := ℕ) (k + 1) 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1 + 1) - 3
have succ : HPow.hPow (α := ℕ) (β := ℕ) 0 2 ≤ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) - 3 →
  HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) 2 ≤ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 + 1) - 3
Tactic: cases k
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
k : ℕ
h : HPow.hPow (β := ℕ) k 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1) - 3
succ :
  HPow.hPow (α := ℕ) (β := ℕ) 0 2 ≤ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) - 3 →
    HPow.hPow (β := ℕ) (HAdd.hAdd (α := ℕ) 0 1) 2 ≤ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1 + 1) - 3
⊢ HPow.hPow (β := ℕ) (k + 1) 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1 + 1) - 3
have succ₁ : ∀ (n : ℕ),
  HPow.hPow (β := ℕ) (n + 1) 2 ≤ HPow.hPow (α := ℕ) 2 (n + 1 + 1) - 3 →
    HPow.hPow (β := ℕ) (n + 1 + 1) 2 ≤ HPow.hPow (α := ℕ) 2 (n + 1 + 1 + 1) - 3
Tactic: cases k
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) n 2 ≤ HPow.hPow (α := ℕ) 2 (n + 1) - 3
have zero : HPow.hPow (α := ℕ) (β := ℕ) 0 2 ≤ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) - 3
Tactic: induction n with
  | zero => simp
  | succ k => cases k <;> lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
zero : HPow.hPow (α := ℕ) (β := ℕ) 0 2 ≤ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) - 3
⊢ HPow.hPow (β := ℕ) n 2 ≤ HPow.hPow (α := ℕ) 2 (n + 1) - 3
have succ : ∀ (k : ℕ),
  HPow.hPow (β := ℕ) k 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1) - 3 →
    HPow.hPow (β := ℕ) (k + 1) 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1 + 1) - 3
Tactic: induction n with
  | zero => simp
  | succ k => cases k <;> lia
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m : ℕ
⊢ HPow.hPow (β := ℕ) (ack (m + 1) 0 + 1) 2 ≤ ack (m + 1 + 3) 0
have rw : HPow.hPow (β := ℕ) (ack m 1 + 1) 2 ≤ ack (m + 3) 1
Tactic: rw [ack_succ_zero, ack_succ_zero]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
⊢ HPow.hPow (β := ℕ) (ack (m + 1) (n + 1) + 1) 2 ≤ ack (m + 1 + 3) (n + 1)
have rw : HPow.hPow (β := ℕ) (ack m (ack (m + 1) n) + 1) 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
Tactic: rw [ack_succ_succ, ack_succ_succ]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
⊢ HPow.hPow (β := ℕ) (ack m (ack (m + 1) n) + 1) 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
have apply : m + 1 ≤ m + 3 + 1
Tactic: apply (ack_add_one_sq_lt_ack_add_three _ _).trans (ack_mono_right _ <| ack_mono_left _ _)
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
⊢ ∃ (m : ℕ), ∀ (n : ℕ), n.succ < ack m n
have succ : ∀ (n : ℕ), n.succ < ack 1 n
Tactic: refine ⟨1, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
n : ℕ
⊢ n.succ < ack 1 n
have succ : 1 + n < ack 1 n
Tactic: rw [succ_eq_one_add]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).1) n < ack m n
have left : ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).1) n < ack 0 n
Tactic: refine ⟨0, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
n : ℕ
⊢ (fun (n : ℕ) ↦ (unpair n).1) n < ack 0 n
have left : (fun (n : ℕ) ↦ (unpair n).1) n ≤ n
Tactic: rw [ack_zero, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).2) n < ack m n
have right : ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).2) n < ack 0 n
Tactic: refine ⟨0, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f : ℕ → ℕ
n : ℕ
⊢ (fun (n : ℕ) ↦ (unpair n).2) n < ack 0 n
have right : (fun (n : ℕ) ↦ (unpair n).2) n ≤ n
Tactic: rw [ack_zero, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ (m : ℕ), ∀ (n : ℕ), f n < ack m n
IHg : ∃ (m : ℕ), ∀ (n : ℕ), g n < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ pair (f n) (g n)) n < ack m n
have pair : ∀ (a : ℕ) (ha : ∀ (n : ℕ), f n < ack a n), ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ pair (f n) (g n)) n < ack m n
Tactic: obtain ⟨a, ha⟩ := IHf
Cleared hypotheses: IHf
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHg : ∃ (m : ℕ), ∀ (n : ℕ), g n < ack m n
a : ℕ
ha : ∀ (n : ℕ), f n < ack a n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ pair (f n) (g n)) n < ack m n
have pair : ∀ (b : ℕ) (hb : ∀ (n : ℕ), g n < ack b n), ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ pair (f n) (g n)) n < ack m n
Tactic: obtain ⟨b, hb⟩ := IHg
Cleared hypotheses: IHg
-- 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 : ℕ), (fun (n : ℕ) ↦ pair (f n) (g n)) n < ack m n
have pair : ∀ (n : ℕ), (fun (n : ℕ) ↦ pair (f n) (g n)) n < ack (max a b + 3) n
Tactic: refine ⟨max a b + 3, fun 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
n : ℕ
⊢ HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (ack (max a b) n + 1) 2
have rw : HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (max (ack a n) (ack b n) + 1) 2
Tactic: rw [max_ack_left]
-- 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
n : ℕ
⊢ HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (max (ack a n) (ack b n) + 1) 2
have hab : f n ≤ ack a n
Tactic: gcongr
-- 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
n : ℕ
hab : f n ≤ ack a n
⊢ HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (max (ack a n) (ack b n) + 1) 2
have hab₁ : g n ≤ ack b n
Tactic: gcongr
-- 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
n : ℕ
⊢ (fun (n : ℕ) ↦ pair (f n) (g n)) n < ack (max a b + 3) n
have pair : HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (ack (max a b) n + 1) 2
Tactic: 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 ..
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f f_1 g : ℕ → ℕ
hf : Nat.Primrec f_1
hg : Nat.Primrec g
IHf : ∃ (m : ℕ), ∀ (n : ℕ), f_1 n < ack m n
IHg : ∃ (m : ℕ), ∀ (n : ℕ), g n < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n
have comp : ∀ (a : ℕ) (ha : ∀ (n : ℕ), f_1 n < ack a n), ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n
Tactic: obtain ⟨a, ha⟩ := IHf
Cleared hypotheses: IHf
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f f_1 g : ℕ → ℕ
hf : Nat.Primrec f_1
hg : Nat.Primrec g
IHg : ∃ (m : ℕ), ∀ (n : ℕ), g n < ack m n
a : ℕ
ha : ∀ (n : ℕ), f_1 n < ack a n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n
have comp : ∀ (b : ℕ) (hb : ∀ (n : ℕ), g n < ack b n), ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n
Tactic: obtain ⟨b, hb⟩ := IHg
Cleared hypotheses: IHg
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHf : ∃ (m : ℕ), ∀ (n : ℕ), f n < ack m n
IHg : ∃ (m : ℕ), ∀ (n : ℕ), g n < ack m 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 prec : ∀ (a : ℕ) (ha : ∀ (n : ℕ), f n < ack a 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
Tactic: obtain ⟨a, ha⟩ := IHf
Cleared hypotheses: IHf
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
f_1 f g : ℕ → ℕ
hf : Nat.Primrec f
hg : Nat.Primrec g
IHg : ∃ (m : ℕ), ∀ (n : ℕ), g n < ack m n
a : ℕ
ha : ∀ (n : ℕ), f n < ack a 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 prec : ∀ (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
Tactic: obtain ⟨b, hb⟩ := IHg
Cleared hypotheses: IHg
-- 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 : ℕ
⊢ rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) 0 < ack (max a b + 9) (m + 0)
have apply : max a b < max a b + 9
Tactic: apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
-- 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)
⊢ g (pair m (pair 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 apply : ack (b + 4) (max m (pair 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))
Tactic: apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
-- 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)
⊢ ack (b + 4) (max m (pair 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 inl : ∀ (h₁ : pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n) < m),
  ack (b + 4) (max m (pair 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))
Tactic: rcases lt_or_ge _ m with h₁ | 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)
inl :
  ∀ (h₁ : pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n) < m),
    ack (b + 4) (max m (pair 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))
⊢ ack (b + 4) (max m (pair 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 : ∀ (h₁ : m ≤ pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n)),
  ack (b + 4) (max m (pair 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))
Tactic: rcases lt_or_ge _ m with h₁ | 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₁ : pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n) < m
⊢ ack (b + 4) (max m (pair 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 inl : ack (b + 4) m ≤ ack (max a b + 9) (m + (n + 1))
Tactic: rw [max_eq_left h₁.le]
-- 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₁ : pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n) < m
⊢ ack (b + 4) m ≤ ack (max a b + 9) (m + (n + 1))
have inl : b ≤ max a b + 5
Tactic: gcongr
-- 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₁ : pair n (rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n) < m
inl : b ≤ max a b + 5
⊢ ack (b + 4) m ≤ ack (max a b + 9) (m + (n + 1))
have inl₁ : m ≤ m + (n + 1)
Tactic: gcongr
-- 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)
⊢ ack (b + 4) (max m (pair 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) (pair 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))
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)
⊢ ack (b + 4) (pair 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) (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))
Tactic: apply (ack_pair_lt _ _ _).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)
⊢ 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 : ∀ (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))
Tactic: rcases lt_or_ge _ n with h₂ | 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)
inr :
  ∀ (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))
⊢ 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₁ : ∀ (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))
Tactic: rcases lt_or_ge _ n with h₂ | h₂