mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.isClassQuickConst? : Lean.Name → Lean.MetaM (Lean.LOption Lean.Name)
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.hpq : ∀ {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J}
  (self : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (i : I₁ × I₂ × I₃), self.q (i.1, self.p i.2) = r i
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∈ m₂ → (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffWithinAt.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieGroup I n G] {f g : M → G} {s : Set M} {x₀ : M},
  ContMDiffWithinAt I' I n f s x₀ → ContMDiffWithinAt I' I n g s x₀ → ContMDiffWithinAt I' I n (fun x => f x / g x) s x₀
-- Mathlib.Order.RelClasses
Prod.Lex.instIsWellFounded : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} [IsWellFounded α r] [IsWellFounded β s],
  IsWellFounded (α × β) (Prod.Lex r s)
-- Lean.Environment
/-- Returns the constants added in the current module, in elaboration tree pre-order: the top-level
declarations in elaboration order, each followed by its asynchronous sub-declarations, recursively.
The recursive part can optionally be skipped for theorems for when their sub-decls are unimportant
and visiting them would only add latency by having to wait for proof elaboration to finish.

Unlike iterating `env.constants.map₂`, this does not block on `env.checked`, i.e. kernel checking.
 -/
Lean.Environment.getLocalConstantInfos : Lean.Environment → optParam Bool false → BaseIO (Array Lean.AsyncConstantInfo)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.takeEndWhile_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice}, (s.copy.takeEndWhile pat).copy = (s.takeEndWhile pat).copy
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.smulCommClass : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u_3}
  [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] (P : Submodule R M) (T : Type u_4)
  [inst_6 : SMul T R] [inst_7 : SMul T M] [inst_8 : IsScalarTower T R M] [SMulCommClass S T M],
  SMulCommClass S T (M ⧸ P)
-- Std.Time.Date.Basic
Std.Time.instHAddOffset : HAdd Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.build : Std.Time.GenericFormat.DateBuilder✝ → Std.Time.Awareness → Option Std.Time.DateTime
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- The tensor product of two monoid algebras is the monoid algebra of their product.  -/
MonoidAlgebra.tensorEquiv : (R : Type u_1) →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommSemiring R] → TensorProduct R (MonoidAlgebra R M) (MonoidAlgebra R N) ≃ₗ[R] MonoidAlgebra R (M × N)
-- Mathlib.Geometry.Manifold.Algebra.Monoid
R_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G : Type u_8}
  [inst_4 : Semigroup G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (g h : G), smoothRightMul I (g * h) = (smoothRightMul I h).comp (smoothRightMul I g)
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.trivial_iff_lower_central_eq_bot : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M],
  LieModule.IsTrivial L M ↔ LieModule.lowerCentralSeries R L M 1 = ⊥
