mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.go.eq_def : ∀ (pat : String.Slice) (table : Array ℕ) (ht₀ : 0 < table.size) (ht : table.size ≤ pat.utf8ByteSize)
  (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i),
  String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat table ht₀ ht h =
    if hs : table.size < pat.utf8ByteSize then
      let patByte := pat.getUTF8Byte { byteIdx := table.size } hs;
      let dist :=
        String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h
          table[table.size - 1] ⋯;
      String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat (table.push ↑dist) ⋯ ⋯ ⋯
    else Vector.mk table ⋯
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- The evaluation `SingleFunctors C D A ⥤ C ⥤ D` for some `a : A`.  -/
CategoryTheory.SingleFunctors.evaluation : (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] →
        {A : Type u_5} →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift D A] →
              A → CategoryTheory.Functor (CategoryTheory.SingleFunctors C D A) (CategoryTheory.Functor C D)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The codomain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.tgtM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₁ m] →
      Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.add_apply : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  {s t : HahnSeries.SummableFamily Γ R α} {a : α}, (s + t) a = s a + t a
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.combineCocones_ι_app_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) (j : J) (k : K),
  ((CategoryTheory.Limits.combineCocones F c).ι.app j).app k = (c k).cocone.ι.app j
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_truncGTIsoTruncGE_inv_ι_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C}
  (h_1 : (t.truncGT a).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ b).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncGTIsoTruncGE a b h).inv.app X) h_1) =
    CategoryTheory.CategoryStruct.comp ((t.truncGTπ a).app X) h_1
-- Batteries.Data.Int
Int.ofBits.eq_1 : ∀ {n : ℕ} (f : Fin n → Bool),
  Int.ofBits f = if 2 * Nat.ofBits f < 2 ^ n then Int.ofNat (Nat.ofBits f) else Int.subNatNat (Nat.ofBits f) (2 ^ n)
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctorMap.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ L₁ : HomologicalComplex C₁ c₁} {K₂ L₂ : HomologicalComplex C₂ c₂}
  (f₁ : K₁ ⟶ L₁) (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J)
  [inst_8 : TotalComplexShape c₁ c₂ c] [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : L₁.HasMapBifunctor L₂ F c]
  [inst_11 : DecidableEq J],
  HomologicalComplex.mapBifunctorMap f₁ f₂ F c =
    HomologicalComplex₂.total.map
      (CategoryTheory.CategoryStruct.comp (((F.mapBifunctorHomologicalComplex c₁ c₂).map f₁).app K₂)
        (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).map f₂))
      c
-- Init.Data.Order.MinMaxOn
minOn.congr_simp : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (x x_1 : α), x = x_1 → ∀ (y y_1 : α), y = y_1 → minOn f x y = minOn f_1 x_1 y_1
-- Init.Data.BitVec.Lemmas
BitVec.two_mul : ∀ {w : ℕ} {x : BitVec w}, 2#w * x = x + x
-- Mathlib.Computability.TuringMachine.Tape
Turing.ListBlank.cons_flatMap : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (a : Γ) (l : Turing.ListBlank Γ)
  (f : Γ → List Γ') (hf : ∃ n, f default = List.replicate n default),
  (Turing.ListBlank.cons a l).flatMap f hf = Turing.ListBlank.append (f a) (l.flatMap f hf)
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.zsmul_self : ∀ {G : Type u_1} [inst : AddGroup G] (a : G) (n : ℤ), AddCommute (n • a) a
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_ge_three_eq_one : ∀ (n m : ℕ), hyperoperation (n + 3) m 0 = 1
-- Mathlib.NumberTheory.Dioph
PFun.fn.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α), f.fn a = (f a).get
-- Init.Data.Vector.Lex
Vector.append_left_lt : ∀ {α : Type u_1} {n m : ℕ} [inst : LT α] {xs : Vector α n} {ys ys' : Vector α m}, ys < ys' → xs ++ ys < xs ++ ys'
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.coe_range : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), ↑φ.range = Set.range ⇑φ
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_comp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f g : CategoryTheory.Subobject A), CategoryTheory.CategoryStruct.comp ((f ⊓ g).ofLE g ⋯) g.arrow = (f ⊓ g).arrow
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.get_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α fun x => β} {a : α}
  {h : Std.DHashMap.Internal.AssocList.contains a l = true},
  Std.DHashMap.Internal.AssocList.get a l h = Std.Internal.List.getValue a l.toList ⋯
