mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.LanguageMap
_private.Mathlib.ModelTheory.LanguageMap.0.FirstOrder.Language.constantsOnFunc.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.iterFromIdx_toArray : ∀ {β : Type w} {n : ℕ} {xs : Vector β n} {pos : ℕ}, xs.toArray.iterFromIdx pos = xs.iterFromIdx pos
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Sdiff.adjDecidable : (V : Type u) → (G H : SimpleGraph V) → [DecidableRel G.Adj] → [DecidableRel H.Adj] → DecidableRel (G \ H).Adj
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.add_assoc : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Init.Data.List.Impl
/-- Inserts an element into a list at the specified index. If the index is greater than the length of
the list, then the list is returned unmodified.

In other words, the new element is inserted into the list `l` after the first `i` elements of `l`.

This is a tail-recursive version of `List.insertIdx`, used at runtime.

Examples:
 * `["tues", "thur", "sat"].insertIdxTR 1 "wed" = ["tues", "wed", "thur", "sat"]`
 * `["tues", "thur", "sat"].insertIdxTR 2 "wed" = ["tues", "thur", "wed", "sat"]`
 * `["tues", "thur", "sat"].insertIdxTR 3 "wed" = ["tues", "thur", "sat", "wed"]`
 * `["tues", "thur", "sat"].insertIdxTR 4 "wed" = ["tues", "thur", "sat"]`

 -/
List.insertIdxTR : {α : Type u_1} → List α → ℕ → α → List α
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_false_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = false ↔ ∀ b ∈ l, (a == b.fst) = false
-- Mathlib.Logic.Equiv.Defs
/-- A `PSigma`-type is equivalent to the corresponding `Sigma`-type.  -/
Equiv.psigmaEquivSigma : {α : Type u_2} → (β : α → Type u_1) → (i : α) ×' β i ≃ (i : α) × β i
-- Mathlib.Data.Nat.Cast.Basic
/-- If two `MonoidWithZeroHom`s agree on the positive naturals they are equal.  -/
ext_nat'' : ∀ {A : Type u_3} {F : Type u_4} [inst : MulZeroOneClass A] [inst_1 : FunLike F ℕ A] [ZeroHomClass F ℕ A] (f g : F),
  (∀ {n : ℕ}, 0 < n → f n = g n) → f = g
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.openCoverOfBase_I₀ : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : Z.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z),
  (AlgebraicGeometry.Scheme.Pullback.openCoverOfBase 𝒰 f g).I₀ = 𝒰.I₀
-- Mathlib.Algebra.Order.Floor.Div
/-- Do not use this. Use `zero_ceilDiv` instead.  -/
CeilDiv.zero_ceilDiv : ∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : CeilDiv α β] (a : α), 0 ⌈/⌉ a = 0
-- Mathlib.Algebra.Group.Defs
/-- One is a left neutral element for multiplication  -/
Monoid.one_mul : ∀ {M : Type u} [self : Monoid M] (a : M), 1 * a = a
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyGE? : {α : Type u} → {β : α → Type v} → [Ord α] → α → Std.DTreeMap.Internal.Impl α β → Option α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of `Left.neg_of_mul_neg_left`. -/
neg_of_mul_neg_left : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : LinearOrder α] [PosMulMono α], a * b < 0 → 0 ≤ b → a < 0
-- Mathlib.CategoryTheory.Subobject.Basic
/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows.  -/
CategoryTheory.Subobject.eq_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} {X Y : CategoryTheory.Subobject B}
  (f : CategoryTheory.Subobject.underlying.obj X ≅ CategoryTheory.Subobject.underlying.obj Y),
  CategoryTheory.CategoryStruct.comp f.hom Y.arrow = X.arrow → X = Y
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- For an adjoint quadruple `L ⊣ F ⊣ G ⊣ R` where `L` and `G` are fully faithful, all components
of the natural transformation `L ⟶ G` are epimorphisms iff all components of the natural
transformation `R ⟶ F` are monomorphisms.  -/
CategoryTheory.Adjunction.Quadruple.epi_leftTriple_leftToRight_app_iff_mono_rightTriple_rightToLeft_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R) [inst_2 : L.Full]
  [inst_3 : L.Faithful] [inst_4 : G.Full] [inst_5 : G.Faithful],
  (∀ (X : C), CategoryTheory.Epi (q.leftTriple.leftToRight.app X)) ↔
    ∀ (X : D), CategoryTheory.Mono (q.rightTriple.rightToLeft.app X)
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The **Sequential Banach-Alaoglu theorem**: the polar set of a neighborhood `s` of the origin in
a separable normed space `V` is a sequentially compact subset of `WeakDual 𝕜 V`.  -/
WeakDual.isSeqCompact_polar : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [TopologicalSpace.SeparableSpace E] [ProperSpace 𝕜] {s : Set E},
  s ∈ nhds 0 → IsSeqCompact (WeakDual.polar 𝕜 s)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Mapping by `f` and then forgetting is the same as forgetting.  -/
