awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
n : ℕ
z : ℂ
simp :
  cexp (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (2 * (↑π : ℂ) * I * z)) =
    cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)
⊢ eta_q n z = cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)

Tactic:
simp [eta_q, Periodic.qParam, ← Complex.exp_nsmul]

Premises used: Function.Periodic.qParam, ModularForm.eta_q, Complex.exp_nsmul
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
n : ℕ
z : ℂ
⊢ cexp (HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * (2 * (↑π : ℂ) * I * z)) =
    cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
n : ℕ
z : ℂ
⊢ eta_q n z = cexp (2 * (↑π : ℂ) * I * z) ^ (n + 1)

Tactic:
simp [eta_q, Periodic.qParam]

Premises used: Function.Periodic.qParam, ModularForm.eta_q
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
n : ℕ
z : ℂ
hz : z ∈ ℍₒ
rw : 1 ≠ cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)
⊢ 1 - eta_q n z ≠ 0

Tactic:
rw [eta_q_eq_cexp, sub_ne_zero]

Premises used: sub_ne_zero, ModularForm.eta_q_eq_cexp
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)
⊢ 0 < ((n + 1) • z).im

Tactic:
simpa [(show 0 < (n + 1 : ℝ) by positivity)] using hz
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
n : ℕ
z : ℂ
hz : z ∈ ℍₒ
h : 1 = cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)
⊢ False

Tactic:
simpa [← mul_assoc, ← h] using norm_exp_two_pi_I_lt_one ⟨(n + 1) • z, by
    simpa [(show 0 < (n + 1 : ℝ) by positivity)] using hz⟩

Premises used: mul_assoc, UpperHalfPlane.norm_exp_two_pi_I_lt_one, UpperHalfPlane.mk, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
q : ℂ
hq : ‖q‖ < 1
apply : Summable (α := ℝ) fun (i : ℕ) ↦ ‖-q ^ (i + 1)‖
⊢ Multipliable (α := ℂ) fun (n : ℕ) ↦ 1 - q ^ (n + 1)

Tactic:
apply multipliable_one_add_of_summable (f := fun n ↦ -q ^ (n + 1))

Premises used: multipliable_one_add_of_summable
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
q : ℂ
hq : ‖q‖ < 1
⊢ Summable (α := ℝ) fun (i : ℕ) ↦ ‖-q ^ (i + 1)‖

Tactic:
simpa using (summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one (norm_nonneg _) hq)

Premises used: Iff.mpr, summable_nat_add_iff, summable_geometric_of_lt_one, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h :
  HasProdLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 - q ^ (n + 1))
    (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (Metric.ball 0 1)
⊢ MultipliableLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 - q ^ (n + 1)) (Metric.ball 0 1)

Tactic:
use fun q ↦ ∏' n, (1 - q ^ (n + 1))

Premises used: HSub.hSub, HPow.hPow, HAdd.hAdd, tprod, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h :
  ∀ K ⊆ Metric.ball 0 1,
    IsCompact K →
      HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1))
        (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
⊢ HasProdLocallyUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1))
    (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) (Metric.ball 0 1)

Tactic:
apply hasProdLocallyUniformlyOn_of_forall_compact Metric.isOpen_ball

Premises used: hasProdLocallyUniformlyOn_of_forall_compact, Metric.isOpen_ball
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
h :
  ∀ (hN : K = ∅),
    HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1)))
      K
h₁ :
  ∀ (hN : K.Nonempty),
    HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1)))
      K
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
rcases K.eq_empty_or_nonempty with hN | hN

Premises used: Set.eq_empty_or_nonempty
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K = ∅
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn, hN] using tendstoUniformlyOn_empty

