mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Divisibility.Basic
mul_dvd_mul_right : ∀ {α : Type u_1} [inst : CommMonoid α] {a b : α}, a ∣ b → ∀ (c : α), a * c ∣ b * c
-- Init.Core
imp_intro : ∀ {α β : Prop}, α → β → α
-- Init.Data.List.Basic
/-- The first list is a contiguous sub-list of the second list. Typically written with the `<:+:`
operator.

In other words, `l₁ <:+: l₂` means that there exist lists `s : List α` and `t : List α` such that
`l₂` has the form `s ++ l₁ ++ t`.


Conventions for notations in identifiers:

 * The recommended spelling of `<:+:` in identifiers is `infix` (not `isInfix`). -/
List.IsInfix : {α : Type u} → List α → List α → Prop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertManyIfNewUnit_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} {k : α},
  t.insertManyIfNewUnit [k] = t.insertIfNew k ()
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insertMany!_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} [inst_1 : Inhabited (β k')],
      List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
        ⟨k, v⟩ ∈ l → (↑(t.insertMany! l)).get! k' = cast ⋯ v
-- Mathlib.Algebra.Order.Sub.Defs
tsub_le_tsub_add_tsub : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], a - c ≤ a - b + (b - c)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn₃₁.desc.multicofork_π_three_assoc : ∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj { len := 2 } ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃)
  {Z : SSet} (h : (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨3, SSet.horn₃₁.desc.multicofork_π_three._proof_1⟩) h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 3).inv f₃) h
-- Mathlib.CategoryTheory.SingleObj
MonoidHom.comp_toFunctor : ∀ {M : Type u} {N : Type v} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) {P : Type w} [inst_2 : Monoid P]
  (g : N →* P), (g.comp f).toFunctor = f.toFunctor.comp g.toFunctor
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The universal property of the direct limit: maps from the components to another StarRing
that respect the directed system structure (i.e. make some diagram commute) give rise
to a unique map out of the direct limit.
 -/
DirectLimit.NonUnitalStarRing.lift : {ι : Type u_2} →
  [inst : Preorder ι] →
    (G : ι → Type u_3) →
      {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 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)] →
                  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                    [inst_6 : (i : ι) → StarRing (G i)] →
                      [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] →
                        [inst_8 : Nonempty ι] →
                          (P : Type u_7) →
                            [inst_9 : NonUnitalNonAssocSemiring P] →
                              [inst_10 : StarRing P] →
                                (g : (i : ι) → G i →⋆ₙ+* P) →
                                  (∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) →
                                    DirectLimit G f →⋆ₙ+* P
-- Mathlib.CategoryTheory.Limits.Opposites
/-- If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
 -/
CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  [CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ C], CategoryTheory.Limits.HasLimitsOfShape J Cᵒᵖ
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_def : ∀ {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {x : MeasurableSpace α} [inst_3 : MeasurableSpace β] (Y : α → Ω) (X : α → β)
  (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.condDistrib Y X μ = (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).condKernel
-- Mathlib.Algebra.BigOperators.Option
Finset.prod_eraseNone : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] (f : α → M) (s : Finset (Option α)),
  ∏ x ∈ Finset.eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.coforkOfCokernelCofork_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.CokernelCofork (f - g)),
  (CategoryTheory.Preadditive.coforkOfCokernelCofork c).π = CategoryTheory.Limits.Cofork.π c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.instHasFiniteProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.Algebra.Field.Defs
/-- `OfScientific.ofScientific` is the simp-normal form.  -/
Rat.ofScientific_eq_ofScientific : ∀ (m : ℕ) (s : Bool) (e : ℕ), Rat.ofScientific (OfNat.ofNat m) s (OfNat.ofNat e) = OfScientific.ofScientific m s e
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.numeratorRingHom_apply : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (r : R),
  OreLocalization.numeratorRingHom r = r /ₒ 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_iff_support_isInfix : ∀ {V : Type u_1} {G : SimpleGraph V} {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'},
  p₁.IsSubwalk p₂ ↔ p₁.support <:+: p₂.support
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `L` with the spectral norm is a `NormedSpace` over `K`.  -/
spectralNorm.normedSpace : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [inst_3 : Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [inst_4 : CompleteSpace K] → NormedSpace K L
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E] {x : 𝕜}
  [inst_6 : NormedAlgebra 𝕜 R] [IsScalarTower 𝕜 R E] {f : 𝕜 → R} {g : 𝕜 → E},
  MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (f • g) x
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instLeftCancelSemigroup : {α : Type u_1} → [LeftCancelSemigroup α] → LeftCancelSemigroup αᵃᵒᵖ
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.isoMk_inv_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map r.hom))
      CategoryTheory.MorphismProperty.Comma.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Comma.isoMk l r h).inv.left = l.inv
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
instIsRightCancelAddOfAddRightReflectLE : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [AddRightReflectLE α], IsRightCancelAdd α
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.smul_closure : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] (a : M)
  (s : Set R), a • Subring.closure s = Subring.closure (a • s)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- The canonical map from `Lᵖ ν` to `Lᵖ μ` when `μ` is bounded by a finite multiple of `ν`.  -/
