mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.Limits.isLocalRing : ∀ {J : Type u'} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CommRingCat)
  {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (j : J) [IsLocalRing ↑(F.obj j)],
  (∀ (x : ↑c.pt),
      IsUnit ((CategoryTheory.ConcreteCategory.hom (c.π.app j)) x) →
        ∀ (i : J),
          ∃ k f g,
            IsLocalHom (CommRingCat.Hom.hom (F.map f)) ∧
              (CategoryTheory.ConcreteCategory.hom (F.map f)) ((CategoryTheory.ConcreteCategory.hom (c.π.app i)) x) =
                (CategoryTheory.ConcreteCategory.hom (F.map g)) ((CategoryTheory.ConcreteCategory.hom (c.π.app j)) x)) →
    IsLocalRing ↑c.pt
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.eq_liftHomotopy_iff : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) {H : C(↑unitInterval × A, X)} {f : C(A, E)}
  (H_0 : ∀ (a : A), H (0, a) = p (f a)) (H' : ↑unitInterval × A → E),
  H' = ⇑(cov.liftHomotopy H f H_0) ↔
    (∀ (a : A), Continuous fun x => H' (x, a)) ∧ p ∘ H' = ⇑H ∧ ∀ (a : A), H' (0, a) = f a
-- Mathlib.Data.List.Dedup
List.dedup_cons_of_notMem' : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α}, a ∉ l.dedup → (a :: l).dedup = a :: l.dedup
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this property asserts the existence of the coend of `F`.  -/
CategoryTheory.Limits.HasCoend : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] → CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C) → Prop
-- Init.Data.BitVec.Lemmas
BitVec.ushiftRight_ofNat_eq : ∀ {w : ℕ} {x : BitVec w} {k : ℕ}, x >>> BitVec.ofNat w k = x >>> (k % 2 ^ w)
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a positive constant, `fun x ↦ r * f x` tends to negative infinity along a filter
if and only if `f` tends to negative infinity along the same filter.  -/
Filter.tendsto_const_mul_atBot_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → (Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.isSimplyLaced_A : ∀ (n : ℕ), (CartanMatrix.A n).IsSimplyLaced
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.Subcomplex.Pairing.IsInner.congr_simp : ∀ {X : SSet} {A : X.Subcomplex} (P P_1 : A.Pairing) (e_P : P = P_1) [inst : P.IsProper], P.IsInner = P_1.IsInner
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.integrableOn_univ : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E},
  μ.IntegrableOn f Set.univ ↔ μ.Integrable f
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.extract_gcd : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  (f : β → α), s.Nonempty → ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1
-- Mathlib.Order.WithBot
WithTop.ofDual_lt_ofDual_iff : ∀ {α : Type u_1} [inst : LT α] {x y : WithTop αᵒᵈ}, WithTop.ofDual y < WithTop.ofDual x ↔ x < y
-- Batteries.Data.AssocList
Batteries.AssocList.beq_nil_cons : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {t : Batteries.AssocList α β} [inst : BEq α] [inst_1 : BEq β],
  (Batteries.AssocList.nil == Batteries.AssocList.cons a b t) = false
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cosh.eq_1 : ∀ (z : ℂ), Complex.cosh z = (Complex.exp z + Complex.exp (-z)) / 2
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.ofHom_comp : ∀ {X Y Z : Type u} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z] (f : C(X, Y))
  (g : C(Y, Z)), TopCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom f) (TopCat.ofHom g)
-- Lean.Elab.PreDefinition.Structural.BRecOn
_private.Lean.Elab.PreDefinition.Structural.BRecOn.0.Lean.Elab.Structural.replaceRecApps : Array Lean.Elab.Structural.RecArgInfo → Lean.Elab.Structural.Positions → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.Algebra.Basic
Mathlib.Tactic.Algebra.Cache.mk : {u : Lean.Level} →
  {A : Q(Type u)} →
    {sA : Q(CommSemiring «$A»)} →
      Mathlib.Tactic.Ring.Common.Cache sA → Option Q(Field «$A») → Mathlib.Tactic.Algebra.Cache sA
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- **Alias** of `FunLike.coeAddMonoidHom`. -/
SchwartzMap.coeHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Lean.Elab.DocString
/-- Generates the wrapper for a typed Markdown renderer `decl` of type `InlineMdRendererOf X` (or
`BlockMdRendererOf X`) that unpacks the custom element from its `Dynamic`.

