mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Fin
List.sum_take_ofFn : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin n → M) (i : ℕ),
  (List.take i (List.ofFn f)).sum = ∑ j with ↑j < i, f j
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalSeminormedRing.toNonUnitalRing : {α : Type u_5} → [self : NonUnitalSeminormedRing α] → NonUnitalRing α
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Compositional version of `Measurable.add` for use by `fun_prop`.  -/
Measurable.add' : ∀ {M : Type u_2} {α : Type u_3} {β : Type u_4} [inst : MeasurableSpace M] [inst_1 : Add M] {m : MeasurableSpace α}
  {mβ : MeasurableSpace β} [MeasurableAdd₂ M] {f g : α → β → M} {h : α → β},
  Measurable ↿f → Measurable ↿g → Measurable h → Measurable fun a => (f a + g a) (h a)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.mem_pairs : ∀ (σ : Type u_1) [inst : DecidableEq σ] [inst_1 : Fintype σ] (k : ℕ) (t : Finset σ × σ),
  t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k ↔ t.1.card ≤ k ∧ (t.1.card = k → t.2 ∈ t.1)
-- Mathlib.Algebra.Order.Group.Abs
min_mabs_mabs_le_mabs_min : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] {a b : G}, min |a|ₘ |b|ₘ ≤ |min a b|ₘ
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
_private.Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup.0.Real.termΓ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBicone_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {J : Type w₁} {f : J → C}
  (b : CategoryTheory.Limits.Bicone f) (j : J), (F.mapBicone b).π j = F.map (b.π j)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintTextEdit.mk.inj : ∀ {range : Lean.Syntax.Range} {newText : String} {range_1 : Lean.Syntax.Range} {newText_1 : String},
  { range := range, newText := newText } = { range := range_1, newText := newText_1 } →
    range = range_1 ∧ newText = newText_1
-- Mathlib.Combinatorics.SimpleGraph.Hasse
/-- A walk induces a homomorphism from a path graph to the graph  -/
SimpleGraph.Walk.pathGraphHom : {V : Type u_3} → {G : SimpleGraph V} → {u v : V} → (w : G.Walk u v) → SimpleGraph.pathGraph (w.length + 1) →g G
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.pairwise_toList_le : ∀ {α : Type u} {r : Std.Roo α} [inst : LE α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLE α] [inst_7 : Std.Rxo.IsAlwaysFinite α],
  List.Pairwise (fun a b => a ≤ b) r.toList
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (input : aig.RefVec w) (idx : ℕ)
  (h1 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop aig input).aig.decls.size) (h2 : idx < aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpop aig input).aig.decls[idx] = aig.decls[idx]
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- `G.PreservesLeftKanExtensionAt F L c` asserts that `G` preserves all pointwise left Kan
extensions of `F` along `L` at the point `c`.  -/
CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt : {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] →
                CategoryTheory.Functor B D → CategoryTheory.Functor A B → CategoryTheory.Functor A C → C → Prop
-- Batteries.Control.AlternativeMonad
ReaderT.instLawfulAlternativeLift : ∀ {m : Type u_1 → Type u_2} {ρ : Type u_1} [inst : AlternativeMonad m], LawfulAlternativeLift m (ReaderT ρ m)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.exists_mem_support_pos_pairingIn_ne_zero : ∀ {ι : 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] {P : RootPairing ι R M N} {b : P.Base}
  [CharZero R] [inst_6 : P.IsCrystallographic] (i : ι), ∃ j ∈ b.support, P.pairingIn ℤ j i ≠ 0
-- Mathlib.Logic.Relation
/-- **Alias** of `Std.Symm.iff`. -/
Symmetric.iff : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r] (x y : α), r x y ↔ r y x
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_symm_apply : ∀ (K : Type u_1) [inst : Field K] (x : NumberField.mixedEmbedding.polarSpace K),
  (NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K).symm x = (fun w => x.1 ↑w, fun w => (x.1 ↑w, x.2 w))
