mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Precomposing `f` with `Prod.fst` is `C^n` at `x : E × F`  -/
ContDiffAt.fst'' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → G} {x : E × F},
  ContDiffAt 𝕜 n f x.1 → ContDiffAt 𝕜 n (fun x => f x.1) x
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  (∀ (j : ι), ∃ i, c.Rel i j) →
    HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K =
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.π K) (HomologicalComplex.cylinder.ι₀ K) -
        CategoryTheory.CategoryStruct.id K.cylinder
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.preimageSingletonHomeomorph_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {b : B} (hb : b ∈ e.baseSet) (p : ↑(proj ⁻¹' {b})),
  (e.preimageSingletonHomeomorph hb) p = (↑e ↑p).2
-- Mathlib.SetTheory.Cardinal.Defs
/-- The universe lift operation on cardinals. You can specify the universes explicitly with
`lift.{u v} : Cardinal.{v} → Cardinal.{max v u}`  -/
Cardinal.lift : Cardinal.{v} → Cardinal.{max v u}
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.bipartiteAbove.congr_simp : ∀ {α : Type u_2} {β : Type u_3} (r r_1 : α → β → Prop),
  r = r_1 →
    ∀ (t t_1 : Finset β),
      t = t_1 →
        ∀ (a a_1 : α),
          a = a_1 →
            ∀ {inst : DecidablePred (r a)} [inst_1 : DecidablePred (r_1 a_1)],
              Finset.bipartiteAbove r t a = Finset.bipartiteAbove r_1 t_1 a_1
-- Lean.Meta.Sym.AlphaShareCommon
/-- Cache used by `shareCommonAlpha` to avoid visiting the same subterm (by pointer) of a
DAG-shaped input over and over again. It maps visited subterms to their maximally
shared results. Note that the `ExprPtr` keys own their expressions, so the cached
subterms are kept alive while the cache is alive and their pointers cannot be recycled.
 -/
Lean.Meta.Sym.AlphaShareCommon.Cache : Type
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.decidableLT.match_1.splitter : {α : Type u_1} →
  (motive : WithBot α → WithBot α → Sort u_2) →
    (x x_1 : WithBot α) →
      ((x : WithBot α) → motive x none) →
        ((a : α) → motive none (some a)) → ((a b : α) → motive (some a) (some b)) → motive x x_1
-- Mathlib.Analysis.Analytic.Constructions
/-- Scalar multiplication is analytic (jointly in both variables). The statement is a little
pedantic to allow towers of field extensions.  -/
analyticAt_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] [inst_5 : Module A E]
  [IsBoundedSMul A E] [IsScalarTower 𝕜 A E] (z : A × E), AnalyticAt 𝕜 (fun x => x.1 • x.2) z
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.monomial_mem_pow_idealOfVars_iff : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (n : ℕ) (x : σ →₀ ℕ) {r : R},
  r ≠ 0 → ((MvPolynomial.monomial x) r ∈ MvPolynomial.idealOfVars σ R ^ n ↔ n ≤ Finsupp.degree x)
-- Batteries.Data.UnionFind.Basic
/-- Index of root node  -/
Batteries.UnionFind.FindAux.root : {n : ℕ} → Batteries.UnionFind.FindAux n → Fin n
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- The counit of an adjunction between `F` and `G`  -/
CategoryTheory.Adjunction.CoreUnitCounit.counit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            CategoryTheory.Adjunction.CoreUnitCounit F G → (G.comp F ⟶ CategoryTheory.Functor.id D)
-- Mathlib.Order.Category.BddDistLat
BddDistLat.hom_ofHom : ∀ {X Y : Type u} [inst : DistribLattice X] [inst_1 : BoundedOrder X] [inst_2 : DistribLattice Y]
  [inst_3 : BoundedOrder Y] (f : BoundedLatticeHom X Y), BddDistLat.Hom.hom (BddDistLat.ofHom f) = f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffWithinAt.ccos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℂ n f s x → ContDiffWithinAt ℂ n (fun x => Complex.cos (f x)) s x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.edgeSet_sInf : ∀ {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph), (sInf s).edgeSet = (⋂ G' ∈ s, G'.edgeSet) ∩ G.edgeSet
-- Mathlib.Topology.Homotopy.Basic
/-- If we have a `ContinuousMap.Homotopy g₀ g₁` and a `ContinuousMap.Homotopy f₀ f₁`, then we can
compose them and get a `ContinuousMap.Homotopy (g₀.comp f₀) (g₁.comp f₁)`.
 -/
ContinuousMap.Homotopy.comp : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            {f₀ f₁ : C(X, Y)} → {g₀ g₁ : C(Y, Z)} → g₀.Homotopy g₁ → f₀.Homotopy f₁ → (g₀.comp f₀).Homotopy (g₁.comp f₁)
-- Mathlib.Data.Set.Restrict
Set.domRestrict_piecewise : ∀ {α : Type u_1} {β : Type u_2} (f g : α → β) (s : Set α) [inst : (x : α) → Decidable (x ∈ s)],
  s.domRestrict (s.piecewise f g) = s.domRestrict f
-- Mathlib.Analysis.Calculus.TangentCone.Defs
/-- A special case of `mem_tangentConeAt_of_frequently`, which avoids `Filter.Frequently`.  -/
mem_tangentConeAt_of_seq : ∀ {R : Type u} {E : Type v} [inst : AddCommGroup E] [inst_1 : SMul R E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x y : E} {α : Type u_1} (l : Filter α) [l.NeBot] (c : α → R) (d : α → E),
  Filter.Tendsto d l (nhds 0) →
    (∀ᶠ (n : α) in l, x + d n ∈ s) → Filter.Tendsto (fun n => c n • d n) l (nhds y) → y ∈ tangentConeAt R s x
-- Init.Data.Range.Polymorphic.Basic
Std.Roo.Internal.get_elem_helper_upper_open : ∀ {α : Type u} {r : Std.Roo α} {hi a : α} [LE α] [inst : LT α], a ∈ r → r.upper = hi → a < hi
-- Init.Data.BitVec.Lemmas
BitVec.not_append : ∀ {w v : ℕ} {x : BitVec w} {y : BitVec v}, ~~~(x ++ y) = ~~~x ++ ~~~y
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.mapErrorImp : {α : Type} → Lean.CoreM α → (Lean.MessageData → Lean.MessageData) → Lean.CoreM α
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.Hom.ext_iff : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W} {f g : A ⟶ B},
  f = g ↔ f.left = g.left ∧ f.right = g.right
