mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instDecidableLT : {n : ℕ} → DecidableLT (BitVec n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasDerivWithinAt.ccos : ∀ {f : ℂ → ℂ} {f' x : ℂ} {s : Set ℂ},
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => Complex.cos (f x)) (-Complex.sin (f x) * f') s x
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.extendScalarsHomOfSurjective_symm_apply : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A ≃ₐ[S] A),
  (AlgEquiv.extendScalarsHomOfSurjective h).symm f = AlgEquiv.restrictScalars R f
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.lintegral_Lp_mul_le_Lq_mul_Lr : ∀ {α : Type u_2} [inst : MeasurableSpace α] {p q r : ℝ},
  0 < p →
    p < q →
      1 / p = 1 / q + 1 / r →
        ∀ (μ : MeasureTheory.Measure α) {f g : α → ENNReal},
          AEMeasurable f μ →
            AEMeasurable g μ →
              (∫⁻ (a : α), (f * g) a ^ p ∂μ) ^ (1 / p) ≤
                (∫⁻ (a : α), f a ^ q ∂μ) ^ (1 / q) * (∫⁻ (a : α), g a ^ r ∂μ) ^ (1 / r)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_smul : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : Module R S] (x : S) (r : R), (r • p).smeval x = r • p.smeval x
-- Init.Internal.Order.Basic
Lean.Order.monotone_id : ∀ {α : Sort u} [inst : Lean.Order.PartialOrder α], Lean.Order.monotone fun x => x
-- Mathlib.Order.CompleteLattice.Defs
CompleteSemilatticeInf.toPartialOrder : {α : Type u_8} → [self : CompleteSemilatticeInf α] → PartialOrder α
-- Mathlib.CategoryTheory.Action.Continuous
/-- For `HasForget₂ V TopCat` a predicate on an `X : Action V G` saying that the induced action on
the underlying topological space is continuous.  -/
Action.IsContinuous : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {FV : V → V → Type u_2} →
      {CV : V → Type u_3} →
        [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory V FV] →
            [CategoryTheory.HasForget₂ V TopCat] →
              {G : Type u_4} → [inst_4 : Monoid G] → [TopologicalSpace G] → Action V G → Prop
-- Mathlib.CategoryTheory.Equivalence
/-- The backwards direction of an equivalence.  -/
CategoryTheory.Equivalence.inverse : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → CategoryTheory.Functor D C
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent.inj : ∀ {x : Lean.Grind.AC.Var} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {x_1 : Lean.Grind.AC.Var}
  {c₁_1 : Lean.Meta.Grind.AC.EqCnstr},
  Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent x c₁ =
      Lean.Meta.Grind.AC.EqCnstrProof.superpose_tail_idempotent x_1 c₁_1 →
    x = x_1 ∧ c₁ = c₁_1
-- Mathlib.CategoryTheory.Limits.ColimitLimit
CategoryTheory.Limits.colimitLimitToLimitColimitCone_hom : ∀ {J : Type u₁} {K : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (G : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  [inst_5 : CategoryTheory.Limits.HasLimit G],
  (CategoryTheory.Limits.colimitLimitToLimitColimitCone G).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colim.map (CategoryTheory.Limits.limitIsoSwapCompLim G).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimitLimitToLimitColimit (CategoryTheory.Functor.uncurry.obj G))
        (CategoryTheory.Limits.lim.map
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.currying.unitIso.app G).inv
            CategoryTheory.Limits.colim)))
