awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
⊢ g ≠ T * S * T ∧ g ≠ -(T * S * T)

Tactic:
have neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T) := by
      have : (T * S * T) • ρ ≠ ρ := by
        simp only [mul_smul, modular_T_smul, modular_S_smul,
          ne_eq, UpperHalfPlane.ext_iff, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow, normSq]
      grind [SL_neg_smul]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T)
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ ρ.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ ρ.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖(↑ρ : ℂ)‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ ρ = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ ρ = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ ρ = ρ

Tactic:
have := cases_of_mem_fd_smul_mem_fd ρ_mem_fd (hg ▸ ρ_mem_fd)
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T)
this :
  (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ ρ.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ ρ.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖(↑ρ : ℂ)‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ ρ = HVAdd.hVAdd (α := ℝ) 1 ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ ρ = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ ρ = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ ρ = ρ
⊢ (g = 1 ∨ g = -1) ∨ (g = S * T ∨ g = -(S * T)) ∨ g = T⁻¹ * S ∨ g = -(T⁻¹ * S)

Tactic:
norm_num [UpperHalfPlane.ext_iff, Complex.ext_iff, norm_ρ, ρ, neS, neT, neTST] at this

Premises used: UpperHalfPlane.ρ, UpperHalfPlane.ext_iff, UpperHalfPlane.norm_ρ, Complex.ext_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T)
this : (g = 1 ∨ g = -1) ∨ (g = S * T ∨ g = -(S * T)) ∨ g = T⁻¹ * S ∨ g = -(T⁻¹ * S)
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g

