mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- `DifferentiableOn 𝕜 f s` means that `f` is differentiable within `s` at any point of `s`.  -/
DifferentiableOn : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : AddCommGroup E] →
        [Module 𝕜 E] →
          [TopologicalSpace E] →
            {F : Type u_3} → [inst_4 : AddCommGroup F] → [Module 𝕜 F] → [TopologicalSpace F] → (E → F) → Set E → Prop
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
/-- There is an explicit change of variables of a `WeierstrassCurve` to
a short normal form, provided that 2 and 3 are invertible in the ring.
It is the composition of an explicit change of variables with `WeierstrassCurve.toCharNeTwoNF`.  -/
WeierstrassCurve.toShortNF : {R : Type u_1} →
  [inst : CommRing R] → WeierstrassCurve R → [Invertible 2] → [Invertible 3] → WeierstrassCurve.VariableChange R
-- Mathlib.Algebra.Category.MonCat.Basic
/-- The forgetful functor from `AddCommMonCat` to `AddMonCat` is fully faithful.  -/
AddCommMonCat.fullyFaithfulForgetToAddMonCat : (CategoryTheory.forget₂ AddCommMonCat AddMonCat).FullyFaithful
-- Init.Data.String.Slice
/-- Finds the position of the first match of the pattern `pat` in a slice `s`. If there
is no match `none` is returned.

This function is generic over all currently supported patterns.

Examples:

* `("coffee tea water".toSlice.find? Char.isWhitespace).map (·.get!) == some ' '`

* `"tea".toSlice.find? (fun (c : Char) => c == 'X') == none`

* `("coffee tea water".toSlice.find? "tea").map (·.get!) == some 't'`
 -/