-- Mathlib.Analysis.RCLike.Sqrt
Complex.sqrt_neg_I : (-Complex.I).sqrt = ↑√2⁻¹ * (1 - Complex.I)
-- Lean.Meta.AppBuilder
/-- Returns a proof of `a = a`.  -/
Lean.Meta.mkEqRefl : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instSetLike.eq_1 : ∀ (M : Type u_1) [inst : AddZeroClass M],
  SaturatedAddSubmonoid.instSetLike M = { coe := fun x => x.carrier, coe_injective := ⋯ }
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- The action by an intermediate field is the action by the underlying field.  -/
IntermediateField.instMulActionSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → {X : Type u_4} → [MulAction L X] → (F : IntermediateField K L) → MulAction (↥F) X
-- Mathlib.Data.Fintype.Sets
Set.mem_toFinset : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] {a : α}, a ∈ s.toFinset ↔ a ∈ s
-- Mathlib.Topology.MetricSpace.Algebra
instLipschitzMulMultiplicativeOfLipschitzAdd : ∀ (α : Type u_1) [inst : PseudoMetricSpace α] [inst_1 : AddMonoid α] [LipschitzAdd α], LipschitzMul (Multiplicative α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Mathlib.Analysis.Complex.Norm
Complex.instIsComplete : CauSeq.IsComplete ℂ fun x => ‖x‖
-- Mathlib.Algebra.Category.Grp.Limits
AddCommGrpCat.addCommGroupObj.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommGrpCat) (j : J),
  AddCommGrpCat.addCommGroupObj F j =
    { toAdd := AddCommGrpCat.addCommGroupObj._aux_1 F j, add_assoc := ⋯,
      toZero := AddCommGrpCat.addCommGroupObj._aux_4 F j, zero_add := ⋯, add_zero := ⋯,
      toNSMul := AddCommGrpCat.addCommGroupObj._aux_8 F j, nsmul_zero := ⋯, nsmul_succ := ⋯,
      toNeg := AddCommGrpCat.addCommGroupObj._aux_12 F j, toSub := AddCommGrpCat.addCommGroupObj._aux_14 F j,
      toZSMul := AddCommGrpCat.addCommGroupObj._aux_16 F j, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯,
      zsmul_neg' := ⋯, neg_add_cancel := ⋯, add_comm := ⋯ }
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.le_of_mem_parts : ∀ {n : ℕ} {p : n.Partition} {m : ℕ}, m ∈ p.parts → m ≤ n
-- Std.Http.Server.Config
/-- Maximum number of trailer headers (default: 20)
 -/
Std.Http.Config.maxTrailerHeaders : Std.Http.Config → ℕ
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_X : ∀ (R : Type u_1) [inst : Semiring R] {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S), Polynomial.X.smeval x = x ^ 1
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.eq_normN : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α)
  (lhs rhs : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.eq_normN_cert lhs rhs = true →
    Lean.Grind.Linarith.Expr.denoteN ctx lhs = Lean.Grind.Linarith.Expr.denoteN ctx rhs
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Backward direction of the counit.  -/
CategoryTheory.OverPresheafAux.counitBackward : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) →
        (s : CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) →
          CategoryTheory.OverPresheafAux.OverArrows (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F)
              s.hom →
            F.obj (Opposite.op s)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.range_ι_le_evenOdd_one : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), (CliffordAlgebra.ι Q).range ≤ CliffordAlgebra.evenOdd Q 1
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
/-- Map from `Δ m → Δ m` which reduces a `FixedDetMatrix` towards a representative element
in reps  -/
FixedDetMatrices.reduce : {m : ℤ} → FixedDetMatrix (Fin 2) ℤ m → FixedDetMatrix (Fin 2) ℤ m
-- Init.Control.Reader
ReaderT.instAlternativeOfMonad : {m : Type u_1 → Type u_2} → {ρ : Type u_1} → [Alternative m] → [Monad m] → Alternative (ReaderT ρ m)
-- Mathlib.Algebra.Lie.Abelian
/-- A type synonym for an `R`-module to have a trivial Lie module structure.  -/
TrivialLieModule : Type u_1 → Type u_2 → Type u_3 → Type u_3
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_self_of_lt_one : ∀ {x y : ℝ}, 0 < x → x < 1 → 1 < y → x ^ y < x
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.RatCoeff.mk : {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«$α»)} → ℚ → Option Lean.Expr → Mathlib.Tactic.Ring.RatCoeff e
-- Std.Sync.StreamMap
/-- Convert to array of name-selector pairs
 -/
Std.StreamMap.toArray : {α β : Type} → Std.StreamMap α β → Array (α × Std.Async.Selector β)
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.ext : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A] {ψ φ : PontryaginDual A},
  (∀ (a : A), ψ a = φ a) → ψ = φ
-- Lean.Parser.Term
Lean.Parser.Term.sufficesDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.coe_ofContinuousOpen_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source),
  ↑(OpenPartialHomeomorph.ofContinuousOpen e hc ho hs).symm = ↑e.symm
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.basicOpen_hom_ext : ∀ {X : AlgebraicGeometry.RingedSpace} {R : CommRingCat} {α β : X ⟶ AlgebraicGeometry.Spec.sheafedSpaceObj R}
  (w : α.hom.base = β.hom.base),
  (∀ (r : ↑R),
      let U := PrimeSpectrum.basicOpen r;
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.CategoryStruct.comp
            (CommRingCat.ofHom
              (algebraMap (↑R) ((AlgebraicGeometry.structureSheafInType ↑R ↑R).obj.obj (Opposite.op U))))
            (α.hom.c.app (Opposite.op U)))
          (X.presheaf.map (CategoryTheory.eqToHom ⋯)) =
        CategoryTheory.CategoryStruct.comp
          (CommRingCat.ofHom (algebraMap (↑R) ((AlgebraicGeometry.structureSheafInType ↑R ↑R).obj.obj (Opposite.op U))))
          (β.hom.c.app (Opposite.op U))) →
    α = β
