mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.algebraMap_eq_inl' : ∀ (S : Type u_1) (R : Type u) (M : Type v) [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] (s : S),
  (algebraMap S (TrivSqZeroExt R M)) s = TrivSqZeroExt.inl ((algebraMap S R) s)
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.instReprParseResult.repr : {α ι : Type} → [Repr α] → [Repr ι] → Std.Internal.Parsec.ParseResult α ι → ℕ → Std.Format
-- Mathlib.GroupTheory.Coset.Basic
mem_rightCoset_rightCoset : ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α}, MulOpposite.op a • ↑s = ↑s → a ∈ s
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.eq_top_of_le_card : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Finite G], Nat.card G ≤ Nat.card ↥H → H = ⊤
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_mul : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k_1 k_2 : ℤ} [inst : Γ.HasDetPlusMinusOne] (f : ModularForm Γ k_1)
  (g : ModularForm Γ k_2), ⇑(f.mul g) = ⇑f * ⇑g
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_succ_of_isSome : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → Option α}, (f 0).isSome = true → Fin.findSome? f = f 0
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_lt_two_pow : ∀ (x : ℕ) {y n : ℕ}, y < 2 ^ n → x &&& y < 2 ^ n
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.toOplaxLeftLinear : {D : Type u_1} →
  {D' : Type u_2} →
    {inst : CategoryTheory.Category.{v_1, u_1} D} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            {inst_2 : CategoryTheory.Category.{v_3, u_3} C} →
              {inst_3 : CategoryTheory.MonoidalCategory C} →
                {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D} →
                  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} →
                    [self : F.LeftLinear C] → F.OplaxLeftLinear C
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
CovariantDerivative.isCovariantDerivativeOnUniv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V] (self : CovariantDerivative I F V),
  IsCovariantDerivativeOn F ↑self
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.reverse_comp_reverse : ∀ {T : Type u_1} {N : Type u_2}, ContextFreeRule.reverse ∘ ContextFreeRule.reverse = id
-- Mathlib.Algebra.Opposites
/-- The canonical bijection between `α` and `αᵃᵒᵖ`.  -/
AddOpposite.opEquiv : {α : Type u_1} → α ≃ αᵃᵒᵖ
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Nat.Prime.log_ne_zero : ∀ {p : ℕ}, Nat.Prime p → Real.log ↑p ≠ 0
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddActionForall.eq_1 : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α],
  DomAddAct.instAddActionForall = { toVAdd := DomAddAct.instVAddForall, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The unoriented angle between two nonzero vectors is the absolute value of the oriented angle,
converted to a real.  -/
Orientation.angle_eq_abs_oangle_toReal : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, x ≠ 0 → y ≠ 0 → InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableOn_of_locally_mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M},
  (∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ MDiff[s ∩ u] f) → MDiff[s] f
-- Batteries.Recycling.RBTree.Alter
RBTree.RBMap.alter.adapt.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (k : α) (f : Option β → Option β),
  RBTree.RBMap.alter.adapt k f none =
    match f none with
    | none => none
    | some v => some (k, v)
-- Mathlib.LinearAlgebra.FreeModule.PID
Submodule.smithNormalFormTopBasis.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsDomain R] [inst_4 : IsPrincipalIdealRing R] {N N_1 : Submodule R M} (e_N : N = N_1) [inst_5 : Finite ι]
  (b b_1 : Module.Basis ι R M),
  b = b_1 →
    ∀ (h : Module.finrank R ↥N = Module.finrank R M),
      Submodule.smithNormalFormTopBasis b h = Submodule.smithNormalFormTopBasis b_1 ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.Epi S.cokernelToAbelianCoimage
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_singleton : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))),
  X.zeroLocus {f} = (↑(X.basicOpen f))ᶜ
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.instInhabitedFixedParamPerms.default : Lean.Elab.FixedParamPerms
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.comp_id_lift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ],
  p.IsHomLift f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) φ)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_cond_pos : ∀ {ι : Type u_3} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M]
  {f : ι → M} {p : ι → Prop},
  (∀ (i : ι), p i → 0 ≤ f i) →
    (∃ i, p i ∧ 0 < f i) → (Function.support f ∩ {i | p i}).Finite → 0 < ∑ᶠ (i : ι) (_ : p i), f i
-- Mathlib.NumberTheory.LSeries.SumCoeff
_private.Mathlib.NumberTheory.LSeries.SumCoeff.0.lemma₂ : ∀ {s T ε : ℝ} {S : ℝ → ℂ},
  1 < s →
    MeasureTheory.LocallyIntegrableOn (fun t => S t) (Set.Ici 1) MeasureTheory.volume →
      (∀ t ≥ T, ‖S t‖ ≤ ε * t) →
        MeasureTheory.IntegrableOn (fun t => ‖S t‖ * t ^ (-s - 1)) (Set.Ici 1) MeasureTheory.volume
