mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.Array.Basic
_private.Batteries.Data.Array.Basic.0.Array.scanrMFast.loop.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m β) (init : β) (as : Array α)
  (start stop : USize) (h_start : start.toNat ≤ as.size) (acc : Array β)
  (h_bound : start.toNat - stop.toNat < acc.size),
  Array.scanrMFast.loop✝ f init as start stop h_start acc h_bound =
    if h_gt : stop < start then
      let startM1 := start - 1;
      have this := ⋯;
      have this_1 := ⋯;
      have this_2 := ⋯;
      do
      let next ← f (as.uget startM1 this_1) init
      Array.scanrMFast.loop✝ f next as startM1 stop ⋯ (acc.uset (startM1 - stop) next ⋯) ⋯
    else pure acc
-- Mathlib.Algebra.AddConstMap.Equiv
/-- An equivalence between `G` and `H` conjugating `(· + a)` to `(· + b)`,
denoted as `G ≃+c[a, b] H`.  -/
AddConstMap.«term_≃+c[_,_]_» : Lean.TrailingParserDescr
-- Lean.Data.PersistentArray
/-- Converts a list to a persistent array.
 -/
Lean.List.toPArray' : {α : Type u} → List α → Lean.PersistentArray α
-- Lean.Elab.PreDefinition.WF.PackMutual
/-- Collect the names of the varying variables (excluding the fixed parameters); this also determines the
arity for the well-founded translations, and is turned into an `ArgsPacker`.
We use the term to determine the arity, but take the name from the type, for better names in the
```
fun : (n : Nat) → Nat | 0 => 0 | n+1 => fun n
```
idiom.
 -/
Lean.Elab.WF.varyingVarNames : Lean.Elab.FixedParamPerms → ℕ → Lean.Elab.PreDefinition → Lean.MetaM (Array Lean.Name)
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- (internal implementation) the fact that the proposed limit cone is the limit  -/
CategoryTheory.Limits.Types.Small.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) →
      [inst_1 : Small.{u, max u v} ↑F.sections] →
        CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.Small.limitCone F)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Non-unital subsemirings of a non-unital semiring form a complete lattice.  -/
NonUnitalSubsemiring.instCompleteLattice : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → CompleteLattice (NonUnitalSubsemiring R)
-- Mathlib.Order.CountableDenseLinearOrder
/-- Given an ideal which intersects `definedAtRight α b`, pick `a : α` such that
some partial function in the ideal maps `a` to `b`.  -/
Order.PartialIso.invOfIdeal : {α : Type u_1} →
  {β : Type u_2} →
    [inst : LinearOrder α] →
      [inst_1 : LinearOrder β] →
        [inst_2 : DenselyOrdered α] →
          [inst_3 : NoMinOrder α] →
            [inst_4 : NoMaxOrder α] →
              [inst_5 : Nonempty α] →
                (b : β) →
                  (I : Order.Ideal (Order.PartialIso α β)) →
                    (∃ f ∈ Order.PartialIso.definedAtRight α b, f ∈ I) → { a // ∃ f ∈ I, (a, b) ∈ ↑f }
-- Mathlib.Algebra.Free
Magma.AssocQuotient.instSemigroup : {α : Type u} → [inst : Mul α] → Semigroup (Magma.AssocQuotient α)
-- Init.Data.SInt.Basic
/-- Converts `true` to `1` and `false` to `0`.
 -/
Bool.toInt64 : Bool → Int64
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.norm : {E : Type u_2} → [Norm E] → Norm (ULift.{u_5, u_2} E)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
op_smul_coe_set : ∀ {G : Type u_2} {S : Type u_4} [inst : Group G] [inst_1 : SetLike S G] [SubgroupClass S G] {s : S} {a : G},
  a ∈ s → MulOpposite.op a • ↑s = ↑s
-- Lean.Util.NumApps
Lean.Expr.NumApps.visit : Lean.Expr → Lean.Expr.NumApps.M Unit
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set: if the derivative of a function within this set is
bounded by `C`, then the function is `C`-Lipschitz. Version with `fderivWithin`.  -/
Convex.norm_image_sub_le_of_norm_fderivWithin_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E},
  DifferentiableOn 𝕜 f s →
    (∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.instInhabited : {α : Type u_1} → {β : Type u_2} → Inhabited (Graph α β)
-- Mathlib.Topology.Filter
Filter.mem_interior : ∀ {α : Type u_2} {s : Set (Filter α)} {l : Filter α}, l ∈ interior s ↔ ∃ t ∈ l, Set.Iic (Filter.principal t) ⊆ s
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.id_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (M : Bimod A B),
  (CategoryTheory.CategoryStruct.id M).hom = CategoryTheory.CategoryStruct.id M.X
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_trunc : ∀ {R : Type u_2} [inst : CommSemiring R] {n : ℕ} (f : PowerSeries R),
  (PowerSeries.trunc n) ↑((PowerSeries.trunc n) f) = (PowerSeries.trunc n) f
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instBot : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Bot (LieSubmodule R L M)
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
/-- To check that a topologically defined morphism property is local at the target,
we may check the corresponding properties on topological spaces.  -/
AlgebraicGeometry.topologically_isZariskiLocalAtTarget : ∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop)
  [(AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso],
  (∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β),
      Continuous f → IsOpen s → P f → P (s.restrictPreimage f)) →
    (∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u}
        (U : ι → TopologicalSpace.Opens β),
        TopologicalSpace.IsOpenCover U → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f) →
      AlgebraicGeometry.IsZariskiLocalAtTarget
        (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P)
