mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- Given a family of measurable sets, its measurable union is its union modulo sets of measure
zero. It is well defined up to measure 0. For instance, the measurable union of all the singleton
sets in `ℝ` is empty (while the usual union would be the whole space).
This lemma shows the existence of a measurable union, writing it as the union of a countable
subfamily.  -/
MeasureTheory.Measure.exists_ae_subset_biUnion_countable : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.SFinite μ] {C : Set (Set α)},
  (∀ s ∈ C, MeasurableSet s) → ∃ D ⊆ C, D.Countable ∧ ∀ s ∈ C, s ≤ᵐ[μ] ⋃₀ D
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_
/-- The equivalences `CommMon (Type u) ≌ CommMonCat.{u}` and `CommGrp (Type u) ≌ CommGrpCat.{u}`
are naturally compatible with the forgetful functors to `GrpCat` and `Grp (Type u)`.
 -/
commGrpTypeEquivalenceCommGrpForgetCommMon : CommGrpTypeEquivalenceCommGrp.functor.comp (CategoryTheory.forget₂ CommGrpCat CommMonCat) ≅
  (CategoryTheory.CommGrp.forget₂CommMon (Type u)).comp CommMonTypeEquivalenceCommMon.functor
-- Lean.Meta.Basic
Lean.Meta.ParamInfo.mk.sizeOf_spec : ∀ (binderInfo : Lean.BinderInfo) (hasFwdDeps : Bool) (backDeps : Array ℕ)
  (isProp isDecInst isInstance higherOrderOutParam dependsOnHigherOrderOutParam : Bool),
  sizeOf
      { binderInfo := binderInfo, hasFwdDeps := hasFwdDeps, backDeps := backDeps, isProp := isProp,
        isDecInst := isDecInst, isInstance := isInstance, higherOrderOutParam := higherOrderOutParam,
        dependsOnHigherOrderOutParam := dependsOnHigherOrderOutParam } =
    1 + sizeOf binderInfo + sizeOf hasFwdDeps + sizeOf backDeps + sizeOf isProp + sizeOf isDecInst + sizeOf isInstance +
        sizeOf higherOrderOutParam +
      sizeOf dependsOnHigherOrderOutParam
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- Multiplication in the colimit is well-defined in the right argument.  -/
MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {x y y' : (j : J) × ↑(F.obj j)},
  CategoryTheory.Limits.Types.FilteredColimit.Rel (F.comp (CategoryTheory.forget MonCat)) y y' →
    MonCat.FilteredColimits.colimitMulAux F x y = MonCat.FilteredColimits.colimitMulAux F x y'
-- Mathlib.RingTheory.PowerSeries.WellKnown
_private.Mathlib.RingTheory.PowerSeries.WellKnown.0.PowerSeries.invOneSubPow.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (d : ℕ) → motive d.succ),
  (match 0 with
    | 0 => h_1 ()
    | d.succ => h_2 d) =
    h_1 ()
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.Nonempty.zero_mul : ∀ {α : Type u_1} [inst : MulZeroClass α] {s : Set α}, s.Nonempty → 0 * s = 0
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.functorEquivalence_inverse : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C],
  (CategoryTheory.ShortComplex.functorEquivalence J C).inverse =
    CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.mem_map_equiv : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M ≃* N} {K : Subsemigroup M} {x : N},
  x ∈ Subsemigroup.map (↑f) K ↔ f.symm x ∈ K
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.var? : {σ : Type} → Lean.Elab.Term.Do.AltExpr σ → Option Lean.Elab.Term.Do.Var
-- Mathlib.Order.Basic
max_rec' : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α} (p : α → Prop), p a → p b → p (max a b)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m.WF →
    ∀ {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (m.insertMany l).getKey! k = m.getKey! k
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : m.WF)
  (h' : k ∈ Std.HashMap.Raw.filterMap f m), (f (m.getKey k ⋯) m[k]).isSome = true
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConePostcompose_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : F ⟶ G} {c : CategoryTheory.Limits.Cone F},
  H.mapConePostcompose.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point.0.tacticMap_simp : Lean.ParserDescr
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instCommMonoid : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → CommMonoid (UpperSet α)
-- Mathlib.Algebra.Polynomial.Roots
/-- `nthRoots n a` noncomputably returns the solutions to `x ^ n = a`.  -/
Polynomial.nthRoots : {R : Type u} → [inst : CommRing R] → [IsDomain R] → ℕ → R → Multiset R
-- Mathlib.Data.Fin.Rev
/-- `Fin.rev` as an `Equiv.Perm`, the antitone involution `Fin n → Fin n` given by
`i ↦ n-(i+1)`.  -/
Fin.revPerm : {n : ℕ} → Equiv.Perm (Fin n)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsStableUnderPostcompHomRel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.HomRel.IsStableUnderPostcomp (HomotopicalAlgebra.BifibrantObject.homRel C)
-- Mathlib.Order.Iterate
/-- If `f` is a strictly monotone map and `x < f x` at some point `x`, then the iterates `f^[n] x`
form a strictly monotone sequence.  -/
StrictMono.strictMono_iterate_of_lt_map : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x : α}, StrictMono f → x < f x → StrictMono fun n => f^[n] x
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_mul_le : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → a / b * b ≤ a
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.setLIntegral_condKernel_univ_right : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {f : β × Ω → ENNReal},
  Measurable f →
    ∀ (a : α) {s : Set β},
      MeasurableSet s →
        ∫⁻ (b : β) in s, ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω) in s ×ˢ Set.univ, f x ∂κ a
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.responseBody.injEq : ∀ {β : Type} (x x_1 : Option Std.Http.Chunk),
  (Std.Http.Server.Connection.Recv.responseBody✝ x = Std.Http.Server.Connection.Recv.responseBody✝ x_1) = (x = x_1)
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingPropertyFixedTop.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) (t : A ⟶ X),
  CategoryTheory.HasLiftingPropertyFixedTop i p t = ∀ (b : B ⟶ Y) (sq : CategoryTheory.CommSq t i p b), sq.HasLift
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialTermInfo.mk.injEq : ∀ (toElabInfo : Lean.Elab.ElabInfo) (lctx : Lean.LocalContext) (expectedType? : Option Lean.Expr)
  (toElabInfo_1 : Lean.Elab.ElabInfo) (lctx_1 : Lean.LocalContext) (expectedType?_1 : Option Lean.Expr),
  ({ toElabInfo := toElabInfo, lctx := lctx, expectedType? := expectedType? } =
      { toElabInfo := toElabInfo_1, lctx := lctx_1, expectedType? := expectedType?_1 }) =
    (toElabInfo = toElabInfo_1 ∧ lctx = lctx_1 ∧ expectedType? = expectedType?_1)
