internlm/Lean-Github huggingface dataset:
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inl
n : ℕ
hn : 100 ≤ n
b c : ℕ
hbc : b < c
hcn : c ≤ 2 * n
h₃ : ∃ m, b + c = m ^ 2
y : ℕ
hxy : y ≠ y
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, c + y = l ^ 2
⊢ ∃ k, y + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inr.inl
n : ℕ
hn : 100 ≤ n
c : ℕ
hcn : c ≤ 2 * n
x y : ℕ
hxy : x ≠ y
hna : n ≤ x
h₂ : ∃ l, c + x = l ^ 2
hbc : y < c
h₃ : ∃ m, y + c = m ^ 2
hab : x < y
h₁ : ∃ k, x + y = k ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inl.inr.inr
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hna : n ≤ x
hab : x < b
h₁ : ∃ k, x + b = k ^ 2
hbc : b < y
hcn : y ≤ 2 * n
h₃ : ∃ m, b + y = m ^ 2
h₂ : ∃ l, y + x = l ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inl
n : ℕ
hn : 100 ≤ n
c : ℕ
hcn : c ≤ 2 * n
x y : ℕ
hxy : x ≠ y
hbc : x < c
h₃ : ∃ m, x + c = m ^ 2
hna : n ≤ y
h₂ : ∃ l, c + y = l ^ 2
hab : y < x
h₁ : ∃ k, y + x = k ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inr.inl
n : ℕ
hn : 100 ≤ n
a c : ℕ
hna : n ≤ a
hcn : c ≤ 2 * n
h₂ : ∃ l, c + a = l ^ 2
y : ℕ
hxy : y ≠ y
hab : a < y
hbc : y < c
h₁ : ∃ k, a + y = k ^ 2
h₃ : ∃ m, y + c = m ^ 2
⊢ ∃ k, y + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inl.inr.inr
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hab : a < x
h₁ : ∃ k, a + x = k ^ 2
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
hbc : x < y
h₃ : ∃ m, x + y = m ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inl
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hbc : b < x
hcn : x ≤ 2 * n
h₃ : ∃ m, b + x = m ^ 2
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, x + y = l ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inl
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hcn : x ≤ 2 * n
h₂ : ∃ l, x + a = l ^ 2
hab : a < y
h₁ : ∃ k, a + y = k ^ 2
hbc : y < x
h₃ : ∃ m, y + x = m ^ 2
⊢ ∃ k, x + y = k ^ 2

