awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 ≤
        A
A' : ℝ
hA' :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A'
this_1 : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this_2 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this_3 :
  IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this :
  IsCompact (X := { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
    (Subtype.val (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) ⁻¹'
      {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }
hg : Membership.mem (γ := Set { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K) g
j : Fin 2
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ max √A √A'

Tactic:
le_trans ?_ <| le_max_right √A √A'

Premises used: le_max_right, Real.sqrt, le_trans
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 ≤
        A
A' : ℝ
hA' :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A'
this_1 : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this_2 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this_3 :
  IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this :
  IsCompact (X := { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
    (Subtype.val (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) ⁻¹'
      {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }
hg : Membership.mem (γ := Set { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K) g
j : Fin 2
1 : |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ √A'
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ max √A √A'

Tactic:
refine le_trans ?_ <| le_max_right √A √A'

Premises used: le_max_right, Real.sqrt, le_trans
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 ≤
        A
A' : ℝ
hA' :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A'
this_1 : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this_2 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this_3 :
  IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this :
  IsCompact (X := { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
    (Subtype.val (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) ⁻¹'
      {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }
hg : Membership.mem (γ := Set { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K) g
j : Fin 2
0 :
  HPow.hPow (β := ℕ)
      |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))|
      2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2
1 :
  HPow.hPow (β := ℕ)
      |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))|
      2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2
⊢ HPow.hPow (β := ℕ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| 2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2

Tactic:
fin_cases j
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 ≤
        A
A' : ℝ
hA' :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A'
this_1 : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this_2 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this_3 :
  IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this :
  IsCompact (X := { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
    (Subtype.val (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) ⁻¹'
      {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }
hg : Membership.mem (γ := Set { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K) g
⊢ HPow.hPow (β := ℕ)
      |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))|
      2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2

Tactic:
simp [sq_nonneg]

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 ≤
        A
A' : ℝ
hA' :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A'
this_1 : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this_2 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this_3 :
  IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this :
  IsCompact (X := { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
    (Subtype.val (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) ⁻¹'
      {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }
hg : Membership.mem (γ := Set { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K) g
⊢ HPow.hPow (β := ℕ)
      |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))|
      2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2

Tactic:
simp [sq_nonneg]

Premises used: sq_nonneg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 ≤
        A
A' : ℝ
hA' :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A'
this_1 : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this_2 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this_3 :
  IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this :
  IsCompact (X := { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
    (Subtype.val (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) ⁻¹'
      {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
g : { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }
hg : Membership.mem (γ := Set { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 }) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K) g
j : Fin 2
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ √A'

Tactic:
exact Real.le_sqrt_of_sq_le <| le_trans (by fin_cases j <;> simp [sq_nonneg]) (hA' g hg)

Premises used: Real.le_sqrt_of_sq_le, le_trans
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
⊢ ProperSMul SL(2, ℝ) ℍ

Tactic:
MulAction.properSMul_of_proper_orbitMap isProperMap_smul_I

Premises used: MulAction.properSMul_of_proper_orbitMap, UpperHalfPlane.isProperMap_smul_I
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
𝒢 : Subgroup SL(2, ℝ)
inst : DiscreteTopology ↥𝒢
⊢ IsClosed (↑𝒢 : Set SL(2, ℝ))

Tactic:
have : IsClosed (𝒢 : Set SL(2, ℝ)) := Subgroup.isClosed_of_discrete
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
𝒢 : Subgroup SL(2, ℝ)
inst : DiscreteTopology ↥𝒢
this : IsClosed (↑𝒢 : Set SL(2, ℝ))
rw : ProperSMul ↥𝒢 ℍ
⊢ ProperlyDiscontinuousSMul ↥𝒢 ℍ

Tactic:
rw [properlyDiscontinuousSMul_iff_properSMul]

Premises used: properlyDiscontinuousSMul_iff_properSMul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
𝒢 : Subgroup SL(2, ℝ)
inst : DiscreteTopology ↥𝒢
this : IsClosed (↑𝒢 : Set SL(2, ℝ))
⊢ ProperSMul ↥𝒢 ℍ

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ IsEmbedding UpperHalfPlane.coe

Tactic:
coe_injective.isEmbedding_induced

Premises used: UpperHalfPlane.coe_injective, Function.Injective.isEmbedding_induced
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ IsOpen (range UpperHalfPlane.coe)

Tactic:
simp [isOpen_upperHalfPlaneSet]

Premises used: UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ Continuous UpperHalfPlane.coe

Tactic:
isEmbedding_coe.continuous

Premises used: UpperHalfPlane.isEmbedding_coe, Topology.IsEmbedding.continuous
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ Continuous re

Tactic:
Complex.continuous_re.comp continuous_coe

Premises used: Complex.continuous_re, Continuous.comp, UpperHalfPlane.re, UpperHalfPlane.continuous_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ Continuous im

Tactic:
Complex.continuous_im.comp continuous_coe

Premises used: Continuous.comp, UpperHalfPlane.im, UpperHalfPlane.continuous_coe, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
X : Type u_1
inst : TopologicalSpace X
f : X → ℂ
hf : Continuous[inst, _] f
hf₀ : ∀ (x : X), 0 < (f x).im
⊢ Continuous[inst, _] fun (x : X) ↦ { coe := f x, coe_im_pos := ⋯ }

Tactic:
isEmbedding_coe.continuous_iff.mpr hf

Premises used: Iff.mpr, Topology.IsEmbedding.continuous_iff, UpperHalfPlane.isEmbedding_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ SecondCountableTopology ℍ

Tactic:
secondCountableTopology_induced ..

Premises used: TopologicalSpace.secondCountableTopology_induced
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ T3Space ℍ

Tactic:
isEmbedding_coe.t3Space

Premises used: Topology.IsEmbedding.t3Space, UpperHalfPlane.isEmbedding_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ T4Space ℍ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
rw : ContractibleSpace (↑upperHalfPlaneSet : Type)
⊢ ContractibleSpace ℍ

Tactic:
rw [isEmbedding_coe.toHomeomorph.trans (.setCongr range_coe) |>.contractibleSpace_iff]

Premises used: Homeomorph.contractibleSpace_iff, Homeomorph.trans, Homeomorph.setCongr, UpperHalfPlane.range_coe, UpperHalfPlane.isEmbedding_coe, Topology.IsEmbedding.toHomeomorph
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ ContractibleSpace (↑upperHalfPlaneSet : Type)

Tactic:
(convex_halfSpace_im_gt 0).contractibleSpace ⟨I, one_pos.trans_eq I_im.symm⟩

Premises used: UpperHalfPlane.coe, Set.Mem, convex_halfSpace_im_gt, Convex.contractibleSpace, LT.lt.trans_eq, Exists.intro, UpperHalfPlane.I, UpperHalfPlane.I_im, OfNat.ofNat, Eq.symm, one_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ ContractibleSpace (↑upperHalfPlaneSet : Type)

Tactic:
exact (convex_halfSpace_im_gt 0).contractibleSpace ⟨I, one_pos.trans_eq I_im.symm⟩

Premises used: UpperHalfPlane.coe, convex_halfSpace_im_gt, Convex.contractibleSpace, LT.lt.trans_eq, Exists.intro, UpperHalfPlane.I, UpperHalfPlane.I_im, OfNat.ofNat, Eq.symm, one_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ LocPathConnectedSpace ℍ

Tactic:
isOpenEmbedding_coe.locPathConnectedSpace

Premises used: UpperHalfPlane.isOpenEmbedding_coe, Topology.IsOpenEmbedding.locPathConnectedSpace
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
h : IsCompact (X := ℍ) univ
⊢ IsCompact (Complex.im ⁻¹' Ioi 0)

Tactic:
simpa [isEmbedding_coe.isCompact_iff] using h

Premises used: Topology.IsEmbedding.isCompact_iff, UpperHalfPlane.isEmbedding_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
h : IsCompact (X := ℍ) univ
⊢ IsCompact (Complex.im ⁻¹' Ioi 0)

Tactic:
have : IsCompact (Complex.im ⁻¹' Ioi 0) := by
      simpa [isEmbedding_coe.isCompact_iff] using h
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
h : IsCompact (X := ℍ) univ
this : IsCompact (Complex.im ⁻¹' Ioi 0)
⊢ False

Tactic:
simpa [closure_preimage_im] using congr(0 ∈ $this.isClosed.closure_eq)

Premises used: Complex.closure_preimage_im, IsClosed.closure_eq, IsCompact.isClosed
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
⊢ LocallyCompactSpace ℍ

Tactic:
isOpenEmbedding_coe.locallyCompactSpace

Premises used: UpperHalfPlane.isOpenEmbedding_coe, Topology.IsOpenEmbedding.locallyCompactSpace
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
simp_rw :
  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 : ℂ))
⊢ Continuous (Y := ℍ) fun (x : ℍ) ↦ g • x

Tactic:
simp_rw [continuous_induced_rng (f := UpperHalfPlane.coe), Function.comp_def,
      UpperHalfPlane.coe_smul, UpperHalfPlane.σ]

Premises used: UpperHalfPlane.coe_smul, Function.comp_def, UpperHalfPlane.σ, continuous_induced_rng
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
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 : ℂ))

Tactic:
.comp ?_ ?_

Premises used: Continuous.comp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
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 : ℂ) → ℂ)
refine_2 : Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ) / denom g (↑x : ℂ)
⊢ 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 : ℂ))

Tactic:
refine .comp ?_ ?_
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
pos :
  LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    Continuous (X := ℂ) (Y := ℂ) (⇑(ContinuousAlgEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)
neg :
  ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    Continuous (X := ℂ) (Y := ℂ) (⇑conjCAE : (a : ℂ) → ℂ)
⊢ Continuous (X := ℂ) (Y := ℂ)
    (⇑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
          ContinuousAlgEquiv.refl ℝ ℂ
        else conjCAE) :
      (a : ℂ) → ℂ)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
h : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ Continuous (X := ℂ) (Y := ℂ) (⇑(ContinuousAlgEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)

Tactic:
continuous_id

Premises used: continuous_id
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
h : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ Continuous (X := ℂ) (Y := ℂ) (⇑conjCAE : (a : ℂ) → ℂ)

Tactic:
continuous_conj

Premises used: Complex.continuous_conj
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
h : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ Continuous (X := ℂ) (Y := ℂ) (⇑(ContinuousAlgEquiv.refl ℝ ℂ) : (a : ℂ) → ℂ)

Tactic:
exacts [continuous_id, continuous_conj]

Premises used: Complex.continuous_conj, continuous_id
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ) / denom g (↑x : ℂ)

Tactic:
.div ?_ ?_ (fun x ↦ denom_ne_zero g x)

Premises used: Continuous.div, UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
refine_2 : Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ)
refine_2₁ : Continuous (Y := ℂ) fun (x : ℍ) ↦ denom g (↑x : ℂ)
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ) / denom g (↑x : ℂ)

Tactic:
refine .div ?_ ?_ (fun x ↦ denom_ne_zero g x)
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ)

Tactic:
(continuous_const.mul continuous_coe).add continuous_const

Premises used: continuous_const, Continuous.mul, UpperHalfPlane.num, Continuous.add, UpperHalfPlane.continuous_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦ num g (↑x : ℂ)

Tactic:
exact (continuous_const.mul continuous_coe).add continuous_const

Premises used: continuous_const, Continuous.mul, Continuous.add, UpperHalfPlane.continuous_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦ denom g (↑x : ℂ)

Tactic:
(continuous_const.mul continuous_coe).add continuous_const

Premises used: continuous_const, Continuous.mul, UpperHalfPlane.denom, Continuous.add, UpperHalfPlane.continuous_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (Y := ℂ) fun (x : ℍ) ↦ denom g (↑x : ℂ)

Tactic:
exact (continuous_const.mul continuous_coe).add continuous_const

Premises used: continuous_const, Continuous.mul, Continuous.add, UpperHalfPlane.continuous_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
A B : ℝ
z : ℍ
⊢ z ∈ verticalStrip A B ↔ |z.re| ≤ A ∧ B ≤ z.im

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, UpperHalfPlane.verticalStrip
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
A B A' B' : ℝ
hA : A ≤ A'
hB : B' ≤ B
z : ℍ
hzre : |z.re| ≤ A
hzim : B ≤ z.im
⊢ z ∈ verticalStrip A' B'

Tactic:
⟨hzre.trans hA, hB.trans hzim⟩

Premises used: Set.Mem, setOf, UpperHalfPlane.verticalStrip, And.intro, LE.le.trans
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
A B A' B' : ℝ
hA : A ≤ A'
hB : B' ≤ B
z : ℍ
hzre : |z.re| ≤ A
hzim : B ≤ z.im
⊢ z ∈ verticalStrip A' B'

Tactic:
exact ⟨hzre.trans hA, hB.trans hzim⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
A A' : ℝ
h : A ≤ A'
B : ℝ
⊢ verticalStrip A B ⊆ verticalStrip A' B

Tactic:
verticalStrip_mono h le_rfl

Premises used: le_rfl, UpperHalfPlane.verticalStrip_mono
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
A B B' : ℝ
h : B' ≤ B
⊢ verticalStrip A B ⊆ verticalStrip A B'

Tactic:
verticalStrip_mono le_rfl h

Premises used: le_rfl, UpperHalfPlane.verticalStrip_mono
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
K : Set ℍ
hK : IsCompact K
inl : ∀ (hK : IsCompact (X := ℍ) ∅), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ ∅ ⊆ verticalStrip A B
inr : ∀ (hne : K.Nonempty), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
rcases K.eq_empty_or_nonempty with rfl | hne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
hK : IsCompact (X := ℍ) ∅
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ ∅ ⊆ verticalStrip A B

Tactic:
⟨1, 1, Real.zero_lt_one, empty_subset _⟩

Premises used: Real.zero_lt_one, And.intro, Set.empty_subset, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
hK : IsCompact (X := ℍ) ∅
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ ∅ ⊆ verticalStrip A B

Tactic:
exact ⟨1, 1, Real.zero_lt_one, empty_subset _⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
inr : ∀ u ∈ K, ∀ (hu : IsMaxOn (abs ∘ re) K u), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
obtain ⟨u, _, hu⟩ := hK.exists_isMaxOn hne (_root_.continuous_abs.comp continuous_re).continuousOn

Premises used: Continuous.continuousOn, Continuous.comp, continuous_abs, IsCompact.exists_isMaxOn, UpperHalfPlane.continuous_re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
u : ℍ
left : u ∈ K
hu : IsMaxOn (abs ∘ re) K u
inr : ∀ v ∈ K, ∀ (hv : IsMinOn im K v), ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
obtain ⟨v, _, hv⟩ := hK.exists_isMinOn hne continuous_im.continuousOn

Premises used: Continuous.continuousOn, IsCompact.exists_isMinOn, UpperHalfPlane.continuous_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
u : ℍ
left : u ∈ K
hu : IsMaxOn (abs ∘ re) K u
v : ℍ
left_1 : v ∈ K
hv : IsMinOn im K v
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
⟨|re u|, im v, v.im_pos, fun k hk ↦ ⟨isMaxOn_iff.mp hu _ hk, isMinOn_iff.mp hv _ hk⟩⟩

Premises used: UpperHalfPlane.im_pos, abs, isMaxOn_iff, UpperHalfPlane.im, And.intro, Exists.intro, Iff.mp, isMinOn_iff, UpperHalfPlane.re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
u : ℍ
left : u ∈ K
hu : IsMaxOn (abs ∘ re) K u
v : ℍ
left_1 : v ∈ K
hv : IsMinOn im K v
⊢ ∃ (A : ℝ) (B : ℝ), 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
exact ⟨|re u|, im v, v.im_pos, fun k hk ↦ ⟨isMaxOn_iff.mp hu _ hk, isMinOn_iff.mp hv _ hk⟩⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology
Goal:
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / (↑N : ℝ)⌋
h : ModularGroup.T ^ ((↑N : ℤ) * -n) • z ∈ verticalStrip (↑N : ℝ) z.im
⊢ ∃ (n : ℤ), ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im

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

Tactic:
rw [modular_T_zpow_smul z (N * -n)]

Premises used: HMul.hMul, Nat.cast, UpperHalfPlane.modular_T_zpow_smul, Neg.neg