awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
pos :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
      Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
        ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
⊢ Eq (α := ℂ)
    ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
    ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have neg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
    Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((Complex.conjCAE : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
pos :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
      Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
        ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
neg :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
      Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)
        ((Complex.conjCAE : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
⊢ Eq (α := ℂ)
    ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
    ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have pos₁ : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
    Eq (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
pos :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
      Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
        ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
neg :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
      Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)
        ((Complex.conjCAE : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
pos₁ :
  ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
      Eq (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
        ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)
⊢ Eq (α := ℂ)
    ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
    ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have neg₁ : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) →
    Eq (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((Complex.conjCAE : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ norm (E := ℂ)
      ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
              ContinuousAlgEquiv.refl ℝ ℂ
            else Complex.conjCAE :
            (a : ℂ) → ℂ)
          z :
        ℂ) =
    ‖z‖
have pos : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  norm (E := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) = ‖z‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℂ
pos :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    norm (E := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) = ‖z‖
⊢ norm (E := ℂ)
      ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
              ContinuousAlgEquiv.refl ℝ ℂ
            else Complex.conjCAE :
            (a : ℂ) → ℂ)
          z :
        ℂ) =
    ‖z‖
have neg : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  norm (E := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) = ‖z‖
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ Complex.im
      ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        (num g z / 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) : ℝ)),
  Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g z / 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) : ℝ)),
    Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g z / denom g z)) =
      HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * z.im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ)
⊢ Complex.im
      ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        (num g z / 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) : ℝ)),
  Complex.im ((Complex.conjCAE : (a : ℂ) → ℂ) (num g z / 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) : ℝ)
⊢ Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g z / denom g z)) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * z.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ)
have pos : Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g z / 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) : ℝ)
⊢ Complex.im ((Complex.conjCAE : (a : ℂ) → ℂ) (num g z / denom g z)) =
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * z.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ)
have neg : Complex.im ((Complex.conjCAE : (a : ℂ) → ℂ) (num g z / 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 : ℂ
⊢ Complex.im
      ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        (num g z / 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) : ℝ)),
  Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g z / 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) : ℝ)),
    Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (num g z / denom g z)) =
      HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * z.im)
        ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ)
⊢ Complex.im
      ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        (num g z / 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) : ℝ)),
  Complex.im ((Complex.conjCAE : (a : ℂ) → ℂ) (num g z / 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 : ℍ
⊢ 0 < (smulAux' g (↑z : ℂ)).im
have rw : 0 <
  HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
    ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
Tactic: rw [smulAux'_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
⊢ denom (g * h) (↑z : ℂ) =
    HMul.hMul (α := ℂ) ((σ h : (a : ℂ) → ℂ) (denom g (↑(smulAux h z) : ℂ)) : ℂ) (denom h (↑z : ℂ))
have simp : denom (g * h) (↑z : ℂ) = denom g (num h (↑z : ℂ) / denom h (↑z : ℂ)) * denom h (↑z : ℂ)
Tactic: simp only [smulAux, smulAux', coe_mk, map_div₀, σ_num, σ_denom, σ_sq]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
⊢ denom (g * h) (↑z : ℂ) =
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (num h (↑z : ℂ) / denom h (↑z : ℂ)) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) *
      denom h (↑z : ℂ)
have field_simp : denom (g * h) (↑z : ℂ) =
  (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * num h (↑z : ℂ) +
    denom h (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)
Tactic: field_simp [denom_ne_zero h z]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
⊢ denom (g * h) (↑z : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * num h (↑z : ℂ) +
      denom h (↑z : ℂ) * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)
have simp : ((↑((↑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) : ℂ)) *
      (↑z : ℂ) +
    ((↑((↑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) : ℂ)) =
  (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) *
      ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) +
    ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) *
      (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)
Tactic: simp only [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, num]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
⊢ smulAux (g * h) z = smulAux g (smulAux h z)
have coe : (↑(smulAux (g * h) z) : ℂ) = (↑(smulAux g (smulAux h z)) : ℂ)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
⊢ (↑(smulAux (g * h) z) : ℂ) = (↑(smulAux g (smulAux h z)) : ℂ)
have coe : num (g * h) ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)) /
    denom (g * h) ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)) =
  num g
      (num h ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)) /
        denom h ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ))) /
    denom g
      (num h ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)) /
        denom h ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)))
Tactic: simp only [smulAux, coe_mk, smulAux', map_div₀, σ_num, σ_denom, σ_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
⊢ num (g * h) ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)) /
      denom (g * h) ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)) =
    num g
        (num h ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)) /
          denom h ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ))) /
      denom g
        (num h ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)) /
          denom h ((σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)))
have coe : ∀ (u : ℂ) (hu : (σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) = u),
  num (g * h) u / denom (g * h) u = num g (num h u / denom h u) / denom g (num h u / denom h u)
Tactic: generalize hu : σ g (σ h z) = u
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu : (σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) = u
⊢ num (g * h) u / denom (g * h) u = num g (num h u / denom h u) / denom g (num h u / denom h u)
have hu₁ : u.im ≠ 0
Tactic: have hu : u.im ≠ 0 := by simpa only [← hu, σ_im_ne_zero] using z.im_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu_1 : (σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) = u
hu : u.im ≠ 0
⊢ (num h u / denom h u).im ≠ 0
have rw : HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) * u.im)
    ((Complex.normSq : (a : ℂ) → ℝ) (denom h u) : ℝ) ≠
  0
Tactic: rw [moebius_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu_1 : (σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) = u
hu : u.im ≠ 0
⊢ num (g * h) u / denom (g * h) u = num g (num h u / denom h u) / denom g (num h u / denom h u)
have hu' : (num h u / denom h u).im ≠ 0
Tactic: have hu' : (num h u / denom h u).im ≠ 0 := by
    rw [moebius_im]
    exact div_ne_zero (mul_ne_zero h.det_ne_zero hu) (normSq_denom_ne_zero _ hu)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ num (g * h) u / denom (g * h) u = num g (num h u / denom h u) / denom g (num h u / denom h u)
have coe : 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) /
    denom h u =
  num g (num h u / denom h u) * denom (g * h) u
Tactic: rw [div_eq_div_iff (denom_ne_zero_of_im _ hu) (denom_ne_zero_of_im _ hu'),
    denom, mul_div, div_add' _ _ _ (denom_ne_zero_of_im _ hu), mul_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ 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) /
      denom h u =
    ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (num h u / denom h u) +
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) *
      denom (g * h) u
have coe : 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) /
    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 /
    denom h u
Tactic: rw [mul_div, div_add' _ _ _ (denom_ne_zero_of_im _ hu), div_mul_eq_mul_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ 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) /
      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 /
      denom h u
have coe : 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: congr 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ 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
have 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) : ℂ)))
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]
-- 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 : ℍ
⊢ smulAux' g (↑z : ℂ) = num g (↑z : ℂ) / denom g (↑z : ℂ)
have rw : (σ g : (a : ℂ) → ℂ) (num g (↑z : ℂ) / denom g (↑z : ℂ)) = num g (↑z : ℂ) / denom g (↑z : ℂ)
Tactic: rw [smulAux', σ, if_pos hg, ContinuousAlgEquiv.refl_apply, num, denom]