mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.dropPrefix?.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (as : List α) (b : α) (bs : List α)
  (h_1 : (list : List α) → motive list []) (h_2 : (head : α) → (tail : List α) → motive [] (head :: tail))
  (h_3 : (a : α) → (as : List α) → (b : α) → (bs : List α) → motive (a :: as) (b :: bs)),
  (match a :: as, b :: bs with
    | list, [] => h_1 list
    | [], head :: tail => h_2 head tail
    | a :: as, b :: bs => h_3 a as b bs) =
    h_3 a as b bs
-- Mathlib.Topology.Connected.Basic
IsPreconnected.subset_or_subset : ∀ {α : Type u} [inst : TopologicalSpace α] {s u v : Set α},
  IsOpen u → IsOpen v → Disjoint u v → s ⊆ u ∪ v → IsPreconnected s → s ⊆ u ∨ s ⊆ v
-- Mathlib.Order.KrullDimension
Order.krullDim.eq_1 : ∀ (α : Type u_1) [inst : Preorder α], Order.krullDim α = ⨆ p, ↑p.length
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.mapAddHom_injective' : ∀ {α : Type u} {β : Type v} [inst : Add α] [inst_1 : Add β], Function.Injective WithZero.mapAddHom
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_lt_wf : ∀ {R : Type u} [inst : Semiring R], WellFounded fun p q => p.degree < q.degree
-- Mathlib.GroupTheory.GroupAction.ConjAct
/-- Reinterpret `g : ConjAct G` as an element of `G`.  -/
ConjAct.ofConjAct : {G : Type u_3} → [inst : DivInvMonoid G] → ConjAct G ≃* G
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.untop_orderTop_of_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} (hx : x ≠ 0),
  x.orderTop.untop ⋯ = ⋯.min ⋯
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instIsDomainCastInt : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d], IsDomain (ℤ√↑d)
-- Mathlib.Combinatorics.Additive.Corner.Defs
IsCornerFree.mono : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A B : Set (G × G)}, A ⊆ B → IsCornerFree B → IsCornerFree A
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.inductionOn : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {motive : Std.ExtDHashMap α β → Prop}
  (m : Std.ExtDHashMap α β), (∀ (a : Std.DHashMap α β), motive (Std.ExtDHashMap.mk a)) → motive m
-- Init.Data.Int.DivMod.Lemmas
Int.mul_sub_fdiv_right : ∀ (a c : ℤ) {b : ℤ}, b ≠ 0 → (a * b - c).fdiv b = a + (-c).fdiv b
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- An element `φ` of the orthogonal group of `F` can be factored as a product of reflections, and
specifically at most as many reflections as the dimension of the complement of the fixed subspace
of `φ`.  -/
LinearIsometryEquiv.reflections_generate_dim_aux : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] [FiniteDimensional ℝ F] {n : ℕ}
  (φ : F ≃ₗᵢ[ℝ] F),
  Module.finrank ℝ ↥(↑(ContinuousLinearMap.id ℝ F - ↑↑φ)).kerᗮ ≤ n →
    ∃ l, l.length ≤ n ∧ φ = (List.map (fun v => (ℝ ∙ v)ᗮ.reflection) l).prod
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.measure_closedBall_le_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f : ContDiffBump c) (μ : MeasureTheory.Measure E) [BorelSpace E]
  [FiniteDimensional ℝ E] [MeasureTheory.IsLocallyFiniteMeasure μ],
  μ.real (Metric.closedBall c f.rIn) ≤ ∫ (x : E), ↑f x ∂μ
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roo.isEmpty.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α] (r : Std.Roo α),
  r.isEmpty = decide (∀ (a : α), Std.PRange.succ? r.lower = some a → ¬a < r.upper)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionItemCapabilities.mk.sizeOf_spec : ∀ (insertReplaceSupport? : Option Bool),
  sizeOf { insertReplaceSupport? := insertReplaceSupport? } = 1 + sizeOf insertReplaceSupport?
