mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.Subobject.inf_eq_of_isDetecting : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {𝒢 : CategoryTheory.ObjectProperty C},
  𝒢.IsDetecting →
    ∀ {X : C} (P Q : CategoryTheory.Subobject X),
      (∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f → Q.Factors f) → P ⊓ Q = P
-- Mathlib.Order.CompleteLattice.Group
iSup_mul_le : ∀ {α : Type u_1} {ι : Sort u_2} [inst : CompleteLattice α] [inst_1 : Mul α] [MulLeftMono α] [MulRightMono α]
  (u v : ι → α), ⨆ i, u i * v i ≤ (⨆ i, u i) * ⨆ i, v i
-- Mathlib.RingTheory.Derivation.Basic
Derivation.coe_add_linearMap : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  (D1 D2 : Derivation R A M), ↑(D1 + D2) = ↑D1 + ↑D2
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'.match_1.eq_1 : ∀ (C : Type u_1)
  (motive :
    CategoryTheory.FreeMonoidalCategory C → CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_2)
  (a : C) (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C)
  (h_1 :
    (a : C) →
      (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
        motive (CategoryTheory.FreeMonoidalCategory.of a) x)
  (h_2 :
    (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
      motive CategoryTheory.FreeMonoidalCategory.unit x)
  (h_3 :
    (X Y : CategoryTheory.FreeMonoidalCategory C) →
      (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → motive (X.tensor Y) n),
  (match CategoryTheory.FreeMonoidalCategory.of a, x with
    | CategoryTheory.FreeMonoidalCategory.of a, x => h_1 a x
    | CategoryTheory.FreeMonoidalCategory.unit, x => h_2 x
    | X.tensor Y, n => h_3 X Y n) =
    h_1 a x
-- Std.Data.DHashMap.Internal.Index
/-- Scramble the hash code in order to protect against bad hash functions.

Example: if `Hashable Float` was implemented using the "identity" reinterpreting the bit pattern as
a `UInt64`, then the hash codes of all small positive or negative integers would end in around 50
zeroes, meaning that they all land in bucket 0 in reasonably-sized hash maps.

To counteract this, we xor the hash code with some shifted-down versions of itself, to make sure
that all of the entropy of the hash code appears in the lower 16 bits at least.

The scrambling operation is very fast. It does not have a measurable impact on performance in the
insert benchmark.
 -/
Std.DHashMap.Internal.scrambleHash : UInt64 → UInt64
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.ComplexMeasure.toComplexMeasure_to_signedMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (c : MeasureTheory.ComplexMeasure α),
  (MeasureTheory.ComplexMeasure.re c).toComplexMeasure (MeasureTheory.ComplexMeasure.im c) = c
-- Mathlib.Geometry.Manifold.Riemannian.Basic
eventually_norm_mfderiv_extChartAt_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] (x : M),
  ∃ C > 0, ∀ᶠ (y : M) in nhds x, ‖mfderiv% ↑(extChartAt I x) y‖ < C
-- Mathlib.Topology.Constructions.SumProd
isInducing_prodMkRight : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X),
  Topology.IsInducing (Prod.mk x)
-- Mathlib.RingTheory.Binomial
Ring.smeval_ascPochhammer_int_ofNat : ∀ {R : Type u_2} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] (r : R) (n : ℕ),
  (ascPochhammer ℤ n).smeval r = (ascPochhammer ℕ n).smeval r
-- Mathlib.Computability.Primrec.List
Nat.Primrec'.cons : ∀ {n m : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ n → List.Vector ℕ m},
  Nat.Primrec' f → Nat.Primrec'.Vec g → Nat.Primrec'.Vec fun v => f v ::ᵥ g v
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Lift an `AddHom` to `Finset` via `image`  -/
Finset.imageAddHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : DecidableEq α] →
        [inst_1 : Add α] →
          [inst_2 : Add β] →
            [inst_3 : FunLike F α β] → [AddHomClass F α β] → F → [inst_5 : DecidableEq β] → Finset α →ₙ+ Finset β
