-- Mathlib/Computability/Ackermann.lean
theorem exists_lt_ack_of_nat_primrec {f : ℕ → ℕ} (hf : Nat.Primrec f) :
    ∃ m, ∀ n, f n < ack m n

Proof state:
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)

Tactic:
intro m n

Result:
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)

Proof state:
case pair.intro.intro
f✝ 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 : ℕ
⊢ f n ⊔ g n ≤ ack (a ⊔ b) n

Tactic:
rw [max_ack_left]

Result:
case pair.intro.intro
f✝ 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 : ℕ
⊢ f n ⊔ g n ≤ ack a n ⊔ ack b n

Proof state:
case succ
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
⊢ g (pair m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) < ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)

Result:
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
⊢ ack (b + 4) (m ⊔ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Proof state:
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).1) n ≤ n

Tactic:
exact unpair_left_le n

Result:
no goals

Proof state:
case inr.inr
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + (4 + 4)) (ack (a ⊔ b + 8 + 1) (m + n)) ≤ ack (a ⊔ b + 8) (ack (a ⊔ b + 8 + 1) (m + n))

Tactic:
exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)

Result:
no goals

Proof state:
case comp.intro.intro
f✝ 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 => f (g n)) n < ack m n

Tactic:
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⟩

Result:
no goals

Proof state:
case inl
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : ?m.129969 < m
⊢ ack (b + 4) (m ⊔ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
rw [max_eq_left h₁.le]

Result:
case inl
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n) < m
⊢ ack (b + 4) m ≤ ack (a ⊔ b + 9) (m + (n + 1))

Proof state:
case inr.inl
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : ?m.130122 < n
⊢ ack (b + 4 + 4) (n ⊔ rec (f m) (fun y IH => g (pair m (pair y IH))) n) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
rw [max_eq_left h₂.le, add_assoc]

Result:
case inr.inl
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : rec (f m) (fun y IH => g (pair m (pair y IH))) n < n
⊢ ack (b + (4 + 4)) n ≤ ack (a ⊔ b + 9) (m + (n + 1))

Proof state:
case prec.intro.intro
f✝ 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
this : ∀ {m n : ℕ}, rec (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n

Tactic:
exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩

Result:
no goals

Proof state:
case succ
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), n.succ < ack m n

Tactic:
refine ⟨1, fun n => ?_⟩

Result:
case succ
f : ℕ → ℕ
n : ℕ
⊢ n.succ < ack 1 n

Proof state:
case inr.inr
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (rec (f m) (fun y IH => g (pair m (pair y IH))) n) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Tactic:
apply (ack_strictMono_right _ IH).le.trans

Result:
case inr.inr
f✝ 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 (f m) (fun y IH => g (pair m (pair y IH))) n < ack (a ⊔ b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ rec (f m) (fun y IH => g (pair m (pair y IH))) n
⊢ ack (b + 4 + 4) (ack (a ⊔ b + 9) (m + n)) ≤ ack (a ⊔ b + 9) (m + (n + 1))

Proof state:
case right
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).2) n < ack m n

Tactic:
refine ⟨0, fun n => ?_⟩

Result:
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).2) n < ack 0 n

Proof state:
case zero
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun x => 0) n < ack m n

Tactic:
exact ⟨0, ack_pos 0⟩

Result:
no goals

Proof state:
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).2) n < ack 0 n

Tactic:
rw [ack_zero, Nat.lt_succ_iff]

Result:
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).2) n ≤ n