-- Init.Data.Dyadic.Inv
/-- For a positive dyadic `x`, `1 < (invAtPrec x prec + 2^(-prec)) * x`.  -/
Dyadic.one_lt_invAtPrec_add_inc_mul : ∀ {x : Dyadic}, 0 < x → ∀ (prec : ℤ), 1 < (x.invAtPrec prec + Dyadic.ofIntWithPrec 1 prec) * x
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.mem_range_aleph_iff : ∀ {c : Cardinal.{u_1}}, c ∈ Set.range ⇑Cardinal.aleph ↔ Cardinal.aleph0 ≤ c
-- Init.Data.Option.Lemmas
Option.isSome_choice : ∀ {α : Type u_1} [Nonempty α], (Option.choice α).isSome = true
-- Mathlib.Data.List.Chain
List.isChain_cons_split : ∀ {α : Type u_1} {R : α → α → Prop} {a c : α} {l₁ l₂ : List α},
  List.IsChain R (a :: (l₁ ++ c :: l₂)) ↔ List.IsChain R (a :: (l₁ ++ [c])) ∧ List.IsChain R (c :: l₂)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.innerSL_apply_comp_of_isSymmetric : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E) {f : E →L[𝕜] E}, (↑f).IsSymmetric → (innerSL 𝕜) x ∘SL f = (innerSL 𝕜) (f x)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.rightAdjointObjIsDefined_limit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (R : CategoryTheory.Functor J D) [inst_3 : CategoryTheory.Limits.HasLimit R]
  [CategoryTheory.Limits.HasLimitsOfShape J C],
  (∀ (j : J), F.rightAdjointObjIsDefined (R.obj j)) → F.rightAdjointObjIsDefined (CategoryTheory.Limits.limit R)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image2_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β},
  Set.image2 (fun x1 x2 => x1 +ᵥ x2) s t = s +ᵥ t
-- Init.NotationExtra
Lean.unifConstraintElem : Lean.ParserDescr
-- Init.Data.ByteArray.Basic
_private.Init.Data.ByteArray.Basic.0.ByteArray.Iterator.remainingBytes.match_1.splitter : (motive : ByteArray.Iterator → Sort u_1) →
  (x : ByteArray.Iterator) → ((arr : ByteArray) → (i : ℕ) → motive { array := arr, idx := i }) → motive x
-- Mathlib.RingTheory.Extension.Generators
/-- Given families of generators `X ⊆ T` over `S` and `Y ⊆ S` over `R`,
there is a map of generators `R[Y] → R[X, Y]`.  -/
Algebra.Generators.toComp : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {ι' : Type u_3} →
              {T : Type u_7} →
                [inst_3 : CommRing T] →
                  [inst_4 : Algebra R T] →
                    [inst_5 : Algebra S T] →
                      [inst_6 : IsScalarTower R S T] →
                        (Q : Algebra.Generators S T ι') → (P : Algebra.Generators R S ι) → P.Hom (Q.comp P)
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
nndist_pi_const : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : Fintype β] [Nonempty β] (a b : α),
  (nndist (fun x => a) fun x => b) = nndist a b
-- Mathlib.Data.Fintype.Lattice
/-- A special case of `Finset.inf_eq_iInf` that omits the useless `x ∈ univ` binder.  -/
Finset.inf_univ_eq_iInf : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : CompleteLattice β] (f : α → β), Finset.univ.inf f = iInf f
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_image : ∀ (f : ZFSet.{u_1} → ZFSet.{u_1}) [inst : ZFSet.Definable₁ f] (x : ZFSet.{u_1}), ↑(ZFSet.image f x) = f '' ↑x
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.Context.mk.sizeOf_spec : ∀ (ellipsis explicit resultIsOutParamSupport : Bool) (numImplicitParams : ℕ),
  sizeOf
      { ellipsis := ellipsis, explicit := explicit, resultIsOutParamSupport := resultIsOutParamSupport,
        numImplicitParams := numImplicitParams } =
    1 + sizeOf ellipsis + sizeOf explicit + sizeOf resultIsOutParamSupport + sizeOf numImplicitParams
