mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Preorder.Chain
IsChain.image_relIso : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsChain r s → ∀ (φ : r ≃r r'), IsChain r' (⇑φ '' s)
-- Init.MetaTypes
/-- When `true` (default: `false`), local definitions are unfolded.
That is, given a local context containing `x : t := e`, then the free variable `x` reduces to `e`.
Otherwise, `x` must be provided as a `simp` argument.
 -/
Lean.Meta.Simp.Config.zetaDelta : Lean.Meta.Simp.Config → Bool
-- Aesop.Util.UnionFind
Aesop.UnionFind.mk : {α : Type u_1} →
  [inst : BEq α] → [inst_1 : Hashable α] → Array USize → Array USize → Std.HashMap α USize → Aesop.UnionFind α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See also `inv_le_of_inv_le₀` for a one-sided implication with one fewer assumption.  -/
inv_le_comm₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → 0 < b → (a⁻¹ ≤ b ↔ b⁻¹ ≤ a)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- To show that a left extension `t` is a Kan extension, we need to show that for every left
extension `s` there is a unique morphism `t ⟶ s`.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {t : CategoryTheory.Bicategory.LeftExtension f g} →
            (desc : (s : CategoryTheory.Bicategory.LeftExtension f g) → t ⟶ s) →
              (∀ (s : CategoryTheory.Bicategory.LeftExtension f g) (τ : t ⟶ s), τ = desc s) → t.IsKan
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuous_iff'_right : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α},
  Continuous f ↔ ∀ (b : β), Filter.Tendsto (fun x => (f b, f x)) (nhds b) (uniformity α)
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.inr_eq_mk : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : L),
  (LieAlgebra.SemiDirectSum.inr ψ) x = { left := 0, right := x }
-- Mathlib.Algebra.Star.Subalgebra
/-- The star operation on `Subalgebra` commutes with `Algebra.adjoin`.  -/
Subalgebra.star_adjoin_comm : ∀ (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] (s : Set A),
  star (Algebra.adjoin R s) = Algebra.adjoin R (star s)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instSemiring : {σ : Type u_1} → {R : Type u_2} → [Semiring R] → Semiring (MvPowerSeries σ R)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- A zero functor preserves colimits.  -/
CategoryTheory.Functor.preservesColimitsOfShape_of_isZero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D),
  CategoryTheory.Limits.IsZero G →
    ∀ (J : Type u_1) [inst_4 : CategoryTheory.Category.{v_1, u_1} J], CategoryTheory.Limits.PreservesColimitsOfShape J G
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_iUnion : ∀ {α : Type u_1} {G : SimpleGraph α} {ι : Type u_3} {s : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s → (G.IsClique (⋃ i, s i) ↔ ∀ (i : ι), G.IsClique (s i))
-- Mathlib.Data.List.Basic
List.idxOf_append_of_notMem : ∀ {α : Type u} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α] {a : α},
  a ∉ l₁ → List.idxOf a (l₁ ++ l₂) = l₁.length + List.idxOf a l₂
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- Preserving finite limits also implies preserving limits over finite shapes in higher universes,
though through a noncomputable instance.  -/
CategoryTheory.Limits.preservesLimitsOfShapeOfPreservesFiniteLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesFiniteLimits F] (J : Type w)
  [inst_3 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Std.Tactic.Do.Syntax
Lean.Elab.Tactic.Do.VCGen.Config.mk.sizeOf_spec : ∀ (trivial leave elimLets jp : Bool) (stepLimit : Option ℕ) (errorOnMissingSpec debug internalize : Bool),
  sizeOf
      { trivial := trivial, leave := leave, elimLets := elimLets, jp := jp, stepLimit := stepLimit,
        errorOnMissingSpec := errorOnMissingSpec, debug := debug, internalize := internalize } =
    1 + sizeOf trivial + sizeOf leave + sizeOf elimLets + sizeOf jp + sizeOf stepLimit + sizeOf errorOnMissingSpec +
        sizeOf debug +
      sizeOf internalize
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.maximalIdeal.congr_simp : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : IsLocalRing R],
  IsLocalRing.maximalIdeal R = IsLocalRing.maximalIdeal R
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functoriality_full : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C)
  (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful], (CategoryTheory.Limits.Cone.functoriality F G).Full
