mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.UInt.Lemmas
USize.toFin.ofNat : ∀ {n : ℕ}, (USize.ofNat n).toFin = Fin.ofNat USize.size n
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.compProd_trim_condExpKernel : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] (hm : m ≤ mΩ),
  (μ.trim hm).compProd (ProbabilityTheory.condExpKernel μ m) = MeasureTheory.Measure.map Function.diag μ
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.RegularEpi.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (W : C) (left right : W ⟶ X)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp left f = CategoryTheory.CategoryStruct.comp right f)
      CategoryTheory.RegularEpi.w._autoParam)
  (isColimit : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f w)) (W_1 : C)
  (left_1 right_1 : W_1 ⟶ X)
  (w_1 :
    autoParam (CategoryTheory.CategoryStruct.comp left_1 f = CategoryTheory.CategoryStruct.comp right_1 f)
      CategoryTheory.RegularEpi.w._autoParam)
  (isColimit_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f w_1)),
  ({ W := W, left := left, right := right, w := w, isColimit := isColimit } =
      { W := W_1, left := left_1, right := right_1, w := w_1, isColimit := isColimit_1 }) =
    (W = W_1 ∧ left ≍ left_1 ∧ right ≍ right_1 ∧ isColimit ≍ isColimit_1)
-- Mathlib.Data.Finset.Sigma
Finset.sigmaLift_eq_empty : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  {f : ⦃i : ι⦄ → α i → β i → Finset (γ i)} {a : (i : ι) × α i} {b : (i : ι) × β i},
  Finset.sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.size_right_le_size_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₂.size ≤ (t₁ ∪ t₂).size
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerLeft_ε_η_assoc : ∀ {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) [inst_4 : F.Monoidal] (T : D) {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj T (CategoryTheory.MonoidalCategoryStruct.tensorUnit D) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft T (CategoryTheory.Functor.OplaxMonoidal.η F)) h) =
    h
-- Mathlib.Geometry.Manifold.ChartedSpace
chartedSpaceSelf_prod : ∀ {H : Type u} {H' : Type u_1} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'],
  prodChartedSpace H H H' H' = chartedSpaceSelf (H × H')
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.spanningCoe_induce_univ : ∀ {V : Type u_1} (G : SimpleGraph V), (SimpleGraph.induce Set.univ G).spanningCoe = G
-- Init.Data.Nat.Lemmas
Nat.pow_add_one' : ∀ {m n : ℕ}, m ^ (n + 1) = m * m ^ n
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_inv : ∀ {x : ENNReal}, x⁻¹.log = -x.log
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.self_le_maxD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k fallback : α},
  (cmp k ((t.insert k).maxD fallback)).isLE = true
-- Init.Data.BitVec.Bitblast
BitVec.add_sub_comm : ∀ {w : ℕ} {z x y : BitVec w}, x + y - z = x - z + y
-- Mathlib.Data.EReal.Inv
EReal.instDivInvOneMonoid : DivInvOneMonoid EReal
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α} {h : a ∈ m}, m.getKey a h = m.getKeyD a fallback
-- Mathlib.Combinatorics.Graph.Basic
Graph.instSymmCompatible : ∀ {α : Type u_1} {β : Type u_2}, Std.Symm Graph.Compatible
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
prodIsoPullback_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (prodIsoPullback X Y).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.terminal.from X)
          (CategoryTheory.Limits.terminal.from Y))
        h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.PreservesEqualizer.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasEqualizer f g]
  [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) G],
  (CategoryTheory.Limits.PreservesEqualizer.iso G f g).hom = CategoryTheory.Limits.equalizerComparison f g G
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
ContinuousAlgEquiv.mk.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (toAlgEquiv toAlgEquiv_1 : A ≃ₐ[R] B) (e_toAlgEquiv : toAlgEquiv = toAlgEquiv_1)
  (continuous_toFun : Continuous toAlgEquiv.toFun) (continuous_invFun : Continuous toAlgEquiv.invFun),
  { toAlgEquiv := toAlgEquiv, continuous_toFun := continuous_toFun, continuous_invFun := continuous_invFun } =
    { toAlgEquiv := toAlgEquiv_1, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Algebra.Group.Action.Opposite
/-- Like `Monoid.toMulAction`, but multiplies on the right.  -/
Monoid.toOppositeMulAction : {α : Type u_3} → [inst : Monoid α] → MulAction αᵐᵒᵖ α
-- Mathlib.Algebra.Group.Basic
eq_mul_of_mul_inv_eq : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, a * c⁻¹ = b → a = b * c
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.isSimpleHOFun : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.of_free_prod : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type w)
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Finite R N] [Module.Free R N] [Module.Free R (M × N)],
  Module.IsStablyFree R M
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.sup_le' : ∀ {G : Type w} [inst : TopologicalSpace G] (self : MeasureTheory.Content G) (K₁ K₂ : TopologicalSpace.Compacts G),
  self.toFun (K₁ ⊔ K₂) ≤ self.toFun K₁ + self.toFun K₂
