mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariant_le_of_covariant_lt : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : PartialOrder N],
  (Covariant M N μ fun x1 x2 => x1 < x2) → Covariant M N μ fun x1 x2 => x1 ≤ x2
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.Functor.LaxBraided.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                {F : CategoryTheory.Functor C D} →
                  [toLaxMonoidal : F.LaxMonoidal] →
                    autoParam
                        (∀ (X Y : C),
                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y)
                              (F.map (β_ X Y).hom) =
                            CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom
                              (CategoryTheory.Functor.LaxMonoidal.μ F Y X))
                        CategoryTheory.Functor.LaxBraided.braided._autoParam →
                      F.LaxBraided
-- Lean.Data.Position
Lean.instInhabitedFileMap : Inhabited Lean.FileMap
-- Mathlib.GroupTheory.QuotientGroup.Finite
Finite.of_addSubgroup_quotient : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G) [Finite ↥H] [Finite (G ⧸ H)], Finite G
-- Mathlib.Algebra.Order.Field.Basic
add_thirds : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] (a : α),
  a / 3 + a / 3 + a / 3 = a
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.Context.declName? : Lean.Elab.Term.Context → Option Lean.Name
-- Mathlib.GroupTheory.Submonoid.Center
AddSubsemigroup.centerCongr_apply_coe : ∀ {M : Type u_2} {N : Type u_1} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (r : ↥(AddSubsemigroup.center M)),
  ↑((AddSubsemigroup.centerCongr e) r) = e ↑r
-- Mathlib.GroupTheory.Subgroup.Simple
IsSimpleAddGroup.isSimpleAddGroup_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_3} [inst_1 : AddGroup H] [IsSimpleAddGroup G] [Nontrivial H]
  (f : G →+ H), Function.Surjective ⇑f → IsSimpleAddGroup H
-- Mathlib.Data.Matrix.Mul
Matrix.ofNat_mulVec : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (x : ℕ)
  [inst_3 : x.AtLeastTwo] (v : m → α), (OfNat.ofNat x).mulVec v = OfNat.ofNat x • v
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram_toFun : ∀ (L : FirstOrder.Language) (M : Type u_1) [inst : L.Structure M] (N : Type u_5) [inst_1 : L.Structure N]
  [inst_2 : (L.withConstants M).Structure N] [inst_3 : (L.lhomWithConstants M).IsExpansionOn N]
  [inst_4 : N ⊨ L.elementaryDiagram M] (a : M),
  (FirstOrder.Language.ElementaryEmbedding.ofModelsElementaryDiagram L M N) a =
    (FirstOrder.Language.constantMap ∘ Sum.inr) a
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.one_mem_toNonUnitalStarSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A),
  1 ∈ S.toNonUnitalStarSubalgebra
-- Mathlib.Computability.Primrec.Basic
Primrec.ite : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Prop}
  [inst_2 : DecidablePred c] {f g : α → σ},
  PrimrecPred c → Primrec f → Primrec g → Primrec fun a => if c a then f a else g a
-- Mathlib.Order.Circular
/-- The betweenness relation obtained from "looping around" `≤`.
See note [reducible non-instances].  -/
LE.toBtw : (α : Type u_1) → [LE α] → Btw α
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.subsingleton_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], Subsingleton (LieSubmodule R L M) ↔ Subsingleton M
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_toSupHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β), ⇑f.toSupHom = ⇑f
-- Mathlib.Algebra.Ring.Parity
/-- **Alias** of the forward direction of `odd_iff_exists_bit1`. -/
Odd.exists_bit1 : ∀ {α : Type u_2} [inst : Semiring α] {a : α}, Odd a → ∃ b, a = 2 * b + 1
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace A] [inst_4 : IsTopologicalSemiring A] [inst_5 : ContinuousConstSMul R A] (r : R),
  SeparationQuotient.mk ((algebraMap R A) r) = (algebraMap R (SeparationQuotient A)) r
