mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_dvd_factorial : ∀ {m n : ℕ}, m ≤ n → m.factorial ∣ n.factorial
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. The number of trees in the forest.  -/
Batteries.BinomialHeap.Imp.Heap.length : {α : Type u_1} → Batteries.BinomialHeap.Imp.Heap α → ℕ
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.MatchResult.mk.inj : ∀ {α : Type} {elts elts_1 : Array (Array (Array α))}, { elts := elts } = { elts := elts_1 } → elts = elts_1
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.head_transpose : ∀ {α : Type u} {n : ℕ} {m' : Type uₘ} (A : Matrix m' (Fin n.succ) α),
  Matrix.vecHead (Matrix.of.symm A.transpose) = Matrix.vecHead ∘ Matrix.of.symm A
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- The space of coordinates for affine combinations indexed by a general type.  -/
finsuppAffineCoords : (ι : Type u_1) → (k : Type u_2) → [inst : Ring k] → AffineSubspace k (ι →₀ k)
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.embSigma.eq_1 : ∀ (n : ℕ) (c : OrderedFinpartition n),
  OrderedFinpartition.embSigma n c = ⟨⟨c.length, ⋯⟩, ⟨fun m => ⟨c.partSize m, ⋯⟩, fun j => c.emb j⟩⟩
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHAddOffset_5 : HAdd Std.Time.Timestamp Std.Time.Millisecond.Offset Std.Time.Timestamp
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.image_eq : ∀ {𝕜 : 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),
  ↑I '' s = ↑I.symm ⁻¹' s ∩ Set.range ↑I
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instHasFiniteColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.HasWeakSheafify J D]
  [CategoryTheory.Limits.HasFiniteColimits D], CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Sheaf J D)
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.NatTrans.toCatHom₂_comp : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  {F G H : CategoryTheory.Functor C D} (η₁ : F ⟶ G) (η₂ : G ⟶ H),
  CategoryTheory.NatTrans.toCatHom₂ (CategoryTheory.CategoryStruct.comp η₁ η₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.toCatHom₂ η₁) (CategoryTheory.NatTrans.toCatHom₂ η₂)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_eq_getMsb?_getD : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getMsbD i = (x.getMsb? i).getD false
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.model_distinctConstantsTheory : ∀ (L : FirstOrder.Language) {α : Type u'} {M : Type w} [inst : (L.withConstants α).Structure M] (s : Set α),
  M ⊨ L.distinctConstantsTheory s ↔ Set.InjOn (fun i => ↑(L.con i)) s
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.zero_rpow : ∀ {x : ℝ}, x ≠ 0 → 0 ^ x = 0
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The **first isomorphism theorem** for commutative algebras (`AlgHom.range` version).  -/
Ideal.quotientKerEquivRange : {R : Type u_5} →
  {A : Type u_6} →
    {B : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] → [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → (A ⧸ RingHom.ker f) ≃ₐ[R] ↥f.range
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂)
  (fg : CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) fg) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv
        (CategoryTheory.MonoidalCategoryStruct.tensorHom fg (CategoryTheory.CategoryStruct.id Z₂)))
