mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the product of `X` and `Y` exists, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y`
induces a morphism `l : W ⟶ X ⨯ Y` satisfying `l ≫ Prod.fst = f` and `l ≫ Prod.snd = g`.  -/
CategoryTheory.Limits.prod.lift' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] →
        (f : W ⟶ X) →
          (g : W ⟶ Y) →
            { l //
              CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.fst = f ∧
                CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.snd = g }
-- Mathlib.Algebra.Algebra.Subalgebra.Prod
Subalgebra.prod_toSubmodule : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R A) (S₁ : Subalgebra R B),
  Subalgebra.toSubmodule (S.prod S₁) = (Subalgebra.toSubmodule S).prod (Subalgebra.toSubmodule S₁)
-- Mathlib.CategoryTheory.Functor.Trifunctor
/-- Given two bifunctors `F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂` and `G : C₁₂ ⥤ C₃ ⥤ C₄`, this is
the trifunctor `C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` obtained by composition.  -/
CategoryTheory.bifunctorComp₁₂ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        {C₁₂ : Type u_5} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] →
                    CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂) →
                      CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄) →
                        CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. The number of items in the RBMap.  -/
RBTree.RBMap.size : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → ℕ
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ModuleDocstringState.mk : Lean.Doc.State →
  Array (Lean.ScopedEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState) →
    Lean.Doc.ModuleDocstringState✝
-- Mathlib.Algebra.Group.Submonoid.BigOperators
SubmonoidClass.coe_multiset_prod : ∀ {B : Type u_3} {S : B} {M : Type u_4} [inst : CommMonoid M] [inst_1 : SetLike B M] [inst_2 : SubmonoidClass B M]
  (m : Multiset ↥S), ↑m.prod = (Multiset.map Subtype.val m).prod
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_biUnion_le : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α]
  {I : Set ι} (μ : F), I.Countable → ∀ (s : ι → Set α), μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)
-- Init.Data.Bool
Bool.eq_true_of_true_le : ∀ {x : Bool}, true ≤ x → x = true
-- Std.Async.Basic
/-- Gets the value of the `MaybeTask` by blocking.
 -/
Std.Async.MaybeTask.get : {α : Type} → Std.Async.MaybeTask α → α
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural projection `FreeMonoid (M ⊕ N) →* M ∗ N`.  -/
Monoid.Coprod.mk : {M : Type u_1} →
  {N : Type u_2} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → FreeMonoid (M ⊕ N) →* Monoid.Coprod M N
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that the action of `M` on `α` has `MeasurableSMul₂` if the map
`(c, x) ↦ c • x` is a measurable function.  -/
MeasurableSMul₂ : (M : Type u_2) → (α : Type u_3) → [SMul M α] → [MeasurableSpace M] → [MeasurableSpace α] → Prop
-- Init.Data.Float.Model.Float
Float.Model.mk : (toBits : UInt64) → Float.Model.Format.binary64.Valid toBits.toBitVec → Float.Model
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- Produces an arbitrary representation of the form `mₒ ⊗ₜ n₀ + ...`.  -/
TensorProduct.instRepr : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → [Repr M] → [Repr N] → Repr (TensorProduct R M N)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : SizeOf C] (τ₁ : S₁.X₁ ⟶ S₂.X₁) (τ₂ : S₁.X₂ ⟶ S₂.X₂)
  (τ₃ : S₁.X₃ ⟶ S₂.X₃)
  (comm₁₂ :
    autoParam (CategoryTheory.CategoryStruct.comp τ₁ S₂.f = CategoryTheory.CategoryStruct.comp S₁.f τ₂)
      CategoryTheory.ShortComplex.Hom.comm₁₂._autoParam)
  (comm₂₃ :
    autoParam (CategoryTheory.CategoryStruct.comp τ₂ S₂.g = CategoryTheory.CategoryStruct.comp S₁.g τ₃)
      CategoryTheory.ShortComplex.Hom.comm₂₃._autoParam),
  sizeOf { τ₁ := τ₁, τ₂ := τ₂, τ₃ := τ₃, comm₁₂ := comm₁₂, comm₂₃ := comm₂₃ } =
    1 + sizeOf τ₁ + sizeOf τ₂ + sizeOf τ₃ + sizeOf comm₁₂ + sizeOf comm₂₃
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- Returns `true` if `s` is a variable.  -/
Lean.Grind.AC.Seq.isVar : Lean.Grind.AC.Seq → Bool
-- Aesop.Stats.Basic
Aesop.GoalStats.forwardStateStats : Aesop.GoalStats → Aesop.ForwardStateStats
-- Mathlib.Analysis.Polynomial.Order
Polynomial.eval_le_zero_of_roots_le_of_leadingCoeff_nonpos : ∀ {P : Polynomial ℝ} {x : ℝ}, (∀ (y : ℝ), P.IsRoot y → y ≤ x) → P.leadingCoeff ≤ 0 → Polynomial.eval x P ≤ 0
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (p' q' : ℤ) (hpq' : p' + n = q'),
  p' ≠ p → (CochainComplex.HomComplex.Cochain.toSingleMk f h).v p' q' hpq' = 0
-- Batteries.Data.ByteArray
ByteArray.size_set : ∀ (a : ByteArray) (i : Fin a.size) (v : UInt8), (a.set (↑i) v ⋯).size = a.size
-- Init.Data.List.Basic
List.extract_eq_drop_take : ∀ {α : Type u_1} {l : List α} {start stop : ℕ}, l.extract start stop = List.take (stop - start) (List.drop start l)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_1 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w idx : ℕ)
  (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.var idx with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_1 w idx
-- Mathlib.Topology.Category.Stonean.Basic
/-- `Projective` implies `Stonean`.  -/
CompHaus.toStonean : (X : CompHaus) → [CategoryTheory.Projective X] → Stonean
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.mk.sizeOf_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} [inst_1 : SizeOf K]
  (a b c : NumberField.RingOfIntegers K) (u : (NumberField.RingOfIntegers K)ˣ) (ha : ¬hζ.toInteger - 1 ∣ a)
  (hb : ¬hζ.toInteger - 1 ∣ b) (hc : c ≠ 0) (coprime : IsCoprime a b) (hcdvd : hζ.toInteger - 1 ∣ c)
  (H : a ^ 3 + b ^ 3 = ↑u * c ^ 3),
  sizeOf { a := a, b := b, c := c, u := u, ha := ha, hb := hb, hc := hc, coprime := coprime, hcdvd := hcdvd, H := H } =
    1 + sizeOf a + sizeOf b + sizeOf c + sizeOf u + sizeOf coprime + sizeOf hcdvd + sizeOf H
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l → ∀ {h : k' ∈ m.insertManyIfNewUnit l}, (m.insertManyIfNewUnit l).getKey k' h = k
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.of_mul_right : ∀ {R : Type u} [inst : CommSemiring R] {f g : Polynomial R}, (f * g).Separable → g.Separable
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionHom_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : C} {d d' : D} (f : c ⟶ c') (g : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f.op g.op =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.add_neg'`.  -/
add_neg' : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b : α}, a < 0 → b < 0 → a + b < 0
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_cos_add_sin_mul_I : ∀ {θ : ℝ}, θ ∈ Set.Ioc (-Real.pi) Real.pi → (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg = θ
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
biUnion_associatedPrimes_eq_zero_divisors : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [IsNoetherianRing R], ⋃ p ∈ associatedPrimes R M, ↑p = {r | ∃ x, x ≠ 0 ∧ r • x = 0}
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapM.match_1.splitter : {β β' : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → n (Option β')} →
      [inst : MonadAttach n] →
        (out : β) →
          (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) →
            (__do_lift : Subtype (MonadAttach.CanReturn (f out))) →
              ((hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩) →
                ((out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩) →
                  motive __do_lift
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.ofHom.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y) [inst_1 : W.ContainsIdentities],
  CategoryTheory.MorphismProperty.LeftFraction.ofHom W f =
    { Y' := Y, f := f, s := CategoryTheory.CategoryStruct.id Y, hs := ⋯ }
-- Mathlib.Data.Set.Countable
Set.countable_union : ∀ {α : Type u} {s t : Set α}, (s ∪ t).Countable ↔ s.Countable ∧ t.Countable
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.card : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N},
  Nat.card (N ⋊[φ] G) = Nat.card N * Nat.card G
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α} {k fallback : α}, k ∈ t → (t.insertManyIfNewUnit l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Negating the orientation negates the angle in `rotation`.  -/
Orientation.rotation_neg_orientation_eq_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle), (-o).rotation θ = o.rotation (-θ)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.symm_ofLinearMap : ∀ {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₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (f : M →ₛₗ[σ₁₂] M₂)
  (g : M₂ →ₛₗ[σ₂₁] M) (h₁ : f ∘ₛₗ g = LinearMap.id) (h₂ : g ∘ₛₗ f = LinearMap.id),
  (LinearEquiv.ofLinearMap f g h₁ h₂).symm = LinearEquiv.ofLinearMap g f h₂ h₁
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.GlueData.instPreservesColimitWalkingMultispanProdJMultispanDiagramForget : ∀ (D : AlgebraicGeometry.Scheme.GlueData),
  CategoryTheory.Limits.PreservesColimit D.diagram.multispan AlgebraicGeometry.Scheme.forget
-- Mathlib.Topology.Sheaves.Stalks
/-- The germ of a section of a presheaf over an open at a point of that open.
 -/
TopCat.Presheaf.germ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          (U : TopologicalSpace.Opens ↑X) → (x : ↑X) → x ∈ U → (F.obj (Opposite.op U) ⟶ F.stalk x)
-- Init.Meta.Defs
Lean.MonadNameGenerator.setNGen : {m : Type → Type} → [self : Lean.MonadNameGenerator m] → Lean.NameGenerator → m Unit
-- Std.Sat.AIG.Basic
/-- The reference to the node in `aig` that this `Entrypoint` targets.
 -/
Std.Sat.AIG.Entrypoint.ref : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → (self : Std.Sat.AIG.Entrypoint α) → self.aig.Ref
-- Init.Data.Int.Order
Int.sub_le_sub_left_iff : ∀ {a b c : ℤ}, c - a ≤ c - b ↔ b ≤ a
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.toComposition_length : ∀ {n : ℕ} (c : CompositionAsSet n), c.toComposition.length = c.length
-- Mathlib.Order.Bounds.Defs
/-- A set is coinitial when for every `x : α` there exists `y ∈ s` with `y ≤ x`.  -/
IsCoinitial : {α : Type u_1} → [LE α] → Set α → Prop
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the right unitor.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityRightUnitor : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Lean.Expr
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.mk.sizeOf_spec : ∀ {J : Type u} (U : J → TopCat) (V : (i : J) → J → TopologicalSpace.Opens ↑(U i))
  (t :
    (i j : J) →
      (TopologicalSpace.Opens.toTopCat (U i)).obj (V i j) ⟶ (TopologicalSpace.Opens.toTopCat (U j)).obj (V j i))
  (V_id : ∀ (i : J), V i i = ⊤) (t_id : ∀ (i : J), ⇑(CategoryTheory.ConcreteCategory.hom (t i i)) = id)
  (t_inter :
    ∀ ⦃i j : J⦄ (k : J) (x : ↥(V i j)), ↑x ∈ V i k → ↑((CategoryTheory.ConcreteCategory.hom (t i j)) x) ∈ V j k)
  (cocycle :
    ∀ (i j k : J) (x : ↥(V i j)) (h : ↑x ∈ V i k),
      ↑((CategoryTheory.ConcreteCategory.hom (t j k)) ⟨↑((CategoryTheory.ConcreteCategory.hom (t i j)) x), ⋯⟩) =
        ↑((CategoryTheory.ConcreteCategory.hom (t i k)) ⟨↑x, h⟩)),
  sizeOf { J := J, U := U, V := V, t := t, V_id := V_id, t_id := t_id, t_inter := t_inter, cocycle := cocycle } =
    1 + sizeOf J
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.toPreOneHypercover_Y : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (x x_1 : data.I₀)
  (j : data.I₁ x x_1), data.toPreOneHypercover.Y j = F.obj (data.Y j)
-- Mathlib.Data.PFun
/-- Restrict a partial function to a smaller domain.  -/
PFun.restrict : {α : Type u_1} → {β : Type u_2} → (f : α →. β) → {p : Set α} → p ⊆ f.Dom → α →. β
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.hcdvd : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3}
  (self : FermatLastTheoremForThreeGen.Solution'✝ hζ), hζ.toInteger - 1 ∣ FermatLastTheoremForThreeGen.Solution'.c✝ self
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ExtendTarget.w : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {newWidth : ℕ} → aig.ExtendTarget newWidth → ℕ
-- Init.Prelude
/-- Assuming `stx` was parsed by `optional`, returns the enclosed syntax
if it parsed something and `none` otherwise.
 -/
Lean.Syntax.getOptional? : Lean.Syntax → Option Lean.Syntax
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.nsmul_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : ℕ) (m : M) (s : ℕ+),
  a • DivisibleHull.mk m s = DivisibleHull.mk (a • m) s
