awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
h :
  (r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ })⁻¹ * ‖![m 0 + a, m 1 + b]‖⁻¹ ≤
    ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖
⊢ ‖(HAdd.hAdd (α := ℂ) (↑(m 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + (↑b : ℂ))⁻¹‖ ≤
    ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖

Tactic:
apply le_trans (by simpa [Real.rpow_neg_one, add_assoc] using
    summand_bound_of_mem_verticalStrip zero_le_one ![m 0 + a, m 1 + b] z.2 h0)

Premises used: le_trans
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
h0 : z ∈ verticalStrip |z.re| z.im
m : Fin 2 → ℤ
⊢ (r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ })⁻¹ * ‖![m 0 + a, m 1 + b]‖⁻¹ ≤
    ‖r { coe := { re := |z.re|, im := z.im : ℂ }, coe_im_pos := ⋯ : ℍ }‖⁻¹ * ‖‖![m 0 + a, m 1 + b]‖⁻¹‖

Tactic:
simp [abs_of_pos (r_pos _)]

Premises used: EisensteinSeries.r_pos, abs_of_pos
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
α : Type u_1
a : α
inst : NormedAddCommGroup α
inst_1 : DiscreteTopology α
inst_2 : ProperSpace α
⊢ IsLittleO (E := α) (F := ℝ) cofinite (fun (x : α) ↦ a) fun (x : α) ↦ ‖x‖

Tactic:
simpa [isLittleO_const_left, Function.comp_def] using
    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding IsClosedEmbedding.id

Premises used: Asymptotics.isLittleO_const_left, Topology.IsClosedEmbedding.id, Function.comp_def, tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
a b : ℤ
⊢ ∀ (x : Fin 2 → ℤ), ![x 0 + a, x 1 + b] = x + ![a, b]

Tactic:
have (x : Fin 2 → ℤ) : ![x 0 + a, x 1 + b] = x + ![a, b] := List.ofFn_inj.mp rfl
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
a b : ℤ
this : ∀ (x : Fin 2 → ℤ), ![x 0 + a, x 1 + b] = x + ![a, b]
rw rw₁ :
  IsTheta (E := ℝ) (F := ℝ) cofinite (fun (x : Fin (Nat.succ 0).succ → ℤ) ↦ ‖x‖) fun (x : Fin (Nat.succ 0).succ → ℤ) ↦
    ‖x‖
⊢ IsTheta (E := Fin (Nat.succ 0).succ → ℤ) (F := ℝ) cofinite (fun (x : Fin 2 → ℤ) ↦ x)
    fun (x : Fin (Nat.succ 0).succ → ℤ) ↦ ‖x‖

Tactic:
rw [← isTheta_norm_left]

Premises used: Asymptotics.isTheta_norm_left
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
a b : ℤ
this : ∀ (x : Fin 2 → ℤ), ![x 0 + a, x 1 + b] = x + ![a, b]
⊢ IsTheta (E := ℝ) (F := ℝ) cofinite (fun (m : Fin 2 → ℤ) ↦ ‖![m 0 + a, m 1 + b]‖⁻¹) fun (m : Fin 2 → ℤ) ↦ ‖m‖⁻¹

Tactic:
simpa only [isTheta_inv, isTheta_norm_left, this] using (IsTheta.add_isLittleO
  (by rw [← isTheta_norm_left]) (isLittleO_const_left_of_properSpace_of_discreteTopology ![a, b]))

Premises used: Asymptotics.isTheta_inv, Asymptotics.IsTheta.add_isLittleO, Asymptotics.isTheta_norm_left, Matrix.vecEmpty, EisensteinSeries.isLittleO_const_left_of_properSpace_of_discreteTopology, Matrix.vecCons
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
z : ℍ
a b : ℤ
⊢ IsBigO (E := ℂ) (F := ℝ) cofinite
    (fun (m : Fin 2 → ℤ) ↦ (HAdd.hAdd (α := ℂ) (↑(m 0) : ℂ) (↑a : ℂ) * (↑z : ℂ) + (↑(m 1) : ℂ) + (↑b : ℂ))⁻¹)
    fun (m : Fin 2 → ℤ) ↦ ‖m‖⁻¹

Tactic:
(aux_isBigO_linear z a b).trans (vec_add_const_isTheta a b).isBigO

Premises used: Asymptotics.IsBigO.trans, Asymptotics.IsTheta.isBigO, _private.0.EisensteinSeries.aux_isBigO_linear, EisensteinSeries.vec_add_const_isTheta
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
f : (Fin 2 → ℤ) → E
a : ℝ
hab : 2 < a
hf : IsBigO (F := ℝ) cofinite f fun (n : Fin 2 → ℤ) ↦ (‖n‖ ^ a)⁻¹
⊢ Summable f

Tactic:
summable_of_isBigO
    ((summable_one_div_norm_rpow hab).congr fun b ↦ Real.rpow_neg (norm_nonneg b) a) hf

Premises used: EisensteinSeries.summable_one_div_norm_rpow, Summable.congr, summable_of_isBigO, Real.rpow_neg, norm_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : 2 < k
⊢ LT.lt (α := ℝ) 2 (↑k : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
⊢ LT.lt (α := ℝ) 2 (↑k : ℝ)

Tactic:
have hk' : (2 : ℝ) < k := by norm_cast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
⊢ Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)

Tactic:
have p_sum : Summable fun x : gammaSet N 1 a ↦ ‖x.val‖ ^ (-k) :=
    mod_cast (summable_one_div_norm_rpow hk').subtype (gammaSet N 1 a)
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
simp :
  ∀ (K : Set ℍ),
    IsCompact K →
      TendstoUniformlyOn (β := ℂ)
        (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
        (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K
⊢ TendstoLocallyUniformly (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ eisensteinSeries a k x) Filter.atTop

Tactic:
simp only [tendstoLocallyUniformly_iff_forall_isCompact, eisensteinSeries]

Premises used: tendstoLocallyUniformly_iff_forall_isCompact, eisensteinSeries
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
obtain :
  ∀ (A B : ℝ) (hB : 0 < B) (HABK : K ⊆ verticalStrip A B),
    TendstoUniformlyOn (β := ℂ)
      (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
      (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K
⊢ TendstoUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K

Tactic:
obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact hK

Premises used: UpperHalfPlane.subset_verticalStrip_of_isCompact
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
⊢ TendstoUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K

Tactic:
(tendstoUniformlyOn_tsum (hu := p_sum.mul_left <| r ⟨⟨A, B⟩, hB⟩ ^ (-k : ℝ))
    (fun p z hz ↦ ?_)).mono HABK

Premises used: Int.cast, EisensteinSeries.r, TendstoUniformlyOn.mono, tendstoUniformlyOn_tsum, UpperHalfPlane.mk, Summable.mul_left, HPow.hPow, Complex.mk, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
refine :
  ∀ (p : (↑(gammaSet N 1 a) : Type)) (z : ℍ) (hz : z ∈ verticalStrip A B),
    ‖eisSummand k (↑p : Fin 2 → ℤ) z‖ ≤
      HPow.hPow (β := ℝ) (r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ }) (-(↑k : ℝ)) *
        ‖(↑p : Fin 2 → ℤ)‖ ^ (-k)
⊢ TendstoUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) (x : ℍ) ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1 : Fin 2 → ℤ) x)
    (fun (x : ℍ) ↦ ∑' (x_1 : (↑(gammaSet N 1 a) : Type)), eisSummand k (↑x_1 : Fin 2 → ℤ) x) Filter.atTop K

Tactic:
refine (tendstoUniformlyOn_tsum (hu := p_sum.mul_left <| r ⟨⟨A, B⟩, hB⟩ ^ (-k : ℝ))
    (fun p z hz ↦ ?_)).mono HABK

Premises used: Int.cast, EisensteinSeries.r, TendstoUniformlyOn.mono, tendstoUniformlyOn_tsum, UpperHalfPlane.mk, Summable.mul_left, HPow.hPow, Complex.mk, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : (↑(gammaSet N 1 a) : Type)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ LE.le (α := ℝ) 0 (↑k : ℝ)

Tactic:
positivity
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : LT.lt (α := ℝ) 2 (↑k : ℝ)
p_sum : Summable (α := ℝ) fun (x : (↑(gammaSet N 1 a) : Type)) ↦ ‖(↑x : Fin 2 → ℤ)‖ ^ (-k)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : (↑(gammaSet N 1 a) : Type)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ ‖eisSummand k (↑p : Fin 2 → ℤ) z‖ ≤
    HPow.hPow (β := ℝ) (r { coe := { re := A, im := B : ℂ }, coe_im_pos := hB : ℍ }) (-(↑k : ℝ)) *
      ‖(↑p : Fin 2 → ℤ)‖ ^ (-k)

Tactic:
simpa only [eisSummand, one_div, ← zpow_neg, norm_zpow, ← Real.rpow_intCast,
    Int.cast_neg] using summand_bound_of_mem_verticalStrip (by positivity) p hB hz

Premises used: Int.cast_neg, EisensteinSeries.summand_bound_of_mem_verticalStrip, zpow_neg, one_div, EisensteinSeries.eisSummand, norm_zpow, Subtype.val, Real.rpow_intCast
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
rw :
  TendstoLocallyUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) ↦
      (fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k (↑x : Fin 2 → ℤ) z) ∘ (↑ofComplex : ℂ → ℍ))
    ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) Filter.atTop (UpperHalfPlane.coe '' Set.univ)
