mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterStep.successor.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3) (it : α)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_2 it
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
MeasureTheory.innerRegularWRT_isCompact_isClosed_iff_innerRegularWRT_isCompact_closure : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [R1Space α],
  μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) IsClosed ↔ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `(F', α)` is a left Kan extension of `F` along `L` and `β : F ⟶ L ⋙ G` is
a natural transformation, this is the induced morphism `F' ⟶ G`.  -/
CategoryTheory.Functor.descOfIsLeftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : F ⟶ L.comp F') →
                    [F'.IsLeftKanExtension α] → (G : CategoryTheory.Functor D H) → (F ⟶ L.comp G) → (F' ⟶ G)
-- Mathlib.Algebra.Order.Module.Defs
smul_le_smul_iff_of_neg_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β]
  [PosSMulReflectLE α β], a < 0 → (a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.modify.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] (a : α) (f : β a → β a)
  (size : ℕ) (buckets : Array (Std.DHashMap.Internal.AssocList α β))
  (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.modify ⟨{ size := size, buckets := buckets }, hm⟩ a f =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, hi⟩ =>
      let bucket := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bucket = true then
        let buckets_1 := buckets.uset i Std.DHashMap.Internal.AssocList.nil hi;
        let bucket := Std.DHashMap.Internal.AssocList.modify a f bucket;
        ⟨{ size := size, buckets := buckets_1.uset i bucket ⋯ }, ⋯⟩
      else ⟨{ size := size, buckets := buckets }, hm⟩
-- Mathlib.CategoryTheory.Retract
/-- If `X` is a retract of `Y`, then `F.obj X` is a retract of `F.obj Y`.  -/
CategoryTheory.Retract.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {X Y : C} →
          CategoryTheory.Retract X Y → (F : CategoryTheory.Functor C D) → CategoryTheory.Retract (F.obj X) (F.obj Y)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_update_same : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ) (a : R), (p.update n a).coeff n = a
-- Mathlib.Analysis.Analytic.IteratedFDeriv
_private.Mathlib.Analysis.Analytic.IteratedFDeriv.0.FormalMultilinearSeries.iteratedFDerivSeries.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsBrownianReal.neg : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ},
  ProbabilityTheory.IsBrownianReal B P → ProbabilityTheory.IsBrownianReal (-B) P
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.proj_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D}, (CategoryTheory.CostructuredArrow.proj S T).Faithful
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.inf : ℝ → ℝ → ℝ
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.ModelsBoundedFormula.realize_boundedFormula : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ : L.BoundedFormula α n},
  T ⊨ᵇ φ → ∀ (M : Type u_1) [inst : L.Structure M] [M ⊨ T] [Nonempty M] {v : α → M} {xs : Fin n → M}, φ.Realize v xs
-- Mathlib.Topology.ContinuousMap.Units
/-- Construct a continuous map into the group of units of a normed ring from a function into the
normed ring and a proof that every element of the range is a unit.  -/
ContinuousMap.unitsOfForallIsUnit : {X : Type u_1} →
  {R : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : NormedRing R] → [CompleteSpace R] → {f : C(X, R)} → (∀ (x : X), IsUnit (f x)) → C(X, Rˣ)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.toAdd_unzero_lt_of_lt_ofAdd : ∀ {α : Type u_1} [inst : Preorder α] {a : WithZero (Multiplicative α)} {b : α} (ha : a ≠ 0),
  a < ↑(Multiplicative.ofAdd b) → Multiplicative.toAdd (WithZero.unzero ha) < b
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.whiskerLeft_left_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T) {Z : C} (h : R.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst R.hom T.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst R.hom S.hom) h
-- Batteries.Tactic.Lint.Simp
/-- When true, the `simpNF` linter sets `backward.isDefEq.respectTransparency true` when
comparing expressions in `isSimpEq`. This is stricter and will flag more simp lemmas as
not in simp-normal form, in particular those where the left-hand side is not in normal form
up to reducible defeq (e.g. lemmas involving type synonyms or bundled carrier types).

