mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.monotone_i₃ : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (pq : κ)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_32)
  (hrr' : autoParam (r ≤ r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_34),
  self.i₃ r pq ⋯ ≤ self.i₃ r' pq ⋯
-- Mathlib.Topology.Path
Path.symm_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y) (a : ↑unitInterval),
  γ.symm a = (⇑γ ∘ unitInterval.symm) a
-- Mathlib.Data.NNRat.Defs
NNRat.nsmul_coe : ∀ (q : ℚ≥0) (n : ℕ), ↑(n • q) = n • ↑q
-- Lean.Data.Lsp.Extra
Lean.Lsp.instReprLineRange : Repr Lean.Lsp.LineRange
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- A cofibrant resolution functor from a model category to the homotopy category
of cofibrant objects.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.resolution : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      CategoryTheory.Functor C (HomotopicalAlgebra.CofibrantObject.HoCat C)
-- Mathlib.LinearAlgebra.JordanChevalley
/-- **Uniqueness of Jordan-Chevalley-Dunford decomposition**: if `n₁ + s₁ = n₂ + s₂` with `nᵢ`
nilpotent, `sᵢ` semisimple, and `nᵢ`, `sᵢ` commuting, then `n₁ = n₂` and `s₁ = s₂`.  -/
Module.End.isNilpotent_isSemisimple_unique : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  [PerfectField K] {n₁ s₁ n₂ s₂ : Module.End K V},
  IsNilpotent n₁ →
    s₁.IsSemisimple →
      IsNilpotent n₂ → s₂.IsSemisimple → Commute n₁ s₁ → Commute n₂ s₂ → n₁ + s₁ = n₂ + s₂ → n₁ = n₂ ∧ s₁ = s₂
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_add : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a b : SkewMonoidAlgebra k G), (a + b).coeff = a.coeff + b.coeff
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.commRingObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (self : CategoryTheory.CommRingObjCat C) → CategoryTheory.CommRingObj self.X
-- Aesop.Tracing
Aesop.TraceOption : Type
-- Mathlib.Computability.StateTransition
StateTransition.Reaches.to₀ : ∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ}, StateTransition.Reaches f a b → StateTransition.Reaches₀ f a b
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Init.Data.List.Sublist
List.append_sublist_iff : ∀ {α : Type u_1} {r l₁ l₂ : List α}, (l₁ ++ l₂).Sublist r ↔ ∃ r₁ r₂, r = r₁ ++ r₂ ∧ l₁.Sublist r₁ ∧ l₂.Sublist r₂
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A generalization of `eVariationOn.union` in which the greatest element of `s` is allowed to lie
to the left of the least element of `t`.  -/
eVariationOn.union' : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s t : Set α}
  {x y : α},
  IsGreatest s x →
    IsLeast t y → x ≤ y → eVariationOn f (s ∪ t) = eVariationOn f s + edist (f x) (f y) + eVariationOn f t
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X)
  (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex),
  CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ),
      CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv ((F.leftDerived n).map f) =
        CategoryTheory.CategoryStruct.comp
          (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp
                (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map
            φ)
          (Q.isoLeftDerivedObj F n).inv
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.coe_mkQL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (S : Submodule R M), ⇑S.mkQL = ⇑S.mkQ
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.ext : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p q : MvPolynomial σ R),
  (∀ (m : σ →₀ ℕ), MvPolynomial.coeff m p = MvPolynomial.coeff m q) → p = q
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.brecOn.go : {motive_1 : Lean.Elab.InfoTree → Sort u} →
  {motive_2 : Lean.PersistentArray Lean.Elab.InfoTree → Sort u} →
    {motive_3 : Lean.PersistentArrayNode Lean.Elab.InfoTree → Sort u} →
      {motive_4 : Array Lean.Elab.InfoTree → Sort u} →
        {motive_5 : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
          {motive_6 : List Lean.Elab.InfoTree → Sort u} →
            {motive_7 : List (Lean.PersistentArrayNode Lean.Elab.InfoTree) → Sort u} →
              (t : Lean.Elab.InfoTree) →
                ((t : Lean.Elab.InfoTree) → t.below → motive_1 t) →
                  ((t : Lean.PersistentArray Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_1 t → motive_2 t) →
                    ((t : Lean.PersistentArrayNode Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_2 t → motive_3 t) →
                      ((t : Array Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_3 t → motive_4 t) →
                        ((t : Array (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                            Lean.Elab.InfoTree.below_4 t → motive_5 t) →
                          ((t : List Lean.Elab.InfoTree) → Lean.Elab.InfoTree.below_5 t → motive_6 t) →
                            ((t : List (Lean.PersistentArrayNode Lean.Elab.InfoTree)) →
                                Lean.Elab.InfoTree.below_6 t → motive_7 t) →
                              motive_1 t ×' t.below
-- Mathlib.Algebra.RingQuot
RingQuot.mk.sizeOf_spec : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} [inst_1 : SizeOf R] [inst_2 : (a a_1 : R) → SizeOf (r a a_1)]
  (toQuot : Quot (RingQuot.Rel r)), sizeOf { toQuot := toQuot } = 1 + sizeOf toQuot
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instContinuousSup : ∀ {α : Type u_1} [inst : TopologicalSpace α], ContinuousSup (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (Topology.WithLower α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.union_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∪ t₂).Equiv (t₃ ∪ t₄)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.support_ne_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.support ≠ []
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.rightRigidCategory : (K : Type u) → [inst : Field K] → CategoryTheory.RightRigidCategory (FGModuleCat K)
-- Mathlib.Logic.Function.Basic
Function.update_eq_self_iff : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] {f : (a : α) → β a} {a : α} {b : β a},
  Function.update f a b = f ↔ b = f a
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.IsNotG2.mk : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [toIsValuedIn : P.IsValuedIn ℤ] [toIsReduced : P.IsReduced] [toIsIrreducible : P.IsIrreducible],
  (∀ (i j : ι), P.pairingIn ℤ i j ∈ {-2, -1, 0, 1, 2}) → P.IsNotG2
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- Right-whiskering in the bicategory `BasedCategory` is given by whiskering the underlying
functors and natural transformations.  -/
CategoryTheory.BasedCategory.whiskerRight : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {𝒳 : CategoryTheory.BasedCategory 𝒮} →
      {𝒴 : CategoryTheory.BasedCategory 𝒮} →
        {𝒵 : CategoryTheory.BasedCategory 𝒮} →
          {F G : CategoryTheory.BasedFunctor 𝒳 𝒴} →
            (F ⟶ G) → (H : CategoryTheory.BasedFunctor 𝒴 𝒵) → F.comp H ⟶ G.comp H
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → k ∉ t₁ \ t₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α},
  k ∈ Std.ExtDTreeMap.filter f t ↔ ∃ (h' : k ∈ t), f (t.getKey k h') (Std.ExtDTreeMap.Const.get t k h') = true
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformEmbedding_subtype_val : ∀ {α : Type u} [inst : UniformSpace α] {p : α → Prop}, IsUniformEmbedding Subtype.val
-- Init.RCases
/-- `(pat)` is a pattern which resets the precedence to low  -/
Lean.Parser.Tactic.rcasesPat.paren : Lean.ParserDescr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.HashMap.ofList l)[k]? = none
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.add_apply : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_5} (F : FormalGroup R) {x y : F.Point σ},
  ↑(x + y) = MvPowerSeries.subst ![↑x, ↑y] F.toPowerSeries
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instMul : {M : Type u_1} → [inst : TopologicalSpace M] → [inst_1 : Mul M] → [ContinuousMul M] → Mul (SeparationQuotient M)
-- Init.Data.SInt.Bitwise
Int32.toUInt32_and : ∀ (a b : Int32), (a &&& b).toUInt32 = a.toUInt32 &&& b.toUInt32
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `strengthenStrictInt h` turns a proof `h` of a strict integer inequality `t1 < t2`
into a proof of `t1 ≤ t2 + 1`.  -/
Mathlib.Tactic.Linarith.strengthenStrictInt : Mathlib.Tactic.Linarith.Preprocessor
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Complex.norm_cpow_le : ∀ (z w : ℂ), ‖z ^ w‖ ≤ ‖z‖ ^ w.re / Real.exp (z.arg * w.im)
-- Mathlib.Data.Fin.VecNotation
Matrix.cons_val_succ' : ∀ {α : Type u} {m i : ℕ} (h : i.succ < m.succ) (x : α) (u : Fin m → α), Matrix.vecCons x u ⟨i.succ, h⟩ = u ⟨i, ⋯⟩
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.map_negY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S)
  (x y : R), (W'.map f).negY (f x) (f y) = f (W'.negY x y)
-- Mathlib.Topology.Algebra.Monoid
continuous_multiset_prod : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Multiset ι),
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => (Multiset.map (fun i => f i a) s).prod
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).minKey ⋯ = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_add_neg_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α}, -a + b < 0 ↔ b < a
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_mk_le : ∀ {α : Type v} {β : Type w},
  Cardinal.lift.{max u w, v} (Cardinal.mk α) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk β) ↔ Nonempty (α ↪ β)
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
GrpCat.instBraidedForgetMonoidHomCarrier : (CategoryTheory.forget GrpCat).Braided
-- Init.System.FilePath
/-- Appends the extension `ext` to a path `p`.

