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
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)
⊢ IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)

Tactic:
obtain ⟨A', hA'⟩ := cdsq_le hK

Premises used: _private.0.UpperHalfPlane.cdsq_le
-- 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 : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
⊢ ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
have : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ) := pi_properSpace
-- 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 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
⊢ IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) (Metric.closedBall 0 (max √A √A'))

Tactic:
ProperSpace.isCompact_closedBall (0 : Matrix (Fin 2) (Fin 2) ℝ) (max √A √A')

Premises used: Max.max, Real.sqrt, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- 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 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
h :
  Eq (α := Set (Matrix (Fin 2) (Fin 2) ℝ)) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
    (Metric.closedBall 0 (max √A √A'))
⊢ IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}

Tactic:
convert! ProperSpace.isCompact_closedBall (0 : Matrix (Fin 2) (Fin 2) ℝ) (max √A √A')

Premises used: Max.max, Real.sqrt, ProperSpace.isCompact_closedBall, OfNat.ofNat
-- 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 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
h :
  Eq (α := Set (Matrix (Fin 2) (Fin 2) ℝ))
    {m : Matrix (Fin 2) (Fin 2) ℝ |
      ((|m 0 0| ≤ √A ∨ |m 0 0| ≤ √A') ∧ (|m 0 1| ≤ √A ∨ |m 0 1| ≤ √A')) ∧
        (|m 1 0| ≤ √A ∨ |m 1 0| ≤ √A') ∧ (|m 1 1| ≤ √A ∨ |m 1 1| ≤ √A')}
    {y : Matrix (Fin 2) (Fin 2) ℝ |
      (|y 0 0| ≤ √A ∧ |y 0 1| ≤ √A) ∧ |y 1 0| ≤ √A ∧ |y 1 1| ≤ √A ∨
        (|y 0 0| ≤ √A' ∧ |y 0 1| ≤ √A') ∧ |y 1 0| ≤ √A' ∧ |y 1 1| ≤ √A'}
⊢ Eq (α := Set (Matrix (Fin 2) (Fin 2) ℝ)) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
    (Metric.closedBall 0 (max √A √A'))

Tactic:
simp only [le_sup_iff, Fin.forall_fin_two, Fin.isValue, Metric.closedBall, dist_zero_right,
      Matrix.norm_def, pi_norm_le_iff_of_nonempty, Real.norm_eq_abs]

Premises used: Fin.forall_fin_two, Matrix.norm_def, Fin.isValue, pi_norm_le_iff_of_nonempty, le_sup_iff, Metric.closedBall, dist_zero_right, Real.norm_eq_abs
-- 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 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
h :
  ∀ (x : Matrix (Fin 2) (Fin 2) ℝ),
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) ℝ))
        {m : Matrix (Fin 2) (Fin 2) ℝ |
          ((|m 0 0| ≤ √A ∨ |m 0 0| ≤ √A') ∧ (|m 0 1| ≤ √A ∨ |m 0 1| ≤ √A')) ∧
            (|m 1 0| ≤ √A ∨ |m 1 0| ≤ √A') ∧ (|m 1 1| ≤ √A ∨ |m 1 1| ≤ √A')}
        x ↔
      Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) ℝ))
        {y : Matrix (Fin 2) (Fin 2) ℝ |
          (|y 0 0| ≤ √A ∧ |y 0 1| ≤ √A) ∧ |y 1 0| ≤ √A ∧ |y 1 1| ≤ √A ∨
            (|y 0 0| ≤ √A' ∧ |y 0 1| ≤ √A') ∧ |y 1 0| ≤ √A' ∧ |y 1 1| ≤ √A'}
        x
⊢ Eq (α := Set (Matrix (Fin 2) (Fin 2) ℝ))
    {m : Matrix (Fin 2) (Fin 2) ℝ |
      ((|m 0 0| ≤ √A ∨ |m 0 0| ≤ √A') ∧ (|m 0 1| ≤ √A ∨ |m 0 1| ≤ √A')) ∧
        (|m 1 0| ≤ √A ∨ |m 1 0| ≤ √A') ∧ (|m 1 1| ≤ √A ∨ |m 1 1| ≤ √A')}
    {y : Matrix (Fin 2) (Fin 2) ℝ |
      (|y 0 0| ≤ √A ∧ |y 0 1| ≤ √A) ∧ |y 1 0| ≤ √A ∧ |y 1 1| ≤ √A ∨
        (|y 0 0| ≤ √A' ∧ |y 0 1| ≤ √A') ∧ |y 1 0| ≤ √A' ∧ |y 1 1| ≤ √A'}

Tactic:
ext
-- 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 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
x : Matrix (Fin 2) (Fin 2) ℝ
⊢ Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) ℝ))
      {m : Matrix (Fin 2) (Fin 2) ℝ |
        ((|m 0 0| ≤ √A ∨ |m 0 0| ≤ √A') ∧ (|m 0 1| ≤ √A ∨ |m 0 1| ≤ √A')) ∧
          (|m 1 0| ≤ √A ∨ |m 1 0| ≤ √A') ∧ (|m 1 1| ≤ √A ∨ |m 1 1| ≤ √A')}
      x ↔
    Membership.mem (γ := Set (Matrix (Fin 2) (Fin 2) ℝ))
      {y : Matrix (Fin 2) (Fin 2) ℝ |
        (|y 0 0| ≤ √A ∧ |y 0 1| ≤ √A) ∧ |y 1 0| ≤ √A ∧ |y 1 1| ≤ √A ∨
          (|y 0 0| ≤ √A' ∧ |y 0 1| ≤ √A') ∧ |y 1 0| ≤ √A' ∧ |y 1 1| ≤ √A'}
      x

