mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.cocone_naturality : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (F.map f) (MonCat.FilteredColimits.coconeMorphism F j') =
    MonCat.FilteredColimits.coconeMorphism F j
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
/-- `U.copy` specialised to graph embeddings.  -/
SimpleGraph.UnitDistEmbedding.embed : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} →
      {H : SimpleGraph W} →
        {E : Type u_3} → [inst : MetricSpace E] → G.UnitDistEmbedding E → H ↪g G → H.UnitDistEmbedding E
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.ofExtendIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cone F} {X : C} (i : X ⟶ s.pt)
  [inst_2 : CategoryTheory.IsIso i] (hs : CategoryTheory.Limits.IsLimit (s.extend i)),
  CategoryTheory.Limits.IsLimit.ofExtendIso i hs = hs.ofIsoLimit (s.extendIso (CategoryTheory.asIso' i)).symm
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.image_preimage_eq_preimage_image_of_isPullback : ∀ {X Y U V : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {f' : U ⟶ V} {iU : U ⟶ X} {iV : V ⟶ Y}
  [inst : AlgebraicGeometry.IsOpenImmersion iV] [inst_1 : AlgebraicGeometry.IsOpenImmersion iU],
  CategoryTheory.IsPullback f' iU iV f →
    ∀ (W : V.Opens),
      (AlgebraicGeometry.Scheme.Hom.opensFunctor iU).obj ((TopologicalSpace.Opens.map f'.base).obj W) =
        (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor iV).obj W)
-- Mathlib.Algebra.Group.Defs
/-- Multiplication is left cancellative (i.e. left regular).  -/
IsLeftCancelMul.mul_left_cancel : ∀ {G : Type u} {inst : Mul G} [self : IsLeftCancelMul G] (a : G), IsLeftRegular a
-- Mathlib.Topology.Connected.Basic
/-- The connected component of a point is the maximal connected set
that contains this point.  -/
connectedComponent : {α : Type u} → [TopologicalSpace α] → α → Set α
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.match_1.congr_eq_5 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (x : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (v : Lean.Grind.Linarith.Var),
  x = Lean.Grind.Linarith.Expr.var v →
    (match x with
      | a.sub b => h_1 a b
      | a.neg => h_2 a
      | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
      | Lean.Grind.Linarith.Expr.zero => h_4 ()
      | Lean.Grind.Linarith.Expr.var v => h_5 v
      | a.add b => h_6 a b
      | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) ≍
      h_5 v
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_le_iff_lipschitz : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F}
  {K : NNReal}, ‖f‖ ≤ ↑K ↔ LipschitzWith K ⇑f
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_trans_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (g : P ≃ₗ[R] Q)
  (f : N ≃ₗ[R] P) (x : TensorProduct R M N),
  (LinearEquiv.lTensor M (f ≪≫ₗ g)) x = (LinearEquiv.lTensor M g) ((LinearEquiv.lTensor M f) x)
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.coalgHomClass : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  CoalgHomClass (A →ₗc[R] B) R A B
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
/-- Given a hom orthogonal family `s : ι → C`
for which each `End (s i)` is a ring with invariant basis number (e.g. if each `s i` is simple),
if two direct sums over `s` are isomorphic, then they have the same multiplicities.
 -/
CategoryTheory.HomOrthogonal.equiv_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  [∀ (i : ι), InvariantBasisNumber (CategoryTheory.End (s i))],
  CategoryTheory.HomOrthogonal s →
    ∀ {α β : Type} [inst_4 : Finite α] [inst_5 : Finite β] {f : α → ι} {g : β → ι}
      (i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)), ∃ e, ∀ (a : α), g (e a) = f a
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.nat_eq_ofENat : ∀ {m : ℕ} {n : ℕ∞}, ↑m = ↑n ↔ ↑m = n
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.instCommRingRing : {R : Type u_1} → [inst : CommRing R] → (P : StandardEtalePair R) → CommRing P.Ring
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.π₀.sound : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} (e : SSet.Edge x₀ x₁), SSet.π₀.mk x₀ = SSet.π₀.mk x₁
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- Use `aesop_graph?` to pass along a `Try this` suggestion when using `aesop_graph`
 -/
aesop_graph? : Lean.ParserDescr
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.ScopedEntries.map : {β : Type} → Lean.ScopedEnvExtension.ScopedEntries β → Lean.SMap Lean.Name (Lean.PArray β)
-- Init.Data.Nat.Div.Basic
Nat.mod_zero : ∀ (a : ℕ), a % 0 = a
-- Init.Grind.AC
Lean.Grind.AC.Seq.insert_k_eq_insert : ∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq), Lean.Grind.AC.Seq.insert_k x s = Lean.Grind.AC.Seq.insert x s
-- Mathlib.RingTheory.MvPolynomial.Localization
_private.Mathlib.RingTheory.MvPolynomial.Localization.0.IsLocalization.Away.auxHom_mk : ∀ {R : Type u_2} [inst : CommRing R] (S : Type u_3) [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (p : MvPolynomial Unit R),
  (IsLocalization.Away.auxHom✝ S r) ((Ideal.Quotient.mk (Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1})) p) =
    (MvPolynomial.aeval fun x => IsLocalization.Away.invSelf r) p
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
For any real `a`, we have that `a ^ (2n+1) / n!` tends to `0` as `n → ∞`.  This is just a
reformulation of tendsto_pow_div_factorial_atTop, which asserts the same for `a ^ n / n!`
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.tendsto_pow_div_factorial_at_top_aux : ∀ (a : ℝ), Filter.Tendsto (fun n => a ^ (2 * n + 1) / ↑n.factorial) Filter.atTop (nhds 0)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.symmIso_inv : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex),
  (SSet.Subcomplex.unionProd.symmIso S T).inv =
    SSet.Subcomplex.lift (CategoryTheory.CategoryStruct.comp (T.unionProd S).ι (β_ Y X).hom) ⋯
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₀₂_τ₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.v₀₁.τ₂ (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Order.Floor.Defs
/-- `⌊a⌋₊` is the greatest natural `n` such that `n ≤ a`. If `a` is negative, then `⌊a⌋₊ = 0`.  -/
Nat.«term⌊_⌋₊» : Lean.ParserDescr
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.mul : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S},
  f₁ =o[l] g₁ → f₂ =o[l] g₂ → (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
-- Mathlib.Tactic.Widget.StringDiagram
/-- Penrose dsl file for string diagrams.  -/
Mathlib.Tactic.Widget.StringDiagram.dsl : String
-- Mathlib.Data.List.AList
AList.empty_entries : ∀ {α : Type u} {β : α → Type v}, ∅.entries = []
-- Lean.Meta.HaveTelescope
/-- The local decl for the `have`, so that the local context can be re-entered `have`-by-`have`.
N.B. This stores the fvarid for the `have` as well as cached versions of the value and type
instantiated with the fvars from the telescope.  -/
Lean.Meta.HaveInfo.decl : Lean.Meta.HaveInfo → Lean.LocalDecl
-- Mathlib.Order.Filter.Basic
Filter.eventually_or_distrib_right : ∀ {α : Type u} {f : Filter α} {p : α → Prop} {q : Prop}, (∀ᶠ (x : α) in f, p x ∨ q) ↔ (∀ᶠ (x : α) in f, p x) ∨ q
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.span_range_subtype_eq_top_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_9}
  (p : Submodule R M) {s : ι → M} (hs : ∀ (i : ι), s i ∈ p),
  Submodule.span R (Set.range fun i => ⟨s i, ⋯⟩) = ⊤ ↔ Submodule.span R (Set.range s) = p