awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℍ
HG :
  Eq (α := ℂ) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 - eta_q i x)) (↑z : ℂ))
    (∑' (i : ℕ), logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) (↑z : ℂ))
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 : ℕ))))
⊢ 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:
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]

Premises used: riemannZeta_two, mul_sub, sub_eq_add_neg, tsum_pow_div_one_sub_eq_tsum_sigma, UpperHalfPlane.norm_exp_two_pi_I_lt_one, EisensteinSeries.G2_eq_tsum_cexp, mul_add
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℍ
HG :
  Eq (α := ℂ) (logDeriv (fun (x : ℂ) ↦ ∏' (i : ℕ), (1 - eta_q i x)) (↑z : ℂ))
    (∑' (i : ℕ), logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) (↑z : ℂ))
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))))))
⊢ 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:
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]

Premises used: ModularForm.eta_q_eq_pow, tsum_pnat_eq_tsum_succ, tsum_mul_left, tsum_neg
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
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 +
      ∑' (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:
grind
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : MDiff F
rw :
  ∀ (hF : DifferentiableOn ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}),
    DifferentiableOn ℂ (D F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
⊢ MDiff (D F)

Tactic:
rw [UpperHalfPlane.mdifferentiable_iff] at hF ⊢

Premises used: UpperHalfPlane.mdifferentiable_iff
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
c : ℂ := (2 * (↑π : ℂ) * I)⁻¹
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) z) upperHalfPlaneSet

Tactic:
simpa [c] using (hF.deriv isOpen_upperHalfPlaneSet).const_mul ((2 * π * I)⁻¹)

Premises used: DifferentiableOn.deriv, Real.pi, HMul.hMul, Complex.ofReal, Inv.inv, DifferentiableOn.const_mul, OfNat.ofNat, UpperHalfPlane.isOpen_upperHalfPlaneSet, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
c : ℂ := (2 * (↑π : ℂ) * I)⁻¹
⊢ 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)⁻¹)
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
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}

Tactic:
hDeriv.congr ?_

Premises used: DifferentiableOn.congr
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
c : ℂ := (2 * (↑π : ℂ) * I)⁻¹
hDeriv : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) z) upperHalfPlaneSet
refine : ∀ x ∈ upperHalfPlaneSet, (D F ∘ (↑ofComplex : ℂ → ℍ)) x = c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) x
⊢ DifferentiableOn ℂ (D F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}

Tactic:
refine hDeriv.congr ?_

Premises used: DifferentiableOn.congr
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
c : ℂ := (2 * (↑π : ℂ) * I)⁻¹
hDeriv : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) z) upperHalfPlaneSet
z : ℂ
hz : z ∈ upperHalfPlaneSet
⊢ (D F ∘ (↑ofComplex : ℂ → ℍ)) z = c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) z

Tactic:
simp [normalizedDerivOfComplex, c, Function.comp_apply, ofComplex_apply_of_im_pos hz]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos, Function.comp_apply, Derivative.normalizedDerivOfComplex
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
h : ∀ (z : ℍ), D (F + G) z = (D F + D G) z
⊢ D (F + G) = D F + D G

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)

Tactic:
have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)

Tactic:
have hGz := UpperHalfPlane.mdifferentiableAt_iff.mp (hG z)
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
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 : ℂ)
h₂ 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 : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F + 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]

Premises used: mul_add, deriv_add, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
h : ∀ (z : ℍ), D (F - G) z = (D F - D G) z
⊢ D (F - G) = D F - D G

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
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 : ℂ)
h₂ 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 : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F - 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]

Premises used: mul_sub, deriv_sub, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
c : ℂ
h : ∀ (z : ℍ), D (fun (x : ℍ) ↦ c) z = 0 z
⊢ (D fun (x : ℍ) ↦ c) = 0

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
c : ℂ
z : ℍ
h : (2 * (↑π : ℂ) * I)⁻¹ * deriv (fun (x : ℂ) ↦ c) (↑z : ℂ) = 0
⊢ D (fun (x : ℍ) ↦ c) z = 0 z

Tactic:
change (2 * π * I)⁻¹ * deriv (fun _ : ℂ ↦ c) (z : ℂ) = 0