-- Mathlib.Order.DirSupClosed
DirSupInacc.iUnion : ∀ {α : Type u_1} [inst : Preorder α] {ι : Sort u_2} {f : ι → Set α},
  (∀ (i : ι), DirSupInacc (f i)) → DirSupInacc (⋃ i, f i)
-- Mathlib.AlgebraicGeometry.Birational.Dominant
AlgebraicGeometry.Scheme.RationalMap.isDominant_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y),
  f.IsDominant ↔ Quotient.liftOn f (fun g => AlgebraicGeometry.IsDominant g.hom) ⋯
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocDecl : Type
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.Arg.mk : Lean.Expr → Option Lean.Expr → Mathlib.Meta.FunProp.Mor.Arg
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_add_sdiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → ∀ (t : Set α), μ s + μ (t \ s) = μ (s ∪ t)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_pnat_eq_tprod_of_eq_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {f : ℕ → M},
  f 0 = 1 → ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n
-- Mathlib.Algebra.Field.GeomSum
geom_sum_eq : ∀ {K : Type u_2} [inst : DivisionRing K] {x : K}, x ≠ 1 → ∀ (n : ℕ), ∑ i ∈ Finset.range n, x ^ i = (x ^ n - 1) / (x - 1)
-- Mathlib.Control.Bitraversable.Basic
Bitraversable.toBifunctor : {t : Type u → Type u → Type u} → [self : Bitraversable t] → Bifunctor t
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_le_one : ∀ {α : Type u_1} [Subsingleton α], ENat.card α ≤ 1
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_iterate_pred_ge : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι} (n : ℕ), -↑n ≤ toZ i0 (Order.pred^[n] i0)
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeSemigroup.toFreeMonoid_ne_one : ∀ {α : Type u_1} (x : FreeSemigroup α), FreeSemigroup.toFreeMonoid x ≠ 1
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.locallyLipschitzOn_interior : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ}
  [FiniteDimensional ℝ E], ConvexOn ℝ C f → LocallyLipschitzOn (interior C) f
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable ISize
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousMul.continuous_mul : ∀ {M : Type u_1} {inst : TopologicalSpace M} {inst_1 : Mul M} [self : ContinuousMul M], Continuous fun p => p.1 * p.2
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.id_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} (X : SheafOfModules R),
  (CategoryTheory.CategoryStruct.id X).val = CategoryTheory.CategoryStruct.id X.val