Defaults to `false` to preserve the historical linter behavior, which uses
`backward.isDefEq.respectTransparency false` to avoid false positives when `simp`/`dsimp`
changes implicit arguments by unfolding carrier types in bundled structures.

To find simp lemmas that fail with the stricter check, use:
```
set_option linter.simpNF.respectTransparency true in
#lint only simpNF
```
 -/
Batteries.Tactic.Lint.linter.simpNF.respectTransparency : Lean.Option Bool
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_minKeyD_eq_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {fallback : α} {hc : Std.DTreeMap.Internal.Impl.contains (t.minKeyD fallback) t = true},
  t.getKey (t.minKeyD fallback) hc = t.minKey ⋯
-- Mathlib.Probability.Independence.Process.Basic
/-- If stochastic processes `X : (i : S) → (j : T i) → Ω → 𝓧 i j` are independent and
for all `i j`, `X' i j` is almost everywhere equal to `X i j`,
then `X'` are also independent. This implies that independence results about
measurable processes should generally also hold
for processes whose marginals are only a.e.-measurable.  -/
ProbabilityTheory.Kernel.iIndepFun.process_congr : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {T : S → Type u_5} {𝓧 : (i : S) → T i → Type u_6}
  [inst : (i : S) → (j : T i) → MeasurableSpace (𝓧 i j)] {X X' : (i : S) → (j : T i) → Ω → 𝓧 i j},
  ProbabilityTheory.Kernel.iIndepFun (fun i ω j => X i j ω) κ P →
    (∀ (i : S) (j : T i), ∀ᵐ (a : α) ∂P, X i j =ᵐ[κ a] X' i j) →
      ProbabilityTheory.Kernel.iIndepFun (fun i ω j => X' i j ω) κ P
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.commAlgEquiv_single_one : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (m : M),
  (MonoidAlgebra.commAlgEquiv R) (MonoidAlgebra.single m 1) = MonoidAlgebra.single 1 (MonoidAlgebra.single m 1)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1π.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.H1π A =
    CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₁ A).inv (groupCohomology.π A 1)
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.memoizedLeft : {α₁ : Type w} →
  {m : Type w → Type w'} →
    {β₁ : Type w} →
      [inst : Std.Iterator α₁ m β₁] →
        {α₂ β₂ : Type w} → Std.Iterators.Types.Zip α₁ m α₂ β₂ → Option { out // ∃ it, it.IsPlausibleOutput out }
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.Iso.mk_hom : ∀ {α β : FinPartOrd} (e : ↑α.toPartOrd ≃o ↑β.toPartOrd), (FinPartOrd.Iso.mk e).hom = FinPartOrd.ofHom ↑e
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- In a pseudometrizable space, if a measure `μ` is supported on
a separable set then the identity function is `AEStronglyMeasurable` with respect to `μ`.  -/
MeasureTheory.aestronglyMeasurable_id_of_isSeparable : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α]
  [TopologicalSpace.PseudoMetrizableSpace α] [OpensMeasurableSpace α] {s : Set α},
  TopologicalSpace.IsSeparable s → μ sᶜ = 0 → MeasureTheory.AEStronglyMeasurable id μ
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- If `a` semiconjugates `x` to `y` and `x'` to `y'`,
then it semiconjugates `x + x'` to `y + y'`.  -/
AddSemiconjBy.add_right : ∀ {S : Type u_1} [inst : AddSemigroup S] {a x y x' y' : S},
  AddSemiconjBy a x y → AddSemiconjBy a x' y' → AddSemiconjBy a (x + x') (y + y')
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_map_swap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)}, (MeasureTheory.Measure.map Prod.swap ρ).snd = ρ.fst
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.cos : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  AEMeasurable f μ → AEMeasurable (fun x => Real.cos (f x)) μ
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
WfDvdMonoid.max_power_factor' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [WfDvdMonoid α] {a₀ x : α},
  a₀ ≠ 0 → ¬IsUnit x → ∃ n a, ¬x ∣ a ∧ a₀ = x ^ n * a
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.self_mul_dual : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L},
  I ≠ 0 → I * FractionalIdeal.dual A K I = FractionalIdeal.dual A K 1
