Theorem: Asymptotics.infinitely_many_more_proofs (FormalBook/Chapter_01.lean)

State before:
fn : ℝ≥0
S : ℕ → ℤ
h₁ : AlmostInjective S
h₂ : ofSubexponentialGrowth S
⊢ Fintype { p // ∃ n, ↑↑p ∣ S n } → False
Tactic:
sorry
State after:
no goals