-- Init.Data.Range.Polymorphic.Nat
Std.instLawfulRcoIntersectionNat : Std.Roo.LawfulRcoIntersection ℕ
-- Init.Data.Nat.Div.Basic
Nat.add_div_right : ∀ (x : ℕ) {z : ℕ}, 0 < z → (x + z) / z = x / z + 1
-- Init.Prelude
Applicative.toSeqLeft : {f : Type u → Type v} → [self : Applicative f] → SeqLeft f
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.regularMonoCategoryOfSplitMonoCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.SplitMonoCategory C],
  CategoryTheory.IsRegularMonoCategory C
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- Returns `true` if `s₁` and `s₂` have at least one variable in common.
The function assumes both of them are sorted.
 -/
Lean.Grind.AC.Seq.sharesVar : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- A measure is called s-finite if it is a countable sum of finite measures.  -/
MeasureTheory.SFinite : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Prop
-- Mathlib.AlgebraicGeometry.Morphisms.Affine
AlgebraicGeometry.isAffineHom_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsAffineHom
-- Mathlib.Topology.Sheaves.AddCommGrpCat
TopCat.Sheaf.sections_exact_of_left_exact : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} {S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)},
  S.Exact →
    CategoryTheory.Mono S.f →
      ∀ (s : ↑(S.X₂.obj.obj (Opposite.op U))),
        (CategoryTheory.ConcreteCategory.hom (S.g.hom.app (Opposite.op U))) s = 0 →
          ∃ t, (CategoryTheory.ConcreteCategory.hom (S.f.hom.app (Opposite.op U))) t = s
