mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.forIn_filter : ∀ {α : Type u₁} {n : Type u₁ → Type u_1} {γ : Type u₁} {m : Type u₁ → Type u_2} {β : Type u₁} {ps : Std.Do.PostShape}
  [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Do.WPMonad n ps]
  [inst_5 : MonadLiftT m n] [LawfulMonadLiftT m n] [inst_7 : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_9 : Std.IteratorLoop α m n] [Std.LawfulIteratorLoop α m n] {it : Std.IterM m β} {f : β → Bool} {init : γ}
  {g : β → γ → n (ForInStep γ)} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄ forIn it init fun out acc => if f out = true then g out acc else pure (ForInStep.yield acc) ⦃Q⦄ →
    ⦃P⦄ forIn (Std.IterM.filter f it) init g ⦃Q⦄
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Construct `HasBinaryProduct Y X` from `HasBinaryProduct X Y`.
This can't be an instance, as it would cause a loop in typeclass search.  -/
CategoryTheory.Limits.HasBinaryProduct.swap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X Y : C) [CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.Limits.HasBinaryProduct Y X
-- Lean.Data.Lsp.InitShutdown
/-- Lean-specific initialization options.  -/
Lean.Lsp.InitializationOptions : Type
-- Aesop.Check
Aesop.Check.rules : Aesop.Check
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instReprDiscrInfo : Repr Lean.Meta.Match.DiscrInfo
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `FunLike.coe_smul`. -/
SlashInvariantForm.coe_smulℝ : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.LieEquiv.ofCoboundary_invFun : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (c c' : ↥(LieModule.Cohomology.twoCocycle R L M)) (x : LieModule.Cohomology.oneCochain R L M)
  (h : ↑c' = ↑c + (LieModule.Cohomology.d₁₂ R L M) x) (z : LieAlgebra.ofTwoCocycle c'),
  (LieAlgebra.LieEquiv.ofCoboundary c c' x h).invFun z =
    (LieAlgebra.ofProd c)
      (((LieAlgebra.ofProd c').symm z).1, ((LieAlgebra.ofProd c').symm z).2 + x ((LieAlgebra.ofProd c').symm z).1)
-- Init.Data.List.MinMaxIdx
List.maxIdxOn_eq_of_maxIdxOn?_eq_some : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} {i : ℕ}
  (h : List.maxIdxOn? f xs = some i), List.maxIdxOn f xs ⋯ = i
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddCancelCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCancelCommMonoid α],
  OrderDual.instAddCancelCommMonoid = { toAddCommMonoid := OrderDual.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coalgebraEquivOver_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  (CategoryTheory.coalgebraEquivOver X).functor = CategoryTheory.coalgebraToOver X
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations preserve subtraction.  -/
AddCon.sub : ∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M) {w x y z : M}, c w x → c y z → c (w - y) (x - z)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.mkArg : Lean.TSyntax `doc_arg → Lean.Doc.DocM (Lean.TSyntax `Lean.Parser.Term.argument)
-- Mathlib.Order.Atoms
OrderDual.instIsStronglyCoatomic : ∀ {α : Type u_4} [inst : Preorder α] [IsStronglyAtomic α], IsStronglyCoatomic αᵒᵈ
-- Init.Grind.Config
/-- When `trace := true`, uses `sorry` to close unsolved branches.
 -/
Lean.Grind.Config.useSorry : Lean.Grind.Config → Bool
-- Mathlib.Data.Multiset.Powerset
Multiset.mem_powersetCardAux : ∀ {α : Type u_1} {n : ℕ} {l : List α} {s : Multiset α}, s ∈ Multiset.powersetCardAux n l ↔ s ≤ ↑l ∧ s.card = n
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparated_iff_quasiSeparatedSpace : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [QuasiSeparatedSpace ↥Y],
  AlgebraicGeometry.QuasiSeparated f ↔ QuasiSeparatedSpace ↥X
-- Mathlib.Order.Atoms
/-- An atom of an `OrderBot` is an element with no other element between it and `⊥`,
which is not `⊥`.  -/
IsAtom : {α : Type u_2} → [inst : Preorder α] → [OrderBot α] → α → Prop
-- Init.Meta.Defs
/-- Configures the behaviour of the `omega` tactic.  -/
Lean.Meta.Omega.OmegaConfig : Type
-- Mathlib.Algebra.Order.Hom.Basic
GroupNormClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : Group α] [inst_1 : AddCommMonoid β]
  [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [toGroupSeminormClass : GroupSeminormClass F α β],
  (∀ (f : F) {a : α}, f a = 0 → a = 1) → GroupNormClass F α β
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_inv_smul_inter : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (c⁻¹ • s ∩ t) = μ (s ∩ c • t)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.natCard_multiples_le_addOrderOf : ∀ {G : Type u_1} [inst : AddMonoid G] {a : G}, IsOfFinAddOrder a → Nat.card ↑↑(AddSubmonoid.multiples a) ≤ addOrderOf a
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instAddCommGroup : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommGroup M] →
        [inst_1 : TopologicalSpace M] → [IsTopologicalAddGroup M] → AddCommGroup (MeasureTheory.VectorMeasure α M)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.liftWith_refl : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps]
  [inst_1 : Pure m] (f : ({β : Type u} → m β → m β) → m α), ⦃(Std.Do.wp (f fun {β} x => x)).apply Q⦄ liftWith f ⦃Q⦄
-- Mathlib.CategoryTheory.Sites.PseudofunctorSheafOver
CategoryTheory.GrothendieckTopology.pseudofunctorOver_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {a b : CategoryTheory.LocallyDiscrete Cᵒᵖ} {f g : a ⟶ b} (φ : f ⟶ g),
  (J.pseudofunctorOver A).map₂ φ = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ρFunctorObj_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ρFunctorObj f πX)
      (CategoryTheory.SmallObject.πFunctorObj f πX) =
    CategoryTheory.SmallObject.π'FunctorObj f πX
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_dvd2_cert.eq_1 : ∀ (p₁ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ) (d' : ℤ) (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_left_split_dvd2_cert p₁ p₃ d k d' p' =
    (d'.beq' (p₁.leadCoeff * d)).and'
      (p'.beq'
        ((Int.Internal.Linear.Poly.combine_mul_k p₃.leadCoeff (-p₁.leadCoeff) p₁.tail p₃.tail).addConst_k
          (p₃.leadCoeff * ↑k)))
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.isFractional_of_fg : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [IsLocalization S P] {I : Submodule R P}, I.FG → IsFractional S I
-- Init.Data.UInt.Basic
/-- Unsigned division for 32-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.
 -/
UInt32.div : UInt32 → UInt32 → UInt32
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Cech
CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A]
  (E : CategoryTheory.SimplicialObject (CategoryTheory.Limits.FormalCoproduct C)) {X Y : CategoryTheory.Functor Cᵒᵖ A}
  (f : X ⟶ Y) (X_1 : SimplexCategory),
  ((CategoryTheory.Limits.FormalCoproduct.cosimplicialObjectFunctor E).map f).app X_1 =
    CategoryTheory.Limits.Pi.map fun i => f.app (Opposite.op ((E.obj (Opposite.op X_1)).obj i))
