mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : ((HomologicalComplex.single C c j).obj A).opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjOpcyclesSelfIso c j A).hom h) =
    CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).iCycles j)
      (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).pOpcycles j) h)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The pushout cocone in the opposite category associated to the cone of
a commutative square identifies to the cocone of the flipped commutative square in
the opposite category  -/
CategoryTheory.CommSq.coneOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W X Y Z : C} →
      {f : W ⟶ X} → {g : W ⟶ Y} → {h : X ⟶ Z} → {i : Y ⟶ Z} → (p : CategoryTheory.CommSq f g h i) → p.cone.op ≅ ⋯.cocone
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Function corresponding to a monomial.  -/
Tactic.ComputeAsymptotics.UnitMonomial.toFun : Tactic.ComputeAsymptotics.UnitMonomial → Tactic.ComputeAsymptotics.Basis → ℝ → ℝ
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.mulLeftCosetsCompSubtypeVal.eq_1 : ∀ {G : Type u} [inst : Group G] (H I : Subgroup G),
  MulAction.mulLeftCosetsCompSubtypeVal H I = MulAction.compHom (G ⧸ H) I.subtype
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rootD.eq_1 : ∀ (self : Batteries.UnionFind) (x : ℕ), self.rootD x = if h : x < self.size then ↑(self.root ⟨x, h⟩) else x
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.evaluation_preservesLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [∀ (k : K), CategoryTheory.Limits.HasLimit (F.flip.obj k)]
  (k : K), CategoryTheory.Limits.PreservesLimit F ((CategoryTheory.evaluation K C).obj k)
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigOWith_abs_right`. -/
Asymptotics.IsBigOWith.of_abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {c : ℝ} {f : α → E} {l : Filter α} {u : α → ℝ},
  (Asymptotics.IsBigOWith c l f fun x => |u x|) → Asymptotics.IsBigOWith c l f u
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  Std.ExtDHashMap.Const.get (m.insertIfNew k v) a h₁ =
    if h₂ : (k == a) = true ∧ k ∉ m then v else Std.ExtDHashMap.Const.get m a ⋯
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Lex.lt_iff_of_unique : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : Unique ι] [inst_2 : (i : ι) → LT (α i)]
  [inst_3 : Preorder ι] {x y : Lex (Π₀ (i : ι), α i)}, x < y ↔ (ofLex x) default < (ofLex y) default
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt16.size ≤ n →
    (UInt16.ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt16.size - 1) UInt16.toUInt32_ofNatClamp_of_le._proof_1
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instMembershipOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Membership α (Std.ExtDHashMap α β)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.foldl_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  [Std.TransCmp cmp] {f : δ → (a : α) → β a → δ} {init : δ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.foldl f init t₁ = Std.DTreeMap.Raw.foldl f init t₂
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_inv : ∀ {K : Type u_4} [inst : Field K] {L : Type u_7} [inst_1 : DivisionRing L] [inst_2 : Algebra K L] [Module.Finite K L]
  (x : L), (Algebra.norm K) x⁻¹ = ((Algebra.norm K) x)⁻¹
-- Std.Internal.UV.System
/-- Gets the process ID of the current process.
 -/
Std.Internal.UV.System.osGetPid : IO UInt64
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.apply_symm_apply : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B) (x : B), e (e.symm x) = x
-- Mathlib.Algebra.GroupWithZero.InjSurj
Function.Injective.isRightCancelMulZero : ∀ {M₀ : Type u_1} {M₀' : Type u_3} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : Mul M₀'] [inst_3 : Zero M₀']
  (f : M₀ → M₀'),
  Function.Injective f →
    f 0 = 0 → (∀ (x y : M₀), f (x * y) = f x * f y) → ∀ [IsRightCancelMulZero M₀'], IsRightCancelMulZero M₀
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.instIsWellOrderContinuousFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : C} [inst_1 : CategoryTheory.Abelian C]
  (hG : CategoryTheory.IsSeparator G) {X : C} [inst_2 : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C]
  (A₀ : CategoryTheory.Subobject X) (J : Type w) [inst_3 : LinearOrder J] [inst_4 : OrderBot J] [inst_5 : SuccOrder J]
  [inst_6 : WellFoundedLT J],
  (CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.functor hG A₀ J).IsWellOrderContinuous
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpCompIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {E : Type u₃} [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.CartesianMonoidalCategory E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} [inst_6 : F.Monoidal] [inst_7 : G.Monoidal],
  CategoryTheory.Functor.mapAddGrpCompIso =
    CategoryTheory.NatIso.ofComponents
      (fun X => CategoryTheory.AddGrp.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapAddGrp.obj X).X) ⋯ ⋯) ⋯
-- Mathlib.Util.WhatsNew
_private.Mathlib.Util.WhatsNew.0.Mathlib.WhatsNew.levelParamsToMessageData : List Lean.Name → Lean.MessageData
-- Mathlib.Topology.EMetricSpace.Defs
PseudoEMetricSpace.mk : {α : Type u} →
  [toEDist : EDist α] →
    (∀ (x : α), edist x x = 0) →
      (∀ (x y : α), edist x y = edist y x) →
        (∀ (x y z : α), edist x z ≤ edist x y + edist y z) →
          (toUniformSpace : UniformSpace α) →
            autoParam (uniformity α = ⨅ ε, ⨅ (_ : ε > 0), Filter.principal {p | edist p.1 p.2 < ε})
                PseudoEMetricSpace.uniformity_edist._autoParam →
              PseudoEMetricSpace α
-- Mathlib.Topology.Compactness.SigmaCompact
/-- In a σ-compact space, `univ` is σ-compact.  -/
isSigmaCompact_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [h : SigmaCompactSpace X], IsSigmaCompact Set.univ
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.drop_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {X Y :
    CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.SimplicialObject C))
      (CategoryTheory.SimplicialObject.const C)}
  (f : X ⟶ Y), CategoryTheory.SimplicialObject.Augmented.drop.map f = f.left
-- Mathlib.Data.List.Basic
_private.Mathlib.Data.List.Basic.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Algebra.Lie.TraceForm
LieModule.trace_toEnd_eq_zero_of_mem_lcs : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] {k : ℕ}
  {x : L}, 1 ≤ k → x ∈ LieModule.lowerCentralSeries R L L k → (LinearMap.trace R M) ((LieModule.toEnd R L M) x) = 0
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.aemeasurable : ∀ {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [inst_2 : AddCommMonoid E] [inst_3 : Module ℝ E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ (t : T), AEMeasurable (X t) P
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD.eq_1 : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : Zero X] (f : X → R) (default : ContinuousMapZero X R),
  ContinuousMapZero.mkD f default =
    if h : Continuous f ∧ f 0 = 0 then { toFun := f, continuous_toFun := ⋯, map_zero' := ⋯ } else default
-- Lean.Elab.Tactic.Basic
/-- Adapt a syntax transformation to a regular tactic evaluator.  -/
Lean.Elab.Tactic.adaptExpander : (Lean.Syntax → Lean.Elab.Tactic.TacticM Lean.Syntax) → Lean.Elab.Tactic.Tactic
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.count_real_singleton' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {a : α}, MeasurableSet {a} → MeasureTheory.Measure.count.real {a} = 1
-- Std.Tactic.Do.Syntax
/-- `mexists` is like `exists`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
  mintro H
  mexists 42
```
 -/