-- Std.Time.Format.Modifier
Std.Time.Fraction.truncated.sizeOf_spec : ∀ (digits : ℕ), sizeOf (Std.Time.Fraction.truncated digits) = 1 + sizeOf digits
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
/-- The derivative (in the analysis sense) of a polynomial `p` is given by `p.derivative`.  -/
Polynomial.hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (p : Polynomial 𝕜) (x : 𝕜),
  HasDerivAt (fun x => Polynomial.eval x p) (Polynomial.eval x (Polynomial.derivative p)) x
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_refl_apply : ∀ {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] (x : TensorProduct R M N),
  (LinearEquiv.lTensor M (LinearEquiv.refl R N)) x = x
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.ε_η_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (X : C)
  [inst_3 : F.Monoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.ε F).app X)
      ((CategoryTheory.Functor.OplaxMonoidal.η F).app X) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor C C)).obj X)
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv.congr_simp : ∀ (R : Type u_1) (p p_1 : ℕ) (e_p : p = p_1) (n n_1 : ℕ),
  n = n_1 →
    ∀ [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
      iterateFrobeniusEquiv R p n = iterateFrobeniusEquiv R p_1 n_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd c = Lean.Meta.Grind.Arith.Cutsat.UnsatProof.dvd c_1 → c = c_1
-- Mathlib.Algebra.PresentedMonoid.Basic
/-- Given a set of relations, `rels`, over a type `α`, `PresentedAddMonoid` constructs
the monoid with generators `x : α` and relations `rels` as a quotient of an AddCon structure over
rels  -/
PresentedAddMonoid : {α : Type u_1} → (FreeAddMonoid α → FreeAddMonoid α → Prop) → Type u_1
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupport.mk.inj : ∀ {codeActionKind codeActionKind_1 : Lean.Lsp.CodeActionLiteralSupportValueSet},
  { codeActionKind := codeActionKind } = { codeActionKind := codeActionKind_1 } → codeActionKind = codeActionKind_1
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Coalgebra.forget_additive : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive], (CategoryTheory.Endofunctor.Coalgebra.forget F).Additive
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.instCoeTypeForall_std : {α : Type u} → Coe (Type v) (α → Type v)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_split : Int.Internal.Linear.Context → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → ℕ → Prop
-- Mathlib.Topology.Algebra.ConstMulAction
properlyDiscontinuousVAdd_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α],
  ProperlyDiscontinuousVAdd M α ↔ ∀ {K L : Set α}, IsCompact K → IsCompact L → {m | ((m +ᵥ K) ∩ L).Nonempty}.Finite
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- A bicategory structure on the oplax functors between bicategories, with lax transformations.  -/
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    (C : Type u₂) → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.Bicategory (CategoryTheory.OplaxFunctor B C)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.hasPullback_of_left_factors_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (i : Z ⟶ W) [CategoryTheory.Mono i],
  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) i
-- Mathlib.Analysis.CStarAlgebra.Projection
IsStarProjection.le_iff_mul_eq_left : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {p q : A},
  IsStarProjection p → IsStarProjection q → (p ≤ q ↔ p * q = p)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.pairwise_div_notMem_range' : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S] [inst_2 : InvolutiveInv ι]
  [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G),
  (∀ (i : ι), v i⁻¹ = (v i)⁻¹) →
    ∀ (f : G →* S),
      (∀ (i : ι), f (v i) ≠ 1) →
        ∀ s ⊆ {j | IsMulIndecomposable v {i | 1 < f (v i)} j}, s.Pairwise fun i j => v i / v j ∉ Set.range v
-- Mathlib.Data.Fin.Tuple.Sort
Tuple.lt_card_gt_iff_apply_gt_of_antitone : ∀ {n : ℕ} {α : Type u_1} {j : Fin n} {f : Fin n → α} [inst : Preorder α] {a : α} [inst_1 : DecidableLT α],
  Antitone f → (↑j < {i | a < f i}.card ↔ a < f j)
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_ofFn : ∀ {α : Type u_1} {β : Type u_2} {as : List α} {f : (i : ℕ) → α → i < as.length → β},
  as.mapFinIdx f = List.ofFn fun i => f (↑i) as[i] ⋯
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for shift left on `BitVec`.  -/
BitVec.reduceShiftLeft : Lean.Meta.Simp.DSimproc
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Server.RequestM.findCmdParsedSnap.go : Lean.Server.FileWorker.EditableDocument →
  String.Pos.Raw →
    Lean.Language.Lean.CommandParsedSnapshot → Lean.Server.ServerTask (Option Lean.Language.Lean.CommandParsedSnapshot)
