internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.succ.succ
c n : ℕ
h : 1 < 2 * (n + 1) + (c + 1)
h0 : (n + 1 + (n + 1 + (c + 1))).Prime
⊢ (n + 1).Coprime c.succ
Tactic:
rw [← Nat.coprime_self_add_right, ← Nat.coprime_self_add_right,
  Nat.coprime_comm, h0.coprime_iff_not_dvd]
Proof state after:
case refine_2.intro.succ.succ
c n : ℕ
h : 1 < 2 * (n + 1) + (c + 1)
h0 : (n + 1 + (n + 1 + (c + 1))).Prime
⊢ ¬n + 1 + (n + 1 + (c + 1)) ∣ n + 1
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.succ.succ
c n : ℕ
h : 1 < 2 * (n + 1) + (c + 1)
h0 : (n + 1 + (n + 1 + (c + 1))).Prime
⊢ ¬n + 1 + (n + 1 + (c + 1)) ∣ n + 1
Tactic:
exact Nat.not_dvd_of_pos_of_lt n.succ_pos <|
  lt_add_of_pos_right _ (n.succ + c).succ_pos
Proof state after:
no goals
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
k c : ℕ
h : good k c
⊢ good (k + 1) (2 * c + 1)
Tactic:
intro n h0
Proof state after:
k c : ℕ
h : good k c
n : ℕ
h0 : 0 < n
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(n + (2 * c + 1)) / ↑n = (map (fun m => ↑(m + 1) / ↑m) S).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
k c : ℕ
h : good k c
n : ℕ
h0 : 0 < n
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(n + (2 * c + 1)) / ↑n = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
rcases n.even_or_odd' with ⟨t, rfl | rfl⟩
Proof state after:
case intro.inl
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod

case intro.inr
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t + 1
⊢ ∃ S,
    card S = k + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inl
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
replace h0 := pos_of_mul_pos_right h0 (Nat.zero_le 2)
Proof state after:
case intro.inl
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < t
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inl
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < t
⊢ ∃ S, card S = k + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
rcases h t h0 with ⟨T, rfl, h1, h2⟩
Proof state after:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ∃ S,
    card S = card T + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ∃ S,
    card S = card T + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
have X := t.add_pos_left h0 c
Proof state after:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ∃ S,
    card S = card T + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ∃ S,
    card S = card T + 1 ∧ (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
refine ⟨(2 * (t + c)) ::ₘ T, card_cons _ T,
  forall_mem_cons.mpr ⟨mul_pos (Nat.succ_pos 1) X, h1⟩, ?_⟩
Proof state after:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) (2 * (t + c) ::ₘ T)).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ↑(2 * t + (2 * c + 1)) / ↑(2 * t) = (map (fun m => ↑(m + 1) / ↑m) (2 * (t + c) ::ₘ T)).prod
Tactic:
rw [map_cons, prod_cons, ← h2, ← add_assoc, ← mul_add,
  div_mul_div_comm, Nat.cast_mul, Nat.cast_mul, mul_right_comm]
Proof state after:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ↑(2 * (t + c) + 1) / (↑2 * ↑t) = ↑(2 * (t + c) + 1) * ↑(t + c) / (↑2 * ↑t * ↑(t + c))
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inl.intro.intro.intro
c t : ℕ
h0 : 0 < t
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + c) / ↑t = (map (fun m => ↑(m + 1) / ↑m) T).prod
X : 0 < t + c
⊢ ↑(2 * (t + c) + 1) / (↑2 * ↑t) = ↑(2 * (t + c) + 1) * ↑(t + c) / (↑2 * ↑t * ↑(t + c))
Tactic:
exact (mul_div_mul_right _ _ <| Nat.cast_ne_zero.mpr X.ne.symm).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inr
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t + 1
⊢ ∃ S,
    card S = k + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
have X := t.succ_pos
Proof state after:
case intro.inr
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
⊢ ∃ S,
    card S = k + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inr
