internlm/Lean-Github huggingface dataset:
Theorem: quickSortImpl.simp_step
Proof state before:
α : Type
inst✝ : Ord α
n : Nat
arr : Vec α n
first : Nat
last : Fin n
lt : first < ↑last
⊢ let parted := partition arr ⟨first, ⋯⟩ last ⋯;
  let mid := parted.fst.val;
  (if lt : first < ↑last then
      let parted := partition arr ⟨first, ⋯⟩ last ⋯;
      let mid := parted.fst.val;
      let hm := ⋯;
      let arr_1 := parted.snd;
      let_fun this := ⋯;
      let_fun this_1 := ⋯;
      let arr_2 := quickSortImpl arr_1 first mid.prev;
      quickSortImpl arr_2 (↑mid + 1) last
    else arr) =
    quickSortImpl (quickSortImpl parted.snd first mid.prev) (↑mid + 1) last
Tactic:
simp [*]
Proof state after:
no goals
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ prodPrimes b = prodPrimes a * ∏ p in primes (Finset.Ioc a b), p
Tactic:
rw [← Nat.Ico_succ_succ]
Proof state after:
b a : ℕ
ha : a ≤ b
⊢ prodPrimes b = prodPrimes a * ∏ p in primes (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ prodPrimes b = prodPrimes a * ∏ p in primes (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Tactic:
simp [prodPrimes, primes]
Proof state after:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.range (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Tactic:
rw [Finset.range_eq_Ico]
Proof state after:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    (∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)), p) *
      ∏ p in Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)), p
Tactic:
rw [← Finset.prod_union]
Proof state after:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in
      Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)) ∪
        Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)),
      x

b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in
      Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)) ∪
        Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)),
      x

b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
Tactic:
. rw [← Finset.filter_union]
  rw [Finset.Ico_union_Ico_eq_Ico (Nat.zero_le a.succ) (Nat.succ_le_succ ha)]
Proof state after:
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
Tactic:
. apply Finset.disjoint_filter_filter
  apply Finset.Ico_disjoint_Ico_consecutive
Proof state after:
no goals
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in
      Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)) ∪
        Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)),
      x
Tactic:
rw [← Finset.filter_union]
Proof state after:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a) ∪ Finset.Ico (Nat.succ a) (Nat.succ b)), x
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ b)), p =
    ∏ x in Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a) ∪ Finset.Ico (Nat.succ a) (Nat.succ b)), x
Tactic:
rw [Finset.Ico_union_Ico_eq_Ico (Nat.zero_le a.succ) (Nat.succ_le_succ ha)]
Proof state after:
no goals
Theorem: prodPrimesSplit
Proof state before:
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.filter Nat.Prime (Finset.Ico 0 (Nat.succ a)))
    (Finset.filter Nat.Prime (Finset.Ico (Nat.succ a) (Nat.succ b)))
Tactic:
apply Finset.disjoint_filter_filter
Proof state after:
case a
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.Ico 0 (Nat.succ a)) (Finset.Ico (Nat.succ a) (Nat.succ b))
Theorem: prodPrimesSplit
Proof state before:
case a
b a : ℕ
ha : a ≤ b
⊢ Disjoint (Finset.Ico 0 (Nat.succ a)) (Finset.Ico (Nat.succ a) (Nat.succ b))
Tactic:
apply Finset.Ico_disjoint_Ico_consecutive
Proof state after:
no goals
Theorem: natRealCoeLtCoe
Proof state before:
a b : ℕ
⊢ ↑a < ↑b ↔ a < b
Tactic:
simp
Proof state after:
no goals
Theorem: natRealCoeLeCoe
Proof state before:
a b : ℕ
⊢ ↑a ≤ ↑b ↔ a ≤ b
Tactic:
simp
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [← natRealCoeLeCoe] at h
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
have : 4^(↑n/3 : ℝ) = 4^(↑n : ℝ) / 4^(2*↑n/3 : ℝ)
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. rw [eq_div_iff]
  swap; {apply ne_of_gt; apply Real.rpow_pos_of_pos (by norm_num)}
  rw [← Real.rpow_add (by norm_num)]
  simp [Real.rpow_def_of_pos]  norm_num
  push_cast
  simp [div_add_div_same]
  norm_cast
  rw [(by linarith : n + 2*n = n*3)]
  simp
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [this]
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ ↑n / 4 ^ (2 * ↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ ↑n / 4 ^ (2 * ↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
clear this
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n / 4 ^ (2 * ↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n / 4 ^ (2 * ↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [div_le_iff]
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)
Tactic:
swap
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Tactic:
{apply Real.rpow_pos_of_pos; norm_num}
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Tactic:
rw [Real.rpow_nat_cast]
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Tactic:
norm_cast
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(4 ^ n) ≤ ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(4 ^ n) ≤ ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Tactic:
apply le_trans h
Proof state after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)) ≤
    ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)) ≤
    ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Tactic:
