mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.ByteArray.Bootstrap
_private.Init.Data.ByteArray.Bootstrap.0.List.toByteArray.match_1.splitter : (motive : List UInt8 → ByteArray → Sort u_1) →
  (x : List UInt8) →
    (x_1 : ByteArray) →
      ((r : ByteArray) → motive [] r) →
        ((b : UInt8) → (bs : List UInt8) → (r : ByteArray) → motive (b :: bs) r) → motive x x_1
-- Mathlib.Algebra.GCDMonoid.Basic
isGCDMonoid_iff_exists_lcm : ∀ {α : Type u_2} [inst : CommMonoidWithZero α],
  IsGCDMonoid α ↔ IsCancelMulZero α ∧ ∀ (a b : α), ∃ c, ∀ (d : α), a ∣ d ∧ b ∣ d ↔ c ∣ d
-- Mathlib.CategoryTheory.Square
/-- The category of commutative squares in a category.  -/
CategoryTheory.Square : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton : ∀ {α : Type u_1} {G : SimpleGraph α},
  G.EdgeDisjointTriangles ↔ ∀ ⦃e : Sym2 α⦄, ¬e.IsDiag → {s | s ∈ G.cliqueSet 3 ∧ e ∈ s.sym2}.Subsingleton
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.popObjectFieldKey! : Lean.Json.CompressWorkItemQueue✝ → String × Lean.Json.CompressWorkItemQueue✝
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.naturality_app : ∀ {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 G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (T : F ⟶ G) (Z : D) {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.map f).app Z) ((T.app Y).app Z) =
    CategoryTheory.CategoryStruct.comp ((T.app X).app Z) ((G.map f).app Z)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (Z : C) (n : ℕ),
  CategoryTheory.Injective ((CategoryTheory.InjectiveResolution.ofCocomplex Z).X n)
-- Mathlib.Logic.Equiv.Prod
Equiv.prodPProd_apply : ∀ {α₂ : Sort u_3} {β₂ : Sort u_6} {α₁ : Type u_9} {β₁ : Type u_10} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a : α₁ × β₁),
  (ea.prodPProd eb) a = ⟨ea a.1, eb a.2⟩
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- A set of generators of an additive free group, chosen arbitrarily  -/
IsFreeAddGroup.Generators : (G : Type u_1) → [inst : AddGroup G] → [IsFreeAddGroup G] → Type u_1
-- Init.Data.Iterators.Consumers.Monadic.Total
Std.IterM.Total.mk.injEq : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} (it it_1 : Std.IterM m β),
  ({ it := it } = { it := it_1 }) = (it = it_1)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.down_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.WithTerminal.down (CategoryTheory.CategoryStruct.id (CategoryTheory.WithTerminal.of X)) =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Topology.FiberBundle.Constructions
FiberBundle.prod_trivializationAt' : ∀ {B : Type u_1} [inst : TopologicalSpace B] (F₁ : Type u_2) [inst_1 : TopologicalSpace F₁] (E₁ : B → Type u_3)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_4) [inst_3 : TopologicalSpace F₂]
  (E₂ : B → Type u_5) [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_5 : (x : B) → Zero (E₁ x)]
  [inst_6 : (x : B) → Zero (E₂ x)] [inst_7 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_8 : (x : B) → TopologicalSpace (E₂ x)] [inst_9 : FiberBundle F₁ E₁] [inst_10 : FiberBundle F₂ E₂] (b : B),
  FiberBundle.trivializationAt' b = (trivializationAt F₁ E₁ b).prod (trivializationAt F₂ E₂ b)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_spanning_iff : ∀ {α : Type u_1} {M : Matroid α} {X C : Set α},
  autoParam (C ⊆ M.E) Matroid.contract_spanning_iff._auto_1 →
    ((M.contract C).Spanning X ↔ M.Spanning (X ∪ C) ∧ Disjoint X C)