CategoryTheory.Over.mapForget_eq : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y),
  (CategoryTheory.Over.map f).comp (CategoryTheory.Over.forget Y) = CategoryTheory.Over.forget X
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toSubmonoid_mono : ∀ {R : Type u} [inst : NonAssocRing R], Monotone fun s => s.toSubmonoid
-- Mathlib.Algebra.Category.Grp.Limits
/-- A functor `F : J ⥤ CommGrpCat.{u}` has a limit iff `(F ⋙ forget CommGrpCat).sections` is
`u`-small.  -/
CommGrpCat.hasLimit_iff_small_sections : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat),
  CategoryTheory.Limits.HasLimit F ↔ Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instMin.eq_1 : ∀ {α : Type u_1} [inst : LE α], LowerSet.instMin = { min := fun s t => { carrier := ↑s ∩ ↑t, lower' := ⋯ } }
-- Init.Try
/-- If `wrapWithBy` is `true`, suggestions are wrapped with `by` for term mode usage.  -/
Lean.Try.Config.wrapWithBy : Lean.Try.Config → Bool
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of a strictly antitone function and an antitone function is strictly antitone.  -/
StrictAnti.mul_antitone' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} [MulLeftMono α]
  [MulRightStrictMono α], StrictAnti f → Antitone g → StrictAnti fun x => f x * g x
-- Mathlib.Order.Heyting.Basic
sdiff_inf_self_right : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), b \ (a ⊓ b) = b \ a
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.singleton_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {t : Set β} {a : α}, {a} • t = a • t
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂CompMap₂Iso_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  {C' : Type u₆} [inst_4 : CategoryTheory.Category.{v₆, u₆} C'] {D' : Type u₅}
  [inst_5 : CategoryTheory.Category.{v₅, u₅} D'] {R : CategoryTheory.Functor C' D'} {F' : CategoryTheory.Functor C' C}
  {G' : CategoryTheory.Functor D' D} {X : D'} (α' : F'.comp S ⟶ R.comp G') (β' : G'.obj X ⟶ T)
  (X_1 : CategoryTheory.CostructuredArrow R X),
  ((CategoryTheory.CostructuredArrow.map₂CompMap₂Iso α β α' β').hom.app X_1).left =
    CategoryTheory.CategoryStruct.id (F.obj (F'.obj X_1.left))
-- Mathlib.Algebra.Group.Prod
Prod.fst_add_snd : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (p : M × N), (p.1, 0) + (0, p.2) = p
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousOn_empty : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [IsEmpty ι]
  (F : ι → X → α) (S : Set X), EquicontinuousOn F S
-- Mathlib.Algebra.Group.PNatPowAssoc
PNatPowAssoc.mk : ∀ {M : Type u_2} [inst : Mul M] [inst_1 : Pow M ℕ+],
  (∀ (k n : ℕ+) (x : M), x ^ (k + n) = x ^ k * x ^ n) → (∀ (x : M), x ^ 1 = x) → PNatPowAssoc M
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_union_eq_right : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s t : Set α},
  Disjoint s t →
    MulAction.stabilizer G t ≤ MulAction.stabilizer G s →
      MulAction.stabilizer G (s ∪ t) ≤ MulAction.stabilizer G s →
        MulAction.stabilizer G (s ∪ t) = MulAction.stabilizer G t
-- Init.System.IOError
IO.Error.mkNoSuchThing : UInt32 → String → IO.Error
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsMk_app_hom : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (X : Rep.{u_1, u, v} k G),
  ModuleCat.Hom.hom ((Rep.coinvariantsMk k G).app X) = Representation.Coinvariants.mk X.ρ
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {a : α}, a +ᵥ ∅ = ∅
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, Array.map Sigma.fst t.toArray = t.keysArray
-- Mathlib.Data.Finset.Union
Finset.filter_disjiUnion : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (f : α → Finset β) (h : (↑s).PairwiseDisjoint f) (p : β → Prop)
  [inst : DecidablePred p], Finset.filter p (s.disjiUnion f h) = s.disjiUnion (fun a => Finset.filter p (f a)) ⋯
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.comp_map₂ : ∀ {B : Type u₁} [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [inst_2 : Quiver C]
  [inst_3 : (a b : C) → Quiver (a ⟶ b)] {D : Type u₃} [inst_4 : Quiver D] [inst_5 : (a b : D) → Quiver (a ⟶ b)]
  (F : CategoryTheory.PrelaxFunctorStruct B C) (G : CategoryTheory.PrelaxFunctorStruct C D) {a b : B} {f g : a ⟶ b}
  (η : f ⟶ g), (F.comp G).map₂ η = G.map₂ (F.map₂ η)
-- Mathlib.RingTheory.Ideal.Maps
RingHom.ker_evalRingHom : ∀ {ι : Type u_1} [inst : DecidableEq ι] (R : ι → Type u_2) [inst_1 : (i : ι) → CommRing (R i)] (i : ι),
  RingHom.ker (Pi.evalRingHom R i) = Ideal.span {1 - Pi.single i 1}
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.isPell_pellZd : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.IsPell (Pell.pellZd a1 n)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  t.contains a = false → t.getKey? a = none
-- Init.Data.UInt.Lemmas
UInt8.ofNatTruncate_eq_ofNat : ∀ n < UInt8.size, UInt8.ofNatClamp n = UInt8.ofNat n
-- Init.Data.Vector.Lemmas
Vector.foldlM_push : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  {a : α} {f : β → α → m β} {b : β},
  Vector.foldlM f b (xs.push a) = do
    let b ← Vector.foldlM f b xs
    f b a
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.addDeclToUnfold : Lean.Meta.SimpTheorems → Lean.Name → Lean.MetaM Lean.Meta.SimpTheorems
-- Mathlib.Algebra.IsPrimePow
IsPrimePow.two_le : ∀ {n : ℕ}, IsPrimePow n → 2 ≤ n
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_zero : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V], MeasureTheory.VectorMeasure.variation 0 = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_diff_of_contains_eq_false_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        m₂.contains k = false →
          Std.DHashMap.Internal.Raw₀.Const.get? (m₁.diff m₂) k = Std.DHashMap.Internal.Raw₀.Const.get? m₁ k
-- Init.Data.UInt.Lemmas
UInt32.toUSize_toUInt16 : ∀ (n : UInt32), n.toUInt16.toUSize = n.toUSize % 65536
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.star.sizeOf_spec : sizeOf Lean.Meta.RefinedDiscrTree.Key.star = 1
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
/-- Existence of local integral curves for a $C^1$ vector field on a `C^1` manifold without
boundary.  -/
exists_isMIntegralCurveAt_of_contMDiffAt_boundaryless : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {v : (x : M) → TangentSpace I x} (t₀ : ℝ) {x₀ : M} [CompleteSpace E]
  [BoundarylessManifold I M],
  ContMDiffAt I I.tangent 1 (fun x => ⟨x, v x⟩) x₀ → ∃ γ, γ t₀ = x₀ ∧ IsMIntegralCurveAt γ v t₀
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Converts `t : Monomial` to real function represented by the corresponding monomial, i.e.
`t.coef * basis[0]^t.exps[0] * basis[1]^t.exps[1] * ...`. It is always assumed that
`t.exps.length = basis.length`, but some theorems below do not require this assumption.  -/
Tactic.ComputeAsymptotics.Monomial.toFun : Tactic.ComputeAsymptotics.Monomial → Tactic.ComputeAsymptotics.Basis → ℝ → ℝ
-- Mathlib.Data.FinEnum
FinEnum.card_Int32 : FinEnum.card Int32 = 2 ^ 32
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` of the image of a function is the span of the pairwise subtractions with a
given point on the right, excluding the subtraction of that point from itself.  -/
vectorSpan_image_eq_span_vsub_set_right_ne : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) {s : Set ι} {i : ι},
  i ∈ s → vectorSpan k (p '' s) = Submodule.span k ((fun x => x -ᵥ p i) '' p '' (s \ {i}))
-- Mathlib.Data.Matrix.Reflection
Matrix.transposeᵣ.eq_def : ∀ {α : Type u_1} (x x_1 : ℕ) (x_2 : Matrix (Fin x) (Fin x_1) α),
  x_2.transposeᵣ =
    match x, x_1, x_2 with
    | x, 0, x_3 => Matrix.of ![]
    | x, n.succ, A => Matrix.of (Matrix.vecCons (FinVec.map (fun v => v 0) A) (A.submatrix id Fin.succ).transposeᵣ)
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- If `E : C ≌ D` and `E' : D ≌ F` are equivalences whose forward functors are compatible with shifts,
so is `(E.trans E').functor`.
 -/
CategoryTheory.Equivalence.CommShift.instCommShiftFunctorTrans : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (E : C ≌ D) →
          (A : Type u_3) →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  [E.functor.CommShift A] →
                    {F : Type u_4} →
                      [inst_6 : CategoryTheory.Category.{v_3, u_4} F] →
                        [inst_7 : CategoryTheory.HasShift F A] →
                          {E' : D ≌ F} → [E'.functor.CommShift A] → (E.trans E').functor.CommShift A
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A strong epi-mono factorisation is a decomposition `f = e ≫ m` with `e` a strong epimorphism
and `m` a monomorphism.  -/
CategoryTheory.Limits.StrongEpiMonoFactorisation : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Type (max u v)
-- Mathlib.CategoryTheory.IsomorphismClasses
/-- The functor that sends each category to the quotient space of its objects up to an isomorphism.
 -/
CategoryTheory.isomorphismClasses : CategoryTheory.Functor CategoryTheory.Cat (Type u)
-- Mathlib.Order.SuccPred.Basic
Order.succ_le_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, a ≤ b → Order.succ a ≤ Order.succ b
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instOfNat : {n : ℕ} → OfNat Std.Time.Timestamp n
-- Mathlib.Data.Set.Function
Set.LeftInvOn.congr_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {f₁' f₂' : β → α},
  Set.LeftInvOn f₁' f s → ∀ {t : Set β}, Set.MapsTo f s t → Set.EqOn f₁' f₂' t → Set.LeftInvOn f₂' f s
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.IsIPCOfShape.of_forall_exists : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape ι C],
  (∀ ⦃J : ι → Type w⦄ [inst_2 : (i : ι) → CategoryTheory.SmallCategory (J i)]
      [∀ (i : ι), CategoryTheory.IsFiltered (J i)] (F : (i : ι) → CategoryTheory.Functor (J i) C)
      [∀ (i : ι), CategoryTheory.Limits.HasColimit (F i)],
      ∃ c x, Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconePointwiseProduct c))) →
    CategoryTheory.Limits.IsIPCOfShape.{w, u_2, v_1, u_1} ι C
-- Batteries.Data.List.Lemmas
List.replaceF_cons_of_some : ∀ {α : Type u_1} {a' a : α} {l : List α} (p : α → Option α), p a = some a' → List.replaceF p (a :: l) = a' :: l
-- Mathlib.RingTheory.Adjoin.PowerBasis
/-- The power basis `1, x, ..., x ^ (d - 1)` for `K[x]`,
where `d` is the degree of the minimal polynomial of `x`. See `Algebra.adjoin.powerBasis'` for
a version over a more general base ring.  -/
Algebra.adjoin.powerBasis : {K : Type u_1} →
  {S : Type u_2} →
    [inst : Field K] → [inst_1 : CommRing S] → [inst_2 : Algebra K S] → {x : S} → IsIntegral K x → PowerBasis K ↥K[x]
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.opIso_hom_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).hom CategoryTheory.Limits.biprod.snd =
    CategoryTheory.Limits.biprod.inr.op
-- Mathlib.Topology.Order.ScottTopology
Topology.WithScott.instIsScottUnivSet : ∀ {α : Type u_1} [inst : Preorder α], Topology.IsScott (Topology.WithScott α) Set.univ
-- Mathlib.Data.Seq.Defs
/-- A sequence terminates if there is some position `n` at which it has terminated.  -/
Stream'.Seq.Terminates : {α : Type u} → Stream'.Seq α → Prop
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.homInduction_edge : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P : {x y : CategoryTheory.Join C D} → (x ⟶ y) → Sort u_1}
  (left : (x y : C) → (f : x ⟶ y) → P ((CategoryTheory.Join.inclLeft C D).map f))
  (right : (x y : D) → (f : x ⟶ y) → P ((CategoryTheory.Join.inclRight C D).map f))
  (edge : (c : C) → (d : D) → P (CategoryTheory.Join.edge c d)) {c : C} {d : D},
  CategoryTheory.Join.homInduction left right edge (CategoryTheory.Join.edge c d) = edge c d
-- Mathlib.CategoryTheory.Widesubcategory
/-- The inclusion of a wide subcategory is faithful.  -/
CategoryTheory.wideSubcategory.faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : P.IsMultiplicative], (CategoryTheory.wideSubcategoryInclusion P).Faithful
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker.eq_1 : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (f : M →ₛₗ[τ₁₂] M₂), f.ker = Submodule.comap f ⊥
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.b_app_ι_app_objEquiv_symm_val : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d) {n : SimplexCategory}
  (f : n ⟶ { len := d }),
  ↑((CategoryTheory.ConcreteCategory.hom ((SSet.relativeCellComplexOfMono.b i d).app (Opposite.op n)))
        ((CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op n)))
          (SSet.stdSimplex.objEquiv.symm f))) =
    (CategoryTheory.ConcreteCategory.hom (Y.map f.op)) c.simplex
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Let `F : C₀ ⥤ C` be a dense subsite and `data : ∀ X, F.OneHypercoverDenseData J₀ J X`
be a family. Let `G₀` be a sheaf on `C₀`. This is a presheaf on `C` which
extends `G₀` (see `OneHypercoverDenseData.essSurj.compPresheafIso`) and it is a sheaf
(see `OneHypercoverDenseData.essSurj.isSheaf`).  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheaf : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    ((X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        CategoryTheory.Sheaf J₀ A → CategoryTheory.Functor Cᵒᵖ A
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The underlying monoid homomorphism.  -/
AddCommMonCat.Hom.hom' : {A B : AddCommMonCat} → A.Hom B → ↑A →+ ↑B
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr),
  aig.decls.size ≤
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeftConst.go aig input distance curr hcurr s).aig.decls.size
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.empty_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp}, ∅ = t ↔ t = ∅
-- Mathlib.Algebra.Group.Basic
/-- Composing two multiplications on the right by `y` and `x`
is equal to a multiplication on the right by `y * x`.
 -/
