mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.prodEquiv.eq_1 : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (A : Subgroup G) (B : Subgroup H),
  QuotientGroup.prodEquiv A B =
    {
      toFun := fun q =>
        Quotient.liftOn' q
          (fun x =>
            match x with
            | (g, h) => (↑g, ↑h))
          ⋯,
      invFun := fun q => Quotient.liftOn₂' q.1 q.2 (fun g h => ↑(g, h)) ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.BitVec.Lemmas
BitVec.neg_mul : ∀ {w : ℕ} (x y : BitVec w), -x * y = -(x * y)
-- Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit
_private.Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit.0.CategoryTheory.coherentTopology.preimageStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preregular C] →
      [inst_2 : CategoryTheory.FinitaryExtensive C] →
        {F : CategoryTheory.Functor ℕᵒᵖ (CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) (Type v))} →
          (∀ (n : ℕ), CategoryTheory.Sheaf.IsLocallySurjective (F.map (CategoryTheory.homOfLE ⋯).op)) →
            (X : C) → (F.obj (Opposite.op 0)).obj.obj (Opposite.op X) → CategoryTheory.coherentTopology.struct✝ F
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.mk : {M : Type u_10} →
  {N : Type u_11} →
    [inst : AddZero M] →
      [inst_1 : AddZero N] →
        (toZeroHom : ZeroHom M N) →
          (∀ (x y : M), toZeroHom.toFun (x + y) = toZeroHom.toFun x + toZeroHom.toFun y) → M →+ N
-- Mathlib.Algebra.Group.Pi.Units
AddEquiv.val_piAddUnits_apply : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → AddMonoid (M i)] (f : AddUnits ((i : ι) → M i)) (i : ι),
  ↑(AddEquiv.piAddUnits f i) = ↑f i
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given a function, there is a contravariant induced map on graphs by pulling back the
adjacency relation.
This is one of the ways of creating induced graphs. See `SimpleGraph.induce` for a wrapper.