-- Init.Data.List.Monadic
List.zipWithM_nil_right : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {l : List α} [inst : Monad m]
  {f : α → β → m γ}, List.zipWithM f l [] = pure []
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLTD_eq_getD_getEntryLT? : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α} {fallback : α × β},
  Std.DTreeMap.Internal.Impl.Const.getEntryLTD k t fallback =
    (Std.DTreeMap.Internal.Impl.Const.getEntryLT? k t).getD fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.hasCokernel_epi_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Limits.HasCokernel f] {W : C} (g : W ⟶ X) [CategoryTheory.Epi g],
  CategoryTheory.Limits.HasCokernel (CategoryTheory.CategoryStruct.comp g f)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.congr_right : ∀ {α : Type u} {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β}, m₁.Equiv m₂ → (m₃.Equiv m₁ ↔ m₃.Equiv m₂)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_ofNat_lt_lift : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.aleph (OfNat.ofNat n) < Cardinal.lift.{v, u} c ↔ Cardinal.aleph (OfNat.ofNat n) < c
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.σ_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X' X : CategoryTheory.SimplicialObject C} (f : X ⟶ X') {n : ℕ}
  (i : Fin (n + 1)) {Z : C} (h : X'.obj (Opposite.op { len := n + 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ i)
      (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n + 1 })) h) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n }))
      (CategoryTheory.CategoryStruct.comp (X'.σ i) h)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorLeftMopIso_inv_app_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  (X_1 : Cᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.tensorLeftMopIso X).inv.app X_1).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1.unmop X)
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsProj.codRestrict_apply : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_6} [inst_1 : AddCommMonoid M] [inst_2 : Module S M] {m : Submodule S M}
  {f : M →ₗ[S] M} (h : LinearMap.IsProj m f) (x : M), ↑(h.codRestrict x) = f x
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.lift_eq_ofENat : ∀ {x : Cardinal.{v}} {m : ℕ∞}, Cardinal.lift.{u, v} x = ↑m ↔ x = ↑m
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.AltExpr.mk.sizeOf_spec : ∀ {σ : Type} [inst : SizeOf σ] (ref : Lean.Syntax) (var? : Option Lean.Elab.Term.Do.Var) (funName : Lean.Syntax)
  (pvars : Array Lean.Syntax) (rhs : σ),
  sizeOf { ref := ref, var? := var?, funName := funName, pvars := pvars, rhs := rhs } =
    1 + sizeOf ref + sizeOf var? + sizeOf funName + sizeOf pvars + sizeOf rhs
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Presieve.ofArrows_mem_comap_jointlySurjectivePrecoverage_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C (Type u)) {X : C}
  {ι : Type u_2} {Y : ι → C} {f : (i : ι) → Y i ⟶ X},
  CategoryTheory.Presieve.ofArrows Y f ∈
      (CategoryTheory.Precoverage.comap F CategoryTheory.Types.jointlySurjectivePrecoverage).coverings X ↔
    ∀ (x : F.obj X), ∃ i, x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map (f i)))
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool} {k : α}, k ∈ Std.ExtHashSet.filter f m ↔ ∃ (h : k ∈ m), f (m.get k h) = true
-- Mathlib.Topology.Compactness.Lindelof
/-- A compact set `s` is Lindelöf.  -/
IsCompact.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsCompact s → IsLindelof s
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.property : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (self : Manifold.LocalPresentationAt I J n f x P), P f self.domChart self.codChart
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.val_mk : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a : M} (h : a ≠ 0),
  ↑(FiniteArchimedeanClass.mk a h) = ArchimedeanClass.mk a
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.SizedBalancedTree.mk : {α : Type u} →
  {β : α → Type v} →
    {lb ub : ℕ} →
      (impl : Std.DTreeMap.Internal.Impl α β) →
        impl.Balanced → lb ≤ impl.size → impl.size ≤ ub → Std.DTreeMap.Internal.Impl.SizedBalancedTree α β lb ub
-- Std.Async.System
Std.Async.System.instOrdUserId.ord : Std.Async.System.UserId → Std.Async.System.UserId → Ordering
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- `CliffordAlgebra.reverseEquiv` as an `AlgEquiv` to the opposite algebra  -/
CliffordAlgebra.reverseOpEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → CliffordAlgebra Q ≃ₐ[R] (CliffordAlgebra Q)ᵐᵒᵖ
-- Mathlib.Data.Bool.Count
List.count_add_count_not : ∀ (l : List Bool) (b : Bool), List.count b l + List.count (!b) l = l.length
-- Mathlib.Combinatorics.Matroid.Loop
/-- A Matroid is `Loopless` if it has no loop  -/
Matroid.Loopless : {α : Type u_1} → Matroid α → Prop
-- Init.Data.Iterators.Basic
/-- If `it'` is a successor iterator of `it`, then `Rel it' it`.  -/
Std.Iterators.FinitenessRelation.subrelation : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β]
  (self : Std.Iterators.FinitenessRelation α m) {it it' : Std.IterM m β},
  it'.IsPlausibleSuccessorOf it → self.Rel it' it
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- A wide equalizer cone for a parallel family `f`.
 -/
CategoryTheory.Limits.wideEqualizer.trident : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} → (f : J → (X ⟶ Y)) → [CategoryTheory.Limits.HasWideEqualizer f] → CategoryTheory.Limits.Trident f
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.mkH1OfIsTrivial_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} [inst_2 : A.IsTrivial] (g : G) (a : ↑A),
  ((groupHomology.mkH1OfIsTrivial A) (Additive.ofMul (Abelianization.of g))) a =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)