comp_mul_right : ∀ {α : Type u_1} [inst : Semigroup α] (x y : α), ((fun x_1 => x_1 * x) ∘ fun x => x * y) = fun x_1 => x_1 * (y * x)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.snd_comp_toProd : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  (AddMonoidHom.snd M N).comp AddMonoid.Coprod.toProd = AddMonoid.Coprod.snd
-- Mathlib.Topology.Instances.Sign
instTopologicalSpaceSignType : TopologicalSpace SignType
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.List.map_unattach.match_1.splitter : {α : Type u_1} →
  {P : α → Prop} → (motive : Subtype P → Sort u_2) → (x : Subtype P) → ((x : α) → (h : P x) → motive ⟨x, h⟩) → motive x
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Type synonym to equip an ordered group with a new `Preorder` defined by the infinitesimal order
of elements. `a` is said less than `b` if `b` is infinitesimal comparing to `a`, or more precisely,
`∀ n, n • |b| < |a|`. If `a` and `b` are neither infinitesimal to each other, they are equivalent
in this order.  -/
ArchimedeanOrder : Type u_1 → Type u_1
-- Lean.Meta.Basic
Lean.Meta.instReprProjReductionKind : Repr Lean.Meta.ProjReductionKind
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey?_modify_eq_maxKey? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β}, (Std.DTreeMap.Const.modify t k f).maxKey? = t.maxKey?