-- Mathlib.CategoryTheory.Preadditive.Projective.Preserves
CategoryTheory.Functor.preservesProjectiveObjects_of_isEquivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [F.IsEquivalence], F.PreservesProjectiveObjects
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `HasDerivWithinAt.fun_finsetProd`. -/
HasDerivWithinAt.fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι]
  {𝔸' : Type u_3} [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'}
  {f' : ι → 𝔸'},
  (∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) →
    HasDerivWithinAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x
-- Init.Data.String.Substring
/-- Returns the next position in a substring after the given position. If the position is at the end of
the substring, it is returned unmodified.

Both the input position and the returned position are interpreted relative to the substring's start
position, not the underlying string.
 -/
Substring.Raw.next : Substring.Raw → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Topology.Separation.Basic
Topology.IsInducing.r1Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [R1Space X] [inst_2 : TopologicalSpace Y] {f : Y → X},
  Topology.IsInducing f → R1Space Y
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_def : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α),
  omegaLimit f ϕ s = ⋂ u ∈ f, closure (Set.image2 ϕ u s)
-- Mathlib.ModelTheory.Equivalence
/-- `φ ⟹[T] ψ` indicates that `φ` implies `ψ` in models of `T`.  -/
FirstOrder.Language.Theory.Imp : {L : FirstOrder.Language} → {α : Type w} → {n : ℕ} → L.Theory → L.BoundedFormula α n → L.BoundedFormula α n → Prop
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_iInf : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → Submonoid N),
  Submonoid.comap f (iInf s) = ⨅ i, Submonoid.comap f (s i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_zsmul_toReal_eq_two_mul : ∀ {θ : Real.Angle}, (2 • θ).toReal = 2 * θ.toReal ↔ θ.toReal ∈ Set.Ioc (-Real.pi / 2) (Real.pi / 2)
-- Mathlib.Analysis.Normed.Algebra.GelfandFormula
/-- **Gelfand's formula**: Given an element `a : A` of a complex Banach algebra, the
`spectralRadius` of `a` is the limit of the sequence `‖a ^ n‖₊ ^ (1 / n)`.  -/
spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius : ∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] (a : A),
  Filter.Tendsto (fun n => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) Filter.atTop (nhds (spectralRadius ℂ a))
-- Mathlib.Algebra.Group.Center
Set.centralizer_empty : ∀ {M : Type u_1} [inst : Mul M], ∅.centralizer = ⊤
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.ae_le_toMeasurable : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  s ≤ᵐ[μ] MeasureTheory.toMeasurable μ s
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xPrevIso.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j), C.xPrevIso r = CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.MvPolynomial.Basic
/-- Multivariate polynomial, where `σ` is the index set of the variables and
`R` is the coefficient ring  -/
MvPolynomial : Type u_1 → (R : Type u_2) → [CommSemiring R] → Type (max u_2 u_1)
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.isUnit : ∀ {M : Type u_6} [inst : Monoid M] {x : M}, IsOfFinOrder x → IsUnit x
-- Init.Prelude
/-- Lifts a function from an underlying type to a function on a quotient, requiring that it respects the
quotient's relation.

Given a relation `r : α → α → Prop` and a quotient `Quot r`, applying a function `f : α → β`
requires a proof `a` that `f` respects `r`. In this case, `Quot.lift f a : Quot r → β` computes the
same values as `f`.

Lean's type theory includes a [definitional reduction](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=type-theory) from
`Quot.lift f h (Quot.mk r v)` to `f v`.

