bump to nightly-2023-06-28-11

mathlib commit leanprover-community/mathlib@8b98191

Mathbin/NumberTheory/ModularForms/SlashInvariantForms.lean

@@ -40,50 +40,62 @@ open ModularForm
 
 variable (F : Type _) (Γ : outParam <| Subgroup SL(2, ℤ)) (k : outParam ℤ)
 
+#print SlashInvariantForm /-
 /-- Functions `ℍ → ℂ` that are invariant under the `slash_action`. -/
 structure SlashInvariantForm where
   toFun : ℍ → ℂ
   slash_action_eq' : ∀ γ : Γ, to_fun ∣[k] γ = to_fun
 #align slash_invariant_form SlashInvariantForm
+-/
 
+#print SlashInvariantFormClass /-
 /-- `slash_invariant_form_class F Γ k` asserts `F` is a type of bundled functions that are invariant
 under the `slash_action`. -/
 class SlashInvariantFormClass extends FunLike F ℍ fun _ => ℂ where
   slash_action_eq : ∀ (f : F) (γ : Γ), (f : ℍ → ℂ) ∣[k] γ = f
 #align slash_invariant_form_class SlashInvariantFormClass
+-/
 
 attribute [nolint dangerous_instance] SlashInvariantFormClass.toFunLike
 
+#print SlashInvariantFormClass.slashInvariantForm /-
 instance (priority := 100) SlashInvariantFormClass.slashInvariantForm :
     SlashInvariantFormClass (SlashInvariantForm Γ k) Γ k
     where
   coe := SlashInvariantForm.toFun
   coe_injective' f g h := by cases f <;> cases g <;> congr
   slash_action_eq := SlashInvariantForm.slash_action_eq'
 #align slash_invariant_form_class.slash_invariant_form SlashInvariantFormClass.slashInvariantForm
+-/
 
 variable {F Γ k}
 
 instance : CoeFun (SlashInvariantForm Γ k) fun _ => ℍ → ℂ :=
   FunLike.hasCoeToFun
 
+#print slashInvariantForm_toFun_eq_coe /-
 @[simp]
 theorem slashInvariantForm_toFun_eq_coe {f : SlashInvariantForm Γ k} : f.toFun = (f : ℍ → ℂ) :=
   rfl
 #align slash_invariant_form_to_fun_eq_coe slashInvariantForm_toFun_eq_coe
+-/
 
+#print slashInvariantForm_ext /-
 @[ext]
 theorem slashInvariantForm_ext {f g : SlashInvariantForm Γ k} (h : ∀ x, f x = g x) : f = g :=
   FunLike.ext f g h
 #align slash_invariant_form_ext slashInvariantForm_ext
+-/
 
+#print SlashInvariantForm.copy /-
 /-- Copy of a `slash_invariant_form` with a new `to_fun` equal to the old one.
 Useful to fix definitional equalities. -/
 protected def SlashInvariantForm.copy (f : SlashInvariantForm Γ k) (f' : ℍ → ℂ) (h : f' = ⇑f) :
     SlashInvariantForm Γ k where
   toFun := f'
   slash_action_eq' := h.symm ▸ f.slash_action_eq'
 #align slash_invariant_form.copy SlashInvariantForm.copy
+-/
 
 end SlashInvariantForms
 
@@ -93,128 +105,168 @@ open SlashInvariantForm
 
 variable {F : Type _} {Γ : outParam <| Subgroup SL(2, ℤ)} {k : outParam ℤ}
 
+#print SlashInvariantForm.SlashInvariantFormClass.coeToFun /-
 @[nolint dangerous_instance]
 instance (priority := 100) SlashInvariantFormClass.coeToFun [SlashInvariantFormClass F Γ k] :
     CoeFun F fun _ => ℍ → ℂ :=
   FunLike.hasCoeToFun
 #align slash_invariant_form.slash_invariant_form_class.coe_to_fun SlashInvariantForm.SlashInvariantFormClass.coeToFun
+-/
 
+#print SlashInvariantForm.slash_action_eqn /-
 @[simp]
 theorem slash_action_eqn [SlashInvariantFormClass F Γ k] (f : F) (γ : Γ) : ⇑f ∣[k] γ = ⇑f :=
   SlashInvariantFormClass.slash_action_eq f γ
 #align slash_invariant_form.slash_action_eqn SlashInvariantForm.slash_action_eqn
+-/
 