Tactic:
grind
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
this : (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g → g • ρ = ρ

Tactic:
simp +contextual [-sl_moeb, or_imp, this]

Premises used: ModularGroup.sl_moeb, or_imp
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
mpr : (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ
⊢ Membership.mem (γ := Finset SL(2, ℤ)) {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} g → g • ρ = ρ

Tactic:
suffices (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ by simp +contextual [-sl_moeb, or_imp, this]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
mpr : (↑ρ : ℂ) = (↑{ coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := ⋯ } : ℂ)
⊢ (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ

Tactic:
rw [mul_smul T⁻¹, inv_smul_eq_iff, ← eq_inv_smul_iff (g := S), S_inv, SL_neg_smul,
      mul_smul, eq_comm, and_self, modular_T_smul, modular_S_smul, UpperHalfPlane.ext_iff]

Premises used: inv_smul_eq_iff, and_self, UpperHalfPlane.ext_iff, ModularGroup.S_inv, ModularGroup.T, UpperHalfPlane.modular_S_smul, eq_comm, Inv.inv, ModularGroup.SL_neg_smul, SemigroupAction.mul_smul, UpperHalfPlane.modular_T_smul, eq_inv_smul_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
⊢ (↑ρ : ℂ) = (↑{ coe := (-(↑(HVAdd.hVAdd (α := ℝ) 1 ρ) : ℂ))⁻¹, coe_im_pos := ⋯ } : ℂ)

Tactic:
norm_num [ρ, Complex.ext_iff, normSq, ← pow_two, div_pow]

Premises used: pow_two, UpperHalfPlane.ρ, Complex.normSq, Complex.ext_iff, div_pow
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
h : ρ ∈ 𝒟ᵒ
⊢ False

Tactic:
grind [norm_ρ, one_lt_normSq_iff.mp h.1]

Premises used: UpperHalfPlane.norm_ρ, And.left, Iff.mp, Complex.one_lt_normSq_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
⊢ ρ ∉ 𝒟ᵒ

Tactic:
have : ρ ∉ 𝒟ᵒ := by
    intro h
    grind [norm_ρ, one_lt_normSq_iff.mp h.1]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
h : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟ᵒ
⊢ (HVAdd.hVAdd (α := ℝ) 1 ρ).re = 1 / 2

Tactic:
norm_num [← coe_re, coe_vadd, ρ]

Premises used: UpperHalfPlane.ρ, UpperHalfPlane.coe_vadd, UpperHalfPlane.coe_re
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
h : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟ᵒ
⊢ (HVAdd.hVAdd (α := ℝ) 1 ρ).re = 1 / 2

Tactic:
have : ((1 : ℝ) +ᵥ ρ).re = 1 / 2 := by norm_num [← coe_re, coe_vadd, ρ]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this_1 : ρ ∉ 𝒟ᵒ
h : HVAdd.hVAdd (α := ℝ) 1 ρ ∈ 𝒟ᵒ
this : (HVAdd.hVAdd (α := ℝ) 1 ρ).re = 1 / 2
⊢ False

Tactic:
grind [h.2]

Premises used: And.right
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
⊢ HVAdd.hVAdd (α := ℝ) 1 ρ ∉ 𝒟ᵒ

Tactic:
have : (1 : ℝ) +ᵥ ρ ∉ 𝒟ᵒ := by
    intro h
    have : ((1 : ℝ) +ᵥ ρ).re = 1 / 2 := by norm_num [← coe_re, coe_vadd, ρ]
    grind [h.2]
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this_1 : ρ ∉ 𝒟ᵒ
this : HVAdd.hVAdd (α := ℝ) 1 ρ ∉ 𝒟ᵒ
⊢ g = 1 ∨ g = -1

Tactic:
grind [one_lt_normSq_iff, hz.1, hz.2, cases_of_mem_fd_smul_mem_fd (fdo_subset_fd hz) hg]

Premises used: ModularGroup.fdo_subset_fd, ModularGroup.cases_of_mem_fd_smul_mem_fd, And.right, And.left, Complex.one_lt_normSq_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ g = 1 ∨ g = -1

Tactic:
eq_one_or_neg_one_of_mem_fdo_mem_fd hz (fdo_subset_fd hg)

Premises used: ModularGroup.fdo_subset_fd, ModularGroup.eq_one_or_neg_one_of_mem_fdo_mem_fd
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
inl : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟ᵒ), Eq (α := ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0
inr : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟ᵒ), Eq (α := ℤ) ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0
⊢ (↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 0

Tactic:
rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl

Premises used: ModularGroup.eq_one_or_neg_one_of_mem_fdo_mem_fdo, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟ᵒ
⊢ Eq (α := ℤ) ((↑1 : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟ᵒ
⊢ Eq (α := ℤ) ((↑(-1) : Matrix (Fin 2) (Fin 2) ℤ) 1 0) 0

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
inl : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟ᵒ), z = HSMul.hSMul (α := SL(2, ℤ)) 1 z
inr : ∀ (hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟ᵒ), z = HSMul.hSMul (α := SL(2, ℤ)) (-1) z
⊢ z = g • z

Tactic:
rcases eq_one_or_neg_one_of_mem_fdo_mem_fdo hz hg with rfl | rfl

Premises used: ModularGroup.eq_one_or_neg_one_of_mem_fdo_mem_fdo, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : HSMul.hSMul (α := SL(2, ℤ)) 1 z ∈ 𝒟ᵒ
⊢ z = HSMul.hSMul (α := SL(2, ℤ)) 1 z

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : HSMul.hSMul (α := SL(2, ℤ)) (-1) z ∈ 𝒟ᵒ
⊢ z = HSMul.hSMul (α := SL(2, ℤ)) (-1) z

Tactic:
simp
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ Continuous (Y := ℝ) fun (z : ℍ) ↦ (normSq : (a : ℂ) → ℝ) (↑z : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Modular
Goal:
refine : IsClosed (X := ℍ) fun (z : ℍ) ↦ Real.le✝ |z.re| (1 / 2)
⊢ IsClosed 𝒟

Tactic:
refine .inter (.preimage (by fun_prop) isClosed_Ici) ?_
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ Continuous (Y := ℝ) fun (z : ℍ) ↦ |z.re|

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℍ) fun (z : ℍ) ↦ Real.le✝ |z.re| (1 / 2)

Tactic:
exact isClosed_le (f := fun z : ℍ ↦ |z.re|) (by fun_prop) continuous_const

Premises used: continuous_const, isClosed_le
-- Module: Mathlib.NumberTheory.Modular
Goal:
refine : IsOpen (X := ℍ) fun (z : ℍ) ↦ Real.lt✝ |z.re| (1 / 2)
⊢ IsOpen 𝒟ᵒ

Tactic:
refine .inter (.preimage (by fun_prop) isOpen_Ioi) ?_
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsOpen (X := ℍ) fun (z : ℍ) ↦ Real.lt✝ |z.re| (1 / 2)

Tactic:
exact isOpen_lt (f := fun z : ℍ ↦ |z.re|) (by fun_prop) continuous_const

Premises used: isOpen_lt, continuous_const
-- Module: Mathlib.NumberTheory.Modular
Goal:
h :
  ∀ (x : ℂ), x ∈ UpperHalfPlane.coe '' 𝒟ᵒ ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} x
⊢ UpperHalfPlane.coe '' 𝒟ᵒ = {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2}

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℂ
⊢ x ∈ UpperHalfPlane.coe '' 𝒟ᵒ ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} x

Tactic:
⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_lt_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩

Premises used: Iff.mpr, UpperHalfPlane.coe, ModularGroup.fdo, _private.0.ModularGroup.coe_fdo.match_1, Membership.mem, UpperHalfPlane.mk, And.intro, Iff.intro, Exists.intro, Complex.one_lt_normSq_iff, Set.image, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℂ
h : x ∈ UpperHalfPlane.coe '' 𝒟ᵒ → Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} x
⊢ x ∈ UpperHalfPlane.coe '' 𝒟ᵒ ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} x

Tactic:
refine ⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_lt_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
hτ : τ ∈ 𝒟ᵒ
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} (↑τ : ℂ)

