Theorem: IMOSL.IMO2019N4.eq_zero_of_prime_add_dvd_sq (IMOSLLean4/IMO2019/N4/N4.lean)

State before:
a p : ℕ
h : p.Prime
h0 : a < p
h1 : p + a ∣ p ^ 2
⊢ a = 0
Tactic:
rw [Nat.dvd_prime_pow h] at h1
State after:
a p : ℕ
h : p.Prime
h0 : a < p
h1 : ∃ k ≤ 2, p + a = p ^ k
⊢ a = 0

State before:
a p : ℕ
h : p.Prime
h0 : a < p
h1 : ∃ k ≤ 2, p + a = p ^ k
⊢ a = 0
Tactic:
rcases h1 with ⟨k, h1, h2⟩
State after:
case intro.intro
a p : ℕ
h : p.Prime
h0 : a < p
k : ℕ
h1 : k ≤ 2
h2 : p + a = p ^ k
⊢ a = 0

State before:
case intro.intro
a p : ℕ
h : p.Prime
h0 : a < p
k : ℕ
h1 : k ≤ 2
h2 : p + a = p ^ k
⊢ a = 0
Tactic:
rw [Nat.le_add_one_iff, Nat.le_add_one_iff, zero_add, le_zero_iff] at h1
State after:
case intro.intro
a p : ℕ
h : p.Prime
h0 : a < p
k : ℕ
h1 : (k = 0 ∨ k = 1) ∨ k = 1 + 1
h2 : p + a = p ^ k
⊢ a = 0

State before:
case intro.intro
a p : ℕ
h : p.Prime
h0 : a < p
k : ℕ
h1 : (k = 0 ∨ k = 1) ∨ k = 1 + 1
h2 : p + a = p ^ k
⊢ a = 0
Tactic:
rcases h1 with (rfl | rfl) | rfl
State after:
case intro.intro.inl.inl
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ 0
⊢ a = 0

case intro.intro.inl.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ 1
⊢ a = 0

case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ a = 0

State before:
case intro.intro.inl.inl
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ 0
⊢ a = 0
Tactic:
exact absurd h2 (h.one_lt.trans_le le_self_add).ne.symm
State after:
no goals

State before:
case intro.intro.inl.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ 1
⊢ a = 0
Tactic:
rwa [pow_one, add_right_eq_self] at h2
State after:
no goals

State before:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ a = 0
Tactic:
refine absurd ((add_lt_add_left h0 p).trans_le ?_) h2.not_lt
State after:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ p + p ≤ p ^ (1 + 1)

State before:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ p + p ≤ p ^ (1 + 1)
Tactic:
rw [sq, ← two_mul]
State after:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ 2 * p ≤ p * p

State before:
case intro.intro.inr
a p : ℕ
h : p.Prime
h0 : a < p
h2 : p + a = p ^ (1 + 1)
⊢ 2 * p ≤ p * p
Tactic:
exact Nat.mul_le_mul_right p h.two_le
State after:
no goals