awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ Continuous (Y := ℝ) fun (h : GL (Fin 2) ℝ) ↦ (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ {h : GL (Fin 2) ℝ | LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g

Tactic:
exact isOpen_Ioi (a := (0 : ℝ)) |>.preimage (by fun_prop) |>.mem_nhds hg

Premises used: isOpen_Ioi, IsOpen.mem_nhds, IsOpen.preimage
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
this : {h : GL (Fin 2) ℝ | ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g
h : GL (Fin 2) ℝ
hh : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)
⊢ σ h = σ g

Tactic:
simp only [σ, hh, ↓reduceIte, hg]

Premises used: reduceIte, UpperHalfPlane.σ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
this : {h : GL (Fin 2) ℝ | ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g
h :
  ∀ (a : GL (Fin 2) ℝ),
    Membership.mem (γ := Set (GL (Fin 2) ℝ))
      {x : GL (Fin 2) ℝ |
        Membership.mem (γ := Set (GL (Fin 2) ℝ))
            {h : GL (Fin 2) ℝ | ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)}
            x →
          Membership.mem (γ := Set (GL (Fin 2) ℝ))
            {x : GL (Fin 2) ℝ | (fun (x : GL (Fin 2) ℝ) ↦ σ x = (fun (x : GL (Fin 2) ℝ) ↦ σ g) x) x} x}
      a
h₁ h₂ :
  ∀ (h : GL (Fin 2) ℝ) (hh : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)),
    σ h = σ g
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g

Tactic:
filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
neg : {h : GL (Fin 2) ℝ | ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g

Tactic:
suffices {h | ¬0 < h.det.val} ∈ 𝓝 g by
      filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
neg :
  ∀ (hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0),
    {h : GL (Fin 2) ℝ | LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) 0} ∈ 𝓝 g
⊢ {h : GL (Fin 2) ℝ | ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g

Tactic:
simp only [not_lt, le_iff_lt_or_eq, Units.ne_zero, or_false] at hg ⊢

Premises used: Units.ne_zero, le_iff_lt_or_eq, not_lt, or_false
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
⊢ Continuous (Y := ℝ) fun (h : GL (Fin 2) ℝ) ↦ (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
⊢ {h : GL (Fin 2) ℝ | LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) 0} ∈ 𝓝 g

Tactic:
exact isOpen_Iio (a := (0 : ℝ)) |>.preimage (by fun_prop) |>.mem_nhds hg

Premises used: isOpen_Iio, IsOpen.mem_nhds, IsOpen.preimage
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
continuous_smul : Continuous (Y := ℍ) fun (p : GL (Fin 2) ℝ × ℍ) ↦ p.1 • p.2
⊢ ContinuousSMul (GL (Fin 2) ℝ) ℍ

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
continuous_smul :
  ∀ (a : GL (Fin 2) ℝ) (b : ℍ),
    ContinuousAt (Y := ℂ)
      (fun (x : GL (Fin 2) ℝ × ℍ) ↦ (σ x.1 : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ))) (a, b)
⊢ Continuous (Y := ℍ) fun (p : GL (Fin 2) ℝ × ℍ) ↦ p.1 • p.2

Tactic:
simp only [continuous_induced_rng, Function.comp_def, coe_smul, continuous_iff_continuousAt,
    Prod.forall]

Premises used: UpperHalfPlane.coe_smul, Function.comp_def, Prod.forall, continuous_iff_continuousAt, continuous_induced_rng
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
⊢ ∀ (a : GL (Fin 2) ℝ × ℍ),
    σ a.1 = σ g →
      Eq (α := ℂ) ((σ g : (a : ℂ) → ℂ) (num a.1 (↑a.2 : ℂ) / denom a.1 (↑a.2 : ℂ)) : ℂ)
        ((σ a.1 : (a : ℂ) → ℂ) (num a.1 (↑a.2 : ℂ) / denom a.1 (↑a.2 : ℂ)) : ℂ)

Tactic:
simp +contextual
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
h :
  ∀ (a : GL (Fin 2) ℝ × ℍ),
    Membership.mem (γ := Set (GL (Fin 2) ℝ × ℍ))
      {x : GL (Fin 2) ℝ × ℍ |
        Membership.mem (γ := Set (GL (Fin 2) ℝ × ℍ))
            {x : GL (Fin 2) ℝ × ℍ | (fun (x : GL (Fin 2) ℝ × ℍ) ↦ σ x.1 = (fun (x : GL (Fin 2) ℝ) ↦ σ g) x.1) x} x →
          Membership.mem (γ := Set (GL (Fin 2) ℝ × ℍ))
            {x : GL (Fin 2) ℝ × ℍ |
              (fun (x : GL (Fin 2) ℝ × ℍ) ↦
                  Eq (α := ℂ)
                    ((fun (x : GL (Fin 2) ℝ × ℍ) ↦
                        ((σ g : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ)) : ℂ))
                      x)
                    ((fun (x : GL (Fin 2) ℝ × ℍ) ↦
                        ((σ x.1 : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ)) : ℂ))
                      x))
                x}
            x}
      a