-- Mathlib.Algebra.Algebra.Operations
Submodule.smul_mono : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A] {M : Type u_1}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M] [inst_6 : IsScalarTower R A M]
  {I J : Submodule R A} {N P : Submodule R M}, I ≤ J → N ≤ P → I • N ≤ J • P
-- Mathlib.Logic.Embedding.Set
subtypeOrEquiv.congr_simp : ∀ {α : Type u_1} (p q : α → Prop) [inst : DecidablePred p] (h : Disjoint p q),
  subtypeOrEquiv p q h = subtypeOrEquiv p q h
-- Mathlib.Analysis.InnerProductSpace.OfNorm
InnerProductSpace.toInnerProductSpaceable_ofReal : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [InnerProductSpace ℝ E], InnerProductSpaceable E
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
MeasureTheory.setIntegral_norm_condExp_le : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {s : Set α},
  MeasurableSet s → ∀ (f : α → E), ∫ (x : α) in s, ‖μ[f | m] x‖ ∂μ ≤ ∫ (x : α) in s, ‖f x‖ ∂μ
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.CommRing.mk : Lean.Meta.Sym.Arith.Ring →
  Option Lean.Expr →
    Option ℕ → Lean.Expr → Lean.Expr → Option Lean.Expr → Option Lean.Expr → Lean.Meta.Sym.Arith.CommRing
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousMultilinearMap.alternatization.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : IsTopologicalAddGroup N] [inst_8 : Fintype ι] [inst_9 : DecidableEq ι],
  ContinuousMultilinearMap.alternatization =
    {
      toFun := fun f =>
        let __ContinuousMultilinearMap := ∑ σ, Equiv.Perm.sign σ • ContinuousMultilinearMap.domDomCongr σ f;
        { toContinuousMultilinearMap := __ContinuousMultilinearMap, map_eq_zero_of_eq' := ⋯ },
      map_zero' := ⋯, map_add' := ⋯ }
-- Std.Http.Data.URI.Encoding
/-- A percent-encoded URI fragment component. Valid characters are `pchar / "/" / "?"`.
 -/
Std.Http.URI.EncodedFragment : Type
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.coe_center : ∀ (G : Type u_1) [inst : Group G], ↑(Subgroup.center G) = Set.center G
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.symm_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β),
  (UpperSet.map f).symm = UpperSet.map f.symm
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanStaleDependencyParams.mk.sizeOf_spec : ∀ (staleDependency : Lean.Lsp.DocumentUri), sizeOf { staleDependency := staleDependency } = 1 + sizeOf staleDependency
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_neg_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β}, MeasureTheory.HasFiniteIntegral (-f) μ ↔ MeasureTheory.HasFiniteIntegral f μ
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forIn'.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (range : Std.Legacy.Range) (init : β)
  (f : (i : ℕ) → i ∈ range → β → m (ForInStep β)),
  range.forIn' init f = Std.Legacy.Range.forIn'.loop✝ range f init range.start ⋯ ⋯
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- Write the iterated Fréchet derivative as the composition of a continuous linear equiv and the
iterated derivative.  -/
iteratedFDeriv_eq_equiv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F},
  iteratedFDeriv 𝕜 n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv n f
-- Mathlib.Order.SymmDiff
/-- **Alias** of `bihimp_compl_self`. -/
bihimp_hnot_self : ∀ {α : Type u_2} [inst : HeytingAlgebra α] (a : α), bihimp a aᶜ = ⊥
-- Mathlib.Tactic.CategoryTheory.ToApp
/-- Given morphisms `f g : C ⟶ D` in the bicategory `Cat`, and an equation `η = θ` between 2-morphisms
(possibly after a `∀` binder), produce the equation `η.toNatTrans = θ.toNatTrans`
 -/