-- Mathlib.Control.Applicative
Functor.Const.map.eq_1 : ∀ {γ : Type u_1} {α : Type u_2} {β : Type u_3} (_f : α → β) (x : Functor.Const γ β), Functor.Const.map _f x = x
-- Mathlib.CategoryTheory.Action.Basic
Action.preservesLimits_forget : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G]
  [CategoryTheory.Limits.HasLimits V], CategoryTheory.Limits.PreservesLimits (Action.forget V G)
-- Init.System.IO
/-- The name of the entry.  -/
IO.FS.DirEntry.fileName : IO.FS.DirEntry → String
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.range_φ : ∀ (R : Type u) [inst : CommSemiring R] {S : Type v} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (s : Finset S),
  (PolynomialLaw.φ R s).range = Algebra.adjoin R ↑s
-- Mathlib.Order.Monotone.Defs
AntitoneOn.reflect_lt : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → f a < f b → b < a
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α}, m₁.WF → m₂.WF → (m₁ ∪ m₂).WF
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
Lean.Meta.Grind.Arith.Linear.getTermStructId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Composition with a function on the right is a continuous linear map on Schwartz space
provided that the function is temperate and growths polynomially near infinity.  -/
SchwartzMap.compCLM : (𝕜 : Type u_2) →
  {D : Type u_4} →
    {E : Type u_5} →
      {F : Type u_6} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                [inst_4 : RCLike 𝕜] →
                  [inst_5 : NormedAddCommGroup D] →
                    [inst_6 : NormedSpace ℝ D] →
                      [inst_7 : NormedSpace 𝕜 F] →
                        {g : D → E} →
                          Function.HasTemperateGrowth g →
                            (∃ k C, ∀ (x : D), ‖x‖ ≤ C * (1 + ‖g x‖) ^ k) → SchwartzMap E F →L[𝕜] SchwartzMap D F
-- Init.Data.Array.Lemmas
Array.getElem_replace_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {i : ℕ} {h : i < xs.size},
  xs[i] ≠ a → (xs.replace a b)[i] = xs[i]
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
AddCommGrpCat.toCommGrp_map : ∀ {x x_1 : AddCommGrpCat} (f : x ⟶ x_1),
  AddCommGrpCat.toCommGrp.map f = CommGrpCat.ofHom (AddMonoidHom.toMultiplicative (AddCommGrpCat.Hom.hom f))
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of a pointwise product of tuples is bounded by the sum
of their logarithmic heights.  -/
Height.logHeight_mul_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x y : ι → K),
  Height.logHeight (x * y) ≤ Height.logHeight x + Height.logHeight y
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.cutMap_add : ∀ {α : Type u_2} (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : LinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a b : α),
  LinearOrderedField.cutMap β (a + b) = LinearOrderedField.cutMap β a + LinearOrderedField.cutMap β b
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.symm_P : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.PathObject A), P.symm.P = P.P
-- Mathlib.Algebra.Divisibility.Basic
exists_eq_mul_right_of_dvd : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∃ c, b = a * c
-- Mathlib.Algebra.Order.Module.Defs
smul_nonpos_iff_neg_imp_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] {a : α} {b : β}, a • b ≤ 0 ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_pow : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : NonAssocSemiring S]
  [inst_2 : Module R S] [inst_3 : Pow S ℕ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S] (n : ℕ),
  (p ^ n).smeval x = p.smeval x ^ n
-- LeanSearchClient.Syntax
LeanSearchClient.instReprSearchResult.repr : LeanSearchClient.SearchResult → ℕ → Std.Format
-- Mathlib.GroupTheory.OrderOfElement
/-- A group element has finite order iff its order is positive.  -/
orderOf_pos_iff : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, 0 < orderOf x ↔ IsOfFinOrder x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {f : α → β → Bool} {k k' : α},
  t.getKey? k = some k' → (Std.TreeMap.filter f t)[k]! = (Option.filter (f k') t[k]?).get!
-- Mathlib.Topology.Separation.CompletelyRegular
instT35SpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [htX : T35Space X]
  [htY : T35Space Y], T35Space (X × Y)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonApplyWorkspaceEditParams.fromJson : Lean.Json → Except String Lean.Lsp.ApplyWorkspaceEditParams
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
/-- Evaluates the `Field` expression `e` with type `type` using the given exponential threshold,
and returns `some (v, h)` s.t. `h : e = ofRat v` if successful.
 -/