-- ProofWidgets.Cancellable
ProofWidgets.CancellableTask : Type
-- Mathlib.Topology.PartitionOfUnity
/-- If `f` is a partition of unity on `s`, then for every `x ∈ s` there exists an index `i` such
that `0 < f i x`.  -/
PartitionOfUnity.exists_pos : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (f : PartitionOfUnity ι X s) {x : X},
  x ∈ s → ∃ i, 0 < (f i) x
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.C_apply : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonAssocSemiring R] (a : R), HahnSeries.C a = (HahnSeries.single 0) a
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.isStarNormal : ∀ {R : Type u_3} [inst : Mul R] [inst_1 : Star R] {x : R}, IsSelfAdjoint x → IsStarNormal x
-- Mathlib.Order.Hom.Lattice
LatticeHom.dual_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (a : α),
  (LatticeHom.dual f) a = f a
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.tensor_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {W X Y Z : C} (f : W ⟶ X)
  (g h : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f (g + h) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f g + CategoryTheory.MonoidalCategoryStruct.tensorHom f h
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, the forgetful functor from `AddCommGrpCat.{u}`
preserves limits of shape `J`.  -/
AddCommGrpCat.forget_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget AddCommGrpCat)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.C_injective : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R], Function.Injective ⇑MvPowerSeries.C
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
Monotone.csSup_image_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] [inst_1 : Preorder α] {f : α → β},
  Monotone f → ∀ {s : Set α}, s.Nonempty → ∀ {B : α}, B ∈ upperBounds s → sSup (f '' s) ≤ f B
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.cond : ∀ {R : Type u_1} [inst : CommRing R] (self : StandardEtalePair R),
  ∃ p₁ p₂ n, Polynomial.derivative self.f * p₁ + self.f * p₂ = self.g ^ n
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.ne_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] {a b : α}, FiniteMultiplicity a b → b ≠ 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
cmp_mul_left' : ∀ {α : Type u_3} [inst : Mul α] [inst_1 : LinearOrder α] [MulLeftStrictMono α] (a b c : α),
  cmp (a * b) (a * c) = cmp b c
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.natMul.injEq : ∀ (k : ℕ) (a : Lean.Grind.Linarith.Expr) (k_1 : ℕ) (a_1 : Lean.Grind.Linarith.Expr),
  (Lean.Grind.Linarith.Expr.natMul k a = Lean.Grind.Linarith.Expr.natMul k_1 a_1) = (k = k_1 ∧ a = a_1)
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
/-- A continuous function with compact support on a product space can be uniformly approximated by
simple functions. The subtlety is that we do not assume that the spaces are separable, so the
product of the Borel sigma algebras might not contain all open sets, but still it contains enough
of them to approximate compactly supported continuous functions.  -/
HasCompactSupport.exists_simpleFunc_approx_of_prod : ∀ {X : Type u_3} {Y : Type u_4} {α : Type u_5} [inst : Zero α] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : MeasurableSpace X] [inst_4 : MeasurableSpace Y] [OpensMeasurableSpace X]
  [OpensMeasurableSpace Y] [inst_7 : PseudoMetricSpace α] {f : X × Y → α},
  Continuous f → HasCompactSupport f → ∀ {ε : ℝ}, 0 < ε → ∃ g, ∀ (x : X × Y), dist (f x) (g x) < ε
-- Std.Http.Protocol.H1.Reader
/-- Advances the input iterator by n bytes.
 -/
Std.Http.Protocol.H1.Reader.advance : {dir : Std.Http.Protocol.H1.Direction} → ℕ → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.forget₂_map_hom_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {X_1 Y : TopCat} (f : X_1 ⟶ Y) (a : ↑X_1),
  (CategoryTheory.HasForget₂.forget₂.map f).hom a = (CategoryTheory.ConcreteCategory.hom f) a