⊢ TendstoLocallyUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) ↦
      (fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k (↑x : Fin 2 → ℤ) z) ∘ (↑ofComplex : ℂ → ℍ))
    ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) Filter.atTop {z : ℂ | 0 < z.im}

Tactic:
rw [← upperHalfPlaneSet, ← range_coe, ← image_univ]

Premises used: Set.image_univ, UpperHalfPlane.upperHalfPlaneSet, UpperHalfPlane.range_coe
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
apply :
  TendstoLocallyUniformlyOn (β := ℂ)
    (fun (n : Finset (↑(gammaSet N 1 a) : Type)) (z : ℍ) ↦ ∑ x ∈ n, eisSummand k (↑x : Fin 2 → ℤ) z)
    (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) Filter.atTop ⊤
apply₁ :
  MapsTo (↑(IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).symm : ℂ → ℍ)
    (IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).target ⊤
⊢ TendstoLocallyUniformlyOn (β := ℂ)
    (fun (s : Finset (↑(gammaSet N 1 a) : Type)) ↦
      (fun (z : ℍ) ↦ ∑ x ∈ s, eisSummand k (↑x : Fin 2 → ℤ) z) ∘ (↑ofComplex : ℂ → ℍ))
    ((⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) ∘ (↑ofComplex : ℂ → ℍ)) Filter.atTop (UpperHalfPlane.coe '' Set.univ)

