mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a locally compact T2 topological space and `U i`, `i : ι`, is a locally finite open
covering of a compact set `s`, then there exists a `BumpCovering ι X s` that is subordinate to `U`.
If `X` is a paracompact space, then the assumption `hf : LocallyFinite U` can be omitted, see
`BumpCovering.exists_isSubordinate`. This version assumes that `p : (X → ℝ) → Prop` is a predicate
that satisfies Urysohn's lemma, and provides a `BumpCovering` such that each function of the
covering satisfies `p`.  -/
BumpCovering.exists_isSubordinate_of_locallyFinite_of_prop_t2space : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [LocallyCompactSpace X] [T2Space X]
  (p : (X → ℝ) → Prop),
  (∀ (s t : Set X),
      IsClosed s →
        IsCompact t → Disjoint s t → ∃ f, p ⇑f ∧ Set.EqOn (⇑f) 0 s ∧ Set.EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Set.Icc 0 1) →
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ (i : ι), IsOpen (U i)) →
          LocallyFinite U →
            s ⊆ ⋃ i, U i → ∃ f, (∀ (i : ι), p ⇑(f i)) ∧ f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_dotProduct_vec : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Mul R] [inst_2 : Fintype m]
  [inst_3 : Fintype n] (A B : Matrix m n R), A.vec ⬝ᵥ B.vec = (A.transpose * B).trace
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_natCast : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : NatCast β] (n : ℕ), ⇑↑n = fun x => ↑n
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.getEntryLE?.go : {α : Type u} → {β : Type v} → [Ord α] → α → Option (α × β) → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- `MonoidHom` version of `autMap`.  -/
CategoryTheory.PreGaloisCategory.autMapHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {A B : C} →
        [CategoryTheory.PreGaloisCategory.IsConnected A] →
          [CategoryTheory.PreGaloisCategory.IsGalois B] → (A ⟶ B) → CategoryTheory.Aut A →* CategoryTheory.Aut B
-- Mathlib.GroupTheory.GroupAction.Support
MulAction.supports_of_mem : ∀ (G : Type u_1) {α : Type u_3} [inst : SMul G α] {s : Set α} {a : α}, a ∈ s → MulAction.Supports G s a
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.uniqueAlgEquiv_symm_apply : ∀ (R : Type u) [inst : CommSemiring R] (σ : Type u_2) [inst_1 : Unique σ] (p : Polynomial R),
  (MvPolynomial.uniqueAlgEquiv R σ).symm p = Polynomial.eval₂ MvPolynomial.C (MvPolynomial.X default) p
-- Std.Http.Protocol.H1
/-- Pulls at most one body chunk from the reader.

It advances body parsing until it either:
- produces a chunk (`some PulledChunk`), or
- cannot continue for now (`none`).
 -/
