mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local extremum equals zero.  -/
IsLocalExtr.hasDerivAt_eq_zero : ∀ {f : ℝ → ℝ} {f' a : ℝ}, IsLocalExtr f a → HasDerivAt f f' a → f' = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.φ.eq_1 : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (d + 2)),
  SSet.prodStdSimplex.pairingCore.IsType₂.φ x hd i =
    if i = (SSet.prodStdSimplex.pairingCore.min x hd).castSucc then
      (k.castSucc, (x.cast hd).simplex.2 (SSet.prodStdSimplex.pairingCore.min x hd))
    else (SSet.prodStdSimplex.objEquiv (x.cast hd).simplex) ((SSet.prodStdSimplex.pairingCore.min x hd).predAbove i)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- The `AddSubgroup G` of the `AddGroup G`.  -/
AddSubgroup.instTop : {G : Type u_1} → [inst : AddGroup G] → Top (AddSubgroup G)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_inv_tensorUnit_right_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv h)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipIsoCurrySwapUncurry_inv_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (X : D) (X_1 : C),
  (F.flipIsoCurrySwapUncurry.inv.app X).app X_1 = CategoryTheory.CategoryStruct.id ((F.obj X_1).obj X)
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.coe_of : ∀ (M : Type u) [inst : Mul M], ↑(MagmaCat.of M) = M
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.last.eq_2 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x x_1 j k : ι) (_hne : j ≠ k)
  (w₁ : Monoid.CoprodI.NeWord M x j) (w₂ : Monoid.CoprodI.NeWord M k x_1), (w₁.append _hne w₂).last = w₂.last
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A subsingleton is totally bounded.  -/
Set.Subsingleton.totallyBounded : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α}, s.Subsingleton → TotallyBounded s
-- Mathlib.Control.Fold
Traversable.foldMap.eq_1 : ∀ {t : Type u → Type u} [inst : Traversable t] {α ω : Type u} [inst_1 : One ω] [inst_2 : Mul ω] (f : α → ω),
  Traversable.foldMap f = traverse (Functor.Const.mk' ∘ f)
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. `upperBoundP cut` retrieves the smallest entry comparing `gt` or `eq` under `cut`,
if it exists. If multiple keys in the map return `eq` under `cut`, any of them may be returned.
 -/
RBTree.RBSet.upperBoundP? : {α : Type u_1} → {cmp : α → α → Ordering} → RBTree.RBSet α cmp → (α → Ordering) → Option α
-- Mathlib.Tactic.Algebraize
/-- Given an expression `g.comp f` which is the composition of two `RingHom`s, this function adds
the instance `IsScalarTower A B C` to the context (if it does not already exist).  -/
Mathlib.Tactic.Algebraize.addIsScalarTowerInstanceFromRingHomComp : Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Analysis.Matrix.Spectrum
Matrix.IsHermitian.eigenvalues₀.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_2} [inst_1 : Fintype n] {A A_1 : Matrix n n 𝕜} (e_A : A = A_1)
  {inst_2 : DecidableEq n} [inst_3 : DecidableEq n] (hA : A.IsHermitian) (a a_1 : Fin (Fintype.card n)),
  a = a_1 → hA.eigenvalues₀ a = ⋯.eigenvalues₀ a_1
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
eq_on_inv₀ : ∀ {G₀ : Type u_3} {M₀' : Type u_4} {F' : Type u_7} [inst : GroupWithZero G₀] [inst_1 : MonoidWithZero M₀']
  [inst_2 : FunLike F' G₀ M₀'] {a : G₀} [MonoidWithZeroHomClass F' G₀ M₀'] (f g : F'), f a = g a → f a⁻¹ = g a⁻¹
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.semigroup.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Semigroup G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : ContMDiffMul I' n G], ContMDiffMap.semigroup = Function.Injective.semigroup DFunLike.coe ⋯ ⋯
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Cont.eval.match_1.eq_3 : ∀ (motive : Turing.ToPartrec.Cont → Sort u_1) (ns : List ℕ) (k : Turing.ToPartrec.Cont)
  (h_1 : Unit → motive Turing.ToPartrec.Cont.halt)
  (h_2 :
    (fs : Turing.ToPartrec.Code) →
      (as : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₁ fs as k))
  (h_3 : (ns : List ℕ) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.cons₂ ns k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.comp f k))
  (h_5 : (f : Turing.ToPartrec.Code) → (k : Turing.ToPartrec.Cont) → motive (Turing.ToPartrec.Cont.fix f k)),
  (match Turing.ToPartrec.Cont.cons₂ ns k with
    | Turing.ToPartrec.Cont.halt => h_1 ()
    | Turing.ToPartrec.Cont.cons₁ fs as k => h_2 fs as k
    | Turing.ToPartrec.Cont.cons₂ ns k => h_3 ns k
    | Turing.ToPartrec.Cont.comp f k => h_4 f k
    | Turing.ToPartrec.Cont.fix f k => h_5 f k) =
    h_3 ns k
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
multipliableUniformlyOn_of_clog : ∀ {α : Type u_1} {ι : Type u_2} {s : Set α} {f : ι → α → ℂ},
  SummableUniformlyOn (fun i x => Complex.log (f i x)) s →
    (∀ x ∈ s, ∀ (i : ι), f i x ≠ 0) →
      BddAbove ((fun x => (∑' (i : ι), Complex.log (f i x)).re) '' s) → MultipliableUniformlyOn f s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.inter_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₁).Equiv ↑m₂ → (↑(m₁.inter m₃)).Equiv ↑(m₂.inter m₃)
-- Mathlib.Data.PFun
/-- Preimage of a set under a partial function.  -/
PFun.preimage : {α : Type u_1} → {β : Type u_2} → (α →. β) → Set β → Set α
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the `minute` component of its `time` to the given value.
 -/
Std.Time.PlainDateTime.withMinutes : Std.Time.PlainDateTime → Std.Time.Minute.Ordinal → Std.Time.PlainDateTime
-- Lean.Message
/-- A lazy message.
The provided thunk will not be run until it is about to be displayed.
This can save computation in cases where the message may never be seen.

The `Dynamic` value is expected to be a `MessageData`,
which is a workaround for the positivity restriction.

If the thunked message is produced for a term that contains a synthetic sorry,
`hasSyntheticSorry` should return `true`.
This is used to filter out certain messages.  -/
Lean.MessageData.ofLazy : (Option Lean.PPContext → BaseIO Dynamic) → (Lean.MetavarContext → Bool) → Lean.MessageData
-- Aesop.Forward.RuleInfo
Aesop.Slot.mk.inj : ∀ {typeDiscrTreeKeys? : Option (Array Lean.Meta.DiscrTree.Key)} {index : Aesop.SlotIndex}
  {premiseIndex : Aesop.PremiseIndex} {deps common : Std.HashSet Aesop.PremiseIndex}
  {forwardDeps : Array Aesop.PremiseIndex} {typeDiscrTreeKeys?_1 : Option (Array Lean.Meta.DiscrTree.Key)}
  {index_1 : Aesop.SlotIndex} {premiseIndex_1 : Aesop.PremiseIndex} {deps_1 common_1 : Std.HashSet Aesop.PremiseIndex}
  {forwardDeps_1 : Array Aesop.PremiseIndex},
  { typeDiscrTreeKeys? := typeDiscrTreeKeys?, index := index, premiseIndex := premiseIndex, deps := deps,
        common := common, forwardDeps := forwardDeps } =
      { typeDiscrTreeKeys? := typeDiscrTreeKeys?_1, index := index_1, premiseIndex := premiseIndex_1, deps := deps_1,
        common := common_1, forwardDeps := forwardDeps_1 } →
    typeDiscrTreeKeys? = typeDiscrTreeKeys?_1 ∧
      index = index_1 ∧ premiseIndex = premiseIndex_1 ∧ deps = deps_1 ∧ common = common_1 ∧ forwardDeps = forwardDeps_1
-- Std.Http.Data.URI.Encoding
Std.Http.URI.EncodedString.instBEq : {r : UInt8 → Bool} → BEq (Std.Http.URI.EncodedString r)
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.markTheoremInstanceProof : Lean.Expr → Lean.Name → Lean.Expr
-- Init.Data.String.Basic
String.Slice.getUTF8Byte.congr_simp : ∀ (s s_1 : String.Slice) (e_s : s = s_1) (p p_1 : String.Pos.Raw) (e_p : p = p_1) (h : p < s.rawEndPos),
  s.getUTF8Byte p h = s_1.getUTF8Byte p_1 ⋯
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalNormedRing.toNormedAddCommGroup : {α : Type u_2} → [β : NonUnitalNormedRing α] → NormedAddCommGroup α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPower : BEq Lean.Grind.CommRing.Power
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Preadditive.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {x y : CategoryTheory.Preadditive C},
  CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroup → x = y
-- Mathlib.Combinatorics.Quiver.Path
/-- The length of a path is the number of arrows it uses.  -/
Quiver.Path.length : {V : Type u} → [inst : Quiver V] → {a b : V} → Quiver.Path a b → ℕ
-- Mathlib.Algebra.Order.Floor.Defs
Nat.floor_nat : Nat.floor = id
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Natural homomorphism sending `x : M`, `M` an `AddCommMonoid`, to the equivalence class of
`(x, 0)` in the Localization of `M` at a Submonoid.  -/
AddLocalization.addMonoidOf : {M : Type u_1} → [inst : AddCommMonoid M] → (S : AddSubmonoid M) → S.LocalizationMap (AddLocalization S)
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget₂CreatesLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J AddCommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections],
  AddCommMonCat.forget₂CreatesLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c' t =>
      {
        liftedCone :=
          {
            pt :=
              AddCommMonCat.of
                (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommMonCat))).pt,
            π :=
              {
                app := fun j =>
                  AddCommMonCat.ofHom
                    (AddMonCat.limitπAddMonoidHom (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)) j),
                naturality := ⋯ } },
        validLift :=
          (AddMonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat))).uniqueUpToIso
            t,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget₂ AddCommMonCat AddMonCat)
            (AddMonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)))
            (fun x =>
              {
                hom' :=
                  {
                    toFun := fun v =>
                      EquivLike.coe
                        (equivShrink
                          ↑((F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)).comp
                                (CategoryTheory.forget AddMonCat)).sections)
                        ⟨fun j =>
                          (CategoryTheory.ConcreteCategory.hom
                              (((CategoryTheory.forget AddMonCat).mapCone
                                      ((CategoryTheory.forget₂ AddCommMonCat AddMonCat).mapCone x)).π.app
                                j))
                            v,
                          ⋯⟩,
                    map_zero' := ⋯, map_add' := ⋯ } })
            ⋯ }