-- Mathlib.Analysis.Convex.StrictCombination
sum_mem_ball_of_strictConvexSpace : ∀ {V : Type u_2} {ι : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  {t : Finset ι} {w : ι → ℝ} {p : V} {r : ℝ} {z : ι → V},
  (∀ i ∈ t, 0 ≤ w i) →
    ∑ i ∈ t, w i = 1 →
      ∀ {i j : ι},
        i ∈ t →
          j ∈ t →
            z i ≠ z j →
              w i ≠ 0 → w j ≠ 0 → (∀ i ∈ t, z i ∈ Metric.closedBall p r) → ∑ k ∈ t, w k • z k ∈ Metric.ball p r
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_3 : Nat.Partrec.Code.left.encodeCode = 2
-- Init.Data.Nat.Basic
Nat.sub_eq_zero_of_le : ∀ {n m : ℕ}, n ≤ m → n - m = 0
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.measure_le_measure_closure_of_levyProkhorovEDist_eq_zero : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  {μ ν : MeasureTheory.Measure Ω},
  MeasureTheory.levyProkhorovEDist μ ν = 0 →
    ∀ {s : Set Ω}, MeasurableSet s → (∃ δ > 0, ν (Metric.thickening δ s) ≠ ⊤) → μ s ≤ ν (closure s)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E) (X : Type u_3)
  [inst_3 : SMul X F] [inst_4 : SMul X E] [inst_5 : IsScalarTower X F E],
  IsScalarTower X ↥(Algebra.adjoin F S) ↥(IntermediateField.adjoin F S)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_roc_eq_fallback : ∀ {m n fallback : ℤ} {i : ℕ}, (n - m).toNat ≤ i → (m<...=n).toArray.getD i fallback = fallback
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_normalizationPullback_fst : ∀ {X S Y : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.Limits.pullback.snd f g))
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationPullback f g)
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Hom.fromNormalization f) g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g)
      (AlgebraicGeometry.Scheme.Hom.toNormalization f)
-- Aesop.BuiltinRules.Ext
Aesop.BuiltinRules.ext : Aesop.RuleTac
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given closed range as a list in ascending order.
 -/
Std.Rio.toList : {α : Type u} →
  [Std.PRange.Least? α] →
    [inst : LT α] →
      [DecidableLT α] →
        [inst_2 : Std.PRange.UpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxo.IsAlwaysFinite α] → Std.Rio α → List α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_inter_conull' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α}, μ (s \ t) = 0 → μ (s ∩ t) = μ s
-- Mathlib.Order.Hom.Basic
OrderIso.symm_dual : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : α ≃o β), f.symm.dual = f.dual.symm
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_cpow_eq_rpow_re_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → ∀ {y : ℂ}, y.re ≠ 0 → ‖↑x ^ y‖ = x ^ y.re
-- Mathlib.Data.Num.Basic
/-- Multiplication of `ZNum`s.  -/
ZNum.mul : ZNum → ZNum → ZNum
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.δ_succ_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (self : f.RelStruct g i), CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) self.map = g.map
-- Mathlib.GroupTheory.GroupAction.Pointwise
/-- `preimage_smul_setₛₗ` in the context of groups  -/
Group.preimage_smul_setₛₗ : ∀ {G : Type u_1} {H : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : Group H] (σ : G → H)
  [inst_2 : MulAction G α] [inst_3 : MulAction H β] {F : Type u_5} [inst_4 : FunLike F α β]
  [MulActionSemiHomClass F σ α β] (f : F) (c : G) (t : Set β), ⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.slash_eq_zero_iff : ∀ {β : Type u_1} {G : Type u_2} {α : Type u_3} [inst : Group G] [inst_1 : AddGroup α] [inst_2 : SlashAction β G α]
  (k : β) (g : G) (a : α), SlashAction.map k g a = 0 ↔ a = 0