MeasureTheory.Lp.LpToLpOfMeasureLeSMul : {α : Type u_1} →
  {E : Type u_4} →
    {m : MeasurableSpace α} →
      {p : ENNReal} →
        {μ : MeasureTheory.Measure α} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              {ν : MeasureTheory.Measure α} →
                {c : ENNReal} →
                  [inst_2 : Fact (1 ≤ p)] →
                    c ≠ ⊤ → μ ≤ c • ν → ↥(MeasureTheory.Lp E p ν) →L[ℝ] ↥(MeasureTheory.Lp E p μ)
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackSnd : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.IsSchemeTheoreticallyDominant f]
  [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.Flat g],
  AlgebraicGeometry.IsSchemeTheoreticallyDominant (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_symm_eq : ∀ {α : Type u_1}, ofBoolRing.symm = toBoolRing
-- Init.Grind.Lemmas
Lean.Grind.or_eq_of_eq_true_right : ∀ {a b : Prop}, b = True → (a ∨ b) = True
-- Mathlib.CategoryTheory.Monoidal.Limits.Colimits
CategoryTheory.Limits.Cocone.tensor_pt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {J : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} J] {F₁ F₂ : CategoryTheory.Functor J C}
  (c₁ : CategoryTheory.Limits.Cocone F₁) (c₂ : CategoryTheory.Limits.Cocone F₂),
  (c₁.tensor c₂).pt = CategoryTheory.MonoidalCategoryStruct.tensorObj c₁.pt c₂.pt
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.IsAffineMap.id : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M], Convexity.IsAffineMap R id
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.naturality_leftUnitor : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c}
  (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf),
  CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Bicategory.leftUnitor f) ≪≫ η_f =
    Mathlib.Tactic.Bicategory.normalizeIsoComp (CategoryTheory.Bicategory.rightUnitor p) η_f
-- Mathlib.Algebra.Order.Field.Basic
div_lt_one_iff : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
-- Mathlib.Algebra.Lie.Loop
/-- The residue pairing on the loop algebra.  When `A = ℤ` and the elements are viewed as Laurent
polynomials with coefficients in `L`, the pairing is interpreted as `(f, g) ↦ Res f dg`.  -/
LieAlgebra.LoopAlgebra.residuePairing : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [AddCommGroup A] →
              [inst_4 : DistribSMul A R] →
                [SMulCommClass A R R] → LinearMap.BilinForm R L → LinearMap.BilinForm R (LieAlgebra.loopAlgebra R A L)
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toArray_iter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β}, m.iter.toArray = m.toArray
-- Mathlib.Topology.Connected.PathConnected
/-- The quotient type of points of a topological space modulo being joined by a continuous path.  -/
ZerothHomotopy : (X : Type u_1) → [TopologicalSpace X] → Type u_1
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonDidChangeWatchedFilesParams.fromJson : Lean.Json → Except String Lean.Lsp.DidChangeWatchedFilesParams
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)] {b : β a}, (m.insert a b).get! a = b
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.bind_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (p : PMF α) (q : PMF β) (f : α → β → PMF γ),
  (p.bind fun a => q.bind (f a)) = q.bind fun b => p.bind fun a => f a b
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- The size of each part  -/
OrderedFinpartition.partSize : {n : ℕ} → (self : OrderedFinpartition n) → Fin self.length → ℕ
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- **Alias** of `CoxeterMatrix.B`.

---

The Coxeter matrix of type Bₙ.

The corresponding Coxeter-Dynkin diagram is:
```
       4
    o --- o --- o ⬝ ⬝ ⬝ ⬝ o --- o
```
 -/
CoxeterMatrix.Bₙ : (n : ℕ) → CoxeterMatrix (Fin n)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_p_pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ), ‖↑p ^ n‖ = ↑p ^ (-↑n)
-- Init.Data.BitVec.Bitblast
/-- A `Poised` DivModState is a state which is `Lawful` and furthermore, has at least
one numerator bit left to process `(0 < wn)`

The input to the shift subtractor is a legal input to `divrem`, and we also need to have an
input bit to perform shift subtraction on, and thus we need `0 < wn`.
 -/
