mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.comp_id : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b} (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.swapCompInl_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : C), (CategoryTheory.Sum.swapCompInl C D).inv.app X = CategoryTheory.CategoryStruct.id (Sum.inr X)
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.insert : Lean.Meta.MVarRenaming → Lean.MVarId → Lean.MVarId → Lean.Meta.MVarRenaming
-- Init.Prelude
Nat.le_of_lt_succ : ∀ {m n : ℕ}, m < n.succ → m ≤ n
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.eval₂Hom_bind₂ : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (f : S →+* T) (g : σ → T) (h : R →+* MvPolynomial σ S) (φ : MvPolynomial σ R),
  (MvPolynomial.eval₂Hom f g) ((MvPolynomial.bind₂ h) φ) =
    (MvPolynomial.eval₂Hom ((MvPolynomial.eval₂Hom f g).comp h) g) φ
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.map_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat}
  (S : CategoryTheory.SubmonoidFunctor M) {U V : C} (f : U ⟶ V),
  Submonoid.map (MonCat.Hom.hom (M.map f)) (S.obj U) ≤ S.obj V
-- Mathlib.RingTheory.Localization.Module
/-- If `M` has an `R`-basis, then localizing `M` at `S` has a basis over `R` localized at `S`.  -/
Module.Basis.ofIsLocalizedModule : {R : Type u_1} →
  (Rₛ : Type u_2) →
    [inst : CommSemiring R] →
      (S : Submonoid R) →
        [inst_1 : CommSemiring Rₛ] →
          [inst_2 : Algebra R Rₛ] →
            [IsLocalization S Rₛ] →
              {M : Type u_3} →
                {Mₛ : Type u_4} →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] →
                      [inst_6 : AddCommMonoid Mₛ] →
                        [inst_7 : Module R Mₛ] →
                          [inst_8 : Module Rₛ Mₛ] →
                            [IsScalarTower R Rₛ Mₛ] →
                              (f : M →ₗ[R] Mₛ) →
                                [IsLocalizedModule S f] → {ι : Type u_5} → Module.Basis ι R M → Module.Basis ι Rₛ Mₛ
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_transpose : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α)
  (C : Matrix o l α) (D : Matrix o m α),
  (Matrix.fromBlocks A B C D).transpose = Matrix.fromBlocks A.transpose C.transpose B.transpose D.transpose
-- Mathlib.Logic.OpClass
instLeftCommutativeOfRightCommutative : ∀ {α : Sort u} {β : Sort v} {f : β → α → β} [h : RightCommutative f], LeftCommutative fun x y => f y x
-- Mathlib.Data.Set.Prod
/-- **Vertical line test** for functions.