Lean.Meta.Grind.Arith.evalFieldExpr? : Lean.Expr → Lean.Expr → Lean.MetaM (Option (ℚ × Lean.Expr))
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.flippingIso_inv_toFunctor_obj_obj_map : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (k : C) {X Y : D} (f : X ⟶ Y),
  ((CategoryTheory.flippingIso.inv.toFunctor.obj F).obj k).map f = (F.map f).app k
-- Mathlib.Data.EReal.Operations
EReal.add_pos_of_pos_of_nonneg : ∀ {a b : EReal}, 0 < a → 0 ≤ b → 0 < a + b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.instAdd : {F : Type u} → [inst : Field F] → {W : WeierstrassCurve.Jacobian F} → Add W.Point
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `f : X ⟶ Spec A` is a morphism of schemes, then `f` factors via
the inclusion of `Spec (specTargetImage f)` into `X`.  -/
AlgebraicGeometry.specTargetImageFactorization : {X : AlgebraicGeometry.Scheme} →
  {A : CommRingCat} →
    (f : X ⟶ AlgebraicGeometry.Spec A) → X ⟶ AlgebraicGeometry.Spec (AlgebraicGeometry.specTargetImage f)
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- A morphism respecting addition, multiplication, and scalar multiplication
(denoted as `A →ₛₙₐ[φ] B`, or `A →ₙₐ[R] B` when `φ` is the identity on `R`).
When these arise from algebra structures, this is the same
as a not-necessarily-unital morphism of algebras.  -/
«term_→ₛₙₐ[_]_» : Lean.TrailingParserDescr
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.below.all : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsPrenex → Prop} {n : ℕ}
  {φ : L.BoundedFormula α (n + 1)} (h : φ.IsPrenex),
  FirstOrder.Language.BoundedFormula.IsPrenex.below h → motive φ h → FirstOrder.Language.BoundedFormula.IsPrenex.below ⋯
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_aux.eq_def : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2) (x : ℕ),
  newton_seq_aux✝ hnorm x =
    match x with
    | 0 => ⟨a, ⋯⟩
    | k.succ => ih_n✝ hnorm ⋯
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  f ≠ 0 → m.leadingCoeff g ∈ nonZeroDivisors R → m.degree (f * g) = m.degree f + m.degree g
-- Mathlib.Algebra.Homology.Embedding.IsSupported
/-- If `K : HomologicalComplex C c'`, then `K.IsSupportedOutside e` holds for
an embedding `e : c.Embedding c'` of complex shapes if `K` is exact at `e.f i` for all `i`.  -/
HomologicalComplex.IsSupportedOutside : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → HomologicalComplex C c' → c.Embedding c' → Prop
-- Mathlib.Data.Rat.Lemmas
Rat.inv_intCast_num_of_pos : ∀ {a : ℤ}, 0 < a → (↑a)⁻¹.num = 1
-- Init.Data.FloatArray.Basic
/-- Converts a list of floats into a `FloatArray`.
 -/
List.toFloatArray : List Float → FloatArray
-- Lean.Elab.Tactic.Omega.Frontend
Lean.Elab.Tactic.Omega.bitvec_to_nat : Lean.Meta.SimpExtension
-- Mathlib.NumberTheory.ModularForms.LFunction
/-- Shared conversion from the completed `Λ`-series to the ordinary `L`-series.  -/
_private.Mathlib.NumberTheory.ModularForms.LFunction.0.ModularForm.hasSum_L_of_hasSum_Λ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [inst_2 : ModularFormClass F Γ k],
  0 < s.re →
    HasSum
        (fun n =>
          ↑Real.pi ^ (-s) * Complex.Gamma s * (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) /
            ↑(2 * ↑n / Γ.strictWidthInfty) ^ s)
        (ModularForm.Λ hk f s) →
      HasSum (fun i => (PowerSeries.coeff i) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) / ↑i ^ s)
        (↑Γ.strictWidthInfty ^ (-s) * ModularForm.L hk f s)
-- Lean.Parser.Term
/-- Logs a warning, tagging the message as a named diagnostic with the specified name and validating
that an associated error explanation exists. The message may be passed as an interpolated string or
a `MessageData` term. The result of `getRef` is used as position information.
 -/
Lean.Parser.Term.logNamedWarningMacro : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.left] [inst_3 : CategoryTheory.Limits.HasCoproduct I.right] (b : J.R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.right b)
      (CategoryTheory.Limits.Multicoequalizer.sigmaπ I) =
    CategoryTheory.Limits.Multicoequalizer.π I b
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.ofList_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {l : List ((a : α) × β a)},
  (Std.DTreeMap.Raw.ofList l cmp).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) ∅ l)
