mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.dropSliceTR.match_1.splitter : (motive : ℕ → Sort u_1) → (m : ℕ) → (Unit → motive 0) → ((m : ℕ) → motive m.succ) → motive m
-- Mathlib.Order.Hom.Lattice
SupHom.instSemilatticeSup : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → SemilatticeSup (SupHom α β)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The composition operator (in the target) with a Lipschitz map is Lipschitz.  -/
BoundedContinuousFunction.lipschitz_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : PseudoMetricSpace γ] {G : β → γ} {C : NNReal} (H : LipschitzWith C G),
  LipschitzWith C (BoundedContinuousFunction.comp G H)
-- Mathlib.Analysis.Normed.Module.Convex
norm_sub_le_of_mem_segment : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {x y z : E},
  y ∈ segment ℝ x z → ‖y - x‖ ≤ ‖z - x‖
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.dual_delete : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), (M.delete X)✶ = M✶.contract X
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- The canonical linear equivalence between `M` and `Module.AEval' φ` as an `R`-module,
where `φ : M →ₗ[R] M`.
 -/
Module.AEval'.of : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (φ : M →ₗ[R] M) → M ≃ₗ[R] Module.AEval' φ
-- Std.Time.Format.Basic
Std.Time.FormatPart.modifier.sizeOf_spec : ∀ (modifier : Std.Time.Modifier), sizeOf (Std.Time.FormatPart.modifier modifier) = 1 + sizeOf modifier
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mul_by_divBy : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : ↥S) (p : LocalizedModule S M),
  ((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) ((LocalizedModule.divBy s) p) = p
-- Mathlib.GroupTheory.Complement
AddSubgroup.vadd_apply_eq_vadd_apply_neg_vadd : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {F : Type u_2} [inst_1 : AddGroup F] [inst_2 : AddAction F G]
  [inst_3 : AddAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (q : G ⧸ H),
  ↑(⋯.leftQuotientEquiv q) = f +ᵥ ↑(⋯.leftQuotientEquiv (-f +ᵥ q))
-- Lean.Linter.Deprecated
Lean.Linter.getDeprecatedNewName : Lean.Environment → Lean.Name → Option Lean.Name
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.leftUnitor_hom : ∀ (C : CategoryTheory.Cat),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor C).hom =
    (CategoryTheory.Prod.snd ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Cat) ↑C).toCatHom
-- Init.Data.List.Find
List.find?_eq_map_findFinIdx?_getElem : ∀ {α : Type u_1} {xs : List α} {p : α → Bool}, List.find? p xs = Option.map (fun x => xs[x]) (List.findFinIdx? p xs)
-- Mathlib.LinearAlgebra.Finsupp.LSum
Submodule.mulLeftMap_eq_mulRightMap_of_commute : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_4} [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : SMulCommClass R R S] [inst_4 : IsScalarTower R S S] [inst_5 : SMulCommClass R S S] {M : Submodule R S}
  (N : Submodule R S) {ι : Type u_5} (m : ι → ↥M),
  (∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n) → Submodule.mulLeftMap N m = N.mulRightMap m