Tactic:
apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (OpenPartialHomeomorph.continuousOn_symm _)

Premises used: TendstoLocallyUniformlyOn.comp, OpenPartialHomeomorph.continuousOn_symm
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
simp :
  TendstoLocallyUniformly (β := ℂ)
    (fun (n : Finset (↑(gammaSet N 1 a) : Type)) (z : ℍ) ↦ ∑ x ∈ n, eisSummand k (↑x : Fin 2 → ℤ) z)
    (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) Filter.atTop
⊢ TendstoLocallyUniformlyOn (β := ℂ)
    (fun (n : Finset (↑(gammaSet N 1 a) : Type)) (z : ℍ) ↦ ∑ x ∈ n, eisSummand k (↑x : Fin 2 → ℤ) z)
    (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) Filter.atTop ⊤

Tactic:
simp only [Set.top_eq_univ, tendstoLocallyUniformlyOn_univ]

Premises used: Set.top_eq_univ, tendstoLocallyUniformlyOn_univ
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformly (β := ℂ)
    (fun (n : Finset (↑(gammaSet N 1 a) : Type)) (z : ℍ) ↦ ∑ x ∈ n, eisSummand k (↑x : Fin 2 → ℤ) z)
    (⇑(eisensteinSeriesSIF a k) : (a : ℍ) → ℂ) Filter.atTop

Tactic:
apply eisensteinSeries_tendstoLocallyUniformly hk

Premises used: EisensteinSeries.eisensteinSeries_tendstoLocallyUniformly
-- Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
Goal:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ MapsTo (↑(IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).symm : ℂ → ℍ)
    (IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).target ⊤

Tactic:
simp only [IsOpenEmbedding.toOpenPartialHomeomorph_target, Set.top_eq_univ, mapsTo_range_iff,
    Set.mem_univ, forall_const]

Premises used: Set.top_eq_univ, Set.mapsTo_range_iff, Topology.IsOpenEmbedding.toOpenPartialHomeomorph_target, Set.mem_univ, forall_const
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
rw :
  Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ)
    (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
        ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) (⇑f : (a : ℍ) → ℂ) τ :
      ℂ)
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ) ((f : (a : ℍ) → ℂ) τ : ℂ)

Tactic:
rw [← congr_fun (slash_action_eqn f _ <| Γ.mem_strictPeriods_iff.mp hH) τ]

Premises used: Iff.mp, Subgroup.mem_strictPeriods_iff, congr_fun, SlashInvariantForm.slash_action_eqn
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
this :
  HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ =
    h +ᵥ τ
simp_rw :
  (f : (a : ℍ) → ℂ) (h +ᵥ τ) =
    HMul.hMul (α := ℂ)
        ((σ ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h) : (a : ℂ) → ℂ)
            ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ) :
          ℂ)
        ((↑|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ)
                      ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h)) :
                  ℝ)| :
            ℂ) ^
          (k - 1)) *
      denom ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h) (↑τ : ℂ) ^ (-k)
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ)
    (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
        ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) (⇑f : (a : ℍ) → ℂ) τ :
      ℂ)

Tactic:
simp_rw [slash_def, this]

Premises used: ModularForm.slash_def
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
this :
  HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ =
    h +ᵥ τ
⊢ (f : (a : ℍ) → ℂ) (h +ᵥ τ) =
    HMul.hMul (α := ℂ)
        ((σ ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h) : (a : ℂ) → ℂ)
            ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ) :
          ℂ)
        ((↑|(↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ)
                      ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h)) :
                  ℝ)| :
            ℂ) ^
          (k - 1)) *
      denom ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h) (↑τ : ℂ) ^ (-k)

