awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
bc : LE.le (α := ℕ) 1 2
bc₁ : 3 ≤ n + 3
⊢ 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)

Tactic:
gcongr
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
⊢ LE.le (α := ℕ) 1 2

Tactic:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
⊢ 3 ≤ n + 3

Tactic:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
calc : HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3
calc₁ : 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)
⊢ HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)

Tactic:
calc 2 * 3
      _ ≤ 2 * 2 ^ 3 := by simp
      _ ≤ 2 * 2 ^ (n + 3) := by gcongr <;> lia

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
zero : ack 3 0 = HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 3) - 3
succ : ∀ (n : ℕ) (IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3), ack 3 (n + 1) = HPow.hPow (α := ℕ) 2 (n + 1 + 3) - 3
⊢ ack 3 n = HPow.hPow (α := ℕ) 2 (n + 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

Premises used: Nat.mul_sub_left_distrib, Nat.sub_add_comm, two_mul, Nat.pow_succ, ack_succ_succ, HAdd.hAdd, ack_two, mul_comm, Nat.add_sub_add_right, Nat.zero, Nat.succ_add, OfNat.ofNat, Nat.succ
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
⊢ 0 < ack 0 n

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
rw : 0 < ack m 1
⊢ 0 < ack (m + 1) 0

Tactic:
rw [ack_succ_zero]

Premises used: ack_succ_zero
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
⊢ 0 < ack m 1

Tactic:
apply ack_pos
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
rw : 0 < ack m (ack (m + 1) n)
⊢ 0 < ack (m + 1) (n + 1)

Tactic:
rw [ack_succ_succ]

Premises used: ack_succ_succ
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ 0 < ack m (ack (m + 1) n)

Tactic:
apply ack_pos
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
⊢ 1 < ack (HAdd.hAdd (α := ℕ) 0 1) n

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
rw : 1 < ack (m + 1) 1
⊢ 1 < ack (m + 1 + 1) 0

Tactic:
rw [ack_succ_zero]

Premises used: ack_succ_zero
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
⊢ 1 < ack (m + 1) 1

Tactic:
apply one_lt_ack_succ_left
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
rw : 1 < ack (m + 1) (ack (m + 1 + 1) n)
⊢ 1 < ack (m + 1 + 1) (n + 1)

Tactic:
rw [ack_succ_succ]

Premises used: ack_succ_succ
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ 1 < ack (m + 1) (ack (m + 1 + 1) n)

Tactic:
apply one_lt_ack_succ_left
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
⊢ 1 < ack 0 (n + 1)

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
Goal:
n₁ n₂ : ℕ
h : n₁ < n₂
⊢ ack 0 n₁ < ack 0 n₂

Tactic:
simpa using h
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
_h : 0 < n + 1
rw : ack m 1 < ack m (ack (m + 1) n)
⊢ ack (m + 1) 0 < ack (m + 1) (n + 1)

Tactic:
rw [ack_succ_zero, ack_succ_succ]

Premises used: ack_succ_zero, ack_succ_succ
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
_h : 0 < n + 1
⊢ ack m 1 < ack m (ack (m + 1) n)

Tactic:
ack_strictMono_right _ (one_lt_ack_succ_left m n)

Premises used: one_lt_ack_succ_left
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
_h : 0 < n + 1
⊢ ack m 1 < ack m (ack (m + 1) n)

Tactic:
exact ack_strictMono_right _ (one_lt_ack_succ_left m n)

Premises used: one_lt_ack_succ_left
-- Module: Mathlib.Computability.Ackermann
Goal:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
rw : ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)
⊢ ack (m + 1) (n₁ + 1) < ack (m + 1) (n₂ + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Premises used: ack_succ_succ
-- Module: Mathlib.Computability.Ackermann
Goal:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
apply : n₁ < n₂
⊢ ack m (ack (m + 1) n₁) < ack m (ack (m + 1) n₂)

Tactic:
apply ack_strictMono_right _ (ack_strictMono_right _ _)
-- Module: Mathlib.Computability.Ackermann
Goal:
m n₁ n₂ : ℕ
h : n₁ + 1 < n₂ + 1
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : n₁ < n₂), n₁ < n₂
⊢ n₁ < n₂

Tactic:
rwa [add_lt_add_iff_right] at h

Premises used: add_lt_add_iff_right
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
⊢ Monotone (ack m)

Tactic:
(ack_strictMono_right m).monotone

Premises used: StrictMono.monotone, ack_strictMono_right
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
⊢ Function.Injective (ack m)

Tactic:
(ack_strictMono_right m).injective