Lean.Parser.Tactic.mexistsError : Lean.ParserDescr
-- Lean.Elab.BuiltinCommand
Lean.Elab.Command.elabCheckFailure : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.sigmaCurry_of : ∀ {ι : Type v} [inst : DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w}
  [inst_1 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] [inst_2 : (i : ι) → DecidableEq (α i)] (k : (i : ι) × α i)
  (x : δ k.fst k.snd),
  DirectSum.sigmaCurry ((DirectSum.of (fun k => δ k.fst k.snd) k) x) =
    (DirectSum.of (fun i' => DirectSum (α i') fun j' => δ i' j') k.fst) ((DirectSum.of (fun j' => δ k.fst j') k.snd) x)
-- Mathlib.Order.Filter.Pointwise
Filter.instInvolutiveInv.eq_1 : ∀ {α : Type u_2} [inst : InvolutiveInv α], Filter.instInvolutiveInv = { toInv := Filter.instInv, inv_inv := ⋯ }
-- Mathlib.Order.Minimal
Set.Subsingleton.maximal_mem_iff : ∀ {α : Type u_2} {x : α} {s : Set α} [inst : Preorder α], s.Subsingleton → (Maximal (fun x => x ∈ s) x ↔ x ∈ s)
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- A template for a valued CSP problem over a domain `D` with costs in `C`.
Regarding `C` we want to support `Bool`, `Nat`, `ENat`, `Int`, `Rat`, `NNRat`,
`Real`, `NNReal`, `EReal`, `ENNReal`, and tuples made of any of those types.  -/
ValuedCSP : Type u_1 →
  (C : Type u_2) → [inst : AddCommMonoid C] → [inst_1 : PartialOrder C] → [IsOrderedAddMonoid C] → Type (max u_1 u_2)
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A set `s` is called totally disconnected if every subset `t ⊆ s` which is preconnected is
a subsingleton, i.e. either empty or a singleton.  -/
IsTotallyDisconnected : {α : Type u} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.Topology.Bornology.BoundedOperation
tendsto_const_add_cobounded : ∀ {R : Type u_1} [inst : SeminormedAddCommGroup R] (x : R),
  Filter.Tendsto (fun x_1 => x + x_1) (Bornology.cobounded R) (Bornology.cobounded R)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- An open immersion is an iso if the underlying continuous map is epi.  -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] [h' : CategoryTheory.Epi f.base], CategoryTheory.IsIso f
-- Mathlib.Order.SymmDiff
himp_bihimp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b c : α), c ⇨ bihimp a b = (b ⊓ c ⇨ a) ⊓ (a ⊓ c ⇨ b)
-- Lean.Parser.Syntax
/-- `postfix:prec "op" => f` is equivalent to `notation:prec x:prec "op" => f x`.
 -/
