awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ (num g z / denom g z).im =
    HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * z.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ)
have simp : HDiv.hDiv (β := ℝ)
    ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 * z.im *
        ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * z.re + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) -
      ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 * z.re + (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) *
        ((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 * z.im))
    ((Complex.normSq : (a : ℂ) → ℝ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) :
      ℝ) =
  HDiv.hDiv (β := ℝ)
    (((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 -
        (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) *
      z.im)
    ((Complex.normSq : (a : ℂ) → ℝ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) :
      ℝ)
Tactic: simp only [num, denom, Complex.div_im, Complex.add_im, Complex.mul_im, Complex.ofReal_re,
    Complex.ofReal_im, zero_mul, add_zero, Complex.add_re, Complex.mul_re, sub_zero, ← sub_div,
    GeneralLinearGroup.val_det_apply, g.1.det_fin_two]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ Eq (α := ℂ)
    ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) :
      ℂ)
    ((starRingEnd ℂ : (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) : ℝ) →
  Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) 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) : ℝ) →
    Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
⊢ Eq (α := ℂ)
    ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) :
      ℂ)
    ((starRingEnd ℂ : (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) : ℝ) →
  Eq (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
y : ℝ
⊢ (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
        else Complex.conjCAE :
        (a : ℂ) → ℂ)
      (↑y : ℂ) =
    (↑y : ℂ)
have pos : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (↑y : ℂ) = (↑y : ℂ)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : GL (Fin 2) ℝ
y : ℝ
pos :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (↑y : ℂ) = (↑y : ℂ)
⊢ (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
        else Complex.conjCAE :
        (a : ℂ) → ℂ)
      (↑y : ℂ) =
    (↑y : ℂ)
have neg : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  (Complex.conjCAE : (a : ℂ) → ℂ) (↑y : ℂ) = (↑y : ℂ)
Tactic: split_ifs
-- 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 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 :
        ℂ) =
    z
have pos : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((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) : ℝ) →
    (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) = z
⊢ (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) ℝ) → ℝˣ) g) : ℝ) then
              ContinuousAlgEquiv.refl ℝ ℂ
            else Complex.conjCAE :
            (a : ℂ) → ℂ)
          z :
        ℂ) =
    z
have neg : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  (Complex.conjCAE : (a : ℂ) → ℂ) ((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 : ℂ) → ℂ)
          z) ≠
      0 ↔
    z.im ≠ 0
have pos : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  (Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z) ≠ 0 ↔ z.im ≠ 0)
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) : ℝ) →
    (Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z) ≠ 0 ↔ z.im ≠ 0)
⊢ Complex.im
        ((if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
              ContinuousAlgEquiv.refl ℝ ℂ
            else Complex.conjCAE :
            (a : ℂ) → ℂ)
          z) ≠
      0 ↔
    z.im ≠ 0
have neg : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
  (Complex.im ((Complex.conjCAE : (a : ℂ) → ℂ) z) ≠ 0 ↔ z.im ≠ 0)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
⊢ Eq (α := ℂ) ((σ (g * g') : (a : ℂ) → ℂ) z : ℂ) ((σ g : (a : ℂ) → ℂ) ((σ g' : (a : ℂ) → ℂ) z : ℂ) : ℂ)
have simp : Eq (α := ℂ)
  ((if
            0 <
              HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
          ContinuousAlgEquiv.refl ℝ ℂ
        else Complex.conjCAE :
        (a : ℂ) → ℂ)
      z :
    ℂ)
  ((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) ℝ) → ℝˣ) g') : ℝ) then
              ContinuousAlgEquiv.refl ℝ ℂ
            else Complex.conjCAE :
            (a : ℂ) → ℂ)
          z :
        ℂ) :
    ℂ)
Tactic: simp only [σ, map_mul, Units.val_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
⊢ Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have inl : ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0),
  Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
Tactic: rcases g.det_ne_zero.lt_or_gt with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
inl :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0),
    Eq (α := ℂ)
      ((if
                0 <
                  HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                    (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
              ContinuousAlgEquiv.refl ℝ ℂ
            else Complex.conjCAE :
            (a : ℂ) → ℂ)
          z :
        ℂ)
      ((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) ℝ) → ℝˣ) g') : ℝ) then
                  ContinuousAlgEquiv.refl ℝ ℂ
                else Complex.conjCAE :
                (a : ℂ) → ℂ)
              z :
            ℂ) :
        ℂ)
⊢ Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have inr : ∀ (h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det),
  Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
Tactic: rcases g.det_ne_zero.lt_or_gt with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have inl : ∀ (h' : (↑g' : Matrix (Fin 2) (Fin 2) ℝ).det < 0),
  Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
Tactic: rcases g'.det_ne_zero.lt_or_gt with (h' | h')
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
inl :
  ∀ (h' : (↑g' : Matrix (Fin 2) (Fin 2) ℝ).det < 0),
    Eq (α := ℂ)
      ((if
                0 <
                  HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                    (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
              ContinuousAlgEquiv.refl ℝ ℂ
            else Complex.conjCAE :
            (a : ℂ) → ℂ)
          z :
        ℂ)
      ((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) ℝ) → ℝˣ) g') : ℝ) then
                  ContinuousAlgEquiv.refl ℝ ℂ
                else Complex.conjCAE :
                (a : ℂ) → ℂ)
              z :
            ℂ) :
        ℂ)
⊢ Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have inl₁ : ∀ (h' : 0 < (↑g' : Matrix (Fin 2) (Fin 2) ℝ).det),
  Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
Tactic: rcases g'.det_ne_zero.lt_or_gt with (h' | h')
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
⊢ Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have inr : ∀ (h' : (↑g' : Matrix (Fin 2) (Fin 2) ℝ).det < 0),
  Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
Tactic: rcases g'.det_ne_zero.lt_or_gt with (h' | h')
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
inr :
  ∀ (h' : (↑g' : Matrix (Fin 2) (Fin 2) ℝ).det < 0),
    Eq (α := ℂ)
      ((if
                0 <
                  HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                    (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
              ContinuousAlgEquiv.refl ℝ ℂ
            else Complex.conjCAE :
            (a : ℂ) → ℂ)
          z :
        ℂ)
      ((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) ℝ) → ℝˣ) g') : ℝ) then
                  ContinuousAlgEquiv.refl ℝ ℂ
                else Complex.conjCAE :
                (a : ℂ) → ℂ)
              z :
            ℂ) :
        ℂ)
⊢ Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
have inr₁ : ∀ (h' : 0 < (↑g' : Matrix (Fin 2) (Fin 2) ℝ).det),
  Eq (α := ℂ)
    ((if
              0 <
                HMul.hMul (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
                  (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g') : ℝ) then
            ContinuousAlgEquiv.refl ℝ ℂ
          else Complex.conjCAE :
          (a : ℂ) → ℂ)
        z :
      ℂ)
    ((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) ℝ) → ℝˣ) g') : ℝ) then
                ContinuousAlgEquiv.refl ℝ ℂ
              else Complex.conjCAE :
              (a : ℂ) → ℂ)
            z :
          ℂ) :
      ℂ)
Tactic: rcases g'.det_ne_zero.lt_or_gt with (h' | h')
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g h : GL (Fin 2) ℝ
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 (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
Tactic: split_ifs