internlm/Lean-Github huggingface dataset:
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
⊢ s (Nat.find h3) < z
Tactic:
have h7 := h4 h6
Proof state after:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : Nat.find h3 - 1 ∉ S
⊢ s (Nat.find h3) < z
Tactic:
rw [Set.mem_setOf_eq] at h7
Proof state after:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : ¬z ≤ s (Nat.find h3 - 1 + 1)
⊢ s (Nat.find h3) < z
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : ¬z ≤ s (Nat.find h3 - 1 + 1)
⊢ s (Nat.find h3) < z
Tactic:
push_neg at h7
Proof state after:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : s (Nat.find h3 - 1 + 1) < z
⊢ s (Nat.find h3) < z
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_1.inr
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
h4 : Nat.find h3 - 1 < Nat.find h3 → Nat.find h3 - 1 ∉ S
h5 : Nat.find h3 > 0
h6 : Nat.find h3 - 1 < Nat.find h3
h7 : s (Nat.find h3 - 1 + 1) < z
⊢ s (Nat.find h3) < z
Tactic:
rwa [Nat.sub_add_cancel h5] at h7
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_2
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ z ≤ s (Nat.find h3 + 1)
Tactic:
exact Nat.find_spec h3
Proof state after:
no goals
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_3
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
⊢ ∀ (y : ℕ), s y < z ∧ z ≤ s (y + 1) → y = Nat.find h3
Tactic:
rintro m ⟨hm1, hm2⟩
Proof state after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ m = Nat.find h3
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ m = Nat.find h3
Tactic:
symm
Proof state after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ Nat.find h3 = m
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ Nat.find h3 = m
Tactic:
rw [Nat.find_eq_iff]
Proof state after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ z ≤ s (m + 1) ∧ ∀ n < m, ¬z ≤ s (n + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ z ≤ s (m + 1) ∧ ∀ n < m, ¬z ≤ s (n + 1)
Tactic:
refine ⟨hm2, ?_⟩
Proof state after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ ∀ n < m, ¬z ≤ s (n + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
⊢ ∀ n < m, ¬z ≤ s (n + 1)
Tactic:
intro k hk
Proof state after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
⊢ ¬z ≤ s (k + 1)
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
⊢ ¬z ≤ s (k + 1)
Tactic:
intro hkk
Proof state after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
hkk : z ≤ s (k + 1)
⊢ False
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
hkk : z ≤ s (k + 1)
⊢ False
Tactic:
have h9 : s (k + 1) ≤ s m := (StrictMono.le_iff_le hmono).mpr hk
Proof state after:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
hkk : z ≤ s (k + 1)
h9 : s (k + 1) ≤ s m
⊢ False
Theorem: Imo2014P1.lemma1
Proof state before:
case h.refine_3.intro
s : ℕ → ℤ
hs : ∀ (i : ℕ), s i < s (i + 1)
z : ℤ
hs0 : s 0 < z
hmono : StrictMono s
S : Set ℕ := {i | z ≤ s (i + 1)}
h3 : ∃ j, j ∈ S
m : ℕ
hm1 : s m < z
hm2 : z ≤ s (m + 1)
k : ℕ
hk : k < m
hkk : z ≤ s (k + 1)
h9 : s (k + 1) ≤ s m
⊢ False
Tactic:
omega
Proof state after:
no goals
Theorem: Hungary1998P6.sum_range_square_mul_six
Proof state before:
n : ℕ
⊢ (∑ i ∈ Finset.range n, (i + 1) ^ 2) * 6 = n * (n + 1) * (2 * n + 1)
Tactic:
induction n with
| zero => rfl
| succ n ih =>
  rw [Finset.sum_range_succ, add_mul, ih]
  ring
Proof state after:
no goals
Theorem: Hungary1998P6.sum_range_square_mul_six
Proof state before:
case zero

⊢ (∑ i ∈ Finset.range 0, (i + 1) ^ 2) * 6 = 0 * (0 + 1) * (2 * 0 + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Hungary1998P6.sum_range_square_mul_six
Proof state before:
case succ
n : ℕ
ih : (∑ i ∈ Finset.range n, (i + 1) ^ 2) * 6 = n * (n + 1) * (2 * n + 1)
⊢ (∑ i ∈ Finset.range (n + 1), (i + 1) ^ 2) * 6 = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1)
Tactic:
rw [Finset.sum_range_succ, add_mul, ih]
Proof state after:
case succ
n : ℕ
ih : (∑ i ∈ Finset.range n, (i + 1) ^ 2) * 6 = n * (n + 1) * (2 * n + 1)
⊢ n * (n + 1) * (2 * n + 1) + (n + 1) ^ 2 * 6 = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1)
Theorem: Hungary1998P6.sum_range_square_mul_six
Proof state before:
case succ
n : ℕ
ih : (∑ i ∈ Finset.range n, (i + 1) ^ 2) * 6 = n * (n + 1) * (2 * n + 1)
⊢ n * (n + 1) * (2 * n + 1) + (n + 1) ^ 2 * 6 = (n + 1) * (n + 1 + 1) * (2 * (n + 1) + 1)
Tactic:
ring
Proof state after:
no goals
Theorem: Hungary1998P6.sum_range_square
Proof state before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, (i + 1) ^ 2 = n * (n + 1) * (2 * n + 1) / 6
Tactic:
rw [← sum_range_square_mul_six n, Nat.mul_div_cancel]
Proof state after:
case H
n : ℕ
⊢ 0 < 6
Theorem: Hungary1998P6.sum_range_square
Proof state before:
case H
n : ℕ
⊢ 0 < 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: Hungary1998P6.cast_sum_square
Proof state before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, (↑i + 1) ^ 2 = ↑(∑ i ∈ Finset.range n, (i + 1) ^ 2)
Tactic:
norm_cast
Proof state after:
no goals
Theorem: Imo1968P2.lemma0
Proof state before:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ (List.mapIdx f l).getLast ⋯ = f l.dropLast.length (l.getLast h2)
Tactic:
simp_rw [List.mapIdx_eq_enum_map]
Proof state after:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ (List.map (Function.uncurry f) l.enum).getLast ⋯ = f l.dropLast.length (l.getLast h2)
Theorem: Imo1968P2.lemma0
Proof state before:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ (List.map (Function.uncurry f) l.enum).getLast ⋯ = f l.dropLast.length (l.getLast h2)
Tactic:
rw [List.getLast_eq_get, List.get_map, List.get_enum]
Proof state after:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ Function.uncurry f
      (↑⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩,
        l.get (Fin.cast ⋯ ⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩)) =
    f l.dropLast.length (l.getLast h2)
Theorem: Imo1968P2.lemma0
Proof state before:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ Function.uncurry f
      (↑⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩,
        l.get (Fin.cast ⋯ ⟨↑⟨(List.map (Function.uncurry f) l.enum).length - 1, ⋯⟩, ⋯⟩)) =
    f l.dropLast.length (l.getLast h2)
Tactic:
simp only [List.length_map, List.enum_length, Function.uncurry_apply_pair, List.length_dropLast]
Proof state after:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ f (l.length - 1) (l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩)) = f (l.length - 1) (l.getLast h2)
Theorem: Imo1968P2.lemma0
Proof state before:
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ f (l.length - 1) (l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩)) = f (l.length - 1) (l.getLast h2)
Tactic:
congr
Proof state after:
case e_a
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩) = l.getLast h2
Theorem: Imo1968P2.lemma0
Proof state before:
case e_a
α β : Type
f : ℕ → α → β
l : List α
h2 : l ≠ []
⊢ l.get (Fin.cast ⋯ ⟨l.length - 1, ⋯⟩) = l.getLast h2
Tactic:
exact List.get_length_sub_one _
Proof state after:
no goals
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
⊢ (b.digits x).prod ≤ x
Tactic:
have h1 : Nat.digits b x ≠ [] :=
  Nat.digits_ne_nil_iff_ne_zero.mpr (Nat.pos_iff_ne_zero.mp xpos)
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).prod ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).prod ≤ x
Tactic:
rw [←List.dropLast_append_getLast h1, List.prod_append, List.prod_singleton]
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h3 := Nat.ofDigits_digits b x
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : Nat.ofDigits b (b.digits x) = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : Nat.ofDigits b (b.digits x) = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
rw [Nat.ofDigits_eq_sum_mapIdx] at h3
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h4 : List.mapIdx (fun i a => a * b ^ i) (Nat.digits b x) ≠ [] :=
  List.mapIdx_eq_nil.not.mpr h1
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).sum = x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
rw [←List.dropLast_append_getLast (List.mapIdx_eq_nil.not.mpr h1),
    List.sum_append, List.sum_singleton] at h3
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h6 : List.getLast (List.mapIdx (fun i a => a * b ^ i) (Nat.digits b x)) h4 ≤ x :=
   by nth_rewrite 2 [←h3]; exact Nat.le_add_left _ _
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h7 : List.getLast (List.mapIdx (fun i a => a * b ^ i) (Nat.digits b x)) h4 =
     b ^ (List.dropLast (Nat.digits b x)).length * List.getLast (Nat.digits b x) h1 := by
  rw [lemma0 _ h1, mul_comm]
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
rw [h7] at h6
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h7 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
clear h7
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
have h8 : List.prod (List.dropLast (Nat.digits b x)) ≤
          b^(List.length (List.dropLast (Nat.digits b x))) := by
  have h10 : ∀ d ∈ List.dropLast (Nat.digits b x), d ≤ b := fun d hd ↦
    Nat.le_of_lt (Nat.digits_lt_base hb (List.mem_of_mem_dropLast hd))
  exact List.prod_le_pow_card (List.dropLast (Nat.digits b x)) b h10
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h8 : (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h8 : (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
⊢ (b.digits x).dropLast.prod * (b.digits x).getLast h1 ≤ x
Tactic:
calc _ ≤ _ := Nat.mul_le_mul_right _ h8
     _ ≤ _ := h6
Proof state after:
no goals
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
Tactic:
nth_rewrite 2 [←h3]
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤
    (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤
    (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯
Tactic:
exact Nat.le_add_left _ _
Proof state after:
no goals
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 ≤ x
⊢ (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast h4 =
    b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1
Tactic:
rw [lemma0 _ h1, mul_comm]
Proof state after:
no goals
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
⊢ (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
Tactic:
have h10 : ∀ d ∈ List.dropLast (Nat.digits b x), d ≤ b := fun d hd ↦
  Nat.le_of_lt (Nat.digits_lt_base hb (List.mem_of_mem_dropLast hd))
Proof state after:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h10 : ∀ d ∈ (b.digits x).dropLast, d ≤ b
⊢ (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
Theorem: Imo1968P2.prod_digits_le
Proof state before:
x b : ℕ
hb : 2 ≤ b
xpos : 0 < x
h1 : b.digits x ≠ []
h3 :
  (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).dropLast.sum +
      (List.mapIdx (fun i a => a * b ^ i) (b.digits x)).getLast ⋯ =
    x
h4 : List.mapIdx (fun i a => a * b ^ i) (b.digits x) ≠ []
h6 : b ^ (b.digits x).dropLast.length * (b.digits x).getLast h1 ≤ x
h10 : ∀ d ∈ (b.digits x).dropLast, d ≤ b
⊢ (b.digits x).dropLast.prod ≤ b ^ (b.digits x).dropLast.length
Tactic:
exact List.prod_le_pow_card (List.dropLast (Nat.digits b x)) b h10
Proof state after:
no goals
Theorem: Imo2013P1.prod_lemma
Proof state before:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
⊢ ∏ i ∈ Finset.range k, (1 + 1 / ↑↑(if i < k then m i else nm)) = ∏ i ∈ Finset.range k, (1 + 1 / ↑↑(m i))
Tactic:
suffices ∀ i, i ∈ Finset.range k → (1 : ℚ) + 1 / ↑(if i < k then m i else nm) = 1 + 1 / m i from
  Finset.prod_congr rfl this
Proof state after:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
⊢ ∀ i ∈ Finset.range k, 1 + 1 / ↑↑(if i < k then m i else nm) = 1 + 1 / ↑↑(m i)
Theorem: Imo2013P1.prod_lemma
Proof state before:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
⊢ ∀ i ∈ Finset.range k, 1 + 1 / ↑↑(if i < k then m i else nm) = 1 + 1 / ↑↑(m i)
Tactic:
intro i hi
Proof state after:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
i : ℕ
hi : i ∈ Finset.range k
⊢ 1 + 1 / ↑↑(if i < k then m i else nm) = 1 + 1 / ↑↑(m i)
Theorem: Imo2013P1.prod_lemma
Proof state before:
m : ℕ → ℕ+
k : ℕ
nm : ℕ+
i : ℕ
hi : i ∈ Finset.range k
⊢ 1 + 1 / ↑↑(if i < k then m i else nm) = 1 + 1 / ↑↑(m i)
Tactic:
simp [Finset.mem_range.mp hi]
Proof state after:
no goals