mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep_of_iIndep_of_le : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {m₁ m₂ : ι → MeasurableSpace Ω},
  ProbabilityTheory.iIndep m₂ μ → (∀ (i : ι), m₁ i ≤ m₂ i) → ProbabilityTheory.iIndep m₁ μ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.insertMany m l) k' = some v
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.rid_symm_comp : ∀ {R : Type u_1} {M : Type u_3} {M' : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  ↑(TensorProduct.rid R M').symm ∘ₗ f = TensorProduct.map f LinearMap.id ∘ₗ ↑(TensorProduct.rid R M).symm
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_toBitVec : ∀ (a : UInt32), { toBitVec := a.toBitVec } = a
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyCoflat.of_isLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint], CategoryTheory.RepresentablyCoflat F
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Cfg.mk.sizeOf_spec : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] [inst_1 : SizeOf Γ] [inst_2 : SizeOf Λ]
  [inst_3 : SizeOf σ] (l : Option Λ) (var : σ) (Tape : Turing.Tape Γ),
  sizeOf { l := l, var := var, Tape := Tape } = 1 + sizeOf l + sizeOf var + sizeOf Tape
-- Mathlib.Control.Monad.Writer
/-- Adapt a monad stack, changing the type of its top-most environment.

This class is comparable to [Control.Lens.Magnify](https://hackage.haskell.org/package/lens-4.15.4/docs/Control-Lens-Zoom.html#t:Magnify),
but does not use lenses (why would it), and is derived automatically for any transformer
implementing `MonadFunctor`.
 -/
MonadWriterAdapter : outParam (Type u) → (Type u → Type v) → Type (max (u + 1) v)
-- Init.Data.Int.Gcd
Int.lcm_zero_left : ∀ (a : ℤ), Int.lcm 0 a = 0
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.iUnion : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  (∀ (i : ι), AEMeasurable f (μ.restrict (s i))) → AEMeasurable f (μ.restrict (⋃ i, s i))
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
/-- Given an inverse of `f 1`, construct the Dirichlet inverse of `f`.  -/
ArithmeticFunction.dirichletInverse : {R : Type u_1} → [inst : Ring R] → (f : ℕ → R) → Invertible (f 1) → ArithmeticFunction R
-- Std.Async.TCP
_private.Std.Async.TCP.0.Std.Async.TCP.Socket.Server.ofNative.inj : ∀ {native native_1 : Std.Internal.UV.TCP.Socket}, { native := native } = { native := native_1 } → native = native_1
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Monad.comparison_map_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) {X Y : D} (f : X ⟶ Y),
  ((CategoryTheory.Monad.comparison h).map f).f = R.map f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.slope_of_X_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  x₁ ≠ x₂ → W.slope x₁ x₂ y₁ y₂ = (y₁ - y₂) / (x₁ - x₂)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- Using `Classical.choice`, extracts an object from a `Nonempty` object property.  -/
CategoryTheory.ObjectProperty.arbitrary : {C : Type u} →
  [inst : CategoryTheory.CategoryStruct.{v, u} C] → (P : CategoryTheory.ObjectProperty C) → [P.Nonempty] → C
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_of_le_of_lt' : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [inst_4 : Zero β] [PosSMulStrictMono α β] [SMulPosMono α β],
  a₁ ≤ a₂ → b₁ < b₂ → 0 < a₂ → 0 ≤ b₁ → a₁ • b₁ < a₂ • b₂
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.comp_toFun : ∀ {X Y Z : Pointed} (f : X.Hom Y) (g : Y.Hom Z) (a : X.X), (f.comp g).toFun a = (g.toFun ∘ f.toFun) a
-- Mathlib.Algebra.Star.Unitary
/-- For unitary `U` in a star-monoid `R`, `U * x = U * y` if and only if `x = y`
for all `x` and `y` in `R`.  -/
Unitary.mul_right_inj : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {x y : R} (U : ↥(unitary R)), ↑U * x = ↑U * y ↔ x = y
-- Mathlib.Data.WSeq.Productive
Stream'.WSeq.head_terminates : ∀ {α : Type u} (s : Stream'.WSeq α) [s.Productive], s.head.Terminates
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.mk.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (τl τl_1 : α.l ⟶ β.l) (e_τl : τl = τl_1) (τr τr_1 : β.r ⟶ α.r) (e_τr : τr = τr_1)
  (conjugateEquiv_τl : (CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) τl = τr),
  { τl := τl, τr := τr, conjugateEquiv_τl := conjugateEquiv_τl } = { τl := τl_1, τr := τr_1, conjugateEquiv_τl := ⋯ }