Returns the element type's name and the name of the generated wrapper. Errors if the type is not of
the expected form or if `X` has no `TypeName` instance.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.mkMdRendererWrapper : Lean.Name → Bool → Lean.MetaM (Lean.Name × Lean.Name)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.re_zero : ∀ {R : Type u_1} {a b : R} [inst : Zero R], QuadraticAlgebra.re 0 = 0
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] (F G : CategoryTheory.Functor C V) (c : C) (X : Cᵒᵖ) {X_1 Y : C}
  (f : X_1 ⟶ Y),
  ((((CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj X).map f =
    (CategoryTheory.ihom (F.obj (Opposite.unop X))).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.add_neg : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α), ↑a + ↑(-a) = 0
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.instAlgHomClass : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  AlgHomClass (𝒜 →ₐᵍ[R] ℬ) R A B
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.imp_eq : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (p : Lean.Grind.Linarith.Poly)
  (x y : Lean.Grind.Linarith.Var),
  Lean.Grind.Linarith.imp_eq_cert p x y = true →
    Lean.Grind.Linarith.Poly.denote' ctx p = 0 →
      Lean.Grind.Linarith.Var.denote ctx x = Lean.Grind.Linarith.Var.denote ctx y
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
CategoryTheory.EnrichedCat.leftUnitor_hom_out_app : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₁} [inst_3 : CategoryTheory.EnrichedCategory V D]
  (F : CategoryTheory.EnrichedFunctor V C D) (X : CategoryTheory.ForgetEnrichment V C),
  (CategoryTheory.EnrichedCat.leftUnitor F).hom.out.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of V (F.obj (CategoryTheory.ForgetEnrichment.to V X)))
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withTopCongr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PartialOrder α] [inst_1 : PartialOrder β]
  [inst_2 : PartialOrder γ] (e₁ : α ≃o β) (e₂ : β ≃o γ),
  (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr
-- Mathlib.Analysis.Normed.Group.Basic
mem_ball_one_iff : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E} {r : ℝ}, a ∈ Metric.ball 1 r ↔ ‖a‖ < r
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates colimits, then `F.leftOp : Cᵒᵖ ⥤ D` creates limits.  -/
CategoryTheory.Limits.createsLimitsOfSizeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F] →
            CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp
-- Init.Data.BitVec.Lemmas
BitVec.some_getElem_eq_getElem? : ∀ {w : ℕ} (l : BitVec w) (i : ℕ) (h : i < w), some l[i] = l[i]? ↔ True
-- Init.Data.Int.Gcd
Int.gcd_dvd_gcd_mul_left_left : ∀ (a b c : ℤ), a.gcd b ∣ (c * a).gcd b
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- Given a nonnegative nonarchimedean function `α → R` such that `f 0 = 0`, a function `g : β → α`
and a multiset `s : Multiset β`, we can always find `b : β`, belonging to `s` if `s` is nonempty,
such that `f (s.sum g) ≤ f (g b)` .  -/
IsNonarchimedean.multiset_image_add : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} {β : Type u_4}
  [inst_2 : AddCommMonoid α] [inst_3 : FunLike F α R] [ZeroHomClass F α R] [NonnegHomClass F α R] [Nonempty β] {f : F},
  IsNonarchimedean ⇑f → ∀ (g : β → α) (s : Multiset β), ∃ b, (s ≠ 0 → b ∈ s) ∧ f (Multiset.map g s).sum ≤ f (g b)
-- Init.Data.Option.Lemmas
Option.pfilter_some : ∀ {α : Type u_1} {x : α} {p : (a : α) → some x = some a → Bool},
  (some x).pfilter p = if p x ⋯ = true then some x else none
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.locallyConvexSpace : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E},
  LocallyConvexSpace ℝ (ContDiffMapSupportedIn E F n K)