-- Mathlib.RingTheory.Ideal.Span
IsPrincipalIdealRing.principal : ∀ {R : Type u} {inst : Semiring R} [self : IsPrincipalIdealRing R] (S : Ideal R), Submodule.IsPrincipal S
-- Init.Data.Vector.Lemmas
Array.toVector_inj : ∀ {α : Type u_1} {xs ys : Array α} (h₁ : xs.size = ys.size), Vector.cast h₁ xs.toVector = ys.toVector → xs = ys
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The weak universal property of `DividedPowerAlgebra R M`.  -/
DividedPowerAlgebra.lift' : {R : Type u_2} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_4} →
            [inst_3 : CommSemiring A] →
              [inst_4 : Algebra R A] →
                {f : ℕ × M → A} →
                  (∀ (m : M), f (0, m) = 1) →
                    (∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)) →
                      (∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)) →
                        (∀ (n : ℕ) (u v : M),
                            f (n, u + v) =
                              ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
                                match x with
                                | (k, l) => f (k, u) * f (l, v)) →
                          DividedPowerAlgebra R M →ₐ[R] A
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.image_list_prod : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : FunLike F α β] [inst_1 : Monoid α] [inst_2 : Monoid β]
  [MonoidHomClass F α β] (f : F) (l : List (Set α)), ⇑f '' l.prod = (List.map (fun s => ⇑f '' s) l).prod
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.normAtPlace_polarCoord_symm_of_isComplex : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realMixedSpace K)
  {w : NumberField.InfinitePlace K} (hw : w.IsComplex),
  (NumberField.mixedEmbedding.normAtPlace w) (↑(NumberField.mixedEmbedding.polarCoord K).symm x) = ‖(x.2 ⟨w, hw⟩).1‖
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_sdiff_right`. -/
Set.diff_diff_right : ∀ {α : Type u_1} {s t u : Set α}, s \ (t \ u) = s \ t ∪ s ∩ u
-- Mathlib.Order.SuccPred.InitialSeg
/-- **Alias** of the reverse direction of `InitialSeg.isSuccLimit_apply_iff`. -/
InitialSeg.map_isSuccLimit : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : PartialOrder α] [inst_1 : PartialOrder β] (f : α ≤i β),
  Order.IsSuccLimit a → Order.IsSuccLimit (f a)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.sum_congr : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {ι : Type u_18} {A : ι → α → E'}
  {s : Finset ι} {B : ι → α → ℝ}, (∀ i ∈ s, A i =O[l] B i) → (fun H => ∑ i ∈ s, A i H) =O[l] fun H => ∑ i ∈ s, ‖B i H‖
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instHImp : {α : Type u_2} → [inst : TopologicalSpace α] → HImp (TopologicalSpace.Clopens α)
-- Lean.Server.Rpc.RequestHandling
/-- Checks whether a builtin RPC procedure exists with the given name.  -/
Lean.Server.existsBuiltinRpcProcedure : Lean.Name → IO Bool
-- Mathlib.MeasureTheory.Constructions.BorelSpace.WithTop
WithTop.instBorelSpace : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι], BorelSpace (WithTop ι)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If a function is countably sub-additive then it is sub-additive on finite sets  -/
rel_iSup_sum : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {γ : Type u_5}
  [inst_2 : CompleteLattice α] (m : α → M),
  m ⊥ = 0 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∑' (i : ℕ), m (s i))) →
        ∀ (s : γ → α) (t : Finset γ), R (m (⨆ d ∈ t, s d)) (∑ d ∈ t, m (s d))
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.weakPullback.lift_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasWeakPullback f g] (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakPullback.lift h k w)
      (CategoryTheory.Limits.weakPullback.snd f g) =
    k
-- Mathlib.Analysis.Real.Hyperreal
/-- A hyperreal number is positive infinite if it is larger than all real numbers.
**Do not use.** Write `0 < x ∧ ArchimedeanClass.mk x < 0` instead.  -/
Hyperreal.InfinitePos : ℝ* → Prop
-- Mathlib.Data.Set.Defs
/-- * `{ pat : X | p }` is notation for pattern matching in set-builder notation,
  where `pat` is a pattern that is matched by all objects of type `X`
  and `p` is a proposition that can refer to variables in the pattern.
  It is the set of all objects of type `X` which, when matched with the pattern `pat`,
  make `p` come out true.
* `{ pat | p }` is the same, but in the case when the type `X` can be inferred.

For example, `{ (m, n) : ℕ × ℕ | m * n = 12 }` denotes the set of all ordered pairs of
natural numbers whose product is 12.

Note that if the type ascription is left out and `p` can be interpreted as an extended binder,
then the extended binder interpretation will be used.  For example, `{ n + 1 | n < 3 }` will
be interpreted as `{ x : Nat | ∃ n < 3, n + 1 = x }` rather than using pattern matching.
 -/
Mathlib.Meta.«term{_|_}_1» : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.hom_ext_iff : ∀ {X Y : SFinKer} {κ η : X ⟶ Y}, κ = η ↔ κ.hom = η.hom
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.IsRefl.eq_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsRefl → ∀ {x y : M}, (B x) y = 0 ↔ (B y) x = 0
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.card_ring : FirstOrder.Language.ring.card = 5
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.length_toList : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.Rxi.HasSize α] [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [Std.Rxi.LawfulHasSize α], r.toList.length = r.size
-- Mathlib.Data.List.Defs
/-- Tail-recursive version of `List.iterate`.  -/
List.iterateTR : {α : Type u_1} → (α → α) → α → ℕ → List α
-- Mathlib.Probability.Kernel.Defs
/-- The underlying function of a kernel.

Do not use this function directly. Instead use the coercion coming from the `DFunLike`
instance.  -/
ProbabilityTheory.Kernel.toFun : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → ProbabilityTheory.Kernel α β → α → MeasureTheory.Measure β
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsFlat.subset_ground : ∀ {α : Type u_2} {M : Matroid α} {F : Set α}, M.IsFlat F → F ⊆ M.E
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add.0.Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cast.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig1 : Std.Sat.AIG α}
  (motive : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig1 → Sort u_1) (lhs rhs cin : aig1.Ref)
  (h_1 : (lhs rhs cin : aig1.Ref) → motive { lhs := lhs, rhs := rhs, cin := cin }),
  (match { lhs := lhs, rhs := rhs, cin := cin } with
    | { lhs := lhs, rhs := rhs, cin := cin } => h_1 lhs rhs cin) =
    h_1 lhs rhs cin
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.hasMul : {n : Type u} →
  [inst : DecidableEq n] →
    [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Mul (Matrix.SpecialLinearGroup n R)
-- Mathlib.Order.OrderDual
denselyOrdered_orderDual : ∀ {α : Type u_1} [inst : LT α], DenselyOrdered αᵒᵈ ↔ DenselyOrdered α
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rio_zero_right_eq_nil : ∀ {m : ℕ}, (m...0).toList = []
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- (Implementation) Transition map for construction of
`AlgebraicGeometry.Scheme.Cover.ColimitGluingData.functor`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [inst_1 : P.IsMultiplicative] →
      {S : AlgebraicGeometry.Scheme} →
        {J : Type u_1} →
          [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
            {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
              {𝒰 : S.OpenCover} →
                [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] →
                  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                    (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) →
                      {i j : 𝒰.I₀} →
                        (hij : i ⟶ j) →
                          (CategoryTheory.MorphismProperty.Over.map ⊤ ⋯).obj (d.cocone i).pt ⟶ (d.cocone j).pt
-- Mathlib.RingTheory.Perfection
/-- A ring homomorphism `R →+* S` induces `Perfection R p →+* Perfection S p`.  -/
Perfection.map : {R : Type u_1} →
  [inst : CommSemiring R] →
    (p : ℕ) →
      [hp : Fact (Nat.Prime p)] →
        [inst_1 : CharP R p] →
          {S : Type u₂} →
            [inst_2 : CommSemiring S] → [inst_3 : CharP S p] → (R →+* S) → Perfection R p →+* Perfection S p
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.continuousOn_Iic : ∀ {f : ℝ → ℝ} {y : ℝ}, ConcaveOn ℝ (Set.Iic y) f → ContinuousWithinAt f (Set.Iic y) y → ContinuousOn f (Set.Iic y)
-- Mathlib.Algebra.Category.Grp.EpiMono
AddGrpCat.epi_iff_surjective : ∀ {A B : AddGrpCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.Separation.Basic
Set.Finite.isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X}, s.Finite → IsClosed s
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instInfSet : {α : Type u_1} → [inst : LE α] → InfSet (UpperSet α)