awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ @SlashAction.map _ _ _ Units.instMonoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k g f = f
have 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
Tactic: rcases hg with rfl | rfl
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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)
have refine_1 : ∀ (q : ℂ) (hq : Membership.mem (γ := Set ℂ) (Metric.ball 0 1) q),
  DifferentiableWithinAt ℂ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ)) (Metric.ball 0 1) q
Tactic: refine eq_const_of_exists_le (fun q hq ↦ ?_) (exp_nonneg (-π)) ?_ (fun q hq ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ Set.EqOn (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ))
    (Function.const ℂ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)) (Metric.ball 0 1)
have refine_2 : rexp (-π) < 1
Tactic: refine eq_const_of_exists_le (fun q hq ↦ ?_) (exp_nonneg (-π)) ?_ (fun q hq ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ Set.EqOn (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ))
    (Function.const ℂ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)) (Metric.ball 0 1)
have 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‖
Tactic: refine eq_const_of_exists_le (fun q hq ↦ ?_) (exp_nonneg (-π)) ?_ (fun q hq ↦ ?_)
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ ∃ (w : ℂ),
    Membership.mem (γ := Set ℂ) (Metric.closedBall 0 (rexp (-π))) w ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
have refine_3 : ∃ (w : ℂ),
  ‖w‖ ≤ rexp (-π) ∧
    ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
Tactic: simp only [Metric.mem_closedBall, dist_zero_right]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ ∃ (w : ℂ),
    ‖w‖ ≤ rexp (-π) ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
have 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‖
Tactic: rcases eq_or_ne q 0 with rfl | hq'
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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‖
⊢ ∃ (w : ℂ),
    ‖w‖ ≤ rexp (-π) ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
have refine_3₁ : ∀ (hq' : q ≠ 0),
  ∃ (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'
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ ∃ (w : ℂ),
    ‖w‖ ≤ rexp (-π) ∧
      ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) w‖
have refine_3 : ∀ (ξ : ℍ) (hξ : 1 / 2 ≤ ξ.im)
  (hξ₂ :
    Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) { coe := invQParam 1 q, coe_im_pos := sorry : ℍ } : ℂ) ≤
      Norm.norm (E := ℂ) ((f : (a : ℍ) → ℂ) ξ : ℂ)),
  ∃ (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'⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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)
have h : ∀ (z : ℍ), (f : (a : ℍ) → ℂ) z = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (hypothesis)
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 : ℍ
⊢ (f : (a : ℍ) → ℂ) z = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0) z
have hQ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (hypothesis)
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
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have hf : (⇑f : (a : ℍ) → ℂ) = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0)
Tactic: have hf := levelOne_nonpos_wt_const hk.le f
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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)
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have inl : ∀ [ModularFormClass F (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0]
  (hk : LT.lt (α := ℤ) 0 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
Tactic: rcases wt_eq_zero_of_eq_const k hf with rfl | hf₀
Cleared hypotheses: k, inst_1, hk
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have inr : ∀ (hf₀ : UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0 = 0), Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
Tactic: rcases wt_eq_zero_of_eq_const k hf with rfl | hf₀
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have inr : Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f : (a : ℍ) → ℂ) 0) = 0
Tactic: rw [hf, hf₀, const_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have inr₁ : Eq (α := (a : ℍ) → ℂ) (Function.const ℍ 0) 0
Tactic: rw [hf, hf₀, const_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
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
⊢ Eq (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) 0
have inr₂ : Eq (α := (a : ℍ) → ℂ) 0 0
Tactic: rw [hf, hf₀, const_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
Goal:
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) = 1
have refine : ∀ (g : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0),
  ∃ (c : ℂ),
    HSMul.hSMul (β := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) c (const 1) =
      g
Tactic: refine rank_eq_one (const 1) (by simp [DFunLike.ne_iff]) fun g ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
Goal:
g : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0
⊢ ∃ (c : ℂ),
    HSMul.hSMul (β := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) c (const 1) =
      g
have obtain : ∀ (c' : ℂ) (hc' : (⇑g : (a : ℍ) → ℂ) = Function.const ℍ c'),
  ∃ (c : ℂ),
    HSMul.hSMul (β := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) 0) c (const 1) =
      g
Tactic: obtain ⟨c', hc'⟩ := levelOne_weight_zero_const g
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.Basic (goal)
Goal:
k : ℤ
hk : k < 0
⊢ Module.rank ℂ (ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k) = 0
have refine : ∀ (f : ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k),
  HSMul.hSMul (α := ℂ) 1 f = 0
Tactic: refine rank_eq_zero_iff.mpr fun f ↦ ⟨_, one_ne_zero, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (hypothesis)
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
γ : SL(2, ℤ)
⊢ Eq (α := (z : ℍ) → ℂ)
    (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
      fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z))
    fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z)
have hγ : Membership.mem (α := GL (Fin 2) ℝ) (γ := Subgroup (GL (Fin 2) ℝ))
  (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
  ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
      ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
    GL (Fin 2) ℝ)
Tactic: have hγ : (γ : GL (Fin 2) ℝ) ∈ 𝒮ℒ := ⟨γ, rfl⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
γ : SL(2, ℤ)
hγ :
  Membership.mem (α := GL (Fin 2) ℝ) (γ := Subgroup (GL (Fin 2) ℝ))
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
      GL (Fin 2) ℝ)
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
      (HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)) =
    HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)