-- Mathlib.Data.Ordmap.Ordset
Ordset.instInsert : {α : Type u_1} → [inst : Preorder α] → [Std.Total fun x1 x2 => x1 ≤ x2] → [DecidableLE α] → Insert α (Ordset α)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.toAddZeroClass.eq_1 : ∀ {M : Type u_4} [inst : AddZeroClass M] {A : Type u_5} [inst_1 : SetLike A M] [inst_2 : AddSubmonoidClass A M] (S : A),
  AddSubmonoidClass.toAddZeroClass S =
    { toZero := ZeroMemClass.zero S, toAdd := AddMemClass.add S, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- Proof follows from "The trace Cayley-Hamilton theorem" by Darij Grinberg, Section 5.3
 -/
Matrix.adjugate_mul_distrib : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A B : Matrix n n α),
  (A * B).adjugate = B.adjugate * A.adjugate
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_univ_iff : ∀ {α : Type u_1} {s : Set α}, sᶜ = Set.univ ↔ s = ∅
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.LeftHomotopy.mk : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {u v : CategoryTheory.Arrow V} →
        {f g : u ⟶ v} →
          (hom : u.right ⟶ v.left) →
            autoParam
                (CategoryTheory.Arrow.Hom.left f - CategoryTheory.Arrow.Hom.left g =
                  CategoryTheory.CategoryStruct.comp u.hom hom)
                CategoryTheory.Arrow.LeftHomotopy.comm._autoParam →
              CategoryTheory.Arrow.LeftHomotopy f g
-- Lean.Language.Lean.Types
/-- State before a command is elaborated. This is separate from `CommandParsedSnapshot` so that all
snapshots belonging to a command are grouped below a task with the command's syntax tree.
 -/
Lean.Language.Lean.CommandElaboratingSnapshot : Type
-- Mathlib.RingTheory.AdicCompletion.Algebra
/-- The canonical algebra map from adic Cauchy sequences to the adic completion.  -/
AdicCompletion.mkₐ : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → AdicCompletion.AdicCauchySequence I R →ₐ[R] AdicCompletion I R
-- Lean.Elab.Term.TermElabM
/-- Metavariable for explicit holes provided by the user (e.g., `_` and `?m`)  -/
Lean.Elab.Term.MVarErrorKind.hole : Lean.Elab.Term.MVarErrorKind
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_nsmul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : AddMonoid α]
  [inst_3 : AddMonoid β] [inst_4 : FunLike F α β] [AddMonoidHomClass F α β] (f : F) (s : Finset α) (n : ℕ),
  Finset.image (⇑f) (n • s) = n • Finset.image (⇑f) s
-- Mathlib.Analysis.Convex.Gauge
gauge_closure_zero : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], gauge (closure 0) = 0
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- The dual of a finite set is dually finitely generated.  -/
PointedCone.DualFG.dual_of_finite : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  (p : M →ₗ[R] N →ₗ[R] R) {s : Set M}, s.Finite → PointedCone.DualFG p (PointedCone.dual p s)
-- Init.Data.String.Defs
/-- The start position of `s`, as an `s.Pos`.  -/
String.startPos : (s : String) → s.Pos
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- **Alias** of `MeasureTheory.setIntegral_eq_of_subset_of_ae_sdiff_eq_zero_aux`. -/
MeasureTheory.setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  s ⊆ t →
    (∀ᵐ (x : X) ∂μ, x ∈ t \ s → f x = 0) →
      MeasureTheory.StronglyMeasurable f →
        MeasureTheory.IntegrableOn f t μ → ∫ (x : X) in t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.GroupTheory.Finiteness
Subgroup.FG.biSup : ∀ {G : Type u_3} [inst : Group G] {ι : Type u_5} {s : Set ι},
  s.Finite → ∀ (P : ι → Subgroup G), (∀ i ∈ s, (P i).FG) → (⨆ i ∈ s, P i).FG
-- Mathlib.Geometry.Polygon.Basic
/-- Embedding from affine triangles to polygons with 3 vertices.  -/
Affine.Triangle.toPolygon : {R : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring R] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module R V] → [inst_3 : AddTorsor V P] → Affine.Triangle R P ↪ Polygon P 3
-- Mathlib.Topology.Sequences
/-- In a Fréchet-Urysohn space, a point belongs to the closure of a set iff it is a limit
of a sequence taking values in this set.  -/
mem_closure_iff_seq_limit : ∀ {X : Type u_1} [inst : TopologicalSpace X] [FrechetUrysohnSpace X] {s : Set X} {a : X},
  a ∈ closure s ↔ ∃ x, (∀ (n : ℕ), x n ∈ s) ∧ Filter.Tendsto x Filter.atTop (nhds a)
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.coe_prodMap : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N'), ⇑(f.prodMap g) = Prod.map ⇑f ⇑g
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- Euclidean Hausdorff measure `μHE[d]`, defined as `μH[d]` scaled to agree with Lebesgue measure
on a `d`-dimensional Euclidean space. While this is defined on any (e)metric space, it is intended
to be used for affine space associated with an inner product space, where it agrees with the volume
measure on the inner product space.
 -/
