mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.JointlySurjective.mk : ∀ {K : CategoryTheory.Precoverage AlgebraicGeometry.Scheme},
  (∀ {X : AlgebraicGeometry.Scheme}, ∀ S ∈ K.coverings X, ∀ (x : ↥X), ∃ Y g, S g ∧ x ∈ Set.range ⇑g) →
    AlgebraicGeometry.Scheme.JointlySurjective K
-- Mathlib.CategoryTheory.Preadditive.LeftExact
/-- A functor between preadditive categories preserves all coequalizers if it preserves all
cokernels.  -/
CategoryTheory.Functor.preservesCoequalizers_of_preservesCokernels : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasBinaryBiproducts C]
  [∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F],
  CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair F
-- Std.Data.HashMap.Basic
/-- Creates a hash map from an array of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.HashMap.ofArray : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Array (α × β) → Std.HashMap α β
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The functor sending an arrow to its target.  -/
CategoryTheory.Arrow.rightFunc : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Arrow C) C
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.leftComp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type w)
  [inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {X Y : C} (Z : C) (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.Linear.leftComp R Z f) g = CategoryTheory.CategoryStruct.comp f g
-- Lean.Message
Lean.MessageData.brecOn_1.go : {motive_1 : Lean.MessageData → Sort u} →
  {motive_2 : Array Lean.MessageData → Sort u} →
    {motive_3 : List Lean.MessageData → Sort u} →
      (t : Array Lean.MessageData) →
        ((t : Lean.MessageData) → t.below → motive_1 t) →
          ((t : Array Lean.MessageData) → Lean.MessageData.below_1 t → motive_2 t) →
            ((t : List Lean.MessageData) → Lean.MessageData.below_2 t → motive_3 t) →
              motive_2 t ×' Lean.MessageData.below_1 t
-- Lean.Meta.PProdN
/-- The value analogue to `PProdN.packLambdas`.

It is the identity if `es.size = 1`.
 -/
Lean.Meta.PProdN.mkLambdas : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.coe_homeoOfIso_symm : ∀ {X Y : AlgebraicGeometry.Scheme} (e : X ≅ Y), ⇑(AlgebraicGeometry.Scheme.homeoOfIso e.symm) = ⇑e.inv
-- Std.Data.HashSet.Basic
Std.HashSet.instSDiff : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → SDiff (Std.HashSet α)
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonAssocSemiring` instance along an injective function.  -/
Function.Injective.nonAssocSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : SMul ℕ S] →
                  [inst_5 : NatCast S] →
                    [inst_6 : NonAssocSemiring R] →
                      f 0 = 0 →
                        f 1 = 1 →
                          (∀ (x y : S), f (x + y) = f x + f y) →
                            (∀ (x y : S), f (x * y) = f x * f y) →
                              (∀ (n : ℕ) (x : S), f (n • x) = n • f x) → (∀ (n : ℕ), f ↑n = ↑n) → NonAssocSemiring S
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.instInitiallySmallOverOfLocallySmall : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.LocallySmall.{w, v, u} J]
  [CategoryTheory.InitiallySmall J] (X : J), CategoryTheory.InitiallySmall (CategoryTheory.Over X)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.bot_eq_zero : ∀ {σ : Type u_1} (m : MonomialOrder σ), ⊥ = 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.writes.eq_6 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Fintype Γ], Turing.TM1to1.writes Turing.TM1.Stmt.halt = ∅
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.congrLeftₗ_apply : ∀ {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₂] (R : Type u_10) (W : Type u_11) [inst_7 : Ring R]
  [inst_8 : AddCommGroup W] [inst_9 : Module k W] [inst_10 : Module R W] [inst_11 : SMulCommClass k R W]
  (e : P₁ ≃ᵃ[k] P₂) (f : P₁ →ᵃ[k] W) (x : P₂), ((AffineEquiv.congrLeftₗ R W e) f) x = f (e.symm x)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instInvCoeOfInvMemClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Inv (R i)] [inst_2 : ∀ (i : ι), InvMemClass (S i) (R i)],
  RestrictedProduct.instInvCoeOfInvMemClass R = { inv := fun x => ⟨fun i => (x i)⁻¹, ⋯⟩ }
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.isEmbedding_singleton : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T0Space α], Topology.IsEmbedding fun x => {x}
-- Init.Internal.Order.Basic
Lean.Order.coind_impl : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] (f₁ f₂ : α → Prop),
  Lean.Order.monotone f₁ → Lean.Order.monotone f₂ → Lean.Order.monotone fun x => f₁ x → f₂ x
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Embeddings of types induce embeddings of complete graphs on those types.  -/
SimpleGraph.Embedding.completeGraph : {α : Type u_5} → {β : Type u_6} → (α ↪ β) → SimpleGraph.completeGraph α ↪g SimpleGraph.completeGraph β
-- Mathlib.Algebra.Group.Defs
zero_add : ∀ {M : Type u} [inst : AddZeroClass M] (a : M), 0 + a = a
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_natural_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (Z₁ Z₂ : C) {X₁ X₂ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Y₁)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₂ Y₂) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ Z₁ Z₂ Y₁ Y₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ Z₁ Z₂ X₁ X₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z₁ f₁)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z₂ f₂))
        h)
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.inhabited : {R : Type u} → [inst : Ring R] → Inhabited (RingTopology R)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.coeFn_mk : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (i : Function.Injective f), ⇑{ toFun := f, inj' := i } = f
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
/-- An open neighborhood of the identity in
the Cartesian product of two nonarchimedean groups contains the Cartesian product of
an open neighborhood in each group.  -/
NonarchimedeanAddGroup.prod_subset : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [NonarchimedeanAddGroup G] {K : Type u_3}
  [inst_3 : AddGroup K] [inst_4 : TopologicalSpace K] [NonarchimedeanAddGroup K] {U : Set (G × K)},
  U ∈ nhds 0 → ∃ V W, ↑V ×ˢ ↑W ⊆ U
-- Mathlib.Data.ENNReal.Inv
ENNReal.half_lt_self : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → a / 2 < a
-- Std.Data.ExtHashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 -/
Std.ExtHashMap.getD : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → α → β → β
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
lTensor.inverse.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g),
  lTensor.inverse Q hfg hg = lTensor.inverse_of_rightInverse Q hfg ⋯
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.empty : ∀ {α : Type u_3} {s : Set (Set α)}, MeasurableSpace.DynkinSystem.GenerateHas s ∅
-- Mathlib.Topology.Algebra.Support
tsupport_comp_subset_preimage : ∀ {X : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : TopologicalSpace X] {Y : Type u_9}
  [inst_2 : TopologicalSpace Y] (g : Y → α) {f : X → Y}, Continuous f → tsupport (g ∘ f) ⊆ f ⁻¹' tsupport g
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_ω₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {D : Type u_3} [inst_7 : CategoryTheory.Category.{v_3, u_3} D] [inst_8 : CategoryTheory.Limits.HasZeroObject D]
  [inst_9 : CategoryTheory.HasShift D ℤ] [inst_10 : CategoryTheory.Preadditive D]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_12 : CategoryTheory.Pretriangulated D]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (F : CategoryTheory.Functor C D) [inst_13 : F.CommShift ℤ]
  [inst_14 : F.IsTriangulated], (X.mapTriangulatedFunctor F).ω₁ = X.ω₁.comp F
-- Init.Data.Dyadic.Instances
Dyadic.instIsCharPOfNatNat : Lean.Grind.IsCharP Dyadic 0
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instIsAlwaysFiniteNat_1 : Std.Rxo.IsAlwaysFinite ℕ
-- Lean.Parser.Term
Lean.Parser.Term.noImplicitLambda.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.SInt.Lemmas
Int32.lt_iff_le_and_ne : ∀ {a b : Int32}, a < b ↔ a ≤ b ∧ a ≠ b
-- Mathlib.Probability.Process.Stopping
/-- Auxiliary lemma for `MeasureTheory.IsStoppingTime.measurableSet_lt`.  -/
MeasureTheory.IsStoppingTime.measurableSet_lt_of_isLUB : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι],
  MeasureTheory.IsStoppingTime f τ → ∀ (i : ι), IsLUB (Set.Iio i) i → MeasurableSet {ω | τ ω < ↑i}
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The `weightedOrder` of the sum of two formal power series
is the minimum of their orders if their orders differ.  -/
MvPowerSeries.weightedOrder_add_of_weightedOrder_ne : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
  MvPowerSeries.weightedOrder w f ≠ MvPowerSeries.weightedOrder w g →
    MvPowerSeries.weightedOrder w (f + g) = min (MvPowerSeries.weightedOrder w f) (MvPowerSeries.weightedOrder w g)
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages commute with addition.  -/
Real.circleAverage_fun_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → E},
  CircleIntegrable f₁ c R →
    CircleIntegrable f₂ c R →
      Real.circleAverage (fun z => f₁ z + f₂ z) c R = Real.circleAverage f₁ c R + Real.circleAverage f₂ c R
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- A finitary (instead of binary) version of `continuous_dom_prod`.  -/
RestrictedProduct.continuous_dom_pi : ∀ {ι : Type u_1} {n : Type u_3} [Finite n] {X : Type u_4} [inst : TopologicalSpace X] {A : n → ι → Type u_5}
  [inst_1 : (j : n) → (i : ι) → TopologicalSpace (A j i)] {C : (j : n) → (i : ι) → Set (A j i)},
  (∀ (j : n) (i : ι), IsOpen (C j i)) →
    ∀ {f : ((j : n) → RestrictedProduct (fun i => A j i) (fun i => C j i) Filter.cofinite) → X},
      Continuous f ↔
        ∀ (S : Set ι) (hS : Filter.cofinite ≤ Filter.principal S),
          Continuous (f ∘ Pi.map fun x => RestrictedProduct.inclusion (A x) (C x) hS)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.prod_eq_prod_mul_prod : ∀ {K : Type u_1} [inst : Field K] {α : Type u_2} [inst_1 : CommMonoid α] [inst_2 : NumberField K]
  (f : NumberField.InfinitePlace K → α), ∏ w, f w = (∏ w, f ↑w) * ∏ w, f ↑w
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.Inv_divided_by_X_pow_order_rightInv : ∀ {k : Type u_2} [inst : Field k] {f : PowerSeries k} (hf : f ≠ 0),
  f.divXPowOrder * PowerSeries.Inv_divided_by_X_pow_order hf = 1
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.List.findSomeM?_cons.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive __do_lift
-- Lean.Environment
Lean.PersistentEnvExtensionDescrCore.addImportedFn : {α β σ : Type} → Lean.PersistentEnvExtensionDescrCore α β σ → Array (Array α) → Lean.ImportM σ
-- Mathlib.Control.Random
/-- Get the range of `Nat` that can be generated by the generator `g`.  -/
Rand.range : {m : Type → Type u_1} → {g : Type} → [RandomGen g] → [Monad m] → RandGT g m (ℕ × ℕ)
-- Init.Data.UInt.Lemmas
USize.toNat_ofNat32 : ∀ {n : ℕ} {h : n < 4294967296}, (USize.ofNat32 n h).toNat = n
-- Mathlib.Order.CountableSupClosed
countableInfClosure_mono : ∀ {α : Type u_2} [inst : Preorder α], Monotone ⇑countableInfClosure
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalenceFunctor_obj_left_as : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G)
  (g : CategoryTheory.StructuredArrow f (CategoryTheory.StructuredArrow.pre e F G)),
  ((CategoryTheory.StructuredArrow.preEquivalenceFunctor F f).obj g).left.as = PUnit.unit
-- Std.Data.String.ToNat
String.isSome_toNat? : ∀ {s : String}, s.toNat?.isSome = s.isNat
-- Init.Data.List.Impl
List.findSome?_singleton : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α}, List.findSome? f [a] = f a
-- Lean.Meta.Tactic.Rewrite
Lean.Meta.RewriteResult.mk.inj : ∀ {eNew eqProof : Lean.Expr} {mvarIds : List Lean.MVarId} {eNew_1 eqProof_1 : Lean.Expr} {mvarIds_1 : List Lean.MVarId},
  { eNew := eNew, eqProof := eqProof, mvarIds := mvarIds } =
      { eNew := eNew_1, eqProof := eqProof_1, mvarIds := mvarIds_1 } →
    eNew = eNew_1 ∧ eqProof = eqProof_1 ∧ mvarIds = mvarIds_1
-- Mathlib.Data.Rel
SetRel.univ_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (S : SetRel β γ), SetRel.comp Set.univ S = {(_b, c) | c ∈ S.cod}
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter!_eq_self_of_not_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      k ∉ t → (f (t.get? k)).isNone = true → (Std.DTreeMap.Internal.Impl.alter! k f t).size = t.size
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertEntryIfNew_le : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  (Std.Internal.List.insertEntryIfNew k v l).length ≤ l.length + 1
-- Mathlib.Order.Filter.CardinalInter
Filter.EventuallyLE.cardinal_bUnion : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {S : Set ι},
  Cardinal.mk ↑S < c →
    ∀ {s t : (i : ι) → i ∈ S → Set α},
      (∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) → ⋃ i, ⋃ (h : i ∈ S), s i h ≤ᶠ[l] ⋃ i, ⋃ (h : i ∈ S), t i h
-- Mathlib.CategoryTheory.Bicategory.SingleObj
CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence_inverse_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y), (CategoryTheory.MonoidalSingleObj.endMonoidalStarFunctorEquivalence C).inverse.map f = f
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.leftAdjointCompNatTrans₀₁₃_eq_conjugateEquiv_symm : ∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₂]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₃] {F₀₁ : CategoryTheory.Functor C₀ C₁}
  {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₁₃ : CategoryTheory.Functor C₁ C₃}
  {F₀₃ : CategoryTheory.Functor C₀ C₃} {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₂₁ : CategoryTheory.Functor C₂ C₁}
  {G₃₂ : CategoryTheory.Functor C₃ C₂} {G₃₁ : CategoryTheory.Functor C₃ C₁} {G₃₀ : CategoryTheory.Functor C₃ C₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₁₃ : F₁₃ ⊣ G₃₁) (adj₀₃ : F₀₃ ⊣ G₃₀)
  (τ₁₂₃ : G₃₁ ⟶ G₃₂.comp G₂₁) (τ₀₁₃ : G₃₀ ⟶ G₃₁.comp G₁₀),
  CategoryTheory.CategoryStruct.comp (F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃))
      (adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃) =
    (CategoryTheory.conjugateEquiv adj₀₃ (adj₀₁.comp (adj₁₂.comp adj₂₃))).symm
      (CategoryTheory.CategoryStruct.comp τ₀₁₃ (CategoryTheory.Functor.whiskerRight τ₁₂₃ G₁₀))
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Binary.parseActions : Std.Internal.Parsec.ByteArray.Parser (Array Std.Tactic.BVDecide.LRAT.IntAction)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_subgroupOf_closure_normalizer : ∀ {G : Type u_1} [inst : Group G] (s : Set G), ((Subgroup.closure s).subgroupOf (Subgroup.normalizer s)).Normal
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.Ioc_subset_uIoc' : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioc a b ⊆ Set.uIoc b a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isEmpty_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.mapCoconeToOver_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F),
  c.mapCoconeToOver.hom.hom = CategoryTheory.CategoryStruct.id c.pt
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_4 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a b : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteS ctx (a.add b) =
    Lean.Grind.CommRing.Expr.denoteS ctx a + Lean.Grind.CommRing.Expr.denoteS ctx b
-- Mathlib.Analysis.Normed.Group.Basic
mem_closedBall_iff_norm_neg_add_le' : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r ↔ ‖-a + b‖ ≤ r
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- Given a monomorphism `f : K ⟶ L` between complexes that are strictly `≥ n₀ + 1`,
this is the limit of the projective system
`cochainComplexFunctor f n₀ : Nᵒᵖ ⥤ CochainComplex C ℤ`: this is the
intermediate object in the factorization lemma `cm5a_cof`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.mid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [CategoryTheory.EnoughInjectives C] →
            [CategoryTheory.Mono f] →
              (n₀ : ℤ) → [K.IsStrictlyGE (n₀ + 1)] → [L.IsStrictlyGE (n₀ + 1)] → CochainComplex C ℤ
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- The length of vertices list equals path length plus one  -/
Quiver.Path.vertices_length : ∀ {V : Type u_2} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), p.vertices.length = p.length + 1
-- Mathlib.Topology.Perfect
PerfectSpace.univ_perfect : ∀ (α : Type u_1) [inst : TopologicalSpace α] [PerfectSpace α], Perfect Set.univ
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.addSubgroup.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (s : UpperSet (FiniteArchimedeanClass M)),
  FiniteArchimedeanClass.addSubgroup s =
    { toAddSubsemigroup := ArchimedeanClass.subsemigroup (FiniteArchimedeanClass.toUpperSetAddArchimedeanClass s),
      zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.RingTheory.NoetherNormalization
/-- `eqv1` is the isomorphism from `k[X_1,...X_n][X]/φ(T(I))`
to `k[X_0,...,X_n]/T(I)`, induced by `φ`.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.eqv1 : {k : Type u_1} →
  [inst : Field k] →
    {n : ℕ} →
      (f : MvPolynomial (Fin (n + 1)) k) →
        (I : Ideal (MvPolynomial (Fin (n + 1)) k)) →
          (Polynomial (MvPolynomial (Fin n) k) ⧸
              Ideal.map (MvPolynomial.finSuccEquiv k n) (Ideal.map (NoetherNormalization.T✝ f) I)) ≃ₐ[k]
            MvPolynomial (Fin (n + 1)) k ⧸ Ideal.map (NoetherNormalization.T✝ f) I
-- Mathlib.Algebra.Group.Defs
mul_left_inj : ∀ {G : Type u_1} [inst : Mul G] [IsRightCancelMul G] (a : G) {b c : G}, b * a = c * a ↔ b = c
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- The formal multilinear series where all terms of positive degree are equal to zero, and the term
of degree zero is `c`. It is the power series expansion of the constant function equal to `c`
everywhere.  -/
constFormalMultilinearSeries : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (E : Type u_2) →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          [inst_3 : ContinuousConstSMul 𝕜 E] →
            [inst_4 : IsTopologicalAddGroup E] →
              {F : Type u_3} →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : IsTopologicalAddGroup F] →
                    [inst_7 : NormedSpace 𝕜 F] → [inst_8 : ContinuousConstSMul 𝕜 F] → F → FormalMultilinearSeries 𝕜 E F
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_tsum_le : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] (f : ι → M),
  ‖∑' (i : ι), f i‖ ≤ ⨆ i, ‖f i‖
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_range : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] (f : α → ZFSet.{u}), (ZFSet.range f).rank = ⨆ i, Order.succ (f i).rank
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The "unlifted" version of taking inverses in the colimit.  -/
GrpCat.FilteredColimits.colimitInvAux : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J GrpCat) → (j : J) × ↑(F.obj j) → ↑(GrpCat.FilteredColimits.G F)
-- Mathlib.Topology.Algebra.Constructions
/-- The units of a monoid are equipped with a topology, via the embedding into `M × M`.  -/
Units.instTopologicalSpaceUnits : {M : Type u_1} → [TopologicalSpace M] → [inst : Monoid M] → TopologicalSpace Mˣ
-- Mathlib.Analysis.Real.Hyperreal
/-- A sample infinite hyperreal ω = ⟦(0, 1, 2, 3, ⋯)⟧. 

Conventions for notations in identifiers:

 * The recommended spelling of `ω` in identifiers is `omega`. -/
Hyperreal.termω : Lean.ParserDescr
-- Mathlib.Topology.Inseparable
not_inseparable_iff_exists_open : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, ¬Inseparable x y ↔ ∃ s, IsOpen s ∧ Xor (x ∈ s) (y ∈ s)