-- Lean.Meta.Tactic.NormCast
Lean.Meta.NormCast.NormCastExtension.mk.inj : ∀ {up down squash up_1 down_1 squash_1 : Lean.Meta.SimpExtension},
  { up := up, down := down, squash := squash } = { up := up_1, down := down_1, squash := squash_1 } →
    up = up_1 ∧ down = down_1 ∧ squash = squash_1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instCommMonoid.eq_1 : ∀ {A : Type u_2} {E : Type u_6} [inst : Monoid A] [inst_1 : TopologicalSpace A] [inst_2 : CommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousMul E],
  ContinuousMonoidHom.instCommMonoid =
    { mul := fun f g => (ContinuousMonoidHom.mul E).comp (f.prod g), mul_assoc := ⋯,
      toOne := ContinuousMonoidHom.instOne A E, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯,
      npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.exists_submodule_linearEquiv_quotient : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  (N : Submodule R M), ∃ P, Nonempty (↥P ≃ₗ[R] M ⧸ N)
-- Mathlib.Order.Minimal
OrderIso.image_setOfPred_maximal : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (P : α → Prop),
  ⇑f '' {x | Maximal P x} = {x | Maximal (fun x => P (f.symm x)) x}
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.updateJmpImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Code pu → Lean.FVarId → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.Code pu
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
_private.Mathlib.Combinatorics.SimpleGraph.FiveWheelLike.0.«term‖_‖» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Basic
Group.conjugatesOfSet_subset : ∀ {G : Type u_1} [inst : Group G] {s : Set G} {N : Subgroup G} [N.Normal], s ⊆ ↑N → Group.conjugatesOfSet s ⊆ ↑N
-- Mathlib.Algebra.Opposites
MulOpposite.unop_eq_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : αᵐᵒᵖ), MulOpposite.unop a = 0 ↔ a = 0
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- The cocones on the `Dᵢ`.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    {S : AlgebraicGeometry.Scheme} →
      {J : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
            {𝒰 : S.OpenCover} →
              [inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀] →
                [inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                  AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰 →
                    (i : 𝒰.I₀) →
                      CategoryTheory.Limits.Cocone (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The coefficients `b i` are less than 1.  -/
AkraBazziRecurrence.b_lt_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (self : AkraBazziRecurrence T g a b r) (i : α), b i < 1
-- Mathlib.Algebra.CubicDiscriminant
Cubic.leadingCoeff_of_b_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b ≠ 0 → P.toPoly.leadingCoeff = P.b
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.add_neg : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (s s' : ↥S),
  ↑s -ₒ s' + (↑s' -ₒ s) = 0
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.valuation_eq_one_iff : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (a : ↥A), IsUnit a ↔ A.valuation ↑a = 1
-- Init.Data.String.Slice
/-- Returns the position after the longest prefix of `s` for which `pat` matches
\(potentially repeatedly\).
 -/
String.Slice.skipPrefixWhile : {ρ : Type} → (s : String.Slice) → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → s.Pos
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_dvd_index_of_le : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H ≤ K → H.relIndex K ∣ H.index
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `FunLike.coe_sum`. -/
QuadraticMap.coeFn_sum : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F),
  ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.transHomeomorph_transHomeomorph : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace Z'] (e : OpenPartialHomeomorph X Y) (f' : Y ≃ₜ Z)
  (f'' : Z ≃ₜ Z'), (e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k a : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).get? a =
        if h : compare k a = Ordering.eq ∧ k ∉ t then some (cast ⋯ v) else t.get? a
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSubNegAddMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubNegMonoid α],
  OrderDual.instSubNegAddMonoid =
    { toAddMonoid := OrderDual.instAddMonoid, toNeg := OrderDual.instNeg, toSub := OrderDual.instSub,
      toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Mathlib.Algebra.Lie.Basic
lie_smul : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] (t : R) (x : L)
  (m : M), ⁅x, t • m⁆ = t • ⁅x, m⁆
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.denoteN.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (k : ℤ)
  (v : Lean.Grind.Linarith.Var) (p_2 : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denoteN ctx (Lean.Grind.Linarith.Poly.add k v p_2) =
    bif decide (k < 0) then 0
    else k.natAbs • Lean.Grind.Linarith.Var.denote ctx v + Lean.Grind.Linarith.Poly.denoteN ctx p_2
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Construct a cocone for a left Kan extension `F' : D ⥤ H` of `F : C ⥤ H` along a functor
`L : C ⥤ D` given a cocone for `F`.  -/
CategoryTheory.Functor.coconeOfIsLeftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : F ⟶ L.comp F') →
                    [F'.IsLeftKanExtension α] → CategoryTheory.Limits.Cocone F → CategoryTheory.Limits.Cocone F'
-- Std.Data.TreeSet.Raw.Slice
Std.TreeSet.Raw.instSliceableRocSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.Raw.instSliceableRocSlice._auto_1) →
    Std.Roc.Sliceable (Std.TreeSet.Raw α cmp) α (Std.DTreeMap.Internal.Unit.RocSlice α)
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorUnivLevelPos.majorType.sizeOf_spec : ∀ (idx : ℕ), sizeOf (Lean.Meta.RecursorUnivLevelPos.majorType idx) = 1 + sizeOf idx
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
/-- For a functor `G : C ⥤ D`, and a morphism `f : G.obj U ⟶ G.obj V`,
`Functor.imageSieve G f` is the sieve of `U`
consisting of those arrows whose composition with `f` has a lift in `G`.

This is the image sieve of `f` under `yonedaMap G V` and hence the name.
See `Functor.imageSieve_eq_imageSieve`.
 -/
CategoryTheory.Functor.imageSieve : {C : Type uC} →
  [inst : CategoryTheory.Category.{vC, uC} C] →
    {D : Type uD} →
      [inst_1 : CategoryTheory.Category.{vD, uD} D] →
        (G : CategoryTheory.Functor C D) → {U V : C} → (G.obj U ⟶ G.obj V) → CategoryTheory.Sieve U
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- Lebesgue dominated convergence theorem for filters with a countable basis  -/
MeasureTheory.VectorMeasure.tendsto_integral_filter_of_dominated_convergence : ∀ {ι : Type u_1} {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F}
  {B : E →L[ℝ] F →L[ℝ] G} {l : Filter ι} [l.IsCountablyGenerated] {F_1 : ι → X → E} {f : X → E} (bound : X → ℝ),
  (∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F_1 n) μ.variation) →
    (∀ᶠ (n : ι) in l, ∀ᵐ (a : X) ∂μ.variation, ‖F_1 n a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ.variation →
        (∀ᵐ (a : X) ∂μ.variation, Filter.Tendsto (fun n => F_1 n a) l (nhds (f a))) →
          Filter.Tendsto (fun n => ∫ᵛ (a : X), F_1 n a ∂[B; μ]) l (nhds ∫ᵛ (a : X), f a ∂[B; μ])
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal : ∀ {X : AlgebraicGeometry.Scheme} (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))) (U : ↑X.affineOpens),
  (AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop I).ideal U =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) I
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.mk'_toAddSubmonoid : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {sg : Subsemigroup R} (hg : ↑sg = s)
  {sa : AddSubmonoid R} (ha : ↑sa = s), (NonUnitalSubsemiring.mk' s sg hg sa ha).toAddSubmonoid = sa
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.IterM.step_takeWhileWithPostcondition.match_3.eq_2 : ∀ {α : 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) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it' h
-- Batteries.Recycling.MonadSatisfying.Basic
SatisfiesM_EStateM_eq : ∀ {ε σ α : Type u_1} {p : α → Prop} {x : EStateM ε σ α},
  SatisfiesM p x ↔ ∀ (s : σ) (a : α) (s' : σ), x.run s = EStateM.Result.ok a s' → p a
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.polyOfInterest_vars_eq : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  (WittVector.polyOfInterest p n).vars =
    (↑p ^ (n + 1) *
        (WittVector.wittMul p (n + 1) + ↑p ^ (n + 1) * MvPolynomial.X (0, n + 1) * MvPolynomial.X (1, n + 1) -
            MvPolynomial.X (0, n + 1) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
          MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)))).vars
