mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_nnratCast : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → DivisionSemiring (G i)] [inst_7 : DivisionSemiring C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] [∀ (i : ι), RingHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (q : ℚ≥0),
  DirectLimit.lift f (fun x => ⇑(g x)) h ↑q = ↑q
-- Mathlib.Data.List.Sort
List.sortedGE_iff_isChain : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGE ↔ List.IsChain (fun x1 x2 => x1 ≥ x2) l
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_eq_top_of_forall_nnreal_isBigO : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F),
  (∀ (r : NNReal), (fun n => ‖p n‖ * ↑r ^ n) =O[Filter.atTop] fun x => 1) → p.radius = ⊤
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G H : CategoryTheory.LaxMonoidalFunctor C D} (α : F ⟶ G) (β : G ⟶ H),
  (CategoryTheory.CategoryStruct.comp α β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.LiftActionCoreResult : Type
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentChangeRegistrationOptions : Type
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.add_mul_of_isSuccLimit : ∀ {a b c : Ordinal.{u_4}}, b + a = a → Order.IsSuccLimit c → (a + b) * c = a * c
-- Mathlib.Analysis.Analytic.Polynomial
AnalyticOn.eval_polynomial : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {A : Type u_5} [inst_1 : NormedCommRing A]
  [inst_2 : NormedAlgebra 𝕜 A] (p : Polynomial A), AnalyticOn 𝕜 (fun x => Polynomial.eval x p) Set.univ
-- Mathlib.AlgebraicTopology.SingularHomology.HomologyZero
/-- The singular homology of a topological space `X` with coefficients in `R`
identifies with the coproduct of copies of `R` indexed by `ZerothHomotopy X`.  -/
TopCat.singularHomology₀Iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [inst_3 : CategoryTheory.CategoryWithHomology C] →
          (X : TopCat) → (R : C) → ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj X ≅ ∐ fun x => R
-- Mathlib.NumberTheory.Height.NumberField
NumberField.sum_archAbsVal_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {M : Type u_2} [inst_2 : AddCommMonoid M]
  (f : AbsoluteValue K ℝ → M), (Multiset.map f Height.AdmissibleAbsValues.archAbsVal).sum = ∑ v, v.mult • f ↑v
-- Mathlib.Data.Finset.Card
/-- `s.card` is the number of elements of `s`, aka its cardinality.

The notation `#s` can be accessed in the `Finset` locale.  -/
Finset.«term#_» : Lean.ParserDescr
-- Mathlib.Analysis.Convex.Between
Wbtw.mem_affineSpan : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P}, Wbtw R x y z → y ∈ line[R, x, z]
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.leftUnitor_naturality : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X Y : CategoryTheory.LocalizedMonoidal L W ε} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.LocalizedMonoidal L W ε)) f)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom f
-- Mathlib.Algebra.Group.Units.Basic
AddUnits.add_left_inj : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α) {b c : α}, b + ↑a = c + ↑a ↔ b = c
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpen_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (OnePoint X)},
  IsOpen s ↔ (OnePoint.infty ∈ s → IsCompact (OnePoint.some ⁻¹' s)ᶜ) ∧ IsOpen (OnePoint.some ⁻¹' s)
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.recF_eq_of_wEquiv : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] (α : TypeVec.{u} n) {β : Type u} (u : F (α ::: β) → β)
  (x y : (MvQPF.P F).W α), MvQPF.WEquiv x y → MvQPF.recF u x = MvQPF.recF u y
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `RightDistribClass` instance along an injective function.  -/
Function.Injective.rightDistribClass : ∀ {R : Type u_1} {S : Type u_2} (f : S → R),
  Function.Injective f →
    ∀ [inst : Add S] [inst_1 : Mul S] [inst_2 : Mul R] [inst_3 : Add R] [RightDistribClass R],
      (∀ (x y : S), f (x + y) = f x + f y) → (∀ (x y : S), f (x * y) = f x * f y) → RightDistribClass S
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- Let $M$ be a flat module. Let $K$ and $N$ be finite $R$-modules with $N$
free, and let $f \colon K \to N$ and $x \colon N \to M$ be linear maps such that
$x \circ f = 0$. Then there exist a finite free module $R^k$ and linear maps
$a \colon N \to R^k$ and $y \colon R^k \to M$ such that $x = y \circ a$ and
$a \circ f = 0$.  -/
Module.Flat.exists_factorization_of_comp_eq_zero_of_free : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Flat R M]
  {K : Type u_3} {N : Type u_4} [inst_4 : AddCommGroup K] [inst_5 : Module R K] [Module.Finite R K]
  [inst_7 : AddCommGroup N] [inst_8 : Module R N] [Module.Free R N] [Module.Finite R N] {f : K →ₗ[R] N} {x : N →ₗ[R] M},
  x ∘ₗ f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a ∘ₗ f = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_eq_none_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey? = none ↔ t.isEmpty = true
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.isSemisimpleModule_iff_jacobson : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M],
  IsSemisimpleModule R M ↔ Module.jacobson R M = ⊥
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.sub_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Zero M] [inst_1 : Zero N] [inst_2 : SubtractionMonoid P]
  (g₁ g₂ : ZeroHom N P) (f : ZeroHom M N), (g₁ - g₂).comp f = g₁.comp f - g₂.comp f
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Iio_of_strictMonoOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Iic a) →
    StrictMonoOn f (Set.Iic a) → Filter.Tendsto f Filter.atBot Filter.atBot → f '' Set.Iio a = Set.Iio (f a)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A typeclass for non-associative monoids with zero elements.  -/
