mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The canonical map `Φ.RightResolution X₂ → Φ.op.LeftResolution (Opposite.op X₂)`.  -/
CategoryTheory.LocalizerMorphism.RightResolution.op : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → Φ.RightResolution X₂ → Φ.op.LeftResolution (Opposite.op X₂)
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.instEssentiallySmallFullSubcategoryCofilteredClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  (f : α → C),
  CategoryTheory.EssentiallySmall.{max v w, v, u} (CategoryTheory.IsCofiltered.cofilteredClosure f).FullSubcategory
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂'_aux_eq : ∀ {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m]
  (M : Matrix n m N₂), Matrix.toLinearMap₂'Aux σ₁ σ₂ M = (Matrix.toLinearMapₛₗ₂' R σ₁ σ₂) M
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformation.documentation? : Lean.Lsp.ParameterInformation → Option Lean.Lsp.MarkupContent
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsCardinalClosure
/-- Given `P : ObjectProperty C` and `κ : Cardinal.{w}`, this is the closure
of `P` under colimits of shape given by categories `J` such that
`Arrow J` is of cardinality `< κ`.  -/
CategoryTheory.ObjectProperty.colimitsCardinalClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C → Cardinal.{w} → CategoryTheory.ObjectProperty C
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_right : ∀ {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]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L')),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.obj X).right = X.right
-- Mathlib.CategoryTheory.Category.Cat
/-- Under certain hypotheses, an equivalence of categories actually
defines an isomorphism in `Cat`.  -/
CategoryTheory.Cat.isoOfEquiv : {C D : CategoryTheory.Cat} →
  (e : ↑C ≌ ↑D) →
    (h₁ : ∀ (X : ↑C), e.inverse.obj (e.functor.obj X) = X) →
      (h₂ : ∀ (Y : ↑D), e.functor.obj (e.inverse.obj Y) = Y) →
        autoParam (∀ (X : ↑C), e.unitIso.hom.app X = CategoryTheory.eqToHom ⋯) CategoryTheory.Cat.isoOfEquiv._auto_1 →
          autoParam (∀ (Y : ↑D), e.counitIso.hom.app Y = CategoryTheory.eqToHom ⋯)
              CategoryTheory.Cat.isoOfEquiv._auto_3 →
            (C ≅ D)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_erase_le_maxKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = false → ∀ {fallback : α}, (cmp ((t.erase k).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true
-- Init.Core
instInhabitedMProd : {α β : Type u_1} → [Inhabited α] → [Inhabited β] → Inhabited (MProd α β)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mk_hom : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} (f : X ⟶ Y), (CategoryTheory.Arrow.mk f).hom = f
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- There exists `π : K` with `v`-adic valuation `WithZero.exp (-1)`.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  ∃ π, (IsDedekindDomain.HeightOneSpectrum.valuation K v) π = WithZero.exp (-1)
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.isRightAdjoint_of_leftAdjointObjIsDefined_eq_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor D C}, F.leftAdjointObjIsDefined = ⊤ → F.IsRightAdjoint
-- Mathlib.Data.Num.Bitwise
NzsNum.brecOn.eq : ∀ {motive : NzsNum → Sort u} (t : NzsNum) (F_1 : (t : NzsNum) → NzsNum.below t → motive t),
  NzsNum.brecOn t F_1 = F_1 t (NzsNum.brecOn.go t F_1).2
-- Mathlib.Order.KrullDimension
Order.krullDim_le_of_orderEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : PartialOrder β] (e : α ↪o β),
  Order.krullDim α ≤ Order.krullDim β
-- Mathlib.Algebra.Group.Action.Defs
IsCentralScalar.mk : ∀ {M : Type u_9} {α : Type u_10} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α],
  (∀ (m : M) (a : α), MulOpposite.op m • a = m • a) → IsCentralScalar M α
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.tendsto_norm_atTop_iff : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α},
  f' =Θ[l] g' → (Filter.Tendsto (norm ∘ f') l Filter.atTop ↔ Filter.Tendsto (norm ∘ g') l Filter.atTop)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasFDerivWithinAt.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E}
  {s : Set E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) • f') s x
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_le_map_iff_of_injective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Injective ⇑f →
    ∀ {S T : L.Substructure M},
      FirstOrder.Language.Substructure.map f S ≤ FirstOrder.Language.Substructure.map f T ↔ S ≤ T
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.withZeroUnitsEquiv_symm_apply_coe : ∀ {G : Type u_4} [inst : GroupWithZero G] [inst_1 : DecidablePred fun a => a = 0] (a : Gˣ),
  WithZero.withZeroUnitsEquiv.symm ↑a = ↑a
