mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.augmentOfIsTerminal_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {T : C}
  (hT : CategoryTheory.Limits.IsTerminal T), (X.augmentOfIsTerminal hT).left = X
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfEquivalence_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cocone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (e : J ≌ K)
  (w : e.functor.comp G ≅ F),
  (P.coconePointsIsoOfEquivalence Q e w).inv =
    Q.desc
      ((CategoryTheory.Limits.Cocone.equivalenceOfReindexing e.symm
              ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
        s)
-- Lean.Elab.Command
/-- Snapshot for incremental reuse and reporting of command elaboration. Currently only used for
(mutual) defs and contained tactics, in which case the `DynamicSnapshot` is a
`HeadersParsedSnapshot`.

Definitely resolved in `Lean.Elab.Command.elabCommandTopLevel`.

Invariant: if the bundle's `old?` is set, the context and state at the beginning of current and
old elaboration are identical.
 -/
Lean.Elab.Command.Context.snap? : Lean.Elab.Command.Context → Option (Lean.Language.SnapshotBundle Lean.Language.DynamicSnapshot)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minEntry?_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {l : List ((a : α) × β a)}, Std.Internal.List.containsKey k l = true → (Std.Internal.List.minEntry? l).isSome = true
-- Mathlib.Order.CompleteBooleanAlgebra
biSup_iInter_of_pairwise_disjoint : ∀ {α : Type u} [inst : CompletelyDistribLattice α] {ι : Type u_1} {κ : Type u_2} [hκ : Nonempty κ] {f : ι → α},
  Pairwise (Function.onFun Disjoint f) → ∀ (s : κ → Set ι), ⨆ i ∈ ⋂ j, s j, f i = ⨅ j, ⨆ i ∈ s j, f i
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.pi_linear : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : AddTorsor V1 P1]
  [inst_3 : Module k V1] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11}
  [inst_4 : (i : ι) → AddCommGroup (φv i)] [inst_5 : (i : ι) → Module k (φv i)]
  [inst_6 : (i : ι) → AddTorsor (φv i) (φp i)] (f : (i : ι) → P1 →ᵃ[k] φp i),
  (AffineMap.pi f).linear = LinearMap.pi fun a => (f a).linear
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- The inner product with values in `ℝ`.  -/
RealInnerProductSpace.«term⟪_,_⟫» : Lean.ParserDescr
-- Lean.Meta.Sym.AbstractS
/-- Similar to `mkLambdaFVars`, but uses the more efficient `abstractFVars` and `abstractFVarsRange`,
and makes the same assumption made by these functions.
 -/
Lean.Meta.Sym.mkLambdaFVarsS : Array Lean.Expr → Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isCardinalPresentable_of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] [CategoryTheory.IsCardinalPresentable X κ] (e : C ≌ C'),
  CategoryTheory.IsCardinalPresentable (e.functor.obj X) κ
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff_of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [inst_1 : K.HasPullbacks] [P.RespectsIso],
  (∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y),
      P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))) →
    P.IsLocalAtTarget K
-- Init.Data.SInt.Lemmas
ISize.toUSize_add : ∀ (a b : ISize), (a + b).toUSize = a.toUSize + b.toUSize
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstAddInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_eqToHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y = Z), CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.eqToHom f) = CategoryTheory.eqToHom ⋯
-- Mathlib.Order.CompleteLattice.Basic
OrderIso.map_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : α ≃o β)
  (x : ι → α), f (⨅ i, x i) = ⨅ i, f (x i)