-- Mathlib.Topology.List
List.tendsto_cons : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {l : List α},
  Filter.Tendsto (fun p => p.1 :: p.2) (nhds a ×ˢ nhds l) (nhds (a :: l))
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.homologyIso_inv_comp_homologyι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.RightHomologyData) {Z : C} (h_1 : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.homologyIso.inv (CategoryTheory.CategoryStruct.comp S.homologyι h_1) =
    CategoryTheory.CategoryStruct.comp h.ι (CategoryTheory.CategoryStruct.comp h.opcyclesIso.inv h_1)
-- Lean.Meta.Basic
/-- `whnf` with default transparency. -/
Lean.Meta.whnfD : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_g : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ) (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃'
        hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).g =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r hr pq' i₀ i₁ i₂ i₃ hi₀ hi₁ hi₂ hi₃ n₀ n₁
          n₂ hn₁' ⋯ ⋯).hom
      (X.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
-- Init.Data.Vector.Count
Vector.count_eq_zero : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α} {xs : Vector α n}, Vector.count a xs = 0 ↔ a ∉ xs
-- Mathlib.Order.Concept
Concept.isCompl_extent_intent : ∀ {α : Type u_2} {r' : α → α → Prop} [IsStrictTotalOrder α r'] (c' : Concept α α r'), IsCompl c'.extent c'.intent
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.support_ofCoeff`. -/
SkewMonoidAlgebra.support_ofFinsupp : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (p : G →₀ k), { coeff := p }.support = p.support
-- Std.Http.Protocol.H1.Writer
/-- Checks if the writer can accept more data from the user.
 -/
Std.Http.Protocol.H1.Writer.canAcceptData : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Bool
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_zero_pnat_eq_tprod_nat : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {f : ℕ → G},
  Multipliable f → f 0 * ∏' (n : ℕ+), f ↑n = ∏' (n : ℕ), f n
-- Mathlib.Order.BooleanAlgebra.Basic
eq_compl_iff_isCompl : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x = yᶜ ↔ IsCompl x y
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instOrderBot : {α : Type u_2} → {β : Type u_3} → [inst : SupSet α] → {x : CompleteLattice β} → OrderBot (sSupHom α β)
-- Mathlib.LinearAlgebra.Basis.Submodule
/-- An element of a non-unital-non-associative algebra is in the center exactly when it commutes
with the basis elements.  -/
Module.Basis.mem_center_iff : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_7} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [SMulCommClass R A A] [SMulCommClass R R A] [IsScalarTower R A A] (b : Module.Basis ι R A)
  {z : A},
  z ∈ Set.center A ↔
    (∀ (i : ι), Commute (b i) z) ∧ ∀ (i j : ι), z * (b i * b j) = z * b i * b j ∧ b i * b j * z = b i * (b j * z)
-- Std.Tactic.BVDecide.LRAT.Internal.Convert
Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT'.eq_1 : ∀ {n : ℕ} (clauses : Std.Sat.CNF (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.CNF.convertLRAT' clauses =
    Array.map Std.Tactic.BVDecide.LRAT.Internal.CNF.Clause.convertLRAT' clauses.clauses
-- Mathlib.Data.Finset.Sups
Finset.infs_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] {s t : Finset α}, s ⊼ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_nonpos : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  (∀ x ∈ spectrum R a, f x ≤ 0) → cfc f a ≤ 0
-- Mathlib.Algebra.Order.SuccPred
Order.one_le_iff_ne_zero : ∀ {α : Type u_1} {x : α} [inst : PartialOrder α] [inst_1 : AddMonoidWithOne α] [NeZero 1] [SuccAddOrder α]
  [IsBotZeroClass α], 1 ≤ x ↔ x ≠ 0
-- Mathlib.Algebra.Group.Prod
MonoidHom.fst.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.fst M N = { toFun := Prod.fst, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso_hom_left_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (X_1 : SimplexCategoryᵒᵖ), X.rightOpLeftOpIso.hom.left.app X_1 = CategoryTheory.CategoryStruct.id (X.left.obj X_1)
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.uliftFunctor_map : ∀ (R : Type u) [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y),
  (ModuleCat.uliftFunctor.{v', v, u} R).map f =
    ModuleCat.ofHom (↑ULift.moduleEquiv.symm ∘ₗ ModuleCat.Hom.hom f ∘ₗ ↑ULift.moduleEquiv)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  [inst_1 : SizeOf C] (homEquiv : {Y : C} → (X ⟶ Y) ≃ F.obj Y)
  (homEquiv_comp :
    autoParam
      (∀ {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
        homEquiv (CategoryTheory.CategoryStruct.comp f g) =
          (CategoryTheory.ConcreteCategory.hom (F.map g)) (homEquiv f))
      CategoryTheory.Functor.CorepresentableBy.homEquiv_comp._autoParam),
  sizeOf { homEquiv := homEquiv, homEquiv_comp := homEquiv_comp } = 1
-- Mathlib.Geometry.Euclidean.Volume.Measure
AffineSubspace.euclideanHausdorffMeasure_coe_image : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : MeasurableSpace P] [inst_4 : BorelSpace P] [inst_5 : NormedAddTorsor V P] (d : ℕ) (s : AffineSubspace ℝ P)
  (t : Set ↥s),
  (MeasureTheory.Measure.euclideanHausdorffMeasure d) (Subtype.val '' t) =
    (MeasureTheory.Measure.euclideanHausdorffMeasure d) t
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.denoteSInt : {α : Type u_1} → [Lean.Grind.Semiring α] → ℤ → α
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsAlt.isRefl : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B₁ : LinearMap.BilinForm R₁ M₁}, B₁.IsAlt → B₁.IsRefl
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∩ t₂).get? k = none
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribMulAction.toDistribSMul : {M : Type u_1} → {A : Type u_7} → [inst : Monoid M] → [inst_1 : AddMonoid A] → [DistribMulAction M A] → DistribSMul M A
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pushoutDesc_inl_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange] {S S' X Y : C} (f : S ⟶ S') {v₁₂ : S ⟶ X} {v₂₂ : S ⟶ Y} {g : Y ⟶ X}
  (hv₁₂ : v₁₂ = CategoryTheory.CategoryStruct.comp v₂₂ g) [inst_2 : CategoryTheory.Limits.HasPushout v₁₂ f]
  [inst_3 : CategoryTheory.Limits.HasPushout v₂₂ f],
  P g →
    P
      (CategoryTheory.Limits.pushout.desc
        (CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.pushout.inl v₁₂ f))
        (CategoryTheory.Limits.pushout.inr v₁₂ f) ⋯)
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.Integrable.withDensityᵥ_eq_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f g : α → E},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → (μ.withDensityᵥ f = μ.withDensityᵥ g ↔ f =ᵐ[μ] g)
-- Mathlib.Data.List.Basic
List.reverse_concat' : ∀ {α : Type u} (l : List α) (a : α), (l ++ [a]).reverse = a :: l.reverse
-- Mathlib.CategoryTheory.Limits.FullSubcategory
CategoryTheory.Limits.hasLimitsOfShape_of_closedUnderLimits : ∀ (J : Type w) [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (P : CategoryTheory.ObjectProperty C) [P.IsClosedUnderLimitsOfShape J] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.HasLimitsOfShape J P.FullSubcategory
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eq_loopyOn_iff_eRank : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M = Matroid.loopyOn X ↔ M.eRank = 0 ∧ M.E = X
-- Mathlib.Data.ZMod.QuotientGroup
finite_zpowers : ∀ {α : Type u_3} [inst : Group α] {a : α}, (↑(Subgroup.zpowers a)).Finite ↔ IsOfFinOrder a
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.isUniformInducing_extend : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  {f : α → β} [CompleteSpace β], IsUniformInducing f → IsUniformInducing (pkg.extend f)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.swap_mul_of_ne : ∀ {R : Type u_1} {n : Type u_2} {m : Type u_3} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  {i j a : n} {b : m}, a ≠ i → a ≠ j → ∀ (g : Matrix n m R), (Matrix.swap R i j * g) a b = g a b
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.ofRestrict_hom_c_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U : TopCat} (X : AlgebraicGeometry.SheafedSpace C)
  {f : U ⟶ ↑X.toPresheafedSpace} (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (V : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ),
  (X.ofRestrict h).hom.c.app V = X.presheaf.map (⋯.adjunction.counit.app (Opposite.unop V)).op
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of the forward direction of `AddMonoidAlgebra.coeff_inj`. -/
AddMonoidAlgebra.ext : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x y : AddMonoidAlgebra R M}, x.coeff = y.coeff → x = y
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- This is the key computation for the proof of
`Scheme.Modules.isQuasicoherent_iff_isIso_fromTildeΓ`.
 [Lemme 1.4.1.1][grothendieck-1971]  -/
_private.Mathlib.AlgebraicGeometry.Modules.Tilde.0.AlgebraicGeometry.QuasicoherentTilde.Aux.of_eq_iSup_basicOpen : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} (V : (AlgebraicGeometry.Spec R).Opens) {ι : Type u_1}
  [Finite ι] (g : ι → ↑R),
  V = ⨆ i, PrimeSpectrum.basicOpen (g i) →
    (∀ (i : ι), AlgebraicGeometry.QuasicoherentTilde.Aux✝ M (PrimeSpectrum.basicOpen (g i))) →
      AlgebraicGeometry.QuasicoherentTilde.Aux✝ M V
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.instInhabited : {B : Type u₁} →
  [inst : Quiver B] → [inst_1 : (a b : B) → Quiver (a ⟶ b)] → Inhabited (CategoryTheory.PrelaxFunctorStruct B B)
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.map_shrinkYonedaEquiv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C}
  {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : CategoryTheory.shrinkYoneda.{w, v, u}.obj X ⟶ P) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (P.map g.op)) (CategoryTheory.shrinkYonedaEquiv f) =
    (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op Y))) (CategoryTheory.shrinkYonedaObjObjEquiv.symm g)
-- Lean.Data.Lsp.Internal
/-- The declaration `«from»` is renamed to `to`.  -/
Lean.Lsp.OpenNamespace.renamed : Lean.Name → Lean.Name → Lean.Lsp.OpenNamespace
-- Mathlib.Algebra.LinearRecurrence
/-- `E.tupleSucc` maps `![s₀, s₁, ..., sₙ]` to `![s₁, ..., sₙ, ∑ (E.coeffs i) * sᵢ]`,
where `n := E.order`.  -/
LinearRecurrence.tupleSucc : {R : Type u_1} → [inst : CommSemiring R] → (E : LinearRecurrence R) → (Fin E.order → R) →ₗ[R] Fin E.order → R
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.tendsto_normThreshold_atTop : ∀ {a : ℝ}, 0 < a → Filter.Tendsto (ProbabilityTheory.Fernique.normThreshold a) Filter.atTop Filter.atTop
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.iff_adjoin_image_compl : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (s : Set ι),
  AlgebraicIndependent R x ↔
    (AlgebraicIndependent R fun i => x ↑i) ∧ AlgebraicIndepOn (↥(Algebra.adjoin R (x '' sᶜ))) x s
-- Lean.Elab.App
Lean.Elab.Term.LValResolution.projFn.injEq : ∀ (baseStructName structName fieldName : Lean.Name) (levels : List Lean.Level)
  (baseStructName_1 structName_1 fieldName_1 : Lean.Name) (levels_1 : List Lean.Level),
  (Lean.Elab.Term.LValResolution.projFn baseStructName structName fieldName levels =
      Lean.Elab.Term.LValResolution.projFn baseStructName_1 structName_1 fieldName_1 levels_1) =
    (baseStructName = baseStructName_1 ∧ structName = structName_1 ∧ fieldName = fieldName_1 ∧ levels = levels_1)