awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
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)
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⁻¹
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ G2 = G2 - D2 γ

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]

Premises used: ModularForm.SL_slash, sub_zero, sub_eq_add_neg, UpperHalfPlane.modular_S_smul, SlashAction.slash_one, SlashAction.neg_slash, ModularForm.mul, SlashAction.slash_mul, Set.mem_singleton_iff, SlashAction.add_slash, EisensteinSeries.D2_one, mul_comm, mul_inv_cancel, Set.mem_insert_iff, add_sub_cancel_right, EisensteinSeries.D2_T, sub_neg_eq_add, EisensteinSeries.D2_mul, Pi.sub_apply, EisensteinSeries.G2_T_transform
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ : SL(2, ℤ)
h :
  ∀ (z : ℍ),
    @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ E2 z =
      (E2 - (1 / (2 * riemannZeta 2)) • D2 γ) z
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ E2 =
    E2 - (1 / (2 * riemannZeta 2)) • D2 γ

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
Goal:
γ : SL(2, ℤ)
z : ℍ
⊢ @SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 2 γ E2 z =
    (E2 - (1 / (2 * riemannZeta 2)) • D2 γ) z

Tactic:
simp [E2, SL_smul_slash, G2_slash_action γ, mul_sub]

Premises used: mul_sub, EisensteinSeries.G2_slash_action, EisensteinSeries.E2, ModularForm.SL_smul_slash
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 2 < k
⊢ LT.lt (α := ℝ) 2 (↑k : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ LT.lt (α := ℝ) 2 (↑k : ℝ)

Tactic:
have hk' : (2 : ℝ) < k := by norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
apply :
  ∀ (b : Fin 2 → ℤ), ‖eisSummand k b z‖ ≤ HPow.hPow (β := ℝ) (r z) (-(↑k : ℝ)) * HPow.hPow (β := ℝ) ‖b‖ (-(↑k : ℝ))
⊢ Summable (α := ℝ) fun (x : Fin 2 → ℤ) ↦ ‖eisSummand k x z‖

Tactic:
apply ((summable_one_div_norm_rpow hk').mul_left <| r z ^ (-k : ℝ)).of_nonneg_of_le
    (fun _ ↦ norm_nonneg _)

Premises used: Int.cast, EisensteinSeries.r, Summable.of_nonneg_of_le, EisensteinSeries.summable_one_div_norm_rpow, Summable.mul_left, HPow.hPow, norm_nonneg, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
b : Fin 2 → ℤ
simp :
  ‖(↑(b 0) : ℂ) * (↑z : ℂ) + (↑(b 1) : ℂ)‖ ^ (-k) ≤
    HPow.hPow (β := ℝ) (r z) (-(↑k : ℝ)) * HPow.hPow (β := ℝ) ‖b‖ (-(↑k : ℝ))
⊢ ‖eisSummand k b z‖ ≤ HPow.hPow (β := ℝ) (r z) (-(↑k : ℝ)) * HPow.hPow (β := ℝ) ‖b‖ (-(↑k : ℝ))

Tactic:
simp only [eisSummand, norm_zpow]

Premises used: EisensteinSeries.eisSummand, norm_zpow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
b : Fin 2 → ℤ
⊢ LE.le (α := ℝ) 0 (↑k : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
k : ℤ
hk : 3 ≤ k
z : ℍ
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
b : Fin 2 → ℤ
⊢ ‖(↑(b 0) : ℂ) * (↑z : ℂ) + (↑(b 1) : ℂ)‖ ^ (-k) ≤
    HPow.hPow (β := ℝ) (r z) (-(↑k : ℝ)) * HPow.hPow (β := ℝ) ‖b‖ (-(↑k : ℝ))

Tactic:
exact_mod_cast summand_bound z (show 0 ≤ (k : ℝ) by positivity) b

Premises used: EisensteinSeries.summand_bound
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ norm (E := ℂ) (∑' (x : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x : Fin 2 → ℤ) z) ≤
    ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖

Tactic:
apply le_trans (norm_tsum_le_tsum_norm ((summable_norm_eisSummand hk z).subtype _))
    (Summable.tsum_subtype_le (fun (x : Fin 2 → ℤ) ↦ ‖(eisSummand k x z)‖) _ (fun _ ↦ norm_nonneg _)
      (summable_norm_eisSummand hk z))

Premises used: Norm.norm, Summable.subtype, EisensteinSeries.summable_norm_eisSummand, Summable.tsum_subtype_le, norm_tsum_le_tsum_norm, EisensteinSeries.eisSummand, norm_nonneg, le_trans
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
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' := ⋯ :
                      SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
                  (a : ℍ) → ℂ)
                z :
              ℂ) ≤
          M
⊢ IsBoundedAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k A
      (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ))

Tactic:
simp_rw [UpperHalfPlane.isBoundedAtImInfty_iff, eisensteinSeriesSIF] at *

Premises used: UpperHalfPlane.isBoundedAtImInfty_iff, EisensteinSeries.eisensteinSeriesSIF
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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

Tactic:
⟨∑'(x : Fin 2 → ℤ), r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k) * ‖x‖ ^ (-k), 2, ?_⟩

Premises used: Norm.norm, HMul.hMul, EisensteinSeries.r, UpperHalfPlane.mk, Nat.ofNat_pos, Nat.cast, HPow.hPow, tsum, Exists.intro, OfNat.ofNat, Complex.mk, Neg.neg, SummationFilter.unconditional
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
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' := ⋯ :
                    SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
                (a : ℍ) → ℂ)
              z :
            ℂ) ≤
        ∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)
