internlm/Lean-Github huggingface dataset:
Theorem: Imo2022P2.lemma0
Proof state before:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ Classical.choose ⋯ = x
Tactic:
have hxw : x = w := by
  apply h1u'
  rw [h2]
  exact h1e
Proof state after:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
hxw : x = w
⊢ Classical.choose ⋯ = x
Theorem: Imo2022P2.lemma0
Proof state before:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
hxw : x = w
⊢ Classical.choose ⋯ = x
Tactic:
rw [hxw]
Proof state after:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
hxw : x = w
⊢ Classical.choose ⋯ = w
Theorem: Imo2022P2.lemma0
Proof state before:
case intro.intro.intro.intro
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
hxw : x = w
⊢ Classical.choose ⋯ = w
Tactic:
exact h1u' _ h4
Proof state after:
no goals
Theorem: Imo2022P2.lemma0
Proof state before:
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ x = w
Tactic:
apply h1u'
Proof state after:
case a
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ p y x
Theorem: Imo2022P2.lemma0
Proof state before:
case a
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ p y x
Tactic:
rw [h2]
Proof state after:
case a
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ p x y
Theorem: Imo2022P2.lemma0
Proof state before:
case a
α : Type
p : α → α → Prop
h1 : ∀ (x : α), ∃! y, p x y
h2 : ∀ (x y : α), p x y ↔ p y x
x y : α
h1e : p x y
h1u : ∀ (y_1 : α), (fun y => p x y) y_1 → y_1 = y
h2' : Classical.choose ⋯ = y
w : α
h1e' : p y w
h1u' : ∀ (y_1 : α), (fun y_2 => p y y_2) y_1 → y_1 = w
h4 : p y (Classical.choose ⋯)
⊢ p x y
Tactic:
exact h1e
Proof state after:
no goals
Theorem: Imo2022P2.amgm
Proof state before:
a b : ℝ+
⊢ ⟨2, ⋯⟩ ≤ a / b + b / a
Tactic:
change 2 ≤ a.val/b.val + b.val/a.val
Proof state after:
a b : ℝ+
⊢ 2 ≤ ↑a / ↑b + ↑b / ↑a
Theorem: Imo2022P2.amgm
Proof state before:
a b : ℝ+
⊢ 2 ≤ ↑a / ↑b + ↑b / ↑a
Tactic:
obtain ⟨a, ha⟩ := a
Proof state after:
case mk
b : ℝ+
a : ℝ
ha : 0 < a
⊢ 2 ≤ ↑⟨a, ha⟩ / ↑b + ↑b / ↑⟨a, ha⟩
Theorem: Imo2022P2.amgm
Proof state before:
case mk
b : ℝ+
a : ℝ
ha : 0 < a
⊢ 2 ≤ ↑⟨a, ha⟩ / ↑b + ↑b / ↑⟨a, ha⟩
Tactic:
obtain ⟨b, hb⟩ := b
Proof state after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ ↑⟨a, ha⟩ / ↑⟨b, hb⟩ + ↑⟨b, hb⟩ / ↑⟨a, ha⟩
Theorem: Imo2022P2.amgm
Proof state before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ ↑⟨a, ha⟩ / ↑⟨b, hb⟩ + ↑⟨b, hb⟩ / ↑⟨a, ha⟩
Tactic:
dsimp only
Proof state after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ a / b + b / a
Theorem: Imo2022P2.amgm
Proof state before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ a / b + b / a
Tactic:
field_simp
Proof state after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ (a * a + b * b) / (b * a)
Theorem: Imo2022P2.amgm
Proof state before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ (a * a + b * b) / (b * a)
Tactic:
have h1 : 0 < b * a := Real.mul_pos hb ha
Proof state after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 ≤ (a * a + b * b) / (b * a)
Theorem: Imo2022P2.amgm
Proof state before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 ≤ (a * a + b * b) / (b * a)
Tactic:
suffices H : 2 * (b * a) ≤ a * a + b * b by exact (le_div_iff h1).mpr H
Proof state after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 * (b * a) ≤ a * a + b * b
Theorem: Imo2022P2.amgm
Proof state before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 * (b * a) ≤ a * a + b * b
Tactic:
suffices H : 0 ≤ (a - b)^2 by linarith
Proof state after:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 0 ≤ (a - b) ^ 2
Theorem: Imo2022P2.amgm
Proof state before:
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 0 ≤ (a - b) ^ 2
Tactic:
exact sq_nonneg (a - b)
Proof state after:
no goals
Theorem: Imo2022P2.amgm
Proof state before:
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
H : 2 * (b * a) ≤ a * a + b * b
⊢ 2 ≤ (a * a + b * b) / (b * a)
Tactic:
exact (le_div_iff h1).mpr H
Proof state after:
no goals
Theorem: Imo2022P2.amgm
Proof state before:
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
H : 0 ≤ (a - b) ^ 2
⊢ 2 * (b * a) ≤ a * a + b * b
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo2022P2.lemma1
Proof state before:
a : ℝ+
⊢ a + a = ⟨2, ⋯⟩ * a
Tactic:
obtain ⟨a, ha⟩ := a
Proof state after:
case mk
a : ℝ
ha : 0 < a
⊢ ⟨a, ha⟩ + ⟨a, ha⟩ = ⟨2, ⋯⟩ * ⟨a, ha⟩
Theorem: Imo2022P2.lemma1
Proof state before:
case mk
a : ℝ
ha : 0 < a
⊢ ⟨a, ha⟩ + ⟨a, ha⟩ = ⟨2, ⋯⟩ * ⟨a, ha⟩
Tactic:
apply Subtype.val_injective
Proof state after:
case mk.a
a : ℝ
ha : 0 < a
⊢ ↑(⟨a, ha⟩ + ⟨a, ha⟩) = ↑(⟨2, ⋯⟩ * ⟨a, ha⟩)
Theorem: Imo2022P2.lemma1
Proof state before:
case mk.a
a : ℝ
ha : 0 < a
⊢ ↑(⟨a, ha⟩ + ⟨a, ha⟩) = ↑(⟨2, ⋯⟩ * ⟨a, ha⟩)
Tactic:
dsimp
Proof state after:
case mk.a
a : ℝ
ha : 0 < a
⊢ a + a = 2 * a
Theorem: Imo2022P2.lemma1
Proof state before:
case mk.a
a : ℝ
ha : 0 < a
⊢ a + a = 2 * a
Tactic:
exact (two_mul a).symm
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ n < 6
Tactic:
have h2 : ∑ i ∈ Finset.range n, i < k := by
  suffices multiplicity 2 (k ! : ℤ) = ↑(∑ i ∈ Finset.range n, i : ℕ) by
    rw [← PartENat.coe_lt_coe, ← this]; change multiplicity ((2 : ℕ) : ℤ) _ < _
    simp_rw [multiplicity.Int.natCast_multiplicity,
             Nat.multiplicity_two_factorial_lt hk.lt.ne.symm]
  rw [h, multiplicity.Finset.prod Int.prime_two, Nat.cast_sum]
  apply Finset.sum_congr rfl; intro i hi
  rw [multiplicity.multiplicity_sub_of_gt,
      multiplicity.multiplicity_pow_self_of_prime Int.prime_two]
  rwa [multiplicity.multiplicity_pow_self_of_prime Int.prime_two,
       multiplicity.multiplicity_pow_self_of_prime Int.prime_two,
    PartENat.coe_lt_coe, ← Finset.mem_range]
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ n < 6
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ n < 6
Tactic:
rw [← not_le]
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ ¬6 ≤ n
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
⊢ ¬6 ≤ n
Tactic:
intro hn
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ False
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ False
Tactic:
apply _root_.ne_of_gt _ h
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i) < ↑k !
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i) < ↑k !
Tactic:
calc ∏ i ∈ Finset.range n, ((2:ℤ) ^ n - (2:ℤ) ^ i) ≤ ∏ __ ∈ Finset.range n, (2:ℤ) ^ n := ?_
  _ < ↑ k ! := ?_