MulZeroOneClass : Type u → Type u
-- Lean.Parser.Command
Lean.Parser.Command.eoi.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Category.HeytAlg
/-- Constructs an isomorphism of Heyting algebras from an order isomorphism between them.  -/
HeytAlg.Iso.mk : {α β : HeytAlg} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.comp_relation : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) [inst_5 : Algebra R T]
  [inst_6 : IsScalarTower R S T] (a : σ' ⊕ σ),
  (Q.comp P).relation a = Sum.elim (Q.compRelationAux P) (fun rp => (MvPolynomial.rename Sum.inr) (P.relation rp)) a
-- Mathlib.Probability.ConditionalProbability
/-- Delaborator for `μ[t | s]` notation.  -/
ProbabilityTheory.delabCondApplied : Lean.PrettyPrinter.Delaborator.Delab
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.request : Lean.JsonRpc.MessageKind
-- Mathlib.Data.Vector.Basic
_private.Mathlib.Data.Vector.Basic.0.List.Vector.ofFn.match_1.eq_1 : ∀ {α : Type u_2} (motive : (x : ℕ) → (Fin x → α) → Sort u_1) (x : Fin 0 → α) (h_1 : (x : Fin 0 → α) → motive 0 x)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → α) → motive n.succ f),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, f => h_2 n f) =
    h_1 x
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.erase_def : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (x : Polynomial R),
  Polynomial.erase n x =
    match x with
    | { toFinsupp := p } => { toFinsupp := AddMonoidAlgebra.erase n p }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : k ∈ t), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.Topology.Order.OrderClosed
Ico_mem_nhdsGE_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b c : α},
  b ∈ Set.Ico c a → Set.Ico c a ∈ nhdsWithin b (Set.Ici b)
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.wordProd.eq_1 : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B),
  cs.wordProd ω = (List.map cs.simple ω).prod
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_eq : ∀ {n : ℕ} {i : Fin n} [NeZero n], i.cycleIcc i = 1
-- Mathlib.CategoryTheory.Opposites
/-- If `f` is an isomorphism, so is `f.op`  -/
CategoryTheory.isIso_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.op
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- This is a definition because it will be helpful to be able to control precisely when this
definition is unfolded.  -/
CategoryTheory.OverPresheafAux.YonedaCollection.yonedaEquivFst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} →
        {X : C} → CategoryTheory.OverPresheafAux.YonedaCollection F X → A.obj (Opposite.op X)
