mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_filter_le : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] (a b c : α),
  {x ∈ Finset.Ico a b | c ≤ x} = Finset.Ico (max a c) b
-- Mathlib.Data.Int.SuccPred
Int.instIsSuccArchimedean : IsSuccArchimedean ℤ
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_conj : ∀ {α : Type u_1} {f g : Equiv.Perm α} (h : Equiv.Perm α), (h * f * h⁻¹).Disjoint (h * g * h⁻¹) ↔ f.Disjoint g
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
/-- Also see `AlgebraicGeometry.Scheme.IdealSheafData.map_ideal`  -/
AlgebraicGeometry.Scheme.IdealSheafData.map_ideal_basicOpen : ∀ {X : AlgebraicGeometry.Scheme} (self : X.IdealSheafData) (U : ↑X.affineOpens)
  (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (self.ideal U) =
    self.ideal (X.affineBasicOpen f)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_int_add : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] [inst_1 : AddCommGroupWithOne G]
  [inst_2 : AddGroupWithOne H] [AddConstMapClass F G H 1 1] (f : F) (n : ℤ) (x : G), f (↑n + x) = f x + ↑n
-- Mathlib.Order.RelClasses
/-- Creates data, given a way to generate a value from all that compare as greater.
See also `WellFoundedGT.fix_eq`.  -/
WellFoundedGT.fix : {α : Type u} →
  [inst : LT α] →
    [WellFoundedGT α] →
      {motive : α → Sort u_1} → ((x : α) → ((y : α) → x < y → motive y) → motive x) → (x : α) → motive x
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) {n : ℕ} (a : { l // l.length = n }),
  List.MergeSort.Internal.mergeSortTR₂.run✝ le a =
    match n, a with
    | 0, ⟨[], property⟩ => []
    | 1, ⟨[a], property⟩ => [a]
    | n.succ.succ, xs =>
      match List.MergeSort.Internal.splitRevInTwo xs with
      | (l, r) =>
        List.MergeSort.Internal.mergeTR (List.MergeSort.Internal.mergeSortTR₂.run'✝ le l)
          (List.MergeSort.Internal.mergeSortTR₂.run✝ le r) le
-- Mathlib.Data.List.Sym
List.first_mem_of_cons_mem_sym : ∀ {α : Type u_1} {xs : List α} {n : ℕ} {a : α} {z : Sym α n}, a ::ₛ z ∈ List.sym (n + 1) xs → a ∈ xs
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Raw.isEmpty.eq_1 : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Raw α β), m.isEmpty = (m.size == 0)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.const_beq_const_add_beq : ∀ {w c b : ℕ} {a : BitVec w}, (BitVec.ofNat w c == BitVec.ofNat w b + a) = (a == BitVec.ofNat w c - BitVec.ofNat w b)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) (hf : Function.HasFiniteMulSupport f),
  ∏ᶠ (i : α), f i = ∏ i ∈ Set.Finite.toFinset hf, f i
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l →
              Std.DHashMap.Internal.Raw₀.Const.get? (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)) k' = some v
-- Lean.Parser.Command
Lean.Parser.Command.optDeriving.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Module.Presentation.Basic
/-- When `M` admits a presentation by generators and relations given
by `solution : relations.Solutions M`, this is the associated linear equivalence
`relations.Quotient ≃ₗ[A] M`.  -/
Module.Relations.Solution.IsPresentation.linearEquiv : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            {solution : relations.Solution M} → solution.IsPresentation → relations.Quotient ≃ₗ[A] M
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.isIndex_zero : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d), SSet.prodStdSimplex.pairingCore.IsIndex x hd 0 ↔ False
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.mk'.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] (c : AddCon M),
  c.mk' = { toFun := c.mkAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The left homology functor `ShortComplex C ⥤ C`, where the left homology of a
