mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.assoc_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {M : C} [inst_4 : CategoryTheory.AddMonObj M] (X : D) [inst_5 : CategoryTheory.AddModObj M X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M CategoryTheory.AddModObj.vadd)
      CategoryTheory.AddModObj.vadd =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.add X)
        CategoryTheory.AddModObj.vadd)
-- ProofWidgets.Component.Basic
/-- Lazily pretty-print and present a `Lean.Expr` as interactive text.

This component is preferrable over `InteractiveCode` when the `Expr` will not necessarily be
displayed in the UI (e.g. it may be hidden by default), in which case laziness saves some work.
On the other hand if the `Expr` will likely be shown and you are in a `MetaM` context, it is
preferrable to use the eager `InteractiveCode` in order to avoid the extra client-server roundtrip
needed for the pretty-printing RPC call.  -/
ProofWidgets.InteractiveExpr : ProofWidgets.Component ProofWidgets.InteractiveExprProps
-- Mathlib.CategoryTheory.Limits.Elements
CategoryTheory.CategoryOfElements.CreatesLimitsAux.map_π_liftedConeElement : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor C (Type w)} {I : Type u₁}
  [inst_1 : CategoryTheory.Category.{v₁, u₁} I] [inst_2 : Small.{w, u₁} I] (F : CategoryTheory.Functor I A.Elements)
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A]
  (i : I),
  (CategoryTheory.ConcreteCategory.hom
        (A.map (CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.CategoryOfElements.π A)) i)))
      (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedConeElement F) =
    (F.obj i).snd
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.step.match_1.eq_1 : ∀ (motive : Turing.ToPartrec.Cfg → Sort u_1) (a : List ℕ) (h_1 : (a : List ℕ) → motive (Turing.ToPartrec.Cfg.halt a))
  (h_2 : (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cfg.ret k v)),
  (match Turing.ToPartrec.Cfg.halt a with
    | Turing.ToPartrec.Cfg.halt a => h_1 a
    | Turing.ToPartrec.Cfg.ret k v => h_2 k v) =
    h_1 a
-- Mathlib.GroupTheory.Congruence.Hom
/-- Given additive congruence relations `c, d` on an `AddMonoid` such that `d`
contains `c`, the definition of the homomorphism from the quotient by `c` to the quotient by `d`
induced by `d`'s quotient map.  -/
AddCon.map_apply : ∀ {M : Type u_1} [inst : AddZeroClass M] {c d : AddCon M} (h : c ≤ d) (x : c.Quotient),
  (c.map d h) x = (c.lift d.mk' ⋯) x
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientKerEquivRange.eq_1 : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (φ : G →+ H),
  QuotientAddGroup.quotientKerEquivRange φ = AddEquiv.ofBijective (QuotientAddGroup.rangeKerLift φ) ⋯
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.markAsFound : Lean.FVarId → Lean.Meta.Grind.Arith.CollectDecVarsM Unit
-- Init.Data.List.Monadic
List.filterMapM_nil : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → m (Option β)},
  List.filterMapM f [] = pure []
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n →
    Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
-- Mathlib.Control.Fold
Monoid.foldlM.ofFreeMonoid : {m : Type u → Type u} →
  [inst : Monad m] → {α β : Type u} → [inst_1 : LawfulMonad m] → (β → α → m β) → FreeMonoid α →* Monoid.foldlM m β
-- Init.Data.Order.FactoriesExtra
/-- Creates an `LT α` instance from an `Ord α` instance.

`OrientedOrd α` must be satisfied so that the resulting `LT α` instance faithfully represents
the `Ord α` instance.
 -/
LT.ofOrd : (α : Type u) → [Ord α] → LT α
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instSubCoeOfAddSubgroupClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → SubNegMonoid (R i)] [inst_2 : ∀ (i : ι), AddSubgroupClass (S i) (R i)],
  RestrictedProduct.instSubCoeOfAddSubgroupClass R = { sub := fun x y => ⟨fun i => x i - y i, ⋯⟩ }
