awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
k : ℂ
hF : MDiff F
⊢ MDiff (HMul.hMul (α := ℍ → ℂ) (fun (z : ℍ) ↦ k * 12⁻¹) fun (z : ℍ) ↦ EisensteinSeries.E2 z * F z)

Tactic:
(MDifferentiable.mul mdifferentiable_const (E2_mdifferentiable.mul hF) :
      MDiff (fun z ↦ (k * 12⁻¹) * (EisensteinSeries.E2 z * F z)))

Premises used: mdifferentiable_const, MDifferentiable.mul, E2_mdifferentiable
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
k : ℂ
hF : MDiff F
h :
  ∀ (x : ℍ),
    k * 12⁻¹ * EisensteinSeries.E2 x * F x =
      HMul.hMul (α := ℍ → ℂ) (β := ℍ → ℂ) (fun (z : ℍ) ↦ k * 12⁻¹) (fun (z : ℍ) ↦ EisensteinSeries.E2 z * F z) x
⊢ MDiff fun (z : ℍ) ↦ k * 12⁻¹ * EisensteinSeries.E2 z * F z

Tactic:
convert!
    (MDifferentiable.mul mdifferentiable_const (E2_mdifferentiable.mul hF) :
      MDiff (fun z ↦ (k * 12⁻¹) * (EisensteinSeries.E2 z * F z)))

Premises used: mdifferentiable_const, MDifferentiable.mul, E2_mdifferentiable
-- Module: Mathlib.NumberTheory.ModularForms.Derivative
Goal:
F : ℍ → ℂ
k : ℂ
hF : MDiff F
x : ℍ
⊢ k * 12⁻¹ * EisensteinSeries.E2 x * F x =
    HMul.hMul (α := ℍ → ℂ) (β := ℍ → ℂ) (fun (z : ℍ) ↦ k * 12⁻¹) (fun (z : ℍ) ↦ EisensteinSeries.E2 z * F z) x

Tactic:
simp [Pi.mul_apply, mul_assoc, mul_left_comm, mul_comm]

Premises used: Pi.mul_apply, mul_assoc, mul_left_comm, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
rw : cexp ((↑24 : ℂ) * (log z / 2)) = HPow.hPow (β := ℕ) z 12
⊢ HPow.hPow (β := ℕ) z.sqrt 24 = HPow.hPow (β := ℕ) z 12

Tactic:
rw [sqrt_eq_exp hz, ← exp_nat_mul]

Premises used: sqrt_eq_exp, Complex.exp_nat_mul
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
ring_nf : cexp (log z * 12) = HPow.hPow (β := ℕ) z 12
⊢ cexp ((↑24 : ℂ) * (log z / 2)) = HPow.hPow (β := ℕ) z 12

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
⊢ log z * 12 = (↑12 : ℂ) * log z

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℂ
hz : z ≠ 0
rw : cexp ((↑12 : ℂ) * log z) = HPow.hPow (β := ℕ) z 12
rw₁ : HPow.hPow (β := ℕ) (cexp (log z)) 12 = HPow.hPow (β := ℕ) z 12
rw₂ rw₃ : HPow.hPow (β := ℕ) z 12 = HPow.hPow (β := ℕ) z 12
⊢ cexp (log z * 12) = HPow.hPow (β := ℕ) z 12

Tactic:
rw [show (log z * 12) = (12 : ℕ) * log z by ring, exp_nat_mul, exp_log hz]

Premises used: Complex.exp_nat_mul, Complex.exp_log
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ 12 = HMul.hMul (α := ℕ) 4 3

Tactic:
lia
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
rw : HPow.hPow (β := ℕ) I 12 = 1
rw₁ : I ^ HMul.hMul (α := ℕ) 4 3 = 1
rw₂ : HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) I 4) 3 = 1
rw₃ : HPow.hPow (α := ℂ) (β := ℕ) 1 3 = 1
rw₄ rw₅ : Eq (α := ℂ) 1 1
⊢ HPow.hPow (β := ℕ) I.sqrt 24 = 1

Tactic:
rw [csqrt_pow_24_eq I_ne_zero, show 12 = 4 * 3 by lia, pow_mul, I_pow_four, one_pow]

