mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.LIntegral
MeasureTheory.lintegral_sub_left_eq_self : ∀ {G : Type u_1} [inst : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_1 : AddGroup G] [MeasurableAdd G]
  [μ.IsAddLeftInvariant] [MeasurableNeg G] [μ.IsNegInvariant] (f : G → ENNReal) (g : G),
  ∫⁻ (x : G), f (g - x) ∂μ = ∫⁻ (x : G), f x ∂μ
-- Mathlib.Condensed.Discrete.Module
/-- Auxiliary definition for `functorIsoDiscrete`.  -/
CondensedMod.LocallyConstant.functorIsoDiscreteAux₂ : (R : Type (u + 1)) →
  [inst : Ring R] →
    (M : ModuleCat R) →
      (Condensed.discrete (ModuleCat R)).obj M ≅
        (Condensed.discrete (ModuleCat R)).obj (ModuleCat.of R (LocallyConstant ↑(CompHaus.of PUnit.{u + 1}).toTop ↑M))
-- Mathlib.Order.PrimeIdeal
Order.PFilter.IsPrime.compl_ideal : ∀ {P : Type u_1} {inst : Preorder P} {F : Order.PFilter P} [self : F.IsPrime], Order.IsIdeal (↑F)ᶜ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `sub_neg`.

---

For `a - -b = a + b`, see `sub_neg_eq_add`.  -/
lt_of_sub_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, a - b < 0 → a < b
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.ExistsHomHomCompEqCompAux.g.eq_1 : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] {S X : AlgebraicGeometry.Scheme}
  {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} {t : D ⟶ (CategoryTheory.Functor.const I).obj S} {f : X ⟶ S}
  [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] [inst_2 : CategoryTheory.IsCofiltered I]
  [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f),
  A.g = CategoryTheory.CategoryStruct.comp (D.map A.hii') (CategoryTheory.Limits.pullback.lift A.a A.b ⋯)
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- **Alias** of the reverse direction of `upperHemicontinuousOn_iff_forall_isOpen`. -/
UpperHemicontinuousOn.of_forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} {s : Set α} [inst_1 : TopologicalSpace β],
  (∀ x ∈ s, ∀ (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ u) → UpperHemicontinuousOn f s
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instAddGroup.eq_1 : ∀ {α : Type u} [inst : AddMonoid α],
  AddUnits.instAddGroup = { toSubNegMonoid := AddUnits.instSubNegAddMonoid, neg_add_cancel := ⋯ }
-- Init.Data.List.Count
List.countP_false : ∀ {α : Type u_1}, (List.countP fun x => false) = Function.const (List α) 0
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPushout.inr_iso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {W X Y : C} (f : W ⟶ X) (g : W ⟶ Y)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) G]
  [inst_3 : CategoryTheory.Limits.HasPushout f g] [inst_4 : CategoryTheory.Limits.HasPushout (G.map f) (G.map g)]
  {Z : D} (h : G.obj (CategoryTheory.Limits.pushout f g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (G.map f) (G.map g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPushout.iso G f g).hom h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pushout.inr f g)) h
-- Init.Data.Slice.Notation
Std.Ric.Sliceable.mk : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → (α → Std.Ric β → γ) → Std.Ric.Sliceable α β γ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α}, (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The centralizer of a set as non-unital subsemiring.  -/
NonUnitalSubsemiring.centralizer : {R : Type u_1} → [inst : NonUnitalSemiring R] → Set R → NonUnitalSubsemiring R
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.formPerm.congr_simp : ∀ {α : Type u_1} [inst : DecidableEq α] (s s_1 : Cycle α) (e_s : s = s_1) (a : s.Nodup), s.formPerm a = s_1.formPerm ⋯
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.MakesOverArrow.of_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A} {X : C}
  {s : CategoryTheory.yoneda.obj X ⟶ A} {f : CategoryTheory.yoneda.obj X ⟶ F},
  CategoryTheory.CategoryStruct.comp f η = s →
    CategoryTheory.OverPresheafAux.MakesOverArrow η s (CategoryTheory.yonedaEquiv f)
