mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.UpperLower.Fibration
/-- **Alias** of `Relation.Fibration.isUpperSet_image`. -/
IsUpperSet.image_fibration : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : LE α] [inst_1 : LE β],
  Relation.Fibration (fun x1 x2 => x1 ≥ x2) (fun x1 x2 => x1 ≥ x2) f → ∀ {s : Set α}, IsUpperSet s → IsUpperSet (f '' s)
-- Init.ByCases
if_false : ∀ {α : Sort u_1} {x : Decidable False} (t e : α), (if False then t else e) = e
-- Init.Data.AC
Lean.Data.AC.insert.eq_def : ∀ (x : ℕ) (x_1 : List ℕ),
  Lean.Data.AC.insert x x_1 =
    match x_1 with
    | [] => [x]
    | a :: as => if x < a then x :: a :: as else a :: Lean.Data.AC.insert x as
-- Lean.Data.LBool
Lean.LBool.undef.sizeOf_spec : sizeOf Lean.LBool.undef = 1
-- Init.Prelude
/-- A potential global constant or section variable reference, with additional field accesses  -/
Lean.Syntax.Preresolved.decl : Lean.Name → List String → Lean.Syntax.Preresolved
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.div_pow : ∀ {R : Type u_1} [inst : EuclideanDomain R] {a b : R} {n : ℕ}, b ∣ a → (a / b) ^ n = a ^ n / b ^ n
-- Init.Data.Subtype.Order
Subtype.instLawfulOrderMin : ∀ {α : Type u} [inst : LE α] [inst_1 : Min α] [inst_2 : Std.LawfulOrderMin α] {P : α → Prop},
  Std.LawfulOrderMin (Subtype P)
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.coeff_charpoly_mem_ideal_pow : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] {M : Matrix n n R}
  {I : Ideal R}, (∀ (i j : n), M i j ∈ I) → ∀ (k : ℕ), M.charpoly.coeff k ∈ I ^ (Fintype.card n - k)
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b c : ℝ} {γ : ℝ → M},
  a ≤ b → b ≤ c → Manifold.pathELength I γ a b + Manifold.pathELength I γ b c = Manifold.pathELength I γ a c
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_obj_obj₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (j : CategoryTheory.ComposableArrows ι 2),
  (X.ω₂.obj j).obj₁ = X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ (j.map (CategoryTheory.homOfLE ⋯)))
-- Mathlib.Tactic.SetNotationForOrder
/-- Dictionary used by `guessName` to autogenerate names.
This only transforms single name components, unlike `abbreviationDict`.

Note: `guessName` capitalizes the output according to the capitalization of the input.
In order for this to work, the input should always start with a lower case letter, and the output
should always start with an upper case letter.
 -/
_private.Mathlib.Tactic.SetNotationForOrder.0.Mathlib.Meta.SetNotationForOrder.nameDict : Std.HashMap String (List String)
-- Mathlib.Order.Filter.Bases.Basic
Filter.hasBasis_top : ∀ {α : Type u_1}, ⊤.HasBasis (fun x => True) fun x => Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.fst_eq_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} (self : I.SymmStruct)
  (i : ι), I.fst (i, i) = I.snd (i, i)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `2 ^ (k + 2)`-th cyclotomic extension of `ℚ` is `2`.
 -/
IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow : ∀ {k : ℕ} {K : Type u_1} [inst : Field K] {ζ : K} [inst_1 : CharZero K] [IsCyclotomicExtension {2 ^ (k + 2)} ℚ K]
  (hζ : IsPrimitiveRoot ζ (2 ^ (k + 2))), (Algebra.norm ℤ) (hζ.toInteger - 1) = 2
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.values_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.values = t₂.values
-- Mathlib.Order.Filter.AtTopBot.Field
/-- The function `fun x ↦ r * f x` tends to infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity.  -/
Filter.tendsto_const_mul_atTop_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔
    0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot
-- Init.Data.SInt.Basic
/-- Computes the absolute value of a 32-bit signed integer.

This function is equivalent to `if a < 0 then -a else a`, so in particular `Int32.minValue` will be
mapped to `Int32.minValue`.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.abs : Int32 → Int32
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallFullSubcategoryOfSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P], Small.{w, u} P.FullSubcategory
-- Mathlib.Algebra.Group.Pi.Lemmas
AddMonoidHom.coeFn_apply : ∀ (α : Type u_5) (β : Type u_6) [inst : AddZeroClass α] [inst_1 : AddCommMonoid β] (g : α →+ β) (a : α),
  (AddMonoidHom.coeFn α β) g a = g a
-- Mathlib.Analysis.Calculus.LHopital
/-- L'Hôpital's rule for approaching -∞, `HasDerivAt` version  -/
HasDerivAt.lhopital_zero_atBot : ∀ {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in Filter.atBot, HasDerivAt f (f' x) x) →
    (∀ᶠ (x : ℝ) in Filter.atBot, HasDerivAt g (g' x) x) →
      (∀ᶠ (x : ℝ) in Filter.atBot, g' x ≠ 0) →
        Filter.Tendsto f Filter.atBot (nhds 0) →
          Filter.Tendsto g Filter.atBot (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) Filter.atBot l → Filter.Tendsto (fun x => f x / g x) Filter.atBot l
-- Mathlib.Data.Set.Prod
Set.graphOn_prod_prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (s : Set α) (t : Set β) (f : α → γ) (g : β → δ),
  Set.graphOn (Prod.map f g) (s ×ˢ t) = ⇑(Equiv.prodProdProdComm α β γ δ) ⁻¹' Set.graphOn f s ×ˢ Set.graphOn g t
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
/-- The linear isomorphism to the submodule from the tensor product with a summand.  -/
DirectSum.decomposeTensorEquiv : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            (ℳ : ι → Submodule R M) →
              (N : Type u_5) →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : Module R N] →
                    [inst_5 : DecidableEq ι] →
                      [DirectSum.Decomposition ℳ] →
                        (i : ι) → TensorProduct R (↥(ℳ i)) N ≃ₗ[R] ↥(DirectSum.decomposeTensor ℳ N i)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.mul_log_nonneg : ∀ {x : ℝ}, 1 ≤ x → 0 ≤ x * Real.log x
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- Typecheck a continuous map as a morphism in the category `CompHausLike P`.  -/
CompHausLike.ofHom : (P : TopCat → Prop) →
  {X : Type u} →
    [inst : TopologicalSpace X] →
      [inst_1 : CompactSpace X] →
        [inst_2 : T2Space X] →
          [inst_3 : CompHausLike.HasProp P X] →
            {Y : Type u} →
              [inst_4 : TopologicalSpace Y] →
                [inst_5 : CompactSpace Y] →
                  [inst_6 : T2Space Y] →
                    [inst_7 : CompHausLike.HasProp P Y] → C(X, Y) → (CompHausLike.of P X ⟶ CompHausLike.of P Y)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.skipSuffix?.eq_1 : ∀ {ρ : Type} (s : String.Slice) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  s.skipSuffix? pat = String.Slice.Pattern.BackwardPattern.skipSuffix? pat s
-- Init.Data.String.Lemmas.Hashable
String.Slice.instLawfulHashable : LawfulHashable String.Slice
-- Mathlib.Algebra.Lie.TransferInstance
LinearEquiv.lieEquiv_symm_apply : ∀ {R : Type u_1} {M : Type u_2} {L : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (e : M ≃ₗ[R] L) (b : L), (LinearEquiv.lieEquiv R e).symm b = e.symm b
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.smul_mem_orbit_smul : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g h : G) (a : α),
  g • a ∈ MulAction.orbit G (h • a)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : LawfulBEq α] {f : α → β → γ} {k : α} {fallback : γ},
  Std.ExtDHashMap.Const.getD (Std.ExtDHashMap.map f m) k fallback =
    (Option.map (f k) (Std.ExtDHashMap.Const.get? m k)).getD fallback
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.ofCoprodI_of : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Monoid (G i)] [inst_1 : Monoid H]
  {φ : (i : ι) → H →* G i} (i : ι) (g : G i), Monoid.PushoutI.ofCoprodI (Monoid.CoprodI.of g) = (Monoid.PushoutI.of i) g
-- Mathlib.Topology.List
/-- Continuity of `Vector.insertIdx`.  -/
List.Vector.continuous_insertIdx' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)},
  Continuous fun p => List.Vector.insertIdx p.1 i p.2
-- Mathlib.Data.Finset.Sups
Finset.mem_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α} {a : α}, a ∈ s.compls ↔ aᶜ ∈ s
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_source_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {s : Set M} {x : M},
  x ∈ f.source → (f.extend I).source ∈ nhdsWithin x s
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is
the obvious functor `w.StructuredArrowRightwards g ⥤ w.CostructuredArrowDownwards g`.  -/
CategoryTheory.TwoSquare.EquivalenceJ.functor : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        (w : CategoryTheory.TwoSquare T L R B) →
                          {X₂ : C₂} →
                            {X₃ : C₃} →
                              (g : R.obj X₂ ⟶ B.obj X₃) →
                                CategoryTheory.Functor (w.StructuredArrowRightwards g) (w.CostructuredArrowDownwards g)
-- Lean.Elab.PreDefinition.WF.Fix
/-- Below we need a way to identify local contexts, and check if one is included in the other.
We use the last free variable for that. This works because

* the code below never sees an empty context
* contexts are extended with fresh variable names
* we do not clear free variable in this code
 -/
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.LCtxId : Type
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
LeftPreLieRing.assoc_symm : ∀ {L : Type u_2} [inst : LeftPreLieRing L] (x y z : L), associator x y z = associator y x z
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.map_bind₂ : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} {T : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (f : R →+* MvPolynomial σ S) (g : S →+* T) (φ : MvPolynomial σ R),
  (MvPolynomial.map g) ((MvPolynomial.bind₂ f) φ) = (MvPolynomial.bind₂ ((MvPolynomial.map g).comp f)) φ
-- Mathlib.RingTheory.PowerSeries.WellKnown
PowerSeries.invOneSubPow_zero : ∀ (S : Type u_1) [inst : CommRing S], PowerSeries.invOneSubPow S 0 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullback.exists_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] (h : W ⟶ X) (k : W ⟶ Y),
  autoParam (CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g)
      CategoryTheory.Limits.pullback.exists_lift._auto_1 →
    ∃ l,
      CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.fst f g) = h ∧
        CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.pullback.snd f g) = k
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balLeft.match_4.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b))
  (h_2 : (l : RBTree.RBNode α) → motive l),
  (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α), l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
    (match l with
      | RBTree.RBNode.node RBTree.RBColor.red a x b => h_1 a x b
      | l => h_2 l) =
      h_2 l