Tactic:
grind
-- 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 : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
⊢ IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}

Tactic:
have : IsCompact {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ i j, |m i j| ≤ max √A √A'} := by
    convert! ProperSpace.isCompact_closedBall (0 : Matrix (Fin 2) (Fin 2) ℝ) (max √A √A')
    simp only [le_sup_iff, Fin.forall_fin_two, Fin.isValue, Metric.closedBall, dist_zero_right,
      Matrix.norm_def, pi_norm_le_iff_of_nonempty, Real.norm_eq_abs]
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `ext` was not necessary.
    The cause of this might be `Matrix` function application defeq abuse. -/
    ext; grind
-- 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 : IsCompact (X := Matrix (Fin 2) (Fin 2) ℝ) {m : Matrix (Fin 2) (Fin 2) ℝ | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
⊢ 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'})

Tactic:
have := Matrix.SpecialLinearGroup.isClosedEmbedding_val.isCompact_preimage this
-- 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'})
⊢ Continuous (Y := ℍ) fun (g : SL(2, ℝ)) ↦ g • I

Tactic:
fun_prop
-- 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'})
refine :
  ∀ (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),
    Membership.mem (γ := Set { 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
⊢ IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)

Tactic:
refine this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop) (fun g hg ↦ ?_)

Premises used: IsCompact.of_isClosed_subset, IsClosed.preimage, IsCompact.isClosed
-- 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
i j : Fin 2
0 : |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j| ≤ max √A √A'
1 : |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) j| ≤ max √A √A'
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) i j| ≤ max √A √A'

Tactic:
fin_cases i
-- 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) (⟨0, ⋯⟩ : Fin 2)) j| ≤ max √A √A'

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

Premises used: Real.sqrt, le_max_left, 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 : |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j| ≤ √A
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j| ≤ max √A √A'

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

Premises used: Real.sqrt, le_max_left, 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) (⟨0, ⋯⟩ : Fin 2))
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))|
      2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) 2
1 :
  HPow.hPow (β := ℕ)
      |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))|
      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 (β := ℕ) |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) j| 2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 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) (⟨0, ⋯⟩ : Fin 2))
          ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))|
      2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 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) (⟨0, ⋯⟩ : Fin 2))
          ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))|
      2 ≤
    HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) 2 +
      HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 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) (⟨0, ⋯⟩ : 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