Mathlib.Tactic.CategoryTheory.ToApp.toNatTransExpr : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule.eq_1 : ∀ (R₀ : Type u_1) {R : Type u_2} [inst : CommRing R₀] [inst_1 : CommRing R] [inst_2 : Algebra R₀ R] {n : ℕ}
  (e : ChevalleyThm.PolynomialC.InductionObj✝ R n),
  ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule✝ R₀ e =
    Submodule.span R₀ ({1} ∪ ⋃ i, Set.range (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).coeff)
-- Lean.Message
/-- Optional tag shown in `trace.profiler.output` output after the trace class name.  -/
Lean.TraceData.tag : Lean.TraceData → String
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.length_toList_ric : ∀ {b : ℕ}, (*...=b).toList.length = b + 1
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the reverse direction of `Order.pred_eq_iff_isMin`. -/
IsMin.pred_eq : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a : α}, IsMin a → Order.pred a = a
-- Mathlib.Algebra.Group.Subgroup.Map
/-- The `MonoidHom` from the preimage of a subgroup to itself.  -/
MonoidHom.subgroupComap : {G : Type u_1} →
  {G' : Type u_2} →
    [inst : Group G] → [inst_1 : Group G'] → (f : G →* G') → (H' : Subgroup G') → ↥(Subgroup.comap f H') →* ↥H'
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_sInf_rng : ∀ {α : Type ua} {β : Type ub} {f : α → β} {u₁ : UniformSpace α} {u₂ : Set (UniformSpace β)},
  UniformContinuous f ↔ ∀ u ∈ u₂, UniformContinuous f
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.mk.sizeOf_spec : ∀ {J : Type u_1} [inst : LinearOrder J] {i j : J} [inst_1 : SizeOf J] (I : Set J)
  (left : autoParam (i ∈ I) CategoryTheory.SimplicialThickening.Path.left._autoParam)
  (right : autoParam (j ∈ I) CategoryTheory.SimplicialThickening.Path.right._autoParam)
  (left_le : autoParam (∀ k ∈ I, i ≤ k) CategoryTheory.SimplicialThickening.Path.left_le._autoParam)
  (le_right : autoParam (∀ k ∈ I, k ≤ j) CategoryTheory.SimplicialThickening.Path.le_right._autoParam),
  sizeOf { I := I, left := left, right := right, left_le := left_le, le_right := le_right } =
    1 + sizeOf left + sizeOf right
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- **The Lebesgue decomposition theorem**:
Any s-finite measure `μ` has Lebesgue decomposition with respect to any σ-finite measure `ν`.
That is to say, there exist a measure `ξ` and a measurable function `f`,
such that `ξ` is mutually singular with respect to `ν` and `μ = ξ + ν.withDensity f`  -/
MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SFinite μ]
  [MeasureTheory.SigmaFinite ν], μ.HaveLebesgueDecomposition ν
-- Mathlib.Algebra.Polynomial.Bivariate
/-- `evalEval x y p` is the evaluation `p(x,y)` of a two-variable polynomial `p : R[X][Y]`.  -/
Polynomial.evalEval : {R : Type u_1} → [inst : Semiring R] → R → R → Polynomial (Polynomial R) → R
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.comp_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃),
  (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃
-- Mathlib.Analysis.Calculus.Deriv.Support
HasStrictDerivAt.of_notMem_tsupport : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, x ∉ tsupport f → HasStrictDerivAt f 0 x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_eq_get_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : a ∈ m}, m.getKey a h = (m.getKey? a).get ⋯
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mkIso'_inv_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (e : M ≅ N)
  [inst_4 : CategoryTheory.IsMonHom e.hom], (CategoryTheory.Mon.mkIso' e).inv.hom = e.inv
-- Mathlib.Algebra.Group.Units.Defs
divp.eq_1 : ∀ {α : Type u} [inst : Monoid α] (a : α) (u : αˣ), a /ₚ u = a * ↑u⁻¹
-- Mathlib.Topology.Gluing
TopCat.GlueData.fromOpenSubsetsGlue_isOpenEmbedding : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α),
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.GlueData.fromOpenSubsetsGlue U))
-- Mathlib.ModelTheory.Syntax
/-- A theory indicating that a structure is infinite.  -/
FirstOrder.Language.infiniteTheory : (L : FirstOrder.Language) → L.Theory
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Mathlib.Algebra.Category.Grp.Images
/-- the corestriction map to the image  -/
AddCommGrpCat.factorThruImage : {G H : AddCommGrpCat} → (f : G ⟶ H) → G ⟶ AddCommGrpCat.image f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_eq_iff_coe_eq_or_eq_neg : ∀ {θ ψ : ℝ}, Real.cos θ = Real.cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ
-- Mathlib.Order.BourbakiWitt
NonemptyChain.isChain' : ∀ {α : Type u_4} [inst : LE α] (self : NonemptyChain α), IsChain (fun x1 x2 => x1 ≤ x2) self.carrier
-- Mathlib.Tactic.SetNotationForOrder
/-- Strict superset relation: `a ⊃ b`.
For types tagged with `@[use_set_notation_for_order]`,
the relation `GT.gt` is used instead of `SSuperset`.
The hover info shows which one is used. 