String.Slice.find? : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        (s : String.Slice) → (pat : ρ) → [String.Slice.Pattern.ToForwardSearcher pat σ] → Option s.Pos
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.CofreeEqualizer.condition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X)
      (CategoryTheory.Comonad.CofreeEqualizer.topMap X) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Comonad.CofreeEqualizer.ι X)
      (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
/-- `tan x` takes the junk value `0` when `cos x = 0`  -/
Complex.tan_eq_zero_of_cos_eq_zero : ∀ {x : ℂ}, Complex.cos x = 0 → Complex.tan x = 0
-- Mathlib.Logic.Equiv.Fintype
Equiv.extendSubtype.congr_simp : ∀ {α : Type u_1} {p q : α → Prop} {inst : DecidablePred p} [inst_1 : DecidablePred p] {inst_2 : DecidablePred q}
  [inst_3 : DecidablePred q] [inst_4 : Finite ↑{x | p x}] (e e_1 : { x // p x } ≃ { x // q x }),
  e = e_1 → e.extendSubtype = e_1.extendSubtype
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
_private.Mathlib.CategoryTheory.Abelian.FreydMitchell.0.CategoryTheory.Abelian.FreydMitchell.H : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.Functor (CategoryTheory.Ind (CategoryTheory.AsSmall C)ᵒᵖ)ᵒᵖ
        (ModuleCat (CategoryTheory.Abelian.FreydMitchell.EmbeddingRing C))
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.Context.alreadyUsedPred : Lean.MetavarContext.LevelMVarToParam.Context → Lean.Name → Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformation.mk.injEq : ∀ (label : Lean.Lsp.ParameterInformationLabel) (documentation? : Option Lean.Lsp.MarkupContent)
  (label_1 : Lean.Lsp.ParameterInformationLabel) (documentation?_1 : Option Lean.Lsp.MarkupContent),
  ({ label := label, documentation? := documentation? } = { label := label_1, documentation? := documentation?_1 }) =
    (label = label_1 ∧ documentation? = documentation?_1)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq_setToFun : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (f : α → E),
  ∫ (a : α), f a ∂μ = MeasureTheory.setToFun μ (MeasureTheory.weightedSMul μ) ⋯ f
-- Mathlib.Analysis.Calculus.Deriv.Pi
hasDerivAt_update : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : NontriviallyNormedField 𝕜] (x : ι → 𝕜) (i : ι) (y : 𝕜),
  HasDerivAt (Function.update x i) (Pi.single i 1) y
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- `∏' i, f i` is the unconditional product of `f`, if it exists, or 1 otherwise.

More generally, if `L` is a `SummationFilter`, `∏'[L] i, f i` is the product of `f` with respect to
`L` if it exists, and `1` otherwise.

(Note that even if the unconditional product exists, it might not be unique if the topology is not
separated. When the multiplicative support of `f` is finite, we make the most reasonable choice,
to use the product over the multiplicative support. Otherwise, we choose arbitrarily an `a`
satisfying `HasProd f a`. Similar remarks apply to more general summation filters.)  -/
«term∏'_,_» : Lean.ParserDescr
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toContinuousOrderHom : α →Co β)
  (exists_map_eq_of_map_le' :
    ∀ ⦃a : α⦄ ⦃b : β⦄, toContinuousOrderHom.toFun a ≤ b → ∃ c, a ≤ c ∧ toContinuousOrderHom.toFun c = b),
  sizeOf { toContinuousOrderHom := toContinuousOrderHom, exists_map_eq_of_map_le' := exists_map_eq_of_map_le' } =
    1 + sizeOf toContinuousOrderHom
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.DirectLimit.equiv_lift.congr_simp : ∀ (L : FirstOrder.Language) (ι : Type v) [inst : Preorder ι] (G : ι → Type w) [inst_1 : (i : ι) → L.Structure (G i)]
  (f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)) [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] (G' : ι → Type w')
  [inst_5 : (i : ι) → L.Structure (G' i)] (f' : (i j : ι) → i ≤ j → L.Embedding (G' i) (G' j))
  (g g_1 : (i : ι) → L.Equiv (G i) (G' i)) (e_g : g = g_1) [inst_6 : DirectedSystem G' fun i j h => ⇑(f' i j h)]
  (H_commuting : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (f' i j hij) ((g i) x)),
  FirstOrder.Language.DirectLimit.equiv_lift L ι G f G' f' g H_commuting =
    FirstOrder.Language.DirectLimit.equiv_lift L ι G f G' f' g_1 ⋯
-- Init.System.IO
/-- Configuration for the process' stdin handle.  -/
IO.Process.StdioConfig.stdin : IO.Process.StdioConfig → IO.Process.Stdio
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.toRationalMap_surjective : ∀ {X Y : AlgebraicGeometry.Scheme}, Function.Surjective AlgebraicGeometry.Scheme.PartialMap.toRationalMap
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C},
  autoParam (∀ (J : Type) [Finite J], P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete J))
      CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts.isClosedUnderLimitsOfShape._autoParam →
    P.IsClosedUnderFiniteProducts
-- Mathlib.Order.SetAccumulate
Set.directed_accumulate : ∀ {α : Type u_1} {s : ℕ → Set α}, Directed (fun x1 x2 => x1 ⊆ x2) (Set.accumulate s)
-- Std.Data.Internal.Cut
Std.Internal.IsCut.gt : ∀ {α : Type u} {cmp : α → α → Ordering} {cut : α → Ordering} [self : Std.Internal.IsCut cmp cut] {k k' : α},
  cut k' = Ordering.gt → cmp k' k = Ordering.gt → cut k = Ordering.gt
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instSDiffOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → SDiff (Std.ExtHashMap α β)
-- Lean.LibrarySuggestions.Basic
/-- Filter out theorems from grind-annotated modules when the caller is "grind".
Modules marked with `grind_annotated` contain manually reviewed/annotated theorems,
so they should be excluded from automatic premise selection for grind.
Other callers (like "simp") still receive suggestions from these modules.
 -/
Lean.LibrarySuggestions.Selector.filterGrindAnnotated : Lean.LibrarySuggestions.Selector → Lean.LibrarySuggestions.Selector
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.FunctorsInverting.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} (F : W.FunctorsInverting D),
  (CategoryTheory.CategoryStruct.id F).hom = CategoryTheory.CategoryStruct.id F.obj
-- Mathlib.Data.Set.Finite.Lattice
Finite.Set.finite_iInter : ∀ {α : Type u} {ι : Sort u_1} [Nonempty ι] (t : ι → Set α) [∀ (i : ι), Finite ↑(t i)], Finite ↑(⋂ i, t i)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mapDomain : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} (f : G → G') (v : SkewMonoidAlgebra k G),
  ((SkewMonoidAlgebra.mapDomain f) v).coeff = Finsupp.mapDomain f v.coeff
-- Mathlib.Tactic.GCongr.Core
/-- Mark the lemma as a `gcongr` lemma, using implication as the relation.
For example, `Or.imp : (a → c) → (b → d) → a ∨ b → c ∨ d`. In the non-strict case,
we want to support such lemmas even if the hypotheses are given in a different order.
So, we find the last hypothesis whose head matches that of the conclusion,
and move it to the end.
 -/
_private.Mathlib.Tactic.GCongr.Core.0.Mathlib.Tactic.GCongr.addGCongrLemma.addImpGCongrLemma : Lean.Name → Lean.AttributeKind → ℕ → Bool → Bool → Lean.ConstantInfo → Array Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_apply_eq : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (x : 𝔸) (n : ℕ),
  ((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = (↑n.factorial)⁻¹ • x ^ n
-- Mathlib.Order.Heyting.Basic
HeytingAlgebra.toBoundedOrder.eq_1 : ∀ {α : Type u_2} [inst : HeytingAlgebra α],
  HeytingAlgebra.toBoundedOrder = { toOrderTop := inst.toOrderTop, toOrderBot := inst.toOrderBot }
-- Init.Data.UInt.Bitwise
UInt32.shiftLeft_add : ∀ {a b c : UInt32}, b < 32 → c < 32 → b + c < 32 → a <<< (b + c) = a <<< b <<< c
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceNat : UniformSpace ℕ
-- Mathlib.Algebra.Group.Action.Defs
Function.Surjective.addAction.eq_1 : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : AddMonoid M] [inst_1 : AddAction M α] [inst_2 : VAdd M β]
  (f : α → β) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c +ᵥ x) = c +ᵥ f x),
  Function.Surjective.addAction f hf smul = { toVAdd := inst_2, add_vadd := ⋯, zero_vadd := ⋯ }
-- Aesop.RuleTac.Forward
Aesop.RuleTac.ForwardM.State : Type
-- Mathlib.Data.Fintype.Basic
Fintype.univ_unit : Finset.univ = {()}
-- Mathlib.Analysis.Fourier.Convolution
/-- The norm of the integrand of the convolution is integrable if the functions are integrable.  -/
Real.integrable_prod_sub : ∀ {𝕜 : Type u_1} {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedAddCommGroup F₂]
  [inst_4 : NormedAddCommGroup F₃] [inst_5 : InnerProductSpace ℝ E] [inst_6 : FiniteDimensional ℝ E]
  [inst_7 : MeasurableSpace E] [inst_8 : BorelSpace E] [inst_9 : NormedSpace 𝕜 F₁] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : NormedSpace 𝕜 F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) {f₁ : E → F₁} {f₂ : E → F₂},
  MeasureTheory.Integrable f₁ MeasureTheory.volume →
    MeasureTheory.Integrable f₂ MeasureTheory.volume →
      MeasureTheory.Integrable (fun p => ‖B‖ * (‖f₁ (p.1 - p.2)‖ * ‖f₂ p.2‖))
        (MeasureTheory.volume.prod MeasureTheory.volume)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.modify.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Sort u_3) →
      (m : Std.DHashMap.Internal.Raw₀ α fun x => β) →
        ((size : ℕ) →
            (buckets : Array (Std.DHashMap.Internal.AssocList α fun x => β)) →
              (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
                motive ⟨{ size := size, buckets := buckets }, hm⟩) →
          motive m
-- Mathlib.Data.Set.Function
Set.mapsTo_singleton : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β} {x : α}, Set.MapsTo f {x} t ↔ f x ∈ t
-- Mathlib.Computability.TuringDegree
TuringReducible.rfl : ∀ {f : ℕ →. ℕ}, TuringReducible f f
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Zipper α β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Zipper α β) →
        (Unit → motive Std.DTreeMap.Internal.Zipper.done) →
          ((k : α) →
              (v : β k) →
                (tree : Std.DTreeMap.Internal.Impl α β) →
                  (next : Std.DTreeMap.Internal.Zipper α β) →
                    motive (Std.DTreeMap.Internal.Zipper.cons k v tree next)) →
            motive x
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.TreeMap.Raw.maxEntry! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap.Raw α β cmp → α × β
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' fallback : α}
  {f : β → β},
  (t.modify k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Init.Data.Array.Perm
Array.perm_iff_toList_perm : ∀ {α : Type u_1} {as bs : Array α}, as.Perm bs ↔ as.toList.Perm bs.toList
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- If `g ≫ f = 0` implies `g = 0` for all `g`, then `f` is a monomorphism.  -/
CategoryTheory.NormalEpiCategory.mono_of_cancel_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C]
  [CategoryTheory.IsNormalEpiCategory C] [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y),
  (∀ (Z : C) (g : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0) → CategoryTheory.Mono f
-- Lean.Meta.SizeOf
/-- See `ignoreField`. We have support for functions of the form `Unit → ...`  -/
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkSizeOfRecFieldFormIH : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Complex.Exponential
Complex.ofReal_exp : ∀ (x : ℝ), ↑(Real.exp x) = Complex.exp ↑x
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map_map_fiber : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G)
  {a b : F.Grothendieck} (f : a ⟶ b),
  ((CategoryTheory.Pseudofunctor.Grothendieck.map α).map f).fiber =
    CategoryTheory.CategoryStruct.comp ((α.naturality f.base.toLoc).inv.toNatTrans.app a.fiber)
      ((α.app { as := b.base }).toFunctor.map f.fiber)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldrM_eq_foldrM_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.DTreeMap.foldrM (fun a x d => f a d) init t = Array.foldrM f init t.keysArray