-- Mathlib.Order.SymmDiff
symmDiff_def : ∀ {α : Type u_2} [inst : Max α] [inst_1 : SDiff α] (a b : α), symmDiff a b = a \ b ⊔ b \ a
-- Mathlib.Tactic.CongrExclamation
/-- As a last pass, perform eta expansion of both sides of an equality. For example,
this transforms a bare `HAdd.hAdd` into `fun x y => x + y`.  -/
Congr!.Config.etaExpand : Congr!.Config → Bool
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.id_app : ∀ (X : TopCat) (x : ↑X), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) x = x
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- If `x` is in the domain of a partial map `f`, then `f` restricts to a map from `Spec 𝒪_x`.  -/
AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMem : {X Y : AlgebraicGeometry.Scheme} →
  (f : X.PartialMap Y) → {x : ↥X} → x ∈ f.domain → (AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.toCompletion_zero : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K),
  NumberField.InfinitePlace.Completion.toCompletion 0 = 0
-- Mathlib.Analysis.Calculus.Deriv.Mul
DifferentiableWithinAt.finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} {𝔸' : Type u_3}
  [inst_1 : NormedCommRing 𝔸'] [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) → DifferentiableWithinAt 𝕜 (∏ i ∈ u, f i) s x
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.lift_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k] (F : G →* A)
  (f : SkewMonoidAlgebra k G), ((SkewMonoidAlgebra.lift k G A) F) f = f.sum fun a b => b • F a
-- Mathlib.Algebra.Group.Commute.Units
AddCommute.addUnits_neg_left_iff : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {u : AddUnits M}, AddCommute (↑(-u)) a ↔ AddCommute (↑u) a
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.ofCommaObject_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (c : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C))
  {X Y : CategoryTheory.WithTerminal C} (f : X ⟶ Y),
  (CategoryTheory.WithTerminal.ofCommaObject c).map f =
    match X, Y, f with
    | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
      c.left.map (CategoryTheory.WithTerminal.down f)
    | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => c.hom.app x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => CategoryTheory.CategoryStruct.id c.right
