mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.hom_ext_iff : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F] {X : C}
  {f g : CategoryTheory.Limits.coend F ⟶ X},
  f = g ↔
    ∀ (j : J),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j) g
-- Mathlib.Data.List.Lemmas
List.mapAccumr₂.eq_3 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β → γ → γ × δ) (x : γ) (x_3 : α) (xr : List α)
  (y : β) (yr : List β),
  List.mapAccumr₂ f (x_3 :: xr) (y :: yr) x =
    ((f x_3 y (List.mapAccumr₂ f xr yr x).1).1,
      (f x_3 y (List.mapAccumr₂ f xr yr x).1).2 :: (List.mapAccumr₂ f xr yr x).2)
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.instInhabitedGoTo.default : ExistsAndEq.GoTo
-- Mathlib.CategoryTheory.Adjunction.Quadruple
CategoryTheory.Adjunction.Quadruple.op_adj₂ : ∀ {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), q.op.adj₂ = q.adj₂.op
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
/-- If each `f i`, `i ∈ s` belongs to `[0, 1]`, then their product is less than or equal to one.
See also `Finset.prod_le_one'` for the case of an ordered commutative multiplicative monoid.  -/
Finset.prod_le_one : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f : ι → R} {s : Finset ι}, (∀ i ∈ s, 0 ≤ f i) → (∀ i ∈ s, f i ≤ 1) → ∏ i ∈ s, f i ≤ 1
-- Mathlib.Algebra.Group.Defs
/-- Bundling an `Add` and `Zero` structure together without any axioms about their
compatibility. See `AddZeroClass` for the additional assumption that 0 is an identity.  -/
AddZero : Type u_2 → Type u_2
-- Mathlib.Analysis.Convex.Function
ConvexOn.le_left_of_right_le' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f →
    ∀ {x y : E},
      x ∈ s → y ∈ s → ∀ {a b : 𝕜}, 0 < a → 0 ≤ b → a + b = 1 → f y ≤ f (a • x + b • y) → f (a • x + b • y) ≤ f x
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
/-- We give this instance a name so that it can be locally disabled when defining `FqtInfty`.
Something similar might be needed after the refactor from `Valued` to `ValuativeRel`.  -/
RatFunc.valuedRatFunc : (K : Type u_1) → [inst : Field K] → Valued (RatFunc K) (WithZero (Multiplicative ℤ))
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxc.Iterator.toList_eq_toList_rxoIterator : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [Std.Rxc.IsAlwaysFinite α] [Std.Rxo.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_10 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α] {it : Std.Iter α},
  it.toList =
    {
        internalState :=
          { next := it.internalState.next, upperBound := Std.PRange.succ it.internalState.upperBound } }.toList
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_list_eq_max_mk_aleph0 : ∀ (α : Type u) [Nonempty α], Cardinal.mk (List α) = max (Cardinal.mk α) Cardinal.aleph0
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instHasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], CategoryTheory.Limits.HasZeroObject (DerivedCategory C)
-- Mathlib.Analysis.Normed.Group.Basic
/-- A translated closed ball is a closed ball.  -/
setOf_sub_mem_closedBall_eq_closedBall : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a : E} {r : ℝ},
  {x | x - a ∈ Metric.closedBall 0 r} = Metric.closedBall a r