MeasureTheory.Measure.euclideanHausdorffMeasure : {X : Type u_1} → [inst : EMetricSpace X] → [inst_1 : MeasurableSpace X] → [BorelSpace X] → ℕ → MeasureTheory.Measure X
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, (Set.Ioc b a).Nonempty ↔ b < a
-- Mathlib.Topology.Category.TopPair
TopPair.proj₁AdjDiag_counit_app : ∀ (X : TopCat), TopPair.proj₁AdjDiag.counit.app X = CategoryTheory.CategoryStruct.id X
-- Init.Data.BEq
/-- `EquivBEq` says that the `BEq` implementation is an equivalence relation.  -/
EquivBEq : (α : Type u_1) → [BEq α] → Prop
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
addInvariantVectorField_eq_mpullback : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [LieAddGroup I (minSmoothness 𝕜 3) G]
  (g : G) (V : (g : G) → TangentSpace I g),
  addInvariantVectorField (V 0) g = VectorField.mpullback I I (fun x => -g + x) V g
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.instUniqueOfSubsingleton : {R : Type u_1} →
  {M : Type u_3} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Subsingleton M] → Unique (Submodule R M)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.sInf_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (S : Set (CategoryTheory.MorphismProperty C)) {X Y : C}
  (f : X ⟶ Y), sInf S f ↔ ∀ W ∈ S, W f
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.functorOfMonoidHom.eq_1 : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)]
  {X : Type u_1} [inst_3 : Monoid X] (f : CategoryTheory.End (IsFreeGroupoid.SpanningTree.root'✝ T) →* X),
  IsFreeGroupoid.SpanningTree.functorOfMonoidHom T f =
    { obj := fun x => (), map := fun {X_1 Y} p => f (IsFreeGroupoid.SpanningTree.loopOfHom T p), map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.representablyFlat_op_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), CategoryTheory.RepresentablyFlat F.op ↔ CategoryTheory.RepresentablyCoflat F
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverMincard_eq_zero_iff : ∀ {X : Type u_1} (T : X → X) (F : Set X) (U : SetRel X X) (n : ℕ), Dynamics.coverMincard T F U n = 0 ↔ F = ∅
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.proper.sizeOf_spec : ∀ {s : String.Slice} (needle : String.Slice) (table : Vector ℕ needle.utf8ByteSize)
  (ht : table = String.Slice.Pattern.ForwardSliceSearcher.buildTable needle) (stackPos needlePos : String.Pos.Raw)
  (hn : needlePos < needle.rawEndPos),
  sizeOf (String.Slice.Pattern.ForwardSliceSearcher.proper needle table ht stackPos needlePos hn) =
    1 + sizeOf needle + sizeOf table + sizeOf ht + sizeOf stackPos + sizeOf needlePos + sizeOf hn
-- Aesop.Frontend.Command
Aesop.Frontend.Parser.evalStatsReport? : Lean.Name → Lean.CoreM (Option Aesop.StatsReport)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
nonZeroDivisorsRight_eq_nonZeroDivisors : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀], nonZeroDivisorsRight M₀ = nonZeroDivisors M₀
-- Mathlib.Topology.Order.IntermediateValue
/-- A "continuous induction principle" for a closed interval: if a set `s` meets `[a, b]`
on a closed subset, contains `b`, and for any `a ≤ y < x ≤ b`, `x ∈ s`, the set `s ∩ [y, x)`
is not empty, then `[a, b] ⊆ s`.  -/
IsClosed.Icc_subset_of_forall_exists_lt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {a b : α}
  {s : Set α},
  IsClosed (s ∩ Set.Icc a b) →
    b ∈ s → (∀ x ∈ s ∩ Set.Ioc a b, ∀ y ∈ Set.Iio x, (s ∩ Set.Ico y x).Nonempty) → Set.Icc a b ⊆ s
-- Batteries.Data.List.Basic
/-- A list of length 1 is a chain.  -/
List.Chain.nil : ∀ {α : Type u_1} {R : α → α → Prop} {a : α}, List.Chain R a []
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.leInfCone_π_app_none : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] {A : C} (s : Set (CategoryTheory.Subobject A))
  (f : CategoryTheory.Subobject A) (k : ∀ g ∈ s, f ≤ g), (CategoryTheory.Subobject.leInfCone s f k).π.app none = f.arrow
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.arrowCongrSL_symm_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {𝕜₄ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  {H : Type u_8} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H]
  [inst_4 : NormedField 𝕜] [inst_5 : NormedField 𝕜₂] [inst_6 : NormedField 𝕜₃] [inst_7 : NormedField 𝕜₄]
  [inst_8 : Module 𝕜 E] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₃ G] [inst_11 : Module 𝕜₄ H]
  [inst_12 : TopologicalSpace E] [inst_13 : TopologicalSpace F] [inst_14 : TopologicalSpace G]
  [inst_15 : TopologicalSpace H] [inst_16 : IsTopologicalAddGroup G] [inst_17 : IsTopologicalAddGroup H]
  [inst_18 : ContinuousConstSMul 𝕜₃ G] [inst_19 : ContinuousConstSMul 𝕜₄ H] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃} {σ₃₄ : 𝕜₃ →+* 𝕜₄} {σ₄₃ : 𝕜₄ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₁₄ : 𝕜 →+* 𝕜₄}
  [inst_20 : RingHomInvPair σ₁₂ σ₂₁] [inst_21 : RingHomInvPair σ₂₁ σ₁₂] [inst_22 : RingHomInvPair σ₃₄ σ₄₃]
  [inst_23 : RingHomInvPair σ₄₃ σ₃₄] [inst_24 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄] [inst_25 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃]
  [inst_26 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_27 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_28 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_29 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [inst_30 : RingHomIsometric σ₁₂]
  [inst_31 : RingHomIsometric σ₂₁] (e₁₂ : E ≃SL[σ₁₂] F) (e₄₃ : H ≃SL[σ₄₃] G) (L : ⋯), ⋯
-- Mathlib.Order.ConditionallyCompleteLattice.Group
ciSup_add_le : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : AddGroup α]
  [AddRightMono α] {a : α} {g : ι → α} {h : α}, (∀ (i : ι), g i + h ≤ a) → iSup g + h ≤ a
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.lintegral_rnDeriv_lt_top : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ],
  ∫⁻ (x : α), μ.rnDeriv ν x ∂ν < ⊤
