mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.isProbabilityMeasure_binomial : ∀ {n : ℕ} {p : ↑unitInterval}, MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.binomial n p)
-- Lean.LibrarySuggestions.SymbolFrequency
/-- The state is just an array of array of maps.
We don't assemble these on import for efficiency reasons: most modules will not query this extension.

Instead, we use an `IO.Ref` below so that within each module we can assemble the global `NameMap Nat` once.

Since we never modify the extension state except on export, the `IO.Ref` does not need updating after first access.
 -/
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.LibrarySuggestions.symbolFrequencyExt : Lean.PersistentEnvExtension (Lean.NameMap ℕ) Empty (Array (Array (Lean.NameMap ℕ)))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.ext_ring : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁}, f 1 = g 1 → f = g
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
/-- Recursion formula for the coefficients of the hypergeometric series.

This is mainly used to calculate the convergence radius.  -/
Complex.regularizedHGFunCoeff_add_one : ∀ {a b : Multiset ℂ} {n : ℕ},
  (∀ k ∈ b, k ≠ -↑n) →
    Complex.regularizedHGFunCoeff a b (n + 1) =
      Complex.regularizedHGFunCoeff a b n *
        ((Multiset.map (fun x => x + ↑n) a).prod / ((Multiset.map (fun x => x + ↑n) b).prod * (↑n + 1)))
-- Mathlib.Topology.UniformSpace.Cauchy
Cauchy.map_of_le : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] {f : Filter α} {m : α → β},
  Cauchy f → ∀ {s : Set α}, UniformContinuousOn m s → f ≤ Filter.principal s → Cauchy (Filter.map m f)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.sections.match_1.splitter : {α : Type u_1} →
  (motive : List (List α) → Sort u_2) →
    (x : List (List α)) → (Unit → motive []) → ((l : List α) → (L : List (List α)) → motive (l :: L)) → motive x
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.torsion.eq_1 : ∀ (K : Type u_1) [inst : Field K], NumberField.Units.torsion K = CommGroup.torsion (NumberField.RingOfIntegers K)ˣ
-- Mathlib.Algebra.Order.Ring.Basic
sq_pos_of_neg : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] {a : R}, a < 0 → 0 < a ^ 2
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_counitIso_hom_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) (X : CategoryTheory.ComposableArrows Cᵒᵖ n)
  (X_1 : Fin (n + 1)),
  ((CategoryTheory.ComposableArrows.opEquivalence C n).counitIso.hom.app X).app X_1 =
    X.map
      (((CategoryTheory.orderDualEquivalence (Fin (n + 1))).symm.trans Fin.revOrderIso.equivalence).symm.counitInv.app
          (Opposite.op X_1)).unop
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.eigenspace_def : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, f.eigenspace μ = (f - μ • 1).ker
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapWithPostcondition_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n γ} {g : γ → Std.Iterators.PostconditionT o δ}
  {it : Std.IterM m β},
  (Std.IterM.mapWithPostcondition g (Std.IterM.mapWithPostcondition f it)).toList =
    (Std.IterM.mapWithPostcondition (fun x => liftM (f x) >>= g) it).toList
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- Given a subgroup `Γ` of a topological group `G` with measure `ν`, and a measure 'μ' on the
quotient `G ⧸ Γ` satisfying `QuotientMeasureEqMeasurePreimage`, the restriction
of `ν` to a fundamental domain is measure-preserving with respect to `μ`.  -/
measurePreserving_quotientGroup_mk_of_QuotientMeasureEqMeasurePreimage : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] (ν : MeasureTheory.Measure G) {Γ : Subgroup G}
  {𝓕 : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) 𝓕 ν →
    ∀ (μ : MeasureTheory.Measure (G ⧸ Γ)) [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ],
      MeasureTheory.MeasurePreserving QuotientGroup.mk (ν.restrict 𝓕) μ
-- Init.Data.Array.Bootstrap
Array.append_empty : ∀ {α : Type u_1} {xs : Array α}, xs ++ #[] = xs
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.funLike.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E], AddGroupSeminorm.funLike = { coe := fun f => f.toFun, coe_injective := ⋯ }
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Obtain a measure by giving an outer measure where all sets in the σ-algebra are
Carathéodory measurable.  -/
MeasureTheory.OuterMeasure.toMeasure : {α : Type u_1} →
  [ms : MeasurableSpace α] → (m : MeasureTheory.OuterMeasure α) → ms ≤ m.caratheodory → MeasureTheory.Measure α
