mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- A "diagonal" morphism from the right object of `u` to the left object of `v`.  -/
CategoryTheory.Arrow.LeftHomotopy.hom : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} → {f g : u ⟶ v} → CategoryTheory.Arrow.LeftHomotopy f g → (u.right ⟶ v.left)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
fderivWithin_congr' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  Set.EqOn f₁ f s → x ∈ s → fderivWithin 𝕜 f₁ s x = fderivWithin 𝕜 f s x
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.sup_adj : ∀ {V : Type u_2} (x y : Digraph V) (v w : V), (x ⊔ y).Adj v w ↔ x.Adj v w ∨ y.Adj v w
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ioc_left : ∀ {α : Type v} [inst : Preorder α] [NoMinOrder α] (a : α), ⋃ b, Set.Ioc b a = Set.Iic a
-- Init.PropLemmas
dite_else_false : ∀ {p : Prop} [inst : Decidable p] {x : p → Prop}, (if h : p then x h else False) ↔ ∃ (h : p), x h
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.ofIsoWeakLimit.eq_1 : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {r t : CategoryTheory.Limits.Cone F}
  (P : CategoryTheory.Limits.IsWeakLimit r) (i : r ≅ t),
  P.ofIsoWeakLimit i = { lift := fun s => CategoryTheory.CategoryStruct.comp (P.lift s) i.hom.hom, fac := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
instLinearOrderedAddCommGroupWithTopAdditiveOrderDual : {α : Type u_1} → [LinearOrderedCommGroupWithZero α] → LinearOrderedAddCommGroupWithTop (Additive αᵒᵈ)
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- Preserving filtered colimits at any universe implies preserving filtered colimits at universe `0`.
 -/
CategoryTheory.Limits.preservesSmallestFilteredColimits_of_preservesFilteredColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
-- Init.Data.List.Lemmas
List.getLast?_isSome : ∀ {α : Type u_1} {l : List α}, l.getLast?.isSome = true ↔ l ≠ []
-- Init.Internal.Order.Basic
/-- The flat partial order generated by `∀ x, b ⊑ x`.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.FlatOrder.rel : {α : Sort u} → {b : α} → Lean.Order.FlatOrder b → Lean.Order.FlatOrder b → Prop
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.image_sdiv_prod : ∀ {α : Type u_2} {β : Type u_3} [inst : SDiv α β] {s t : Set β}, (fun x => x.1 /ₛ x.2) '' s ×ˢ t = s /ₛ t
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- The walk in reverse.  -/
SimpleGraph.Walk.reverse : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Walk u v → G.Walk v u
-- Mathlib.Algebra.Notation.FiniteSupport
Function.support_along_fiber_finite_of_finite : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (f : α × β → γ) (a : α),
  Function.HasFiniteSupport f → Function.HasFiniteSupport fun b => f (a, b)
-- Mathlib.Data.Stream.Init
Stream'.mem_of_mem_odd : ∀ {α : Type u} (a : α) (s : Stream' α), a ∈ s.odd → a ∈ s
-- Mathlib.Analysis.ODE.Transform
isIntegralCurveOn_comp_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ}
  {dt : ℝ}, IsIntegralCurveOn (γ ∘ fun x => x - dt) (v ∘ fun x => x - dt) (dt +ᵥ s) ↔ IsIntegralCurveOn γ v s
-- Init.Data.Iterators.Basic
Std.IterM.TerminationMeasures.Finite.Rel.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β],
  Std.IterM.TerminationMeasures.Finite.Rel =
    Relation.TransGen (InvImage Std.IterM.IsPlausibleSuccessorOf Std.IterM.TerminationMeasures.Finite.it)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.compMeasurable_toGerm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] [inst_3 : MeasurableSpace β] [inst_4 : BorelSpace β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : TopologicalSpace.PseudoMetrizableSpace γ]
  [inst_7 : SecondCountableTopology γ] [inst_8 : MeasurableSpace γ] [inst_9 : OpensMeasurableSpace γ] (g : β → γ)
  (hg : Measurable g) (f : α →ₘ[μ] β), (MeasureTheory.AEEqFun.compMeasurable g hg f).toGerm = Filter.Germ.map g f.toGerm
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [IsAddTorsionFree R],
  Polynomial.derivative p = 0 ↔ p.natDegree = 0
