mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- `m₁` is the morphism `a` of (TR 4) as presented in Stacks.  -/
CategoryTheory.Triangulated.Octahedron.m₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : X₂ ⟶ Z₁₂} →
                          {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : X₃ ⟶ Z₂₃} →
                                {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : X₃ ⟶ Z₁₃} →
                                      {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ → (Z₁₂ ⟶ Z₁₃)
-- Batteries.Data.UnionFind.Basic
/-- Auxiliary data structure for find operation  -/
Batteries.UnionFind.FindAux : ℕ → Type
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.IterM.step_drop.match_3.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        {it : Std.IterM m β} →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextEdit : Lean.FromJson Lean.Lsp.TextEdit
-- Lean.Setup
Lean.instReprImport.repr : Lean.Import → ℕ → Std.Format
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.map_fst_toList_eq_keys : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α], List.map Prod.fst (Std.DHashMap.Const.toList m) = m.keys
-- Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike
aemeasurable_of_re_im : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace α] {f : α → 𝕜}
  {μ : MeasureTheory.Measure α},
  AEMeasurable (fun x => RCLike.re (f x)) μ → AEMeasurable (fun x => RCLike.im (f x)) μ → AEMeasurable f μ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {f : β → β}, cmp (t.modify k f).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.congr_apply_of : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [inst_2 : (i : ι) → CommRing (G' i)]
  {f' : (i j : ι) → i ≤ j → G' i →+* G' j} (e : (i : ι) → G i ≃+* G' i)
  (he : ∀ (i j : ι) (h : i ≤ j), (e j).toRingHom.comp (f i j h) = (f' i j h).comp ↑(e i)) {i : ι} (g : G i),
  (Ring.DirectLimit.congr e he) ((Ring.DirectLimit.of G (fun x x_1 h => ⇑(f x x_1 h)) i) g) =
    (Ring.DirectLimit.of G' (fun x x_1 h => ⇑(f' x x_1 h)) i) ((e i) g)
-- Init.Data.Option.Lemmas
Option.isSome_of_isSome_bind : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → Option β}, (x.bind f).isSome = true → x.isSome = true
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.grpObjMkPullbackSnd_mul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [inst_2 : CategoryTheory.GrpObj (CategoryTheory.Over.mk f)],
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback g) (CategoryTheory.Over.mk f)
        (CategoryTheory.Over.mk f))
      ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.mul)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [Inhabited γ] {f : α → β → γ} {k k' : α} {fallback : γ},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.getD (Std.DTreeMap.map f t) k fallback =
      (Option.map (f k') (Std.DTreeMap.Const.get? t k)).getD fallback
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_eq_zero_of_lt_lt : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m n : ℕ),
  f.natDegree < m → g.natDegree < n → f.resultant g m n = 0
-- Init.Data.SInt.Lemmas
ISize.ofNat_int16ToNatClampNeg : ∀ (x : Int16), 0 ≤ x → ISize.ofNat x.toNatClampNeg = x.toISize
-- Mathlib.Algebra.Group.Action.Opposite
MulOpposite.instSMulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass M N αᵐᵒᵖ
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
isBoundedBilinearMap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F],
  IsBoundedBilinearMap 𝕜 fun p => p.1 p.2
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.hasCoproduct_of_hasBiproduct : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} [CategoryTheory.Limits.HasBiproduct F],
  CategoryTheory.Limits.HasCoproduct F
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.injective_codRestrict : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {S : Type u_5} [inst_2 : SetLike S N]
  [inst_3 : SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), f x ∈ s),
  Function.Injective ⇑(f.codRestrict s h) ↔ Function.Injective ⇑f
-- Std.Async.Process
/-- Returns the absolute path of the current executable.
 -/