`Quot.lift` is a built-in primitive:
 * `Quot` is the built-in quotient type.
 * `Quot.mk` places elements of the underlying type `α` into the quotient.
 * `Quot.sound` asserts the equality of elements related by `r`
 * `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
   with `Quot.mk`; it is analogous to the [recursor](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=recursors) for a
   structure.
 -/
Quot.lift : {α : Sort u} → {r : α → α → Prop} → {β : Sort v} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β
-- Mathlib.Tactic.TermCongr
/-- For error reporting purposes, make the hole pretty print as its value.
We can still see that it is a hole in the info view on mouseover.  -/
Mathlib.Tactic.TermCongr.unexpandCHole : Lean.PrettyPrinter.Unexpander
-- Init.Data.SInt.Lemmas
ISize.ofInt_neg : ∀ (a : ℤ), ISize.ofInt (-a) = -ISize.ofInt a
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.integral_binomial : ∀ {n : ℕ} {p : ↑unitInterval} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  (f : ℕ → E),
  ∫ (x : ℕ), f x ∂ProbabilityTheory.binomial n p = ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f k
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- The lattice of submodules of a module over a division ring is atomistic.  -/
instIsAtomisticSubmodule : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  IsAtomistic (Submodule K V)
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNonUnitalSemiring : {R : Type u_1} → [NonUnitalSemiring R] → NonUnitalSemiring Rᵃᵒᵖ
-- Init.Data.List.MinMaxOn
List.maxOn?_id : ∀ {α : Type u_1} [inst : Max α] [inst_1 : LE α] [inst_2 : DecidableLE α] [Std.LawfulOrderLeftLeaningMax α]
  {xs : List α}, List.maxOn? id xs = xs.max?
-- Mathlib.Topology.Category.TopCat.ULift
TopCat.instFaithfulUliftFunctor : TopCat.uliftFunctor.Faithful
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueSet_zero : ∀ {α : Type u_1} (G : SimpleGraph α), G.cliqueSet 0 = {∅}
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- the index type of the covering of `S`  -/
CategoryTheory.PreZeroHypercover.I₀ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S : C} → CategoryTheory.PreZeroHypercover S → Type w
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.IsStrongLimit.isSuccLimit : ∀ {c : Cardinal.{u_1}}, c.IsStrongLimit → Order.IsSuccLimit c
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.responseBody : {β : Type} → Option Std.Http.Chunk → Std.Http.Server.Connection.Recv✝ β
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.SignedMeasure.im_toComplexMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (s t : MeasureTheory.SignedMeasure α),
  MeasureTheory.ComplexMeasure.im (s.toComplexMeasure t) = t
-- Mathlib.Util.FormatTable
instBEqAlignment : BEq Alignment
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_comp_inv_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f CategoryTheory.GrpObj.inv) f)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A) CategoryTheory.MonObj.one
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_C : ∀ {R : Type u} [inst : Semiring R] {a : R}, a ≠ 0 → (Polynomial.C a).support = {0}
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᴹᵒᵖ} {f : X ⟶ Y} {g : Y ⟶ Z},
  (CategoryTheory.CategoryStruct.comp f g).unmop = CategoryTheory.CategoryStruct.comp f.unmop g.unmop
-- Mathlib.Algebra.Group.Action.Faithful
/-- `instSMulOfMul` is faithful when multiplication is right cancellative.  -/
instFaithfulSMulOfIsRightCancelMul : ∀ (R : Type u_4) [inst : Mul R] [IsRightCancelMul R], FaithfulSMul R R
-- Mathlib.CategoryTheory.Localization.Trifunctor
CategoryTheory.Localization.instLifting₃Lift₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_6} →
        {D₂ : Type u_7} →
          {D₃ : Type u_8} →
            {E : Type u_13} →
              [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_6} D₁] →
                      [inst_4 : CategoryTheory.Category.{v_5, u_7} D₂] →
                        [inst_5 : CategoryTheory.Category.{v_6, u_8} D₃] →
                          [inst_6 : CategoryTheory.Category.{v_13, u_13} E] →
                            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) →
                              {W₁ : CategoryTheory.MorphismProperty C₁} →
                                {W₂ : CategoryTheory.MorphismProperty C₂} →
                                  {W₃ : CategoryTheory.MorphismProperty C₃} →
                                    (hF : W₁.IsInvertedBy₃ W₂ W₃ F) →
                                      (L₁ : CategoryTheory.Functor C₁ D₁) →
                                        (L₂ : CategoryTheory.Functor C₂ D₂) →
                                          (L₃ : CategoryTheory.Functor C₃ D₃) →
                                            [inst_7 : L₁.IsLocalization W₁] →
                                              [inst_8 : L₂.IsLocalization W₂] →
                                                [inst_9 : L₃.IsLocalization W₃] →
                                                  [inst_10 : W₁.ContainsIdentities] →
                                                    [inst_11 : W₂.ContainsIdentities] →
                                                      [inst_12 : W₃.ContainsIdentities] →
                                                        CategoryTheory.Localization.Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F
                                                          (CategoryTheory.Localization.lift₃ F hF L₁ L₂ L₃)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.insertManyIfNewUnit_cons : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k : α},
  Std.ExtDTreeMap.Const.insertManyIfNewUnit t (k :: l) =
    Std.ExtDTreeMap.Const.insertManyIfNewUnit (t.insertIfNew k ()) l
-- Mathlib.Algebra.Order.Module.Rat
PosSMulStrictMono.nnrat_of_rat : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : MulAction ℚ≥0 α] [inst_2 : MulAction ℚ α] [IsScalarTower ℚ≥0 ℚ α]
  [PosSMulStrictMono ℚ α], PosSMulStrictMono ℚ≥0 α
-- Batteries.Data.List.Perm
List.subperm_of_subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Nodup → l₁ ⊆ l₂ → l₁.Subperm l₂
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Unlike for the binary tensor product, we require `R` to be a `CommRing` here, otherwise
this is false in the case where `ι` is empty.  -/
PiTensorProduct.instAddCommGroup : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {s : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommGroup (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] → AddCommGroup (PiTensorProduct R fun i => s i)
-- Lean.Server.FileWorker.SignatureHelp
_private.Lean.Server.FileWorker.SignatureHelp.0.Lean.Server.FileWorker.SignatureHelp.lineCommentPosition? : (s : String) → Option s.Pos
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- A natural transformation `R₁ ⟶ R₂` induces a functor `P.Comma L R₁ Q W ⥤ P.Comma L R₂ Q W`.  -/
CategoryTheory.MorphismProperty.Comma.mapRight : {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) →
              {P : CategoryTheory.MorphismProperty T} →
                {Q : CategoryTheory.MorphismProperty A} →
                  {W : CategoryTheory.MorphismProperty B} →
                    [inst_3 : Q.IsMultiplicative] →
                      [inst_4 : W.IsMultiplicative] →
                        {R₁ R₂ : CategoryTheory.Functor B T} →
                          (r : R₁ ⟶ R₂) →
                            (∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
                                P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right))) →
                              CategoryTheory.Functor (CategoryTheory.MorphismProperty.Comma L R₁ P Q W)
                                (CategoryTheory.MorphismProperty.Comma L R₂ P Q W)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.coe_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.PositiveCompacts α), ↑s.toCompacts = ↑s
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank function for a proper pairing of a subcomplex of a
simplicial set, this is the coproduct of the horns corresponding to
all cells of rank `j`.  -/
SSet.Subcomplex.Pairing.RankFunction.sigmaHorn : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} → {ι : Type v} → [inst : LinearOrder ι] → P.RankFunction ι → [P.IsProper] → ι → SSet
-- Mathlib.Algebra.Module.LinearMap.Basic
/-- The map `Sum.elim` specialised with zero in the first argument, as a linear map.  -/
Sum.elimZeroLeft : {ι : Type u_6} → {κ : Type u_7} → {R : Type u_8} → [inst : Semiring R] → (ι → R) →ₗ[R] κ ⊕ ι → R
-- Mathlib.Order.Filter.Map
Filter.seq_eq_filter_seq : ∀ {α β : Type u} (f : Filter (α → β)) (g : Filter α), f <*> g = f.seq g
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- The category of cocones on `F` is just the comma category `(F ↓ Δ)`, where `Δ` is the constant
functor.  -/
CategoryTheory.Limits.Cocone.equivStructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) →
          CategoryTheory.Limits.Cocone F ≌ CategoryTheory.StructuredArrow F (CategoryTheory.Functor.const J)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Count
MeasureTheory.eLpNorm_count_lt_top : ∀ {α : Type u_1} {ε : Type u_2} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : α → ε} {p : ENNReal} [Finite α],
  p ≠ 0 → (MeasureTheory.eLpNorm f p MeasureTheory.Measure.count < ⊤ ↔ ∀ (i : α), ‖f i‖ₑ < ⊤)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
/-- Given `Φ : SuccStruct C` and a well-ordered type `J`, this
is the functor `J ⥤ C` which gives the iterations of `Φ` indexed by `J`.  -/
CategoryTheory.SmallObject.SuccStruct.iterationFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.SmallObject.SuccStruct C →
      (J : Type w) →
        [inst_1 : LinearOrder J] →
          [OrderBot J] →
            [SuccOrder J] →
              [WellFoundedLT J] → [CategoryTheory.Limits.HasIterationOfShape J C] → CategoryTheory.Functor J C
-- Mathlib.Data.Multiset.MapFold
Multiset.rel_map : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {δ : Type u_3} {p : γ → δ → Prop} {s : Multiset α} {t : Multiset β}
  {f : α → γ} {g : β → δ},
  Multiset.Rel p (Multiset.map f s) (Multiset.map g t) ↔ Multiset.Rel (fun a b => p (f a) (g b)) s t
-- Mathlib.Data.Finset.Defs
Finset.lt_eq_subset : ∀ {α : Type u_1}, (fun x1 x2 => x1 ⊂ x2) = fun x1 x2 => x1 ⊂ x2
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.zero_fst : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F], 0.1 = 0
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.sectL_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (Z : D) (X : C), (CategoryTheory.Prod.sectL C Z).obj X = (X, Z)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_toSubfield : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  (IntermediateField.adjoin F S).toSubfield = Subfield.closure (Set.range ⇑(algebraMap F E) ∪ S)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.instAlgebra' : {R : Type u_3} →
  {A : Type u_4} →
    {M : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : CommRing A] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R M] →
                [inst_5 : Module A M] → (Q : QuadraticForm A M) → [IsScalarTower R A M] → Algebra R (CliffordAlgebra Q)
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_comp_eq : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (e : α ≃ β) (f : γ → α) (g : γ → β), ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
-- Mathlib.Algebra.Algebra.Equiv
/-- The proposition that the function preserves multiplication  -/
AlgEquiv.map_mul' : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (self : A ≃ₐ[R] B) (x y : A),
  self.toFun (x * y) = self.toFun x * self.toFun y
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasProd.sum : ∀ {α : Type u_4} {β : Type u_5} {M : Type u_6} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  {f : α ⊕ β → M} {a b : M}, HasProd (f ∘ Sum.inl) a → HasProd (f ∘ Sum.inr) b → HasProd f (a * b)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_zpow_right`. -/
Equiv.Perm.SameCycle.of_zpow_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle x ((f ^ n) y) → f.SameCycle x y
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.volume_frontier_normLeOne : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.volume (frontier (NumberField.mixedEmbedding.fundamentalCone.normLeOne K)) = 0
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- The colimit cocone for the coproduct with a zero object.  -/
CategoryTheory.Limits.binaryCofanZeroRight : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → CategoryTheory.Limits.BinaryCofan X 0
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- In a fiber bundle, the preimage under the projection of a set with unique differentials
in the base has unique differentials in the bundle. Version with a point `⟨b, x⟩`.  -/
UniqueMDiffWithinAt.bundle_preimage' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {F : Type u_9} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] (Z : M → Type u_10) [inst_8 : TopologicalSpace (Bundle.TotalSpace F Z)]
  [inst_9 : (b : M) → TopologicalSpace (Z b)] [inst_10 : FiberBundle F Z] {b : M},
  UniqueMDiffAt[s] b → ∀ (x : Z b), UniqueMDiffAt[Bundle.TotalSpace.proj ⁻¹' s] ⟨b, x⟩
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.instProdT0Space : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [T0Space α]
  [T0Space β], T0Space (WithLp p (α × β))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.logError : Lean.Elab.Term.LevelMVarErrorInfo → Lean.Elab.TermElabM Unit