awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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 : ℂ))
⊢ f w = (f ∘ (↑ofComplex : ℂ → ℍ)) (↑w : ℂ)
have h₁ : f w = f w
Tactic: rw [Function.comp_apply, ofComplex_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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 : ℍ
⊢ ∃ᶠ (z : ℂ) in 𝓝[≠] (↑τ : ℂ), (f ∘ (↑ofComplex : ℂ → ℍ)) z = 0
have h : ∀ (hτ : ∀ᶠ (x : ℂ) in 𝓝[≠] (↑τ : ℂ), (f ∘ (↑ofComplex : ℂ → ℍ)) x ≠ 0), ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0
Tactic: contrapose! hτ
Cleared hypotheses: hτ
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (hypothesis)
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
⊢ ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0
have hτ₁ : ∀ᶠ (a : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℂ) {(↑τ : ℂ)}ᶜ (↑a : ℂ) → (f ∘ (↑ofComplex : ℂ → ℍ)) (↑a : ℂ) ≠ 0
Tactic: rw [eventually_nhdsWithin_iff, ← isOpenEmbedding_coe.map_nhds_eq, eventually_map] at hτ
Cleared hypotheses: hτ
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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
⊢ ∀ᶠ (x : ℍ) in 𝓝[≠] τ, f x ≠ 0
have h : ∀ᶠ (x : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℍ) {τ}ᶜ x → f x ≠ 0
Tactic: rw [eventually_nhdsWithin_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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
⊢ ∀ᶠ (x : ℍ) in 𝓝 τ, Membership.mem (γ := Set ℍ) {τ}ᶜ x → f x ≠ 0
have h : ∀ (a : ℍ) (ha : Membership.mem (γ := Set ℂ) {(↑τ : ℂ)}ᶜ (↑a : ℂ) → (f ∘ (↑ofComplex : ℂ → ℍ)) (↑a : ℂ) ≠ 0),
  Membership.mem (γ := Set ℍ) {τ}ᶜ a → f a ≠ 0
Tactic: filter_upwards [hτ] with a ha
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
⊢ Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0 ↔ ∃ i ∈ s, f i = 0
have refine : ∀ (h0 : 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'⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (hypothesis)
Goal:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : Eq (α := ℍ → ℂ) (∏ i ∈ s, f i) 0
⊢ ∃ i ∈ s, f i = 0
have this : ∃ᶠ (τ : ℍ) in 𝓝[≠] I, Eq (α := ℂ) (∏ i ∈ s, f i τ) 0
Tactic: have : ∃ᶠ τ in 𝓝[≠] I, ∏ i ∈ s, f i τ = 0 := .of_forall <| by simpa using congrFun h0
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (hypothesis)
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, f i = 0
have this₁ : ∃ i ∈ s, ∃ᶠ (x : ℍ) in 𝓝[≠] I, f i x = 0
Tactic: simp only [Finset.prod_eq_zero_iff, Finset.frequently_exists] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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) (↑τ : ℂ)
have refine : num g / denom g =ᶠ[𝓝 (↑τ : ℂ)] fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)
Tactic: refine this.congr_of_eventuallyEq ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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 =ᶠ[𝓝 (↑τ : ℂ)] fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)
have rw : (num g / denom g) ∘ UpperHalfPlane.coe =ᶠ[𝓝 τ] (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) ∘ UpperHalfPlane.coe
Tactic: rw [← isOpenEmbedding_coe.map_nhds_eq, eventuallyEq_map]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ HasStrictDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ))
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)
have suffices : HasStrictDerivAt (num g / denom g)
  ((↑(↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ HasStrictDerivAt (num g / denom g)
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)
have 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)
Tactic: convert!
    ((hasStrictDerivAt_id (τ : ℂ)).const_mul _ |>.add_const _).div
      ((hasStrictDerivAt_id (τ : ℂ)).const_mul _ |>.add_const _) _ using 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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)
⊢ HasStrictDerivAt (num g / denom g)
    ((↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2) (↑τ : ℂ)
have convert_5 : (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * id (↑τ : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) ≠ 0
Tactic: convert!
    ((hasStrictDerivAt_id (τ : ℂ)).const_mul _ |>.add_const _).div
      ((hasStrictDerivAt_id (τ : ℂ)).const_mul _ |>.add_const _) _ using 2
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ (↑(↑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)
have 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) : ℂ)
Tactic: simp [Matrix.det_fin_two]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ Ne (α := ℂ) (deriv (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (↑τ : ℂ)) 0
have rw : (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0
Tactic: rw [deriv_smul hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0
have ha : (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) ≠ 0
Tactic: apply div_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
ha : (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) ≠ 0
⊢ (↑(↑g : Matrix (Fin 2) (Fin 2) ℝ).det : ℂ) / HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0
have hb : HPow.hPow (β := ℕ) (denom g (↑τ : ℂ)) 2 ≠ 0
Tactic: apply div_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
⊢ AnalyticAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (↑τ : ℂ)
have refine : ∀ (z : ℂ) (hz : z ∈ upperHalfPlaneSet),
  DifferentiableWithinAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) upperHalfPlaneSet z
Tactic: refine DifferentiableOn.analyticAt (fun z hz ↦ ?_) (isOpen_upperHalfPlaneSet.mem_nhds τ.im_pos)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
hg : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
τ : ℍ
z : ℂ
hz : z ∈ upperHalfPlaneSet
⊢ DifferentiableWithinAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) upperHalfPlaneSet z
have h : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) z
Tactic: apply DifferentiableAt.differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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
have h : ∀ (x : ℂ), f (g • (↑ofComplex : ℂ → ℍ) x) = (F ∘ G) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (hypothesis)
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)
⊢ meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) (↑τ : ℂ) =
    meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)) (↑(g • τ) : ℂ)