clear h
Proof state after:
n : ℕ
hn : 0 < n
⊢ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)) ≤
    ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)) ≤
    ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Tactic:
push_cast
Proof state after:
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Tactic:
apply mul_le_mul
Proof state after:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. rw [← Real.rpow_nat_cast]
  rw [Real.rpow_le_rpow_left_iff (by norm_cast; linarith)]
  simp [-Real.sqrt_mul']
  norm_cast
  apply Real.nat_sqrt_le_real_sqrt
Proof state after:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. rw [← Real.rpow_nat_cast]
  rw [Real.rpow_le_rpow_left_iff (by norm_cast)]
  rw [le_div_iff (by norm_num)]
  norm_cast
  apply Nat.le_trans (Nat.mul_le_mul_right 3 (Nat.pred_le _))
  apply Nat.div_mul_le_self
Proof state after:
case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. apply pow_nonneg (by norm_num)
Proof state after:
case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. apply Real.rpow_nonneg_of_nonneg (by norm_cast; linarith)
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
Tactic:
rw [eq_div_iff]
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n

case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n

case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0
Tactic:
swap
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0

case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0

case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n
Tactic:
{apply ne_of_gt; apply Real.rpow_pos_of_pos (by norm_num)}
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n
Tactic:
rw [← Real.rpow_add (by norm_num)]
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3 + 2 * ↑n / 3) = 4 ^ ↑n
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3 + 2 * ↑n / 3) = 4 ^ ↑n
Tactic:
simp [Real.rpow_def_of_pos]
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n ∨ 4 = -1
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n ∨ 4 = -1
Tactic:
norm_num
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n
Tactic:
simp [div_add_div_same]
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ (↑n + 2 * ↑n) / 3 = ↑n
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ (↑n + 2 * ↑n) / 3 = ↑n
Tactic:
norm_cast
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(n + 2 * n) / 3 = ↑n
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(n + 2 * n) / 3 = ↑n
Tactic:
rw [(by linarith : n + 2*n = n*3)]
Proof state after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(n * 3) / 3 = ↑n
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(n * 3) / 3 = ↑n
Tactic:
simp
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0
Tactic:
apply ne_of_gt
Proof state after:
case this.h
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)
Theorem: rpowDivThreeLe
Proof state before:
case this.h
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)
Tactic:
apply Real.rpow_pos_of_pos (by norm_num)
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ n + 2 * n = n * 3
Tactic:
linarith
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)
Tactic:
apply Real.rpow_pos_of_pos
Proof state after:
case hx
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4
Theorem: rpowDivThreeLe
Proof state before:
case hx
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [← Real.rpow_nat_cast]
Proof state after:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ ↑(1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Theorem: rpowDivThreeLe
Proof state before:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ ↑(1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [Real.rpow_le_rpow_left_iff (by norm_cast; linarith)]
Proof state after:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(1 + Nat.sqrt (2 * n)) ≤ 1 + Real.sqrt (2 * ↑n)
Theorem: rpowDivThreeLe
Proof state before:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(1 + Nat.sqrt (2 * n)) ≤ 1 + Real.sqrt (2 * ↑n)
Tactic:
simp [-Real.sqrt_mul']
Proof state after:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(Nat.sqrt (2 * n)) ≤ Real.sqrt (2 * ↑n)
Theorem: rpowDivThreeLe
Proof state before:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(Nat.sqrt (2 * n)) ≤ Real.sqrt (2 * ↑n)
Tactic:
norm_cast
Proof state after:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(Nat.sqrt (2 * n)) ≤ Real.sqrt ↑(2 * n)
Theorem: rpowDivThreeLe
Proof state before:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(Nat.sqrt (2 * n)) ≤ Real.sqrt ↑(2 * n)
Tactic:
apply Real.nat_sqrt_le_real_sqrt
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ 1 < 2 * ↑n
Tactic:
norm_cast
Proof state after:
n : ℕ
hn : 0 < n
⊢ 1 < 2 * n
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ 1 < 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)
Tactic:
rw [← Real.rpow_nat_cast]
Proof state after:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ ↑(Nat.pred (2 * n / 3)) ≤ 4 ^ (2 * ↑n / 3)
Theorem: rpowDivThreeLe
Proof state before:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ ↑(Nat.pred (2 * n / 3)) ≤ 4 ^ (2 * ↑n / 3)
Tactic:
rw [Real.rpow_le_rpow_left_iff (by norm_cast)]
Proof state after:
case h₂
n : ℕ
hn : 0 < n
⊢ ↑(Nat.pred (2 * n / 3)) ≤ 2 * ↑n / 3
Theorem: rpowDivThreeLe
Proof state before:
case h₂
n : ℕ
hn : 0 < n
⊢ ↑(Nat.pred (2 * n / 3)) ≤ 2 * ↑n / 3
Tactic:
rw [le_div_iff (by norm_num)]
Proof state after:
case h₂
n : ℕ
hn : 0 < n
⊢ ↑(Nat.pred (2 * n / 3)) * 3 ≤ 2 * ↑n
Theorem: rpowDivThreeLe
Proof state before:
case h₂
n : ℕ
hn : 0 < n
⊢ ↑(Nat.pred (2 * n / 3)) * 3 ≤ 2 * ↑n
Tactic:
norm_cast
Proof state after:
case h₂
n : ℕ
hn : 0 < n
⊢ Nat.pred (2 * n / 3) * 3 ≤ 2 * n
Theorem: rpowDivThreeLe
Proof state before:
case h₂
n : ℕ
hn : 0 < n
⊢ Nat.pred (2 * n / 3) * 3 ≤ 2 * n
Tactic:
apply Nat.le_trans (Nat.mul_le_mul_right 3 (Nat.pred_le _))
Proof state after:
case h₂
n : ℕ
hn : 0 < n
⊢ 2 * n / 3 * 3 ≤ 2 * n
Theorem: rpowDivThreeLe
Proof state before:
case h₂
n : ℕ
hn : 0 < n
⊢ 2 * n / 3 * 3 ≤ 2 * n
Tactic:
apply Nat.div_mul_le_self
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ 1 < 4
Tactic:
norm_cast
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)
Tactic:
apply pow_nonneg (by norm_num)
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
apply Real.rpow_nonneg_of_nonneg (by norm_cast; linarith)
Proof state after:
no goals
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ 0 ≤ 2 * ↑n
Tactic:
norm_cast
Proof state after:
n : ℕ
hn : 0 < n
⊢ 0 ≤ 2 * n
Theorem: rpowDivThreeLe
Proof state before:
n : ℕ
hn : 0 < n
⊢ 0 ≤ 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: succLtTwoPow
Proof state before:
a : ℕ
h2 : 2 ≤ a
⊢ Nat.succ a < 2 ^ a
Tactic:
replace h2 := Nat.exists_eq_add_of_le h2
Proof state after:
a : ℕ
h2 : ∃ k, a = 2 + k
⊢ Nat.succ a < 2 ^ a
Theorem: succLtTwoPow
Proof state before:
a : ℕ
h2 : ∃ k, a = 2 + k
⊢ Nat.succ a < 2 ^ a
Tactic:
cases h2 with | intro u hu =>
rw [hu]
clear a hu
induction u with
| zero => simp
| succ u h =>
  rw [Nat.add_succ, Nat.pow_succ, Nat.mul_two]
  rw [← Nat.add_one]
  apply Nat.add_lt_add h
  apply Nat.one_lt_pow <;> linarith
Proof state after:
no goals