-- Mathlib.Order.Interval.Finset.Basic
/-- `Finset.cons` version of `Finset.Ioo_insert_right`.  -/
Finset.Ioc_eq_cons_Ioo : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α},
  a < b → Finset.Ioc a b = Finset.cons b (Finset.Ioo a b) ⋯
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.squashGCF.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_comp_inv : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : Semifield R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [inst_9 : ContinuousFunctionalCalculus R A p] [ContinuousInv₀ R]
  [ContinuousMap.UniqueHom R A] (f : R → R) (a : Aˣ),
  autoParam (ContinuousOn f ((fun x => x⁻¹) '' spectrum R ↑a)) cfc_comp_inv._auto_1 →
    autoParam (p ↑a) cfc_comp_inv._auto_3 → cfc (fun x => f x⁻¹) ↑a = cfc f ↑a⁻¹
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₃_eq_zero_of_mono₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, CategoryTheory.Mono T.mor₁ → T.mor₃ = 0
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The free monic polynomial of degree `n`, as a `MonicDegreeEq` in `R[X₁,...,Xₙ][X]`.  -/
Polynomial.MonicDegreeEq.freeMonic : (R : Type u_1) → [inst : CommRing R] → (n : ℕ) → Polynomial.MonicDegreeEq (MvPolynomial (Fin n) R) n
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The L-function of an odd function vanishes at negative odd integers.  -/
ZMod.LFunction_neg_two_mul_nat_sub_one : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ}, Function.Odd Φ → ∀ (n : ℕ), ZMod.LFunction Φ (-(2 * ↑n) - 1) = 0
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.fromLoop_apply : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  {p : LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const} {t : N → ↑unitInterval},
  (GenLoop.fromLoop i p) t = (p (t i)) ((Cube.splitAt i) t).2
-- Std.Data.HashMap.Basic
Std.HashMap.instBEq : {α : Type u} → {β : Type v} → {x : Hashable α} → [inst : BEq α] → [BEq β] → BEq (Std.HashMap α β)
-- Mathlib.Data.Set.Insert
/-- **Alias** of `LE.le.ssubset_of_mem_notMem`. -/
HasSubset.Subset.ssubset_of_mem_notMem : ∀ {α : Type u_1} {s t : Set α} {a : α}, s ⊆ t → a ∈ t → a ∉ s → s ⊂ t
-- Lean.Elab.Command
/-- Includes a given task (such as from `wrapAsyncAsSnapshot`) in the overall snapshot tree for this
command's elaboration, making its result available to reporting and the language server. The
reporter will not know about this snapshot tree node until the main elaboration thread for this
command has finished so this function is not useful for incremental reporting within a longer
elaboration thread but only for tasks that outlive it such as background kernel checking or proof
elaboration.
 -/
Lean.Elab.Command.logSnapshotTask : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.Topology.Hom.ContinuousEval
/-- If a type `F'` of bundled morphisms admits a continuous projection
to a type satisfying `ContinuousEval`,
then `F'` satisfies this predicate too.

The word "forget" in the name is motivated by the term "forgetful functor".  -/
ContinuousEval.of_continuous_forget : ∀ {F : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : FunLike F X Y] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [ContinuousEval F X Y] {F' : Type u_5}
  [inst_5 : FunLike F' X Y] [inst_6 : TopologicalSpace F'] {f : F' → F},
  Continuous f → autoParam (∀ (g : F'), ⇑(f g) = ⇑g) ContinuousEval.of_continuous_forget._auto_1 → ContinuousEval F' X Y
-- Mathlib.Order.Interval.Set.Disjoint
Set.Iio_disjoint_Ioi_same : ∀ {α : Type v} [inst : Preorder α] {a : α}, Disjoint (Set.Iio a) (Set.Ioi a)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward_obj_map_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R) (M : PresheafOfModules R) {X Y : Cᵒᵖ} (f : X ⟶ Y)
  (m : ↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app X))).obj (M.obj (Opposite.op (F.obj (Opposite.unop X)))))),
  (ModuleCat.Hom.hom (((PresheafOfModules.pushforward φ).obj M).map f)) m =
    (CategoryTheory.ConcreteCategory.hom (M.map (F.map f.unop).op)) m
-- Aesop.Frontend.Extension.Init
/-- Structure containing information about all declared Aesop rule sets.
 -/