have this : (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) = F ∘ G
Tactic: have : (fun z : ℂ ↦ f (g • ofComplex z)) = F ∘ G := by ext; simp [F, G]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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 (E := ℂ) (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) (↑τ : ℂ) =
    meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)) (↑(g • τ) : ℂ)
have rw : meromorphicOrderAt F (G (↑τ : ℂ)) =
  meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)) (↑(g • τ) : ℂ)
Tactic: rw [this, meromorphicOrderAt_comp_of_deriv_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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 • τ) : ℂ)
⊢ meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) (↑τ : ℂ) =
    meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)) (↑(g • τ) : ℂ)
have hg₁ : AnalyticAt ℂ G (↑τ : ℂ)
Tactic: rw [this, meromorphicOrderAt_comp_of_deriv_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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 (↑τ : ℂ)
⊢ meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f (g • (↑ofComplex : ℂ → ℍ) z)) (↑τ : ℂ) =
    meromorphicOrderAt (E := ℂ) (fun (z : ℂ) ↦ f ((↑ofComplex : ℂ → ℍ) z)) (↑(g • τ) : ℂ)
have hg' : deriv G (↑τ : ℂ) ≠ 0
Tactic: rw [this, meromorphicOrderAt_comp_of_deriv_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ smulFDeriv (J * g) z = -(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z
have h : ∀ (x : ℂ),
  Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
    ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
z x : ℂ
⊢ Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
    ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)
have 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 : ℂ)
Tactic: by_cases hg : 0 < g.val.det
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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 : ℂ)
⊢ Eq (α := ℂ) ((smulFDeriv (J * g) z : (a : ℂ) → ℂ) x : ℂ)
    ((-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ) ∘SL smulFDeriv g z : (a : ℂ) → ℂ) x : ℂ)
have 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 : ℂ)
Tactic: by_cases hg : 0 < g.val.det
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
z : ℂ
⊢ 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
have 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
Tactic: rcases g.det_ne_zero.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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
⊢ 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
have 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
Tactic: rcases g.det_ne_zero.lt_or_gt with h | h
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
g : GL (Fin 2) ℝ
τ : ℍ
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
have 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 (↑τ : ℂ)) (↑τ : ℂ)
Tactic: wlog hg : 0 < g.det.val generalizing g
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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 (↑τ : ℂ)) (↑τ : ℂ)
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
have 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 (↑τ : ℂ)) (↑τ : ℂ)
Tactic: wlog hg : 0 < g.det.val generalizing g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (hypothesis)
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) : ℝ)
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
have hg₁ : LT.lt (α := ℝ) (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
Tactic: replace hg := g.det.ne_zero.lt_or_gt.resolve_right hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
have h : ∀ (x : ℂ),
  (↑(g • (↑ofComplex : ℂ → ℍ) x) : ℂ) = (-(⇑Complex.conjCLE : (a : ℂ) → ℂ)) (↑((J * g) • (↑ofComplex : ℂ → ℍ) x) : ℂ)
Tactic: convert! Complex.conjCLE.hasStrictFDerivAt.neg.comp _ (this (J * g) (by simpa))
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
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) : ℂ)
⊢ HasStrictFDerivAt (fun (z : ℂ) ↦ (↑(g • (↑ofComplex : ℂ → ℍ) z) : ℂ)) (smulFDeriv g (↑τ : ℂ)) (↑τ : ℂ)
have h₁ : Complex.addCommGroup = NormedAddCommGroup.toAddCommGroup →
  HEq (α := Module ℝ ℂ) NormedSpace.toModule (β := Module ℝ ℂ) NormedSpace.toModule →
    smulFDeriv g (↑τ : ℂ) = (-(↑Complex.conjCLE : ℂ →L[ℝ] ℂ)) ∘SL smulFDeriv (J * g) (↑τ : ℂ)
Tactic: convert! Complex.conjCLE.hasStrictFDerivAt.neg.comp _ (this (J * g) (by simpa))