awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦
    (if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
          ContinuousAlgEquiv.refl ℝ ℂ
        else conjCAE :
        (a : ℂ) → ℂ)
      (num g (↑x : ℂ) / denom g (↑x : ℂ))
have refine_1 : Continuous (X := ℂ) (Y := ℂ)
  (⇑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
        ContinuousAlgEquiv.refl ℝ ℂ
      else conjCAE) :
    (a : ℂ) → ℂ)
Tactic: refine .comp ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
g : GL (Fin 2) ℝ
refine_1 :
  Continuous (X := ℂ) (Y := ℂ)
    (⇑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
          ContinuousAlgEquiv.refl ℝ ℂ
        else conjCAE) :
      (a : ℂ) → ℂ)
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦
    (if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
          ContinuousAlgEquiv.refl ℝ ℂ
        else conjCAE :
        (a : ℂ) → ℂ)
      (num g (↑x : ℂ) / denom g (↑x : ℂ))
have refine_2 : Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ) / denom g (↑x : ℂ)
Tactic: refine .comp ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (X := ℂ) (Y := ℂ)
    (⇑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
          ContinuousAlgEquiv.refl ℝ ℂ
        else conjCAE) :
      (a : ℂ) → ℂ)
have pos : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  Continuous (X := ℂ) (Y := ℂ) (⇑(ContinuousAlgEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
g : GL (Fin 2) ℝ
pos :
  LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    Continuous (X := ℂ) (Y := ℂ) (⇑(ContinuousAlgEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
⊢ Continuous (X := ℂ) (Y := ℂ)
    (⇑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
          ContinuousAlgEquiv.refl ℝ ℂ
        else conjCAE) :
      (a : ℂ) → ℂ)
have neg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  Continuous (X := ℂ) (Y := ℂ) (⇑conjCAE : (a : ℂ) → ℂ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ) / denom g (↑x : ℂ)
have refine_2 : Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ)
Tactic: refine .div ?_ ?_ (fun x ↦ denom_ne_zero g x)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
g : GL (Fin 2) ℝ
refine_2 : Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ)
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ) / denom g (↑x : ℂ)
have refine_2₁ : Continuous (Y := ℂ) fun (x : ℍ) ↦ denom g (↑x : ℂ)
Tactic: refine .div ?_ ?_ (fun x ↦ denom_ne_zero g x)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
K : Set ℍ
hK : IsCompact K
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
have inl : ∀ (hK : IsCompact (X := ℍ) ∅), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ ∅ ⊆ verticalStrip A B
Tactic: rcases K.eq_empty_or_nonempty with rfl | hne
Cleared hypotheses: K, hK
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
K : Set ℍ
hK : IsCompact K
inl : ∀ (hK : IsCompact (X := ℍ) ∅), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ ∅ ⊆ verticalStrip A B
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
have inr : ∀ (hne : K.Nonempty), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
Tactic: rcases K.eq_empty_or_nonempty with rfl | hne
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
have inr : ∀ u ∈ K, ∀ (hu : IsMaxOn (abs ∘ re) K u), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
Tactic: obtain ⟨u, _, hu⟩ := hK.exists_isMaxOn hne (_root_.continuous_abs.comp continuous_re).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
u : ℍ
left : u ∈ K
hu : IsMaxOn (abs ∘ re) K u
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
have inr : ∀ v ∈ K, ∀ (hv : IsMinOn im K v), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
Tactic: obtain ⟨v, _, hv⟩ := hK.exists_isMinOn hne continuous_im.continuousOn
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
⊢ ∃ (n : ℤ), ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im
have h : ModularGroup.T ^ ((↑N : ℤ) * -n) • z ∈ verticalStrip (↑N : ℝ) z.im
Tactic: use -n
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
⊢ ModularGroup.T ^ ((↑N : ℤ) * -n) • z ∈ verticalStrip (↑N : ℝ) z.im
have h : HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z ∈ verticalStrip (↑N : ℝ) z.im
Tactic: rw [modular_T_zpow_smul z (N * -n)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
⊢ HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z ∈ verticalStrip (↑N : ℝ) z.im
have h : |(HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re| ≤ (↑N : ℝ)
Tactic: refine ⟨?_, by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
⊢ |(HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re| ≤ (↑N : ℝ)
have h : (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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
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 : ℝ)
have h₁ : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
Tactic: norm_cast at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
⊢ |(HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re| ≤ (↑N : ℝ)
have h₁ : |z.re + (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ)| ≤ (↑N : ℝ)
Tactic: rw [h, add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
⊢ |z.re + (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ)| ≤ (↑N : ℝ)
have h₁ : |z.re + -HMul.hMul (α := ℝ) (↑N : ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ)| ≤ (↑N : ℝ)
Tactic: simp only [neg_mul, Int.cast_neg, Int.cast_mul, Int.cast_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * -n) : ℝ) z).re = (↑(-(↑N : ℤ) * ⌊z.re / (↑N : ℝ)⌋) : ℝ) + z.re
⊢ |z.re + -HMul.hMul (α := ℝ) (↑N : ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ)| ≤ (↑N : ℝ)
have hnn : LT.lt (α := ℝ) 0 (↑N : ℝ)
Tactic: have hnn : (0 : ℝ) < (N : ℝ) := by norm_cast at *
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
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 : ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ)| ≤ (↑N : ℝ)
have h2 : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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 (α := ℝ) (↑N : ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ)| ≤ (↑N : ℝ)
have h₁ : z.re - HMul.hMul (α := ℝ) (↑⌊z.re / (↑N : ℝ)⌋ : ℝ) (↑N : ℝ) ≤ (↑N : ℝ)
Tactic: rw [h2, abs_eq_self.2 (Int.sub_floor_div_mul_nonneg (z.re : ℝ) hnn)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
w : ℂ
⊢ (↑ofComplex : ℂ → ℍ) w = if hw : 0 < w.im then { coe := w, coe_im_pos := hw } else Classical.choice ⋯
have pos : ∀ (hw : 0 < w.im), (↑ofComplex : ℂ → ℍ) w = { coe := w, coe_im_pos := hw }
Tactic: split_ifs with hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
w : ℂ
pos : ∀ (hw : 0 < w.im), (↑ofComplex : ℂ → ℍ) w = { coe := w, coe_im_pos := hw }
⊢ (↑ofComplex : ℂ → ℍ) w = if hw : 0 < w.im then { coe := w, coe_im_pos := hw } else Classical.choice ⋯
have neg : ∀ (hw : ¬0 < w.im), (↑ofComplex : ℂ → ℍ) w = Classical.choice sorry
Tactic: split_ifs with hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
w : ℂ
hw : ¬0 < w.im
⊢ invFunOn UpperHalfPlane.coe univ w = Classical.choice ⋯
have neg : ∀ (h : ∃ (a : ℍ), (↑a : ℂ) = w), Eq (α := ℍ) (Classical.choose (p := fun (a : ℍ) ↦ (↑a : ℂ) = w) sorry) (Classical.choice sorry)
Tactic: simp only [invFunOn, dite_eq_right_iff, mem_univ, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
z : ℂ
hz : 0 < z.im
⊢ UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ) =ᶠ[𝓝 z] id
have h : ∀ (x : ℂ) (hx : 0 < x.im), (UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ)) x = id x
Tactic: filter_upwards [isOpen_upperHalfPlaneSet.mem_nhds hz] with x hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
⊢ J • τ = (↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))
have coe : (↑(J • τ) : ℂ) = (↑((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))) : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
⊢ (↑(J • τ) : ℂ) = (↑((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))) : ℂ)
have coe : -(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ) = (↑((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))) : ℂ)
Tactic: rw [coe_J_smul, ofComplex_apply_of_im_pos (by simpa using τ.im_pos)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
coe : -(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ) = (↑((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))) : ℂ)
⊢ (↑(J • τ) : ℂ) = (↑((↑ofComplex : ℂ → ℍ) (-(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ))) : ℂ)
have coe₁ : -(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ) = (↑{ coe := -(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ), coe_im_pos := sorry : ℍ } : ℂ)
Tactic: rw [coe_J_smul, ofComplex_apply_of_im_pos (by simpa using τ.im_pos)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
⊢ IsOpenMap (Y := ℝ) fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖
have refine : ∀ (τ : ℍ) (U : Set ℝ) (hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U), U ∈ 𝓝 ‖(↑τ : ℂ)‖
Tactic: refine .of_nhds_le fun τ U hU ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
⊢ U ∈ 𝓝 ‖(↑τ : ℂ)‖
have obtain : ∀ (s : Set ℍ) (hs : s ∈ 𝓝 τ) (hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U), U ∈ 𝓝 ‖(↑τ : ℂ)‖
Tactic: obtain ⟨s, hs, hs'⟩ := Filter.mem_map_iff_exists_image.mp hU
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs : s ∈ 𝓝 τ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
⊢ U ∈ 𝓝 ‖(↑τ : ℂ)‖
have simp_rw : ∀ (hs : ∃ ε > 0, Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s), ∃ ε > 0, Metric.ball ‖(↑τ : ℂ)‖ ε ⊆ U
Tactic: simp_rw [← isOpenEmbedding_coe.image_mem_nhds, Metric.mem_nhds_iff] at hs ⊢
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
τ : ℍ
U : Set ℝ
hU : Membership.mem (γ := Filter ℝ) (map (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (𝓝 τ)) U
s : Set ℍ
hs' : (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s ⊆ U
hs : ∃ ε > 0, Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s
⊢ ∃ ε > 0, Metric.ball ‖(↑τ : ℂ)‖ ε ⊆ U
have obtain : ∀ (ε : ℝ) (hεpos : ε > 0) (hεs : Metric.ball (↑τ : ℂ) ε ⊆ UpperHalfPlane.coe '' s),
  ∃ ε > 0, Metric.ball ‖(↑τ : ℂ)‖ ε ⊆ U
Tactic: obtain ⟨ε, hεpos, hεs⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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
have refine : ∀ (r : ℝ) (hr : r ∈ Metric.ball ‖(↑τ : ℂ)‖ ε), Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r
Tactic: refine ⟨ε, hεpos, subset_trans (fun r hr ↦ ?_) hs'⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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
have by_contra! : ∀ (hr' : r < 0), False
Tactic: by_contra! hr'
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
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
⊢ False
have hr₁ : -ε < r - ‖(↑τ : ℂ)‖ ∧ r - ‖(↑τ : ℂ)‖ < ε
Tactic: rw [mem_ball_iff_norm, Real.norm_eq_abs, abs_lt] at hr
Cleared hypotheses: hr, hr'
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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
⊢ ‖(↑τ : ℂ)‖ < ε
have linarith : ε ≤ ‖(↑τ : ℂ)‖ → -ε - (r - ‖(↑τ : ℂ)‖) + (r - 0) + (ε - ‖(↑τ : ℂ)‖) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
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
⊢ False
have this : ‖(↑τ : ℂ)‖ < ε
Tactic: have : ‖(τ : ℂ)‖ < ε := by linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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 (↑τ : ℂ) ε
have rwa : ‖(↑τ : ℂ) - 0‖ < ε
Tactic: rwa [mem_ball_iff_norm', sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
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 : ‖(↑τ : ℂ)‖ < ε
⊢ False
have this₁ : 0 ∈ Metric.ball (↑τ : ℂ) ε
Tactic: have : 0 ∈ Metric.ball (τ : ℂ) ε := by rwa [mem_ball_iff_norm', sub_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
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 ‖(↑τ : ℂ)‖ ε
⊢ Membership.mem (γ := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' s) r
have hr' : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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) : ℂ) * (↑τ : ℂ)
have simp : (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ) = ((↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) - 1) * (↑τ : ℂ)
Tactic: simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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 (↑τ : ℂ) ε
have rwa : ‖(↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ)‖ < ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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 : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) - (↑τ : ℂ)‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₁ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ) * (↑τ : ℂ)‖ < ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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) : ℂ) * (↑τ : ℂ)‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₂ : ‖(↑(r / ‖(↑τ : ℂ)‖ - 1) : ℂ)‖ * ‖(↑τ : ℂ)‖ < ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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) : ℂ)‖ * ‖(↑τ : ℂ)‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₃ : ‖r / ‖(↑τ : ℂ)‖ - 1‖ * ‖(↑τ : ℂ)‖ < ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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‖ * ‖(↑τ : ℂ)‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₄ : ‖r / ‖‖(↑τ : ℂ)‖‖ - 1‖ * ‖‖(↑τ : ℂ)‖‖ < ε
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
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‖ * ‖‖(↑τ : ℂ)‖‖ < ε
⊢ (↑r : ℂ) / (↑‖(↑τ : ℂ)‖ : ℂ) * (↑τ : ℂ) ∈ Metric.ball (↑τ : ℂ) ε
have rwa₅ : ‖(r / ‖‖(↑τ : ℂ)‖‖ - 1) * ‖(↑τ : ℂ)‖‖ < ε
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]