Premises used: tendstoUniformlyOn_empty, hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
⊢ ContinuousOn (Y := ℝ) (fun (q : ℂ) ↦ ‖q‖) K

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
h :
  ∀ (q₀ : ℂ) (hq₀ : q₀ ∈ K),
    sSup ((fun (q : ℂ) ↦ ‖q‖) '' K) = ‖q₀‖ →
      ∀ (HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖),
        HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1))
          (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
obtain ⟨q₀, hq₀, _, HB⟩ := hcK.exists_sSup_image_eq_and_ge hN
      (show ContinuousOn (fun q : ℂ ↦ ‖q‖) K by fun_prop)

Premises used: IsCompact.exists_sSup_image_eq_and_ge
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left : sSup ((fun (q : ℂ) ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
⊢ ‖q₀‖ < 1

Tactic:
simpa [Metric.mem_ball, dist_zero_right] using hK hq₀

Premises used: Metric.mem_ball, dist_zero_right
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left : sSup ((fun (q : ℂ) ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
x : ℕ
⊢ ContinuousOn (Y := ℂ) (fun (q : ℂ) ↦ -q ^ (x + 1)) K

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left : sSup ((fun (q : ℂ) ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
h : ∀ (n : ℕ) (x : ℂ) (hx : x ∈ K), ‖-x ^ (n + 1)‖ ≤ ‖q₀‖ ^ (n + 1)
⊢ HasProdUniformlyOn (α := ℂ) (fun (n : ℕ) (q : ℂ) ↦ 1 + -q ^ (n + 1)) (fun (q : ℂ) ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
refine ((summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one (norm_nonneg _)
      (by simpa [Metric.mem_ball, dist_zero_right] using hK hq₀))).hasProdUniformlyOn_nat_one_add
      hcK (.of_forall fun n x hx ↦ ?_) (fun _ ↦ by fun_prop)

Premises used: Iff.mpr, summable_nat_add_iff, Summable.hasProdUniformlyOn_nat_one_add, Filter.Eventually.of_forall, summable_geometric_of_lt_one, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
hN : K.Nonempty
q₀ : ℂ
hq₀ : q₀ ∈ K
left : sSup ((fun (q : ℂ) ↦ ‖q‖) '' K) = ‖q₀‖
HB : ∀ y ∈ K, ‖y‖ ≤ ‖q₀‖
n : ℕ
x : ℂ
hx : x ∈ K
⊢ ‖-x ^ (n + 1)‖ ≤ ‖q₀‖ ^ (n + 1)

Tactic:
simpa using pow_le_pow_left₀ (norm_nonneg _) (HB x hx) (n + 1)

Premises used: pow_le_pow_left₀, HAdd.hAdd, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
x : Finset ℕ
x_1 : ℕ
h : x_1 ∈ x
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x2 : ℂ) ↦ 1 - x2 ^ (x_1 + 1)) (Metric.ball 0 1)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
x : Finset ℕ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x2 : ℂ) ↦ ∏ i ∈ x, (fun (n : ℕ) (q : ℂ) ↦ 1 - q ^ (n + 1)) i x2) (Metric.ball 0 1)

Tactic:
simpa [Finset.prod_fn] using
      DifferentiableOn.finsetProd (fun _ _ ↦ by fun_prop)

Premises used: DifferentiableOn.finsetProd, Finset.prod_fn
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
k : ℕ
x : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) x
⊢ ‖x‖ < 1

Tactic:
simpa using hq
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℍ
⊢ Summable (α := ℝ) fun (n : ℕ) ↦ ‖-eta_q n (↑z : ℂ)‖

Tactic:
simpa [summable_nat_add_iff] using
    summable_geometric_of_lt_one (norm_nonneg _) (mod_cast norm_qParam_lt_one 1 z)

Premises used: summable_nat_add_iff, summable_geometric_of_lt_one, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ Membership.mem (γ := Set ℂ) (Metric.ball 0 1) (𝕢 1 z)

Tactic:
simpa using norm_qParam_lt_one 1 ⟨z, hz⟩

Premises used: UpperHalfPlane.mk, UpperHalfPlane.norm_qParam_lt_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
⊢ ContinuousOn (𝕢 1) ℍₒ

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ Ne (α := ℂ) (∏' (n : ℕ), (1 - eta_q n z)) 0

Tactic:
tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z) ?_ ?_

Premises used: tprod_one_add_ne_zero_of_summable
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
refine_1 : ∀ (i : ℕ), HAdd.hAdd (α := ℂ) 1 ((fun (n : ℕ) ↦ -eta_q n z) i) ≠ 0
refine_2 : Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((fun (n : ℕ) ↦ -eta_q n z) x)
⊢ Ne (α := ℂ) (∏' (n : ℕ), (1 - eta_q n z)) 0

Tactic:
refine tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z) ?_ ?_

Premises used: tprod_one_add_ne_zero_of_summable
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
i : ℕ
⊢ HAdd.hAdd (α := ℂ) 1 ((fun (n : ℕ) ↦ -eta_q n z) i) ≠ 0

Tactic:
simpa using one_sub_eta_q_ne_zero i hz

Premises used: ModularForm.one_sub_eta_q_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ ∀ (i : ℕ), HAdd.hAdd (α := ℂ) 1 ((fun (n : ℕ) ↦ -eta_q n z) i) ≠ 0

Tactic:
exact fun i ↦ by simpa using one_sub_eta_q_ne_zero i hz
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ Summable (α := ℝ) fun (x : ℕ) ↦ norm (E := ℂ) ((fun (n : ℕ) ↦ -eta_q n z) x)

Tactic:
simpa [eta_q, ← summable_norm_iff] using summable_eta_q ⟨z, hz⟩

Premises used: ModularForm.eta_q, UpperHalfPlane.mk, summable_norm_iff, ModularForm.summable_eta_q
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ η z ≠ 0

Tactic:
mul_ne_zero (Periodic.qParam_ne_zero z) (eta_tprod_ne_zero hz)

Premises used: ModularForm.eta, ModularForm.eta_tprod_ne_zero, Function.Periodic.qParam_ne_zero, mul_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
r : ℂ
h : ∀ (z : ℂ), logDeriv (fun (z : ℂ) ↦ 1 - r * cexp z) z = -r * cexp z / (1 - r * cexp z)
⊢ Eq (α := (x : ℂ) → ℂ) (logDeriv fun (z : ℂ) ↦ 1 - r * cexp z) fun (z : ℂ) ↦ -r * cexp z / (1 - r * cexp z)

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
r z : ℂ
⊢ logDeriv (fun (z : ℂ) ↦ 1 - r * cexp z) z = -r * cexp z / (1 - r * cexp z)

Tactic:
simp [logDeriv]

Premises used: logDeriv
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
h : ∀ (y : ℂ), logDeriv ((fun (z : ℂ) ↦ 1 - r * cexp z) ∘ g) y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))
⊢ Eq (α := (x : ℂ) → ℂ) (logDeriv ((fun (z : ℂ) ↦ 1 - r * cexp z) ∘ g)) fun (z : ℂ) ↦
    -r * deriv g z * cexp (g z) / (1 - r * cexp (g z))

Tactic:
ext y
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
y : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ 1 - r * cexp z) (g y)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
y : ℂ
h :
  (fun (z : ℂ) ↦ -r * cexp z / (1 - r * cexp z)) (g y) * deriv g y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))
