awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
G : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)
F : (z : ℂ) → ℂ := fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)
this : (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) = F ∘ G
⊢ AnalyticAt ℂ G (↑τ : ℂ)

Tactic:
exact τ.analyticAt_smul hg

Premises used: UpperHalfPlane.analyticAt_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
G : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)
F : (z : ℂ) → ℂ := fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)
this : (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) = F ∘ G
⊢ deriv G (↑τ : ℂ) ≠ 0

Tactic:
τ.deriv_smul_ne_zero hg

Premises used: UpperHalfPlane.deriv_smul_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
G : (z : ℂ) → ℂ := fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)
F : (z : ℂ) → ℂ := fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)
this : (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) = F ∘ G
⊢ deriv G (↑τ : ℂ) ≠ 0

Tactic:
exact τ.deriv_smul_ne_zero hg

Premises used: UpperHalfPlane.deriv_smul_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h :
  ∀ (x : ℂ),
    Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
      ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)
⊢ smulFDeriv (J * g) z = -(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
z x : ℂ
pos :
  ∀ (hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det),
    Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
      ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)
neg :
  ∀ (hg : ¬0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det),
    Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
      ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)
⊢ Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
    ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)

Tactic:
by_cases hg : 0 < g.val.det

Premises used: Units.val, Matrix.det
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
z x : ℂ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
⊢ Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
    ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)

Tactic:
simp [smulFDeriv, σ, hg, hg.not_gt, neg_div]

Premises used: neg_div, UpperHalfPlane.smulFDeriv, LT.lt.not_gt, UpperHalfPlane.σ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
z x : ℂ
hg : ¬0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
⊢ Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
    ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)

Tactic:
simp [smulFDeriv, σ, hg, g.det_ne_zero.lt_or_gt.resolve_right hg, neg_div]

Premises used: neg_div, Matrix.GeneralLinearGroup.det_ne_zero, UpperHalfPlane.smulFDeriv, UpperHalfPlane.σ, Or.resolve_right, Ne.lt_or_gt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
z : ℂ
inl :
  ∀ (h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0),
    ContinuousLinearMap.det
        ((↑(↑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
                    ContinuousAlgEquiv.refl ℝ ℂ
                  else Complex.conjCAE) :
                ℂ ≃L[ℝ] ℂ) :
            ℂ →L[ℝ] ℂ) ∘SL
          ContinuousLinearMap.restrictScalars ℝ
            (ContinuousLinearMap.toSpanSingleton ℂ
              ((↑(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) : ℂ) /
                HPow.hPow (β := ℕ) (denom g z) 2))) =
      (↑((SignType.sign : (a : ℝ) → SignType) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)) :
            ℝ) *
          HPow.hPow (α := ℝ) (β := ℕ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 2 /
        HPow.hPow (β := ℕ) ‖denom g z‖ 4
inr :
  ∀ (h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det),
    ContinuousLinearMap.det
        ((↑(↑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
                    ContinuousAlgEquiv.refl ℝ ℂ
                  else Complex.conjCAE) :
                ℂ ≃L[ℝ] ℂ) :
            ℂ →L[ℝ] ℂ) ∘SL
          ContinuousLinearMap.restrictScalars ℝ
            (ContinuousLinearMap.toSpanSingleton ℂ
              ((↑(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) : ℂ) /
                HPow.hPow (β := ℕ) (denom g z) 2))) =
      (↑((SignType.sign : (a : ℝ) → SignType) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)) :
            ℝ) *
          HPow.hPow (α := ℝ) (β := ℕ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 2 /
        HPow.hPow (β := ℕ) ‖denom g z‖ 4
⊢ ContinuousLinearMap.det
      ((↑(↑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
                  ContinuousAlgEquiv.refl ℝ ℂ
                else Complex.conjCAE) :
              ℂ ≃L[ℝ] ℂ) :
          ℂ →L[ℝ] ℂ) ∘SL
        ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton ℂ
            ((↑(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) : ℂ) /
              HPow.hPow (β := ℕ) (denom g z) 2))) =
    (↑((SignType.sign : (a : ℝ) → SignType) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)) : ℝ) *
        HPow.hPow (α := ℝ) (β := ℕ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 2 /
      HPow.hPow (β := ℕ) ‖denom g z‖ 4

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.Manifold
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ ContinuousLinearMap.det
      ((↑(↑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
                  ContinuousAlgEquiv.refl ℝ ℂ
                else Complex.conjCAE) :
              ℂ ≃L[ℝ] ℂ) :
          ℂ →L[ℝ] ℂ) ∘SL
        ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton ℂ
            ((↑(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) : ℂ) /
              HPow.hPow (β := ℕ) (denom g z) 2))) =
    (↑((SignType.sign : (a : ℝ) → SignType) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)) : ℝ) *
        HPow.hPow (α := ℝ) (β := ℕ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 2 /
      HPow.hPow (β := ℕ) ‖denom g z‖ 4

Tactic:
simp [h.not_gt, ContinuousLinearMap.det, LinearMap.det_restrictScalars,
      Algebra.norm_complex_eq, Complex.normSq_eq_norm_sq, ← pow_mul, sign_neg h, neg_div]

Premises used: neg_div, Complex.normSq_eq_norm_sq, ContinuousLinearMap.det, Algebra.norm_complex_eq, pow_mul, LinearMap.det_restrictScalars, sign_neg, LT.lt.not_gt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
⊢ ContinuousLinearMap.det
      ((↑(↑(if LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) then
                  ContinuousAlgEquiv.refl ℝ ℂ
                else Complex.conjCAE) :
              ℂ ≃L[ℝ] ℂ) :
          ℂ →L[ℝ] ℂ) ∘SL
        ContinuousLinearMap.restrictScalars ℝ
          (ContinuousLinearMap.toSpanSingleton ℂ
            ((↑(↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) : ℂ) /
              HPow.hPow (β := ℕ) (denom g z) 2))) =
    (↑((SignType.sign : (a : ℝ) → SignType) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)) : ℝ) *
        HPow.hPow (α := ℝ) (β := ℕ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 2 /
      HPow.hPow (β := ℕ) ‖denom g z‖ 4

Tactic:
simp [ContinuousLinearMap.det, h, LinearMap.det_restrictScalars,
      Algebra.norm_complex_eq, Complex.normSq_eq_norm_sq, ← pow_mul]

Premises used: Complex.normSq_eq_norm_sq, ContinuousLinearMap.det, Algebra.norm_complex_eq, pow_mul, LinearMap.det_restrictScalars
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
inr :
  ∀
    (this :
      ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
        HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ))
    (hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
wlog :
  ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)

