awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
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) : ℂ)) :
        ℝ)
⊢ (num g z / denom g z).im =
    HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * z.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ)

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]

Premises used: Complex.mul_im, Units.val, Complex.add_im, Complex.mul_re, sub_zero, MulZeroClass.zero_mul, Complex.div_im, Complex.add_re, sub_div, UpperHalfPlane.denom, Complex.ofReal_re, Complex.ofReal_im, Matrix.det_fin_two, add_zero, UpperHalfPlane.num, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ 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:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 : ℂ) : ℂ)
neg :
  ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    Eq (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((Complex.conjCAE : (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 :
          ℂ) :
      ℂ)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ Eq (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ Eq (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ) : ℂ)
    ((starRingEnd ℂ : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
y : ℝ
pos :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (↑y : ℂ) = (↑y : ℂ)
neg :
  ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    (Complex.conjCAE : (a : ℂ) → ℂ) (↑y : ℂ) = (↑y : ℂ)
⊢ (if LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then ContinuousAlgEquiv.refl ℝ ℂ
        else Complex.conjCAE :
        (a : ℂ) → ℂ)
      (↑y : ℂ) =
    (↑y : ℂ)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
y : ℝ
h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (↑y : ℂ) = (↑y : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
y : ℝ
h : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ (Complex.conjCAE : (a : ℂ) → ℂ) (↑y : ℂ) = (↑y : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
⊢ (σ g : (a : ℂ) → ℂ) (num h z) = num h ((σ g : (a : ℂ) → ℂ) z)

Tactic:
simp [num]

Premises used: UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
⊢ (σ g : (a : ℂ) → ℂ) (denom h z) = denom h ((σ g : (a : ℂ) → ℂ) z)

Tactic:
simp [denom]

Premises used: UpperHalfPlane.denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
⊢ σ (-g) = σ g

Tactic:
simp [σ, det_neg]

Premises used: Matrix.det_neg, UpperHalfPlane.σ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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
neg :
  ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    (Complex.conjCAE : (a : ℂ) → ℂ) ((Complex.conjCAE : (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

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) = z

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ (Complex.conjCAE : (a : ℂ) → ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) = z

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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)
neg :
  ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    (Complex.im ((Complex.conjCAE : (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

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ Complex.im ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z) ≠ 0 ↔ z.im ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ Complex.im ((Complex.conjCAE : (a : ℂ) → ℂ) z) ≠ 0 ↔ z.im ≠ 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
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 :
          ℂ) :
      ℂ)
⊢ Eq (α := ℂ) ((σ (g * g') : (a : ℂ) → ℂ) z : ℂ) ((σ g : (a : ℂ) → ℂ) ((σ g' : (a : ℂ) → ℂ) z : ℂ) : ℂ)

Tactic:
simp only [σ, map_mul, Units.val_mul]

Premises used: map_mul, UpperHalfPlane.σ, Units.val_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 :
            ℂ) :
        ℂ)
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 :
            ℂ) :
        ℂ)
⊢ 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)

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 :
            ℂ) :
        ℂ)
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 :
            ℂ) :
        ℂ)
⊢ 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')

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 :
            ℂ) :
        ℂ)
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 :
            ℂ) :
        ℂ)
⊢ 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')

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
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:
simp [mul_pos_of_neg_of_neg h h', h.not_gt, h'.not_gt]

Premises used: LT.lt.not_gt, mul_pos_of_neg_of_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
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:
simp [(mul_neg_of_neg_of_pos h h').not_gt, h.not_gt, h']

Premises used: mul_neg_of_neg_of_pos, LT.lt.not_gt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
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:
simp [(mul_neg_of_pos_of_neg h h').not_gt, h, h'.not_gt]

Premises used: LT.lt.not_gt, mul_neg_of_pos_of_neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
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:
simp [mul_pos h h', h, h']

Premises used: mul_pos