Tactic:
⟨τ.im_pos, one_lt_normSq_iff.mp hτ.1, hτ.2⟩

Premises used: UpperHalfPlane.im_pos, Set.Mem, setOf, And.right, And.left, And.intro, Iff.mp, Complex.one_lt_normSq_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
hτ : τ ∈ 𝒟ᵒ
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 < ‖z‖ ∧ |z.re| < 1 / 2} (↑τ : ℂ)

Tactic:
exact ⟨τ.im_pos, one_lt_normSq_iff.mp hτ.1, hτ.2⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
h : ∀ (x : ℂ), x ∈ UpperHalfPlane.coe '' 𝒟 ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x
⊢ UpperHalfPlane.coe '' 𝒟 = {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

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

Tactic:
⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_le_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩

Premises used: Iff.mpr, Complex.one_le_normSq_iff, UpperHalfPlane.coe, Membership.mem, UpperHalfPlane.mk, And.intro, Iff.intro, Exists.intro, Set.image, ModularGroup.fd, _private.0.ModularGroup.coe_fd.match_1, rfl
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℂ
h : x ∈ UpperHalfPlane.coe '' 𝒟 → Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x
⊢ x ∈ UpperHalfPlane.coe '' 𝒟 ↔ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x

Tactic:
refine ⟨?_, fun ⟨hxim, hxnorm, hxre⟩ ↦ ⟨⟨x, hxim⟩, ⟨one_le_normSq_iff.mpr hxnorm, hxre⟩, rfl⟩⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
hτ : τ ∈ 𝒟
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} (↑τ : ℂ)

Tactic:
⟨τ.im_pos, one_le_normSq_iff.mp hτ.1, hτ.2⟩

Premises used: Complex.one_le_normSq_iff, UpperHalfPlane.im_pos, Set.Mem, setOf, And.right, And.left, And.intro, Iff.mp
-- Module: Mathlib.NumberTheory.Modular
Goal:
τ : ℍ
hτ : τ ∈ 𝒟
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} (↑τ : ℂ)

Tactic:
exact ⟨τ.im_pos, one_le_normSq_iff.mp hτ.1, hτ.2⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
rw : IsClosed (X := ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
⊢ IsClosed (UpperHalfPlane.coe '' 𝒟)

Tactic:
rw [coe_fd]

Premises used: ModularGroup.coe_fd
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
.inter ?_ (.inter ?_ ?_)

Premises used: Set.Mem, setOf, Set.inter, IsClosed.inter
-- Module: Mathlib.NumberTheory.Modular
Goal:
refine_1 : IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 0 z.im
refine_2 : IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 1 ‖z‖
refine_3 : IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ |z.re| (1 / 2)
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
refine .inter ?_ (.inter ?_ ?_)
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 0 z.im

Tactic:
isClosed_le continuous_const Complex.continuous_im

Premises used: continuous_const, isClosed_le, Complex.continuous_im
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 0 z.im

Tactic:
exact isClosed_le continuous_const Complex.continuous_im

Premises used: continuous_const, isClosed_le, Complex.continuous_im
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 1 ‖z‖

Tactic:
isClosed_le continuous_const continuous_norm

Premises used: continuous_const, isClosed_le, continuous_norm
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ 1 ‖z‖

Tactic:
exact isClosed_le continuous_const continuous_norm

Premises used: continuous_const, isClosed_le, continuous_norm
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ |z.re| (1 / 2)

Tactic:
isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const

Premises used: abs, Complex.continuous_re, Continuous.comp, continuous_const, isClosed_le, continuous_abs
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℂ) fun (z : ℂ) ↦ Real.le✝ |z.re| (1 / 2)

Tactic:
exact isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const

Premises used: Complex.continuous_re, Continuous.comp, continuous_const, isClosed_le, continuous_abs
-- Module: Mathlib.NumberTheory.Modular
Goal:
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
have : IsClosed {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1/2} := by
    refine .inter ?_ (.inter ?_ ?_)
    · exact isClosed_le continuous_const Complex.continuous_im
    · exact isClosed_le continuous_const continuous_norm
    · exact isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const
