awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (hypothesis)
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
⊢ IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
have this₁ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
Tactic: have : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ) := pi_properSpace
-- 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
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'}
have 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'))
Tactic: convert! ProperSpace.isCompact_closedBall (0 : Matrix (Fin 2) (Fin 2) ℝ) (max √A √A')
-- 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
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) ℝ)
⊢ 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'))
have 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'}
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]
-- 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
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) ℝ)
⊢ 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'}
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (hypothesis)
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 := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
have this₁ : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (hypothesis)
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 := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
have 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'})
Tactic: have := Matrix.SpecialLinearGroup.isClosedEmbedding_val.isCompact_preimage this
-- 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
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'})
⊢ IsCompact (X := SL(2, ℝ)) ((fun (g : SL(2, ℝ)) ↦ g • I) ⁻¹' K)
have 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
Tactic: refine this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop) (fun g hg ↦ ?_)
-- 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
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
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) i j| ≤ max √A √A'
have 0 : |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j| ≤ max √A √A'
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
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'
⊢ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) i j| ≤ max √A √A'
have 1 : |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j| ≤ max √A √A'
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
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'
have 0 : |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) j| ≤ √A
Tactic: refine le_trans ?_ <| le_max_left √A √A'
-- 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
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
⊢ 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
have 0 : HPow.hPow (β := ℕ)
    |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : 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: fin_cases j
Cleared hypotheses: j
-- 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
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
⊢ 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
have 1 : HPow.hPow (β := ℕ)
    |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : 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: fin_cases j
Cleared hypotheses: j
-- 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
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'
have 1 : |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) j| ≤ √A'
Tactic: refine le_trans ?_ <| le_max_right √A √A'
-- 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
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
⊢ 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
have 0 : HPow.hPow (β := ℕ)
    |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : 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: fin_cases j
Cleared hypotheses: j
-- 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
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
⊢ 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
have 1 : HPow.hPow (β := ℕ)
    |(↑g : Matrix (Fin 2) (Fin 2) ℝ) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : 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: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (hypothesis)
Goal:
𝒢 : Subgroup SL(2, ℝ)
inst : DiscreteTopology ↥𝒢
⊢ ProperlyDiscontinuousSMul ↥𝒢 ℍ
have this : IsClosed (↑𝒢 : Set SL(2, ℝ))
Tactic: have : IsClosed (𝒢 : Set SL(2, ℝ)) := Subgroup.isClosed_of_discrete
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
𝒢 : Subgroup SL(2, ℝ)
inst : DiscreteTopology ↥𝒢
this : IsClosed (↑𝒢 : Set SL(2, ℝ))
⊢ ProperlyDiscontinuousSMul ↥𝒢 ℍ
have rw : ProperSMul ↥𝒢 ℍ
Tactic: rw [properlyDiscontinuousSMul_iff_properSMul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
⊢ ContractibleSpace ℍ
have rw : ContractibleSpace (↑upperHalfPlaneSet : Type)
Tactic: rw [isEmbedding_coe.toHomeomorph.trans (.setCongr range_coe) |>.contractibleSpace_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (hypothesis)
Goal:
h : IsCompact (X := ℍ) univ
⊢ False
have this : IsCompact (Complex.im ⁻¹' Ioi 0)
Tactic: have : IsCompact (Complex.im ⁻¹' Ioi 0) := by
      simpa [isEmbedding_coe.isCompact_iff] using h
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Topology (goal)
Goal:
g : GL (Fin 2) ℝ
⊢ Continuous (Y := ℍ) fun (x : ℍ) ↦ g • x
have 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 : ℂ))
Tactic: simp_rw [continuous_induced_rng (f := UpperHalfPlane.coe), Function.comp_def,
      UpperHalfPlane.coe_smul, UpperHalfPlane.σ]