case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inr
n : ℕ
hn : 100 ≤ n
a b : ℕ
hna : n ≤ a
hab : a < b
h₁ : ∃ k, a + b = k ^ 2
y : ℕ
hxy : y ≠ y
hbc : b < y
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
h₃ : ∃ m, b + y = m ^ 2
⊢ ∃ k, y + y = k ^ 2
Tactic:
all_goals
  first
  | contradiction
  | assumption
  | simpa only [add_comm x y]
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inr
n : ℕ
hn : 100 ≤ n
a b : ℕ
hna : n ≤ a
hab : a < b
h₁ : ∃ k, a + b = k ^ 2
y : ℕ
hxy : y ≠ y
hbc : b < y
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
h₃ : ∃ m, b + y = m ^ 2
⊢ ∃ k, y + y = k ^ 2
Tactic:
first
| contradiction
| assumption
| simpa only [add_comm x y]
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inr
n : ℕ
hn : 100 ≤ n
a b : ℕ
hna : n ≤ a
hab : a < b
h₁ : ∃ k, a + b = k ^ 2
y : ℕ
hxy : y ≠ y
hbc : b < y
hcn : y ≤ 2 * n
h₂ : ∃ l, y + a = l ^ 2
h₃ : ∃ m, b + y = m ^ 2
⊢ ∃ k, y + y = k ^ 2
Tactic:
contradiction
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inl
n : ℕ
hn : 100 ≤ n
b x y : ℕ
hxy : x ≠ y
hbc : b < x
hcn : x ≤ 2 * n
h₃ : ∃ m, b + x = m ^ 2
hna : n ≤ y
hab : y < b
h₁ : ∃ k, y + b = k ^ 2
h₂ : ∃ l, x + y = l ^ 2
⊢ ∃ k, x + y = k ^ 2
Tactic:
assumption
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.inr.inr.inr.inl
n : ℕ
hn : 100 ≤ n
a : ℕ
hna : n ≤ a
x y : ℕ
hxy : x ≠ y
hcn : x ≤ 2 * n
h₂ : ∃ l, x + a = l ^ 2
hab : a < y
h₁ : ∃ k, a + y = k ^ 2
hbc : y < x
h₃ : ∃ m, y + x = m ^ 2
⊢ ∃ k, x + y = k ^ 2
Tactic:
simpa only [add_comm x y]
Proof state after:
no goals
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
n : ℕ
hn : 100 ≤ n
a b c : ℕ
hna : n ≤ a
hab : a < b
hbc : b < c
hcn : c ≤ 2 * n
h₁ : ∃ k, a + b = k ^ 2
h₂ : ∃ l, c + a = l ^ 2
h₃ : ∃ m, b + c = m ^ 2
⊢ ∀ c_1 ∈ {a, b, c}, n ≤ c_1 ∧ c_1 ≤ 2 * n
Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton]
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
n : ℕ
hn : 100 ≤ n
a b c : ℕ
hna : n ≤ a
hab : a < b
hbc : b < c
hcn : c ≤ 2 * n
h₁ : ∃ k, a + b = k ^ 2
h₂ : ∃ l, c + a = l ^ 2
h₃ : ∃ m, b + c = m ^ 2
⊢ ∀ (c_1 : ℕ), c_1 = a ∨ c_1 = b ∨ c_1 = c → n ≤ c_1 ∧ c_1 ≤ 2 * n
Theorem: Imo2021P1.exists_finset_3_le_card_with_pairs_summing_to_squares
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_3
n : ℕ
hn : 100 ≤ n
a b c : ℕ
hna : n ≤ a
hab : a < b
hbc : b < c
hcn : c ≤ 2 * n
h₁ : ∃ k, a + b = k ^ 2
h₂ : ∃ l, c + a = l ^ 2
h₃ : ∃ m, b + c = m ^ 2
⊢ ∀ (c_1 : ℕ), c_1 = a ∨ c_1 = b ∨ c_1 = c → n ≤ c_1 ∧ c_1 ≤ 2 * n
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1960P1.ge_100
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ 100 ≤ n
Tactic:
have h2 : 10 ^ 3 ≤ 10 * n := by
  rw [← h1.left]
  refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
  simp
Proof state after:
n : ℕ
h1 : ProblemPredicate n
h2 : 10 ^ 3 ≤ 10 * n
⊢ 100 ≤ n
Theorem: Imo1960P1.ge_100
Proof state before:
n : ℕ
h1 : ProblemPredicate n
h2 : 10 ^ 3 ≤ 10 * n
⊢ 100 ≤ n
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1960P1.ge_100
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ 10 ^ 3 ≤ 10 * n
Tactic:
rw [← h1.left]
Proof state after:
n : ℕ
h1 : ProblemPredicate n
⊢ 10 ^ (digits 10 n).length ≤ 10 * n
Theorem: Imo1960P1.ge_100
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ 10 ^ (digits 10 n).length ≤ 10 * n
Tactic:
refine Nat.base_pow_length_digits_le 10 n ?_ (not_zero h1)
Proof state after:
n : ℕ
h1 : ProblemPredicate n
⊢ 1 < 10
Theorem: Imo1960P1.ge_100
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ 1 < 10
Tactic:
simp
Proof state after:
no goals
Theorem: Imo1960P1.lt_1000
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ n < 1000
Tactic:
have h2 : n < 10 ^ 3 := by
  rw [← h1.left]
  exact lt_base_pow_length_digits'
