Theorem: IMOSL.IMO2012N3.final_solution (IMOSLLean4/IMO2012/N3/N3.lean)

State before:
m : ℕ
h : 1 < m
⊢ (∀ (n : ℕ), 2 * n ≤ m → n ∣ n.choose (m - 2 * n)) ↔ m.Prime
Tactic:
refine ⟨λ h0 ↦ ?_, λ h0 n h1 ↦ ?_⟩
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)

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
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)

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⟩
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

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
State after:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k ∣ k.choose (2 * k - 2 * k)
⊢ (2 * k).Prime

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
State after:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k = 1
⊢ (2 * k).Prime

State before:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k = 1
⊢ (2 * k).Prime
Tactic:
rw [h0, mul_one]
State after:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k = 1
⊢ Nat.Prime 2

State before:
case pos.intro
k : ℕ
h : 1 < 2 * k
h0 : k = 1
⊢ Nat.Prime 2
Tactic:
exact Nat.prime_two
State after:
no goals

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⟩
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

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
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

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⟩
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

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]
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

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
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

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
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

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)
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

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
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

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)
State after:
no goals

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]
State after:
no goals

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
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)

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⟩
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)

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]
State after:
case refine_2.intro
n c : ℕ
h : 1 < 2 * n + c
h0 : (2 * n + c).Prime
⊢ n ∣ n.choose c

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
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)

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
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)

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
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

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⟩
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

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)]
State after:
no goals

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
State after:
no goals

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⟩
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

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
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

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]
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

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
State after:
no goals