Proof state after:
case calc_1
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i) ≤ ∏ __ ∈ Finset.range n, 2 ^ n

case calc_2
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ __ ∈ Finset.range n, 2 ^ n < ↑k !
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_2
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ __ ∈ Finset.range n, 2 ^ n < ↑k !
Tactic:
norm_cast
Proof state after:
case calc_2
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ i ∈ Finset.range n, 2 ^ n < k !
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_2
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ i ∈ Finset.range n, 2 ^ n < k !
Tactic:
calc ∏ __ ∈ Finset.range n, 2 ^ n = 2 ^ (n * n) := by
       rw [Finset.prod_const, Finset.card_range, ← pow_mul]
  _ < (∑ i ∈ Finset.range n, i)! := ?_
  _ ≤ k ! := by gcongr
Proof state after:
case calc_2
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ 2 ^ (n * n) < (∑ i ∈ Finset.range n, i)!
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_2
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ 2 ^ (n * n) < (∑ i ∈ Finset.range n, i)!
Tactic:
clear h h2
Proof state after:
case calc_2
k n : ℕ
hk : k > 0
hn : 6 ≤ n
⊢ 2 ^ (n * n) < (∑ i ∈ Finset.range n, i)!
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_2
k n : ℕ
hk : k > 0
hn : 6 ≤ n
⊢ 2 ^ (n * n) < (∑ i ∈ Finset.range n, i)!
Tactic:
induction' n, hn using Nat.le_induction with n' hn' IH
Proof state after:
case calc_2.base
k n : ℕ
hk : k > 0
⊢ 2 ^ (6 * 6) < (∑ i ∈ Finset.range 6, i)!

