mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderivFun_add : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {i : σ} (f g : MvPowerSeries σ R),
  MvPowerSeries.pderivFun i (f + g) = MvPowerSeries.pderivFun i f + MvPowerSeries.pderivFun i g
-- Mathlib.Algebra.GroupWithZero.Shrink
instMulZeroClassShrink : {α : Type u_2} → [inst : Small.{v, u_2} α] → [MulZeroClass α] → MulZeroClass (Shrink.{v, u_2} α)
-- Mathlib.Data.Finset.Sups
Finset.singleton_diffs : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {t : Finset α} {a : α},
  {a}.diffs t = Finset.image (fun x => a \ x) t
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.oplaxFunctorOfIsLocallyDiscrete_mapComp : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory B]
  [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] [inst_2 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ⟶ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ⟶ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.comp g h))
              (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h))) =
          CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g) (map h))
              (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom))
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀) (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁))
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁))
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.oplaxFunctorOfIsLocallyDiscrete._auto_5)
  {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.oplaxFunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).mapComp
      f g =
    mapComp f g
-- Lean.Meta.Tactic.Grind.EqResolution
_private.Lean.Meta.Tactic.Grind.EqResolution.0.Lean.Meta.Grind.eqResCore : Lean.Expr → Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.instQuiver : {C D : CategoryTheory.Cat} → Quiver (C ⟶ D)
-- Init.GrindInstances.ToInt
Lean.Grind.instAddNatCiOfNatInt : Lean.Grind.ToInt.Add ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.Topology.GDelta.Basic
IsGδ.univ : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsGδ Set.univ
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
/-- If the sequence `fun i ↦ (c i).toReal * ‖f (x i)‖` is summable, then
`∫ x, f x, ∂Measure.sum (fun i ↦ (c i) • .dirac (x i)) = ∑' i, (c i).toReal • f (x i)`.  -/
MeasureTheory.integral_sum_dirac_eq_tsum : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_3} [Countable ι] {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  {f : X → E} [inst_1 : NormedSpace ℝ E] [MeasurableSingletonClass X] {x : ι → X} {c : ι → ENNReal} [CompleteSpace E],
  (∀ (i : ι), c i ≠ ⊤) →
    (Summable fun i => (c i).toReal * ‖f (x i)‖) →
      (∫ (x : X), f x ∂MeasureTheory.Measure.sum fun i => c i • MeasureTheory.Measure.dirac (x i)) =
        ∑' (i : ι), (c i).toReal • f (x i)
-- Mathlib.Order.Sublattice
Sublattice.prod_mono_right : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {M₁ M₂ : Sublattice β},
  M₁ ≤ M₂ → L.prod M₁ ≤ L.prod M₂
-- Mathlib.Analysis.Real.Cardinality
/-- The body of the sum in `cantorFunction`.
`cantorFunctionAux c f n = c ^ n` if `f n = true`;
`cantorFunctionAux c f n = 0` if `f n = false`.  -/
Cardinal.cantorFunctionAux : ℝ → (ℕ → Bool) → ℕ → ℝ
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- The function `x : ℝ ↦ x * log x + 1 - x`.
The Kullback-Leibler divergence is an f-divergence for this function.  -/
InformationTheory.klFun : ℝ → ℝ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List (α × β)} {k : α}, k ∈ t.insertMany l ↔ k ∈ t ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.Order.Filter.AtTopBot.Disjoint
Filter.disjoint_atBot_principal_Ici : ∀ {α : Type u_3} [inst : Preorder α] [NoBotOrder α] (x : α), Disjoint Filter.atBot (Filter.principal (Set.Ici x))
-- Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
Complex.hasStrictFDerivAt_log_real : ∀ {x : ℂ}, x ∈ Complex.slitPlane → HasStrictFDerivAt Complex.log (x⁻¹ • 1) x
-- Mathlib.Order.PartialSups
/-- The monotone sequence whose value at `i` is the supremum of the `f j` where `j ≤ i`.  -/
partialSups : {α : Type u_1} →
  {ι : Type u_3} → [inst : SemilatticeSup α] → [inst_1 : Preorder ι] → [LocallyFiniteOrderBot ι] → (ι → α) → ι →o α
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J},
  F.IsEventuallyConstantTo i₀ → ∀ [CategoryTheory.IsCofiltered J], CategoryTheory.Limits.HasLimit F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKeyD_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare k ((Std.DTreeMap.Internal.Impl.insert! k v t).maxKeyD fallback)).isLE = true
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.Hom.mk.injEq : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ⟶ Y.obj)
  (comm :
    autoParam
      (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) =
        CategoryTheory.CategoryStruct.comp f Y.d)
      CategoryTheory.DifferentialObject.Hom.comm._autoParam)
  (f_1 : X.obj ⟶ Y.obj)
  (comm_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f_1) =
        CategoryTheory.CategoryStruct.comp f_1 Y.d)
      CategoryTheory.DifferentialObject.Hom.comm._autoParam),
  ({ f := f, comm := comm } = { f := f_1, comm := comm_1 }) = (f = f_1)