-- Lean.Expr
Lean.mkApp8 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.tensorObj_ext : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] {X₁ X₂ : CategoryTheory.GradedObject I C} [inst_3 : X₁.HasTensor X₂]
  {A : C} {j : I} (f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ j ⟶ A),
  (∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) g) →
    f = g
-- Mathlib.Data.Tree.Basic
/-- The left child of the tree, or `nil` if the tree is `nil`  -/
BinaryTree.left : {α : Type u} → BinaryTree α → BinaryTree α
-- Mathlib.Logic.Equiv.Defs
/-- A `PSigma`-type is equivalent to the corresponding `Sigma`-type.  -/
Equiv.psigmaEquivSigmaPLift : {α : Sort u_2} → (β : α → Sort u_1) → (i : α) ×' β i ≃ (i : PLift α) × PLift (β i.down)
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
CategoryTheory.Abelian.Pseudoelement.zero_eq_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C},
  ⟦CategoryTheory.Over.mk 0⟧ = 0
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.postEquiv_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : T ≌ D),
  (CategoryTheory.Under.postEquiv X F).unitIso =
    CategoryTheory.NatIso.ofComponents (fun A => CategoryTheory.Under.isoMk (F.unitIso.app A.right) ⋯) ⋯
-- Mathlib.Analysis.CStarAlgebra.Classes
CommCStarAlgebra.toCompleteSpace : ∀ {A : Type u_1} [self : CommCStarAlgebra A], CompleteSpace A
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
hasProd_nat_add_iff : ∀ {G : Type u_2} [inst : CommGroup G] {g : G} [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℕ → G} (k : ℕ),
  HasProd (fun n => f (n + k)) g ↔ HasProd f (g * ∏ i ∈ Finset.range k, f i)