-- Mathlib.Algebra.Homology.Single
CochainComplex.fromSingle₀Equiv_symm_apply_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {C : CochainComplex V ℕ} {X : V} (f : X ⟶ C.X 0)
  (hf : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0), ((C.fromSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f
-- Mathlib.Topology.Path
Path.neg_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} [inst_1 : Neg X] [inst_2 : ContinuousNeg X] (γ : Path a b)
  (a_1 : ↑unitInterval), γ.neg a_1 = -γ a_1
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt.eq_1 : ∀ {α : Type u_1} (n : ℕ) (l : List α),
  List.MergeSort.Internal.splitRevAt n l = List.MergeSort.Internal.splitRevAt.go✝ l n []
-- Mathlib.MeasureTheory.Function.Holder
MeasureTheory.Lp.coeFn_lpSMul : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q r : ENNReal}
  [hpqr : p.HolderTriple q r] [inst : NormedRing 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : MulActionWithZero 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] (f : ↥(MeasureTheory.Lp 𝕜 p μ)) (g : ↥(MeasureTheory.Lp E q μ)),
  ↑↑(f • g) =ᵐ[μ] ↑↑f • ↑↑g
-- Mathlib.Control.Applicative
Applicative.map_seq_map : ∀ {F : Type u → Type v} [inst : Applicative F] [LawfulApplicative F] {α β γ σ : Type u} (f : α → β → γ) (g : σ → β)
  (x : F α) (y : F σ), f <$> x <*> g <$> y = ((fun x => x ∘ g) ∘ f) <$> x <*> y
-- Mathlib.Order.Hom.Set
/-- Taking complements as an order isomorphism to the order dual.  -/
OrderIso.compl : (α : Type u_1) → [inst : BooleanAlgebra α] → α ≃o αᵒᵈ
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.support_congr : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {f g : Equiv.Perm α},
  f.support ⊆ g.support → (∀ x ∈ g.support, f x = g x) → f = g
-- Mathlib.Algebra.EuclideanDomain.Field
Field.mod_eq : ∀ {K : Type u_1} [inst : Field K] (a b : K), a % b = a - a * b / b