-- Mathlib.Tactic.Translate.Reorder
/-- Return the successor of `n` in a cycle, where `head` is the head of the cycle list.  -/
_private.Mathlib.Tactic.Translate.Reorder.0.Mathlib.Tactic.Translate.ArgReorder.reverse.getCycleSuccessor : ℕ → ℕ → List ℕ → Option ℕ
-- Init.Data.SInt.Bitwise
instCommutativeISizeHOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.contains a = false → m.getKey! a = default
-- Init.Data.List.Lemmas
List.eq_or_mem_of_mem_insert : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {b a : α} {l : List α}, a ∈ List.insert b l → a = b ∨ a ∈ l
-- Init.Omega.IntList
_private.Init.Omega.IntList.0.List.getElem?_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : α → β → γ} {i : ℕ},
  (List.zipWith f as bs)[i]? =
    match as[i]?, bs[i]? with
    | some a, some b => some (f a b)
    | x, x_1 => none
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.destruct_congr_iff : ∀ {α : Type u} {s t : Stream'.WSeq α},
  s ~ʷ t ↔ Computation.LiftRel (Stream'.WSeq.BisimO fun x1 x2 => x1 ~ʷ x2) s.destruct t.destruct
-- Mathlib.Algebra.Module.Submodule.IterateMapComap
LinearMap.iterateMapComap.eq_1 : ∀ {R : Type u_1} {N : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f i : N →ₗ[R] M) (n : ℕ),
  f.iterateMapComap i n = (fun K => Submodule.comap f (Submodule.map i K))^[n]
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.instRingEquivClass : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S],
  RingEquivClass (R ≃+* S) R S
-- Aesop.RuleTac.Basic
Aesop.RuleTacInput.mk.sizeOf_spec : ∀ (goal : Lean.MVarId) (mvars : Aesop.UnorderedArraySet Lean.MVarId)
  (indexMatchLocations : Array Aesop.IndexMatchLocation) (patternSubsts? : Option (Array Aesop.Substitution))
  (options : Aesop.Options'),
  sizeOf
      { goal := goal, mvars := mvars, indexMatchLocations := indexMatchLocations, patternSubsts? := patternSubsts?,
        options := options } =
    1 + sizeOf goal + sizeOf mvars + sizeOf indexMatchLocations + sizeOf patternSubsts? + sizeOf options
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Alt.mk : Lean.Syntax →
  ℕ →
    Lean.Expr →
      List Lean.LocalDecl → List Lean.Meta.Match.Pattern → List (Lean.Expr × Lean.Expr) → Array ℕ → Lean.Meta.Match.Alt
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.comap_equiv_eq_map_symm : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R ≃+* S) (K : Subring S),
  Subring.comap (↑f) K = Subring.map (↑f.symm) K
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- `C_c(α, β)` is the type of continuous functions `α → β` with compact support from a topological
space to a topological space with a zero element.

When possible, instead of parametrizing results over `f : C_c(α, β)`,
you should parametrize over `{F : Type*} [CompactlySupportedContinuousMapClass F α β] (f : F)`.

When you extend this structure, make sure to extend `CompactlySupportedContinuousMapClass`.  -/
CompactlySupported.«term_→C_c_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.eval_lsingle : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R) (i : ℕ)
  (m : M), (PolynomialModule.eval r) ((PolynomialModule.lsingle R i) m) = r ^ i • m
-- Mathlib.Data.Fin.Basic
/-- The `Fin.pos_iff_ne_zero` in `Lean` only applies in `Fin (n+1)`.
This one instead uses a `NeZero n` typeclass hypothesis.
 -/
Fin.pos_iff_ne_zero' : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), 0 < a ↔ a ≠ 0
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.sheafedSpaceMap_hom_c_app_hom_apply_coe : ∀ {A B σ τ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B]
  [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜]
  [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (U : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Proj.toSheafedSpace 𝒜).toPresheafedSpace)ᵒᵖ)
  (s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj (Opposite.op (Opposite.unop U))))
  (y :
    ↥(Opposite.unop
        (Opposite.op
          ((TopologicalSpace.Opens.map (TopCat.ofHom (AlgebraicGeometry.ProjectiveSpectrum.comap f hf))).obj
            (Opposite.unop U))))),
  ↑((CommRingCat.Hom.hom ((AlgebraicGeometry.Proj.sheafedSpaceMap f hf).hom.c.app U)) s) y =
    AlgebraicGeometry.Proj.comapStructureSheafFun f hf (Opposite.unop U)
      ((TopologicalSpace.Opens.map (TopCat.ofHom (AlgebraicGeometry.ProjectiveSpectrum.comap f hf))).obj
        (Opposite.unop U))
      ⋯ (↑s) y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.abs_sinc_le_one : ∀ (x : ℝ), |Real.sinc x| ≤ 1
