mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSliceData : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_prod_iff : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F' : Type u_11}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_12} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {n : WithTop ℕ∞} (f : M → M' × N'),
  ContMDiff I (I'.prod J') n f ↔ ContMDiff I I' n (Prod.fst ∘ f) ∧ ContMDiff I J' n (Prod.snd ∘ f)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple_zero_right : ∀ (k : ℕ), List.Nat.antidiagonalTuple k 0 = [0]
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse],
  (CategoryTheory.Equivalence.sheafCongr J K e A).inverse = CategoryTheory.Equivalence.sheafCongr.inverse J K e A
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from additive commutative groups to types creates all limits.  -/
AddCommGrpCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommGrpCat)
-- Init.Data.Vector.Range
Vector.pop_range' : ∀ {s n step : ℕ}, (Vector.range' s n step).pop = Vector.range' s (n - 1) step
-- Mathlib.Data.Fintype.EquivFin
/-- If the cardinality of `α` is `n`, there is noncomputably a bijection between `α` and `Fin n`.

See `Fintype.truncEquivFinOfCardEq` for the computable definition,
and `Fintype.truncEquivFin` and `Fintype.equivFin` for the bijection `α ≃ Fin (card α)`.
 -/
Fintype.equivFinOfCardEq : {α : Type u_1} → [inst : Fintype α] → {n : ℕ} → Fintype.card α = n → α ≃ Fin n
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.stabilizer_inf_stabilizer_le_stabilizer_apply₂ : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s t : Set α} {f : Set α → Set α → Set α},
  (∀ (a : G), a • f s t = f (a • s) (a • t)) →
    MulAction.stabilizer G s ⊓ MulAction.stabilizer G t ≤ MulAction.stabilizer G (f s t)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.struct.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.struct = 1
