Theorem: countably_infinite (meetings/ex4.lean)

State before:
⊢ Set.Infinite A ∧ Set.Countable A
Tactic:
constructor
State after:
case left

⊢ Set.Infinite A

case right

⊢ Set.Countable A

State before:
case left

⊢ Set.Infinite A
Tactic:
let f (n : ℕ) : ℕ × ℕ := (n, n + 1)
State after:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
⊢ Set.Infinite A

State before:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
⊢ Set.Infinite A
Tactic:
have inj_f : Function.Injective f := by
  intros a b heq
  simp only [f] at heq
  simp only [Prod.mk.inj_iff] at heq
  exact heq.1
State after:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
⊢ Set.Infinite A

State before:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
⊢ Set.Infinite A
Tactic:
have hf : ∀ (x : ℕ), f x ∈ A := by
  intro x
  simp only [A, f]
  simp only [Set.mem_setOf_eq, le_add_iff_nonneg_right, zero_le]
State after:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
hf : ∀ (x : ℕ), f x ∈ A
⊢ Set.Infinite A

State before:
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
hf : ∀ (x : ℕ), f x ∈ A
⊢ Set.Infinite A
Tactic:
exact Set.infinite_of_injective_forall_mem inj_f hf
State after:
no goals

State before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
⊢ Function.Injective f
Tactic:
intros a b heq
State after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : f a = f b
⊢ a = b

State before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : f a = f b
⊢ a = b
Tactic:
simp only [f] at heq
State after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : (a, a + 1) = (b, b + 1)
⊢ a = b

State before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : (a, a + 1) = (b, b + 1)
⊢ a = b
Tactic:
simp only [Prod.mk.inj_iff] at heq
State after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : a = b ∧ a + 1 = b + 1
⊢ a = b

State before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
a b : ℕ
heq : a = b ∧ a + 1 = b + 1
⊢ a = b
Tactic:
exact heq.1
State after:
no goals

State before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
⊢ ∀ (x : ℕ), f x ∈ A
Tactic:
intro x
State after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
x : ℕ
⊢ f x ∈ A

State before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
x : ℕ
⊢ f x ∈ A
Tactic:
simp only [A, f]
State after:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
x : ℕ
⊢ (x, x + 1) ∈ {p | p.1 ≤ p.2}

State before:
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
x : ℕ
⊢ (x, x + 1) ∈ {p | p.1 ≤ p.2}
Tactic:
simp only [Set.mem_setOf_eq, le_add_iff_nonneg_right, zero_le]
State after:
no goals

State before:
case right

⊢ Set.Countable A
Tactic:
rw [Set.countable_iff_exists_injective]
State after:
case right

⊢ ∃ f, Function.Injective f

State before:
case right

⊢ ∃ f, Function.Injective f
Tactic:
let f (n : A) : ℕ  := 2^n.val.1 * 3^n.val.2
State after:
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
⊢ ∃ f, Function.Injective f

State before:
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
⊢ ∃ f, Function.Injective f
Tactic:
have inj_f : Function.Injective f := by
  intros a b heq
  simp only [f] at heq
  have unique_fac := two_pow_three_pow_unique_factorization heq
  rw [←Prod.eq_iff_fst_eq_snd_eq] at unique_fac
  exact SetCoe.ext unique_fac
State after:
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
inj_f : Function.Injective f
⊢ ∃ f, Function.Injective f

State before:
case right
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
inj_f : Function.Injective f
⊢ ∃ f, Function.Injective f
Tactic:
use f
State after:
no goals

State before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
⊢ Function.Injective f
Tactic:
intros a b heq
State after:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : f a = f b
⊢ a = b

State before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : f a = f b
⊢ a = b
Tactic:
simp only [f] at heq
State after:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
⊢ a = b

State before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
⊢ a = b
Tactic:
have unique_fac := two_pow_three_pow_unique_factorization heq
State after:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : (↑a).1 = (↑b).1 ∧ (↑a).2 = (↑b).2
⊢ a = b

State before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : (↑a).1 = (↑b).1 ∧ (↑a).2 = (↑b).2
⊢ a = b
Tactic:
rw [←Prod.eq_iff_fst_eq_snd_eq] at unique_fac
State after:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : ↑a = ↑b
⊢ a = b

State before:
f : ↑A → ℕ := fun n => 2 ^ (↑n).1 * 3 ^ (↑n).2
a b : ↑A
heq : 2 ^ (↑a).1 * 3 ^ (↑a).2 = 2 ^ (↑b).1 * 3 ^ (↑b).2
unique_fac : ↑a = ↑b
⊢ a = b
Tactic:
exact SetCoe.ext unique_fac
State after:
no goals