-- Mathlib.Analysis.Analytic.Linear
analyticOn_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E}, AnalyticOn 𝕜 (fun x => x) s
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingHom.quotientKerEquivOfSurjective_apply_mk : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {f : R →+* S} (hf : Function.Surjective ⇑f) (x : R),
  (RingHom.quotientKerEquivOfSurjective hf) ((Ideal.Quotient.mk (RingHom.ker f)) x) = f x
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ioc_right_eq_Ioc_add_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] {a b : α} [NoMaxOrder α], a ≤ b → insert (b + 1) (Finset.Ioc a b) = Finset.Ioc a (b + 1)
-- Mathlib.CategoryTheory.Limits.Creates
/-- When `F` is fully faithful, to show that `F` creates the limit for `K` it suffices to exhibit a lift
of a limit cone for `K ⋙ F`.
 -/
CategoryTheory.createsLimitOfFullyFaithfulOfLift' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    {l : CategoryTheory.Limits.Cone (K.comp F)} →
                      CategoryTheory.Limits.IsLimit l →
                        (c : CategoryTheory.Limits.Cone K) → (F.mapCone c ≅ l) → CategoryTheory.CreatesLimit K F
-- Plausible.Testable
/-- In a goal of the shape `⊢ DecorationsOf p`, `mk_decoration` examines
the syntax of `p` and adds `NamedBinder` around universal quantifications
to improve error messages. This tool can be used in the declaration of a
function as follows:
```lean
def foo (p : Prop) (p' : Decorations.DecorationsOf p := by mk_decorations) [Testable p'] : ...
```
`p` is the parameter given by the user, `p'` is a definitionally equivalent
proposition where the quantifiers are annotated with `NamedBinder`.
 -/
Plausible.Decorations.tacticMk_decorations : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_natCast : ∀ (x : ℝ) (n : ℕ), x ^ ↑n = x ^ n
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_pure : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {c : ℝ} {f : α → E} {g : α → F}
  {x : α}, Asymptotics.IsBigOWith c (pure x) f g ↔ ‖f x‖ ≤ c * ‖g x‖
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.image_face_index_compl : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (c : f.Cell i) [inst_1 : P.IsProper], (SSet.stdSimplex.face {c.index}ᶜ).image c.map = (↑c.s).subcomplex
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.mk : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : Module k V1] →
                [inst_3 : AddTorsor V1 P1] →
                  [inst_4 : AddCommGroup V2] →
                    [inst_5 : Module k V2] →
                      [inst_6 : AddTorsor V2 P2] →
                        (toFun : P1 → P2) →
                          (linear : V1 →ₗ[k] V2) →
                            (∀ (p : P1) (v : V1), toFun (v +ᵥ p) = linear v +ᵥ toFun p) → P1 →ᵃ[k] P2
-- Mathlib.Combinatorics.Derangements.Finite
card_derangements_eq_numDerangements : ∀ (α : Type u_2) [inst : Fintype α] [inst_1 : DecidableEq α],
  Fintype.card ↑(derangements α) = numDerangements (Fintype.card α)
