awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
rw :
  Eq (α := Subgroup (GL (Fin 2) ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ) ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) S : GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) T : GL (Fin 2) ℝ))))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))
⊢ Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))

Tactic:
rw [MonoidHom.range_eq_map, ← SpecialLinearGroup.SL2Z_generators, MonoidHom.map_closure,
      Set.image_pair]

Premises used: Set.image_pair, MonoidHom.range_eq_map, SpecialLinearGroup.SL2Z_generators, MonoidHom.map_closure
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
⊢ Eq (α := Subgroup (GL (Fin 2) ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ) ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) S : GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) T : GL (Fin 2) ℝ))))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))

Tactic:
rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
⊢ Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))

Tactic:
have h𝒮ℒ : 𝒮ℒ = Subgroup.closure ({↑S, ↑T} : Set (GL (Fin 2) ℝ)) := by
    change (Matrix.SpecialLinearGroup.mapGL ℝ).range = _
    rw [MonoidHom.range_eq_map, ← SpecialLinearGroup.SL2Z_generators, MonoidHom.map_closure,
      Set.image_pair]
    rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
h𝒮ℒ :
  Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))
g : GL (Fin 2) ℝ
hg :
  Membership.mem (γ := Set (GL (Fin 2) ℝ))
    (insert (α := GL (Fin 2) ℝ)
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
        GL (Fin 2) ℝ)
      (singleton (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
          GL (Fin 2) ℝ)))
    g
inl :
  @SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
        GL (Fin 2) ℝ)
      f =
    f
inr :
  @SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
        GL (Fin 2) ℝ)
      f =
    f
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f = f

Tactic:
rcases hg with rfl | rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
h𝒮ℒ :
  Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))
⊢ @SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
        GL (Fin 2) ℝ)
      f =
    f

Tactic:
assumption
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
h𝒮ℒ :
  Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))
⊢ @SlashAction.map _ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
        GL (Fin 2) ℝ)
      f =
    f

Tactic:
assumption
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
f : ℍ → ℂ
k : ℤ
hS : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k S f = f
hT : @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k T f = f
γ : SL(2, ℤ)
h𝒮ℒ :
  Eq (α := Subgroup (GL (Fin 2) ℝ)) (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    (Subgroup.closure
      (insert (α := GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S) :
          GL (Fin 2) ℝ)
        (singleton (α := GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) T) :
            GL (Fin 2) ℝ))))
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ f = f

Tactic:
exact (slash_action_generators h𝒮ℒ).mpr (fun g hg ↦ by rcases hg with rfl | rfl <;> assumption)
    _ (MonoidHom.mem_range.mpr ⟨γ, rfl⟩)

Premises used: Iff.mpr, SlashInvariantForm.slash_action_generators, MonoidHom.mem_range, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
⊢ 1 ∈ Subgroup.strictPeriods (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
⊢ Set.EqOn (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ))
    (Function.const ℂ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)) (Metric.ball 0 1)

Tactic:
eq_const_of_exists_le (fun q hq ↦ ?_) (exp_nonneg (-π)) ?_ (fun q hq ↦ ?_)

Premises used: Complex.eq_const_of_exists_le, Real.pi, Real.exp_nonneg, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
refine_1 :
  ∀ (q : ℂ) (hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q),
    DifferentiableWithinAt ℂ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ)) (Metric.ball 0 1) q
refine_2 : rexp (-π) < 1
refine_3 :
  ∀ (q : ℂ) (hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q),
    ∃ (w : ℂ),
      Membership.mem (γ := Set ℂ) (Metric.closedBall 0 (rexp (-π))) w ∧
        ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
⊢ Set.EqOn (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ))
    (Function.const ℂ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)) (Metric.ball 0 1)

Tactic:
refine eq_const_of_exists_le (fun q hq ↦ ?_) (exp_nonneg (-π)) ?_ (fun q hq ↦ ?_)

Premises used: Complex.eq_const_of_exists_le, Real.pi, Real.exp_nonneg, Neg.neg
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
⊢ DifferentiableWithinAt ℂ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ)) (Metric.ball 0 1) q

Tactic:
(ModularFormClass.differentiableAt_cuspFunction f one_pos one_mem_strictPeriods_SL
      (mem_ball_zero_iff.mp hq)).differentiableWithinAt

Premises used: one_mem_strictPeriods_SL, DifferentiableAt.differentiableWithinAt, ModularFormClass.differentiableAt_cuspFunction, Iff.mp, one_pos, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
⊢ DifferentiableWithinAt ℂ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ)) (Metric.ball 0 1) q

Tactic:
exact (ModularFormClass.differentiableAt_cuspFunction f one_pos one_mem_strictPeriods_SL
      (mem_ball_zero_iff.mp hq)).differentiableWithinAt

Premises used: one_mem_strictPeriods_SL, DifferentiableAt.differentiableWithinAt, ModularFormClass.differentiableAt_cuspFunction, Iff.mp, one_pos, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
⊢ rexp (-π) < 1

Tactic:
simp [pi_pos]

Premises used: Real.pi_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
refine_3 :
  ∃ (w : ℂ),
    ‖w‖ ≤ rexp (-π) ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
⊢ ∃ (w : ℂ),
    Membership.mem (γ := Set ℂ) (Metric.closedBall 0 (rexp (-π))) w ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖

Tactic:
simp only [Metric.mem_closedBall, dist_zero_right]

Premises used: Metric.mem_closedBall, dist_zero_right
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
refine_3 :
  ∀ (hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0),
    ∃ (w : ℂ),
      ‖w‖ ≤ rexp (-π) ∧
        ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