Lean.Parser.Command.postfix : Lean.Parser.Parser
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.MonadShareCommon.mk : {m : Type → Type} →
  (Lean.Expr → m Lean.Expr) → (Lean.Expr → m Unit) → m Bool → Lean.Meta.Sym.Internal.MonadShareCommon m
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_prod : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [Module.Free R S] [Module.Free R T] [Module.Finite R S]
  [Module.Finite R T], Algebra.trace R (S × T) = (Algebra.trace R S).coprod (Algebra.trace R T)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- Property in the model space of a model with corners of being `C^n` within a set at a point,
when read in the model vector space. This property will be lifted to manifolds to define `C^n`
functions between manifolds.
The parameter `n` belongs to `ℕ∞ω` (accessible in the `ContDiff` scope), i.e. it can be a natural
number, `∞`, or `ω`, where `C^ω` corresponds to analytic functions.
 -/
ContDiffWithinAtProp : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {E' : Type u_5} →
                  [inst_4 : NormedAddCommGroup E'] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      {H' : Type u_6} →
                        [inst_6 : TopologicalSpace H'] →
                          ModelWithCorners 𝕜 E' H' → WithTop ℕ∞ → (H → H') → Set H → H → Prop
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Add element `a` to the given heap `h`.  -/
Batteries.BinomialHeap.insert : {α : Type u} → {le : α → α → Bool} → α → Batteries.BinomialHeap α le → Batteries.BinomialHeap α le
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_le_one_of_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ ≤ ν → ∀ [MeasureTheory.SigmaFinite ν], μ.rnDeriv ν ≤ᵐ[ν] 1
-- Lean.Elab.BuiltinNotation
/-- Returns true if the given expression contains a cdot for the given `HygieneInfo` name.
If no `HygieneInfo` name is given, then returns true if there is any cdot.
The search is delimited by cdot binders (any syntax satisfying `isCDotBinderKind`).
 -/
Lean.Elab.Term.hasCDot : Lean.Syntax → Option Lean.Name → Bool
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (f : (n → R) →ₗ[R] m → R) (i : m) (j : n), LinearMap.toMatrix' f i j = f (Pi.single j 1) i
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_repr : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E),
  ∑ i, (b.repr x).ofLp i • b i = x
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instWeakEquivalenceIResolutionObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj X)
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurveAt.hasDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ},
  IsIntegralCurveAt γ v t₀ → HasDerivAt γ (v t₀ (γ t₀)) t₀
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The type of Cauchy sequences of rationals with respect to the `p`-adic norm.  -/
PadicSeq : ℕ → Type
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- If `f : X ⟶ Spec A` is a morphism of schemes, the induced morphism on spectra of
`specTargetImageRingHom f` is the inclusion of the scheme-theoretic image of `f` into `Spec A`.  -/
AlgebraicGeometry.specTargetImageRingHom : {X : AlgebraicGeometry.Scheme} →
  {A : CommRingCat} → (f : X ⟶ AlgebraicGeometry.Spec A) → A ⟶ AlgebraicGeometry.specTargetImage f
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.relations.congr_simp : ∀ (R : Type u) [inst : CommRing R] (ι ι_1 : Type u_4),
  ι = ι_1 →
    ∀ {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι_1] (M : Type u_5) [inst_3 : AddCommGroup M]
      [inst_4 : Module R M], exteriorPower.presentation.relations R ι M = exteriorPower.presentation.relations R ι_1 M
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The differential on the alternating face map complex is the alternate
sum of the face maps  -/
AlgebraicTopology.AlternatingFaceMapComplex.objD : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] →
      (X : CategoryTheory.SimplicialObject C) →
        (n : ℕ) → X.obj (Opposite.op { len := n + 1 }) ⟶ X.obj (Opposite.op { len := n })
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.HasRightDual.exact : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} → [self : CategoryTheory.HasRightDual X] → CategoryTheory.ExactPairing X Xᘁ
-- Mathlib.Topology.Algebra.InfiniteSum.Real
/-- If the distance between consecutive points of a sequence is estimated by a summable series,
then the original sequence is a Cauchy sequence.  -/
cauchySeq_of_dist_le_of_summable : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {f : ℕ → α} (d : ℕ → ℝ),
  (∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n) → Summable d → CauchySeq f