-- Std.Time.Format.DateFormat
Std.Time.DateFormatSymbols.mk : Vector String 12 →
  Vector String 12 →
    Vector String 12 →
      Vector String 7 →
        Vector String 7 →
          Vector String 7 →
            Vector String 7 →
              Vector String 2 →
                Vector String 2 →
                  Vector String 2 →
                    Vector String 4 →
                      Vector String 4 →
                        Vector String 4 →
                          String →
                            String →
                              String →
                                String →
                                  String →
                                    String →
                                      Std.Time.DayPeriodSymbols →
                                        Std.Time.DayPeriodSymbols →
                                          Std.Time.DayPeriodSymbols →
                                            Vector String 6 →
                                              Vector String 6 → Vector String 6 → Std.Time.DateFormatSymbols
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.PreservesFiniteLimitsOfFlat.uniq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type v₁} [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J]
  (F : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat F] {K : CategoryTheory.Functor J C}
  {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone (K.comp F))
  (f₁ f₂ : s.pt ⟶ F.obj c.pt),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp f₁ ((F.mapCone c).π.app j) = s.π.app j) →
    (∀ (j : J), CategoryTheory.CategoryStruct.comp f₂ ((F.mapCone c).π.app j) = s.π.app j) → f₁ = f₂
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whisker_ι : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  (E : CategoryTheory.Functor K J) (c : CategoryTheory.Limits.Cocone F),
  (CategoryTheory.Limits.Cocone.whisker E c).ι = E.whiskerLeft c.ι
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.isRatCondKernelCDF : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel ν],
      ProbabilityTheory.IsRatCondKernelCDF f κ ν
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instLawfulEqOrdOffset : Std.LawfulEqOrd Std.Time.Millisecond.Offset
-- Init.Data.Array.Basic
/-- Returns the first element of the array for which the predicate `p` returns `true`, or `none` if no
such element is found.