Premises used: StrictMono.injective, ack_strictMono_right
-- Module: Mathlib.Computability.Ackermann
Goal:
m n₁ n₂ : ℕ
⊢ ack m n₁ < ack m n₂ ↔ n₁ < n₂

Tactic:
(ack_strictMono_right m).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, ack_strictMono_right
-- Module: Mathlib.Computability.Ackermann
Goal:
m n₁ n₂ : ℕ
⊢ ack m n₁ ≤ ack m n₂ ↔ n₁ ≤ n₂

Tactic:
(ack_strictMono_right m).le_iff_le

Premises used: ack_strictMono_right, StrictMono.le_iff_le
-- Module: Mathlib.Computability.Ackermann
Goal:
m n₁ n₂ : ℕ
⊢ ack m n₁ = ack m n₂ ↔ n₁ = n₂

Tactic:
(ack_injective_right m).eq_iff

Premises used: ack_injective_right, Function.Injective.eq_iff
-- Module: Mathlib.Computability.Ackermann
Goal:
m n₁ n₂ : ℕ
⊢ ack m (max n₁ n₂) = max (ack m n₁) (ack m n₂)

Tactic:
(ack_mono_right m).map_max

Premises used: Monotone.map_max, ack_mono_right
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
⊢ 0 + n < ack 0 n

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
⊢ m + 1 + 0 < ack (m + 1) 0

Tactic:
simpa using add_lt_ack m 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ m + 1 + n + 1 ≤ m + (m + n + 2)

Tactic:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ m + n + 2 = m + 1 + n + 1

Tactic:
ring_nf
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ m + n + 1 ≤ ack m n

Tactic:
succ_le_of_lt (add_lt_ack m n)

Premises used: Nat.succ_le_of_lt, add_lt_ack
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ m < ack m n

Tactic:
(self_le_add_right m n).trans_lt <| add_lt_ack m n

Premises used: self_le_add_right, add_lt_ack, LE.le.trans_lt
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ n < ack m n

Tactic:
(self_le_add_left n m).trans_lt <| add_lt_ack m n

Premises used: self_le_add_left, add_lt_ack, LE.le.trans_lt
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
_h : 0 < m + 1
⊢ ack 0 0 < ack (m + 1) 0

Tactic:
simpa using one_lt_ack_succ_right m 0

Premises used: one_lt_ack_succ_right, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
h : 0 < m + 1
rw : n + 1 + 1 < ack m (ack (m + 1) n)
⊢ ack 0 (n + 1) < ack (m + 1) (n + 1)

Tactic:
rw [ack_zero, ack_succ_succ]

Premises used: ack_succ_succ, ack_zero
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
h : 0 < m + 1
⊢ n + 1 + 1 ≤ m + (m + 1 + n + 1)

Tactic:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
h : 0 < m + 1
bc : m + 1 + n + 1 ≤ ack (m + 1) n
⊢ m + (m + 1 + n + 1) ≤ m + ack (m + 1) n

Tactic:
gcongr
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
h : 0 < m + 1
⊢ m + 1 + n + 1 ≤ ack (m + 1) n

Tactic:
add_add_one_le_ack ..

Premises used: add_add_one_le_ack
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
h : 0 < m + 1
⊢ m + 1 + n + 1 ≤ ack (m + 1) n

Tactic:
exact add_add_one_le_ack ..

Premises used: add_add_one_le_ack
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
h : 0 < m + 1
⊢ m + ack (m + 1) n < ack m (ack (m + 1) n)

Tactic:
add_lt_ack ..

Premises used: add_lt_ack
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
h : 0 < m + 1
n₁ : n + 1 + 1 ≤ m + (m + 1 + n + 1)
n₂ : m + (m + 1 + n + 1) ≤ m + ack (m + 1) n
⊢ n + 1 + 1 < ack 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 ..

Premises used: ack, add_lt_ack, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack (m₁ + 1) 0 < ack (m₂ + 1) 0

Tactic:
simpa using ack_strict_mono_left' 1 ((add_lt_add_iff_right 1).1 h)

Premises used: Iff.mp, OfNat.ofNat, add_lt_add_iff_right
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
rw : ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)
⊢ ack (m₁ + 1) (n + 1) < ack (m₂ + 1) (n + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Premises used: ack_succ_succ
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)

