awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ : SL(2, ℤ)
this : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) γ
one :
  @SlashAction.map ℤ SL(2, ℤ) _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 1 G2 =
    G2 - D2 1
mem :
  ∀ (g : SL(2, ℤ)) (hg : Membership.mem (γ := Set SL(2, ℤ)) {S, T} g),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ G2 = G2 - D2 γ
have mul : ∀ (g h : SL(2, ℤ)),
  Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g →
    Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) h →
      ∀
        (ig :
          @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 =
            G2 - D2 g)
        (ih :
          @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 h G2 =
            G2 - D2 h),
        @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 (g * h) G2 =
          G2 - D2 (g * h)
Tactic: induction this using Subgroup.closure_induction with
  | one => simp only [SlashAction.slash_one, D2_one, sub_zero]
  | mem g hg =>
      simp only [mem_insert_iff, mem_singleton_iff] at hg
      rcases hg with (h1 | h2)
      · ext z
        simp only [Pi.sub_apply, h1, D2_S z, SlashInvariantForm.slash_S_apply G2 2 z, mul_comm,
          G2_S_transform z, modular_S_smul]
        ring_nf
        aesop
      · simpa only [h2, D2_T, sub_zero] using G2_T_transform
  | mul g h _ _ ig ih =>
      rw [D2_mul, SlashAction.slash_mul, ig, sub_eq_add_neg, SlashAction.add_slash, ih]
      grind [SlashAction.neg_slash, SL_slash]
  | inv g _ ig =>
      have H1 : (G2 ∣[(2 : ℤ)] g) ∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g) ∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
      simp_rw [← SlashAction.slash_mul, sub_eq_add_neg, SlashAction.add_slash, mul_inv_cancel,
        SlashAction.slash_one, SL_slash, SlashAction.neg_slash] at H1
      nth_rw 2 [H1]
      have := D2_inv g
      simp only [SL_slash] at this
      rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ : SL(2, ℤ)
this : Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) γ
one :
  @SlashAction.map ℤ SL(2, ℤ) _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 1 G2 =
    G2 - D2 1
mem :
  ∀ (g : SL(2, ℤ)) (hg : Membership.mem (γ := Set SL(2, ℤ)) {S, T} g),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 = G2 - D2 g
mul :
  ∀ (g h : SL(2, ℤ)),
    Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g →
      Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) h →
        ∀
          (ig :
            @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 =
              G2 - D2 g)
          (ih :
            @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 h G2 =
              G2 - D2 h),
          @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 (g * h) G2 =
            G2 - D2 (g * h)
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ G2 = G2 - D2 γ
have inv : ∀ (g : SL(2, ℤ)),
  Membership.mem (γ := Subgroup SL(2, ℤ)) (Subgroup.closure {S, T}) g →
    ∀
      (ig :
        @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g G2 =
          G2 - D2 g),
      @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 g⁻¹ G2 =
        G2 - D2 g⁻¹
Tactic: induction this using Subgroup.closure_induction with
  | one => simp only [SlashAction.slash_one, D2_one, sub_zero]
  | mem g hg =>
      simp only [mem_insert_iff, mem_singleton_iff] at hg
      rcases hg with (h1 | h2)
      · ext z
        simp only [Pi.sub_apply, h1, D2_S z, SlashInvariantForm.slash_S_apply G2 2 z, mul_comm,
          G2_S_transform z, modular_S_smul]
        ring_nf
        aesop
      · simpa only [h2, D2_T, sub_zero] using G2_T_transform
  | mul g h _ _ ig ih =>
      rw [D2_mul, SlashAction.slash_mul, ig, sub_eq_add_neg, SlashAction.add_slash, ih]
      grind [SlashAction.neg_slash, SL_slash]
  | inv g _ ig =>
      have H1 : (G2 ∣[(2 : ℤ)] g) ∣[(2 : ℤ)] g⁻¹ = (G2 - D2 g) ∣[(2 : ℤ)] g⁻¹ := by
        rw [ig]
      simp_rw [← SlashAction.slash_mul, sub_eq_add_neg, SlashAction.add_slash, mul_inv_cancel,
        SlashAction.slash_one, SL_slash, SlashAction.neg_slash] at H1
      nth_rw 2 [H1]
      have := D2_inv g
      simp only [SL_slash] at this
      rw [← sub_eq_add_neg, this, SL_slash, sub_neg_eq_add, add_sub_cancel_right]
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform (goal)
Goal:
γ : SL(2, ℤ)
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ E2 =
    E2 - (1 / (2 * riemannZeta 2)) • D2 γ