BitVec.DivModState.Poised : {w : ℕ} → BitVec.DivModArgs w → BitVec.DivModState w → Prop
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.isAlgebraic : ∀ (F : Type u_1) (E : Type u_2) [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E] [Nontrivial F]
  [IsPurelyInseparable F E], Algebra.IsAlgebraic F E
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tsum_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α),
  ∑' (x : ↑Set.univ), f ↑x = ∑' (x : β), f x
-- Mathlib.Algebra.Free
FreeMagma.toFreeSemigroup_of : ∀ {α : Type u} (x : α), FreeMagma.toFreeSemigroup (FreeMagma.of x) = FreeSemigroup.of x
-- Mathlib.LinearAlgebra.Dimension.DivisionRing
DivisionRing.hasRankNullity : ∀ {K : Type u} [inst : DivisionRing K], HasRankNullity.{u₀, u} K
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.tan_sub' : ∀ {x y : ℂ},
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * ↑Real.pi / 2) →
    Complex.tan (x - y) = (Complex.tan x - Complex.tan y) / (1 + Complex.tan x * Complex.tan y)
-- Init.Data.Int.Order
Int.add_one_le_iff : ∀ {a b : ℤ}, a + 1 ≤ b ↔ a < b
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.categoryStruct : {B : Type u} → [Quiver B] → CategoryTheory.CategoryStruct.{max u v, u} (CategoryTheory.FreeBicategory B)
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- If `i ≠ j`, the pullback `Xᵢ ×[Z] Xⱼ` is initial, if `Z` is the coproduct of the `Xᵢ`.  -/
CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : ι → C} →
        [CategoryTheory.Limits.CoproductDisjoint X] →
          {i j : ι} →
            i ≠ j →
              {Z : C} →
                {f : (i : ι) → X i ⟶ Z} →
                  [inst_2 : CategoryTheory.Limits.HasPullback (f i) (f j)] →
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk Z f) →
                      CategoryTheory.Limits.IsInitial (CategoryTheory.Limits.pullback (f i) (f j))
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCofan_isColimit_iff : ∀ {X Y : Type u} (c : CategoryTheory.Limits.BinaryCofan X Y),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom c.inl) ∧
      Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inl))
          (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inr))
-- Lean.Meta.Tactic.ElimInfo
/-- A declaration corresponding to the inductive constructor.
(For custom recursors, the alternatives correspond to parameter names in the
recursor, so we may not have a declaration to point to.)
This is used for go-to-definition on the alternative name.  -/
Lean.Meta.ElimAltInfo.declName? : Lean.Meta.ElimAltInfo → Option Lean.Name
-- Mathlib.CategoryTheory.Adjunction.FullyFaithfulLimits
CategoryTheory.Adjunction.preservesColimitsOfSize_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {E : Type u₃}
  [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (H : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.HasColimitsOfSize.{v, u, v₁, u₁} C] [G.Full] [G.Faithful],
  CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₂, v₃, u₂, u₃} H ↔
    CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₃, u₁, u₃} (F.comp H)
-- Init.Data.String.OrderInstances
String.Pos.Raw.instLawfulOrderLT : Std.LawfulOrderLT String.Pos.Raw
-- Batteries.Data.MLList.Basic
/-- Deconstruct a `MLList`, returning inside the monad an optional pair `α × MLList m α`
representing the head and tail of the list.  -/
MLList.uncons : {m : Type u → Type u} → {α : Type u} → [Monad m] → MLList m α → m (Option (α × MLList m α))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a k : α) (v : β k) (l : List ((a : α) × β a)),
  Std.Internal.List.getValueCast? a (⟨k, v⟩ :: l) =
    if h : (k == a) = true then some (cast ⋯ v) else Std.Internal.List.getValueCast? a l
-- Mathlib.Analysis.SpecificLimits.Basic
summable_geometric_of_lt_one : ∀ {r : ℝ}, 0 ≤ r → r < 1 → Summable fun n => r ^ n
-- Mathlib.Analysis.Complex.Exponential
Complex.expMonoidHom_apply : ∀ (z : Multiplicative ℂ), Complex.expMonoidHom z = Complex.exp (Multiplicative.toAdd z)
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
/-- `H` as a real Hilbert space. This instance is declared inside `ClosedSubmodule` namespace. If
one needs this structure (for example when considering standard subspaces), one should just `open
ClosedSubmodule` and not declare another instance.  -/
ClosedSubmodule.instInnerProductSpaceReal : {H : Type u_1} → [inst : NormedAddCommGroup H] → [ipc : InnerProductSpace ℂ H] → InnerProductSpace ℝ H
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M],
  UniqueFactorizationMonoid.radical 0 = 1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor that preserves biproducts of a pair preserves binary biproducts.  -/