short complex `S` is understood as a cokernel of the obvious map `S.toCycles : S.X₁ ⟶ S.cycles`
where `S.cycles` is a kernel of `S.g : S.X₂ ⟶ S.X₃`.  -/
CategoryTheory.ShortComplex.leftHomologyFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasKernels C] →
        [CategoryTheory.Limits.HasCokernels C] → CategoryTheory.Functor (CategoryTheory.ShortComplex C) C
-- Mathlib.Data.Finite.Defs
/-- Projection of `Set.Finite` to its `Finite` instance.
This is intended to be used with dot notation.
See also `Set.Finite.Fintype` and `Set.Finite.nonempty_fintype`.  -/
Set.Finite.to_subtype : ∀ {α : Type u} {s : Set α}, s.Finite → Finite ↑s
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.div_coe_eq_zero : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I : Ideal A} (H : g.IsWeierstrassDivisorAt I)
  [inst_1 : IsAdicComplete I A] {r : Polynomial A},
  r.degree < ↑((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat → H.div ↑r = 0
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The measurable equivalence `(∀ i : s, π i) × (∀ i : t, π i) ≃ᵐ (∀ i : s ∪ t, π i)`
for disjoint finsets `s` and `t`. `Equiv.piFinsetUnion` as a measurable equivalence.  -/
MeasurableEquiv.piFinsetUnion : {δ' : Type u_5} →
  (π : δ' → Type u_6) →
    [inst : (x : δ') → MeasurableSpace (π x)] →
      [inst_1 : DecidableEq δ'] →
        {s t : Finset δ'} → Disjoint s t → ((i : ↥s) → π ↑i) × ((i : ↥t) → π ↑i) ≃ᵐ ((i : ↥(s ∪ t)) → π ↑i)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.collectStats : {α : Type u_1} →
  {β : Type u_2} → Lean.PersistentHashMap.Node α β → Lean.PersistentHashMap.Stats → ℕ → Lean.PersistentHashMap.Stats
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getLetIdDeclVars : Lean.Syntax → Array Lean.Elab.Term.Do.Var
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.mk0_one : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] (h : optParam (1 ≠ 0) ⋯), Units.mk0 1 h = 1
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_singleton : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (x : P), intrinsicClosure 𝕜 {x} = {x}
-- Mathlib.Data.Set.Finite.Basic
Set.finite_range_iff : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Injective f → ((Set.range f).Finite ↔ Finite α)
-- Mathlib.CategoryTheory.GlueData
/-- For each `i j : J`, a transition map `t i j : V i j ⟶ V j i`  -/
CategoryTheory.GlueData.t : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (self : CategoryTheory.GlueData C) → (i j : self.J) → self.V (i, j) ⟶ self.V (j, i)
-- Mathlib.Algebra.Squarefree.Basic
not_squarefree_zero : ∀ {R : Type u_1} [inst : MonoidWithZero R] [Nontrivial R], ¬Squarefree 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.instMulActionElemFinset : (G : Type u_1) →
  [inst : Group G] → {α : Type u_2} → [MulAction G α] → {n : ℕ} → [DecidableEq α] → MulAction G ↑(Set.powersetCard α n)
-- Mathlib.Analysis.InnerProductSpace.StarOrder
/-- Because this takes `ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint` as an argument,
and for the moment we only have this for `𝕜 := ℂ`, this is not registered as an instance.  -/
ContinuousLinearMap.instStarOrderedRingRCLike : ∀ {𝕜 : Type u_1} {H : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] [inst_4 : Algebra ℝ (H →L[𝕜] H)] [IsScalarTower ℝ 𝕜 (H →L[𝕜] H)]
  [ContinuousFunctionalCalculus ℝ (H →L[𝕜] H) IsSelfAdjoint], StarOrderedRing (H →L[𝕜] H)
-- Mathlib.Order.Grade
Flag.instGradeOrderSubtypeMem : {𝕆 : Type u_1} →
  {α : Type u_3} → [inst : PartialOrder α] → [inst_1 : Preorder 𝕆] → [GradeOrder 𝕆 α] → (s : Flag α) → GradeOrder 𝕆 ↥s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_eq_some_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} (h : a ∈ m),
  Std.ExtDHashMap.Const.get? m a = some (Std.ExtDHashMap.Const.get m a h)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unitInv_app_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (Y : D), e.unitInv.app (e.inverse.obj Y) = e.inverse.map (e.counit.app Y)
-- Lean.Meta.CongrTheorems
Lean.Meta.congrSimpSuffix : String
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addCommMagma : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddCommMagma (f i)] → AddCommMagma ((i : I) → f i)
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOnFilter.congr_inseparable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α} {F' : ι → α → β},
  TendstoUniformlyOnFilter F f p p' →
    (∀ᶠ (n : ι × α) in p ×ˢ p', Inseparable (F n.1 n.2) (F' n.1 n.2)) → TendstoUniformlyOnFilter F' f p p'
-- Lean.Syntax
Lean.Syntax.Range.bsize : Lean.Syntax.Range → ℕ
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_closure_of_mem : ∀ {K : Type u} [inst : DivisionRing K] {s : Set K} {x : K}, x ∈ s → x ∈ Subfield.closure s
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_def : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_5} [inst_1 : AddCommMonoid S] (p : SkewPolynomial R) (f : ℕ → R → S),
  p.sum f = ∑ n ∈ p.support, f n (p.coeff n)
-- Init.Data.Random
StdGen.s2 : StdGen → ℕ
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionObj : ∀ (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ᵒᵖ) (d : Dᵒᵖ),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj (Opposite.unop c) (Opposite.unop d))
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.associator_inv_left_fst_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (R S T : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.associator R S T).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom S.hom) S.hom) T.hom)
        (CategoryTheory.ChosenPullbacksAlong.fst R.hom S.hom)) =
    CategoryTheory.ChosenPullbacksAlong.fst R.hom (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).hom
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for directional derivatives.

