awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
⊢ z.im ≤ (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).im

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : |(HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re| ≤ (↑N : ℝ)
⊢ HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z ∈ verticalStrip (↑N : ℝ) z.im

Tactic:
refine ⟨?_, by simp⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
⊢ (HMul.hMul (α := ℝ) (↑N : ℝ) (-(↑n : ℝ)) +ᵥ z).re = HMul.hMul (α := ℝ) (-(↑N : ℝ)) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ) + z.re

Tactic:
simp only [n, mul_neg, vadd_re, neg_mul]

Premises used: UpperHalfPlane.vadd_re, neg_mul, mul_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
⊢ (HMul.hMul (α := ℝ) (↑N : ℝ) (-(↑n : ℝ)) +ᵥ z).re = HMul.hMul (α := ℝ) (-(↑N : ℝ)) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ) + z.re

Tactic:
have h : (N * (-n : ℝ) +ᵥ z).re = -N * Int.floor (z.re / N) + z.re := by
    simp only [n, mul_neg, vadd_re, neg_mul]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HMul.hMul (α := ℝ) (↑N : ℝ) (-(↑n : ℝ)) +ᵥ z).re = HMul.hMul (α := ℝ) (-(↑N : ℝ)) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ) + z.re
⊢ (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
h₁ : |z.re + (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ)| ≤ (↑N : ℝ)
⊢ |(HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re| ≤ (↑N : ℝ)

Tactic:
rw [h, add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
h₁ : |z.re + -HMul.hMul (α := ℝ) (↑N : ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ)| ≤ (↑N : ℝ)
⊢ |z.re + (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ)| ≤ (↑N : ℝ)

Tactic:
simp only [neg_mul, Int.cast_neg, Int.cast_mul, Int.cast_natCast]

Premises used: Int.cast_neg, Int.cast_natCast, Int.cast_mul, neg_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 0 < N
⊢ LT.lt (α := ℝ) 0 (↑N : ℝ)

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
⊢ LT.lt (α := ℝ) 0 (↑N : ℝ)

Tactic:
have hnn : (0 : ℝ) < (N : ℝ) := by norm_cast at *
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
hnn : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ z.re + -HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) = z.re - HMul.hMul (α := ℝ) (↑n : ℝ) (↑N : ℝ)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
hnn : LT.lt (α := ℝ) 0 (↑N : ℝ)
⊢ z.re + -HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) = z.re - HMul.hMul (α := ℝ) (↑n : ℝ) (↑N : ℝ)

Tactic:
have h2 : z.re + -(N * n) = z.re - n * N := by ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
hnn : LT.lt (α := ℝ) 0 (↑N : ℝ)
h2 : z.re + -HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) = z.re - HMul.hMul (α := ℝ) (↑n : ℝ) (↑N : ℝ)
h₁ : z.re - HMul.hMul (α := ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ) (↑N : ℝ) ≤ (↑N : ℝ)
⊢ |z.re + -HMul.hMul (α := ℝ) (↑N : ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ)| ≤ (↑N : ℝ)

Tactic:
rw [h2, abs_eq_self.2 (Int.sub_floor_div_mul_nonneg (z.re : ℝ) hnn)]

Premises used: Iff.mpr, Int.sub_floor_div_mul_nonneg, abs_eq_self, UpperHalfPlane.re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
hnn : LT.lt (α := ℝ) 0 (↑N : ℝ)
h2 : z.re + -HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) = z.re - HMul.hMul (α := ℝ) (↑n : ℝ) (↑N : ℝ)
⊢ z.re - HMul.hMul (α := ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ) (↑N : ℝ) ≤ (↑N : ℝ)

Tactic:
apply (Int.sub_floor_div_mul_lt (z.re : ℝ) hnn).le

Premises used: LT.lt.le, UpperHalfPlane.re, Int.sub_floor_div_mul_lt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
⊢ (↑ofComplex : ℂ → ℍ) (↑z : ℂ) = z