Examples:
* `#[7, 6, 5, 8, 1, 2, 6].find? (· < 5) = some 1`
* `#[7, 6, 5, 8, 1, 2, 6].find? (· < 1) = none`
 -/
Array.find? : {α : Type u} → (α → Bool) → Array α → Option α
-- Lean.LocalContext
Lean.LocalDecl.replaceFVarId : Lean.FVarId → Lean.Expr → Lean.LocalDecl → Lean.LocalDecl
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_min_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {s : Multiset ι}
  {f g : ι → α}, (Multiset.map (fun i => min (f i) (g i)) s).prod ≤ min (Multiset.map f s).prod (Multiset.map g s).prod
-- Batteries.Recycling.RBTree.Basic
/-- `O(n₂ * log (n₁ + n₂))`. Merges the maps `t₁` and `t₂`. If equal keys exist in both,
then use `mergeFn a₁ a₂` to produce the new merged value.
 -/
RBTree.RBSet.mergeWith : {α : Type u_1} → {cmp : α → α → Ordering} → (α → α → α) → RBTree.RBSet α cmp → RBTree.RBSet α cmp → RBTree.RBSet α cmp
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
spectrum_realPart' : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) spectrum_realPart'._auto_1 → spectrum ℝ ↑(realPart a) = Complex.re '' spectrum ℂ a
-- Mathlib.ModelTheory.Syntax
/-- Restricts a term to use only a set of the given variables.  -/
FirstOrder.Language.Term.restrictVar : {L : FirstOrder.Language} →
  {α : Type u'} → {β : Type v'} → [inst : DecidableEq α] → (t : L.Term α) → (↥t.varFinset → β) → L.Term β