h₁ :
  ∀ (a : GL (Fin 2) ℝ × ℍ),
    σ a.1 = σ g →
      Eq (α := ℂ) ((σ g : (a : ℂ) → ℂ) (num a.1 (↑a.2 : ℂ) / denom a.1 (↑a.2 : ℂ)) : ℂ)
        ((σ a.1 : (a : ℂ) → ℂ) (num a.1 (↑a.2 : ℂ) / denom a.1 (↑a.2 : ℂ)) : ℂ)
⊢ (nhds (g, τ)).EventuallyEq (β := ℂ)
    (fun (x : GL (Fin 2) ℝ × ℍ) ↦ (σ g : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ)))
    fun (x : GL (Fin 2) ℝ × ℍ) ↦ (σ x.1 : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ))

Tactic:
filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual

Premises used: Filter.Eventually.prod_inl_nhds, UpperHalfPlane.σ_eventuallyEq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
continuous_smul :
  ∀ (g : GL (Fin 2) ℝ) (τ : ℍ),
    ContinuousAt (Y := ℂ) (fun (x : GL (Fin 2) ℝ × ℍ) ↦ (σ g : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ)))
      (g, τ)
⊢ ∀ (a : GL (Fin 2) ℝ) (b : ℍ),
    ContinuousAt (Y := ℂ)
      (fun (x : GL (Fin 2) ℝ × ℍ) ↦ (σ x.1 : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ))) (a, b)

Tactic:
refine fun g τ ↦ .congr ?_ (f := fun x ↦ (σ g) (num x.1 x.2 / denom x.1 x.2))
    (by filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual)
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
⊢ denom (g, τ).1 (↑(g, τ).2 : ℂ) ≠ 0

Tactic:
apply denom_ne_zero

Premises used: UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
funProp : denom (g, τ).1 (↑(g, τ).2 : ℂ) ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (x : GL (Fin 2) ℝ × ℍ) ↦ (σ g : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ)))
    (g, τ)

Tactic:
fun_prop (disch := apply denom_ne_zero)

Premises used: UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
inl :
  ∀ (hK : IsCompact (X := ℍ) ∅),
    ∃ (A : ℝ),
      ∀ (g : SL(2, ℝ)),
        Membership.mem (γ := Set ℍ) ∅ (g • I) →
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
              HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
            A