-- Mathlib.LinearAlgebra.Dimension.Torsion.Finite
Module.rank_eq_zero_iff_isTorsion : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M],
  Module.rank R M = 0 ↔ Module.IsTorsion R M
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
MeasureTheory.tendstoInMeasure_iff_tendsto_toNNReal : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : EDist E]
  [MeasureTheory.IsFiniteMeasure μ] {f : ι → α → E} {l : Filter ι} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f l g ↔
    ∀ (ε : ENNReal), 0 < ε → Filter.Tendsto (fun i => (μ {x | ε ≤ edist (f i x) (g x)}).toNNReal) l (nhds 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.functoriality_full : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {D : Type uD} [inst_2 : CategoryTheory.Category.{uD', uD} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {F : J → C} (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [G.Full] [G.Faithful], (CategoryTheory.Limits.Bicones.functoriality F G).Full
-- Mathlib.Algebra.Group.Center
Set.decidableMemAddCenter : {M : Type u_1} →
  [inst : AddSemigroup M] →
    [(a : M) → Decidable (∀ (b : M), b + a = a + b)] → DecidablePred fun x => x ∈ Set.addCenter M
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Nanosecond.Ordinal n
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.comp_quasiMeasurePreserving : ∀ {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure δ} {f : α → δ} {g : δ → β},
  AEMeasurable g ν → MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → AEMeasurable (g ∘ f) μ
-- Init.Data.List.Basic
List.mapTR_loop_eq : ∀ {α : Type u} {β : Type v} {f : α → β} {as : List α} {bs : List β},
  List.mapTR.loop f as bs = bs.reverse ++ List.map f as
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.right.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : SizeOf C] [inst_3 : SizeOf D] (a : D), sizeOf (CategoryTheory.Join.right a) = 1 + sizeOf a
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sub_iUnion : ∀ {α : Type u_2} {ι : Sort u_5} [inst : Sub α] (s : Set α) (t : ι → Set α), s - ⋃ i, t i = ⋃ i, s - t i
-- Mathlib.Data.TypeVec
/-- split off the prefix of an arrow  -/
TypeVec.dropFun : {n : ℕ} → {α : TypeVec.{u_1} (n + 1)} → {β : TypeVec.{u_2} (n + 1)} → α.Arrow β → α.drop.Arrow β.drop
-- Lean.Compiler.IR.Basic
Lean.IR.addParamRename : Lean.IR.IndexRenaming → Lean.IR.Param → Lean.IR.Param → Option Lean.IR.IndexRenaming
-- Mathlib.Tactic.FBinop
/-- Given a type expression, try to remove the last argument(s) and create an `SRec` for the
underlying "functor". Only applies to function applications with a constant head, and,
after dropping all instance arguments, it requires that the remaining last argument be a type.
Returns the `SRec` and the argument.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.extractS : Lean.Expr → Lean.Elab.TermElabM (Option (FBinopElab.SRec × Lean.Expr))
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
LinearIsometryEquiv.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  (iso : E ≃ₗᵢ[𝕜] F), DifferentiableAt 𝕜 (⇑iso) x
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.factors : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : C} [self : CategoryTheory.Projective P] {E X : C}
  (f : P ⟶ X) (e : E ⟶ X) [CategoryTheory.Epi e], ∃ f', CategoryTheory.CategoryStruct.comp f' e = f
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.transvection_inv : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b : F),
  (Matrix.SpecialLinearGroup.transvection hij b)⁻¹ = Matrix.SpecialLinearGroup.transvection hij (-b)
-- Mathlib.Analysis.Calculus.FDeriv.Extend
/-- If a function is differentiable on the left of a point `a : ℝ`, continuous at `a`, and
its derivative also converges at `a`, then `f` is differentiable on the left at `a`.  -/
hasDerivWithinAt_Iic_of_tendsto_deriv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set ℝ} {e : E} {a : ℝ} {f : ℝ → E},
  DifferentiableOn ℝ f s →
    ContinuousWithinAt f s a →
      s ∈ nhdsWithin a (Set.Iio a) →
        Filter.Tendsto (fun x => deriv f x) (nhdsWithin a (Set.Iio a)) (nhds e) → HasDerivWithinAt f e (Set.Iic a) a