Tactic:
wlog hg : 0 < g.det.val generalizing g

Premises used: Units.val, Matrix.GeneralLinearGroup.det, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0

Tactic:
replace hg := g.det.ne_zero.lt_or_gt.resolve_right hg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
⊢ LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) (J * g)) : ℝ)

Tactic:
simpa
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
h :
  ∀ (x : ℂ),
    (↑(g • (↑ofComplex : ℂ → ℍ) x) : ℂ) = (-(⇑Complex.conjCLE : (a : ℂ) → ℂ)) (↑((J * g) • (↑ofComplex : ℂ → ℍ) x) : ℂ)
h₁ :
  Complex.addCommGroup = NormedAddCommGroup.toAddCommGroup →
    HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule →
      smulFDeriv g (↑τ : ℂ) = (-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ)) ∘SL smulFDeriv (J * g) (↑τ : ℂ)
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)

Tactic:
convert! Complex.conjCLE.hasStrictFDerivAt.neg.comp _ (this (J * g) (by simpa))

Premises used: HMul.hMul, HasStrictFDerivAt.neg, ContinuousLinearEquiv.hasStrictFDerivAt, Complex.conjCLE, HasStrictFDerivAt.comp, UpperHalfPlane.J
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
x : ℂ
⊢ (↑(g • (↑ofComplex : ℂ → ℍ) x) : ℂ) = (-(⇑Complex.conjCLE : (a : ℂ) → ℂ)) (↑((J * g) • (↑ofComplex : ℂ → ℍ) x) : ℂ)

Tactic:
simp [mul_smul, coe_J_smul]

Premises used: UpperHalfPlane.coe_J_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
e_4 : Complex.addCommGroup = NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule
h :
  ∀ (x : ℂ),
    Eq (α := ℂ) ((smulFDeriv g (↑τ : ℂ) : (a : ℂ) → ℂ) x : ℂ)
      (((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ)) ∘SL smulFDeriv (J * g) (↑τ : ℂ) : (a : ℂ) → ℂ) x : ℂ)
