awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu_1 : (σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
coe :
  (((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) +
            (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) *
          u +
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) +
          (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))) *
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) *
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * u + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) *
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * u + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))) =
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) *
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * u + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) *
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * u + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))) *
      (((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) +
            (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) *
          u +
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) +
          (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)))
⊢ num (g * h) u *
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * num h u +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * denom h u) =
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * num h u +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) * denom h u) *
      denom (g * h) u

Tactic:
simp only [num, denom, Units.val_mul, mul_apply, Fin.sum_univ_succ,
    Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one,
    Complex.ofReal_add, Complex.ofReal_mul]

Premises used: Complex.ofReal_add, Matrix.mul_apply, Finset.univ_unique, Fin.succ_zero_eq_one, Finset.sum_singleton, UpperHalfPlane.denom, Fin.default_eq_zero, UpperHalfPlane.num, Units.val_mul, Complex.ofReal_mul, Fin.sum_univ_succ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu_1 : (σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ (((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) +
            (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) *
          u +
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) +
          (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))) *
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) *
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * u + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) *
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * u + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))) =
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) *
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * u + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) *
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * u + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))) *
      (((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) +
            (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)) *
          u +
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ) +
          (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) * (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)))

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ smulAux 1 z = z

Tactic:
simp [smulAux, smulAux', num, denom, σ]

Premises used: UpperHalfPlane.smulAux, UpperHalfPlane.smulAux', UpperHalfPlane.denom, UpperHalfPlane.σ, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (↑(g • z) : ℂ) = (σ g : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ))

Tactic:
rfl

Premises used: UpperHalfPlane.smulAux', rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 : ℂ)
rw₅ 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) : ℂ))
⊢ smulAux' g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)

Tactic:
rw [smulAux', σ, if_pos hg, ContinuousAlgEquiv.refl_apply, num, denom]

Premises used: UpperHalfPlane.smulAux', if_pos, UpperHalfPlane.denom, ContinuousAlgEquiv.refl_apply, UpperHalfPlane.σ, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
⊢ denom (g * h) (↑z : ℂ) = HMul.hMul (α := ℂ) ((σ h : (a : ℂ) → ℂ) (denom g (↑(h • z) : ℂ)) : ℂ) (denom h (↑z : ℂ))

Tactic:
denom_cocycle' g h z

Premises used: UpperHalfPlane.denom_cocycle'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
z : ℍ
coe : (↑(g • z) : ℂ) = (↑{ coe := num g (↑z : ℂ) / denom g (↑z : ℂ), coe_im_pos := ⋯ } : ℂ)
⊢ g • z = { coe := num g (↑z : ℂ) / denom g (↑z : ℂ), coe_im_pos := ⋯ }

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 := ⋯ } : ℂ)

Tactic:
simp [coe_smul_of_det_pos hg]

Premises used: UpperHalfPlane.coe_smul_of_det_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (smulAux' g (↑z : ℂ)).re = (num g (↑z : ℂ) / denom g (↑z : ℂ)).re

Tactic:
simp +contextual [smulAux', σ, DFunLike.ite_apply, apply_ite, Complex.div_re]

Premises used: apply_ite, UpperHalfPlane.smulAux', DFunLike.ite_apply, Complex.div_re, UpperHalfPlane.σ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
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 : ℂ)) : ℝ)
⊢ (smulAux' g (↑z : ℂ)).im = |(num g (↑z : ℂ) / denom g (↑z : ℂ)).im|

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 _]

Premises used: neg_div, UpperHalfPlane.im_pos, UpperHalfPlane.moebius_im, Complex.conjCAE_apply, abs_mul, abs_div, Eq.rec, apply_ite, Complex.conj_im, UpperHalfPlane.smulAux', DFunLike.ite_apply, Complex.normSq_nonneg, ContinuousAlgEquiv.refl_apply, abs_of_nonneg, neg_mul, UpperHalfPlane.σ, abs_of_pos, Eq.symm, UpperHalfPlane.coe_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 : ℂ)) : ℝ)
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 : ℂ)) : ℝ)
⊢ (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:
split_ifs with h
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
pos 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 : ℂ)) : ℝ)
⊢ 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]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
h : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
neg 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 : ℂ)) : ℝ)
⊢ 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)]

Premises used: abs_of_nonpos, not_lt, Iff.mp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 : ℂ)) : ℝ)
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 : ℂ)) : ℝ)
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 : ℂ)) : ℝ)
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 : ℂ)) : ℝ)
⊢ (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:
split_ifs with h <;> [rw [abs_of_pos h]; rw [abs_of_nonpos (not_lt.mp h)]]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (g • z).im =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * z.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)

Tactic:
smulAux'_im g z

