mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_assoc : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a)
  (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X)
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X)) h) =
    h
-- Mathlib.MeasureTheory.SetAlgebra
/-- If a family of sets is countable then so is the algebra of sets generated by it.  -/
MeasureTheory.countable_generateSetAlgebra : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, 𝒜.Countable → (MeasureTheory.generateSetAlgebra 𝒜).Countable
-- Mathlib.Order.Cover
WCovBy.image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} (f : α ↪o β),
  a ⩿ b → (Set.range ⇑f).OrdConnected → f a ⩿ f b
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_coe_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H}, ↑(f.extend I).symm = ↑f.symm ∘ ↑I.symm
-- Lean.Level
Lean.instInhabitedLMVarIdSet : Inhabited Lean.LMVarIdSet
-- Lean.Server.Rpc.Basic
/-- `RpcEncodable α` means `α` can be used as an argument or return value
in Remote Procedure Call (RPC) methods.

The following types are `RpcEncodable` by default:
- Any type with both `FromJson` and `ToJson` instances.
- Any type all of whose components
  (meaning the fields of a `structure`, or the arguments to `inductive` constructors)
  are `RpcEncodable`.
  Use `deriving RpcEncodable` to construct an instance in this case.
- Certain common containers, if containing `RpcEncodable` data (see instances below).
- Any `WithRpcRef α` where `[TypeName α]`.

Some names are reserved for internal use and must not appear
as the name of a field or constructor argument in any `RpcEncodable` type,
or as an object key in any nested JSON.
The following are currently reserved:
- `__rpcref`

It is also possible (but discouraged for non-experts)
to implement custom `RpcEncodable` instances.
These must respect the `RpcObjectStore.wireFormat`.
 -/