Tactic:
(ack_strict_mono_left' _ <| (add_lt_add_iff_right 1).1 h).trans
        (ack_strictMono_right _ <| ack_strict_mono_left' n h)

Premises used: ack_strictMono_right, Iff.mp, LT.lt.trans, OfNat.ofNat, add_lt_add_iff_right
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ n : ℕ
h : m₁ + 1 < m₂ + 1
⊢ ack m₁ (ack (m₁ + 1) n) < ack m₂ (ack (m₂ + 1) n)

Tactic:
exact
      (ack_strict_mono_left' _ <| (add_lt_add_iff_right 1).1 h).trans
        (ack_strictMono_right _ <| ack_strict_mono_left' n h)

Premises used: ack_strictMono_right, Iff.mp, LT.lt.trans, OfNat.ofNat, add_lt_add_iff_right
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
⊢ StrictMono (β := ℕ) fun (m : ℕ) ↦ ack m n

Tactic:
fun _m₁ _m₂ =>
  ack_strict_mono_left' n

Premises used: StrictMono, _private.0.ack_strict_mono_left'
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
⊢ Monotone (β := ℕ) fun (m : ℕ) ↦ ack m n

Tactic:
(ack_strictMono_left n).monotone

Premises used: ack_strictMono_left, StrictMono.monotone
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
⊢ Function.Injective (β := ℕ) fun (m : ℕ) ↦ ack m n

Tactic:
(ack_strictMono_left n).injective

Premises used: ack_strictMono_left, StrictMono.injective
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ n : ℕ
⊢ ack m₁ n < ack m₂ n ↔ m₁ < m₂

Tactic:
(ack_strictMono_left n).lt_iff_lt

Premises used: ack_strictMono_left, StrictMono.lt_iff_lt
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ n : ℕ
⊢ ack m₁ n ≤ ack m₂ n ↔ m₁ ≤ m₂

Tactic:
(ack_strictMono_left n).le_iff_le

Premises used: ack_strictMono_left, StrictMono.le_iff_le
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ n : ℕ
⊢ ack m₁ n = ack m₂ n ↔ m₁ = m₂

Tactic:
(ack_injective_left n).eq_iff

Premises used: Function.Injective.eq_iff, ack_injective_left
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ n : ℕ
⊢ ack (max m₁ m₂) n = max (ack m₁ n) (ack m₂ n)

Tactic:
(ack_mono_left n).map_max

Premises used: Monotone.map_max, ack_mono_left
-- Module: Mathlib.Computability.Ackermann
Goal:
m₁ m₂ n₁ n₂ : ℕ
hm : m₁ ≤ m₂
hn : n₁ ≤ n₂
⊢ ack m₁ n₁ ≤ ack m₂ n₂

Tactic:
(ack_mono_left n₁ hm).trans <| ack_mono_right m₂ hn

Premises used: ack_mono_right, LE.le.trans, ack_mono_left
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
zero : ack m (HAdd.hAdd (α := ℕ) 0 1) ≤ ack (m + 1) 0
succ : ∀ (n : ℕ), ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)
⊢ ack m (n + 1) ≤ ack (m + 1) n

Tactic:
rcases n with - | n
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
⊢ ack m (HAdd.hAdd (α := ℕ) 0 1) ≤ ack (m + 1) 0

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
succ : ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)
⊢ ack m (n + 1 + 1) ≤ ack (m + 1) (n + 1)

Tactic:
rw [ack_succ_succ]

Premises used: ack_succ_succ
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
apply : n + 1 + 1 ≤ m + 1 + n + 1
⊢ ack m (n + 1 + 1) ≤ ack m (ack (m + 1) n)

Tactic:
apply ack_mono_right m (le_trans _ <| add_add_one_le_ack _ n)

Premises used: ack_mono_right, add_add_one_le_ack, le_trans
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ n + 1 + 1 ≤ m + 1 + n + 1

Tactic:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
⊢ HPow.hPow (α := ℕ) (β := ℕ) 0 2 ≤ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) - 3

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
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
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
⊢ HPow.hPow (β := ℕ) (k + 1) 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1 + 1) - 3

Tactic:
cases k
-- Module: Mathlib.Computability.Ackermann
Goal:
h : 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:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
h : 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:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
zero : HPow.hPow (α := ℕ) (β := ℕ) 0 2 ≤ HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 1) - 3
succ :
  ∀ (k : ℕ),
    HPow.hPow (β := ℕ) k 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1) - 3 →
      HPow.hPow (β := ℕ) (k + 1) 2 ≤ HPow.hPow (α := ℕ) 2 (k + 1 + 1) - 3
⊢ HPow.hPow (β := ℕ) n 2 ≤ HPow.hPow (α := ℕ) 2 (n + 1) - 3

Tactic:
induction n with
  | zero => simp
  | succ k => cases k <;> lia

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
⊢ HPow.hPow (β := ℕ) (ack 0 n + 1) 2 ≤ ack (HAdd.hAdd (α := ℕ) 0 3) n