-- Mathlib.Tactic.Translate.Core
/-- Add the structure fields of `src` to the translations dictionary
so that they will be translated correctly.  -/
Mathlib.Tactic.Translate.proceedFields : Mathlib.Tactic.Translate.TranslateData → Lean.Name → Lean.Name → Mathlib.Tactic.Translate.Config → Lean.CoreM Unit
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.fold_mapWithPostcondition : ∀ {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → Std.Iterators.PostconditionT n γ} {g : δ → γ → δ} {init : δ} {it : Std.Iter β},
  Std.IterM.fold g init (Std.Iter.mapWithPostcondition f it) =
    Std.Iter.foldM
      (fun d b => do
        let c ← (f b).run
        pure (g d c))
      init it
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.mul_def : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (f g : E →ₗᵢ[R] E), f * g = f.comp g
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} {S : C}
  {toPreZeroHypercover : CategoryTheory.PreZeroHypercover S} {mem₀ : toPreZeroHypercover.presieve₀ ∈ J.coverings S}
  {toPreZeroHypercover_1 : CategoryTheory.PreZeroHypercover S}
  {mem₀_1 : toPreZeroHypercover_1.presieve₀ ∈ J.coverings S},
  { toPreZeroHypercover := toPreZeroHypercover, mem₀ := mem₀ } =
      { toPreZeroHypercover := toPreZeroHypercover_1, mem₀ := mem₀_1 } →
    toPreZeroHypercover = toPreZeroHypercover_1
-- Mathlib.Algebra.Lie.CartanExists
_private.Mathlib.Algebra.Lie.CartanExists.0.LieAlgebra.engel_isBot_of_isMin.termφ : Lean.ParserDescr
-- Lean.Structure
/-- If `fieldName` is a subobject (that it, if it is an embedded parent structure),
then returns the name of that parent structure.
 -/