-- Mathlib.Order.WellFounded
/-- **Alias** of the forward direction of `WellFounded.wellFoundedLT_iff_exists_minimal`. -/
WellFoundedLT.exists_minimal : ∀ {α : Type u_1} [inst : Preorder α], WellFoundedLT α → ∀ (s : Set α), s.Nonempty → ∃ m, Minimal (fun x => x ∈ s) m
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
SeparationQuotient.mkCLM_comp_outCLM : ∀ (K : Type u_1) (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul K E],
  SeparationQuotient.mkCLM K E ∘SL SeparationQuotient.outCLM K E = ContinuousLinearMap.id K (SeparationQuotient E)
-- Mathlib.Logic.Basic
/-- **Alias** of `Classical.axiomOfChoice`. -/
Classical.axiom_of_choice : ∀ {α : Sort u} {β : α → Sort v} {r : (x : α) → β x → Prop}, (∀ (x : α), ∃ y, r x y) → ∃ f, ∀ (x : α), r x (f x)
-- Lean.Meta.Tactic.Delta
/-- Delta expand declarations that satisfy `p` at `fvarId` type.
 -/
Lean.MVarId.deltaLocalDecl : Lean.MVarId → Lean.FVarId → (Lean.Name → Bool) → Lean.MetaM Lean.MVarId
-- Mathlib.Analysis.Normed.Ring.Basic
NNReal.nnnorm_eq : ∀ (x : NNReal), ‖↑x‖₊ = x
-- Mathlib.SetTheory.Ordinal.Notation
NONote.instPreorder : Preorder NONote
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.instSymmBoundedFormula : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ}, Std.Symm T.Iff
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_congr_ae : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  f =ᵐ[μ] g → μ.withDensity f = μ.withDensity g
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_Icc_eq_integral_Ico : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder X] {x y : X} [MeasureTheory.NullSingletonClass μ],
  ∫ (t : X) in Set.Icc x y, f t ∂μ = ∫ (t : X) in Set.Ico x y, f t ∂μ
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_id : ∀ {β : Type u_2} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure β), MeasureTheory.Measure.comap (fun x => x) μ = μ
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrime_scalar_tower : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (P : Ideal ↥A) [inst_1 : P.IsPrime],
  IsScalarTower (↥A) (↥(A.ofPrime P)) K
