mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
/-- Cocones on `F : Jᵒᵖ ⥤ C` are equivalent to cones on `F.rightOp : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.coneRightOpOfCoconeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ C} → (CategoryTheory.Limits.Cocone F)ᵒᵖ ≌ CategoryTheory.Limits.Cone F.rightOp
-- Mathlib.Analysis.Convex.Deriv
/-- If `f` is convex on `S` and differentiable on `S`, then its derivative within `S` is monotone
on `S`.  -/
StrictConvexOn.strictMonoOn_derivWithin : ∀ {S : Set ℝ} {f : ℝ → ℝ}, StrictConvexOn ℝ S f → DifferentiableOn ℝ f S → StrictMonoOn (derivWithin f S) S
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.closed.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction}, sizeOf Std.Http.Protocol.H1.Reader.State.closed = 1
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.trivial_addMon_zero : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMonObj.zero = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Order.Iterate
/-- If `f` is a monotone map and `f x ≤ x` at some point `x`, then the iterates `f^[n] x` form
an antitone sequence.  -/
Monotone.antitone_iterate_of_map_le : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {x : α}, Monotone f → f x ≤ x → Antitone fun n => f^[n] x
-- Std.Data.HashMap.Iterator
/-- Returns a finite iterator over the values of a hash map.
The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.HashMap.Raw.valuesIter : {α β : Type u} → Std.HashMap.Raw α β → Std.Iter β
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_le_of_isTriangulatedClosed₂' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {Q : CategoryTheory.ObjectProperty C} [Q.IsTriangulatedClosed₂],
  P ≤ Q → ∀ (n : ℕ), P.extensionProductIter n ≤ Q.isoClosure
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- The rank of the range of a linear map is at most the rank of the source.  -/
lift_rank_range_le : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Cardinal.lift.{v, v'} (Module.rank R ↥f.range) ≤ Cardinal.lift.{v', v} (Module.rank R M)
-- Init.Prelude
/-- Strict inequality of natural numbers, usually accessed via the `<` operator.

It is defined as `n < m = n + 1 ≤ m`.
 -/
Nat.lt : ℕ → ℕ → Prop
-- Mathlib.NumberTheory.Dioph
/-- Diophantine functions are closed under multiplication.  -/
Dioph.«term_D*_» : Lean.TrailingParserDescr
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.brecOn.eq : ∀ {motive : Turing.ToPartrec.Code → Sort u} (t : Turing.ToPartrec.Code)
  (F_1 : (t : Turing.ToPartrec.Code) → Turing.ToPartrec.Code.below t → motive t),
  Turing.ToPartrec.Code.brecOn t F_1 = F_1 t (Turing.ToPartrec.Code.brecOn.go t F_1).2
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X : C} →
        (one : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) →
          (mul : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X) →
            autoParam
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one X) mul =
                  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom)
                CategoryTheory.MonObj.one_mul._autoParam →
              autoParam
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X one) mul =
                    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom)
                  CategoryTheory.MonObj.mul_one._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X) mul =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul)
                          mul))
                    CategoryTheory.MonObj.mul_assoc._autoParam →
                  CategoryTheory.MonObj X
-- Mathlib.Tactic.DefEqAbuse
/-- Convenience wrapper which accumulates the results of `visitM` across `arr`, attempting to
produce `empty` and `combine` from `{}` and `(· ++ ·)` or `(· ∪ ·)`.  -/
_private.Mathlib.Tactic.DefEqAbuse.0.Lean.MessageData.visitWithM : {m : Type → Type} →
  [Monad m] →
    {α : Type} →
      {β : Type u_1} →
        Array β →
          (β → m α) →
            autoParam α Lean.MessageData.visitWithM._auto_1✝ →
              autoParam (α → α → α) Lean.MessageData.visitWithM._auto_3✝ → m α
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (self : RootPairing ι R M N) (i j : ι),
  self.root j - (self.toLinearMap (self.root j)) (self.coroot i) • self.root i = self.root ((self.reflectionPerm i) j)
-- Mathlib.Data.Set.Function
Set.LeftInvOn.image_inter : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β} {f' : β → α},
  Set.LeftInvOn f' f s → f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.link.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced)
  (hr_2 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  Std.DTreeMap.Internal.Impl.link k v Std.DTreeMap.Internal.Impl.leaf r hr_2 hr =
    { impl := (Std.DTreeMap.Internal.Impl.insertMin k v r ⋯).impl, balanced_impl := ⋯, size_impl := ⋯ }
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance.eq_def : ∀ (pat : String.Slice) (patByte : UInt8) (table : Array ℕ) (ht : table.size ≤ pat.utf8ByteSize)
  (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i) (guess : ℕ) (hg : guess < table.size),
  String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h guess hg =
    if pat.getUTF8Byte { byteIdx := guess } ⋯ = patByte then ⟨guess + 1, ⋯⟩
    else
      if h₀ : guess = 0 then ⟨0, ⋯⟩
      else
        have this := ⋯;
        String.Slice.Pattern.ForwardSliceSearcher.buildTable.computeDistance✝ pat patByte table ht h table[guess - 1] ⋯
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.instQuotient : {A : Type u_1} → [inst : Ring A] → (relations : Module.Relations A) → Module A relations.Quotient
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.braiding_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (P Q : C),
  (CategoryTheory.Limits.coprod.braiding P Q).inv =
    CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_z : ∀ (u : PNat.XgcdType), u.flip.z = u.w
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.ιM_jointly_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM}
  (m : PresheafOfModules.ModuleColimit hcR hcM), ∃ U x, PresheafOfModules.ModuleColimit.ιM x = m
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mem_map_of_mem : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {m : M},
  m ∈ N → f m ∈ LieSubmodule.map f N
-- Mathlib.Algebra.Group.Action.Sum
Sum.smul_inl : ∀ {M : Type u_1} {α : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul M β] (a : M) (b : α),
  a • Sum.inl b = Sum.inl (a • b)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function preserves 1  -/
MulDistribMulActionHom.map_one' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (self : A →ₑ*[φ] B), self.toFun 1 = 1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating the second vector passed to `oangle` negates the sign of the angle.  -/
Orientation.oangle_sign_neg_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle x (-y)).sign = -(o.oangle x y).sign
-- Mathlib.CategoryTheory.Limits.Fubini
/-- The Fubini theorem for a functor `G : J × K ⥤ C`,
showing that the limit of `G` can be computed as
the limit of the limits of the functors `G.obj (j, _)`.
 -/
CategoryTheory.Limits.limitIsoLimitCurryCompLim : {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) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C] →
                [inst_4 :
                    CategoryTheory.Limits.HasLimit
                      ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] →
                  CategoryTheory.Limits.limit G ≅
                    CategoryTheory.Limits.limit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)
-- Mathlib.Combinatorics.Derangements.Basic
/-- The set of permutations `f` such that the preimage of `(a, f)` under
`Equiv.Perm.decomposeOption` is a derangement.  -/
derangements.Equiv.RemoveNone.fiber : {α : Type u_1} → [DecidableEq α] → Option α → Set (Equiv.Perm α)
-- Mathlib.Analysis.Normed.Group.Basic
dist_neg : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (x y : E), dist (-x) y = dist x (-y)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The category of simplicial objects valued in a category `C`.
This is the category of contravariant functors from `SimplexCategory` to `C`.  -/
CategoryTheory.SimplicialObject : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max v u)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Interpret a `LinearIsometryEquiv` as a `ContinuousLinearEquiv`.  -/
LinearIsometryEquiv.toContinuousLinearEquiv : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃SL[σ₁₂] E₂
-- Mathlib.Topology.Instances.CantorSet
cantorSequence_eq_self_sub_sum_cantorToTernary : ∀ (x : ℝ) (n : ℕ),
  (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, Real.ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n
-- Mathlib.Geometry.Manifold.ChartedSpace
sum_chartAt_inr_apply : ∀ {H : Type u} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] {x y : M'},
  ↑(chartAt H (Sum.inr x)) (Sum.inr y) = ↑(chartAt H x) y
-- Mathlib.RingTheory.Radical.Basic
/-- If `a` is a radical element, then it divides its radical.  -/
IsRadical.dvd_radical : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, IsRadical a → a ≠ 0 → a ∣ UniqueFactorizationMonoid.radical a
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.IsClosedUnderQuotients.prop_of_epi : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  [self : P.IsClosedUnderQuotients] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], P X → P Y
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsNonempty.of_nonempty_vertexSet : ∀ {α : Type u_1} {H : Hypergraph α}, H.vertexSet.Nonempty → H.IsNonempty
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.regularEpiIsStableUnderBaseChange : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Regular C],
  (CategoryTheory.MorphismProperty.regularEpi C).IsStableUnderBaseChange
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.δ_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) {i j : ℕ} (hij : j + 1 = i) (z : (Fin i → G) →₀ ↑X.X₃)
  (hz : (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₃).d i j)) z = 0)
  (y : (Fin i → G) →₀ ↑X.X₂),
  (CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap (MonoidHom.id G) X.g).f i)) y = z →
    ∀ (x : (Fin j → G) →₀ ↑X.X₁)
      (hx :
        (Finsupp.mapRange.linearMap (Rep.Hom.hom X.f).toLinearMap) x =
          (CategoryTheory.ConcreteCategory.hom ((groupHomology.inhomogeneousChains X.X₂).d i j)) y),
      (CategoryTheory.ConcreteCategory.hom (groupHomology.δ hX i j hij))
          ((CategoryTheory.ConcreteCategory.hom (groupHomology.π X.X₃ i)) (groupHomology.cyclesMk i j ⋯ z ⋯)) =
        (CategoryTheory.ConcreteCategory.hom (groupHomology.π X.X₁ j)) (groupHomology.cyclesMkOfCompEqD hX hx)
-- Lean.Elab.Command
Lean.Elab.Command.instMonadMacroAdapterCommandElabM : Lean.Elab.MonadMacroAdapter Lean.Elab.Command.CommandElabM
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.Options.mk.inj : ∀ {map : Lean.NameMap Lean.DataValue} {hasTrace : Bool} {map_1 : Lean.NameMap Lean.DataValue} {hasTrace_1 : Bool},
  { map := map, hasTrace := hasTrace } = { map := map_1, hasTrace := hasTrace_1 } → map = map_1 ∧ hasTrace = hasTrace_1
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.below.gate : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)}
  {motive : (a : ℕ) → (a_1 : Std.HashMap α ℕ) → Std.Sat.AIG.RelabelNat.State.Inv2 decls a a_1 → Prop} {idx : ℕ}
  {map : Std.HashMap α ℕ} {l r : Std.Sat.AIG.Fanin} (hinv : Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map)
  (hlt : idx < decls.size) (hatom : decls[idx] = Std.Sat.AIG.Decl.gate l r),
  Std.Sat.AIG.RelabelNat.State.Inv2.below hinv → motive idx map hinv → Std.Sat.AIG.RelabelNat.State.Inv2.below ⋯
-- Mathlib.Algebra.Group.Fin.Tuple
Fin.insertNth_mul : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (j : Fin (n + 1)) → Mul (α j)] (i : Fin (n + 1)) (x y : α i)
  (p q : (j : Fin n) → α (i.succAbove j)), i.insertNth (x * y) (p * q) = i.insertNth x p * i.insertNth y q
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernelIso_hom_desc : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0),
  CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelIso f).hom
      (CategoryTheory.Limits.cokernel.desc f g w) =
    SemiNormedGrp.explicitCokernelDesc w
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofFin : ∀ (x : Fin UInt16.size), (UInt16.ofFin x).toNat = ↑x
-- Std.Data.DHashMap.Basic
/-- Returns a list of all values present in the hash map in some order.  -/
Std.DHashMap.values : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → {β : Type v} → (Std.DHashMap α fun x => β) → List β
-- Mathlib.Data.Set.NAry
Set.Nonempty.image2 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
  s.Nonempty → t.Nonempty → (Set.image2 f s t).Nonempty
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.dropLast.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) →
      (Unit → motive []) →
        ((head : α) → motive [head]) → ((a : α) → (as : List α) → (as = [] → False) → motive (a :: as)) → motive x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The natural transformation `S.X₁ ⟶ S.cycles` for all short complexes `S`.  -/
CategoryTheory.ShortComplex.toCyclesNatTrans : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          CategoryTheory.ShortComplex.π₁ ⟶ CategoryTheory.ShortComplex.cyclesFunctor C
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.SpecialLinear.val_single : ∀ {n : Type u_1} {R : Type u₂} [inst : CommRing R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n) (h : i ≠ j)
  (r : R), ↑((LieAlgebra.SpecialLinear.single i j h) r) = Matrix.single i j r
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The morphism in the fiber over the domain.  -/
CategoryTheory.Pseudofunctor.Grothendieck.Hom.fiber : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      {X Y : F.Grothendieck} → (self : X.Hom Y) → (F.map self.base.toLoc).toFunctor.obj X.fiber ⟶ Y.fiber
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_pi' : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] {s : Set ι} {t : (i : ι) → Set (α i)}
  [h : ∀ (i : ι), (t i).OrdConnected], (s.pi t).OrdConnected
-- Init.Core
/-- Blocks the current thread until the given task has finished execution, and then returns the result
of the task. If the current thread is itself executing a (non-dedicated) task, the maximum
threadpool size is temporarily increased by one while waiting so as to ensure the process cannot
be deadlocked by threadpool starvation. Note that when the current thread is unblocked, more tasks
than the configured threadpool size may temporarily be running at the same time until sufficiently
many tasks have finished.

`Task.map` and `Task.bind` should be preferred over `Task.get` for setting up task dependencies
where possible as they do not require temporarily growing the threadpool in this way. In
particular, calling `Task.get` in a task continuation with `(sync := true)` will panic as the
continuation is decidedly not "cheap" in this case and deadlocks may otherwise occur. The
waited-upon task should instead be returned and unwrapped using `Task.bind/IO.bindTask`.
 -/
Task.get : {α : Type u} → Task α → α
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.neighborSet_ne_univ : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.neighborSet v ≠ Set.univ
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.le_toAddSubmonoid_saturation : ∀ {M : Type u_1} [inst : AddZeroClass M] {a : AddSubmonoid M}, a ≤ a.saturation.toAddSubmonoid
-- Mathlib.Order.OrdContinuous
/-- **Alias** of `LeftOrdContinuous.dual`. -/
LeftOrdContinuous.rightOrdContinuous_dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  LeftOrdContinuous f → RightOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_combineC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (p₁.combineC p₂ c) =
    Lean.Grind.CommRing.Poly.denote ctx p₁ + Lean.Grind.CommRing.Poly.denote ctx p₂
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_mul_of_le_one : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [AddLeftReflectLE R] [AddLeftMono R]
  [ExistsAddOfLE R] [inst_5 : Sub R] [OrderedSub R] {x : R},
  x ≤ 1 → ∀ (n : ℕ), (∑ i ∈ Finset.range n, x ^ i) * (1 - x) = 1 - x ^ n
-- Mathlib.RingTheory.PowerSeries.Substitution
_private.Mathlib.RingTheory.PowerSeries.Substitution.0.PowerSeries.substInvFun.match_1.splitter : (motive : ℕ → Sort u_1) →
  (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → (n = 0 → False) → motive n.succ) → motive x
-- Lean.Parser.Term
Lean.Parser.Command.versoCommentBody.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
AlgebraicGeometry.instIsOpenImmersionMapScheme : ∀ {X Y X' Y' : AlgebraicGeometry.Scheme} (f : X ⟶ X') (g : Y ⟶ Y') [AlgebraicGeometry.IsOpenImmersion f]
  [AlgebraicGeometry.IsOpenImmersion g], AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Limits.coprod.map f g)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_diff_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]? = none
-- Std.Data.HashMap.Lemmas
Std.HashMap.insertMany_ind : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {ρ : Type w} [inst : ForIn Id ρ (α × β)]
  {motive : Std.HashMap α β → Prop} (m : Std.HashMap α β) {l : ρ},
  motive m → (∀ (m : Std.HashMap α β) (a : α) (b : β), motive m → motive (m.insert a b)) → motive (m.insertMany l)
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)),
  (CochainComplex.mappingCone.trianglehMapOfHomotopy H).hom₂ = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeSet.ofList l cmp).get! k' = k
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.decidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (WithZero α)
-- Mathlib.Tactic.Algebra.Basic
/-- Push `algebraMap`s into sums and products and convert `algebraMap`s from `ℕ`, `ℤ` and `ℚ`
into casts.  -/
Mathlib.Tactic.Algebra.pushCast : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Data.Finsupp.Basic
Finsupp.domCongr_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (e : α ≃ β) (l : α →₀ M),
  (Finsupp.domCongr e) l = Finsupp.equivMapDomain e l
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.collectUsed : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.CodeDecl pu → optParam Lean.FVarIdHashSet ∅ → Lean.FVarIdHashSet
-- Std.Data.String.ToInt
String.Slice.toInt?_eq_toNat?_of_startsWith_eq_false : ∀ {s : String.Slice}, s.startsWith '-' = false → s.toInt? = Option.map (fun n => ↑n) s.toNat?