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
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
⊢ Set.Infinite A
case left
f : ℕ → ℕ × ℕ := fun n => (n, n + 1)
inj_f : Function.Injective f
⊢ Set.Infinite A