⊢ smulFDeriv g (↑τ : ℂ) = (-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ)) ∘SL smulFDeriv (J * g) (↑τ : ℂ)

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ) (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
hg : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
e_4 : Complex.addCommGroup = NormedAddCommGroup.toAddCommGroup
e_5 : HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule
x : ℂ
⊢ Eq (α := ℂ) ((smulFDeriv g (↑τ : ℂ) : (a : ℂ) → ℂ) x : ℂ)
    (((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ)) ∘SL smulFDeriv (J * g) (↑τ : ℂ) : (a : ℂ) → ℂ) x : ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
τ : ℍ
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ))
    (ContinuousLinearMap.restrictScalars ℝ
      (ContinuousLinearMap.toSpanSingleton ℂ
        ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2)))
    (↑τ : ℂ)

Tactic:
have := (hasStrictDerivAt_smul hg τ).hasStrictFDerivAt.restrictScalars ℝ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
τ : ℍ
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
this :
  HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ))
    (ContinuousLinearMap.restrictScalars ℝ
      (ContinuousLinearMap.toSpanSingleton ℂ
        ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2)))
    (↑τ : ℂ)
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)

Tactic:
simp_all [smulFDeriv, σ]

Premises used: UpperHalfPlane.smulFDeriv, UpperHalfPlane.σ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure
Goal:
⊢ BorelSpace ℍ

Tactic:
⟨borel_comap.symm⟩

Premises used: BorelSpace.mk, Eq.symm, borel_comap
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure
Goal:
⊢ MeasurableEmbedding UpperHalfPlane.coe

Tactic:
isOpenEmbedding_coe.measurableEmbedding

Premises used: UpperHalfPlane.isOpenEmbedding_coe, Topology.IsOpenEmbedding.measurableEmbedding
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure
Goal:
⊢ Measurable UpperHalfPlane.coe

Tactic:
measurableEmbedding_coe.measurable

Premises used: UpperHalfPlane.measurableEmbedding_coe, MeasurableEmbedding.measurable
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure
Goal:
⊢ Eq (α := Measure ℍ) volume
    (Measure.withDensity (Measure.comap UpperHalfPlane.coe volume) fun (z : ℍ) ↦
      (↑(HPow.hPow (β := ℕ) (1 / NNReal.mk z.im ⋯) 2) : ENNReal))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure
Goal:
⊢ IsFiniteMeasureOnCompacts (m0 := instMeasurableSpace) (Measure.comap UpperHalfPlane.coe volume)

Tactic:
.comap' _ continuous_coe measurableEmbedding_coe

Premises used: MeasureTheory.IsFiniteMeasureOnCompacts.comap', UpperHalfPlane.measurableEmbedding_coe, UpperHalfPlane.continuous_coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure
Goal:
⊢ IsLocallyFiniteMeasure (m0 := instMeasurableSpace) (Measure.comap UpperHalfPlane.coe volume)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure
Goal:
⊢ SigmaFinite (m0 := instMeasurableSpace) (Measure.comap UpperHalfPlane.coe volume)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure
Goal:
⊢ SFinite (m0 := instMeasurableSpace) (Measure.comap UpperHalfPlane.coe volume)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ dist z w = 2 * arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
rw :
  sinh (2 * arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))) / 2) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
rw₁ : sinh (arsinh (dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)))) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
rw₂ rw₃ : dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))
⊢ sinh (dist z w / 2) = dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im))

Tactic:
rw [dist_eq, mul_div_cancel_left₀ (arsinh _) two_ne_zero, sinh_arsinh]

Premises used: Real.sinh_arsinh, mul_div_cancel_left₀, UpperHalfPlane.dist_eq, Real.arsinh, two_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
rw :
  (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2) /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2 /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im))
rw₁ : 0 ≤ z.im * w.im
rw₂ : HPow.hPow (β := ℕ) (2 * √(z.im * w.im)) 2 ≠ 0
ha : 0 ≤ cosh (dist z w / 2)
hb : 0 ≤ dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
⊢ cosh (dist z w / 2) = dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))

Tactic:
rw [← sq_eq_sq₀, cosh_sq', sinh_half_dist, div_pow, div_pow, one_add_div, mul_pow, sq_sqrt]

Premises used: Real.sq_sqrt, div_pow, Real.cosh_sq', one_add_div, UpperHalfPlane.sinh_half_dist, sq_eq_sq₀, mul_pow
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
e_a :
  HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2
⊢ (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2) /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im)) =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2 /
      (HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im))