-- Init.Data.Array.Find
Array.isNone_idxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, ((xs.idxOf? a).isNone = true) = (a ∉ xs)
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.id_functor : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] (W₁ : CategoryTheory.MorphismProperty C₁),
  (CategoryTheory.LocalizerMorphism.id W₁).functor = CategoryTheory.Functor.id C₁
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots_map_le_degree : ∀ {A : Type u_3} {B : Type u_4} [inst : Semiring A] [inst_1 : CommRing B] [inst_2 : IsDomain B] {f : A →+* B}
  (p : Polynomial A), p ≠ 0 → ↑(Polynomial.map f p).roots.card ≤ p.degree
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Two parallel morphisms `f` and `g` have an equalizer if the diagram `parallelPair f g` has a
limit.  -/
CategoryTheory.Limits.HasEqualizer : {C : Type u} → {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (X ⟶ Y) → (X ⟶ Y) → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_eq_head!_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.minKey! = t.keys.head!
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The type of morphisms in the category `Pseudofunctor.DescentData`.  -/
CategoryTheory.Pseudofunctor.DescentData.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} → {X : ι → C} → {f : (i : ι) → X i ⟶ S} → F.DescentData f → F.DescentData f → Type (max t v')
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatAddInst : Lean.Meta.Simp.DSimproc
-- Init.Core
Thunk.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (fn : Unit → α), sizeOf { fn := fn } = 1 + sizeOf fn
-- Mathlib.Order.Interval.Set.Disjoint
iInter_Iic_eq_empty_iff : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ι → α}, ⋂ i, Set.Iic (f i) = ∅ ↔ ¬BddBelow (Set.range f)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.tensorTensorTensorComm_symm : ∀ (R : Type uR) (S : Type uS) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}
  [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : AddCommMonoid P] [inst_15 : Module A P]
  [inst_16 : AddCommMonoid Q] [inst_17 : Module R Q] [inst_18 : Module R P] [inst_19 : IsScalarTower R A P]
  [inst_20 : Algebra A B] [inst_21 : IsScalarTower A B M] [inst_22 : CommSemiring S] [inst_23 : Algebra R S]
  [inst_24 : Algebra S B] [inst_25 : Module S M] [inst_26 : Module S N] [inst_27 : IsScalarTower R S M]
  [inst_28 : SMulCommClass A S M] [inst_29 : SMulCommClass S A M] [inst_30 : IsScalarTower S B M]
  [inst_31 : IsScalarTower R S N],
  (TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S A B M N P Q).symm =
    TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A S B M P N Q