-- Init.Data.BitVec.Bitblast
BitVec.DivModArgs.mk.injEq : ∀ {w : ℕ} (n d n_1 d_1 : BitVec w), ({ n := n, d := d } = { n := n_1, d := d_1 }) = (n = n_1 ∧ d = d_1)
-- Mathlib.CategoryTheory.IsoCat
/-- A functor which is an isomorphism of categories is bijective on objects.  -/
CategoryTheory.Functor.IsIso.bijective_obj : ∀ {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) [self : F.IsIso],
  Function.Bijective F.obj
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.PreservesKernel.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f] [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G],
  (CategoryTheory.Limits.PreservesKernel.iso G f).hom = CategoryTheory.Limits.kernelComparison f G
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.entryAtIdx?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.Equiv t₂ → t₁.entryAtIdx? i = t₂.entryAtIdx? i
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.conj_eq : ∀ {α : Type u_3} [inst : CommSemiring α] [inst_1 : StarRing α] {a : α}, IsSelfAdjoint a → (starRingEnd α) a = a
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.sin.eq_1 : ∀ (A : Type u_1) [inst : Ring A] [inst_1 : Algebra ℚ A],
  PowerSeries.sin A = PowerSeries.mk fun n => if Even n then 0 else (algebraMap ℚ A) ((-1) ^ (n / 2) / ↑n.factorial)
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
_private.Mathlib.CategoryTheory.Abelian.FreydMitchell.0.CategoryTheory.Abelian.FreydMitchell.G.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Abelian.FreydMitchell.G✝ C = CategoryTheory.Ind.yoneda.rightOp
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.mk.sizeOf_spec : ∀
  (userTime systemTime maxRSS ixRSS idRSS isRSS minFlt majFlt nSwap inBlock outBlock msgSent msgRecv signals voluntaryCS
    involuntaryCS : UInt64),
  sizeOf
      { userTime := userTime, systemTime := systemTime, maxRSS := maxRSS, ixRSS := ixRSS, idRSS := idRSS,
        isRSS := isRSS, minFlt := minFlt, majFlt := majFlt, nSwap := nSwap, inBlock := inBlock, outBlock := outBlock,
        msgSent := msgSent, msgRecv := msgRecv, signals := signals, voluntaryCS := voluntaryCS,
        involuntaryCS := involuntaryCS } =
    1 + sizeOf userTime + sizeOf systemTime + sizeOf maxRSS + sizeOf ixRSS + sizeOf idRSS + sizeOf isRSS +
                        sizeOf minFlt +
                      sizeOf majFlt +
                    sizeOf nSwap +
                  sizeOf inBlock +
                sizeOf outBlock +
              sizeOf msgSent +
            sizeOf msgRecv +
          sizeOf signals +
        sizeOf voluntaryCS +
      sizeOf involuntaryCS
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- A vector space has dimension `1` if and only if there is a
single non-zero vector of which all vectors are multiples.  -/
rank_eq_one_iff : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V], Module.rank K V = 1 ↔ ∃ v₀, v₀ ≠ 0 ∧ ∀ (v : V), ∃ r, r • v₀ = v
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` is preserved by localization away, then so is `Locally P`.  -/
RingHom.locally_localizationAwayPreserves : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.forget_reflects_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C},
  (CategoryTheory.Endofunctor.Coalgebra.forget F).ReflectsIsomorphisms
-- Mathlib.Algebra.Homology.QuasiIso
/-- The isomorphism `K.homology i ≅ L.homology i` induced by a morphism `f : K ⟶ L` such
that `[QuasiIsoAt f i]` holds.  -/
isoOfQuasiIsoAt : {ι : Type u_1} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} →
            (f : K ⟶ L) →
              (i : ι) →
                [inst_2 : K.HasHomology i] → [inst_3 : L.HasHomology i] → [QuasiIsoAt f i] → K.homology i ≅ L.homology i
-- Init.Prelude
MonadFunctorT.mk : {m : Type u → Type v} →
  {n : Type u → Type w} → ({α : Type u} → ({β : Type u} → m β → m β) → n α → n α) → MonadFunctorT m n
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprULift_mathlib : {α : Type s} → [Lean.ToExpr α] → [Lean.ToLevel] → [Lean.ToLevel] → Lean.ToExpr (ULift.{r, s} α)
-- Mathlib.Topology.MetricSpace.PiNat
/-- The distance function on a product space `Π n, E n`, given by `dist x y = (1/2)^n` where `n` is
the first index at which `x` and `y` differ.  -/
PiNat.dist : {E : ℕ → Type u_1} → Dist ((n : ℕ) → E n)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.instInhabitedPreDiscrTree.default : {α : Type} → Lean.Meta.RefinedDiscrTree.PreDiscrTree α
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.dvd_monomial_mul_iff_exists : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {p q : MvPolynomial σ R} [IsCancelMulZero R] {n : σ →₀ ℕ},
  p ∣ (MvPolynomial.monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (MvPolynomial.monomial m) 1 * r
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.count_map_roots_of_injective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : DecidableEq B]
  (p : Polynomial A) {f : A →+* B},
  Function.Injective ⇑f →
    ∀ (b : B), Multiset.count b (Multiset.map (⇑f) p.roots) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_mem_vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set β} {a : α} {b : β}, b ∈ s → a +ᵥ b ∈ a +ᵥ s
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instIsScalarTower : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : SMulCommClass 𝕜 A A] [inst_4 : IsScalarTower 𝕜 A A] {S : Type u_3}
  [inst_5 : Monoid S] [inst_6 : DistribMulAction S A] [inst_7 : SMulCommClass 𝕜 S A] [inst_8 : ContinuousConstSMul S A]
  [inst_9 : IsScalarTower S A A] [inst_10 : SMulCommClass S A A] {T : Type u_4} [inst_11 : Monoid T]
  [inst_12 : DistribMulAction T A] [inst_13 : SMulCommClass 𝕜 T A] [inst_14 : ContinuousConstSMul T A]
  [inst_15 : IsScalarTower T A A] [inst_16 : SMulCommClass T A A] [inst_17 : SMul S T] [IsScalarTower S T A],
  IsScalarTower S T (DoubleCentralizer 𝕜 A)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnitsTopEquiv.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M], AddSubgroup.ofAddUnitsTopEquiv = ⊤.ofAddUnitsEquivType.trans AddSubgroup.topEquiv
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.isoOver_hom_app_hom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} {ℱ ℱ' : CategoryTheory.Sheaf K A}
  (α : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : A) (X_1 : Cᵒᵖ)
  (g :
    { obj := fun Y => Opposite.unop Y ⟶ (G.op.comp ℱ.obj).obj X_1,
          map := fun {X Y} f => TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp f.unop g, map_id := ⋯,
          map_comp := ⋯ }.obj
      (Opposite.op X)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.IsCoverDense.isoOver α X).hom.app X_1)) g =
    CategoryTheory.CategoryStruct.comp g (α.hom.app X_1)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.PosDef.smul : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : PartialOrder N] [inst_2 : AddCommMonoid N]
  {R : Type u_8} [inst_3 : CommSemiring R] [inst_4 : PartialOrder R] [inst_5 : Module R M] [inst_6 : Module R N]
  [PosSMulStrictMono R N] {Q : QuadraticMap R M N}, Q.PosDef → ∀ {a : R}, 0 < a → (a • Q).PosDef
-- Mathlib.Geometry.Manifold.Sheaf.Basic
StructureGroupoid.LocalInvariantProp.sheafHasCoeToFun : {H : Type u_1} →
  [inst : TopologicalSpace H] →
    {H' : Type u_2} →
      [inst_1 : TopologicalSpace H'] →
        {G : StructureGroupoid H} →
          {G' : StructureGroupoid H'} →
            {P : (H → H') → Set H → H → Prop} →
              (M : Type u) →
                [inst_2 : TopologicalSpace M] →
                  [inst_3 : ChartedSpace H M] →
                    (M' : Type u) →
                      [inst_4 : TopologicalSpace M'] →
                        [inst_5 : ChartedSpace H' M'] →
                          (hG : G.LocalInvariantProp G' P) →
                            (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                              CoeFun ((StructureGroupoid.LocalInvariantProp.sheaf M M' hG).obj.obj U) fun x =>
                                ↥(Opposite.unop U) → M'
-- Mathlib.Order.Hom.Basic
OrderEmbedding.acc : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β) (a : α),
  Acc (fun x1 x2 => x1 < x2) (f a) → Acc (fun x1 x2 => x1 < x2) a
-- Mathlib.Tactic.Attr.Register
/-- A simp set for simplifying expressions involving `⊤` in `enat_to_nat`.  -/
Parser.Attr.enat_to_nat_top : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Balancing
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.balanceₘ : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Init.Data.Vector.Lemmas
/-- `map_id_fun'` differs from `map_id_fun` by representing the identity function as a lambda, rather than `id`.  -/
Vector.map_id_fun' : ∀ {n : ℕ} {α : Type u_1}, (Vector.map fun a => a) = id
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `NoNatZeroDivisors`  -/
Lean.Meta.Grind.Arith.Linear.Struct.noNatDivInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_inter_mul_sdiff' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α} (t : Set α),
  (s ∩ Function.mulSupport f).Finite →
    (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Init.Data.Vector.Basic
Vector.findSome? : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → (α → Option β) → Vector α n → Option β
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.toIndGroupInfo : Lean.Elab.Structural.IndGroupInst → Lean.Elab.Structural.IndGroupInfo
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.quotientTensorQuotientEquiv_symm_apply_mk_tmul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (m : Submodule R M) (n : Submodule R N) (x : M) (y : N),
  (TensorProduct.quotientTensorQuotientEquiv m n).symm (Submodule.Quotient.mk (x ⊗ₜ[R] y)) =
    Submodule.Quotient.mk x ⊗ₜ[R] Submodule.Quotient.mk y
-- Mathlib.NumberTheory.Dioph
Dioph.inject_dummies : ∀ {α β γ : Type u} {S : Set (α → ℕ)} (f : β → γ) (g : γ → Option β),
  (∀ (x : β), g (f x) = some x) →
    ∀ (p : Poly (α ⊕ β)),
      (∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (Sum.elim v t) = 0) → ∃ q, ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, q (Sum.elim v t) = 0
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasSum.zero_add : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] {m : M} [ContinuousAdd M] {f : ℕ → M},
  HasSum (fun n => f (n + 1)) m → HasSum f (f 0 + m)
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
HomotopyCategory.instIsTriangulatedIntUp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] [inst_3 : CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.IsTriangulated (HomotopyCategory C (ComplexShape.up ℤ))
-- Mathlib.Order.BoundedOrder.Basic
not_isTop_iff_ne_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, ¬IsTop a ↔ a ≠ ⊤
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.subgroup.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  (s : UpperSet (FiniteMulArchimedeanClass M)),
  FiniteMulArchimedeanClass.subgroup s =
    { toSubsemigroup := MulArchimedeanClass.subsemigroup (FiniteMulArchimedeanClass.toUpperSetMulArchimedeanClass s),
      one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.of_mul_left : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, (s * t).Nonempty → s.Nonempty
-- Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
CategoryTheory.coherentTopology.presheafIsLocallySurjective_iff : ∀ {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] {FD : D → D → Type u_3} {CD : D → Type w}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  {F G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G) [inst_4 : CategoryTheory.Preregular C]
  [inst_5 : CategoryTheory.FinitaryPreExtensive C] [CategoryTheory.Limits.PreservesFiniteProducts F]
  [CategoryTheory.Limits.PreservesFiniteProducts G]
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)],
  CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.coherentTopology C) f ↔
    CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.regularTopology C) f
