mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.insertIdx.loop : {α : Type u} → ℕ → (as : Array α) → Fin as.size → Array α
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.homInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (M : CategoryTheory.AddMon C) → Inhabited (M.Hom M)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.comp_continuous_iff : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] {α : Type u_8} [inst_10 : TopologicalSpace α] (e : M₁ ≃SL[σ₁₂] M₂)
  {f : α → M₁}, Continuous (⇑e ∘ f) ↔ Continuous f
-- Std.Http.Data.Chunk
Std.Http.Trailer.mk : Std.Http.Headers → Std.Http.Trailer
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Computation.BisimO.match_1.eq_3 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (x x_1 : α ⊕ Computation α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_2 : α ⊕ Computation α) → motive x x_2),
  (∀ (a a' : α), x = Sum.inl a → x_1 = Sum.inl a' → False) →
    (∀ (s s' : Computation α), x = Sum.inr s → x_1 = Sum.inr s' → False) →
      (match x, x_1 with
        | Sum.inl a, Sum.inl a' => h_1 a a'
        | Sum.inr s, Sum.inr s' => h_2 s s'
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of limits along a natural isomorphism in the diagram.  -/
CategoryTheory.Limits.reflectsLimit_of_iso_diagram : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K₁ K₂ : CategoryTheory.Functor J C}
  (F : CategoryTheory.Functor C D) (h : K₁ ≅ K₂) [CategoryTheory.Limits.ReflectsLimit K₁ F],
  CategoryTheory.Limits.ReflectsLimit K₂ F
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.basis.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f),
  h.basis =
    {
      repr :=
        { toFun := fun x => Finsupp.comapDomain Fin.val (h.modByMonicHom x).toFinsupp.coeff ⋯, map_add' := ⋯,
          map_smul' := ⋯,
          invFun := fun g => h.map { toFinsupp := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain Fin.val g) },
          left_inv := ⋯, right_inv := ⋯ } }
-- Lean.Meta.Tactic.Grind.Types
/-- Current source of tracking E-matching theorem instantiation (see `grind.ematch.instances`).  -/
Lean.Meta.Grind.Context.ematchDiagSource : Lean.Meta.Grind.Context → Lean.Meta.Grind.EMatchDiagSource
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of `x` is the set of points that can be joined to `x`.  -/
pathComponent : {X : Type u_1} → [TopologicalSpace X] → X → Set X
-- Mathlib.Data.Set.Card
Set.exists_subset_or_subset_of_two_mul_lt_ncard : ∀ {α : Type u_1} {s t : Set α} {n : ℕ}, 2 * n < (s ∪ t).ncard → ∃ r, n < r.ncard ∧ (r ⊆ s ∨ r ⊆ t)
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.CompleteEquipartiteSubgraph.ext : ∀ {V : Type u_1} {G : SimpleGraph V} {r t : ℕ} {x y : G.CompleteEquipartiteSubgraph r t}, x.parts = y.parts → x = y
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
toDegLex_inj : ∀ {α : Type u_1} {a b : α}, toDegLex a = toDegLex b ↔ a = b
-- Mathlib.Topology.Category.Profinite.AsLimit
/-- A cone over `X.diagram` whose cone point is `X`.  -/
Profinite.asLimitCone : (X : Profinite) → CategoryTheory.Limits.Cone X.diagram
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (l l_1 : Std.ExtTreeSet α cmp),
  l = l_1 → ∀ (a a_1 : α), a = a_1 → l.contains a = l_1.contains a_1
