mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Limits.exists_hom_of_preservesColimit_coyoneda : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D}
  (hc : CategoryTheory.Limits.IsColimit c) {X : C}
  [CategoryTheory.Limits.PreservesColimit D (CategoryTheory.coyoneda.obj (Opposite.op X))] (f : X ⟶ c.pt),
  ∃ j p, CategoryTheory.CategoryStruct.comp p (c.ι.app j) = f
-- Mathlib.Data.Multiset.Filter
Multiset.filterMap_add : ∀ {α : Type u_1} {β : Type v} (f : α → Option β) (s t : Multiset α),
  Multiset.filterMap f (s + t) = Multiset.filterMap f s + Multiset.filterMap f t
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumInr_injective : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language}, FirstOrder.Language.LHom.sumInr.Injective
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.withBRecOnArgs.go.eq_def : ∀ (k : Array Lean.Expr → Array Lean.Expr → Lean.MetaM Unit) (ctx : Lean.Meta.IndPredBelow.Context✝) (i : ℕ)
  (newMinors : Array Lean.Expr),
  Lean.Meta.IndPredBelow.withBRecOnArgs.go✝ k ctx i newMinors =
    if h : i < (Lean.Meta.IndPredBelow.Context.motives✝ ctx).size then
      have motive := (Lean.Meta.IndPredBelow.Context.motives✝ ctx)[i];
      do
      let motiveType ← Lean.Meta.inferType motive
      let type ←
        Lean.Meta.forallTelescope motiveType fun majors x => do
            let type ←
              liftM
                  (Lean.mkArrow (Lean.mkAppN (Lean.Meta.IndPredBelow.mkBelowAppOfIdx✝ i ctx) majors)
                    (Lean.mkAppN motive majors))
            Lean.Meta.mkForallFVars majors type
      Lean.Meta.withLocalDeclD (`F.appendIndexAfter (i + 1)) type fun minor =>
          Lean.Meta.IndPredBelow.withBRecOnArgs.go✝ k ctx (i + 1) (newMinors.push minor)
    else
      have recMotives :=
        Array.map (fun x => Lean.Meta.IndPredBelow.mkBelowAppOfIdx✝ x ctx)
          (Array.range (Lean.Meta.IndPredBelow.Context.motives✝ ctx).size);
      have recMinors := #[];
      do
      let __s ←
        forIn (Lean.Meta.IndPredBelow.Context.minors✝ ctx) recMinors fun minor __s =>
            have recMinors := __s;
            do
            let minorType ← Lean.Meta.inferType minor
            have i : ℕ :=
              Std.TreeMap.get! (Lean.Meta.IndPredBelow.Context.motiveToIdx✝ ctx)
                minorType.getForallBody.getAppFn.fvarId!
            let name ← minor.fvarId!.getUserName
            have belowCtorName : Lean.Name := (Lean.Meta.IndPredBelow.Context.belowNames✝ ctx)[i]! ++ name
            let expr ←
              Lean.Meta.forallTelescope minorType fun minorArgs res =>
                  Lean.Meta.IndPredBelow.withBRecOnArgs.go.go2✝ ctx newMinors belowCtorName minorArgs 0 #[] #[]
            have recMinors : Array Lean.Expr := recMinors.push expr
            pure (ForInStep.yield recMinors)
      have recMinors : Array Lean.Expr := __s
      k newMinors (Lean.Meta.IndPredBelow.Context.params✝ ctx ++ recMotives ++ recMinors)
-- Mathlib.Analysis.Convex.StrictConvexSpace
strictConvexSpace_iff : ∀ (𝕜 : Type u_1) (E : Type u_2) [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E], StrictConvexSpace 𝕜 E ↔ ∀ (r : ℝ), 0 < r → StrictConvex 𝕜 (Metric.closedBall 0 r)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α}, m.getKey? k = some k' ↔ ∃ (h : k ∈ m), m.getKey k h = k'
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.addRight_toEquiv : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd Gᵃᵒᵖ G] (c : G),
  (IsometryEquiv.addRight c).toEquiv = Equiv.addRight c
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_injective : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F],
  Function.Injective ContinuousLinearMapWOT.toCLM
-- Mathlib.Control.ULiftable
StateT.instULiftableULiftULift : {s : Type u₀} →
  {m : Type (max u₀ v₀) → Type u_5} →
    {m' : Type (max u₀ v₁) → Type u_6} →
      [ULiftable m m'] → ULiftable (StateT (ULift.{max v₀ u₀, u₀} s) m) (StateT (ULift.{max v₁ u₀, u₀} s) m')
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.mk_mul : ∀ {M : Type u_1} [inst : Mul M] (a b : M), DomMulAct.mk (a * b) = DomMulAct.mk b * DomMulAct.mk a
-- Mathlib.Algebra.Notation.Prod
Prod.smul_fst : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SMul E α] [inst_1 : SMul E β] (c : E) (p : α × β),
  (c • p).1 = c • p.1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorAppendTargetBlastAppend : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastAppend
-- Std.Http.Protocol.H1.Parser
Std.Http.Protocol.H1.TakeResult.incomplete.sizeOf_spec : ∀ (data : ByteSlice) (remaining : ℕ),
  sizeOf (Std.Http.Protocol.H1.TakeResult.incomplete data remaining) = 1 + sizeOf data + sizeOf remaining
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_eq_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {he : t.isEmpty = false}, t.maxKey he = t.maxKey!
-- Lean.Meta.Match.MatchPatternAttr
/-- Instructs the pattern matcher to unfold occurrences of this definition.

By default, only constructors and literals can be used for pattern matching. Using
`@[match_pattern]` allows using other definitions, as long as they eventually reduce to
constructors and literals.

Example:
```
@[match_pattern]
def yellowString : String := "yellow"

def isYellow (color : String) : Bool :=
  match color with
  | yellowString => true
  | _ => false
```
 -/
Lean.matchPatternAttr : Lean.TagAttribute
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- `Under.pushout f` is left adjoint to `Under.map f`.  -/
CategoryTheory.Under.mapPushoutAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f] →
          CategoryTheory.Under.pushout f ⊣ CategoryTheory.Under.map f
-- Mathlib.Analysis.SpecificLimits.Basic
ENNReal.exists_pos_sum_of_countable' : ∀ {ε : ENNReal}, ε ≠ 0 → ∀ (ι : Type u_4) [Countable ι], ∃ ε', (∀ (i : ι), 0 < ε' i) ∧ ∑' (i : ι), ε' i < ε
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addU_ne_zero_of_Y_ne : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → P 1 * Q 2 ≠ Q 1 * P 2 → WeierstrassCurve.Projective.addU P Q ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.lift_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N₁ N₂ : CategoryTheory.AddMon C} (f : M ⟶ N₁) (g : M ⟶ N₂),
  (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
-- Std.Data.HashMap.Lemmas
Std.HashMap.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, List.find? (fun x_2 => x_2.1 == k) m.toList = none ↔ m.contains k = false
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.erase_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, ∅.erase k = ∅
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.instTrans : {α : Type u} → {β : α → Type v} → Trans Std.DHashMap.Raw.Equiv Std.DHashMap.Raw.Equiv Std.DHashMap.Raw.Equiv
-- Mathlib.Data.List.Lattice
List.Subset.union_eq_right : ∀ {α : Type u_1} [inst : DecidableEq α] {xs ys : List α}, xs ⊆ ys → xs ∪ ys = ys
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_closure_of_mem : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α} {x : α}, x ∈ s → x ∈ BooleanSubalgebra.closure s
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Rco α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.succMany? pref.size r.lower).get ⋯
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair : ∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace V] [IsTopologicalRing R] [inst_5 : Module R V] [SeparatingDual R V] {x y : V},
  x ≠ 0 → y ≠ 0 → ∃ f, f x = 1 ∧ f y ≠ 0
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_nonpos_of_nonneg_of_nonpos : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b : R}, 0 ≤ a → b ≤ 0 → a * b ≤ 0
-- Mathlib.Algebra.Group.Action.Defs
/-- Type class for monoid actions on types, with notation `g • p`.

The `MulAction G P` typeclass says that the monoid `G` acts multiplicatively on a type `P`.
More precisely this means that the action satisfies the two axioms `1 • p = p` and
`(g₁ * g₂) • p = g₁ • (g₂ • p)`. A mathematician might simply say that the monoid `G`
acts on `P`.

For example, if `G` is a group and `X` is a type, if a mathematician says
say "let `G` act on the set `X`" they will probably mean `[MulAction G X]`.


[Wikidata Q288465](https://www.wikidata.org/wiki/Q288465) -/
MulAction : (α : Type u_9) → Type u_10 → [Monoid α] → Type (max u_10 u_9)
-- Mathlib.Data.Int.ModEq
Int.mod_modEq : ∀ (a n : ℤ), a % n ≡ a [ZMOD n]
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
NonUnitalClosedEmbeddingContinuousFunctionalCalculus.isClosedEmbedding : ∀ {R : Type u_1} {A : Type u_2} {p : outParam (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}
  [self : NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p] (a : A) (ha : p a),
  Topology.IsClosedEmbedding ⇑(cfcₙHom ha)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntryD.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : α × β) →
          ((fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (r : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (x : α × β) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β) →
                            (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                              (fallback : α × β) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                  fallback) →
                motive x x_1
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mk.injEq : ∀ {K : Type u} [inst : Field K] (toSubring : Subring K)
  (mem_or_inv_mem' : ∀ (x : K), x ∈ toSubring.carrier ∨ x⁻¹ ∈ toSubring.carrier) (toSubring_1 : Subring K)
  (mem_or_inv_mem'_1 : ∀ (x : K), x ∈ toSubring_1.carrier ∨ x⁻¹ ∈ toSubring_1.carrier),
  ({ toSubring := toSubring, mem_or_inv_mem' := mem_or_inv_mem' } =
      { toSubring := toSubring_1, mem_or_inv_mem' := mem_or_inv_mem'_1 }) =
    (toSubring = toSubring_1)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.monomial.eq_1 : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ →₀ ℕ), MvPolynomial.monomial s = AddMonoidAlgebra.lsingle s
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Two continuous multiplicative isomorphisms agree if they are defined by the
same underlying function.  -/
ContinuousMulEquiv.ext : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {f g : M ≃ₜ* N}, (∀ (x : M), f x = g x) → f = g
-- Lean.Message
Lean.MessageData.trace.injEq : ∀ (data : Lean.TraceData) (msg : Lean.MessageData) (children : Array Lean.MessageData) (data_1 : Lean.TraceData)
  (msg_1 : Lean.MessageData) (children_1 : Array Lean.MessageData),
  (Lean.MessageData.trace data msg children = Lean.MessageData.trace data_1 msg_1 children_1) =
    (data = data_1 ∧ msg = msg_1 ∧ children = children_1)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonLocation : Lean.ToJson Lean.Lsp.Location
-- Mathlib.Computability.Partrec
Partrec.const' : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] (s : Part σ), Partrec fun x => s
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- An oplax monoidal functor takes comonoid objects to comonoid objects.

That is, an oplax monoidal functor `F : C ⥤ D` induces a functor `Comon C ⥤ Comon D`.
 -/
CategoryTheory.Functor.mapComon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.OplaxMonoidal] → CategoryTheory.Functor (CategoryTheory.Comon C) (CategoryTheory.Comon D)
-- Lean.Elab.Tactic.Simp
Lean.Meta.DSimp.ConfigWithOptions.mk.inj : ∀ {config : Lean.Meta.DSimp.Config} {userConfig : Lean.Options} {config_1 : Lean.Meta.DSimp.Config}
  {userConfig_1 : Lean.Options},
  { config := config, userConfig := userConfig } = { config := config_1, userConfig := userConfig_1 } →
    config = config_1 ∧ userConfig = userConfig_1
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
/-- An auxiliary result bounding the size of the entries of the representatives in `reps`  -/
FixedDetMatrices.reps_entries_le_m' : ∀ {m : ℤ} {A : FixedDetMatrix (Fin 2) ℤ m},
  A ∈ FixedDetMatrices.reps m → ∀ (i j : Fin 2), ↑A i j ∈ Finset.Icc (-|m|) |m|
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (curr : ℕ) → motive curr.succ),
  (match 0 with
    | 0 => h_1 ()
    | curr.succ => h_2 curr) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- **Alias** of `SimpleGraph.Walk.IsHamiltonian.setOfPred_support`. -/
SimpleGraph.Walk.IsHamiltonian.setOf_support : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b},
  p.IsHamiltonian → {v | v ∈ p.support} = Set.univ
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A variant of `lift_unique` with `Z` a terminal object.  -/
CategoryTheory.WithTerminal.liftToTerminalUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (hZ : CategoryTheory.Limits.IsTerminal Z) →
              (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) →
                (CategoryTheory.WithTerminal.incl.comp G ≅ F) →
                  (G.obj CategoryTheory.WithTerminal.star ≅ Z) → (G ≅ CategoryTheory.WithTerminal.liftToTerminal F hZ)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_congr_subtype : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) {P Q : β → Prop},
  (∀ (x : β), P x ↔ Q x) → ∑' (x : { x // P x }), f ↑x = ∑' (x : { x // Q x }), f ↑x
-- Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
SummableLocallyUniformlyOn_of_locally_bounded : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup F] [CompleteSpace F]
  [inst_2 : TopologicalSpace β] [LocallyCompactSpace β] {f : α → β → F} {s : Set β},
  IsOpen s →
    (∀ K ⊆ s, IsCompact K → ∃ u, Summable u ∧ ∀ (n : α), ∀ k ∈ K, ‖f n k‖ ≤ u n) → SummableLocallyUniformlyOn f s
-- Mathlib.RingTheory.Nakayama
/-- **Nakayama's Lemma** - Statement (2) in
[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV).
See also `eq_smul_of_le_smul_of_le_jacobson` for a generalisation
to the `jacobson` of any ideal  -/
Submodule.eq_bot_of_le_smul_of_le_jacobson_bot : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (N : Submodule R M), N.FG → N ≤ I • N → I ≤ ⊥.jacobson → N = ⊥
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.preservesColimitsOfSize_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C}
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v, u} C] {Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v, v, max u v, max u v} (CategoryTheory.Over.map f)
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The integrand in `next` is continuous.  -/
ODE.FunSpace.continuousOn_comp_compProj : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∀ (α : ODE.FunSpace t₀ x₀ r L), ContinuousOn (fun t' => f t' (α.compProj t')) (Set.Icc tmin tmax)
-- Mathlib.Algebra.Lie.Extension
/-- Given an extension of `L` by `M` whose kernel `M` is abelian, the kernel `M` gets an `L`-module
structure. We do not make this an instance, because we may have to work with more than one
extension.  -/
LieAlgebra.Extension.ringModuleOf : {R : Type u_1} →
  {L : Type u_3} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : LieRing M] →
              [inst_4 : LieAlgebra R M] → [IsLieAbelian M] → LieAlgebra.Extension R M L → LieRingModule L M
-- Mathlib.Data.Set.Prod
Set.pi_eq_empty_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t : (i : ι) → Set (α i)},
  s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
-- Mathlib.Topology.Separation.Hausdorff
limUnder_nhdsWithin_id : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {x : X} {s : Set X},
  x ∈ closure s → (nhdsWithin x s).limUnder id = x
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.writeResponseError : IO.FS.Stream → Lean.JsonRpc.ResponseError Unit → IO Unit
-- Mathlib.RingTheory.Coprime.Basic
isCoprime_self : ∀ {R : Type u} [inst : CommSemiring R] {x : R}, IsCoprime x x ↔ IsUnit x
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.induction_on : ∀ {α : Type u} {s : Set α} {p : Set α → Prop}, s.Subsingleton → p ∅ → (∀ (x : α), p {x}) → p s
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.AddMon C),
  CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.counitIsoAux C F =
    CategoryTheory.Iso.refl
      (((CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal C).comp
              (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToAddMon C)).obj
          F).X
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagSource.other : Lean.Meta.Grind.EMatchDiagSource
-- Mathlib.Algebra.Group.Finsupp
Finsupp.addCommute_iff_inter : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [inst_1 : DecidableEq ι] {f g : ι →₀ M},
  AddCommute f g ↔ ∀ x ∈ f.support ∩ g.support, AddCommute (f x) (g x)
-- Mathlib.Algebra.Group.Irreducible.Defs
AddIrreducible.ne_zero : ∀ {M : Type u_1} [inst : AddMonoid M] {p : M}, AddIrreducible p → p ≠ 0
-- Mathlib.Data.Set.Finite.Lattice
DirectedOn.exists_mem_subset_of_finite_of_subset_sUnion : ∀ {α : Type u_1} {c : Set (Set α)},
  c.Nonempty → DirectedOn (fun x1 x2 => x1 ⊆ x2) c → ∀ {s : Set α}, s.Finite → s ⊆ ⋃₀ c → ∃ t ∈ c, s ⊆ t
-- Mathlib.Algebra.Category.Ring.Instances
localization_unit_isIso : ∀ (R : CommRingCat), CategoryTheory.IsIso (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away 1)))
-- Mathlib.Order.Partition.Equipartition
Finpartition.not_isEquipartition : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s},
  ¬P.IsEquipartition ↔ ∃ a ∈ P.parts, ∃ b ∈ P.parts, b.card + 1 < a.card
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.sub : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f g : α → β} [inst_1 : SubtractionMonoid β] [ContinuousSub β],
  MeasureTheory.AEFinStronglyMeasurable f μ →
    MeasureTheory.AEFinStronglyMeasurable g μ → MeasureTheory.AEFinStronglyMeasurable (f - g) μ
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- For any functor `K : J ⥤ Over X`, there is a canonical extension
`WithTerminal J ⥤ C`, that sends `star` to `X`.  -/
CategoryTheory.WithTerminal.liftFromOver : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          CategoryTheory.Functor (CategoryTheory.Functor J (CategoryTheory.Over X))
            (CategoryTheory.Functor (CategoryTheory.WithTerminal J) C)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_span : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (s : Set A), ProjectiveSpectrum.zeroLocus 𝒜 ↑(Ideal.span s) = ProjectiveSpectrum.zeroLocus 𝒜 s
-- Mathlib.CategoryTheory.Quotient.Linear
/-- Auxiliary definition for `Quotient.linear`.  -/
CategoryTheory.Quotient.Linear.module : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear R C] →
            (r : HomRel C) →
              [CategoryTheory.Congruence r] →
                (∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) →
                  [inst_5 : CategoryTheory.Preadditive (CategoryTheory.Quotient r)] →
                    [(CategoryTheory.Quotient.functor r).Additive] →
                      (X Y : CategoryTheory.Quotient r) → Module R (X ⟶ Y)
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubmonoid.coe_even : ∀ {M : Type u_1} [inst : AddCommMonoid M], ↑(AddSubmonoid.even M) = {s | Even s}
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.N₁Γ₀_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ),
  AlgebraicTopology.DoldKan.N₁Γ₀.inv.app K =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Idempotents.toKaroubi (ChainComplex C ℕ)).map
        (AlgebraicTopology.DoldKan.Γ₀NondegComplexIso K).inv)
      (AlgebraicTopology.DoldKan.Γ₀.splitting K).toKaroubiNondegComplexIsoN₁.hom
-- Mathlib.Algebra.CharP.Algebra
Subfield.expChar : ∀ {R : Type u_1} [inst : DivisionRing R] (L : Subfield R) (p : ℕ) [ExpChar R p], ExpChar (↥L) p