Theorem: Nat.Prime.eq_of_dvd_of_prime (LeanCourse/MIL/C05_Elementary_Number_Theory/solutions/Solutions_S03_Infinitely_Many_Primes.lean)

State before:
p q : ℕ
prime_p : Nat.Prime p
prime_q : Nat.Prime q
h : p ∣ q
⊢ p = q
Tactic:
cases prime_q.eq_one_or_self_of_dvd _ h
State after:
case inl
p q : ℕ
prime_p : Nat.Prime p
prime_q : Nat.Prime q
h : p ∣ q
h✝ : p = 1
⊢ p = q

case inr
p q : ℕ
prime_p : Nat.Prime p
prime_q : Nat.Prime q
h : p ∣ q
h✝ : p = q
⊢ p = q

State before:
case inr
p q : ℕ
prime_p : Nat.Prime p
prime_q : Nat.Prime q
h : p ∣ q
h✝ : p = q
⊢ p = q
Tactic:
assumption
State after:
no goals

State before:
case inl
p q : ℕ
prime_p : Nat.Prime p
prime_q : Nat.Prime q
h : p ∣ q
h✝ : p = 1
⊢ p = q
Tactic:
linarith [prime_p.two_le]
State after:
no goals