-- Mathlib.Order.Defs.PartialOrder
le_of_eq_or_lt' : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a = b ∨ b < a → b ≤ a
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.evenOdd.gradedMonoid : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), SetLike.GradedMonoid (CliffordAlgebra.evenOdd Q)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.image_baseOf_inv_comp_eq : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S] [inst_2 : InvolutiveInv ι]
  [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G),
  (∀ (i : ι), v i⁻¹ = (v i)⁻¹) →
    ∀ (f : G →* S),
      v '' IsMulIndecomposable.baseOf v (invMonoidHom.comp f) = ⇑invMonoidHom ∘ v '' IsMulIndecomposable.baseOf v f
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.instInhabited : {d : ℤ} → Inhabited (ℤ√d)
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
IsNonarchimedean.add_eq_right_of_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} [inst_2 : AddGroup α]
  [inst_3 : FunLike F α R] [AddGroupSeminormClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {x y : α}, f x < f y → f (x + y) = f y
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toAlgEquiv_injective : ∀ {R : Type u_6} {A : Type u_7} {B : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Star A] [inst_6 : Star B],
  Function.Injective StarAlgEquiv.toAlgEquiv
-- Mathlib.Order.Category.BddOrd
/-- The equivalence between `BddOrd` and itself induced by `OrderDual` both ways.  -/
BddOrd.dualEquiv : BddOrd ≌ BddOrd
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_min_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  {s : Multiset ι} {f g : ι → α},
  (Multiset.map (fun i => min (f i) (g i)) s).sum ≤ min (Multiset.map f s).sum (Multiset.map g s).sum
-- Init.Data.Nat.Lemmas
Nat.succ_add_sub_one : ∀ (n m : ℕ), m.succ + n - 1 = m + n
-- Lean.Meta.Basic
/-- Return the array of postponed universe level constraints.  -/
Lean.Meta.getPostponed : Lean.MetaM (Lean.PersistentArray Lean.Meta.PostponedEntry)
-- Batteries.Data.AssocList
Batteries.AssocList.forIn.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {δ : Type u_1} [inst : Monad m] (init : δ)
  (f : α × β → δ → m (ForInStep δ)), Batteries.AssocList.nil.forIn init f = pure init
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Coloring.sumRight_sum : ∀ {V : Type u_3} {W : Type u_5} {γ : Type u_7} {G : SimpleGraph V} {H : SimpleGraph W} (cG : G.Coloring γ)
  (cH : H.Coloring γ), (cG.sum cH).sumRight = cH
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_eq_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, t.contains k = true → t.get! k = k
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- [Stacks Tag 09HX](https://stacks.math.columbia.edu/tag/09HX) (This theorem is stronger than 09HX. It removes the abelian condition, and requires only `≤` instead of `=`.) -/
isCyclic_of_card_pow_eq_one_le : ∀ {α : Type u_1} [inst : Group α] [inst_1 : DecidableEq α] [inst_2 : Fintype α],
  (∀ (n : ℕ), 0 < n → {a | a ^ n = 1}.card ≤ n) → IsCyclic α
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- Given an adjunction `L ⊣ R`, if `R ⋙ L` is abstractly isomorphic to the identity functor, then the
counit is an isomorphism.
 -/
CategoryTheory.Adjunction.counitAsIsoOfIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} →
            (L ⊣ R) → (R.comp L ≅ CategoryTheory.Functor.id D) → (R.comp L ≅ CategoryTheory.Functor.id D)
-- Mathlib.Topology.Instances.Int
Int.instIsOrderBornology : IsOrderBornology ℤ
-- Mathlib.Logic.Hydra
Relation.cutExpand_add_right : ∀ {α : Type u_1} {r : α → α → Prop} {s' s : Multiset α} (t : Multiset α),
  Relation.CutExpand r (s' + t) (s + t) ↔ Relation.CutExpand r s' s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendBit.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget aig w → Sort u_1) →
            (target : Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget aig w) →
              ((start : ℕ) → (x : aig.RefVec w) → motive { start := start, x := x }) → motive target
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionClientCapabilities.mk : Option Lean.Lsp.CompletionItemCapabilities → Lean.Lsp.CompletionClientCapabilities
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitization_nnnorm_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A]
  (x : A), ‖WithLp.toLp 1 ↑x‖₊ = ‖x‖₊
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.smul : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : SMul M X] [ContinuousSMul M X] {f : α → M} {g : α → X} {l : Filter α} {c : M} {a : X},
  Filter.Tendsto f l (nhds c) → Filter.Tendsto g l (nhds a) → Filter.Tendsto (fun x => f x • g x) l (nhds (c • a))
