Theorem: PrimeRange.prodDvdOfLt (FromTheBook/Ch02/UnboundedGaps.lean)

State before:
k p : ℕ
hp : Nat.Prime p
⊢ p < k → p ∣ prod k
Tactic:
intro hk
State after:
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p ∣ prod k

State before:
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p ∣ prod k
Tactic:
apply List.dvd_prod
State after:
case ha
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p ∈ PrimeRange k

State before:
case ha
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p ∈ PrimeRange k
Tactic:
simp [PrimeRange, List.mem_filter]
State after:
case ha
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p < k ∧ Nat.Prime p

State before:
case ha
k p : ℕ
hp : Nat.Prime p
hk : p < k
⊢ p < k ∧ Nat.Prime p
Tactic:
exact ⟨hk, hp⟩
State after:
no goals