Std.Http.Protocol.H1.Machine.pullBody : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.closure_subset_topologicalClosure_span : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] (s : Set M),
  closure s ⊆ ↑(Submodule.span R s).topologicalClosure
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.sub : ∀ {α : Type u} [inst : SubtractionMonoid α] {a b : α}, IsAddUnit a → IsAddUnit b → IsAddUnit (a - b)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
addMonoidHomOfForallMemZMultiples_apply_gen : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G}
  (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' ∣ addOrderOf g),
  (addMonoidHomOfForallMemZMultiples hg hg') g = g'
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instPow : {α : Type u_1} → {β : Type u_2} → [Pow α β] → Pow αᵒᵈ β
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getDoIdDeclVar : Lean.Syntax → Lean.Elab.Term.Do.Var
-- Lean.Elab.Do.Legacy
/-- Generate `CodeBlock` for `doTry; doElems`
```
def doTry := leading_parser "try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
def doCatch      := leading_parser "catch " >> binderIdent >> optional (":" >> termParser) >> darrow >> doSeq
def doCatchMatch := leading_parser "catch " >> doMatchAlts
def doFinally    := leading_parser "finally " >> doSeq
```
 -/
Lean.Elab.Term.Do.ToCodeBlock.doTryToCode : Lean.Syntax → List Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M Lean.Elab.Term.Do.CodeBlock
-- Mathlib.LinearAlgebra.Multilinear.DFinsupp
MultilinearMap.dfinsuppFamily_single_left : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : Semiring R]
  [inst_3 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_4 : (p : (i : ι) → κ i) → AddCommMonoid (N p)]
  [inst_5 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_6 : (p : (i : ι) → κ i) → Module R (N p)]
  [inst_7 : (i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (f : MultilinearMap R (fun i => M i (p i)) (N p)),
  MultilinearMap.dfinsuppFamily (Pi.single p f) =
    (DFinsupp.lsingle p).compMultilinearMap (f.compLinearMap fun i => DFinsupp.lapply (p i))
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.leftUnitor_hom_iso : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitor x).hom.iso = CategoryTheory.Bicategory.leftUnitor x.of
-- Mathlib.Algebra.Ring.Defs
MulZeroClass.negZeroClass : {α : Type u} → [inst : MulZeroClass α] → [HasDistribNeg α] → NegZeroClass α
-- Mathlib.LinearAlgebra.Complex.Module
Complex.conjAe_coe : ⇑Complex.conjAe = ⇑(starRingEnd ℂ)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonFoldingRangeKind : Lean.ToJson Lean.Lsp.FoldingRangeKind
-- Init.Data.Sum.Lemmas
Sum.LiftRel.mono_right : ∀ {β : Type u_1} {β_1 : Type u_2} {s₁ s₂ : β → β_1 → Prop} {α : Type u_3} {α_1 : Type u_4} {r : α → α_1 → Prop}
  {x : α ⊕ β} {y : α_1 ⊕ β_1}, (∀ (a : β) (b : β_1), s₁ a b → s₂ a b) → Sum.LiftRel r s₁ x y → Sum.LiftRel r s₂ x y
-- Lean.Parser.Module
Lean.Parser.testParseModule : Lean.Environment → String → String → IO Lean.Syntax
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.nonneg_iff_isPositive : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (f : E →ₗ[𝕜] E), 0 ≤ f ↔ f.IsPositive
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, returning `fallback` if the tree map is empty.
 -/
Std.DTreeMap.minKeyD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → α → α
-- Mathlib.LinearAlgebra.Determinant
Module.Basis.smul_det : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (e : Module.Basis ι R M) {G : Type u_5} [inst_5 : Group G]
  [inst_6 : DistribMulAction G M] [inst_7 : SMulCommClass G R M] (g : G) (v : ι → M), (g • e).det v = e.det (g⁻¹ • v)
-- Batteries.Recycling.RBTree.Lemmas
/-- Asserts that `p` holds on all elements to the right of the hole.  -/
RBTree.RBNode.Path.AllR : {α : Type u_1} → (α → Prop) → RBTree.RBNode.Path α → Prop
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instMax : {α : Type u_1} → [inst : TopologicalSpace α] → Max (TopologicalSpace.CompactOpens α)
-- Init.Meta.Defs
Lean.TSyntax.getDocString : Lean.TSyntax `Lean.Parser.Command.docComment → String
-- Init.Data.Iterators.Basic
Std.Iterators.FinitenessRelation.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : SizeOf α]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] (Rel : Std.IterM m β → Std.IterM m β → Prop)
  (wf : WellFounded Rel) (subrelation : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSuccessorOf it → Rel it' it),
  sizeOf { Rel := Rel, wf := wf, subrelation := subrelation } = 1 + sizeOf wf
-- ProofWidgets.Component.RefreshComponent
/-- HACK: We cancel background threads driving `RefreshComponent`s when they are no longer needed.
However, there is currently no good way to do this when the infoview closes,
as in that case React effect cleanup functions are never executed.
Instead, `RefreshComponent` calls this persistent monitor task during creation.
The call is auto-cancelled when the infoview closes, setting `cancelTk`.  -/
ProofWidgets.RefreshComponent.monitor : ProofWidgets.RefreshComponent.Props → Lean.Server.RequestM (Lean.Server.RequestTask Unit)
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.options? : Lean.Lsp.DeleteFile → Option Lean.Lsp.DeleteFile.Options
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.instLawfulOperatorBinaryInputMkImpCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput Std.Sat.AIG.mkImpCached
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.ins.match_1.eq_5 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (y : α)
  (parent : RBTree.RBNode.Path α) (b : RBTree.RBNode α) (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_5 a y parent b
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionRule.mk.inj : ∀ {spec : Std.Time.TimeZone.TransitionSpec} {time : Std.Time.Second.Offset} {spec_1 : Std.Time.TimeZone.TransitionSpec}
  {time_1 : Std.Time.Second.Offset},
  { spec := spec, time := time } = { spec := spec_1, time := time_1 } → spec = spec_1 ∧ time = time_1
-- Mathlib.Computability.Language
Language.mul_def : ∀ {α : Type u_1} (l m : Language α), l * m = Set.image2 (fun x1 x2 => x1 ++ x2) l m
-- Std.Data.TreeSet.Basic
/-- Given a proof that the tree set is not empty, retrieves the largest element.
 -/
Std.TreeSet.max : {α : Type u} → {cmp : α → α → Ordering} → (t : Std.TreeSet α cmp) → t.isEmpty = false → α
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.CategoryStruct.{v, u} C],
  CategoryTheory.MorphismProperty C = (⦃X Y : C⦄ → (X ⟶ Y) → Prop)
-- Lean.SubExpr
/-- The Pos representing the root subexpression.  -/
Lean.SubExpr.Pos.root : Lean.SubExpr.Pos
-- Mathlib.Order.Minimal
maximal_true_subtype : ∀ {α : Type u_2} {P : α → Prop} [inst : LE α] {x : Subtype P}, Maximal (fun x => True) x ↔ Maximal P ↑x
-- Init.Data.BitVec.Lemmas
BitVec.twoPow_le_toInt_sub_toInt_iff : ∀ {w : ℕ} {x y : BitVec w},
  2 ^ (w - 1) ≤ x.toInt - y.toInt ↔ 0 ≤ x.toInt ∧ y.toInt < 0 ∧ (x.toInt - y.toInt).bmod (2 ^ w) < 0
-- Mathlib.Data.List.Pi
Multiset.Pi.cons_coe : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {i : ι} {l : List ι} (a : α i) (f : (j : ι) → j ∈ l → α j),
  Multiset.Pi.cons (↑l) i a f = List.Pi.cons i l a f
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_fun_one : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (f : α →₀ M),
  (f.prod fun x x_1 => 1) = 1
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.instModuleOfTwoCocycle : {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] →
                    (c : ↥(LieModule.Cohomology.twoCocycle R L M)) → Module R (LieAlgebra.ofTwoCocycle c)
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.mapId_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.FreeGroupoid C),
  (CategoryTheory.FreeGroupoid.mapId C).inv.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.closure_le_centralizer_centralizer : ∀ {M : Type u_1} [inst : Semigroup M] (s : Set M),
  Subsemigroup.closure s ≤ Subsemigroup.centralizer ↑(Subsemigroup.centralizer s)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- any morphism `X ⟶ Y` is part of a distinguished triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧`  -/
CategoryTheory.Pretriangulated.distinguished_cocone_triangle : ∀ {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} [self : CategoryTheory.Pretriangulated C] {X Y : C}
  (f : X ⟶ Y),
  ∃ Z g h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Given a t-structure `t` on `C`, `X : C` and `n : ℤ`, this is a distinguished
triangle `obj₁ ⟶ X ⟶ obj₃ ⟶ obj₁⟦1⟧` where `obj₁` is `< n` and `obj₃` is `≥ n`.
(This should not be used directly: use `truncLT` and `truncGE` instead.)  -/
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → ℤ → C → CategoryTheory.Pretriangulated.Triangle C
-- Init.Prelude
Lean.Macro.instMonadQuotationMacroM : Lean.MonadQuotation Lean.MacroM
-- Mathlib.Data.Set.Card
Set.Finite.eq_of_subset_of_encard_le' : ∀ {α : Type u_1} {s t : Set α}, t.Finite → s ⊆ t → t.encard ≤ s.encard → s = t
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.add_def : ∀ (α β : Type u), Cardinal.mk α + Cardinal.mk β = Cardinal.mk (α ⊕ β)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNormedAlgebra : {α : Type u} →
  {γ : Type w} →
    {𝕜 : Type u_1} →
      [inst : NormedField 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : NormedRing γ] → [NormedAlgebra 𝕜 γ] → NormedAlgebra 𝕜 (BoundedContinuousFunction α γ)
-- Mathlib.CategoryTheory.Opposites
/-- Another variant of the opposite of functor, turning a functor `Cᵒᵖ ⥤ D` into a functor `C ⥤ Dᵒᵖ`.
In informal mathematics no distinction is made.
 -/
CategoryTheory.Functor.rightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor Cᵒᵖ D → CategoryTheory.Functor C Dᵒᵖ
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg : ∀ {x y : ℝ*}, x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg
-- Std.Http.Data.Body.Empty
Std.Http.Body.instBEqEmpty : BEq Std.Http.Body.Empty
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor'_obj_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor'.obj sq).hom.right = sq.f₂₄
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getIntValue? : Lean.Expr → OptionT Id ℤ
-- Lean.Environment
/-- Returns the module name of the current file.  -/
Lean.getMainModule : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → m Lean.Name
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.of_mul_right : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, (s * t).Nonempty → t.Nonempty
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_eq_zero_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v = 0 ↔ u = v
-- Mathlib.Data.Set.Lattice
Set.iUnion_inter : ∀ {β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β), (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `f` is an isomorphism, `map f` is an equivalence of categories.  -/
CategoryTheory.Over.mapIso : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → {X Y : T} → (X ≅ Y) → (CategoryTheory.Over X ≌ CategoryTheory.Over Y)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.toOver_map_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (X : T)
  {X_1 Y : CategoryTheory.Comma (F.comp (CategoryTheory.Functor.id T)) (CategoryTheory.Functor.fromPUnit X)}
  (f : X_1 ⟶ Y), ((CategoryTheory.CostructuredArrow.toOver F X).map f).left = F.map f.left
-- Init.Data.List.Control
List.findSomeM?_nil : ∀ {m : Type u → Type u_1} [inst : Monad m] {α : Type w} {β : Type u} {f : α → m (Option β)},
  List.findSomeM? f [] = pure none
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The property that the first morphism of a factorisation is
a quasi-isomorphisms in degrees `≤ n`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.quasiIsoLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        {f : K ⟶ L} →
          ℤ →
            CategoryTheory.ObjectProperty (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cofFib✝ f).FullSubcategory
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.setOfFloorNeg.eq_1 : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsProperLinearSet.setOfFloorNeg✝ hs =
    {x | IsProperLinearSet.fract✝ hs x = IsProperLinearSet.base✝ hs ∧ ∃ i, IsProperLinearSet.floor✝ hs x i < 0}
-- Init.Grind.Order
Lean.Grind.Order.lt_le_trans_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b c : α} {k₁ k₂ : ℤ} (k : ℤ),
  a < b + ↑k₁ → b ≤ c + ↑k₂ → (k == k₂ + k₁) = true → a < c + ↑k
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : C) (p₀ p₁ : P ⟶ A) (ι : A ⟶ P)
  (ι_p₀ :
    autoParam (CategoryTheory.CategoryStruct.comp ι p₀ = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₀._autoParam)
  (ι_p₁ :
    autoParam (CategoryTheory.CategoryStruct.comp ι p₁ = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₁._autoParam)
  (P_1 : C) (p₀_1 p₁_1 : P_1 ⟶ A) (ι_1 : A ⟶ P_1)
  (ι_p₀_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι_1 p₀_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₀._autoParam)
  (ι_p₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp ι_1 p₁_1 = CategoryTheory.CategoryStruct.id A)
      HomotopicalAlgebra.PrepathObject.ι_p₁._autoParam),
  ({ P := P, p₀ := p₀, p₁ := p₁, ι := ι, ι_p₀ := ι_p₀, ι_p₁ := ι_p₁ } =
      { P := P_1, p₀ := p₀_1, p₁ := p₁_1, ι := ι_1, ι_p₀ := ι_p₀_1, ι_p₁ := ι_p₁_1 }) =
    (P = P_1 ∧ p₀ ≍ p₀_1 ∧ p₁ ≍ p₁_1 ∧ ι ≍ ι_1)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.coe_symm_continuousLinearEquiv : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} (β : ι → Type u_4) [inst : Semiring 𝕜]
  [inst_1 : (i : ι) → AddCommGroup (β i)] [inst_2 : (i : ι) → Module 𝕜 (β i)]
  [inst_3 : (i : ι) → TopologicalSpace (β i)], ⇑(PiLp.continuousLinearEquiv p 𝕜 β).symm = WithLp.toLp p
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabInfo.kind : Lean.Elab.DocElabInfo → Lean.Elab.DocElabKind
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.ext : ∀ {X Y : AlgebraicGeometry.Scheme} {f g : X ⟶ Y} (h_base : f.base = g.base),
  (∀ (U : Y.Opens),
      CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U)
          (X.presheaf.map (CategoryTheory.eqToHom ⋯).op) =
        AlgebraicGeometry.Scheme.Hom.app g U) →
    f = g