-- Lean.Parser.Syntax
Lean.Parser.Command.binderPredicate.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A] {Z : A}
  (h : ι.obj ((Λ.chainComplex X).X 0) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ι.map ((Λ.chainComplex X).d 1 0)) h =
    CategoryTheory.CategoryStruct.comp (ι.map (Λ.chainComplexXOneIso X).hom)
      (CategoryTheory.CategoryStruct.comp (Λ.π.app (CategoryTheory.Limits.kernel (Λ.π.app X)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (Λ.π.app X))
          (CategoryTheory.CategoryStruct.comp (ι.map (Λ.chainComplexXZeroIso X).inv) h)))
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.div_right : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s t : Set α},
  IsUpperSet s → IsUpperSet (s / t)
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.flip_X_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (i : I₂) (j j' : I₁), (K.flip.X i).d j j' = (K.d j j').f i
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_aeval_eq_zero : ∀ {S : Type v} {A : Type u_1} [inst : CommSemiring S] [inst_1 : Semiring A] [inst_2 : Algebra S A] {f : Polynomial S}
  {z : A},
  (Polynomial.aeval z) f = 0 →
    (∀ (x : S), (algebraMap S A) x = 0 → x = 0) →
      (Polynomial.aeval ((algebraMap S A) f.leadingCoeff * z)) f.integralNormalization = 0
-- Mathlib.Data.Rat.Cast.Lemmas
NNRat.cast_zpow_of_ne_zero : ∀ {K : Type u_1} [inst : DivisionSemiring K] (q : ℚ≥0) (z : ℤ), ↑q.num ≠ 0 → ↑(q ^ z) = ↑q ^ z
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- If `B` is a (2,1)-category, then every oplax functor `F` from a bicategory to `B` defines
a `CategoryTheory.OplaxFunctor.PseudoCore` structure on `F` that can be used to promote `F`
to a pseudofunctor using `CategoryTheory.Pseudofunctor.mkOfOplax`.  -/
CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {B' : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory B'] →
        [CategoryTheory.Bicategory.IsLocallyGroupoid B] → (F : CategoryTheory.OplaxFunctor B' B) → F.PseudoCore
-- ProofWidgets.Component.Basic
/-- Construct a structured message from a ProofWidgets component.

For the meaning of `alt`, see `MessageData.ofWidget`.  -/
Lean.MessageData.ofComponent : {Props : Type} →
  [Lean.Server.RpcEncodable Props] → ProofWidgets.Component Props → Props → String → Lean.CoreM Lean.MessageData
-- Mathlib.Order.Heyting.Basic
sdiff_le : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b : α}, a \ b ≤ a
-- Mathlib.Data.EReal.Operations
EReal.add_ne_top_iff_of_ne_bot_of_ne_top : ∀ {x y : EReal}, y ≠ ⊥ → y ≠ ⊤ → (x + y ≠ ⊤ ↔ x ≠ ⊤)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.comp_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] {P : Type u_1}
  [inst_2 : L.Structure P] (hnp : L.Equiv N P) (hmn : L.Equiv M N),
  (hnp.comp hmn).toEmbedding = hnp.toEmbedding.comp hmn.toEmbedding
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.sinKernel_zero : ∀ (x : ℝ), HurwitzZeta.sinKernel 0 x = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryLE_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, (compare a k).isLE = true},
  Std.DTreeMap.Internal.Impl.getEntryLE k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.getEntryLE k t₂ ⋯ ⋯
-- Mathlib.Geometry.Manifold.Algebra.SMul
/-- The scalar multiplication `𝕜 × E → E` of any normed vector space `E` over `𝕜` is smooth.  -/
instContMDiffSMulModelWithCornersSelf : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞}, ContMDiffSMul (modelWithCornersSelf 𝕜 𝕜) (modelWithCornersSelf 𝕜 E) n 𝕜 E
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryLED_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : α × β},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryLED t₁ k fallback = Std.DTreeMap.Raw.Const.getEntryLED t₂ k fallback
-- Mathlib.AlgebraicGeometry.Geometrically.Connected
AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyConnectedOfUniversallyOpen_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyConnected g]
  [AlgebraicGeometry.UniversallyOpen g] [ConnectedSpace ↥X], ConnectedSpace ↥(CategoryTheory.Limits.pullback f g)
-- Lean.Meta.Basic
/-- Lift a `MkBindingM` monadic action `x` to `MetaM`.
 -/
Lean.Meta.liftMkBindingM : {α : Type} → Lean.MetavarContext.MkBindingM α → Lean.MetaM α
-- Mathlib.Topology.Algebra.Group.Pointwise
add_singleton_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : AddGroup α] [ContinuousConstVAdd αᵃᵒᵖ α] {s : Set α} (a : α)
  {b : α}, s ∈ nhds b → s + {a} ∈ nhds (b + a)
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Sieve.equalizer_eq_equalizerSieve : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {U V : C} (f₁ f₂ : U ⟶ V),
  CategoryTheory.Sieve.equalizer f₁ f₂ = CategoryTheory.Presheaf.equalizerSieve f₁ f₂
