Theorem: Section15Sheet3Solutions.infinite_iff_arb_large (FormalisingMathematics2024/Solutions/Section15numberTheory/Sheet3.lean)

State before:
S : Set ℕ
⊢ Set.Infinite S ↔ ∀ (N : ℕ), ∃ n > N, n ∈ S
Tactic:
constructor
State after:
case mp
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n > N, n ∈ S

case mpr
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n > N, n ∈ S) → Set.Infinite S

State before:
case mp
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n > N, n ∈ S
Tactic:
intro h n
State after:
case mp
S : Set ℕ
h : Set.Infinite S
n : ℕ
⊢ ∃ n_1 > n, n_1 ∈ S

State before:
case mp
S : Set ℕ
h : Set.Infinite S
n : ℕ
⊢ ∃ n_1 > n, n_1 ∈ S
Tactic:
have h2 := Set.Infinite.exists_not_mem_finset h (Finset.range (n + 1))
State after:
case mp
S : Set ℕ
h : Set.Infinite S
n : ℕ
h2 : ∃ a ∈ S, a ∉ Finset.range (n + 1)
⊢ ∃ n_1 > n, n_1 ∈ S

State before:
case mp
S : Set ℕ
h : Set.Infinite S
n : ℕ
h2 : ∃ a ∈ S, a ∉ Finset.range (n + 1)
⊢ ∃ n_1 > n, n_1 ∈ S
Tactic:
rcases h2 with ⟨m, hm, h3⟩
State after:
case mp.intro.intro
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ ∃ n_1 > n, n_1 ∈ S

State before:
case mp.intro.intro
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ ∃ n_1 > n, n_1 ∈ S
Tactic:
use m
State after:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ m > n ∧ m ∈ S

State before:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ m > n ∧ m ∈ S
Tactic:
refine' ⟨_, hm⟩
State after:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ m > n

State before:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ∉ Finset.range (n + 1)
⊢ m > n
Tactic:
contrapose! h3
State after:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ≤ n
⊢ m ∈ Finset.range (n + 1)

State before:
case h
S : Set ℕ
h : Set.Infinite S
n m : ℕ
hm : m ∈ S
h3 : m ≤ n
⊢ m ∈ Finset.range (n + 1)
Tactic:
exact Finset.mem_range_succ_iff.mpr h3
State after:
no goals

State before:
case mpr
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n > N, n ∈ S) → Set.Infinite S
Tactic:
contrapose!
State after:
case mpr
S : Set ℕ
⊢ ¬Set.Infinite S → ∃ N, ∀ n > N, n ∉ S

State before:
case mpr
S : Set ℕ
⊢ ¬Set.Infinite S → ∃ N, ∀ n > N, n ∉ S
Tactic:
intro h
State after:
case mpr
S : Set ℕ
h : ¬Set.Infinite S
⊢ ∃ N, ∀ n > N, n ∉ S

State before:
case mpr
S : Set ℕ
h : ¬Set.Infinite S
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
rw [Set.not_infinite] at h
State after:
case mpr
S : Set ℕ
h : Set.Finite S
⊢ ∃ N, ∀ n > N, n ∉ S

State before:
case mpr
S : Set ℕ
h : Set.Finite S
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
let S2 : Finset ℕ := Set.Finite.toFinset h
State after:
case mpr
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ N, ∀ n > N, n ∉ S

State before:
case mpr
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
have h2 : ∃ B, ∀ n ∈ S2, n ≤ B := by
  use Finset.sup S2 id
  intros _ H
  apply Finset.le_sup H
State after:
case mpr
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ n ∈ S2, n ≤ B
⊢ ∃ N, ∀ n > N, n ∉ S

State before:
case mpr
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ n ∈ S2, n ≤ B
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
cases' h2 with N hN
State after:
case mpr.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∃ N, ∀ n > N, n ∉ S

State before:
case mpr.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∃ N, ∀ n > N, n ∉ S
Tactic:
use N
State after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∀ n > N, n ∉ S

State before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∀ n > N, n ∉ S
Tactic:
have h3 : ∀ n : ℕ, n ∈ S ↔ n ∈ S2
State after:
case h3
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∀ (n : ℕ), n ∈ S ↔ n ∈ S2

case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S

State before:
case h3
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
⊢ ∀ (n : ℕ), n ∈ S ↔ n ∈ S2

case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Tactic:
intro n
State after:
case h3
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
n : ℕ
⊢ n ∈ S ↔ n ∈ S2

case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S

State before:
case h3
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
n : ℕ
⊢ n ∈ S ↔ n ∈ S2

case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Tactic:
exact (Set.Finite.mem_toFinset h).symm
State after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S

State before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ n > N, n ∉ S
Tactic:
intro n hn h4
State after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S
⊢ False

State before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S
⊢ False
Tactic:
rw [h3] at h4
State after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
⊢ False

State before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ n ∈ S2, n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
⊢ False
Tactic:
specialize hN n h4
State after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
hN : n ≤ N
⊢ False

State before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
hN : n ≤ N
⊢ False
Tactic:
linarith
State after:
no goals

State before:
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ B, ∀ n ∈ S2, n ≤ B
Tactic:
use Finset.sup S2 id
State after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∀ n ∈ S2, n ≤ Finset.sup S2 id

State before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∀ n ∈ S2, n ≤ Finset.sup S2 id
Tactic:
intros _ H
State after:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
n✝ : ℕ
H : n✝ ∈ S2
⊢ n✝ ≤ Finset.sup S2 id

State before:
case h
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
n✝ : ℕ
H : n✝ ∈ S2
⊢ n✝ ≤ Finset.sup S2 id
Tactic:
apply Finset.le_sup H
State after:
no goals