mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.linearIndependent_coord : ∀ {ι : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {R : Type u_7} [inst_1 : CommSemiring R] [inst_2 : Module R M]
  (b : Module.Basis ι R M), LinearIndependent R b.coord
-- Mathlib.Algebra.Group.Defs
/-- `ZSMul` is an implementation detail of `SubNegMonoid`. It is needed because it is
impossible to extend `SMUl ℕ M` and `SMul ℤ M` at the same time.  -/
ZSMul : Type u → Type u
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a limit for `F.unop : J ⥤ C` into a colimit for `F : Jᵒᵖ ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.isColimitCoconeOfConeUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cone F.unop} →
            CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeUnop c)
-- Aesop.Stats.Basic
Aesop.GoalStats.mk.injEq : ∀ (goalId : ℕ) (goalKind : Aesop.GoalKind) (lctxSize depth : ℕ) (forwardStateStats : Aesop.ForwardStateStats)
  (goalId_1 : ℕ) (goalKind_1 : Aesop.GoalKind) (lctxSize_1 depth_1 : ℕ) (forwardStateStats_1 : Aesop.ForwardStateStats),
  ({ goalId := goalId, goalKind := goalKind, lctxSize := lctxSize, depth := depth,
        forwardStateStats := forwardStateStats } =
      { goalId := goalId_1, goalKind := goalKind_1, lctxSize := lctxSize_1, depth := depth_1,
        forwardStateStats := forwardStateStats_1 }) =
    (goalId = goalId_1 ∧
      goalKind = goalKind_1 ∧ lctxSize = lctxSize_1 ∧ depth = depth_1 ∧ forwardStateStats = forwardStateStats_1)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_norm_eq_pos_sub_neg : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {f : X → ℝ},
  MeasureTheory.Integrable f μ →
    ∫ (x : X), ‖f x‖ ∂μ = ∫ (x : X) in {x | 0 ≤ f x}, f x ∂μ - ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.instLTQOfOrderedAdd : {α : Type u} →
  [inst : Lean.Grind.Semiring α] →
    [inst_1 : LE α] → [inst_2 : Std.IsPreorder α] → [Lean.Grind.OrderedAdd α] → LT (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup_sub_left : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Sub α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderBot β] (s t : Finset α) (f : α → β), (s - t).sup f = s.sup fun x => t.sup fun x_1 => f (x - x_1)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_trans : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal]
  [inst_1 : MeasureTheory.OuterMeasureClass F α] {μ : F} {f g h : α → β}, f =ᵐ[μ] g → g =ᵐ[μ] h → f =ᵐ[μ] h
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.comp_homeomorph_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s : Set X}
  {E' : Type u_3} [inst_2 : TopologicalSpace E'] (g : E' ≃ₜ E), IsCoveringMapOn (f ∘ ⇑g) s ↔ IsCoveringMapOn f s
-- Mathlib.GroupTheory.Exponent
AddMonoidHom.exponent_dvd : ∀ {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : AddMonoid M₁] [inst_1 : AddMonoid M₂]
  [inst_2 : FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {f : F},
  Function.Surjective ⇑f → AddMonoid.exponent M₂ ∣ AddMonoid.exponent M₁
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The valuative relation on `WithPreorder R` arising from the valuative relation on `R`.
This is defined as the preorder itself.  -/
ValuativeRel.instWithPreorder : {R : Type u_1} → [inst : Semiring R] → [ValuativeRel R] → ValuativeRel (ValuativeRel.WithPreorder R)
-- Mathlib.RingTheory.Regular.RegularSequence
IsLocalRing.isRegular_iff_isWeaklyRegular_of_subset_maximalIdeal : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Nontrivial M] [Module.Finite R M] {rs : List R},
  (∀ r ∈ rs, r ∈ IsLocalRing.maximalIdeal R) →
    (RingTheory.Sequence.IsRegular M rs ↔ RingTheory.Sequence.IsWeaklyRegular M rs)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimits_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimits F.unop],
  CategoryTheory.Limits.ReflectsColimits F
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- If a pair of measures `HaveLebesgueDecomposition`, then `singularPart` chooses the
measure from `HaveLebesgueDecomposition`, otherwise it returns the zero measure. For sigma-finite
measures, `μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)`.  -/
MeasureTheory.Measure.singularPart : {α : Type u_2} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → MeasureTheory.Measure α
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.zero_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (CommRingCat.Colimits.Prequotient.zero.mul x) CommRingCat.Colimits.Prequotient.zero
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.snd_apply : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (self : α × β), (OrderMonoidHom.snd α β) self = self.2
-- Init.Data.Option.Array
Option.toArray_toList : ∀ {α : Type u_1} {o : Option α}, o.toList.toArray = o.toArray
-- Lean.Meta.Basic
/-- Similar to `isDefEq`, but ensures that only reducible definitions and instances can be reduced.  -/
Lean.Meta.isDefEqI : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Init.Data.Fin.Fold
/-- Inner loop for `Fin.foldrM`.
```
Fin.foldrM.loop n f i xᵢ = do
  let xᵢ₋₁ ← f (i-1) xᵢ
  ...
  let x₁ ← f 1 x₂
  let x₀ ← f 0 x₁
  pure x₀