-- Mathlib.Analysis.Convex.EGauge
le_egauge_of_forall_ne_zero : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} {x : E} [(nhdsWithin 0 {0}ᶜ).NeBot] {r : ENNReal},
  0 ∈ s → (∀ (c : 𝕜), c ≠ 0 → x ∈ c • s → r ≤ ‖c‖ₑ) → r ≤ egauge 𝕜 s x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).H = h.H
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.dual_iff : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ t o₂ ↔ Ordnode.Valid' o₂ t.dual o₁
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.smul_one_eq_zero : ∀ {R : Type u_1} {A : Type u_2} [sR : CommSemiring R] [sA : CommSemiring A] [sAlg : Algebra R A] {r : R},
  r = 0 → r • 1 = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_alter_of_beq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k k' : α}
  {f : Option (β k) → Option (β k)}, (k == k') = true → (k' ∈ m.alter k f ↔ (f (m.get? k)).isSome = true)
-- Lean.Meta.InferType
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult.bvar.injEq : ∀ (idx idx_1 : ℕ), (Lean.Meta.ArrowPropResult.bvar✝ idx = Lean.Meta.ArrowPropResult.bvar✝ idx_1) = (idx = idx_1)
-- Lean.Elab.Term.TermElabM
/-- Creates a fresh inaccessible binder name based on `x`.
Equivalent to ``Lean.Core.mkFreshUserName `x``.

Do not confuse with `Lean.mkFreshId`, for creating fresh free variable and metavariable ids.
 -/
Lean.Elab.Term.mkFreshBinderName : {m : Type → Type} → [Monad m] → [Lean.MonadQuotation m] → m Lean.Name
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] [inst_2 : Inhabited α] {f : (a : α) → β a → Option (γ a)} {k : α}
  (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap! f t).getKey! k =
    ((t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome).get!
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- The cocone `finiteSubcoproductsCocone` is a colimit cocone.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.isColimitFiniteSubproductsCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        (f : α → C) →
          [CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C] →
            [inst_3 : CategoryTheory.Limits.HasCoproduct f] →
              CategoryTheory.Limits.IsColimit
                (CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone f)
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.homeoOfIso_symm_apply : ∀ {X Y : CompactlyGenerated} (f : X ≅ Y) (a : ↑Y.toTop),
  (CompactlyGenerated.homeoOfIso f).symm a = (CategoryTheory.ConcreteCategory.hom f.inv) a
-- Init.Data.Nat.Dvd
Nat.dvd_eq_false_of_mod_ne_zero : ∀ {m n : ℕ}, (n % m != 0) = true → (m ∣ n) = False
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : TopologicalSpace.Opens ↥Z),
  CategoryTheory.CategoryStruct.comp f g ∣_ U =
    CategoryTheory.CategoryStruct.comp (f ∣_ (TopologicalSpace.Opens.map g.base).obj U) (g ∣_ U)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β]
  (κ : ProbabilityTheory.Kernel α β), κ.bound = 0
-- Mathlib.Algebra.Order.Positive.Ring
Positive.commMonoid : {R : Type u_2} →
  [inst : CommSemiring R] → [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → CommMonoid { x // 0 < x }
-- Std.Http.Server.Connection
/-- Extensions to attach to each request (e.g., remote address).
 -/
Std.Http.Server.Connection.extensions : {α : Type} → Std.Http.Server.Connection α → Std.Http.Extensions
-- Mathlib.Combinatorics.Graph.Lattice
/-- The infimum of two graphs `G` and `H`. The edges are precisely those on which `G` and `H` agree,
and the edge set is a subset of `E(G) ∩ E(H)`, with equality if `G` and `H` are compatible.  -/
Graph.instSemilatticeInf : {α : Type u_1} → {β : Type u_2} → SemilatticeInf (Graph α β)
-- Std.Sat.AIG.CachedLemmas
_private.Std.Sat.AIG.CachedLemmas.0.Std.Sat.AIG.mkGateCached.go.match_4.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (motive : (aig : Std.Sat.AIG α) → aig.BinaryInput → Sort u_1) →
        (aig : Std.Sat.AIG α) →
          (input : aig.BinaryInput) →
            ((decls : Array (Std.Sat.AIG.Decl α)) →
                (cache : Std.Sat.AIG.Cache α decls) →
                  (hdag : Std.Sat.AIG.IsDAG α decls) →
                    (hzero : 0 < decls.size) →
                      (hconst : decls[0] = Std.Sat.AIG.Decl.false) →
                        (input :
                            { decls := decls, cache := cache, hdag := hdag, hzero := hzero,
                                hconst := hconst }.BinaryInput) →
                          motive { decls := decls, cache := cache, hdag := hdag, hzero := hzero, hconst := hconst }
                            input) →
              motive aig input
-- Mathlib.Data.Stream.Init
Stream'.length_take : ∀ {α : Type u} (n : ℕ) (s : Stream' α), (Stream'.take n s).length = n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.mk_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W)
  (inr : Z ⟶ W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr),
  (CategoryTheory.Limits.PushoutCocone.mk inl inr eq).inl = inl
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex_H : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.leftHomologyDataShortComplex._auto_3),
  (X.leftHomologyDataShortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).H =
    CategoryTheory.Limits.cokernel (X.δToCycles f₁ f₂ f₃ n₀ n₁ ⋯)
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_bot : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S], Ideal.absNorm ⊥ = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.Truncated.whiskering_obj_obj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} (D : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (H : CategoryTheory.Functor C D)
  (F : CategoryTheory.Functor (SimplexCategory.Truncated n) C) {X Y : SimplexCategory.Truncated n} (f : X ⟶ Y),
  (((CategoryTheory.CosimplicialObject.Truncated.whiskering C D).obj H).obj F).map f = H.map (F.map f)
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- The affine space as a functor.  -/
AlgebraicGeometry.AffineSpace.functor : CategoryTheory.Functor Type uᵒᵖ (CategoryTheory.Functor AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme)
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `G` acts properly on `X`, then the quotient space is Hausdorff (T2).  -/
t2Space_quotient_mulAction_of_properSMul : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperSMul G X], T2Space (Quotient (MulAction.orbitRel G X))
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitForward_naturality₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F G : CategoryTheory.Functor Cᵒᵖ (Type v)} {η : F ⟶ A}
  {μ : G ⟶ A} (ε : F ⟶ G) (hε : CategoryTheory.CategoryStruct.comp ε μ = η) (X : C)
  (p : CategoryTheory.OverPresheafAux.YonedaCollection (CategoryTheory.OverPresheafAux.restrictedYonedaObj η) X),
  CategoryTheory.OverPresheafAux.unitForward μ X
      (CategoryTheory.OverPresheafAux.YonedaCollection.map₁
        (CategoryTheory.OverPresheafAux.restrictedYonedaObjMap₁ ε hε) p) =
    (CategoryTheory.ConcreteCategory.hom (ε.app (Opposite.op X))) (CategoryTheory.OverPresheafAux.unitForward η X p)
-- Init.Core
/-- `a \ b` is the set difference of `a` and `b`,
consisting of all elements in `a` that are not in `b`.


Conventions for notations in identifiers:

 * The recommended spelling of `\` in identifiers is `sdiff`. -/
«term_\_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Prod
Prod.instAddGroup : {G : Type u_1} → {H : Type u_2} → [AddGroup G] → [AddGroup H] → AddGroup (G × H)
-- Lean.Meta.Tactic.Grind.Types
/-- Mapping from binary functions `f` to a theorem `thm : ∀ a, f a a = .eq`
if it implements the `ReflCmp` type class.
 -/
Lean.Meta.Grind.State.reflCmpMap : Lean.Meta.Grind.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)
-- Mathlib.LinearAlgebra.Contraction
_private.Mathlib.LinearAlgebra.Contraction.0.finite_projective_of_one_mem_range_dualTensorHom : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  1 ∈ (dualTensorHom R M M).range → Module.Finite R M ∧ Module.Projective R M
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp},
  t₁.Equiv t₂ → ∀ (f : α → β → Option γ), (Std.TreeMap.filterMap f t₁).Equiv (Std.TreeMap.filterMap f t₂)
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- The part in the partition that `v` belongs to.  -/
SimpleGraph.Partition.partOfVertex : {V : Type u} → {G : SimpleGraph V} → G.Partition → V → Set V
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
/-- An ordered additive monoid with one-sided 'subtraction' in the sense that
if `a ≤ b`, then there is some `c` for which `a + c = b`. This is a weaker version
of the condition on canonical orderings defined by `CanonicallyOrderedAdd`.  -/
ExistsAddOfLE : (α : Type u) → [Add α] → [LE α] → Prop
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.isoMk_hom_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] [inst_3 : Q.RespectsIso] [inst_4 : W.RespectsIso]
  {A B : P.Arrow Q W} (f : A.left ≅ B.left) (g : A.right ≅ B.right)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp f.hom B.hom = CategoryTheory.CategoryStruct.comp A.hom g.hom)
      CategoryTheory.MorphismProperty.Arrow.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.Arrow.isoMk f g w).hom.left = f.hom
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l)[k'] = v
-- Init.Data.SInt.Lemmas
Int32.add_eq_right : ∀ {a b : Int32}, a + b = b ↔ a = 0
-- Mathlib.NumberTheory.MulChar.Basic
/-- The `n`th power of a quadratic character is the trivial character, when `n` is even.  -/
MulChar.IsQuadratic.pow_even : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {χ : MulChar R R'},
  χ.IsQuadratic → ∀ {n : ℕ}, Even n → χ ^ n = 1
-- Mathlib.Control.Functor
Functor.Comp.map_mk : ∀ {F : Type u → Type w} {G : Type v → Type u} [inst : Functor F] [inst_1 : Functor G] {α β : Type v} (h : α → β)
  (x : F (G α)), h <$> Functor.Comp.mk x = Functor.Comp.mk ((fun x => h <$> x) <$> x)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Right map, from `J.R` to `C`  -/
CategoryTheory.Limits.MultispanIndex.right : {J : CategoryTheory.Limits.MultispanShape} →
  {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Limits.MultispanIndex J C → J.R → C
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Given f : Y ⟶ X, this is the obvious functor from (T/X)/f to T/Y  -/
CategoryTheory.Over.iteratedSliceForward : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → (f : CategoryTheory.Over X) → CategoryTheory.Functor (CategoryTheory.Over f) (CategoryTheory.Over f.left)
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.bot_vertexSet : ∀ (α : Type u_4), ⊥.vertexSet = ∅
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.orthogonalProjectionSpan_reindex : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {m n : ℕ}
  (s : Affine.Simplex 𝕜 P m) (e : Fin (m + 1) ≃ Fin (n + 1)) (p : P),
  ↑((s.reindex e).orthogonalProjectionSpan p) = ↑(s.orthogonalProjectionSpan p)
-- Mathlib.Analysis.Complex.Norm
Complex.isCauSeq_norm : ∀ {f : ℕ → ℂ}, IsCauSeq (fun x => ‖x‖) f → IsCauSeq abs ((fun x => ‖x‖) ∘ f)
-- Init.Meta.Defs
Lean.idBeginEscape : Char
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LevelMVarErrorInfo.mk : Lean.LocalContext → Lean.Expr → Lean.Syntax → Option Lean.MessageData → Lean.Elab.Term.LevelMVarErrorInfo
-- Init.SimpLemmas
Bool.and_false : ∀ (b : Bool), (b && false) = false
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.ult_congr : ∀ {w : ℕ} (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → lhs'.ult rhs' = lhs.ult rhs
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.isBasis_iff_eq_sdiff_singleton : ∀ {α : Type u_1} {M : Matroid α} {C I : Set α}, M.IsCircuit C → (M.IsBasis I C ↔ ∃ e ∈ C, I = C \ {e})
-- Mathlib.CategoryTheory.InducedCategory
/-- Construct an isomorphism in the induced category
from an isomorphism in the original category.  -/
CategoryTheory.InducedCategory.isoMk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v, u₂} D] →
      {F : C → D} → {X Y : CategoryTheory.InducedCategory D F} → (F X ≅ F Y) → (X ≅ Y)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.mul_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α} [DecompositionMonoid α],
  IsRelPrime x z → IsRelPrime y z → IsRelPrime (x * y) z
-- Mathlib.ModelTheory.Fraisse
/-- A class `K` has the hereditary property when all finitely-generated structures that embed into
structures in `K` are also in `K`.  -/
FirstOrder.Language.Hereditary : {L : FirstOrder.Language} → Set (CategoryTheory.Bundled L.Structure) → Prop
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- The Hausdorff dimension of a set `s` is the infimum of all `d : ℝ≥0` such that the
`d`-dimensional Hausdorff measure of `s` is zero. This infimum is taken in `ℝ≥0∞`.
This gives an equivalent definition of the Hausdorff dimension.  -/
dimH_eq_iInf : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (s : Set X),
  dimH s = ⨅ d, ⨅ (_ : (MeasureTheory.Measure.hausdorffMeasure ↑d) s = 0), ↑d
-- Mathlib.RingTheory.DedekindDomain.GaussLemma
Polynomial.gaussNorm_intAdicAbv_le_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b) (p : Polynomial R), Polynomial.gaussNorm (v.intAdicAbv hb) 1 p ≤ 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_of_singular : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  ¬W.Nonsingular P → WeierstrassCurve.Jacobian.Point.toAffine W P = 0
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_mod_256 : ∀ (n : UInt8), n.toUInt32 % 256 = n.toUInt32
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.compare_getKey?_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  Option.all (fun x => decide (cmp x k = Ordering.eq)) (t.getKey? k) = true
-- Mathlib.Analysis.Normed.Order.Lattice
continuous_negPart : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  Continuous negPart
-- Mathlib.Analysis.Calculus.Deriv.Slope
HasDerivWithinAt.limsup_slope_le' : ∀ {f : ℝ → ℝ} {f' : ℝ} {s : Set ℝ} {x r : ℝ},
  HasDerivWithinAt f f' s x → x ∉ s → f' < r → ∀ᶠ (z : ℝ) in nhdsWithin x s, slope f x z < r
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.disjoint_base_iUnion_openCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D],
  Disjoint D (⋃ n, ⋃ j, Topology.RelCWComplex.openCell n j)
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
ContinuousLinearEquiv.conjContinuousAlgEquiv_surjective : ∀ (𝕜 : Type u_1) (V : Type u_2) (W : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : SeminormedAddCommGroup W] [inst_3 : NormedSpace 𝕜 V] [inst_4 : NormedSpace 𝕜 W] [SeparatingDual 𝕜 V]
  [SeparatingDual 𝕜 W], Function.Surjective ContinuousLinearEquiv.conjContinuousAlgEquiv
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Reorder a sum.

The difference with `Finset.sum_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.sum_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the sums.