-- Init.Data.SInt.Lemmas
Int32.toUInt32_le : ∀ {a b : Int32}, 0 ≤ a → a ≤ b → a.toUInt32 ≤ b.toUInt32
-- Init.Data.SInt.Bitwise
Int16.or_neg_one : ∀ {a : Int16}, a ||| -1 = -1
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.Iter.step_drop.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive n
-- Mathlib.Order.CompleteLattice.Basic
iInf_ulift : ∀ {α : Type u_1} {ι : Type u_8} [inst : InfSet α] (f : ULift.{u_9, u_8} ι → α), ⨅ i, f i = ⨅ i, f { down := i }
-- Mathlib.Data.Finset.Dedup
Multiset.mem_toFinset : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s.toFinset ↔ a ∈ s
-- Lean.Meta.Tactic.Grind.Internalize
/-- We say `MatchCond` is simple if its argument is an implication such as `x = 0 -> ...`
If that is the case, we also internalize the implication to ensure grind can split on the antecedents.
We added this extra case to make sure the user is not surprised by `grind` failing at
```
example (x y : Nat)
    : 0 < match x, y with
          | 0, 0   => 1
          | _, _ => x + y := by -- x or y must be greater than 0
  grind
```
We should try to find a better and more general approach for handling the example above.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.internalizeMatchCond.internalizeSimpleMatchCondImp : Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.shape_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), (K.d i₁ i₁').f i₂ = 0
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_eq_max_of_aleph0_le_right : ∀ {a b : Cardinal.{u_1}}, a ≠ 0 → Cardinal.aleph0 ≤ b → a * b = max a b
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1CLM.congr_simp : ∀ {α : Type u_1} (F' : Type u_3) [inst : NormedAddCommGroup F'] [inst_1 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α}
  (hm : m ≤ m0) (μ : MeasureTheory.Measure α) [inst_2 : CompleteSpace ↥(MeasureTheory.Lp F' 1 μ)]
  [inst_3 : MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.condExpL1CLM F' hm μ = MeasureTheory.condExpL1CLM F' hm μ
-- Std.Data.DTreeMap.Basic
/-- Two tree maps are equivalent in the sense of Equiv iff all the keys and values are equal.  -/
Std.DTreeMap.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.MvPolynomial.Ideal
MvPolynomial.idealOfVars.eq_1 : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R],
  MvPolynomial.idealOfVars σ R = Ideal.span (Set.range MvPolynomial.X)
-- Mathlib.Data.Nat.Factorial.BigOperators
Finset.prod_range_add_one_eq_factorial : ∀ (n : ℕ), ∏ i ∈ Finset.range n, (i + 1) = n.factorial
-- Mathlib.Order.Filter.Lift
Filter.lift_iInf_of_directed : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Nonempty ι] {f : ι → Filter α} {g : Set α → Filter β},
  Directed (fun x1 x2 => x1 ≥ x2) f → Monotone g → (iInf f).lift g = ⨅ i, (f i).lift g
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- The functor `SpectralSequence C c r₀ ⥤ HomologicalComplex C (c r)` which
sends a spectral sequence to its `r`th page.  -/
CategoryTheory.SpectralSequence.pageFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        (c : ℤ → ComplexShape κ) →
          (r₀ r : ℤ) →
            autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageFunctor._auto_1 →
              CategoryTheory.Functor (CategoryTheory.SpectralSequence C c r₀) (HomologicalComplex C (c r))
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The natural isomorphism `HoCat.resolution ⋙ HoCat.toLocalization L ⟶ L` when
`L : C ⥤ D` is a localization functor.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionCompToLocalizationNatTrans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (L : CategoryTheory.Functor C D) →
            [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              HomotopicalAlgebra.CofibrantObject.HoCat.resolution.comp
                  (HomotopicalAlgebra.CofibrantObject.HoCat.toLocalization L) ⟶
                L
-- Mathlib.SetTheory.ZFC.Class
ZFSet.choice_mem : ∀ (x : ZFSet.{u}), ∅ ∉ x → ∀ y ∈ x, ↑x.choice ′ ↑y ∈ ↑y
-- Mathlib.Algebra.Group.Even
/-- **Alias** of the forward direction of `isSquare_iff_exists_sq`. -/
IsSquare.exists_sq : ∀ {α : Type u_2} [inst : Monoid α] (a : α), IsSquare a → ∃ r, a = r ^ 2
-- Init.Data.UInt.Bitwise
UInt8.toBitVec_shiftRight : ∀ (a b : UInt8), (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 8)
-- Std.Internal.UV.UDP
/-- Creates a new UDP socket.
 -/
Std.Internal.UV.UDP.Socket.new : IO Std.Internal.UV.UDP.Socket
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a localization map `f : M →* N` for a submonoid `S ⊆ M`, for all `z : N` we have that if
`x : M, y ∈ S` are such that `z * f y = f x`, then `f x * (f y)⁻¹ = z`.  -/
Submonoid.LocalizationMap.mk'_sec : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (z : N), f.mk' (f.sec z).1 (f.sec z).2 = z
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instFunLike : {X : Type u_1} →
  {R : Type u_3} →
    [inst : Zero X] →
      [inst_1 : Zero R] →
        [inst_2 : TopologicalSpace X] → [inst_3 : TopologicalSpace R] → FunLike (ContinuousMapZero X R) X R
-- Mathlib.Algebra.Lie.Free
_private.Mathlib.Algebra.Lie.Free.0.«termLib.lift_of_apply» : Lean.ParserDescr
-- Mathlib.Algebra.MvPolynomial.Supported
MvPolynomial.mem_supported_vars : ∀ {σ : Type u_1} {R : Type u} [inst : CommSemiring R] (p : MvPolynomial σ R), p ∈ MvPolynomial.supported R ↑p.vars
-- Mathlib.Topology.NhdsWithin
self_mem_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} {s : Set α}, s ∈ nhdsWithin a s
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsMaximumClique.congr_simp : ∀ {α : Type u_3} [inst : Finite α] (G G_1 : SimpleGraph α),
  G = G_1 → ∀ (s s_1 : Finset α), s = s_1 → G.IsMaximumClique s = G_1.IsMaximumClique s_1
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_tfae : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : C} (f : X ⟶ Y),
  [CategoryTheory.Epi (L.map f), P.epiModSerre f,
      ∀ ⦃Z : C⦄ (z : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (L.map f) (L.map z) = 0 → L.map z = 0].TFAE
-- Mathlib.SetTheory.ZFC.Class
Class.notMem_empty : ∀ (x : Class.{u}), x ∉ ∅
-- Aesop.Tree.Data
Aesop.Rapp.setState : Aesop.NodeState → Aesop.Rapp → Aesop.Rapp
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.instMax : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] → [inst_3 : Module A W] → {ρ : Representation A G W} → Max (Subrepresentation ρ)
-- Mathlib.Data.Finsupp.Indicator
/-- Create an element of `ι →₀ α` from a finset `s` and a function `f` defined on this finset.  -/
Finsupp.indicator : {ι : Type u_1} → {α : Type u_2} → [inst : Zero α] → (s : Finset ι) → ((i : ι) → i ∈ s → α) → ι →₀ α
-- Mathlib.RingTheory.Jacobson.Ideal
/-- The Jacobson radical of `I` is the infimum of all maximal (left) ideals containing `I`.  -/
TwoSidedIdeal.jacobson : {R : Type u} → [inst : Ring R] → TwoSidedIdeal R → TwoSidedIdeal R
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.repr_ker : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (hx : AlgebraicIndependent R x), RingHom.ker ↑hx.repr = ⊥
-- Lean.Meta.Tactic.Repeat
/-- `repeat1' f` runs `f` on all of the goals to produce a new list of goals,
then runs `f` again on all of those goals, and repeats until `f` fails on all remaining goals,
or until `maxIters` total calls to `f` have occurred.
Fails if `f` does not succeed at least once.
 -/
Lean.Meta.repeat1' : {m : Type → Type} →
  {ε : Type u_1} →
    {s : Type} →
      [Monad m] →
        [Lean.MonadError m] →
          [MonadExcept ε m] →
            [Lean.MonadBacktrack s m] →
              [Lean.MonadMCtx m] →
                (Lean.MVarId → m (List Lean.MVarId)) → List Lean.MVarId → optParam ℕ 100000 → m (List Lean.MVarId)
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toNat = n % 2 ^ 64
-- Mathlib.Geometry.Euclidean.SignedDist
Affine.Simplex.signedInfDist.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.signedInfDist i = (affineSpan ℝ (s.points '' {i}ᶜ)).signedInfDist (s.points i)
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.MatchEqns.eqnNames : Lean.Meta.Match.MatchEqns → Array Lean.Name
-- Aesop.Search.Queue
Aesop.FIFOQueue.mk.sizeOf_spec : ∀ (goals : Array Aesop.GoalRef) (pos : ℕ), sizeOf { goals := goals, pos := pos } = 1 + sizeOf goals + sizeOf pos
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.Context.mk.injEq : ∀ (proof : Lean.Expr) (xs : Array Lean.Expr) (proof_1 : Lean.Expr) (xs_1 : Array Lean.Expr),
  ({ proof := proof, xs := xs } = { proof := proof_1, xs := xs_1 }) = (proof = proof_1 ∧ xs = xs_1)
-- Mathlib.NumberTheory.LSeries.Convolution
/-- Dirichlet convolution of two sequences.

We define this in terms of the already existing definition for arithmetic functions.  -/
LSeries.notation.«term_⍟_» : Lean.TrailingParserDescr
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.combineMinIdxOn_assoc : ∀ {β : Type u_1} {α : Type u_2} {xys : List α} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β]
  {xs ys zs : List α} {i j k : ℕ} {f : α → β} (hi : i < xs.length) (hj : j < ys.length) (hk : k < zs.length)
  (h : xys = xs ++ ys),
  List.combineMinIdxOn✝ f (List.combineMinIdxOn✝ f i j hi hj) k ⋯ hk =
    List.combineMinIdxOn✝ f i (List.combineMinIdxOn✝ f j k hj hk) hi ⋯