-- Init.Data.UInt.Lemmas
USize.zero_sub : ∀ (a : USize), 0 - a = -a
-- Mathlib.Data.List.Cycle
List.next.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ l), l.next x h = l.nextOr x (l.get ⟨0, ⋯⟩)
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.u_iInf_l : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  (gi : GaloisCoinsertion l u) {ι : Sort x} (f : ι → β), u (⨅ i, l (f i)) = ⨅ i, f i
-- Mathlib.CategoryTheory.Category.Cat
/-- The natural isomorphism corresponding to a 2-iso in `Cat`  -/
CategoryTheory.Cat.Hom.toNatIso : {X Y : CategoryTheory.Cat} → {F G : X ⟶ Y} → (F ≅ G) → (F.toFunctor ≅ G.toFunctor)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.inf_apply : ∀ (f g : CircleDeg1Lift) (x : ℝ), (f ⊓ g) x = min (f x) (g x)
-- Mathlib.Order.Hom.Basic
denselyOrdered_iff_of_strictAnti : ∀ {X : Type u_6} {Y : Type u_7} {F : Type u_8} [inst : LinearOrder X] [inst_1 : Preorder Y] [inst_2 : EquivLike F X Y]
  (f : F), StrictAnti ⇑f → (DenselyOrdered X ↔ DenselyOrdered Y)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableOn.iterate : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {f : E → E},
  DifferentiableOn 𝕜 f s → Set.MapsTo f s s → ∀ (n : ℕ), DifferentiableOn 𝕜 f^[n] s
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_nonneg : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (f : PadicSeq p), 0 ≤ f.norm
-- Aesop.Rule
Aesop.Safety.safe.sizeOf_spec : sizeOf Aesop.Safety.safe = 1
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertSmallerList.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l₁ l₂ : List ((a : α) × β a)),
  Std.Internal.List.insertSmallerList l₁ l₂ =
    if l₁.length ≤ l₂.length then Std.Internal.List.insertListIfNew l₂ l₁ else Std.Internal.List.insertList l₁ l₂
-- Mathlib.Analysis.Normed.Group.Constructions
/-- The (additive) norm on the multiplicative opposite is the same as the norm on the original type.

Note that we do not provide this more generally as `Norm Eᵐᵒᵖ`, as this is not always a good
choice of norm in the multiplicative `SeminormedGroup E` case.

We could repeat this instance to provide a `[SeminormedGroup E] : SeminormedGroup Eᵃᵒᵖ` instance,
but that case would likely never be used.
 -/
MulOpposite.instSeminormedAddGroup : {E : Type u_2} → [SeminormedAddGroup E] → SeminormedAddGroup Eᵐᵒᵖ
-- Mathlib.Algebra.Ring.Pi
Pi.addGroupWithOne : {I : Type u} → {f : I → Type v} → [(i : I) → AddGroupWithOne (f i)] → AddGroupWithOne ((i : I) → f i)
-- Lean.Level
Lean.Level.one : Lean.Level
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.instIsCocontinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D)
  [CategoryTheory.Functor.IsDenseSubsite J K G], G.IsCocontinuous J K
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (Std.DHashMap.Raw.Const.unitOfList l).contains k = l.contains k
-- Init.Data.Option.Lemmas
Option.any_false : ∀ {α : Type u_1} {o : Option α}, Option.any (fun x => false) o = false
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instOrdOrdinal : Ord Std.Time.Weekday.Ordinal
-- Init.Data.Array.MapIdx
Array.mapFinIdxM.map.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α) (f : (i : ℕ) → α → i < as.size → m β)
  (i j : ℕ) (inv : i + j = as.size) (bs : Array β),
  Array.mapFinIdxM.map as f i j inv bs =
    match i, inv with
    | 0, x => pure bs
    | i.succ, inv =>
      have j_lt := ⋯;
      have this := ⋯;
      do
      let __do_lift ← f j as[j] j_lt
      Array.mapFinIdxM.map as f i (j + 1) this (bs.push __do_lift)
-- Mathlib.Data.Option.Basic
Option.bind_congr' : ∀ {α : Type u_1} {β : Type u_2} {f g : α → Option β} {x y : Option α},
  x = y → (∀ a ∈ y, f a = g a) → x.bind f = y.bind g