have simp_rw : HDiv.hDiv (α := ℍ → ℂ)
    (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
      (⇑f : (a : ℍ) → ℂ))
    (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ
      (⇑discriminant : (a : ℍ) → ℂ)) =
  HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)
Tactic: simp_rw [div_slash_SL2, SL_slash, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
γ : SL(2, ℤ)
hγ :
  Membership.mem (α := GL (Fin 2) ℝ) (γ := Subgroup (GL (Fin 2) ℝ))
    (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
    ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
      GL (Fin 2) ℝ)
simp_rw :
  HDiv.hDiv (α := ℍ → ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ k γ
        (⇑f : (a : ℍ) → ℂ))
      (@SlashAction.map ℤ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12 γ
        (⇑discriminant : (a : ℍ) → ℂ)) =
    HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)
⊢ @SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
      (HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)) =
    HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)
have simp_rw₁ : HDiv.hDiv (α := ℍ → ℂ)
    (@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, ℝ)) γ) :
        GL (Fin 2) ℝ)
      (⇑f : (a : ℍ) → ℂ))
    (@SlashAction.map ℤ (GL (Fin 2) ℝ) _ (Units.instMonoid : Monoid (Matrix (Fin 2) (Fin 2) ℝ)ˣ)
      (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ 12
      ((Matrix.SpecialLinearGroup.toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) γ) :
        GL (Fin 2) ℝ)
      (⇑discriminant : (a : ℍ) → ℂ)) =
  HDiv.hDiv (α := (a : ℍ) → ℂ) (⇑f : (a : ℍ) → ℂ) (⇑discriminant : (a : ℍ) → ℂ)
Tactic: simp_rw [div_slash_SL2, SL_slash, slash_action_eqn _ _ hγ]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
⊢ c.IsBoundedAt (fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z)) (k - 12)
have rw : ∀ (γ : SL(2, ℤ)),
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
        ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
      c →
    IsBoundedAtImInfty (α := ℂ)
      (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
        fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z))
Tactic: rw [isBoundedAt_iff_forall_SL2Z hc]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
f : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
c : OnePoint ℝ
hc : IsCusp c (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ))
γ : SL(2, ℤ)
h :
  HSMul.hSMul (α := GL (Fin 2) ℝ) (β := OnePoint ℝ)
      ((Matrix.SpecialLinearGroup.mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) γ : GL (Fin 2) ℝ) ∞ =
    c
⊢ IsBoundedAtImInfty (α := ℂ)
    (@SlashAction.map _ _ _ Matrix.SpecialLinearGroup.monoid (Pi.addMonoid (f := fun (a : ℍ) ↦ ℂ)) _ (k - 12) γ
      fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z))
have rw : IsBigO (E := ℂ) (F := ℝ) atImInfty (fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((f : (a : ℍ) → ℂ) z : ℂ) (Δ z)) 1
Tactic: rw [divByDiscriminant_slash_eq f γ, IsBoundedAtImInfty, BoundedAtFilter]
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
a b : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
⊢ { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a + b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
      bdd_at_cusps' := ⋯ } =
    HAdd.hAdd (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
      { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
        bdd_at_cusps' := ⋯ :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }
      { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯, holo' := ⋯,
        bdd_at_cusps' := ⋯ :
        ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }
have h : ∀ (z : ℍ),
  Eq (α := ℂ)
    (({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a + b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := sorry,
            holo' := sorry, bdd_at_cusps' := sorry } :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((HAdd.hAdd (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
            { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := sorry,
              holo' := sorry, bdd_at_cusps' := sorry :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }
            { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := sorry,
              holo' := sorry, bdd_at_cusps' := sorry :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) } :
          (a : ℍ) → ℂ)
        z :
      ℂ)
Tactic: ext z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
a b : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
⊢ Eq (α := ℂ)
    (({ toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a + b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
            holo' := ⋯, bdd_at_cusps' := ⋯ } :
          (a : ℍ) → ℂ)
        z :
      ℂ)
    ((HAdd.hAdd (α := ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12))
            { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
              holo' := ⋯, bdd_at_cusps' := ⋯ :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) }
            { toFun := fun (z : ℍ) ↦ HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z), slash_action_eq' := ⋯,
              holo' := ⋯, bdd_at_cusps' := ⋯ :
              ModularForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) (k - 12) } :
          (a : ℍ) → ℂ)
        z :
      ℂ)
have h : HAdd.hAdd (α := ℂ) (β := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) / Δ z =
  HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) + HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z)
Tactic: change (a z + b z) / Δ z = a z / Δ z + b z / Δ z
-- Lean 4 proof step from Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula (goal)
Goal:
k : ℤ
a b : CuspForm (MonoidHom.range (G := SL(2, ℤ)) (Matrix.SpecialLinearGroup.mapGL ℝ)) k
z : ℍ
⊢ HAdd.hAdd (α := ℂ) (β := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) / Δ z =
    HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) + HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z)
have h : HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) + HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z) =
  HDiv.hDiv (α := ℂ) ((a : (a : ℍ) → ℂ) z : ℂ) (Δ z) + HDiv.hDiv (α := ℂ) ((b : (a : ℍ) → ℂ) z : ℂ) (Δ z)
Tactic: rw [add_div]