Tactic:
IsOpenEmbedding.toOpenPartialHomeomorph_left_inv ..

Premises used: UpperHalfPlane.ofComplex, Topology.IsOpenEmbedding.toOpenPartialHomeomorph_left_inv
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
w : ℂ
pos : ∀ (hw : 0 < w.im), (↑ofComplex : ℂ → ℍ) w = { coe := w, coe_im_pos := hw }
neg : ∀ (hw : ¬0 < w.im), (↑ofComplex : ℂ → ℍ) w = Classical.choice ⋯
⊢ (↑ofComplex : ℂ → ℍ) w = if hw : 0 < w.im then { coe := w, coe_im_pos := hw } else Classical.choice ⋯

Tactic:
split_ifs with hw
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
w : ℂ
hw : 0 < w.im
⊢ (↑ofComplex : ℂ → ℍ) w = { coe := w, coe_im_pos := hw }

Tactic:
ofComplex_apply ⟨w, hw⟩

Premises used: UpperHalfPlane.mk, UpperHalfPlane.ofComplex_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
w : ℂ
hw : 0 < w.im
⊢ (↑ofComplex : ℂ → ℍ) w = { coe := w, coe_im_pos := hw }

Tactic:
exact ofComplex_apply ⟨w, hw⟩

Premises used: UpperHalfPlane.mk, UpperHalfPlane.ofComplex_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
w : ℂ
hw : ¬0 < w.im
neg :
  ∀ (h : ∃ (a : ℍ), (↑a : ℂ) = w),
    Eq (α := ℍ) (Classical.choose (p := fun (a : ℍ) ↦ (↑a : ℂ) = w) ⋯) (Classical.choice ⋯)
⊢ invFunOn UpperHalfPlane.coe univ w = Classical.choice ⋯

Tactic:
simp only [invFunOn, dite_eq_right_iff, mem_univ, true_and]

Premises used: Function.invFunOn, dite_eq_right_iff, Set.mem_univ, true_and
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
a : ℍ
hw : ¬0 < (↑a : ℂ).im
⊢ a.im ≤ 0

Tactic:
simpa using hw
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
a : ℍ
hw : ¬0 < (↑a : ℂ).im
⊢ Eq (α := ℍ) (Classical.choose (p := fun (a_1 : ℍ) ↦ (↑a_1 : ℂ) = (↑a : ℂ)) ⋯) (Classical.choice ⋯)

Tactic:
exact (a.im_pos.not_ge (by simpa using hw)).elim

Premises used: UpperHalfPlane.im_pos, False.elim, LT.lt.not_ge
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℂ
hz : 0 < z.im
⊢ (↑ofComplex : ℂ → ℍ) z = { coe := z, coe_im_pos := hz }

Tactic:
ofComplex_apply ⟨z, hz⟩

Premises used: UpperHalfPlane.mk, UpperHalfPlane.ofComplex_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
w : ℂ
hw : w.im ≤ 0
⊢ (↑ofComplex : ℂ → ℍ) w = Classical.choice ⋯

Tactic:
simp [ofComplex_apply_eq_ite w, hw]

Premises used: UpperHalfPlane.ofComplex_apply_eq_ite
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
w w' : ℂ
hw : w.im ≤ 0
hw' : w'.im ≤ 0
⊢ (↑ofComplex : ℂ → ℍ) w = (↑ofComplex : ℂ → ℍ) w'

