awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Ackermann
Goal:
f f_1 g : ℕ → ℕ
hf : Nat.Primrec f_1
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f_1 n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n

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

Premises used: HAdd.hAdd, Max.max, ack_strictMono_right, Exists.intro, ack_ack_lt_ack_max_add_two, LT.lt.trans, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
f f_1 g : ℕ → ℕ
hf : Nat.Primrec f_1
hg : Nat.Primrec g
a : ℕ
ha : ∀ (n : ℕ), f_1 n < ack a n
b : ℕ
hb : ∀ (n : ℕ), g n < ack b n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (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⟩
-- Module: Mathlib.Computability.Ackermann
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
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
⊢ ∃ (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
-- Module: Mathlib.Computability.Ackermann
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
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
⊢ ∃ (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
-- Module: Mathlib.Computability.Ackermann
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 : ℕ
apply : max a b < max a b + 9
⊢ rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) 0 < ack (max a b + 9) (m + 0)

Tactic:
apply (ha m).trans (ack_strictMono_left m <| (le_max_left a b).trans_lt _)

Premises used: ack_strictMono_left, LT.lt.trans, le_max_left, LE.le.trans_lt
-- Module: Mathlib.Computability.Ackermann
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 : ℕ
⊢ max a b < max a b + 9

Tactic:
lia
-- Module: Mathlib.Computability.Ackermann
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)
succ :
  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))
⊢ 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:
simp only
-- Module: Mathlib.Computability.Ackermann
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)
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))
⊢ 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))

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

Premises used: ack_pair_lt, LT.lt.trans_le, LT.lt.trans
-- Module: Mathlib.Computability.Ackermann
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))
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))
⊢ 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₁

Premises used: lt_or_ge
-- Module: Mathlib.Computability.Ackermann
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 : ack (b + 4) m ≤ 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))

Tactic:
rw [max_eq_left h₁.le]

Premises used: LT.lt.le, max_eq_left
-- Module: Mathlib.Computability.Ackermann
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
inl₁ : m ≤ m + (n + 1)
⊢ ack (b + 4) m ≤ ack (max a b + 9) (m + (n + 1))

Tactic:
gcongr
-- Module: Mathlib.Computability.Ackermann
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
⊢ b ≤ max a b + 5

Tactic:
omega
-- Module: Mathlib.Computability.Ackermann
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
⊢ m ≤ m + (n + 1)

Tactic:
omega
-- Module: Mathlib.Computability.Ackermann
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 :
  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))
⊢ 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:
rw [max_eq_right h₁]

Premises used: max_eq_right
-- Module: Mathlib.Computability.Ackermann
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 :
  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) (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 (ack_pair_lt _ _ _).le.trans

Premises used: LT.lt.le, ack_pair_lt, LE.le.trans
-- Module: Mathlib.Computability.Ackermann
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))
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))
⊢ 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₂

Premises used: lt_or_ge
-- Module: Mathlib.Computability.Ackermann
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
inr : ack (b + HAdd.hAdd (α := ℕ) 4 4) 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))

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

Premises used: add_assoc, LT.lt.le, max_eq_left
-- Module: Mathlib.Computability.Ackermann
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
⊢ HAdd.hAdd (α := ℕ) 4 4 ≤ 9

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
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 + HAdd.hAdd (α := ℕ) 4 4) n ≤ ack (max a b + 9) (m + (n + 1))

Tactic:
exact
            ack_le_ack (Nat.add_le_add (le_max_right a b) <| by simp)
              ((le_succ n).trans <| self_le_add_left _ _)

Premises used: le_max_right, self_le_add_left, Nat.le_succ, Nat.add_le_add, LE.le.trans, ack_le_ack
-- Module: Mathlib.Computability.Ackermann
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
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))
⊢ 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:
rw [max_eq_right h₂]

Premises used: max_eq_right
-- Module: Mathlib.Computability.Ackermann
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
inr : ack (b + 4 + 4) (ack (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + (n + 1))
⊢ 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:
apply (ack_strictMono_right _ IH).le.trans

Premises used: LT.lt.le, ack_strictMono_right, LE.le.trans
-- Module: Mathlib.Computability.Ackermann
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
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))
⊢ ack (b + 4 + 4) (ack (max a b + 9) (m + n)) ≤ ack (max a b + 9) (m + (n + 1))

Tactic:
rw [add_succ m, add_succ _ 8, succ_eq_add_one, succ_eq_add_one,
            ack_succ_succ (_ + 8), add_assoc]

Premises used: Nat.succ_eq_add_one, add_assoc, ack_succ_succ, HAdd.hAdd, Nat.add_succ, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
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 + 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:
ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)

