mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedMethods.default : Lean.Meta.Simp.Methods
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α} {h : (t.get? a).isSome = true}, (t.get? a).get h = t.get a ⋯
-- Lean.Meta.Tactic.Contradiction
Lean.Meta.Contradiction.Config.mk.injEq : ∀ (useDecide emptyType : Bool) (searchFuel : ℕ) (genDiseq useDecide_1 emptyType_1 : Bool) (searchFuel_1 : ℕ)
  (genDiseq_1 : Bool),
  ({ useDecide := useDecide, emptyType := emptyType, searchFuel := searchFuel, genDiseq := genDiseq } =
      { useDecide := useDecide_1, emptyType := emptyType_1, searchFuel := searchFuel_1, genDiseq := genDiseq_1 }) =
    (useDecide = useDecide_1 ∧ emptyType = emptyType_1 ∧ searchFuel = searchFuel_1 ∧ genDiseq = genDiseq_1)
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
/-- Applying `IsLocalRing.ResidueField.map` to the identity ring homomorphism gives the identity
ring homomorphism.  -/
IsLocalRing.ResidueField.map_id : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R],
  IsLocalRing.ResidueField.map (RingHom.id R) = RingHom.id (IsLocalRing.ResidueField R)
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mapObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j₁ j₂ : J}
  (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂) {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂)
  (hj : j₁ ≤ j₂),
  iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (iter₂.F.map (CategoryTheory.homOfLE h₁₂))
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_iff_exists_coe : ∀ {α : Type u_1} [inst : LT α] {x y : WithZero α}, x < y ↔ ∃ b, y = ↑b ∧ x < ↑b
-- Mathlib.CategoryTheory.Limits.Cones
/-- Cones on `F : Jᵒᵖ ⥤ Cᵒᵖ` are equivalent to cocones on `F.unop : J ⥤ C`.  -/
CategoryTheory.Limits.coconeUnopOfConeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} → (CategoryTheory.Limits.Cone F)ᵒᵖ ≌ CategoryTheory.Limits.Cocone F.unop
-- Mathlib.Order.Closure
LowerAdjoint.subset_closure : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe) (s : Set β),
  s ⊆ ↑(l.toFun s)
-- Batteries.Data.String.Lemmas
String.Legacy.length_eq_of_map_eq : ∀ {a b : String} {f g : Char → Char}, String.Legacy.map f a = String.Legacy.map g b → a.length = b.length
-- Lean.Parser.Basic
Lean.Parser.decQuotDepth : Lean.Parser.Parser → Lean.Parser.Parser
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_diff_le_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ \ t₂).size ≤ t₁.size
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- The first projection `mappingCocone φ ⟶ K`.  -/
CochainComplex.mappingCocone.fst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) → [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] → CochainComplex.mappingCocone φ ⟶ K
-- Mathlib.Topology.Instances.Real.Lemmas
closure_of_rat_image_lt : ∀ {q : ℚ}, closure (Rat.cast '' {x | q < x}) = {r | ↑q ≤ r}
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod_mono_right : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (K : AddSubgroup G),
  Monotone fun t => K.prod t
-- Mathlib.CategoryTheory.IsConnected
/-- **Alias** of `CategoryTheory.zigzag_symm`. -/
CategoryTheory.zigzag_symmetric : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], Std.Symm CategoryTheory.Zigzag
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closedCell_subset_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.closedCell n j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑n)
-- Mathlib.Order.Monotone.Monovary
Monovary.dual : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β},
  Monovary f g → Monovary (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g)