-- Lean.DocString.Markdown
Lean.Doc.MdRendererState.mk.sizeOf_spec : ∀ (imported current : Lean.NameMap Lean.Name),
  sizeOf { imported := imported, current := current } = 1 + sizeOf imported + sizeOf current
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.monic_map_iff : ∀ {R : Type u} {S : Type v} [inst : Ring R] [IsSimpleRing R] [inst_2 : Semiring S] [Nontrivial S] {f : R →+* S}
  {p : Polynomial R}, (Polynomial.map f p).Monic ↔ p.Monic
-- Init.Notation
/-- Addition of priorities. This is normally used only for offsetting, e.g. `default + 1`.  -/
Lean.Parser.Syntax.addPrio : Lean.TrailingParserDescr
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans'_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (h : e.target = e'.source)
  (a : γ), ↑(e.trans' e' h).symm a = (↑e.symm ∘ ↑e'.symm) a
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.mul_def : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (e e' : P₁ ≃ᵃ[k] P₁), e * e' = e'.trans e
-- Mathlib.Data.Fin.Tuple.Basic
/-- Updating the last element of a tuple does not change the beginning.  -/
Fin.init_update_last : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (q : (i : Fin (n + 1)) → α i) (z : α (Fin.last n)),
  Fin.init (Function.update q (Fin.last n) z) = Fin.init q
-- Mathlib.CategoryTheory.Limits.Cones
/-- Functorially postcompose a cone for `F` by a natural transformation `F ⟶ G` to give a cone for `G`.
 -/
CategoryTheory.Limits.Cone.postcompose : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (F ⟶ G) → CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone G)
-- Mathlib.Data.Fin.Tuple.Finset
Finset.filter_piFinset_eq_map_snocEquiv : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α i.castSucc) → Prop)
  [inst : DecidablePred P],
  {r ∈ Fintype.piFinset S | P (Fin.init r)} =
    Finset.map (Fin.snocEquiv α).toEmbedding (S (Fin.last n) ×ˢ {r ∈ Fintype.piFinset (Fin.init S) | P r})
-- Aesop.Util.UnionFind
Aesop.UnionFind.toRep : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Aesop.UnionFind α → Std.HashMap α USize
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SOppSide.congr_simp : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s s_1 : AffineSubspace R P),
  s = s_1 → ∀ (x x_1 : P), x = x_1 → ∀ (y y_1 : P), y = y_1 → s.SOppSide x y = s_1.SOppSide x_1 y_1
-- Mathlib.GroupTheory.Coset.Basic
LeftCosetEquivalence.eq_1 : ∀ {α : Type u_1} [inst : Mul α] (s : Set α) (a b : α), LeftCosetEquivalence s a b = (a • s = b • s)
-- Std.Http.Data.URI.Config
/-- Maximum number of query parameters (key-value pairs separated by `&`).
 -/
Std.Http.URI.Config.maxQueryParams : Std.Http.URI.Config → ℕ
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.homRel_equivalence_of_isFibrant_tgt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.CofibrantObject C} [HomotopicalAlgebra.IsFibrant Y.obj],
  Equivalence fun x1 x2 => HomotopicalAlgebra.CofibrantObject.homRel C x1 x2