-- Mathlib.RingTheory.Bialgebra.Hom
Bialgebra.ext_to_ring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  (f g : A →ₐc[R] R), f = g
-- Mathlib.Algebra.Group.Basic
eq_add_of_neg_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, -b + a = c → a = b + c
-- Mathlib.Topology.Sets.VietorisTopology
/-- **Alias** of `TopologicalSpace.NonemptyCompacts.dense_setOfPred_finite`. -/
TopologicalSpace.NonemptyCompacts.dense_setOf_finite : ∀ {α : Type u_1} [inst : TopologicalSpace α], Dense {K | (↑K).Finite}
-- Mathlib.Algebra.Field.Subfield.Defs
/-- A subfield is closed under multiplication.  -/
Subfield.mul_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {x y : K}, x ∈ s → y ∈ s → x * y ∈ s
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProd_adj_left : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} {a₁ : α} {b : β} {a₂ : α},
  (G □ H).Adj (a₁, b) (a₂, b) ↔ G.Adj a₁ a₂
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] (K : ChainComplex C ℕ) {n : ℕ} {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj (AlgebraicTopology.DoldKan.Γ₀.obj K)).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op { len := n })).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) h) =
    CategoryTheory.CategoryStruct.comp
      (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan (Opposite.op { len := n })).inj
        (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n })))
      h
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- Copy an additive submonoid replacing `carrier` with a set that is equal to it.  -/
AddSubmonoid.copy : {M : Type u_1} → [inst : AddZeroClass M] → (S : AddSubmonoid M) → (s : Set M) → s = ↑S → AddSubmonoid M
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.shrinkFunctorIsoFunctor_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (X_1 : Cᵒᵖ),
  S.shrinkFunctorIsoFunctor.hom.app X_1 = (CategoryTheory.shrinkYonedaObjObjEquiv.subtypeEquiv ⋯).toIso.hom
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.coe_oneLE : ∀ {H : Type u_1} [inst : CommGroup H] [inst_1 : PartialOrder H] [inst_2 : IsOrderedMonoid H],
  ↑(GroupCone.oneLE H) = {x | 1 ≤ x}
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.Scheme.Hom.isConnected_preimage_singleton : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyConnected f] (x : ↥S),
  IsConnected (⇑f ⁻¹' {x})
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderivFun_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {i : σ}, MvPowerSeries.pderivFun i 1 = 0
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.drop.eq_1 : ∀ (p : DyckWord) (i : ℕ) (hi : List.count DyckStep.U (List.take i ↑p) = List.count DyckStep.D (List.take i ↑p)),
  p.drop i hi = { toList := List.drop i ↑p, count_U_eq_count_D := ⋯, count_D_le_count_U := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An independent set in a graph `G` such that there is no independent set with more vertices.  -/
SimpleGraph.IsMaximumIndepSet : {α : Type u_3} → [Finite α] → SimpleGraph α → Finset α → Prop
-- Std.Sync.Channel
/-- Create a new channel. If:
- `capacity` is `none` it will be unbounded (the default)
- `capacity` is `some 0` it will always force a rendezvous between sender and receiver
- `capacity` is `some n` with `n > 0` it will use a buffer of size `n` and begin blocking once it
  is filled
 -/
Std.Channel.new : {α : Type} → optParam (Option ℕ) none → BaseIO (Std.Channel α)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'_cons.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (x : ForInStep β) → ((b : β) → motive (ForInStep.done b)) → ((b : β) → motive (ForInStep.yield b)) → motive x
-- Lean.Meta.Canonicalizer
_private.Lean.Meta.Canonicalizer.0.Lean.Meta.Canonicalizer.mkKey.unsafe_1 : Lean.Expr → Lean.Meta.Canonicalizer.State → Option UInt64
-- Mathlib.Topology.MetricSpace.Congruence
/-- A congruence pairwise preserves extended distance. Forward direction of
`congruent_iff_pairwise_edist_eq`.  -/
Congruent.pairwise_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  Congruent v₁ v₂ → Pairwise fun i₁ i₂ => edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
-- Init.Core
heq_self_iff_true : ∀ {α : Sort u_1} (a : α), a ≍ a ↔ True
-- Lean.Data.Lsp.Internal
/-- Identifier that caused this location link.  -/
Lean.Lsp.LeanLocationLink.ident? : Lean.Lsp.LeanLocationLink → Option Lean.Lsp.LeanDeclIdent
-- Mathlib.Data.FunLike.Basic
DFunLike.congr : ∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [i : FunLike F α β] {f g : F} {x y : α}, f = g → x = y → f x = g y
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.inducing_totalSpaceMk_of_inducing_comp : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B),
  Topology.IsInducing (↑(a.pretrivializationAt b) ∘ Bundle.TotalSpace.mk b) →
    Topology.IsInducing (Bundle.TotalSpace.mk b)
-- Mathlib.Order.Concept
Concept.intent_injective : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop}, Function.Injective Concept.intent
-- Mathlib.CategoryTheory.Preadditive.Opposite
CategoryTheory.Functor.rightOp_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor Cᵒᵖ D) [F.Additive], F.rightOp.Additive
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_finset_sdiff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β] {s t : Finset β}
  {a : α}, a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
-- Mathlib.Analysis.Calculus.BumpFunction.SmoothApprox
/-- **Alias** of `ContinuousMap.dense_setOfPred_contDiff`.

---

