internlm/Lean-Github huggingface dataset:
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
c : R
hc : 0 < c ∧ c < 1
h0 : f (-c) = 0
y : R
h : f (⌊-c⌋ • -y) = f (-c) * ↑⌊f (-y)⌋
⊢ -1 ≤ -c ∧ -c < 0
Tactic:
exact ⟨neg_le_neg hc.2.le, neg_lt_zero.mpr hc.1⟩
Proof state after:
no goals
Theorem: IMOSL.IMO2010A1.good_iff_of_DenselyOrdered
Proof state before:
R : Type u_2
inst✝⁴ : LinearOrderedRing R
inst✝³ : FloorRing R
S : Type u_1
inst✝² : DenselyOrdered R
inst✝¹ : LinearOrderedRing S
inst✝ : FloorRing S
f : R → S
h✝ : (∃ C, ⌊C⌋ = 1 ∧ f = fun x => C) ∨ f = 0
x✝² : ∃ C, ⌊C⌋ = 1 ∧ f = fun x => C
x✝¹ x✝ : R
C : S
h : ⌊C⌋ = 1
h0 : f = fun x => C
⊢ f (⌊x✝¹⌋ • x✝) = f x✝¹ * ↑⌊f x✝⌋
Tactic:
rw [h0, h, Int.cast_one, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2008A3.final_solution_part_2_general
Proof state before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p < q
⊢ (p.1.succ, p.2) < (q.1.succ, q.2)
Tactic:
rwa [prod_lex_lt_iff, Nat.succ_lt_succ_iff, Nat.succ_inj', ← prod_lex_lt_iff]
Proof state after:
no goals
Theorem: IMOSL.IMO2008A3.final_solution_part_2_general
Proof state before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p < q
⊢ (p.1, φ^[3 ^ p.1] p.2) < (q.1, φ^[3 ^ q.1] q.2)
Tactic:
rw [prod_lex_lt_iff] at h2 ⊢
Proof state after:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p.1 < q.1 ∨ p.1 = q.1 ∧ p.2 < q.2
⊢ (p.1, φ^[3 ^ p.1] p.2).1 < (q.1, φ^[3 ^ q.1] q.2).1 ∨
    (p.1, φ^[3 ^ p.1] p.2).1 = (q.1, φ^[3 ^ q.1] q.2).1 ∧ (p.1, φ^[3 ^ p.1] p.2).2 < (q.1, φ^[3 ^ q.1] q.2).2
Theorem: IMOSL.IMO2008A3.final_solution_part_2_general
Proof state before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p.1 < q.1 ∨ p.1 = q.1 ∧ p.2 < q.2
⊢ (p.1, φ^[3 ^ p.1] p.2).1 < (q.1, φ^[3 ^ q.1] q.2).1 ∨
    (p.1, φ^[3 ^ p.1] p.2).1 = (q.1, φ^[3 ^ q.1] q.2).1 ∧ (p.1, φ^[3 ^ p.1] p.2).2 < (q.1, φ^[3 ^ q.1] q.2).2
Tactic:
refine h2.imp_right λ h3 ↦ ⟨h3.1, (h.iterate _ h3.2).trans_eq ?_⟩
Proof state after:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p.1 < q.1 ∨ p.1 = q.1 ∧ p.2 < q.2
h3 : p.1 = q.1 ∧ p.2 < q.2
⊢ φ^[3 ^ p.1] q.2 = (q.1, φ^[3 ^ q.1] q.2).2
Theorem: IMOSL.IMO2008A3.final_solution_part_2_general
Proof state before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p q : Lex (ℕ × β)
h2 : p.1 < q.1 ∨ p.1 = q.1 ∧ p.2 < q.2
h3 : p.1 = q.1 ∧ p.2 < q.2
⊢ φ^[3 ^ p.1] q.2 = (q.1, φ^[3 ^ q.1] q.2).2
Tactic:
rw [← h3.1]
Proof state after:
no goals
Theorem: IMOSL.IMO2008A3.final_solution_part_2_general
Proof state before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).1.succ,
      ((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).2) <
    ((p.1.succ, p.2).1, φ^[3 ^ (p.1.succ, p.2).1] (p.1.succ, p.2).2)
Tactic:
refine prod_lex_lt_iff.mpr <| Or.inr <| ⟨rfl, ?_⟩
Proof state after:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).1.succ,
        ((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).2).2 <
    ((p.1.succ, p.2).1, φ^[3 ^ (p.1.succ, p.2).1] (p.1.succ, p.2).2).2
