-- Module: Mathlib.Computability.Ackermann
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
right : ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).2) n < ack m n
pair :
  ∀ {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 : ℕ) ↦ Nat.pair (f n) (g n)) n < ack m n
comp :
  ∀ {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 : ℕ) ↦ f (g n)) n < ack m n
prec :
  ∀ {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 (Nat.pair z (Nat.pair y IH))) n)
            n <
          ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), f 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⟩

Premises used: ack_add_one_sq_lt_ack_add_three, Nat.pair, Nat.pair_lt_max_add_one_sq, add_lt_ack, Nat.succ_eq_one_add, Nat.lt_succ_iff, Nat.zero, ack_zero, Nat.succ