⊢ ∃ (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

Tactic:
refine ⟨∑'(x : Fin 2 → ℤ), r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k) * ‖x‖ ^ (-k), 2, ?_⟩
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
Goal:
N : ℕ
inst : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
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' := ⋯ :
                  SlashInvariantForm (Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)) k } :
              (a : ℍ) → ℂ)
            z :
          ℂ) ≤
      ∑' (x : Fin 2 → ℤ), r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)
⊢ 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)

Tactic:
obtain ⟨n, hn⟩ := (ModularGroup_T_zpow_mem_verticalStrip z (NeZero.pos N))

Premises used: UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip, NeZero.pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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
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 := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)
⊢ 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)

Tactic:
rw [SlashInvariantForm.coe_mk, eisensteinSeries_slash_apply, ← eisensteinSeriesSIF_apply,
    ← T_zpow_width_invariant N k n (eisensteinSeriesSIF (a ᵥ* A) k) z]

Premises used: Matrix.vecMul, SlashInvariantForm.coe_mk, ZMod, Matrix.SpecialLinearGroup.map, Int.castRingHom, EisensteinSeries.eisensteinSeriesSIF, EisensteinSeries.eisensteinSeriesSIF_apply, Subtype.val, EisensteinSeries.eisensteinSeries_slash_apply, DFunLike.coe, SlashInvariantForm.T_zpow_width_invariant
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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
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 := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k))
⊢ 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)

Tactic:
apply le_trans (norm_le_tsum_norm N (a ᵥ* A) k hk _)

Premises used: Matrix.vecMul, EisensteinSeries.norm_le_tsum_norm, ZMod, Matrix.SpecialLinearGroup.map, Int.castRingHom, Subtype.val, DFunLike.coe, le_trans
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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_cast norm_cast₁ norm_cast₂ norm_cast₃ : 2 < k
⊢ LT.lt (α := ℝ) 2 (↑k : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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 : ℝ)

Tactic:
have hk' : (2 : ℝ) < k := by norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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)
apply₁ :
  ∀ (i : Fin 2 → ℤ),
    ‖eisSummand k i (ModularGroup.T ^ ((↑N : ℤ) * n) • z)‖ ≤
      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))

Tactic:
apply (summable_norm_eisSummand hk _).tsum_le_tsum _

Premises used: EisensteinSeries.summable_norm_eisSummand, Summable.tsum_le_tsum
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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 : ℝ)
⊢ Summable (α := ℝ) fun (i : Fin 2 → ℤ) ↦
    r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖i‖ ^ (-k)

Tactic:
exact_mod_cast (summable_one_div_norm_rpow hk').mul_left <| r ⟨⟨N, 2⟩, Nat.ofNat_pos⟩ ^ (-k)

Premises used: EisensteinSeries.r, UpperHalfPlane.mk, Nat.ofNat_pos, EisensteinSeries.summable_one_div_norm_rpow, Nat.cast, Summable.mul_left, OfNat.ofNat, Complex.mk, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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 → ℤ
simp_rw :
  ‖(↑(x 0) : ℂ) * (↑(ModularGroup.T ^ ((↑N : ℤ) * n) • z) : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤
    r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)
⊢ ‖eisSummand k x (ModularGroup.T ^ ((↑N : ℤ) * n) • z)‖ ≤
    r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
simp_rw [eisSummand, norm_zpow]

Premises used: EisensteinSeries.eisSummand, norm_zpow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
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 → ℤ
⊢ ‖(↑(x 0) : ℂ) * (↑(ModularGroup.T ^ ((↑N : ℤ) * n) • z) : ℂ) + (↑(x 1) : ℂ)‖ ^ (-k) ≤
    r { coe := { re := (↑N : ℝ), im := 2 : ℂ }, coe_im_pos := ⋯ : ℍ } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
exact_mod_cast
      summand_bound_of_mem_verticalStrip (lt_trans two_pos hk').le x two_pos
      (verticalStrip_anti_right N hz hn)

Premises used: EisensteinSeries.summand_bound_of_mem_verticalStrip, lt_trans, two_pos, LT.lt.le, Nat.cast, UpperHalfPlane.verticalStrip_anti_right
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
inl :
  ∀ (ha : a ≠ 0),
    DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
inr : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(0 0) : ℂ) * z + (↑(0 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}

Tactic:
rcases ne_or_eq a 0 with ha | rfl

Premises used: ne_or_eq, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
inl : DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ)) {z : ℂ | 0 < z.im}
inl₁ : (∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ) ≠ 0) ∨ 0 ≤ -k
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}