-- Mathlib.MeasureTheory.Function.Floor
Int.measurable_ceil : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [inst_3 : TopologicalSpace R]
  [OrderTopology R] [inst_5 : MeasurableSpace R] [OpensMeasurableSpace R], Measurable Int.ceil
-- Mathlib.Data.Num.Bitwise
PosNum.instHAndNum : HAnd PosNum PosNum Num
-- Mathlib.Topology.Category.Stonean.Limits
Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier : CompHausLike.HasExplicitFiniteCoproducts fun Y => ExtremallyDisconnected ↑Y
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_const_smul₀ : ∀ {G₀ : Type u_2} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [MeasurableConstSMul G₀ α] {c : G₀}, c ≠ 0 → MeasurableEmbedding fun x => c • x
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.Indep.indep_delete_of_disjoint : ∀ {α : Type u_1} {M : Matroid α} {I D : Set α}, M.Indep I → Disjoint I D → (M.delete D).Indep I
-- Mathlib.Data.Rel
/-- The inverse relation : `R.inv x y ↔ R y x`. Note that this is *not* a groupoid inverse.  -/
SetRel.inv : {α : Type u_1} → {β : Type u_2} → SetRel α β → SetRel β α
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.toArray_iter : ∀ {β : Type w} {n : ℕ} {xs : Vector β n}, xs.iter.toArray = xs.toArray
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnNat : Lean.Expr → Int.Internal.Linear.Var → Int.Internal.Linear.Expr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.getConst : Lean.Grind.CommRing.Poly → ℤ
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.sum_finsupport : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s),
  ∀ x₀ ∈ s, ∑ i ∈ ρ.finsupport x₀, (ρ i) x₀ = 1
-- Mathlib.Algebra.Order.Module.Defs
SMulPosReflectLE.toSMulPosReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : PartialOrder α]
  [inst_4 : PartialOrder β] [SMulPosReflectLE α β], SMulPosReflectLT α β
-- Lean.Elab.ParseImportsFast
Lean.PrintImportResult : Type
-- Mathlib.Topology.List
List.Vector.tendsto_cons : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {a : α} {l : List.Vector α n},
  Filter.Tendsto (fun p => p.1 ::ᵥ p.2) (nhds a ×ˢ nhds l) (nhds (a ::ᵥ l))
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_inv : ∀ {R : Type u} [inst : Neg R] (x : Tropical R), Tropical.untrop x⁻¹ = -Tropical.untrop x
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_radius_pos : ∀ (𝕂 : Type u_1) (𝔸 : Type u_2) [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸], 0 < (NormedSpace.expSeries 𝕂 𝔸).radius
-- Init.Grind.Lemmas
Lean.Grind.heq_congr' : ∀ {α β : Sort u} {a₁ b₁ : α} {a₂ b₂ : β}, a₁ ≍ b₂ → b₁ ≍ a₂ → (a₁ = b₁) = (a₂ = b₂)
-- Std.Http.Data.Status
/-- Returns `true` for every status code that has a dedicated named constructor in `Status`.
Used to ensure `Status.other` is never constructed with a code that already has a name.
 -/
Std.Http.isKnownStatusCode : UInt16 → Bool
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost_hom_app_app' : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F]
  {X₁ X₂ : C} {Y₁ Y₂ : D} (e₁ : Y₁ ≅ L.obj X₁) (e₂ : Y₂ ≅ L.obj X₂),
  ((CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost L W F G).hom.app Y₁).app Y₂ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.comp (F.map e₁.hom)
          ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app X₁))
        (CategoryTheory.CategoryStruct.comp (F.map e₂.hom)
          ((CategoryTheory.Localization.Lifting.iso L W G F).hom.app X₂)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ G X₁ X₂)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Lifting.iso L W G F).inv.app
            (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
          (F.map
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ L X₁ X₂)
              (CategoryTheory.MonoidalCategoryStruct.tensorHom e₁.inv e₂.inv)))))
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- If `X` and `Y` are isomorphic, then `X` is terminal iff `Y` is.  -/
CategoryTheory.Limits.IsTerminal.equivOfIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (X ≅ Y) → CategoryTheory.Limits.IsTerminal X ≃ CategoryTheory.Limits.IsTerminal Y
-- Lean.Compiler.IR.Format
Lean.IR.formatParams : Array Lean.IR.Param → Std.Format
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.LaxMonoidalFunctor.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {toFunctor : CategoryTheory.Functor C D}
  {laxMonoidal : autoParam toFunctor.LaxMonoidal CategoryTheory.LaxMonoidalFunctor.laxMonoidal._autoParam}
  {toFunctor_1 : CategoryTheory.Functor C D}
  {laxMonoidal_1 : autoParam toFunctor_1.LaxMonoidal CategoryTheory.LaxMonoidalFunctor.laxMonoidal._autoParam},
  { toFunctor := toFunctor, laxMonoidal := laxMonoidal } = { toFunctor := toFunctor_1, laxMonoidal := laxMonoidal_1 } →
    toFunctor = toFunctor_1 ∧ laxMonoidal ≍ laxMonoidal_1