This is surjective when `f` is injective (see `SimpleGraph.comap_surjective`).  -/
SimpleGraph.comap : {V : Type u_1} → {W : Type u_2} → (V → W) → SimpleGraph W → SimpleGraph V
-- Mathlib.Topology.UniformSpace.Basic
instIsCountablyGeneratedProdUniformity : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [(uniformity α).IsCountablyGenerated] [inst_2 : UniformSpace β]
  [(uniformity β).IsCountablyGenerated], (uniformity (α × β)).IsCountablyGenerated
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.map_extend_symm_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {y : M},
  y ∈ f.source →
    Filter.map (↑(f.extend I).symm) (nhdsWithin (↑(f.extend I) y) (↑(f.extend I).symm ⁻¹' s ∩ Set.range ↑I)) =
      nhdsWithin y s
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.eq_loopyOn_iff_loops_eq : ∀ {α : Type u_1} {M : Matroid α} {E : Set α}, M = Matroid.loopyOn E ↔ M.loops = E ∧ M.E = E
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instIsZeroApply : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, IsZeroApply (TestFunction Ω F n) E F
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.partialOrder : {α : Type u_1} →
  {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [PartialOrder β] → PartialOrder C(α, β)
-- Mathlib.Order.Interval.Finset.Defs
/-- Left-closed right-infinite interval  -/
LocallyFiniteOrderTop.finsetIci : {α : Type u_1} → {inst : Preorder α} → [self : LocallyFiniteOrderTop α] → α → Finset α
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.NonnegCoeffs.below.add : ∀ {motive : (a : Lean.Grind.Linarith.Poly) → a.NonnegCoeffs → Prop} (a : ℤ) (x : Lean.Grind.Linarith.Var)
  (p : Lean.Grind.Linarith.Poly) (a_1 : a ≥ 0) (a_2 : p.NonnegCoeffs),
  Lean.Grind.Linarith.Poly.NonnegCoeffs.below a_2 → motive p a_2 → Lean.Grind.Linarith.Poly.NonnegCoeffs.below ⋯
-- Mathlib.Order.SymmDiff
bihimp.eq_1 : ∀ {α : Type u_2} [inst : Min α] [inst_1 : HImp α] (a b : α), bihimp a b = (b ⇨ a) ⊓ (a ⇨ b)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList_done : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Zipper.done.toList = []
-- Lean.Elab.Tactic.Omega.Core
/-- The facts which give a lower bound on the target variable,
and the coefficient of the target variable in each.
 -/
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.lowerBounds : Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData → List (Lean.Elab.Tactic.Omega.Fact × ℤ)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The trifunctor `X₁ X₂ X₃ ↦ (X₂ ⊗ X₃) ⊗ X₁`  -/
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C C))
-- Lean.Server.References
/-- Transient reference information from a file worker.
We track this information so that we have up-to-date reference information before a file has been
built.
 -/
Lean.Server.TransientWorkerILean : Type
-- Init.Data.Fin.Lemmas
Fin.succ_pred : ∀ {n : ℕ} (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_const_sub_nhds_zero_iff : ∀ {α : Type u_1} {l : Filter α} {f : α → ENNReal} {a : ENNReal},
  a ≠ ⊤ →
    (∀ (n : α), f n ≤ a) → (Filter.Tendsto (fun n => a - f n) l (nhds 0) ↔ Filter.Tendsto (fun n => f n) l (nhds a))
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
/-- If `2` is invertible in the coefficient ring,
the radical of a quadratic map is the kernel of its associated bilinear map.  -/
QuadraticMap.radical_eq_ker_associated : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P} [inst_5 : Invertible 2],
  Q.radical = LinearMap.ker (QuadraticMap.associated Q)
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.pos.inj : ∀ {a a_1 : ℕ}, Sat.Literal.pos a = Sat.Literal.pos a_1 → a = a_1
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_union_eq_left_of_ae_aux : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s t : Set X} {μ : MeasureTheory.Measure X},
  (∀ᵐ (x : X) ∂μ.restrict t, f x = 0) →
    MeasureTheory.StronglyMeasurable f →
      MeasureTheory.IntegrableOn f (s ∪ t) μ → ∫ (x : X) in s ∪ t, f x ∂μ = ∫ (x : X) in s, f x ∂μ
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.comp_evaluation : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) (b : B),
  F.comp ((CategoryTheory.evaluation B C).obj b) = F.flip.obj b
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.ker_rootForm_eq_dualAnnihilator : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], LinearMap.ker P.RootForm = Submodule.map (↑P.toPerfPair.symm) (P.corootSpan R).dualAnnihilator
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- additive equivalences between `AddSemigroup`s are
the same as (isomorphic to) isomorphisms in `AddSemigroup`  -/
addEquivIsoAddSemigrpIso : {X Y : Type u} → [inst : AddSemigroup X] → [inst_1 : AddSemigroup Y] → X ≃+ Y ≅ AddSemigrp.of X ≅ AddSemigrp.of Y
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.add : ∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] {A B : Matrix n n α},
  A.IsHermitian → B.IsHermitian → (A + B).IsHermitian
-- Lean.Data.Name
/-- Return true if the name is in a namespace associated to metaprogramming.  -/
Lean.Name.isMetaprogramming : Lean.Name → Bool
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
/-- Turn a function `f : α → ℚ → ℝ` into another with the property `IsRatStieltjesPoint f a`
everywhere. At `a` that does not satisfy that property, `f a` is replaced by an arbitrary suitable
function.
Mainly useful when `f` satisfies the property `IsRatStieltjesPoint f a` almost everywhere with
respect to some measure.  -/
ProbabilityTheory.toRatCDF : {α : Type u_1} → (α → ℚ → ℝ) → α → ℚ → ℝ
-- Mathlib.NumberTheory.SumFourSquares
_private.Mathlib.NumberTheory.SumFourSquares.0.Nat.sum_four_squares_of_two_mul_sum_four_squares : ∀ {m a b c d : ℤ}, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m → ∃ w x y z, w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = m
-- Init.Core
/-- The quotient of `α` by the universal relation. The elements of `Squash α` are those of `α`, but all
of them are equal and cannot be distinguished.