Std.IO.Process.getExecutablePath : IO System.FilePath
-- Mathlib.Order.SymmDiff
symmDiff_left_involutive : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a : α), Function.Involutive fun x => symmDiff x a
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.reduced.sizeOf_spec : ∀ (val : Lean.Expr), sizeOf (Lean.Meta.ReduceMatcherResult.reduced val) = 1 + sizeOf val
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp (t.minKey ⋯) k).isLE = true
-- Plausible.Sampleable
Plausible.SampleableExt.proxyRepr : {α : Sort u} → [self : Plausible.SampleableExt α] → Repr (Plausible.SampleableExt.proxy α)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_pos_iff_of_nonneg : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : PartialOrder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ x ∈ s, 0 ≤ f x) → (0 < ∑ x ∈ s, f x ↔ ∃ x ∈ s, 0 < f x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert! k v t).getKey? k = some k
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.inclusionCreatesFiniteColimits : {J : Type} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.FinCategory J] → CategoryTheory.CreatesColimitsOfShape J FintypeCat.incl
-- Mathlib.Analysis.Analytic.Binomial
Complex.one_div_sub_sq_hasFPowerSeriesOnBall_zero : ∀ {z : ℂ},
  z ≠ 0 →
    HasFPowerSeriesOnBall (fun x => 1 / (z - x) ^ 2)
      (FormalMultilinearSeries.ofScalars ℂ fun n => (z ^ (n + 2))⁻¹ * (↑n + 1)) 0 ‖z‖ₑ
-- Mathlib.Algebra.Category.ModuleCat.Free
/-- In a short exact sequence `0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0`, given bases for `X₁` and `X₃`
indexed by `ι` and `ι'` respectively, we get a basis for `X₂` indexed by `ι ⊕ ι'`.  -/
ModuleCat.Basis.ofShortExact : {ι : Type u_1} →
  {ι' : Type u_2} →
    {R : Type u_3} →
      [inst : Ring R] →
        {S : CategoryTheory.ShortComplex (ModuleCat R)} →
          S.ShortExact → Module.Basis ι R ↑S.X₁ → Module.Basis ι' R ↑S.X₃ → Module.Basis (ι ⊕ ι') R ↑S.X₂
-- Mathlib.Order.Bounds.Basic
lowerBounds_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → lowerBounds (Set.Ico b a) = Set.Iic b
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.omega0_lt_ord : ∀ {a : Cardinal.{u_1}}, Ordinal.omega0 < a.ord ↔ Cardinal.aleph0 < a
-- Mathlib.GroupTheory.Coset.Basic
/-- An equivalence between any fiber of a surjective `MonoidHom` and its kernel.  -/
MonoidHom.fiberEquivKerOfSurjective : {α : Type u_1} →
  [inst : Group α] →
    {H : Type u_2} → [inst_1 : Group H] → {f : α →* H} → Function.Surjective ⇑f → (h : H) → ↑(⇑f ⁻¹' {h}) ≃ ↥f.ker
-- Init.Data.UInt.Lemmas
instAssociativeUInt16HAdd : Std.Associative fun x1 x2 => x1 + x2
-- Mathlib.Algebra.GroupWithZero.Associated
eq_of_prime_pow_eq' : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [IsCancelMulZero R] [Subsingleton Rˣ] {p₁ p₂ : R} {k₁ k₂ : ℕ},
  Prime p₁ → Prime p₂ → 0 < k₂ → p₁ ^ k₁ = p₂ ^ k₂ → p₁ = p₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.containsThenInsert_fst : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.containsThenInsert k v).1 = t.contains k
-- Init.Data.Sum.Basic
/-- `inl a` and `inl c` are related via `LiftRel r s` if `a` and `c` are related via `r`.  -/
Sum.LiftRel.inl : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {r : α → γ → Prop} {s : β → δ → Prop} {a : α} {c : γ},
  r a c → Sum.LiftRel r s (Sum.inl a) (Sum.inl c)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  v.restrict i ≤ MeasureTheory.VectorMeasure.restrict 0 i → v i ≤ 0
-- Mathlib.Order.OrdContinuous
/-- A right adjoint in a Galois connection is right-continuous in the order-theoretic sense.  -/
GaloisConnection.rightOrdContinuous : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {g : β → α},
  GaloisConnection f g → RightOrdContinuous g
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₆_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.b₆ = 4 * W.a₆
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toCone_π_app_left : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q),
  c.toCone.π.app { as := CategoryTheory.Limits.WalkingPair.left } = c.fst
