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

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

case left
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).fst) n < ack m n

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

case pair
f✝ 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

case comp
f✝ 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

case prec
f✝ 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 (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
f : ℕ → ℕ
hf : Nat.Primrec f
⊢ ∃ m, ∀ (n : ℕ), f n < ack m n
induction' hf with f g hf hg IHf IHg f g hf hg IHf IHg f g hf hg IHf IHg
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
⊢ ∃ m, ∀ (n : ℕ), (fun n => pair (f n) (g n)) n < ack m n

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

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
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
case pair
f✝ 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

case comp
f✝ 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

case prec
f✝ 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 (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
all_goals cases' IHf with a ha; cases' IHg with b hb
no goals
case zero
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun x => 0) n < ack m n
exact ⟨0, ack_pos 0⟩
case succ
f : ℕ → ℕ
n : ℕ
⊢ succ n < ack 1 n
case succ
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), succ n < ack m n
refine' ⟨1, fun n => _⟩
case succ
f : ℕ → ℕ
n : ℕ
⊢ 1 + n < ack 1 n
case succ
f : ℕ → ℕ
n : ℕ
⊢ succ n < ack 1 n
rw [succ_eq_one_add]
no goals
case succ
f : ℕ → ℕ
n : ℕ
⊢ 1 + n < ack 1 n
apply add_lt_ack
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).fst) n < ack 0 n
case left
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).fst) n < ack m n
refine' ⟨0, fun n => _⟩
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).fst) n ≤ n
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).fst) n < ack 0 n
rw [ack_zero, lt_succ_iff]
no goals
case left
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).fst) n ≤ n
exact unpair_left_le n
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).snd) n < ack 0 n
case right
f : ℕ → ℕ
⊢ ∃ m, ∀ (n : ℕ), (fun n => (unpair n).snd) n < ack m n
refine' ⟨0, fun n => _⟩
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).snd) n ≤ n
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).snd) n < ack 0 n
rw [ack_zero, lt_succ_iff]
no goals
case right
f : ℕ → ℕ
n : ℕ
⊢ (fun n => (unpair n).snd) n ≤ n
exact unpair_right_le n
case prec.intro
f✝ 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 (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
case prec
f✝ 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 (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
cases' IHf with a ha
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
⊢ ∃ m, ∀ (n : ℕ), unpaired (fun z n => rec (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
case prec.intro
f✝ 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 (f z) (fun y IH => g (pair z (pair y IH))) n) n < ack m n
cases' IHg with b hb
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 : ℕ
⊢ max (f n) (g n) ≤ ack (max a b) n
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
⊢ ∃ m, ∀ (n : ℕ), (fun n => pair (f n) (g n)) n < ack m n
refine'
  ⟨max a b + 3, fun n =>
    (pair_lt_max_add_one_sq _ _).trans_le <|
      (pow_le_pow_of_le_left (add_le_add_right _ _) 2).trans <|
        ack_add_one_sq_lt_ack_add_three _ _⟩
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 : ℕ
⊢ max (f n) (g n) ≤ max (ack a n) (ack b n)
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 : ℕ
⊢ max (f n) (g n) ≤ ack (max a b) n
rw [max_ack_left]
no goals
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 : ℕ
⊢ max (f n) (g n) ≤ max (ack a n) (ack b n)
exact max_le_max (ha n).le (hb n).le
no goals
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
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⟩
no goals
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 (max 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
exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩
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 (max a b + 9) (m + n)
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 (max a b + 9) (m + n)
intro m n
case zero
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 : ℕ
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) zero < ack (max a b + 9) (m + zero)

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 (max a b + 9) (m + n)
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) (succ n) < ack (max a b + 9) (m + succ n)
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 (max a b + 9) (m + n)
induction' n with n IH
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 : ℕ
⊢ max a b < max a b + 9
case zero
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 : ℕ
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) zero < ack (max a b + 9) (m + zero)
apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)
no goals
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 : ℕ
⊢ max a b < max a b + 9
linarith
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 (max a b + 9) (m + n)
⊢ g (pair m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) < ack (max a b + 9) (m + succ n)
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 (max a b + 9) (m + n)
⊢ rec (f m) (fun y IH => g (pair m (pair y IH))) (succ n) < ack (max a b + 9) (m + succ n)
simp only [ge_iff_le]
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 (max a b + 9) (m + n)
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)
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 (max a b + 9) (m + n)
⊢ g (pair m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) < ack (max a b + 9) (m + succ n)
apply (hb _).trans ((ack_pair_lt _ _ _).trans_le _)
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 (max a b + 9) (m + n)
h₁ : ?m.125091 < m
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)

case 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 (max a b + 9) (m + n)
h₁ : m ≤ ?m.125091
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)
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 (max a b + 9) (m + n)
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)
cases' lt_or_le _ m with h₁ h₁
case 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 (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4) (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
case 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 (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)
rw [max_eq_right h₁]
case 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 (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
case 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 (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4) (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
apply (ack_pair_lt _ _ _).le.trans
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 (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : ?m.125452 < n
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)

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 (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : n ≤ ?m.125452
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
case 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 (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
cases' lt_or_le _ n with h₂ h₂
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 (max 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 (max a b + 9) (m + succ n)
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 (max 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) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
rw [max_eq_right h₂]
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 (max 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 (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + succ n)
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 (max 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 (max a b + 9) (m + succ n)
apply (ack_strictMono_right _ IH).le.trans
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 (max 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 (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8) (ack (max a b + 8 + 1) (m + n))
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 (max 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 (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + succ n)
rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
    ack_succ_succ (_ + 8), add_assoc]
no goals
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 (max 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 (max a b + 8 + 1) (m + n)) ≤ ack (max a b + 8) (ack (max a b + 8 + 1) (m + n))
exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)
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 (max 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 (max a b + 9) (m + succ n)
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 (max a b + 9) (m + n)
h₁ : ?m.125091 < m
⊢ ack (b + 4) (max m (pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n))) ≤ ack (max a b + 9) (m + succ n)
rw [max_eq_left h₁.le]
no goals
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 (max 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 (max a b + 9) (m + succ n)
exact ack_le_ack (Nat.add_le_add (le_max_right a b) <| by norm_num)
                 (self_le_add_right m _)
no goals
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 (max a b + 9) (m + n)
h₁ : pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n) < m
⊢ 4 ≤ 9
norm_num
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 (max 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 (max a b + 9) (m + succ n)
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 (max a b + 9) (m + n)
h₁ : m ≤ pair n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)
h₂ : ?m.125452 < n
⊢ ack (b + 4 + 4) (max n (rec (f m) (fun y IH => g (pair m (pair y IH))) n)) ≤ ack (max a b + 9) (m + succ n)
rw [max_eq_left h₂.le, add_assoc]
no goals
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 (max 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 (max a b + 9) (m + succ n)
exact
  ack_le_ack (Nat.add_le_add (le_max_right a b) <| by norm_num)
    ((le_succ n).trans <| self_le_add_left _ _)
no goals
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 (max 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
⊢ 4 + 4 ≤ 9
norm_num