Premises used: UpperHalfPlane.coe, UpperHalfPlane.im, UpperHalfPlane.smulAux'_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
set :
  let c := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0;
  HPow.hPow (β := ℕ) (c * z.im) 2 ≤ (Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ))
⊢ HPow.hPow (β := ℕ) ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * z.im) 2 ≤ (Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ))

Tactic:
set c := g 1 0

Premises used: Units.val, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
d : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
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
⊢ HPow.hPow (β := ℕ) (c * z.im) 2 ≤ HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2

Tactic:
nlinarith
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
c : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
d : ℝ := (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
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)
⊢ HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2 =
    (Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ))

Tactic:
simp [denom, Complex.normSq]

Premises used: Complex.normSq, UpperHalfPlane.denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 =
    ((↑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:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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
by₁ :
  HPow.hPow (β := ℕ) (c * z.im) 2 + HPow.hPow (β := ℕ) (c * z.re + d) 2 =
    (Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ))
⊢ HPow.hPow (β := ℕ) (c * z.im) 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

Premises used: HMul.hMul, UpperHalfPlane.coe, Complex.normSq, UpperHalfPlane.denom, UpperHalfPlane.im, HAdd.hAdd, DFunLike.coe, UpperHalfPlane.re
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
coe : (↑(-g • z) : ℂ) = (↑(g • z) : ℂ)
⊢ -g • z = g • z

Tactic:
ext1
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ (↑(-g • z) : ℂ) = (↑(g • z) : ℂ)

Tactic:
simp [coe_smul]

Premises used: UpperHalfPlane.coe_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ num 1 (↑z : ℂ) = (↑z : ℂ)

Tactic:
simp [num]

Premises used: UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ denom 1 (↑z : ℂ) = 1

Tactic:
simp [denom]

Premises used: UpperHalfPlane.denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
u : ℝˣ
z : ℍ
⊢ num ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u) (↑z : ℂ) = (↑(↑u : ℝ) : ℂ) * (↑z : ℂ)

Tactic:
simp [num]

Premises used: UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
u : ℝˣ
z : ℍ
⊢ denom ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u) (↑z : ℂ) = (↑(↑u : ℝ) : ℂ)

Tactic:
simp [denom]

Premises used: UpperHalfPlane.denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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
hg :
  LT.lt (α := ℝ) 0
    (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ)
          ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u)) :
      ℝ)
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u : GL (Fin 2) ℝ) z = z

Tactic:
rw [glPos_smul_def]

Premises used: UpperHalfPlane.glPos_smul_def
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
u : ℝˣ
z : ℍ
⊢ {
      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

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
u : ℝˣ
z : ℍ
⊢ LT.lt (α := ℝ) 0
    (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ)
          ((GeneralLinearGroup.scalar (Fin 2) : (a : ℝˣ) → GL (Fin 2) ℝ) u)) :
      ℝ)

Tactic:
simp [sq_pos_iff]

Premises used: sq_pos_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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]
⊢ m.det ≠ 0

Tactic:
simp [m, im_ne_zero]

Premises used: UpperHalfPlane.im_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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]
refine : GeneralLinearGroup.mkOfDetNeZero m ⋯ • z = w
⊢ ∃ (g : GL (Fin 2) ℝ), g • z = w

Tactic:
refine ⟨.mkOfDetNeZero m <| by simp [m, im_ne_zero], ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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]
coe : (↑(GeneralLinearGroup.mkOfDetNeZero m ⋯ • z) : ℂ) = (↑w : ℂ)
⊢ GeneralLinearGroup.mkOfDetNeZero m ⋯ • z = w

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 : ℂ)

Tactic:
simp [coe_smul_of_det_pos, im_pos, num, denom, m, Complex.ext_iff, im_ne_zero]

Premises used: UpperHalfPlane.im_pos, UpperHalfPlane.im_ne_zero, UpperHalfPlane.coe_smul_of_det_pos, Complex.ext_iff, UpperHalfPlane.denom, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ HSMul.hSMul (α := PGL(2, ℝ)) ((ProjGenLinGroup.mk : (a : GL (Fin 2) ℝ) → PGL(2, ℝ)) g : PGL(2, ℝ)) z = g • z

Tactic:
ProjGenLinGroup.mk_smul ..

Premises used: Matrix.ProjGenLinGroup.mk_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
⊢ MulAction.IsPretransitive PGL(2, ℝ) ℍ

Tactic:
.of_smul_eq .mk <| pglMk_smul _ _

Premises used: MulAction.IsPretransitive.of_smul_eq, UpperHalfPlane.pglMk_smul, Matrix.ProjGenLinGroup.mk, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ LT.lt (α := ℝ) 0
    (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ)
          (((mapGL ℝ : SL(2, R) →* GL (Fin 2) ℝ) : (a : SL(2, R)) → GL (Fin 2) ℝ) g)) :
      ℝ)

Tactic:
simp