mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Consumer.waiter : {α : Type} → Std.Broadcast.Consumer✝ α → Option (Std.Async.Waiter (Option α))
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep.coeq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)} →
        {k k' : ℕ} →
          (hk : k < n) →
            (hk' : k' < n) →
              (j : (X k hk).fst) →
                (j' : (X k' hk').fst) →
                  ((X k hk).snd j ⟶ (X k' hk').snd j') →
                    ((X k hk).snd j ⟶ (X k' hk').snd j') →
                      CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝ n X
-- Mathlib.Algebra.Group.End
/-- Left-multiplying a permutation with `swap i j` twice gives the original permutation.

This specialization of `swap_mul_self` is useful when using cosets of permutations.
 -/
Equiv.swap_mul_self_mul : ∀ {α : Type u_4} [inst : DecidableEq α] (i j : α) (σ : Equiv.Perm α), Equiv.swap i j * (Equiv.swap i j * σ) = σ
-- Init.Data.Vector.Lemmas
Vector.foldr_push : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β → β} {init : β} {xs : Vector α n} {a : α},
  Vector.foldr f init (xs.push a) = Vector.foldr f (f a init) xs
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.of_mem_Icc_enorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {a b : ENNReal},
  a ≠ ⊤ →
    b ≠ ⊤ → ∀ {X : α → ENNReal}, AEMeasurable X μ → (∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) → MeasureTheory.Integrable X μ
-- Init.System.FilePath
System.instInhabitedFilePath.default : System.FilePath
-- Mathlib.Data.FunLike.Group
FunLike.addLeftCancelMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : AddLeftCancelMonoid β] [inst_5 : IsZeroApply F α β] [inst_6 : IsAddApply F α β]
  [inst_7 : IsSMulApply ℕ F α β],
  FunLike.addLeftCancelMonoid = Function.Injective.addLeftCancelMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯
-- Mathlib.RingTheory.Coalgebra.Quotient
Submodule.IsCoideal.mk : ∀ {R : Type u_1} {C : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup C] [inst_2 : Module R C]
  [inst_3 : CoalgebraStruct R C] {I : Submodule R C},
  (∀ ⦃x : C⦄, x ∈ I → CoalgebraStruct.counit x = 0) →
    (∀ ⦃x : C⦄, x ∈ I → (TensorProduct.map I.mkQ I.mkQ) (CoalgebraStruct.comul x) = 0) → I.IsCoideal
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.IterM.step_flatMapAfterM.match_3.eq_2 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m γ) → Sort u_3) (it₂ : Std.IterM m γ)
  (h_1 : Unit → motive none) (h_2 : (it₂ : Std.IterM m γ) → motive (some it₂)),
  (match some it₂ with
    | none => h_1 ()
    | some it₂ => h_2 it₂) =
    h_2 it₂
-- Lean.Elab.PreDefinition.Structural.Basic
/-- Let `positions.size = ys.size` and `positions.numIndices = xs.size`. Maps `f` over each `y` in `ys`,
also passing in those elements `xs` that belong to that are those elements of `xs` that belong to
`y` according to `positions`.
 -/