-- Init.GetElem
getElem?_neg : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] (c : cont) (i : idx), ¬dom c i → c[i]? = none
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerMap_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U V W : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V)
  (g : V ⟶ W) (α : Type t) [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C]
  {Z : CategoryTheory.Limits.FormalCoproduct C} (h : W.power α ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.FormalCoproduct.powerMap (CategoryTheory.CategoryStruct.comp f g) α) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap f α)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.FormalCoproduct.powerMap g α) h)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.hasDimensionLT_face : ∀ {n : ℕ} (S : Finset (Fin (n + 1))) (d : ℕ), S.card ≤ d → (SSet.stdSimplex.face S).toSSet.HasDimensionLT d
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.instFaithfulSingle : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι} (j : ι),
  (HomologicalComplex.single V c j).Faithful
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk : ∀ {R : Type u_1} [inst : CommRing R] (c : R),
  (Set.range (PrimeSpectrum.comap (algebraMap (Polynomial R) (Polynomial (Localization.Away c)))))ᶜ =
    Set.range (PrimeSpectrum.comap (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- Embedding of a submodule `p` to the ambient space `M`.  -/
Submodule.subtype : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p : Submodule R M) → ↥p →ₗ[R] M
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.inline : Lean.Name → String → Lean.ExternEntry
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.size_eq_size_roi : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α] [Std.Rxi.LawfulHasSize α],
  r.size = r.lower<...*.size + 1
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The strictly positive cone of an ordered module is always blunt.  -/
ConvexCone.blunt_strictlyPositive : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup M]
  [inst_3 : PartialOrder M] [inst_4 : IsOrderedAddMonoid M] [inst_5 : Module R M] [inst_6 : PosSMulStrictMono R M],
  (ConvexCone.strictlyPositive R M).Blunt
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The entire function differing from `completedHurwitzZetaEven a s` by a linear combination of
`1 / s` and `1 / (1 - s)`.  -/
HurwitzZeta.completedHurwitzZetaEven₀ : UnitAddCircle → ℂ → ℂ
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatDvd.eq_1 : ∀ (k : ℤ) (p : Int.Internal.Linear.Poly), Int.Internal.Linear.Poly.isUnsatDvd k p = (p.getConst % p.gcdCoeffs k != 0)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.limplies_of_assignmentsInvariant : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.AssignmentsInvariant →
    Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f f.assignments
-- Lean.Elab.Term.TermElabM
/-- Disables incremental tactic reuse *and* reporting for `act` if `cond` is true by setting `tacSnap?`
to `none`. This should be done for tactic blocks that are run multiple times as otherwise the
reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is
similarly questionable).
 -/
Lean.Elab.Term.withoutTacticIncrementality : {m : Type → Type} →
  {α : Type} → [Monad m] → [MonadWithReaderOf Lean.Elab.Term.Context m] → [Lean.MonadOptions m] → Bool → m α → m α
-- Mathlib.Combinatorics.Quiver.Arborescence
Quiver.RootedConnected.mk : ∀ {V : Type u} [inst : Quiver V] {r : V}, (∀ (b : V), Nonempty (Quiver.Path r b)) → Quiver.RootedConnected r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.ordCompare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Raw α (fun x => β) compare},
  t.WF →
    ∀ {k : α} {f : β → β} {fallback : α},
      compare ((Std.DTreeMap.Raw.Const.modify t k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.ideal_fg : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.EssFiniteType R S], (KaehlerDifferential.ideal R S).FG
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_singleton : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {m : M},
  m ≠ 0 → (R ∙ m).spanFinrank = 1
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  {F : CategoryTheory.Functor C FintypeCat} (obj : C) (pt : (F.obj obj).obj)
  (isGalois :
    autoParam (CategoryTheory.PreGaloisCategory.IsGalois obj)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois._autoParam)
  (obj_1 : C) (pt_1 : (F.obj obj_1).obj)
  (isGalois_1 :
    autoParam (CategoryTheory.PreGaloisCategory.IsGalois obj_1)
      CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois._autoParam),
  ({ obj := obj, pt := pt, isGalois := isGalois } = { obj := obj_1, pt := pt_1, isGalois := isGalois_1 }) =
    (obj = obj_1 ∧ pt ≍ pt_1)
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_cons : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (b : β) (s : Stream'.WSeq α) (t : Stream'.WSeq β),
  Stream'.WSeq.LiftRel R (Stream'.WSeq.cons a s) (Stream'.WSeq.cons b t) ↔ R a b ∧ Stream'.WSeq.LiftRel R s t
-- Lean.Data.Lsp.Utf16
Lean.DeclarationRange.ofFilePositions : Lean.FileMap → Lean.Position → Lean.Position → Lean.DeclarationRange
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.comp_iff : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsPreimmersion g],
  AlgebraicGeometry.IsPreimmersion (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsPreimmersion f
-- Mathlib.RingTheory.HopfAlgebra.Convolution
AlgHom.instCommGroupWithConvOfIsCocomm : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : CommSemiring C] →
            [inst_3 : Bialgebra R C] →
              [inst_4 : HopfAlgebra R A] → [Coalgebra.IsCocomm R A] → CommGroup (WithConv (A →ₐ[R] C))
