awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℍ
⊢ logDeriv (fun (z : ℂ) ↦ 𝕢 24 z * ∏' (n : ℕ), (1 - eta_q n z)) (↑z : ℂ) = (↑π : ℂ) * I / 12 * E2 z
have rw : logDeriv (𝕢 24) (↑z : ℂ) + logDeriv (fun (x : ℂ) ↦ ∏' (n : ℕ), (1 - eta_q n x)) (↑z : ℂ) = (↑π : ℂ) * I / 12 * E2 z
Tactic: rw [logDeriv_mul _ (Periodic.qParam_ne_zero _) (eta_tprod_ne_zero z.2) (by fun_prop)
    (differentiableAt_eta_tprod z.2)]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (hypothesis)
Goal:
z : ℍ
⊢ logDeriv (𝕢 24) (↑z : ℂ) + logDeriv (fun (x : ℂ) ↦ ∏' (n : ℕ), (1 - eta_q n x)) (↑z : ℂ) = (↑π : ℂ) * I / 12 * E2 z
have HG : Eq (α := ℂ) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 - eta_q i x)) (↑z : ℂ))
  (∑' (i : ℕ), logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) (↑z : ℂ))
Tactic: have HG := logDeriv_tprod_eq_tsum isOpen_upperHalfPlaneSet z.2
    (one_sub_eta_q_ne_zero · z.2) (by fun_prop) (summable_logDeriv_one_sub_eta_q z.2)
    multipliableLocallyUniformlyOn_eta (eta_tprod_ne_zero z.2)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℍ
HG :
  Eq (α := ℂ) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 - eta_q i x)) (↑z : ℂ))
    (∑' (i : ℕ), logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) (↑z : ℂ))
⊢ logDeriv (𝕢 24) (↑z : ℂ) + logDeriv (fun (x : ℂ) ↦ ∏' (n : ℕ), (1 - eta_q n x)) (↑z : ℂ) = (↑π : ℂ) * I / 12 * E2 z
have simp : 2 * (↑π : ℂ) * I / (↑24 : ℂ) +
    2 * (↑π : ℂ) * I * ∑' (n : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n (↑z : ℂ) / (1 - eta_q n (↑z : ℂ)) =
  (↑π : ℂ) * I / 12 * ((riemannZeta 2)⁻¹ * 2⁻¹ * G2 z)
Tactic: simp only [logDeriv_qParam 24 z, HG, tsum_logDeriv_eta_q z, E2, one_div,
    mul_inv_rev, Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℍ
HG :
  Eq (α := ℂ) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 - eta_q i x)) (↑z : ℂ))
    (∑' (i : ℕ), logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) (↑z : ℂ))
⊢ 2 * (↑π : ℂ) * I / (↑24 : ℂ) +
      2 * (↑π : ℂ) * I * ∑' (n : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n (↑z : ℂ) / (1 - eta_q n (↑z : ℂ)) =
    (↑π : ℂ) * I / 12 * ((riemannZeta 2)⁻¹ * 2⁻¹ * G2 z)
have rw : 2 * (↑π : ℂ) * I / (↑24 : ℂ) +
    2 * (↑π : ℂ) * I * ∑' (n : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n (↑z : ℂ) / (1 - eta_q n (↑z : ℂ)) =
  (↑π : ℂ) * I / 12 * ((HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6)⁻¹ * 2⁻¹ * (2 * (HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6))) +
    (↑π : ℂ) * I / 12 *
      -((HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6)⁻¹ * 2⁻¹ *
          (8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
            ∑' (n : ℕ+),
              HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) /
                (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))))