-- Module: Mathlib.NumberTheory.Modular
Goal:
this : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
⊢ IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
this
-- Module: Mathlib.NumberTheory.Modular
Goal:
this : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
h : Eq (α := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
⊢ IsClosed (X := ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
convert! this using 1
-- Module: Mathlib.NumberTheory.Modular
Goal:
this : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
h :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x ↔
      Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x
⊢ Eq (α := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
ext x
-- Module: Mathlib.NumberTheory.Modular
Goal:
this : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
x : ℂ
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x ↔
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x

Tactic:
⟨fun ⟨him, hre, hnorm⟩ ↦ ⟨him.le, hre, hnorm⟩, fun ⟨him, hre, hnorm⟩ ↦ ⟨?_, hre, hnorm⟩⟩

Premises used: Norm.norm, abs, _private.0.ModularGroup.isClosed_coe_fd.match_1, Complex.im, setOf, Membership.mem, HDiv.hDiv, LT.lt.le, LE.le, Complex.re, And, And.intro, LT.lt, Iff.intro, OfNat.ofNat, _private.0.ModularGroup.coe_fd.match_1
-- Module: Mathlib.NumberTheory.Modular
Goal:
this : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
x : ℂ
h :
  Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x →
    ∀ (him : 0 ≤ x.im) (hre : 1 ≤ ‖x‖) (hnorm : |x.re| ≤ 1 / 2), 0 < x.im
⊢ Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x ↔
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x

Tactic:
refine ⟨fun ⟨him, hre, hnorm⟩ ↦ ⟨him.le, hre, hnorm⟩, fun ⟨him, hre, hnorm⟩ ↦ ⟨?_, hre, hnorm⟩⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
this : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
x : ℂ
h : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x
him : 0 ≤ x.im
hre : 1 ≤ ‖x‖
hnorm : |x.re| ≤ 1 / 2
⊢ x.im ≠ 0

Tactic:
grind [abs_re_eq_norm]

Premises used: Complex.abs_re_eq_norm
-- Module: Mathlib.NumberTheory.Modular
Goal:
this : IsClosed (X := ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}
x : ℂ
h : Membership.mem (γ := Set ℂ) {z : ℂ | 0 ≤ z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2} x
him : 0 ≤ x.im
hre : 1 ≤ ‖x‖
hnorm : |x.re| ≤ 1 / 2
⊢ 0 < x.im

Tactic:
exact him.lt_of_ne' <| by grind [abs_re_eq_norm]

Premises used: LE.le.lt_of_ne'
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
h : ∃ᶠ (x_1 : ℝ) in 𝓝[<] 1, (↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ)) ∈ 𝒟ᵒ
hf : Filter.Tendsto (fun (t : ℝ) ↦ (↑ofComplex : ℂ → ℍ) ((↑t : ℂ) * (↑x : ℂ))) (𝓝[<] 1) (𝓝 x)
⊢ x ∈ closure 𝒟ᵒ

Tactic:
apply mem_closure_of_frequently_of_tendsto (α := ℝ)
      (b := 𝓝[<] 1) (f := fun t ↦ ofComplex (t * x))

Premises used: mem_closure_of_frequently_of_tendsto
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
h : ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, (↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ)) ∈ 𝒟ᵒ
⊢ ∃ᶠ (x_1 : ℝ) in 𝓝[<] 1, (↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ)) ∈ 𝒟ᵒ

Tactic:
apply Filter.Eventually.frequently

Premises used: Filter.Eventually.frequently
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
h :
  (∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, 1 < ‖(↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)‖) ∧
    ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))).re| < 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, (↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ)) ∈ 𝒟ᵒ

Tactic:
simp only [fdo, Set.mem_setOf, Filter.eventually_and, one_lt_normSq_iff]

Premises used: Filter.eventually_and, ModularGroup.fdo, Set.mem_setOf, Complex.one_lt_normSq_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ (∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, 1 < ‖(↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)‖) ∧
    ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))).re| < 1 / 2

Tactic:
⟨Filter.Tendsto.eventually_const_lt hxnorm (.mono_left ?_ nhdsWithin_le_nhds), ?_⟩

Premises used: Filter.Tendsto.eventually_const_lt, nhdsWithin_le_nhds, And.intro, Filter.Tendsto.mono_left
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
h : Filter.Tendsto (fun (x_1 : ℝ) ↦ ‖(↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)‖) (𝓝 1) (𝓝 ‖(↑x : ℂ)‖)
h₁ : ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))).re| < 1 / 2
⊢ (∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, 1 < ‖(↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)‖) ∧
    ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))).re| < 1 / 2