Let `s : Set (β × γ)` be a set in a product. Assume that `s` maps bijectively to the first factor.
Then `s` is the graph of some function `f : β → γ`.  -/
Set.exists_eq_mgraphOn_univ : ∀ {β : Type u_2} {γ : Type u_3} {s : Set (β × γ)},
  Function.Bijective (Prod.fst ∘ Subtype.val) → ∃ f, s = Set.graphOn f Set.univ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_whiskerRight : ∀ {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 : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] {X Y : C} (f : X ⟶ Y) (Z : C),
  F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Z))
        (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
-- Mathlib.CategoryTheory.Limits.Cones
/-- An object of `C`  -/
CategoryTheory.Limits.Cone.pt : {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 → C
-- Lean.Data.JsonRpc
/-- A non-successful response.  -/
Lean.JsonRpc.Message.responseError : Lean.JsonRpc.RequestID → Lean.JsonRpc.ErrorCode → String → Option Lean.Json → Lean.JsonRpc.Message
-- Mathlib.RingTheory.Congruence.Hom
/-- The kernel of a ring homomorphism as a ring congruence relation.  -/
RingCon.ker : {M : Type u_1} → {N : Type u_2} → [inst : NonAssocSemiring M] → [inst_1 : NonAssocSemiring N] → (M →+* N) → RingCon M
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.isContained_iff_exists_le_comap : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W},
  H.IsContained G ↔ ∃ f, H ≤ SimpleGraph.comap (⇑f) G
-- Mathlib.SetTheory.Cardinal.Finite
/-- `ENat.card α` is the cardinality of `α` as an extended natural number.
If `α` is infinite, `ENat.card α = ⊤`.  -/
ENat.card : Type u_3 → ℕ∞
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- Given two left-invariant measures which are finite on
compacts, they coincide in the following sense: they give the same value to the integral of
continuous compactly supported functions, up to a multiplicative constant.  -/
MeasureTheory.Measure.exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [BorelSpace G] (μ' μ : MeasureTheory.Measure G) [μ.IsHaarMeasure] [MeasureTheory.IsFiniteMeasureOnCompacts μ']
  [μ'.IsMulLeftInvariant],
  ∃ c, ∀ (f : G → ℝ), Continuous f → HasCompactSupport f → ∫ (x : G), f x ∂μ' = ∫ (x : G), f x ∂c • μ
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {H K : AddSubgroup G} (hHK : H ≤ K) (g : ↥H),
  (AddSubgroup.addSubgroupOfContinuousAddEquivOfLe hHK).symm g = ⟨⟨↑g, ⋯⟩, ⋯⟩
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instSMulCommClass : ∀ {k : Type u_1} {G : Type u_2} {S₁ : Type u_4} {S₂ : Type u_5} [inst : AddMonoid k] [inst_1 : SMulZeroClass S₁ k]
  [inst_2 : SMulZeroClass S₂ k] [SMulCommClass S₁ S₂ k], SMulCommClass S₁ S₂ (SkewMonoidAlgebra k G)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.isoRightDerivedObj_hom_naturality : ∀ {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 : ℕ),
      CategoryTheory.CategoryStruct.comp ((F.rightDerived n).map f) (J.isoRightDerivedObj F n).hom =
        CategoryTheory.CategoryStruct.comp (I.isoRightDerivedObj F n).hom
          (((F.mapHomologicalComplex (ComplexShape.up ℕ)).comp
                (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n)).map
            φ)
-- Mathlib.MeasureTheory.Group.AEStabilizer
/-- A.e. stabilizer of a set under an additive group action.  -/
AddAction.aestabilizer : (G : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G α] →
        {x : MeasurableSpace α} →
          (μ : MeasureTheory.Measure α) → [MeasureTheory.VAddInvariantMeasure G α μ] → Set α → AddSubgroup G
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mapIsoToOrderIso_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) (a : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.mapIsoToOrderIso e) a = (CategoryTheory.Subobject.map e.hom).obj a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.equiv_empty_iff_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.Equiv Std.TreeSet.Raw.empty ↔ t.isEmpty = true
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : OrderTop α] [Nontrivial α] (a : α),
  Order.pred a < ⊤
-- Mathlib.Tactic.IrreducibleDef
/-- Introduces an irreducible definition.
`irreducible_def foo := 42` generates
a constant `foo : Nat` as well as
a theorem `foo_def : foo = 42`.
 -/