-- Mathlib.Order.Category.Preord
Preord.ext_iff : ∀ {X Y : Preord} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Init.Prelude
/-- Divisibility. `a ∣ b` (typed as `\|`) means that there is some `c` such that `b = a * c`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∣` in identifiers is `dvd`. -/
Dvd.dvd : {α : Type u_1} → [self : Dvd α] → α → α → Prop
-- Mathlib.FieldTheory.Relrank
Subfield.relfinrank_comap_comap_eq_relfinrank_of_le : ∀ {E : Type v} [inst : Field E] {L : Type w} [inst_1 : Field L] (A B : Subfield E) (f : L →+* E),
  B ≤ f.fieldRange → (Subfield.comap f A).relfinrank (Subfield.comap f B) = A.relfinrank B
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (self.map f)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C}
  (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl))
  (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c)
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  [CategoryTheory.Limits.MonoCoprod C] (inl : c₁.pt ⟶ c.pt),
  (∀ (i₁ : I₁), CategoryTheory.CategoryStruct.comp (c₁.inj i₁) inl = c.inj (Sum.inl i₁)) → CategoryTheory.Mono inl
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_erase_lt_of_pos : ∀ {ι : Type u_1} {κ : Type u_5} [inst : DecidableEq ι] [inst_1 : AddCommMonoid κ] [inst_2 : LT κ] [AddLeftStrictMono κ]
  {s : Finset ι} {d : ι}, d ∈ s → ∀ {f : ι → κ}, 0 < f d → ∑ m ∈ s.erase d, f m < ∑ m ∈ s, f m
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
/-- If the canonical functor `CostructuredArrow (G ≫ F) Y ⥤ CostructuredArrow F Y` is final, then
`G ⋙ F` is dense at `Y` if and only if `F` is dense at `Y`.  -/
CategoryTheory.Functor.DenseAt.precompEquivOfFinal : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {Y : D} →
            {C' : Type u_1} →
              [inst_2 : CategoryTheory.Category.{v_1, u_1} C'] →
                (G : CategoryTheory.Functor C' C) →
                  [(CategoryTheory.CostructuredArrow.pre G F Y).Final] → (G.comp F).DenseAt Y ≃ F.DenseAt Y
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.copy_eq : ∀ {M : Type u_1} [inst : Mul M] {S : Subsemigroup M} {s : Set M} (hs : s = ↑S), S.copy s hs = S
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.not_revMatchesAt_skipSuffixWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] (s : String.Slice),
  ¬String.Slice.Pattern.Model.RevMatchesAt pat (s.skipSuffixWhile pat)
-- Mathlib.Algebra.Order.Antidiag.Nat
_private.Mathlib.Algebra.Order.Antidiag.Nat.0.Nat.primeFactorsPiBij.eq_1 : ∀ (d n : ℕ) (f : (a : ℕ) → a ∈ n.primeFactors → Fin d) (x : f ∈ n.primeFactors.pi fun x => Finset.univ) (i : Fin d),
  Nat.primeFactorsPiBij✝ d n f x i = ∏ p ∈ n.primeFactors.attach with f ↑p ⋯ = i, ↑p
-- Mathlib.Topology.CompactOpen
/-- The currying process is a continuous map between function spaces.  -/
ContinuousMap.continuous_curry : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactSpace (X × Y)], Continuous ContinuousMap.curry
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `LE` instance if available  -/
Lean.Meta.Grind.Arith.Linear.Struct.leInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.ofHom_id : ∀ {R : Type u} [inst : Semiring R],
  SemiRingCat.ofHom (RingHom.id R) = CategoryTheory.CategoryStruct.id (SemiRingCat.of R)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- An additive group admitting an additive free group basis is an additive free group.  -/
FreeAddGroupBasis.isFreeAddGroup : ∀ {ι : Type u_1} {G : Type u_3} [inst : AddGroup G] (b : FreeAddGroupBasis ι G), IsFreeAddGroup G
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- If `Function.Surjective (algebraMap A B)`, then `IsCyclotomicExtension {1} A B`.  -/
IsCyclotomicExtension.singleton_one_of_algebraMap_bijective : ∀ {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B],
  Function.Surjective ⇑(algebraMap A B) → IsCyclotomicExtension {1} A B
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.quotientAddGroupMk_eq_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  (x : M), ↑x = Submodule.Quotient.mk x
-- Std.Async.Process
Std.IO.Process.PId.mk.sizeOf_spec : ∀ (toUInt64 : UInt64), sizeOf { toUInt64 := toUInt64 } = 1 + sizeOf toUInt64
-- Std.Tactic.BVDecide.LRAT.Internal.LRATChecker
Std.Tactic.BVDecide.LRAT.Internal.Result.outOfProof.sizeOf_spec : sizeOf Std.Tactic.BVDecide.LRAT.Internal.Result.outOfProof = 1
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderiv_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i},
  (∀ (i : ι), DifferentiableAt 𝕜 (φ i) x) →
    fderiv 𝕜 (fun x i => φ i x) x = ContinuousLinearMap.pi fun i => fderiv 𝕜 (φ i) x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.biprod.lift_mapBiprod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] (X Y : C)
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_6 : CategoryTheory.Limits.PreservesBinaryBiproduct X Y F] {W : C} (f : W ⟶ X) (g : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.lift (F.map f) (F.map g)) (F.mapBiprod X Y).inv =
    F.map (CategoryTheory.Limits.biprod.lift f g)
-- Mathlib.Data.List.Sigma
List.nodupKeys_of_nodupKeys_cons : ∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)}, (s :: l).NodupKeys → l.NodupKeys
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.indicator : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → MeasurableSet t → MeasureTheory.IntegrableOn (t.indicator f) s μ
-- Init.Data.List.Lemmas
List.filter_eq_self : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.filter p l = l ↔ ∀ a ∈ l, p a = true
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.inhabitedM : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u} n} → [I : Inhabited P.A] → [(i : Fin2 n) → Inhabited (α i)] → Inhabited (P.M α)
-- Lean.Meta.Tactic.LibrarySearch
/-- the original declaration  -/
Lean.Meta.LibrarySearch.DeclMod.none : Lean.Meta.LibrarySearch.DeclMod