Infinitely smooth functions are dense in the space of continuous functions.  -/
ContinuousMap.dense_setOf_contDiff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F], Dense {f | ContDiff ℝ ↑⊤ ⇑f}
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.subcomplex_map_le : ∀ {X : SSet} (x y : X.S) (f : { len := x.dim } ⟶ { len := y.dim }),
  (CategoryTheory.ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex → x.subcomplex ≤ y.subcomplex
-- Mathlib.Data.Set.Operations
/-- The off-diagonal of a set `s` is the set of pairs `(a, b)` with `a, b ∈ s` and `a ≠ b`.  -/
Set.offDiag : {α : Type u} → Set α → Set (α × α)
-- Mathlib.Data.Fin.Tuple.Reflection
/-- This can be used to prove
```lean
example (a : Fin 2 → α) : a = ![a 0, a 1] :=
  (etaExpand_eq _).symm
```
 -/
FinVec.etaExpand_eq : ∀ {α : Type u_1} {m : ℕ} (v : Fin m → α), FinVec.etaExpand v = v
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleCommShiftIso_hom_app_hom₂ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive] (n : ℤ)
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((F.mapTriangleCommShiftIso n).hom.app X).hom₂ = (CategoryTheory.Functor.commShiftIso F n).hom.app X.obj₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.mk : String →
  Option String →
    Option Lean.Lsp.MarkupContent →
      Option Lean.Lsp.CompletionItemKind →
        Option Lean.Lsp.InsertReplaceEdit →
          Option String → Option Lean.Json → Option (Array Lean.Lsp.CompletionItemTag) → Lean.Lsp.CompletionItem
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.rootSpan.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Module S M], P.rootSpan S = Submodule.span S (Set.range ⇑P.root)
-- Lean.Level
Lean.simpLevelIMax' : Lean.Level → Lean.Level → Lean.Level → Lean.Level
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.toHoCat_map_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.CofibrantObject C} {f g : X ⟶ Y},
  HomotopicalAlgebra.CofibrantObject.homRel C f g →
    HomotopicalAlgebra.CofibrantObject.toHoCat.map f = HomotopicalAlgebra.CofibrantObject.toHoCat.map g
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.toRingHom_ofAlgHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommSemiring S] [inst_2 : Algebra S R] (p : Polynomial R),
  ↑(AdjoinRoot.ofAlgHom S p) = AdjoinRoot.of p
-- Mathlib.Data.NNRat.Defs
NNRat.mul_den_eq_num : ∀ (q : ℚ≥0), q * ↑q.den = ↑q.num
-- Init.Data.Vector.Count
Vector.countP_cast : ∀ {α : Type u_1} {n a : ℕ} {h : n = a} (p : α → Bool) (xs : Vector α n),
  Vector.countP p (Vector.cast h xs) = Vector.countP p xs
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.Agree'.step : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} {a : F.A} (x y : F.B a → F.M) {x' y' : F.M},
  x' = PFunctor.M.mk ⟨a, x⟩ →
    y' = PFunctor.M.mk ⟨a, y⟩ → (∀ (i : F.B a), PFunctor.M.Agree' n (x i) (y i)) → PFunctor.M.Agree' n.succ x' y'
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.exists : ∀ {α : Type u_1} {ι : Sort uι} [inst : MeasurableSpace α] [Countable ι] {p : ι → α → Prop},
  (∀ (i : ι), Measurable (p i)) → Measurable fun a => ∃ i, p i a
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTop_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β), (f.comp g).withTop = f.withTop.comp g.withTop
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the reverse direction of `AddCommGroup.neg_modEq_neg`. -/
AddCommGroup.ModEq.neg : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G}, a ≡ b [PMOD p] → -a ≡ -b [PMOD p]
-- Mathlib.Analysis.InnerProductSpace.Convex
InnerProductSpace.toUniformConvexSpace : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [InnerProductSpace ℝ F], UniformConvexSpace F
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase.eq_5 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (hrb_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced) (rs : ℕ) (rk : α)
  (rv : β rk) (rls : ℕ) (rlk : α) (rlv : β rlk) (rll rlr : Std.DTreeMap.Internal.Impl α β) (rrs : ℕ) (k_1 : α)
  (v_1 : β k_1) (l r_3 : Std.DTreeMap.Internal.Impl α β)
  (hrb_4 :
    (Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
        (Std.DTreeMap.Internal.Impl.inner rrs k_1 v_1 l r_3)).Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
      (Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
          (Std.DTreeMap.Internal.Impl.inner rrs k_1 v_1 l r_3)).size
      Std.DTreeMap.Internal.Impl.leaf.size),
  Std.DTreeMap.Internal.Impl.balanceRErase k v Std.DTreeMap.Internal.Impl.leaf
      (Std.DTreeMap.Internal.Impl.inner rs rk rv (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr)
        (Std.DTreeMap.Internal.Impl.inner rrs k_1 v_1 l r_3))
      hrb_2 hrb_4 hlr_3 =
    Std.DTreeMap.Internal.Impl.inner (1 + rs) rk rv
      (Std.DTreeMap.Internal.Impl.inner (1 + rls) k v Std.DTreeMap.Internal.Impl.leaf
        (Std.DTreeMap.Internal.Impl.inner rls rlk rlv rll rlr))
      (Std.DTreeMap.Internal.Impl.inner rrs k_1 v_1 l r_3)