case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
Tactic:
let A := ∑ i ∈ Finset.range n', i
Proof state after:
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
Tactic:
have le_sum : ∑ i ∈ Finset.range 6, i ≤ A := by
  apply Finset.sum_le_sum_of_subset
  simpa using hn'
Proof state after:
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_2.succ
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 2 ^ ((n' + 1) * (n' + 1)) < (∑ i ∈ Finset.range (n' + 1), i)!
Tactic:
calc 2 ^ ((n' + 1) * (n' + 1))
    ≤ 2 ^ (n' * n' + 4 * n') := by gcongr <;> linarith
  _ = 2 ^ (n' * n') * (2 ^ 4) ^ n' := by rw [← pow_mul, ← pow_add]
  _ < A ! * (2 ^ 4) ^ n' := by gcongr
  _ = A ! * (15 + 1) ^ n' := rfl
  _ ≤ A ! * (A + 1) ^ n' := by gcongr; exact le_sum
  _ ≤ (A + n')! := Nat.factorial_mul_pow_le_factorial
  _ = (∑ i ∈ Finset.range (n' + 1), i)! := by rw [Finset.sum_range_succ]
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∑ i ∈ Finset.range n, i < k
Tactic:
suffices multiplicity 2 (k ! : ℤ) = ↑(∑ i ∈ Finset.range n, i : ℕ) by
  rw [← PartENat.coe_lt_coe, ← this]; change multiplicity ((2 : ℕ) : ℤ) _ < _
  simp_rw [multiplicity.Int.natCast_multiplicity,
           Nat.multiplicity_two_factorial_lt hk.lt.ne.symm]
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
Tactic:
rw [h, multiplicity.Finset.prod Int.prime_two, Nat.cast_sum]
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∑ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ∑ x ∈ Finset.range n, ↑x
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∑ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ∑ x ∈ Finset.range n, ↑x
Tactic:
apply Finset.sum_congr rfl
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∀ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ↑x
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
⊢ ∀ x ∈ Finset.range n, multiplicity 2 (2 ^ n - 2 ^ x) = ↑x
Tactic:
intro i hi
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ n - 2 ^ i) = ↑i
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ n - 2 ^ i) = ↑i
Tactic:
rw [multiplicity.multiplicity_sub_of_gt,
    multiplicity.multiplicity_pow_self_of_prime Int.prime_two]
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ i) < multiplicity 2 (2 ^ n)
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
i : ℕ
hi : i ∈ Finset.range n
⊢ multiplicity 2 (2 ^ i) < multiplicity 2 (2 ^ n)
Tactic:
rwa [multiplicity.multiplicity_pow_self_of_prime Int.prime_two,
     multiplicity.multiplicity_pow_self_of_prime Int.prime_two,
  PartENat.coe_lt_coe, ← Finset.mem_range]
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ ∑ i ∈ Finset.range n, i < k
Tactic:
rw [← PartENat.coe_lt_coe, ← this]
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity 2 ↑k ! < ↑k
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity 2 ↑k ! < ↑k
Tactic:
change multiplicity ((2 : ℕ) : ℤ) _ < _
Proof state after:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity ↑2 ↑k ! < ↑k
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
this : multiplicity 2 ↑k ! = ↑(∑ i ∈ Finset.range n, i)
⊢ multiplicity ↑2 ↑k ! < ↑k
Tactic:
simp_rw [multiplicity.Int.natCast_multiplicity,
         Nat.multiplicity_two_factorial_lt hk.lt.ne.symm]
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_1
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i) ≤ ∏ __ ∈ Finset.range n, 2 ^ n
Tactic:
gcongr
Proof state after:
case calc_1.h0
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∀ i ∈ Finset.range n, 0 ≤ 2 ^ n - 2 ^ i

case calc_1.h1
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 2 ^ n - 2 ^ i✝ ≤ 2 ^ n
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_1.h0
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∀ i ∈ Finset.range n, 0 ≤ 2 ^ n - 2 ^ i
Tactic:
intro i hi
Proof state after:
case calc_1.h0
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i ∈ Finset.range n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_1.h0
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i ∈ Finset.range n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Tactic:
simp only [Finset.mem_range] at hi
Proof state after:
case calc_1.h0
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i < n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_1.h0
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i < n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Tactic:
have : (2:ℤ) ^ i ≤ (2:ℤ) ^ n := by gcongr; norm_num
Proof state after:
case calc_1.h0
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i < n
this : 2 ^ i ≤ 2 ^ n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_1.h0
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i < n
this : 2 ^ i ≤ 2 ^ n
⊢ 0 ≤ 2 ^ n - 2 ^ i
Tactic:
omega
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i < n
⊢ 2 ^ i ≤ 2 ^ n
Tactic:
gcongr
Proof state after:
case ha
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i < n
⊢ 1 ≤ 2
Theorem: Imo2019P4.upper_bound
Proof state before:
case ha
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i : ℕ
hi : i < n
⊢ 1 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_1.h1
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 2 ^ n - 2 ^ i✝ ≤ 2 ^ n
Tactic:
apply sub_le_self
Proof state after:
case calc_1.h1.a
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 0 ≤ 2 ^ i✝
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_1.h1.a
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
i✝ : ℕ
a✝ : i✝ ∈ Finset.range n
⊢ 0 ≤ 2 ^ i✝
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ ∏ __ ∈ Finset.range n, 2 ^ n = 2 ^ (n * n)
Tactic:
rw [Finset.prod_const, Finset.card_range, ← pow_mul]
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
h : ↑k ! = ∏ i ∈ Finset.range n, (2 ^ n - 2 ^ i)
h2 : ∑ i ∈ Finset.range n, i < k
hn : 6 ≤ n
⊢ (∑ i ∈ Finset.range n, i)! ≤ k !
Tactic:
gcongr
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
case calc_2.base
k n : ℕ
hk : k > 0
⊢ 2 ^ (6 * 6) < (∑ i ∈ Finset.range 6, i)!
Tactic:
decide
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
⊢ ∑ i ∈ Finset.range 6, i ≤ A
Tactic:
apply Finset.sum_le_sum_of_subset
Proof state after:
case h
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
⊢ Finset.range 6 ⊆ Finset.range n'
Theorem: Imo2019P4.upper_bound
Proof state before:
case h
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
⊢ Finset.range 6 ⊆ Finset.range n'
Tactic:
simpa using hn'
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 2 ^ ((n' + 1) * (n' + 1)) ≤ 2 ^ (n' * n' + 4 * n')
Tactic:
gcongr <;> linarith
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 2 ^ (n' * n' + 4 * n') = 2 ^ (n' * n') * (2 ^ 4) ^ n'
Tactic:
rw [← pow_mul, ← pow_add]
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 2 ^ (n' * n') * (2 ^ 4) ^ n' < A ! * (2 ^ 4) ^ n'
Tactic:
gcongr
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ A ! * (15 + 1) ^ n' ≤ A ! * (A + 1) ^ n'
Tactic:
gcongr
Proof state after:
case bc.hab.bc
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 15 ≤ A
Theorem: Imo2019P4.upper_bound
Proof state before:
case bc.hab.bc
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ 15 ≤ A
Tactic:
exact le_sum
Proof state after:
no goals
Theorem: Imo2019P4.upper_bound
Proof state before:
k n : ℕ
hk : k > 0
n' : ℕ
hn' : 6 ≤ n'
IH : 2 ^ (n' * n') < (∑ i ∈ Finset.range n', i)!
A : ℕ := ∑ i ∈ Finset.range n', i
le_sum : ∑ i ∈ Finset.range 6, i ≤ A
⊢ (A + n')! = (∑ i ∈ Finset.range (n' + 1), i)!
Tactic:
rw [Finset.sum_range_succ]
Proof state after:
no goals