`ext` should not have leading `.`, as this function adds one. If `ext` is the empty string, no
`.` is added.

Unlike `System.FilePath.withExtension`, this does not remove any existing extension.
 -/
System.FilePath.addExtension : System.FilePath → String → System.FilePath
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.ι_range_comap_reverse : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M),
  Submodule.comap CliffordAlgebra.reverse (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
/-- `F` is dense at `Y` if `Y` identifies to the colimit of the obvious functor
`CostructuredArrow F Y ⥤ D`.  -/
CategoryTheory.Functor.denseAtEquiv : {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) →
            F.DenseAt Y ≃
              CategoryTheory.Limits.IsColimit
                ((CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D) F.rightUnitor.inv).coconeAt Y)
-- Lean.Util.Trace
_private.Lean.Util.Trace.0.Lean.expandTraceMacro : Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.DoElem
-- Init.WFComputable
_private.Init.WFComputable.0.WellFounded.fixFC.eq_1 : ∀ {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (a : Acc r x),
  WellFounded.fixFC F x a = Acc.recC (fun x₁ h ih => F x₁ ih) a
-- Lean.Data.AssocList
Lean.AssocList.cons.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (key : α) (value : β) (tail : Lean.AssocList α β),
  sizeOf (Lean.AssocList.cons key value tail) = 1 + sizeOf key + sizeOf value + sizeOf tail
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.instMonoIntι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.ι✝ f n)
-- Mathlib.RingTheory.Finiteness.Basic
/-- Maps from a finite module have a finite range.  -/
Submodule.fg_range : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_3}
  {P : Type u_4} [inst_3 : Semiring S] [inst_4 : AddCommMonoid P] [inst_5 : Module S P] {σ : R →+* S}
  [inst_6 : RingHomSurjective σ] [Module.Finite R M] (f : M →ₛₗ[σ] P), f.range.FG