Version for scalar multiplication.  -/
SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left : ∀ {𝕜 : Type u_2} {D : Type u_4} {F : Type u_8} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup D] [inst_3 : NormedSpace ℝ D] [inst_4 : MeasurableSpace D] {μ : MeasureTheory.Measure D}
  [BorelSpace D] [FiniteDimensional ℝ D] [μ.IsAddHaarMeasure] [inst_8 : RCLike 𝕜] [inst_9 : NormedSpace 𝕜 F]
  (f : SchwartzMap D 𝕜) (g : SchwartzMap D F) (v : D),
  ∫ (x : D), f x • (LineDeriv.lineDerivOp v g) x ∂μ = -∫ (x : D), (LineDeriv.lineDerivOp v f) x • g x ∂μ
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.finite : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M}, Module.DualBases e ε → ∀ (m : M), {i | (ε i) m ≠ 0}.Finite
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
continuousAt_cpow_const : ∀ {a b : ℂ}, a ∈ Complex.slitPlane → ContinuousAt (fun x => x ^ b) a
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.mapPullbackAdj_unit_app : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} [inst_2 : P.IsStableUnderComposition] [inst_3 : Q.IsStableUnderBaseChange]
  (f : X ⟶ Y) [inst_4 : P.HasPullbacksAlong f] [inst_5 : P.IsStableUnderBaseChangeAlong f]
  [inst_6 : Q.HasOfPostcompProperty Q] (hPf : P f) (hQf : Q f) (A : P.Over Q X),
  (CategoryTheory.MorphismProperty.Over.mapPullbackAdj P Q f hPf hQf).unit.app A =
    CategoryTheory.MorphismProperty.Over.homMk
      (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id A.left) A.hom ⋯) ⋯ ⋯
-- Mathlib.RingTheory.PowerSeries.Schroder
PowerSeries.coeff_X_mul_largeSchroderSeriesSeries_sq : ∀ (n : ℕ),
  0 < n →
    (PowerSeries.coeff n) (PowerSeries.X * PowerSeries.largeSchroderSeries ^ 2) =
      ∑ i ∈ Finset.range n, i.largeSchroder * (n - 1 - i).largeSchroder