-- Batteries.Data.AssocList
Batteries.AssocList.foldlM.eq_2 : ∀ {m : Type u_1 → Type u_2} {δ : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : δ → α → β → m δ) (x : δ)
  (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.foldlM f x (Batteries.AssocList.cons a b es) = do
    let __do_lift ← f x a b
    Batteries.AssocList.foldlM f __do_lift es
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 ω₁ s x →
      DifferentiableWithinAt 𝕜 ω₂ s x → extDerivWithin (ω₁ + ω₂) s x = extDerivWithin ω₁ s x + extDerivWithin ω₂ s x
-- Mathlib.Tactic.ApplyFun
/-- Apply a function to the main goal.  -/
Mathlib.Tactic.applyFunTarget : Lean.Term → Option Lean.Term → Lean.MVarId → Lean.Elab.Tactic.TacticM (List Lean.MVarId)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.instFiniteSubtypeMemBot : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], Module.Finite F ↥⊥
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnits_sSup : ∀ {M : Type u_1} [inst : Monoid M] (s : Set (Subgroup Mˣ)), (sSup s).ofUnits = ⨆ S ∈ s, S.ofUnits
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
IsMIntegralCurveOn.continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ}, IsMIntegralCurveOn γ v s → ContinuousOn γ s
-- Mathlib.Algebra.Group.Defs
/-- A `Monoid` which `IsMulCommutative` is a `CommMonoid`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instCommMonoid : {M : Type u_2} → [inst : Monoid M] → [IsMulCommutative M] → CommMonoid M
-- Mathlib.Analysis.Convex.Function
ConcaveOn.left_lt_of_lt_right' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f →
    ∀ {x y : E},
      x ∈ s → y ∈ s → ∀ {a b : 𝕜}, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) < f y → f x < f (a • x + b • y)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.toSpecΓ_unop : ∀ (R : CommRingCatᵒᵖ),
  AlgebraicGeometry.toSpecΓ (Opposite.unop R) =
    CommRingCat.ofHom
      (algebraMap (↑R.1)
        ((AlgebraicGeometry.structureSheafInType ↑(Opposite.unop (Opposite.op (Opposite.unop R)))
                ↑(Opposite.unop (Opposite.op (Opposite.unop R)))).obj.obj
          (Opposite.op ⊤)))
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.presieve₀_mem_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} [J.RespectsIso] {S : C}
  {E : J.ZeroHypercover S} {F : CategoryTheory.PreZeroHypercover S} (e : E.toPreZeroHypercover ≅ F),
  F.presieve₀ ∈ J.coverings S
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.of_algebraMap_eq : ∀ {R : Type u} {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A],
  (∀ (x : R), (algebraMap R A) x = (algebraMap S A) ((algebraMap R S) x)) → IsScalarTower R S A
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveHypothesisBundle.type : Lean.Widget.InteractiveHypothesisBundle → Lean.Widget.CodeWithInfos
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.smul_cancel : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : MulAction R X] {r : X} {s t : ↥S}, (↑s /ₒ t) • (r /ₒ s) = r /ₒ t
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.mem_pi : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)] (I : Set ι) {S : (i : ι) → AddSubmonoid (M i)}
  {p : (i : ι) → M i}, p ∈ AddSubmonoid.pi I S ↔ ∀ i ∈ I, p i ∈ S i
-- Mathlib.MeasureTheory.Function.EssSup
essSup_measure_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] {m : MeasurableSpace α} {f : α → β}, essSup f 0 = ⊥
-- Init.Data.Int.LemmasAux
Int.max_min_distrib_right : ∀ (a b c : ℤ), max (min a b) c = min (max a c) (max b c)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.exists_mem_ne_zero_of_ne_bot : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p : Submodule R M}, p ≠ ⊥ → ∃ b ∈ p, b ≠ 0
-- Mathlib.Data.Num.Basic
/-- Ordering of `Num`s.  -/
Num.cmp : Num → Num → Ordering
-- Mathlib.Algebra.Category.Grp.Basic
/-- The type of morphisms in `AddGrpCat R`.  -/
AddGrpCat.Hom : AddGrpCat → AddGrpCat → Type u
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.isoRightDerivedObj_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ) {Z : D} (h : (F.rightDerived n).obj Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).inv
          (CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) h) =
        CategoryTheory.CategoryStruct.comp
          ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).map
            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ))
          (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedObj F n).inv h)
-- Init.Data.Vector.Lemmas
Vector.contains.eq_1 : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] (xs : Vector α n) (a : α), xs.contains a = xs.toArray.contains a
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
/-- A ring homomorphism between local rings is a local ring hom iff it reflects units,
i.e. any preimage of a unit is still a unit.  -/
IsLocalRing.local_hom_TFAE : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : IsLocalRing R] [inst_2 : CommSemiring S]
  [inst_3 : IsLocalRing S] (f : R →+* S),
  [IsLocalHom f, ⇑f '' ↑(IsLocalRing.maximalIdeal R) ⊆ ↑(IsLocalRing.maximalIdeal S),
      Ideal.map f (IsLocalRing.maximalIdeal R) ≤ IsLocalRing.maximalIdeal S,
      IsLocalRing.maximalIdeal R ≤ Ideal.comap f (IsLocalRing.maximalIdeal S),
      Ideal.comap f (IsLocalRing.maximalIdeal S) = IsLocalRing.maximalIdeal R].TFAE
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.checkCol0Fn : String → Lean.Parser.ParserFn
-- Mathlib.Data.Countable.Defs
Equiv.uncountable_iff : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Uncountable α ↔ Uncountable β
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportKind.mk.sizeOf_spec : ∀ (isPrivate isAll : Bool) (metaKind : Lean.Lsp.LeanImportMetaKind),
  sizeOf { isPrivate := isPrivate, isAll := isAll, metaKind := metaKind } =
    1 + sizeOf isPrivate + sizeOf isAll + sizeOf metaKind