-- Mathlib.Topology.Bases
/-- A sum type of two second countable spaces is second countable.  -/
TopologicalSpace.instSecondCountableTopologySum : ∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [inst : TopologicalSpace β] [SecondCountableTopology α]
  [SecondCountableTopology β], SecondCountableTopology (α ⊕ β)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.beq_iff_equiv : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  m₁.WF → m₂.WF → ((m₁ == m₂) = true ↔ m₁.Equiv m₂)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The presheaf induced by a sieve is a subobject of the yoneda embedding.  -/
CategoryTheory.Sieve.functorInclusion_is_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X},
  CategoryTheory.Mono S.functorInclusion
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_eq_top_iff : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α}, s.einfsep = ⊤ ↔ s.Subsingleton
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.shiftFunctorZero'.congr_simp : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (ha : a = 0),
  CategoryTheory.shiftFunctorZero' C a ha = CategoryTheory.shiftFunctorZero' C a ha
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (Std.DTreeMap.Internal.Impl.insert! k v t).minKeyD fallback =
        t.minKey?.elim k fun k' => if (compare k k').isLE = true then k else k'
-- Lean.Elab.Deriving.Util
/-- Anticipates the default instance name for a derived instance.
 -/
Lean.Elab.Deriving.mkInstName : Lean.Name → Lean.Name → Lean.Elab.TermElabM Lean.Name
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Re-indexing the components of the tensor product by an equivalence `e` is compatible
with `PiTensorProduct.map`.  -/
PiTensorProduct.map_comp_reindex_eq : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11}
  [inst_3 : (i : ι) → AddCommMonoid (t i)] [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i)
  (e : ι ≃ ι₂),
  (PiTensorProduct.map fun i => f (e.symm i)) ∘ₗ ↑(PiTensorProduct.reindex R s e) =
    ↑(PiTensorProduct.reindex R t e) ∘ₗ PiTensorProduct.map f
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.extract.eq_1 : ∀ (s : String.Slice) (p₀ p₁ : s.Pos), s.extract p₀ p₁ = String.extract p₀.str p₁.str
-- Mathlib.Data.Rel
SetRel.core_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ) (u : Set γ),
  (R.comp S).core u = R.core (S.core u)
-- Mathlib.Algebra.Ring.Defs
Ring.toNonAssocRing : {α : Type u} → [Ring α] → NonAssocRing α
-- Mathlib.Algebra.Order.GroupWithZero.Finset
Finset.sup'_mul₀ : ∀ {ι : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : SemilatticeSup G₀] {a : G₀} [MulPosReflectLT G₀],
  0 ≤ a → ∀ (f : ι → G₀) (s : Finset ι) (hs : s.Nonempty), s.sup' hs f * a = s.sup' hs fun i => f i * a
-- Mathlib.Algebra.Group.Subgroup.Defs
exists_inv_mem_iff_exists_mem : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [SubgroupClass S G] {P : G → Prop},
  (∃ x ∈ H, P x⁻¹) ↔ ∃ x ∈ H, P x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
