mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.Lemmas
List.getElem?_insert : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List α} {a : α} {i : ℕ},
  (List.insert a l)[i]? = if a ∈ l then l[i]? else if i = 0 then some a else l[i - 1]?
-- Mathlib.Algebra.Module.Equiv.Basic
/-- Between two zero modules, the zero map is an equivalence.  -/
LinearEquiv.instZero : {R : Type u_1} →
  {R₂ : Type u_2} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      {σ₂₁ : R₂ →+* R} →
                        [inst_6 : RingHomInvPair σ₁₂ σ₂₁] →
                          [inst_7 : RingHomInvPair σ₂₁ σ₁₂] →
                            [Subsingleton M] → [Subsingleton M₂] → Zero (M ≃ₛₗ[σ₁₂] M₂)
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- When `K` is a cochain complex indexed by `ℤ`, this is the isomorphism
`(K.truncGE n).X n ≅ K.opcycles n`.  -/
CochainComplex.truncGEXIsoOpcycles : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_3, u_2} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        (K : CochainComplex C ℤ) →
          [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] →
            (n : ℤ) → (K.truncGE n).X n ≅ HomologicalComplex.opcycles K n
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.instSMulCommClass' : ∀ {R' : Type u'} {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] (S : NonUnitalStarSubalgebra R A) [inst_4 : Semiring R'] [inst_5 : SMul R' R]
  [inst_6 : Module R' A] [inst_7 : IsScalarTower R' R A] [SMulCommClass R' R A], SMulCommClass R' R ↥S
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.Functor.instIsEquivalence : ∀ {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) [F.IsIso], F.IsEquivalence
-- Mathlib.Algebra.Group.Translate
translate_neg_right : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] [inst_1 : Neg α] (a : G) (f : G → α),
  translate a (-f) = -translate a f
-- Init.Tactics
/-- `show t` finds the first goal whose target unifies with `t`. It makes that the main goal,
performs the unification, and replaces the target with the unified version of `t`.
 -/
Lean.Parser.Tactic.show : Lean.ParserDescr
-- Init.MetaTypes
/-- When `true` (default: `false`), rewrites a proposition `p` to `True` or `False` by inferring
a `Decidable p` instance and reducing it.
 -/
Lean.Meta.Simp.Config.decide : Lean.Meta.Simp.Config → Bool
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.instNormedCommRing : (p : ℕ) → [hp : Fact (Nat.Prime p)] → NormedCommRing ℤ_[p]
-- Lean.Parser.Attr
Lean.Parser.Attr.instance.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_zsmul : ∀ {α : Type u_1} {N : Type u_16} [inst : SubtractionCommMonoid N] [inst_1 : Fintype α] (f : α →₀ ℤ) (g : α → N),
  (f.sum fun a b => b • g a) = ∑ a, f a • g a
-- Mathlib.Topology.Sets.Closeds
/-- The preimage of a closed set under a continuous map.  -/
TopologicalSpace.Closeds.preimage : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        TopologicalSpace.Closeds β → {f : α → β} → Continuous f → TopologicalSpace.Closeds α
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.mk : {α : Type w} → Array α → ℕ → Std.Iterators.Types.ArrayIterator α
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.equivalenceOfIsInitial_inverse_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X) (Y : T),
  (CategoryTheory.Under.equivalenceOfIsInitial hX).inverse.obj Y = CategoryTheory.Under.mk (hX.to Y)
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (aig : Std.Sat.AIG α) →
        aig.Ref →
          ℕ →
            (len : ℕ) →
              aig.RefVec len →
                (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α) →
                  [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] → Std.Sat.AIG.Entrypoint α
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.naturality_2'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ⟶ G) (f : X ⟶ Y) {x : CategoryTheory.IsIso (α.app Y)} {Z : D}
  (h : F.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.app X)
      (CategoryTheory.CategoryStruct.comp (G.map f)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (α.app Y)) h)) =
    CategoryTheory.CategoryStruct.comp (F.map f) h