Lean.Elab.Command.command_Irreducible_def____ : Lean.ParserDescr
-- Mathlib.Computability.MyhillNerode
Language.mem_accept_toDFA : ∀ {α : Type u} {L : Language α} (s : ↑(Set.range L.leftQuotient)), s ∈ L.toDFA.accept ↔ [] ∈ ↑s
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.isOrderedAddMonoid : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddCommGroup (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedAddMonoid (α i)],
  IsOrderedAddMonoid (Colex (Π₀ (i : ι), α i))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k fallback : α},
  (Std.ExtHashMap.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x_2 h' => f x_2 m[x_2]).getD fallback
-- Mathlib.Data.WSeq.Defs
/-- Get the first element of `s` satisfying `p`.  -/
Stream'.WSeq.find : {α : Type u} → (p : α → Prop) → [DecidablePred p] → Stream'.WSeq α → Computation (Option α)
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_castSucc_self : ∀ {n : ℕ} (j : Fin n), j.castSucc.succAbove j = j.succ
-- Mathlib.Topology.Algebra.ConstMulAction
Continuous.const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] {g : β → α}, Continuous g → ∀ (c : M), Continuous (c • g)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_zero_one : ∀ {R : Type u_1} [inst : Semiring R], (PowerSeries.coeff 0) 1 = 1
-- Mathlib.RingTheory.AdjoinRoot
/-- The natural isomorphism `(R/I)[x]/(f mod I) ≅ (R[x]/I*R[x])/(f mod I[x])` where
`f : R[X]` and `I : Ideal R`  -/
AdjoinRoot.Polynomial.quotQuotEquivComm : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (f : Polynomial R) →
        Polynomial (R ⧸ I) ⧸ Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f} ≃+*
          (Polynomial R ⧸ Ideal.map Polynomial.C I) ⧸ Ideal.span {(Ideal.Quotient.mk (Ideal.map Polynomial.C I)) f}
-- Init.Tactics
/-- `trace_state` displays the current state in the info view.  -/
Lean.Parser.Tactic.traceState : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_inter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β},
      Std.DTreeMap.Internal.Impl.Const.getD (m₁.inter m₂ ⋯) k fallback =
        if Std.DTreeMap.Internal.Impl.contains k m₂ = true then Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
        else fallback
-- Mathlib.Data.Nat.Dist
Nat.dist_eq_sub_of_le_right : ∀ {n m : ℕ}, m ≤ n → n.dist m = n - m
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_comp_subst_apply : ∀ {R : Type u_2} [inst : CommRing R] {S : Type u_4} [inst_1 : CommRing S] {υ : Type u_5} {T : Type u_6}
  [inst_2 : CommRing T] [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] {a : PowerSeries S}
  {b : MvPowerSeries υ T} [IsScalarTower R S T],
  PowerSeries.HasSubst a →
    PowerSeries.HasSubst b →
      ∀ (f : PowerSeries R), PowerSeries.subst b (PowerSeries.subst a f) = PowerSeries.subst (PowerSeries.subst b a) f
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- Two linear maps on `⋀[R]^n M` that agree on the image of `exteriorPower.ιMulti`
are equal.  -/
exteriorPower.linearMap_ext : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f g : ↥(⋀[R]^n M) →ₗ[R] N},
  f.compAlternatingMap (exteriorPower.ιMulti R n) = g.compAlternatingMap (exteriorPower.ιMulti R n) → f = g
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `FunLike.coeAddMonoidHom_apply`. -/
MeasureTheory.VectorMeasure.coeFnAddMonoidHom_apply : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β] (f : F), (FunLike.coeAddMonoidHom F α β) f = ⇑f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) k).isLE = true
-- Init.Data.String.Basic
ByteArray.isValidUTF8_utf8Encode_singleton_append_iff : ∀ {b : ByteArray} {c : Char}, ([c].utf8Encode ++ b).IsValidUTF8 ↔ b.IsValidUTF8
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNatCast : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [NatCast β] → NatCast (MeasureTheory.SimpleFunc α β)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIci_self : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α), Set.projIci a a = ⟨a, ⋯⟩
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.assignOutParams : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] (f : FrameHom β γ) (g : FrameHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.homOfPath.eq_1 : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)],
  IsFreeGroupoid.SpanningTree.homOfPath T Quiver.Path.nil =
    CategoryTheory.CategoryStruct.id (IsFreeGroupoid.SpanningTree.root'✝ T)
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- Linear equivalence between two equal submodules.  -/
LinearEquiv.ofEq : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p q : Submodule R M) → p = q → ↥p ≃ₗ[R] ↥q
-- 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] [inst_3 : OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {t : Set X}
  {x : X}, (∀ i ∈ s, ContinuousWithinAt (f i) t x) → ContinuousWithinAt (s.inf f) t x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides.  -/
EuclideanGeometry.sin_oangle_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₃ p₁ p₂).sin = dist p₃ p₂ / dist p₁ p₃
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- Product of elements of an intermediate field indexed by a `Finset` is in the intermediate field.
 -/