⊢ logDeriv ((fun (z : ℂ) ↦ 1 - r * cexp z) ∘ g) y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))

Tactic:
rw [logDeriv_comp (by fun_prop) (hg y), logDeriv_one_sub_cexp]

Premises used: logDeriv_comp, ModularForm.logDeriv_one_sub_cexp
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
r : ℂ
g : ℂ → ℂ
hg : Differentiable ℂ g
y : ℂ
⊢ (fun (z : ℂ) ↦ -r * cexp z / (1 - r * cexp z)) (g y) * deriv g y = -r * deriv g y * cexp (g y) / (1 - r * cexp (g y))

Tactic:
ring
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
n : ℕ
⊢ Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x))
    ((fun (z : ℂ) ↦ 1 - 1 * cexp z) ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x)

Tactic:
aesop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
n : ℕ
⊢ Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x))
    ((fun (z : ℂ) ↦ 1 - 1 * cexp z) ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x)

Tactic:
have h2 : (fun x ↦ 1 - cexp (2 * ↑π * I * (n + 1) * x)) =
      ((fun z ↦ 1 - 1 * cexp z) ∘ fun x ↦ 2 * ↑π * I * (n + 1) * x) := by aesop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
n : ℕ
h2 :
  Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x))
    ((fun (z : ℂ) ↦ 1 - 1 * cexp z) ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x)
⊢ Differentiable ℂ (F := ℂ) fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
n : ℕ
h2 :
  Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x))
    ((fun (z : ℂ) ↦ 1 - 1 * cexp z) ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x)
simp_rw :
  -1 * (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) *
        cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z) /
      (1 - 1 * cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)) =
    2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z) /
      (1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z))
⊢ logDeriv (fun (x : ℂ) ↦ 1 - eta_q n x) z =
    2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n z / (1 - eta_q n z)

Tactic:
simp_rw [eta_q_eq_cexp, h2, logDeriv_one_sub_mul_cexp_comp 1
    (g := fun x ↦ (2 * π * I * (n + 1) * x)) (by fun_prop), deriv_const_mul_id]

