Proof review: Infinity Hotel

Stream: new members

[Huỳnh Trần Khanh]

This is the solution to the Infinity Hotel problem. The goal_bijective proof is partially generated with gptf.

I learned a lot from this problem. Now I know that we can count elements in an infinite set too! This is really surprising to me.

Thanks a lot for your help! :heart: :tada:

lemma goal_bijective : ∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ → ℕ), bijective h ∧ set.restrict h ↑S = f := begin
  intros a b,
  have := @cardinal.extend_function_of_lt ℕ ℕ (↑a : set ℕ) b begin
    rw cardinal.mk_nat,
    exact cardinal.finset_card_lt_omega a,
  end (cardinal.eq.mp rfl),
  cases this with c d,
  use ⇑c,
  split,
  { exact equiv.bijective c, },
  { ext; simp, exact d _, },
end

lemma goal_injective :
  ∀ {S : finset ℕ} (f : ↥(↑S : set ℕ) ↪ ℕ), ∃ (h : ℕ ↪ ℕ), set.restrict h ↑S = f := begin
  intros a b,
  have := goal_bijective b,
  cases this with c d,
  cases d with e f,
  use c,
  { exact e.injective, },
  { exact f, },
end