have h : ∀ (z : ℍ),
  @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ E2 z =
    (E2 - (1 / (2 * riemannZeta 2)) • D2 γ) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ LT.lt (α := ℝ) 2 (↑k : ℝ)
have norm_cast : 2 < k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (hypothesis)
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ Summable (α := ℝ) fun (x : Fin 2 → ℤ) ↦ ‖eisSummand k x z‖
have hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
Tactic: have hk' : (2 : ℝ) < k := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
⊢ Summable (α := ℝ) fun (x : Fin 2 → ℤ) ↦ ‖eisSummand k x z‖
have apply : ∀ (b : Fin 2 → ℤ), ‖eisSummand k b z‖ ≤ HPow.hPow (β := ℝ) (r z) (-(↑k : ℝ)) * HPow.hPow (β := ℝ) ‖b‖ (-(↑k : ℝ))
Tactic: apply ((summable_one_div_norm_rpow hk').mul_left <| r z ^ (-k : ℝ)).of_nonneg_of_le
    (fun _ ↦ norm_nonneg _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
b : Fin 2 → ℤ
⊢ ‖eisSummand k b z‖ ≤ HPow.hPow (β := ℝ) (r z) (-(↑k : ℝ)) * HPow.hPow (β := ℝ) ‖b‖ (-(↑k : ℝ))
have simp : ‖(↑(b 0) : ℂ) * (↑z : ℂ) + (↑(b 1) : ℂ)‖ ^ (-k) ≤
  HPow.hPow (β := ℝ) (r z) (-(↑k : ℝ)) * HPow.hPow (β := ℝ) ‖b‖ (-(↑k : ℝ))
Tactic: simp only [eisSummand, norm_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ IsBoundedAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A
      (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ))
have simp_rw : ∃ (M : ℝ) (A_1 : ℝ),
  ∀ (z : ℍ),
    A_1 ≤ z.im →
      norm (E := ℂ)
          (@SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A
              (⇑{ toFun := eisensteinSeries a k, slash_action_eq' := sorry :
                    SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
                (a : ℍ) → ℂ)
              z :
            ℂ) ≤
        M
Tactic: simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeriesSIF] at *
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ ∃ (M : ℝ) (A_1 : ℝ),
    ∀ (z : ℍ),
      A_1 ≤ z.im →
        norm (E := ℂ)
            (@SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A
                (⇑{ toFun := eisensteinSeries a k, slash_action_eq' := ⋯ :
                      SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
                  (a : ℍ) → ℂ)
                z :
              ℂ) ≤
          M
have refine : ∀ (z : ℍ),
  2 ≤ z.im →
    norm (E := ℂ)
        (@SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A
            (⇑{ toFun := eisensteinSeries a k, slash_action_eq' := sorry :
                  SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
              (a : ℍ) → ℂ)
            z :
          ℂ) ≤
      ∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := sorry : ℍ } ^ (-k) * ‖x‖ ^ (-k)
Tactic: refine ⟨∑'(x : Fin 2 → ℤ), r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k) * ‖x‖ ^ (-k), 2, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
⊢ norm (E := ℂ)
      (@SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A
          (⇑{ toFun := eisensteinSeries a k, slash_action_eq' := ⋯ :
                SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
            (a : ℍ) → ℂ)
          z :
        ℂ) ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)
have obtain : ∀ (n : ℤ) (hn : ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im),
  norm (E := ℂ)
      (@SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A
          (⇑{ toFun := eisensteinSeries a k, slash_action_eq' := sorry :
                SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
            (a : ℍ) → ℂ)
          z :
        ℂ) ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := sorry : ℍ } ^ (-k) * ‖x‖ ^ (-k)
Tactic: obtain ⟨n, hn⟩ := (ModularGroup_T_zpow_mem_verticalStrip z (NeZero.pos N))
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im
⊢ norm (E := ℂ)
      (@SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A
          (⇑{ toFun := eisensteinSeries a k, slash_action_eq' := ⋯ :
                SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
            (a : ℍ) → ℂ)
          z :
        ℂ) ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)
have rw : norm (E := ℂ)
    ((eisensteinSeriesSIF
            (a ᵥ*
              (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) A) :
                Matrix (Fin 2) (Fin 2) (ZMod N)))
            k :
          (a : ℍ) → ℂ)
        (ModularGroup.T ^ ((↑N : ℤ) * n) • z) :
      ℂ) ≤
  ∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := sorry : ℍ } ^ (-k) * ‖x‖ ^ (-k)
Tactic: rw [SlashInvariantForm.coe_mk, eisensteinSeries_slash_apply, ← eisensteinSeriesSIF_apply,
    ← T_zpow_width_invariant N k n (eisensteinSeriesSIF (a ᵥ* A) k) z]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im
⊢ norm (E := ℂ)
      ((eisensteinSeriesSIF
              (a ᵥ*
                (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N)) : (a : SL(2, ℤ)) → SL(2, ZMod N)) A) :
                  Matrix (Fin 2) (Fin 2) (ZMod N)))
              k :
            (a : ℍ) → ℂ)
          (ModularGroup.T ^ ((↑N : ℤ) * n) • z) :
        ℂ) ≤
    ∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)