-- Lean.Meta.Sym.AbstractS
/-- Abstracts free variables `xs[start...*]` in expression `e`, converting them to de Bruijn indices.

Assumptions:
- The local context of the metavariables occurring in `e` do not include the free variables being
  abstracted. This invariant holds when abstracting over binders during pattern matching/unification:
  metavariables in the pattern were created before entering the binder, so their contexts exclude
  the bound variable's corresponding fvar.

- If `xs[start...*]` is not empty, then the minimal variable is `xs[start]`.

- Subterms whose `maxFVar` is below `minFVarId` are skipped entirely. This function does not assume
the `maxFVar` cache contains information for every subterm in `e`.
 -/
Lean.Meta.Sym.abstractFVarsRange : Lean.Expr → ℕ → Array Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Algebra.Field.Basic
ofLex_ratCast : ∀ {K : Type u_1} [inst : RatCast K] (n : ℚ), ofLex ↑n = ↑n
-- Lean.DocString.Types
Lean.Doc.instReprPart : {i : Type u_1} → {b : Type u_2} → {p : Type u_3} → [Repr i] → [Repr b] → [Repr p] → Repr (Lean.Doc.Part i b p)
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- `MetricSpace` instance on the product of two metric spaces, using the `L^p` distance,
and having as uniformity the product uniformity.  -/
WithLp.instProdMetricSpace : (p : ENNReal) →
  (α : Type u_2) →
    (β : Type u_3) → [hp : Fact (1 ≤ p)] → [MetricSpace α] → [MetricSpace β] → MetricSpace (WithLp p (α × β))