inr :
  ∀ (hKne : K.Nonempty),
    ∃ (A : ℝ),
      ∀ (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
⊢ ∃ (A : ℝ),
    ∀ (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

Tactic:
rcases K.eq_empty_or_nonempty with rfl | hKne

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
hK : IsCompact (X := ℍ) ∅
⊢ ∃ (A : ℝ),
    ∀ (g : SL(2, ℝ)),
      Membership.mem (γ := Set ℍ) ∅ (g • I) →
        HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
            HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
          A

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
⊢ ∃ δ > 0, ∀ z ∈ K, δ ≤ z.im

Tactic:
match hK.exists_isMinOn hKne continuous_im.continuousOn with | ⟨z, _, h⟩ => ⟨_, z.im_pos, h⟩

Premises used: UpperHalfPlane.im_pos, Continuous.continuousOn, Exists, GT.gt, And, UpperHalfPlane.im, _private.0.UpperHalfPlane.cdsq_le.match_1, IsCompact.exists_isMinOn, UpperHalfPlane.continuous_im, And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
inr :
  ∀ (δ : ℝ) (hδ : δ > 0) (hδK : ∀ z ∈ K, δ ≤ z.im),
    ∃ (A : ℝ),
      ∀ (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
⊢ ∃ (A : ℝ),
    ∀ (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

Tactic:
obtain ⟨δ, hδ, hδK⟩ : ∃ δ > 0, ∀ z ∈ K, δ ≤ z.im :=
    match hK.exists_isMinOn hKne continuous_im.continuousOn with | ⟨z, _, h⟩ => ⟨_, z.im_pos, h⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
hδK : ∀ z ∈ K, δ ≤ z.im
⊢ ∃ (A : ℝ),
    ∀ (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

Tactic:
⟨1 / δ, fun g hg ↦ ?_⟩

Premises used: HDiv.hDiv, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
hδK : ∀ z ∈ K, δ ≤ z.im
inr :
  ∀ (g : SL(2, ℝ)) (hg : 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 ≤
      1 / δ
⊢ ∃ (A : ℝ),
    ∀ (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

Tactic:
refine ⟨1 / δ, fun g hg ↦ ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
hδK : ∀ z ∈ K, δ ≤ z.im
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ δ ≤ (g • I).im

Tactic:
specialize hδK (g • I) hg

Premises used: HSMul.hSMul, UpperHalfPlane.I
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK : δ ≤ (g • I).im
⊢ δ ≤
    HDiv.hDiv (α := ℝ) (β := ℝ) (1 : ℝ)
      ((Complex.normSq : (a : ℂ) → ℝ)
          (denom ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) g) (↑I : ℂ)) :
        ℝ)

Tactic:
simp only [MulAction.compHom_smul_def, im_smul_eq_div_normSq, Matrix.SpecialLinearGroup.det_mapGL,
    Units.val_one, abs_one, I_im, mul_one] at hδK

Premises used: MulAction.compHom_smul_def, UpperHalfPlane.im_smul_eq_div_normSq, Units.val_one, Matrix.SpecialLinearGroup.det_mapGL, mul_one, UpperHalfPlane.I_im, abs_one
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK :
  δ ≤
    HDiv.hDiv (α := ℝ) (β := ℝ) (1 : ℝ)
      ((Complex.normSq : (a : ℂ) → ℝ)
          (denom ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) g) (↑I : ℂ)) :
        ℝ)
⊢ I.im ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK :
  δ ≤
    HDiv.hDiv (α := ℝ) (β := ℝ) (1 : ℝ)
      ((Complex.normSq : (a : ℂ) → ℝ)
          (denom ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) g) (↑I : ℂ)) :
        ℝ)
⊢ (Complex.normSq : (a : ℂ) → ℝ)
      (denom ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) g) (↑I : ℂ)) ≤
    1 / δ

Tactic:
rw [le_div_iff₀ (normSq_denom_pos (Matrix.SpecialLinearGroup.mapGL ℝ g) (show I.im ≠ 0 by simp)),
    mul_comm, ← le_div_iff₀ hδ] at hδK

Premises used: Real, UpperHalfPlane.normSq_denom_pos, mul_comm, Matrix.SpecialLinearGroup.mapGL, le_div_iff₀, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK :
  (Complex.normSq : (a : ℂ) → ℝ)
      (denom ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) g) (↑I : ℂ)) ≤
    1 / δ
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
    1 / δ

Tactic:
simpa [Complex.normSq, add_comm, denom, sq] using hδK