Tactic:
simp [σ, denom, GeneralLinearGroup.val_det_apply, denom]

Premises used: UpperHalfPlane.denom, UpperHalfPlane.σ, Matrix.GeneralLinearGroup.val_det_apply
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
suffices :
  HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ =
    h +ᵥ τ
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (h +ᵥ τ) : ℂ)
    (@SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
        (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
        ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) (⇑f : (a : ℍ) → ℂ) τ :
      ℂ)

Tactic:
suffices GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ by
    simp_rw [slash_def, this]
    simp [σ, denom, GeneralLinearGroup.val_det_apply, denom]
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
coe :
  (↑(HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ) :
      ℂ) =
    (↑(h +ᵥ τ) : ℂ)
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ =
    h +ᵥ τ

Tactic:
ext
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst : FunLike F ℍ ℂ
inst_1 : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
⊢ (↑(HSMul.hSMul (α := GL (Fin 2) ℝ) ((GeneralLinearGroup.upperRightHom : (a : ℝ) → GL (Fin 2) ℝ) h : GL (Fin 2) ℝ) τ) :
      ℂ) =
    (↑(h +ᵥ τ) : ℂ)

Tactic:
simp [σ, num, denom, coe_vadd, UpperHalfPlane.coe_smul, num, add_comm]

Premises used: UpperHalfPlane.coe_smul, add_comm, UpperHalfPlane.denom, UpperHalfPlane.coe_vadd, UpperHalfPlane.σ, UpperHalfPlane.num
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
hH : HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) ∈ Subgroup.strictPeriods (Subgroup.map (mapGL ℝ) Γ(N))
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) +ᵥ z) : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
apply vAdd_apply_of_mem_strictPeriods

Premises used: SlashInvariantForm.vAdd_apply_of_mem_strictPeriods
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ HMul.hMul (α := ℝ) (↑N : ℝ) (↑n : ℝ) ∈ Subgroup.strictPeriods (Subgroup.map (mapGL ℝ) Γ(N))

Tactic:
simp [strictPeriods_Gamma, AddSubgroup.mem_zmultiples_iff, mul_comm]

Premises used: AddSubgroup.mem_zmultiples_iff, CongruenceSubgroup.strictPeriods_Gamma, mul_comm
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
rw : Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * n) : ℝ) z) : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (ModularGroup.T ^ ((↑N : ℤ) * n) • z) : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
rw [modular_T_zpow_smul z (N * n)]

Premises used: HMul.hMul, Nat.cast, UpperHalfPlane.modular_T_zpow_smul
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ Eq (α := ℂ) ((f : (a : ℍ) → ℂ) (HVAdd.hVAdd (α := ℝ) (↑((↑N : ℤ) * n) : ℝ) z) : ℂ) ((f : (a : ℍ) → ℂ) z : ℂ)

Tactic:
simpa only [Int.cast_mul, Int.cast_natCast] using vAdd_width_periodic N k n f z

Premises used: Int.cast_natCast, Int.cast_mul, SlashInvariantForm.vAdd_width_periodic
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
k : ℤ
z : ℍ
rw :
  f { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } *
      denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) ModularGroup.S))
          (↑z : ℂ) ^
        (-k) =
    f { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (↑z : ℂ) ^ (-k)
⊢ @SlashAction.map _ _ _ monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k ModularGroup.S f z =
    f { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (↑z : ℂ) ^ (-k)

Tactic:
rw [SL_slash_apply, modular_S_smul]

Premises used: UpperHalfPlane.modular_S_smul, ModularForm.SL_slash_apply
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ f { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } *
      denom
          ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) ModularGroup.S))
          (↑z : ℂ) ^
        (-k) =
    f { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ : ℍ } * (↑z : ℂ) ^ (-k)

Tactic:
simp [ModularGroup.S, denom]

Premises used: ModularGroup.S, UpperHalfPlane.denom
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
mp :
  (∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f) →
    ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
mpr :
  (∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f) →
    ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
⊢ (∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f) ↔
    ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f

Tactic:
constructor
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ s
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f

Tactic:
h γ (hΓ ▸ Subgroup.mem_closure_of_mem hγ)

Premises used: Eq.rec, Subgroup.mem_closure_of_mem, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ Γ, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ s
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f

Tactic:
exact h γ (hΓ ▸ Subgroup.mem_closure_of_mem hγ)

Premises used: Eq.rec, Subgroup.mem_closure_of_mem, Eq.symm
-- Module: Mathlib.NumberTheory.ModularForms.Identities
Goal:
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ @SlashAction.map _ (GL (Fin 2) ℝ) _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k 1 f = f

Tactic:
simp