-- Mathlib.Order.InitialSeg
InitialSeg.instFunLike : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → FunLike (InitialSeg r s) α β
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.induction_on_all_ex : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {P : {m : ℕ} → L.BoundedFormula α m → Prop}
  (φ : L.BoundedFormula α n),
  (∀ {m : ℕ} {ψ : L.BoundedFormula α m}, ψ.IsQF → P ψ) →
    (∀ {m : ℕ} {ψ : L.BoundedFormula α (m + 1)}, P ψ → P ψ.all) →
      (∀ {m : ℕ} {φ : L.BoundedFormula α (m + 1)}, P φ → P φ.ex) →
        (∀ {m : ℕ} {φ₁ φ₂ : L.BoundedFormula α m}, ∅.Iff φ₁ φ₂ → (P φ₁ ↔ P φ₂)) → P φ
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNonUnitalCommSemiring : {R : Type u_1} → [NonUnitalCommSemiring R] → NonUnitalCommSemiring Rᵃᵒᵖ
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffAt_finsetSum'`. -/
contMDiffAt_finset_sum' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (∑ i ∈ t, f i) x
-- Init.Data.List.Basic
List.isEmpty_nil : ∀ {α : Type u}, [].isEmpty = true
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.zero_div : ∀ (a : Ordinal.{u_4}), 0 / a = 0
-- Mathlib.Order.Category.PartOrd
PartOrd.Hom.ext_iff : ∀ {X Y : PartOrd} {x y : X.Hom Y}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Algebra.BigOperators.Finprod
finprod_emb_domain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : CommMonoid M] (f : α ↪ β)
  [inst_1 : DecidablePred fun x => x ∈ Set.range ⇑f] (g : α → M),
  (∏ᶠ (b : β), if h : b ∈ Set.range ⇑f then g (Classical.choose h) else 1) = ∏ᶠ (a : α), g a
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Constant functions are locally Lipschitz.  -/
LocallyLipschitz.const : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (b : β),
  LocallyLipschitz fun x => b
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.coe_mkHomeomorph_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], ⇑DomAddAct.mkHomeomorph.symm = ⇑DomAddAct.mk.symm
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_empty : ∀ {α : Type u}, ∅.size = 0
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.pruneSolvedGoals : Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Analysis.Normed.Group.Bounded
Filter.hasBasis_cobounded_norm' : ∀ {E : Type u_2} [inst : SeminormedGroup E], (Bornology.cobounded E).HasBasis (fun x => True) fun x => {x_1 | x ≤ ‖x_1‖}
-- Mathlib.Data.Option.Basic
guard.eq_1 : ∀ {f : Type → Type v} [inst : Alternative f] (p : Prop) [inst_1 : Decidable p], guard p = if p then pure () else failure
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasDetector.hasSeparator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasEqualizers C]
  [CategoryTheory.HasDetector C], CategoryTheory.HasSeparator C