CategoryTheory.Limits.preservesBinaryBiproduct_of_preservesBiproduct : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] (X Y : C)
  [CategoryTheory.Limits.PreservesBiproduct (CategoryTheory.Limits.pairFunction X Y) F],
  CategoryTheory.Limits.PreservesBinaryBiproduct X Y F
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.homOfPath.eq_2 : ∀ {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)] (x : G)
  (b : WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)
  (p : Quiver.Path (Quiver.root (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)) b)
  (f : b ⟶ x),
  IsFreeGroupoid.SpanningTree.homOfPath T (p.cons f) =
    CategoryTheory.CategoryStruct.comp (IsFreeGroupoid.SpanningTree.homOfPath T p)
      (Sum.recOn (↑f) (fun e => IsFreeGroupoid.of e) fun e => CategoryTheory.inv (IsFreeGroupoid.of e))
-- Mathlib.Logic.Equiv.Defs
Equiv.mk.injEq : ∀ {α : Sort u_1} {β : Sort u_2} (toFun : α → β) (invFun : β → α)
  (left_inv : autoParam (Function.LeftInverse invFun toFun) Equiv.left_inv._autoParam)
  (right_inv : autoParam (Function.RightInverse invFun toFun) Equiv.right_inv._autoParam) (toFun_1 : α → β)
  (invFun_1 : β → α) (left_inv_1 : autoParam (Function.LeftInverse invFun_1 toFun_1) Equiv.left_inv._autoParam)
  (right_inv_1 : autoParam (Function.RightInverse invFun_1 toFun_1) Equiv.right_inv._autoParam),
  ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }) =
    (toFun = toFun_1 ∧ invFun = invFun_1)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.move.inj : ∀ {p : Turing.PartrecToTM2.Γ' → Bool} {k₁ k₂ : Turing.PartrecToTM2.K'} {q : Turing.PartrecToTM2.Λ'}
  {p_1 : Turing.PartrecToTM2.Γ' → Bool} {k₁_1 k₂_1 : Turing.PartrecToTM2.K'} {q_1 : Turing.PartrecToTM2.Λ'},
  Turing.PartrecToTM2.Λ'.move p k₁ k₂ q = Turing.PartrecToTM2.Λ'.move p_1 k₁_1 k₂_1 q_1 →
    p = p_1 ∧ k₁ = k₁_1 ∧ k₂ = k₂_1 ∧ q = q_1
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.nontrivial_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], Nontrivial (TopologicalSpace.Compacts α) ↔ Nonempty α
-- Init.Data.Nat.Lemmas
Nat.mod_eq_iff : ∀ {a b c : ℕ}, a % b = c ↔ b = 0 ∧ a = c ∨ c < b ∧ ∃ k, a = b * k + c
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.Origin.other.inj : ∀ {name name_1 : Lean.Name}, Lean.Meta.Origin.other name = Lean.Meta.Origin.other name_1 → name = name_1
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- Deleting the incident set of the vertex `x` deletes exactly `G.degree x` edges from the edge
set of the simple graph `G`.  -/
SimpleGraph.card_edgeFinset_deleteIncidenceSet : ∀ {V : Type u_1} [inst : Fintype V] [inst_1 : DecidableEq V] (G : SimpleGraph V) [inst_2 : DecidableRel G.Adj] (x : V),
  (G.deleteIncidenceSet x).edgeFinset.card = G.edgeFinset.card - G.degree x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K L : CochainComplex C ℤ} {n₁ n₃ n₁₃ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁)
  (z₂ : CochainComplex.HomComplex.Cochain G K 0) (z₃ : CochainComplex.HomComplex.Cochain K L n₃) (h₁₃ : n₁ + n₃ = n₁₃),
  (z₁.comp z₂ ⋯).comp z₃ h₁₃ = z₁.comp (z₂.comp z₃ ⋯) h₁₃
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.norm_cnstr_cert.eq_1 : ∀ (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_cnstr_cert lhs rhs lhs' rhs' = (rhs.sub lhs).toPoly_k.beq' (rhs'.sub lhs').toPoly_k
-- Init.Data.SInt.Lemmas
Int32.toInt16_mul : ∀ (a b : Int32), (a * b).toInt16 = a.toInt16 * b.toInt16
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.homInhabited : {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.MonoidalLeftAction C D] →
            {A : C} → [inst_4 : CategoryTheory.MonObj A] → (M : CategoryTheory.Mod D A) → Inhabited (M.Hom M)