Tactic:
simp [ofComplex_apply_of_im_nonpos, hw, hw']

Premises used: UpperHalfPlane.ofComplex_apply_of_im_nonpos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
f : ℍ → ℂ
z : ℍ
⊢ (f ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) = f z

Tactic:
congrArg _ <| ofComplex_apply z

Premises used: congrArg, UpperHalfPlane.ofComplex_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
f : ℍ → ℂ
z : ℂ
hz : 0 < z.im
⊢ (f ∘ (↑ofComplex : ℂ → ℍ)) z = f { coe := z, coe_im_pos := hz }

Tactic:
congrArg _ <| ofComplex_apply ⟨z, hz⟩

Premises used: congrArg, UpperHalfPlane.mk, UpperHalfPlane.ofComplex_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
f : ℍ → ℂ
z z' : ℂ
hz : z.im ≤ 0
hz' : z'.im ≤ 0
⊢ (f ∘ (↑ofComplex : ℂ → ℍ)) z = (f ∘ (↑ofComplex : ℂ → ℍ)) z'

Tactic:
simp [ofComplex_apply_of_im_nonpos, hz, hz']

Premises used: UpperHalfPlane.ofComplex_apply_of_im_nonpos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℂ
hz : 0 < z.im
h : ∀ (x : ℂ) (hx : 0 < x.im), (UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ)) x = id x
⊢ UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ) =ᶠ[𝓝 z] id

Tactic:
filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds hz] with x hx

Premises used: IsOpen.mem_nhds, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℂ
hz : 0 < z.im
x : ℂ
hx : 0 < x.im
⊢ (UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ)) x = id x

Tactic:
simp only [Function.comp_apply, ofComplex_apply_of_im_pos hx, id_eq]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos, Function.comp_apply, id_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
coe : (↑(J • τ) : ℂ) = (↑((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))) : ℂ)
⊢ J • τ = (↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
⊢ 0 < Complex.im (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))

Tactic:
simpa using τ.im_pos