-- Mathlib.RingTheory.KrullDimension.Zero
Ring.KrullDimLE.isField_of_isReduced : ∀ {R : Type u_1} [inst : CommSemiring R] [Ring.KrullDimLE 0 R] [IsReduced R] [IsLocalRing R], IsField R
-- Mathlib.Analysis.Convex.Side
Wbtw.wSameSide₁₂ : ∀ {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 : AffineSubspace R P} {x y z : P}, Wbtw R x y z → z ∈ s → s.WSameSide x y
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_eq_one : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K = 1 ↔ K ≤ H
-- Mathlib.Algebra.Field.Basic
toDual_ratCast : ∀ {K : Type u_1} [inst : RatCast K] (n : ℚ), OrderDual.toDual ↑n = ↑n
-- Mathlib.Topology.Category.TopCat.Opens
Topology.IsInducing.functor_map : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f))
  {U V : TopologicalSpace.Opens ↑X} (h : U ⟶ V), hf.functor.map h = CategoryTheory.homOfLE ⋯
-- Mathlib.CategoryTheory.Functor.EpiMono
/-- **Alias** of `CategoryTheory.Functor.PreservesMonomorphisms.of_natTrans`. -/
CategoryTheory.Functor.preservesMonomorphisms.of_natTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} [F.PreservesMonomorphisms] (f : G ⟶ F) [∀ (X : C), CategoryTheory.Mono (f.app X)],
  G.PreservesMonomorphisms
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
IsAssociatedPrime.eq_radical : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R}, I.IsPrimary → IsAssociatedPrime J (R ⧸ I) → J = I.radical
-- Init.Data.List.MapIdx
/-- Applies a monadic function to each element of the list along with the index at which that element is
found, returning the list of results. In addition to the index, the function is also provided with a
proof that the index is valid.

`List.mapIdxM` is a variant that does not provide the function with evidence that the index is
valid.
 -/