Tactic: rw [G2_eq_tsum_cexp, riemannZeta_two, ← tsum_pow_div_one_sub_eq_tsum_sigma
    (norm_exp_two_pi_I_lt_one z), mul_sub, sub_eq_add_neg, mul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.DedekindEta (goal)
Goal:
z : ℍ
HG :
  Eq (α := ℂ) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 - eta_q i x)) (↑z : ℂ))
    (∑' (i : ℕ), logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) (↑z : ℂ))
⊢ 2 * (↑π : ℂ) * I / (↑24 : ℂ) +
      2 * (↑π : ℂ) * I * ∑' (n : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n (↑z : ℂ) / (1 - eta_q n (↑z : ℂ)) =
    (↑π : ℂ) * I / 12 * ((HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6)⁻¹ * 2⁻¹ * (2 * (HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6))) +
      (↑π : ℂ) * I / 12 *
        -((HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6)⁻¹ * 2⁻¹ *
            (8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
              ∑' (n : ℕ+),
                HPow.hPow (α := ℂ) (β := ℕ) (↑(↑n : ℕ) : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ) /
                  (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (↑n : ℕ))))
have simp : 2 * (↑π : ℂ) * I / 24 +
    ∑' (x : ℕ),
      2 * (↑π : ℂ) * I *
        (-(HAdd.hAdd (α := ℂ) (↑x : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (x + 1)) /
          (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (x + 1))) =
  (↑π : ℂ) * I / 12 * (6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ * (2 * (HPow.hPow (β := ℕ) (↑π : ℂ) 2 / 6))) +
    ∑' (x : ℕ),
      -((↑π : ℂ) * I / 12 *
          (6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
            (8 * HPow.hPow (β := ℕ) (↑π : ℂ) 2 *
              (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1 * cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (x + 1) /
                (1 - cexp (2 * (↑π : ℂ) * I * (↑z : ℂ)) ^ (x + 1))))))
Tactic: simp [eta_q_eq_pow, ← tsum_mul_left, tsum_pnat_eq_tsum_succ (f := fun n ↦
        n * cexp (2 * π * I * z) ^ n / (1 - cexp (2 * π * I * z) ^ n)), ← tsum_neg]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F : ℍ → ℂ
hF : MDiff F
⊢ MDiff (D F)
have rw : ∀ (hF : DifferentiableOn ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}),
  DifferentiableOn ℂ (D F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
Tactic: rw [UpperHalfPlane.mdifferentiable_iff] at hF ⊢
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
c : ℂ := (2 * (↑π : ℂ) * I)⁻¹
⊢ DifferentiableOn ℂ (D F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
have hDeriv : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) z) upperHalfPlaneSet
Tactic: have hDeriv : DifferentiableOn ℂ (fun z ↦ c * deriv (F ∘ ofComplex) z) upperHalfPlaneSet := by
    simpa [c] using (hF.deriv isOpen_upperHalfPlaneSet).const_mul ((2 * π * I)⁻¹)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
c : ℂ := (2 * (↑π : ℂ) * I)⁻¹
hDeriv : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) z) upperHalfPlaneSet
⊢ DifferentiableOn ℂ (D F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
have refine : ∀ x ∈ upperHalfPlaneSet, (D F ∘ (↑ofComplex : ℂ → ℍ)) x = c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) x
Tactic: refine hDeriv.congr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F + G) = D F + D G
have h : ∀ (z : ℍ), D (F + G) z = (D F + D G) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D (F + G) z = (D F + D G) z
have hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ D (F + G) z = (D F + D G) z
have hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F + G) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
have h : (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ) + G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: rw [show (F + G) ∘ ofComplex = F ∘ ofComplex + G ∘ ofComplex from rfl,
    deriv_add hFz hGz, mul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
h :
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ) + G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F + G) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
have h₁ : (2 * (↑π : ℂ) * I)⁻¹ * (deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) + deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: rw [show (F + G) ∘ ofComplex = F ∘ ofComplex + G ∘ ofComplex from rfl,
    deriv_add hFz hGz, mul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
h :
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ) + G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
h₁ :
  (2 * (↑π : ℂ) * I)⁻¹ * (deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) + deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F + G) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
have h₂ : (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: rw [show (F + G) ∘ ofComplex = F ∘ ofComplex + G ∘ ofComplex from rfl,
    deriv_add hFz hGz, mul_add]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F - G) = D F - D G