IntermediateField.prod_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {ι : Type u_4} {t : Finset ι} {f : ι → L}, (∀ c ∈ t, f c ∈ S) → ∏ i ∈ t, f i ∈ S
-- Lean.Elab.Term.TermElabM
/-- Registers a term elaborator for the given syntax node kind.

A term elaborator should have type `Lean.Elab.Term.TermElab` (which is
`Lean.Syntax → Option Lean.Expr → Lean.Elab.Term.TermElabM Lean.Expr`), i.e. should take syntax of
the given syntax node kind and an optional expected type as parameters and produce an expression.

The `elab_rules` and `elab` commands should usually be preferred over using this attribute
directly.
 -/
Lean.Elab.Term.termElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Term.TermElab
-- Std.Data.DHashMap.AdditionalOperations
Std.DHashMap.Raw.WF.filterMap : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  m.WF → ∀ {f : (a : α) → β a → Option (δ a)}, (Std.DHashMap.Raw.filterMap f m).WF
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.π₀.comp_fromChainComplexXZero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (x : X.obj (Opposite.op { len := 0 })) {Z : C}
  (h : (∐ fun x => R) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιChainComplex x)
      (CategoryTheory.CategoryStruct.comp (SSet.π₀.fromChainComplexXZero X R) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => R) (SSet.π₀.mk x)) h
-- Aesop.Search.Queue
Aesop.LIFOQueue.mk.inj : ∀ {goals goals_1 : Array Aesop.GoalRef}, { goals := goals } = { goals := goals_1 } → goals = goals_1
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop.0.Std.Iterators.Types.Drop.instIterator.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (x = 0 → motive 0) → ((k : ℕ) → x = k.succ → motive k.succ) → motive x
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- A pair of measures `μ` and `ν` is said to `HaveLebesgueDecomposition` if there exists a
measure `ξ` and a measurable function `f`, such that `ξ` is mutually singular with respect to
`ν` and `μ = ξ + ν.withDensity f`.  -/
MeasureTheory.Measure.HaveLebesgueDecomposition : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → Prop
-- Init.Data.Ord.Basic
Ordering.isGE_eq_not_beq_lt : ∀ {o : Ordering}, o.isGE = !o == Ordering.lt
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Corecursor for `Cofix F`  -/
MvQPF.Cofix.corec : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] → {α : TypeVec.{u} n} → {β : Type u} → (β → F (α ::: β)) → β → MvQPF.Cofix F α
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.ext₀ : ∀ {X : SSet} {f g : X.Path 0}, f.vertex 0 = g.vertex 0 → f = g
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo.decSubsingleton.sizeOf_spec : ∀ (lhs rhs : Lean.FVarId), sizeOf (Lean.Meta.EqInfo.decSubsingleton✝ lhs rhs) = 1 + sizeOf lhs + sizeOf rhs
-- Mathlib.Data.List.Basic
/-- **Alias** of `List.disjoint_map`.

---