have apply : LE.le (α := ℝ) (∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ ((↑N : ℤ) * n) • z)‖)
  (∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := sorry : ℍ } ^ (-k) * ‖x‖ ^ (-k))
Tactic: apply le_trans (norm_le_tsum_norm N (a ᵥ* A) k hk _)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im
⊢ LT.lt (α := ℝ) 2 (↑k : ℝ)
have norm_cast : 2 < k
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (hypothesis)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im
⊢ LE.le (α := ℝ) (∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ ((↑N : ℤ) * n) • z)‖)
    (∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k))
have hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
Tactic: have hk' : (2 : ℝ) < k := by norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
⊢ LE.le (α := ℝ) (∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ ((↑N : ℤ) * n) • z)‖)
    (∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k))
have apply : Summable (α := ℝ) fun (i : Fin 2 → ℤ) ↦
  r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := sorry : ℍ } ^ (-k) * ‖i‖ ^ (-k)
Tactic: apply (summable_norm_eisSummand hk _).tsum_le_tsum _
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
apply :
  Summable (α := ℝ) fun (i : Fin 2 → ℤ) ↦
    r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖i‖ ^ (-k)
⊢ LE.le (α := ℝ) (∑' (x : Fin 2 → ℤ), ‖eisSummand k x (ModularGroup.T ^ ((↑N : ℤ) * n) • z)‖)
    (∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k))
have apply₁ : ∀ (i : Fin 2 → ℤ),
  ‖eisSummand k i (ModularGroup.T ^ ((↑N : ℤ) * n) • z)‖ ≤
    r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := sorry : ℍ } ^ (-k) * ‖i‖ ^ (-k)
Tactic: apply (summable_norm_eisSummand hk _).tsum_le_tsum _
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty (goal)
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ ((↑N : ℤ) * n) • z ∈ verticalStrip (↑N : ℝ) z.im
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
x : Fin 2 → ℤ
⊢ ‖eisSummand k x (ModularGroup.T ^ ((↑N : ℤ) * n) • z)‖ ≤
    r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)
have simp_rw : ‖(↑(x 0) : ℂ) * (↑(ModularGroup.T ^ ((↑N : ℤ) * n) • z) : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤
  r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := sorry : ℍ } ^ (-k) * ‖x‖ ^ (-k)
Tactic: simp_rw [eisSummand, norm_zpow]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
a : Fin 2 → ℤ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
have inl : ∀ (ha : a ≠ 0), DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
Tactic: rcases ne_or_eq a 0 with ha | rfl
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
a : Fin 2 → ℤ
inl :
  ∀ (ha : a ≠ 0),
    DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
