mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.dualProdDualEquivDual_apply_apply : ∀ (R : Type u_1) (M : Type u_3) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (M' : Type u_4)
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : (M →ₗ[R] R) × (M' →ₗ[R] R)) (a : M × M'),
  ((Module.dualProdDualEquivDual R M M') f) a = f.1 a.1 + f.2 a.2
-- Mathlib.Control.ULiftable
instULiftableStateTULift : {s : Type u₀} →
  {m : Type u₀ → Type u_5} →
    {m' : Type (max u₀ u_6) → Type u_7} → [ULiftable m m'] → ULiftable (StateT s m) (StateT (ULift.{u_6, u₀} s) m')
-- Lean.Data.Lsp.Basic
Lean.Lsp.ProgressParams.mk.injEq : ∀ {α : Type} (token : Lean.Lsp.ProgressToken) (value : α) (token_1 : Lean.Lsp.ProgressToken) (value_1 : α),
  ({ token := token, value := value } = { token := token_1, value := value_1 }) = (token = token_1 ∧ value = value_1)
-- Mathlib.RingTheory.MvPowerSeries.Equiv
/-- An inverse function of `optionFunLeft`.  -/
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.optionInvFunLeft : (σ : Type u_1) → (R : Type u_2) → [CommSemiring R] → PowerSeries (MvPowerSeries σ R) → MvPowerSeries (Option σ) R
-- Mathlib.Algebra.Torsor.Defs
/-- Adding a group element then subtracting the original point
produces that group element.  -/
vadd_vsub : ∀ {G : Type u_1} {P : Type u_2} [inst : AddGroup G] [T : AddTorsor G P] (g : G) (p : P), (g +ᵥ p) -ᵥ p = g
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- The `j`-th inclusion to the pushout.  -/
CategoryTheory.Limits.WidePushout.ι : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {B : C} →
        {objs : J → C} →
          (arrows : (j : J) → B ⟶ objs j) →
            [inst_1 : CategoryTheory.Limits.HasWidePushout B objs arrows] →
              (j : J) → objs j ⟶ CategoryTheory.Limits.widePushout B objs arrows
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL!.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3) (lls : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α) (lrv : β lrk) (lrl lrr : Std.DTreeMap.Internal.Impl α β)
  (h_1 :
    (lls : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner lls k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_3 : (x : Std.DTreeMap.Internal.Impl α β) → motive Std.DTreeMap.Internal.Impl.leaf x),
  (match Std.DTreeMap.Internal.Impl.inner lls k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr with
    | Std.DTreeMap.Internal.Impl.inner lls k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
      h_1 lls k v l r lrs lrk lrv lrl lrr
    | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l r
    | Std.DTreeMap.Internal.Impl.leaf, x => h_3 x) =
    h_1 lls k v l r lrs lrk lrv lrl lrr
-- Mathlib.Data.Int.ModEq
Int.modEq_and_modEq_iff_modEq_mul : ∀ {a b m n : ℤ}, m.natAbs.Coprime n.natAbs → (a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n])
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.epi_homologyMap_of_epi_of_not_rel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] [CategoryTheory.Epi (φ.f i)],
  (∀ (j : ι), ¬c.Rel i j) → CategoryTheory.Epi (HomologicalComplex.homologyMap φ i)
-- Std.Sync.RecursiveMutex
Std.instNonemptyBaseRecursiveMutex : Nonempty Std.BaseRecursiveMutex
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.eventually_measure_mul_le_scalingConstantOf_mul : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] (K : ℝ),
  ∃ R,
    0 < R ∧
      ∀ (x : α) (t r : ℝ),
        t ∈ Set.Ioc 0 K →
          r ≤ R →
            μ (Metric.closedBall x (t * r)) ≤
              ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
-- Init.Data.List.Lemmas
absurd.congr_simp : ∀ {a a_1 : Prop} (e_a : a = a_1) {b : Sort v} (h₁ : a) (h₂ : ¬a), absurd h₁ h₂ = absurd ⋯ ⋯
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
/-- The shift functor on the opposite category identifies to the opposite functor
of a shift functor on the original category.  -/
CategoryTheory.Pretriangulated.shiftFunctorOpIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (n m : ℤ) → n + m = 0 → (CategoryTheory.shiftFunctor Cᵒᵖ n ≅ (CategoryTheory.shiftFunctor C m).op)
-- Mathlib.Data.Finset.Sum
Finset.disjSum_ssubset_disjSum_of_ssubset_of_subset : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Finset α} {t₁ t₂ : Finset β}, s₁ ⊂ s₂ → t₁ ⊆ t₂ → s₁.disjSum t₁ ⊂ s₂.disjSum t₂
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_inv_right`. -/
MonovaryOn.of_inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g⁻¹ s → AntivaryOn f g s
-- Mathlib.RepresentationTheory.FDRep
/-- When `V` and `W` are finite-dimensional representations of a group `G`, the isomorphism
`dualTensorHomEquiv k V W` of vector spaces induces an isomorphism of representations.  -/
FDRep.dualTensorIsoLinHom : {k : Type u} →
  {G : Type v} →
    {V : Type u} →
      [inst : Field k] →
        [inst_1 : Group G] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              [inst_4 : FiniteDimensional k V] →
                (ρV : Representation k G V) →
                  (W : FDRep k G) →
                    CategoryTheory.MonoidalCategoryStruct.tensorObj (FDRep.of ρV.dual) W ≅ FDRep.of (ρV.linHom W.ρ)
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.mapConeToUnder_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F),
  c.mapConeToUnder.hom.hom = CategoryTheory.CategoryStruct.id c.pt
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a fallback : α} {v : β k},
      (t.insertIfNew k v).getKeyD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKeyD a fallback
-- Mathlib.NumberTheory.LSeries.Basic
LSeries.eq_zero_of_not_LSeriesSummable : ∀ (f : ℕ → ℂ) (s : ℂ), ¬LSeriesSummable f s → LSeries f s = 0
-- Mathlib.Dynamics.FixedPoints.Basic
/-- Any two maps `f : α → β` and `g : β → α` are inverse of each other on the sets of fixed points
of `f ∘ g` and `g ∘ f`, respectively.  -/
Function.invOn_fixedPoints_comp : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α),
  Set.InvOn f g (Function.fixedPoints (f ∘ g)) (Function.fixedPoints (g ∘ f))
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.addAssoc : FirstOrder.Field.FieldAxiom
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.toSyn_strictMono : ∀ {σ : Type u_1} (m : MonomialOrder σ), StrictMono ⇑m.toSyn
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_one : ∀ {α : Type u} [inst : Monoid α] [inst_1 : Invertible 1], ⅟1 = 1
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union₀ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet t μ →
    MeasureTheory.AEDisjoint μ s t →
      autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_union₀._auto_1 →
        autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_union₀._auto_3 → μ.real (s ∪ t) = μ.real s + μ.real t
-- Lean.Meta.Basic
/-- `higherOrderOutParam` is true if this parameter is a higher-order output parameter
of local instance.
Example:
```
getElem :
  {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
  {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
  (xs : cont) → (i : idx) → dom xs i → elem
```
This flag is true for the parameter `dom` because it is output parameter of
`[self : GetElem cont idx elem dom]`
 -/
Lean.Meta.ParamInfo.higherOrderOutParam : Lean.Meta.ParamInfo → Bool
-- Std.Sync.StreamMap
_private.Std.Sync.StreamMap.0.Std.StreamMap.mk.inj : ∀ {α β : Type} {streams streams_1 : Array (α × Std.Async.Selector β × IO Unit)},
  { streams := streams } = { streams := streams_1 } → streams = streams_1
-- Mathlib.Algebra.Ring.Equiv
RingEquivClass.toRingHomClass : ∀ {F : Type u_1} {R : Type u_4} {S : Type u_5} [inst : EquivLike F R S] [inst_1 : NonAssocSemiring R]
  [inst_2 : NonAssocSemiring S] [h : RingEquivClass F R S], RingHomClass F R S
-- Mathlib.Algebra.Ring.GrindInstances
Semiring.toGrindSemiring_ofNat : ∀ (α : Type u_1) [inst : Semiring α] (n : ℕ), OfNat.ofNat n = ↑n
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- In a strictly convex space, two vectors `x`, `y` are in the same ray if and only if the triangle
inequality for `x` and `y` becomes an equality.  -/
sameRay_iff_norm_add : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  SameRay ℝ x y ↔ ‖x + y‖ = ‖x‖ + ‖y‖
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.Legacy.foldr.eq_1 : ∀ {α : Type u} (f : Char → α → α) (init : α) (s_2 : String) (b e : String.Pos.Raw),
  Substring.Raw.Legacy.foldr f init { str := s_2, startPos := b, stopPos := e } = String.Legacy.foldrAux f init s_2 e b
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.HasInjectiveResolutions.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C],
  (∀ (Z : C), CategoryTheory.HasInjectiveResolution Z) → CategoryTheory.HasInjectiveResolutions C
-- Mathlib.Condensed.Discrete.Module
CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor : ∀ (R : Type (u + 1)) [inst : Ring R] (M : ModuleCat R),
  CategoryTheory.IsIso
    ((Condensed.forget R).map
      ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app ((CondensedMod.LocallyConstant.functor R).obj M)))
-- Init.PropLemmas
right_eq_dite_iff : ∀ {α : Sort u_1} {p : Prop} [inst : Decidable p] {x : p → α} {y : α},
  (y = if h : p then x h else y) ↔ ∀ (h : p), y = x h
-- Mathlib.Order.SupClosed
supClosure_isClosed : ∀ {α : Type u_3} [inst : SemilatticeSup α] (s : Set α), supClosure.IsClosed s = SupClosed s
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance_balance : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size),
  (Std.DTreeMap.Internal.Impl.balance k v l r hlb hrb hlr).Balanced
-- Init.Data.String.Slice
String.Slice.SplitIterator.operating.sizeOf_spec : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToForwardSearcher pat σ] [inst_1 : (a : String.Slice) → SizeOf (σ a)] [inst_2 : SizeOf ρ]
  (currPos : s.Pos) (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)),
  sizeOf (String.Slice.SplitIterator.operating currPos searcher) = 1 + sizeOf currPos + sizeOf searcher
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The Lie algebra of type Aₙ₋₁, isomorphic to sl(n).  -/
CartanMatrix.aₙ : (R : Type u_1) → [CommRing R] → ℕ → Type u_1
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instIsDedekindFiniteMonoid : ∀ {α : Type u_1} [inst : MulOne α] [IsDedekindFiniteMonoid α], IsDedekindFiniteMonoid αᵐᵒᵖ
-- Lean.Parser.Command
/-- `declVal` matches the right-hand side of a declaration, one of:
* `:= expr` (a "simple declaration")
* a sequence of `| pat => expr` (a declaration by equations), shorthand for a `match`
* `where` and then a sequence of `field := value` initializers, shorthand for a structure constructor
 -/
Lean.Parser.Command.declVal : Lean.Parser.Parser
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.iff_exact_iff_lTensor_exact : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔
    ∀ {N1 : Type (max u v)} [inst_3 : AddCommGroup N1] [inst_4 : Module R N1] {N2 : Type (max u v)}
      [inst_5 : AddCommGroup N2] [inst_6 : Module R N2] {N3 : Type (max u v)} [inst_7 : AddCommGroup N3]
      [inst_8 : Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
      Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.lTensor M l12) ⇑(LinearMap.lTensor M l23)
-- Mathlib.Order.SuccPred.Archimedean
le_total_of_directed : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [IsPredArchimedean α] {r v₁ v₂ : α},
  v₁ ≤ r → v₂ ≤ r → v₂ ≤ v₁ ∨ v₁ ≤ v₂
-- Init.Prelude
/-- Lifts a fully-polymorphic transformation of `m` into `n`.
 -/
MonadFunctorT.monadMap : {m : Type u → Type v} →
  {n : Type u → Type w} → [self : MonadFunctorT m n] → {α : Type u} → ({β : Type u} → m β → m β) → n α → n α
-- Mathlib.Order.CompleteBooleanAlgebra
Pi.instCoframe : {ι : Type u_1} → {π : ι → Type u_2} → [(i : ι) → Order.Coframe (π i)] → Order.Coframe ((i : ι) → π i)
-- Mathlib.Data.PNat.Basic
/-- Lemmas with div, dvd and mod operations  -/
PNat.modDivAux_spec : ∀ (k : ℕ+) (r q : ℕ), ¬(r = 0 ∧ q = 0) → ↑(k.modDivAux r q).1 + ↑k * (k.modDivAux r q).2 = r + ↑k * q
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
/-- Figures out the nested type formers of an inductive group, with parameters instantiated
and indices still forall-abstracted.

For example given a nested inductive
```
inductive Tree α where | node : α → Vector (Tree α) n → Tree α
```
(where `n` is an index of `Vector`) and the instantiation `Tree Int` it will return
```
#[(n : Nat) → Vector (Tree Int) n]
```

 -/
Lean.Elab.Structural.IndGroupInst.nestedTypeFormers : Lean.Elab.Structural.IndGroupInst → Lean.MetaM (Array Lean.Expr)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.ext_iff : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {S T : IntermediateField K L}, S = T ↔ ∀ (x : L), x ∈ S ↔ x ∈ T
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.fundamentalFrontier.eq_1 : ∀ (G : Type u_1) {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] (s : Set α),
  MeasureTheory.fundamentalFrontier G s = s ∩ ⋃ g, ⋃ (_ : g ≠ 1), g • s
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_counitIso_inv_app_hom_app_hom_apply_hom_apply : ∀ (X : CategoryTheory.Sheaf CategoryTheory.typesGrothendieckTopology (Type u)) (X_1 : Type uᵒᵖ)
  (x : X.obj.obj (Opposite.op (Opposite.unop X_1))) (x_1 : Opposite.unop X_1),
  (CategoryTheory.ConcreteCategory.hom
        ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.typeEquiv.counitIso.inv.app X).hom.app X_1)) x))
      x_1 =
    (CategoryTheory.ConcreteCategory.hom (X.obj.map (TypeCat.ofHom fun x => x_1).op)) x
-- Lean.Meta.SizeOf
Lean.Meta.SizeOfSpecNested.M : Type → Type
-- Init.Data.List.Find
List.Sublist.findSome?_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l₁ l₂ : List α},
  l₁.Sublist l₂ → (List.findSome? f l₁).isSome = true → (List.findSome? f l₂).isSome = true
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_mul : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f g : SkewMonoidAlgebra k G) [inst_3 : DecidableEq G], (f * g).support ⊆ f.support * g.support
-- Lean.Elab.PreDefinition.WF.GuessLex
/-- Internal monad used by `withRecApps`  -/
Lean.Elab.WF.GuessLex.M : Lean.Name → Type → Type → Type
-- Mathlib.Topology.Algebra.Module.Equiv
/-- If M is an `R`-module and `S`-module and `R`-module structure is defined by an action of `R` on
`S` (formally, we have two scalar towers), then any `S`-linear equivalence on `M` is an `R`-linear
equivalence.  -/
ContinuousLinearEquiv.restrictScalars : (R : Type u_1) →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              [inst_4 : Module S M] →
                [inst_5 : TopologicalSpace M] → [LinearMap.CompatibleSMul M M R S] → (M ≃L[S] M) → M ≃L[R] M
-- Mathlib.GroupTheory.ClassEquation
ConjClasses.noncenter.eq_1 : ∀ (G : Type u_6) [inst : Monoid G], ConjClasses.noncenter G = {x | x.carrier.Nontrivial}
-- Lean.Data.Lsp.Extra
/-- Internal `$/lean/waitForILeans` client->server request.

Yields a response once the watchdog process has loaded all .ilean files and has received
an ILean finalization notification for the worker and the document version designated in the request.
Used for test stability in tests that use the .ileans.
 -/
Lean.Lsp.WaitForILeansParams : Type
-- Init.Data.List.Attach
/-- This lemma identifies folds over lists of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
List.foldl_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : List { x // p x }} {f : β → { x // p x } → β} {g : β → α → β}
  {x : β}, (∀ (b : β) (x : α) (h : p x), f b ⟨x, h⟩ = g b x) → List.foldl f x l = List.foldl g x l.unattach
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.support_eq : ∀ {R : Type u_1} {E : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup E] [inst_4 : Module R E] (C : PointedCone R E), C.support = C.lineal.toAddSubgroup
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.occursInAt.eq_1 : ∀ {A : Type u_1} {G : Type u_2} [inst : Inhabited A] [inst_1 : AddMonoid G] (p : SymbolicDynamics.FullShift.Pattern A G)
  (x : G → A) (g : G), p.occursInAt x g = ∀ h ∈ p.support, x (g + h) = p.config h
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.contains_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.contains k = m₂.contains k
-- Mathlib.Topology.Inseparable
inseparable_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y ↔ nhds x = nhds y
-- Mathlib.Logic.Function.Basic
Function.RightInverse.leftInverse_of_injective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {g : β → α},
  Function.RightInverse f g → Function.Injective g → Function.LeftInverse f g
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimits.has_limits_of_shape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C] (J : Type v)
  [inst_2 : CategoryTheory.Category.{v, v} J], CategoryTheory.Limits.HasLimitsOfShape J C
-- Mathlib.Tactic.Simps.Basic
/-- A list of natural numbers, which is the projection number(s) that have to be applied to the
Expression. For example the list `[0, 1]` corresponds to applying the first projection of the
structure, and then the second projection of the resulting structure (this assumes that the
target of the first projection is a structure with at least two projections).
The composition of these projections is required to be definitionally equal to the provided
Expression.  -/
Simps.ProjectionData.projNrs : Simps.ProjectionData → List ℕ
-- Batteries.Data.MLList.Basic
/-- Implementation of `MLList.takeAsList`.  -/
_private.Batteries.Data.MLList.Basic.0.MLList.takeAsList.go : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → ℕ → List α → MLList m α → m (List α)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.le_restrict_univ_iff_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v w : MeasureTheory.VectorMeasure α M), v.restrict Set.univ ≤ w.restrict Set.univ ↔ v ≤ w
-- Mathlib.Analysis.Analytic.CPolynomial
CPolynomialAt.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  CPolynomialAt 𝕜 f x → CPolynomialAt 𝕜 g x → CPolynomialAt 𝕜 (f + g) x
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.apply_single : ∀ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} [inst : (i : ι) → Zero (M i)] [inst_1 : (i : ι) → Zero (N i)]
  [inst_2 : DecidableEq ι] (f' : (i : ι) → M i → N i),
  (∀ (i : ι), f' i 0 = 0) → ∀ (i : ι) (x : M i) (j : ι), f' j (Pi.single i x j) = Pi.single i (f' i x) j
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- If `x` is a nondegenerate `d`-simplex of `Δ[n]`, this is the order isomorphism
between `Fin (d + 1)` and the corresponding subset of `Fin (n + 1)` of cardinality `d + 1`.  -/
SSet.stdSimplex.orderIsoOfNonDegenerate : {n d : ℕ} →
  (x : ↑((SSet.stdSimplex.obj { len := n }).nonDegenerate d)) → Fin (d + 1) ≃o ↥↑(SSet.stdSimplex.nonDegenerateEquiv' x)
-- Init.Omega.Constraint
Lean.Omega.positivize?_eq_some : ∀ {s : Lean.Omega.Constraint} {x : Lean.Omega.Coeffs} {s' : Lean.Omega.Constraint} {x' : Lean.Omega.Coeffs},
  Lean.Omega.positivize? (s, x) = some (s', x') →
    Lean.Omega.positivizeConstraint s x = s' ∧ Lean.Omega.positivizeCoeffs s x = x'
-- Mathlib.Algebra.Divisibility.Basic
mul_dvd_mul_left : ∀ {α : Type u_1} [inst : Semigroup α] {b c : α} (a : α), b ∣ c → a * b ∣ a * c
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSliceData.mk.injEq : ∀ {α : Type u} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit) (range : Std.Rci α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit) (range_1 : Std.Rci α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The proposed colimit cocone is a colimit in `AddCommMonCat`.  -/
AddCommMonCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddCommMonCat) →
        CategoryTheory.Limits.IsColimit (AddCommMonCat.FilteredColimits.colimitCocone F)
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
/-- Constructor for `ModuleCat.Derivation`.  -/
ModuleCat.Derivation.mk : {A B : CommRingCat} →
  {M : ModuleCat ↑B} →
    {f : A ⟶ B} →
      (d : ↑B → ↑M) →
        autoParam (∀ (b b' : ↑B), d (b + b') = d b + d b') ModuleCat.Derivation.mk._auto_1 →
          autoParam (∀ (b b' : ↑B), d (b * b') = b • d b' + b' • d b) ModuleCat.Derivation.mk._auto_3 →
            autoParam (∀ (a : ↑A), d ((CategoryTheory.ConcreteCategory.hom f) a) = 0) ModuleCat.Derivation.mk._auto_5 →
              M.Derivation f
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.op_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} {Z' : Cᵒᵖ}
  {h : Opposite.op X ⟶ Z'},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).op h =
    CategoryTheory.CategoryStruct.comp g.op (CategoryTheory.CategoryStruct.comp f.op h)
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.instIsIsoInverse : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (e : CategoryTheory.IsoCat C D), e.inverse.IsIso
-- Std.Net.Addr
/-- Representation of an IPv6 address.
 -/
Std.Net.IPv6Addr : Type