-- Mathlib.Data.Set.Lattice
Set.sInter_eq_compl_sUnion_compl : ∀ {α : Type u_1} (S : Set (Set α)), ⋂₀ S = (⋃₀ (compl '' S))ᶜ
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `add_apply`. -/
GroupSeminorm.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.isIso_homologyMap_of_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [CategoryTheory.IsIso φ], CategoryTheory.IsIso (CategoryTheory.ShortComplex.homologyMap φ)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contStack.eq_4 : ∀ (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.contStack (Turing.ToPartrec.Cont.comp c k) = Turing.PartrecToTM2.contStack k
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.Realize.match_1.splitter : {L : FirstOrder.Language} →
  {M : Type u_5} →
    {α : Type u_3} →
      (motive : (x : ℕ) → L.BoundedFormula α x → (α → M) → (Fin x → M) → Sort u_4) →
        (x : ℕ) →
          (x_1 : L.BoundedFormula α x) →
            (x_2 : α → M) →
              (x_3 : Fin x → M) →
                ((x : ℕ) →
                    (_v : α → M) → (_xs : Fin x → M) → motive x FirstOrder.Language.BoundedFormula.falsum _v _xs) →
                  ((x : ℕ) →
                      (t₁ t₂ : L.Term (α ⊕ Fin x)) →
                        (v : α → M) →
                          (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂) v xs) →
                    ((x l : ℕ) →
                        (R : L.Relations l) →
                          (ts : Fin l → L.Term (α ⊕ Fin x)) →
                            (v : α → M) →
                              (xs : Fin x → M) → motive x (FirstOrder.Language.BoundedFormula.rel R ts) v xs) →
                      ((x : ℕ) →
                          (f₁ f₂ : L.BoundedFormula α x) → (v : α → M) → (xs : Fin x → M) → motive x (f₁.imp f₂) v xs) →
                        ((x : ℕ) →
                            (f : L.BoundedFormula α (x + 1)) → (v : α → M) → (xs : Fin x → M) → motive x f.all v xs) →
                          motive x x_1 x_2 x_3
-- Mathlib.Order.Filter.AtTopBot.Map
OrderIso.tendsto_atBot_iff : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β] {l : Filter γ} {f : γ → α}
  (e : α ≃o β), Filter.Tendsto (fun x => e (f x)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.eq_3 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none),
  (match none with
    | some (some c) => h_1 c
    | some none => h_2 ()
    | none => h_3 ()) =
    h_3 ()
-- Mathlib.Order.Filter.Basic
Filter.eventually_const : ∀ {α : Type u} {f : Filter α} [t : f.NeBot] {p : Prop}, (∀ᶠ (x : α) in f, p) ↔ p
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Result.rfl.inj : ∀ {done done_1 : Bool}, Lean.Meta.Sym.DSimp.Result.rfl done = Lean.Meta.Sym.DSimp.Result.rfl done_1 → done = done_1
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_zero : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Zero α],
  Matrix.fromBlocks 0 0 0 0 = 0
-- Lean.Linter.Deprecated
Lean.Linter.instInhabitedDeprecationEntry.default : Lean.Linter.DeprecationEntry
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.point_mem_logSizeBallSeq_init : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ), (PairReduction.logSizeBallSeq J hJ a c i).point ∈ J
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.ucs_eq_self_of_normalizer_eq_self : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] {N₁ : LieSubmodule R L M}
  [inst_6 : LieModule R L M], N₁.normalizer = N₁ → ∀ (k : ℕ), LieSubmodule.ucs k N₁ = N₁
-- Mathlib.Algebra.Ring.Parity
Nat.two_dvd_mul_sub_one : ∀ (k : ℕ), 2 ∣ k * (k - 1)
-- Mathlib.Data.Rat.Floor
/-- `norm_num` extension for `Int.ceil`  -/
Rat.evalIntCeil : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_uIcc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι] (f : (i : ι) → α i)
  (i : ι) (a b : α i), Function.update f i '' Set.uIcc a b = Set.uIcc (Function.update f i a) (Function.update f i b)