Theorem: IMOSL.IMO2008A3.final_solution_part_2_general
Proof state before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).1.succ,
        ((p.1, φ^[3 ^ p.1] p.2).1, φ^[3 ^ (p.1, φ^[3 ^ p.1] p.2).1] (p.1, φ^[3 ^ p.1] p.2).2).2).2 <
    ((p.1.succ, p.2).1, φ^[3 ^ (p.1.succ, p.2).1] (p.1.succ, p.2).2).2
Tactic:
rw [← Function.iterate_add_apply, ← two_mul, pow_succ']
Proof state after:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[2 * 3 ^ (p.1, φ^[3 ^ p.1] p.2).1] p.2).1.succ,
        ((p.1, φ^[3 ^ p.1] p.2).1, φ^[2 * 3 ^ (p.1, φ^[3 ^ p.1] p.2).1] p.2).2).2 <
    ((p.1.succ, p.2).1, φ^[3 * 3 ^ p.1] (p.1.succ, p.2).2).2
Theorem: IMOSL.IMO2008A3.final_solution_part_2_general
Proof state before:
β : Type u_1
φ : β → β
inst✝ : Preorder β
h : StrictMono φ
h0 : ∀ (x : β), x < φ x
p : Lex (ℕ × β)
⊢ (((p.1, φ^[3 ^ p.1] p.2).1, φ^[2 * 3 ^ (p.1, φ^[3 ^ p.1] p.2).1] p.2).1.succ,
        ((p.1, φ^[3 ^ p.1] p.2).1, φ^[2 * 3 ^ (p.1, φ^[3 ^ p.1] p.2).1] p.2).2).2 <
    ((p.1.succ, p.2).1, φ^[3 * 3 ^ p.1] (p.1.succ, p.2).2).2