-- Mathlib.Data.Finset.NAry
Finset.inf_image₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq γ] {f : α → β → γ} (s : Finset α)
  (t : Finset β) [inst_1 : SemilatticeInf δ] [inst_2 : OrderTop δ] (g : γ → δ),
  (Finset.image₂ f s t).inf g = s.inf fun x => t.inf (g ∘ f x)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.isClosed_preimage : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (A : Set (Quotient S.toSetoid)),
  IsClosed (S.proj ⁻¹' A)
-- Mathlib.Algebra.Group.Action.Pi
Pi.vaddCommClass'' : ∀ {ι : Type u_1} {α : ι → Type u_4} {β : ι → Type u_5} {γ : ι → Type u_6} [inst : (i : ι) → VAdd (β i) (γ i)]
  [inst_1 : (i : ι) → VAdd (α i) (γ i)] [∀ (i : ι), VAddCommClass (α i) (β i) (γ i)],
  VAddCommClass ((i : ι) → α i) ((i : ι) → β i) ((i : ι) → γ i)
-- Mathlib.Data.Num.Lemmas
Num.of_to_nat : ∀ (n : Num), ↑↑n = n
-- Init.Data.UInt.Lemmas
UInt32.toFin_ofFin : ∀ (n : Fin UInt32.size), (UInt32.ofFin n).toFin = n
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_eq_coe_ofAdd : ∀ {M : Type u_4} (a : M), WithZero.exp a = ↑(Multiplicative.ofAdd a)
-- Mathlib.Data.List.Defs
List.permutations'Aux.eq_def : ∀ {α : Type u_1} (t : α) (x : List α),
  List.permutations'Aux t x =
    match x with
    | [] => [[t]]
    | y :: ys => (t :: y :: ys) :: List.map (List.cons y) (List.permutations'Aux t ys)
-- Lean.Elab.Match
Lean.Elab.Term.withDepElimPatterns : {α : Type} →
  Array Lean.Elab.Term.PatternVarDecl →
    Array Lean.Expr →
      Lean.Expr →
        (Array Lean.LocalDecl → Array Lean.Meta.Match.Pattern → Lean.Expr → Lean.Elab.TermElabM α) →
          Lean.Elab.TermElabM α
-- Mathlib.RepresentationTheory.Equiv
Representation.finsuppTensorRight_symm_apply_single : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {W : Type w'} [inst_2 : AddCommMonoid W]
  {k : Type u} [inst_3 : CommSemiring k] [inst_4 : Module k V] [inst_5 : Module k W] (σ : Representation k G V)
  (ρ : Representation k G W) {α : Type w'} [inst_6 : DecidableEq α] (i : α) (v : V) (w : W),
  ((σ.finsuppTensorRight ρ α).symm fun₀ | i => v ⊗ₜ[k] w) = v ⊗ₜ[k] fun₀ | i => w
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.map_inl : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M] {N : Type u_3} [inst_5 : AddCommMonoid N]
  [inst_6 : Module R' N] [inst_7 : Module R'ᵐᵒᵖ N] [inst_8 : IsCentralScalar R' N] (f : M →ₗ[R'] N) (r : R'),
  (TrivSqZeroExt.map f) (TrivSqZeroExt.inl r) = TrivSqZeroExt.inl r
-- Lean.MetavarContext
Lean.DelayedMetavarAssignment.fvars : Lean.DelayedMetavarAssignment → Array Lean.Expr
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.Const.getD : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → β → β
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  LowerSemicontinuousOn f s ↔ ∀ x ∈ s, LowerSemicontinuousWithinAt f s x
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
/-- The postcomposition on the types `SmallShiftedHom W` with a morphism
which satisfies `W` is a bijection.  -/
CategoryTheory.Localization.SmallShiftedHom.postcompEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {M : Type w'} →
        [inst_1 : AddMonoid M] →
          [inst_2 : CategoryTheory.HasShift C M] →
            {X Y Z : C} →
              [W.RespectsIso] →
                [W.IsCompatibleWithShift M] →
                  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] →
                    [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z] →
                      [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z] →
                        [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Y] →
                          [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Y] →
                            [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z] →
                              (f : Y ⟶ Z) →
                                W f →
                                  {a : M} →
                                    CategoryTheory.Localization.SmallShiftedHom W X Y a ≃
                                      CategoryTheory.Localization.SmallShiftedHom W X Z a
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_mul_single : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] [inst_2 : IsRightCancelAdd G]
  (f : AddMonoidAlgebra k G) (r : k),
  (∀ (y : k), y * r = 0 ↔ y = 0) →
    ∀ (x : G), (f * AddMonoidAlgebra.single x r).coeff.support = Finset.map (addRightEmbedding x) f.coeff.support
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_eq_of_ne : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] {i j : ι}
  (r : G i), j ≠ i → (RestrictedProduct.mulSingle A i r) j = 1
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache.mk.sizeOf_spec : ∀ (ngen : Lean.NameGenerator) (core : Lean.Core.Cache) («meta» : Lean.Meta.Cache),
  sizeOf { ngen := ngen, core := core, «meta» := «meta» } = 1 + sizeOf ngen + sizeOf core + sizeOf «meta»
-- Mathlib.RingTheory.Polynomial.Quotient
MvPolynomial.quotient_map_C_eq_zero : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommRing R] {I : Ideal R} {i : R},
  i ∈ I → ((Ideal.Quotient.mk (Ideal.map MvPolynomial.C I)).comp MvPolynomial.C) i = 0