Premises used: Real.pi, HMul.hMul, UpperHalfPlane.coe, deriv, Complex.ofReal, OfNat.ofNat, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
c : ℂ
z : ℍ
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv (fun (x : ℂ) ↦ c) (↑z : ℂ) = 0

Tactic:
simp [deriv_const]

Premises used: deriv_const
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
h : ∀ (z : ℍ), D (c • F) z = (c • D F) z
⊢ D (c • F) = c • D F

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
⊢ DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)

Tactic:
have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
h :
  (2 * (↑π : ℂ) * I)⁻¹ * (c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
    c * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((c • 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]

Premises used: deriv_const_smul, smul_eq_mul, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ (2 * (↑π : ℂ) * I)⁻¹ * (c * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
    c * ((2 * (↑π : ℂ) * I)⁻¹ * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : MDiff F
h : ∀ (x : ℍ), (-F) x = HSMul.hSMul (α := ℂ) (-1) F x
⊢ -F = HSMul.hSMul (α := ℂ) (-1) F

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : MDiff F
x : ℍ
⊢ (-F) x = HSMul.hSMul (α := ℂ) (-1) F x

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : MDiff F
⊢ -F = HSMul.hSMul (α := ℂ) (-1) F

Tactic:
have : -F = (-1 : ℂ) • F := by ext; simp
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : MDiff F
this : -F = HSMul.hSMul (α := ℂ) (-1) F
rw : HSMul.hSMul (α := ℂ) (-1) (D F) = -D F
⊢ D (-F) = -D F

Tactic:
rw [this, normalizedDerivOfComplex_smul _ _ hF]

Premises used: Derivative.normalizedDerivOfComplex_smul
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : MDiff F
this : -F = HSMul.hSMul (α := ℂ) (-1) F
h : ∀ (x : ℍ), HSMul.hSMul (α := ℂ) (-1) (D F) x = (-D F) x
⊢ HSMul.hSMul (α := ℂ) (-1) (D F) = -D F

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
hF : MDiff F
this : -F = HSMul.hSMul (α := ℂ) (-1) F
x : ℍ
⊢ HSMul.hSMul (α := ℂ) (-1) (D F) x = (-D F) x

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
h : ∀ (z : ℍ), D (F * G) z = (D F * G + F * D G) z
⊢ D (F * G) = D F * G + F * D G

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
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 : ℂ → ℍ)) (↑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 : ℂ))
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F * 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]

Premises used: deriv_mul, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
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 : ℂ)))
⊢ (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:
simp [Function.comp_apply, ofComplex_apply]

Premises used: UpperHalfPlane.ofComplex_apply, Function.comp_apply
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
hGz : DifferentiableAt ℂ (G ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ -(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:
ring
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
h : ∀ (z : ℍ), D (F ^ n) z = ((↑n : (z : ℍ) → ℂ) * F ^ (n - 1) * D F) z
⊢ D (F ^ n) = (↑n : (z : ℍ) → ℂ) * F ^ (n - 1) * D F

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
⊢ DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)

Tactic:
have hFz := UpperHalfPlane.mdifferentiableAt_iff.mp (hF z)
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
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 : ℂ))
⊢ (2 * (↑π : ℂ) * I)⁻¹ * deriv ((F ^ n) ∘ (↑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]

Premises used: deriv_pow, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
h :
  I * ((↑π : ℂ)⁻¹ * 2⁻¹) * ((↑n : ℂ) * F z ^ (n - 1) * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
    (↑n : ℂ) * F z ^ (n - 1) * (I * ((↑π : ℂ)⁻¹ * 2⁻¹) * deriv (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 : ℂ))

Tactic:
simp [Function.comp_apply, ofComplex_apply]

Premises used: UpperHalfPlane.ofComplex_apply, Function.comp_apply
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
n : ℕ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)
⊢ I * ((↑π : ℂ)⁻¹ * 2⁻¹) * ((↑n : ℂ) * F z ^ (n - 1) * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ)) =
    (↑n : ℂ) * F z ^ (n - 1) * (I * ((↑π : ℂ)⁻¹ * 2⁻¹) * deriv (F ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k : ℂ
F : ℍ → ℂ
z : ℍ
⊢ serreDerivative k F z = D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z

Tactic:
rfl

Premises used: Derivative.serreDerivative, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k : ℂ
F : ℍ → ℂ
⊢ serreDerivative k F = fun (z : ℍ) ↦ D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z

Tactic:
rfl

Premises used: Derivative.serreDerivative, rfl
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
h : ∀ (z : ℍ), serreDerivative k (F + G) z = (serreDerivative k F + serreDerivative k G) z
⊢ serreDerivative k (F + G) = serreDerivative k F + serreDerivative k G

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
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)
⊢ serreDerivative k (F + G) z = (serreDerivative k F + serreDerivative k G) z

Tactic:
simp [serreDerivative, normalizedDerivOfComplex_add F G hF hG]

Premises used: Derivative.serreDerivative, Derivative.normalizedDerivOfComplex_add
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ 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:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
h : ∀ (z : ℍ), serreDerivative k (F - G) z = (serreDerivative k F - serreDerivative k G) z
⊢ serreDerivative k (F - G) = serreDerivative k F - serreDerivative k G

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
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)
⊢ serreDerivative k (F - G) z = (serreDerivative k F - serreDerivative k G) z