refine_3₁ :
  ∀ (hq' : q ≠ 0),
    ∃ (w : ℂ),
      ‖w‖ ≤ rexp (-π) ∧
        ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
⊢ ∃ (w : ℂ),
    ‖w‖ ≤ rexp (-π) ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖

Tactic:
rcases eq_or_ne q 0 with rfl | hq'

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0
⊢ Norm.norm (E := ℂ) 0 ≤ rexp (-π)

Tactic:
simpa only [norm_zero] using exp_nonneg _

Premises used: norm_zero, Real.exp_nonneg
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) 0
⊢ ∃ (w : ℂ),
    ‖w‖ ≤ rexp (-π) ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖

Tactic:
refine ⟨0, by simpa only [norm_zero] using exp_nonneg _, le_rfl⟩
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
hq' : q ≠ 0
refine_3 :
  ∀ (ξ : ℍ) (hξ : 1 / 2 ≤ ξ.im)
    (hξ₂ :
      Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) { coe := invQParam 1 q, coe_im_pos := ⋯ : ℍ } : ℂ) ≤
        Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) ξ : ℂ)),
    ∃ (w : ℂ),
      ‖w‖ ≤ rexp (-π) ∧
        ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
⊢ ∃ (w : ℂ),
    ‖w‖ ≤ rexp (-π) ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖

Tactic:
obtain ⟨ξ, hξ, hξ₂⟩ := exists_one_half_le_im_and_norm_le hk f
        ⟨_, im_invQParam_pos_of_norm_lt_one Real.zero_lt_one (mem_ball_zero_iff.mp hq) hq'⟩

Premises used: UpperHalfPlane.mk, SlashInvariantForm.exists_one_half_le_im_and_norm_le, Real.zero_lt_one, Function.Periodic.im_invQParam_pos_of_norm_lt_one, Iff.mp, mem_ball_zero_iff
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ :
  Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) { coe := invQParam 1 q, coe_im_pos := ⋯ : ℍ } : ℂ) ≤
    Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) ξ : ℂ)
⊢ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤
    ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) (𝕢 1 (↑ξ : ℂ))‖

Tactic:
simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL
            one_ne_zero, qParam_right_inv one_ne_zero hq'] using hξ₂

Premises used: SlashInvariantFormClass.eq_cuspFunction, one_mem_strictPeriods_SL, Function.Periodic.qParam_right_inv, one_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
q : ℂ
hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ :
  Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) { coe := invQParam 1 q, coe_im_pos := ⋯ : ℍ } : ℂ) ≤
    Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) ξ : ℂ)
⊢ ∃ (w : ℂ),
    ‖w‖ ≤ rexp (-π) ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖

Tactic:
exact ⟨_, norm_qParam_le_of_one_half_le_im hξ,
        by simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL
            one_ne_zero, qParam_right_inv one_ne_zero hq'] using hξ₂⟩
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
h : ∀ (z : ℍ), (f : (a : ℍ) → ℂ) z = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0) z
⊢ (⇑f : (a : ℍ) → ℂ) = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)

Tactic:
ext z
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
z : ℍ
⊢ Membership.mem (γ := Set ℂ) (Metric.ball 0 1) (𝕢 1 (↑z : ℂ))

Tactic:
simpa using (norm_qParam_lt_iff zero_lt_one 0 z.1).mpr z.2

Premises used: Iff.mpr, Function.Periodic.norm_qParam_lt_iff, UpperHalfPlane.coe, zero_lt_one, OfNat.ofNat, UpperHalfPlane.coe_im_pos
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
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_iff zero_lt_one 0 z.1).mpr z.2
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k ≤ 0
f : F
z : ℍ
hQ : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) (𝕢 1 (↑z : ℂ))
⊢ (f : (a : ℍ) → ℂ) z = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0) z

Tactic:
simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL one_ne_zero]
    using cuspFunction_eqOn_const_of_nonpos_wt hk f hQ

Premises used: SlashInvariantFormClass.eq_cuspFunction, one_mem_strictPeriods_SL, _private.0.ModularFormClass.cuspFunction_eqOn_const_of_nonpos_wt, one_ne_zero
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k < 0
f : F
⊢ (⇑f : (a : ℍ) → ℂ) = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)

Tactic:
have hf := levelOne_nonpos_wt_const hk.le f
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k < 0
f : F
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)
inl :
  ∀ [ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0]
    (hk : LT.lt (α := ℤ) 0 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
inr : ∀ (hf₀ : UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0 = 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
rcases wt_eq_zero_of_eq_const k hf with rfl | hf₀

Premises used: SlashInvariantForm.wt_eq_zero_of_eq_const, rfl
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0
hk : LT.lt (α := ℤ) 0 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
(lt_irrefl _ hk).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
f : F
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0
hk : LT.lt (α := ℤ) 0 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
exact (lt_irrefl _ hk).elim

Premises used: lt_irrefl, False.elim
-- Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic
Goal:
F : Type u_1
inst : FunLike F ℍ ℂ
k : ℤ
inst_1 : ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
hk : k < 0
f : F
hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)
hf₀ : UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0 = 0
inr : Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0) = 0
inr₁ : Eq (α := (a : ℍ) → ℂ) (Function.const ℍ 0) 0
inr₂ inr₃ : Eq (α := (a : ℍ) → ℂ) 0 0
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0

Tactic:
rw [hf, hf₀, const_zero]

Premises used: Function.const_zero