-- Std.Data.DTreeMap.Basic
/-- Partitions a tree map into two tree maps based on a predicate.  -/
Std.DTreeMap.partition : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      ((a : α) → β a → Bool) → Std.DTreeMap α β cmp → Std.DTreeMap α β cmp × Std.DTreeMap α β cmp
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_iInf_rng : ∀ {α : Type ua} {β : Type ub} {ι : Sort u_1} {f : α → β} {u₁ : UniformSpace α} {u₂ : ι → UniformSpace β},
  UniformContinuous f ↔ ∀ (i : ι), UniformContinuous f
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map_mapAccumr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₂ : Type u_7} {n : ℕ} (xs : List.Vector α n) (f₂ : α → σ₂ → σ₂ × β)
  {s : σ₂} (f₁ : β → γ),
  List.Vector.map f₁ (List.Vector.mapAccumr f₂ xs s).2 =
    (List.Vector.mapAccumr
        (fun x s =>
          have r := f₂ x s;
          (r.1, f₁ r.2))
        xs s).2
-- Mathlib.Data.ENNReal.Inv
ENNReal.smul_sSup : ∀ {R : Type u_3} [inst : SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (s : Set ENNReal) (c : R),
  c • sSup s = ⨆ a ∈ s, c • a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forM_eq_forM_toArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {m' : Type w → Type w'}
  [inst_2 : Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit.{w + 1}},
  m.WF → Std.HashMap.Raw.forM f m = Array.forM (fun a => f a.1 a.2) m.toArray
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
derivWithin_ccosh : ∀ {f : ℂ → ℂ} {x : ℂ} {s : Set ℂ},
  DifferentiableWithinAt ℂ f s x →
    UniqueDiffWithinAt ℂ s x → derivWithin (fun x => Complex.cosh (f x)) s x = Complex.sinh (f x) * derivWithin f s x
-- Mathlib.Topology.ApproximateUnit
/-- An *approximate unit* is a proper filter (i.e., `≠ ⊥`) such that multiplication on the left
(and separately on the right) by `m : α` tends to `𝓝 m` along the filter.  -/
Filter.IsApproximateUnit : {α : Type u_1} → [TopologicalSpace α] → [Mul α] → Filter α → Prop
-- Mathlib.Data.List.Destutter
List.destutter.congr_simp : ∀ {α : Type u_1} (R R_1 : α → α → Prop),
  R = R_1 →
    ∀ {inst : DecidableRel R} [inst_1 : DecidableRel R_1] (a a_1 : List α),
      a = a_1 → List.destutter R a = List.destutter R_1 a_1
-- Mathlib.Data.Num.Lemmas
PosNum.pred'_succ' : ∀ (n : Num), n.succ'.pred' = n
-- Init.Data.UInt.Lemmas
UInt16.ofFin_mod : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a % b) = UInt16.ofFin a % UInt16.ofFin b
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.ringEquivOpMop_symm_apply_coe : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R) (a : (↥S.op)ᵐᵒᵖ),
  ↑(S.ringEquivOpMop.symm a) = MulOpposite.unop ↑(MulOpposite.unop a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonInlayHintLabelPart : Lean.FromJson Lean.Lsp.InlayHintLabelPart
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_lowerBounds_eq_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  BddBelow s → s.Nonempty → sSup (lowerBounds s) = sInf s
-- Mathlib.Analysis.Distribution.Support
Distribution.not_isVanishingOn_iff : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] {f : F → V} {s : Set α} [inst_3 : Zero V],
  ¬Distribution.IsVanishingOn f s ↔ ∃ u, tsupport ⇑u ⊆ s ∧ f u ≠ 0