Lean.Server.RpcEncodable : Type → Type
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_maxKey?_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km : α} (hc : t.contains k = true), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy`.

---

Abbreviation to enable dot notation on the hypothesis `h` stating that the subobjects presheaf
is representable by some object `Ω`.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasPullbacks C] → C → Type (max (max u u v) v)
-- Std.Data.TreeMap.Raw.Basic
/-- Folds the given monadic function over the mappings in the map in ascending order.  -/
Std.TreeMap.Raw.foldlM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (δ → α → β → m δ) → δ → Std.TreeMap.Raw α β cmp → m δ
-- Mathlib.Analysis.Convex.Function
/-- Left translation preserves convexity.  -/
ConvexOn.translate_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E}
  {f : E → β}, ConvexOn 𝕜 s f → ∀ (c : E), ConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c)
-- Mathlib.Algebra.Homology.DerivedCategory.KInjective
CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  {n : ℤ}
  [inst_2 :
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
  [inst_3 : L.IsKInjective] (x : CochainComplex.HomComplex.CohomologyClass K L n),
  CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective x = x.toSmallShiftedHom
-- Mathlib.Algebra.GradedMonoid
SetLike.isHomogeneousElem_one : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Zero ι] [inst_2 : One R] (A : ι → S)
  [SetLike.GradedOne A], SetLike.IsHomogeneousElem A 1
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.sigmaFinite_stopping_time_of_le : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {ι : Type u_4} [inst : SemilatticeSup ι] [OrderBot ι]
  {μ : MeasureTheory.Measure Ω} {f : MeasureTheory.Filtration ι m} {τ : Ω → WithTop ι}
  [MeasureTheory.SigmaFiniteFiltration μ f] (hτ : MeasureTheory.IsStoppingTime f τ) {n : ι}
  (hτ_le : ∀ (ω : Ω), τ ω ≤ ↑n), MeasureTheory.SigmaFinite (μ.trim ⋯)
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_rightInverse : ∀ {n : ℕ}, Function.RightInverse ZMod.cast Int.cast
-- Mathlib.Topology.Separation.Hausdorff
T2Space.r1Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X], R1Space X
-- Aesop.Stats.Basic
Aesop.ForwardInstantiationStats.hyps : Aesop.ForwardInstantiationStats → ℕ
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instUniformSpace : {X : Type u_1} →
  {R : Type u_2} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : Zero R] → [inst_3 : UniformSpace R] → UniformSpace (ContinuousMapZero X R)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Function.Injective.hasProd_comap_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} {f : β → α} {a : α} {g : γ → β} (hg : Function.Injective g),
  (∀ x ∉ Set.range g, f x = 1) → (HasProd (f ∘ g) a (L.comap { toFun := g, inj' := hg }) ↔ HasProd f a L)
-- Mathlib.SetTheory.ZFC.PSet
PSet.toSet_empty : ∅.toSet = ∅
-- Lean.Elab.PreDefinition.WF.Rel
/-- The termination measures must not depend on the varying parameters of the function, and in
a mutual clique, they must be the same for all functions.

This ensures the preconditions for `ArgsPacker.uncurryND`.
 -/
Lean.Elab.WF.checkCodomains : Array Lean.Name →
  Lean.Elab.FixedParamPerms → Array Lean.Expr → Array ℕ → Lean.Elab.TerminationMeasures → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Testing.Plausible.Functions
/-- Create a finitely supported function from a total function by taking the default value to
zero.  -/
Plausible.TotalFunction.applyFinsupp : {α : Type u} → {β : Type v} → [DecidableEq α] → [inst : Zero β] → [DecidableEq β] → Plausible.TotalFunction α β → α →₀ β
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.coveringRadius_pos : ∀ {X : Type u_3} [inst : MetricSpace X] (self : Delone.DeloneSet X), 0 < self.coveringRadius
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.hom_ext_iff : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ] {M : Type u_5}
  [inst_9 : AddCommMonoid M] [inst_10 : Module R M] {f g : GradedTensorProduct R 𝒜 ℬ →ₗ[R] M},
  f = g ↔ f ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ) = g ∘ₗ ↑(GradedTensorProduct.of R 𝒜 ℬ)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.identEq.parenthesizer : Lean.Name → Lean.PrettyPrinter.Parenthesizer
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Option.orElse.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → (Unit → Option α) → Sort u_2) (a : α) (x : Unit → Option α)
  (h_1 : (a : α) → (x : Unit → Option α) → motive (some a) x) (h_2 : (b : Unit → Option α) → motive none b),
  (match some a, x with
    | some a, x => h_1 a x
    | none, b => h_2 b) =
    h_1 a x
-- Mathlib.Topology.Separation.Basic
instT1SpaceProd : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T1Space X] [T1Space Y],
  T1Space (X × Y)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_uncurry_index : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : Zero M] [inst_1 : AddCommMonoid N]
  (f : α →₀ β →₀ M) (g : α × β → M → N), (f.uncurry.sum fun p c => g p c) = f.sum fun a f => f.sum fun b => g (a, b)
-- Mathlib.Data.Finsupp.Order
Finsupp.sum_pos : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedCancelAddMonoid β] [AddLeftStrictMono β] {f : ι →₀ α} {g : ι → α → β},
  (∀ i ∈ f.support, 0 < g i (f i)) → f ≠ 0 → 0 < f.sum g
-- Mathlib.Tactic.LinearCombination
/-- Performs macro expansion of a linear combination expression,
using `+`/`-`/`*`/`/` on equations and values.
* `.proof eq p` means that `p` is a syntax corresponding to a proof of an equation.
  For example, if `h : a = b` then `expandLinearCombo (2 * h)` returns `.proof (c_add_pf 2 h)`
  which is a proof of `2 * a = 2 * b`.
  Similarly, `.proof le p` means that `p` is a syntax corresponding to a proof of a non-strict
  inequality, and `.proof lt p` means that `p` is a syntax corresponding to a proof of a strict
  inequality.
* `.const c` means that the input expression is not an equation but a value.
 -/
Mathlib.Tactic.LinearCombination.expandLinearCombo : Option Lean.Expr → Lean.Term → Lean.Elab.TermElabM Mathlib.Tactic.LinearCombination.Expanded
-- Init.Control.Except
instInhabitedExceptTOfMonad : {m : Type u_1 → Type u_2} → {ε α : Type u_1} → [Monad m] → [Inhabited ε] → Inhabited (ExceptT ε m α)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
Topology.IsOpenEmbedding.toOpenPartialHomeomorph_right_inv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsOpenEmbedding f) [inst_2 : Nonempty X] {x : Y},
  x ∈ Set.range f → f (↑(Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).symm x) = x
-- Init.Data.UInt.Lemmas
USize.toUInt16_neg : ∀ (a : USize), (-a).toUInt16 = -a.toUInt16
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.sq_pos : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a : R}, a ≠ 0 → 0 < a ^ 2
-- Mathlib.Algebra.Ring.Pi
/-- A family of non-unital ring homomorphisms `f a : γ →ₙ+* β a` defines a non-unital ring
homomorphism `NonUnitalRingHom.pi f : γ →+* Π a, β a` given by
`NonUnitalRingHom.pi f x b = f b x`.  -/
NonUnitalRingHom.pi : {I : Type u} →
  {f : I → Type u_1} →
    {γ : Type u_2} →
      [inst : (i : I) → NonUnitalNonAssocSemiring (f i)] →
        [inst_1 : NonUnitalNonAssocSemiring γ] → ((i : I) → γ →ₙ+* f i) → γ →ₙ+* (i : I) → f i
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β},
  m.WF →
    (m.alter k f).getKeyD k' fallback =
      if (k == k') = true then if (f m[k]?).isSome = true then k else fallback else m.getKeyD k' fallback
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesIsoX₂.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] (hg : S.g = 0), S.cyclesIsoX₂ hg = S.cyclesIsoX₂ hg
-- Mathlib.RingTheory.Finiteness.Basic
/-- A submodule that is finite as a module is finitely generated.  -/
Submodule.FG.of_finite : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  [Module.Finite R ↥N], N.FG
-- Mathlib.Algebra.Algebra.Operations
Submodule.mem_smul_iff_inv_mul_mem : ∀ {R : Type u} [inst : CommSemiring R] {S : Type u_1} [inst_1 : DivisionSemiring S] [inst_2 : Algebra R S] {x : S}
  {p : Submodule R S} {y : S}, x ≠ 0 → (y ∈ x • p ↔ x⁻¹ * y ∈ p)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.id_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B),
  (CategoryTheory.Limits.CatCospanTransform.id F G).left = CategoryTheory.Functor.id A
-- Mathlib.RingTheory.GradedAlgebra.Basic
GradedRing.coe_projZeroRingHom'_apply : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [inst_4 : CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] (a : A), ↑((GradedRing.projZeroRingHom' 𝒜) a) = (GradedRing.projZeroRingHom 𝒜) a
-- Init.GrindInstances.ToInt
Lean.Grind.instZeroISizeSintNumBits : Lean.Grind.ToInt.Zero ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
-- Mathlib.Order.Nucleus
Nucleus.coe_lt_coe : ∀ {X : Type u_1} [inst : SemilatticeInf X] {n m : Nucleus X}, ⇑m < ⇑n ↔ m < n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMapM_eq_toListRev_filterMapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n (Option γ)} {it : Std.IterM m β},
  (Std.IterM.filterMapM f it).toListRev =
    (Std.IterM.filterMapWithPostcondition (fun b => Std.Iterators.PostconditionT.attachLift (f b)) it).toListRev
-- Mathlib.Algebra.Homology.CochainComplexOpposite
/-- The homotopy between two morphisms of cochain complexes indexed by `ℤ`
which correspond to an homotopy between morphisms of cochain complexes
in the opposite category.  -/
CochainComplex.homotopyUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {f g : K ⟶ L} →
          Homotopy ((CochainComplex.opEquivalence C).functor.map f.op)
              ((CochainComplex.opEquivalence C).functor.map g.op) →
            Homotopy f g
-- Lean.DocString.Markdown
/-- Checks whether `c` needs escaping in a context that could potentially start a block. In these
contexts, potential list and blockquote markers need escaping.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.markerPrefixSpecial : Option Char → Char → Option Char → Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {fallback : β k},
  (m₁.union m₂ ⋯ ⋯).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.free.eq_1 : ∀ (R : Type u) [inst : Ring R],
  ModuleCat.free R =
    { obj := fun X => ModuleCat.of R (X →₀ R),
      map := fun {x x_1} f => ModuleCat.ofHom (Finsupp.lmapDomain R R ⇑(CategoryTheory.ConcreteCategory.hom f)),
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Data.List.Cycle
Cycle.next_prev : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : s.Nodup) (x : α) (hx : x ∈ s),
  s.next hs (s.prev hs x hx) ⋯ = x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a} {k fallback : α},
  m.WF → (Std.DHashMap.Raw.map f m).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.vlt_iff_vlt : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [ValuativeExtension A B] {a b : A},
  (algebraMap A B) a <ᵥ (algebraMap A B) b ↔ a <ᵥ b
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_map : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} {S : Type u_5} [inst : Fintype n] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] (f : R →+* S) (M : Matrix m n R) (i : m),
  (M.map ⇑f).toMvPolynomial i = (MvPolynomial.map f) (M.toMvPolynomial i)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeOpEquiv_functor_obj : ∀ {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.Cocone F)ᵒᵖ),
  CategoryTheory.Limits.coconeOpEquiv.functor.obj c = (Opposite.unop c).op
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_sInf : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] {x : M} {S : Set (ConvexCone R M)}, x ∈ sInf S ↔ ∀ C ∈ S, x ∈ C
-- Mathlib.Order.Hom.Order
OrderHom.iInf_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {ι : Sort u_3} [inst_1 : CompleteLattice β] (f : ι → α →o β)
  (x : α), (⨅ i, f i) x = ⨅ i, (f i) x
-- Mathlib.Analysis.Convex.MetricSpace
Convexity.dist_sConvexComb_left_le : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X]
  (f : Convexity.StdSimplex ℝ X) (x : X),
  dist (Convexity.sConvexComb f) x ≤ Convexity.iConvexComb f fun x_1 => dist x_1 x
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.lipschitzWith_eval : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace β] (x : α), LipschitzWith 1 fun f => UniformFun.toFun f x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr.mk.inj : ∀ {p : Lean.Grind.CommRing.Poly} {h : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof} {p_1 : Lean.Grind.CommRing.Poly}
  {h_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof},
  { p := p, h := h } = { p := p_1, h := h_1 } → p = p_1 ∧ h = h_1
-- Mathlib.RingTheory.Radical.NatInt
Int.radical_le_one_iff : ∀ {z : ℤ}, UniqueFactorizationMonoid.radical z ≤ 1 ↔ z.natAbs ≤ 1
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
IsCovariantDerivativeOn.zero : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : Set M} [VectorBundle 𝕜 F V],
  IsCovariantDerivativeOn F cov s → ∀ {x : M}, autoParam (x ∈ s) IsCovariantDerivativeOn.zero._auto_1 → cov 0 x = 0
-- Mathlib.Algebra.Homology.Homotopy
/-- Compatibility of `nullHomotopicMap` with the precomposition by a morphism
of complexes.  -/
Homotopy.comp_nullHomotopicMap : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : C ⟶ D) (hom : (i j : ι) → D.X i ⟶ E.X j),
  CategoryTheory.CategoryStruct.comp f (Homotopy.nullHomotopicMap hom) =
    Homotopy.nullHomotopicMap fun i j => CategoryTheory.CategoryStruct.comp (f.f i) (hom i j)
-- Init.Data.Order.Ord
Std.ReflCmp.ne_of_cmp_ne_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.ReflCmp cmp] {a b : α}, cmp a b ≠ Ordering.eq → a ≠ b
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
WellFounded.extrinsicFix₂.congr_simp : ∀ {α : Sort u_1} {β : α → Sort u_2} {C₂ : (a : α) → β a → Sort u_3} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  (R : (a : α) ×' β a → (a : α) ×' β a → Prop)
  (F F_1 : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b),
  F = F_1 → ∀ (a : α) (b : β a), WellFounded.extrinsicFix₂ R F a b = WellFounded.extrinsicFix₂ R F_1 a b
-- Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical
/-- Glue a family of morphisms along a `1`-hypercover for a subcanonical topology.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.glueMorphisms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [J.Subcanonical] →
        {S T : C} →
          (E : J.OneHypercover S) →
            (f : (i : E.I₀) → E.X i ⟶ T) →
              (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
                  CategoryTheory.CategoryStruct.comp (E.p₁ k) (f i) =
                    CategoryTheory.CategoryStruct.comp (E.p₂ k) (f j)) →
                (S ⟶ T)
-- Init.Data.Order.Ord
Std.TransCmp.lt_of_lt_of_isLE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.lt → (cmp b c).isLE = true → cmp a c = Ordering.lt
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- In the case where `f` is not a monomorphism but `C` has images,
we can still take the "forward map" under it, which agrees with `MonoOver.map f`.
 -/
CategoryTheory.MonoOver.exists : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [CategoryTheory.Limits.HasImages C] →
        (X ⟶ Y) → CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y)
-- Mathlib.Data.Multiset.MapFold
Multiset.map_add : ∀ {α : Type u_1} {β : Type v} (f : α → β) (s t : Multiset α),
  Multiset.map f (s + t) = Multiset.map f s + Multiset.map f t
-- Batteries.Data.List.Basic
/-- Left-biased version of `List.zip`. `zipLeft' as bs` returns the list of
pairs `(aᵢ, bᵢ)` for `aᵢ ∈ as` and `bᵢ ∈ bs`. If `bs` is shorter than `as`, the
remaining `aᵢ` are paired with `none`. Also returns the remaining `bs`.
```
zipLeft' [1, 2] ['a'] = ([(1, some 'a'), (2, none)], [])
zipLeft' [1] ['a', 'b'] = ([(1, some 'a')], ['b'])
zipLeft' = zipWithLeft' prod.mk
```
 -/
List.zipLeft' : {α : Type u_1} → {β : Type u_2} → List α → List β → List (α × Option β) × List β
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Pullback of a `0`-hypercover along a morphism. The components are `pullback (E.f i) f`.  -/
CategoryTheory.Precoverage.ZeroHypercover.pullback₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S T : C} →
        [J.IsStableUnderBaseChange] →
          (f : S ⟶ T) →
            (E : J.ZeroHypercover T) → [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) f] → J.ZeroHypercover S
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.Decidable.instBackwardPatternForallCharPropOfDecidablePred : {p : Char → Prop} → [DecidablePred p] → String.Slice.Pattern.BackwardPattern p
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- **Alias** of the forward direction of `neg_dvd`.

---

The negation of an element `a` of a semigroup with a distributive negation divides another
element `b` iff `a` divides `b`.  -/
Dvd.dvd.of_neg_left : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, -a ∣ b → a ∣ b