-- Mathlib.Data.ENNReal.Action
ENNReal.nnreal_smul_lt_top_iff : ∀ {x : NNReal} {y : ENNReal}, x ≠ 0 → (x • y < ⊤ ↔ y < ⊤)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mk.inj : ∀ {ι : 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} {inst_5 : FiniteDimensional ℝ E} {s : Set M} {c : ι → M}
  {toFun : (i : ι) → SmoothBumpFunction I (c i)} {c_mem' : ∀ (i : ι), c i ∈ s}
  {locallyFinite' : LocallyFinite fun i => Function.support ↑(toFun i)}
  {eventuallyEq_one' : ∀ x ∈ s, ∃ i, ↑(toFun i) =ᶠ[nhds x] 1} {c_1 : ι → M}
  {toFun_1 : (i : ι) → SmoothBumpFunction I (c_1 i)} {c_mem'_1 : ∀ (i : ι), c_1 i ∈ s}
  {locallyFinite'_1 : LocallyFinite fun i => Function.support ↑(toFun_1 i)}
  {eventuallyEq_one'_1 : ∀ x ∈ s, ∃ i, ↑(toFun_1 i) =ᶠ[nhds x] 1},
  { c := c, toFun := toFun, c_mem' := c_mem', locallyFinite' := locallyFinite',
        eventuallyEq_one' := eventuallyEq_one' } =
      { c := c_1, toFun := toFun_1, c_mem' := c_mem'_1, locallyFinite' := locallyFinite'_1,
        eventuallyEq_one' := eventuallyEq_one'_1 } →
    c = c_1 ∧ toFun ≍ toFun_1
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.ObjectProperty.fullSubcategoryCongr_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P'),
  (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).functor = CategoryTheory.ObjectProperty.ιOfLE ⋯