-- Mathlib.Topology.Category.Locale
Locale.instCoeSortType : CoeSort Locale (Type u_1)
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesRightKanExtensionAt F L c` asserts that `G` preserves all right pointwise right Kan
extensions of `F` along `L` at `c`.  -/
CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A B → CategoryTheory.Functor A C → C → Prop
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- The category of seminormed abelian groups and bounded group homomorphisms.  -/
SemiNormedGrp : Type (u + 1)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instSMulCommClass_1 : ∀ {α : Type u} {β : Type v} {𝕜 : Type u_1} [inst : PseudoMetricSpace 𝕜] [inst_1 : TopologicalSpace α]
  [inst_2 : NonUnitalSeminormedRing β] [inst_3 : Zero 𝕜] [inst_4 : SMul 𝕜 β] [inst_5 : IsBoundedSMul 𝕜 β]
  [SMulCommClass 𝕜 β β], SMulCommClass 𝕜 (BoundedContinuousFunction α β) (BoundedContinuousFunction α β)
-- Lean.Elab.Do.Basic
/-- Construct `m α` from `α`.  -/
Lean.Elab.Do.DoOps.mkMonadApp : Lean.Elab.Do.DoOps → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.id_toNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Comonad C),
  (CategoryTheory.CategoryStruct.id T).toNatTrans = CategoryTheory.CategoryStruct.id T.toFunctor
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
_private.Mathlib.RingTheory.WittVector.DiscreteValuationRing.0.WittVector.inverseCoeff.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- On any local site with morphism types in `Type v`, the global sections functor to any category
with colimits and products of size `v` is a left adjoint. See `ΓIsLeftAdjoint` for a
version for `w`-locally small sites that can't be registered as an instance because of the extra
universe parameter `w`.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.instIsLeftAdjointSheafΓOfHasColimitsOfSizeOfHasProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.IsLocalSite] (A : Type u') [inst_2 : CategoryTheory.Category.{v', u'} A]
  [CategoryTheory.Limits.HasColimitsOfSize.{v, v, v', u'} A] [CategoryTheory.Limits.HasProducts A]
  [inst_5 : CategoryTheory.HasWeakSheafify J A], (CategoryTheory.Sheaf.Γ J A).IsLeftAdjoint
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.toFiniteSpanningSetsIn.congr_simp : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [h : MeasureTheory.SigmaFinite μ],
  μ.toFiniteSpanningSetsIn = μ.toFiniteSpanningSetsIn
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.comapₐ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : CommSemiring R] [inst_3 : Semiring Z] [inst_4 : Algebra R Z] (f : C(X, Y)) (g : LocallyConstant Y Z)
  (a : X), ((LocallyConstant.comapₐ R f) g) a = g (f a)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- **Alias** of `UpperHalfPlane.coe_inj`. -/
UpperHalfPlane.ext_iff' : ∀ {a b : UpperHalfPlane}, ↑a = ↑b ↔ a = b
-- Mathlib.Analysis.Analytic.Basic
/-- `f` is analytic within `s` if it is analytic within `s` at each point of `s`.  Note that
this is weaker than `AnalyticOnNhd 𝕜 f s`, as `f` is allowed to be arbitrary outside `s`.  -/
AnalyticOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → Set E → Prop
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.Sign.plus.sizeOf_spec : ∀ {v : Lean.Level} {M : Q(Type v)}, sizeOf Mathlib.Tactic.FieldSimp.Sign.plus = 1
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} (hfi : MeasureTheory.Integrable f μ),
  μ.withDensityᵥ f =
    (μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure -
      (μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure
-- Lean.Message
Lean.NamingContext.mk.injEq : ∀ (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (currNamespace_1 : Lean.Name)
  (openDecls_1 : List Lean.OpenDecl),
  ({ currNamespace := currNamespace, openDecls := openDecls } =
      { currNamespace := currNamespace_1, openDecls := openDecls_1 }) =
    (currNamespace = currNamespace_1 ∧ openDecls = openDecls_1)
-- Init.Data.List.Lemmas
List.getElem?_dropLast : ∀ {α : Type u_1} {xs : List α} {i : ℕ}, xs.dropLast[i]? = if i < xs.length - 1 then xs[i]? else none
-- Mathlib.Analysis.Normed.Module.Ball.Action
mulActionClosedBallClosedBall : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [NormedSpace 𝕜 E] → {r : ℝ} → MulAction ↑(Metric.closedBall 0 1) ↑(Metric.closedBall 0 r)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instCommMonoidQuotient : {R : Type u_1} → [inst : Add R] → [inst_1 : CommMonoid R] → (c : RingCon R) → CommMonoid c.Quotient
-- Mathlib.Lean.Meta.CongrTheorems
/-- Runs `mx` in a context where all local `Subsingleton` and `IsEmpty` instances
have associated `FastSubsingleton` and `FastIsEmpty` instances.
The function passed to `mx` eliminates these instances from expressions,
since they are only locally valid inside this context.
 -/
Lean.Meta.withSubsingletonAsFast : {α : Type} → [Inhabited α] → ((Lean.Expr → Lean.Expr) → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Data.Rel
SetRel.instIsSymmInv : ∀ {α : Type u_1} {R : SetRel α α} [R.IsSymm], R.inv.IsSymm
-- Lean.Level
Lean.instForInLMVarIdMapProdLMVarIdOfMonad : {m : Type u_1 → Type u_2} → {α : Type} → [Monad m] → ForIn m (Lean.LMVarIdMap α) (Lean.LMVarId × α)
-- Mathlib.Topology.Constructions
Pi.topologicalSpace : {ι : Type u_5} → {Y : ι → Type v} → [t₂ : (i : ι) → TopologicalSpace (Y i)] → TopologicalSpace ((i : ι) → Y i)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.instOrderTop : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → OrderTop (J.Cover X)
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.isOpenEmbedding_f_zeroHypercover : ∀ {X : TopCat} (E : TopCat.precoverage.ZeroHypercover X) (i : E.I₀),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (E.f i))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth w len : ℕ}
  (oldLayer : aig.RefVec (len * w)) (h : outWidth = (len + 1) / 2 * w) (hlen : 0 < len) (w_1 len_1 : ℕ)
  (oldLayer_1 : aig.RefVec (len_1 * w_1)) (h_1 : outWidth = (len_1 + 1) / 2 * w_1) (hlen_1 : 0 < len_1),
  ({ w := w, len := len, oldLayer := oldLayer, h := h, hlen := hlen } =
      { w := w_1, len := len_1, oldLayer := oldLayer_1, h := h_1, hlen := hlen_1 }) =
    (w = w_1 ∧ len = len_1 ∧ oldLayer ≍ oldLayer_1)
-- Mathlib.Algebra.Notation.Pi.Basic
/-- On non-dependent functions, `Pi.mulSingle` can be expressed as an `ite`  -/
Pi.mulSingle_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : Type u_9} [inst_1 : One M] (i : ι) (x : M) (i' : ι),
  Pi.mulSingle i x i' = if i' = i then x else 1
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_insert_of_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v v' : α} [Std.TransCmp cmp] (t : RBTree.RBSet α cmp),
  cmp v v' = Ordering.eq → v' ∈ t.insert v
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- **Alias** of the forward direction of `SimpleGraph.chromaticNumber_eq_zero_iff`. -/
SimpleGraph.isEmpty_of_chromaticNumber_eq_zero : ∀ {V : Type u} {G : SimpleGraph V}, G.chromaticNumber = 0 → IsEmpty V
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.constComp_hom_app : ∀ (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] (X : C) (F : CategoryTheory.Functor C D) (x : J),
  (CategoryTheory.Functor.constComp J X F).hom.app x =
    CategoryTheory.CategoryStruct.id ((((CategoryTheory.Functor.const J).obj X).comp F).obj x)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- `RingFunc.zero`, but with the defeq type `Language.ring.Functions 0` instead
of `RingFunc 0`  -/
FirstOrder.Ring.zeroFunc : FirstOrder.Language.ring.Functions 0
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_sub_iff_add_le_left : ∀ {a b c : ENNReal}, c ≠ ⊤ → c ≤ b → (a ≤ b - c ↔ c + a ≤ b)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
/-- Inserts an `Option` case distinction after the first computation of a call to `MonadAttach.pbind`.
This lemma is useful for simplifying the second computation, which often involves `match` expressions
that use `pbind`'s proof term.
 -/
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.pbind_eq_pbind_if_isSome : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] (x : m (Option α))
  (f : (x_1 : Option α) → MonadAttach.CanReturn x x_1 → m β),
  MonadAttach.pbind x f =
    MonadAttach.pbind x fun a ha => Std.Internal.optionPelim'✝ a (fun x_1 => f none ⋯) fun a_1 x_1 => f (some a_1) ⋯
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.percent.injEq : ∀ (p p_1 : Aesop.Percent), (Aesop.Frontend.Priority.percent p = Aesop.Frontend.Priority.percent p_1) = (p = p_1)
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.InftyValuation.map_mul' : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] (x y : RatFunc F),
  RatFunc.inftyValuationDef F (x * y) = RatFunc.inftyValuationDef F x * RatFunc.inftyValuationDef F y
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_cancel_of_tmod_eq_zero : ∀ {a b : ℤ}, a.tmod b = 0 → b * a.tdiv b = a
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₃_app_three : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  (app₀ : f.obj' 0 _proof_297✝ ⟶ g.obj' 0 _proof_297✝) (app₁ : f.obj' 1 _proof_298✝ ⟶ g.obj' 1 _proof_298✝)
  (app₂ : f.obj' 2 _proof_299✝ ⟶ g.obj' 2 _proof_299✝) (app₃ : f.obj' 3 _proof_300✝ ⟶ g.obj' 3 _proof_300✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_298✝))
      _auto_325✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_299✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_299✝))
      _auto_327✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_300✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_300✝))
      _auto_329✝),
  (CategoryTheory.ComposableArrows.homMk₃ app₀ app₁ app₂ app₃ w₀ w₁ w₂).app
      ⟨3, CategoryTheory.ComposableArrows.homMk₃._proof_4⟩ =
    app₃
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- When `D` is a monoidal category,
comonoid objects in `C ⥤ D` are the same thing
as functors from `C` into the comonoid objects of `D`.
 -/
CategoryTheory.Monoidal.comonFunctorCategoryEquivalence : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Comon (CategoryTheory.Functor C D) ≌ CategoryTheory.Functor C (CategoryTheory.Comon D)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.compare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {f : β → β}, cmp (t.modify k f).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.comp_liftNatTrans : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F₁ F₂ F₃ : CategoryTheory.Functor C E) (F₁' F₂' F₃' : CategoryTheory.Functor D E)
  [h₁ : CategoryTheory.Localization.Lifting L W F₁ F₁'] [h₂ : CategoryTheory.Localization.Lifting L W F₂ F₂']
  [h₃ : CategoryTheory.Localization.Lifting L W F₃ F₃'] (τ : F₁ ⟶ F₂) (τ' : F₂ ⟶ F₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ)
      (CategoryTheory.Localization.liftNatTrans L W F₂ F₃ F₂' F₃' τ') =
    CategoryTheory.Localization.liftNatTrans L W F₁ F₃ F₁' F₃' (CategoryTheory.CategoryStruct.comp τ τ')
-- Lean.Data.PrefixTree
_private.Lean.Data.PrefixTree.0.Lean.PrefixTreeNode.insert.insertEmpty : {α : Type u_1} → {β : Type u_2} → (cmp : α → α → Ordering) → β → List α → Lean.PrefixTreeNode α β cmp
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- Eta-expanded form of `HasDerivWithinAt.mul` -/
HasDerivWithinAt.fun_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c d : 𝕜 → 𝔸} {c' d' : 𝔸},
  HasDerivWithinAt c c' s x →
    HasDerivWithinAt d d' s x → HasDerivWithinAt (fun i => c i * d i) (c' * d x + c x * d') s x
-- Init.Data.Order.LemmasExtra
Classical.Order.instLawfulOrderOrd : ∀ {α : Type u} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2], Std.LawfulOrderOrd α
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.card_le : ∀ {L : FirstOrder.Language} {α : Type u'},
  Cardinal.mk ((n : ℕ) × L.BoundedFormula α n) ≤
    max Cardinal.aleph0 (Cardinal.lift.{max u v, u'} (Cardinal.mk α) + Cardinal.lift.{u', max u v} L.card)
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.Etale f],
  AlgebraicGeometry.Etale (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.add : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f g : ℝ → ε} {a b : ℝ}
  {μ : MeasureTheory.Measure ℝ} [ContinuousAdd ε],
  IntervalIntegrable f μ a b → IntervalIntegrable g μ a b → IntervalIntegrable (fun x => f x + g x) μ a b
-- Lean.Elab.InfoTree.Types
/-- Denotes TermInfo with additional configurations to control interactions with delaborated terms.

For example, the omission term `⋯` that is emitted by the delaborator when omitting a term
due to `pp.deepTerms false` or `pp.proofs false` uses this.
Omission needs to be treated differently from regular terms because
it has to be delaborated differently in `Lean.Widget.InteractiveDiagnostics.infoToInteractive`:
Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with
regular delaboration settings. Additionally, omissions come with a reason for omission.
 -/
Lean.Elab.DelabTermInfo : Type
-- Init.Data.UInt.Lemmas
UInt64.ofNat_bitVecToNat : ∀ (n : BitVec 64), UInt64.ofNat n.toNat = { toBitVec := n }
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.toSubgraph_verts : ∀ {V : Type u} {G : SimpleGraph V} (H : SimpleGraph V) (h : H ≤ G), (SimpleGraph.toSubgraph H h).verts = Set.univ
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.betaPDFReal.eq_1 : ∀ (α β x : ℝ),
  ProbabilityTheory.betaPDFReal α β x =
    if 0 < x ∧ x < 1 then 1 / ProbabilityTheory.beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.addSubgroup_strictAntiOn : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  StrictAntiOn ArchimedeanClass.addSubgroup (Set.Iio ⊤)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.commRing : {R : Type u_1} → {M : Type u_4} → [inst : CommRing R] → [CommMonoid M] → CommRing (MonoidAlgebra R M)
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
MDifferentiable.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H')
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (f : M → M'),
  MDiff f = ∀ (x : M), MDiffAt f x
-- Init.Data.String.Bootstrap
String.Internal.getUTF8Byte : (s : String) → (n : ℕ) → n < s.utf8ByteSize → UInt8
-- Mathlib.Tactic.Translate.Core
/-- An optional flag stating that the target of the translation is the target itself.
This can be used to reorder arguments, such as in
`attribute [to_dual self (reorder := 3 4)] LE.le`.
If `self := true`, we should also have `existing := true`.  -/
Mathlib.Tactic.Translate.Config.self : Mathlib.Tactic.Translate.Config → Bool
-- Mathlib.CategoryTheory.Comma.Arrow
/-- Given a square from an arrow `i` to an isomorphism `p`, express the source part of `sq`
in terms of the inverse of `p`.  -/
CategoryTheory.Arrow.square_to_iso_invert : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] (i : CategoryTheory.Arrow T) {X Y : T} (p : X ≅ Y)
  (sq : i ⟶ CategoryTheory.Arrow.mk p.hom),
  CategoryTheory.CategoryStruct.comp i.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) p.inv) =
    CategoryTheory.Arrow.Hom.left sq
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toExtensionHom_id : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), (Algebra.Generators.Hom.id P).toExtensionHom = Algebra.Extension.Hom.id P.toExtension
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
/-- If `r` has no zero smul divisors for all small-enough sections, then `r` has no zero smul divisors
in the colimit.
 -/
CategoryTheory.Limits.Concrete.colimit_no_zero_smul_divisor : ∀ (R : Type u_1) [inst : Ring R] {J : Type w} [inst_1 : CategoryTheory.Category.{r, w} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget (ModuleCat R))] [CategoryTheory.IsFiltered J]
  [inst_4 : CategoryTheory.Limits.HasColimit F] (r : R),
  (∃ j', ∀ (j : J) (x : j' ⟶ j) (c : ↑(F.obj j)), r • c = 0 → c = 0) →
    ∀ (x : CategoryTheory.ToType (CategoryTheory.Limits.colimit F)), r • x = 0 → x = 0
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoLocallyUniformly.mul` -/
TendstoLocallyUniformly.fun_mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l → TendstoLocallyUniformly (fun i i_1 => F i i_1 * G i i_1) (fun i => f i * g i) l
-- Mathlib.Algebra.Ring.ULift
ULift.addCommGroupWithOne : {R : Type u} → [AddCommGroupWithOne R] → AddCommGroupWithOne (ULift.{u_1, u} R)