-- Lean.Elab.Tactic.Induction
/-- Return the variables in the first LHS of the given alternative.  -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.getAltVars : Lean.Syntax → Array Lean.Syntax
-- Mathlib.Topology.Order.Basic
tendsto_nhds_bot_mono : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace β] [inst_1 : Preorder β] [inst_2 : OrderBot β] [OrderTopology β]
  {l : Filter α} {f g : α → β}, Filter.Tendsto f l (nhds ⊥) → g ≤ᶠ[l] f → Filter.Tendsto g l (nhds ⊥)
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divLeft_apply : ∀ {G : Type u_5} [inst : Group G] (a b : G), (Equiv.divLeft a) b = a / b
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀AddMonoidHom_apply : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → AddZeroClass (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)]
  (x : (i : ι) → G i), (DirectLimit.map₀AddMonoidHom f) x = DirectLimit.map₀ f x
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- An induction principle for closure membership. If `p` holds for `1` and all elements of `k`, and
is preserved under multiplication and inverse, then `p` holds for all elements of the closure
of `k`.

See also `Subgroup.closure_induction_left` and `Subgroup.closure_induction_right` for versions that
only require showing `p` is preserved by multiplication by elements in `k`.  -/
Subgroup.closure_induction : ∀ {G : Type u_1} [inst : Group G] {k : Set G} {p : (g : G) → g ∈ Subgroup.closure k → Prop},
  (∀ (x : G) (hx : x ∈ k), p x ⋯) →
    p 1 ⋯ →
      (∀ (x y : G) (hx : x ∈ Subgroup.closure k) (hy : y ∈ Subgroup.closure k), p x hx → p y hy → p (x * y) ⋯) →
        (∀ (x : G) (hx : x ∈ Subgroup.closure k), p x hx → p x⁻¹ ⋯) → ∀ {x : G} (hx : x ∈ Subgroup.closure k), p x hx
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the largest element that is less than or equal to the
given element, returning `none` if no such element exists.
 -/
Std.ExtTreeSet.getLE? : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Option α
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α →CO β) (f' : α → β)
  (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Homology.Homotopy
/-- Tautological construction of the `Homotopy` to zero for maps constructed by
`nullHomotopicMap`, at least when we have the `zero` condition.  -/
Homotopy.nullHomotopy : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            (hom : (i j : ι) → C.X i ⟶ D.X j) →
              (∀ (i j : ι), ¬c.Rel j i → hom i j = 0) → Homotopy (Homotopy.nullHomotopicMap hom) 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extensions_app : ∀ {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) (x : Cᵒᵖ),
  c.extensions.app x =
    TypeCat.ofHom fun f => CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f.down) c.π
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finprod_mem_mul_diff` that requires `t ∩ mulSupport f` rather than
`t` to be finite.  -/
finprod_mem_mul_sdiff' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  s ⊆ t →
    (t ∩ Function.mulSupport f).Finite →
      (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Tactic.ITauto
/-- A variant on `Proof.orElim'` that performs opportunistic simplification.  -/
Mathlib.Tactic.ITauto.Proof.orElim : Mathlib.Tactic.ITauto.Proof →
  Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.Logic.Function.Basic
Function.bijective_iff_has_inverse : ∀ {α : Sort u} {β : Sort v} {f : α → β},
  Function.Bijective f ↔ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.toList_filterMapWithPostcondition_filterMapWithPostcondition.match_1.splitter : {γ : Type u_1} →
  (motive : Option γ → Sort u_2) →
    (__do_lift : Option γ) → (Unit → motive none) → ((fb : γ) → motive (some fb)) → motive __do_lift
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.IsFredholm.closedComplemented_ker : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F}, u.IsFredholm → (↑u).ker.ClosedComplemented
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
/-- The invariant vector field associated to the value at the identity of the Lie bracket of
two invariant vector fields, is everywhere the Lie bracket of the invariant vector fields.  -/
mulInvariantVector_mlieBracket : ∀ {𝕜 : 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 : Group G] [LieGroup I (minSmoothness 𝕜 3) G]
  [CompleteSpace E] (v w : GroupLieAlgebra I G),
  mulInvariantVectorField (VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) =
    VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
