awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
⊢ MDiff fun (τ : ℍ) ↦ (denom g (↑τ : ℂ))⁻¹

Tactic:
(contMDiff_inv_denom g).mdifferentiable one_ne_zero

Premises used: UpperHalfPlane.contMDiff_inv_denom, ContMDiff.mdifferentiable, one_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ MDiff fun (τ : ℍ) ↦ g • τ

Tactic:
(contMDiff_smul hg).mdifferentiable one_ne_zero

Premises used: ContMDiff.mdifferentiable, one_ne_zero, UpperHalfPlane.contMDiff_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : MDiff f
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
rw :
  ∀ (hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}) {τ : ℍ}
    (hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0), f = 0
⊢ f = 0

Tactic:
rw [mdifferentiable_iff] at hf

Premises used: UpperHalfPlane.mdifferentiable_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}

Tactic:
have := hf.analyticOnNhd isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
h : ∀ (w : ℍ), f w = 0 w
⊢ f = 0

Tactic:
ext w
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
⊢ (f ∘ (↑ofComplex : ℂ → ℍ)) (↑w : ℂ) = 0 (↑w : ℂ)

Tactic:
this.eqOn_zero_of_preconnected_of_frequently_eq_zero (z₀ := ↑τ) ?_ τ.2 ?_ w.im_pos

Premises used: UpperHalfPlane.im_pos, AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
h : f w = (f ∘ (↑ofComplex : ℂ → ℍ)) (↑w : ℂ)
h₁ : IsPreconnected (α := ℂ) {z : ℂ | 0 < z.im}
h₂ : ∃ᶠ (z : ℂ) in 𝓝[≠] (↑τ : ℂ), (f ∘ (↑ofComplex : ℂ → ℍ)) z = 0
⊢ f w = 0 w

Tactic:
convert! this.eqOn_zero_of_preconnected_of_frequently_eq_zero (z₀ := ↑τ) ?_ τ.2 ?_ w.im_pos

Premises used: UpperHalfPlane.im_pos, AnalyticOnNhd.eqOn_zero_of_preconnected_of_frequently_eq_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
h : f w = f ((↑ofComplex : ℂ → ℍ) (↑w : ℂ))
h₁ h₂ : f w = f w
⊢ f w = (f ∘ (↑ofComplex : ℂ → ℍ)) (↑w : ℂ)

Tactic:
rw [Function.comp_apply, ofComplex_apply]

Premises used: UpperHalfPlane.ofComplex_apply, Function.comp_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
⊢ Subset (α := Set ℂ) {z : ℂ | 0 < z.im} {z : ℂ | 0 ≤ z.im}

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
⊢ IsPreconnected (α := ℂ) {z : ℂ | 0 < z.im}

Tactic:
exact (Complex.isConnected_of_upperHalfPlane subset_rfl (by grind)).isPreconnected

Premises used: Complex.isConnected_of_upperHalfPlane, IsConnected.isPreconnected, subset_rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
h : ∀ (hτ : ∀ᶠ (x : ℂ) in 𝓝[≠] (↑τ : ℂ), (f ∘ (↑ofComplex : ℂ → ℍ)) x ≠ 0), ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] (↑τ : ℂ), (f ∘ (↑ofComplex : ℂ → ℍ)) z = 0

Tactic:
contrapose! hτ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (x : ℂ) in 𝓝[≠] (↑τ : ℂ), (f ∘ (↑ofComplex : ℂ → ℍ)) x ≠ 0
⊢ ∀ᶠ (a : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℂ) {(↑τ : ℂ)}ᶜ (↑a : ℂ) → (f ∘ (↑ofComplex : ℂ → ℍ)) (↑a : ℂ) ≠ 0

Tactic:
rw [eventually_nhdsWithin_iff, ← isOpenEmbedding_coe.map_nhds_eq, eventually_map] at hτ

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, UpperHalfPlane.isOpenEmbedding_coe, Filter.eventually_map, eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℂ) {(↑τ : ℂ)}ᶜ (↑a : ℂ) → (f ∘ (↑ofComplex : ℂ → ℍ)) (↑a : ℂ) ≠ 0
h : ∀ᶠ (x : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℍ) {τ}ᶜ x → f x ≠ 0
⊢ ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0