have inr : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(0 0) : ℂ) * z + (↑(0 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
Tactic: rcases ne_or_eq a 0 with ha | rfl
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
have inl : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ)) {z : ℂ | 0 < z.im}
Tactic: apply DifferentiableOn.zpow
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
inl : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ)) {z : ℂ | 0 < z.im}
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
have inl₁ : (∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ) ≠ 0) ∨ 0 ≤ -k
Tactic: apply DifferentiableOn.zpow
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ (∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ) ≠ 0) ∨ 0 ≤ -k
have inl : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ) ≠ 0
Tactic: left
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(0 0) : ℂ) * z + (↑(0 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
have inr : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) 0 (-k)) {z : ℂ | 0 < z.im}
Tactic: simp only [Pi.zero_apply, Int.cast_zero, zero_mul, add_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
a : Fin 2 → ℤ
⊢ DifferentiableOn ℂ (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
have apply : ∀ (x : ℂ),
  Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x →
    (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) x = ((↑(a 0) : ℂ) * x + (↑(a 1) : ℂ)) ^ (-k)
Tactic: apply DifferentiableOn.congr (div_linear_zpow_differentiableOn k a)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
a : Fin 2 → ℤ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
⊢ (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) z = ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)
have lift : ∀ (z : ℍ), (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) = ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) ^ (-k)
Tactic: lift z to ℍ using hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
this : DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ MDiffAt (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) τ
have h : Eq (α := ℍ → ℂ) (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ)
  (((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) ∘ UpperHalfPlane.coe)
Tactic: convert!
      MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ MDiffAt (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) τ
have suffices : DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
Tactic: suffices DifferentiableAt ℂ (↑ₕeisensteinSeriesSIF a k) τ.1 by
    convert!
      MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
    exact funext fun z ↦ (comp_ofComplex (eisensteinSeriesSIF a k) z).symm
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable (goal)
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
⊢ DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
have refine : DifferentiableOn ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) upperHalfPlaneSet
Tactic: refine DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
⊢ EqOn (β := ℂ) (iteratedDerivWithin k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) S)
    (fun (s : ℂ) ↦ (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) S
have apply : EqOn (β := ℂ) (iteratedDeriv k fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ)))
  (fun (s : ℂ) ↦ (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) S
Tactic: apply EqOn.trans (iteratedDerivWithin_of_isOpen hs)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
⊢ Eq (α := (s : ℂ) → ℂ) (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) fun (s : ℂ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * s)
have h : ∀ (z : ℂ), cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * z / (↑p : ℂ)) = cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * z)
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (hypothesis)
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
⊢ Eq (α := ℂ) (iteratedDeriv k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) x)
    ((fun (s : ℂ) ↦ (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) x)
have this : Eq (α := (s : ℂ) → ℂ) (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) fun (s : ℂ) ↦
  cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * s)
Tactic: have : (fun s ↦ cexp (2 * π * I * m * s / p)) = fun s ↦ cexp (((2 * π * I * m) / p) * s) := by
    ext z
    ring_nf
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
this :
  Eq (α := (s : ℂ) → ℂ) (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) fun (s : ℂ) ↦
    cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * s)
⊢ Eq (α := ℂ) (iteratedDeriv k (fun (s : ℂ) ↦ cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) x)
    ((fun (s : ℂ) ↦ (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * s / (↑p : ℂ))) x)
have simp : (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ) * x) =
  (2 * (↑π : ℂ) * I * (↑m : ℂ) / (↑p : ℂ)) ^ k * cexp (2 * (↑π : ℂ) * I * (↑m : ℂ) * x / (↑p : ℂ))
Tactic: simp only [this, iteratedDeriv_cexp_const_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion (goal)
Goal:
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : Asymptotics.IsBigO (F := ℝ) atTop f fun (n : ℕ) ↦ HPow.hPow (α := ℝ) (↑n : ℝ) l
⊢ Eq (α := (n : ℕ) → ℂ) (fun (n : ℕ) ↦ (2 * (↑π : ℂ) * I * (↑n : ℂ) / (↑p : ℂ)) ^ k) fun (n : ℕ) ↦
    (2 * (↑π : ℂ) * I / (↑p : ℂ)) ^ k * HPow.hPow (α := ℂ) (↑n : ℂ) k
have h : ∀ (z : ℕ),
  (2 * (↑π : ℂ) * I * (↑z : ℂ) / (↑p : ℂ)) ^ k = (2 * (↑π : ℂ) * I / (↑p : ℂ)) ^ k * HPow.hPow (α := ℂ) (↑z : ℂ) k
Tactic: ext z