-- Mathlib.FieldTheory.Fixed
/-- `MulSemiringAction.toAlgAut` is bijective.  -/
FixedPoints.toAlgAut_bijective : ∀ (G : Type u_2) (F : Type u_3) [inst : Group G] [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [Finite G]
  [FaithfulSMul G F], Function.Bijective ⇑(MulSemiringAction.toAlgAut G (↥(FixedPoints.subfield G F)) F)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.simplicialEvalσ_succ_getElem : ∀ {m : ℕ} (L : List ℕ),
  SimplexCategoryGenRel.IsAdmissible m L →
    ∀ {k : ℕ} {hk : k < L.length},
      SimplexCategoryGenRel.simplicialEvalσ L L[k] = SimplexCategoryGenRel.simplicialEvalσ L (L[k] + 1)
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.deriv_log_log_apply : ∀ {x : ℝ}, deriv (fun x => Real.log (Real.log x)) x = x⁻¹ / Real.log x
-- Init.Data.ByteArray.Basic
/-- True if the iterator is valid; that is, it is not past the array's last byte.
 -/
ByteArray.Iterator.hasNext : ByteArray.Iterator → Bool
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_le_succ : ∀ (a c : ℕ), a.choose c ≤ a.succ.choose c
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_lt_of_lt_div : ∀ {a b c : ENNReal}, a < b / c → a * c < b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_comp_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct Z W] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y W]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X W] {Z_1 : C} (h : Z ⨿ W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id W))
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map g (CategoryTheory.CategoryStruct.id W)) h)
-- Mathlib.Algebra.Algebra.Hom
/-- This is a special case of a more general instance that we define in a later file.  -/
Algebra.subsingleton_id : ∀ {R : Type u} (A : Type v) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Subsingleton (R →ₐ[R] A)
-- Mathlib.Analysis.Calculus.FDeriv.Pow
fderivWithin_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedAlgebra 𝕜 𝔸] [inst_4 : NormedSpace 𝕜 E] {f : E → 𝔸} {x : E}
  {s : Set E},
  UniqueDiffWithinAt 𝕜 s x →
    ∀ (n : ℕ),
      DifferentiableWithinAt 𝕜 f s x →
        fderivWithin 𝕜 (f ^ n) s x =
          ∑ i ∈ Finset.range n, MulOpposite.op (f x ^ i) • f x ^ (n.pred - i) • fderivWithin 𝕜 f s x
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- The origin corresponding to the converse direction (`← thm` vs. `thm`)  -/
Lean.Meta.Origin.converse : Lean.Meta.Origin → Option Lean.Meta.Origin
-- Mathlib.Order.Monotone.Defs
antitone_prod_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {h : α × β → γ}, Antitone h ↔ (∀ (a : α), Antitone fun b => h (a, b)) ∧ ∀ (b : β), Antitone fun a => h (a, b)
-- Lean.Setup
Lean.Import.module : Lean.Import → Lean.Name
-- Mathlib.NumberTheory.ZetaValues
/-- Reflection principle: `B_s(1 - x) = (-1)^s B_s(x)`  -/
bernoulliFun_eval_one_sub : ∀ {k : ℕ} {x : ℝ}, bernoulliFun k (1 - x) = (-1) ^ k * bernoulliFun k x
-- Mathlib.Order.WithBotTop
/-- A recursor for `WithBotTop` in terms of the coercion.  -/
WithBotTop.rec : {ι : Type u_1} →
  {motive : WithBotTop ι → Sort u_2} →
    motive ⊥ → ((a : ι) → motive (WithBotTop.coe a)) → motive ⊤ → (a : WithBotTop ι) → motive a
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.comap_subtype_eq_top : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M}, Submodule.comap p.subtype p' = ⊤ ↔ p ≤ p'
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.apply_coe_mem_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (S : Subsemigroup M) (x : ↥S),
  f ↑x ∈ Subsemigroup.map f S
-- Mathlib.RingTheory.OrzechProperty
OrzechProperty.instOfFinite : ∀ (R : Type u) [inst : Semiring R] [Finite R], OrzechProperty R
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.closure_range_inl_union_inr : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H],
  AddSubgroup.closure (Set.range ⇑AddMonoid.Coprod.inl ∪ Set.range ⇑AddMonoid.Coprod.inr) = ⊤
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorph_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : CompleteSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : CompleteSpace E] {F : Type u_3}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] [inst_7 : FiniteDimensional 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤),
  a ∈ (HasStrictFDerivAt.implicitToOpenPartialHomeomorph f f' hf hf').source
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsTransitive.union : ∀ {x y : ZFSet.{u}}, x.IsTransitive → y.IsTransitive → (x ∪ y).IsTransitive
-- Mathlib.Logic.Equiv.Sum
Equiv.sumAssoc_symm_apply_inr_inl : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (b : β),
  (Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
-- Lean.Parser.Basic
Lean.Parser.strAux : String → String → String.Pos.Raw → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.mkIso_inv_right : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (left : ψ.left ≅ ψ'.left) (right : ψ.right ≅ ψ'.right)
  (base : ψ.base ≅ ψ'.base)
  (left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left.hom F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_1)
  (right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right.hom G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base.hom)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransform.mkIso._auto_3),
  (CategoryTheory.Limits.CatCospanTransform.mkIso left right base left_coherence right_coherence).inv.right = right.inv
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The category `hoFunctor.obj (Δ[0])` is terminal.  -/
SSet.isTerminalHoFunctorDeltaZero : CategoryTheory.Limits.IsTerminal (SSet.hoFunctor.obj (SSet.stdSimplex.obj { len := 0 }))
-- Init.Data.BitVec.Lemmas
BitVec.sle_eq_decide : ∀ {w : ℕ} {x y : BitVec w}, x.sle y = decide (x.toInt ≤ y.toInt)