Tactic:
exact h.strictMono_iterate_of_lt_map (h0 p.2)
  (Nat.mul_lt_mul_of_pos_right (Nat.lt_succ_self 2)
    (pow_pos (Nat.succ_pos 2) _))
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₄.add_mul
Proof state before:
x y z : 𝔽₄
⊢ (x + y) * z = x * z + y * z
Tactic:
rw [𝔽₄.mul_comm, 𝔽₄.mul_add, z.mul_comm, z.mul_comm]
Proof state after:
no goals
Theorem: IMOSL.Extra.EventuallyEqual.symm
Proof state before:
α✝ : Sort u_1
a b : Nat → α✝
h : EventuallyEqual a b
⊢ EventuallyEqual b a
Tactic:
rcases h with ⟨N_a, N_b, h⟩
Proof state after:
case intro.intro
α✝ : Sort u_1
a b : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
⊢ EventuallyEqual b a
Theorem: IMOSL.Extra.EventuallyEqual.symm
Proof state before:
case intro.intro
α✝ : Sort u_1
a b : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
⊢ EventuallyEqual b a
Tactic:
exact ⟨N_b, N_a, λ k ↦ (h k).symm⟩
Proof state after:
no goals
Theorem: IMOSL.Extra.EventuallyEqual.trans
Proof state before:
α✝ : Sort u_1
a b c : Nat → α✝
h : EventuallyEqual a b
h0 : EventuallyEqual b c
⊢ EventuallyEqual a c
Tactic:
rcases h with ⟨N_a, N_b, h⟩
Proof state after:
case intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
h0 : EventuallyEqual b c
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
⊢ EventuallyEqual a c
Theorem: IMOSL.Extra.EventuallyEqual.trans
Proof state before:
case intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
h0 : EventuallyEqual b c
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
⊢ EventuallyEqual a c
Tactic:
rcases h0 with ⟨K_b, K_c, h0⟩
Proof state after:
case intro.intro.intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
K_b K_c : Nat
h0 : ∀ (k : Nat), b (k + K_b) = c (k + K_c)
⊢ EventuallyEqual a c
Theorem: IMOSL.Extra.EventuallyEqual.trans
Proof state before:
case intro.intro.intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
K_b K_c : Nat
h0 : ∀ (k : Nat), b (k + K_b) = c (k + K_c)
⊢ EventuallyEqual a c
Tactic:
refine ⟨K_b + N_a, K_c + N_b, λ k ↦ ?_⟩
Proof state after:
case intro.intro.intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
K_b K_c : Nat
h0 : ∀ (k : Nat), b (k + K_b) = c (k + K_c)
k : Nat
⊢ a (k + (K_b + N_a)) = c (k + (K_c + N_b))
Theorem: IMOSL.Extra.EventuallyEqual.trans
Proof state before:
case intro.intro.intro.intro
α✝ : Sort u_1
a b c : Nat → α✝
N_a N_b : Nat
h : ∀ (k : Nat), a (k + N_a) = b (k + N_b)
K_b K_c : Nat
h0 : ∀ (k : Nat), b (k + K_b) = c (k + K_c)
k : Nat
⊢ a (k + (K_b + N_a)) = c (k + (K_c + N_b))
Tactic:
rw [← Nat.add_assoc, h, Nat.add_right_comm, h0, Nat.add_right_comm, Nat.add_assoc]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₃.add_mul
Proof state before:
x y z : 𝔽₃
⊢ (x + y) * z = x * z + y * z
Tactic:
rw [𝔽₃.mul_comm, 𝔽₃.mul_add, z.mul_comm, z.mul_comm]
Proof state after:
no goals
Theorem: IMOSL.IMO2012A5.𝔽₃.cast_add
Proof state before:
R : Type u_1
inst✝ : AddGroupWithOne R
h : 3 = 0
x y : 𝔽₃
⊢ 1 + 1 = -1
Tactic:
rwa [one_add_one_eq_two, eq_neg_iff_add_eq_zero, two_add_one_eq_three]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.Semiring_of_two_eq_zero
Proof state before:
R : Type u_1
inst✝ : NonAssocSemiring R
h : 2 = 0
x : R
⊢ x + x = 0
Tactic:
rw [← two_mul, h, zero_mul]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.two_eq_zero
Proof state before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
⊢ 2 = 0
Tactic:
rw [← one_add_one_eq_two, add_self_eq_zero]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_mul_self_of_Commute
Proof state before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
x y : R
h : x * y = y * x
⊢ (x + y) * (x + y) = x * x + y * y
Tactic:
rw [add_mul, mul_add, mul_add, ← add_assoc, h, add_add_cancel_right]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_one_mul_self
Proof state before:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharTwo R
x : R
⊢ (x + 1) * (x + 1) = x * x + 1
Tactic:
rw [add_mul_self_of_Commute ((mul_one x).trans (one_mul x).symm), one_mul]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.mul_self_eq_one_iff
Proof state before:
R : Type u_1
inst✝² : NonAssocSemiring R
inst✝¹ : CharTwo R
inst✝ : NoZeroDivisors R
x : R
⊢ x * x = 1 ↔ x = 1
Tactic:
rw [← add_eq_zero_iff_eq, ← add_one_mul_self, mul_self_eq_zero, add_eq_zero_iff_eq]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_sq_of_Commute
Proof state before:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharTwo R
x y : R
h : x * y = y * x
⊢ (x + y) ^ 2 = x ^ 2 + y ^ 2
Tactic:
rw [sq, sq, sq, add_mul_self_of_Commute h]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.add_one_sq
Proof state before:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharTwo R
x : R
⊢ (x + 1) ^ 2 = x ^ 2 + 1
Tactic:
rw [sq, sq, add_one_mul_self]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.sq_eq_one_iff
Proof state before:
R : Type u_1
inst✝² : Semiring R
inst✝¹ : CharTwo R
inst✝ : NoZeroDivisors R
x : R
⊢ x ^ 2 = 1 ↔ x = 1
Tactic:
rw [sq, mul_self_eq_one_iff]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.mul_self_eq_iff
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CharTwo R
inst✝ : NoZeroDivisors R
x y : R
⊢ x * x = y * y ↔ x = y
Tactic:
rw [← add_eq_zero_iff_eq, ← add_mul_self, mul_self_eq_zero, add_eq_zero_iff_eq]
Proof state after:
no goals
Theorem: IMOSL.Extra.CharTwo.sq_eq_iff
Proof state before:
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CharTwo R
inst✝ : NoZeroDivisors R
x y : R
⊢ x ^ 2 = y ^ 2 ↔ x = y
Tactic:
rw [sq, sq, mul_self_eq_iff]
Proof state after:
no goals
Theorem: IMOSL.IMO2012N3.prime_not_dvd_descFactorial
Proof state before:
p : ℕ
h : p.Prime
k : ℕ
⊢ ∀ r < p, ¬p ∣ (p * k + r).descFactorial r
Tactic:
refine Nat.rec (λ _ ↦ h.not_dvd_one) (λ r h0 h1 ↦ ?_)
Proof state after:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ (p * k + r.succ).descFactorial r.succ
Theorem: IMOSL.IMO2012N3.prime_not_dvd_descFactorial
Proof state before:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ (p * k + r.succ).descFactorial r.succ
Tactic:
rw [Nat.add_succ, Nat.succ_descFactorial_succ]
Proof state after:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ (p * k + r + 1) * (p * k + r).descFactorial r
Theorem: IMOSL.IMO2012N3.prime_not_dvd_descFactorial
Proof state before:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ (p * k + r + 1) * (p * k + r).descFactorial r
Tactic:
refine h.not_dvd_mul ?_ (h0 <| r.lt_succ_self.trans h1)
Proof state after:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ p * k + r + 1
Theorem: IMOSL.IMO2012N3.prime_not_dvd_descFactorial
Proof state before:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ p * k + r + 1
Tactic:
rw [add_assoc, Nat.dvd_add_right ⟨k, rfl⟩]
Proof state after:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ r + 1
Theorem: IMOSL.IMO2012N3.prime_not_dvd_descFactorial
Proof state before:
p : ℕ
h : p.Prime
k r : ℕ
h0 : r < p → ¬p ∣ (p * k + r).descFactorial r
h1 : r.succ < p
⊢ ¬p ∣ r + 1
Tactic:
exact Nat.not_dvd_of_pos_of_lt r.succ_pos h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012N3.prime_binom_not_dvd
Proof state before:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ False
Tactic:
apply prime_not_dvd_descFactorial h k.pred p.pred (p.pred_lt_self h.pos)
Proof state after:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ p ∣ (p * k.pred + p.pred).descFactorial p.pred
Theorem: IMOSL.IMO2012N3.prime_binom_not_dvd
Proof state before:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ p ∣ (p * k.pred + p.pred).descFactorial p.pred
Tactic:
rw [← Nat.mul_dvd_mul_iff_left (p * k.pred + p.pred).succ_pos,
  ← Nat.succ_descFactorial_succ, ← Nat.succ_eq_add_one, ← Nat.add_succ,
  ← Nat.succ_eq_add_one, Nat.succ_pred h.ne_zero, ← p.mul_succ,
  Nat.succ_pred h0, Nat.descFactorial_eq_factorial_mul_choose, mul_comm]