-- Lean.Environment
Lean.PersistentEnvExtensionDescr : Type → Type → Type → Type
-- Init.Data.List.Basic
List.mapTR.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (as : List α), List.mapTR f as = List.mapTR.loop f as []
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roc_eq_nil_iff : ∀ {m n : ℕ}, (m<...=n).toList = [] ↔ n ≤ m
-- Std.Time.Time.Unit.Basic
/-- Converts an `Hour.Offset` to a `Minute.Offset`.
 -/
Std.Time.Hour.Offset.toMinutes : Std.Time.Hour.Offset → Std.Time.Minute.Offset
-- Mathlib.Data.Fintype.EquivFin
/-- For efficiency reasons, we want `Finite` instances to have higher
priority than ones coming from `Fintype` instances.  -/
Finite.of_fintype : ∀ (α : Type u_4) [Fintype α], Finite α
-- Mathlib.Order.SupIndep
iSupIndep.supIndep' : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {f : ι → α} (s : Finset ι), iSupIndep f → s.SupIndep f
-- Lean.Data.Options
/-- Whether any option with prefix `trace` is set. This does *not* imply that any of such option is
set to `true` but it does capture the most common case that no such option has ever been touched.
 -/
Lean.Options.hasTrace : Lean.Options → Bool
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.functor_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F : CategoryTheory.MonoidalCategory.DayFunctor C V), { functor := F.functor } = F
-- Mathlib.Data.Finset.Grade
/-- Finsets are multiset-graded. This is not very meaningful mathematically but rather a handy way
to record that the inclusion `Finset α ↪ Multiset α` preserves the covering relation.  -/
Finset.instGradeMinOrder_multiset : {α : Type u_1} → GradeMinOrder (Multiset α) (Finset α)
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
AlgebraicGeometry.instIsReducedFiberOfGeometricallyReduced : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (s : ↥S) [AlgebraicGeometry.GeometricallyReduced f],
  AlgebraicGeometry.IsReduced (AlgebraicGeometry.Scheme.Hom.fiber f s)