Lean.Elab.Structural.Positions.mapMwith : {γ : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      {m : Type u_1 → Type u_4} →
        [Monad m] →
          [Inhabited β] → (α → Array β → m γ) → Lean.Elab.Structural.Positions → Array α → Array β → m (Array γ)
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.rel_of_isEqvAux : ∀ {α : Type u_1} {r : α → α → Bool} {xs ys : Array α} (hsz : xs.size = ys.size) {i : ℕ} (hi : i ≤ xs.size),
  xs.isEqvAux ys hsz r i hi = true → ∀ {j : ℕ} (hj : j < i), r xs[j] ys[j] = true
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.instEpiId : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.Epi (CategoryTheory.CategoryStruct.id X)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denoteAsIntModule.eq_2 : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (m : Lean.Grind.CommRing.Mon) (p_2 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denoteAsIntModule ctx (Lean.Grind.CommRing.Poly.add k m p_2) =
    k • Lean.Grind.CommRing.Mon.denoteAsIntModule ctx m + Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p_2
-- Mathlib.Data.List.Cycle
Cycle.instInhabited : {α : Type u_1} → Inhabited (Cycle α)
-- Init.Data.Vector.Lemmas
Vector.getElem?_push : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α} {i : ℕ}, (xs.push x)[i]? = if i = n then some x else xs[i]?
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.mkCommaObject_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D),
  (CategoryTheory.WithTerminal.mkCommaObject F).right = F.obj CategoryTheory.WithTerminal.star
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.multisetSum_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R) {ι : Type u_2} (s : Multiset ι) (f : ι → R),
  (∀ x ∈ s, f x ∈ I) → (Multiset.map f s).sum ∈ I
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
_private.Mathlib.Algebra.Category.ModuleCat.Topology.Basic.0.TopModuleCat.Hom.ofHom' : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] → {X Y : TopModuleCat R} → (↑X.toModuleCat →L[R] ↑Y.toModuleCat) → X.Hom Y
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.Comonad.counit_def : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B},
  CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coeFn_injective : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂], Function.Injective DFunLike.coe
-- Batteries.Data.List.Lemmas
List.insertP.eq_1 : ∀ {α : Type u_1} (p : α → Bool) (a : α) (l : List α), List.insertP p a l = List.insertP.loop p a l []
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shift_sup : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] (a : A), (P ⊔ Q).shift a = P.shift a ⊔ Q.shift a
-- Batteries.Data.BitVec.Lemmas
BitVec.toFin_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool), (BitVec.ofFnLE f).toFin = Fin.ofBits f
-- Init.Data.List.Lex
/-- `l₁` is *not* lexicographically less than `l₂`
(which you might think of as "`l₂` is lexicographically greater than or equal to `l₁`"") if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.length` or
- there exists an index `i` such that
  - for all `j < i`, `l₁[j] == l₂[j]` and
  - `l₂[i] < l₁[i]`

This formulation requires that `==` and `lt` are compatible in the following senses:
- `==` is symmetric
  (we unnecessarily further assume it is transitive, to make use of the existing typeclasses)
- `lt` is irreflexive with respect to `==` (i.e. if `x == y` then `lt x y = false`
- `lt` is asymmetric  (i.e. `lt x y = true → lt y x = false`)
- `lt` is antisymmetric with respect to `==` (i.e. `lt x y = false → lt y x = false → x == y`)
 -/
List.lex_eq_false_iff_exists : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [PartialEquivBEq α] (lt : α → α → Bool),
  (∀ (x y : α), (x == y) = true → lt x y = false) →
    (∀ (x y : α), lt x y = true → lt y x = false) →
      (∀ (x y : α), lt x y = false → lt y x = false → (x == y) = true) →
        (l₁.lex l₂ lt = false ↔
          (l₂.isEqv (List.take l₂.length l₁) fun x1 x2 => x1 == x2) = true ∨
            ∃ i,
              ∃ (h₁ : i < l₁.length) (h₂ : i < l₂.length),
                (∀ (j : ℕ) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₂[i] l₁[i] = true)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Reinterpret an element of a type of linear maps as a linear map.  -/
LinearMapClass.instCoeToLinearMap : {R : Type u_1} →
  {M₁ : Type u_9} →
    {M₂ : Type u_10} →
      {F : Type u_14} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : Module R M₁] →
                [inst_4 : Module R M₂] →
                  [inst_5 : FunLike F M₁ M₂] → [LinearMapClass F R M₁ M₂] → CoeHead F (M₁ →ₗ[R] M₂)
-- Mathlib.Order.Lattice
OrderDual.instLattice : (α : Type u_1) → [Lattice α] → Lattice αᵒᵈ
-- Lean.Structure
/-- Whether this parent structure is represented as a subobject. If so, then there is a `fieldInfo` entry with the same `projFn`.  -/
Lean.StructureParentInfo.subobject : Lean.StructureParentInfo → Bool
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Arg.fvar : {pu : Lean.Compiler.LCNF.Purity} → Lean.FVarId → Lean.Compiler.LCNF.Arg pu
-- Mathlib.Analysis.Convex.Basic
/-- Affine subspaces are convex.  -/
AffineSubspace.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (Q : AffineSubspace 𝕜 E), Convex 𝕜 ↑Q
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplex_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C), Φ.shortComplex.g = Φ.π
-- Mathlib.Data.Nat.Init
Nat.not_pos_pow_dvd : ∀ {a n : ℕ}, 1 < a → 1 < n → ¬a ^ n ∣ a
-- Mathlib.MeasureTheory.Measure.LogLikelihoodRatio
/-- Log-Likelihood Ratio between two measures.  -/
MeasureTheory.llr : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → α → ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- A variant of `of_is_product` that is more useful with `apply`.  -/
CategoryTheory.IsPullback.of_is_product' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  (h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd))
  (t : CategoryTheory.Limits.IsTerminal Z), CategoryTheory.IsPullback fst snd (t.from X) (t.from Y)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_filter_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool}, (Std.ExtDHashMap.filter f m).size ≤ m.size
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmullerAux.eq_2 : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  (x : Perfection (R ⧸ I) p) (n : ℕ), x.teichmullerAux n.succ = Quotient.out ((Perfection.coeff (R ⧸ I) p n) x) ^ p ^ n
-- Mathlib.Algebra.Homology.FullSubcategory
/-- The functor `D ⥤ HomologicalComplex P.FullSubcategory c`
which is obtained by lifting a functor `D ⥤ HomologicalComplex V c`
when for any `X : D` and `n`, the object `(F.obj X).X n`
satisfies a property `P : ObjectProperty V`.  -/
HomologicalComplex.liftFunctorObjectProperty : {D : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} D] →
    {ι : Type u_2} →
      {c : ComplexShape ι} →
        {V : Type u_3} →
          [inst_1 : CategoryTheory.Category.{v_2, u_3} V] →
            [inst_2 : CategoryTheory.Preadditive V] →
              (P : CategoryTheory.ObjectProperty V) →
                (F : CategoryTheory.Functor D (HomologicalComplex V c)) →
                  (∀ (X : D) (n : ι), P ((F.obj X).X n)) →
                    CategoryTheory.Functor D (HomologicalComplex P.FullSubcategory c)