-- Mathlib.Tactic.CategoryTheory.Slice
/-- `slice` is a conv tactic; if the current focus is a composition of several morphisms,
`slice a b` reassociates as needed, and zooms in on the `a`-th through `b`-th morphisms.
Thus if the current focus is `(a ≫ b) ≫ ((c ≫ d) ≫ e)`, then `slice 2 3` zooms to `b ≫ c`.
 -/
Mathlib.Tactic.Slice.slice : Lean.ParserDescr
-- Mathlib.RingTheory.Derivation.MapCoeffs
/-- `algHom_deriv` in a separable algebra
 -/
Differential.algHom_deriv' : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] {R : Type u_2} [inst_2 : CommRing R]
  [inst_3 : Differential R] [inst_4 : Algebra A R] [DifferentialAlgebra A R] {R' : Type u_3} [inst_6 : CommRing R']
  [inst_7 : Differential R'] [inst_8 : Algebra A R'] [DifferentialAlgebra A R'] [IsDomain R'] [Nontrivial R]
  [Algebra.IsSeparable A R] (f : R →ₐ[A] R'), Function.Injective ⇑f → ∀ (x : R), f x′ = (f x)′
-- Mathlib.Analysis.Normed.Module.FiniteDimension
summable_of_sum_range_norm_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {c : ℝ} {f : ℕ → E},
  (∀ (n : ℕ), ∑ i ∈ Finset.range n, ‖f i‖ ≤ c) → Summable f
-- Mathlib.Logic.Embedding.Basic
Subtype.impEmbedding_apply_coe : ∀ {α : Type u_1} (p q : α → Prop) (h : ∀ (x : α), p x → q x) (x : { x // p x }), ↑((Subtype.impEmbedding p q h) x) = ↑x
-- Mathlib.Data.Finset.Fold
Finset.fold_cons : ∀ {α : Type u_1} {β : Type u_2} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op] {f : α → β} {b : β}
  {s : Finset α} {a : α} (h : a ∉ s), Finset.fold op b f (Finset.cons a s h) = op (f a) (Finset.fold op b f s)
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2},
  Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma =
    {
      IsPlausibleStep := fun it x =>
        match x with
        | Std.IterStep.yield it' out =>
          it.internalState.l = Std.DHashMap.Internal.AssocList.cons out.fst out.snd it'.internalState.l
        | Std.IterStep.skip it => False
        | Std.IterStep.done => it.internalState.l = Std.DHashMap.Internal.AssocList.nil,
      step := fun it =>
        pure
          (match it with
          | { internalState := { l := Std.DHashMap.Internal.AssocList.nil } } =>
            Std.Shrink.deflate ⟨Std.IterStep.done, ⋯⟩
          | { internalState := { l := Std.DHashMap.Internal.AssocList.cons k v l } } =>
            Std.Shrink.deflate ⟨Std.IterStep.yield { internalState := { l := l } } ⟨k, v⟩, ⋯⟩) }
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Special case of `logCounting_add_analyticOn`: Subtracting a constant does not change the logarithmic
counting function for the poles.
 -/
ValueDistribution.logCounting_sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E},
  Meromorphic f → ValueDistribution.logCounting (f - fun x => a₀) ⊤ = ValueDistribution.logCounting f ⊤
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.end_mem_tail_support_of_ne : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, u ≠ v → ∀ (p : G.Walk u v), v ∈ p.support.tail
-- Mathlib.Algebra.Module.Presentation.Cokernel
/-- The obvious solution in `M₂ ⧸ LinearMap.range f` to the equations in
`pres₂.cokernelRelations data`.  -/
Module.Presentation.cokernelSolution : {A : Type u} →
  [inst : Ring A] →
    {M₁ : Type v₁} →
      {M₂ : Type v₂} →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module A M₁] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module A M₂] →
                (pres₂ : Module.Presentation A M₂) →
                  {f : M₁ →ₗ[A] M₂} →
                    {ι : Type w₁} →
                      {g₁ : ι → M₁} →
                        (data : pres₂.CokernelData f g₁) → (pres₂.cokernelRelations data).Solution (M₂ ⧸ f.range)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.instHasZeroObject : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D], CategoryTheory.Limits.HasZeroObject (CategoryTheory.Mon D)
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.PreservesPullbacksOfInclusions.preservesPullbackInl : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {D : Type u_2}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {F : CategoryTheory.Functor C D}
  {inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C} [self : CategoryTheory.PreservesPullbacksOfInclusions F]
  {X Y Z : C} (f : Z ⟶ X ⨿ Y),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan CategoryTheory.Limits.coprod.inl f) F
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_C_mul : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ : PowerSeries R) (a : R),
  (PowerSeries.coeff n) (PowerSeries.C a * φ) = a * (PowerSeries.coeff n) φ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_insertEntry_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)} {k : α}
  {v : β k}, Std.Internal.List.getKey! k (Std.Internal.List.insertEntry k v l) = k