-- Mathlib.CategoryTheory.Types.Set
Set.functorToTypes_obj : ∀ {X : Type u} (S : Set X), Set.functorToTypes.obj S = ↑S
-- Mathlib.Data.ENNReal.Basic
ENNReal.lt_iff_exists_nnreal_btwn : ∀ {a b : ENNReal}, a < b ↔ ∃ r, a < ↑r ∧ ↑r < b
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- The zeroth iteration is the zeroth object .  -/
CategoryTheory.SmallObject.SuccStruct.Iteration.obj_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} (self : Φ.Iteration j),
  self.F.obj ⟨⊥, ⋯⟩ = Φ.X₀
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.forget_preservesPullback_of_right : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f)
    AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
a vertex `i` with `j ≤ i` can be identified with vertex `i + 1` in the original
path.  -/
SSet.Truncated.StrictSegal.spine_δ_vertex_ge : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) {i : Fin (m + 1)}
  {j : Fin (m + 2)},
  j ≤ i.castSucc →
    (X.spine m ⋯
            ((CategoryTheory.ConcreteCategory.hom
                (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op))
              (sx.spineToSimplex (m + 1) ⋯ f))).vertex
        i =
      f.vertex i.succ
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- Any two measures satisfying `QuotientMeasureEqMeasurePreimage` are equal.  -/
MeasureTheory.QuotientMeasureEqMeasurePreimage.unique : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {ν : MeasureTheory.Measure α} [hasFun : MeasureTheory.HasFundamentalDomain G α ν]
  (μ μ' : MeasureTheory.Measure (Quotient (MulAction.orbitRel G α)))
  [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ] [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ'], μ = μ'
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
integrable_mulExpNegMulSq_comp_restrict_of_isCompact : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : MeasurableSpace E] [BorelSpace E] {P : MeasureTheory.Measure E}
  [MeasureTheory.IsFiniteMeasure P] {ε : ℝ} {K : Set E},
  IsCompact K →
    MeasurableSet K → ∀ (g : C(E, ℝ)), MeasureTheory.Integrable (fun x => ε.mulExpNegMulSq (g x)) (P.restrict K)