-- Mathlib.Algebra.Group.Torsion
IsAddTorsionFree.zsmul_eq_zero_iff_right : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a : G}, n ≠ 0 → (n • a = 0 ↔ a = 0)
-- Mathlib.Topology.FiberBundle.Basic
/-- The base space of a fiber bundle core, as a convenience function for dot notation  -/
FiberBundleCore.Base : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} → [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → FiberBundleCore ι B F → Type u_2
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHSubOffset_5 : HSub Std.Time.WallTime Std.Time.Millisecond.Offset Std.Time.WallTime
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.map_hom_inv_id_eval_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {X Y : CategoryTheory.GradedObject J C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  (j : J) (Y_1 : D),
  CategoryTheory.CategoryStruct.comp ((F.map (e.hom j)).app Y_1) ((F.map (e.inv j)).app Y_1) =
    CategoryTheory.CategoryStruct.id ((F.obj (X j)).obj Y_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).getKey k ⋯ = k
-- Mathlib.Data.List.Induction
_private.Mathlib.Data.List.Induction.0.List.reverseRec.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (l : List α) → motive (a :: l)) → motive x
-- Mathlib.RingTheory.Unramified.Locus
/-- We say that an `R`-algebra `A` is unramified at a prime `q` of `A`
if `A_q` is formally unramified over `R`.

If `A` is of finite type over `R` and `q` is lying over `p`, then this is equivalent to
`κ(q)/κ(p)` being separable and `pA_q = qA_q`.
See `Algebra.isUnramifiedAt_iff_map_eq` in `RingTheory.Unramified.LocalRing`  -/
Algebra.IsUnramifiedAt : (R : Type u_1) →
  {A : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → (q : Ideal A) → [q.IsPrime] → Prop
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_same₂₃ : ∀ {R : Type u_1} [inst : CommRing R] (W : ℤ → R) (a b c : ℤ),
  IsEllipticNet.atomRel W a b b c = W b * W 0 * IsEllipticNet.atom W a c
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = true → ∀ {fallback : α}, t.maxKeyD fallback = fallback
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.of_zero : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : SMul R V] [inst_2 : Zero V],
  (HahnModule.of R) 0 = 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- This is the *continuous functional calculus* of an element `a : A` in a non-unital algebra
applied to bare functions.  When either `a` does not satisfy the predicate `p` (i.e., `a` is not
`IsStarNormal`, `IsSelfAdjoint`, or `0 ≤ a` when `R` is `ℂ`, `ℝ`, or `ℝ≥0`, respectively), or when
`f : R → R` is not continuous on the quasispectrum of `a` or `f 0 ≠ 0`, then `cfcₙ f a` returns the
junk value `0`.

This is the primary declaration intended for widespread use of the continuous functional calculus
for non-unital algebras, and all the API applies to this declaration. For more information, see the
module documentation for `Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital`.  -/
cfcₙ : {R : Type u_3} →
  {A : Type u_4} →
    {p : A → Prop} →
      [inst : CommSemiring R] →
        [inst_1 : Nontrivial R] →
          [inst_2 : StarRing R] →
            [inst_3 : MetricSpace R] →
              [inst_4 : IsTopologicalSemiring R] →
                [inst_5 : ContinuousStar R] →
                  [inst_6 : NonUnitalRing A] →
                    [inst_7 : StarRing A] →
                      [inst_8 : TopologicalSpace A] →
                        [inst_9 : Module R A] →
                          [inst_10 : IsScalarTower R A A] →
                            [inst_11 : SMulCommClass R A A] →
                              [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] → (R → R) → A → A
-- Mathlib.Algebra.Homology.SpectralObject.Homology
CategoryTheory.Abelian.SpectralObject.dKernelSequence_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₂₃ : i₁ ⟶ i₃)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.dKernelSequence._auto_5),
  (X.dKernelSequence f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃).f =
    X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.unique' : {R : Type u_1} →
  {M : Type u_3} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Subsingleton R] → Unique (Submodule R M)