-- Mathlib.Logic.ExistsUnique
existsUnique_eq : ∀ {α : Sort u_1} {a' : α}, ∃! a, a = a'
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
/-- The equivalence `ToType (X₁ ⨯ X₂) ≃ (ToType X₁) × (ToType X₂)`
if `X₁` and `X₂` are objects in a concrete category `C`.  -/
CategoryTheory.Limits.Concrete.prodEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type w} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            (X₁ X₂ : C) →
              [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂] →
                [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)] →
                  CategoryTheory.ToType (X₁ ⨯ X₂) ≃ CategoryTheory.ToType X₁ × CategoryTheory.ToType X₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.mapArrowLeft_comp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₂ : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom)
  {f₁'' : CategoryTheory.Arrow C₁} (sq₁₂'' : F.PushoutObjObj f₁''.hom f₂.hom) (sq : f₁ ⟶ f₁') (sq' : f₁' ⟶ f₁''),
  CategoryTheory.CategoryStruct.comp (sq₁₂.mapArrowLeft sq₁₂' sq) (sq₁₂'.mapArrowLeft sq₁₂'' sq') =
    sq₁₂.mapArrowLeft sq₁₂'' (CategoryTheory.CategoryStruct.comp sq sq')
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.distribSMul.eq_1 : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : DistribSMul N R],
  MonoidAlgebra.distribSMul = { toSMulZeroClass := MonoidAlgebra.smulZeroClass, smul_add := ⋯ }
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.eq_1 : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  (s1 s2 : Set (Set Ω)) (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndepSets m' hm' s1 s2 μ =
    ProbabilityTheory.Kernel.IndepSets s1 s2 (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')
-- Mathlib.Order.Antisymmetrization
/-- `ofAntisymmetrization` as an order embedding.  -/
OrderEmbedding.ofAntisymmetrization : (α : Type u_1) → [inst : Preorder α] → (Antisymmetrization α fun x1 x2 => x1 ≤ x2) ↪o α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulMon : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulMon k m p) =
    ↑k * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.card_le : ∀ {L : FirstOrder.Language} {α : Type u'},
  Cardinal.mk (L.Term α) ≤ max Cardinal.aleph0 (Cardinal.mk (α ⊕ (i : ℕ) × L.Functions i))
-- Init.Grind.Ring.Basic
/-- One is the left identity for multiplication.  -/
Lean.Grind.Semiring.one_mul : ∀ {α : Type u} [self : Lean.Grind.Semiring α] (a : α), 1 * a = a
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_iff_eq_mul_right : ∀ {a b c : ℤ}, b ≠ 0 → b ∣ a → (a / b = c ↔ a = b * c)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_quotQuotEquivCommₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ⇑(DoubleQuot.quotQuotEquivCommₐ R I J) = ⇑(DoubleQuot.quotQuotEquivComm I J)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Increment.0.SzemerediRegularity.distinctPairs.eq_1 : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} (hP : P.IsEquipartition)
  (G : SimpleGraph α) [inst_2 : DecidableRel G.Adj] (ε : ℝ) (x : ↥P.parts.offDiag),
  SzemerediRegularity.distinctPairs✝ hP G ε x =
    (SzemerediRegularity.chunk hP G ε ⋯).parts ×ˢ (SzemerediRegularity.chunk hP G ε ⋯).parts
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.mem_inf : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S T : IntermediateField F E}
  {x : E}, x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyLED_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLED k fallback = t₂.getKeyLED k fallback
-- Mathlib.CategoryTheory.Limits.Constructions.Equalizers
CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst_eq_pullback_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C),
  CategoryTheory.Limits.HasEqualizersOfHasPullbacksAndBinaryProducts.pullbackFst F =
    CategoryTheory.Limits.pullback.snd
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.zero))
        (F.map CategoryTheory.Limits.WalkingParallelPairHom.left))
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.id (F.obj CategoryTheory.Limits.WalkingParallelPair.zero))
        (F.map CategoryTheory.Limits.WalkingParallelPairHom.right))
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.HasPathObject.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K K_1 : HomologicalComplex C c) (e_K : K = K_1)
  [inst_2 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)], K.HasPathObject = K_1.HasPathObject
-- Std.Sync.CancellationContext
Std.CancellationContext.mk.injEq : ∀ (state : Std.Mutex Std.CancellationContext.State) (token : Std.CancellationToken) (id : UInt64)
  (state_1 : Std.Mutex Std.CancellationContext.State) (token_1 : Std.CancellationToken) (id_1 : UInt64),
  ({ state := state, token := token, id := id } = { state := state_1, token := token_1, id := id_1 }) =
    (state = state_1 ∧ token = token_1 ∧ id = id_1)