-- Std.Http.Data.Chunk
Std.Http.Trailer.mk.sizeOf_spec : ∀ (headers : Std.Http.Headers), sizeOf { headers := headers } = 1 + sizeOf headers
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_of_sub : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    ∀ {k : ι}, P.root k = P.root j - P.root i → RootPairing.chainTopCoeff i k = RootPairing.chainTopCoeff i j + 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_eq_default : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a : α}, a ∉ m → Std.DHashMap.Raw.Const.get! m a = default
-- Mathlib.CategoryTheory.Localization.Trifunctor
/-- Given functors `L₁ : C₁ ⥤ D₁`, `L₂ : C₂ ⥤ D₂`, `L₃ : C₃ ⥤ D₃`,
morphisms properties `W₁` on `C₁`, `W₂` on `C₂`, `W₃` on `C₃`, and
functors `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ E` and `F' : D₁ ⥤ D₂ ⥤ D₃ ⥤ E`, we say
`Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F F'` holds if `F` is induced by `F'`, up to an isomorphism.  -/
CategoryTheory.Localization.Lifting₃ : {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] →
                            CategoryTheory.Functor C₁ D₁ →
                              CategoryTheory.Functor C₂ D₂ →
                                CategoryTheory.Functor C₃ D₃ →
                                  CategoryTheory.MorphismProperty C₁ →
                                    CategoryTheory.MorphismProperty C₂ →
                                      CategoryTheory.MorphismProperty C₃ →
                                        CategoryTheory.Functor C₁
                                            (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)) →
                                          CategoryTheory.Functor D₁
                                              (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)) →
                                            Type (max (max (max u_1 u_2) u_3) v_13)
-- Mathlib.Order.WithBot
WithBot.ofDual.eq_1 : ∀ {α : Type u_1}, WithBot.ofDual = Equiv.refl (WithBot αᵒᵈ)
-- Mathlib.Topology.Instances.Matrix
/-- The topology on finite matrices over a discrete space is discrete.  -/
instDiscreteTopologyMatrixOfFinite : ∀ {m : Type u_4} {n : Type u_5} {R : Type u_8} [inst : TopologicalSpace R] [Finite m] [Finite n] [DiscreteTopology R],
  DiscreteTopology (Matrix m n R)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_negPart_eq_max : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} (f : ↥(MeasureTheory.Lp ℝ p μ)),
  ∀ᵐ (a : α) ∂μ, ↑↑(MeasureTheory.Lp.negPart f) a = max (-↑↑f a) 0
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.symm_trans_restr : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} (e' : OpenPartialHomeomorph X Y),
  IsOpen s → e'.symm.trans (e.restr s) ≈ (e'.symm.trans e).restr (e'.target ∩ ↑e'.symm ⁻¹' s)