Premises used: le_max_right, le_rfl, Nat.add_le_add, ack_mono_left
-- Module: Mathlib.Computability.Ackermann
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 + 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:
exact ack_mono_left _ (Nat.add_le_add (le_max_right a b) le_rfl)

Premises used: le_max_right, le_rfl, Nat.add_le_add, ack_mono_left
-- Module: Mathlib.Computability.Ackermann
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)
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))
⊢ rec (motive := fun (x : ℕ) ↦ ℕ) (f m) (fun (y IH : ℕ) ↦ g (pair m (pair y IH))) n < ack (max a b + 9) (m + n)

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)

Premises used: le_max_right, ack_strictMono_left, le_rfl, Nat.succ_eq_add_one, add_assoc, self_le_add_left, LT.lt.le, ack_succ_succ, Nat.le_succ, ack_pair_lt, HAdd.hAdd, LT.lt.trans_le, Nat.add_succ, Nat.add_le_add, LT.lt.trans, Nat.zero, lt_or_ge, LE.le.trans, OfNat.ofNat, le_max_left, LE.le.trans_lt, Nat.succ, ack_le_ack, ack_mono_left
-- Module: Mathlib.Computability.Ackermann
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)

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)
-- Module: Mathlib.Computability.Ackermann
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
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)
⊢ ∃ (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:
⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩

Premises used: ack_mono_right, HAdd.hAdd, Max.max, LT.lt.trans_le, Exists.intro, Nat.unpair_add_le, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
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
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)
⊢ ∃ (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:
exact ⟨max a b + 9, fun n => this.trans_le <| ack_mono_right _ <| unpair_add_le n⟩
-- Module: Mathlib.Computability.Ackermann
Goal:
h : Nat.Primrec fun (n : ℕ) ↦ ack n n
obtain : ∀ (m : ℕ) (hm : ∀ (n : ℕ), ack n n < ack m n), False
⊢ False

Tactic:
obtain ⟨m, hm⟩ := exists_lt_ack_of_nat_primrec h

Premises used: exists_lt_ack_of_nat_primrec
-- Module: Mathlib.Computability.Ackermann
Goal:
h : Nat.Primrec fun (n : ℕ) ↦ ack n n
m : ℕ
hm : ∀ (n : ℕ), ack n n < ack m n
⊢ False

Tactic:
(hm m).false

Premises used: LT.lt.false
-- Module: Mathlib.Computability.Ackermann
Goal:
h : Nat.Primrec fun (n : ℕ) ↦ ack n n
m : ℕ
hm : ∀ (n : ℕ), ack n n < ack m n
⊢ False

Tactic:
exact (hm m).false

Premises used: LT.lt.false
-- Module: Mathlib.Computability.Ackermann
Goal:
rw : ¬Nat.Primrec fun (n : ℕ) ↦ ack n n
⊢ ¬Primrec (β := ℕ) fun (n : ℕ) ↦ ack n n

Tactic:
rw [Primrec.nat_iff]

Premises used: Primrec.nat_iff
-- Module: Mathlib.Computability.Ackermann
Goal:
⊢ ¬Nat.Primrec fun (n : ℕ) ↦ ack n n

Tactic:
not_nat_primrec_ack_self

Premises used: not_nat_primrec_ack_self
-- Module: Mathlib.Computability.Ackermann
Goal:
⊢ ¬Nat.Primrec fun (n : ℕ) ↦ ack n n

Tactic:
exact not_nat_primrec_ack_self

Premises used: not_nat_primrec_ack_self
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p : ℝ
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
⊢ 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

Tactic:
filter_upwards [eventually_gt_atTop 1] with x hx

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
h : DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ z ^ p) x
h₁ : DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 - ε z) 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:
rw [deriv_fun_mul]

Premises used: deriv_fun_mul
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
⊢ x ≠ 0

Tactic:
positivity
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ z ^ p) x

Tactic:
exact differentiableAt_rpow_const_of_ne _ (by positivity)

Premises used: Real.differentiableAt_rpow_const_of_ne
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 - ε z) x

Tactic:
differentiableAt_one_sub_smoothingFn hx

Premises used: AkraBazziRecurrence.differentiableAt_one_sub_smoothingFn
-- Module: Mathlib.Computability.AkraBazzi.AkraBazzi
Goal:
p x : ℝ
hx : 1 < x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (z : ℝ) ↦ 1 - ε z) x

Tactic:
exact differentiableAt_one_sub_smoothingFn hx

Premises used: AkraBazziRecurrence.differentiableAt_one_sub_smoothingFn