List.mapFinIdxM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → [Monad m] → (as : List α) → ((i : ℕ) → α → i < as.length → m β) → m (List β)
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.size.eq_def : ∀ {α : Type u_1} (x : RBTree.RBNode α),
  x.size =
    match x with
    | RBTree.RBNode.nil => 0
    | RBTree.RBNode.node c x v y => x.size + y.size + 1
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Set β`.  -/
Set.mulActionSet : {α : Type u_2} → {β : Type u_3} → [inst : Monoid α] → [MulAction α β] → MulAction α (Set β)
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.brecOn : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a a_1 : FreeAlgebra.Pre R X}
  (t : FreeAlgebra.Rel R X a a_1),
  (∀ (a a_2 : FreeAlgebra.Pre R X) (t : FreeAlgebra.Rel R X a a_2), FreeAlgebra.Rel.below t → motive a a_2 t) →
    motive a a_1 t
-- Init.Data.UInt.Lemmas
UInt64.neg_mul_comm : ∀ (a b : UInt64), -a * b = a * -b
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.smul_nnreal : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.InnerRegular]
  (c : NNReal), (c • μ).InnerRegular
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagram_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J),
  D.diagram.snd (i, j) = CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_associator_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d)
  {Z : self.obj a ⟶ self.obj d}
  (h_1 : self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.Bicategory.associator f g h).hom) h_1 =
    CategoryTheory.CategoryStruct.comp (self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapComp f g).hom (self.map h))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (self.map f) (self.map g) (self.map h)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (self.map f) (self.mapComp g h).inv)
            (CategoryTheory.CategoryStruct.comp (self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv h_1))))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {km : α},
  t.min? = some km → t.get? km = some km
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.atTop_eq_generate_Ici : ∀ {α : Type u_3} [inst : Preorder α], Filter.atTop = Filter.generate (Set.range Set.Ici)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.foldlM_eq_foldlM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : δ → α → m δ}
  {init : δ}, Std.ExtDTreeMap.foldlM (fun d a x => f d a) init t = List.foldlM f init t.keys
-- Mathlib.Order.Iterate
Function.antitone_iterate_of_le_id : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α}, f ≤ id → Antitone fun m => f^[m]
-- Init.Data.SInt.Bitwise
Int8.shiftLeft_xor : ∀ {a b c : Int8}, (a ^^^ b) <<< c = a <<< c ^^^ b <<< c
-- Mathlib.Data.List.SplitLengths
_private.Mathlib.Data.List.SplitLengths.0.List.splitLengths.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α × List α → Sort u_2) (x0 x1 : List α) (h_1 : (x0 x1 : List α) → motive (x0, x1)),
  (match (x0, x1) with
    | (x0, x1) => h_1 x0 x1) =
    h_1 x0 x1
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_apply : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] (f : m ≃. n)
  (i : m) (j : n), f.toMatrix i j = if j ∈ f i then 1 else 0
-- Init.Data.Int.Order
Int.sign_zero : Int.sign 0 = 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOfConeRightOp_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F.rightOp),
  (CategoryTheory.Limits.coconeOfConeRightOp c).ι = CategoryTheory.NatTrans.removeRightOp c.π
-- Mathlib.CategoryTheory.Functor.TypeValuedFlat
CategoryTheory.Functor.isCofiltered_elements : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  [CategoryTheory.Limits.HasFiniteLimits C] [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.IsCofiltered F.Elements
-- Mathlib.Analysis.Calculus.Rademacher
/-- *Rademacher's theorem*: a Lipschitz function between finite-dimensional real vector spaces is
differentiable almost everywhere.  -/
LipschitzWith.ae_differentiableAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {F : Type u_2} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] {C : NNReal} {μ : MeasureTheory.Measure E}
  [FiniteDimensional ℝ E] [FiniteDimensional ℝ F] [μ.IsAddHaarMeasure] {f : E → F},
  LipschitzWith C f → ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ f x
-- Mathlib.Algebra.Notation.Prod
Prod.instAdd : {M : Type u_8} → {N : Type u_9} → [Add M] → [Add N] → Add (M × N)
-- Mathlib.Data.Nat.Choose.Dvd
Nat.Prime.dvd_choose : ∀ {p a b : ℕ}, Nat.Prime p → a < p → b - a < p → p ≤ b → p ∣ b.choose a
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The localized category `W.Localization` that was constructed satisfies
the universal property of the localization.  -/
CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (E : Type u_3) →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} E] →
          CategoryTheory.Localization.StrictUniversalPropertyFixedTarget W.Q W E
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_eq_delete_of_subset_loops : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, X ⊆ M.loops → M.contract X = M.delete X
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instMulActionWithZero_1 : {G₀ : Type u_1} →
  {M₀ : Type u_2} →
    [inst : MonoidWithZero G₀] → [inst_1 : AddMonoid M₀] → [MulActionWithZero G₀ M₀] → MulActionWithZero G₀ M₀ᵒᵈ
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_def : ∀ (x y : ℂ), x ^ y = if x = 0 then if y = 0 then 1 else 0 else Complex.exp (Complex.log x * y)
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.ofBialgHom_symm : ∀ {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] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₐc[R] B) (g : B →ₐc[R] A) (h₁ : f.comp g = BialgHom.id R B) (h₂ : g.comp f = BialgHom.id R A),
  (BialgEquiv.ofBialgHom f g h₁ h₂).symm = BialgEquiv.ofBialgHom g f h₂ h₁
-- Mathlib.Data.Set.Finite.Lattice
/-- **Alias** of `Set.finite_sdiff_iUnion_Ioo'`. -/
Set.finite_diff_iUnion_Ioo' : ∀ {α : Type u} [inst : LinearOrder α] (s : Set α), (s \ ⋃ x, Set.Ioo ↑x.1 ↑x.2).Finite
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F], F.leftDerivedZeroIsoSelf = F.leftDerivedZeroIsoSelf
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- **Alias** of `Convexity.ConvexSpace.sConvexComb`.

---

Take a convex combination with the given probability distribution over points.  -/
Convexity.ConvexSpace.convexCombination : {R : Type u} →
  {M : Type v} →
    [inst₁ : PartialOrder R] →
      [inst₂ : Semiring R] →
        [inst₃ : IsStrictOrderedRing R] → [self : Convexity.ConvexSpace R M] → Convexity.StdSimplex R M → M
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal i)
        (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
          (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f