-- Mathlib.Analysis.Complex.Circle
Circle.coe_injective : Function.Injective Subtype.val
-- Mathlib.GroupTheory.Torsion
CommGroup.torsion_eq_top_iff : ∀ {G : Type u_1} [inst : CommGroup G], CommGroup.torsion G = ⊤ ↔ IsMulTorsion G
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rio : ∀ {n i : ℕ}, (*...n).toList[i]! = if i < n then i else 0
-- Mathlib.Algebra.Group.Submonoid.Defs
OneMemClass.one_def : ∀ {A : Type u_3} {M₁ : Type u_4} [inst : SetLike A M₁] [inst_1 : One M₁] [hA : OneMemClass A M₁] (S' : A), 1 = ⟨1, ⋯⟩
-- Lean.Parser.Extension
Lean.Parser.addSyntaxNodeKind : Lean.Environment → Lean.SyntaxNodeKind → Lean.Environment
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instNegSubtypeMem : {R : Type u} →
  {M : Type v} → [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : SubMulAction R M) → Neg ↥p
-- Mathlib.Probability.Moments.SubGaussian
/-- For `ν : Measure Ω'`, `κ : Kernel Ω' Ω` and `η : Ω Ω''`, if a random variable `X : Ω → ℝ`
has a sub-Gaussian mgf with respect to `κ` and `ν` and another random variable `Y : Ω'' → ℝ` has
a sub-Gaussian mgf with respect to `η` and `κ ∘ₘ ν : Measure Ω`, then `X + Y` (random
variable on the measurable space `Ω × Ω''`) has a sub-Gaussian mgf with respect to
`κ ⊗ₖ prodMkLeft Ω' η : Kernel Ω' (Ω × Ω'')` and `ν`.  -/
ProbabilityTheory.Kernel.HasSubgaussianMGF.add_comp : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {κ : ProbabilityTheory.Kernel Ω' Ω} {X : Ω → ℝ} {c : NNReal} {Ω'' : Type u_3} {mΩ'' : MeasurableSpace Ω''}
  {Y : Ω'' → ℝ} {cY : NNReal} [MeasureTheory.SFinite ν] {η : ProbabilityTheory.Kernel Ω Ω''}
  [ProbabilityTheory.IsZeroOrMarkovKernel η],
  ProbabilityTheory.Kernel.HasSubgaussianMGF X c κ ν →
    ProbabilityTheory.Kernel.HasSubgaussianMGF Y cY η (ν.bind ⇑κ) →
      ProbabilityTheory.Kernel.HasSubgaussianMGF (fun p => X p.1 + Y p.2) (c + cY)
        (κ.compProd (ProbabilityTheory.Kernel.prodMkLeft Ω' η)) ν
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Subalgebra.centralizer_tensorProduct_eq_center_tensorProduct_right : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [Module.Free R A],
  Subalgebra.centralizer R ↑(Algebra.TensorProduct.map (Algebra.ofId R A) (AlgHom.id R B)).range =
    (Algebra.TensorProduct.map (AlgHom.id R A) (Subalgebra.center R B).val).range
-- Init.Data.Nat.Coprime
Nat.Coprime.coprime_mul_left : ∀ {k m n : ℕ}, (k * m).Coprime n → m.Coprime n
-- Mathlib.NumberTheory.MulChar.Basic
/-- **Alias** of `MulChar.domRestrict`.

---

The restriction of a `MulChar` to a submonoid.
 -/
MulChar.restrict : {R : Type u_1} →
  [inst : CommMonoid R] →
    {R' : Type u_2} →
      [inst_1 : CommMonoidWithZero R'] →
        {S : Type u_3} →
          [inst_2 : SetLike S R] → [inst_3 : SubmonoidClass S R] → (T : S) → MulChar R R' → MulChar (↥T) R'
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α}, (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.uniqueHomFromTrivial.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.AddGrp C),
  A.uniqueHomFromTrivial =
    (have this := CategoryTheory.InducedCategory.homEquiv;
      this).unique
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLE.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α]
  [toContravariantClass : ContravariantClass { x // 0 < x } α (fun x y => ↑x * y) fun x1 x2 => x1 ≤ x2],
  PosMulReflectLE α
-- Mathlib.RingTheory.Polynomial.SmallDegreeVieta
/-- **Vieta's formula** for quadratics as an iff (`aroots` version).  -/
Polynomial.aroots_quadratic_eq_pair_iff_of_ne_zero : ∀ {T : Type u_2} {S : Type u_3} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  {a b c : T} {x1 x2 : S},
  (algebraMap T S) a ≠ 0 →
    ((Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).aroots S = {x1, x2} ↔
      (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2) ∧ (algebraMap T S) c = (algebraMap T S) a * x1 * x2)
-- Mathlib.RingTheory.IdealFilter.Topology
/-- A set `s` is a neighbourhood of `0` iff it contains an ideal belonging to `F`.  -/
WithIdealFilter.mem_nhds_zero_iff : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} {s : Set (WithIdealFilter F)},
  s ∈ nhds 0 ↔ ∃ I ∈ F, WithIdealFilter.idealSet I ⊆ s
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_comm : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {ι' : Type u_8} (μ : ι → ι' → MeasureTheory.Measure α),
  (MeasureTheory.Measure.sum fun n => MeasureTheory.Measure.sum (μ n)) =
    MeasureTheory.Measure.sum fun m => MeasureTheory.Measure.sum fun n => μ n m
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.mem_supported' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  {s : Set M} {x : AddMonoidAlgebra S M}, x ∈ AddMonoidAlgebra.supported R S s ↔ ∀ m ∉ s, x.coeff m = 0
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.Hom.hom.eq_1 : ∀ {X Y : MonCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
SeparationQuotient.outCLM_isUniformEmbedding : ∀ (K : Type u_1) (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : UniformSpace E] [inst_4 : IsUniformAddGroup E] [inst_5 : ContinuousConstSMul K E],
  IsUniformEmbedding ⇑(SeparationQuotient.outCLM K E)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.norm_pos : ∀ {x : GaussianInt}, 0 < Zsqrtd.norm x ↔ x ≠ 0
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.limitModule : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] →
            Module R (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt
-- Mathlib.LinearAlgebra.Matrix.Block
/-- The inverse of an upper-left subblock of a block-triangular matrix `M` is the upper-left
subblock of `M⁻¹`.  -/
Matrix.BlockTriangular.inv_toBlock : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : CommRing R] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : LinearOrder α] [Invertible M],
  M.BlockTriangular b →
    ∀ (k : α), (M.toBlock (fun i => b i < k) fun i => b i < k)⁻¹ = M⁻¹.toBlock (fun i => b i < k) fun i => b i < k
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
AffineBasis.coords.eq_1 : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P),
  b.coords =
    { toFun := fun q i => (b.coord i) q,
      linear := { toFun := fun v i => -(b.basisOf i).sumCoords v, map_add' := ⋯, map_smul' := ⋯ }, map_vadd' := ⋯ }
-- Init.Data.Int.Cooper
Int.add_of_le : {a b : ℤ} → a ≤ b → { c // b = a + ↑c }
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal C =
    {
      obj := fun A =>
        CategoryTheory.LaxMonoidalFunctor.of
          (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A),
      map := fun {X Y} f => { hom := { app := fun x => f.hom, naturality := ⋯ }, isMonoidal := ⋯ }, map_id := ⋯,
      map_comp := ⋯ }
-- Mathlib.CategoryTheory.Products.Basic
/-- `Category.uniformProd C D` is an additional instance specialised so both factors have the same
universe levels. This helps typeclass resolution.
 -/
CategoryTheory.uniformProd : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₁) → [CategoryTheory.Category.{v₁, u₁} D] → CategoryTheory.Category.{v₁, u₁} (C × D)
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.instInhabitedCancelParams : Inhabited Lean.Lsp.CancelParams
-- Mathlib.Algebra.GCDMonoid.Basic
instNormalizedGCDMonoidOfStrongNormalizedGCDMonoid : (α : Type u_2) → [inst : CommMonoidWithZero α] → [StrongNormalizedGCDMonoid α] → NormalizedGCDMonoid α
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.base_eqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g : X ⟶ Y} (α : f = g),
  CategoryTheory.CatEnrichedOrdinary.Hom.base (CategoryTheory.eqToHom α) = CategoryTheory.eqToHom ⋯
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The projection on the `i`-th coordinate of `EuclideanSpace 𝕜 ι`, as a linear map.  -/
EuclideanSpace.projₗ : {ι : Type u_1} → {𝕜 : Type u_3} → [inst : RCLike 𝕜] → ι → EuclideanSpace 𝕜 ι →ₗ[𝕜] 𝕜
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_le_tsum_of_inj : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {g : κ → α} (e : ι → κ),
  Function.Injective e →
    (∀ c ∉ Set.range e, 0 ≤ g c) → (∀ (i : ι), f i ≤ g (e i)) → Summable f → Summable g → tsum f ≤ tsum g
-- Mathlib.Algebra.Group.Int.Defs
zsmul_int_int : ∀ (a b : ℤ), a • b = a * b
-- Mathlib.Data.List.Chain
List.isChain_map : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} (f : β → α) {l : List β},
  List.IsChain R (List.map f l) ↔ List.IsChain (fun a b => R (f a) (f b)) l
-- Lean.Meta.AppBuilder
/-- If `e` is `@Eq.refl α a`, returns `a`.
 -/
Lean.Meta.isRefl? : Lean.Expr → Option Lean.Expr
-- Mathlib.Algebra.CubicDiscriminant
Cubic.a_of_eq : ∀ {R : Type u_1} {P Q : Cubic R} [inst : Semiring R], P.toPoly = Q.toPoly → P.a = Q.a
-- Mathlib.Topology.ContinuousMap.Basic
/-- "Precomposition" as a continuous map between dependent types.  -/
ContinuousMap.precomp : {I : Type u_5} →
  {X : I → Type u_7} →
    [inst : (i : I) → TopologicalSpace (X i)] → {ι : Type u_9} → (φ : ι → I) → C((i : I) → X i, (i : ι) → X (φ i))
-- Mathlib.GroupTheory.Perm.Closure
Equiv.Perm.closure_cycle_coprime_swap : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {n : ℕ} {σ : Equiv.Perm α},
  n.Coprime (Fintype.card α) →
    σ.IsCycle → σ.support = Finset.univ → ∀ (x : α), Subgroup.closure {σ, Equiv.swap x ((σ ^ n) x)} = ⊤
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabPProdMk : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instSeminormedAddCommGroup : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : SeminormedAddCommGroup β] → SeminormedAddCommGroup (ZeroAtInftyContinuousMap α β)
-- Mathlib.MeasureTheory.Measure.OpenPos
Continuous.ae_eq_iff_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {m : MeasurableSpace X} [inst_1 : TopologicalSpace Y]
  [T2Space Y] (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure] {f g : X → Y},
  Continuous f → Continuous g → (f =ᵐ[μ] g ↔ f = g)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.zsmul.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (i : ℤ) (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.zsmul i a = Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.intCast i) a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (j : D),
  ((CategoryTheory.evaluation D C).obj j).PreservesZeroMorphisms
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafificationIso_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Sheaf J D), (CategoryTheory.sheafificationIso P).inv.hom = (CategoryTheory.isoSheafify J ⋯).inv
-- Mathlib.Data.Ordmap.Invariants
Ordnode.size_eq_realSize : ∀ {α : Type u_1} {t : Ordnode α}, t.Sized → t.size = t.realSize
-- Aesop.Rule.Name
Aesop.DisplayRuleName.instToString : ToString Aesop.DisplayRuleName
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ} {k k' : α},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.get? (Std.DTreeMap.filterMap f t) k = (Std.DTreeMap.Const.get? t k).bind (f k')
-- Init.Control.Lawful.MonadLift.Basic
/-- The `MonadLift` typeclass only contains the lifting operation. `LawfulMonadLift` further
  asserts that lifting commutes with `pure` and `bind`:
```
monadLift (pure a) = pure a
monadLift (ma >>= f) = monadLift ma >>= monadLift ∘ f
```
 -/
LawfulMonadLift : (m : semiOutParam (Type u → Type v)) → (n : Type u → Type w) → [Monad m] → [Monad n] → [inst : MonadLift m n] → Prop
-- Mathlib.MeasureTheory.Measure.AEMeasurable
Subsingleton.aemeasurable : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [Subsingleton α], AEMeasurable f μ
-- Mathlib.Analysis.InnerProductSpace.Completion
SeparationQuotient.instInner : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → Inner 𝕜 (SeparationQuotient E)
-- Mathlib.Order.Filter.CountableInter
Filter.EventuallyLE.countable_bInter : ∀ {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι},
  S.Countable →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) → ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
AbsoluteValue.IsAdmissible.mk.inj : ∀ {R : Type u_1} {inst : EuclideanDomain R} {abv : AbsoluteValue R ℤ} {toIsEuclidean : abv.IsEuclidean} {card : ℝ → ℕ}
  {exists_partition' :
    ∀ (n : ℕ) {ε : ℝ},
      0 < ε →
        ∀ {b : R},
          b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε}
  {toIsEuclidean_1 : abv.IsEuclidean} {card_1 : ℝ → ℕ}
  {exists_partition'_1 :
    ∀ (n : ℕ) {ε : ℝ},
      0 < ε →
        ∀ {b : R},
          b ≠ 0 → ∀ (A : Fin n → R), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε},
  { toIsEuclidean := toIsEuclidean, card := card, exists_partition' := exists_partition' } =
      { toIsEuclidean := toIsEuclidean_1, card := card_1, exists_partition' := exists_partition'_1 } →
    card = card_1
