awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
z : ℍ
rw : (σ g : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
⊢ smulAux' g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
have rw₁ : (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE :
      (a : ℂ) → ℂ)
    (num g (↑z : ℂ) / denom g (↑z : ℂ)) =
  num g (↑z : ℂ) / denom g (↑z : ℂ)
Tactic: rw [smulAux', σ, if_pos hg, ContinuousAlgEquiv.refl_apply, num, denom]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
z : ℍ
rw : (σ g : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₁ :
  (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
        else Complex.conjCAE :
        (a : ℂ) → ℂ)
      (num g (↑z : ℂ) / denom g (↑z : ℂ)) =
    num g (↑z : ℂ) / denom g (↑z : ℂ)
⊢ smulAux' g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
have rw₂ : (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
Tactic: rw [smulAux', σ, if_pos hg, ContinuousAlgEquiv.refl_apply, num, denom]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
z : ℍ
rw : (σ g : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₁ :
  (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
        else Complex.conjCAE :
        (a : ℂ) → ℂ)
      (num g (↑z : ℂ) / denom g (↑z : ℂ)) =
    num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₂ :
  (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
⊢ smulAux' g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
have rw₃ : num g (↑z : ℂ) / denom g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
Tactic: rw [smulAux', σ, if_pos hg, ContinuousAlgEquiv.refl_apply, num, denom]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
z : ℍ
rw : (σ g : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₁ :
  (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
        else Complex.conjCAE :
        (a : ℂ) → ℂ)
      (num g (↑z : ℂ) / denom g (↑z : ℂ)) =
    num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₂ :
  (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₃ : num g (↑z : ℂ) / denom g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
⊢ smulAux' g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
have rw₄ : ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
    denom g (↑z : ℂ) =
  ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
    denom g (↑z : ℂ)
Tactic: rw [smulAux', σ, if_pos hg, ContinuousAlgEquiv.refl_apply, num, denom]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
z : ℍ
rw : (σ g : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₁ :
  (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
        else Complex.conjCAE :
        (a : ℂ) → ℂ)
      (num g (↑z : ℂ) / denom g (↑z : ℂ)) =
    num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₂ :
  (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₃ : num g (↑z : ℂ) / denom g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
rw₄ :
  ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
      denom g (↑z : ℂ) =
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
      denom g (↑z : ℂ)
⊢ smulAux' g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
have rw₅ : ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) =
  ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))
Tactic: rw [smulAux', σ, if_pos hg, ContinuousAlgEquiv.refl_apply, num, denom]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
z : ℍ
⊢ g • z = { coe := num g (↑z : ℂ) / denom g (↑z : ℂ), coe_im_pos := ⋯ }
have coe : (↑(g • z) : ℂ) = (↑{ coe := num g (↑z : ℂ) / denom g (↑z : ℂ), coe_im_pos := sorry } : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (smulAux' g (↑z : ℂ)).im = |(num g (↑z : ℂ) / denom g (↑z : ℂ)).im|
have simp : (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
    HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
  else
    HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)) =
  HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
    ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
Tactic: simp only [smulAux', σ, DFunLike.ite_apply, ContinuousAlgEquiv.refl_apply, apply_ite, moebius_im,
    Complex.conjCAE_apply, Complex.conj_im, ← neg_div, ← neg_mul, abs_div, abs_mul,
    abs_of_pos (show 0 < (z : ℂ).im from z.coe_im ▸ z.im_pos),
    abs_of_nonneg <| Complex.normSq_nonneg _]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
      HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
    else
      HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
have pos : ∀ (h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
  HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
pos :
  ∀ (h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
      HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
⊢ (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
      HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
    else
      HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
have neg : ∀ (h : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
  HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
have pos : HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
    ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
  HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
    ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
Tactic: rw [abs_of_pos h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
have neg : HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
    ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
  HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
    ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
Tactic: rw [abs_of_nonpos (not_lt.mp h)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
      HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
    else
      HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
have pos : ∀ (h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
  HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
Tactic: split_ifs with h <;> [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
pos :
  ∀ (h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
      HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
⊢ (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
      HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
    else
      HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
have neg : ∀ (h : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
  HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
Tactic: split_ifs with h <;> [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
d : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
⊢ HPow.hPow (β := ℕ) (c * z.im) 2 ≤ HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2
have nlinarith : HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2 < HPow.hPow (β := ℕ) (c * z.im) 2 →
  0 - HPow.hPow (β := ℕ) (c * z.re + d) 2 +
      (HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2 - HPow.hPow (β := ℕ) (c * z.im) 2) =
    0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
d : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
⊢ HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2 =
    (Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ))
have simp : HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2 =
  ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * z.re + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) *
      ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * z.re + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) +
    (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * z.im * ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * z.im)
Tactic: simp [denom, Complex.normSq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
d : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
⊢ HPow.hPow (β := ℕ) (c * z.im) 2 ≤ (Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ))
have by : HPow.hPow (β := ℕ) (c * z.im) 2 ≤ HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2
Tactic: calc
    (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
    _ = Complex.normSq (denom g z) := by simp [denom, Complex.normSq]; ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
d : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
by : HPow.hPow (β := ℕ) (c * z.im) 2 ≤ HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2
⊢ HPow.hPow (β := ℕ) (c * z.im) 2 ≤ (Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ))
have by₁ : HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2 =
  (Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ))
Tactic: calc
    (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
    _ = Complex.normSq (denom g z) := by simp [denom, Complex.normSq]; ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ -g • z = g • z
have coe : (↑(-g • z) : ℂ) = (↑(g • z) : ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
u : ℝˣ
z : ℍ
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u : GL (Fin 2) ℝ) z = z
have rw : {
    coe :=
      num ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u) (↑z : ℂ) /
        denom ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u) (↑z : ℂ),
    coe_im_pos := sorry : ℍ } =
  z
Tactic: rw [glPos_smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
u : ℝˣ
z : ℍ
rw :
  {
      coe :=
        num ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u) (↑z : ℂ) /
          denom ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u) (↑z : ℂ),
      coe_im_pos := ⋯ : ℍ } =
    z
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u : GL (Fin 2) ℝ) z = z
have hg : LT.lt (α := ℝ) 0
  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ)
        ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u)) :
    ℝ)
Tactic: rw [glPos_smul_def]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z_1 z w : ℍ
m : Matrix (Fin 2) (Fin 2) ℝ := !![w.im, z.im * w.re - w.im * z.re; 0, z.im]
⊢ ∃ (g : GL (Fin 2) ℝ), g • z = w
have refine : GeneralLinearGroup.mkOfDetNeZero m sorry • z = w
Tactic: refine ⟨.mkOfDetNeZero m <| by simp [m, im_ne_zero], ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z_1 z w : ℍ
m : Matrix (Fin 2) (Fin 2) ℝ := !![w.im, z.im * w.re - w.im * z.re; 0, z.im]
⊢ GeneralLinearGroup.mkOfDetNeZero m ⋯ • z = w
have coe : (↑(GeneralLinearGroup.mkOfDetNeZero m sorry • z) : ℂ) = (↑w : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ (↑(g • z) : ℂ) =
    ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
      ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ))
have rw : num (((mapGL ℝ : SL(2, R) →* GL (Fin 2) ℝ) : (a : SL(2, R)) → GL (Fin 2) ℝ) g) (↑z : ℂ) /
    denom (((mapGL ℝ : SL(2, R) →* GL (Fin 2) ℝ) : (a : SL(2, R)) → GL (Fin 2) ℝ) g) (↑z : ℂ) =
  ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
      (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
    ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
      (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ))
Tactic: rw [MulAction.compHom_smul_def, coe_smul_of_det_pos (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ g • z =
    {
      coe :=
        ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
          ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ)),
      coe_im_pos := ⋯ }
have coe : (↑(g • z) : ℂ) =
  (↑{
        coe :=
          ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
              (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
            ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
              (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ)),
        coe_im_pos := sorry } :
    ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
z : ℍ
⊢ ModularGroup.S • z = { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ }
have rw : {
    coe :=
      ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
          (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
        ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
          (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)),
    coe_im_pos := sorry : ℍ } =
  { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := sorry }
Tactic: rw [specialLinearGroup_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
z : ℍ
n : ℤ
⊢ ModularGroup.T ^ n • z = HVAdd.hVAdd (α := ℝ) (↑n : ℝ) z
have rw : ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
      (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
    ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
      (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)) =
  (↑z : ℂ) + (↑(↑n : ℝ) : ℂ)
Tactic: rw [UpperHalfPlane.ext_iff, coe_vadd, add_comm, coe_specialLinearGroup_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : SL(2, ℝ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ ∃ (u : { x : ℝ // 0 < x }) (v : ℝ),
    Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
have obtain : ∀ (a b : ℝ) (ha : a ≠ 0)
  (hc :
    Eq (α := ℝ)
      ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] sorry) :
            Matrix (Fin 2) (Fin 2) ℝ)
          1 0 :
        ℝ)
      (0 : ℝ)),
  ∃ (u : { x : ℝ // 0 < x }) (v : ℝ),
    Eq (α := ℍ → ℍ)
      (fun (x : ℍ) ↦
        HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] sorry :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          x)
      ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
Tactic: obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc
Cleared hypotheses: g, hc