-- Mathlib.CategoryTheory.Sites.Plus
/-- A helper definition used to define the morphisms for `plus`.  -/
CategoryTheory.GrothendieckTopology.diagramPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            (P : CategoryTheory.Functor Cᵒᵖ D) →
              {X Y : C} → (f : X ⟶ Y) → J.diagram P Y ⟶ (J.pullback f).op.comp (J.diagram P X)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Hom.of.injEq : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (as as_1 : CategoryTheory.Oplax.LaxTrans.Modification η θ),
  ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.Data.List.Chain
List.isChain_singleton : ∀ {α : Type u_1} {R : α → α → Prop} (a : α), List.IsChain R [a]
-- Init.Data.Iterators.Consumers.Total
/-- The wrapped iterator, which was wrapped by `Iter.ensureTermination`.
   -/
Std.Iter.Total.it : {α β : Type w} → Std.Iter.Total β → Std.Iter β
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (y, xy)` sends the measure `μ × ν` to `ν × μ`.  -/
MeasureTheory.measurePreserving_prod_mul_swap_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [μ.IsMulRightInvariant],
  MeasureTheory.MeasurePreserving (fun z => (z.2, z.1 * z.2)) (μ.prod ν) (ν.prod μ)
-- Mathlib.Data.ENNReal.Inv
ENNReal.mulLeftOrderIso_apply : ∀ (a : ENNReal) (ha : IsUnit a) (x : ENNReal), (a.mulLeftOrderIso ha) x = a * x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- The connecting homomorphism `Hⁱ(G, X₃) ⟶ Hʲ(G, X₁)` associated to an exact sequence
`0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0` of representations.  -/
groupCohomology.δ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)} →
        X.ShortExact → (i j : ℕ) → i + 1 = j → (groupCohomology X.X₃ i ⟶ groupCohomology X.X₁ j)
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.addRightCancelSemigroup : {α : Type u} → [RightCancelSemigroup α] → AddRightCancelSemigroup (Additive α)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_right_differentiableWithinAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : F → G} {s : Set F} {x : E},
  DifferentiableWithinAt 𝕜 (f ∘ ⇑iso) (⇑iso ⁻¹' s) x ↔ DifferentiableWithinAt 𝕜 f s (iso x)
-- Init.Data.Vector.Lemmas
Vector.replace_replicate_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b c : α},
  (!b == a) = true → (Vector.replicate n a).replace b c = Vector.replicate n a
-- Mathlib.GroupTheory.OrderOfElement
AddSubgroup.zmultiples_eq_zmultiples_iff : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G},
  ¬IsOfFinAddOrder x → (AddSubgroup.zmultiples x = AddSubgroup.zmultiples y ↔ x = y ∨ -x = y)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M), MonoidAlgebra.single m 0 = 0
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.mk : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              (obj : (j : J) → CategoryTheory.Limits.Cone (F.obj j)) →
                (map :
                    {j j' : J} →
                      (f : j ⟶ j') → (CategoryTheory.Limits.Cone.postcompose (F.map f)).obj (obj j) ⟶ obj j') →
                  autoParam
                      (∀ (j : J),
                        (map (CategoryTheory.CategoryStruct.id j)).hom =
                          CategoryTheory.CategoryStruct.id
                            ((CategoryTheory.Limits.Cone.postcompose (F.map (CategoryTheory.CategoryStruct.id j))).obj
                                (obj j)).pt)
                      CategoryTheory.Limits.DiagramOfCones.id._autoParam →
                    autoParam
                        (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
                          (map (CategoryTheory.CategoryStruct.comp f g)).hom =
                            CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom)
                        CategoryTheory.Limits.DiagramOfCones.comp._autoParam →
                      CategoryTheory.Limits.DiagramOfCones F
-- Mathlib.Data.List.Chain
List.isChain_cons_of_isChain_cons_map : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {a : α} {S : β → β → Prop} (f : α → β),
  (∀ (a b : α), S (f a) (f b) → R a b) → ∀ {l : List α}, List.IsChain S (f a :: List.map f l) → List.IsChain R (a :: l)
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The unique monoid homomorphism `FreeMonoid α →* FreeMonoid β` that sends
each `of x` to `of (f x)`.  -/
FreeMonoid.map : {α : Type u_1} → {β : Type u_2} → (α → β) → FreeMonoid α →* FreeMonoid β
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned : Std.Tactic.BVDecide.LRAT.Internal.Assignment