Tactic:
rw [eventually_nhdsWithin_iff]

Premises used: eventually_nhdsWithin_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℂ) {(↑τ : ℂ)}ᶜ (↑a : ℂ) → (f ∘ (↑ofComplex : ℂ → ℍ)) (↑a : ℂ) ≠ 0
h :
  ∀ (a : ℍ) (ha : Membership.mem (γ := Set ℂ) {(↑τ : ℂ)}ᶜ (↑a : ℂ) → (f ∘ (↑ofComplex : ℂ → ℍ)) (↑a : ℂ) ≠ 0),
    Membership.mem (γ := Set ℍ) {τ}ᶜ a → f a ≠ 0
⊢ ∀ᶠ (x : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℍ) {τ}ᶜ x → f x ≠ 0

Tactic:
filter_upwards [hτ] with a ha
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℂ) {(↑τ : ℂ)}ᶜ (↑a : ℂ) → (f ∘ (↑ofComplex : ℂ → ℍ)) (↑a : ℂ) ≠ 0
a : ℍ
ha : Membership.mem (γ := Set ℂ) {(↑τ : ℂ)}ᶜ (↑a : ℂ) → (f ∘ (↑ofComplex : ℂ → ℍ)) (↑a : ℂ) ≠ 0
⊢ Membership.mem (γ := Set ℍ) {τ}ᶜ a → f a ≠ 0

Tactic:
simpa using ha
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f g : ℍ → ℂ
hf : MDiff f
hg : MDiff g
hfg : f * g = 0
⊢ ∀ (x : ℍ), f x = 0 ∨ g x = 0

Tactic:
simpa using congrFun hfg

Premises used: congrFun
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f g : ℍ → ℂ
hf : MDiff f
hg : MDiff g
⊢ f = 0 ∨ g = 0 → f * g = 0

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
⊢ Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0 ↔ ∃ i ∈ s, f i = 0

Tactic:
⟨fun h0 ↦ ?_, fun ⟨i, hi, hi'⟩ ↦ Finset.prod_eq_zero hi hi'⟩

Premises used: Finset.prod, _private.0.UpperHalfPlane.prod_eq_zero_iff.match_1, Iff.intro, Finset.prod_eq_zero, OfNat.ofNat, Eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
refine : ∀ (h0 : Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0), ∃ i ∈ s, f i = 0
⊢ Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0 ↔ ∃ i ∈ s, f i = 0

Tactic:
refine ⟨fun h0 ↦ ?_, fun ⟨i, hi, hi'⟩ ↦ Finset.prod_eq_zero hi hi'⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0
⊢ ∀ (x : ℍ), Eq (α := ℂ) (∏ i ∈ s, f i x) 0

Tactic:
simpa using congrFun h0

Premises used: congrFun
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0
⊢ ∃ᶠ (τ : ℍ) in 𝓝[≠] I, Eq (α := ℂ) (∏ i ∈ s, f i τ) 0

Tactic:
have : ∃ᶠ τ in 𝓝[≠] I, ∏ i ∈ s, f i τ = 0 := .of_forall <| by simpa using congrFun h0
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0
this : ∃ᶠ (τ : ℍ) in 𝓝[≠] I, Eq (α := ℂ) (∏ i ∈ s, f i τ) 0
⊢ ∃ i ∈ s, ∃ᶠ (x : ℍ) in 𝓝[≠] I, f i x = 0

Tactic:
simp only [Finset.prod_eq_zero_iff, Finset.frequently_exists] at this

Premises used: Finset.frequently_exists, Finset.prod_eq_zero_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0
this : ∃ i ∈ s, ∃ᶠ (x : ℍ) in 𝓝[≠] I, f i x = 0
⊢ ∃ i ∈ s, f i = 0