instCoeTCOrderMonoidWithZeroHomOfOrderHomClassOfMonoidWithZeroHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : MulZeroOneClass α] →
            [inst_3 : MulZeroOneClass β] →
              [inst_4 : FunLike F α β] → [OrderHomClass F α β] → [MonoidWithZeroHomClass F α β] → CoeTC F (α →*₀o β)
-- Lean.Widget.TaggedText
/-- Remove tags, leaving just the pretty-printed string.  -/
Lean.Widget.TaggedText.stripTags : {α : Type u_1} → Lean.Widget.TaggedText α → String
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.fvar.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId fvarId_1 : Lean.FVarId},
  Lean.Compiler.LCNF.Arg.fvar fvarId = Lean.Compiler.LCNF.Arg.fvar fvarId_1 → fvarId = fvarId_1
-- Batteries.Data.Fin.Fold
Fin.dfoldl_zero : ∀ {α : Fin (0 + 1) → Type u_1} (f : (i : Fin 0) → α i.castSucc → α i.succ) (x : α 0), Fin.dfoldl 0 α f x = x
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.types_tensorUnit_def : CategoryTheory.MonoidalCategoryStruct.tensorUnit (Type u) = PUnit.{u + 1}
-- Lean.Data.Position
Lean.instInhabitedFileMap.default : Lean.FileMap
-- Mathlib.SetTheory.ZFC.Basic
/-- The ZFC universe of sets consists of the type of pre-sets,
quotiented by extensional equivalence.  -/
ZFSet : Type (u + 1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
instMulActionSubtypeMemSubgroupStabilizerSetElem.eq_1 : ∀ (G : Type u_1) [inst : Group G] (α : Type u_2) [inst_1 : MulAction G α] (s : Set α),
  instMulActionSubtypeMemSubgroupStabilizerSetElem G α s =
    { toSMul := SMul.ofStabilizer G α s, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- The submonoid of non-zero-divisors of a `MonoidWithZero` `M₀`.  -/
nonZeroDivisors : (M₀ : Type u_1) → [inst : MonoidWithZero M₀] → Submonoid M₀
-- Mathlib.Order.Interval.Set.Disjoint
Set.Ioi_disjoint_Iio_iff : ∀ {α : Type v} [inst : Preorder α] {a b : α} [DenselyOrdered α], Disjoint (Set.Ioi a) (Set.Iio b) ↔ ¬a < b
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.left.injEq : ∀ {J : CategoryTheory.Limits.MultispanShape} (a a_1 : J.L),
  (CategoryTheory.Limits.WalkingMultispan.left a = CategoryTheory.Limits.WalkingMultispan.left a_1) = (a = a_1)
-- Init.GetElem
getElem?_eq_some_getElem_iff : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)] (h : dom c i), c[i]? = some c[i] ↔ True
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `upperHemicontinuous_iff_frequently`. -/
UpperHemicontinuous.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  UpperHemicontinuous f →
    ∀ (x : α) (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
-- Init.Data.Vector.Monadic
/-- We can express a for loop over a vector as a fold,
in which whenever we reach `.done b` we keep that value through the rest of the fold.
 -/
Vector.forIn'_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  (f : (a : α) → a ∈ xs → β → m (ForInStep β)) (init : β),
  forIn' xs init f =
    ForInStep.value <$>
      Vector.foldlM
        (fun b x =>
          match x with
          | ⟨a, m_1⟩ =>
            match b with
            | ForInStep.yield b => f a m_1 b
            | ForInStep.done b => pure (ForInStep.done b))
        (ForInStep.yield init) xs.attach
-- Mathlib.MeasureTheory.Measure.AEMeasurable
_private.Mathlib.MeasureTheory.Measure.AEMeasurable.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.lift_cof_iSup_add_one : ∀ {β : Type v} [inst : LinearOrder β] [Small.{u, v} β] {f : β → Ordinal.{u}},
  StrictMono f → Cardinal.lift.{v, u} (⨆ i, f i + 1).cof = Cardinal.lift.{u, v} (Order.cof β)
-- Mathlib.InformationTheory.Hamming
Hamming.ofHamming_smul : ∀ {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → SMul α (β i)] {r : α} {x : Hamming β},
  Hamming.ofHamming (r • x) = r • Hamming.ofHamming x
-- Init.Data.Array.Lemmas
Array.findFinIdx?_toList : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α},
  List.findFinIdx? p xs.toList = Option.map (Fin.cast ⋯) (Array.findFinIdx? p xs)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonNatTrans.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (f : F ⟶ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal f],
  CategoryTheory.Functor.mapAddMonNatTrans f =
    { app := fun X => CategoryTheory.AddMon.Hom.mk' (f.app X.X) ⋯ ⋯, naturality := ⋯ }
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toArray.go.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] (it : Std.IterM m β)
  (acc : Array β),
  Std.IterM.toArray.go it acc =
    WellFounded.extrinsicFix₂ (InvImage Std.IterM.TerminationMeasures.Finite.Rel fun x => x.fst.finitelyManySteps!)
      (fun it acc recur => do
        let __do_lift ← it.step
        match __do_lift.inflate with
          | ⟨Std.IterStep.yield it' out, h⟩ => recur it' (acc.push out) ⋯
          | ⟨Std.IterStep.skip it', h⟩ => recur it' acc ⋯
          | ⟨Std.IterStep.done, property⟩ => pure acc)
      it acc
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α}, s.Nonempty → ∀ {n : ℕ}, (s ^ n).Nonempty
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.mult.eq_1 : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K), w.mult = if w.IsReal then 1 else 2
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A natural transformation to a representable functor induces a sieve. This is the left inverse of
`functorInclusion`, shown in `sieveOfSubfunctor_functorInclusion`.
 -/