Proof state after:
n : ℕ
h1 : ProblemPredicate n
h2 : n < 10 ^ 3
⊢ n < 1000
Theorem: Imo1960P1.lt_1000
Proof state before:
n : ℕ
h1 : ProblemPredicate n
h2 : n < 10 ^ 3
⊢ n < 1000
Tactic:
linarith
Proof state after:
no goals
Theorem: Imo1960P1.lt_1000
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ n < 10 ^ 3
Tactic:
rw [← h1.left]
Proof state after:
n : ℕ
h1 : ProblemPredicate n
⊢ n < 10 ^ (digits 10 n).length
Theorem: Imo1960P1.lt_1000
Proof state before:
n : ℕ
h1 : ProblemPredicate n
⊢ n < 10 ^ (digits 10 n).length
Tactic:
exact lt_base_pow_length_digits'
Proof state after:
no goals
Theorem: Imo1960P1.searchUpTo_start
Proof state before:
n : ℕ
h : n < 99
p : ProblemPredicate n
⊢ SolutionPredicate n
Tactic:
linarith [ge_100 p]
Proof state after:
no goals
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
c n : ℕ
H : SearchUpTo c n
c' n' : ℕ
ec : c + 1 = c'
en : n + 11 = n'
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo c' n'
Tactic:
subst ec
Proof state after:
c n : ℕ
H : SearchUpTo c n
n' : ℕ
en : n + 11 = n'
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) n'
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
c n : ℕ
H : SearchUpTo c n
n' : ℕ
en : n + 11 = n'
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) n'
Tactic:
subst en
Proof state after:
c n : ℕ
H : SearchUpTo c n
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
c n : ℕ
H : SearchUpTo c n
l : List ℕ
el : digits 10 n = l
H' : c = sumOfSquares l → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)
Tactic:
subst el
Proof state after:
c n : ℕ
H : SearchUpTo c n
H' : c = sumOfSquares (digits 10 n) → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
c n : ℕ
H : SearchUpTo c n
H' : c = sumOfSquares (digits 10 n) → c = 50 ∨ c = 73
⊢ SearchUpTo (c + 1) (n + 11)
Tactic:
obtain ⟨rfl, H⟩ := H
Proof state after:
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
⊢ SearchUpTo (c + 1) (c * 11 + 11)
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
⊢ SearchUpTo (c + 1) (c * 11 + 11)
Tactic:
refine ⟨by ring, fun m l p => ?_⟩
Proof state after:
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : m < c * 11 + 11
p : ProblemPredicate m
⊢ SolutionPredicate m
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
case intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : m < c * 11 + 11
p : ProblemPredicate m
⊢ SolutionPredicate m
Tactic:
obtain ⟨h₁, ⟨m, rfl⟩, h₂⟩ := id p
Proof state after:
case intro.intro.intro.intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
⊢ SolutionPredicate (11 * m)
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
case intro.intro.intro.intro
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
⊢ SolutionPredicate (11 * m)
Tactic:
by_cases h : 11 * m < c * 11
Proof state after:
case pos
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : 11 * m < c * 11
⊢ SolutionPredicate (11 * m)