-- Std.Do.SPred.Laws
Std.Do.SPred.apply_pure : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {φ : Prop}, ⌜φ⌝ s = ⌜φ⌝
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_exp_Iic : ∀ (c : ℝ), MeasureTheory.IntegrableOn Real.exp (Set.Iic c) MeasureTheory.volume
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- An edge labeling of the complete graph on `V` with labels in type `K`.
 -/
SimpleGraph.TopEdgeLabeling : Type u_5 → Type u_6 → Type (max u_5 u_6)
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.eq_def : ∀ (s : String) (p₀ : s.Pos) (res : Lean.Name) (acc : String) (ucount : ℕ),
  Lean.Name.demangleAux✝ s p₀ res acc ucount =
    if hp₀ : p₀ = s.endPos then res.str (acc.pushn '_' (ucount / 2))
    else
      let ch := p₀.get hp₀;
      let p := p₀.next hp₀;
      if ch = '_' then Lean.Name.demangleAux✝ s p res acc (ucount + 1)
      else
        if ucount % 2 = 0 then Lean.Name.demangleAux✝ s p res ((acc.pushn '_' (ucount / 2)).push ch) 0
        else
          if ch.isDigit = true then
            have res := res.str (acc.pushn '_' (ucount / 2));
            if h : ch = '0' ∧ ∃ (h : p ≠ s.endPos), p.get h = '0' then Lean.Name.demangleAux✝ s (p.next ⋯) res "" 0
            else Lean.Name.demangleAux.decodeNum✝ s p res (ch.val - 48).toNat
          else
            match ch, h₁ : Lean.parseLowerHex?✝ 2 s p 0 with
            | 'x', some (q, v) =>
              have acc := acc.pushn '_' (ucount / 2);
              have this := ⋯;
              Lean.Name.demangleAux✝ s q res (acc.push (Char.ofNat v)) 0
            | x, x_1 =>
              match ch, h₂ : Lean.parseLowerHex?✝ 4 s p 0 with
              | 'u', some (q, v) =>
                have acc := acc.pushn '_' (ucount / 2);
                have this := ⋯;
                Lean.Name.demangleAux✝ s q res (acc.push (Char.ofNat v)) 0
              | x, x_2 =>
                match ch, h₃ : Lean.parseLowerHex?✝ 8 s p 0 with
                | 'U', some (q, v) =>
                  have acc := acc.pushn '_' (ucount / 2);
                  have this := ⋯;
                  Lean.Name.demangleAux✝ s q res (acc.push (Char.ofNat v)) 0
                | x, x_3 => Lean.Name.demangleAux✝ s p (res.str acc) (("".pushn '_' (ucount / 2)).push ch) 0
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.hasSum_qExpansion_of_norm_lt : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f →
        UpperHalfPlane.IsBoundedAtImInfty f →
          ∀ {q : ℂ},
            ‖q‖ < 1 →
              HasSum (fun m => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion h f) • q ^ m)
                (UpperHalfPlane.cuspFunction h f q)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.calc_eval_z'_norm : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a z z' z1 : ℤ_[p]} {n : ℕ},
  ih_gen✝ n z →
    ∀ {q : ℤ_[p]},
      (Polynomial.aeval z') F = q * z1 ^ 2 →
        ∀ (h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1),
          z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩ →
            ‖(Polynomial.aeval z') F‖ ≤
              ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen✝ p F a ^ 2 ^ (n + 1)
-- Mathlib.SetTheory.ZFC.Basic
_private.Mathlib.SetTheory.ZFC.Basic.0.ZFSet.ext_aux : ∀ {x y : ZFSet.{u}}, (∀ (z : ZFSet.{u}), z ∈ x.toSet ↔ z ∈ y.toSet) → x = y
-- Mathlib.Analysis.Meromorphic.Order
/-- If the order of a meromorphic function is positive, then this function converges to zero
at this point. See also the iff version `tendsto_zero_iff_meromorphicOrderAt_pos`.  -/
tendsto_zero_of_meromorphicOrderAt_pos : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  0 < meromorphicOrderAt f x → Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds 0)
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The Lie algebra of a Lie group, i.e., its tangent space at the identity. We use the word
`GroupLieAlgebra` instead of `LieAlgebra` as the latter is taken as a generic class.  -/
GroupLieAlgebra : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              ModelWithCorners 𝕜 E H →
                (G : Type u_4) → [inst : TopologicalSpace G] → [ChartedSpace H G] → [Group G] → Type u_3
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : Mul α] [inst_1 : Add α] [inst_2 : Mul β] [inst_3 : Add β] [inst_4 : LE α]
  [inst_5 : LE β] (toRingEquiv : α ≃+* β)
  (map_le_map_iff' : ∀ {a b : α}, toRingEquiv.toFun a ≤ toRingEquiv.toFun b ↔ a ≤ b) (toRingEquiv_1 : α ≃+* β)
  (map_le_map_iff'_1 : ∀ {a b : α}, toRingEquiv_1.toFun a ≤ toRingEquiv_1.toFun b ↔ a ≤ b),
  ({ toRingEquiv := toRingEquiv, map_le_map_iff' := map_le_map_iff' } =
      { toRingEquiv := toRingEquiv_1, map_le_map_iff' := map_le_map_iff'_1 }) =
    (toRingEquiv = toRingEquiv_1)
-- Mathlib.Topology.Order.IsLocallyClosed
isLocallyClosed_Ioc : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} [inst_1 : LinearOrder X] [ClosedIicTopology X],
  IsLocallyClosed (Set.Ioc a b)
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instAddCommMonoid.eq_1 : ∀ {α : Type u} [inst : AddCommSemigroup α],
  WithZero.instAddCommMonoid = { toAddMonoid := WithZero.instAddMonoid, add_comm := ⋯ }
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The forgetful functor from the subcategory `P.CostructuredArrow Q F X`.  -/
CategoryTheory.MorphismProperty.CostructuredArrow.forget : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} D] →
        (P : CategoryTheory.MorphismProperty D) →
          (Q : CategoryTheory.MorphismProperty C) →
            [inst_2 : Q.IsMultiplicative] →
              (F : CategoryTheory.Functor C D) →
                (X : D) → CategoryTheory.Functor (P.CostructuredArrow Q F X) (CategoryTheory.CostructuredArrow F X)