CategoryTheory.Sieve.sieveOfSubfunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → {R : CategoryTheory.Functor Cᵒᵖ (Type v₁)} → (R ⟶ CategoryTheory.yoneda.obj X) → CategoryTheory.Sieve X
-- Mathlib.Analysis.SumIntegralComparisons
/-- The partial sums of a nonnegative antitone function are bounded
by the integral over `(a, ∞)`.  -/
AntitoneOn.sum_Ico_le_integral : ∀ {f : ℝ → ℝ} {a b : ℕ},
  AntitoneOn f (Set.Icc ↑a ↑b) →
    MeasureTheory.IntegrableOn f (Set.Ioi ↑a) MeasureTheory.volume →
      (∀ t ∈ Set.Ioi ↑a, 0 ≤ f t) → ∑ n ∈ Finset.Ico a b, f ↑(n + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑a, f x
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffine.iff_of_isIso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  AlgebraicGeometry.IsAffine X ↔ AlgebraicGeometry.IsAffine Y
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.normedField : (p : ℕ) → [inst : Fact (Nat.Prime p)] → NormedField ℚ_[p]
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- One line is contained in another differing in the second point if the second point of the
first line is contained in the second line.  -/
affineSpan_pair_le_of_right_mem : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p₁ p₂ p₃ : P}, p₁ ∈ line[k, p₂, p₃] → line[k, p₂, p₁] ≤ line[k, p₂, p₃]
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- Also see `Module.finrank_top_le_finrank_of_isScalarTower_of_free`
for a version with different typeclass constraints.  -/
Module.finrank_top_le_finrank_of_isScalarTower : ∀ (R : Type u) (S : Type u_1) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [StrongRankCondition R] [Module.Finite R M] [inst_5 : Semiring S] [inst_6 : Module S M] [inst_7 : Module R S]
  [IsScalarTower R S S] [FaithfulSMul R S] [IsScalarTower R S M], Module.finrank S M ≤ Module.finrank R M