Proof state after:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ p * (p * k) ∣ p.factorial * (p * k).choose p
Theorem: IMOSL.IMO2012N3.prime_binom_not_dvd
Proof state before:
k p : ℕ
h : p.Prime
h0 : k ≠ 0
h1 : p * k ∣ (p * k).choose p
⊢ p * (p * k) ∣ p.factorial * (p * k).choose p
Tactic:
exact mul_dvd_mul (Nat.dvd_factorial h.pos p.le_refl) h1
Proof state after:
no goals
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
m : ℕ
h : 1 < m
⊢ (∀ (n : ℕ), 2 * n ≤ m → n ∣ n.choose (m - 2 * n)) ↔ m.Prime
Tactic:
refine ⟨λ h0 ↦ ?_, λ h0 n h1 ↦ ?_⟩
Proof state after:
case refine_1
m : ℕ
h : 1 < m
h0 : ∀ (n : ℕ), 2 * n ≤ m → n ∣ n.choose (m - 2 * n)
⊢ m.Prime

case refine_2
m : ℕ
h : 1 < m
h0 : m.Prime
n : ℕ
h1 : 2 * n ≤ m
⊢ n ∣ n.choose (m - 2 * n)
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_1
m : ℕ
h : 1 < m
h0 : ∀ (n : ℕ), 2 * n ≤ m → n ∣ n.choose (m - 2 * n)
⊢ m.Prime