```
 -/
_private.Init.Data.Fin.Fold.0.Fin.foldrM.loop : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → (n : ℕ) → (Fin n → α → m α) → { i // i ≤ n } → α → m α
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instPartialOrder.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenNormalAddSubgroup.instPartialOrder = PartialOrder.ofSetLike (OpenNormalAddSubgroup G) G
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup is closed under multiplication.  -/
Subgroup.mul_mem : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → y ∈ H → x * y ∈ H
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.hij : ∀ {n : Type u_1} {R : Type u₂} (self : Matrix.TransvectionStruct n R), self.i ≠ self.j
-- Mathlib.Order.Atoms.Finite
Fintype.IsSimpleOrder.univ : ∀ {α : Type u_1} [inst : LE α] [inst_1 : BoundedOrder α] [inst_2 : IsSimpleOrder α] [inst_3 : DecidableEq α],
  Finset.univ = {⊤, ⊥}
-- Mathlib.Order.Preorder.Finite
Set.Finite.exists_minimalFor' : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] [IsTrans α fun a a_1 => a_1 ≤ a] (f : ι → α) (s : Set ι),
  (f '' s).Finite → s.Nonempty → ∃ i, MinimalFor (fun x => x ∈ s) f i
-- Lean.MetavarContext
/-- At what depth level mvars can be assigned.  -/
Lean.MetavarContext.levelAssignDepth : Lean.MetavarContext → ℕ
-- Init.Data.Option.Monadic
Option.forIn_pure_yield_eq_elim : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option α)
  (f : α → β → β) (b : β), (forIn o b fun a b => pure (ForInStep.yield (f a b))) = pure (o.elim b fun a => f a b)
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_add : ∀ (f g : ℕ → ℂ) (s : ℂ), LSeries.term (f + g) s = LSeries.term f s + LSeries.term g s
-- Mathlib.Data.Part
Part.left_dom_of_mod_dom : ∀ {α : Type u_1} [inst : Mod α] {a b : Part α}, (a % b).Dom → a.Dom
-- Mathlib.Order.Filter.Pi
Filter.pi_inf_principal_univ_pi_eq_bot : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)},
  Filter.pi f ⊓ Filter.principal (Set.univ.pi s) = ⊥ ↔ ∃ i, f i ⊓ Filter.principal (s i) = ⊥
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
CategoryTheory.Abelian.FreydMitchell.instNonemptyAsSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C], Nonempty (CategoryTheory.AsSmall C)
-- Lean.Parser.Extension
Lean.Parser.declareBuiltinParser : Lean.Name → Lean.Name → Lean.Name → ℕ → Lean.CoreM Unit
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Typecheck an `AddHom` as a morphism in `AddSemigrp`.  -/
AddSemigrp.ofHom : {X Y : Type u} → [inst : AddSemigroup X] → [inst_1 : AddSemigroup Y] → (X →ₙ+ Y) → (AddSemigrp.of X ⟶ AddSemigrp.of Y)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The `AddSubgroup`s of an `AddGroup` form a complete lattice.  -/
AddSubgroup.instCompleteLattice : {G : Type u_1} → [inst : AddGroup G] → CompleteLattice (AddSubgroup G)
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.toList.match_1.eq_2 : ∀ (γ : Type u_1) (motive : WType (WType.Listβ γ) → Sort u_2) (hd : γ)
  (f : WType.Listβ γ (WType.Listα.cons hd) → WType (WType.Listβ γ))
  (h_1 : (f : WType.Listβ γ WType.Listα.nil → WType (WType.Listβ γ)) → motive (WType.mk WType.Listα.nil f))
  (h_2 :
    (hd : γ) →
      (f : WType.Listβ γ (WType.Listα.cons hd) → WType (WType.Listβ γ)) → motive (WType.mk (WType.Listα.cons hd) f)),
  (match WType.mk (WType.Listα.cons hd) f with
    | WType.mk WType.Listα.nil f => h_1 f
    | WType.mk (WType.Listα.cons hd) f => h_2 hd f) =
    h_2 hd f
-- Init.Data.List.Basic
List.set.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : ℕ) (x_2 : α),
  x.set x_1 x_2 =
    match x, x_1, x_2 with
    | head :: as, 0, b => b :: as
    | a :: as, n.succ, b => a :: as.set n b
    | [], x, x_3 => []
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.max_prod_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {s : Multiset ι}
  {f g : ι → α}, max (Multiset.map f s).prod (Multiset.map g s).prod ≤ (Multiset.map (fun i => max (f i) (g i)) s).prod
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instAddCommMonoid : {A : Type u_2} →
  {E : Type u_6} →
    [inst : AddMonoid A] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : AddCommMonoid E] → [inst_3 : TopologicalSpace E] → [ContinuousAdd E] → AddCommMonoid (A →ₜ+ E)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mk.sizeOf_spec : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : SizeOf α] (carrier : Set α) (is_open' : IsOpen carrier),
  sizeOf { carrier := carrier, is_open' := is_open' } = 1 + sizeOf is_open'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- The yoneda embedding for `AddMon C` is fully faithful.  -/
CategoryTheory.yonedaAddMonFullyFaithful : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.yonedaAddMon.FullyFaithful
-- Init.Data.Repr
List.repr : {α : Type u_1} → [Repr α] → List α → ℕ → Std.Format
-- Mathlib.Algebra.Algebra.Hom
AlgHom.one_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A), 1 x = x
-- Std.Async.System
Std.Async.System.GroupId.mk.inj : ∀ {toNat toNat_1 : ℕ}, { toNat := toNat } = { toNat := toNat_1 } → toNat = toNat_1
-- Mathlib.Data.Sum.Order
Sum.Lex.not_inr_lt_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a : α} {b : β}, ¬toLex (Sum.inr b) < toLex (Sum.inl a)
-- Mathlib.Data.Option.NAry
Option.map₂_coe_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) (a : α) (b : β),
  Option.map₂ f (some a) (some b) = some (f a b)
-- Mathlib.Data.Finset.Card
Finset.card_filter_eq_iff : ∀ {α : Type u_1} {s : Finset α} {p : α → Prop} [inst : DecidablePred p],
  (Finset.filter p s).card = s.card ↔ ∀ x ∈ s, p x
-- Std.Data.Internal.List.Associative
/-- Returns the smallest key in an associative list or `fallback` if the list is empty.  -/
Std.Internal.List.maxKeyD : {α : Type u} → {β : α → Type v} → [Ord α] → List ((a : α) × β a) → α → α
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- The components of the natural transformation  -/
CategoryTheory.ProfunctorCore.Hom.app : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} →
          P.Hom Q → (X : C) → (Y : D) → P.obj X Y ⟶ Q.obj X Y
-- Mathlib.Topology.Algebra.MulAction
AddSubmonoid.continuousVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : AddMonoid M]
  [inst_3 : AddAction M X] [ContinuousVAdd M X] {S : AddSubmonoid M}, ContinuousVAdd (↥S) X
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- An octahedron' is a type of datum whose existence follows from
the octahedron axiom (TR 4). It is a rotated version of an octahedron.
The input is given by the following diagram:
```
       v₁₂       u₁₃      w₂₃
  Z₁₂ ────> X₁ ─────> X₃ ─────> Z₂₃⟦1⟧
          ^  \       ^  \
      v₁₃/ u₁₂\  u₂₃/    \w₁₃
        /     V    /      V
      Z₁₃       X₂       Z₁₃⟦1⟧
                ^ \
            v₂₃/   \w₁₂
              /     V
           Z₂₃      Z₁₂⟦1⟧