-- Mathlib.Algebra.Group.Equiv.Basic
/-- A family indexed by a type with a unique element
is `AddEquiv` to the element at the single index.  -/
AddEquiv.piUnique : {ι : Type u_16} →
  (M : ι → Type u_17) → [inst : (j : ι) → Add (M j)] → [inst_1 : Unique ι] → ((j : ι) → M j) ≃+ M default
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- The function `CanonicalFactor R w` vanishes only at `w`.
 -/
Complex.canonicalFactor_eq_zero_iff : ∀ {R : ℝ} {w z : ℂ}, w ∈ Metric.ball 0 R → z ∈ Metric.ball 0 R → (Complex.canonicalFactor R w z = 0 ↔ z = w)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For every nonzero ideal `I` of `v`, `v^(val_v(I) + 1)` does not divide `∏_v v^(val_v(I))`.  -/
Ideal.finprod_not_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (I : Ideal R),
  I ≠ 0 →
    ¬v.asIdeal ^ ((Associates.mk v.asIdeal).count (Associates.mk I).factors + 1) ∣
        ∏ᶠ (v : IsDedekindDomain.HeightOneSpectrum R), v.maxPowDividing I
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.GuessLexRel.eq : Lean.Elab.WF.GuessLex.GuessLexRel
-- Mathlib.Data.Int.Cast.Lemmas
Commute.intCast_left : ∀ {α : Type u_3} [inst : NonAssocRing α] {a : α} {n : ℤ}, Commute (↑n) a
-- Init.Core
Std.Symm.mk : ∀ {α : Sort u} {r : α → α → Prop}, (∀ (a b : α), r a b → r b a) → Std.Symm r
-- Mathlib.Data.Real.Basic
Real.ofCauchy_sub : ∀ (a b : CauSeq.Completion.Cauchy abs), { cauchy := a - b } = { cauchy := a } - { cauchy := b }
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.shiftFunctorAdd'_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) (i j k : A) (h : i + j = k)
  (X : t.Category),
  (CategoryTheory.shiftFunctorAdd' t.Category i j k h).inv.app X =
    ↑(t.z i j)⁻¹ •
      CategoryTheory.CategoryStruct.comp ((t.shiftIso j).hom.app ((CategoryTheory.shiftFunctor t.Category i).obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((t.shiftIso i).hom.app X))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C i j k h).inv.app X)
            ((t.shiftIso k).inv.app X)))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instToStringLVal : ToString Lean.Elab.Term.LVal