-- Mathlib.Order.ULift
ULift.instLawfulBEqOrd_mathlib : ∀ {α : Type u} [inst : BEq α] [inst_1 : Ord α] [inst_2 : Std.LawfulBEqOrd α], Std.LawfulBEqOrd (ULift.{v, u} α)
-- Mathlib.Data.Set.Prod
Set.snd_image_prod_subset : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), Prod.snd '' s ×ˢ t ⊆ t
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_apply_coe : ∀ {M : Type v} [inst : Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u))
  (a : CategoryTheory.Limits.limit J),
  ↑((CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints J) a) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π J (CategoryTheory.SingleObj.star M))) a
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
/-- Let `it` be an iterator and `f` a function mapping `it`'s outputs to iterators.
Then `it.flatMap f` is an iterator that goes over `it` and for each output, it applies `f` and
iterates over the resulting iterator. `it.flatMap f` emits all values obtained from the inner
iterators -- first, all of the first inner iterator, then all of the second one, and so on.

**Marble diagram:**

```text
it                 ---a      --b      c    --d -⊥
f a                    a1-a2⊥
f b                             b1-b2⊥
f c                                    c1-c2⊥
f d                                           ⊥
it.flatMap         ----a1-a2----b1-b2--c1-c2----⊥
```

**Termination properties:**

* `Finite` instance: only if `it` and the inner iterators are finite
* `Productive` instance: only if `it` is finite and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
iterator is productive and the inner
iterators are productive *and provably never empty*, then the resulting iterator is also productive.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.

For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
Std.IterM.flatMap : {α β α₂ γ : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [Std.Iterator α m β] → [Std.Iterator α₂ m γ] → (f : β → Std.IterM m γ) → Std.IterM m β → Std.IterM m γ
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.inseparable_iff_of_le_nhds : ∀ {α : Type u} [inst : UniformSpace α] {f g : CauchyFilter α} {a b : α},
  ↑f ≤ nhds a → ↑g ≤ nhds b → (Inseparable a b ↔ Inseparable f g)
-- Mathlib.Topology.Algebra.Group.Torsor
instIsTopologicalAddTorsorForall : ∀ {ι : Type u_1} {V : ι → Type u_2} {P : ι → Type u_3} [inst : (i : ι) → AddCommGroup (V i)]
  [inst_1 : (i : ι) → TopologicalSpace (V i)] [inst_2 : (i : ι) → AddTorsor (V i) (P i)]
  [inst_3 : (i : ι) → TopologicalSpace (P i)] [∀ (i : ι), IsTopologicalAddTorsor (P i)],
  IsTopologicalAddTorsor ((i : ι) → P i)
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.curryingIso_hom_toFunctor_map_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  {X Y : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : X ⟶ Y) (X_1 : C × D),
  (CategoryTheory.curryingIso.hom.toFunctor.map T).app X_1 = (T.app X_1.1).app X_1.2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.unitOfArray_eq_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (a : Array α),
  Std.HashMap.Raw.unitOfArray a = Std.HashMap.Raw.unitOfList a.toList
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.union_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ ∪ t₃).Equiv (t₂ ∪ t₃)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates limits of shape `Jᵒᵖ`, then `F : C ⥤ D` creates colimits
of shape `J`.  -/
CategoryTheory.Limits.createsColimitsOfShapeOfOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor C D) →
              [CategoryTheory.CreatesLimitsOfShape Jᵒᵖ F.op] → CategoryTheory.CreatesColimitsOfShape J F
-- Lean.Meta.Tactic.Simp.Diagnostics
_private.Lean.Meta.Tactic.Simp.Diagnostics.0.Lean.Meta.Simp.originToKey : Lean.Meta.Origin → Lean.MetaM Lean.MessageData
-- Mathlib.Order.Interval.Set.Monotone
Antitone.Ioc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f g : α → β},
  Antitone f → Monotone g → Monotone fun x => Set.Ioc (f x) (g x)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
isStrictlyPositive_add : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a b : A},
  IsStrictlyPositive a ∧ 0 ≤ b ∨ 0 ≤ a ∧ IsStrictlyPositive b → IsStrictlyPositive (a + b)