k c : ℕ
h : good k c
t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
⊢ ∃ S,
    card S = k + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
rcases h (t + 1) X with ⟨T, rfl, h1, h2⟩
Proof state after:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ∃ S,
    card S = card T + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ∃ S,
    card S = card T + 1 ∧
      (∀ m ∈ S, 0 < m) ∧ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) S).prod
Tactic:
refine ⟨(2 * t + 1) ::ₘ T, card_cons _ T,
  forall_mem_cons.mpr ⟨(2 * t).succ_pos, h1⟩, ?_⟩
Proof state after:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) ((2 * t + 1) ::ₘ T)).prod
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ↑(2 * t + 1 + (2 * c + 1)) / ↑(2 * t + 1) = (map (fun m => ↑(m + 1) / ↑m) ((2 * t + 1) ::ₘ T)).prod
Tactic:
rw [map_cons, prod_cons, ← h2, add_add_add_comm, add_right_comm,
  add_assoc (2 * t) 1, ← mul_add_one (α := ℕ), ← mul_add, div_mul_div_comm,
  Nat.cast_mul, Nat.cast_mul, mul_right_comm]
Proof state after:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ↑2 * ↑(t + 1 + c) / ↑(2 * t + 1) = ↑2 * ↑(t + 1 + c) * ↑(t + 1) / (↑(2 * t + 1) * ↑(t + 1))
Theorem: IMOSL.IMO2013N2.good_two_mul_add_one
Proof state before:
case intro.inr.intro.intro.intro
c t : ℕ
h0 : 0 < 2 * t + 1
X : 0 < t.succ
T : Multiset ℕ
h : good (card T) c
h1 : ∀ m ∈ T, 0 < m
h2 : ↑(t + 1 + c) / ↑(t + 1) = (map (fun m => ↑(m + 1) / ↑m) T).prod
⊢ ↑2 * ↑(t + 1 + c) / ↑(2 * t + 1) = ↑2 * ↑(t + 1 + c) * ↑(t + 1) / (↑(2 * t + 1) * ↑(t + 1))
Tactic:
exact (mul_div_mul_right _ _ <| Nat.cast_ne_zero.mpr X.ne.symm).symm
Proof state after:
no goals
Theorem: IMOSL.IMO2013N2.final_solution
Proof state before:
n : ℕ
h : 0 < n
⊢ ↑(n + (2 ^ 0 - 1)) / ↑n = (map (fun m => ↑(m + 1) / ↑m) 0).prod
Tactic:
rw [pow_zero, Nat.sub_self, add_zero]
Proof state after:
n : ℕ
h : 0 < n
⊢ ↑n / ↑n = (map (fun m => ↑(m + 1) / ↑m) 0).prod
Theorem: IMOSL.IMO2013N2.final_solution
Proof state before:
n : ℕ
h : 0 < n
⊢ ↑n / ↑n = (map (fun m => ↑(m + 1) / ↑m) 0).prod
Tactic:
exact div_self (Nat.cast_ne_zero.mpr h.ne.symm)
Proof state after:
no goals
Theorem: IMOSL.IMO2013N2.final_solution
Proof state before:
k : ℕ
⊢ good (k + 1) (2 ^ (k + 1) - 1)
Tactic:
have h := good_two_mul_add_one (final_solution k)
Proof state after:
k : ℕ
h : good (k + 1) (2 * (2 ^ k - 1) + 1)
⊢ good (k + 1) (2 ^ (k + 1) - 1)
Theorem: IMOSL.IMO2013N2.final_solution
Proof state before:
k : ℕ
h : good (k + 1) (2 * (2 ^ k - 1) + 1)
⊢ good (k + 1) (2 ^ (k + 1) - 1)
Tactic:
have h0 := k.one_le_pow 2 (Nat.succ_pos 1)
Proof state after:
k : ℕ
h : good (k + 1) (2 * (2 ^ k - 1) + 1)
h0 : 1 ≤ 2 ^ k
⊢ good (k + 1) (2 ^ (k + 1) - 1)
Theorem: IMOSL.IMO2013N2.final_solution
Proof state before:
k : ℕ
h : good (k + 1) (2 * (2 ^ k - 1) + 1)
h0 : 1 ≤ 2 ^ k
⊢ good (k + 1) (2 ^ (k + 1) - 1)
Tactic:
rwa [two_mul, add_assoc, Nat.sub_add_cancel h0, add_comm _ (2 ^ k),
  ← Nat.add_sub_assoc h0, ← two_mul, ← pow_succ'] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2022A1.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
N : ℕ
h1 : 2 ≤ N
⊢ a N ≤ 1
Tactic:
have h2 (i : ℕ) (h1 : 1 < a (i + 1)) (h2 : 1 < a (i + 2)) : False :=
  (main_ineq h1.le h2 (h _) (h0 _)).asymm <| main_ineq2 (h i) h1 h2.le (h0 _)
Proof state after:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
N : ℕ
h1 : 2 ≤ N
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
⊢ a N ≤ 1
Theorem: IMOSL.IMO2022A1.final_solution
Proof state before:
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
N : ℕ
h1 : 2 ≤ N
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
⊢ a N ≤ 1
Tactic:
rcases Nat.exists_eq_add_of_le' h1 with ⟨n, rfl⟩
Proof state after:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1 : 2 ≤ n + 2
⊢ a (n + 2) ≤ 1
Theorem: IMOSL.IMO2022A1.final_solution
Proof state before:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1 : 2 ≤ n + 2
⊢ a (n + 2) ≤ 1
Tactic:
refine le_of_not_lt λ h1 ↦ (h0 (n + 1)).not_lt ?_
Proof state after:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1✝ : 2 ≤ n + 2
h1 : 1 < a (n + 2)
⊢ a (n + 1) + a (n + 1 + 2) < a (n + 1 + 1) ^ 2 + a (n + 1) * a (n + 1 + 2)
Theorem: IMOSL.IMO2022A1.final_solution
Proof state before:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1✝ : 2 ≤ n + 2
h1 : 1 < a (n + 2)
⊢ a (n + 1) + a (n + 1 + 2) < a (n + 1 + 1) ^ 2 + a (n + 1) * a (n + 1 + 2)
Tactic:
rw [← sub_lt_iff_lt_add, add_sub_assoc, ← one_sub_mul]
Proof state after:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1✝ : 2 ≤ n + 2
h1 : 1 < a (n + 2)
⊢ a (n + 1) + (1 - a (n + 1)) * a (n + 1 + 2) < a (n + 1 + 1) ^ 2
Theorem: IMOSL.IMO2022A1.final_solution
Proof state before:
case intro
R : Type u_1
inst✝ : LinearOrderedRing R
a : ℕ → R
h : ∀ (i : ℕ), 0 ≤ a i
h0 : ∀ (i : ℕ), a (i + 1) ^ 2 + a i * a (i + 2) ≤ a i + a (i + 2)
h2 : ∀ (i : ℕ), 1 < a (i + 1) → 1 < a (i + 2) → False
n : ℕ
h1✝ : 2 ≤ n + 2
h1 : 1 < a (n + 2)
⊢ a (n + 1) + (1 - a (n + 1)) * a (n + 1 + 2) < a (n + 1 + 1) ^ 2
Tactic:
exact (one_lt_pow h1 <| Nat.succ_ne_zero 1).trans_le' <|
  add_le_of_le_sub_left <| mul_le_of_le_one_right
    (sub_nonneg_of_le <| le_of_not_lt <| λ h3 ↦ h2 _ h3 h1)
    (le_of_not_lt <| h2 _ h1)
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.and_and_or_not_iff
Proof state before:
P Q R : Prop
⊢ (P ∧ Q) ∧ (R ∨ ¬Q) ↔ (P ∧ R) ∧ Q
Tactic:
rw [and_assoc, and_or_left, and_not_self_iff,
  or_false_iff, and_assoc, and_comm (b := Q)]
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.Iic_filter_dvd_card
Proof state before:
k n : ℕ
⊢ (filter (fun i => n + 1 ∣ i + 1) (Icc k (k + n))).card = 1
Tactic:
let h := (k + (n + 1)).card_multiples (n + 1)
Proof state after:
k n : ℕ
h : (filter (fun e => n + 1 ∣ e + 1) (range (k + (n + 1)))).card = (k + (n + 1)) / (n + 1) :=
  Nat.card_multiples (k + (n + 1)) (n + 1)
⊢ (filter (fun i => n + 1 ∣ i + 1) (Icc k (k + n))).card = 1
Theorem: IMOSL.IMO2009C1.Iic_filter_dvd_card
Proof state before:
k n : ℕ
h : (filter (fun e => n + 1 ∣ e + 1) (range (k + (n + 1)))).card = (k + (n + 1)) / (n + 1) :=
  Nat.card_multiples (k + (n + 1)) (n + 1)
⊢ (filter (fun i => n + 1 ∣ i + 1) (Icc k (k + n))).card = 1
Tactic:
rwa [range_eq_Ico, ← Ico_union_Ico_eq_Ico k.zero_le le_self_add, filter_union,
  card_union_of_disjoint (disjoint_filter_filter <| Ico_disjoint_Ico_consecutive 0 k _),
  ← range_eq_Ico, Nat.card_multiples, k.add_div_right n.succ_pos,
  Nat.succ_eq_add_one, add_right_inj] at h
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.symmDiff_card_add_two_mul_inter_card
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
A B : Finset α
⊢ (symmDiff A B).card + 2 * (A ∩ B).card = A.card + B.card
Tactic:
rw [two_mul, ← add_assoc, ← card_union_of_disjoint (disjoint_symmDiff_inter A B),
  symmDiff_union_inter_eq_union, card_union_add_card_inter]
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.symmDiff_card_mod_two
Proof state before:
α : Type u_1
inst✝ : DecidableEq α
A B : Finset α
⊢ (symmDiff A B).card % 2 = (A.card + B.card) % 2
Tactic:
rw [← symmDiff_card_add_two_mul_inter_card, Nat.add_mul_mod_self_left]
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.filter_symmDiff
Proof state before:
α : Type u_1
inst✝¹ : DecidableEq α
A B : Finset α
p : α → Prop
inst✝ : DecidablePred p
x : α
⊢ x ∈ filter p (symmDiff A B) ↔ x ∈ symmDiff (filter p A) (filter p B)
Tactic:
rw [mem_filter, mem_symmDiff, mem_symmDiff,
mem_filter, mem_filter, not_and_or, not_and_or,
and_and_or_not_iff, and_and_or_not_iff, ← or_and_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.GameState.Ends_iff
Proof state before:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
⊢ i ∈ range n
Tactic:
rw [mem_range, ← not_le]
Proof state after:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
⊢ ¬n ≤ i
Theorem: IMOSL.IMO2009C1.GameState.Ends_iff
Proof state before:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
⊢ ¬n ≤ i
Tactic:
refine λ h1 ↦ h _ <| ValidMove.flip (i - n) ?_
Proof state after:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
h1 : n ≤ i
⊢ i - n + n ∈ X.board
Theorem: IMOSL.IMO2009C1.GameState.Ends_iff
Proof state before:
n : ℕ
X : GameState n
h : X.Ends
i : ℕ
h0 : i ∈ X.board
h1 : n ≤ i
⊢ i - n + n ∈ X.board
Tactic:
rwa [Nat.sub_add_cancel h1]
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
n : ℕ
X Y : GameState n
h : X.ValidMove Y
⊢ { ofColex := Y.board } < { ofColex := X.board }
Tactic:
rcases h with ⟨i, h⟩
Proof state after:
case flip
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ { ofColex := { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board } <
    { ofColex := X.board }
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
case flip
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ { ofColex := { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board } <
    { ofColex := X.board }
Tactic:
refine Colex.toColex_lt_toColex.mpr ⟨?_, λ j h0 h1 ↦ ?_⟩
Proof state after:
case flip.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board ≠ X.board

case flip.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
⊢ ∃ b ∈ X.board, b ∉ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board ∧ j ≤ b
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
case flip.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board ≠ X.board
Tactic:
rw [Ne, symmDiff_eq_left]
Proof state after:
case flip.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ ¬Icc i (i + n) = ⊥
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
case flip.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
⊢ ¬Icc i (i + n) = ⊥
Tactic:
exact ne_empty_of_mem (left_mem_Icc.mpr le_self_add)
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
case flip.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
⊢ ∃ b ∈ X.board, b ∉ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board ∧ j ≤ b
Tactic:
refine ⟨i + n, h, λ h2 ↦ ?_, ?_⟩
Proof state after:
case flip.refine_2.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
h2 : i + n ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
⊢ False

case flip.refine_2.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
⊢ j ≤ i + n
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
case flip.refine_2.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
h2 : i + n ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
⊢ False
Tactic:
rw [mem_symmDiff, mem_Icc] at h2
Proof state after:
case flip.refine_2.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
h2 : i + n ∈ X.board ∧ ¬(i ≤ i + n ∧ i + n ≤ i + n) ∨ (i ≤ i + n ∧ i + n ≤ i + n) ∧ i + n ∉ X.board
⊢ False
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
case flip.refine_2.refine_1
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
h2 : i + n ∈ X.board ∧ ¬(i ≤ i + n ∧ i + n ≤ i + n) ∨ (i ≤ i + n ∧ i + n ≤ i + n) ∧ i + n ∉ X.board
⊢ False
Tactic:
exact h2.elim (λ h2 ↦ h2.2 ⟨le_self_add, (i + n).le_refl⟩) (λ h2 ↦ h2.2 h)
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
case flip.refine_2.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : j ∈ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.board
h1 : j ∉ X.board
⊢ j ≤ i + n
Tactic:
rw [mem_symmDiff, or_iff_right (λ h2 ↦ h1 h2.1), mem_Icc] at h0
Proof state after:
case flip.refine_2.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : (i ≤ j ∧ j ≤ i + n) ∧ j ∉ X.board
h1 : j ∉ X.board
⊢ j ≤ i + n
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_Colex
Proof state before:
case flip.refine_2.refine_2
n : ℕ
X : GameState n
i : ℕ
h : i + n ∈ X.board
j : ℕ
h0 : (i ≤ j ∧ j ≤ i + n) ∧ j ∉ X.board
h1 : j ∉ X.board
⊢ j ≤ i + n
Tactic:
exact h0.1.2
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.GameState.isReachable_sum_two_pow_add_numMoves
Proof state before:
n : ℕ
X Y : GameState n
h : X.IsReachable Y
a✝ c✝ : GameState n
h0 : a✝.ValidMove c✝
x✝ : ReflTransGen ValidMove c✝ Y
h1 : ∑ i ∈ Y.board, 2 ^ i + Y.numMoves ≤ ∑ i ∈ c✝.board, 2 ^ i + c✝.numMoves
⊢ ∑ i ∈ c✝.board, 2 ^ i + c✝.numMoves ≤ ∑ i ∈ a✝.board, 2 ^ i + a✝.numMoves
Tactic:
rw [ValidMove_numMoves h0, ← add_assoc, Nat.succ_le_iff]
Proof state after:
n : ℕ
X Y : GameState n
h : X.IsReachable Y
a✝ c✝ : GameState n
h0 : a✝.ValidMove c✝
x✝ : ReflTransGen ValidMove c✝ Y
h1 : ∑ i ∈ Y.board, 2 ^ i + Y.numMoves ≤ ∑ i ∈ c✝.board, 2 ^ i + c✝.numMoves
⊢ ∑ i ∈ c✝.board, 2 ^ i + a✝.numMoves < ∑ i ∈ a✝.board, 2 ^ i + a✝.numMoves
Theorem: IMOSL.IMO2009C1.GameState.isReachable_sum_two_pow_add_numMoves
Proof state before:
n : ℕ
X Y : GameState n
h : X.IsReachable Y
a✝ c✝ : GameState n
h0 : a✝.ValidMove c✝
x✝ : ReflTransGen ValidMove c✝ Y
h1 : ∑ i ∈ Y.board, 2 ^ i + Y.numMoves ≤ ∑ i ∈ c✝.board, 2 ^ i + c✝.numMoves
⊢ ∑ i ∈ c✝.board, 2 ^ i + a✝.numMoves < ∑ i ∈ a✝.board, 2 ^ i + a✝.numMoves
Tactic:
exact Nat.add_lt_add_right (ValidMove_sum_two_pow h0) _
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.GameState.ValidMove_central_card_mod_two
Proof state before:
n : ℕ
X Y : GameState n
h : X.ValidMove Y
i : ℕ
x✝ : i + n ∈ X.board
⊢ { board := symmDiff X.board (Icc i (i + n)), numMoves := X.numMoves.succ }.centralCards.card % 2 =
    (X.centralCards.card + 1) % 2
Tactic:
rw [centralCards, filter_symmDiff, ← centralCards,
  symmDiff_card_mod_two, Iic_filter_dvd_card]
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.GameState.isReachable_central_card_add_numMoves_mod_two
Proof state before:
n : ℕ
X Y : GameState n
h : X.IsReachable Y
a✝ c✝ : GameState n
h0 : a✝.ValidMove c✝
x✝ : ReflTransGen ValidMove c✝ Y
h1 : (Y.centralCards.card + Y.numMoves) % 2 = (c✝.centralCards.card + c✝.numMoves) % 2
⊢ (c✝.centralCards.card + c✝.numMoves) % 2 = (a✝.centralCards.card + a✝.numMoves) % 2
Tactic:
rw [ValidMove_numMoves h0, Nat.add_mod, ValidMove_central_card_mod_two h0,
  ← Nat.add_mod, add_add_add_comm, Nat.add_mod_right]
Proof state after:
no goals
Theorem: IMOSL.IMO2009C1.GameState.numMoves_mod_two_eq_div_of_ends
Proof state before:
M n : ℕ
X : GameState n
h : (init M n).IsReachable X
h0 : X.Ends
⊢ X.numMoves % 2 = M / n.succ % 2
Tactic:
have h1 := isReachable_central_card_add_numMoves_mod_two h
Proof state after:
M n : ℕ
X : GameState n
h : (init M n).IsReachable X
h0 : X.Ends
h1 : (X.centralCards.card + X.numMoves) % 2 = ((init M n).centralCards.card + (init M n).numMoves) % 2
⊢ X.numMoves % 2 = M / n.succ % 2
Theorem: IMOSL.IMO2009C1.GameState.numMoves_mod_two_eq_div_of_ends
Proof state before:
M n : ℕ
X : GameState n
h : (init M n).IsReachable X
h0 : X.Ends
h1 : (X.centralCards.card + X.numMoves) % 2 = ((init M n).centralCards.card + (init M n).numMoves) % 2
⊢ X.numMoves % 2 = M / n.succ % 2
Tactic:
rwa [filter_central_init_card, numMoves_init, Nat.add_zero,
  filter_central_ends h0, card_empty, Nat.zero_add] at h1
Proof state after:
no goals