-- Mathlib.Order.Interval.Set.SuccPred
Set.Iic_pred_eq_Iio_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {b : α}, ¬IsMin b → Set.Iic (Order.pred b) = Set.Iio b
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- For the version where the second space in the product is countable,
see `measurable_from_prod_countable_left`.  -/
measurable_from_prod_countable_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  [Countable α] [MeasurableSingletonClass α] {f : α × β → γ}, (∀ (x : α), Measurable fun y => f (x, y)) → Measurable f
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- The heterogeneous differential as a linear map, denoted as `𝒅ₕ` within the `Manifold` namespace.
Instead of taking a function as an argument, this
differential takes `h : f x = y`. It is particularly handy for situations where the points
at which it has to be evaluated are equal but not definitionally equal.  -/
Manifold.«term𝒅ₕ» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelImageι_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasImage f]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)]
  [inst_4 : CategoryTheory.Limits.HasCokernel f]
  [inst_5 : CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)],
  (CategoryTheory.Limits.cokernelImageι f).hom =
    CategoryTheory.Limits.cokernel.desc (CategoryTheory.Limits.image.ι f) (CategoryTheory.Limits.cokernel.π f) ⋯
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.coe_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  {R : Type u_5} [inst_3 : SMulZeroClass R β] [inst_4 : ContinuousConstSMul R β] (r : R)
  (f : CompactlySupportedContinuousMap α β), ⇑(r • f) = r • ⇑f
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} →
        (aig : Std.Sat.AIG α) →
          (idx : ℕ) →
            aig.RefVec idx →
              idx ≤ len →
                aig.RefVec len →
                  aig.RefVec len →
                    (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) →
                      [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] →
                        [Std.Sat.AIG.RefVec.LawfulZipOperator α f] → Std.Sat.AIG.RefVecEntry α len
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The limit of `(1 + g n) ^ n` as `(n : ℝ) → ∞` is `exp t`,
where `t : ℂ` is the limit of `n * g n`.  -/
Complex.tendsto_one_add_pow_exp_of_tendsto : ∀ {g : ℕ → ℂ} {t : ℂ},
  Filter.Tendsto (fun n => ↑n * g n) Filter.atTop (nhds t) →
    Filter.Tendsto (fun n => (1 + g n) ^ n) Filter.atTop (nhds (Complex.exp t))
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instAddMonoid : (A : Type u_3) → (E : Type u_4) → [AddMonoid E] → AddMonoid (WithCStarModule A E)
-- Init.Data.String.TakeDrop
/-- If `pat` matches a prefix of `s`, returns the remainder. Returns `s` unmodified
otherwise.

Use `String.dropPrefix?` to return `none` when `pat` does not match a prefix.

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".dropPrefix "red " == "green blue".toSlice`

* `"red green blue".dropPrefix "reed " == "red green blue".toSlice`

* `"red green blue".dropPrefix 'r' == "ed green blue".toSlice`

* `"red green blue".dropPrefix Char.isLower == "ed green blue".toSlice`
 -/
String.dropPrefix : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → String.Slice
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ ∩ m₂).getKeyD k fallback = if k ∈ m₂ then m₁.getKeyD k fallback else fallback
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapM.match_1.eq_2 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {β' : Type u_1} {f : β → n (Option β')} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (out' : β')
  (hf : MonadAttach.CanReturn (f out) (some out')) (h_1 : (hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩)
  (h_2 : (out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩),
  (match ⟨some out', hf⟩ with
    | ⟨none, hf⟩ => h_1 hf
    | ⟨some out', hf⟩ => h_2 out' hf) =
    h_2 out' hf
-- Mathlib.Algebra.Group.Basic
one_mul_eq_id : ∀ {M : Type u_4} [inst : MulOneClass M], (fun x => 1 * x) = id
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] {Z : D} (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.factorThruCoimage (F.map f)) h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.factorThruCoimage f)) h
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE?_eq_map : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α},
  Std.DTreeMap.Internal.Impl.Const.getEntryGE? k t =
    Option.map (fun x => (x.fst, x.snd)) (Std.DTreeMap.Internal.Impl.getEntryGE? k t)
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.mkAdmProj : Lean.Expr → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.FunProp.Core
/-- Try to apply a theorem `thmOrigin` to the goal `e`.  -/
Mathlib.Meta.FunProp.tryTheorem? : Lean.Expr →
  Mathlib.Meta.FunProp.Origin →
    (Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)) →
      optParam Bool false → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.Order.Heyting.Hom
BiheytingHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] {f g : BiheytingHom α β},
  (∀ (a : α), f a = g a) → f = g