/-- The walk obtained by taking the first `n` darts of a walk.  -/
SimpleGraph.Walk.take : {V : Type u} → {G : SimpleGraph V} → {u v : V} → (p : G.Walk u v) → (n : ℕ) → G.Walk u (p.getVert n)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- Two affine subspaces are parallel if one is related to the other by adding the same vector
to all points.  -/
Affine.«term_∥_» : Lean.TrailingParserDescr
-- Init.Core
PSum.nonemptyRight : ∀ {β : Sort u_1} {α : Sort u_2} [h : Nonempty β], Nonempty (α ⊕' β)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Codegeneracy maps for a cosimplicial object.  -/
CategoryTheory.CosimplicialObject.σ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.CosimplicialObject C) → {n : ℕ} → Fin (n + 1) → (X.obj { len := n + 1 } ⟶ X.obj { len := n })
-- Mathlib.Order.RelSeries
RelSeries.mem_toList : ∀ {α : Type u_1} {r : SetRel α α} {s : RelSeries r} {x : α}, x ∈ s.toList ↔ x ∈ s
-- Init.Data.UInt.Lemmas
USize.ofNatClamp_uInt8ToNat : ∀ (n : UInt8), USize.ofNatClamp n.toNat = n.toUSize
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂)[k]? = t₂[k]?
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The bottom map in the left unitality square.
 -/
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (F : CategoryTheory.Functor C D) →
            ((CategoryTheory.MonoidalCategory.curriedTensor C).obj
                    (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).comp
                F ⟶
              F
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.commShiftIso_inv_app_counit_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (Y : D),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (G.comp F) a).inv.app Y)
      (adj.counit.app ((CategoryTheory.shiftFunctor D a).obj Y)) =
    (CategoryTheory.shiftFunctor D a).map (adj.counit.app Y)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
/-- Bijection between a subsemiring `S` and its opposite.  -/
Subsemiring.addEquivOp : {R : Type u_2} → [inst : NonAssocSemiring R] → (S : Subsemiring R) → ↥S ≃+ ↥S.op
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_mul_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M},
  UniqueFactorizationMonoid.radical (a * b) ∣ UniqueFactorizationMonoid.radical a * UniqueFactorizationMonoid.radical b
-- Mathlib.Order.MinMax
max_le_max : ∀ {α : Type u} [inst : LinearOrder α] {a b c d : α}, a ≤ c → b ≤ d → max a b ≤ max c d
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxiLawfulHasSize : ∀ {n : ℕ}, Std.Rxi.LawfulHasSize (BitVec n)
-- Init.Data.SInt.Bitwise
Int16.toISize_and : ∀ (a b : Int16), (a &&& b).toISize = a.toISize &&& b.toISize
-- Mathlib.Order.Cover
/-- **Alias** of the reverse direction of `toDual_wcovBy_toDual_iff`. -/
WCovBy.toDual : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b → OrderDual.toDual b ⩿ OrderDual.toDual a
-- Mathlib.GroupTheory.FixedPointFree
/-- The commutator map `g ↦ g / φ g`. If `φ g = h * g * h⁻¹`, then `g / φ g` is exactly the
commutator `[g, h] = g * h * g⁻¹ * h⁻¹`.  -/
MonoidHom.commutatorMap : {G : Type u_2} → (G → G) → [Div G] → G → G
-- Lean.Elab.Tactic.Omega.OmegaM
/-- If `groundInt? e = some i`,
then `e` is definitionally equal to the standard expression for `i`.
 -/
Lean.Elab.Tactic.Omega.groundInt? : Lean.Expr → Option ℤ
-- Mathlib.Topology.UniformSpace.Defs
uniformity_eq_symm : ∀ {α : Type ua} [inst : UniformSpace α], uniformity α = Filter.map Prod.swap (uniformity α)
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.denote'.go.match_1.splitter : (motive : Lean.Grind.Linarith.Poly → Sort u_1) →
  (p : Lean.Grind.Linarith.Poly) →
    (Unit → motive Lean.Grind.Linarith.Poly.nil) →
      ((v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add 1 v p)) →
        ((k : ℤ) →
            (v : Lean.Grind.Linarith.Var) →
              (p : Lean.Grind.Linarith.Poly) → (k = 1 → False) → motive (Lean.Grind.Linarith.Poly.add k v p)) →
          motive p