-- Aesop.Script.SScript
Aesop.Script.SScript.empty : Aesop.Script.SScript
-- Mathlib.Algebra.Group.Basic
add_sub_assoc' : ∀ {G : Type u_3} [inst : SubNegMonoid G] (a b c : G), a + (b - c) = a + b - c
-- Mathlib.FieldTheory.RatFunc.Basic
/-- The equivalence between `K⟮X⟯` and the field of fractions of `K[X]`
 -/
RatFunc.toFractionRingAlgEquiv : (K : Type u) →
  [inst : CommRing K] →
    [inst_1 : IsDomain K] →
      (R : Type u_1) →
        [inst_2 : CommSemiring R] → [inst_3 : Algebra R (Polynomial K)] → RatFunc K ≃ₐ[R] FractionRing (Polynomial K)
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.algebraMap_σ : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (self : Algebra.Extension R S) (x : S), (algebraMap self.Ring S) (self.σ x) = x
-- Mathlib.Data.List.MinMax
List.not_lt_minimum_of_mem : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] {l : List α} {a m : α}, a ∈ l → l.minimum = ↑m → ¬a < m
-- Init.Data.Nat.Dvd
Nat.dvd_sub : ∀ {k m n : ℕ}, k ∣ m → k ∣ n → k ∣ m - n
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.unop_nonpos : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] {a : αᵃᵒᵖ}, AddOpposite.unop a ≤ 0 ↔ a ≤ 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rco_eq_some_iff : ∀ {k m n i : ℕ}, (m...n).toList[i]? = some k ↔ i < n - m ∧ m + i = k
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The functor `X.HomotopyCategory × Y.HomotopyCategory ⥤ (X ⊗ Y).HomotopyCategory`
when `X` and `Y` are `2`-truncated simplicial sets.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse : (X Y : SSet.Truncated 2) →
  CategoryTheory.Functor (X.HomotopyCategory × Y.HomotopyCategory)
    (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
/-- The functor `toDescentDataFunctor : F.DescentData' sq sq₃ ⥤ F.DescentData f`, on objects.  -/
CategoryTheory.Pseudofunctor.DescentData'.descentData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)} →
                {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)} →
                  F.DescentData' sq sq₃ → F.DescentData f