-- Mathlib.Algebra.Group.End
MulAut.symm_inv : ∀ (M : Type u_2) [inst : Mul M] (e : MulAut M), (MulEquiv.symm e)⁻¹ = e
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelMonoid.le_of_mul_le_mul_right : ∀ {α : Type u_2} {inst : CommMonoid α} {inst_1 : Preorder α} [self : IsOrderedCancelMonoid α] (a b c : α),
  b * a ≤ c * a → b ≤ c
-- Mathlib.Algebra.Category.CommBialgCat
commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom : ∀ {R : Type u} [inst : CommRing R] {A B : (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ} (f : A ⟶ B),
  ↑(CommBialgCat.Hom.hom ((commBialgCatEquivComonCommAlgCat R).inverse.map f)) = CommAlgCat.Hom.hom f.unop.hom.unop
-- Mathlib.Tactic.Simps.Basic
Simps.Config.mk.inj : ∀ {isSimp : Bool} {attrs : Array Lean.Elab.Attribute} {simpRhs dsimpLhs : Bool}
  {typeMd rhsMd : Lean.Meta.TransparencyMode} {fullyApplied : Bool} {notRecursive : List Lean.Name} {debug : Bool}
  {nameStem : Option String} {isSimp_1 : Bool} {attrs_1 : Array Lean.Elab.Attribute} {simpRhs_1 dsimpLhs_1 : Bool}
  {typeMd_1 rhsMd_1 : Lean.Meta.TransparencyMode} {fullyApplied_1 : Bool} {notRecursive_1 : List Lean.Name}
  {debug_1 : Bool} {nameStem_1 : Option String},
  { isSimp := isSimp, attrs := attrs, simpRhs := simpRhs, dsimpLhs := dsimpLhs, typeMd := typeMd, rhsMd := rhsMd,
        fullyApplied := fullyApplied, notRecursive := notRecursive, debug := debug, nameStem := nameStem } =
      { isSimp := isSimp_1, attrs := attrs_1, simpRhs := simpRhs_1, dsimpLhs := dsimpLhs_1, typeMd := typeMd_1,
        rhsMd := rhsMd_1, fullyApplied := fullyApplied_1, notRecursive := notRecursive_1, debug := debug_1,
        nameStem := nameStem_1 } →
    isSimp = isSimp_1 ∧
      attrs = attrs_1 ∧
        simpRhs = simpRhs_1 ∧
          dsimpLhs = dsimpLhs_1 ∧
            typeMd = typeMd_1 ∧
              rhsMd = rhsMd_1 ∧
                fullyApplied = fullyApplied_1 ∧ notRecursive = notRecursive_1 ∧ debug = debug_1 ∧ nameStem = nameStem_1
-- Init.Data.UInt.Bitwise
UInt64.toUInt32_shiftLeft : ∀ (a b : UInt64), b < 32 → (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32
-- Lean.Data.JsonRpc
Lean.JsonRpc.ResponseError.mk.inj : ∀ {α : Type u} {id : Lean.JsonRpc.RequestID} {code : Lean.JsonRpc.ErrorCode} {message : String} {data? : Option α}
  {id_1 : Lean.JsonRpc.RequestID} {code_1 : Lean.JsonRpc.ErrorCode} {message_1 : String} {data?_1 : Option α},
  { id := id, code := code, message := message, data? := data? } =
      { id := id_1, code := code_1, message := message_1, data? := data?_1 } →
    id = id_1 ∧ code = code_1 ∧ message = message_1 ∧ data? = data?_1
-- Lean.Meta.Tactic.Simp.Types
/-- Name of a declaration stored in the environment which has type `Simproc`.  -/
Lean.Meta.Simp.SimprocOLeanEntry.declName : Lean.Meta.Simp.SimprocOLeanEntry → Lean.Name
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.below_of_lt' : ∀ {o : ONote} {b : Ordinal.{0}}, o.repr < Ordinal.omega0 ^ b → o.NF → o.NFBelow b
-- Mathlib.Algebra.GroupWithZero.Defs
/-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`  -/
CommGroupWithZero.zpow_neg' : ∀ {G₀ : Type u_2} [self : CommGroupWithZero G₀] (n : ℕ) (a : G₀), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.arrowArrowEquivalence'_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Square.arrowArrowEquivalence'.unitIso =
    CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.Square C))
-- Mathlib.Data.Sym.Sym2
/-- `mk a` as an embedding. This is the symmetric version of `Function.Embedding.sectL`.  -/
Sym2.mkEmbedding : {α : Type u_1} → α → α ↪ Sym2 α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get?_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k a : α} {v : β k},
      (m.insertIfNew k v).get? a = if h : (k == a) = true ∧ m.contains k = false then some (cast ⋯ v) else m.get? a
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.fullyFaithfulIncl_preimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ (CategoryTheory.Limits.FormalCoproduct.incl C).obj Y),
  CategoryTheory.Limits.FormalCoproduct.fullyFaithfulIncl.preimage f = f.φ PUnit.unit
-- Lean.Server.Requests
_private.Lean.Server.Requests.0.Lean.Language.SnapshotTree.foldSnaps.traverseTree : {α : Type u_1} →
  (Lean.Language.SnapshotTask Lean.Language.SnapshotTree →
      α → Lean.Server.ServerTask (α × Lean.Language.SnapshotTree.foldSnaps.Control)) →
    α → Lean.Language.SnapshotTree → Lean.Server.ServerTask (α × Bool)
-- Mathlib.Algebra.Ring.NonZeroDivisors
IsMulTorsionFree.pow_right_injective : ∀ {M : Type u_2} [inst : CancelMonoid M] [IsMulTorsionFree M] {x : M}, x ≠ 1 → Function.Injective fun n => x ^ n
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.sSameSide_point_excenter_iff : ∀ {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} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {i : Fin (n + 1)},
      (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.points i) (s.excenter signs) ↔
        0 < s.excenterWeights signs i
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.bot_eq_one : ∀ {M : Type u_1} [inst : Monoid M], ⊥ = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.isIso_π_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {j : J} (I : CategoryTheory.Limits.IsTerminal j) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasLimit F] [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)],
  CategoryTheory.IsIso (CategoryTheory.Limits.limit.π F j)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.bijective_weightMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (self : P.Equiv Q), Function.Bijective ⇑(↑self).weightMap
-- Mathlib.Logic.Equiv.Defs
Quot.congr_mk : ∀ {α : Sort u} {β : Sort v} {ra : α → α → Prop} {rb : β → β → Prop} (e : α ≃ β)
  (eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)) (a : α), (Quot.congr e eq) (Quot.mk ra a) = Quot.mk rb (e a)
-- Lean.Parser.Extra
Lean.Parser.many.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
/-- Not differentiable, hence `deriv` has junk value zero.  -/
Real.deriv_mul_log_zero : deriv (fun x => x * Real.log x) 0 = 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get_eq_getElem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {a : α} {h : a ∈ t}, t.get a h = t[a]
-- Init.Data.Vector.Lemmas
Vector.all_append : ∀ {α : Type u_1} {n m : ℕ} {f : α → Bool} {xs : Vector α n} {ys : Vector α m}, (xs ++ ys).all f = (xs.all f && ys.all f)
-- Mathlib.Order.Atoms
isAtom_iff_le_of_ge : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, IsAtom a ↔ a ≠ ⊥ ∧ ∀ (b : α), b ≠ ⊥ → b ≤ a → a ≤ b
-- Batteries.Data.MLList.Basic
/-- Group the elements of a lazy list into chunks of a given size.
If the lazy list is finite, the last chunk may be smaller (possibly even length 0).  -/
MLList.chunk : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → ℕ → MLList m (Array α)
-- Mathlib.CategoryTheory.Limits.Over
CategoryTheory.Over.liftCocone_ι_app : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {X : C} (f : c.pt ⟶ X) (j : J),
  (CategoryTheory.Over.liftCocone c f).ι.app j = CategoryTheory.Over.homMk (c.ι.app j) ⋯
-- Init.Grind.Config
/-- Maximum number of library suggestions to use. If `none`, uses the default limit.
Only relevant when `suggestions` is `true`.
 -/
Lean.Grind.Config.maxSuggestions : Lean.Grind.Config → Option ℕ
-- Init.Internal.Order.Basic
Lean.Order.instCompleteLatticePi : {α : Sort u} →
  {β : α → Sort v} → [(x : α) → Lean.Order.CompleteLattice (β x)] → Lean.Order.CompleteLattice ((x : α) → β x)
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.instInhabitedParamKind.default : Lean.PrettyPrinter.Delaborator.ParamKind
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_add : ∀ {R : Type u_3} [inst : CommRing R] (a b : Quaternion R),
  Quaternion.normSq (a + b) = Quaternion.normSq a + Quaternion.normSq b + 2 * (a * star b).re
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_isBase_iff : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α → β) (hf : Set.InjOn f M.E) {B : Set β},
  (M.map f hf).IsBase B ↔ ∃ B₀, M.IsBase B₀ ∧ B = f '' B₀
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
smul_closedBall' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜}, c ≠ 0 → ∀ (x : E) (r : ℝ), c • Metric.closedBall x r = Metric.closedBall (c • x) (‖c‖ * r)
-- Mathlib.Topology.Category.Stonean.Basic
/-- If `X` is compact Hausdorff, `presentation X` is a Stonean space equipped with an epimorphism
down to `X` (see `CompHaus.presentation.π` and `CompHaus.presentation.epi_π`). It is a
"constructive" witness to the fact that `CompHaus` has enough projectives.  -/
CompHaus.presentation : CompHaus → Stonean
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.coe_map : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Hom M N)
  (S : L.Substructure M), ↑(FirstOrder.Language.Substructure.map φ S) = ⇑φ '' ↑S
-- Mathlib.Data.List.Sort
List.sortedLT_iff_getElem_lt_getElem_of_lt : ∀ {α : Type u_1} {l : List α} [inst : Preorder α],
  l.SortedLT ↔ ∀ ⦃i j : ℕ⦄ ⦃hi : i < l.length⦄ ⦃hj : j < l.length⦄, i < j → l[i] < l[j]
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.continuousOn_sinKernel : ∀ (a : UnitAddCircle), ContinuousOn (HurwitzZeta.sinKernel a) (Set.Ioi 0)
-- Mathlib.Algebra.Star.Subalgebra
/-- The `StarSubalgebra` obtained from `S : Subalgebra R A` by taking the smallest subalgebra
containing both `S` and `star S`.  -/
Subalgebra.starClosure : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : StarRing A] → [inst_5 : StarModule R A] → Subalgebra R A → StarSubalgebra R A
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `f ≫ g = 0`.  -/
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ {Z : C} (h : T.obj₃ ⟶ Z),
      CategoryTheory.CategoryStruct.comp T.mor₁ (CategoryTheory.CategoryStruct.comp T.mor₂ h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Init.Data.SInt.Basic
instMaxISize : Max ISize
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed
/-- The projections maps assemble into a wedge.  -/
CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [inst_4 : CategoryTheory.MonoidalClosed V] {F G H : CategoryTheory.Functor C V}
  (self : CategoryTheory.MonoidalCategory.DayConvolutionInternalHom F G H) (c : C) ⦃i j : C⦄ (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (self.π c i)
      ((CategoryTheory.ihom (F.obj i)).map (G.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f c))) =
    CategoryTheory.CategoryStruct.comp (self.π c j)
      ((CategoryTheory.MonoidalClosed.pre (F.map f)).app (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj j c)))
-- Mathlib.Order.BoundedOrder.Basic
Pi.bot_def : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → Bot (α' i)], ⊥ = fun x => ⊥
-- Mathlib.Order.Defs.Unbundled
/-- `IsRefl X r` means the binary relation `r` on `X` is reflexive.  -/
IsRefl : (α : Sort u_1) → (α → α → Prop) → Prop
-- Mathlib.Probability.Independence.Process.Basic
/-- A stochastic process $(X_s)_{s \in S}$ is independent from a random variable $Y$ if
for all $s_1, ..., s_p \in S$ the family $(X_{s_1}, ..., X_{s_p})$ is independent from $Y$.  -/
ProbabilityTheory.IndepFun.process_indepFun : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : S → Type u_4} {𝓨 : Type u_5}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : MeasurableSpace 𝓨] {X : (i : S) → Ω → 𝓧 i} {Y : Ω → 𝓨},
  (∀ (i : S), Measurable (X i)) →
    Measurable Y →
      (∀ (I : Finset S), ProbabilityTheory.IndepFun (fun ω i => X (↑i) ω) Y P) →
        ∀ [MeasureTheory.IsZeroOrProbabilityMeasure P], ProbabilityTheory.IndepFun (fun ω i => X i ω) Y P