-- Mathlib.Algebra.Quaternion
/-- `QuaternionAlgebra.re` as a `LinearMap`  -/
QuaternionAlgebra.reₗ : {R : Type u_3} → (c₁ c₂ c₃ : R) → [inst : CommRing R] → QuaternionAlgebra R c₁ c₂ c₃ →ₗ[R] R
-- Mathlib.Order.RelIso.Basic
RelHomClass.irrefl : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} {F : Type u_5} [inst : FunLike F α β]
  [RelHomClass F r s] (f : F) [Std.Irrefl s], Std.Irrefl r
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit.match_1.eq_1 : ∀ {n : ℕ}
  (motive :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment →
      Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
  (b : Bool)
  (h_1 :
    (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
      (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → (b : Bool) → motive assignments (l, b)),
  (match assignments, (l, b) with
    | assignments, (l, b) => h_1 assignments l b) =
    h_1 assignments l b
-- Mathlib.Order.Fin.Basic
Fin.addNatOrderEmb_apply : ∀ {n : ℕ} (m : ℕ) (x : Fin n), (Fin.addNatOrderEmb m) x = x.addNat m
-- Lean.LocalContext
Lean.instInhabitedLocalContext.default : Lean.LocalContext
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k : α}, (Std.DHashMap.Const.insertManyIfNewUnit m l).contains k = (m.contains k || l.contains k)
-- Mathlib.Data.Set.Disjoint
Set.disjoint_union_left : ∀ {α : Type u} {s t u : Set α}, Disjoint (s ∪ t) u ↔ Disjoint s u ∧ Disjoint t u
-- Mathlib.CategoryTheory.Limits.Shapes.KernelPair
CategoryTheory.IsKernelPair.instInhabitedIdOfMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [CategoryTheory.Mono f] →
          Inhabited
            (CategoryTheory.IsKernelPair f (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
InnerProductSpace.HarmonicContOnCl.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] (f f_1 : E → F),
  f = f_1 →
    ∀ (s s_1 : Set E), s = s_1 → InnerProductSpace.HarmonicContOnCl f s = InnerProductSpace.HarmonicContOnCl f_1 s_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingular_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 → (W.Nonsingular P ↔ W.toAffine.Nonsingular (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3))
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is positive, the first two points are not
equal.  -/
EuclideanGeometry.left_ne_of_oangle_sign_eq_one : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = 1 → p₁ ≠ p₂
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β → ENNReal}
  (κ : ProbabilityTheory.Kernel α β) [inst : ProbabilityTheory.IsSFiniteKernel κ],
  Measurable (Function.uncurry f) → ∀ (a : α) (s : Set β), ((κ.withDensity f) a) s = ∫⁻ (b : β) in s, f a b ∂κ a
-- Mathlib.Order.Interval.Set.OrdConnected
/-- In a dense order `α`, the subtype from an `OrdConnected` set is also densely ordered.  -/
Set.instDenselyOrdered : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {s : Set α} [hs : s.OrdConnected], DenselyOrdered ↑s
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_monomial : ∀ {R : Type u_1} [inst : Semiring R] (N n : ℕ),
  Polynomial.reflect N (Polynomial.X ^ n) = Polynomial.X ^ (Polynomial.revAt N) n
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- `Module.Free R M` is the statement that the `R`-module `M` is free.  -/
Module.Free : (R : Type u) → (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.findAtom_ne_bot : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] [inst_3 : OrderBot α]
  [inst_4 : DecidableEq α] {r : α}, IsPredArchimedean.findAtom r ≠ ⊥ ↔ r ≠ ⊥
-- Init.Data.List.Lemmas
List.getElem?_reverse : ∀ {α : Type u_1} {l : List α} {i : ℕ}, i < l.length → l.reverse[i]? = l[l.length - 1 - i]?
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.instOne : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubgroupClass σ A] →
            [inst_3 : AddCommMonoid ι] →
              [inst_4 : DecidableEq ι] →
                {𝒜 : ι → σ} → [GradedRing 𝒜] → (x : Submonoid A) → One (HomogeneousLocalization 𝒜 x)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorCore.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : SizeOf B] [inst_3 : SizeOf C] (toStrictPseudofunctorPreCore : CategoryTheory.StrictPseudofunctorPreCore B C)
  (map₂_left_unitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.Bicategory.leftUnitor (toStrictPseudofunctorPreCore.map f)).hom)
      CategoryTheory.StrictPseudofunctorCore.map₂_left_unitor._autoParam)
  (map₂_right_unitor :
    autoParam
      (∀ {a b : B} (f : a ⟶ b),
        toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.Bicategory.rightUnitor (toStrictPseudofunctorPreCore.map f)).hom)
      CategoryTheory.StrictPseudofunctorCore.map₂_right_unitor._autoParam)
  (map₂_associator :
    autoParam
      (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
        toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.associator f g h).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (toStrictPseudofunctorPreCore.map f)
                  (toStrictPseudofunctorPreCore.map g) (toStrictPseudofunctorPreCore.map h)).hom
              (CategoryTheory.eqToHom ⋯)))
      CategoryTheory.StrictPseudofunctorCore.map₂_associator._autoParam),
  sizeOf
      { toStrictPseudofunctorPreCore := toStrictPseudofunctorPreCore, map₂_left_unitor := map₂_left_unitor,
        map₂_right_unitor := map₂_right_unitor, map₂_associator := map₂_associator } =
    1 + sizeOf toStrictPseudofunctorPreCore
-- Mathlib.Data.List.Permutation
List.perm_of_mem_permutationsAux : ∀ {α : Type u_1} {ts is l : List α}, l ∈ ts.permutationsAux is → l.Perm (ts ++ is)
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_mul_pos_iff : ∀ {K : Type u_1} [inst : RCLike K] (x : ℝ) (z : K), 0 < ↑x * z ↔ x < 0 ∧ z < 0 ∨ 0 < x ∧ 0 < z
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_norm_poly : ∀ (ctx : Int.Internal.Linear.Context) (d : ℤ) (p p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote' ctx p = Int.Internal.Linear.Poly.denote' ctx p' →
    d ∣ Int.Internal.Linear.Poly.denote' ctx p → d ∣ Int.Internal.Linear.Poly.denote' ctx p'
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_image_le : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, s.Finite → Nat.card ↑(f '' s) ≤ Nat.card ↑s
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_neg : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i), ⇑(-g) = -⇑g
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- An `AddSubmonoid` of an `AddCommMonoid` is an `AddCommMonoid`.  -/
AddSubmonoidClass.toAddCommMonoid : {M : Type u_5} →
  [inst : AddCommMonoid M] →
    {A : Type u_4} → [inst_1 : SetLike A M] → [AddSubmonoidClass A M] → (S : A) → AddCommMonoid ↥S