-- Mathlib.Algebra.DirectSum.LinearMap
/-- If a linear map `f : M₁ → M₂` respects direct sum decompositions of `M₁` and `M₂`, then it has a
block diagonal matrix with respect to bases compatible with the direct sum decompositions.  -/
LinearMap.toMatrix_directSum_collectedBasis_eq_blockDiagonal' : ∀ {ι : Type u_1} [inst : DecidableEq ι] {R : Type u_4} {M₁ : Type u_5} {M₂ : Type u_6} [inst_1 : CommSemiring R]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M₁] {N₁ : ι → Submodule R M₁} (h₁ : DirectSum.IsInternal N₁)
  [inst_4 : AddCommMonoid M₂] [inst_5 : Module R M₂] {N₂ : ι → Submodule R M₂} (h₂ : DirectSum.IsInternal N₂)
  {κ₁ : ι → Type u_7} {κ₂ : ι → Type u_8} [inst_6 : (i : ι) → Fintype (κ₁ i)] [inst_7 : ∀ (i : ι), Finite (κ₂ i)]
  [inst_8 : (i : ι) → DecidableEq (κ₁ i)] [inst_9 : Fintype ι] (b₁ : (i : ι) → Module.Basis (κ₁ i) R ↥(N₁ i))
  (b₂ : (i : ι) → Module.Basis (κ₂ i) R ↥(N₂ i)) {f : M₁ →ₗ[R] M₂} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N₁ i) ↑(N₂ i)),
  (LinearMap.toMatrix (h₁.collectedBasis b₁) (h₂.collectedBasis b₂)) f =
    Matrix.blockDiagonal' fun i => (LinearMap.toMatrix (b₁ i) (b₂ i)) (f.restrict ⋯)