-- Mathlib.Order.Grade
Flag.isMin_coe : ∀ {α : Type u_3} [inst : PartialOrder α] {s : Flag α} {a : ↥s}, IsMin ↑a ↔ IsMin a
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Split polynomial functor, get an n-ary functor
from an `n+1`-ary functor  -/
MvPFunctor.drop : {n : ℕ} → MvPFunctor.{u} (n + 1) → MvPFunctor.{u} n
-- Mathlib.CategoryTheory.Presentable.Limits
CategoryTheory.isCardinalPresentable.congr_simp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (κ κ_1 : Cardinal.{w}) (e_κ : κ = κ_1)
  [inst_1 : Fact κ.IsRegular] (a a_1 : C),
  a = a_1 → CategoryTheory.isCardinalPresentable C κ a = CategoryTheory.isCardinalPresentable C κ_1 a_1
-- Mathlib.Tactic.Translate.ToAdditive
/-- `insert_to_additive_translation mulName addName` inserts the translation `mulName ↦ addName`
into the `to_additive` dictionary. This is useful for translating namespaces that don't (yet)
have a corresponding translated declaration.  -/
Mathlib.Tactic.ToAdditive.commandInsert_to_additive_translation__ : Lean.ParserDescr
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.toLocalRuleFilters : Aesop.Frontend.RuleExpr → Aesop.ElabM (Array Aesop.RuleFilter)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.mul_monomial_mem_coeffsIn : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S} {p : MvPolynomial σ S} {i : σ →₀ ℕ},
  p * (MvPolynomial.monomial i) 1 ∈ MvPolynomial.coeffsIn σ M ↔ p ∈ MvPolynomial.coeffsIn σ M
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.instInhabited : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → Inhabited (I.Filtration M)
-- Mathlib.Algebra.Module.Presentation.Free
Module.Relations.solutionFinsupp.congr_simp : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A) [inst_1 : IsEmpty relations.R],
  relations.solutionFinsupp = relations.solutionFinsupp
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β) →
                            (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size k v l
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))) →
              motive x
-- Mathlib.Order.Bounds.Basic
/-- If the range of a function `g` is bounded above, then `g ∘ f` is bounded above for all functions
`f`.  -/
BddAbove.range_comp_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] (f : γ → β) {g : β → α},
  BddAbove (Set.range g) → BddAbove (Set.range (g ∘ f))
-- Mathlib.Data.Part
Part.eq_of_mem : ∀ {α : Type u_1} {a b : Part α} (ha : a.Dom), a.get ha ∈ b → a = b
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.smul_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x y : R) (m : ↥M),
  x • IsLocalization.mk' S y m = IsLocalization.mk' S (x * y) m
-- Mathlib.Topology.Separation.NotNormal
/-- Let `s` be a closed set in a normal space and `d` be a dense set. If the induced topology on `s`
is discrete, then `𝒫 s` has cardinality less than or equal to `𝒫 d`.  -/
IsClosed.two_pow_mk_le_two_pow_mk_dense : ∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s d : Set X},
  IsClosed s → ∀ [DiscreteTopology ↑s], Dense d → 2 ^ Cardinal.mk ↑s ≤ 2 ^ Cardinal.mk ↑d
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.sumFrom_fin_tail : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (i : Fin n) (f : ℕ → R), BirdDet.sumFrom n (↑i + 1) f = ∑ k > i, f ↑k
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_inv : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Inv α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s : Finset α) (f : α → β), s⁻¹.sup f = s.sup fun x => f x⁻¹
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.instMonadAttachExceptTOfMonad.match_1.splitter : {m : Type (max u_1 u_2) → Type u_3} →
  {ε : Type (max u_1 u_2)} →
    [inst : MonadAttach m] →
      {α : Type (max u_1 u_2)} →
        (x : ExceptT ε m α) →
          (motive : (a : Except ε α) → MonadAttach.CanReturn x a → Sort u_4) →
            (a : Except ε α) →
              (h : MonadAttach.CanReturn x a) →
                ((a : α) → (h : MonadAttach.CanReturn x (Except.ok a)) → motive (Except.ok a) h) →
                  ((e : ε) → (h : MonadAttach.CanReturn x (Except.error e)) → motive (Except.error e) h) → motive a h