-- Mathlib.Data.Set.Finite.Lattice
iInf_iSup_eq_of_finite : ∀ {α : Type u} {ι : Sort v} {κ : ι → Sort w} [inst : Order.Frame α] [Finite ι] {f : (a : ι) → κ a → α},
  ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
-- Mathlib.Combinatorics.SetFamily.Shatter
/-- The set family of sets that are shattered by `𝒜`.  -/
Finset.shatterer : {α : Type u_1} → [DecidableEq α] → Finset (Finset α) → Finset (Finset α)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castLEEmb_Ico : ∀ {n m : ℕ} (a b : Fin n) (h : n ≤ m),
  Finset.map (Fin.castLEEmb h) (Finset.Ico a b) = Finset.Ico (Fin.castLE h a) (Fin.castLE h b)
-- Init.Data.SInt.Lemmas
ISize.ofInt_toInt : ∀ (x : ISize), ISize.ofInt x.toInt = x
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- `closure` forms a Galois insertion with the coercion to set.  -/
AddSubmonoid.gi : (M : Type u_1) → [inst : AddZeroClass M] → GaloisInsertion AddSubmonoid.closure SetLike.coe
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
CategoryTheory.CostructuredArrow.ιCompGrothendieckProj_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (X : D)
  (X_1 : ↑(((CategoryTheory.Functor.id D).comp (CategoryTheory.CostructuredArrow.functor L)).obj X)),
  (CategoryTheory.CostructuredArrow.ιCompGrothendieckProj L X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CostructuredArrow.left X_1)