-- Mathlib.Algebra.Notation
/-- The *positive part* of an element `a`.  -/
OneLePart.oneLePart : {α : Type u_1} → [self : OneLePart α] → α → α
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.instUniqueCarrierObjTopCatToTopMkOfNatNat : Unique ↑(SimplexCategory.toTop.{u}.obj { len := 0 })
-- Mathlib.Topology.Homeomorph.Defs
IsHomeomorph.image_closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → ∀ (s : Set X), f '' closure s = closure (f '' s)
-- Mathlib.Algebra.Field.Defs
/-- However `qsmul` is defined, it must be propositionally equal to multiplication by `Rat.cast`.

Do not use this lemma directly. Use `Rat.cast_def` instead.  -/
DivisionRing.qsmul_def : ∀ {K : Type u_2} [self : DivisionRing K] (a : ℚ) (x : K), DivisionRing.qsmul a x = ↑a * x
-- Lean.Elab.Term.TermElabM
/-- When `errToSorry` is set to true, the method `elabTerm` catches
exceptions and converts them into synthetic `sorry`s.
The implementation of choice nodes and overloaded symbols rely on the fact
that when `errToSorry` is set to false for an elaboration function `F`, then
`errToSorry` remains `false` for all elaboration functions invoked by `F`.
That is, it is safe to transition `errToSorry` from `true` to `false`, but
we must not set `errToSorry` to `true` when it is currently set to `false`.
 -/
Lean.Elab.Term.Context.errToSorry : Lean.Elab.Term.Context → Bool
-- Mathlib.Algebra.Field.Basic
ofDual_ratCast : ∀ {K : Type u_1} [inst : RatCast K] (n : ℚ), OrderDual.ofDual ↑n = ↑n
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A field extension `E / F` is purely inseparable if and only if for every element `x` of `E`,
its minimal polynomial has separable degree one.  -/
isPurelyInseparable_iff_natSepDegree_eq_one : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.instAddAction.eq_1 : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (H : AddSubgroup G),
  AddAction.instAddAction H =
    { toAddSemigroupAction := (AddSubmonoid.instAddActionSubtypeMem H).toAddSemigroupAction, zero_vadd := ⋯ }
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
/-- For any morphism property `W` on `C`, `W.paths` is the morphism property on `Paths C`
containing all paths of morphisms in `W`.  -/
CategoryTheory.MorphismProperty.paths : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty (CategoryTheory.Paths C)
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_zero : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], ↑0 = 0
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ordMonoidWithZeroHom_eq_zero_iff : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Nontrivial R] (y : ↥(nonZeroDivisors R)),
  (Ring.ordMonoidWithZeroHom R) ↑y = 0 ↔ Ring.ord R ↑y = ⊤
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- The space of continuous multilinear maps on `Π(i : Fin (n+1)), G` is canonically isomorphic to
the space of continuous multilinear maps on `Π(i : Fin n), G` with values in the space
of continuous linear maps on `G`, by separating the last variable. We register this
isomorphism as a continuous linear equiv in `continuousMultilinearCurryRightEquiv' 𝕜 n G G'`.
For a version allowing dependent types, see `continuousMultilinearCurryRightEquiv`. When there
are no dependent types, use the primed version as it helps Lean a lot for unification.

