[GOAL]
S : Set ℍ
⊢ S ∈ atImInfty ↔ ∃ A, ∀ (z : ℍ), A ≤ im z → z ∈ S
[PROOFSTEP]
simp only [atImInfty_basis.mem_iff, true_and]
[GOAL]
S : Set ℍ
⊢ (∃ i, im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ A, ∀ (z : ℍ), A ≤ im z → z ∈ S
[PROOFSTEP]
rfl
[GOAL]
f g : ℍ → ℂ
hf : IsBoundedAtImInfty f
hg : IsBoundedAtImInfty g
⊢ IsBoundedAtImInfty (f * g)
[PROOFSTEP]
simpa only [Pi.one_apply, mul_one, norm_eq_abs] using hf.mul hg
[GOAL]
f : ℍ → ℂ
⊢ IsBoundedAtImInfty f ↔ ∃ M A, ∀ (z : ℍ), A ≤ im z → ↑Complex.abs (f z) ≤ M
[PROOFSTEP]
simp [IsBoundedAtImInfty, BoundedAtFilter, Asymptotics.isBigO_iff, Filter.Eventually, atImInfty_mem]
[GOAL]
f : ℍ → ℂ
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ (x : ℍ), x ∈ im ⁻¹' Set.Ici ia → f x ∈ Metric.closedBall 0 ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ im z → ↑Complex.abs (f z) ≤ ε
[PROOFSTEP]
simp only [true_and, mem_closedBall_zero_iff]
[GOAL]
f : ℍ → ℂ
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, ∀ (x : ℍ), x ∈ im ⁻¹' Set.Ici ia → ‖f x‖ ≤ ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ A, ∀ (z : ℍ), A ≤ im z → ↑Complex.abs (f z) ≤ ε
[PROOFSTEP]
rfl