Lean.isSubobjectField? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.mem_sdiff_singleton`. -/
Set.mem_diff_singleton : ∀ {α : Type u_1} {s : Set α} {a b : α}, a ∈ s \ {b} ↔ a ∈ s ∧ a ≠ b
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_sdiff_singleton_add_one`. -/
Set.encard_diff_singleton_add_one : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → (s \ {a}).encard + 1 = s.encard
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- The global ref for looking up `grw` lemmas.  -/
Mathlib.Tactic.ClickSuggestions.grwRef : IO.Ref (Option (Lean.Meta.RefinedDiscrTree Mathlib.Tactic.ClickSuggestions.GrwLemma))
-- Init.Data.UInt.Lemmas
UInt64.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < UInt64.size → b < UInt64.size → (UInt64.ofNat a < UInt64.ofNat b ↔ a < b)
-- Init.Omega.Int
Lean.Omega.Int.natCast_ofNat : ∀ {x : ℕ}, ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_of_mem_maximalAtlas : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} {x : M} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) →
      e ∈ StructureGroupoid.maximalAtlas M G → x ∈ e.source → ChartedSpace.LiftPropAt Q (↑e) x
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.map_prod : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommMonoidWithZero R] (g : ι → ℕ) {f : ArithmeticFunction R},
  f.IsMultiplicative →
    ∀ (s : Finset ι), (↑s).Pairwise (Function.onFun Nat.Coprime g) → f (∏ i ∈ s, g i) = ∏ i ∈ s, f (g i)
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellation.mk : Lean.Server.RequestCancellation
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyOutgoingCall.toJson : Lean.Lsp.CallHierarchyOutgoingCall → Lean.Json
-- Mathlib.CategoryTheory.Sites.LeftExact
/-- `plusPlusFunctor` is isomorphic to `sheafification`.  -/
CategoryTheory.plusPlusFunctorIsoSheafification : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type w) →
        [inst_1 : CategoryTheory.Category.{t, w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {FD : D → D → Type u_1} →
                {CD : D → Type t} →
                  [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                    [inst_5 : CategoryTheory.ConcreteCategory D FD] →
                      [inst_6 :
                          ∀ (X : C),
                            CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)] →
                        [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] →
                          [inst_8 :
                              ∀ {X : C} (S : J.Cover X),
                                CategoryTheory.Limits.PreservesLimitsOfShape
                                  (CategoryTheory.Limits.WalkingMulticospan S.shape) (CategoryTheory.forget D)] →
                            J.sheafification D ≅ CategoryTheory.sheafification J D
-- Mathlib.Data.Fin.Tuple.Basic
Fin.lt_find_iff : ∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] (h : ∃ k, p k) (i : Fin n), i < Fin.find p h ↔ ∀ m ≤ i, ¬p m
-- Mathlib.RepresentationTheory.Equiv
Representation.freeLift.eq_1 : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) {α : Type w'} (f : α → V),
  σ.freeLift f =
    {
      toLinearMap :=
        (Finsupp.linearCombination k fun x => (σ x.2) (f x.1)) ∘ₗ
          ↑(Finsupp.curryLinearEquiv k).symm ∘ₗ Finsupp.mapRange.linearMap ↑(MonoidAlgebra.coeffLinearEquiv k),
      isIntertwining' := ⋯ }
-- Init.Internal.Order.Basic
Lean.Order.admissible_or : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] (P Q : α → Prop),
  Lean.Order.admissible P → Lean.Order.admissible Q → Lean.Order.admissible fun x => P x ∨ Q x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospan_map_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospan f g).map CategoryTheory.Limits.WalkingCospan.Hom.inl = f
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatUInt32UintOfNatNat : Lean.Grind.ToInt.OfNat UInt32 (Lean.Grind.IntInterval.uint 32)
-- Mathlib.Order.Disjoint
IsCompl.disjoint_right_iff : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl y z → (Disjoint x z ↔ x ≤ y)
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- Every value of the approximation is greater or equal than every fixed point of `f`
less or equal than the initial value  -/
OrdinalApprox.le_gfpApprox_of_mem_fixedPoints : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x a : α},
  a ∈ Function.fixedPoints ⇑f → a ≤ x → ∀ (i : Ordinal.{u}), a ≤ OrdinalApprox.gfpApprox f x i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).getKey? k = none
-- Mathlib.Topology.UniformSpace.Defs
/-- If a function `T` is uniformly continuous in a uniform space `β`,
then its `n`-th iterate `T^[n]` is also uniformly continuous.  -/
UniformContinuous.iterate : ∀ {β : Type ub} [inst : UniformSpace β] (T : β → β) (n : ℕ), UniformContinuous T → UniformContinuous T^[n]
-- Mathlib.Computability.Encoding
Computability.encodePosNum_nonempty : ∀ (n : PosNum), Computability.encodePosNum n ≠ []
-- Mathlib.AlgebraicGeometry.Noetherian
AlgebraicGeometry.instIsLocallyNoetherianXScheme : ∀ {X : AlgebraicGeometry.Scheme} {U : X.OpenCover} (i : U.I₀) [AlgebraicGeometry.IsLocallyNoetherian X],
  AlgebraicGeometry.IsLocallyNoetherian (U.X i)
