mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Matrix.Order
_private.Mathlib.Analysis.Matrix.Order.0.Matrix.le_antisymm_aux : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] {A : Matrix n n 𝕜}, A.PosSemidef → (-A).PosSemidef → A = 0
-- Mathlib.Logic.Equiv.Defs
/-- `Function.swap` as an equivalence.  -/
Equiv.functionSwap : (α : Sort u_1) → (β : Sort u_2) → (γ : α → β → Sort u_3) → ((a : α) → (b : β) → γ a b) ≃ ((b : β) → (a : α) → γ a b)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.ComonObj A]
  {X Y : C} (f : X ⟶ Y), ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObj A).map f).hom = A.map f
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.coe_hom : ∀ {V : Type u} {G : SimpleGraph V} (x : G.Subgraph), ⇑x.hom = fun v => ↑v
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k k' : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).getKey? k' =
    if cmp k k' = Ordering.eq then if k ∈ t then some k else none else t.getKey? k'
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzWith_iff_norm_neg_add_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F} {C : NNReal},
  LipschitzWith C f ↔ ∀ (x y : E), ‖-f x + f y‖ ≤ ↑C * ‖-x + y‖
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_eq_get! : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] [inst_3 : Inhabited β], m.WF → ∀ {a : α}, Std.DHashMap.Raw.Const.get! m a = m.get! a
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W)
  (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inl)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (hP.desc h k w)) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q h
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ = o(1)`.  -/
FormalMultilinearSeries.isLittleO_one_of_lt_radius : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
  ↑r < p.radius → (fun n => ‖p n‖ * ↑r ^ n) =o[Filter.atTop] fun x => 1
-- Mathlib.Data.Finsupp.Multiset
Multiset.toFinsupp_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), Multiset.toFinsupp {a} = fun₀ | a => 1
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.eventually_le_mul : ∀ {u : ℕ → EReal} {a : EReal}, LinearGrowth.linearGrowthSup u < a → ∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ a * ↑n
-- Mathlib.Data.List.Rotate
List.length_rotate : ∀ {α : Type u} (l : List α) (n : ℕ), (l.rotate n).length = l.length
-- Mathlib.Logic.Equiv.Prod
Equiv.coe_prodComm : ∀ (α : Type u_9) (β : Type u_10), ⇑(Equiv.prodComm α β) = Prod.swap
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move_right_n_head : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (T : Turing.Tape Γ) (i : ℕ),
  ((Turing.Tape.move Turing.Dir.right)^[i] T).head = T.nth ↑i
-- Mathlib.Order.ModularLattice
IsModularLattice.exists_disjoint_and_sup_eq : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a b : α} [inst_2 : BoundedOrder α] [ComplementedLattice α],
  a ≤ b → ∃ a', Disjoint a a' ∧ a ⊔ a' = b
-- Mathlib.CategoryTheory.Shift.Pullback
/-- The functor `F`, seen as a functor from `PullbackShift C φ` to `PullbackShift D φ`.
Then a `CommShift B` instance on `F` will define a `CommShift A` instance on
`PullbackShift.functor F φ`, and we won't have to juggle with two `CommShift` instances
on `F`.
 -/
CategoryTheory.PullbackShift.functor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) →
                {D : Type u_4} →
                  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] →
                    [inst_5 : CategoryTheory.HasShift D B] →
                      CategoryTheory.Functor C D →
                        CategoryTheory.Functor (CategoryTheory.PullbackShift C φ) (CategoryTheory.PullbackShift D φ)
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.inf_dom_left : ∀ {α : Type ua} {β : Type ub} {f : α → β} {u₁ u₂ : UniformSpace α} {u₃ : UniformSpace β},
  UniformContinuous f → UniformContinuous f
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- If the neighborhoods of every point for a given topology are defined by a valuation `v`
compatible with the valuative relation, then the topology is a valuative topology.  -/
IsValuativeTopology.of_mem_nhds_iff_vle : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_3 : TopologicalSpace R] (v : Valuation R Γ₀) [v.Compatible],
  (∀ {s : Set R} {x : R}, s ∈ nhds x ↔ ∃ γ, {z | v.restrict (z - x) < ↑γ} ⊆ s) → IsValuativeTopology R
-- Mathlib.Algebra.Module.Projective
LinearMap.exists_rightInverse_of_surjective : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Module.Projective R P] (f : M →ₗ[R] P),
  f.range = ⊤ → ∃ g, f ∘ₗ g = LinearMap.id
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.comp_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  {ψ₁ ψ₂ : S₂ ⟶ S₃} (h' : CategoryTheory.ShortComplex.Homotopy ψ₁ ψ₂),
  (h.comp h').h₂ = CategoryTheory.CategoryStruct.comp h.h₂ ψ₁.τ₂ + CategoryTheory.CategoryStruct.comp φ₂.τ₃ h'.h₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {h : k ∈ Std.DTreeMap.Raw.Const.unitOfList l cmp},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.unitOfList l cmp) k h = ()
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vsub_subset_vsub_left : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t₁ t₂ : Set β}, t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.IsImage s t
-- Mathlib.Geometry.Euclidean.Volume.Measure
Submodule.measurePreserving_measurableEquivProd : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MetricSpace P]
  [inst_6 : MeasurableSpace P] [inst_7 : BorelSpace P] [inst_8 : NormedAddTorsor V P] (s : Submodule ℝ V) (p : P),
  MeasureTheory.MeasurePreserving (⇑(s.measurableEquivProd p))
    (MeasureTheory.Measure.euclideanHausdorffMeasure (Module.finrank ℝ V)) MeasureTheory.volume
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp.injEq : ∀ (e : Lean.Expr) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁) (η θ : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (e_1 : Lean.Expr) (f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁)
  (η_1 θ_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e f g h η θ =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.comp e_1 f_1 g_1 h_1 η_1 θ_1) =
    (e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1 ∧ θ = θ_1)
-- Mathlib.Data.Real.Basic
Real.leTotal_R : Std.Total fun x1 x2 => x1 ≤ x2
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toList_iter : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β}, m.iter.toList = m.toList
-- Mathlib.Algebra.Ring.Parity
Nat.not_even_iff_odd : ∀ {n : ℕ}, ¬Even n ↔ Odd n
-- Lean.Declaration
Lean.mkRecursorValEx : Lean.Name →
  List Lean.Name → Lean.Expr → List Lean.Name → ℕ → ℕ → ℕ → ℕ → List Lean.RecursorRule → Bool → Bool → Lean.RecursorVal
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.isLocalization_leftAdjoint' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  [F.Full] [F.Faithful] (adj : G ⊣ F),
  G.IsLocalization ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G)
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.succ_lt : ∀ {α : Type u_1} {a b : α} [inst : PartialOrder α] [inst_1 : SuccOrder α],
  Order.IsSuccPrelimit b → a < b → Order.succ a < b
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom_map_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X₀ W₀ : C₀}
  (a : W₀ ⟶ X₀) {i : (data (F.obj X₀)).I₀} (p : F.obj W₀ ⟶ F.obj ((data (F.obj X₀)).X i)),
  CategoryTheory.CategoryStruct.comp p ((data (F.obj X₀)).f i) = F.map a →
    ∀ {Z : A} (h : G₀.obj.obj (Opposite.op W₀) ⟶ Z),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjObjIso.hom data G₀ X₀)
          (CategoryTheory.CategoryStruct.comp (G₀.obj.map a.op) h) =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ (F.obj X₀) i)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ p) h)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.get?_nil : ∀ {α : Type u} (n : ℕ), Stream'.Seq.nil.get? n = none
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- A modification `Γ` between lax natural transformations `η` and `θ` (between oplax functors)
consists of a family of 2-morphisms `Γ.app a : η.app a ⟶ θ.app a`, which satisfies the equation
`(app a ▷ G.map f) ≫ θ.naturality f = η.naturality f ≫ (F.map f ◁ app b)`
for each 1-morphism `f : a ⟶ b`.
 -/
CategoryTheory.Oplax.LaxTrans.Modification : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.range_eq_top : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_7} [inst_1 : AddGroup N] {f : G →+ N},
  f.range = ⊤ ↔ Function.Surjective ⇑f
-- Init.Data.List.Lemmas
List.splitAt.go.eq_def : ∀ {α : Type u} (l a : List α) (a_1 : ℕ) (a_2 : List α),
  List.splitAt.go l a a_1 a_2 =
    match a, a_1, a_2 with
    | [], x, x_1 => (l, [])
    | x :: xs, n.succ, acc => List.splitAt.go l xs n (x :: acc)
    | xs, x, acc => (acc.reverse, xs)
-- Init.Data.BitVec.Basic
/-- Checks whether the negation of a bitvector results in overflow.

For a bitvector `x` with nonzero width, this only happens if `x = intMin`.

SMT-Lib name: `bvnego`.
 -/
BitVec.negOverflow : {w : ℕ} → BitVec w → Bool
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atBot_of_monotone_of_subseq : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [inst : Preorder ι] [inst_1 : Preorder α] {u : ι → α} {φ : ι' → ι},
  Monotone u →
    ∀ {l : Filter ι'} [l.NeBot], Filter.Tendsto (u ∘ φ) l Filter.atBot → Filter.Tendsto u Filter.atBot Filter.atBot
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.section_comp_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy),
  CategoryTheory.CategoryStruct.comp ed.section_ X.hom =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.SimplicialObject.const C).obj X.right)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.codomain_eq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ], p.obj b = S
-- Mathlib.Algebra.Ring.Shrink
Shrink.instCommRing : {α : Type u_1} → [inst : Small.{v, u_1} α] → [CommRing α] → CommRing (Shrink.{v, u_1} α)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- the codiagonal of the (pre)cylinder  -/
HomotopicalAlgebra.Precylinder.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {A : C} → (self : HomotopicalAlgebra.Precylinder A) → self.I ⟶ A
-- Mathlib.Data.List.AList
AList.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : AList β),
  AList.insert a b s = { entries := List.kinsert a b s.entries, nodupKeys := ⋯ }
-- Mathlib.Order.WithBot
WithBot.le_unbotA : ∀ {α : Type u_1} [inst : PartialOrder α] {y : WithBot α} {b : α} [inst_1 : Nonempty α], ↑b ≤ y → b ≤ y.unbotA
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mk.injEq : ∀ {M : Type u_1} [inst : MulOneClass M] (toSubmonoid : Submonoid M) (mulSaturated : toSubmonoid.MulSaturated)
  (toSubmonoid_1 : Submonoid M) (mulSaturated_1 : toSubmonoid_1.MulSaturated),
  ({ toSubmonoid := toSubmonoid, mulSaturated := mulSaturated } =
      { toSubmonoid := toSubmonoid_1, mulSaturated := mulSaturated_1 }) =
    (toSubmonoid = toSubmonoid_1)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- A functor preserves the right homology of a short complex `S` if it preserves all the
right homology data of `S`.  -/
CategoryTheory.Functor.PreservesRightHomologyOf : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → CategoryTheory.ShortComplex C → Prop
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] {P Q : CategoryTheory.Functor Cᵒᵖ A} (g : P ⟶ Q)
  (X : C) (x : Φ.fiber.obj X),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x P) (Φ.presheafFiber.map g) =
    CategoryTheory.CategoryStruct.comp (g.app (Opposite.op X)) (Φ.toPresheafFiber X x Q)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.iInf : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : ConditionallyCompleteLattice M] {ι : Sort u_3} [Nonempty ι]
  [Finite ι] {f : ι → α → M},
  (∀ (i : ι), Function.HasFiniteSupport (f i)) → Function.HasFiniteSupport fun a => ⨅ i, f i a
-- Aesop.Frontend.Tactic
Aesop.Frontend.Parser.«tactic_clause(Erase_)» : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The `GradedObject.BifunctorComp₂₃IndexData` which arises from complex shapes.  -/
ComplexShape.ρ₂₃ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {I₁₂ : Type u_4} →
        {I₂₃ : Type u_5} →
          {J : Type u_6} →
            (c₁ : ComplexShape I₁) →
              (c₂ : ComplexShape I₂) →
                (c₃ : ComplexShape I₃) →
                  (c₁₂ : ComplexShape I₁₂) →
                    (c₂₃ : ComplexShape I₂₃) →
                      (c : ComplexShape J) →
                        [inst : TotalComplexShape c₁ c₂ c₁₂] →
                          [inst_1 : TotalComplexShape c₁₂ c₃ c] →
                            [inst_2 : TotalComplexShape c₂ c₃ c₂₃] →
                              [inst_3 : TotalComplexShape c₁ c₂₃ c] →
                                [c₁.Associative c₂ c₃ c₁₂ c₂₃ c] →
                                  CategoryTheory.GradedObject.BifunctorComp₂₃IndexData (c₁.r c₂ c₃ c₁₂ c)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_one_iff : ∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] {f : α → E} {l : Filter α}
  [inst_2 : One F] [NormOneClass F],
  (f =O[l] fun _x => 1) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x‖
-- Mathlib.Data.Countable.Defs
/-- A type `α` is uncountable if it is not countable.  -/
Uncountable.not_countable : ∀ {α : Sort u_1} [self : Uncountable α], ¬Countable α
-- Mathlib.Algebra.Group.Prod
MonoidHom.inl.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.inl M N = { toFun := fun x => (x, 1), map_one' := ⋯, map_mul' := ⋯ }
-- Init.Data.BitVec.Bitblast
/-- Given a `BitVec (len * w)` of `len` flattened `w`-long words,
construct a binary tree that sums two-by-two the `w`-long words in the previous layer,
ultimately returning a single `w`-long words corresponding to the whole addition.
 -/
BitVec.cpopTree : {len w : ℕ} → BitVec (len * w) → BitVec w
-- Init.Data.List.MinMaxOn
List.maxOn?_replicate : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {n : ℕ} {a : α}
  {f : α → β}, List.maxOn? f (List.replicate n a) = if n = 0 then none else some a
-- Mathlib.Algebra.Category.MonCat.Adjunctions
/-- The free functor `Type u ⥤ AddMonCat` sending a type `X` to the free additive monoid on `X`.  -/
AddMonCat.free : CategoryTheory.Functor (Type u) AddMonCat
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.then_lt : ∀ (o : Ordering), ¬o.then Ordering.lt = Ordering.eq
-- Mathlib.Analysis.Normed.Module.Normalize
/-- **Alias** of the reverse direction of `NormedSpace.norm_normalize_eq_one_iff`. -/
NormedSpace.norm_normalize : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {x : V}, x ≠ 0 → ‖NormedSpace.normalize x‖ = 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
vectorSpan_eq_bot_iff_subsingleton : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : Set P}, vectorSpan k s = ⊥ ↔ s.Subsingleton
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.Iterators.Types.Append.instIterator.match_1.eq_1 : ∀ {m : Type u_1 → Type u_2} {β α₁ : Type u_1} [inst : Std.Iterator α₁ m β] (it₁ : Std.IterM m β)
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (out : β)
  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₁' out, h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₁' out h
-- Lean.Data.SMap
Lean.SMap.contains : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → α → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.σ_apply : ∀ {n d : ℕ} (x : (SSet.stdSimplex.obj { len := n }).obj (Opposite.op { len := d })) (i : Fin (d + 1)) (j : Fin (d + 2)),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (SSet.stdSimplex.obj { len := n }) i)) x) j =
    x (i.predAbove j)
-- Init.Data.String.Basic
ByteArray.isSome_utf8Decode?_iff : ∀ {b : ByteArray}, b.utf8Decode?.isSome = true ↔ b.IsValidUTF8
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.instHasBinaryBiproductOppositeXOp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c)
  [∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] (i : α),
  CategoryTheory.Limits.HasBinaryBiproduct (K.op.X i) (K.op.X i)
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instCompleteSemilatticeSup : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → CompleteSemilatticeSup (TwoSidedIdeal R)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_compl : ∀ {ι : Type u_3} [Finite ι] {s : Set (ι → ℕ)}, IsSemilinearSet s → IsSemilinearSet sᶜ
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.mem_unitaryGroup_iff : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  {A : Matrix n n α}, A ∈ Matrix.unitaryGroup n α ↔ A * star A = 1
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.mapCompIso.eq_1 : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} (α : F ⟶ G)
  (β : G ⟶ H),
  CategoryTheory.Pseudofunctor.CoGrothendieck.mapCompIso α β =
    CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin_self_inter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {x : α}, s ∈ nhdsWithin x (s ∩ t)
-- Mathlib.Testing.Plausible.Functions
/-- A list, in decreasing order, of sizes that should be
sliced off a list of length `n`
 -/
Plausible.InjectiveFunction.sliceSizes : ℕ → MLList Id ℕ+
-- Mathlib.Algebra.Group.Defs
AddCommGroup.toAddCancelCommMonoid.eq_1 : ∀ {G : Type u_1} [inst : AddCommGroup G],
  AddCommGroup.toAddCancelCommMonoid = { toAddMonoid := inst.toAddMonoid, add_comm := ⋯, toIsLeftCancelAdd := ⋯ }
-- Mathlib.Analysis.Distribution.Support
Distribution.dsupport_subset_dsupport : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f g : F → V},
  (∀ (s : Set α), IsOpen s → Distribution.IsVanishingOn g s → Distribution.IsVanishingOn f s) →
    Distribution.dsupport f ⊆ Distribution.dsupport g
-- Mathlib.Data.Fintype.OfMap
Fintype.instPEmpty : Fintype PEmpty.{u_4 + 1}
-- Mathlib.CategoryTheory.IsConnected
/-- Any equivalence relation containing (⟶) holds for all pairs of a connected category.  -/
CategoryTheory.equiv_relation : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J] (r : J → J → Prop),
  Equivalence r → (∀ {j₁ j₂ : J} (x : j₁ ⟶ j₂), r j₁ j₂) → ∀ (j₁ j₂ : J), r j₁ j₂
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.Fibration.mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
  {inst_1 : HomotopicalAlgebra.CategoryWithFibrations C} [self : HomotopicalAlgebra.Fibration f],
  HomotopicalAlgebra.fibrations C f