-- Mathlib.Geometry.Manifold.Algebra.Monoid
L_mul : ∀ {𝕜 : 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_8}
  [inst_4 : Semigroup G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (g h : G), smoothLeftMul I (g * h) = (smoothLeftMul I g).comp (smoothLeftMul I h)
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.EStateM.run_bind.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.error e s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error e s => h_2 e s) =
    h_2 e s
-- Init.PropLemmas
and_and_right : ∀ {a b c : Prop}, (a ∧ b) ∧ c ↔ (a ∧ c) ∧ b ∧ c
-- Mathlib.Algebra.Module.Basic
Function.support_smul_subset_right : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (f : α → R) (g : α → M),
  Function.support (f • g) ⊆ Function.support g
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_sum_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E),
  ‖∑ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊
-- Mathlib.Data.Set.Lattice.Image
Set.prod_sInter : ∀ {α : Type u_1} {β : Type u_2} {T : Set (Set β)}, T.Nonempty → ∀ (s : Set α), s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- If the measure of the symmetric difference of two sets is finite,
then one has infinite measure if and only if the other one does.  -/
MeasureTheory.measure_eq_top_iff_of_symmDiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  μ (symmDiff s t) ≠ ⊤ → (μ s = ⊤ ↔ μ t = ⊤)
-- Mathlib.Topology.Category.CompHaus.Projective
/-- For any compact Hausdorff space `X`,
the natural map `Ultrafilter X → X` is a projective presentation.  -/
CompHaus.projectivePresentation : (X : CompHaus) → CategoryTheory.ProjectivePresentation X
-- Init.Omega.IntList
Lean.Omega.IntList.sdiv_cons : ∀ {x : ℤ} {xs : List ℤ} {g : ℤ}, Lean.Omega.IntList.sdiv (x :: xs) g = x / g :: Lean.Omega.IntList.sdiv xs g
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBlastExtractAndExtendTargetBlastExtractAndExtend : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.imp : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
-- Mathlib.Algebra.NoZeroSMulDivisors.Defs
/-- `NoZeroSMulDivisors R M` states that a scalar multiple is `0` only if either argument is `0`.
This is a version of saying that `M` is torsion free, without assuming `R` is zero-divisor free.

The main application of `NoZeroSMulDivisors R M`, when `M` is a module,
is the result `smul_eq_zero`: a scalar multiple is `0` iff either argument is `0`.

It is a generalization of the `NoZeroDivisors` class to heterogeneous multiplication.
 -/
NoZeroSMulDivisors : (R : Type u_4) → (M : Type u_5) → [Zero R] → [Zero M] → [SMul R M] → Prop
-- Init.System.IOError
/-- An operation was not supported.

This corresponds to POSIX errors `EADDRNOTAVAIL`, `EAFNOSUPPORT`, `ENODEV`, `ENOPROTOOPT`
`ENOSYS`, `EOPNOTSUPP`, `ERANGE`, `ESPIPE`, and `EXDEV`.
 -/
IO.Error.unsupportedOperation : UInt32 → String → IO.Error