-- Lean.Setup
/-- The module's direct imports.
  If `none`, uses the imports from the module header.
   -/
Lean.ModuleSetup.imports? : Lean.ModuleSetup → Option (Array Lean.Import)
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.normalize.addVar : Lean.Expr → Lean.Elab.Term.ToDepElimPattern.M Unit
-- Mathlib.Topology.VectorBundle.Hom
/-- Consider a continuous map `v : M → E₁` to a vector bundle, over a base map `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
continuously on `m`, one can apply `ϕ m` to `g m`, and the resulting map is continuous.

Note that the continuity of `ϕ` cannot be always be stated as continuity of a map into a bundle,
as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only have a nice topology when `b₁` and `b₂` are
globally continuous, but we want to apply this lemma with only local information. Therefore, we
formulate it using continuity of `ϕ` read in coordinates.

Version for `ContinuousWithinAt`. We also give a version for `ContinuousAt`, but no version for
`ContinuousOn` or `Continuous` as our assumption, written in coordinates, only makes sense around
a point.

For a version with `B₁ = B₂` and `b₁ = b₂`, in which continuity can be expressed without
`inCoordinates`, see `ContinuousWithinAt.clm_bundle_apply`
 -/
ContinuousWithinAt.clm_apply_of_inCoordinates : ∀ {𝕜 : Type u_8} {F₁ : Type u_9} {F₂ : Type u_10} {B₁ : Type u_11} {B₂ : Type u_12} {M : Type u_13}
  {E₁ : B₁ → Type u_14} {E₂ : B₂ → Type u_15} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (x : B₁) → AddCommGroup (E₁ x)] [inst_2 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁]
  [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B₁) → TopologicalSpace (E₁ x)] [inst_7 : (x : B₂) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B₂) → TopologicalSpace (E₂ x)]
  [inst_13 : TopologicalSpace B₁] [inst_14 : TopologicalSpace B₂] [inst_15 : TopologicalSpace M]
  [inst_16 : FiberBundle F₁ E₁] [inst_17 : VectorBundle 𝕜 F₁ E₁] [inst_18 : FiberBundle F₂ E₂]
  [inst_19 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)}
  {v : (m : M) → E₁ (b₁ m)} {s : Set M},
  ContinuousWithinAt (fun m => ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) s m₀ →
    ContinuousWithinAt (fun m => ⟨b₁ m, v m⟩) s m₀ →
      ContinuousWithinAt b₂ s m₀ → ContinuousWithinAt (fun m => ⟨b₂ m, (ϕ m) (v m)⟩) s m₀
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path.ext_iff : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} {m : ℕ} {f g : X.Path m}, f = g ↔ f.vertex = g.vertex ∧ f.arrow = g.arrow
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Real.sinh` is real analytic.  -/
Real.analyticOnNhd_sinh : ∀ {s : Set ℝ}, AnalyticOnNhd ℝ Real.sinh s
-- Mathlib.Order.Atoms
/-- A coatom of an `OrderTop` is an element with no other element between it and `⊤`,
which is not `⊤`.  -/
IsCoatom : {α : Type u_2} → [inst : Preorder α] → [OrderTop α] → α → Prop
-- Mathlib.Algebra.DirectSum.Module
DirectSum.support_smul : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] [inst_4 : (i : ι) → (x : M i) → Decidable (x ≠ 0)]
  (c : R) (v : DirectSum ι fun i => M i), DFinsupp.support (c • v) ⊆ DFinsupp.support v
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldl_eq_foldl_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.DTreeMap.foldl (fun d a x => f d a) init t = List.foldl f init t.keys
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.DSmooth.comp' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : DiffeologicalSpace X] [inst_1 : DiffeologicalSpace Y]
  [inst_2 : DiffeologicalSpace Z] {f : X → Y} {g : Y → Z},
  Diffeology.DSmooth g → Diffeology.DSmooth f → Diffeology.DSmooth fun x => g (f x)