The images of disjoint lists under an injective map are disjoint  -/
List.Disjoint.map : ∀ {α : Type u} {β : Type v} {f : α → β} {s t : List α},
  Function.Injective f → s.Disjoint t → (List.map f s).Disjoint (List.map f t)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.closedInterior_face_ssubset_closedInterior : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] [inst_4 : PartialOrder k] [Nontrivial k] [ZeroLEOneClass k] {n : ℕ}
  (s : Affine.Simplex k P n) {fs : Finset (Fin (n + 1))},
  fs ≠ Finset.univ → ∀ {m : ℕ} (h : fs.card = m + 1), (s.face h).closedInterior ⊂ s.closedInterior
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mk₁_comp_eqToHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ X₁' : C} (f : X₀ ⟶ X₁) (h : X₁ = X₁'),
  CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) =
    CategoryTheory.ComposableArrows.mk₁ f
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.compl_ofPred`. -/
Set.compl_setOf : ∀ {α : Type u_3} (p : α → Prop), {a | p a}ᶜ = {a | ¬p a}
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.zero_power_le : ∀ (c : Cardinal.{u}), 0 ^ c ≤ 1
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
/-- If `s` is a bounded set, then for small enough `r`, the set `{x} + r • s` is contained in any
fixed neighborhood of `x`.  -/
eventually_singleton_add_smul_subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {x : E} {s : Set E}, Bornology.IsBounded s → ∀ {u : Set E}, u ∈ nhds x → ∀ᶠ (r : 𝕜) in nhds 0, {x} + r • s ⊆ u
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabPatterns : Array Lean.Syntax →
  ℕ → Lean.Expr → ExceptT Lean.Elab.Term.PatternElabException Lean.Elab.TermElabM (Array Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instSMulCommClass' : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass M (Lex N) α
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.toPiLocalization_injective : ∀ (R : Type u_1) [inst : CommSemiring R], Function.Injective ⇑(PrimeSpectrum.toPiLocalization R)
-- Mathlib.Algebra.Order.Floor.Div
Pi.floorDiv_def : ∀ {ι : Type u_1} {α : Type u_2} {π : ι → Type u_4} [inst : AddCommMonoid α] [inst_1 : PartialOrder α]
  [inst_2 : (i : ι) → AddCommMonoid (π i)] [inst_3 : (i : ι) → PartialOrder (π i)]
  [inst_4 : (i : ι) → SMulZeroClass α (π i)] [inst_5 : (i : ι) → FloorDiv α (π i)] (f : (i : ι) → π i) (a : α),
  f ⌊/⌋ a = fun i => f i ⌊/⌋ a
-- Mathlib.Analysis.Complex.Circle
Circle.instSMul : {α : Type u_1} → [SMul ℂ α] → SMul Circle α
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- Given a pre-submersive presentation `P` and equivalences `ι' ≃ ι` and
`σ' ≃ σ`, this is the induced pre-submersive presentation with variables indexed
by `ι` and relations indexed by `κ`.  -/
Algebra.PreSubmersivePresentation.reindex : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              Algebra.PreSubmersivePresentation R S ι σ →
                {ι' : Type u_1} → {σ' : Type u_2} → ι' ≃ ι → σ' ≃ σ → Algebra.PreSubmersivePresentation R S ι' σ'
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.Reason.no : Std.Time.Reason✝
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ComparisonResult.noConfusionType : Sort v✝ → Mathlib.Linter.TextBased.ComparisonResult✝ → Mathlib.Linter.TextBased.ComparisonResult✝ → Sort v✝
-- Mathlib.Order.Bounds.Basic
lowerBounds_mono_set : ∀ {α : Type u_1} [inst : Preorder α] ⦃s t : Set α⦄, s ⊆ t → lowerBounds t ⊆ lowerBounds s
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.id : ∀ {X : Type u_1} [inst : TopologicalSpace X], Topology.IsEmbedding id
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFramePureTrueDown : ∀ {P : Std.Do.SPred []}, Std.Do.SPred.Tactic.HasFrame P ⌜True⌝ P.down
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.right_distrib : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S]
  (x y z : OreLocalization S R), (x + y) * z = x * z + y * z
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ}
  (lhs rhs lhs_1 rhs_1 : aig.RefVec len),
  ({ lhs := lhs, rhs := rhs } = { lhs := lhs_1, rhs := rhs_1 }) = (lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsNonempty.of_nonempty_edgeSet : ∀ {α : Type u_1} {H : Hypergraph α}, H.edgeSet.Nonempty → H.IsNonempty