have h : ∀ (z : ℍ), D (F - G) z = (D F - D G) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D (F - G) z = (D F - D G) z
have hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ D (F - G) z = (D F - D G) z
have hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F - G) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
have h : (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ) - G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: rw [show (F - G) ∘ ofComplex = F ∘ ofComplex - G ∘ ofComplex from rfl,
    deriv_sub hFz hGz, mul_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
h :
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ) - G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F - G) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
have h₁ : (2 * (↑π : ℂ) * I)⁻¹ * (deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) - deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: rw [show (F - G) ∘ ofComplex = F ∘ ofComplex - G ∘ ofComplex from rfl,
    deriv_sub hFz hGz, mul_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
h :
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ) - G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
h₁ :
  (2 * (↑π : ℂ) * I)⁻¹ * (deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) - deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F - G) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
      (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
have h₂ : (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) -
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: rw [show (F - G) ∘ ofComplex = F ∘ ofComplex - G ∘ ofComplex from rfl,
    deriv_sub hFz hGz, mul_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
c : ℂ
⊢ (D fun (x : ℍ) ↦ c) = 0
have h : ∀ (z : ℍ), D (fun (x : ℍ) ↦ c) z = 0 z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
c : ℂ
z : ℍ
⊢ D (fun (x : ℍ) ↦ c) z = 0 z
have h : (2 * (↑π : ℂ) * I)⁻¹ * deriv (fun (x : ℂ) ↦ c) (↑z : ℂ) = 0
Tactic: change (2 * π * I)⁻¹ * deriv (fun _ : ℂ ↦ c) (z : ℂ) = 0
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
⊢ D (c • F) = c • D F
have h : ∀ (z : ℍ), D (c • F) z = (c • D F) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
⊢ D (c • F) z = (c • D F) z
have hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((c • F) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    c * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
have h : (2 * (↑π : ℂ) * I)⁻¹ * (c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
  c * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
Tactic: rw [show (c • F) ∘ ofComplex = c • (F ∘ ofComplex) from rfl,
    deriv_const_smul c hFz, smul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F : ℍ → ℂ
hF : MDiff F
⊢ -F = HSMul.hSMul (α := ℂ) (-1) F
have h : ∀ (x : ℍ), (-F) x = HSMul.hSMul (α := ℂ) (-1) F x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F : ℍ → ℂ
hF : MDiff F
⊢ D (-F) = -D F
have this : -F = HSMul.hSMul (α := ℂ) (-1) F
Tactic: have : -F = (-1 : ℂ) • F := by ext; simp
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F : ℍ → ℂ
hF : MDiff F
this : -F = HSMul.hSMul (α := ℂ) (-1) F
⊢ D (-F) = -D F
have rw : HSMul.hSMul (α := ℂ) (-1) (D F) = -D F
Tactic: rw [this, normalizedDerivOfComplex_smul _ _ hF]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F : ℍ → ℂ
hF : MDiff F
this : -F = HSMul.hSMul (α := ℂ) (-1) F
⊢ HSMul.hSMul (α := ℂ) (-1) (D F) = -D F
have h : ∀ (x : ℍ), HSMul.hSMul (α := ℂ) (-1) (D F) x = (-D F) x
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F * G) = D F * G + F * D G
have h : ∀ (z : ℍ), D (F * G) z = (D F * G + F * D G) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D (F * G) z = (D F * G + F * D G) z
have hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ D (F * G) z = (D F * G + F * D G) z
have hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F * G) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * G z +
      F z * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
have h : (2 * (↑π : ℂ) * I)⁻¹ *
    (deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
      (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
  (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * G z +
    F z * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
Tactic: rw [show (F * G) ∘ ofComplex = (F ∘ ofComplex) * (G ∘ ofComplex) from rfl,
    deriv_mul hFz hGz]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ *
      (deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) +
        (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
    (2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * G z +
      F z * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
have h : -(I * ((↑π : ℂ)⁻¹ * 2⁻¹) *
      (deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * G z + F z * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))) =
  -(I * ((↑π : ℂ)⁻¹ * 2⁻¹) * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) * G z) +
    -(F z * (I * ((↑π : ℂ)⁻¹ * 2⁻¹) * deriv (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)))
Tactic: simp [Function.comp_apply, ofComplex_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
⊢ D (F ^ n) = (↑n : (z : ℍ) → ℂ) * F ^ (n - 1) * D F
have h : ∀ (z : ℍ), D (F ^ n) z = ((↑n : (z : ℍ) → ℂ) * F ^ (n - 1) * D F) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (hypothesis)
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
⊢ D (F ^ n) z = ((↑n : (z : ℍ) → ℂ) * F ^ (n - 1) * D F) z
have hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
Tactic: have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F ^ n) ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) =
    (↑n : (z : ℍ) → ℂ) z * F z ^ (n - 1) * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
have h : (2 * (↑π : ℂ) * I)⁻¹ *
    ((↑n : ℂ) * (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) ^ (n - 1) * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
  (↑n : (z : ℍ) → ℂ) z * F z ^ (n - 1) * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
Tactic: rw [show (F ^ n) ∘ ofComplex = (F ∘ ofComplex) ^ n from rfl, deriv_pow hFz n]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ *
      ((↑n : ℂ) * (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) ^ (n - 1) * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
    (↑n : (z : ℍ) → ℂ) z * F z ^ (n - 1) * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
have h : I * ((↑π : ℂ)⁻¹ * 2⁻¹) * ((↑n : ℂ) * F z ^ (n - 1) * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
  (↑n : ℂ) * F z ^ (n - 1) * (I * ((↑π : ℂ)⁻¹ * 2⁻¹) * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
Tactic: simp [Function.comp_apply, ofComplex_apply]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ serreDerivative k (F + G) = serreDerivative k F + serreDerivative k G
have h : ∀ (z : ℍ), serreDerivative k (F + G) z = (serreDerivative k F + serreDerivative k G) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ serreDerivative k (F + G) z = (serreDerivative k F + serreDerivative k G) z
have h : D F z + D G z - k * 12⁻¹ * EisensteinSeries.E2 z * (F z + G z) =
  D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z + (D G z - k * 12⁻¹ * EisensteinSeries.E2 z * G z)
Tactic: simp [serreDerivative, normalizedDerivOfComplex_add F G hF hG]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ serreDerivative k (F - G) = serreDerivative k F - serreDerivative k G
have h : ∀ (z : ℍ), serreDerivative k (F - G) z = (serreDerivative k F - serreDerivative k G) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ serreDerivative k (F - G) z = (serreDerivative k F - serreDerivative k G) z
have h : D F z - D G z - k * 12⁻¹ * EisensteinSeries.E2 z * (F z - G z) =
  D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z - (D G z - k * 12⁻¹ * EisensteinSeries.E2 z * G z)
Tactic: simp [serreDerivative, normalizedDerivOfComplex_sub F G hF hG]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
k c : ℂ
F : ℍ → ℂ
hF : MDiff F
⊢ serreDerivative k (c • F) = c • serreDerivative k F
have h : ∀ (z : ℍ), serreDerivative k (c • F) z = (c • serreDerivative k F) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
k c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
⊢ serreDerivative k (c • F) z = (c • serreDerivative k F) z
have h : c * D F z - k * 12⁻¹ * EisensteinSeries.E2 z * (c * F z) = c * (D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z)
Tactic: simp [serreDerivative, normalizedDerivOfComplex_smul c F hF, smul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.Derivative (goal)
Goal:
k₁ k₂ : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ serreDerivative (k₁ + k₂) (F * G) = serreDerivative k₁ F * G + F * serreDerivative k₂ G
have h : ∀ (z : ℍ), serreDerivative (k₁ + k₂) (F * G) z = (serreDerivative k₁ F * G + F * serreDerivative k₂ G) z
Tactic: ext z