-- Mathlib.CategoryTheory.Limits.Preserves.Lattice
CategoryTheory.Limits.CompleteLattice.preservesLimitsOfShape_finite_toFunctor : ∀ {α : Type u} {β : Type v} {F : Type u_1} [inst : FunLike F α β] (f : F) [inst_1 : SemilatticeInf α]
  [inst_2 : OrderTop α] [inst_3 : SemilatticeInf β] [inst_4 : OrderTop β] [inst_5 : InfTopHomClass F α β] {J : Type w}
  [inst_6 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (↑f).toFunctor
-- Mathlib.Data.Fin.Embedding
Fin.castSuccEmb_apply : ∀ {n : ℕ} (i : Fin n), Fin.castSuccEmb i = i.castSucc
-- Mathlib.Data.Multiset.Range
Multiset.notMem_range_self : ∀ {n : ℕ}, n ∉ Multiset.range n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t : Std.DTreeMap.Internal.Impl α β) (k : α)
  (hlk : k ∈ t),
  t.get k hlk =
    match t, hlk with
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, hlk =>
      match h : compare k k' with
      | Ordering.lt => l.get k ⋯
      | Ordering.gt => r.get k ⋯
      | Ordering.eq => cast ⋯ v'
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_le_iff_le_coe : ∀ {q : ℚ} {p : ℚ≥0}, q.toNNRat ≤ p ↔ q ≤ ↑p
-- Init.Coe
/-- `↥ t` coerces `t` to a type.  -/
coeSortNotation : Lean.ParserDescr
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_X : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (n : σ), MvPolynomial.eval₂ f g (MvPolynomial.X n) = g n
-- Mathlib.Algebra.MvPolynomial.Basic
/-- Similar to `MvPolynomial.induction_on` but only a yet weaker form of `h_add` is required.
In particular, this version only requires us to show
that `motive` is closed under addition of monomials not present in the support
for which `motive` is already known to hold.
 -/