Tactic:
apply DifferentiableOn.zpow

Premises used: DifferentiableOn.zpow
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ DifferentiableOn ℂ (F := ℂ) (fun (x : ℂ) ↦ (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ)) {z : ℂ | 0 < z.im}

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
inl : ∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ) ≠ 0
⊢ (∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ) ≠ 0) ∨ 0 ≤ -k

Tactic:
left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ) ≠ 0

Tactic:
fun z hz ↦ linear_ne_zero ⟨z, hz⟩
        ((comp_ne_zero_iff _ Int.cast_injective Int.cast_zero).mpr ha)

Premises used: Iff.mpr, Function.comp_ne_zero_iff, Int.cast_zero, UpperHalfPlane.mk, UpperHalfPlane.linear_ne_zero, Int.cast_injective
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ ∀ (x : ℂ), Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x → (↑(a 0) : ℂ) * x + (↑(a 1) : ℂ) ≠ 0

Tactic:
exact fun z hz ↦ linear_ne_zero ⟨z, hz⟩
        ((comp_ne_zero_iff _ Int.cast_injective Int.cast_zero).mpr ha)

Premises used: Iff.mpr, Function.comp_ne_zero_iff, Int.cast_zero, UpperHalfPlane.mk, UpperHalfPlane.linear_ne_zero, Int.cast_injective
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
inr : DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) 0 (-k)) {z : ℂ | 0 < z.im}
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ ((↑(0 0) : ℂ) * z + (↑(0 1) : ℂ)) ^ (-k)) {z : ℂ | 0 < z.im}

Tactic:
simp only [Pi.zero_apply, Int.cast_zero, zero_mul, add_zero]

Premises used: Int.cast_zero, MulZeroClass.zero_mul, Pi.zero_apply, add_zero
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
⊢ DifferentiableOn ℂ (F := ℂ) (fun (z : ℂ) ↦ HPow.hPow (α := ℂ) 0 (-k)) {z : ℂ | 0 < z.im}

Tactic:
apply differentiableOn_const

Premises used: differentiableOn_const
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
apply :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} x →
      (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) x = ((↑(a 0) : ℂ) * x + (↑(a 1) : ℂ)) ^ (-k)
⊢ DifferentiableOn ℂ (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}

Tactic:
apply DifferentiableOn.congr (div_linear_zpow_differentiableOn k a)

Premises used: DifferentiableOn.congr, EisensteinSeries.div_linear_zpow_differentiableOn
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
⊢ 0 < z.im

Tactic:
hz

Premises used: Set.Mem
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
z : ℂ
hz : Membership.mem (γ := Set ℂ) {z : ℂ | 0 < z.im} z
lift : ∀ (z : ℍ), (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) = ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) ^ (-k)
⊢ (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) z = ((↑(a 0) : ℂ) * z + (↑(a 1) : ℂ)) ^ (-k)

Tactic:
lift z to ℍ using hz
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
a : Fin 2 → ℤ
z : ℍ
⊢ (eisSummand k a ∘ (↑ofComplex : ℂ → ℍ)) (↑z : ℂ) = ((↑(a 0) : ℂ) * (↑z : ℂ) + (↑(a 1) : ℂ)) ^ (-k)

Tactic:
apply comp_ofComplex

Premises used: UpperHalfPlane.comp_ofComplex
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
this : DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ MDiffAt (((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) ∘ UpperHalfPlane.coe) τ

Tactic:
MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe

Premises used: UpperHalfPlane.mdifferentiable_coe, MDifferentiableAt.comp, DifferentiableAt.mdifferentiableAt
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
this : DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
h :
  Eq (α := ℍ → ℂ) (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ)
    (((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) ∘ UpperHalfPlane.coe)
⊢ MDiffAt (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) τ

Tactic:
convert!
      MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe

Premises used: UpperHalfPlane.mdifferentiable_coe, MDifferentiableAt.comp, DifferentiableAt.mdifferentiableAt
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
τ : ℍ
this : DifferentiableAt ℂ (F := ℂ) ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ Eq (α := ℍ → ℂ) (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ)
    (((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) ∘ UpperHalfPlane.coe)

Tactic:
funext fun z ↦ (comp_ofComplex (eisensteinSeriesSIF a k) z).symm

Premises used: UpperHalfPlane.comp_ofComplex, funext, EisensteinSeries.eisensteinSeriesSIF, Eq.symm, DFunLike.coe