-- Init.Conv
/-- `left` traverses into the left argument. Synonym for `lhs`.  -/
Lean.Parser.Tactic.Conv.convLeft : Lean.ParserDescr
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_sup : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  (I J : Ideal R) [RingHomClass F R S], Ideal.map f (I ⊔ J) = Ideal.map f I ⊔ Ideal.map f J
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
/-- (Implementation). The basic open set of the section `π꙳ s`.  -/
AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.imageBasicOpen : {X Y : AlgebraicGeometry.LocallyRingedSpace} →
  (f g : X ⟶ Y) →
    (U :
        TopologicalSpace.Opens
          ↑↑(CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
                  (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).toPresheafedSpace) →
      ↑((CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
                  (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).presheaf.obj
            (Opposite.op U)) →
        TopologicalSpace.Opens ↑Y.toTopCat
-- Mathlib.RingTheory.Algebraic.Integral
Algebra.IsAlgebraic.instIsLocalizedModuleNonZeroDivisorsToLinearMapToAlgHom : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (S' : Type u_5)
  [inst_3 : CommRing S'] [FaithfulSMul R S] [alg : Algebra.IsAlgebraic R S] [NoZeroDivisors S] [inst_6 : Algebra S S']
  [IsFractionRing S S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R S S'],
  IsLocalizedModule (nonZeroDivisors R) (IsScalarTower.toAlgHom R S S').toLinearMap
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.instIsZLatticeRealMixedSpaceIntegerLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], IsZLattice ℝ (NumberField.mixedEmbedding.integerLattice K)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.min?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Min α]
  [inst_1 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.keys.min? = t.minKey?
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {V W : BialgCat R} [inst_1 : SizeOf R] (toBialgHom' : V.carrier →ₐc[R] W.carrier),
  sizeOf { toBialgHom' := toBialgHom' } = 1 + sizeOf toBialgHom'
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If orders are finite, the divisor of a product of meromorphic functions is the sum of the divisors.
 -/
MeromorphicOn.divisor_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜},
  (∀ i ∈ s, MeromorphicOn (f i) U) →
    (∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤) →
      MeromorphicOn.divisor (∏ i ∈ s, f i) U = ∑ i ∈ s, MeromorphicOn.divisor (f i) U
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap.eq_1 : ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap =
  {
    forget₂ :=
      { obj := fun G => G.toProfinite,
        map := fun {X Y} f =>
          CompHausLike.ofHom (fun X => TotallyDisconnectedSpace ↑X)
            { toFun := ⇑(ProfiniteGrp.Hom.hom f), continuous_toFun := ⋯ },
        map_id :=
          ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap._proof_2,
        map_comp :=
          @ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap._proof_3 },
    forget_comp :=
      ProfiniteGrp.instHasForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap._proof_5 }
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNat.injEq : ∀ (inst lit proof inst_1 lit_1 proof_1 : Lean.Expr),
  (Mathlib.Meta.NormNum.Result'.isNat inst lit proof = Mathlib.Meta.NormNum.Result'.isNat inst_1 lit_1 proof_1) =
    (inst = inst_1 ∧ lit = lit_1 ∧ proof = proof_1)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter₂_add_subset : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Add α] (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋂ i, ⋂ j, s i j) + t ⊆ ⋂ i, ⋂ j, s i j + t
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_or' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] (p q : Prop) (f : p ∨ q → α),
  ⨆ (h : p ∨ q), f h = max (⨆ (h : p), f ⋯) (⨆ (h : q), f ⋯)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
/-- A cylinder object for `A` can be obtained from a factorization of the obvious
map `A ⨿ A ⟶ A` as a cofibration followed by a trivial fibration.  -/
HomotopicalAlgebra.Cylinder.ofFactorizationData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {A : C} →
        (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
            (CategoryTheory.Limits.codiag A) →
          HomotopicalAlgebra.Cylinder A
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.ofList_nil : ∀ {α : Type u_1}, FreeAddMonoid.ofList [] = 0
-- Init.Data.UInt.Lemmas
UInt8.ofInt_add : ∀ (x y : ℤ), UInt8.ofInt (x + y) = UInt8.ofInt x + UInt8.ofInt y
-- Lean.Parser.Command
Lean.Parser.Command.declModifiersF.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.SpaceResult : Type
-- Mathlib.Algebra.Category.Ring.Under.Property
RingHom.HasEqualizers.isClosedUnderLimitsOfShape : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) →
      ∀ (R : CommRingCat),
        (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).underObj.IsClosedUnderLimitsOfShape
          CategoryTheory.Limits.WalkingParallelPair