case refine_2
m : ℕ
h : 1 < m
h0 : m.Prime
n : ℕ
h1 : 2 * n ≤ m
⊢ n ∣ n.choose (m - 2 * n)
Tactic:
by_cases h1 : 2 ∣ m
Proof state after:
case pos
m : ℕ
h : 1 < m
h0 : ∀ (n : ℕ), 2 * n ≤ m → n ∣ n.choose (m - 2 * n)
h1 : 2 ∣ m
⊢ m.Prime

case neg
m : ℕ
h : 1 < m
h0 : ∀ (n : ℕ), 2 * n ≤ m → n ∣ n.choose (m - 2 * n)
h1 : ¬2 ∣ m
⊢ m.Prime

case refine_2
m : ℕ
h : 1 < m
h0 : m.Prime
n : ℕ
h1 : 2 * n ≤ m
⊢ n ∣ n.choose (m - 2 * n)
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case pos
m : ℕ
h : 1 < m
h0 : ∀ (n : ℕ), 2 * n ≤ m → n ∣ n.choose (m - 2 * n)
h1 : 2 ∣ m
⊢ m.Prime
Tactic:
rcases h1 with ⟨k, rfl⟩
Proof state after:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : ∀ (n : ℕ), 2 * n ≤ 2 * k → n ∣ n.choose (2 * k - 2 * n)
⊢ (2 * k).Prime
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : ∀ (n : ℕ), 2 * n ≤ 2 * k → n ∣ n.choose (2 * k - 2 * n)
⊢ (2 * k).Prime
Tactic:
specialize h0 k (2 * k).le_refl
Proof state after:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k ∣ k.choose (2 * k - 2 * k)
⊢ (2 * k).Prime
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k ∣ k.choose (2 * k - 2 * k)
⊢ (2 * k).Prime
Tactic:
rw [Nat.sub_self, k.choose_zero_right, Nat.dvd_one] at h0
Proof state after:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k = 1
⊢ (2 * k).Prime
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k = 1
⊢ (2 * k).Prime
Tactic:
rw [h0, mul_one]
Proof state after:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k = 1
⊢ Nat.Prime 2
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k = 1
⊢ Nat.Prime 2
Tactic:
exact Nat.prime_two
Proof state after:
no goals
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg
m : ℕ
h : 1 < m
h0 : ∀ (n : ℕ), 2 * n ≤ m → n ∣ n.choose (m - 2 * n)
h1 : ¬2 ∣ m
⊢ m.Prime
Tactic:
obtain ⟨p, h2, k, rfl⟩ : ∃ p : ℕ, p.Prime ∧ p ∣ m :=
  ⟨m.minFac, Nat.minFac_prime h.ne.symm, m.minFac_dvd⟩