-- Init.Grind.AC
Lean.Grind.AC.instBEqSeq : BEq Lean.Grind.AC.Seq
-- Mathlib.RingTheory.Extension.Generators
/-- The hom from `P` to `P'` given by the designated section of `P'`.  -/
Algebra.Generators.defaultHom : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            (P : Algebra.Generators R S ι) →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst_3 : CommRing R'] →
                      [inst_4 : CommRing S'] →
                        [inst_5 : Algebra R' S'] →
                          (P' : Algebra.Generators R' S' ι') → [inst_6 : Algebra S S'] → P.Hom P'
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get!_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).get! k = default
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {toOrderHom : α →o β} {map_top' : toOrderHom.toFun ⊤ = ⊤}
  {map_bot' : toOrderHom.toFun ⊥ = ⊥} {toOrderHom_1 : α →o β} {map_top'_1 : toOrderHom_1.toFun ⊤ = ⊤}
  {map_bot'_1 : toOrderHom_1.toFun ⊥ = ⊥},
  { toOrderHom := toOrderHom, map_top' := map_top', map_bot' := map_bot' } =
      { toOrderHom := toOrderHom_1, map_top' := map_top'_1, map_bot' := map_bot'_1 } →
    toOrderHom = toOrderHom_1
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Given a t-structure `t` on `C` and `n : ℤ`, this is the
functorial (distinguished) triangle `obj₁ ⟶ X ⟶ obj₃ ⟶ obj₁⟦1⟧` for any `X : C`,
where `obj₁` is `< n` and `obj₃` is `≥ n`.
(This should not be used directly: use `triangleLTGE` instead.)  -/
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C →
                ℤ → CategoryTheory.Functor C (CategoryTheory.Pretriangulated.Triangle C)
-- Init.Omega.IntList
Lean.Omega.IntList.dot_neg_left : ∀ (xs ys : Lean.Omega.IntList), (-xs).dot ys = -xs.dot ys
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort : Type
-- Mathlib.Algebra.Lie.Engel
LieSubmodule.lie_top_eq_of_span_sup_eq_top : ∀ {R : Type u₁} {L : Type u₂} {M : Type u₄} [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] [inst_6 : LieModule R L M]
  {I : LieIdeal R L} {x : L},
  R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤ →
    ∀ (N : LieSubmodule R L M), ↑⁅⊤, N⁆ = Submodule.map ((LieModule.toEnd R L M) x) ↑N ⊔ ↑⁅I, N⁆
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.instMulActionDistribMulActionHomIdOfSMulCommClass : {M : Type u_1} →
  {N : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : Monoid M] →
          [inst_1 : AddMonoid A] →
            [inst_2 : DistribMulAction M A] →
              [inst_3 : Monoid N] →
                [inst_4 : AddMonoid B] →
                  [inst_5 : DistribMulAction N A] →
                    [SMulCommClass M N A] → [inst_7 : DistribMulAction N B] → MulAction Mᵈᵐᵃ (A →+[N] B)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toLinearEquiv_inj : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  {f g : E ≃ₛₗᵢ[σ₁₂] E₂}, f.toLinearEquiv = g.toLinearEquiv ↔ f = g
-- Mathlib.Order.Filter.Pointwise
Filter.sub_le_sub_right : ∀ {α : Type u_2} [inst : Sub α] {f₁ f₂ g : Filter α}, f₁ ≤ f₂ → f₁ - g ≤ f₂ - g
-- Mathlib.Order.Sublattice
Sublattice.mem_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {f : LatticeHom α β} {b : β},
  b ∈ Sublattice.map f L ↔ ∃ a ∈ L, f a = b
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Obtain an `ImageMap` from a `HasImageMap` instance.  -/
CategoryTheory.Limits.HasImageMap.imageMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      [inst_1 : CategoryTheory.Limits.HasImage f.hom] →
        [inst_2 : CategoryTheory.Limits.HasImage g.hom] →
          (sq : f ⟶ g) → [CategoryTheory.Limits.HasImageMap sq] → CategoryTheory.Limits.ImageMap sq
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- Unfold the definition of `compTranspose`.
This exists to streamline the proof of `MonoidalClosed.assoc`  -/
CategoryTheory.MonoidalClosed.compTranspose_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y],
  CategoryTheory.MonoidalClosed.compTranspose x y z =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator x (x ⟹ y) (y ⟹ z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((CategoryTheory.ihom.ev x).app y) (y ⟹ z))
        ((CategoryTheory.ihom.ev y).app z))
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesHasSum_congr : ∀ {f g : ℕ → ℂ} (s a : ℂ), (∀ {n : ℕ}, n ≠ 0 → f n = g n) → (LSeriesHasSum f s a ↔ LSeriesHasSum g s a)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.subtype_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A) (x : ↥S),
  S.subtype x = ↑x