MvPolynomial.induction_on'' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {motive : MvPolynomial σ R → Prop} (p : MvPolynomial σ R),
  (∀ (a : R), motive (MvPolynomial.C a)) →
    (∀ (a : σ →₀ ℕ) (b : R) (f : MvPolynomial σ R),
        a ∉ f.coeff.support →
          b ≠ 0 → motive f → motive ((MvPolynomial.monomial a) b) → motive ((MvPolynomial.monomial a) b + f)) →
      (∀ (p : MvPolynomial σ R) (n : σ), motive p → motive (p * MvPolynomial.X n)) → motive p
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The map which shall exhibit `reflectionObj W Z κ` as the image of `Z` by
the left adjoint of the inclusion of `W.isLocal`, see `corepresentableBy`.  -/
CategoryTheory.OrthogonalReflection.reflection : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [inst_1 : CategoryTheory.Limits.HasPushouts C] →
          [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
            [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
              [inst_4 :
                  ∀ (Z : C),
                    CategoryTheory.Limits.HasMulticoequalizer
                      (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)] →
                (κ : Cardinal.{w}) →
                  [inst_5 : OrderBot κ.ord.ToType] →
                    [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] →
                      Z ⟶ CategoryTheory.OrthogonalReflection.reflectionObj W Z κ
-- Init.GrindInstances.Ring.BitVec
Lean.Grind.instCommRingBitVec : {w : ℕ} → Lean.Grind.CommRing (BitVec w)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendRestrictScalarsAdj_unit_app_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (M : ModuleCat R) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.extendRestrictScalarsAdj f).unit.app M)) m = 1 ⊗ₜ[R] m
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_of_lt : ∀ {n : ℕ} {i j k : Fin n}, k < i → (i.cycleIcc j) k = k
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.qaryEntropy_zero : ∀ (q : ℕ), Real.qaryEntropy q 0 = 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.ennreal_ofReal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => ENNReal.ofReal (f x)
-- Mathlib.Data.Fintype.EquivFin
/-- See `Infinite.exists_subset_card_eq` for a version that provides an arbitrary
`s : Finset α` for any cardinality.  -/
Infinite.exists_superset_card_eq : ∀ {α : Type u_1} [Infinite α] (s : Finset α) (n : ℕ), s.card ≤ n → ∃ t, s ⊆ t ∧ t.card = n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∪ t₂).getKey! k = t₁.getKey! k
-- Batteries.Classes.Order
Std.TransCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : DecidableEq α],
  (∀ (x : α), ¬x < x) →
    (∀ {x y z : α}, x < y → y < z → x < z) →
      (∀ {x y : α}, ¬x < y → ¬y < x → x = y) → Std.TransCmp fun x1 x2 => compareOfLessAndEq x1 x2
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.ofParallelHoms_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.Limits.MulticospanShape) {X Y : C}
  (f g : X ⟶ Y) (x : J.R), (CategoryTheory.Limits.MulticospanIndex.ofParallelHoms J f g).snd x = g
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {X Y : CategoryTheory.StructuredArrow S T} (f g : X ⟶ Y),
  CategoryTheory.StructuredArrow.Hom.right f = CategoryTheory.StructuredArrow.Hom.right g → f = g
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- Construct a morphism to the explicit pullback given morphisms to the factors
which are compatible with the maps to the base.
This is essentially the universal property of the pullback.
 -/
CompHausLike.pullback.lift : {P : TopCat → Prop} →
  {X Y B : CompHausLike P} →
    (f : X ⟶ B) →
      (g : Y ⟶ B) →
        [inst : CompHausLike.HasExplicitPullback f g] →
          {Z : CompHausLike P} →
            (a : Z ⟶ X) →
              (b : Z ⟶ Y) →
                CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g →
                  (Z ⟶ CompHausLike.pullback f g)