Proof state after:
case neg.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * k
h0 : ∀ (n : ℕ), 2 * n ≤ p * k → n ∣ n.choose (p * k - 2 * n)
h1 : ¬2 ∣ p * k
⊢ (p * k).Prime
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * k
h0 : ∀ (n : ℕ), 2 * n ≤ p * k → n ∣ n.choose (p * k - 2 * n)
h1 : ¬2 ∣ p * k
⊢ (p * k).Prime
Tactic:
rw [Nat.two_dvd_ne_zero, ← Nat.odd_iff, Nat.odd_mul] at h1
Proof state after:
case neg.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * k
h0 : ∀ (n : ℕ), 2 * n ≤ p * k → n ∣ n.choose (p * k - 2 * n)
h1 : Odd p ∧ Odd k
⊢ (p * k).Prime
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * k
h0 : ∀ (n : ℕ), 2 * n ≤ p * k → n ∣ n.choose (p * k - 2 * n)
h1 : Odd p ∧ Odd k
⊢ (p * k).Prime
Tactic:
rcases h1 with ⟨-, k, rfl⟩
Proof state after:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
⊢ (p * (2 * k + 1)).Prime
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
⊢ (p * (2 * k + 1)).Prime
Tactic:
suffices k = 0 by rwa [this, mul_zero, zero_add, mul_one]
Proof state after:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
⊢ k = 0
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
⊢ k = 0
Tactic:
by_contra h1
Proof state after:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
h1 : ¬k = 0
⊢ False
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
h1 : ¬k = 0
⊢ False
Tactic:
apply prime_binom_not_dvd h2 h1
Proof state after:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
h1 : ¬k = 0
⊢ p * k ∣ (p * k).choose p
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
h1 : ¬k = 0
⊢ p * k ∣ (p * k).choose p
Tactic:
specialize h0 (p * k)
Proof state after:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h1 : ¬k = 0
h0 : 2 * (p * k) ≤ p * (2 * k + 1) → p * k ∣ (p * k).choose (p * (2 * k + 1) - 2 * (p * k))
⊢ p * k ∣ (p * k).choose p
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h1 : ¬k = 0
h0 : 2 * (p * k) ≤ p * (2 * k + 1) → p * k ∣ (p * k).choose (p * (2 * k + 1) - 2 * (p * k))
⊢ p * k ∣ (p * k).choose p
Tactic:
rw [mul_add_one (α := ℕ), mul_left_comm, Nat.add_sub_cancel_left] at h0
Proof state after:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h1 : ¬k = 0
h0 : p * (2 * k) ≤ p * (2 * k) + p → p * k ∣ (p * k).choose p
⊢ p * k ∣ (p * k).choose p
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case neg.intro.intro.intro.intro.intro
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h1 : ¬k = 0
h0 : p * (2 * k) ≤ p * (2 * k) + p → p * k ∣ (p * k).choose p
⊢ p * k ∣ (p * k).choose p
Tactic:
exact h0 (Nat.le_add_right (p * (2 * k)) p)
Proof state after:
no goals
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
p : ℕ
h2 : p.Prime
k : ℕ
h : 1 < p * (2 * k + 1)
h0 : ∀ (n : ℕ), 2 * n ≤ p * (2 * k + 1) → n ∣ n.choose (p * (2 * k + 1) - 2 * n)
this : k = 0
⊢ (p * (2 * k + 1)).Prime
Tactic:
rwa [this, mul_zero, zero_add, mul_one]
Proof state after:
no goals
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2
m : ℕ
h : 1 < m
h0 : m.Prime
n : ℕ
h1 : 2 * n ≤ m
⊢ n ∣ n.choose (m - 2 * n)
Tactic:
rw [le_iff_exists_add] at h1
Proof state after:
case refine_2
m : ℕ
h : 1 < m
h0 : m.Prime
n : ℕ
h1 : ∃ c, m = 2 * n + c
⊢ n ∣ n.choose (m - 2 * n)
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2
m : ℕ
h : 1 < m
h0 : m.Prime
n : ℕ
h1 : ∃ c, m = 2 * n + c
⊢ n ∣ n.choose (m - 2 * n)
Tactic:
rcases h1 with ⟨c, rfl⟩
Proof state after:
case refine_2.intro
n c : ℕ
h : 1 < 2 * n + c
h0 : (2 * n + c).Prime
⊢ n ∣ n.choose (2 * n + c - 2 * n)
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro
n c : ℕ
h : 1 < 2 * n + c
h0 : (2 * n + c).Prime
⊢ n ∣ n.choose (2 * n + c - 2 * n)
Tactic:
rw [Nat.add_sub_cancel_left]
Proof state after:
case refine_2.intro
n c : ℕ
h : 1 < 2 * n + c
h0 : (2 * n + c).Prime
⊢ n ∣ n.choose c
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro
n c : ℕ
h : 1 < 2 * n + c
h0 : (2 * n + c).Prime
⊢ n ∣ n.choose c
Tactic:
rcases c with _ | c
Proof state after:
case refine_2.intro.zero
n : ℕ
h : 1 < 2 * n + 0
h0 : (2 * n + 0).Prime
⊢ n ∣ n.choose 0

