awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
a : ℝ
ha : 0 < a
ha' : Membership.mem (γ := Set ℝ) (Set.Iio 1) a
nlinarith : 1 / 2 ≤ a * |x.re| → 2 / 2 = 1
nlinarith₁ nlinarith₂ : 1 / 2 ≤ a * |x.re| → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₃ : 1 / 2 ≤ a * |x.re| → GT.gt (α := ℝ) 2 0
nlinarith₄ : 1 / 2 ≤ a * |x.re| → 2 / 2 = 1
nlinarith₅ : 1 / 2 ≤ a * |x.re| → HMul.hMul (α := ℝ) 1 2 = 2
nlinarith₆ : 1 / 2 ≤ a * |x.re| → GT.gt (α := ℝ) 2 0
nlinarith₇ :
  1 / 2 ≤ a * |x.re| →
    HMul.hMul (α := ℝ) 1 1 - 1 * a * (2 * |x.re|) + (a - 1) + (0 - (2 * |x.re| - HMul.hMul (α := ℝ) 1 1) * (0 - a)) = 0
⊢ a * |x.re| < 1 / 2

Tactic:
nlinarith [Set.mem_Iio.mp ha']

Premises used: Set.mem_Iio, Iff.mp
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun (t : ℝ) ↦ (↑ofComplex : ℂ → ℍ) ((↑t : ℂ) * (↑x : ℂ))) (𝓝[<] 1) (𝓝 x)

Tactic:
.mono_left ?_ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
hf : Filter.Tendsto (fun (t : ℝ) ↦ (↑ofComplex : ℂ → ℍ) ((↑t : ℂ) * (↑x : ℂ))) (𝓝 1) (𝓝 x)
⊢ Filter.Tendsto (fun (t : ℝ) ↦ (↑ofComplex : ℂ → ℍ) ((↑t : ℂ) * (↑x : ℂ))) (𝓝[<] 1) (𝓝 x)

Tactic:
refine .mono_left ?_ nhdsWithin_le_nhds
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
hf : Filter.Tendsto (fun (x_1 : ℝ) ↦ (↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))
⊢ Filter.Tendsto (fun (t : ℝ) ↦ (↑ofComplex : ℂ → ℍ) ((↑t : ℂ) * (↑x : ℂ))) (𝓝 1) (𝓝 x)

Tactic:
rw [isOpenEmbedding_coe.tendsto_nhds_iff, Function.comp_def]

Premises used: UpperHalfPlane.isOpenEmbedding_coe, Function.comp_def, Topology.IsOpenEmbedding.tendsto_nhds_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ 𝓝 (↑x : ℂ) = 𝓝 ((↑1 : ℂ) * (↑x : ℂ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
rw : Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 ((↑1 : ℂ) * (↑x : ℂ)))
⊢ Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))

Tactic:
rw [show 𝓝 (x : ℂ) = 𝓝 ((1 : ℝ) * (x : ℂ)) by simp]
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ Continuous (Y := ℂ) fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 ((↑1 : ℂ) * (↑x : ℂ)))

Tactic:
exact Continuous.tendsto (by fun_prop) _

Premises used: Continuous.tendsto
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))

Tactic:
have : Filter.Tendsto (fun t : ℝ ↦ t * (x : ℂ)) (𝓝 1) (𝓝 (x : ℂ)) := by
      rw [show 𝓝 (x : ℂ) = 𝓝 ((1 : ℝ) * (x : ℂ)) by simp]
      exact Continuous.tendsto (by fun_prop) _
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))
⊢ Filter.Tendsto (fun (x_1 : ℝ) ↦ (↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))

Tactic:
this.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))
hf :
  Filter.EventuallyEq (β := ℂ) (𝓝 1) (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) fun (x_1 : ℝ) ↦
    (↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)
⊢ Filter.Tendsto (fun (x_1 : ℝ) ↦ (↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))

Tactic:
refine this.congr' ?_