-- Mathlib.Data.Nat.Cast.Prod
Prod.instAddMonoidWithOne : {α : Type u_1} → {β : Type u_2} → [AddMonoidWithOne α] → [AddMonoidWithOne β] → AddMonoidWithOne (α × β)
-- Mathlib.Data.List.Basic
List.forall_mem_of_forall_mem_cons : ∀ {α : Type u} {p : α → Prop} {a : α} {l : List α}, (∀ x ∈ a :: l, p x) → ∀ x ∈ l, p x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertMany.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {ρ : Type u_1}
  [inst_1 : ForIn Id ρ (α × β)] (t t_1 : Std.ExtDTreeMap α (fun x => β) cmp),
  t = t_1 → ∀ (l l_1 : ρ), l = l_1 → Std.ExtDTreeMap.Const.insertMany t l = Std.ExtDTreeMap.Const.insertMany t_1 l_1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.size.eq_1 : ∀ {α : Type u} (x : Std.Rii α) [inst : Std.PRange.Least? α] [inst_1 : Std.Rxi.HasSize α],
  x.size =
    match Std.PRange.least? with
    | none => 0
    | some least => Std.Rxi.HasSize.size least
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedNewRawFact.default : Lean.Meta.Grind.NewRawFact
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.Gate.or : Std.Tactic.BVDecide.Gate
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.whiskerRight_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.LaxTrans.Modification η θ) {a b : B}
  {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g)
      (CategoryTheory.Bicategory.whiskerRight (θ.naturality f) g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) g)
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft (F.map f) (Γ.app b)) g)
-- Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
/-- `ConvexSpace.sConvexComb` in an affine space is the affine combination.  -/
AddTorsor.sConvexComb_eq_affineCombination : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  (s : Convexity.StdSimplex R P), Convexity.sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.constOfIsEmpty_apply : ∀ (R : Type u_1) [inst : Semiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (ι : Type u_7) [inst_5 : IsEmpty ι] (m : N),
  ⇑(AlternatingMap.constOfIsEmpty R M ι m) = Function.const (ι → M) m
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- `mapCompIso` gives rise to the lax functoriality constraint  -/
CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F : CategoryTheory.LaxFunctor B C} (self : F.PseudoCore) {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (self.mapCompIso f g).inv = F.mapComp f g
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_pow : ∀ (a : BitVec 8) (n : ℕ), { toBitVec := a ^ n } = { toBitVec := a } ^ n
-- Mathlib.Data.QPF.Univariate.Basic
QPF.suppPreservation_iff_liftpPreservation : ∀ {F : Type u → Type u} [q : QPF F], QPF.SuppPreservation ↔ QPF.LiftpPreservation
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.join₂.eq_1 : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R],
  MvPolynomial.join₂ = MvPolynomial.eval₂Hom (RingHom.id (MvPolynomial σ R)) MvPolynomial.X
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensorLift_tmul : ∀ {R : Type u} [inst : CommSemiring R] {M₁ M₂ M₃ : SemimoduleCat R} (f : ↑M₁ → ↑M₂ → ↑M₃)
  (h₁ : ∀ (m₁ m₂ : ↑M₁) (n : ↑M₂), f (m₁ + m₂) n = f m₁ n + f m₂ n)
  (h₂ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f (a • m) n = a • f m n)
  (h₃ : ∀ (m : ↑M₁) (n₁ n₂ : ↑M₂), f m (n₁ + n₂) = f m n₁ + f m n₂)
  (h₄ : ∀ (a : R) (m : ↑M₁) (n : ↑M₂), f m (a • n) = a • f m n) (m : ↑M₁) (n : ↑M₂),
  (CategoryTheory.ConcreteCategory.hom (SemimoduleCat.MonoidalCategory.tensorLift f h₁ h₂ h₃ h₄)) (m ⊗ₜ[R] n) = f m n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.equiv_iff_keysArray_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.keysArray = t₂.keysArray)
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The subgroup of elements fixed under the whole action.  -/
FixedPoints.subgroup : (M : Type u) → (α : Type v) → [inst : Monoid M] → [inst_1 : Group α] → [MulDistribMulAction M α] → Subgroup α
-- Init.Prelude
/-- `a > b` is an abbreviation for `b < a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `>` in identifiers is `gt`. -/
GT.gt : {α : Type u} → [LT α] → α → α → Prop
-- Mathlib.LinearAlgebra.Matrix.Block
/-- `BlockTriangular` matrices form a subsemiring.  -/
Matrix.blockTriangularSubsemiring : {α : Type u_1} →
  {m : Type u_3} →
    (R : Type v) →
      (m → α) →
        [LinearOrder α] →
          [inst : DecidableEq m] → [inst_1 : Fintype m] → [inst_2 : Semiring R] → Subsemiring (Matrix m m R)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_single_mul_eq_mul_coeff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : AddMonoidAlgebra R M} {r : R} {m m₁ : M} [inst_1 : Add M]
  (m₂ : M),
  (∀ m' ∈ x.coeff.support, m + m' = m₁ ↔ m' = m₂) → (AddMonoidAlgebra.single m r * x).coeff m₁ = r * x.coeff m₂
-- Mathlib.LinearAlgebra.Projectivization.PSL.PSL2
/-- `commutator (PSL ι F) = ⊤`.  -/
SL2Simple.PSL_commutator_eq_top : ∀ {F : Type u_2} [inst : Field F],
  (∃ a, a ≠ 0 ∧ a ^ 2 ≠ 1) → commutator (Matrix.ProjectiveSpecialLinearGroup (Fin 2) F) = ⊤
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.range : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSemisimpleModule R M] (f : M →ₗ[R] N),
  IsSemisimpleModule R ↥f.range
-- Mathlib.Data.Matrix.Block
Matrix.toBlock_mul_eq_mul : ∀ {R : Type u_10} [inst : CommRing R] {m : Type u_14} {n : Type u_15} {k : Type u_16} [inst_1 : Fintype n]
  (p : m → Prop) (q : k → Prop) (A : Matrix m n R) (B : Matrix n k R),
  (A * B).toBlock p q = A.toBlock p ⊤ * B.toBlock ⊤ q
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.ext_from_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : j + 1 = i)
  {A : C} (f g : (CochainComplex.mappingCone φ).X j ⟶ A),
  f = g ↔
    CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) f =
        CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl φ).v i j ⋯) g ∧
      CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) f =
        CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f j) g
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_mul : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x y : R) [inst : CommRing R], ↑(x * y) = ↑x * ↑y
-- Lean.Data.Lsp.Extra
Lean.Lsp.instInhabitedLineRange : Inhabited Lean.Lsp.LineRange
-- Mathlib.Algebra.Lie.Weights.RootSystem
/-- The reflection of a root along another.  -/
LieAlgebra.IsKilling.reflectRoot : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [CharZero K] →
        [inst_2 : LieRing L] →
          [inst_3 : LieAlgebra K L] →
            [LieAlgebra.IsKilling K L] →
              [FiniteDimensional K L] →
                {H : LieSubalgebra K L} →
                  [inst_6 : H.IsCartanSubalgebra] →
                    [LieModule.IsTriangularizable K (↥H) L] →
                      LieModule.Weight K (↥H) L → LieModule.Weight K (↥H) L → LieModule.Weight K (↥H) L
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `Bundle.Trivialization.localFrameCoeff_apply_of_notMem_baseSet`. -/
Bundle.Trivialization.localFrame_coeff_apply_of_notMem_baseSet : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F)
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M},
  x ∉ e.baseSet → ∀ (i : ι), Bundle.Trivialization.localFrameCoeff I e b i x = 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.drop.eq_3 : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (v_3 : V) (h : G.Adj u v_3) (n_2 : ℕ) (q : G.Walk v_3 v),
  (SimpleGraph.Walk.cons h q).drop n_2.succ = q.drop n_2
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.lt_cancel_var : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LT α] (ctx : Lean.Grind.CommRing.Context α) (c : ℤ)
  (x : Lean.Grind.CommRing.Var) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.cancel_var_cert c x p₁ p₂ = true →
    ↑c * Lean.Grind.CommRing.Var.denote ctx x = 1 →
      Lean.Grind.CommRing.Poly.denote ctx p₁ < 0 → Lean.Grind.CommRing.Poly.denote ctx p₂ < 0
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C}
  (toNatTrans : CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor)
  (app_η :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (T₁.η.app X) (toNatTrans.app X) = T₂.η.app X)
      CategoryTheory.MonadHom.app_η._autoParam)
  (app_μ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (toNatTrans.app X) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (T₁.map (toNatTrans.app X)) (toNatTrans.app (T₂.obj X))) (T₂.μ.app X))
      CategoryTheory.MonadHom.app_μ._autoParam)
  (toNatTrans_1 : CategoryTheory.NatTrans T₁.toFunctor T₂.toFunctor)
  (app_η_1 :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (T₁.η.app X) (toNatTrans_1.app X) = T₂.η.app X)
      CategoryTheory.MonadHom.app_η._autoParam)
  (app_μ_1 :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (T₁.μ.app X) (toNatTrans_1.app X) =
          CategoryTheory.CategoryStruct.comp
            (CategoryTheory.CategoryStruct.comp (T₁.map (toNatTrans_1.app X)) (toNatTrans_1.app (T₂.obj X)))
            (T₂.μ.app X))
      CategoryTheory.MonadHom.app_μ._autoParam),
  ({ toNatTrans := toNatTrans, app_η := app_η, app_μ := app_μ } =
      { toNatTrans := toNatTrans_1, app_η := app_η_1, app_μ := app_μ_1 }) =
    (toNatTrans = toNatTrans_1)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.

Version where the multiplication is replaced by a general bilinear form `M`.  -/
SchwartzMap.integral_bilin_fourier_eq : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℂ F] {G : Type u_5}
  [inst_9 : NormedAddCommGroup G] [inst_10 : NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E)
  (g : SchwartzMap V F) (M : E →L[ℂ] F →L[ℂ] G),
  ∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) (g ξ) = ∫ (x : V), (M (f x)) ((FourierTransform.fourier g) x)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- The map `a ↦ quasispectrum 𝕜 a` is upper hemicontinuous.  -/
upperHemicontinuous_quasispectrum : ∀ (𝕜 : Type u_1) (A : Type u_2) [inst : NontriviallyNormedField 𝕜] [ProperSpace 𝕜] [inst_2 : NonUnitalNormedRing A]
  [inst_3 : NormedSpace 𝕜 A] [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] [CompleteSpace A],
  UpperHemicontinuous (quasispectrum 𝕜)
-- Mathlib.Algebra.Lie.BaseChange
LieSubmodule.baseChange_bot : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : CommRing A] [inst_8 : Algebra R A], LieSubmodule.baseChange A ⊥ = ⊥
-- Mathlib.Order.Filter.Pointwise
Filter.nonneg_sub_iff : ∀ {α : Type u_2} [inst : AddGroup α] {f g : Filter α}, 0 ≤ f - g ↔ ¬Disjoint f g
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] (G : CategoryTheory.Functor D H) (β : L.comp G ⟶ F) (X : C),
  CategoryTheory.CategoryStruct.comp ((F'.liftOfIsRightKanExtension α G β).app (L.obj X)) (α.app X) = β.app X
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- If `C` has finite coproducts and filtered colimits, we can construct arbitrary coproducts by
taking the colimit of the diagram formed by the coproducts of finite sets over the indexing type.  -/
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetLimitCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [CategoryTheory.Limits.HasFiniteProducts C] →
        [CategoryTheory.Limits.HasLimitsOfShape (Finset (CategoryTheory.Discrete α))ᵒᵖ C] →
          (F : CategoryTheory.Functor (CategoryTheory.Discrete α) C) → CategoryTheory.Limits.LimitCone F
-- Batteries.Linter.UnnecessarySeqFocus
/-- * `true`: this `<;>` has been used unnecessarily at least once
* `false`: it has never been executed
* If it has been used properly at least once, the entry is removed from the table.
 -/
Batteries.Linter.UnnecessarySeqFocus.Entry.used : Batteries.Linter.UnnecessarySeqFocus.Entry → Bool
-- Aesop.Index
Aesop.Index.add : {α : Type} → Aesop.Rule α → Aesop.IndexingMode → Aesop.Index α → Aesop.Index α
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofZeros_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg).Q = S.X₂
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.UnitLike.State.map : Lean.Meta.Grind.UnitLike.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.inv_hom_id_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e.inv) (CategoryTheory.Arrow.Hom.right e.hom) =
    CategoryTheory.CategoryStruct.id g.right
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∩ t₂).getKey? k = none
-- Mathlib.Order.Hom.Lattice
/-- The constant function as an `InfHom`.  -/
InfHom.const : (α : Type u_2) → {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → β → InfHom α β
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integrableOn_Ioi_norm_cpow_iff : ∀ {s : ℂ} {t : ℝ}, 0 < t → (MeasureTheory.IntegrableOn (fun x => ‖↑x ^ s‖) (Set.Ioi t) MeasureTheory.volume ↔ s.re < -1)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.instUnique : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (r : HomRel C) → [Unique C] → Unique (CategoryTheory.Quotient r)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.step_filterWithPostcondition : ∀ {α β : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)} [inst_1 : Monad n] [LawfulMonad n]
  [inst_3 : MonadLiftT m n],
  (Std.IterM.filterWithPostcondition f it).step = do
    let __do_lift ← liftM it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← (f out).operation
        match __do_lift with
          | ⟨{ down := false }, h'⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterWithPostcondition f it') ⋯))
          | ⟨{ down := true }, h'⟩ =>
            pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.filterWithPostcondition f it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.filterWithPostcondition f it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_limit : ∀ {o : Ordinal.{u_1}}, Order.IsSuccLimit o → Cardinal.aleph o = ⨆ a, Cardinal.aleph ↑a
-- Init.Data.Array.Attach
Array.back?_attachWith : ∀ {α : Type u_1} {P : α → Prop} {xs : Array α} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H).back? = xs.back?.pbind fun a h => some ⟨a, ⋯⟩
-- Std.Async.System
Std.Async.System.instDecidableEqSystemUser : DecidableEq Std.Async.System.SystemUser
-- Mathlib.Order.Monotone.Defs
Function.const_mono : ∀ {α : Type u} {β : Type v} [inst : Preorder α], Monotone (Function.const β)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_linear_comp : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {M' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {v : α → M} (f : M →ₗ[R] M'),
  Finsupp.linearCombination R (⇑f ∘ v) = f ∘ₗ Finsupp.linearCombination R v
-- Mathlib.Computability.Primrec.Basic
Primrec₂.curry : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α × β → σ}, Primrec₂ (Function.curry f) ↔ Primrec f
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin.fst.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] (F F_1 : Finset (α × α)) (e_F : F = F_1) {k : ℕ} (h : F.card = k) (a a_1 : α),
  a = a_1 →
    ∀ (i i_1 : Fin (k + 1)),
      i = i_1 → Finset.intervalGapsWithin.fst F h a i = Finset.intervalGapsWithin.fst F_1 ⋯ a_1 i_1
-- Mathlib.Algebra.Tropical.Basic
Tropical.instPreorderTropical : {R : Type u} → [Preorder R] → Preorder (Tropical R)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- The unit for the monoidal structure on `AugmentedSimplexCategory` is the initial object.  -/
AugmentedSimplexCategory.tensorUnit : AugmentedSimplexCategory
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f : α → E}
  {a b : α} (hf : BoundedVariationOn f Set.univ),
  a ≤ b → hf.vectorMeasure (Set.Ico a b) = Function.leftLim f b - Function.leftLim f a
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousLinearMap.compContinuousMultilinearMap_coe : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  (g : M₂ →L[R] M₃) (f : ContinuousMultilinearMap R M₁ M₂), ⇑(g.compContinuousMultilinearMap f) = ⇑g ∘ ⇑f
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.pairwise_disjoint_Ioo_add_intCast : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] (a : α),
  Pairwise (Function.onFun Disjoint fun n => Set.Ioo (a + ↑n) (a + ↑n + 1))
-- Mathlib.Algebra.Group.Conj
IsConj.refl : ∀ {α : Type u} [inst : Monoid α] (a : α), IsConj a a