Theorem: infinite_iff_arb_large (IIScExperiments/Solutions/NumberTheory3Solutions.lean)

State before:
S : Set ℕ
⊢ Set.Infinite S ↔ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
refine ⟨?_, ?_⟩
State after:
case refine_1
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S

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

State before:
case refine_1
S : Set ℕ
⊢ Set.Infinite S → ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S

case refine_2
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S) → Set.Infinite S
Tactic:
{ intro h
  have h2 := Set.Infinite.exists_nat_lt h
  intro n
  rcases h2 n with ⟨m, hm, h3⟩
  use m
  exact ⟨h3, hm⟩
}
State after:
case refine_2
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S) → Set.Infinite S

State before:
case refine_2
S : Set ℕ
⊢ (∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S) → Set.Infinite S
Tactic:
{ contrapose! 
  intro h
  rw [Set.not_infinite] at h
  let S2 : Finset ℕ := Set.Finite.toFinset h
  have h2 : ∃ B, ∀n ∈ S2, n ≤ B
  { use Finset.sup S2 id
    intro n hn
    apply Finset.le_sup hn }
  cases' h2 with N hN
  use N
  have h3 : ∀n : ℕ, n ∈ S ↔ n ∈ S2 := by
    intro n
    exact (Set.Finite.mem_toFinset h).symm
  intros n hn h4
  rw [h3] at h4
  specialize hN n h4
  linarith
}
State after:
no goals

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

State before:
case refine_1
S : Set ℕ
h : Set.Infinite S
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
have h2 := Set.Infinite.exists_nat_lt h
State after:
case refine_1
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S

State before:
case refine_1
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
⊢ ∀ (N : ℕ), ∃ n, n > N ∧ n ∈ S
Tactic:
intro n
State after:
case refine_1
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n : ℕ
⊢ ∃ n_1, n_1 > n ∧ n_1 ∈ S

State before:
case refine_1
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n : ℕ
⊢ ∃ n_1, n_1 > n ∧ n_1 ∈ S
Tactic:
rcases h2 n with ⟨m, hm, h3⟩
State after:
case refine_1.intro.intro
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n m : ℕ
hm : m ∈ S
h3 : n < m
⊢ ∃ n_1, n_1 > n ∧ n_1 ∈ S

State before:
case refine_1.intro.intro
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n m : ℕ
hm : m ∈ S
h3 : n < m
⊢ ∃ n_1, n_1 > n ∧ n_1 ∈ S
Tactic:
use m
State after:
case refine_1.intro.intro
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n m : ℕ
hm : m ∈ S
h3 : n < m
⊢ m > n ∧ m ∈ S

State before:
case refine_1.intro.intro
S : Set ℕ
h : Set.Infinite S
h2 : ∀ (n : ℕ), ∃ m, m ∈ S ∧ n < m
n m : ℕ
hm : m ∈ S
h3 : n < m
⊢ m > n ∧ m ∈ S
Tactic:
exact ⟨h3, hm⟩
State after:
no goals

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

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

State before:
case refine_2
S : Set ℕ
h : ¬Set.Infinite S
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
rw [Set.not_infinite] at h
State after:
case refine_2
S : Set ℕ
h : Set.Finite S
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S

State before:
case refine_2
S : Set ℕ
h : Set.Finite S
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
let S2 : Finset ℕ := Set.Finite.toFinset h
State after:
case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S

State before:
case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
have h2 : ∃ B, ∀n ∈ S2, n ≤ B
State after:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B

case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S

State before:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B

case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
{ use Finset.sup S2 id
  intro n hn
  apply Finset.le_sup hn }
State after:
case refine_2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
h2 : ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
⊢ ∃ N, ∀ (n : ℕ), n > N → ¬n ∈ S

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

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

State before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
⊢ ∀ (n : ℕ), n > N → ¬n ∈ S
Tactic:
have h3 : ∀n : ℕ, n ∈ S ↔ n ∈ S2 := by
  intro n
  exact (Set.Finite.mem_toFinset h).symm
State after:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
⊢ ∀ (n : ℕ), n > N → ¬n ∈ S

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

State before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), 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 refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
h3 : ∀ (n : ℕ), n ∈ S ↔ n ∈ S2
n : ℕ
hn : n > N
h4 : n ∈ S2
⊢ False

State before:
case refine_2.intro
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), 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 refine_2.intro
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 refine_2.intro
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:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∃ B, ∀ (n : ℕ), n ∈ S2 → n ≤ B
Tactic:
use Finset.sup S2 id
State after:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∀ (n : ℕ), n ∈ S2 → n ≤ Finset.sup S2 id

State before:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
⊢ ∀ (n : ℕ), n ∈ S2 → n ≤ Finset.sup S2 id
Tactic:
intro n hn
State after:
case h2
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
n : ℕ
hn : n ∈ S2
⊢ n ≤ Finset.sup S2 id

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

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

State before:
S : Set ℕ
h : Set.Finite S
S2 : Finset ℕ := Set.Finite.toFinset h
N : ℕ
hN : ∀ (n : ℕ), n ∈ S2 → n ≤ N
n : ℕ
⊢ n ∈ S ↔ n ∈ S2
Tactic:
exact (Set.Finite.mem_toFinset h).symm
State after:
no goals