-- Mathlib.Algebra.Module.Torsion.Basic
isAddTorsion_iff_isTorsion_nat : ∀ {M : Type u_2} [inst : AddCommMonoid M], IsAddTorsion M ↔ Module.IsTorsion ℕ M
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- **Alias** of `Finset.prod_inter_mul_prod_sdiff`. -/
Finset.prod_inter_mul_prod_diff : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s t : Finset ι) (f : ι → M),
  (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x
-- Mathlib.CategoryTheory.Limits.Cones
/-- Cones on `F : J ⥤ C` are equivalent to cocones on `F.op : Jᵒᵖ ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coneOpEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → (CategoryTheory.Limits.Cone F)ᵒᵖ ≌ CategoryTheory.Limits.Cocone F.op
-- Mathlib.Logic.Encodable.Basic
/-- Explicit decoding function for a decidable subtype of an encodable type  -/
Encodable.decodeSubtype : {α : Type u_1} → {P : α → Prop} → [encA : Encodable α] → [decP : DecidablePred P] → ℕ → Option { a // P a }
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.hasFiniteIntegral_compProd_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  ⦃f : β × γ → E⦄,
  MeasureTheory.StronglyMeasurable f →
    (MeasureTheory.HasFiniteIntegral f ((κ.compProd η) a) ↔
      (∀ᵐ (x : β) ∂κ a, MeasureTheory.HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧
        MeasureTheory.HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a))
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Variant of `mul_le_of_le_one_left` for `b` non-positive instead of non-negative.  -/
le_mul_of_le_one_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
  [AddRightReflectLE R], b ≤ 0 → a ≤ 1 → b ≤ a * b
-- Init.GrindInstances.ToInt
Lean.Grind.instLEUInt64UintOfNatNat : Lean.Grind.ToInt.LE UInt64 (Lean.Grind.IntInterval.uint 64)
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_pos_iff_nontrivial_of_finite : ∀ {α : Type u_1} [inst : MetricSpace α] {s : Set α} [Finite ↑s], 0 < s.infsep ↔ s.Nontrivial
-- Mathlib.Computability.Reduce
OneOneReducible.of_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {e : α ≃ β} (q : β → Prop),
  Computable ⇑e → (q ∘ ⇑e) ≤₁ q
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The top map in the oplax left unitality square.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapₗ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            F ⟶
              ((CategoryTheory.MonoidalCategory.curriedTensor C).obj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).comp
                F
-- Mathlib.CategoryTheory.Category.Basic
/-- `rfl_cat` is a macro for `intros; rfl` which is attempted in `aesop_cat` before
doing the more expensive `aesop` tactic.

This gives a speedup because `simp` (called by `aesop`) can be very slow.
https://github.com/leanprover-community/mathlib4/pull/25475 contains measurements from June 2025.

Implementation notes:
* `refine id ?_`:
  In some cases it is important that the type of the proof matches the expected type exactly.
  e.g. if the goal is `2 = 1 + 1`, the `rfl` tactic will give a proof of type `2 = 2`.
  Starting a proof with `refine id ?_` is a trick to make sure that the proof has exactly
  the expected type, in this case `2 = 1 + 1`. See also
  https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/changing.20a.20proof.20can.20break.20a.20later.20proof
* `apply_rfl`:
  `rfl` is a macro that attempts both `eq_refl` and `apply_rfl`. Since `apply_rfl`
  subsumes `eq_refl`, we can use `apply_rfl` instead. This fails twice as fast as `rfl`.

 -/
CategoryTheory.rfl_cat : Lean.ParserDescr
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeFailureId : Lean.InternalExceptionId
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.pushforward_pullback_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.pushforward f (CategoryTheory.Presieve.pullback f R) ≤ R
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
/-- The underlying family for the basis of ideals in a multivariate power series ring.  -/
MvPowerSeries.LinearTopology.basis : (σ : Type u_1) → (R : Type u_2) → [inst : Ring R] → TwoSidedIdeal R × (σ →₀ ℕ) → TwoSidedIdeal (MvPowerSeries σ R)
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.toGradedObjectFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (K : HomologicalComplex₂ C c₁ c₂),
  (HomologicalComplex₂.toGradedObjectFunctor C c₁ c₂).obj K = K.toGradedObject
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.norm_expSeries_div_summable_of_mem_ball : ∀ (𝕂 : Type u_1) {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedDivisionRing 𝔸]
  [inst_2 : NormedAlgebra 𝕂 𝔸],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, Summable fun n => ‖x ^ n / ↑n.factorial‖
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_mono : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {F : α → Type u_5}
  [inst_1 : (i : α) → NormedAddCommGroup (F i)] {p : ENNReal},
  p ≠ 0 → ∀ {x : ↥(lp E p)} {y : ↥(lp F p)}, (∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖) → ‖x‖ ≤ ‖y‖
-- Mathlib.Condensed.Discrete.Basic
LightCondensed.discrete_map : ∀ (C : Type w) [inst : CategoryTheory.Category.{u, w} C]
  [inst_1 : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C] {X Y : C} (f : X ⟶ Y),
  (LightCondensed.discrete C).map f =
    (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).map
      ((CategoryTheory.Functor.const LightProfiniteᵒᵖ).map f)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- Given a natural transformation `τ : F ⟶ G` between functors `C ⥤ D` which preserve
the left homology of a short complex `S`, and a left homology data for `S`,
this is the left homology map data for the morphism `S.mapNatTrans τ`
obtained by evaluating `τ`.  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {S : CategoryTheory.ShortComplex C} →
              {F G : CategoryTheory.Functor C D} →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : G.PreservesZeroMorphisms] →
                    [inst_6 : F.PreservesLeftHomologyOf S] →
                      [inst_7 : G.PreservesLeftHomologyOf S] →
                        (h : S.LeftHomologyData) →
                          (τ : F ⟶ G) →
                            CategoryTheory.ShortComplex.LeftHomologyMapData (S.mapNatTrans τ) (h.map F) (h.map G)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.aevalAeval_C : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (x y : A)
  (p : Polynomial R), (Polynomial.aevalAeval x y) (Polynomial.C p) = (Polynomial.aeval x) p
-- Mathlib.Analysis.Complex.Basic
Complex.imCLM_apply : ∀ (z : ℂ), Complex.imCLM z = z.im
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.LocalGeneratorsData.quasiCoherentData_presentation_relations_s : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R}
  (q : M.LocalGeneratorsData) [inst_3 : q.IsLocallyFreeData] (i : q.I) (j : ULift.{u, 0} Empty),
  (q.quasiCoherentData.presentation i).relations.s j =
    Empty.rec (fun x => (CategoryTheory.Limits.kernel (q.generators i).π).sections) j.down
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {A B : C},
  CategoryTheory.Limits.kernelSubobject 0 = ⊤
-- Lean.LocalContext
Lean.LocalContext.contains : Lean.LocalContext → Lean.FVarId → Bool
-- Mathlib.Analysis.LocallyConvex.Basic
balanced_empty : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E], Balanced 𝕜 ∅
-- Mathlib.SetTheory.ZFC.Class
Class.coe_sUnion : ∀ (x : ZFSet.{u}), ↑x.sUnion = (↑x).sUnion
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.coker_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasCokernels C] (f : CategoryTheory.Arrow C),
  (CategoryTheory.Limits.coker C).obj f = CategoryTheory.Limits.cokernel f.hom
-- Mathlib.Algebra.QuaternionBasis
/-- A `QuaternionAlgebra.Basis` implies an `AlgHom` from the quaternions.  -/
QuaternionAlgebra.Basis.liftHom : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Algebra R A] →
          {c₁ c₂ c₃ : R} → QuaternionAlgebra.Basis A c₁ c₂ c₃ → QuaternionAlgebra R c₁ c₂ c₃ →ₐ[R] A
-- Mathlib.Topology.Sheaves.Stalks
/-- The stalks are isomorphic on inseparable points  -/
TopCat.Presheaf.stalkCongr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X : TopCat} → (F : TopCat.Presheaf C X) → {x y : ↑X} → Inseparable x y → (F.stalk x ≅ F.stalk y)
-- Init.Data.Int.Lemmas
Int.mul_add : ∀ (a b c : ℤ), a * (b + c) = a * b + a * c
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.union : Lean.Name → Array Lean.IR.IRType → Lean.IR.IRType
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_add_right : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ j → i ≠ k → ProbabilityTheory.CondIndepFun m' hm' (f i) (f j + f k) μ
-- Lean.Util.CollectLevelParams
Lean.collectLevelParams : Lean.CollectLevelParams.State → Lean.Expr → Lean.CollectLevelParams.State
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TermElabResult : Type → Type
-- Init.Data.String.Defs
String.str_toSlice : ∀ {s : String}, s.toSlice.str = s
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.analyticOnNhd_derivWeierstrassPExcept : ∀ (L : PeriodPair) (l₀ : ℂ), AnalyticOnNhd ℂ (L.derivWeierstrassPExcept l₀) (↑L.lattice \ {l₀})ᶜ
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- A measurable set such that `μ.restrict μ.sigmaFiniteSet` is sigma-finite,
and for all measurable sets `s ⊆ μ.sigmaFiniteSetᶜ`, either `μ s = 0` or `μ s = ∞`.  -/
MeasureTheory.Measure.sigmaFiniteSet : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → Set α