Aesop.DeclaredRuleSets : Type
-- Mathlib.Algebra.BigOperators.Finprod
one_lt_finprod_cond : ∀ {ι : Type u_3} {M : Type u_7} [inst : CommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {p : ι → Prop},
  (∀ (i : ι), p i → 1 ≤ f i) →
    (∃ i, p i ∧ 1 < f i) → (Function.mulSupport f ∩ {i | p i}).Finite → 1 < ∏ᶠ (i : ι) (_ : p i), f i
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.Epi.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  (∀ {Z : C} (g h : Y ⟶ Z), CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f h → g = h) →
    CategoryTheory.Epi f
-- Mathlib.NumberTheory.FactorisationProperties
/-- A positive natural number `n` is _pseudoperfect_ if there exists a subset of the proper
divisors of `n` such that the sum of that subset is equal to `n`.  -/
Nat.Pseudoperfect : ℕ → Prop
-- Init.Data.Ord.Basic
Ordering.ne_gt_iff_isLE : ∀ {o : Ordering}, ¬o = Ordering.gt ↔ o.isLE = true
-- Mathlib.Algebra.Homology.Homotopy
/-- Any complex is homotopy equivalent to itself.  -/
HomotopyEquiv.refl : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] → {c : ComplexShape ι} → (C : HomologicalComplex V c) → HomotopyEquiv C C
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.mk.sizeOf_spec : ∀ {A : Type u_7} {B : Type u_8} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] [inst_4 : SizeOf A] [inst_5 : SizeOf B] (toAddMonoidHom : A →+ B)
  (continuous_toFun : autoParam (Continuous (↑toAddMonoidHom).toFun) ContinuousMap.continuous_toFun._autoParam),
  sizeOf { toAddMonoidHom := toAddMonoidHom, continuous_toFun := continuous_toFun } =
    1 + sizeOf toAddMonoidHom + sizeOf continuous_toFun
-- Mathlib.SetTheory.ZFC.Class
Class.coe_apply : ∀ {x y : ZFSet.{u}}, ↑y x ↔ x ∈ y
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.mk.injEq : ∀ (α : Type u) [isUniformSpace : UniformSpace α] [isCompleteSpace : CompleteSpace α] [isT0 : T0Space α] (α_1 : Type u)
  (isUniformSpace_1 : UniformSpace α_1) (isCompleteSpace_1 : CompleteSpace α_1) (isT0_1 : T0Space α_1),
  ({ α := α, isUniformSpace := isUniformSpace, isCompleteSpace := isCompleteSpace, isT0 := isT0 } =
      { α := α_1, isUniformSpace := isUniformSpace_1, isCompleteSpace := isCompleteSpace_1, isT0 := isT0_1 }) =
    (α = α_1 ∧ isUniformSpace ≍ isUniformSpace_1)
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_appIso : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (V : (↑U).Opens),
  AlgebraicGeometry.Scheme.Hom.appIso U.ι V =
    CategoryTheory.Iso.refl (X.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj V)))
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.cmp.match_1.eq_2 : ∀ (motive : PosNum → PosNum → Sort u_1) (x : PosNum) (h_1 : Unit → motive PosNum.one PosNum.one)
  (h_2 : (x : PosNum) → motive x PosNum.one) (h_3 : (x : PosNum) → motive PosNum.one x)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit0) (h_5 : (a b : PosNum) → motive a.bit0 b.bit1)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit0) (h_7 : (a b : PosNum) → motive a.bit1 b.bit1),
  (x = PosNum.one → False) →
    (match x, PosNum.one with
      | PosNum.one, PosNum.one => h_1 ()
      | x, PosNum.one => h_2 x
      | PosNum.one, x => h_3 x
      | a.bit0, b.bit0 => h_4 a b
      | a.bit0, b.bit1 => h_5 a b
      | a.bit1, b.bit0 => h_6 a b
      | a.bit1, b.bit1 => h_7 a b) =
      h_2 x
-- Mathlib.Order.Category.BddOrd
/-- The category of bounded orders with monotone functions.  -/
BddOrd : Type (u_1 + 1)
-- Mathlib.Algebra.Category.BoolRing
BoolRing.hasForgetToBoolAlg_forget₂_obj_coe : ∀ (X : BoolRing), ↑(CategoryTheory.HasForget₂.forget₂.obj X) = AsBoolAlg ↑X
-- Mathlib.Algebra.Polynomial.CoeffList
/-- Coefficients of a polynomial `P` are always the leading coefficient, some number of zeros, and
then `coeffList P.eraseLead`.  -/
Polynomial.coeffList_eraseLead : ∀ {R : Type u_1} [inst : Semiring R] {P : Polynomial R},
  P ≠ 0 →
    P.coeffList = P.leadingCoeff :: (List.replicate (P.natDegree - P.eraseLead.degree.succ) 0 ++ P.eraseLead.coeffList)
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_atTop : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [IsStrictOrderedRing α],
  Filter.Tendsto Int.ceil Filter.atTop Filter.atTop
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.map_comp : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} {T : Type u_3} [inst_1 : Semiring S] [inst_2 : Semiring T]
  (f : R →+* S) (g : S →+* T), PowerSeries.map (g.comp f) = (PowerSeries.map g).comp (PowerSeries.map f)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Bundled version of `compAlongOrderedFinpartition`, depending linearly on `f`