case neg
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : ¬11 * m < c * 11
⊢ SolutionPredicate (11 * m)
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
case neg
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : ¬11 * m < c * 11
⊢ SolutionPredicate (11 * m)
Tactic:
obtain rfl : m = c := by omega
Proof state after:
case neg
m : ℕ
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
H' : m = sumOfSquares (digits 10 (m * 11)) → m = 50 ∨ m = 73
H : ∀ m_1 < m * 11, ProblemPredicate m_1 → SolutionPredicate m_1
l : 11 * m < m * 11 + 11
h : ¬11 * m < m * 11
⊢ SolutionPredicate (11 * m)
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
case neg
m : ℕ
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
H' : m = sumOfSquares (digits 10 (m * 11)) → m = 50 ∨ m = 73
H : ∀ m_1 < m * 11, ProblemPredicate m_1 → SolutionPredicate m_1
l : 11 * m < m * 11 + 11
h : ¬11 * m < m * 11
⊢ SolutionPredicate (11 * m)
Tactic:
rw [Nat.mul_div_cancel_left _ (by norm_num : 11 > 0), mul_comm] at h₂
Proof state after:
case neg
m : ℕ
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : m = sumOfSquares (digits 10 (m * 11))
H' : m = sumOfSquares (digits 10 (m * 11)) → m = 50 ∨ m = 73
H : ∀ m_1 < m * 11, ProblemPredicate m_1 → SolutionPredicate m_1
l : 11 * m < m * 11 + 11
h : ¬11 * m < m * 11
⊢ SolutionPredicate (11 * m)
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
⊢ c * 11 + 11 = (c + 1) * 11
Tactic:
ring
Proof state after:
no goals
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
case pos
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : 11 * m < c * 11
⊢ SolutionPredicate (11 * m)
Tactic:
exact H _ h p
Proof state after:
no goals
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
c : ℕ
H' : c = sumOfSquares (digits 10 (c * 11)) → c = 50 ∨ c = 73
H : ∀ m < c * 11, ProblemPredicate m → SolutionPredicate m
m : ℕ
l : 11 * m < c * 11 + 11
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
h : ¬11 * m < c * 11
⊢ m = c
Tactic:
omega
Proof state after:
no goals
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
m : ℕ
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : 11 * m / 11 = sumOfSquares (digits 10 (11 * m))
H' : m = sumOfSquares (digits 10 (m * 11)) → m = 50 ∨ m = 73
H : ∀ m_1 < m * 11, ProblemPredicate m_1 → SolutionPredicate m_1
l : 11 * m < m * 11 + 11
h : ¬11 * m < m * 11
⊢ 11 > 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
case neg.refine_2
m : ℕ
p : ProblemPredicate (11 * m)
h₁ : (digits 10 (11 * m)).length = 3
h₂ : m = sumOfSquares (digits 10 (m * 11))
H' : m = sumOfSquares (digits 10 (m * 11)) → m = 50 ∨ m = 73
H : ∀ m_1 < m * 11, ProblemPredicate m_1 → SolutionPredicate m_1
l : 11 * m < m * 11 + 11
h : ¬11 * m < m * 11
⊢ m = 73 → 11 * m = 803
Tactic:
rintro rfl
Proof state after:
case neg.refine_2
p : ProblemPredicate (11 * 73)
h₁ : (digits 10 (11 * 73)).length = 3
h₂ : 73 = sumOfSquares (digits 10 (73 * 11))
H' : 73 = sumOfSquares (digits 10 (73 * 11)) → 73 = 50 ∨ 73 = 73
H : ∀ m < 73 * 11, ProblemPredicate m → SolutionPredicate m
l : 11 * 73 < 73 * 11 + 11
h : ¬11 * 73 < 73 * 11
⊢ 11 * 73 = 803
Theorem: Imo1960P1.searchUpTo_step
Proof state before:
case neg.refine_2
p : ProblemPredicate (11 * 73)
h₁ : (digits 10 (11 * 73)).length = 3
h₂ : 73 = sumOfSquares (digits 10 (73 * 11))
H' : 73 = sumOfSquares (digits 10 (73 * 11)) → 73 = 50 ∨ 73 = 73
H : ∀ m < 73 * 11, ProblemPredicate m → SolutionPredicate m
l : 11 * 73 < 73 * 11 + 11
h : ¬11 * 73 < 73 * 11
⊢ 11 * 73 = 803
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo1960P1.searchUpTo_end
Proof state before:
c : ℕ
H : SearchUpTo c 1001
n : ℕ
ppn : ProblemPredicate n
⊢ n < 1001
Tactic:
linarith [lt_1000 ppn]
Proof state after:
no goals
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
⊢ ProblemPredicate n → SolutionPredicate n
Tactic:
have := searchUpTo_start
Proof state after:
n : ℕ
this : SearchUpTo 9 99
⊢ ProblemPredicate n → SolutionPredicate n
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
this : SearchUpTo 9 99
⊢ ProblemPredicate n → SolutionPredicate n
Tactic:
iterate 82
  replace :=
    searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) rfl
      (by norm_num <;> decide)