-- Mathlib.GroupTheory.Congruence.Defs
Con.hasInv.eq_1 : ∀ {M : Type u_1} [inst : Group M] (c : Con M), c.hasInv = { inv := Quotient.map' Inv.inv ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v).minKey? = some (t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k')
-- Mathlib.CategoryTheory.Monoidal.Tor
CategoryTheory.Tor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.HasProjectiveResolutions C] (n : ℕ) (X : C),
  (CategoryTheory.Tor C n).obj X = ((CategoryTheory.MonoidalCategory.tensoringLeft C).obj X).leftDerived n
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.add_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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 g : M →ₛₗ[σ₁₂] M₂) (x : M), (f + g) x = f x + g x
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.eq_top_iff' : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H = ⊤ ↔ ∀ (x : G), x ∈ H
-- Lean.Server.Rpc.Basic
Lean.Server.instRpcEncodableProd : {α β : Type} → [Lean.Server.RpcEncodable α] → [Lean.Server.RpcEncodable β] → Lean.Server.RpcEncodable (α × β)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.equivOfAlgebraic'.congr_simp : ∀ (R : Type u) (S : Type u_3) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field L]
  [inst_3 : Field M] [inst_4 : Algebra R M] [inst_5 : Module.IsTorsionFree R M] [inst_6 : IsAlgClosure R M]
  [inst_7 : Algebra S L] [inst_8 : Module.IsTorsionFree S L] [inst_9 : IsAlgClosure S L] [inst_10 : Algebra R S]
  [inst_11 : Algebra R L] [inst_12 : IsScalarTower R S L] [inst_13 : IsDomain R] [inst_14 : IsDomain S]
  [inst_15 : Module.IsTorsionFree R S] [inst_16 : Algebra.IsAlgebraic R L],
  IsAlgClosure.equivOfAlgebraic' R S L M = IsAlgClosure.equivOfAlgebraic' R S L M
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_ric_eq_self : ∀ {n i : ℕ}, i ≤ n → (*...=n).toList[i]! = i
-- Mathlib.Order.Filter.IndicatorFunction
Filter.mulIndicator_const_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} [inst : One β] {l : Filter α} {c : β},
  c ≠ 1 → ∀ {s t : Set α}, ((s.mulIndicator fun x => c) =ᶠ[l] t.mulIndicator fun x => c) ↔ s =ᶠ[l] t
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (m.insertMany l).getKeyD k' fallback = k
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderivWithin_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {s : Set M} {z : M} {f g : M → E'},
  MDiffAt[s] f z → MDiffAt[s] g z → UniqueMDiffAt[s] z → mfderiv[s] (f + g) z = mfderiv[s] f z + mfderiv[s] g z
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instToJsonFileSystemWatcher.toJson : Lean.Lsp.FileSystemWatcher → Lean.Json
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_eq_iff_natDegree_eq_of_pos : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, 0 < n → (p.degree = ↑n ↔ p.natDegree = n)
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionCyclesIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (j k k_1 : ι) (e_k : k = k_1)
  (hk : c.next j = k) {j' k' k'_1 : ι'} (e_k' : k' = k'_1) (hj' : e.f j = j') (hk' : e.f k = k')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j],
  K.restrictionCyclesIso e j k hk hj' hk' hk'' = K.restrictionCyclesIso e j k_1 ⋯ hj' ⋯ ⋯
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.ext_iff : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {x y : AdicCompletion I M}, x = y ↔ ∀ (n : ℕ), ↑x n = ↑y n
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.rank_s : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (self : f.Cell i), f.rank self.s = i
-- Mathlib.Data.PEquiv
PEquiv.instOrderBot : {α : Type u} → {β : Type v} → OrderBot (α ≃. β)
-- Lean.Meta.Tactic.LibrarySearch
/-- Wrapper for calling `Lean.Meta.SolveByElim.solveByElim with
appropriate arguments for library search.

If `grind` is true, `grind` will be used as a fallback discharger for subgoals
that cannot be closed by other means.
If `try?` is true, `try?` will be used as a fallback discharger (via grind internally).
 -/
Lean.Meta.LibrarySearch.solveByElim : List Lean.Expr → Bool → List Lean.MVarId → ℕ → optParam Bool false → optParam Bool false → Lean.MetaM (List Lean.MVarId)
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_emod_self_right : ∀ (a b c : ℤ), (a - b * c) % c = a % c
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.isoLimit_inv_π_assoc : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasLimit X]
  (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π X { as := j }) h
-- Mathlib.Analysis.Matrix.Spectrum
/-- A choice of an orthonormal basis of eigenvectors of a Hermitian matrix.  -/
Matrix.IsHermitian.eigenvectorBasis : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : Fintype n] →
        {A : Matrix n n 𝕜} → [DecidableEq n] → A.IsHermitian → OrthonormalBasis n 𝕜 (EuclideanSpace 𝕜 n)
-- Aesop.Search.ExpandSafePrefix
_private.Aesop.Search.ExpandSafePrefix.0.Aesop.liftSearchM : {Q : Type} → [inst : Aesop.Queue Q] → {α : Type} → Aesop.SearchM Q α → Aesop.SafeExpansionM Q α
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.mem_toLieSubalgebra_iff : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {h e f x : L}
  {t : IsSl2Triple h e f}, x ∈ IsSl2Triple.toLieSubalgebra R t ↔ ∃ c₁ c₂ c₃, x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.pairwise_primeFactors_isRelPrime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, (↑(UniqueFactorizationMonoid.primeFactors a)).Pairwise IsRelPrime
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.mem₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (self : J.OneHypercover S), self.sieve₀ ∈ J S
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a : R) (x : σ), MvPolynomial.degreeOf x (MvPolynomial.C a) = 0
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.isClopen_singleton_bot : ∀ {α : Type u_1} [inst : TopologicalSpace α], IsClopen {⊥}
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.minEntry!.eq_def : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (x : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.minEntry! x =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.minEntry!" 816 13
        "Map is empty"
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      Std.DTreeMap.Internal.Impl.Const.minEntry! l
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isoMk_inv_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left)
  (r : f.right ≅ g.right)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom)
      CategoryTheory.Arrow.isoMk._auto_1),
  (CategoryTheory.Arrow.isoMk l r h).inv.right = r.inv
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotientInfEquivSupQuotient_injective : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M),
  Function.Injective ⇑(LinearMap.quotientInfToSupQuotient p p')
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.ObjectProperty.instHasZeroMorphismsFullSubcategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] →
      (P : CategoryTheory.ObjectProperty C) → CategoryTheory.Limits.HasZeroMorphisms P.FullSubcategory
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.IsAffineMap.neg : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {f : M → N},
  Convexity.IsAffineMap R f → Convexity.IsAffineMap R (-f)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_hom : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.obj k) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.comp CategoryTheory.Limits.colim) k)
        (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k)
      (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j)
-- Mathlib.Combinatorics.SetFamily.FourFunctions
_private.Mathlib.Combinatorics.SetFamily.FourFunctions.0.four_functions_theorem_aux : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] (f₁ f₂ f₃ f₄ : Finset α → β) [ExistsAddOfLE β] [Finite α],
  0 ≤ f₁ →
    0 ≤ f₂ →
      0 ≤ f₃ →
        0 ≤ f₄ →
          (∀ (s t : Finset α), f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) →
            ∀ (𝒜 ℬ : Finset (Finset α)), (∑ s ∈ 𝒜, f₁ s) * ∑ s ∈ ℬ, f₂ s ≤ (∑ s ∈ 𝒜 ⊼ ℬ, f₃ s) * ∑ s ∈ 𝒜 ⊻ ℬ, f₄ s
-- Mathlib.Combinatorics.Quiver.Push
Quiver.Push.lift_unique : ∀ {V : Type u_1} [inst : Quiver V] {W : Type u_2} (σ : V → W) {W' : Type u_3} [inst_1 : Quiver W'] (φ : V ⥤q W')
  (τ : W → W') (h : ∀ (x : V), φ.obj x = τ (σ x)) (Φ : Quiver.Push σ ⥤q W'),
  Φ.obj = τ → Quiver.Push.of σ ⋙q Φ = φ → Φ = Quiver.Push.lift σ φ τ h
-- Mathlib.Geometry.Manifold.Algebra.SMul
instContMDiffSMulOfTopWithTopENat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : SMul G M] {n : WithTop ℕ∞}
  [ContMDiffSMul I I' ⊤ G M], ContMDiffSMul I I' n G M
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Fintype.sum_fiberwise' : ∀ {M : Type u_4} {κ : Type u_6} {ι : Type u_7} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  [inst_3 : DecidableEq κ] (g : ι → κ) (f : κ → M), ∑ j, ∑ _i, f j = ∑ i, f (g i)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff distance satisfies the triangle inequality.  -/
Metric.hausdorffEDist_triangle : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t u : Set α},
  Metric.hausdorffEDist s u ≤ Metric.hausdorffEDist s t + Metric.hausdorffEDist t u
-- Mathlib.Topology.VectorBundle.Riemannian
/-- The family of inner products on the fibers  -/
Bundle.RiemannianBundle.g : {B : Type u_4} →
  {E : B → Type u_6} →
    {inst : (b : B) → TopologicalSpace (E b)} →
      {inst_1 : (b : B) → AddCommGroup (E b)} →
        {inst_2 : (b : B) → Module ℝ (E b)} → [self : Bundle.RiemannianBundle E] → Bundle.RiemannianMetric E
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B] (F : CategoryTheory.LaxFunctor B' B) (x : B'),
  ((CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid F).mapIdIso x).hom =
    CategoryTheory.inv (F.mapId x)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.sub_isLittleO : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c₁ c₂ : ℝ}
  {g : α → F} {l : Filter α} {f₁ f₂ : α → E'},
  Asymptotics.IsBigOWith c₁ l f₁ g → f₂ =o[l] g → c₁ < c₂ → Asymptotics.IsBigOWith c₂ l (fun x => f₁ x - f₂ x) g
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.dist_le_infDist_add_diam : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x y : α},
  Bornology.IsBounded s → y ∈ s → dist x y ≤ Metric.infDist x s + Metric.diam s
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_int : ∀ (x : ℤ), ↑x = x
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.nonneg_toAddGroupCone : ∀ {T : Type u_1} [inst : Ring T] [inst_1 : PartialOrder T] [inst_2 : IsOrderedRing T],
  (RingCone.nonneg T).toAddGroupCone = AddGroupCone.nonneg T
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.W_eq_isLocal_range_sheafToPresheaf_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  (A : Type u_2) [inst_1 : CategoryTheory.Category.{v_2, u_2} A],
  J.W = CategoryTheory.ObjectProperty.isLocal fun x => x ∈ Set.range (CategoryTheory.sheafToPresheaf J A).obj
-- Mathlib.SetTheory.Ordinal.Basic
WellOrder.mk.sizeOf_spec : ∀ (α : Type u) (r : α → α → Prop) (wo : IsWellOrder α r), sizeOf { α := α, r := r, wo := wo } = 1 + sizeOf α + sizeOf wo
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- Build an isomorphism in the category `Module R` from a `LinearEquiv` between `Module`s.  -/
LinearEquiv.toModuleIso : {R : Type u} →
  [inst : Ring R] →
    {X₁ X₂ : Type v} →
      {g₁ : AddCommGroup X₁} →
        {g₂ : AddCommGroup X₂} →
          {m₁ : Module R X₁} → {m₂ : Module R X₂} → (X₁ ≃ₗ[R] X₂) → (ModuleCat.of R X₁ ≅ ModuleCat.of R X₂)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- An auxiliary lemma used twice in the proof of `WithLp.prodPseudoMetricAux` below. Not intended
for use outside this file.  -/
WithLp.prod_sup_edist_ne_top_aux : ∀ {α : Type u_2} {β : Type u_3} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (f g : WithLp ⊤ (α × β)),
  max (edist f.fst g.fst) (edist f.snd g.snd) ≠ ⊤
-- Mathlib.Analysis.Meromorphic.Basic
/-- Meromorphic functions are measurable.
 -/
Meromorphic.measurable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} [inst_3 : MeasurableSpace 𝕜] [SecondCountableTopology 𝕜] [BorelSpace 𝕜]
  [inst_6 : MeasurableSpace E] [CompleteSpace E] [BorelSpace E], Meromorphic f → Measurable f
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepFun.comp : ∀ {Ω : Type u_1} {β : Type u_3} {β' : Type u_4} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  {hm' : m' ≤ mΩ} {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {f : Ω → β} {g : Ω → β'}
  {γ : Type u_5} {γ' : Type u_6} {_mβ : MeasurableSpace β} {_mβ' : MeasurableSpace β'} {_mγ : MeasurableSpace γ}
  {_mγ' : MeasurableSpace γ'} {φ : β → γ} {ψ : β' → γ'},
  ProbabilityTheory.CondIndepFun m' hm' f g μ →
    Measurable φ → Measurable ψ → ProbabilityTheory.CondIndepFun m' hm' (φ ∘ f) (ψ ∘ g) μ