Premises used: one_pow, _private.0.ModularForm.csqrt_pow_24_eq, Complex.I_ne_zero, Complex.I_pow_four, pow_mul
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
simp : logDeriv (η ∘ fun (x : ℂ) ↦ -x⁻¹) (↑z : ℂ) = (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * logDeriv η (-(↑z : ℂ)⁻¹)
⊢ logDeriv (η ∘ fun (x : ℂ) ↦ -1 / x) (↑z : ℂ) = (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * logDeriv η (-(↑z : ℂ))⁻¹

Tactic:
simp only [neg_div, one_div, inv_neg]

Premises used: neg_div, inv_neg, one_div
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
rw :
  deriv (fun (x : ℂ) ↦ -x⁻¹) (↑z : ℂ) * logDeriv η (-(↑z : ℂ)⁻¹) =
    (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * logDeriv η (-(↑z : ℂ)⁻¹)
hf : DifferentiableAt ℂ η (-(↑z : ℂ)⁻¹)
hg : DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ -x⁻¹) (↑z : ℂ)
⊢ logDeriv (η ∘ fun (x : ℂ) ↦ -x⁻¹) (↑z : ℂ) = (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * logDeriv η (-(↑z : ℂ)⁻¹)

Tactic:
rw [logDeriv_comp, mul_comm]

Premises used: logDeriv_comp, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ deriv (fun (x : ℂ) ↦ -x⁻¹) (↑z : ℂ) * logDeriv η (-(↑z : ℂ)⁻¹) =
    (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * logDeriv η (-(↑z : ℂ)⁻¹)

Tactic:
simp [zpow_ofNat]

Premises used: zpow_ofNat
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ -(↑z : ℂ)⁻¹ ∈ upperHalfPlaneSet

Tactic:
grind [im_pnat_div_pos 1 z]

Premises used: OfNat.ofNat, UpperHalfPlane.im_pnat_div_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ DifferentiableAt ℂ η (-(↑z : ℂ)⁻¹)

Tactic:
exact differentiableAt_eta_of_mem_upperHalfPlaneSet (by grind [im_pnat_div_pos 1 z])

Premises used: ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ (↑z : ℂ) ≠ 0

Tactic:
z.ne_zero

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ (↑z : ℂ) ≠ 0

Tactic:
exact z.ne_zero

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
funProp : (↑z : ℂ) ≠ 0
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ -x⁻¹) (↑z : ℂ)

Tactic:
fun_prop (disch := exact z.ne_zero)

Premises used: UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ (↑z : ℂ).sqrt ≠ 0

Tactic:
simp [sqrt, ne_zero z]

Premises used: Complex.sqrt, UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
rw :
  (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * logDeriv η (-(↑z : ℂ))⁻¹ =
    deriv sqrt (↑z : ℂ) / (↑z : ℂ).sqrt + logDeriv η (↑z : ℂ)
⊢ logDeriv (η ∘ fun (x : ℂ) ↦ -1 / x) (↑z : ℂ) = logDeriv (sqrt * η) (↑z : ℂ)

Tactic:
rw [logDeriv_eta_comp_div_eq z, Pi.mul_def,
      logDeriv_mul _ (by simp [sqrt, ne_zero z]) (eta_ne_zero z.2)
      (differentiableAt_sqrt (mem_slitPlane z))
      (differentiableAt_eta_of_mem_upperHalfPlaneSet z.2), logDeriv_apply sqrt]

Premises used: _private.0.ModularForm.logDeriv_eta_comp_div_eq, logDeriv_mul, Complex.sqrt, UpperHalfPlane.mem_slitPlane, logDeriv_apply, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, Complex.differentiableAt_sqrt, ModularForm.eta_ne_zero, Pi.mul_def, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 ModularGroup.S E2
      z =
    (E2 - (1 / (2 * riemannZeta 2)) • D2 ModularGroup.S) z

Tactic:
have hE2 := congrFun (E2_slash_action ModularGroup.S) z
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
hE2 :
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 ModularGroup.S E2
      z =
    (E2 - (1 / (2 * riemannZeta 2)) • D2 ModularGroup.S) z
⊢ E2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ =
    E2 z -
      6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
        (2 * (↑π : ℂ) * I * (↑((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) / (↑z : ℂ))

Tactic:
simp only [one_div, SL_slash_def, modular_S_smul, ModularGroup.denom_S,
    Int.reduceNeg, zpow_neg, riemannZeta_two, mul_inv_rev, inv_div, Pi.sub_apply, Pi.smul_apply,
    D2, ModularGroup.denom_S, smul_eq_mul] at hE2

Premises used: riemannZeta_two, Int.reduceNeg, UpperHalfPlane.modular_S_smul, ModularGroup.denom_S, ModularForm.SL_slash_def, zpow_neg, one_div, inv_div, mul_inv_rev, smul_eq_mul, EisensteinSeries.D2, Pi.sub_apply, Pi.smul_apply
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
hE2 :
  E2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ =
    E2 z -
      6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
        (2 * (↑π : ℂ) * I * (↑((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) / (↑z : ℂ))
⊢ (↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0 = 1

Tactic:
simp [ModularGroup.S]

Premises used: ModularGroup.S
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
hE2 :
  E2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ =
    E2 z -
      6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
        (2 * (↑π : ℂ) * I * (↑((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) / (↑z : ℂ))
rw :
  (E2 z - 6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ * (2 * (↑π : ℂ) * I * (↑1 : ℂ) / (↑z : ℂ))) * ((↑π : ℂ) * I / 12) =
    (↑z : ℂ) ^ (-1 / 2) / 2 * (HPow.hPow (β := ℂ) (↑z : ℂ) 2⁻¹)⁻¹ + (↑π : ℂ) * I / 12 * E2 z
⊢ (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ * logDeriv η (-(↑z : ℂ))⁻¹ =
    deriv sqrt (↑z : ℂ) / (↑z : ℂ).sqrt + logDeriv η (↑z : ℂ)

Tactic:
rw [deriv_sqrt (mem_slitPlane z), div_eq_mul_inv, logDeriv_eta_eq_E2 z,
    logDeriv_eta_eq_E2 (.mk _ z.im_inv_neg_coe_pos), ← mul_assoc, mul_comm, ← mul_assoc, hE2, sqrt,
    show ModularGroup.S 1 0 = 1 by simp [ModularGroup.S]]

Premises used: mul_assoc, Complex.sqrt, UpperHalfPlane.mem_slitPlane, UpperHalfPlane.mk, div_eq_mul_inv, ModularForm.logDeriv_eta_eq_E2, mul_comm, UpperHalfPlane.im_inv_neg_coe_pos, Complex.deriv_sqrt
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
hE2 :
  E2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ =
    E2 z -
      6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
        (2 * (↑π : ℂ) * I * (↑((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) / (↑z : ℂ))
transitivity :
  (E2 z - 6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ * (2 * (↑π : ℂ) * I * (↑1 : ℂ) / (↑z : ℂ))) * ((↑π : ℂ) * I / 12) =
    1 / (↑z : ℂ) / 2 + (↑π : ℂ) * I / 12 * E2 z
transitivity₁ :
  1 / (↑z : ℂ) / 2 + (↑π : ℂ) * I / 12 * E2 z =
    (↑z : ℂ) ^ (-1 / 2) / 2 * (HPow.hPow (β := ℂ) (↑z : ℂ) 2⁻¹)⁻¹ + (↑π : ℂ) * I / 12 * E2 z
⊢ (E2 z - 6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ * (2 * (↑π : ℂ) * I * (↑1 : ℂ) / (↑z : ℂ))) * ((↑π : ℂ) * I / 12) =
    (↑z : ℂ) ^ (-1 / 2) / 2 * (HPow.hPow (β := ℂ) (↑z : ℂ) 2⁻¹)⁻¹ + (↑π : ℂ) * I / 12 * E2 z

Tactic:
transitivity 1 / z / 2 + π * I / 12 * E2 z

Premises used: EisensteinSeries.E2, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
hE2 :
  E2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ =
    E2 z -
      6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
        (2 * (↑π : ℂ) * I * (↑((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) / (↑z : ℂ))
field_simp : 2 * I * (E2 z * (↑π : ℂ) - 6 * I * (↑1 : ℂ) / (↑z : ℂ)) = 12 / (↑z : ℂ) + E2 z * (↑π : ℂ) * 2 * I
⊢ (E2 z - 6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ * (2 * (↑π : ℂ) * I * (↑1 : ℂ) / (↑z : ℂ))) * ((↑π : ℂ) * I / 12) =
    1 / (↑z : ℂ) / 2 + (↑π : ℂ) * I / 12 * E2 z

Tactic:
field_simp
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
hE2 :
  E2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ =
    E2 z -
      6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
        (2 * (↑π : ℂ) * I * (↑((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) / (↑z : ℂ))
⊢ 2 * I * (E2 z * (↑π : ℂ) - 6 * I * (↑1 : ℂ) / (↑z : ℂ)) = 12 / (↑z : ℂ) + E2 z * (↑π : ℂ) * 2 * I

Tactic:
grind [I_sq]

Premises used: Complex.I_sq
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
hE2 :
  E2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ =
    E2 z -
      6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
        (2 * (↑π : ℂ) * I * (↑((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) / (↑z : ℂ))
rw : 1 / (↑z : ℂ) / 2 + (↑π : ℂ) * I / 12 * E2 z = ((↑z : ℂ) ^ (1 / 2 + 2⁻¹))⁻¹ / 2 + (↑π : ℂ) * I / 12 * E2 z
⊢ 1 / (↑z : ℂ) / 2 + (↑π : ℂ) * I / 12 * E2 z =
    (↑z : ℂ) ^ (-1 / 2) / 2 * (HPow.hPow (β := ℂ) (↑z : ℂ) 2⁻¹)⁻¹ + (↑π : ℂ) * I / 12 * E2 z

Tactic:
rw [div_mul_eq_mul_div₀ _ _ (2 : ℂ), neg_div, cpow_neg, ← mul_inv, ← cpow_add _ _ z.ne_zero]

Premises used: neg_div, mul_inv, Complex.cpow_neg, UpperHalfPlane.ne_zero, Complex.cpow_add, OfNat.ofNat, div_mul_eq_mul_div₀
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
hE2 :
  E2 { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (HPow.hPow (β := ℤ) (↑z : ℂ) 2)⁻¹ =
    E2 z -
      6 / HPow.hPow (β := ℕ) (↑π : ℂ) 2 * 2⁻¹ *
        (2 * (↑π : ℂ) * I * (↑((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) / (↑z : ℂ))
⊢ 1 / (↑z : ℂ) / 2 + (↑π : ℂ) * I / 12 * E2 z = ((↑z : ℂ) ^ (1 / 2 + 2⁻¹))⁻¹ / 2 + (↑π : ℂ) * I / 12 * E2 z

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
rw : Set.EqOn (logDeriv (η ∘ fun (z : ℂ) ↦ -1 / z)) (logDeriv (sqrt * η)) upperHalfPlaneSet
hf : DifferentiableOn ℂ (η ∘ fun (z : ℂ) ↦ -1 / z) upperHalfPlaneSet
hg : DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet
hs2 : IsOpen upperHalfPlaneSet
hsc : IsPreconnected upperHalfPlaneSet
hgn : ∀ x ∈ upperHalfPlaneSet, (sqrt * η) x ≠ 0
hfn : ∀ x ∈ upperHalfPlaneSet, (η ∘ fun (z : ℂ) ↦ -1 / z) x ≠ 0
⊢ ∃ (c : ℂ), c ≠ 0 ∧ Set.EqOn (η ∘ fun (z : ℂ) ↦ -1 / z) (c • (sqrt * η)) upperHalfPlaneSet

Tactic:
rw [← logDeriv_eqOn_iff]

Premises used: logDeriv_eqOn_iff
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ Set.EqOn (logDeriv (η ∘ fun (z : ℂ) ↦ -1 / z)) (logDeriv (sqrt * η)) upperHalfPlaneSet

Tactic:
fun z hz ↦ logDeriv_eta_comp_eq_logDeriv_csqrt_eta ⟨z, hz⟩

Premises used: UpperHalfPlane.mk, Set.EqOn, _private.0.ModularForm.logDeriv_eta_comp_eq_logDeriv_csqrt_eta
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ Set.EqOn (logDeriv (η ∘ fun (z : ℂ) ↦ -1 / z)) (logDeriv (sqrt * η)) upperHalfPlaneSet

Tactic:
exact fun z hz ↦ logDeriv_eta_comp_eq_logDeriv_csqrt_eta ⟨z, hz⟩

Premises used: UpperHalfPlane.mk, _private.0.ModularForm.logDeriv_eta_comp_eq_logDeriv_csqrt_eta
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
hf : DifferentiableOn ℂ η upperHalfPlaneSet
hf₁ : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ -1 / z) upperHalfPlaneSet
hf₂ : Set.MapsTo (fun (z : ℂ) ↦ -1 / z) upperHalfPlaneSet upperHalfPlaneSet
⊢ DifferentiableOn ℂ (η ∘ fun (z : ℂ) ↦ -1 / z) upperHalfPlaneSet

Tactic:
apply DifferentiableOn.comp (t := upperHalfPlaneSet)

Premises used: DifferentiableOn.comp
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ DifferentiableOn ℂ η upperHalfPlaneSet

Tactic:
fun x hx ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, DifferentiableOn
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ DifferentiableOn ℂ η upperHalfPlaneSet

Tactic:
exact fun x hx ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hx).differentiableWithinAt

Premises used: DifferentiableAt.differentiableWithinAt, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ -1) upperHalfPlaneSet

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ z) upperHalfPlaneSet

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ -1 / z) upperHalfPlaneSet

Tactic:
exact DifferentiableOn.div (by fun_prop) (by fun_prop)
        (fun x hx ↦ ne_zero (⟨x, hx⟩ : ℍ))

Premises used: UpperHalfPlane.mk, UpperHalfPlane.ne_zero, DifferentiableOn.div
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
y : ℂ
hy : y ∈ upperHalfPlaneSet
⊢ -1 / y ∈ upperHalfPlaneSet

Tactic:
grind [im_pnat_div_pos 1 (⟨y, hy⟩ : ℍ)]

Premises used: UpperHalfPlane.mk, OfNat.ofNat, UpperHalfPlane.im_pnat_div_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ Set.MapsTo (fun (z : ℂ) ↦ -1 / z) upperHalfPlaneSet upperHalfPlaneSet

Tactic:
exact fun y hy ↦ by grind [im_pnat_div_pos 1 (⟨y, hy⟩ : ℍ)]
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet

Tactic:
fun x hx ↦ ((differentiableAt_sqrt (mem_slitPlane ⟨x, hx⟩)).mul
     (differentiableAt_eta_of_mem_upperHalfPlaneSet hx)).differentiableWithinAt

Premises used: DifferentiableAt.mul, DifferentiableAt.differentiableWithinAt, UpperHalfPlane.mem_slitPlane, UpperHalfPlane.mk, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, Complex.differentiableAt_sqrt, DifferentiableOn
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ DifferentiableOn ℂ (sqrt * η) upperHalfPlaneSet

Tactic:
exact fun x hx ↦ ((differentiableAt_sqrt (mem_slitPlane ⟨x, hx⟩)).mul
     (differentiableAt_eta_of_mem_upperHalfPlaneSet hx)).differentiableWithinAt

Premises used: DifferentiableAt.mul, DifferentiableAt.differentiableWithinAt, UpperHalfPlane.mem_slitPlane, UpperHalfPlane.mk, ModularForm.differentiableAt_eta_of_mem_upperHalfPlaneSet, Complex.differentiableAt_sqrt
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ IsOpen upperHalfPlaneSet

Tactic:
isOpen_upperHalfPlaneSet

Premises used: UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ IsOpen upperHalfPlaneSet

Tactic:
exact isOpen_upperHalfPlaneSet

Premises used: UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ IsPreconnected upperHalfPlaneSet

Tactic:
Convex.isPreconnected (convex_halfSpace_im_gt 0)

Premises used: convex_halfSpace_im_gt, OfNat.ofNat, Convex.isPreconnected
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ IsPreconnected upperHalfPlaneSet

Tactic:
exact Convex.isPreconnected (convex_halfSpace_im_gt 0)

Premises used: convex_halfSpace_im_gt, OfNat.ofNat, Convex.isPreconnected
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
x : ℂ
hx : x ∈ upperHalfPlaneSet
⊢ x.sqrt ≠ 0

Tactic:
simp [sqrt, ne_zero ⟨x, hx⟩]

Premises used: Complex.sqrt, UpperHalfPlane.mk, UpperHalfPlane.ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ ∀ x ∈ upperHalfPlaneSet, (sqrt * η) x ≠ 0

Tactic:
exact fun x hx ↦ mul_ne_zero (by simp [sqrt, ne_zero ⟨x, hx⟩]) (eta_ne_zero hx)

Premises used: ModularForm.eta_ne_zero, mul_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
x : ℂ
hx : x ∈ upperHalfPlaneSet
⊢ (fun (z : ℂ) ↦ -1 / z) x ∈ upperHalfPlaneSet

Tactic:
grind [im_pnat_div_pos 1 ⟨x, hx⟩]

Premises used: UpperHalfPlane.mk, OfNat.ofNat, UpperHalfPlane.im_pnat_div_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
⊢ ∀ x ∈ upperHalfPlaneSet, (η ∘ fun (z : ℂ) ↦ -1 / z) x ≠ 0

Tactic:
exact fun x hx ↦ eta_ne_zero (by grind [im_pnat_div_pos 1 ⟨x, hx⟩])

Premises used: ModularForm.eta_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
simp :
  HPow.hPow (β := ℕ) (𝕢 24 (↑z : ℂ)) 24 * HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - eta_q n (↑z : ℂ))) 24 =
    𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24
⊢ Δ z = 𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24

Tactic:
simp only [discriminant, eta, mul_pow]

Premises used: ModularForm.eta, ModularForm.discriminant, mul_pow
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
e_a : HPow.hPow (β := ℕ) (𝕢 24 (↑z : ℂ)) 24 = 𝕢 1 (↑z : ℂ)
e_a₁ :
  HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - eta_q n (↑z : ℂ))) 24 =
    ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24
⊢ HPow.hPow (β := ℕ) (𝕢 24 (↑z : ℂ)) 24 * HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - eta_q n (↑z : ℂ))) 24 =
    𝕢 1 (↑z : ℂ) * ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24

Tactic:
congr
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
e_a : cexp (24 * (2 * (↑π : ℂ) * I * (↑z : ℂ) / 24)) = cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))
⊢ HPow.hPow (β := ℕ) (𝕢 24 (↑z : ℂ)) 24 = 𝕢 1 (↑z : ℂ)

Tactic:
simp [Periodic.qParam, ← exp_nsmul, nsmul_eq_mul, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Function.Periodic.qParam, Complex.exp_nsmul, nsmul_eq_mul
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ cexp (24 * (2 * (↑π : ℂ) * I * (↑z : ℂ) / 24)) = cexp (2 * (↑π : ℂ) * I * (↑z : ℂ))

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - eta_q n (↑z : ℂ))) 24 =
    ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24

Tactic:
((multipliableLocallyUniformlyOn_eta.multipliable z.2).tprod_pow _).symm

Premises used: MultipliableLocallyUniformlyOn.multipliable, Multipliable.tprod_pow, Eq.symm, UpperHalfPlane.coe_im_pos, ModularForm.multipliableLocallyUniformlyOn_eta
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ HPow.hPow (α := ℂ) (β := ℕ) (∏' (n : ℕ), (1 - eta_q n (↑z : ℂ))) 24 =
    ∏' (n : ℕ), HPow.hPow (β := ℕ) (1 - eta_q n (↑z : ℂ)) 24

Tactic:
exact ((multipliableLocallyUniformlyOn_eta.multipliable z.2).tprod_pow _).symm

Premises used: MultipliableLocallyUniformlyOn.multipliable, Multipliable.tprod_pow, Eq.symm, UpperHalfPlane.coe_im_pos, ModularForm.multipliableLocallyUniformlyOn_eta
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
⊢ Δ z ≠ 0

Tactic:
simpa [discriminant] using eta_ne_zero z.2

Premises used: ModularForm.eta_ne_zero, ModularForm.discriminant, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
h :
  ∀ (z : ℍ),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 ModularGroup.T Δ
        z =
      Δ z
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 ModularGroup.T Δ =
    Δ

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.Discriminant
Goal:
z : ℍ
h :
  Δ (HVAdd.hVAdd (α := ℝ) 1 z) *
      HPow.hPow (β := ℤ)
        ((↑((↑((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
                          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![1, 1; 0, 1]
                            ModularGroup.T._proof_1))) :
                    Matrix (Fin 2) (Fin 2) ℝ)
                  1 0) :
              ℂ) *
            (↑z : ℂ) +
          (↑((↑((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                      ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ))
                        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℤ) ↦ A.det = 1) !![1, 1; 0, 1]
                          ModularGroup.T._proof_1))) :
                  Matrix (Fin 2) (Fin 2) ℝ)
                1 1) :
            ℂ))
        (-12) =
    Δ z
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 ModularGroup.T Δ
      z =
    Δ z

Tactic:
rw [SL_slash_apply, denom, modular_T_smul, ModularGroup.T]

Premises used: ModularGroup.T, UpperHalfPlane.denom, ModularForm.SL_slash_apply, UpperHalfPlane.modular_T_smul