awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
⊢ Continuous (Y := Matrix (Fin 2) (Fin 2) ℝ) fun (x : ℍ) ↦ !![√x.im, x.re / √x.im; 0, 1 / √x.im]
have funProp : ∀ (x : ℍ), √x.im ≠ 0
Tactic: fun_prop (disch := grind [im_pos])
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
⊢ Continuous (Y := ℍ) fun (p : SL(2, ℝ) × ℍ) ↦ p.1 • p.2
have suffices : ∀ (g : SL(2, ℝ)) (τ : ℍ),
  ContinuousAt (Y := ℂ)
    (fun (x : SL(2, ℝ) × ℍ) ↦
      match (motive := SL(2, ℝ) × ℍ → ℂ) x with
      | (h, z) =>
        ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)))
    (g, τ)
Tactic: suffices ∀ (g : SL(2, ℝ)) (τ : ℍ),
        ContinuousAt (fun ⟨h, z⟩ ↦ (h 0 0 * (z : ℂ) + h 0 1) / (h 1 0 * z + h 1 1)) (g, τ) by
      simpa [continuous_induced_rng, continuous_iff_continuousAt, Function.comp_def,
        coe_specialLinearGroup_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
g : SL(2, ℝ)
τ : ℍ
⊢ ContinuousAt (Y := ℂ)
    (fun (x : SL(2, ℝ) × ℍ) ↦
      match (motive := SL(2, ℝ) × ℍ → ℂ) x with
      | (h, z) =>
        ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)))
    (g, τ)
have funProp : (↑((↑(g, τ).1 : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑(g, τ).2 : ℂ) +
    (↑((↑(g, τ).1 : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) ≠
  0
Tactic: fun_prop (disch := exact denom_ne_zero g τ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
g : GL (Fin 2) ℝ
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
have pos : ∀ (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
  σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
Tactic: by_cases hg : 0 < g.det.val
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
g : GL (Fin 2) ℝ
pos :
  ∀ (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
have neg : ∀ (hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
  σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
Tactic: by_cases hg : 0 < g.det.val
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
have 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
Tactic: filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
have h₁ : ∀ (a : GL (Fin 2) ℝ), LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) a) : ℝ) → σ a = σ g
Tactic: filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
have pos : {h : GL (Fin 2) ℝ | LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g
Tactic: suffices {h | 0 < h.det.val} ∈ 𝓝 g by
      filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
have 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
Tactic: filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
have h₁ : ∀ (a : GL (Fin 2) ℝ), ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) a) : ℝ) → σ a = σ g
Tactic: filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
g : GL (Fin 2) ℝ
hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
have neg : {h : GL (Fin 2) ℝ | ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g
Tactic: suffices {h | ¬0 < h.det.val} ∈ 𝓝 g by
      filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
have 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
Tactic: simp only [not_lt, le_iff_lt_or_eq, Units.ne_zero, or_false] at hg ⊢
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
⊢ ContinuousSMul (GL (Fin 2) ℝ) ℍ
have continuous_smul : Continuous (Y := ℍ) fun (p : GL (Fin 2) ℝ × ℍ) ↦ p.1 • p.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
⊢ Continuous (Y := ℍ) fun (p : GL (Fin 2) ℝ × ℍ) ↦ p.1 • p.2
have 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)
Tactic: simp only [continuous_induced_rng, Function.comp_def, coe_smul, continuous_iff_continuousAt,
    Prod.forall]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
g : GL (Fin 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 : ℂ))
have 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
Tactic: filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
⊢ (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 : ℂ))
have 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 : ℂ)) : ℂ)
Tactic: filter_upwards [(σ_eventuallyEq g).prod_inl_nhds _] using by simp +contextual
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
⊢ ∀ (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)
have 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, τ)
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)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
⊢ ContinuousAt (Y := ℂ) (fun (x : GL (Fin 2) ℝ × ℍ) ↦ (σ g : (a : ℂ) → ℂ) (num x.1 (↑x.2 : ℂ) / denom x.1 (↑x.2 : ℂ)))
    (g, τ)
have funProp : denom (g, τ).1 (↑(g, τ).2 : ℂ) ≠ 0
Tactic: fun_prop (disch := apply denom_ne_zero)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
K : Set ℍ
hK : IsCompact K
⊢ ∃ (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
have 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
Tactic: rcases K.eq_empty_or_nonempty with rfl | hKne
Cleared hypotheses: K, hK
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
⊢ ∃ (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
have 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
Tactic: rcases K.eq_empty_or_nonempty with rfl | hKne
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
K : Set ℍ
hK : IsCompact K
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
have 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
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⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
have 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 / δ
Tactic: refine ⟨1 / δ, fun g hg ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (hypothesis)
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
hδK : ∀ z ∈ K, δ ≤ z.im
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 / δ
have hδK₁ : δ ≤ (g • I).im
Tactic: specialize hδK (g • I) hg
Cleared hypotheses: hδK
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (hypothesis)
Goal:
K : Set ℍ
hK : IsCompact K
hKne : K.Nonempty
δ : ℝ
hδ : δ > 0
g : SL(2, ℝ)
hg : g • I ∈ K
hδK : δ ≤ (g • I).im
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
    1 / δ
have hδK₁ : δ ≤
  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
Cleared hypotheses: hδK
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (hypothesis)
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 : ℂ)) :
        ℝ)
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) 2 ≤
    1 / δ
have hδK₁ : (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
Cleared hypotheses: hδK
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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 : ℝ),
    ∀ (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
have 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
Tactic: obtain ⟨A, hA⟩ := cdsq_le (K := S • K) (hK.image <| continuous_const_smul S)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
have 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
Tactic: refine ⟨A, fun g hg ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
⊢ (S * g) • I ∈ S • K
have rwa : S • g • I ∈ S • K
Tactic: rwa [mul_smul, Set.smul_mem_smul_set_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2 ≤
    A
have 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
Tactic: convert! hA (S * g) (by rwa [mul_smul, Set.smul_mem_smul_set_iff]) using 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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) 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
have 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
Tactic: rw [Matrix.SpecialLinearGroup.coe_mul, Matrix.eta_fin_two g.val, Matrix.mul_fin_two]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
⊢ IsProperMap (Y := ℍ) fun (g : SL(2, ℝ)) ↦ g • I
have refine : ∀ (K : Set ℍ) (hK : IsCompact K), IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
Tactic: refine isProperMap_iff_isCompact_preimage.mpr ⟨by fun_prop, fun K hK ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
K : Set ℍ
hK : IsCompact K
⊢ IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
have 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)
Tactic: obtain ⟨A, hA⟩ := absq_le hK
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
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
⊢ IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
have obtain : ∀ (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'),
  IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
Tactic: obtain ⟨A', hA'⟩ := cdsq_le hK