Proof state after:
n : ℕ
this : SearchUpTo 91 1001
⊢ ProblemPredicate n → SolutionPredicate n
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
this : SearchUpTo 91 1001
⊢ ProblemPredicate n → SolutionPredicate n
Tactic:
exact searchUpTo_end this
Proof state after:
no goals
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
this : SearchUpTo 90 990
⊢ ProblemPredicate n → SolutionPredicate n
Tactic:
replace :=
  searchUpTo_step this (by norm_num1; rfl) (by norm_num1; rfl) rfl
    (by norm_num <;> decide)
Proof state after:
n : ℕ
this : SearchUpTo 91 1001
⊢ ProblemPredicate n → SolutionPredicate n
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
this : SearchUpTo 90 990
⊢ 90 + 1 = ?m.34900
Tactic:
norm_num1
Proof state after:
n : ℕ
this : SearchUpTo 90 990
⊢ 91 = ?m.34900
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
this : SearchUpTo 90 990
⊢ 91 = ?m.34900
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
this : SearchUpTo 90 990
⊢ 990 + 11 = ?m.34901
Tactic:
norm_num1
Proof state after:
n : ℕ
this : SearchUpTo 90 990
⊢ 1001 = ?m.34901
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
this : SearchUpTo 90 990
⊢ 1001 = ?m.34901
Tactic:
rfl
Proof state after:
no goals
Theorem: Imo1960P1.right_direction
Proof state before:
n : ℕ
this : SearchUpTo 90 990
⊢ 90 = sumOfSquares (digits 10 990) → 90 = 50 ∨ 90 = 73
Tactic:
norm_num <;> decide
Proof state after:
no goals
Theorem: Imo1960P1.left_direction
Proof state before:
n : ℕ
spn : SolutionPredicate n
⊢ ProblemPredicate n
Tactic:
rcases spn with (rfl | rfl) <;> exact ⟨by norm_num, by decide, by norm_num; rfl⟩
Proof state after:
no goals
Theorem: Imo1960P1.left_direction
Proof state before:
⊢ (digits 10 803).length = 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo1960P1.left_direction
Proof state before:
⊢ 11 ∣ 803
Tactic:
decide
Proof state after:
no goals
Theorem: Imo1960P1.left_direction
Proof state before:
⊢ 803 / 11 = sumOfSquares (digits 10 803)
Tactic:
norm_num
Proof state after:
⊢ 73 = sumOfSquares [3, 0, 8]
Theorem: Imo1960P1.left_direction
Proof state before:
⊢ 73 = sumOfSquares [3, 0, 8]
Tactic:
rfl
Proof state after:
no goals
Theorem: Bulgaria1998P3.geom_sum_bound
Proof state before:
n : ℕ
⊢ ∑ i ∈ Finset.range n, 1 / 2 ^ i = ∑ i ∈ Finset.range n, (1 / 2) ^ i
Tactic:
congr
Proof state after:
case e_f
n : ℕ
⊢ (fun i => 1 / 2 ^ i) = fun i => (1 / 2) ^ i
Theorem: Bulgaria1998P3.geom_sum_bound
Proof state before:
case e_f
n : ℕ
⊢ (fun i => 1 / 2 ^ i) = fun i => (1 / 2) ^ i
Tactic:
simp [div_eq_mul_inv]
Proof state after:
no goals
Theorem: Bulgaria1998P3.geom_sum_bound
Proof state before:
n : ℕ
⊢ 2 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 / (a ^ 4 + b ^ 4 + c ^ 4) ≤ a ^ 3 / √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
Tactic:
rw [div_le_div_iff (by positivity) (by positivity)]
Proof state after:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)
Tactic:
calc a ^ 4 * sqrt ((a ^ 3) ^ 2 + (8:ℝ) * b ^ 3 * c ^ 3)
    = a ^ 3 * (a * sqrt ((a ^ 3) ^ 2 + (8:ℝ) * b ^ 3 * c ^ 3)) := by ring
  _ ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4) := ?_