Tactic:
this.imp fun i hi ↦ ⟨hi.1, eq_zero_of_frequently (hf i hi.1) hi.2⟩

Premises used: Exists.imp, UpperHalfPlane.eq_zero_of_frequently, And.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0
this : ∃ i ∈ s, ∃ᶠ (x : ℍ) in 𝓝[≠] I, f i x = 0
⊢ ∃ i ∈ s, f i = 0

Tactic:
exact this.imp fun i hi ↦ ⟨hi.1, eq_zero_of_frequently (hf i hi.1) hi.2⟩

Premises used: Exists.imp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
this :
  HasStrictDerivAt (num g / denom g)
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)
⊢ HasStrictDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ))
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)

Tactic:
this.congr_of_eventuallyEq ?_

Premises used: HasStrictDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
this :
  HasStrictDerivAt (num g / denom g)
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)
refine : num g / denom g =ᶠ[𝓝 (↑τ : ℂ)] fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)
⊢ HasStrictDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ))
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)

Tactic:
refine this.congr_of_eventuallyEq ?_

Premises used: HasStrictDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
this :
  HasStrictDerivAt (num g / denom g)
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)
rw :
  (num g / denom g) ∘ UpperHalfPlane.coe =ᶠ[𝓝 τ]
    (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) ∘ UpperHalfPlane.coe
⊢ num g / denom g =ᶠ[𝓝 (↑τ : ℂ)] fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)

Tactic:
rw [← isOpenEmbedding_coe.map_nhds_eq, eventuallyEq_map]

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, UpperHalfPlane.isOpenEmbedding_coe, Filter.eventuallyEq_map
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
this :
  HasStrictDerivAt (num g / denom g)
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)
⊢ (num g / denom g) ∘ UpperHalfPlane.coe =ᶠ[𝓝 τ]
    (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) ∘ UpperHalfPlane.coe

Tactic:
simp [Function.comp_def, coe_smul_of_det_pos hg]

Premises used: UpperHalfPlane.coe_smul_of_det_pos, Function.comp_def
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
suffices :
  HasStrictDerivAt (num g / denom g)
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)
⊢ HasStrictDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ))
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)

Tactic:
suffices HasStrictDerivAt (num g / denom g) (g.val.det / denom g τ ^ 2) τ by
    refine this.congr_of_eventuallyEq ?_
    rw [← isOpenEmbedding_coe.map_nhds_eq, eventuallyEq_map]
    simp [Function.comp_def, coe_smul_of_det_pos hg]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ HasStrictDerivAt
    (HDiv.hDiv (α := ℂ → ℂ)
      (fun (x : ℂ) ↦ (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * id x + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ))
      fun (x : ℂ) ↦ (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * id x + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))
    (((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * 1 *
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) -
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) *
          ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * 1)) /
      HPow.hPow (β := ℕ)
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) 2)
    (↑τ : ℂ)

Tactic:
((hasStrictDerivAt_id (τ : ℂ)).const_mul _ |>.add_const _).div
      ((hasStrictDerivAt_id (τ : ℂ)).const_mul _ |>.add_const _) _

Premises used: UpperHalfPlane.coe, HasStrictDerivAt.div, HasStrictDerivAt.const_mul, HasStrictDerivAt.add_const, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
h :
  (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * 1 *
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) -
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) *
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * 1)
convert_5 :
  (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) ≠ 0
⊢ HasStrictDerivAt (num g / denom g)
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)

Tactic:
convert!
    ((hasStrictDerivAt_id (τ : ℂ)).const_mul _ |>.add_const _).div
      ((hasStrictDerivAt_id (τ : ℂ)).const_mul _ |>.add_const _) _ using 2

Premises used: UpperHalfPlane.coe, HasStrictDerivAt.div, HasStrictDerivAt.const_mul, HasStrictDerivAt.add_const, hasStrictDerivAt_id
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
h :
  (↑((↑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) : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) *
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) -
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) *
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
⊢ (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * 1 *
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) -
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) *
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * 1)

Tactic:
simp [Matrix.det_fin_two]