Tactic:
congr 1
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
e_a :
  HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) +
      (HAdd.hAdd (α := ℝ) (β := ℝ) ((Complex.normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
          ((Complex.normSq : (a : ℂ) → ℝ) (↑w : ℂ) : ℝ) -
        2 * ((↑z : ℂ).re * (↑w : ℂ).re - z.im * -w.im)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((Complex.normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
        ((Complex.normSq : (a : ℂ) → ℝ) (↑w : ℂ) : ℝ) -
      2 * ((↑z : ℂ).re * (↑w : ℂ).re - z.im * w.im)
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 =
    HPow.hPow (β := ℕ) (dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) 2

Tactic:
simp only [Complex.dist_eq, Complex.sq_norm, Complex.normSq_sub, Complex.normSq_conj,
      Complex.conj_conj, Complex.mul_re, Complex.conj_re, Complex.conj_im, coe_im]

Premises used: Complex.mul_re, Complex.sq_norm, Complex.normSq_sub, Complex.conj_im, Complex.normSq_conj, Complex.dist_eq, Complex.conj_re, Complex.conj_conj, UpperHalfPlane.coe_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 * (z.im * w.im) +
      (HAdd.hAdd (α := ℝ) (β := ℝ) ((Complex.normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
          ((Complex.normSq : (a : ℂ) → ℝ) (↑w : ℂ) : ℝ) -
        2 * ((↑z : ℂ).re * (↑w : ℂ).re - z.im * -w.im)) =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((Complex.normSq : (a : ℂ) → ℝ) (↑z : ℂ) : ℝ)
        ((Complex.normSq : (a : ℂ) → ℝ) (↑w : ℂ) : ℝ) -
      2 * ((↑z : ℂ).re * (↑w : ℂ).re - z.im * w.im)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ 0 ≤ z.im * w.im

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ HPow.hPow (β := ℕ) (2 * √(z.im * w.im)) 2 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ 0 ≤ dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
rw : 2 * √(z.im * w.im) ≠ 0
⊢ tanh (dist z w / 2) = dist (↑z : ℂ) (↑w : ℂ) / dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))

Tactic:
rw [tanh_eq_sinh_div_cosh, sinh_half_dist, cosh_half_dist, div_div_div_comm, div_self, div_one]

Premises used: Real.tanh_eq_sinh_div_cosh, div_div_div_comm, UpperHalfPlane.cosh_half_dist, UpperHalfPlane.sinh_half_dist, div_one, div_self
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ 2 * √(z.im * w.im) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
rw :
  sinh (dist z w / 2) + cosh (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
rw₁ :
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) + cosh (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
rw₂ :
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) +
      dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im)) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))
rw₃ rw₄ :
  dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) +
      dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im)) =
    dist (↑z : ℂ) (↑w : ℂ) / (2 * √(z.im * w.im)) +
      dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ)) / (2 * √(z.im * w.im))
⊢ rexp (dist z w / 2) =
    (dist (↑z : ℂ) (↑w : ℂ) + dist (↑z : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑w : ℂ))) / (2 * √(z.im * w.im))

Tactic:
rw [← sinh_add_cosh, sinh_half_dist, cosh_half_dist, add_div]

Premises used: UpperHalfPlane.cosh_half_dist, Real.sinh_add_cosh, UpperHalfPlane.sinh_half_dist, add_div
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
hc : Ne (α := ℝ) 2 0
rw : 0 ≤ z.im * w.im
⊢ cosh (dist z w) = 1 + HPow.hPow (β := ℕ) (dist (↑z : ℂ) (↑w : ℂ)) 2 / (2 * z.im * w.im)

Tactic:
rw [dist_eq, cosh_two_mul, cosh_sq', add_assoc, ← two_mul, sinh_arsinh, div_pow, mul_pow,
    sq_sqrt, sq (2 : ℝ), mul_assoc, ← mul_div_assoc, mul_assoc, mul_div_mul_left]

Premises used: add_assoc, mul_assoc, mul_div_assoc, two_mul, Real.sinh_arsinh, Real.sq_sqrt, sq, UpperHalfPlane.dist_eq, div_pow, mul_div_mul_left, Real.cosh_sq', OfNat.ofNat, mul_pow, Real.cosh_two_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric
Goal:
z w : ℍ
⊢ Ne (α := ℝ) 2 0

Tactic:
positivity