Proof state after:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 3 * (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 3 * (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ≤ a ^ 3 * (a ^ 4 + b ^ 4 + c ^ 4)
Tactic:
gcongr
Proof state after:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 4 + b ^ 4 + c ^ 4
Theorem: Imo2001P2.bound
Proof state before:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) ≤ a ^ 4 + b ^ 4 + c ^ 4
Tactic:
apply le_of_pow_le_pow_left two_ne_zero (by positivity)
Proof state after:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ^ 2 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2
Theorem: Imo2001P2.bound
Proof state before:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)) ^ 2 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2
Tactic:
rw [mul_pow, sq_sqrt (by positivity), ← sub_nonneg]
Proof state after:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
Theorem: Imo2001P2.bound
Proof state before:
case h
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 ≤ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
Tactic:
calc
  (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
    = 2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 +
      (2 * (a ^ 2 * b * c - b ^ 2 * c ^ 2)) ^ 2 := by ring
  _ ≥ 0 := by positivity
Proof state after:
no goals
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 < a ^ 4 + b ^ 4 + c ^ 4
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 < √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3)
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) = a ^ 3 * (a * √((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3))
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 ≤ a ^ 4 + b ^ 4 + c ^ 4
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 0 ≤ (a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ (a ^ 4 + b ^ 4 + c ^ 4) ^ 2 - a ^ 2 * ((a ^ 3) ^ 2 + 8 * b ^ 3 * c ^ 3) =
    2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 + (2 * (a ^ 2 * b * c - b ^ 2 * c ^ 2)) ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Imo2001P2.bound
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ 2 * (a ^ 2 * (b ^ 2 - c ^ 2)) ^ 2 + (b ^ 4 - c ^ 4) ^ 2 + (2 * (a ^ 2 * b * c - b ^ 2 * c ^ 2)) ^ 2 ≥ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2001P2.imo2001_p2'
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a ^ 4 + b ^ 4 + c ^ 4 ≠ 0
Tactic:
positivity
Proof state after:
no goals
Theorem: Imo2001P2.imo2001_p2'
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
H : a ^ 4 + b ^ 4 + c ^ 4 ≠ 0
⊢ a ^ 4 / (a ^ 4 + b ^ 4 + c ^ 4) + b ^ 4 / (b ^ 4 + c ^ 4 + a ^ 4) + c ^ 4 / (c ^ 4 + a ^ 4 + b ^ 4) = 1
Tactic:
ring_nf at H ⊢
Proof state after:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
H : a ^ 4 + b ^ 4 + c ^ 4 ≠ 0
⊢ a ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ + b ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ + c ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ = 1
Theorem: Imo2001P2.imo2001_p2'
Proof state before:
a b c : ℝ
ha : 0 < a
hb : 0 < b
hc : 0 < c
H : a ^ 4 + b ^ 4 + c ^ 4 ≠ 0
⊢ a ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ + b ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ + c ^ 4 * (a ^ 4 + b ^ 4 + c ^ 4)⁻¹ = 1
Tactic:
field_simp
Proof state after:
no goals
Theorem: Usa1992P1.digits_append_zeroes_append_digits
Proof state before:
b k m n : ℕ
hm : 0 < m
hb : 1 < b
⊢ b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)
Tactic:
revert m
Proof state after:
b k n : ℕ
hb : 1 < b
⊢ ∀ {m : ℕ}, 0 < m → b.digits n ++ List.replicate k 0 ++ b.digits m = b.digits (n + b ^ (k + (b.digits n).length) * m)