-- Mathlib.Topology.AlexandrovDiscrete
interior_sInter : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] (S : Set (Set α)),
  interior (⋂₀ S) = ⋂ s ∈ S, interior s
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_dep_iff_forall : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M✶.Dep I ↔ (∀ (B : Set α), M.IsBase B → (I ∩ B).Nonempty) ∧ I ⊆ M.E
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.singleton_eq_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {p : (a : α) × β a}, {p} = ∅.insert p.fst p.snd
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
CategoryTheory.Functor.EffectivelyEnough.mk : ∀ {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] {F : CategoryTheory.Functor C D},
  (∀ (X : D), Nonempty (F.EffectivePresentation X)) → F.EffectivelyEnough
-- Mathlib.Topology.Homotopy.Product
/-- Products commute with path composition.
This is `trans_prod_eq_prod_trans` descended to the quotient.  -/
Path.Homotopic.comp_prod_eq_prod_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {a₁ a₂ a₃ : α} {b₁ b₂ b₃ : β}
  (q₁ : Path.Homotopic.Quotient a₁ a₂) (q₂ : Path.Homotopic.Quotient b₁ b₂) (r₁ : Path.Homotopic.Quotient a₂ a₃)
  (r₂ : Path.Homotopic.Quotient b₂ b₃),
  (Path.Homotopic.prod q₁ q₂).trans (Path.Homotopic.prod r₁ r₂) = Path.Homotopic.prod (q₁.trans r₁) (q₂.trans r₂)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.evaluation_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {x x_1 : C} (f : x ⟶ x_1) (F : CategoryTheory.Functor C D), ((CategoryTheory.evaluation C D).map f).app F = F.map f
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the spans of two vectors are equal, twice angles with those vectors on the left are
equal.  -/
Orientation.two_zsmul_oangle_left_of_span_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V} (z : V), ℝ ∙ x = ℝ ∙ y → 2 • o.oangle x z = 2 • o.oangle y z
-- Mathlib.Util.CountHeartbeats
/-- The "countHeartbeats" linter counts the heartbeats of every declaration.

The effect of the linter is similar to `#count_heartbeats in xxx`, except that it applies
to all declarations.

Note that the linter only counts heartbeats in "top-level" declarations:
it looks inside `set_option ... in`, but not, for instance, inside `mutual` blocks.

There is a convenience notation `#count_heartbeats` that simply sets the linter option to true.
 -/
Mathlib.Linter.linter.countHeartbeats : Lean.Option Bool
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalarsEmbedding_apply : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] (V : Submodule R M),
  (Submodule.restrictScalarsEmbedding S R M) V = Submodule.restrictScalars S V