-- Mathlib.Analysis.Complex.TaylorSeries
/-- **Alias** of `Complex.taylorSeries_eq_on_eball'`.

---

A function that is complex differentiable on the open ball of radius `r ≤ ∞` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.taylorSeries_eq_on_emetric_ball' : ∀ ⦃c : ℂ⦄ ⦃r : ENNReal⦄ ⦃z : ℂ⦄,
  z ∈ Metric.eball c r →
    ∀ {f : ℂ → ℂ},
      DifferentiableOn ℂ f (Metric.eball c r) → ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
-- Mathlib.Order.JordanHolder
CompositionSeries.eq_of_head_eq_head_of_last_eq_last_of_length_eq_zero : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
  RelSeries.head s₁ = RelSeries.head s₂ → RelSeries.last s₁ = RelSeries.last s₂ → s₁.length = 0 → s₁ = s₂
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instRing : {R : Type u_1} → [inst : Ring R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → Ring (OreLocalization S R)
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo.isBinder : Lean.Elab.TermInfo → Bool
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM_const : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (c : ℂ),
  (TemperedDistribution.fourierMultiplierCLM F fun x => c) = c • ContinuousLinearMap.id ℂ (TemperedDistribution E F)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv
-- Mathlib.Data.Finset.Dedup
Finset.nodup_toList : ∀ {α : Type u_1} (s : Finset α), s.toList.Nodup
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.univ : ∀ {M : Type u_1} [inst : AddCommMonoid M] [AddMonoid.FG M], IsLinearSet Set.univ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_zero : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.AddMonObj X],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.AddMonObj.zero)
      CategoryTheory.AddMonObj.add =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Mathlib.RingTheory.DedekindDomain.Factorization
FractionalIdeal.divMod.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (c b a : FractionalIdeal (nonZeroDivisors R) K),
  c.divMod b a = if h : a ≤ c ∧ a ≠ 0 ∧ b ≠ 0 then ⋯.choose else 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_eq_fallback : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  {fallback : β a}, Std.Internal.List.containsKey a l = false → Std.Internal.List.getValueCastD a l fallback = fallback
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_mul_right_add : ∀ {α : Type u} [inst : CommRing α] (x y z : α), Ideal.span {z * y + x, y} = Ideal.span {x, y}
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- If `f` has finite integral, then `∫ x in s, f x ∂μ` is absolutely continuous in `s`: it tends
to zero as `μ s` tends to zero.  -/
MeasureTheory.HasFiniteIntegral.tendsto_setIntegral_nhds_zero : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_6} {f : α → G},
  MeasureTheory.HasFiniteIntegral f μ →
    ∀ {l : Filter ι} {s : ι → Set α},
      Filter.Tendsto (⇑μ ∘ s) l (nhds 0) → Filter.Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (nhds 0)
-- Mathlib.Algebra.Group.AddChar
AddChar.pow_eq_nsmul : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ : AddChar A M) (n : ℕ), ψ ^ n = n • ψ
-- Std.Time.Format
/-- Parses a `String` in the lean date time format with timezone format and returns a `DateTime` object.
 -/