-- Init.Data.Range.Polymorphic.IntLemmas
Int.zero_lt_getElem!_toArray_roc_iff : ∀ {m n : ℤ} {i : ℕ}, (m<...=n).toArray[i]! ≠ 0 ↔ i < (n - m).toNat ∧ m + ↑i ≠ -1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_zero_of_head_neg : ∀ {exps_hd : ℝ} {exps_tl : Tactic.ComputeAsymptotics.UnitMonomial} {basis_hd : ℝ → ℝ}
  {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl) →
    exps_hd < 0 →
      Filter.Tendsto (Tactic.ComputeAsymptotics.UnitMonomial.toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl))
        Filter.atTop (nhds 0)
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- If a measurable space is countably generated and equipped with a `σ`-finite measure, then the
measure is separable. This is not an instance because it is used below to prove the more
general case where `μ` is s-finite.  -/
MeasureTheory.isSeparable_of_sigmaFinite : ∀ {X : Type u_1} [m : MeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasurableSpace.CountablyGenerated X]
  [MeasureTheory.SigmaFinite μ], MeasureTheory.IsSeparable μ
-- Lean.Elab.ComputedFields
Lean.Elab.ComputedFields.Context.indices : Lean.Elab.ComputedFields.Context → Array Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- **Alias** of `CategoryTheory.Limits.Fan.IsLimit.mk`.

---

Make a fan `f` into a limit fan by providing `lift`, `fac`, and `uniq` --
just a convenience lemma to avoid having to go through `Discrete`  -/
CategoryTheory.Limits.mkFanLimit : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f : β → C} →
        (t : CategoryTheory.Limits.Fan f) →
          (lift : (s : CategoryTheory.Limits.Fan f) → s.pt ⟶ t.pt) →
            autoParam
                (∀ (s : CategoryTheory.Limits.Fan f) (j : β),
                  CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j)
                CategoryTheory.Limits.Fan.IsLimit.mk._auto_1 →
              autoParam
                  (∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt ⟶ t.pt),
                    (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s)
                  CategoryTheory.Limits.Fan.IsLimit.mk._auto_3 →
                CategoryTheory.Limits.IsLimit t
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.coe_toSubmonoid_apply : ∀ {A : Type u_4} [inst : AddZeroClass A] (S : AddSubmonoid A),
  ↑(AddSubmonoid.toSubmonoid S) = ⇑Multiplicative.toAdd ⁻¹' ↑S
-- Mathlib.CategoryTheory.Yoneda
/-- `FullyFaithful.homEquiv` as a natural isomorphism.  -/
CategoryTheory.Functor.FullyFaithful.homNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          F.FullyFaithful →
            (X : C) →
              F.op.comp (CategoryTheory.uliftYoneda.{v₁, v₂, u₂}.obj (F.obj X)) ≅
                CategoryTheory.uliftYoneda.{v₂, v₁, u₁}.obj X
-- Mathlib.Algebra.Lie.Nilpotent
LieAlgebra.isSolvable_of_isNilpotent : ∀ (L : Type v) [inst : LieRing L] [hL : LieModule.IsNilpotent L L], LieAlgebra.IsSolvable L
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.cmp.match_1.eq_2 : ∀ (motive : ONote → ONote → Sort u_1) (x : ONote) (h_1 : Unit → motive ONote.zero ONote.zero)
  (h_2 : (x : ONote) → motive x ONote.zero) (h_3 : (x : ONote) → motive ONote.zero x)
  (h_4 :
    (_o₁ e₁ : ONote) →
      (n₁ : ℕ+) →
        (a₁ : ONote) →
          _o₁ = e₁.oadd n₁ a₁ →
            (_o₂ e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → _o₂ = e₂.oadd n₂ a₂ → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)),
  (x = ONote.zero → False) →
    (match x, ONote.zero with
      | ONote.zero, ONote.zero => h_1 ()
      | x, ONote.zero => h_2 x
      | ONote.zero, x => h_3 x
      | _o₁@h:(e₁.oadd n₁ a₁), _o₂@h_5:(e₂.oadd n₂ a₂) => h_4 _o₁ e₁ n₁ a₁ h _o₂ e₂ n₂ a₂ h_5) =
      h_2 x