Premises used: UpperHalfPlane.im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
coe : -(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ) = (↑((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))) : ℂ)
coe₁ coe₂ :
  -(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ) =
    (↑{ coe := -(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ)
⊢ (↑(J • τ) : ℂ) = (↑((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))) : ℂ)

Tactic:
rw [coe_J_smul, ofComplex_apply_of_im_pos (by simpa using τ.im_pos)]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos, UpperHalfPlane.coe_J_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ IsOpenMap re

Tactic:
Complex.isOpenMap_re.comp isOpenEmbedding_coe.isOpenMap

Premises used: UpperHalfPlane.isOpenEmbedding_coe, Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.comp, UpperHalfPlane.re, Complex.isOpenMap_re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ IsOpenMap im

Tactic:
Complex.isOpenMap_im.comp isOpenEmbedding_coe.isOpenMap

Premises used: Complex.isOpenMap_im, UpperHalfPlane.isOpenEmbedding_coe, Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.comp, UpperHalfPlane.im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ IsOpenMap (Y := ℝ) fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖

Tactic:
.of_nhds_le fun τ U hU ↦ ?_

Premises used: IsOpenMap.of_nhds_le
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
refine :
  ∀ (τ : ℍ) (U : Set ℝ) (hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U), U ∈ 𝓝 ‖(↑τ : ℂ)‖
⊢ IsOpenMap (Y := ℝ) fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖

Tactic:
refine .of_nhds_le fun τ U hU ↦ ?_
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
obtain : ∀ (s : Set ℍ) (hs : s ∈ 𝓝 τ) (hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U), U ∈ 𝓝 ‖(↑τ : ℂ)‖
⊢ U ∈ 𝓝 ‖(↑τ : ℂ)‖

Tactic:
obtain ⟨s, hs, hs'⟩ := Filter.mem_map_iff_exists_image.mp hU

Premises used: Iff.mp, Filter.mem_map_iff_exists_image
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs : s ∈ 𝓝 τ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
simp_rw : ∀ (hs : ∃ ε > 0, Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s), ∃ ε > 0, Metric.ball ‖(↑τ : ℂ)‖ ε ⊆ U
⊢ U ∈ 𝓝 ‖(↑τ : ℂ)‖

Tactic:
simp_rw [← isOpenEmbedding_coe.image_mem_nhds, Metric.mem_nhds_iff] at hs ⊢

Premises used: UpperHalfPlane.isOpenEmbedding_coe, Topology.IsOpenEmbedding.image_mem_nhds, Metric.mem_nhds_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
hs : ∃ ε > 0, Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
obtain :
  ∀ (ε : ℝ) (hεpos : ε > 0) (hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s),
    ∃ ε > 0, Metric.ball ‖(↑τ : ℂ)‖ ε ⊆ U
⊢ ∃ ε > 0, Metric.ball ‖(↑τ : ℂ)‖ ε ⊆ U

Tactic:
obtain ⟨ε, hεpos, hεs⟩ := hs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
⊢ ∃ ε > 0, Metric.ball ‖(↑τ : ℂ)‖ ε ⊆ U

Tactic:
⟨ε, hεpos, subset_trans (fun r hr ↦ ?_) hs'⟩

Premises used: subset_trans, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
refine : ∀ (r : ℝ) (hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε), Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r
⊢ ∃ ε > 0, Metric.ball ‖(↑τ : ℂ)‖ ε ⊆ U

Tactic:
refine ⟨ε, hεpos, subset_trans (fun r hr ↦ ?_) hs'⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
by_contra! : ∀ (hr' : r < 0), False
⊢ 0 ≤ r

Tactic:
by_contra! hr'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : r < 0
⊢ -ε < r - ‖(↑τ : ℂ)‖ ∧ r - ‖(↑τ : ℂ)‖ < ε

Tactic:
rw [mem_ball_iff_norm, Real.norm_eq_abs, abs_lt] at hr

Premises used: mem_ball_iff_norm, abs_lt, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : r < 0
hr₁ : -ε < r - ‖(↑τ : ℂ)‖ ∧ r - ‖(↑τ : ℂ)‖ < ε
⊢ r < 0

Tactic:
rw [mem_ball_iff_norm, Real.norm_eq_abs, abs_lt] at hr

Premises used: mem_ball_iff_norm, abs_lt, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖(↑τ : ℂ)‖ ∧ r - ‖(↑τ : ℂ)‖ < ε
hr' : r < 0
linarith : ε ≤ ‖(↑τ : ℂ)‖ → -ε - (r - ‖(↑τ : ℂ)‖) + (r - 0) + (ε - ‖(↑τ : ℂ)‖) = 0
⊢ ‖(↑τ : ℂ)‖ < ε

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖(↑τ : ℂ)‖ ∧ r - ‖(↑τ : ℂ)‖ < ε
hr' : r < 0
⊢ ‖(↑τ : ℂ)‖ < ε

Tactic:
have : ‖(τ : ℂ)‖ < ε := by linarith
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖(↑τ : ℂ)‖ ∧ r - ‖(↑τ : ℂ)‖ < ε
hr' : r < 0
this : ‖(↑τ : ℂ)‖ < ε
rwa : ‖(↑τ : ℂ) - 0‖ < ε
rwa₁ rwa₂ rwa₃ rwa₄ : ‖(↑τ : ℂ)‖ < ε
⊢ 0 ∈ Metric.ball (↑τ : ℂ) ε

Tactic:
rwa [mem_ball_iff_norm', sub_zero]

Premises used: sub_zero, mem_ball_iff_norm'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖(↑τ : ℂ)‖ ∧ r - ‖(↑τ : ℂ)‖ < ε
hr' : r < 0
this : ‖(↑τ : ℂ)‖ < ε
⊢ 0 ∈ Metric.ball (↑τ : ℂ) ε

Tactic:
have : 0 ∈ Metric.ball (τ : ℂ) ε := by rwa [mem_ball_iff_norm', sub_zero]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖(↑τ : ℂ)‖ ∧ r - ‖(↑τ : ℂ)‖ < ε
hr' : r < 0
this_1 : ‖(↑τ : ℂ)‖ < ε
this : 0 ∈ Metric.ball (↑τ : ℂ) ε
⊢ False

Tactic:
simpa [UpperHalfPlane.ne_zero] using hεs this

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
⊢ 0 ≤ r

Tactic:
have hr' : 0 ≤ r := by
    by_contra! hr'
    rw [mem_ball_iff_norm, Real.norm_eq_abs, abs_lt] at hr
    have : ‖(τ : ℂ)‖ < ε := by linarith
    have : 0 ∈ Metric.ball (τ : ℂ) ε := by rwa [mem_ball_iff_norm', sub_zero]
    simpa [UpperHalfPlane.ne_zero] using hεs this
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
simp : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ) = ((↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) - 1) * (↑τ : ℂ)
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ) = (↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ) * (↑τ : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ) = ((↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) - 1) * (↑τ : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
⊢ ‖(↑τ : ℂ)‖ ≠ 0

Tactic:
simpa using τ.ne_zero

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
rwa : ‖(↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ)‖ < ε
rwa₁ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ) * (↑τ : ℂ)‖ < ε
rwa₂ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ)‖ * ‖(↑τ : ℂ)‖ < ε
rwa₃ : ‖r / ‖(↑τ : ℂ)‖ - 1‖ * ‖(↑τ : ℂ)‖ < ε
rwa₄ : ‖r / ‖‖(↑τ : ℂ)‖‖ - 1‖ * ‖‖(↑τ : ℂ)‖‖ < ε
rwa₅ : ‖(r / ‖‖(↑τ : ℂ)‖‖ - 1) * ‖(↑τ : ℂ)‖‖ < ε
rwa₆ : ‖r / ‖‖(↑τ : ℂ)‖‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
rwa₇ : ‖r / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ - 1 * ‖(↑τ : ℂ)‖‖ < ε
rwa₈ : ‖r / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ - ‖(↑τ : ℂ)‖‖ < ε
rwa₉ : ‖r - ‖(↑τ : ℂ)‖‖ < ε
rwa₁₀ rwa₁₁ rwa₁₂ rwa₁₃ : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε

Tactic:
rwa [mem_ball_iff_norm,
      show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,
      norm_mul, norm_real, ← norm_norm (τ : ℂ), ← norm_mul, sub_mul, norm_norm, one_mul,
      div_mul_cancel₀ _ (by simpa using τ.ne_zero), ← mem_ball_iff_norm]

Premises used: div_mul_cancel₀, UpperHalfPlane.coe, norm_mul, mem_ball_iff_norm, Complex.norm_real, norm_norm, sub_mul, one_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε

Tactic:
have : r / ‖(τ : ℂ)‖ * (τ : ℂ) ∈ Metric.ball (τ : ℂ) ε := by
    rwa [mem_ball_iff_norm,
      show r / ‖(τ : ℂ)‖ * (τ : ℂ) - τ = ↑(r / ‖(τ : ℂ)‖ - 1) * (τ : ℂ) by simp; ring,
      norm_mul, norm_real, ← norm_norm (τ : ℂ), ← norm_mul, sub_mul, norm_norm, one_mul,
      div_mul_cancel₀ _ (by simpa using τ.ne_zero), ← mem_ball_iff_norm]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
obtain :
  ∀ (ξ : ℍ) (hξs : ξ ∈ s) (hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)),
    Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r
⊢ Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r

Tactic:
obtain ⟨ξ, hξs, hξτ⟩ := Set.mem_of_mem_of_subset this hεs

Premises used: Set.mem_of_mem_of_subset
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)
right : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) ξ = r
⊢ Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r

Tactic:
use ξ, hξs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)
right : ‖r‖ / ‖(↑τ : ℂ)‖ * ‖(↑τ : ℂ)‖ = r
⊢ (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) ξ = r

Tactic:
simp_rw [hξτ, norm_mul, norm_div, norm_real, norm_norm]

Premises used: norm_mul, Complex.norm_real, norm_norm, norm_div
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε
hr' : 0 ≤ r
this : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : (↑ξ : ℂ) = (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ)
⊢ ‖(↑τ : ℂ)‖ ≠ 0

Tactic:
simpa using τ.ne_zero

Premises used: UpperHalfPlane.ne_zero