case refine_2.intro.succ
n c : ℕ
h : 1 < 2 * n + (c + 1)
h0 : (2 * n + (c + 1)).Prime
⊢ n ∣ n.choose (c + 1)
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.succ
n c : ℕ
h : 1 < 2 * n + (c + 1)
h0 : (2 * n + (c + 1)).Prime
⊢ n ∣ n.choose (c + 1)
Tactic:
rcases n with _ | n
Proof state after:
case refine_2.intro.succ.zero
c : ℕ
h : 1 < 2 * 0 + (c + 1)
h0 : (2 * 0 + (c + 1)).Prime
⊢ 0 ∣ Nat.choose 0 (c + 1)

case refine_2.intro.succ.succ
c n : ℕ
h : 1 < 2 * (n + 1) + (c + 1)
h0 : (2 * (n + 1) + (c + 1)).Prime
⊢ n + 1 ∣ (n + 1).choose (c + 1)
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.zero
n : ℕ
h : 1 < 2 * n + 0
h0 : (2 * n + 0).Prime
⊢ n ∣ n.choose 0
Tactic:
rw [Nat.add_zero, Nat.prime_mul_iff] at h0
Proof state after:
case refine_2.intro.zero
n : ℕ
h : 1 < 2 * n + 0
h0 : Nat.Prime 2 ∧ n = 1 ∨ n.Prime ∧ 2 = 1
⊢ n ∣ n.choose 0
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.zero
n : ℕ
h : 1 < 2 * n + 0
h0 : Nat.Prime 2 ∧ n = 1 ∨ n.Prime ∧ 2 = 1
⊢ n ∣ n.choose 0
Tactic:
rcases h0 with ⟨-, rfl⟩ | ⟨-, h1⟩
Proof state after:
case refine_2.intro.zero.inl.intro
h : 1 < 2 * 1 + 0
⊢ 1 ∣ Nat.choose 1 0

case refine_2.intro.zero.inr.intro
n : ℕ
h : 1 < 2 * n + 0
h1 : 2 = 1
⊢ n ∣ n.choose 0
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.zero.inl.intro
h : 1 < 2 * 1 + 0
⊢ 1 ∣ Nat.choose 1 0

case refine_2.intro.zero.inr.intro
n : ℕ
h : 1 < 2 * n + 0
h1 : 2 = 1
⊢ n ∣ n.choose 0
Tactic:
exacts [Nat.dvd_refl 1, absurd h1 (Nat.succ_ne_self 1)]
Proof state after:
no goals
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.succ.zero
c : ℕ
h : 1 < 2 * 0 + (c + 1)
h0 : (2 * 0 + (c + 1)).Prime
⊢ 0 ∣ Nat.choose 0 (c + 1)
Tactic:
exact Nat.dvd_refl 0
Proof state after:
no goals
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.succ.succ
c n : ℕ
h : 1 < 2 * (n + 1) + (c + 1)
h0 : (2 * (n + 1) + (c + 1)).Prime
⊢ n + 1 ∣ (n + 1).choose (c + 1)
Tactic:
refine (Nat.Coprime.dvd_mul_right ?_).mp
  ⟨_, (n.succ_mul_choose_eq c).symm⟩
Proof state after:
case refine_2.intro.succ.succ
c n : ℕ
h : 1 < 2 * (n + 1) + (c + 1)
h0 : (2 * (n + 1) + (c + 1)).Prime
⊢ (n + 1).Coprime c.succ
Theorem: IMOSL.IMO2012N3.final_solution
Proof state before:
case refine_2.intro.succ.succ
c n : ℕ
h : 1 < 2 * (n + 1) + (c + 1)
h0 : (2 * (n + 1) + (c + 1)).Prime
⊢ (n + 1).Coprime c.succ
Tactic:
rw [two_mul, add_assoc] at h0
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).Coprime c.succ