-- Mathlib.Data.Part
/-- `restrict p o h` replaces the domain of `o` with `p`, and is well defined when
`p` implies `o` is defined.  -/
Part.restrict : {α : Type u_1} → (p : Prop) → (o : Part α) → (p → o.Dom) → Part α
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.one_sub_inv : ∀ {p q : NNReal}, p.HolderConjugate q → 1 - p⁻¹ = q⁻¹
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- We say that there exists an absolute left Kan lift of `g` along `f` if any 1-morphism `h`
commutes with the left Kan lift `f₊ g`.  -/
CategoryTheory.Bicategory.HasAbsLeftKanLift : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b c : B} → (b ⟶ a) → (c ⟶ a) → Prop
-- Mathlib.Topology.MetricSpace.Thickening
/-- The (open) thickening `Metric.thickening δ E` of a fixed subset `E` is an increasing function of
the thickening radius `δ`.  -/
Metric.thickening_mono : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ},
  δ₁ ≤ δ₂ → ∀ (E : Set α), Metric.thickening δ₁ E ⊆ Metric.thickening δ₂ E
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_reindex : ∀ {R : Type u_1} {M : Type u_3} {I : Type u_6} {J : Type u_7} [inst : PartialOrder R] [inst_1 : Semiring R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I ≃ J)
  (g : I → M), Convexity.iConvexComb s g = Convexity.iConvexComb (Convexity.StdSimplex.map (⇑f) s) (g ∘ ⇑f.symm)
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.instIsIsoStrictInv : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [inst_2 : F.IsIso], F.strictInv.IsIso
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_getElem_utf8EncodeChar_three_of_utf8Size_eq_four : ∀ {c : Char} (hc : c.utf8Size = 4),
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte (String.utf8EncodeChar c)[3] = false
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.toContinuousOrderHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : TopologicalSpace α] →
      [inst_1 : Preorder α] → [inst_2 : TopologicalSpace β] → [inst_3 : Preorder β] → EsakiaHom α β → α →Co β
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.base_eqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (h : X = Y), (CategoryTheory.eqToHom h).base = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.Ideal
Order.Ideal.top_toLowerSet : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P], ⊤.toLowerSet = ⊤
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- A finite-dimensional t2 vector space over a complete field must carry the module topology.

Not declared as a global instance only for performance reasons.  -/
isModuleTopologyOfFiniteDimensional : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [CompleteSpace 𝕜] [T2Space E]
  [FiniteDimensional 𝕜 E], IsModuleTopology 𝕜 E
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- If `P` implies `P'`, then there is a functor from `CompHausLike P` to `CompHausLike P'`.  -/
CompHausLike.toCompHausLike : {P P' : TopCat → Prop} →
  (∀ (X : CompHausLike P), P X.toTop → P' X.toTop) → CategoryTheory.Functor (CompHausLike P) (CompHausLike P')
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.topologicalClosure.congr_simp : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] (s s_1 : Subgroup G),
  s = s_1 → s.topologicalClosure = s_1.topologicalClosure
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lequivProdDirectSum_symm_apply : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {α : Option ι → Type w} [inst_1 : (i : Option ι) → AddCommMonoid (α i)]
  [inst_2 : (i : Option ι) → Module R (α i)] (a : α none × DirectSum ι fun i => α (some i)),
  (DirectSum.lequivProdDirectSum R).symm a = DirectSum.addEquivProdDirectSum.invFun a
-- Mathlib.Geometry.Manifold.PartitionOfUnity
BumpCovering.contMDiff_toPartitionOfUnity : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (f : BumpCovering ι M s),
  (∀ (i : ι), ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ ⇑(f i)) →
    ∀ (i : ι), ContMDiff I (modelWithCornersSelf ℝ ℝ) ↑⊤ ⇑(f.toPartitionOfUnity i)
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.dest.eq_1 : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α : TypeVec.{u} n} (x : P.M α),
  MvPFunctor.M.dest P x = MvPFunctor.M.dest' P ⋯ x.snd