```
where `u₁₂ ≫ u₂₃ = u₁₃` and `(v₁₂,u₁₂,w₁₂), (v₁₃,u₁₃,w₁₃)` and `(v₂₃,u₂₃,w₂₃)`
are distinguished triangles.. An `Octahedron'` for this data consists of
maps `m₁ : Z₁₂ ⟶ Z₁₃` and `m₃ : Z₁₃ ⟶ Z₂₃` such that `(m₁, m₃, v₂₃ ≫ w₁₂)` is
a distinguished triangle and the completed diagram commutes:
```
       v₁₂       u₁₃      w₂₃
  Z₁₂ ────> X₁ ─────> X₃ ─────> Z₂₃⟦1⟧
   \       ^  \       ^  \      ^
  m₁\  v₁₃/ u₁₂\  u₂₃/    \w₁₃ /m₃⟦1⟧'
     V   /     V    /      V  /
      Z₁₃       X₂       Z₁₃⟦1⟧
       \        ^ \      ^
      m₃\   v₂₃/   \w₁₂ /m₁⟦1⟧'
         V    /     V  /
          Z₂₃  ────> Z₁₂⟦1⟧
```
 -/
CategoryTheory.Triangulated.Octahedron' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃ →
                        {v₁₂ : Z₁₂ ⟶ X₁} →
                          {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂} →
                            CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈
                                CategoryTheory.Pretriangulated.distinguishedTriangles →
                              {v₂₃ : Z₂₃ ⟶ X₂} →
                                {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃} →
                                  CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈
                                      CategoryTheory.Pretriangulated.distinguishedTriangles →
                                    {v₁₃ : Z₁₃ ⟶ X₁} →
                                      {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃} →
                                        CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈
                                            CategoryTheory.Pretriangulated.distinguishedTriangles →
                                          Type v_1