-- Aesop.Forward.RuleInfo
Aesop.Slot.mk.injEq : ∀ (typeDiscrTreeKeys? : Option (Array Lean.Meta.DiscrTree.Key)) (index : Aesop.SlotIndex)
  (premiseIndex : Aesop.PremiseIndex) (deps common : Std.HashSet Aesop.PremiseIndex)
  (forwardDeps : Array Aesop.PremiseIndex) (typeDiscrTreeKeys?_1 : Option (Array Lean.Meta.DiscrTree.Key))
  (index_1 : Aesop.SlotIndex) (premiseIndex_1 : Aesop.PremiseIndex) (deps_1 common_1 : Std.HashSet Aesop.PremiseIndex)
  (forwardDeps_1 : Array Aesop.PremiseIndex),
  ({ typeDiscrTreeKeys? := typeDiscrTreeKeys?, index := index, premiseIndex := premiseIndex, deps := deps,
        common := common, forwardDeps := forwardDeps } =
      { typeDiscrTreeKeys? := typeDiscrTreeKeys?_1, index := index_1, premiseIndex := premiseIndex_1, deps := deps_1,
        common := common_1, forwardDeps := forwardDeps_1 }) =
    (typeDiscrTreeKeys? = typeDiscrTreeKeys?_1 ∧
      index = index_1 ∧ premiseIndex = premiseIndex_1 ∧ deps = deps_1 ∧ common = common_1 ∧ forwardDeps = forwardDeps_1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The category of `S`-costructured arrows with target `T : D` (here `S : C ⥤ D`),
has as its objects `D`-morphisms of the form `S Y ⟶ T`, for some `Y : C`,
and morphisms `C`-morphisms `Y ⟶ Y'` making the obvious triangle commute.
 -/
CategoryTheory.CostructuredArrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → D → Type (max u₁ v₂)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.symmetry_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  {g : F.obj a ⟶ Y} (hg : F.relativelyRepresentable g) [inst_2 : F.Full] [F.Faithful],
  CategoryTheory.CategoryStruct.comp (hf'.symmetry hg) (hg.fst' f') = hf'.snd g
-- Mathlib.LinearAlgebra.CrossProduct
/-- The cross product of two vectors in $R^3$ for $R$ a commutative ring.  -/
crossProduct : {R : Type u_1} → [inst : CommRing R] → (Fin 3 → R) →ₗ[R] (Fin 3 → R) →ₗ[R] Fin 3 → R
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.fderivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} (p : Polynomial 𝕜),
  UniqueDiffWithinAt 𝕜 s x →
    fderivWithin 𝕜 (fun x => Polynomial.eval x p) s x =
      ContinuousLinearMap.smulRight 1 (Polynomial.eval x (Polynomial.derivative p))
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList_two : Nat.primeFactorsList 2 = [2]
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- The map from the GNS space to the C⋆-algebra, as a linear equivalence.  -/
PositiveLinearMap.ofPreGNS : {A : Type u_1} → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → (f : A →ₚ[ℂ] ℂ) → f.PreGNS ≃ₗ[ℂ] A
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.int_add : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (m : ℤ), LiouvilleWith p (↑m + x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_maxKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.getKey? t.maxKey! = some t.maxKey!
-- Lean.Meta.Tactic.Grind.Arith.CommRing.MonadRing
Lean.Meta.Grind.Arith.CommRing.MonadRing.mk : {m : Type → Type} →
  m Lean.Meta.Grind.Arith.CommRing.Ring →
    ((Lean.Meta.Grind.Arith.CommRing.Ring → Lean.Meta.Grind.Arith.CommRing.Ring) → m Unit) →
      Lean.Meta.Grind.Arith.CommRing.MonadRing m
-- Mathlib.Order.Lattice
Pi.instSemilatticeSup.eq_1 : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → SemilatticeSup (α' i)],
  Pi.instSemilatticeSup =
    { toPartialOrder := Pi.partialOrder, sup := fun x y i => x i ⊔ y i, le_sup_left := ⋯, le_sup_right := ⋯,
      sup_le := ⋯ }
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.gmonoid : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → GradedMonoid.GMonoid fun i => TensorPower R i M
-- Mathlib.Topology.Algebra.InfiniteSum.Real
Real.tsum_le_of_sum_le : ∀ {ι : Type u_3} {f : ι → ℝ} {c : ℝ}, 0 ≤ f → (∀ (u : Finset ι), ∑ x ∈ u, f x ≤ c) → ∑' (x : ι), f x ≤ c
-- Init.Data.BitVec.Bitblast
BitVec.negOverflow_eq : ∀ {w : ℕ} (x : BitVec w), x.negOverflow = (decide (0 < w) && x == BitVec.intMin w)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.hom_inv_apply : ∀ {R S : RingCat} (e : R ≅ S) (s : ↑S),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.NumberTheory.Niven
IsIntegral.exists_int_iff_exists_rat : ∀ {α : Type u_1} [inst : DivisionRing α] [CharZero α] {x : α}, IsIntegral ℤ x → ((∃ q, x = ↑q) ↔ ∃ k, x = ↑k)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.copy_eq : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α) (s : Set α) (hs : s = ↑L), L.copy s hs = L
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkAuxDeclFor : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadQuotation m] → Lean.Syntax → (Lean.Syntax → m Lean.Elab.Term.Do.Code) → m Lean.Elab.Term.Do.Code
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.coeff_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ) (s : σ),
  (MvPowerSeries.coeff n) (MvPowerSeries.X s) = if n = fun₀ | s => 1 then 1 else 0
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.step_done : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {upper : α},
  { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper }.step = Std.IterStep.done
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_le : ∀ {m n : ℕ∞}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Format a `RefinedDiscrTree.Key`.  -/
Lean.Meta.RefinedDiscrTree.Key.format : Lean.Meta.RefinedDiscrTree.Key → Std.Format