-- Init.Data.List.Perm
List.Perm.all_eq : ∀ {α : Type u_1} {l₁ l₂ : List α} {f : α → Bool}, l₁.Perm l₂ → l₁.all f = l₂.all f
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_le : ∀ {s : String} {p : s.Pos} {h : p ≠ s.startPos}, p.prev h ≤ p
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_comp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : CommSemiring R₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} {M : Type u_7} {N : Type u_8}
  {M₂ : Type u_12} {M₃ : Type u_13} {N₂ : Type u_14} {N₃ : Type u_15} [inst_3 : AddCommMonoid M]
  [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid M₂] [inst_6 : AddCommMonoid N₂] [inst_7 : AddCommMonoid M₃]
  [inst_8 : AddCommMonoid N₃] [inst_9 : Module R M] [inst_10 : Module R N] [inst_11 : Module R₂ M₂]
  [inst_12 : Module R₂ N₂] [inst_13 : Module R₃ M₃] [inst_14 : Module R₃ N₃] [inst_15 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (f₂ : M₂ →ₛₗ[σ₂₃] M₃) (g₂ : N₂ →ₛₗ[σ₂₃] N₃) (f₁ : M →ₛₗ[σ₁₂] M₂) (g₁ : N →ₛₗ[σ₁₂] N₂),
  TensorProduct.map (f₂ ∘ₛₗ f₁) (g₂ ∘ₛₗ g₁) = TensorProduct.map f₂ g₂ ∘ₛₗ TensorProduct.map f₁ g₁
-- Mathlib.Analysis.BoundedVariation
eVariationOn_smul_le : ∀ {α : Type u_2} [inst : LinearOrder α] {F : Type u_4} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {𝕜 : Type u_6} {f : α → 𝕜} {g : α → F} [inst_3 : NormedRing 𝕜] [inst_4 : NormedAlgebra ℝ 𝕜] [inst_5 : Module 𝕜 F]
  [NormSMulClass 𝕜 F] [IsScalarTower ℝ 𝕜 F] {C D : ENNReal} {s : Set α},
  (∀ x ∈ s, ‖f x‖ₑ ≤ C) → (∀ x ∈ s, ‖g x‖ₑ ≤ D) → eVariationOn (f • g) s ≤ C * eVariationOn g s + D * eVariationOn f s
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_eq_right : ∀ {M : Type u_1} [inst : Monoid M] {a b : M}, IsUnit b → (a * b = b ↔ a = 1)
-- Mathlib.MeasureTheory.Measure.MeasuredSets
MeasureTheory.MeasuredSets.continuous_measure : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α}, Continuous fun s => μ ↑s
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (i : ℕ),
  ModuleCat.Hom.hom ((groupHomology.chainsMap f φ).f i) =
    Finsupp.mapRange.linearMap (Rep.Hom.hom φ).toLinearMap ∘ₗ Finsupp.lmapDomain (↑A) k fun x => ⇑f ∘ x
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.eval.eq_4 : ∀ (f : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.comp f k).eval = fun v => f.eval v >>= k.eval
-- Mathlib.NumberTheory.LSeries.Positivity
/-- If all values of `a : ℕ → ℂ` are nonnegative reals and `a 1`
is positive, and the L-series of `a` agrees with an entire function `f` on some open
right half-plane where it converges, then `f` is real and positive on `ℝ`.  -/
LSeries.positive_of_differentiable_of_eqOn : ∀ {a : ℕ → ℂ},
  0 ≤ a →
    0 < a 1 →
      ∀ {f : ℂ → ℂ},
        Differentiable ℂ f →
          ∀ {x : ℝ}, LSeries.abscissaOfAbsConv a ≤ ↑x → Set.EqOn f (LSeries a) {s | x < s.re} → ∀ (y : ℝ), 0 < f ↑y