+#print SlashInvariantForm.slash_action_eqn' /-
 theorem slash_action_eqn' (k : ℤ) (Γ : Subgroup SL(2, ℤ)) [SlashInvariantFormClass F Γ k] (f : F)
     (γ : Γ) (z : ℍ) : f (γ • z) = ((↑ₘ[ℤ] γ 1 0 : ℂ) * z + (↑ₘ[ℤ] γ 1 1 : ℂ)) ^ k * f z :=
   by
   rw [← ModularForm.slash_action_eq'_iff]
   simp
 #align slash_invariant_form.slash_action_eqn' SlashInvariantForm.slash_action_eqn'
+-/
 
 instance [SlashInvariantFormClass F Γ k] : CoeTC F (SlashInvariantForm Γ k) :=
   ⟨fun f =>
     { toFun := f
       slash_action_eq' := slash_action_eqn f }⟩
 
+#print SlashInvariantForm.SlashInvariantFormClass.coe_coe /-
 @[simp]
 theorem SlashInvariantFormClass.coe_coe [SlashInvariantFormClass F Γ k] (f : F) :
     ((f : SlashInvariantForm Γ k) : ℍ → ℂ) = f :=
   rfl
 #align slash_invariant_form.slash_invariant_form_class.coe_coe SlashInvariantForm.SlashInvariantFormClass.coe_coe
+-/
 
+#print SlashInvariantForm.hasAdd /-
 instance hasAdd : Add (SlashInvariantForm Γ k) :=
   ⟨fun f g =>
     { toFun := f + g
       slash_action_eq' := fun γ => by
         rw [SlashAction.add_slash, slash_action_eqn, slash_action_eqn] }⟩
 #align slash_invariant_form.has_add SlashInvariantForm.hasAdd
+-/
 
+#print SlashInvariantForm.coe_add /-
 @[simp]
 theorem coe_add (f g : SlashInvariantForm Γ k) : ⇑(f + g) = f + g :=
   rfl
 #align slash_invariant_form.coe_add SlashInvariantForm.coe_add
+-/
 
+#print SlashInvariantForm.add_apply /-
 @[simp]
 theorem add_apply (f g : SlashInvariantForm Γ k) (z : ℍ) : (f + g) z = f z + g z :=
   rfl
 #align slash_invariant_form.add_apply SlashInvariantForm.add_apply
+-/
 
+#print SlashInvariantForm.hasZero /-
 instance hasZero : Zero (SlashInvariantForm Γ k) :=
   ⟨{  toFun := 0
       slash_action_eq' := SlashAction.zero_slash _ }⟩
 #align slash_invariant_form.has_zero SlashInvariantForm.hasZero
+-/
 
+#print SlashInvariantForm.coe_zero /-
 @[simp]
 theorem coe_zero : ⇑(0 : SlashInvariantForm Γ k) = (0 : ℍ → ℂ) :=
   rfl
 #align slash_invariant_form.coe_zero SlashInvariantForm.coe_zero
+-/
 
 section
 
 variable {α : Type _} [SMul α ℂ] [IsScalarTower α ℂ ℂ]
 
+#print SlashInvariantForm.hasSmul /-
 instance hasSmul : SMul α (SlashInvariantForm Γ k) :=
   ⟨fun c f =>
     { toFun := c • f
       slash_action_eq' := fun γ => by rw [SlashAction.smul_slash_of_tower, slash_action_eqn] }⟩
 #align slash_invariant_form.has_smul SlashInvariantForm.hasSmul
+-/
 
+#print SlashInvariantForm.coe_smul /-
 @[simp]
 theorem coe_smul (f : SlashInvariantForm Γ k) (n : α) : ⇑(n • f) = n • f :=
   rfl
 #align slash_invariant_form.coe_smul SlashInvariantForm.coe_smul
+-/
 
+#print SlashInvariantForm.smul_apply /-
 @[simp]
 theorem smul_apply (f : SlashInvariantForm Γ k) (n : α) (z : ℍ) : (n • f) z = n • f z :=
   rfl
 #align slash_invariant_form.smul_apply SlashInvariantForm.smul_apply
+-/
 
 end
 
+#print SlashInvariantForm.hasNeg /-
 instance hasNeg : Neg (SlashInvariantForm Γ k) :=
   ⟨fun f =>
     { toFun := -f
       slash_action_eq' := fun γ => by rw [SlashAction.neg_slash, slash_action_eqn] }⟩
 #align slash_invariant_form.has_neg SlashInvariantForm.hasNeg
+-/
 
+#print SlashInvariantForm.coe_neg /-
 @[simp]
 theorem coe_neg (f : SlashInvariantForm Γ k) : ⇑(-f) = -f :=
   rfl
 #align slash_invariant_form.coe_neg SlashInvariantForm.coe_neg
+-/
 
+#print SlashInvariantForm.neg_apply /-
 @[simp]
 theorem neg_apply (f : SlashInvariantForm Γ k) (z : ℍ) : (-f) z = -f z :=
   rfl
 #align slash_invariant_form.neg_apply SlashInvariantForm.neg_apply
+-/
 
+#print SlashInvariantForm.hasSub /-
 instance hasSub : Sub (SlashInvariantForm Γ k) :=
   ⟨fun f g => f + -g⟩
 #align slash_invariant_form.has_sub SlashInvariantForm.hasSub
+-/
 
+#print SlashInvariantForm.coe_sub /-
 @[simp]
 theorem coe_sub (f g : SlashInvariantForm Γ k) : ⇑(f - g) = f - g :=
   rfl
 #align slash_invariant_form.coe_sub SlashInvariantForm.coe_sub
+-/
 
+#print SlashInvariantForm.sub_apply /-
 @[simp]
 theorem sub_apply (f g : SlashInvariantForm Γ k) (z : ℍ) : (f - g) z = f z - g z :=
   rfl
 #align slash_invariant_form.sub_apply SlashInvariantForm.sub_apply
+-/
 
 instance : AddCommGroup (SlashInvariantForm Γ k) :=
   FunLike.coe_injective.AddCommGroup _ rfl coe_add coe_neg coe_sub coe_smul coe_smul
 
+#print SlashInvariantForm.coeHom /-
 /-- Additive coercion from `slash_invariant_form` to `ℍ → ℂ`.-/
 def coeHom : SlashInvariantForm Γ k →+ ℍ → ℂ
     where
   toFun f := f
   map_zero' := rfl
   map_add' _ _ := rfl
 #align slash_invariant_form.coe_hom SlashInvariantForm.coeHom
+-/
 
+#print SlashInvariantForm.coeHom_injective /-
 theorem coeHom_injective : Function.Injective (@coeHom Γ k) :=
   FunLike.coe_injective
 #align slash_invariant_form.coe_hom_injective SlashInvariantForm.coeHom_injective
+-/
 
 instance : Module ℂ (SlashInvariantForm Γ k) :=
   coeHom_injective.Module ℂ coeHom fun _ _ => rfl
@@ -223,10 +275,12 @@ instance : One (SlashInvariantForm Γ 0) :=
   ⟨{  toFun := 1
       slash_action_eq' := fun A => ModularForm.is_invariant_one A }⟩
 
+#print SlashInvariantForm.one_coe_eq_one /-
 @[simp]
 theorem one_coe_eq_one : ((1 : SlashInvariantForm Γ 0) : ℍ → ℂ) = 1 :=
   rfl
 #align slash_invariant_form.one_coe_eq_one SlashInvariantForm.one_coe_eq_one
+-/
 
 instance : Inhabited (SlashInvariantForm Γ k) :=
   ⟨0⟩

lake-manifest.json

@@ -10,15 +10,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean3port.git",
     "subDir?": null,
-    "rev": "dc9173dafb79cc4968ea917bffaba2823dbfdacd",
+    "rev": "484963a6aa63ee8668e06b2e1e63f15159cc8a7d",
     "name": "lean3port",
-    "inputRev?": "dc9173dafb79cc4968ea917bffaba2823dbfdacd"}},
+    "inputRev?": "484963a6aa63ee8668e06b2e1e63f15159cc8a7d"}},
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "e703ae87cdacf4b5445b4d174d81bf13f423689d",
+    "rev": "fd35d093f0887cf7c01c81eaa04545e4b18d8007",
     "name": "mathlib",
-    "inputRev?": "e703ae87cdacf4b5445b4d174d81bf13f423689d"}},
+    "inputRev?": "fd35d093f0887cf7c01c81eaa04545e4b18d8007"}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
     "subDir?": null,

lakefile.lean

@@ -4,7 +4,7 @@ open Lake DSL System
 -- Usually the `tag` will be of the form `nightly-2021-11-22`.
 -- If you would like to use an artifact from a PR build,
 -- it will be of the form `pr-branchname-sha`.
-def tag : String := "nightly-2023-06-28-09"
+def tag : String := "nightly-2023-06-28-11"
 def releaseRepo : String := "leanprover-community/mathport"
 def oleanTarName : String := "mathlib3-binport.tar.gz"
 
@@ -38,7 +38,7 @@ target fetchOleans (_pkg : Package) : Unit := do
     untarReleaseArtifact releaseRepo tag oleanTarName libDir
   return .nil
 
-require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"dc9173dafb79cc4968ea917bffaba2823dbfdacd"
+require lean3port from git "https://github.com/leanprover-community/lean3port.git"@"484963a6aa63ee8668e06b2e1e63f15159cc8a7d"
 
 @[default_target]
 lean_lib Mathbin where