-- Mathlib.Order.Filter.Pointwise
Filter.vsub.instNeBot : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f g : Filter β} [f.NeBot] [g.NeBot], (f -ᵥ g).NeBot
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.pseudofunctorOfIsLocallyDiscrete_obj : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory B]
  [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] [inst_2 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_5)
  (a : B),
  (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).obj
      a =
    obj a
-- Mathlib.Data.Finset.Image
/-- If a `Finset` of a subtype is converted to the main type with
`Embedding.subtype`, all elements of the result have the property of
the subtype.  -/
Finset.property_of_mem_map_subtype : ∀ {α : Type u_1} {p : α → Prop} (s : Finset { x // p x }) {a : α},
  a ∈ Finset.map (Function.Embedding.subtype fun x => p x) s → p a
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.instMul : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Monoid R] → [inst_1 : MulAction R M] → [inst_2 : Mul M] → [IsScalarTower R M M] → Mul (SubMulAction R M)
-- Init.Data.Slice.Notation
Std.Rco.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Rco β → γ) → Std.Rco.Sliceable α β γ
-- Init.Grind.Interactive
/-- `· grindSeq` focuses on the main `grind` goal and tries to solve it using the given
sequence of `grind` tactics.
 -/
Lean.Parser.Tactic.Grind.«grind·_» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.mul_subset : ∀ {M : Type u_3} [inst : Monoid M] {s t : Set M} {S : Submonoid M}, s ⊆ ↑S → t ⊆ ↑S → s * t ⊆ ↑S
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Writing explicitly the `n+1`-th derivative as the composition of a currying linear equiv,
and the `n`-th derivative of the derivative.  -/
iteratedFDerivWithin_succ_eq_comp_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : ℕ},
  UniqueDiffOn 𝕜 s →
    x ∈ s →
      iteratedFDerivWithin 𝕜 (n + 1) f s x =
        (⇑(continuousMultilinearCurryRightEquiv' 𝕜 n E F).symm ∘
            iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s)
          x
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.slt_eq_ult : ∀ {w : ℕ} (x y : BitVec w), x.slt y = (!x.getLsbD (w - 1) == y.getLsbD (w - 1) ^^ x.ult y)
-- Init.Data.Format.Instances
instToFormatProd : {α : Type u} → {β : Type v} → [Std.ToFormat α] → [Std.ToFormat β] → Std.ToFormat (α × β)
-- Mathlib.Topology.Algebra.Ring.Basic
instIsTopologicalRingMulOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R],
  IsTopologicalRing Rᵐᵒᵖ
-- Lean.Data.DeclarationRange
Lean.instReprDeclarationLocation.repr : Lean.DeclarationLocation → ℕ → Std.Format
-- Init.Data.List.Pairwise
List.Pairwise.of_map : ∀ {β : Type u_1} {α : Type u_2} {R : α → α → Prop} {l : List α} {S : β → β → Prop} (f : α → β),
  (∀ (a b : α), S (f a) (f b) → R a b) → List.Pairwise S (List.map f l) → List.Pairwise R l
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.congr_ac : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ μ₂ ν ν₂ : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous μ₂ →
    μ₂.AbsolutelyContinuous μ →
      ν.AbsolutelyContinuous ν₂ → ν₂.AbsolutelyContinuous ν → (μ.MutuallySingular ν ↔ μ₂.MutuallySingular ν₂)
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Generalised ultrametric triangle inequality for finite sums in additive
commutative groups with an ultrametric norm.  -/
IsUltrametricDist.nnnorm_sum_le_of_forall_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M}
  {C : NNReal}, (∀ i ∈ s, ‖f i‖₊ ≤ C) → ‖∑ i ∈ s, f i‖₊ ≤ C
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Adjunction.IsMonoidal.leftAdjoint_ε : ∀ {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 : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G} {inst_4 : F.OplaxMonoidal}
  {inst_5 : G.LaxMonoidal} [self : adj.IsMonoidal],
  CategoryTheory.Functor.LaxMonoidal.ε G =
    CategoryTheory.CategoryStruct.comp (adj.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (G.map (CategoryTheory.Functor.OplaxMonoidal.η F))
-- Mathlib.RingTheory.NormalClosure
Ring.instIsIntegrallyClosedNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S] [Module.Finite R S],
  IsIntegrallyClosed (Ring.NormalClosure R S)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.rightKanExtension_hom_ext : ∀ {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]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasRightKanExtension F]
  {G : CategoryTheory.Functor D H} (γ₁ γ₂ : G ⟶ L.rightKanExtension F),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft γ₁) (L.rightKanExtensionCounit F) =
      CategoryTheory.CategoryStruct.comp (L.whiskerLeft γ₂) (L.rightKanExtensionCounit F) →
    γ₁ = γ₂