Premises used: Matrix.det_fin_two
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ (↑((↑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) : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) *
        ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)) -
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) *
        (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) ≠ 0

Tactic:
apply denom_ne_zero

Premises used: UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ deriv (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (↑τ : ℂ) =
    (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2

Tactic:
hasStrictDerivAt_smul hg τ |>.hasDerivAt |>.deriv

Premises used: HasDerivAt.deriv, UpperHalfPlane.hasStrictDerivAt_smul, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
rw : (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0
⊢ Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (↑τ : ℂ)) 0

Tactic:
rw [deriv_smul hg]

Premises used: UpperHalfPlane.deriv_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
ha : (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) ≠ 0
hb : HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0
⊢ (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0

Tactic:
apply div_ne_zero

Premises used: div_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) ≠ 0

Tactic:
exact_mod_cast hg.ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0

Tactic:
pow_ne_zero _ (denom_ne_zero g τ)

Premises used: pow_ne_zero, UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0

Tactic:
exact pow_ne_zero _ (denom_ne_zero g τ)

Premises used: pow_ne_zero, UpperHalfPlane.denom_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (↑τ : ℂ)

Tactic:
DifferentiableOn.analyticAt (fun z hz ↦ ?_) (isOpen_upperHalfPlaneSet.mem_nhds τ.im_pos)

Premises used: UpperHalfPlane.im_pos, IsOpen.mem_nhds, DifferentiableOn.analyticAt, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
refine :
  ∀ (z : ℂ) (hz : z ∈ upperHalfPlaneSet),
    DifferentiableWithinAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) upperHalfPlaneSet z
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (↑τ : ℂ)

Tactic:
refine DifferentiableOn.analyticAt (fun z hz ↦ ?_) (isOpen_upperHalfPlaneSet.mem_nhds τ.im_pos)

Premises used: UpperHalfPlane.im_pos, IsOpen.mem_nhds, DifferentiableOn.analyticAt, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
z : ℂ
hz : z ∈ upperHalfPlaneSet
h : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) z
⊢ DifferentiableWithinAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) upperHalfPlaneSet z

Tactic:
apply DifferentiableAt.differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
z : ℂ
hz : z ∈ upperHalfPlaneSet
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) z

Tactic:
simpa [mdifferentiableAt_iff] using
    (mdifferentiable_coe.comp <| (mdifferentiable_smul hg)).mdifferentiableAt (x := ⟨z, hz⟩)

Premises used: MDifferentiable.mdifferentiableAt, MDifferentiable.comp, UpperHalfPlane.mdifferentiable_coe, UpperHalfPlane.mdifferentiableAt_iff, UpperHalfPlane.mdifferentiable_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)
h : ∀ (x : ℂ), f (g • (↑ofComplex : ℂ → ℍ) x) = (F ∘ G) x
⊢ (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) = F ∘ G

Tactic:
ext
-- 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)
x : ℂ
⊢ f (g • (↑ofComplex : ℂ → ℍ) x) = (F ∘ G) x

Tactic:
simp [F, G]
-- 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)
⊢ (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) = F ∘ G

Tactic:
have : (fun z : ℂ ↦ f (g • ofComplex z)) = F ∘ G := by ext; simp [F, G]
-- 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
rw :
  meromorphicOrderAt F (G (↑τ : ℂ)) =
    meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)) (↑(g • τ) : ℂ)
hg₁ : AnalyticAt ℂ G (↑τ : ℂ)
hg' : deriv G (↑τ : ℂ) ≠ 0
⊢ meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) (↑τ : ℂ) =
    meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)) (↑(g • τ) : ℂ)

Tactic:
rw [this, meromorphicOrderAt_comp_of_deriv_ne_zero]

Premises used: meromorphicOrderAt_comp_of_deriv_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
⊢ meromorphicOrderAt F (G (↑τ : ℂ)) =
    meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)) (↑(g • τ) : ℂ)

Tactic:
simp [F, G]
-- 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:
τ.analyticAt_smul hg

Premises used: UpperHalfPlane.analyticAt_smul