-- Mathlib.Algebra.Homology.ExactSequenceFour
/-- If `S` is an exact sequence, this is the morphism from a cokernel
of `S.map' k (k + 1)` to a kernel of `S.map' (k + 2) (k + 3)`.  -/
CategoryTheory.ComposableArrows.Exact.cokerToKer' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {n : ℕ} →
        {S : CategoryTheory.ComposableArrows C (n + 3)} →
          S.Exact →
            (k : ℕ) →
              (hk : k ≤ n) →
                (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯)) →
                  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) →
                    CategoryTheory.Limits.IsColimit cc → CategoryTheory.Limits.IsLimit kf → (cc.pt ⟶ kf.pt)
-- Mathlib.Topology.MetricSpace.PiNat
PiCountable.dist_summable : ∀ {ι : Type u_2} [inst : Encodable ι] {F : ι → Type u_3} [inst_1 : (i : ι) → PseudoMetricSpace (F i)]
  (x y : (i : ι) → F i), Summable fun i => min (2⁻¹ ^ Encodable.encode i) (dist (x i) (y i))
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuousWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {s : Set H}
  {x : H}, ContinuousWithinAt (↑I) s x
-- Init.Data.Option.Monadic
Option.forIn_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m] [LawfulMonad m]
  (o : Option α) (g : α → β) (f : β → γ → m (ForInStep γ)),
  forIn (Option.map g o) init f = forIn o init fun a y => f (g a) y
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Implementation of `CommMon.equivLaxBraidedFunctorPUnit`.  -/
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor (CategoryTheory.CommMon C)
          (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C)
-- Mathlib.Order.Minimal
exists_minimalFor_of_wellFoundedLT : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [WellFoundedLT α] (P : ι → Prop) (f : ι → α),
  (∃ i, P i) → ∃ i, MinimalFor P f i
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.SemiRingCat.Hom.mk.sizeOf_spec : ∀ {R S : SemiRingCat} (hom' : ↑R →+* ↑S), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.Analysis.Normed.Group.Basic
norm_sum_le : ∀ {ι : Type u_3} {E : Type u_9} [inst : SeminormedAddCommGroup E] (s : Finset ι) (f : ι → E),
  ‖∑ i ∈ s, f i‖ ≤ ∑ i ∈ s, ‖f i‖
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.j : {n : Type u_1} → {R : Type u₂} → Matrix.TransvectionStruct n R → n
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
SymmetricPower.tprod.eq_1 : ∀ (R : Type u) {ι : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  SymmetricPower.tprod R = (SymmetricPower.mk R ι M).compMultilinearMap (PiTensorProduct.tprod R)
-- Mathlib.Algebra.Order.SuccPred
Order.IsPredLimit.lt_sub_one : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α],
  Order.IsPredLimit x → x < y → x < y - 1
-- Batteries.Recycling.RBTree.Basic
/-- An "iterator" over the values of the map. This is a trivial wrapper over the underlying map,
but it comes with a small API to use it in a `for` loop or convert it to an array or list.
 -/
RBTree.RBMap.Values : (α : Type u_1) → Type u_2 → (α → α → Ordering) → Type (max u_1 u_2)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.smul_induction_on : ∀ {R : Type u_2} {A : Type u_3} [inst : AddMonoid R] [inst_1 : AddMonoid A] [inst_2 : DistribSMul R A]
  {M : AddSubmonoid R} {N : AddSubmonoid A} {C : A → Prop} {a : A},
  a ∈ M • N → (∀ m ∈ M, ∀ n ∈ N, C (m • n)) → (∀ (x y : A), C x → C y → C (x + y)) → C a
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.inv_hom_whiskerRight_whiskerRight_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) (k : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g h) k ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.inv h) k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.hom h) k) h_1) =
    h_1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.opCospan_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Limits.WalkingCospanᵒᵖ),
  (CategoryTheory.Limits.opCospan f g).hom.app X_1 =
    (match Opposite.unop X_1 with
      | none => CategoryTheory.Iso.refl (Opposite.op Z)
      | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl (Opposite.op X)
      | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl (Opposite.op Y)).inv
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.sameCycle_zpow_left`. -/
Equiv.Perm.SameCycle.zpow_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle x y → f.SameCycle ((f ^ n) x) y
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.Functor.Elements.isCorepresentable_of_hasInitial : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w))
  [CategoryTheory.Limits.HasInitial F.Elements], F.IsCorepresentable