Tactic:
refine ⟨Filter.Tendsto.eventually_const_lt hxnorm (.mono_left ?_ nhdsWithin_le_nhds), ?_⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ ContinuousAt UpperHalfPlane.coe ((↑ofComplex : ℂ → ℍ) ((↑1 : ℂ) * (↑x : ℂ)))

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ ContinuousAt (Y := ℂ) (fun (a : ℝ) ↦ (↑a : ℂ) * (↑x : ℂ)) 1

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
refine : (↑1 : ℂ) * (↑x : ℂ) ∈ ofComplex.source
⊢ ContinuousAt (Y := ℂ) (fun (a : ℝ) ↦ (↑((↑ofComplex : ℂ → ℍ) ((↑a : ℂ) * (↑x : ℂ))) : ℂ)) 1

Tactic:
refine .comp (by fun_prop) ((OpenPartialHomeomorph.continuousAt _ ?_).comp (by fun_prop))
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ (↑1 : ℂ) * (↑x : ℂ) ∈ ofComplex.source

Tactic:
simpa [ofComplex] using x.coe_im_pos

Premises used: UpperHalfPlane.ofComplex, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
⊢ ContinuousAt (Y := ℂ) (fun (a : ℝ) ↦ (↑((↑ofComplex : ℂ → ℍ) ((↑a : ℂ) * (↑x : ℂ))) : ℂ)) 1

Tactic:
have : ContinuousAt (fun a : ℝ ↦ (ofComplex (a * x : ℂ) : ℂ)) 1 := by
        refine .comp (by fun_prop) ((OpenPartialHomeomorph.continuousAt _ ?_).comp (by fun_prop))
        simpa [ofComplex] using x.coe_im_pos
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
this : ContinuousAt (Y := ℂ) (fun (a : ℝ) ↦ (↑((↑ofComplex : ℂ → ℍ) ((↑a : ℂ) * (↑x : ℂ))) : ℂ)) 1
⊢ Filter.Tendsto (fun (x_1 : ℝ) ↦ ‖(↑((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))) : ℂ)‖) (𝓝 1) (𝓝 ‖(↑x : ℂ)‖)

Tactic:
simpa [ofComplex_apply_of_im_pos x.coe_im_pos] using this.tendsto.norm

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos, Filter.Tendsto.norm, ContinuousAt.tendsto, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
h :
  ∀ᶠ (x_1 : ℝ) in 𝓝 1,
    Membership.mem (γ := Set ℝ) (Set.Iio 1) x_1 → |((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))).re| < 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝[<] 1, |((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))).re| < 1 / 2

Tactic:
simp only [eventually_nhdsWithin_iff]

Premises used: eventually_nhdsWithin_iff
-- Module: Mathlib.NumberTheory.Modular
Goal:
x : ℍ
hxnorm : 1 < ‖(↑x : ℂ)‖
hxre : |x.re| ≤ 1 / 2
h :
  ∀ (a : ℝ) (ha : 0 < a) (ha' : Membership.mem (γ := Set ℝ) (Set.Iio 1) a),
    |((↑ofComplex : ℂ → ℍ) ((↑a : ℂ) * (↑x : ℂ))).re| < 1 / 2
⊢ ∀ᶠ (x_1 : ℝ) in 𝓝 1,
    Membership.mem (γ := Set ℝ) (Set.Iio 1) x_1 → |((↑ofComplex : ℂ → ℍ) ((↑x_1 : ℂ) * (↑x : ℂ))).re| < 1 / 2

Tactic:
filter_upwards [eventually_gt_nhds zero_lt_one] with a ha ha'

Premises used: eventually_gt_nhds, zero_lt_one
-- 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
⊢ 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
a : ℝ
ha : 0 < a
ha' : Membership.mem (γ := Set ℝ) (Set.Iio 1) a
h : |(↑{ coe := (↑a : ℂ) * (↑x : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ).re| < 1 / 2
⊢ |((↑ofComplex : ℂ → ℍ) ((↑a : ℂ) * (↑x : ℂ))).re| < 1 / 2

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

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos, UpperHalfPlane.coe_re
-- 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
this : a * |x.re| < 1 / 2
⊢ |(↑{ coe := (↑a : ℂ) * (↑x : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ).re| < 1 / 2

Tactic:
simpa [abs_of_pos ha]

Premises used: abs_of_pos
-- 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
h : a * |x.re| < 1 / 2
⊢ |(↑{ coe := (↑a : ℂ) * (↑x : ℂ), coe_im_pos := ⋯ : ℍ } : ℂ).re| < 1 / 2

Tactic:
suffices a * |x.re| < 1 / 2 by simpa [abs_of_pos ha]