-- Mathlib.RingTheory.Finiteness.Small
Submodule.small_iSup : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  {P : ι → Submodule R M} [Small.{u, u_3} ι] [∀ (i : ι), Small.{u, u_2} ↥(P i)], Small.{u, u_2} ↥(iSup P)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.singleton_ne_univ : ∀ {α : Type u_1} [inst : Fintype α] [Nontrivial α] (a : α), {a} ≠ Finset.univ
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If a function `f` tends to infinity along a filter,
then `f` divided by a negative constant tends to negative infinity.  -/
Filter.Tendsto.atTop_div_const_of_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, r < 0 → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x / r) l Filter.atBot
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
QuadraticMap.Isometry.map_app : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} {N : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (f : Q₁ →qᵢ Q₂) (m : M₁), Q₂ (f m) = Q₁ m
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_insertMany_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α},
  (t.insertMany l).size ≤ t.size + l.length
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the entry (key-value pair) for the key `k`.  -/
Std.DTreeMap.Internal.Impl.getEntry : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → (t : Std.DTreeMap.Internal.Impl α β) → (k : α) → k ∈ t → (a : α) × β a
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.instCoeSphereSet : {P : Type u_2} → [inst : MetricSpace P] → Coe (EuclideanGeometry.Sphere P) (Set P)
-- Init.Data.Vector.Nat
Vector.prod_append_nat : ∀ {n m : ℕ} {as₁ : Vector ℕ n} {as₂ : Vector ℕ m}, (as₁ ++ as₂).prod = as₁.prod * as₂.prod
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Equiv.subtypeQuotientEquivQuotientSubtype.congr_simp : ∀ {α : Sort u_1} (p₁ : α → Prop) {s₁ : Setoid α} {s₂ : Setoid (Subtype p₁)} (p₂ : Quotient s₁ → Prop)
  (hp₂ : ∀ (a : α), p₁ a ↔ p₂ ⟦a⟧) (h : ∀ (x y : Subtype p₁), s₂ x y ↔ s₁ ↑x ↑y),
  Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h = Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h
-- Mathlib.Topology.Order.Compact
eq_Icc_of_connected_compact : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {s : Set α}, IsConnected s → IsCompact s → s = Set.Icc (sInf s) (sSup s)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CnstrRHS.mk : Array Lean.Name → ℕ → Lean.Expr → Lean.Meta.Grind.CnstrRHS
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.swap_mapComp_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Prod.swap B C).mapComp f g).inv =
    CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.2 g.2))
      (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f.1 g.1))