-- Mathlib.Analysis.Complex.Trigonometric
Real.two_mul_cos_mul_cos : ∀ (x y : ℝ), 2 * Real.cos x * Real.cos y = Real.cos (x - y) + Real.cos (x + y)
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Helper structure in order to prove `Module.Relations.Solutions.IsPresentation`
by showing the universal property of the module defined by generators and relations.
The universal property is restricted to modules that are in `Type w'` for
an auxiliary universe `w'`. See `IsPresentationCore.isPresentation`.  -/
Module.Relations.Solution.IsPresentationCore : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] → relations.Solution M → Type (max (max (max u v) (w' + 1)) w₀)
-- Mathlib.Topology.Algebra.Monoid
continuous_multiset_sum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [ContinuousAdd M] {f : ι → X → M} (s : Multiset ι),
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => (Multiset.map (fun i => f i a) s).sum
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toHomeomorph_trans : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_5 : RingHomInvPair σ₁₃ σ₃₁] [inst_6 : RingHomInvPair σ₃₁ σ₁₃] [inst_7 : RingHomInvPair σ₂₃ σ₃₂]
  [inst_8 : RingHomInvPair σ₃₂ σ₂₃] [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_11 : SeminormedAddCommGroup E] [inst_12 : SeminormedAddCommGroup E₂] [inst_13 : SeminormedAddCommGroup E₃]
  [inst_14 : Module R E] [inst_15 : Module R₂ E₂] [inst_16 : Module R₃ E₃] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃),
  (e.trans e').toHomeomorph = e.toHomeomorph.trans e'.toHomeomorph
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- Projection on `WithLp p (α × β)` with range `β` and kernel `α`  -/
WithLp.idemSnd : {α : Type u_2} →
  {β : Type u_3} →
    [inst : SeminormedAddCommGroup α] →
      [inst_1 : SeminormedAddCommGroup β] → {p : ENNReal} → AddMonoid.End (WithLp p (α × β))
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).ι = h.ι
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.size_toOrdNode : ∀ {α : Type u_1} (b : BinaryTree α), b.toOrdNode.size = b.numNodes
-- Mathlib.Order.Circular
Set.compl_cIoo : ∀ {α : Type u_1} [inst : CircularOrder α] {a b : α}, (Set.cIoo a b)ᶜ = Set.cIcc b a
-- Mathlib.Topology.UnitInterval
unitInterval.symm_bijective : Function.Bijective unitInterval.symm
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableAt.sum_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {ι : Type u_9}
  {s : Finset ι} {t : ι → (x : B) → E x} {x₀ : B},
  (∀ i ∈ s, MDiffAt (T% t) x₀) → (MDiffAt fun x => ⟨x, ∑ i ∈ s, t i x⟩) x₀
-- Mathlib.Computability.Primrec.Basic
Primrec.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] (f : α → β),
  Primrec f = Nat.Primrec fun n => Encodable.encode (Option.map f (Encodable.decode n))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDefinitionParams.fromJson : Lean.Json → Except String Lean.Lsp.DefinitionParams
-- Std.Http.Data.URI.Basic
/-- An IPv6 address.
 -/
Std.Http.URI.Host.ipv6 : Std.Net.IPv6Addr → Std.Http.URI.Host
-- Mathlib.Topology.Compactness.LocallyCompact
IsOpen.locallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {s : Set X}, IsOpen s → LocallyCompactSpace ↑s
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- First step in Bojanić's proof of Mahler's theorem (equation (10) of [bojanic74]): rewrite
`Δ^[n + R] f 0` in a shape that makes it easy to bound `p`-adically.  -/
_private.Mathlib.NumberTheory.Padics.MahlerBasis.0.bojanic_mahler_step1 : ∀ {M : Type u_1} {G : Type u_2} [inst : AddCommMonoidWithOne M] [inst_1 : AddCommGroup G] (f : M → G) (n : ℕ) {R : ℕ},
  1 ≤ R →
    (fwdDiff 1)^[n + R] f 0 =
      -∑ j ∈ Finset.range (R - 1), R.choose (j + 1) • (fwdDiff 1)^[n + (j + 1)] f 0 +
        ∑ k ∈ Finset.range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocExtension : Type
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.toCore_toTopologicalSpace : ∀ {α : Type ua} (u : UniformSpace α), u.toCore.toTopologicalSpace = u.toTopologicalSpace
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparison_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C) {Z : D} (h : F.obj A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst (F.obj A) (F.obj B)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst A B)) h
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
/-- The left homotopy relation on morphisms of `Arrow V`.  -/
CategoryTheory.Arrow.rightHomotopic : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] → [CategoryTheory.Preadditive V] → HomRel (CategoryTheory.Arrow V)
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.free_hom_ext : ∀ {R : Type u} [inst : Ring R] {X : Type u} {M : ModuleCat R} {f g : (ModuleCat.free R).obj X ⟶ M},
  (∀ (x : X),
      (CategoryTheory.ConcreteCategory.hom f) (ModuleCat.freeMk x) =
        (CategoryTheory.ConcreteCategory.hom g) (ModuleCat.freeMk x)) →
    f = g