-- Init.Data.Option.List
Option.forIn'_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (o : Option α) (b : β)
  (f : (a : α) → a ∈ o.toList → β → m (ForInStep β)), forIn' o.toList b f = forIn' o b fun a m b => f a ⋯ b
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap'_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.RightHomologyData)
  (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) {Z : C} (h : h₃.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.opcyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ₁ h₁ h₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap' φ₂ h₂ h₃) h)
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instSMulPosStrictMono : ∀ {ι : Type u_1} {α : Type u_3} {β : ι → Type u_4} [inst : Semiring α] [inst_1 : PartialOrder α]
  [inst_2 : (i : ι) → AddCommMonoid (β i)] [inst_3 : (i : ι) → PartialOrder (β i)] [inst_4 : (i : ι) → Module α (β i)]
  [∀ (i : ι), SMulPosStrictMono α (β i)], SMulPosStrictMono α (Π₀ (i : ι), β i)
-- Mathlib.Probability.Kernel.Disintegration.Basic
ProbabilityTheory.Kernel.IsCondKernel.mk : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α (β × Ω)} {κCond : ProbabilityTheory.Kernel (α × β) Ω},
  κ.fst.compProd κCond = κ → κ.IsCondKernel κCond
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertManyIfNewUnit_cons : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {l : List α} {k : α},
  m.insertManyIfNewUnit (k :: l) = (m.insertIfNew k ()).insertManyIfNewUnit l
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.sum_finset_product : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ)
  (t : γ → Finset α),
  (∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) → ∀ {f : γ × α → β}, ∑ p ∈ r, f p = ∑ c ∈ s, ∑ a ∈ t c, f (c, a)
-- Mathlib.Algebra.Group.Action.Faithful
FaithfulSMul.trans : ∀ (R : Type u_4) (S : Type u_5) (T : Type u_6) [inst : Monoid S] [inst_1 : MulOneClass T] [inst_2 : SMul R S]
  [IsScalarTower R S S] [inst_4 : MulAction S T] [IsScalarTower S T T] [inst_6 : SMul R T] [IsScalarTower R T T]
  [IsScalarTower R S T] [FaithfulSMul R S] [FaithfulSMul S T], FaithfulSMul R T
-- Std.Data.Internal.List.Associative
Std.Internal.List.eq_getKey_getValue_of_getEntry?_eq_some : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {k : α} {y : (_ : α) × β}
  (h : Std.Internal.List.getEntry? k l = some y), y = ⟨Std.Internal.List.getKey k l ⋯, Std.Internal.List.getValue k l ⋯⟩
-- Mathlib.Data.Fintype.Sets
Set.coe_toFinset : ∀ {α : Type u_1} (s : Set α) [inst : Fintype ↑s], ↑s.toFinset = s
-- Mathlib.CategoryTheory.Sites.Descent.IsStack
CategoryTheory.Pseudofunctor.IsStack.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C} [toIsPrestack : F.IsPrestack J],
  (∀ {S : C}, ∀ R ∈ J S, (F.toDescentData fun f => f.obj.hom).EssSurj) → F.IsStack J
-- Mathlib.Algebra.Order.Module.Defs
smul_min_of_nonpos : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : AddCommGroup β]
  [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β] [PosSMulMono α β] {a : α},
  a ≤ 0 → ∀ (b₁ b₂ : β), a • min b₁ b₂ = max (a • b₁) (a • b₂)
-- Lean.DocString.Parser
/-- The specific list type and its indicator style  -/
Lean.Doc.Parser.InList.type : Lean.Doc.Parser.InList → Lean.Doc.Parser.OrderedListType ⊕ Lean.Doc.Parser.UnorderedListType
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- A function is differentiable on two open sets iff it is differentiable on their union.  -/
differentiableOn_union_iff_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {s t : Set E},
  IsOpen s → IsOpen t → (DifferentiableOn 𝕜 f (s ∪ t) ↔ DifferentiableOn 𝕜 f s ∧ DifferentiableOn 𝕜 f t)
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderivWithin_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} (c : F), fderivWithin 𝕜 (Function.const E c) s = 0