The difference with `Finset.sum_equiv` is that bijectivity is only required to hold on the domains
of the sums, rather than on the entire types.  -/
Finset.sum_nbij' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : ι → κ) (j : κ → ι),
  (∀ a ∈ s, i a ∈ t) →
    (∀ a ∈ t, j a ∈ s) →
      (∀ a ∈ s, j (i a) = a) → (∀ a ∈ t, i (j a) = a) → (∀ a ∈ s, f a = g (i a)) → ∑ x ∈ s, f x = ∑ x ∈ t, g x
-- Mathlib.Analysis.Asymptotics.Theta
ContinuousOn.isTheta_principal : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : TopologicalSpace α] {s : Set α} {f : α → E} {c : F},
  ContinuousOn f s → IsCompact s → ‖c‖ ≠ 0 → (∀ i ∈ s, f i ≠ 0) → f =Θ[Filter.principal s] fun x => c
-- Lean.Elab.Tactic.Basic
/-- Get the mvarid of the main goal, run the given `tactic`,
then set the new goals to be the resulting goal list. -/
Lean.Elab.Tactic.liftMetaTactic : (Lean.MVarId → Lean.MetaM (List Lean.MVarId)) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.finset_sup_nhds : ∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L} {l : Filter α}
  {g : ι → L} [inst_1 : SemilatticeSup L] [inst_2 : OrderBot L] [ContinuousSup L],
  (∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) → Filter.Tendsto (s.sup f) l (nhds (s.sup g))