-- Mathlib.Order.Filter.Germ.Basic
/-- Setoid used to define the space of germs.  -/
Filter.germSetoid : {α : Type u_1} → Filter α → (β : Type u_5) → Setoid (α → β)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Mapping by the identity morphism is just the identity functor.  -/
CategoryTheory.Under.mapId_eq : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (Y : T),
  CategoryTheory.Under.map (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.Functor.id (CategoryTheory.Under Y)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from types to its "ring id". We cache failures using `none`.
`typeIdOf[type]` is `some id`, then `id < rings.size`.  -/
Lean.Meta.Grind.Arith.CommRing.State.typeIdOf : Lean.Meta.Grind.Arith.CommRing.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)
-- Std.Net.Addr
Std.Net.SocketAddress.v6.inj : ∀ {addr addr_1 : Std.Net.SocketAddressV6},
  Std.Net.SocketAddress.v6 addr = Std.Net.SocketAddress.v6 addr_1 → addr = addr_1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_ric : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.Ordered →
    ∀ (bound : α),
      Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) =
        List.filter (fun e => (compare e.1 bound).isLE) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The canonical map from `G` to its profinite completion, as a function.  -/
ProfiniteAddGrp.ProfiniteCompletion.etaFn : (G : AddGrpCat) → ↑G → ↑(ProfiniteAddGrp.ProfiniteCompletion.completion G).toProfinite.toTop
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.π_mapOfIsColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} {X' Y' : C} {f' : X' ⟶ Y'} {cc : CategoryTheory.Limits.CokernelCofork f}
  (hf : CategoryTheory.Limits.IsColimit cc) (cc' : CategoryTheory.Limits.CokernelCofork f')
  (φ : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc)
      (CategoryTheory.Limits.CokernelCofork.mapOfIsColimit hf cc' φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right φ) (CategoryTheory.Limits.Cofork.π cc')
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ {fallback : α}, t₁.minKeyD fallback = t₂.minKeyD fallback
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α} {he : t.isEmpty = false},
  (cmp k (t.min he)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Init.Data.Array.Lemmas
Array.replace_extract : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {xs : Array α} {i : ℕ},
  (xs.extract 0 i).replace a b = (xs.replace a b).extract 0 i
-- Mathlib.CategoryTheory.Comma.Basic
/-- The functor `(L, R) ⥤ (L ⋙ F, R ⋙ F)`  -/
CategoryTheory.Comma.post : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {C : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C] →
                (L : CategoryTheory.Functor A T) →
                  (R : CategoryTheory.Functor B T) →
                    (F : CategoryTheory.Functor T C) →
                      CategoryTheory.Functor (CategoryTheory.Comma L R) (CategoryTheory.Comma (L.comp F) (R.comp F))
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit.functor =
    CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.Std.Iter.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Lean.Parser.Term
/-- `wait_for_expected_type% e` elaborates `e` against its expected type, postponing while that type
is an unassigned metavariable so an `outParam` determined by instance synthesis is resolved first.  -/
Lean.Parser.Term.waitForExpectedType : Lean.Parser.Parser
-- Init.Data.Vector.Lemmas
Vector.forall_mem_flatMap : ∀ {β : Type u_1} {α : Type u_2} {n m : ℕ} {p : β → Prop} {xs : Vector α n} {f : α → Vector β m},
  (∀ x ∈ xs.flatMap f, p x) ↔ ∀ a ∈ xs, ∀ b ∈ f a, p b
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
/-- a well order continuous functor `F : J ⥤ C`  -/
CategoryTheory.TransfiniteCompositionOfShape.F : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : LinearOrder J] →
        [inst_2 : OrderBot J] →
          {X Y : C} →
            {f : X ⟶ Y} →
              [inst_3 : SuccOrder J] →
                [inst_4 : WellFoundedLT J] →
                  CategoryTheory.TransfiniteCompositionOfShape J f → CategoryTheory.Functor J C
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.coe_toMonoidWithZeroHom : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) [inst_3 : IsDomain S] [inst_4 : Nontrivial R], ⇑abv.toMonoidWithZeroHom = ⇑abv
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The inclusion map from Schwartz functions to bounded continuous functions as a continuous linear
map.  -/
SchwartzMap.toBoundedContinuousFunctionCLM : (𝕜 : Type u_2) →
  (E : Type u_5) →
    (F : Type u_6) →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : RCLike 𝕜] →
                [inst_5 : NormedSpace 𝕜 F] →
                  [inst_6 : SMulCommClass ℝ 𝕜 F] → SchwartzMap E F →L[𝕜] BoundedContinuousFunction E F
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The data of chosen ends in `C`.  -/
CategoryTheory.Limits.ChosenEnds : (C : Type u_3) →
  [CategoryTheory.Category.{v_3, u_3} C] → Type (max (max (max (max (max (max (u + 1) (v + 1)) u) u_3) v_3) u) v)