Premises used: ModularForm.eta_q_eq_cexp, ModularForm.logDeriv_one_sub_mul_cexp_comp, deriv_const_mul_id, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
n : ℕ
h2 :
  Eq (α := (x : ℂ) → ℂ) (fun (x : ℂ) ↦ 1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x))
    ((fun (z : ℂ) ↦ 1 - 1 * cexp z) ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * x)
⊢ -1 * (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1) *
        cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z) /
      (1 - 1 * cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z)) =
    2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z) /
      (1 - cexp (2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * z))

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
rw :
  Eq (α := ℂ) (∑' (b : ℕ), 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 * -eta_q b z / (1 - eta_q b z))
    (∑' (x : ℕ), 2 * (↑π : ℂ) * I * (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1 * -eta_q x z / (1 - eta_q x z)))
⊢ ∑' (n : ℕ), logDeriv (fun (x : ℂ) ↦ 1 - eta_q n x) z =
    2 * (↑π : ℂ) * I * ∑' (n : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n z / (1 - eta_q n z)

Tactic:
rw [tsum_congr (one_sub_eta_logDeriv_eq z), ← tsum_mul_left]

Premises used: tsum_congr, tsum_mul_left, _private.0.ModularForm.one_sub_eta_logDeriv_eq
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
⊢ Eq (α := ℂ) (∑' (b : ℕ), 2 * (↑π : ℂ) * I * HAdd.hAdd (α := ℂ) (↑b : ℂ) 1 * -eta_q b z / (1 - eta_q b z))
    (∑' (x : ℕ), 2 * (↑π : ℂ) * I * (HAdd.hAdd (α := ℂ) (↑x : ℂ) 1 * -eta_q x z / (1 - eta_q x z)))

Tactic:
grind
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ Membership.mem (γ := Set ℂ) (Metric.ball 0 1) (𝕢 1 z)

Tactic:
have hq : 𝕢 1 z ∈ Metric.ball 0 1 := by simpa using norm_qParam_lt_one 1 ⟨z, hz⟩
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) (𝕢 1 z)
⊢ DifferentiableAt ℂ (𝕢 1) z

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) (𝕢 1 z)
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ ∏' (n : ℕ), (1 - eta_q n x)) z

Tactic:
exact (differentiableOn_tprod_one_sub_pow.differentiableAt
    (Metric.isOpen_ball.mem_nhds hq)).comp z (by fun_prop)

Premises used: DifferentiableOn.differentiableAt, Metric.isOpen_ball, IsOpen.mem_nhds, DifferentiableAt.comp, ModularForm.differentiableOn_tprod_one_sub_pow
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ DifferentiableAt ℂ (𝕢 24) z

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h : ℝ
z : ℂ
h₁ : ∀ (x : ℂ), 𝕢 h x = (cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x) x
⊢ 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h : ℝ
z x : ℂ
⊢ 𝕢 h x = (cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x) x

Tactic:
grind [Periodic.qParam]

Premises used: Function.Periodic.qParam
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h : ℝ
z : ℂ
⊢ 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x

Tactic:
have : 𝕢 h = cexp ∘ ((2 * π * I / h) * ·) := by
    ext
    grind [Periodic.qParam]
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x
⊢ DifferentiableAt ℂ cexp (2 * (↑π : ℂ) * I / (↑h : ℂ) * z)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x
⊢ DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x) z

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x
rw : logDeriv cexp (2 * (↑π : ℂ) * I / (↑h : ℂ) * z) * (2 * (↑π : ℂ) * I / (↑h : ℂ)) = 2 * (↑π : ℂ) * I / (↑h : ℂ)
⊢ logDeriv (𝕢 h) z = 2 * (↑π : ℂ) * I / (↑h : ℂ)

Tactic:
rw [this, logDeriv_comp (by fun_prop) (by fun_prop), deriv_const_mul_id]

Premises used: logDeriv_comp, deriv_const_mul_id
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
h : ℝ
z : ℂ
this : 𝕢 h = cexp ∘ fun (x : ℂ) ↦ 2 * (↑π : ℂ) * I / (↑h : ℂ) * x
⊢ logDeriv cexp (2 * (↑π : ℂ) * I / (↑h : ℂ) * z) * (2 * (↑π : ℂ) * I / (↑h : ℂ)) = 2 * (↑π : ℂ) * I / (↑h : ℂ)

Tactic:
simp [logDeriv_exp]

Premises used: Complex.logDeriv_exp
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
⊢ Summable (α := ℂ) fun (n : ℕ) ↦
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n /
      (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n)

Tactic:
have := summable_norm_pow_mul_geometric_div_one_sub 1 (norm_qParam_lt_one 1 ⟨z, hz⟩)
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n /
      (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n)
⊢ Summable (α := ℂ) fun (i : ℕ) ↦
    -2 * (↑π : ℂ) * I *
      (HPow.hPow (α := ℂ) (β := ℕ) (↑(i + 1) : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ (i + 1) /
        (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ (i + 1)))

Tactic:
((summable_nat_add_iff 1).mpr this).mul_left (-2 * π * I)

Premises used: Iff.mpr, summable_nat_add_iff, Real.pi, HMul.hMul, Complex.ofReal, Summable.mul_left, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n /
      (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n)
h :
  Eq (α := ℕ → ℂ) (fun (i : ℕ) ↦ logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) z) fun (i : ℕ) ↦
    -2 * (↑π : ℂ) * I *
      (HPow.hPow (α := ℂ) (β := ℕ) (↑(i + 1) : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ (i + 1) /
        (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ (i + 1)))
⊢ Summable (α := ℂ) fun (i : ℕ) ↦ logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) z

Tactic:
convert! ((summable_nat_add_iff 1).mpr this).mul_left (-2 * π * I) using 1 with n

Premises used: Iff.mpr, summable_nat_add_iff, Real.pi, HMul.hMul, Complex.ofReal, Summable.mul_left, OfNat.ofNat, Neg.neg, Complex.I
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℂ
hz : z ∈ ℍₒ
this :
  Summable (α := ℂ) fun (n : ℕ) ↦
    HPow.hPow (α := ℂ) (β := ℕ) (↑n : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n /
      (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ n)
⊢ Eq (α := ℕ → ℂ) (fun (i : ℕ) ↦ logDeriv (fun (x : ℂ) ↦ 1 - eta_q i x) z) fun (i : ℕ) ↦
    -2 * (↑π : ℂ) * I *
      (HPow.hPow (α := ℂ) (β := ℕ) (↑(i + 1) : ℂ) 1 * 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ (i + 1) /
        (1 - 𝕢 (↑1 : ℝ) (↑{ coe := z, coe_im_pos := hz : ℍ } : ℂ) ^ (i + 1)))

Tactic:
grind [one_sub_eta_logDeriv_eq]

Premises used: _private.0.ModularForm.one_sub_eta_logDeriv_eq
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℍ
⊢ DifferentiableAt ℂ (𝕢 24) (↑z : ℂ)

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℍ
rw : logDeriv (𝕢 24) (↑z : ℂ) + logDeriv (fun (x : ℂ) ↦ ∏' (n : ℕ), (1 - eta_q n x)) (↑z : ℂ) = (↑π : ℂ) * I / 12 * E2 z
⊢ logDeriv (fun (z : ℂ) ↦ 𝕢 24 z * ∏' (n : ℕ), (1 - eta_q n z)) (↑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)]

Premises used: logDeriv_mul, ModularForm.differentiableAt_eta_tprod, Function.Periodic.qParam_ne_zero, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℍ
⊢ ∀ (i : ℕ), DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ 1 - eta_q i x) ℍₒ

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.DedekindEta
Goal:
z : ℍ
⊢ 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)
-- 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 : ℂ) +
      2 * (↑π : ℂ) * I * ∑' (n : ℕ), HAdd.hAdd (α := ℂ) (↑n : ℂ) 1 * -eta_q n (↑z : ℂ) / (1 - eta_q n (↑z : ℂ)) =
    (↑π : ℂ) * I / 12 * ((riemannZeta 2)⁻¹ * 2⁻¹ * G2 z)
⊢ logDeriv (𝕢 24) (↑z : ℂ) + logDeriv (fun (x : ℂ) ↦ ∏' (n : ℕ), (1 - eta_q n x)) (↑z : ℂ) = (↑π : ℂ) * I / 12 * E2 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]

Premises used: UpperHalfPlane.coe, ModularForm.tsum_logDeriv_eta_q, one_div, EisensteinSeries.E2, mul_inv_rev, smul_eq_mul, OfNat.ofNat, ModularForm.logDeriv_qParam, Pi.smul_apply