-- Init.Data.BitVec.Bitblast
BitVec.resRec.congr_simp : ∀ {w : ℕ} (x x_1 : BitVec w),
  x = x_1 →
    ∀ (y y_1 : BitVec w),
      y = y_1 → ∀ (s s_1 : ℕ) (e_s : s = s_1) (hs : s < w) (hslt : 0 < s), x.resRec y s hs hslt = x_1.resRec y_1 s_1 ⋯ ⋯
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `IntModule` instance  -/
Lean.Meta.Grind.Arith.Linear.Struct.intModuleInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- structure morphism of the coalgebra  -/
CategoryTheory.Endofunctor.Coalgebra.str : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → (self : CategoryTheory.Endofunctor.Coalgebra F) → self.V ⟶ F.obj self.V
-- Mathlib.Topology.Sheaves.Sheaf
TopCat.Sheaf.forget_full : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (X : TopCat), (TopCat.Sheaf.forget C X).Full
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_eq_of_norm_add_lt_right : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z1 z2 : ℚ_[p]}, ‖z1 + z2‖ < ‖z2‖ → ‖z1‖ = ‖z2‖
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
/-- The **spectral mapping theorem** for the continuous functional calculus.  -/
cfc_map_spectrum : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  autoParam (p a) cfc_map_spectrum._auto_1 →
    autoParam (ContinuousOn f (spectrum R a)) cfc_map_spectrum._auto_3 → spectrum R (cfc f a) = f '' spectrum R a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_maxKey?_of_isSome_maxKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).maxKey?.isSome = true → t.maxKey?.isSome = true
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingFaceMapComplex.objD.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  AlgebraicTopology.AlternatingFaceMapComplex.objD X n = ∑ i, (-1) ^ ↑i • X.δ i
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.derivFamily_zero : ∀ {ι : Type u_1} (f : ι → Ordinal.{u_2} → Ordinal.{u_2}), Ordinal.derivFamily f 0 = Ordinal.nfpFamily f 0
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.toLinearMap_symm_rid : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(TensorProduct.rid R M).symm = (TensorProduct.mk R M R).flip 1
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_tensorMap_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {F G H K : CategoryTheory.Functor C C} {α : F ⟶ G} {β : H ⟶ K}
  (X : C),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom α β).app X =
    CategoryTheory.CategoryStruct.comp (β.app (F.obj X)) (K.map (α.app X))
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
CochainComplex.homologyMap_homologyδOfTriangle_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)),
  DerivedCategory.Q.mapTriangle.obj T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ (n₀ n₁ : ℤ) (h : autoParam (n₀ + 1 = n₁) CochainComplex.homologyMap_homologyδOfTriangle._auto_1) {Z : C}
      (h_1 : HomologicalComplex.homology T.obj₁ n₁ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap T.mor₂ n₀)
          (CategoryTheory.CategoryStruct.comp (CochainComplex.homologyδOfTriangle T n₀ n₁ h) h_1) =
        CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRk_le_of_subset : ∀ {α : Type u} {X Y : Set α} (M : Matroid α), X ⊆ Y → M.cRk X ≤ M.cRk Y
-- Mathlib.Tactic.Translate.Core
/-- A version of `insertTranslation` that checks whether the translation is valid, and only
inserts the translation if it is valid.  -/
Mathlib.Tactic.Translate.insertTranslationChecked : Mathlib.Tactic.Translate.TranslateData → Lean.Name → Lean.Name → Mathlib.Tactic.Translate.Config → Lean.CoreM Unit
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_surjective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → Function.Surjective (AddSubmonoid.map f)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_minKey?_iff_ne_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.minKey?.isSome = true ↔ ¬t = ∅
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- A submodule closed under multiplication is a non-unital subalgebra.  -/
Submodule.toNonUnitalSubalgebra : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → (p : Submodule R A) → (∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p) → NonUnitalSubalgebra R A
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_ne_top_iff : ∀ {x : EReal}, x.toENNReal ≠ ⊤ ↔ x ≠ ⊤
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.re_intCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (z : ℤ), (↑z).re = ↑z
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot_mem_affineSpan_faceOpposite : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.altitudeFoot i ∈ affineSpan ℝ (Set.range (s.faceOpposite i).points)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
_private.Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer.0.CategoryTheory.Limits.MultispanIndex.multispanMapIso.match_1.splitter : {J : CategoryTheory.Limits.MultispanShape} →
  (motive : CategoryTheory.Limits.WalkingMultispan J → Sort u_3) →
    (i : CategoryTheory.Limits.WalkingMultispan J) →
      ((a : J.L) → motive (CategoryTheory.Limits.WalkingMultispan.left a)) →
        ((a : J.R) → motive (CategoryTheory.Limits.WalkingMultispan.right a)) → motive i