Premises used: Complex.normSq, sq, add_comm, UpperHalfPlane.denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
⊢ Eq (α := ℝ) (Matrix.det (n := Fin 2) !![0, -1; 1, 0]) 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![0, -1; 1, 0] ⋯
obtain :
  ∀ (A : ℝ)
    (hA :
      ∀ (g : SL(2, ℝ)),
        g • I ∈ S • K →
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
              HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
            A),
    ∃ (A : ℝ),
      ∀ (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 : ℝ),
    ∀ (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

Tactic:
obtain ⟨A, hA⟩ := cdsq_le (K := S • K) (hK.image <| continuous_const_smul S)

Premises used: ContinuousConstSMul.continuous_const_smul, _private.0.UpperHalfPlane.cdsq_le, IsCompact.image
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![0, -1; 1, 0] ⋯
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ S • K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A
⊢ ∃ (A : ℝ),
    ∀ (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

Tactic:
⟨A, fun g hg ↦ ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![0, -1; 1, 0] ⋯
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ S • K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A
refine :
  ∀ (g : SL(2, ℝ)) (hg : 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 : ℝ),
    ∀ (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

Tactic:
refine ⟨A, fun g hg ↦ ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![0, -1; 1, 0] ⋯
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ S • K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A
g : SL(2, ℝ)
hg : g • I ∈ K
rwa : S • g • I ∈ S • K
rwa₁ rwa₂ rwa₃ rwa₄ : g • I ∈ K
⊢ (S * g) • I ∈ S • K

Tactic:
rwa [mul_smul, Set.smul_mem_smul_set_iff]

Premises used: Set.smul_mem_smul_set_iff, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![0, -1; 1, 0] ⋯
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ S • K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A
g : SL(2, ℝ)
hg : g • I ∈ K
h :
  HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 =
    HPow.hPow (β := ℕ) ((↑(S * g) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑(S * g) : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 ≤
    A

Tactic:
convert! hA (S * g) (by rwa [mul_smul, Set.smul_mem_smul_set_iff]) using 1

Premises used: HMul.hMul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![0, -1; 1, 0] ⋯
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ S • K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A
g : SL(2, ℝ)
hg : g • I ∈ K
h :
  HPow.hPow (α := ℝ) (β := ℕ)
        (!![(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0, (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1;
              (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0, (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1]
            0 0 :
          ℝ)
        2 +
      HPow.hPow (α := ℝ) (β := ℕ)
        (!![(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0, (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1;
              (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0, (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1]
            0 1 :
          ℝ)
        2 =
    HPow.hPow (α := ℝ) (β := ℕ)
        (!![0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + -1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
                0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 + -1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1;
              1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
                1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 + 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1]
            1 0 :
          ℝ)
        2 +
      HPow.hPow (α := ℝ) (β := ℕ)
        (!![0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + -1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
                0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 + -1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1;
              1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
                1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 + 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1]
            1 1 :
          ℝ)
        2
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 =
    HPow.hPow (β := ℕ) ((↑(S * g) : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑(S * g) : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2

Tactic:
rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.eta_fin_two g.val, Matrix.mul_fin_two]

Premises used: Matrix.eta_fin_two, Matrix.mul_fin_two, Subtype.val, Matrix.SpecialLinearGroup.coe_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
S : SL(2, ℝ) := Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![0, -1; 1, 0] ⋯
A : ℝ
hA :
  ∀ (g : SL(2, ℝ)),
    g • I ∈ S • K →
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
          HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
        A
g : SL(2, ℝ)
hg : g • I ∈ K
⊢ HPow.hPow (α := ℝ) (β := ℕ)
        (!![(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0, (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1;
              (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0, (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1]
            0 0 :
          ℝ)
        2 +
      HPow.hPow (α := ℝ) (β := ℕ)
        (!![(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0, (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1;
              (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0, (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1]
            0 1 :
          ℝ)
        2 =
    HPow.hPow (α := ℝ) (β := ℕ)
        (!![0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + -1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
                0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 + -1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1;
              1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
                1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 + 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1]
            1 0 :
          ℝ)
        2 +
      HPow.hPow (α := ℝ) (β := ℕ)
        (!![0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + -1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
                0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 + -1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1;
              1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 + 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
                1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 + 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1]
            1 1 :
          ℝ)
        2

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
⊢ Continuous (Y := ℍ) fun (g : SL(2, ℝ)) ↦ g • I

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
refine : ∀ (K : Set ℍ) (hK : IsCompact K), IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
⊢ IsProperMap (Y := ℍ) fun (g : SL(2, ℝ)) ↦ g • I

Tactic:
refine isProperMap_iff_isCompact_preimage.mpr ⟨by fun_prop, fun K hK ↦ ?_⟩

Premises used: Iff.mpr, isProperMap_iff_isCompact_preimage, And.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
K : Set ℍ
hK : IsCompact K
obtain :
  ∀ (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),
    IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
⊢ IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)

Tactic:
obtain ⟨A, hA⟩ := absq_le hK

Premises used: _private.0.UpperHalfPlane.absq_le