`Squash α` is a `Subsingleton`: it is empty if `α` is empty, otherwise it has just one element. It
is the “universal `Subsingleton`” mapped from `α`.

`Nonempty α` also has these properties. It is a proposition, which means that its elements (i.e.
proofs) are erased from compiled code and represented by a dummy value. `Squash α` is a `Type u`,
and its representation in compiled code is identical to that of `α`.

Consequently, `Squash.lift` may extract an `α` value into any subsingleton type `β`, while
`Nonempty.rec` can only do the same when `β` is a proposition.

`Squash` is defined in terms of `Quotient`, so `Squash` can be used when a `Quotient` argument is
expected.
 -/
Squash : Sort u → Sort u
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- The Galois group of a polynomial.  -/
Polynomial.Gal : {F : Type u_1} → [inst : Field F] → Polynomial F → Type u_1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : m[a]?.isSome = true}, m[a]?.get h = m[a]
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_minKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.getKey! t.minKey! = t.minKey!
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- Range of a simple function `α →ₛ β` as a `Finset β`.  -/
MeasureTheory.SimpleFunc.range : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → MeasureTheory.SimpleFunc α β → Finset β
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.FG.of_restrictScalars : ∀ {A : Type u_5} {M : Type u_6} [inst : Semiring A] [inst_1 : AddCommMonoid M] [inst_2 : Module A M] {S : Submodule A M}
  (R : Type u_7) [inst_3 : Semiring R] [inst_4 : Module R M] [inst_5 : SMul R A] [inst_6 : IsScalarTower R A M],
  (Submodule.restrictScalars R S).FG → S.FG