Std.Time.DateTime.fromLeanDateTimeWithZoneString : String → Except String Std.Time.DateTime
-- Mathlib.Order.RelIso.Set
subrel_val : ∀ {α : Type u_1} (r : α → α → Prop) (p : α → Prop) {a b : Subtype p}, Subrel r p a b ↔ r ↑a ↑b
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.uncurry`:

Linearly constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P`
with the property that its composition with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is
the given bilinear map `M →[A] N →[R] P`.  -/
TensorProduct.AlgebraTensorModule.uncurry : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      (M : Type uM) →
        (N : Type uN) →
          (P : Type uP) →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Semiring B] →
                  [inst_3 : Algebra R A] →
                    [inst_4 : Algebra R B] →
                      [inst_5 : AddCommMonoid M] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module A M] →
                            [inst_8 : IsScalarTower R A M] →
                              [inst_9 : AddCommMonoid N] →
                                [inst_10 : Module R N] →
                                  [inst_11 : AddCommMonoid P] →
                                    [inst_12 : Module R P] →
                                      [inst_13 : Module A P] →
                                        [inst_14 : IsScalarTower R A P] →
                                          [inst_15 : Module B P] →
                                            [inst_16 : IsScalarTower R B P] →
                                              [inst_17 : SMulCommClass A B P] →
                                                (M →ₗ[A] N →ₗ[R] P) →ₗ[B] TensorProduct R M N →ₗ[A] P
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
/-- The decomposition of a tensor product induced by a decomposition of the left module.  -/
DirectSum.tensorDecomposition : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            (ℳ : ι → Submodule R M) →
              [inst_3 : DecidableEq ι] →
                [DirectSum.Decomposition ℳ] →
                  (N : Type u_6) →
                    [inst_5 : AddCommGroup N] →
                      [inst_6 : Module R N] → DirectSum.Decomposition (DirectSum.decomposeTensor ℳ N)
-- Init.Data.Nat.Lemmas
/-- See `exists_lt_succ_left'` for a variant where `p` takes the bound as an argument.  -/
Nat.exists_lt_succ_left : ∀ {n : ℕ} {p : ℕ → Prop}, (∃ m < n + 1, p m) ↔ p 0 ∨ ∃ m < n, p (m + 1)
-- Mathlib.LinearAlgebra.TensorProduct.Associator
Algebra.algHom.congr_simp : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
  Algebra.algHom R S A = Algebra.algHom R S A
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Coercion to function `fun h : M ≃ₘ^n⟮I, I'⟯ M' ↦ (h : M → M')` is injective.  -/
Diffeomorph.coeFn_injective : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {H' : Type u_6} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_10} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞},
  Function.Injective DFunLike.coe
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, (t₁ ∪ t₂).getKey! k = t₂.getKeyD k (t₁.getKey! k)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.hasLimit_of_hasLimitπ : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₁)]
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₂)]
  [CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.ShortComplex.π₃)], CategoryTheory.Limits.HasLimit F
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.apply.sizeOf_spec : ∀ (term : Aesop.RuleTerm) (md : Lean.Meta.TransparencyMode),
  sizeOf (Aesop.RuleTacDescr.apply term md) = 1 + sizeOf term + sizeOf md
-- Lean.Elab.App
/-- Adds the `TermInfo` for the field of a projection. See `Lean.Parser.Term.identProjKind`.  -/
_private.Lean.Elab.App.0.Lean.Elab.Term.addProjTermInfo : Lean.Syntax →
  Lean.Expr →
    optParam (Option Lean.Expr) none →
      optParam (Option Lean.LocalContext) none →
        optParam Lean.Name Lean.Name.anonymous →
          optParam Bool false → optParam Bool false → optParam Bool false → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.ι_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.ι f g)
      CategoryTheory.Limits.biprod.fst =
    CategoryTheory.Limits.kernel.ι (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Topology.LocalAtTarget
IsProperMap.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsProperMap f → ∀ (s : Set β), IsProperMap (s.restrictPreimage f)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.comp_aemeasurable' : ∀ {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β},
  AEMeasurable g (MeasureTheory.Measure.map f μ) → AEMeasurable f μ → AEMeasurable (fun x => g (f x)) μ
-- Mathlib.Control.LawfulFix
Pi.ωScottContinuous_curry : ∀ (α : Type u_1) (β : α → Type u_2) (γ : (a : α) → β a → Type u_3)
  [inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)],
  OmegaCompletePartialOrder.ωScottContinuous ⇑(Pi.monotoneCurry α β γ)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.continuous_integral_boundedContinuousFunction : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (f : BoundedContinuousFunction X ℝ), Continuous fun μ => ∫ (x : X), f x ∂↑μ