-- Lean.Data.Lsp.Internal
/-- Whether setting up the header using `lake setup-file` has failed.  -/
Lean.Lsp.LeanILeanHeaderSetupInfoParams.isSetupFailure : Lean.Lsp.LeanILeanHeaderSetupInfoParams → Bool
-- Mathlib.Geometry.Convex.Hull
Convexity.IsConvexSet.sdiff_singleton_iff_notMem_convexHull : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X} {x : X},
  Convexity.IsConvexSet R s → (Convexity.IsConvexSet R (s \ {x}) ↔ x ∉ (Convexity.convexHull R) (s \ {x}))
-- Init.Data.List.Basic
/-- Returns `true` if `as` and `bs` have the same length and they are pairwise related by `eqv`.

`O(min |as| |bs|)`. Short-circuits at the first non-related pair of elements.

Examples:
* `[1, 2, 3].isEqv [2, 3, 4] (· < ·) = true`
* `[1, 2, 3].isEqv [2, 2, 4] (· < ·) = false`
* `[1, 2, 3].isEqv [2, 3] (· < ·) = false`
 -/
List.isEqv : {α : Type u} → List α → List α → (α → α → Bool) → Bool
-- Init.Data.ByteArray.Lemmas
ByteArray.emptyc_eq_empty : ∅ = ByteArray.empty
-- Init.Data.Vector.Lemmas
Vector.getElem_set!_ne : ∀ {α : Type u_1} {n j i : ℕ} {xs : Vector α n} {x : α} (hj : j < n), i ≠ j → (xs.set! i x)[j] = xs[j]
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_counitIso_hom_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.AddMon C),
  (CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.IsSplitCoequalizer.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (rightSection : Z ⟶ Y) (leftSection : Y ⟶ X)
  (condition :
    autoParam (CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
      CategoryTheory.IsSplitCoequalizer.condition._autoParam)
  (rightSection_π :
    autoParam (CategoryTheory.CategoryStruct.comp rightSection π = CategoryTheory.CategoryStruct.id Z)
      CategoryTheory.IsSplitCoequalizer.rightSection_π._autoParam)
  (leftSection_bottom :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection g = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.IsSplitCoequalizer.leftSection_bottom._autoParam)
  (leftSection_top :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection f = CategoryTheory.CategoryStruct.comp π rightSection)
      CategoryTheory.IsSplitCoequalizer.leftSection_top._autoParam)
  (rightSection_1 : Z ⟶ Y) (leftSection_1 : Y ⟶ X)
  (condition_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
      CategoryTheory.IsSplitCoequalizer.condition._autoParam)
  (rightSection_π_1 :
    autoParam (CategoryTheory.CategoryStruct.comp rightSection_1 π = CategoryTheory.CategoryStruct.id Z)
      CategoryTheory.IsSplitCoequalizer.rightSection_π._autoParam)
  (leftSection_bottom_1 :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection_1 g = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.IsSplitCoequalizer.leftSection_bottom._autoParam)
  (leftSection_top_1 :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection_1 f = CategoryTheory.CategoryStruct.comp π rightSection_1)
      CategoryTheory.IsSplitCoequalizer.leftSection_top._autoParam),
  ({ rightSection := rightSection, leftSection := leftSection, condition := condition, rightSection_π := rightSection_π,
        leftSection_bottom := leftSection_bottom, leftSection_top := leftSection_top } =
      { rightSection := rightSection_1, leftSection := leftSection_1, condition := condition_1,
        rightSection_π := rightSection_π_1, leftSection_bottom := leftSection_bottom_1,
        leftSection_top := leftSection_top_1 }) =
    (rightSection = rightSection_1 ∧ leftSection = leftSection_1)