-- Init.Data.FloatArray.Basic
FloatArray.mk : Array Float → FloatArray
-- Mathlib.Logic.Equiv.PartialEquiv
/-- **Alias** of the reverse direction of `PartialEquiv.IsImage.iff_symm_preimage_eq`. -/
PartialEquiv.IsImage.of_symm_preimage_eq : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t → e.IsImage s t
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.den.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), I.den = ⟨Exists.choose ⋯, ⋯⟩
-- Batteries.Tactic.Init
/-- `exacts [e1, ..., en]` is like `exact`, using the terms `e1`, ..., `en` to close all the current
`n` goals. It raises an error if the number of goals does not match.
 -/
Batteries.Tactic.exacts : Lean.ParserDescr
-- Mathlib.RingTheory.Kaehler.Basic
/-- The (universal) derivation into `(S →₀ S) ⧸ KaehlerDifferential.kerTotal R S`.  -/
KaehlerDifferential.derivationQuotKerTotal : (R : Type u) →
  (S : Type v) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Derivation R S ((S →₀ S) ⧸ KaehlerDifferential.kerTotal R S)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.submatrix : ∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} {A : Matrix V V α} [inst : Zero α] [inst_1 : One α],
  A.IsAdjMatrix → ∀ (f : W → V), (A.submatrix f f).IsAdjMatrix
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_union_le_eRk_add_encard : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk (X ∪ Y) ≤ M.eRk X + Y.encard
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α},
  Std.ExtDTreeMap.Const.get! (t₁ \ t₂) k = if k ∈ t₂ then default else Std.ExtDTreeMap.Const.get! t₁ k
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.toList.match_1.splitter : {α : Type u_1} →
  (motive : (x : Bool) → Lists' α x → Sort u_2) →
    (x : Bool) →
      (x_1 : Lists' α x) →
        ((a : α) → motive false (Lists'.atom a)) →
          (Unit → motive true Lists'.nil) →
            ((b : Bool) → (a : Lists' α b) → (l : Lists' α true) → motive true (a.cons' l)) → motive x x_1
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coeOutAddMonoidHom : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → CoeOut (A →ₐ[R] B) (A →+ B)
-- Mathlib.Topology.Order.ScottTopology
/-- The Scott-Hausdorff topology.

A set `u` is open in the Scott-Hausdorff topology iff when the least upper bound of a directed set
`d` lies in `u` then there is a tail of `d` which is a subset of `u`.

For mild conditions on `D`, this is equivalent to saying that open sets are `DirSupInaccOn D`,
and closed sets are `DirSupClosedOn D`.  -/
Topology.scottHausdorff : (α : Type u_3) → Set (Set α) → [Preorder α] → TopologicalSpace α