and multilinearly on `p`.  -/
OrderedFinpartition.compAlongOrderedFinpartitionₗ : {𝕜 : 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] →
                      {n : ℕ} →
                        (c : OrderedFinpartition n) →
                          (F [×c.length]→L[𝕜] G) →ₗ[𝕜]
                            MultilinearMap 𝕜 (fun i => E [×c.partSize i]→L[𝕜] F) (E [×n]→L[𝕜] G)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
AEMeasurable.const_inner : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {m : MeasurableSpace α} [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E]
  [SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f : α → E} {c : E},
  AEMeasurable f μ → AEMeasurable (fun x => inner 𝕜 c (f x)) μ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPullbacks.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  autoParam (∀ {X Y S : C} {f : X ⟶ S} (g : Y ⟶ S), P f → CategoryTheory.Limits.HasPullback f g)
      CategoryTheory.MorphismProperty.HasPullbacks.hasPullback._autoParam →
    P.HasPullbacks
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheaf.contMDiff_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] {N : Type u}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H N] {U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ}
  (f : (smoothSheaf IM I M N).presheaf.obj U), ContMDiff IM I ↑⊤ ↑f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get? k' = some k
-- Std.Time.Format
/-- Parses a `String` and returns a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.fromLeanDateTimeString : String → Except String Std.Time.PlainDateTime
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_biUnion : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {ι : Type u_4} {s : Set ι} {f : ι → Set α},
  s.Countable →
    s.Pairwise (Function.onFun Disjoint f) → (∀ b ∈ s, MeasurableSet (f b)) → v (⋃ b ∈ s, f b) = ∑' (p : ↑s), v (f ↑p)
-- Init.Prelude
/-- `BEq α` is a typeclass for supplying a boolean-valued equality relation on
`α`, notated as `a == b`. Unlike `DecidableEq α` (which uses `a = b`), this
is `Bool` valued instead of `Prop` valued, and it also does not have any
axioms like being reflexive or agreeing with `=`. It is mainly intended for
programming applications. See `LawfulBEq` for a version that requires that
`==` and `=` coincide.

Typically we prefer to put the "more variable" term on the left,
and the "more constant" term on the right.
 -/
BEq : Type u → Type u
-- Init.Data.List.Nat.Range
List.take_range'_of_length_ge : ∀ {n k start step : ℕ}, n ≥ k → List.take k (List.range' start n step) = List.range' start k step
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffOn_finsetSum`. -/
contMDiffOn_finset_sum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffOn I' I n (f i) s) → ContMDiffOn I' I n (fun x => ∑ i ∈ t, f i x) s
-- Lean.Data.NameTrie
Lean.instBEqNamePart.beq : Lean.NamePart → Lean.NamePart → Bool
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.InductionCandidate.mk : Lean.FVarId → Lean.InductiveVal → Lean.Meta.Try.Collector.InductionCandidate
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.finite_of_finite_mconv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : MeasurableSpace M] (μ ν : MeasureTheory.Measure M)
  [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν], MeasureTheory.IsFiniteMeasure (μ.mconv ν)
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.differentiableWithinAt_sqrt : ∀ {z : ℂ} {s : Set ℂ}, z ∈ Complex.slitPlane → DifferentiableWithinAt ℂ Complex.sqrt s z
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.equivBoundedOfCompact_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β],
  ⇑(ContinuousMap.equivBoundedOfCompact α β) = BoundedContinuousFunction.mkOfCompact
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_of_isEmpty : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m.WF → ∀ {a : α}, m.isEmpty = true → m.getKey! a = default
-- Mathlib.Combinatorics.Matroid.Basic
/-- If the difference of two IsBases is a singleton, then they differ by an insertion/removal  -/
Matroid.IsBase.eq_exchange_of_sdiff_eq_singleton : ∀ {α : Type u_1} {M : Matroid α} {B B' : Set α} {e : α},
  M.IsBase B → M.IsBase B' → B \ B' = {e} → ∃ f ∈ B' \ B, B' = insert f B \ {e}
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_map : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_4} (f : α → β) (g : β → γ) (m : MeasureTheory.OuterMeasure α),
  (MeasureTheory.OuterMeasure.map g) ((MeasureTheory.OuterMeasure.map f) m) = (MeasureTheory.OuterMeasure.map (g ∘ f)) m