Theorem: C05S03.ex_finset_of_bounded (MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
Q : ℕ → Prop
inst✝ : DecidablePred Q
⊢ (∃ n, ∀ (k : ℕ), Q k → k ≤ n) → ∃ s, ∀ (k : ℕ), Q k ↔ k ∈ s
Tactic:
rintro ⟨n, hn⟩
State after:
case intro
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∃ s, ∀ (k : ℕ), Q k ↔ k ∈ s

State before:
case intro
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∃ s, ∀ (k : ℕ), Q k ↔ k ∈ s
Tactic:
use (range (n + 1)).filter Q
State after:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∀ (k : ℕ), Q k ↔ k ∈ filter Q (range (n + 1))

State before:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
⊢ ∀ (k : ℕ), Q k ↔ k ∈ filter Q (range (n + 1))
Tactic:
intro k
State after:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
k : ℕ
⊢ Q k ↔ k ∈ filter Q (range (n + 1))

State before:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
k : ℕ
⊢ Q k ↔ k ∈ filter Q (range (n + 1))
Tactic:
simp [Nat.lt_succ_iff]
State after:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
k : ℕ
⊢ Q k → k ≤ n

State before:
case h
Q : ℕ → Prop
inst✝ : DecidablePred Q
n : ℕ
hn : ∀ (k : ℕ), Q k → k ≤ n
k : ℕ
⊢ Q k → k ≤ n
Tactic:
exact hn k
State after:
no goals