awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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 : ℂ) : ℂ)
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 : ℂ) : ℂ)
⊢ 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 :
          ℂ) :
      ℂ)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
h_1 : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
h_2 : 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:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
h_1 : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
h_2 : ¬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:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
h_1 : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
h_2 : 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:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℂ
h_1 : ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
h_2 : ¬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:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℂ
pos :
  LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    norm (E := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) z : ℂ) = ‖z‖
neg :
  ¬LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) →
    norm (E := ℂ) ((Complex.conjCAE : (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‖

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) : ℝ)
⊢ norm (E := ℂ) ((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) : ℝ)
⊢ norm (E := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) z : ℂ) = ‖z‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
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) : ℝ)
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) : ℝ)
⊢ 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) : ℝ)

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 :
  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 ((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]

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 :
  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) : ℝ)
⊢ 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)]

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) : ℝ)),
    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) : ℝ)
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) : ℝ)
⊢ 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) : ℝ)

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 : ℂ
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:
simpa only [Complex.conjCAE_apply, Complex.star_def, Complex.conj_im,
    neg_mul, neg_div, neg_inj] using moebius_im g z

Premises used: Complex.star_def, neg_div, UpperHalfPlane.moebius_im, Complex.conjCAE_apply, Complex.conj_im, neg_inj, neg_mul
-- 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 : ℂ) → ℂ) (num g z / denom g z)) =
    HDiv.hDiv (β := ℝ) (-(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) * z.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g z) : ℝ)

Tactic:
simpa only [Complex.conjCAE_apply, Complex.star_def, Complex.conj_im,
    neg_mul, neg_div, neg_inj] using moebius_im g z

Premises used: Complex.star_def, neg_div, UpperHalfPlane.moebius_im, Complex.conjCAE_apply, Complex.conj_im, neg_inj, neg_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
rw :
  0 <
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)
⊢ 0 < (smulAux' g (↑z : ℂ)).im

Tactic:
rw [smulAux'_im]

Premises used: UpperHalfPlane.smulAux'_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ 0 <
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)

Tactic:
div_pos (mul_pos (abs_pos.mpr g.det.ne_zero) z.im_pos) (normSq_denom_pos _ z.im_ne_zero)

Premises used: Iff.mpr, UpperHalfPlane.im_pos, UpperHalfPlane.im_ne_zero, Units.ne_zero, UpperHalfPlane.normSq_denom_pos, abs_pos, mul_pos, div_pos, Matrix.GeneralLinearGroup.det, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
z : ℍ
⊢ 0 <
    HDiv.hDiv (β := ℝ) (|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)| * (↑z : ℂ).im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom g (↑z : ℂ)) : ℝ)

Tactic:
exact div_pos (mul_pos (abs_pos.mpr g.det.ne_zero) z.im_pos) (normSq_denom_pos _ z.im_ne_zero)

Premises used: Iff.mpr, UpperHalfPlane.im_pos, UpperHalfPlane.im_ne_zero, Units.ne_zero, UpperHalfPlane.normSq_denom_pos, abs_pos, mul_pos, div_pos, Matrix.GeneralLinearGroup.det, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
simp : denom (g * h) (↑z : ℂ) = denom g (num h (↑z : ℂ) / denom h (↑z : ℂ)) * denom h (↑z : ℂ)
⊢ denom (g * h) (↑z : ℂ) =
    HMul.hMul (α := ℂ) ((σ h : (a : ℂ) → ℂ) (denom g (↑(smulAux h z) : ℂ)) : ℂ) (denom h (↑z : ℂ))

Tactic:
simp only [smulAux, smulAux', coe_mk, map_div₀, σ_num, σ_denom, σ_sq]

Premises used: UpperHalfPlane.σ_sq, UpperHalfPlane.smulAux, UpperHalfPlane.σ_num, UpperHalfPlane.smulAux', map_div₀, UpperHalfPlane.coe_mk, UpperHalfPlane.σ_denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
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) : ℂ)
⊢ 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 : ℂ)

Tactic:
field_simp [denom_ne_zero h z]

Premises used: UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
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) : ℂ)
⊢ 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:
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]

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 : ℍ
⊢ ((↑((↑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:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
coe : (↑(smulAux (g * h) z) : ℂ) = (↑(smulAux g (smulAux h z)) : ℂ)
⊢ smulAux (g * h) z = smulAux g (smulAux h z)

Tactic:
ext : 1
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
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 : ℂ) : ℂ)))
⊢ (↑(smulAux (g * h) z) : ℂ) = (↑(smulAux g (smulAux h z)) : ℂ)

Tactic:
simp only [smulAux, coe_mk, smulAux', map_div₀, σ_num, σ_denom, σ_mul]

Premises used: UpperHalfPlane.smulAux, UpperHalfPlane.σ_mul, UpperHalfPlane.σ_num, UpperHalfPlane.smulAux', map_div₀, UpperHalfPlane.coe_mk, UpperHalfPlane.σ_denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
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)
⊢ 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:
generalize hu : σ g (σ h z) = u

Premises used: UpperHalfPlane.coe, UpperHalfPlane.σ, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu : (σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) = u
⊢ u.im ≠ 0

Tactic:
simpa only [← hu, σ_im_ne_zero] using z.im_ne_zero

Premises used: UpperHalfPlane.im_ne_zero, UpperHalfPlane.σ_im_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu : (σ g : (a : ℂ) → ℂ) ((σ h : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) = u
⊢ u.im ≠ 0

Tactic:
have hu : u.im ≠ 0 := by simpa only [← hu, σ_im_ne_zero] using z.im_ne_zero
-- 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
rw :
  HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) * u.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom h u) : ℝ) ≠
    0
⊢ (num h u / denom h u).im ≠ 0

Tactic:
rw [moebius_im]

Premises used: UpperHalfPlane.moebius_im
-- 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
⊢ HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) * u.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom h u) : ℝ) ≠
    0

Tactic:
div_ne_zero (mul_ne_zero h.det_ne_zero hu) (normSq_denom_ne_zero _ hu)

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, div_ne_zero, UpperHalfPlane.normSq_denom_ne_zero, mul_ne_zero
-- 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
⊢ HDiv.hDiv (β := ℝ) ((↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ) * u.im)
      ((Complex.normSq : (a : ℂ) → ℝ) (denom h u) : ℝ) ≠
    0

Tactic:
exact div_ne_zero (mul_ne_zero h.det_ne_zero hu) (normSq_denom_ne_zero _ hu)

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, div_ne_zero, UpperHalfPlane.normSq_denom_ne_zero, mul_ne_zero
-- 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
⊢ (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)
-- 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 :
  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
⊢ 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:
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]

Premises used: mul_div, UpperHalfPlane.denom_ne_zero_of_im, div_add', div_eq_div_iff, UpperHalfPlane.denom
-- 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 :
  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
⊢ 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

Tactic:
rw [mul_div, div_add' _ _ _ (denom_ne_zero_of_im _ hu), div_mul_eq_mul_div]

Premises used: mul_div, UpperHalfPlane.denom_ne_zero_of_im, div_add', div_mul_eq_mul_div
-- 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 :
  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
⊢ 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:
congr 1