-- Mathlib.Algebra.Regular.Basic
/-- If multiplying by `1` on either side is the identity, `1` is regular.  -/
isRegular_one : ∀ {R : Type u_1} [inst : MulOneClass R], IsRegular 1
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₂.exists_desc : ∀ {X : SSet} (f₀ f₁ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₁ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₃ →
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃ →
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₀ =
          CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₁ →
        ∃ φ,
          CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₀ φ = f₀ ∧
            CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₁ φ = f₁ ∧
              CategoryTheory.CategoryStruct.comp SSet.horn₃₂.ι₃ φ = f₃
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ordered_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a b = Ordering.lt) t.toList
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.mapMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} [inst_1 : MulOneClass Y]
  [inst_2 : MulOneClass Z] (f : Y →* Z) (g : LocallyConstant X Y),
  (LocallyConstant.mapMonoidHom f) g = LocallyConstant.map (⇑f) g
-- Mathlib.CategoryTheory.Filtered.Small
/-- The "cofiltered closure" of an `α`-indexed family of objects in `C` is the set of objects in `C`
obtained by starting with the family and successively adding minima and equalizers.  -/
CategoryTheory.IsCofiltered.cofilteredClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsCofilteredOrEmpty C] → {α : Type w} → (α → C) → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Order.Group.Synonym
pow_ofColex : ∀ {α : Type u_1} {β : Type u_2} [inst : Pow α β] (a : α) (b : Colex β), a ^ ofColex b = a ^ b
-- Mathlib.Probability.Moments.IntegrableExpMul
/-- If `exp ((v + t) * X)` and `exp ((v - t) * X)` are integrable, then for all nonnegative `p : ℝ`,
`X ^ p * exp (v * X)` is integrable.  -/
ProbabilityTheory.integrable_rpow_mul_exp_of_integrable_exp_mul : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t v : ℝ},
  t ≠ 0 →
    MeasureTheory.Integrable (fun ω => Real.exp ((v + t) * X ω)) μ →
      MeasureTheory.Integrable (fun ω => Real.exp ((v - t) * X ω)) μ →
        ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => X ω ^ p * Real.exp (v * X ω)) μ
-- Init.Data.List.Sublist
List.sublist_flatten_iff : ∀ {α : Type u_1} {L : List (List α)} {l : List α},
  l.Sublist L.flatten ↔ ∃ L', l = L'.flatten ∧ ∀ (i : ℕ) (x : i < L'.length), L'[i].Sublist (L[i]?.getD [])
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.sSup_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R A)), S.Nonempty → (sSup S).toSubsemiring = sSup (Subalgebra.toSubsemiring '' S)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instAddCommGroup : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [AddCommGroup Y] → AddCommGroup (LocallyConstant X Y)
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.Indep.closure_insert_sdiff_eq_of_mem_closure`. -/
Matroid.Indep.closure_insert_diff_eq_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α},
  M.Indep I → f ∈ M.closure I → e ∈ M.closure (insert f I \ {e}) → M.closure (insert f I \ {e}) = M.closure I
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesColimitsOfShape_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D),
  Subsingleton (CategoryTheory.Limits.PreservesColimitsOfShape J F)