-- Init.Data.UInt.Lemmas
UInt32.zero_mul : ∀ {a : UInt32}, 0 * a = 0
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.homCategory.ext : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {m n : η ⟶ θ}, (∀ (a : B), m.as.app a = n.as.app a) → m = n
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.IndGroupInst.mk.inj : ∀ {toIndGroupInfo : Lean.Elab.Structural.IndGroupInfo} {levels : List Lean.Level} {params : Array Lean.Expr}
  {toIndGroupInfo_1 : Lean.Elab.Structural.IndGroupInfo} {levels_1 : List Lean.Level} {params_1 : Array Lean.Expr},
  { toIndGroupInfo := toIndGroupInfo, levels := levels, params := params } =
      { toIndGroupInfo := toIndGroupInfo_1, levels := levels_1, params := params_1 } →
    toIndGroupInfo = toIndGroupInfo_1 ∧ levels = levels_1 ∧ params = params_1
-- Init.Control.Lawful.Instances
EStateM.run.eq_1 : ∀ {ε σ α : Type u} (x : EStateM ε σ α) (s : σ), x.run s = x s
-- Lean.Level
Lean.Level.PP.Result.num : ℕ → Lean.Level.PP.Result
-- Std.Data.ExtDHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.
 -/
Std.ExtDHashMap.Const.get? : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {β : Type v} → [EquivBEq α] → [LawfulHashable α] → (Std.ExtDHashMap α fun x => β) → α → Option β
-- Init.Data.BitVec.Lemmas
BitVec.eq_of_toFin_eq : ∀ {w : ℕ} {x y : BitVec w}, x.toFin = y.toFin → x = y
-- Mathlib.RepresentationTheory.Induced
Rep.coinvariantsTensorIndInv_mk_tmul_indMk : ∀ {k : Type u} [inst : CommRing k] {G H : Type u} [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  {A : Rep.{u, u, u} k G} {B : Rep.{u, u, u} k H} (x : ↑A) (y : ↑B),
  (CategoryTheory.ConcreteCategory.hom (Rep.coinvariantsTensorIndInv φ A B))
      ((Representation.Coinvariants.mk (A.ρ.tprod (Rep.res φ B).ρ)) (x ⊗ₜ[k] y)) =
    (((Rep.ind φ A).coinvariantsTensorMk B) ((Representation.IndV.mk φ A.ρ 1) x)) y
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_necessary_assignment : ∀ {n : ℕ} {p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool}
  {c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n}
  {l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)},
  Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c →
    ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval (fun v => if v = l.1 then l.2 else p v) c →
      l.negate ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c
-- Batteries.Data.Nat.Basic
/-- Strong recursor for `Nat`
 -/
Nat.strongRec : {motive : ℕ → Sort u_1} → ((n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) → (t : ℕ) → motive t
-- Mathlib.LinearAlgebra.Vandermonde
/-- The formula for the determinant of a Vandermonde matrix.  -/
Matrix.det_vandermonde : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R), (Matrix.vandermonde v).det = ∏ i, ∏ j > i, (v j - v i)
-- Mathlib.Data.TypeVec
TypeVec.prod_id : ∀ {n : ℕ} {α β : TypeVec.{u} n}, TypeVec.prod.map TypeVec.id TypeVec.id = TypeVec.id
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The full subcategory of bifibrant objects.  -/
HomotopicalAlgebra.BifibrantObject : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] →
      [CategoryTheory.Limits.HasInitial C] →
        [HomotopicalAlgebra.CategoryWithFibrations C] → [CategoryTheory.Limits.HasTerminal C] → Type u
-- Mathlib.Analysis.Convex.Topology
closedConvexHull_closure_eq_closedConvexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {s : Set E},
  (closedConvexHull 𝕜) (closure s) = (closedConvexHull 𝕜) s
-- Mathlib.SetTheory.Lists
Lists'.toList.eq_3 : ∀ {α : Type u_1} (b : Bool) (a : Lists' α b) (l : Lists' α true), (a.cons' l).toList = ⟨b, a⟩ :: l.toList
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.neg` -/
CircleIntegrable.fun_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {c : ℂ} {R : ℝ},
  CircleIntegrable f c R → CircleIntegrable (fun i => -f i) c R
-- Mathlib.Algebra.Order.BigOperators.Ring.List
/-- A variant of `List.prod_pos` for `CanonicallyOrderedAdd`.  -/
CanonicallyOrderedAdd.list_prod_pos : ∀ {α : Type u_2} [inst : CommSemiring α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α]
  [Nontrivial α] {l : List α}, 0 < l.prod ↔ ∀ x ∈ l, 0 < x