Premises used: Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))
h : ∀ (a : ℝ) (ha : 0 < a), (↑a : ℂ) * (↑x : ℂ) = (↑((↑ofComplex : ℂ → ℍ) ((↑a : ℂ) * (↑x : ℂ))) : ℂ)
⊢ Filter.EventuallyEq (β := ℂ) (𝓝 1) (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) fun (x_1 : ℝ) ↦
    (↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)

Tactic:
filter_upwards [eventually_gt_nhds zero_lt_one] with a ha

Premises used: eventually_gt_nhds, zero_lt_one
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))
a : ℝ
ha : 0 < a
⊢ 0 < ((↑a : ℂ) * (↑x : ℂ)).im

Tactic:
simpa using mul_pos ha x.coe_im_pos

Premises used: mul_pos, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
this : Filter.Tendsto (fun (t : ℝ) ↦ (↑t : ℂ) * (↑x : ℂ)) (𝓝 1) (𝓝 (↑x : ℂ))
a : ℝ
ha : 0 < a
h h₁ : (↑a : ℂ) * (↑x : ℂ) = (↑{ coe := (↑a : ℂ) * (↑x : ℂ), coe_im_pos := ⋯ } : ℂ)
⊢ (↑a : ℂ) * (↑x : ℂ) = (↑((↑ofComplex : ℂ → ℍ) ((↑a : ℂ) * (↑x : ℂ))) : ℂ)

Tactic:
rw [ofComplex_apply_of_im_pos (by simpa using mul_pos ha x.coe_im_pos)]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
rw : x ∈ closure (closure 𝒟ᵒ)
⊢ x ∈ closure 𝒟ᵒ

Tactic:
rw [← closure_closure]

Premises used: closure_closure
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
t : ℝ≥0
⊢ 0 < ((↑x : ℂ) + (↑(↑t : ℝ) : ℂ) * Complex.I).im

Tactic:
simpa using add_pos_of_pos_of_nonneg x.coe_im_pos t.property