-- Init.Data.List.Nat.Count
List.IsSuffix.le_countP : ∀ {α : Type u_1} {l₁ l₂ : List α} {p : α → Bool},
  l₁ <:+ l₂ → List.countP p l₂ - (l₂.length - l₁.length) ≤ List.countP p l₁
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- Build an isomorphism in the category `QuadraticModuleCat R` from a
`QuadraticForm.IsometryEquiv`.  -/
QuadraticModuleCat.ofIso : {R : Type u} →
  [inst : CommRing R] →
    {X Y : Type v} →
      [inst_1 : AddCommGroup X] →
        [inst_2 : Module R X] →
          [inst_3 : AddCommGroup Y] →
            [inst_4 : Module R Y] →
              {Q₁ : QuadraticForm R X} →
                {Q₂ : QuadraticForm R Y} →
                  QuadraticMap.IsometryEquiv Q₁ Q₂ → (QuadraticModuleCat.of Q₁ ≅ QuadraticModuleCat.of Q₂)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.ofFreeAddGroup_apply : ∀ {X : Type u_5} (x : X), (FreeAddGroupBasis.ofFreeAddGroup X) x = FreeAddGroup.of x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.hasEqualizer_comp_mono : ∀ (C : Type u) {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [CategoryTheory.Limits.HasEqualizer f g] {Z : C} (h : Y ⟶ Z) [CategoryTheory.Mono h],
  CategoryTheory.Limits.HasEqualizer (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Order.Category.Preord
Preord.of.inj : ∀ {carrier : Type u_1} {str : Preorder carrier} {carrier_1 : Type u_1} {str_1 : Preorder carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.finset_inf' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {t : Set X} {x : X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousWithinAt (f i) t x) → ContinuousWithinAt (s.inf' hne f) t x
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.mono_of_mem_nhdsWithin : ∀ {𝕜 : 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 : M → M'} {s t : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → s ∈ nhdsWithin x t → ContMDiffWithinAt I I' n f t x
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.unrev.eq_1 : Turing.PartrecToTM2.unrev =
  Turing.PartrecToTM2.Λ'.move (fun x => false) Turing.PartrecToTM2.K'.rev Turing.PartrecToTM2.K'.main
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzWith_neg_iff`. -/
LipschitzWith.of_neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal}
  {f : α → E}, LipschitzWith K (-f) → LipschitzWith K f
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_eq_ediv_of_nonneg : ∀ {a b : ℤ}, 0 ≤ a → a.tdiv b = a / b
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldrM.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : (a : α) → β a → δ → m δ)
  (x : δ), Std.DHashMap.Internal.AssocList.foldrM f x Std.DHashMap.Internal.AssocList.nil = pure x
-- Init.Data.Fin.Basic
Fin.ne_of_val_ne : ∀ {n : ℕ} {i j : Fin n}, ↑i ≠ ↑j → i ≠ j
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The second morphism of the factorisation.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.π : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            (n : ℤ) → CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.mid✝ f n ⟶ L
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- The cokernel sequence of the monomorphism `K.ιTruncLE n`.  -/
CochainComplex.shortComplexTruncLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CochainComplex C ℤ → ℤ → CategoryTheory.ShortComplex (CochainComplex C ℤ)
-- Mathlib.Algebra.Order.Group.Int
Int.instIsOrderedAddMonoid : IsOrderedAddMonoid ℤ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_insert_perm : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : BEq α]
  [Std.TransOrd α] [Std.LawfulBEqOrd α] (h : t.WF) {k : α} {v : β},
  (Std.DTreeMap.Internal.Impl.Const.toList (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl).Perm
    ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) (Std.DTreeMap.Internal.Impl.Const.toList t))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.flip_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g), t.flip.snd = t.fst
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.isCaratheodory_compl_iff : ∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α}, m.IsCaratheodory sᶜ ↔ m.IsCaratheodory s
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.iso_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasInjectiveResolutions C] {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) →
    ∀ {Z : HomotopyCategory C (ComplexShape.up ℕ)} (h : (CategoryTheory.injectiveResolutions C).obj Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp I.iso.inv
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.injectiveResolutions C).map f) h) =
        CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient C (ComplexShape.up ℕ)).map φ)
          (CategoryTheory.CategoryStruct.comp J.iso.inv h)
-- Mathlib.Algebra.Group.Defs
/-- A semigroup is a type with an associative `(*)`.  -/
Semigroup : Type u → Type u
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.setTag : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Lean.Compiler.LCNF.Code pu →
        autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_13 → Lean.Compiler.LCNF.Code pu
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.le_one_iff : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v w : AbsoluteValue R S} [IsDomain S] [Nontrivial R], v.IsEquiv w → ∀ {x : R}, v x ≤ 1 ↔ w x ≤ 1
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haarMeasure_closure_self : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G},
  (MeasureTheory.Measure.haarMeasure K₀) (closure ↑K₀) = 1
-- Lean.Meta.Match.Match
/-- Used alternatives  -/
Lean.Meta.Match.State.used : Lean.Meta.Match.State → Std.HashSet ℕ
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
/-- By iterating `φ` to the power `j : κ₁.ord.ToType` and evaluating
on `A`, we get a subset that is of cardinality `< κ₂`.  -/
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.hasCardinalLT_transfiniteIterate_φ : ∀ {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular],
  κ₁ < κ₂ →
    ∀ {X : Type w}
      (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)),
      (∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), HasCardinalLT (↑(Y B hB)) κ₂) →
        ∀
          (m :
            (B : Set X) →
              (hB : HasCardinalLT (↑B) κ₂) →
                (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X)
          (A : Set X),
          HasCardinalLT (↑A) κ₂ →
            ∀ (j : κ₁.ord.ToType),
              HasCardinalLT
                (↑(transfiniteIterate (Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.φ✝ Y m) j A)) κ₂
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.instCoverOfIsAffineOfFiniteI₀ : ∀ {S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine S]
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.AffineCover P S)
  [Finite 𝒰.I₀], AlgebraicGeometry.QuasiCompactCover 𝒰.cover.toPreZeroHypercover
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.id_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y), (CategoryTheory.Monad.id C).map f = f
-- Mathlib.Probability.Process.Adapted
MeasureTheory.stronglyAdapted_iff_adapted : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → TopologicalSpace (β i)] {u : (i : ι) → Ω → β i}
  [mΒ : (i : ι) → MeasurableSpace (β i)] [∀ (i : ι), BorelSpace (β i)]
  [∀ (i : ι), TopologicalSpace.PseudoMetrizableSpace (β i)] [∀ (i : ι), SecondCountableTopology (β i)],
  MeasureTheory.StronglyAdapted f u ↔ MeasureTheory.Adapted f u
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.closedCell_zero_injective`. -/
Topology.CWComplex.closedCell_zero_injective : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D],
  Function.Injective (Topology.RelCWComplex.closedCell 0)
-- Init.Data.Int.DivMod.Lemmas
Int.emod_eq_tmod : ∀ {a b : ℤ}, a % b = a.tmod b + ↑(if 0 ≤ a ∨ b ∣ a then 0 else b.natAbs)
-- Init.Omega.Constraint
/-- A upper bound at `y` is satisfied at `t` if `t ≤ y`.  -/
Lean.Omega.UpperBound.sat : Lean.Omega.UpperBound → ℤ → Bool
-- Lean.Util.CollectMVars
Lean.CollectMVars.State.visitedExpr : Lean.CollectMVars.State → Lean.ExprSet
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.gcorec_nil : ∀ {β : Type u_1} {γ : Type u_2} {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {F : β → Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl × γ × β)}
  {op :
    γ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  [inst : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op] {b : β},
  F b = none →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.gcorec F op b =
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKeyD_le_maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {k : α} {v : β k} {fallback : α}, (cmp (t.maxKeyD fallback) ((t.insert k v).maxKeyD fallback)).isLE = true
-- Mathlib.Order.UpperLower.Closure
IsUpperSet.disjoint_lowerClosure_right : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsUpperSet s → (Disjoint s ↑(lowerClosure t) ↔ Disjoint s t)
-- Mathlib.MeasureTheory.MeasurableSpace.Pi
/-- The product σ-algebra is generated from boxes, i.e. `s ×ˢ t` for sets `s : set α` and
`t : set β`.  -/
generateFrom_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [inst : (i : ι) → MeasurableSpace (α i)],
  MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi fun i => {s | MeasurableSet s}) = MeasurableSpace.pi
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algEquivOfAssociated_toAlgHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hfg : Associated f g), ↑(AdjoinRoot.algEquivOfAssociated R f g hfg) = AdjoinRoot.algHomOfDvd R f g ⋯
-- Mathlib.RingTheory.Polynomial.Quotient
/-- For a commutative ring $R$, evaluating a polynomial at an element $x \in R$ induces an
isomorphism of $R$-algebras $R[X] / \langle X - x \rangle \cong R$.  -/
Polynomial.quotientSpanXSubCAlgEquiv : {R : Type u_1} → [inst : CommRing R] → (x : R) → (Polynomial R ⧸ Ideal.span {Polynomial.X - Polynomial.C x}) ≃ₐ[R] R
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.ext : ∀ {X : Type u_1} {R : Type u_2} {inst : Zero R} {inst_1 : Add R} {inst_2 : LE R} {x y : PseudoMetric X R},
  x.toFun = y.toFun → x = y
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.syntaxInt : ℤ → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.sInf_neg : ∀ (s : Set ℝ), sInf (-s) = -sSup s