Tactic:
simpa using sq_le_two_pow_add_one_minus_three (n + 2)

Premises used: HAdd.hAdd, OfNat.ofNat, _private.0.sq_le_two_pow_add_one_minus_three
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
rw : HPow.hPow (β := ℕ) (ack m 1 + 1) 2 ≤ ack (m + 3) 1
⊢ HPow.hPow (β := ℕ) (ack (m + 1) 0 + 1) 2 ≤ ack (m + 1 + 3) 0

Tactic:
rw [ack_succ_zero, ack_succ_zero]

Premises used: ack_succ_zero
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
⊢ HPow.hPow (β := ℕ) (ack m 1 + 1) 2 ≤ ack (m + 3) 1

Tactic:
apply ack_add_one_sq_lt_ack_add_three
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
rw : HPow.hPow (β := ℕ) (ack m (ack (m + 1) n) + 1) 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)
⊢ HPow.hPow (β := ℕ) (ack (m + 1) (n + 1) + 1) 2 ≤ ack (m + 1 + 3) (n + 1)

Tactic:
rw [ack_succ_succ, ack_succ_succ]

Premises used: ack_succ_succ
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
apply : m + 1 ≤ m + 3 + 1
⊢ HPow.hPow (β := ℕ) (ack m (ack (m + 1) n) + 1) 2 ≤ ack (m + 3) (ack (m + 3 + 1) n)

Tactic:
apply (ack_add_one_sq_lt_ack_add_three _ _).trans (ack_mono_right _ <| ack_mono_left _ _)

Premises used: ack_mono_right, LE.le.trans, ack_mono_left
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ m + 1 ≤ m + 3 + 1

Tactic:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
m n k : ℕ
⊢ ack m (ack n k) < ack (max m n + 2) k

Tactic:
calc
    ack m (ack n k) ≤ ack (max m n) (ack n k) := ack_mono_left _ (le_max_left _ _)
    _ < ack (max m n) (ack (max m n + 1) k) :=
      ack_strictMono_right _ <| ack_strictMono_left k <| lt_succ_of_le <| le_max_right m n
    _ = ack (max m n + 1) (k + 1) := (ack_succ_succ _ _).symm
    _ ≤ ack (max m n + 2) k := ack_succ_right_le_ack_succ_left _ _

Premises used: le_max_right, ack_strictMono_left, Trans.trans, ack_succ_succ, Nat.lt_succ_of_le, ack_succ_right_le_ack_succ_left, ack_strictMono_right, Eq.symm, le_max_left, ack_mono_left
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
⊢ m ≤ m + 2

Tactic:
lia
-- Module: Mathlib.Computability.Ackermann
Goal:
m n k : ℕ
⊢ ack m (pair n k) < ack (m + 4) (max n k)

Tactic:
(ack_strictMono_right m <| pair_lt_max_add_one_sq n k).trans <|
    ack_add_one_sq_lt_ack_add_four _ _

Premises used: Nat.pair_lt_max_add_one_sq, ack_add_one_sq_lt_ack_add_four, ack_strictMono_right, LT.lt.trans
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (x : ℕ) ↦ (0 : ℕ)) n < ack m n

Tactic:
⟨0, ack_pos 0⟩

Premises used: ack_pos, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (x : ℕ) ↦ (0 : ℕ)) n < ack m n

Tactic:
exact ⟨0, ack_pos 0⟩
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
⊢ ∃ (m : ℕ), ∀ (n : ℕ), n.succ < ack m n

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

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
succ : ∀ (n : ℕ), n.succ < ack 1 n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), n.succ < ack m n

Tactic:
refine ⟨1, fun n => ?_⟩
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
n : ℕ
succ : 1 + n < ack 1 n
⊢ n.succ < ack 1 n

Tactic:
rw [succ_eq_one_add]

Premises used: Nat.succ_eq_one_add
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
n : ℕ
⊢ 1 + n < ack 1 n

Tactic:
apply add_lt_ack

Premises used: add_lt_ack
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).1) n < ack m n

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

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
left : ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).1) n < ack 0 n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).1) n < ack m n

Tactic:
refine ⟨0, fun n => ?_⟩
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
n : ℕ
left : (fun (n : ℕ) ↦ (unpair n).1) n ≤ n
⊢ (fun (n : ℕ) ↦ (unpair n).1) n < ack 0 n