Tactic:
simp [serreDerivative, normalizedDerivOfComplex_sub F G hF hG]

Premises used: Derivative.normalizedDerivOfComplex_sub, Derivative.serreDerivative
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ 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:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k c : ℂ
F : ℍ → ℂ
hF : MDiff F
h : ∀ (z : ℍ), serreDerivative k (c • F) z = (c • serreDerivative k F) z
⊢ serreDerivative k (c • F) = c • serreDerivative k F

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
h : c * D F z - k * 12⁻¹ * EisensteinSeries.E2 z * (c * F z) = c * (D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z)
⊢ serreDerivative k (c • F) z = (c • serreDerivative k F) z

Tactic:
simp [serreDerivative, normalizedDerivOfComplex_smul c F hF, smul_eq_mul]

Premises used: Derivative.normalizedDerivOfComplex_smul, Derivative.serreDerivative, smul_eq_mul
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
⊢ c * D F z - k * 12⁻¹ * EisensteinSeries.E2 z * (c * F z) = c * (D F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k₁ k₂ : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
h : ∀ (z : ℍ), serreDerivative (k₁ + k₂) (F * G) z = (serreDerivative k₁ F * G + F * serreDerivative k₂ G) z
⊢ serreDerivative (k₁ + k₂) (F * G) = serreDerivative k₁ F * G + F * serreDerivative k₂ G

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k₁ k₂ : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
h :
  D F z * G z + F z * D G z - (k₁ + k₂) * 12⁻¹ * EisensteinSeries.E2 z * (F z * G z) =
    (D F z - k₁ * 12⁻¹ * EisensteinSeries.E2 z * F z) * G z + F z * (D G z - k₂ * 12⁻¹ * EisensteinSeries.E2 z * G z)
⊢ serreDerivative (k₁ + k₂) (F * G) z = (serreDerivative k₁ F * G + F * serreDerivative k₂ G) z

Tactic:
simp [serreDerivative, normalizedDerivOfComplex_mul F G hF hG]

Premises used: Derivative.serreDerivative, Derivative.normalizedDerivOfComplex_mul
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
k₁ k₂ : ℂ
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D F z * G z + F z * D G z - (k₁ + k₂) * 12⁻¹ * EisensteinSeries.E2 z * (F z * G z) =
    (D F z - k₁ * 12⁻¹ * EisensteinSeries.E2 z * F z) * G z + F z * (D G z - k₂ * 12⁻¹ * EisensteinSeries.E2 z * G z)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
k : ℂ
hF : MDiff F
⊢ MDiff (serreDerivative k F)

Tactic:
(normalizedDerivOfComplex_mdifferentiable hF).sub ?_

Premises used: Derivative.serreDerivative, MDifferentiable.sub, Derivative.normalizedDerivOfComplex_mdifferentiable
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
k : ℂ
hF : MDiff F
refine : MDiff fun (z : ℍ) ↦ k * 12⁻¹ * EisensteinSeries.E2 z * F z
⊢ MDiff (serreDerivative k F)

Tactic:
refine (normalizedDerivOfComplex_mdifferentiable hF).sub ?_

Premises used: MDifferentiable.sub, Derivative.normalizedDerivOfComplex_mdifferentiable