-- Mathlib.GroupTheory.Torsion
/-- `g` lies in the additive `p`-primary component iff `p ^ k • g = 0` for some `k`.  -/
AddCommMonoid.mem_primaryComponent : ∀ {G : Type u_1} [inst : AddCommMonoid G] {p : ℕ} {g : G}, g ∈ AddCommMonoid.primaryComponent G p ↔ ∃ k, p ^ k • g = 0
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- The natural equivalence between `X` and `Snowflaking X α hr₀ hr₁`.  -/
Metric.Snowflaking.toSnowflaking : {X : Type u_1} → {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → X ≃ Metric.Snowflaking X α hα₀ hα₁
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_unique_nonempty : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Unique ι] (s : Finset ι) (f : ι → M),
  s.Nonempty → ∏ x ∈ s, f x = f default
-- Mathlib.Combinatorics.Matroid.Circuit
/-- **Alias** of `Matroid.IsBase.compl_closure_sdiff_singleton_isCocircuit`.

---

For an element `e` of a base `B`, the complement of the closure of `B \ {e}` is a cocircuit.  -/
Matroid.IsBase.compl_closure_diff_singleton_isCocircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α} {B : Set α}, M.IsBase B → e ∈ B → M.IsCocircuit (M.E \ M.closure (B \ {e}))
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.PrefixTable.step.match_3.eq_1 : ∀ {α : Type u_1} (t : Array.PrefixTable α) (motive : Fin (t.size + 1) → Sort u_2) (k : ℕ) (hk : k < t.size + 1)
  (h_1 : (k : ℕ) → (hk : k < t.size + 1) → motive ⟨k, hk⟩),
  (match ⟨k, hk⟩ with
    | ⟨k, hk⟩ => h_1 k hk) =
    h_1 k hk
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAdd.eq_1 : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Add M],
  Filter.Germ.instAdd = { add := Filter.Germ.map₂ fun x1 x2 => x1 + x2 }
-- Mathlib.Algebra.Algebra.Basic
FaithfulSMul.to_isTorsionFree : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  [Nontrivial R] [IsCancelMulZero A], Module.IsTorsionFree R A
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice_8 : Std.Rii.Sliceable ByteArray ℕ ByteSlice
-- Init.PropLemmas
exists_idem : ∀ {P : Prop} (f : P → P → Prop), (∃ (p₁ : P) (p₂ : P), f p₁ p₂) ↔ ∃ (p : P), f p p
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanShape.prod_snd : ∀ (ι : Type w) (self : ι × ι), (CategoryTheory.Limits.MulticospanShape.prod ι).snd self = self.2
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.semilinearEquivOfRingEquiv.eq_1 : ∀ {A : Type u_8} {B : Type u_9} (K : Type u_10) (L : Type u_11) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : CommRing K] [inst_3 : CommRing L] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K]
  [inst_6 : Algebra B L] [inst_7 : IsFractionRing B L] (f : A ≃+* B),
  IsFractionRing.semilinearEquivOfRingEquiv K L f =
    { toFun := (IsFractionRing.ringEquivOfRingEquiv f).toFun, map_add' := ⋯, map_smul' := ⋯,
      invFun := (IsFractionRing.ringEquivOfRingEquiv f).invFun, left_inv := ⋯, right_inv := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.filterMap_equiv_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.filterMap (fun k v => some (f k v)) t).Equiv (Std.DTreeMap.map f t)
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α =
    { obj := CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj,
      map := fun {X Y} β => { app := fun x => CategoryTheory.Limits.Sigma.map fun x_1 => β.app ↑x_1, naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData) (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData),
  CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.leftHomologyMap' (CategoryTheory.CategoryStruct.id S) h₁ h.left)
      (CategoryTheory.CategoryStruct.comp h.iso.hom
        (CategoryTheory.ShortComplex.rightHomologyMap' (CategoryTheory.CategoryStruct.id S) h.right h₂))
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_neg : ∀ {ι : 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 : ι) → AddGroup (G i)] [inst_7 : AddGroup C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), AddMonoidHomClass (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)) (x : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (-x) = -DirectLimit.lift f (fun x => ⇑(g x)) h x
-- Lean.Parser.Attr
Lean.Parser.Attr.simple.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ne_empty_of_erase_ne_empty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.erase k ≠ ∅ → t ≠ ∅
-- Mathlib.Order.Hom.Basic
OrderHom.coe_le_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {f g : α →o β}, ⇑f ≤ ⇑g ↔ f ≤ g