Theorem: C05S03.bounded_of_ex_finset (LeanCourse/MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
Q : ℕ → Prop
⊢ (∃ s, ∀ (k : ℕ), Q k → k ∈ s) → ∃ n, ∀ (k : ℕ), Q k → k < n
Tactic:
rintro ⟨s, hs⟩
State after:
case intro
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∃ n, ∀ (k : ℕ), Q k → k < n

State before:
case intro
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∃ n, ∀ (k : ℕ), Q k → k < n
Tactic:
use s.sup id + 1
State after:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∀ (k : ℕ), Q k → k < sup s id + 1

State before:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
⊢ ∀ (k : ℕ), Q k → k < sup s id + 1
Tactic:
intro k Qk
State after:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k < sup s id + 1

State before:
case h
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k < sup s id + 1
Tactic:
apply Nat.lt_succ_of_le
State after:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k ≤ sup s id

State before:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ k ≤ sup s id
Tactic:
show id k ≤ s.sup id
State after:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ id k ≤ sup s id

State before:
case h.a
Q : ℕ → Prop
s : Finset ℕ
hs : ∀ (k : ℕ), Q k → k ∈ s
k : ℕ
Qk : Q k
⊢ id k ≤ sup s id
Tactic:
apply le_sup (hs k Qk)
State after:
no goals