-- Init.Prelude
/-- Decides whether two strings are equal. Normally used via the `DecidableEq String` instance and the
`=` operator.

At runtime, this function is overridden with an efficient native implementation.
 -/
String.decEq : (s₁ s₂ : String) → Decidable (s₁ = s₂)
-- Mathlib.RingTheory.Polynomial.Basic
/-- If `R` is a nontrivial ring, the polynomials `R[X]` are not finite as an `R`-module. When `R` is
a field, this is equivalent to `R[X]` being an infinite-dimensional vector space over `R`.  -/
Polynomial.not_finite : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], ¬Module.Finite R (Polynomial R)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The restriction of a vector measure on some set.  -/
MeasureTheory.VectorMeasure.restrict : {α : Type u_1} →
  {mα : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] → MeasureTheory.VectorMeasure α M → Set α → MeasureTheory.VectorMeasure α M
-- Mathlib.Algebra.Group.Basic
add_eq_of_eq_add_neg : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a = c + -b → a + b = c
-- Aesop.RuleSet
Aesop.unindexPredicate? : Aesop.Options' → Option (Aesop.RuleName → Bool)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- Special case of the **Plünnecke-Ruzsa inequality**. Addition version.  -/
Finset.pluennecke_ruzsa_inequality_nsmul_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddCommGroup G] {A : Finset G},
  A.Nonempty → ∀ (B : Finset G) (n : ℕ), ↑(n • B).card ≤ (↑(A + B).card / ↑A.card) ^ n * ↑A.card
-- Mathlib.Algebra.Algebra.Basic
Module.isTorsionFree_iff_faithfulSMul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [IsDomain R] [IsDomain A],
  Module.IsTorsionFree R A ↔ FaithfulSMul R A
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
AEMeasurable.inner_const : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {m : MeasurableSpace α} [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E]
  [SecondCountableTopology E] {μ : MeasureTheory.Measure α} {f : α → E} {c : E},
  AEMeasurable f μ → AEMeasurable (fun x => inner 𝕜 (f x) c) μ