-- Lean.Util.ReplaceLevel
Lean.Expr.ReplaceLevelImpl.State.mk.sizeOf_spec : ∀ (keys results : Array Lean.Expr), sizeOf { keys := keys, results := results } = 1 + sizeOf keys + sizeOf results
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} [inst_1 : SizeOf C] [inst_2 : SizeOf α] (ι : Type w) (π : ι → α)
  (cofan₁ : CategoryTheory.Limits.Cofan fun i => A (π i)) (cofan₂ : CategoryTheory.Limits.Cofan fun i => B (π i))
  (isColimit₁ : CategoryTheory.Limits.IsColimit cofan₁) (isColimit₂ : CategoryTheory.Limits.IsColimit cofan₂)
  (m : cofan₁.pt ⟶ cofan₂.pt)
  (hm :
    autoParam
      (∀ (i : ι),
        CategoryTheory.CategoryStruct.comp (cofan₁.inj i) m =
          CategoryTheory.CategoryStruct.comp (g (π i)) (cofan₂.inj i))
      HomotopicalAlgebra.AttachCells.hm._autoParam)
  (g₁ : cofan₁.pt ⟶ X₁) (g₂ : cofan₂.pt ⟶ X₂) (isPushout : CategoryTheory.IsPushout g₁ m f g₂),
  sizeOf
      { ι := ι, π := π, cofan₁ := cofan₁, cofan₂ := cofan₂, isColimit₁ := isColimit₁, isColimit₂ := isColimit₂, m := m,
        hm := hm, g₁ := g₁, g₂ := g₂, isPushout := isPushout } =
    1 + sizeOf ι + sizeOf cofan₁ + sizeOf cofan₂ + sizeOf isColimit₁ + sizeOf isColimit₂ + sizeOf m + sizeOf g₁ +
        sizeOf g₂ +
      sizeOf isPushout
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.Core.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (uniformity : Filter (α × α)) (refl : Filter.principal SetRel.id ≤ uniformity)
  (symm : Filter.Tendsto Prod.swap uniformity uniformity)
  (comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity),
  sizeOf { uniformity := uniformity, refl := refl, symm := symm, comp := comp } = 1 + sizeOf uniformity
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.toKaroubi_obj_X : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C),
  ((CategoryTheory.Idempotents.toKaroubi C).obj X).X = X
-- Mathlib.Data.Nat.Periodic
Function.Periodic.map_mod_nat : ∀ {α : Type u_1} {f : ℕ → α} {a : ℕ}, Function.Periodic f a → ∀ (n : ℕ), f (n % a) = f n
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.modify_bind_modify : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  (f g : σ → σ),
  (do
      modify f
      modify g) =
    modify (g ∘ f)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- If `F : D ⥤ C` is a functor to an abelian category, `i : X ⟶ Y` is a morphism
admitting a cokernel such that `F` preserves this cokernel and `F.map i` is a mono,
then `F.map X` identifies to the kernel of `F.map (cokernel.π i)`.  -/
CategoryTheory.Abelian.isLimitMapConeOfKernelForkOfι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : D} →
              (i : X ⟶ Y) →
                [inst_4 : CategoryTheory.Limits.HasCokernel i] →
                  (F : CategoryTheory.Functor D C) →
                    [F.PreservesZeroMorphisms] →
                      [CategoryTheory.Mono (F.map i)] →
                        [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair i 0) F] →
                          CategoryTheory.Limits.IsLimit (F.mapCone (CategoryTheory.Limits.KernelFork.ofι i ⋯))
-- Mathlib.Data.Matrix.Mul
Matrix.pow_apply_nonneg : ∀ {n : Type u_3} {α : Type v} [inst : Semiring α] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  [inst_3 : PartialOrder α] [IsOrderedRing α] {A : Matrix n n α},
  (∀ (i j : n), 0 ≤ A i j) → ∀ (k : ℕ) (i j : n), 0 ≤ (A ^ k) i j
-- Mathlib.Analysis.Complex.AbelLimit
/-- **Abel's limit theorem**. Given a power series converging at 1, the corresponding function
is continuous at 1 when approaching 1 within any fixed Stolz cone.  -/
Complex.tendsto_tsum_powerSeries_nhdsWithin_stolzCone : ∀ {f : ℕ → ℂ} {l : ℂ},
  Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds l) →
    ∀ {s : ℝ}, 0 < s → Filter.Tendsto (fun z => ∑' (n : ℕ), f n * z ^ n) (nhdsWithin 1 (Complex.stolzCone s)) (nhds l)
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_add : ∀ {α : Type u_1} [inst : Add α] (a b : Colex α), ofColex (a + b) = ofColex a + ofColex b
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.mapComposableArrows₅.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂)
  (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact) (i j : ι) (hij : c.Rel i j),
  HomologicalComplex.HomologySequence.mapComposableArrows₅ φ hS₁ hS₂ i j hij =
    CategoryTheory.ComposableArrows.homMk₅ (HomologicalComplex.homologyMap φ.τ₁ i)
      (HomologicalComplex.homologyMap φ.τ₂ i) (HomologicalComplex.homologyMap φ.τ₃ i)
      (HomologicalComplex.homologyMap φ.τ₁ j) (HomologicalComplex.homologyMap φ.τ₂ j)
      (HomologicalComplex.homologyMap φ.τ₃ j) ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.eq_zero_of_isEmpty_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [IsEmpty β], κ = 0
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsStarNormal.norm_add_eq_max : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {a b : A},
  IsStarNormal a → IsStarNormal b → Commute a b → a * b = 0 → ‖a + b‖ = max ‖a‖ ‖b‖