The direct and inverse maps are given by `f.curryRight` and `f.uncurryRight`. Use these
unless you need the full framework of linear isometric equivs.  -/
continuousMultilinearCurryRightEquiv' : (𝕜 : Type u) →
  (n : ℕ) →
    (G : Type wG) →
      (G' : Type wG') →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : NormedAddCommGroup G] →
            [inst_2 : NormedSpace 𝕜 G] →
              [inst_3 : NormedAddCommGroup G'] →
                [inst_4 : NormedSpace 𝕜 G'] → (G [×n.succ]→L[𝕜] G') ≃ₗᵢ[𝕜] G [×n]→L[𝕜] G →L[𝕜] G'
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
/-- Special case of the sandwich lemma; see `tendsto_of_tendsto_of_tendsto_of_le_of_le'` for the
general case.  -/
squeeze_zero' : ∀ {α : Type u_3} {f g : α → ℝ} {t₀ : Filter α},
  (∀ᶠ (t : α) in t₀, 0 ≤ f t) →
    (∀ᶠ (t : α) in t₀, f t ≤ g t) → Filter.Tendsto g t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange_add : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f : M → N}
  {hf : f 0 = 0},
  (∀ (x y : M), f (x + y) = f x + f y) →
    ∀ (v₁ v₂ : ι →₀ M), Finsupp.mapRange f hf (v₁ + v₂) = Finsupp.mapRange f hf v₁ + Finsupp.mapRange f hf v₂
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofHasKernel_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : CategoryTheory.Limits.HasKernel S.g],
  (CategoryTheory.ShortComplex.HomologyData.ofHasKernel S hf).left =
    CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel S hf
-- Mathlib.RingTheory.Flat.CategoryTheory
Module.Flat.iff_rTensor_preserves_shortComplex_exact : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R),
  Module.Flat R ↑M ↔
    ∀ (C : CategoryTheory.ShortComplex (ModuleCat R)),
      C.Exact → (C.map (CategoryTheory.MonoidalCategory.tensorRight M)).Exact
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.insert k).min! = t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Data.Finsupp.Basic
/-- The additive equivalence between `(α ⊕ β) →₀ M` and `(α →₀ M) × (β →₀ M)`.

This is the `Finsupp` version of `Equiv.sum_arrow_equiv_prod_arrow`.  -/
Finsupp.sumFinsuppAddEquivProdFinsupp : {M : Type u_5} → [inst : AddMonoid M] → {α : Type u_12} → {β : Type u_13} → (α ⊕ β →₀ M) ≃+ (α →₀ M) × (β →₀ M)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.map_shiftFunctorCompIsoId_hom_app_assoc : ∀ {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) {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] (X : C)
  (a b : A) (h : a + b = 0) {Z : D} (h_1 : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).hom.app X)) h_1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F b).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId D a b h).hom.app (F.obj X)) h_1))
-- Init.Data.SInt.Lemmas
Int32.zero_le_ofNat_of_lt : ∀ {a : ℕ}, a < 2 ^ 31 → 0 ≤ Int32.ofNat a
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.instHasInjectiveDimensionLTSucc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ)
  [CategoryTheory.HasInjectiveDimensionLT X n], CategoryTheory.HasInjectiveDimensionLT X n.succ
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.iterate : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μa : MeasureTheory.Measure α} {f : α → α},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μa →
    ∀ (n : ℕ), MeasureTheory.Measure.QuasiMeasurePreserving f^[n] μa μa
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- This right homology map data expresses compatibilities of the right homology data
constructed by `RightHomologyData.ofEpiOfIsIsoOfMono`  -/
CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h : S₁.RightHomologyData) →
            [inst_2 : CategoryTheory.Epi φ.τ₁] →
              [inst_3 : CategoryTheory.IsIso φ.τ₂] →
                [inst_4 : CategoryTheory.Mono φ.τ₃] →
                  CategoryTheory.ShortComplex.RightHomologyMapData φ h
                    (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The derivative of Weierstrass `℘` function with the `l₀`-term missing.
This is mainly a tool for calculations where one would want to omit a diverging term.
This has the notation `℘'[L - l₀]` in the namespace `PeriodPairs`.  -/
PeriodPair.derivWeierstrassPExcept : PeriodPair → ℂ → ℂ → ℂ