-- Mathlib.Topology.Homotopy.Basic
/-- Composition of a `ContinuousMap.Homotopy g₀ g₁` and `f : C(X, Y)` as a homotopy between
`g₀.comp f` and `g₁.comp f`.  -/
ContinuousMap.Homotopy.compContinuousMap : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : TopologicalSpace X] →
        [inst_1 : TopologicalSpace Y] →
          [inst_2 : TopologicalSpace Z] →
            {g₀ g₁ : C(Y, Z)} → g₀.Homotopy g₁ → (f : C(X, Y)) → (g₀.comp f).Homotopy (g₁.comp f)
-- Mathlib.CategoryTheory.Yoneda
/-- The curried version of the Coyoneda lemma.  -/
CategoryTheory.largeCurriedCoyonedaLemma : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.coyoneda.rightOp.comp CategoryTheory.coyoneda ≅
      (CategoryTheory.evaluation C (Type v₁)).comp
        ((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor C (Type v₁)) (Type v₁) (Type (max u₁ v₁))).obj
          CategoryTheory.uliftFunctor.{u₁, v₁})
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_div'' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : Preorder α] [MulLeftMono α] {a b c d : α}, a ≤ b → c ≤ d → a / d ≤ b / c
-- Init.Data.Array.MapIdx
List.mapIdxM.go.eq_def : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : ℕ → α → m β) (a : List α)
  (a_1 : Array β),
  List.mapIdxM.go f a a_1 =
    match a, a_1 with
    | [], acc => pure acc.toList
    | a :: as, acc => do
      let __do_lift ← f acc.size a
      List.mapIdxM.go f as (acc.push __do_lift)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_sSup : ∀ {V : Type u} {G : SimpleGraph V} (s : Set G.Subgraph) (v : V), (sSup s).neighborSet v = ⋃ G' ∈ s, G'.neighborSet v
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_eq_getD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a : α}, Std.DTreeMap.Const.get! t a = Std.DTreeMap.Const.getD t a default
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.mk.sizeOf_spec : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  [inst_3 : SizeOf H] (toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H))
  (centralizer_centralizer' : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier),
  sizeOf { toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer' } =
    1 + sizeOf toStarSubalgebra + sizeOf centralizer_centralizer'
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.endFunctor_map : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (C : Type u') [inst_1 : CategoryTheory.Category.{v', u'} C]
  [inst_2 : ∀ (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)), CategoryTheory.Limits.HasEnd F]
  {X Y : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (f : X ⟶ Y),
  (CategoryTheory.Limits.endFunctor J C).map f = CategoryTheory.Limits.end_.map f
-- Mathlib.Util.AddRelatedDecl
/-- Elaborate an `(attr := ...)` argument.  -/
Mathlib.Tactic.elabOptAttrArg : Lean.TSyntax `Mathlib.Tactic.optAttrArg → Lean.Elab.TermElabM (Array Lean.Elab.Attribute)
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.comp_onRelation : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {L'' : FirstOrder.Language} (g : L' →ᴸ L'') (f : L →ᴸ L') (x : ℕ)
  (R : L.Relations x), (g.comp f).onRelation R = g.onRelation (f.onRelation R)
-- Mathlib.Algebra.Module.LinearMap.Defs
SemilinearMapClass.distribMulActionSemiHomClass : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} (F : Type u_14) [inst : Semiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M]
  [inst_5 : Module S M₃] {σ : R →+* S} [inst_6 : FunLike F M M₃] [SemilinearMapClass F σ M M₃],
  DistribMulActionSemiHomClass F (⇑σ) M M₃
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.degHom_lt_or_of_degHom_comp_lt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Z Y : C} (f : X ⟶ Z) (g : Z ⟶ Y),
  r.degHom (CategoryTheory.CategoryStruct.comp f g) < r.deg Z → r.degHom f < r.deg Z ∨ r.degHom g < r.deg Z
-- Mathlib.Analysis.Normed.Group.Defs
/-- A seminormed group is a group endowed with a norm for which `dist x y = ‖x⁻¹ * y‖` defines a
pseudometric space structure.  -/
SeminormedGroup : Type u_8 → Type u_8
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- A right extension `E : RightExtension L F` is a pointwise right Kan extension when
it is a pointwise right Kan extension at any object.  -/
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} → L.RightExtension F → Type (max (max (max (max u_2 u_4) v_4) v_2) u_1)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of two strictly monotone functions is strictly monotone.  -/
StrictMonoOn.mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} {s : Set β}
  [MulLeftStrictMono α] [MulRightStrictMono α],
  StrictMonoOn f s → StrictMonoOn g s → StrictMonoOn (fun x => f x * g x) s
-- Init.Classical
Classical.not_imp_iff_and_not : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The pullback cone `(𝟙 X, 𝟙 X)` for the pair `(f, f)` is a limit if `f` is a mono. The converse is
shown in `mono_of_pullback_is_id`.
 -/
CategoryTheory.Limits.PullbackCone.isLimitMkIdId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f : X ⟶ Y) →
        [CategoryTheory.Mono f] →
          CategoryTheory.Limits.IsLimit
            (CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.CategoryStruct.id X)
              (CategoryTheory.CategoryStruct.id X) ⋯)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.instInhabited : Inhabited Bipointed
-- Mathlib.Data.Set.Operations
Set.restrictPreimage_coe : ∀ {α : Type u} {β : Type v} (t : Set β) (f : α → β) (a : ↑(f ⁻¹' t)), ↑(t.restrictPreimage f a) = f ↑a
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_union_coloops_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.closure (X ∪ M.coloops) = M.closure X ∪ M.coloops
-- Mathlib.Data.Set.Lattice
Set.Ici_iSup : ∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] (f : ι → α), Set.Ici (⨆ i, f i) = ⋂ i, Set.Ici (f i)
-- Mathlib.Logic.Equiv.Defs
Equiv.ofBijective_coe : ∀ {α : Sort u} {β : Sort v} {f : α ≃ β}, Equiv.ofBijective ⇑f ⋯ = f
-- Mathlib.Algebra.Notation.Indicator
/-- See `Set.eqOn_mulIndicator` for the version with `s`.  -/
Set.eqOn_mulIndicator' : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M}, Set.EqOn (s.mulIndicator f) 1 sᶜ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  (Std.ExtHashMap.unitOfList l)[k]! = ()
-- Mathlib.Algebra.Group.EvenFunction
/-- An even function `f` satisfies `f (-x) = f x`.  -/
Function.Even.eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {f : α → β}, Function.Even f → ∀ (x : α), f (-x) = f x
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- The natural map from `G →₀ k` to `SkewMonoidAlgebra k G`.  -/
SkewMonoidAlgebra.ofCoeff : {k : Type u_1} → {G : Type u_2} → [inst : Zero k] → (G →₀ k) → SkewMonoidAlgebra k G
-- Lean.Elab.Do.Legacy
/-- Return true if the give code contains an exit point that satisfies `p`  -/
Lean.Elab.Term.Do.hasExitPointPred : Lean.Elab.Term.Do.Code → (Lean.Elab.Term.Do.Code → Bool) → Bool