-- Mathlib.Data.Complex.Basic
Complex.im_nsmul : ∀ (n : ℕ) (z : ℂ), (n • z).im = n • z.im
-- Mathlib.Topology.PartitionOfUnity
BumpCovering.coe_single : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] (i : ι) (s : Set X), ⇑(BumpCovering.single i s) = Pi.single i 1
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
FirstOrder.Language.presburger.isSemilinearSet_formula_realize_semilinear : ∀ {α : Type u_1} {A : Set ℕ} [Finite α] (φ : (FirstOrder.Language.presburger.withConstants ↑A).Formula α),
  IsSemilinearSet (Set.ofPred φ.Realize)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_hom_snd_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- If `f` belongs to `lpMeasSubgroup F m p μ`, then the measurable function it is almost
everywhere equal to (given by `AEMeasurable.mk`) belongs to `ℒp` for the measure `μ.trim hm`.  -/
MeasureTheory.memLp_trim_of_mem_lpMeasSubgroup : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp F p μ))
  (hf_meas : f ∈ MeasureTheory.lpMeasSubgroup F m p μ), MeasureTheory.MemLp (Exists.choose ⋯) p (μ.trim hm)
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.zsmul_sub : ∀ {M : Type u} [inst : Lean.Grind.IntModule M] (k : ℤ) (a b : M), k • (a - b) = k • a - k • b
-- Mathlib.Topology.Closure
interior_maximal : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, t ⊆ s → IsOpen t → t ⊆ interior s
-- Std.Http.Internal.Char
/-- Checks if a character is ASCII (Unicode code point < 128).
 -/
Std.Http.Internal.Char.isAscii : Char → Bool
-- Mathlib.Combinatorics.Enumerative.Composition
/-- List of the sizes of the blocks in a `CompositionAsSet`.  -/
CompositionAsSet.blocks : {n : ℕ} → CompositionAsSet n → List ℕ
-- Mathlib.Data.Sum.Lattice
Sum.Lex.inl_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (a₁ a₂ : α),
  Sum.inlₗ (a₁ ⊓ a₂) = Sum.inlₗ a₁ ⊓ Sum.inlₗ a₂
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- `setToL1S` does not change if we replace the measure `μ` by `μ'` with `μ ≪ μ'`. The statement
uses two functions `f` and `f'` because they have to belong to different types, but morally these
are the same function (we have `f =ᵐ[μ] f'`).  -/
MeasureTheory.L1.SimpleFunc.setToL1S_congr_measure : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ μ' : MeasureTheory.Measure α}
  (T : Set α → E →L[ℝ] F),
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      μ.AbsolutelyContinuous μ' →
        ∀ (f : ↥(α →₁ₛ[μ] E)) (f' : ↥(α →₁ₛ[μ'] E)),
          ↑↑↑f =ᵐ[μ] ↑↑↑f' → MeasureTheory.L1.SimpleFunc.setToL1S T f = MeasureTheory.L1.SimpleFunc.setToL1S T f'
-- Mathlib.Data.Prod.Basic
Prod.mk_right_inj : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β}, (a, b₁) = (a, b₂) ↔ b₁ = b₂
-- Init.Data.BitVec.Lemmas
BitVec.getElem_shiftConcat : ∀ {w i : ℕ} {x : BitVec w} {b : Bool} (h : i < w), (x.shiftConcat b)[i] = if i = 0 then b else x[i - 1]
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.isStrictlySupported_of_iso : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (e' : K ≅ L) (e : c.Embedding c') [K.IsStrictlySupported e], L.IsStrictlySupported e
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.isNormalEpiCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.IsNormalEpiCategory D