-- Std.Data.DHashMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DHashMap.getKeyD : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → α → α → α
-- Mathlib.Algebra.BigOperators.Pi
Pi.monoidHomMulEquiv.eq_1 : ∀ {ι : Type u_7} [inst : Fintype ι] [inst_1 : DecidableEq ι] (M : ι → Type u_8) [inst_2 : (i : ι) → CommMonoid (M i)]
  (M' : Type u_9) [inst_3 : CommMonoid M'],
  Pi.monoidHomMulEquiv M M' =
    { toFun := fun φ i => φ.comp (MonoidHom.mulSingle M i), invFun := fun φ => ∏ i, (φ i).comp (Pi.evalMonoidHom M i),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.List.Basic
List.singleton_injective : ∀ {α : Type u}, Function.Injective fun a => [a]
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iff'ₛ : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  LinearIndependent R v ↔ ∀ (s : Finset ι) (f g : ι → R), ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i ∈ s, f i = g i
-- Mathlib.Data.FunLike.Basic
DFunLike.congr_arg : ∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [i : FunLike F α β] (f : F) {x y : α}, x = y → f x = f y
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.toEquiv_inclusion : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N} (h : f ≤ g),
  g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ⋯) =
    (FirstOrder.Language.Substructure.inclusion ⋯).comp f.toEquiv.toEmbedding
-- Mathlib.Algebra.Category.ModuleCat.Basic
/-- The type of morphisms in `ModuleCat R`.  -/
ModuleCat.Hom : {R : Type u} → [inst : Ring R] → ModuleCat R → ModuleCat R → Type v
-- Std.Tactic.Do.Syntax
/-- Stops the stateful proof mode of `Std.Do.SPred`.
This will simply forget all the names given to stateful hypotheses and pretty-print
a bit differently.
 -/
Lean.Parser.Tactic.mstop : Lean.ParserDescr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- In an emetric ball, the distance between points is everywhere finite  -/
edist_ne_top_of_mem_ball : ∀ {β : Type u_2} [inst : EMetricSpace β] {a : β} {r : ENNReal} (x y : ↑(Metric.eball a r)), edist ↑x ↑y ≠ ⊤
-- Mathlib.Data.Finsupp.Basic
Finsupp.prod_filter_index : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M)
  [inst_2 : CommMonoid N] (g : α → M → N), (Finsupp.filter p f).prod g = ∏ x ∈ (Finsupp.filter p f).support, g x (f x)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMapPresentation_σ' : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k)
  (f : TensorProduct R (MvPolynomial (Fin m) R) (MvPolynomial (Fin k) R)),
  (MvPolynomial.universalFactorizationMapPresentation R n m k hn).σ' f =
    (MvPolynomial.map MvPolynomial.C) ((MvPolynomial.tensorEquivSum R (Fin m) (Fin k) R) f)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Hom.mk : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (toHom : X.Hom Y.toPresheafedSpace) →
    (∀ (x : ↑↑X.toPresheafedSpace), IsLocalHom (CommRingCat.Hom.hom (toHom.stalkMap x))) → X.Hom Y
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.rfl : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {s : Set X}, Metric.IsCover ε s s