Conventions for notations in identifiers:

 * The recommended spelling of `⊃` in identifiers is `ssuperset`. -/
Mathlib.Meta.SetNotationForOrder.ssupsetStx' : Lean.TrailingParserDescr
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
/-- The commutator of a derivation `D` and a derivation of the form `ad x` is `ad (D x)`.  -/
LieDerivation.lie_der_ad_eq_ad_der : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (D : LieDerivation R L L) (x : L), ⁅D, (LieDerivation.ad R L) x⁆ = (LieDerivation.ad R L) (D x)
-- Init.Data.Fin.Basic
/-- Coarsens a bound to one at least as large.

See also `Fin.natAdd` and `Fin.addNat` for addition functions that increase the bound, and
`Fin.castLE` for a version that uses an explicit inequality proof.
 -/
Fin.castAdd : {n : ℕ} → (m : ℕ) → Fin n → Fin (n + m)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
HasFDerivAt.fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {f₂ : E → F × G} {f₂' : E →L[𝕜] F × G},
  HasFDerivAt f₂ f₂' x → HasFDerivAt (fun x => (f₂ x).1) (ContinuousLinearMap.fst 𝕜 F G ∘SL f₂') x
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategoryStruct.mk : {C : Type u} →
  [𝒞 : CategoryTheory.Category.{v, u} C] →
    (tensorObj : C → C → C) →
      ((X : C) → {Y₁ Y₂ : C} → (Y₁ ⟶ Y₂) → (tensorObj X Y₁ ⟶ tensorObj X Y₂)) →
        ({X₁ X₂ : C} → (X₁ ⟶ X₂) → (Y : C) → tensorObj X₁ Y ⟶ tensorObj X₂ Y) →
          ({X₁ Y₁ X₂ Y₂ : C} → (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (tensorObj X₁ X₂ ⟶ tensorObj Y₁ Y₂)) →
            (tensorUnit : C) →
              ((X Y Z : C) → tensorObj (tensorObj X Y) Z ≅ tensorObj X (tensorObj Y Z)) →
                ((X : C) → tensorObj tensorUnit X ≅ X) →
                  ((X : C) → tensorObj X tensorUnit ≅ X) → CategoryTheory.MonoidalCategoryStruct C
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.finsum_weightedHomogeneousComponent : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  (φ : MvPolynomial σ R), ∑ᶠ (m : M), (MvPolynomial.weightedHomogeneousComponent w m) φ = φ
-- Mathlib.Data.Finmap
Finmap.notMem_erase_self : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : Finmap β}, a ∉ Finmap.erase a s
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LRATStep.add.injEq : ∀ (id : ℕ) (lits proof : Array ℤ) (id_1 : ℕ) (lits_1 proof_1 : Array ℤ),
  (Mathlib.Tactic.Sat.LRATStep.add id lits proof = Mathlib.Tactic.Sat.LRATStep.add id_1 lits_1 proof_1) =
    (id = id_1 ∧ lits = lits_1 ∧ proof = proof_1)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∪ t₂).get? k = (t₂.get? k).or (t₁.get? k)