-- Aesop.Util.Basic
Aesop.time : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadLiftT BaseIO m] → m α → m (α × Aesop.Nanos)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.PreOneHypercover.map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : C} (E : CategoryTheory.PreOneHypercover X) (F : CategoryTheory.Functor C D) {D' : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D'] (G : CategoryTheory.Functor D D'), E.map (F.comp G) = (E.map F).map G
-- Mathlib.Data.Semiquot
Semiquot.mk' : {α : Type u_1} → (s : Set α) → Trunc ↑s → Semiquot α
-- Mathlib.Tactic.DepRewrite
/-- A piece of metadata associated with `depRewrite`.  -/
Mathlib.Tactic.DepRewrite.castMData : Lean.MData
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- `Injective.under X` provides an arbitrarily chosen injective object equipped with
a monomorphism `Injective.ι : X ⟶ Injective.under X`.
 -/
CategoryTheory.Injective.under : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.EnoughInjectives C] → C → C
-- Init.Data.List.Lemmas
List.elem_cons_self : ∀ {α : Type u_1} {as : List α} [inst : BEq α] [LawfulBEq α] {a : α}, List.elem a (a :: as) = true
-- Mathlib.Topology.Algebra.Ring.Basic
/-- If a subring of a topological ring is commutative, then so is its topological closure.

See note [reducible non-instances].  -/
Subring.commRingTopologicalClosure : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : Ring R] →
      [inst_2 : IsSemitopologicalRing R] →
        [T2Space R] → (s : Subring R) → (∀ (x y : ↥s), x * y = y * x) → CommRing ↥s.topologicalClosure
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- Given a functor `F : I ⥤ C`, a cocone `c` on `F ⋙ yoneda : I ⥤ Cᵒᵖ ⥤ Type v₁` induces a
functor `I ⥤ CostructuredArrow yoneda c.pt` which maps `i : I` to the leg
`yoneda.obj (F.obj i) ⟶ c.pt`. If `c` is a colimit cocone, then that functor is
final.