Tactic:
rw [ack_zero, Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff, ack_zero
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
n : ℕ
⊢ (fun (n : ℕ) ↦ (unpair n).1) n ≤ n

Tactic:
unpair_left_le n

Premises used: Nat.unpair_left_le
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
n : ℕ
⊢ (fun (n : ℕ) ↦ (unpair n).1) n ≤ n

Tactic:
exact unpair_left_le n

Premises used: Nat.unpair_left_le
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).2) n < ack m n

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

Premises used: Exists.intro, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
right : ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).2) n < ack 0 n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ (unpair n).2) n < ack m n

Tactic:
refine ⟨0, fun n => ?_⟩
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
n : ℕ
right : (fun (n : ℕ) ↦ (unpair n).2) n ≤ n
⊢ (fun (n : ℕ) ↦ (unpair n).2) n < ack 0 n

Tactic:
rw [ack_zero, Nat.lt_succ_iff]

Premises used: Nat.lt_succ_iff, ack_zero
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
n : ℕ
⊢ (fun (n : ℕ) ↦ (unpair n).2) n ≤ n

Tactic:
unpair_right_le n

Premises used: Nat.unpair_right_le
-- Module: Mathlib.Computability.Ackermann
Goal:
f : ℕ → ℕ
n : ℕ
⊢ (fun (n : ℕ) ↦ (unpair n).2) n ≤ n

Tactic:
exact unpair_right_le n

Premises used: Nat.unpair_right_le
-- 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
pair : ∀ (a : ℕ) (ha : ∀ (n : ℕ), f n < ack a n), ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ Nat.pair (f n) (g n)) n < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ Nat.pair (f n) (g 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
pair : ∀ (b : ℕ) (hb : ∀ (n : ℕ), g n < ack b n), ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ Nat.pair (f n) (g n)) n < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ Nat.pair (f n) (g 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 : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ pair (f n) (g n)) n < ack m n

Tactic:
⟨max a b + 3, fun n => ?_⟩

Premises used: HAdd.hAdd, Max.max, Exists.intro, 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
pair : ∀ (n : ℕ), (fun (n : ℕ) ↦ Nat.pair (f n) (g n)) n < ack (max a b + 3) n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ Nat.pair (f n) (g n)) n < ack m n

Tactic:
refine ⟨max a b + 3, fun n => ?_⟩
-- 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
n : ℕ
⊢ pair (f n) (g n) < HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2

Tactic:
pair_lt_max_add_one_sq ..

Premises used: Nat.pair_lt_max_add_one_sq
-- 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
n : ℕ
rw : HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (max (ack a n) (ack b n) + 1) 2
⊢ HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (ack (max a b) n + 1) 2

Tactic:
rw [max_ack_left]

Premises used: max_ack_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
n : ℕ
hab : f n ≤ ack a n
hab₁ : g n ≤ ack b n
⊢ HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (max (ack a n) (ack b n) + 1) 2

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
n : ℕ
⊢ f n ≤ ack a n

Tactic:
(ha n).le

Premises used: LT.lt.le
-- 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
n : ℕ
⊢ g n ≤ ack b n

Tactic:
(hb n).le

Premises used: LT.lt.le
-- 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
n : ℕ
⊢ f n ≤ ack a n

Tactic:
exacts [(ha n).le, (hb n).le]

Premises used: LT.lt.le
-- 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
n : ℕ
⊢ HPow.hPow (β := ℕ) (ack (max a b) n + 1) 2 ≤ ack (max a b + 3) n

Tactic:
ack_add_one_sq_lt_ack_add_three ..

Premises used: ack_add_one_sq_lt_ack_add_three
-- 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
n : ℕ
pair : HPow.hPow (β := ℕ) (max (f n) (g n) + 1) 2 ≤ HPow.hPow (β := ℕ) (ack (max a b) n + 1) 2
⊢ (fun (n : ℕ) ↦ Nat.pair (f n) (g n)) n < ack (max a b + 3) n

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 ..

Premises used: ack_add_one_sq_lt_ack_add_three, ack, Nat.pair, Nat.pair_lt_max_add_one_sq, HAdd.hAdd, Max.max, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
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
comp : ∀ (a : ℕ) (ha : ∀ (n : ℕ), f_1 n < ack a n), ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n

Tactic:
obtain ⟨a, ha⟩ := IHf
-- Module: Mathlib.Computability.Ackermann
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
comp : ∀ (b : ℕ) (hb : ∀ (n : ℕ), g n < ack b n), ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n
⊢ ∃ (m : ℕ), ∀ (n : ℕ), (fun (n : ℕ) ↦ f_1 (g n)) n < ack m n

Tactic:
obtain ⟨b, hb⟩ := IHg