-- Init.Data.Nat.Basic
Nat.add_le_add_iff_right : ∀ {m k n : ℕ}, m + n ≤ k + n ↔ m ≤ k
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- A generalisation of `FriendlyOperation.coind` that allows using `op' ∘ opf` in the tail
of `op s` where `opf` is friendly and `op'` is a function satisfying `motive`.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind_comp_friend_right : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} (motive : (Stream'.Seq α → Stream'.Seq α) → Prop),
  motive op →
    (∀ (op : Stream'.Seq α → Stream'.Seq α),
        motive op →
          ∃ T,
            ∀ (s : Stream'.Seq α),
              (op s).destruct =
                Option.map
                  (fun x =>
                    match x with
                    | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
                  (T s.head)) →
      Tactic.ComputeAsymptotics.Seq.FriendlyOperation op
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion₂_mul : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Mul α] (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋃ i, ⋃ j, s i j) * t = ⋃ i, ⋃ j, s i j * t
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.instInhabitedMatchEqns.default : Lean.Meta.Match.MatchEqns
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
/-- The unit for the equivalence `Mon (C ⥤ D) ≌ C ⥤ Mon D`.
 -/
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor.id (CategoryTheory.Mon (CategoryTheory.Functor C D)) ≅
            CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functor.comp
              CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.inverse
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- Restrict domain and codomain of a linear map.  -/
LinearMap.restrict : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      (f : M →ₛₗ[σ₁₂] M₂) →
                        {p : Submodule R M} → {q : Submodule R₂ M₂} → (∀ x ∈ p, f x ∈ q) → ↥p →ₛₗ[σ₁₂] ↥q
-- Std.Tactic.Do.Syntax
/-- An invariant alternative of the form `· term`, one per invariant goal.
 -/
Lean.Parser.Tactic.invariantDotAlt : Lean.ParserDescr
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m] (v : m → α),
  Matrix.vecMul v 0 = 0
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instMul : Mul ONote
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsCofiltered.iff_of_equivalence : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (e : C ≌ D), CategoryTheory.IsCofiltered C ↔ CategoryTheory.IsCofiltered D
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves.eq_1 : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F],
  G.rightKanExtensionCompIsoOfPreserves F L =
    ((L.rightKanExtension F).comp G).rightKanExtensionUnique
      (CategoryTheory.CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv
        (CategoryTheory.Functor.whiskerRight (L.rightKanExtensionCounit F) G))
      (L.rightKanExtension (F.comp G)) (L.rightKanExtensionCounit (F.comp G))
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.contDiffOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {m n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → m ≤ n → (m = ↑⊤ → n = ⊤) → ∃ u ∈ nhds x, ContDiffOn 𝕜 m f u
-- Lean.Elab.Quotation
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.hasNoErrorIfUnused : Lean.Syntax → Bool
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.exists_add_of_le : ∀ {α : Type u_2} [inst : TopologicalSpace α] {f₁ f₂ : CompactlySupportedContinuousMap α NNReal},
  f₁ ≤ f₂ → ∃ g, f₁ + g = f₂
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Defs
IsIntegralClosure.mk : ∀ {A : Type u_1} {R : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R B] [inst_4 : Algebra A B],
  Function.Injective ⇑(algebraMap A B) →
    (∀ {x : B}, IsIntegral R x ↔ ∃ y, (algebraMap A B) y = x) → IsIntegralClosure A R B
-- Init.Data.Array.Lemmas
Array.flatMap_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} {f : α → Array β} {xs : Array α},
  Array.flatMap f xs = Array.foldl (fun acc a => acc ++ f a) #[] xs
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Given a diagram `D` of limit cones over the `curry.obj G j`, and a cone over `G`,
we can construct a cone over the diagram consisting of the cone points from `D`.
 -/
CategoryTheory.Limits.coneOfConeCurry : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              {D : CategoryTheory.Limits.DiagramOfCones (CategoryTheory.Functor.curry.obj G)} →
                ((j : J) → CategoryTheory.Limits.IsLimit (D.obj j)) →
                  CategoryTheory.Limits.Cone G → CategoryTheory.Limits.Cone D.conePoints
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.get? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → [Std.LawfulEqCmp cmp] → Std.ExtDTreeMap α β cmp → (a : α) → Option (β a)
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarAlgebra.elemental.instCompleteSpaceSubtypeMemNonUnitalStarSubalgebra : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : StarRing R] {A : Type u_3} [inst_2 : UniformSpace A]
  [CompleteSpace A] [inst_4 : NonUnitalSemiring A] [inst_5 : StarRing A] [inst_6 : IsSemitopologicalSemiring A]
  [inst_7 : ContinuousStar A] [inst_8 : Module R A] [inst_9 : IsScalarTower R A A] [inst_10 : SMulCommClass R A A]
  [inst_11 : StarModule R A] [inst_12 : ContinuousConstSMul R A] (x : A),
  CompleteSpace ↥(NonUnitalStarAlgebra.elemental R x)
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.applyAttributesCore : Lean.Name → Array Lean.Elab.Attribute → Option Lean.AttributeApplicationTime → Lean.Elab.TermElabM Unit
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_intro_l : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, (P ⊢ₛ Q) → P ⊢ₛ Q ∧ P
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The type (II) simplices of `h : A.PairingCore`, as a subset of `A.N`.  -/
SSet.Subcomplex.PairingCore.II : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → Set A.N
-- Init.Data.SInt.Bitwise
ISize.not_and_self : ∀ {a : ISize}, ~~~a &&& a = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_filter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool} {k : α},
  m.WF → (k ∈ Std.HashMap.Raw.filter f m ↔ ∃ (h' : k ∈ m), f (m.getKey k h') m[k] = true)