Proposition 2.6.3(ii) in [Kashiwara2006]  -/
CategoryTheory.Presheaf.final_toCostructuredArrow_comp_pre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.SmallCategory I]
  (F : CategoryTheory.Functor I C) {c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)}
  (hc : CategoryTheory.Limits.IsColimit c),
  (c.toCostructuredArrow.comp (CategoryTheory.CostructuredArrow.pre F CategoryTheory.yoneda c.pt)).Final
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.findSome?_eq_findSomeM? : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.IteratorLoop α m m] {it : Std.IterM m β} {f : β → Option γ},
  it.findSome? f = it.findSomeM? fun x => pure (f x)
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.id_toPrelaxFunctor : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B],
  (CategoryTheory.LaxFunctor.id B).toPrelaxFunctor = CategoryTheory.PrelaxFunctor.id B
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `(F ⋙ G, S) ⥤ (G, S)`.  -/
CategoryTheory.CostructuredArrow.pre : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {B : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} B] →
            (F : CategoryTheory.Functor B C) →
              (G : CategoryTheory.Functor C D) →
                (S : D) →
                  CategoryTheory.Functor (CategoryTheory.CostructuredArrow (F.comp G) S)
                    (CategoryTheory.CostructuredArrow G S)
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNat' : ∀ {n : ℕ}, (UInt8.ofNat n).toNat = n % 2 ^ 8
-- Init.Data.Array.Extract
Array.popWhile_append_of_pos : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α},
  (∀ a ∈ ys, p a = true) → Array.popWhile p (xs ++ ys) = Array.popWhile p xs
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- Consider using `congr(f $h)` instead.  -/
GradedAlgHom.congr_arg : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] (f : 𝒜 →ₐᵍ[R] ℬ)
  {x y : A}, x = y → f x = f y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_sub_const_iff : ∀ {α : Type u} {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [ContinuousSub G] (b : G) {c : G}
  {f : α → G} {l : Filter α}, Filter.Tendsto (fun x => f x - b) l (nhds (c - b)) ↔ Filter.Tendsto f l (nhds c)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.zero_comp : ∀ {E : Type u_3} {F : Type u_4} [inst : Group E] [inst_1 : Group F] (f : F →* E), GroupSeminorm.comp 0 f = 0
-- Mathlib.MeasureTheory.MeasurableSpace.Pi
MeasurableSpace.pi_eq_generateFrom_projections : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)},
  MeasurableSpace.pi = MeasurableSpace.generateFrom {B | ∃ i A, MeasurableSet A ∧ Function.eval i ⁻¹' A = B}
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.instAddRightReflectLT : AddRightReflectLT Ordinal.{u}
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.instIsIsoε : ∀ {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) [inst_4 : F.Monoidal], CategoryTheory.IsIso (CategoryTheory.Functor.LaxMonoidal.ε F)
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.fdecl.inj : ∀ {f : Lean.IR.FunId} {xs : Array Lean.IR.Param} {type : Lean.IR.IRType} {body : Lean.IR.FnBody}
  {info : Lean.IR.DeclInfo} {f_1 : Lean.IR.FunId} {xs_1 : Array Lean.IR.Param} {type_1 : Lean.IR.IRType}
  {body_1 : Lean.IR.FnBody} {info_1 : Lean.IR.DeclInfo},
  Lean.IR.Decl.fdecl f xs type body info = Lean.IR.Decl.fdecl f_1 xs_1 type_1 body_1 info_1 →
    f = f_1 ∧ xs = xs_1 ∧ type = type_1 ∧ body = body_1 ∧ info = info_1
-- Init.Prelude
instInhabitedReaderT : (ρ : Type u) → (m : Type u → Type v) → (α : Type u) → [Inhabited (m α)] → Inhabited (ReaderT ρ m α)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WOppSide.congr_simp : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s s_1 : AffineSubspace R P),
  s = s_1 → ∀ (x x_1 : P), x = x_1 → ∀ (y y_1 : P), y = y_1 → s.WOppSide x y = s_1.WOppSide x_1 y_1
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.basisFun_toBasis : ∀ (ι : Type u_1) (𝕜 : Type u_3) [inst : RCLike 𝕜] [inst_1 : Fintype ι],
  (EuclideanSpace.basisFun ι 𝕜).toBasis = PiLp.basisFun 2 𝕜 ι
-- Mathlib.Analysis.ODE.Gronwall
/-- If `f` and `g` are two approximate solutions of the same ODE, then the distance between them
can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some
people call this Grönwall's inequality too.

This version assumes all inequalities to be true in the whole space.  -/
dist_le_of_approx_trajectories_ODE : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal}
  {f g f' g' : ℝ → E} {a b εf εg δ : ℝ},
  (∀ (t : ℝ), LipschitzWith K (v t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (f' t) (Set.Ici t) t) →
        (∀ t ∈ Set.Ico a b, dist (f' t) (v t (f t)) ≤ εf) →
          ContinuousOn g (Set.Icc a b) →
            (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (g' t) (Set.Ici t) t) →
              (∀ t ∈ Set.Ico a b, dist (g' t) (v t (g t)) ≤ εg) →
                dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ gronwallBound δ (↑K) (εf + εg) (t - a)
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
CategoryTheory.forget₂_comp_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {D : Type u_3} [inst_3 : CategoryTheory.Category.{v_2, u_3} D]
  {FD : outParam (D → D → Type u_4)} {CD : outParam (D → Type w)}
  [inst_4 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : CategoryTheory.HasForget₂ C D] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  (x : CategoryTheory.ToType ((CategoryTheory.forget₂ C D).obj X)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C D).map (CategoryTheory.CategoryStruct.comp f g))) x =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C D).map g))
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C D).map f)) x)
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats.mk : ℕ → ℕ → ℕ → Lean.PersistentArray.Stats