Premises used: UpperHalfPlane.coe_im_pos, add_pos_of_pos_of_nonneg, Subtype.property
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
h : ∃ᶠ (x_1 : ℝ≥0) in 𝓝[>] 0, { coe := (↑x : ℂ) + (↑(↑x_1 : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } ∈ closure 𝒟ᵒ
hf : Filter.Tendsto (fun (t : ℝ≥0) ↦ { coe := (↑x : ℂ) + (↑(↑t : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)
⊢ x ∈ closure (closure 𝒟ᵒ)

Tactic:
apply mem_closure_of_frequently_of_tendsto (b := 𝓝[>] 0)
    (f := fun t : ℝ≥0 ↦ ⟨x + t * Complex.I, by
      simpa using add_pos_of_pos_of_nonneg x.coe_im_pos t.property⟩)

Premises used: mem_closure_of_frequently_of_tendsto
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
h : ∀ᶠ (x_1 : ℝ≥0) in 𝓝[>] 0, { coe := (↑x : ℂ) + (↑(↑x_1 : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } ∈ closure 𝒟ᵒ
⊢ ∃ᶠ (x_1 : ℝ≥0) in 𝓝[>] 0, { coe := (↑x : ℂ) + (↑(↑x_1 : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } ∈ closure 𝒟ᵒ

Tactic:
apply Filter.Eventually.frequently

Premises used: Filter.Eventually.frequently
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
h : ∀ (ha : 0 < a), { coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } ∈ closure 𝒟ᵒ
⊢ Membership.mem (γ := Set ℝ≥0) (Set.Ioi 0) a →
    { coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } ∈ closure 𝒟ᵒ

Tactic:
(ha : 0 < a)
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
h : ∀ (a : ℝ≥0) (ha : 0 < a), { coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } ∈ closure 𝒟ᵒ
⊢ ∀ᶠ (x_1 : ℝ≥0) in 𝓝[>] 0, { coe := (↑x : ℂ) + (↑(↑x_1 : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } ∈ closure 𝒟ᵒ

Tactic:
filter_upwards [self_mem_nhdsWithin] with a (ha : 0 < a)

Premises used: self_mem_nhdsWithin
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ |{ coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ }.re| ≤ 1 / 2

Tactic:
simpa using hxre
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
h : 1 < ‖(↑{ coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } : ℂ)‖
⊢ { coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } ∈ closure 𝒟ᵒ

Tactic:
refine mem_closure_of_one_lt_norm ?_ (by simpa using hxre)

Premises used: _private.0.ModularGroup.mem_closure_of_one_lt_norm
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
rw :
  LT.lt (α := ℝ) (1 : ℝ)
    ((normSq : (a : ℂ) → ℝ) (↑{ coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } : ℂ) : ℝ)
⊢ 1 < ‖(↑{ coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } : ℂ)‖

Tactic:
rw [← one_lt_normSq_iff]

Premises used: Complex.one_lt_normSq_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
⊢ 1 < HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im

Tactic:
this
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
h :
  (normSq : (a : ℂ) → ℝ) (↑{ coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } : ℂ) =
    HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
⊢ LT.lt (α := ℝ) (1 : ℝ)
    ((normSq : (a : ℂ) → ℝ) (↑{ coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } : ℂ) : ℝ)

Tactic:
convert! this
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
h :
  x.re * x.re + (x.im + (↑a : ℝ)) * (x.im + (↑a : ℝ)) =
    x.re * x.re + x.im * x.im + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
⊢ (normSq : (a : ℂ) → ℝ) (↑{ coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } : ℂ) =
    HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im

Tactic:
simp [← normSq_eq_norm_sq, normSq_apply]

Premises used: Complex.normSq_eq_norm_sq, Complex.normSq_apply
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
this : 1 < HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
⊢ x.re * x.re + (x.im + (↑a : ℝ)) * (x.im + (↑a : ℝ)) =
    x.re * x.re + x.im * x.im + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im

Tactic:
ring
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
h : 1 < HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
⊢ 1 < ‖(↑{ coe := (↑x : ℂ) + (↑(↑a : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ : ℍ } : ℂ)‖

Tactic:
suffices 1 < ‖(x : ℂ)‖ ^ 2 + a ^ 2 + 2 * a * x.im by
      rw [← one_lt_normSq_iff]
      convert! this
      simp [← normSq_eq_norm_sq, normSq_apply]
      ring
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
h : 0 < HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im
⊢ 1 < HPow.hPow (β := ℕ) ‖(↑x : ℂ)‖ 2 + HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im

Tactic:
rw [hxnorm, one_pow, add_assoc, lt_add_iff_pos_right]

Premises used: one_pow, lt_add_iff_pos_right, add_assoc
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
a : ℝ≥0
ha : 0 < a
⊢ 0 < HPow.hPow (β := ℕ) (↑a : ℝ) 2 + 2 * (↑a : ℝ) * x.im

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun (t : ℝ≥0) ↦ { coe := (↑x : ℂ) + (↑(↑t : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)

Tactic:
.mono_left ?_ nhdsWithin_le_nhds

Premises used: nhdsWithin_le_nhds, Filter.Tendsto.mono_left
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
hf : Filter.Tendsto (fun (t : ℝ≥0) ↦ { coe := (↑x : ℂ) + (↑(↑t : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ }) (𝓝 0) (𝓝 x)
⊢ Filter.Tendsto (fun (t : ℝ≥0) ↦ { coe := (↑x : ℂ) + (↑(↑t : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ }) (𝓝[>] 0) (𝓝 x)

Tactic:
refine .mono_left ?_ nhdsWithin_le_nhds
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ 𝓝 (↑x : ℂ) = 𝓝 ((↑x : ℂ) + (↑(↑0 : ℝ) : ℂ) * Complex.I)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Continuous (X := ℝ≥0)
    (UpperHalfPlane.coe ∘ fun (t : ℝ≥0) ↦ { coe := (↑x : ℂ) + (↑(↑t : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ })

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : ‖(↑x : ℂ)‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ Filter.Tendsto (fun (t : ℝ≥0) ↦ { coe := (↑x : ℂ) + (↑(↑t : ℝ) : ℂ) * Complex.I, coe_im_pos := ⋯ }) (𝓝 0) (𝓝 x)

Tactic:
simpa [show 𝓝 (x : ℂ) = 𝓝 (x + (((0 : ℝ≥0) : ℝ) : ℂ) * Complex.I) by simp,
      isOpenEmbedding_coe.tendsto_nhds_iff] using Continuous.tendsto (by fun_prop) _

Premises used: UpperHalfPlane.isOpenEmbedding_coe, Continuous.tendsto, Topology.IsOpenEmbedding.tendsto_nhds_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ 𝒟 = closure 𝒟ᵒ

Tactic:
subset_antisymm ?_ (isClosed_fd.closure_subset_iff.mpr fdo_subset_fd)

Premises used: Iff.mpr, ModularGroup.fdo_subset_fd, subset_antisymm, IsClosed.closure_subset_iff, ModularGroup.isClosed_fd
-- Module: Mathlib.NumberTheory.Modular
Goal:
refine : 𝒟 ⊆ closure 𝒟ᵒ
⊢ 𝒟 = closure 𝒟ᵒ

Tactic:
refine subset_antisymm ?_ (isClosed_fd.closure_subset_iff.mpr fdo_subset_fd)

Premises used: Iff.mpr, ModularGroup.fdo_subset_fd, subset_antisymm, IsClosed.closure_subset_iff, ModularGroup.isClosed_fd
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
this : ∀ (hx : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑x : ℂ) : ℝ)) (hx' : |x.re| ≤ 1 / 2), x ∈ closure 𝒟ᵒ
⊢ x ∈ 𝒟 → x ∈ closure 𝒟ᵒ

Tactic:
⟨hx, hx'⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hx : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑x : ℂ) : ℝ)
hx' : |x.re| ≤ 1 / 2
⊢ 1 ≤ ‖(↑x : ℂ)‖

Tactic:
rw [one_le_normSq_iff] at hx

Premises used: Complex.one_le_normSq_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hx : LE.le (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑x : ℂ) : ℝ)
hx' : |x.re| ≤ 1 / 2
hx₁ : 1 ≤ ‖(↑x : ℂ)‖
⊢ |x.re| ≤ 1 / 2

Tactic:
rw [one_le_normSq_iff] at hx

Premises used: Complex.one_le_normSq_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hx : 1 ≤ ‖(↑x : ℂ)‖
hx' : |x.re| ≤ 1 / 2
inl : ∀ (hx : 1 < ‖(↑x : ℂ)‖), x ∈ closure 𝒟ᵒ
inr : ∀ (hx : 1 = ‖(↑x : ℂ)‖), x ∈ closure 𝒟ᵒ
⊢ x ∈ closure 𝒟ᵒ

Tactic:
rcases lt_or_eq_of_le hx with hx | hx

Premises used: lt_or_eq_of_le
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hx_1 : 1 ≤ ‖(↑x : ℂ)‖
hx' : |x.re| ≤ 1 / 2
hx : 1 < ‖(↑x : ℂ)‖
⊢ x ∈ closure 𝒟ᵒ

Tactic:
mem_closure_of_one_lt_norm hx hx'

Premises used: _private.0.ModularGroup.mem_closure_of_one_lt_norm
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hx_1 : 1 ≤ ‖(↑x : ℂ)‖
hx' : |x.re| ≤ 1 / 2
hx : 1 < ‖(↑x : ℂ)‖
⊢ x ∈ closure 𝒟ᵒ

Tactic:
exact mem_closure_of_one_lt_norm hx hx'

Premises used: _private.0.ModularGroup.mem_closure_of_one_lt_norm
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hx_1 : 1 ≤ ‖(↑x : ℂ)‖
hx' : |x.re| ≤ 1 / 2
hx : 1 = ‖(↑x : ℂ)‖
⊢ x ∈ closure 𝒟ᵒ

Tactic:
mem_closure_of_arc hx.symm hx'

Premises used: _private.0.ModularGroup.mem_closure_of_arc, Eq.symm
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hx_1 : 1 ≤ ‖(↑x : ℂ)‖
hx' : |x.re| ≤ 1 / 2
hx : 1 = ‖(↑x : ℂ)‖
⊢ x ∈ closure 𝒟ᵒ

Tactic:
exact mem_closure_of_arc hx.symm hx'

Premises used: _private.0.ModularGroup.mem_closure_of_arc, Eq.symm
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ 𝒟ᵒ = interior 𝒟

Tactic:
subset_antisymm (isOpen_fdo.subset_interior_iff.mpr fdo_subset_fd) ?_

Premises used: Iff.mpr, ModularGroup.fdo_subset_fd, IsOpen.subset_interior_iff, subset_antisymm, ModularGroup.isOpen_fdo
-- Module: Mathlib.NumberTheory.Modular
Goal:
refine : interior 𝒟 ⊆ 𝒟ᵒ
⊢ 𝒟ᵒ = interior 𝒟

Tactic:
refine subset_antisymm (isOpen_fdo.subset_interior_iff.mpr fdo_subset_fd) ?_

Premises used: Iff.mpr, ModularGroup.fdo_subset_fd, IsOpen.subset_interior_iff, subset_antisymm, ModularGroup.isOpen_fdo
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ UpperHalfPlane.re '' interior 𝒟 ⊆ interior (UpperHalfPlane.re '' 𝒟)

Tactic:
have ho1 := isOpenMap_re.image_interior_subset 𝒟
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : UpperHalfPlane.re '' interior 𝒟 ⊆ interior (UpperHalfPlane.re '' 𝒟)
⊢ Subset (α := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' interior 𝒟) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))

Tactic:
have ho2 := isOpenMap_norm.image_interior_subset 𝒟
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : UpperHalfPlane.re '' interior 𝒟 ⊆ interior (UpperHalfPlane.re '' 𝒟)
ho2 : Subset (α := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' interior 𝒟) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
rw :
  ∀ (ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟))
    (ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟)))
    ⦃x : ℍ⦄ (hx : x ∈ interior 𝒟), x ∈ 𝒟ᵒ
⊢ x ∈ 𝒟ᵒ

Tactic:
rw [Set.image_subset_iff] at *

Premises used: Set.image_subset_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
left : LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑x : ℂ) : ℝ)
right : |x.re| < 1 / 2
⊢ x ∈ 𝒟ᵒ

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
left : Membership.mem (γ := Set ℝ) (interior (Set.Ici 1)) ‖(↑x : ℂ)‖
⊢ LT.lt (α := ℝ) (1 : ℝ) ((normSq : (a : ℂ) → ℝ) (↑x : ℂ) : ℝ)

Tactic:
rw [one_lt_normSq_iff, ← Set.mem_Ioi, ← interior_Ici]

Premises used: interior_Ici, Set.mem_Ioi, Complex.one_lt_normSq_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
rw : 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (Set.Ici 1)
⊢ Subset (α := Set ℝ) ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟) (Set.Ici 1)

Tactic:
rw [Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
ξ : ℍ
hξ : ξ ∈ 𝒟
⊢ Membership.mem (γ := Set ℍ) (Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (Set.Ici 1)) ξ

Tactic:
simpa [Set.mem_preimage, Set.mem_Ici, one_le_normSq_iff] using hξ.1

Premises used: Complex.one_le_normSq_iff, And.left, Set.mem_Ici, Set.mem_preimage
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
right : x.re ∈ interior (Set.Icc (-(1 / 2)) (1 / 2))
⊢ |x.re| < 1 / 2

Tactic:
rw [abs_lt, ← Set.mem_Ioo, ← interior_Icc]

Premises used: Set.mem_Ioo, interior_Icc, abs_lt
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
apply : UpperHalfPlane.re '' 𝒟 ⊆ Set.Icc (-(1 / 2)) (1 / 2)
⊢ x.re ∈ interior (Set.Icc (-(1 / 2)) (1 / 2))

Tactic:
apply Set.mem_of_mem_of_subset ((Set.mem_preimage.mp (ho1 hx))) (interior_mono ?_)

Premises used: interior_mono, Set.mem_of_mem_of_subset, Iff.mp, Set.mem_preimage
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
rw : 𝒟 ⊆ UpperHalfPlane.re ⁻¹' Set.Icc (-(1 / 2)) (1 / 2)
⊢ UpperHalfPlane.re '' 𝒟 ⊆ Set.Icc (-(1 / 2)) (1 / 2)

Tactic:
rw [Set.image_subset_iff]

Premises used: Set.image_subset_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ Set.preimage (β := ℝ) (fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) (interior ((fun (τ : ℍ) ↦ ‖(↑τ : ℂ)‖) '' 𝒟))
x : ℍ
hx : x ∈ interior 𝒟
ξ : ℍ
hξ : ξ ∈ 𝒟
⊢ ξ ∈ UpperHalfPlane.re ⁻¹' Set.Icc (-(1 / 2)) (1 / 2)

Tactic:
simpa [Set.mem_preimage, Set.mem_Icc, abs_le] using hξ.2

Premises used: abs_le, And.right, Set.mem_Icc, Set.mem_preimage
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
h :
  ∀ (z : ℂ),
    z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y ↔
      Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
⊢ UpperHalfPlane.coe '' truncatedFundamentalDomain y = {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
ext z
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
h :
  z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y →
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z
h₁ :
  Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z →
    z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y ↔
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} z

Tactic:
constructor
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 < z.im
h : { coe := z, coe_im_pos := hz : ℍ } ∈ truncatedFundamentalDomain y
⊢ 1 ≤ ‖(↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ)‖

Tactic:
simpa [Complex.normSq_eq_norm_sq] using h.1.1

Premises used: Complex.normSq_eq_norm_sq, And.left
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 < z.im
h : { coe := z, coe_im_pos := hz : ℍ } ∈ truncatedFundamentalDomain y
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
    (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ)

Tactic:
exact ⟨hz.le, h.2, h.1.2, by simpa [Complex.normSq_eq_norm_sq] using h.1.1⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
apply : 0 ≠ z.im
⊢ 0 < z.im

Tactic:
apply hz.lt_of_ne

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
contrapose! : ∀ (h3 : 0 = z.im), ‖z‖ < 1
⊢ 0 ≠ z.im

Tactic:
contrapose! h3
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 0 = z.im
⊢ 1 / 2 < 1

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 0 = z.im
⊢ ‖z‖ < 1

Tactic:
simpa [← sq_lt_one_iff₀ (norm_nonneg _), ← Complex.normSq_eq_norm_sq, Complex.normSq,
        ← h3, ← sq] using h2.trans_lt (by norm_num)

Premises used: sq_lt_one_iff₀, Complex.normSq_eq_norm_sq, Complex.normSq, sq, LE.le.trans_lt, norm_nonneg
-- Module: Mathlib.NumberTheory.Modular
Goal:
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
⊢ 0 < z.im

Tactic:
have hz' : 0 < z.im := by
      apply hz.lt_of_ne
      contrapose! h3
      simpa [← sq_lt_one_iff₀ (norm_nonneg _), ← Complex.normSq_eq_norm_sq, Complex.normSq,
        ← h3, ← sq] using h2.trans_lt (by norm_num)