-- Batteries.Data.Fin.Coding
Fin.encodeOption.eq_2 : ∀ {n : ℕ} (i : ℕ) (h : i < n), Fin.encodeOption (some ⟨i, h⟩) = ⟨i + 1, ⋯⟩
-- Batteries.Lean.PersistentHashSet
/-- Obtain a `PersistentHashSet` from an array.
 -/
Lean.PersistentHashSet.ofArray : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Array α → Lean.PersistentHashSet α
-- Init.Data.BitVec.Basic
/-- Turns a `Bool` into a bitvector of length `1`.  -/
BitVec.ofBool : Bool → BitVec 1
-- Mathlib.Topology.Algebra.Valued.ValuativeRel
/-- Helper `Valued` instance when `ValuativeTopology R` over a `UniformSpace R`,
for use in porting files from `Valued` to `ValuativeRel`.  -/
IsValuativeTopology.instValuedValueGroupWithZeroOfIsUniformAddGroup : {R : Type u_2} →
  [inst : Ring R] →
    [inst_1 : ValuativeRel R] →
      [inst_2 : UniformSpace R] →
        [IsUniformAddGroup R] → [IsValuativeTopology R] → Valued R (ValuativeRel.ValueGroupWithZero R)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.measurePreserving_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ],
  MeasureTheory.MeasurePreserving Prod.swap (μ.prod ν) (ν.prod μ)
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.homOfLE_ι_assoc : ∀ {X : SSet} {S₁ S₂ : X.Subcomplex} (h : S₁ ≤ S₂) {Z : SSet} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.Subcomplex.homOfLE h) (CategoryTheory.CategoryStruct.comp S₂.ι h_1) =
    CategoryTheory.CategoryStruct.comp S₁.ι h_1
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.toSub : {M : Type u} → [self : Lean.Grind.AddCommGroup M] → Sub M
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.toZSMul : {R : Type u} → [self : AddGroupWithOne R] → ZSMul R