mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.single_blocksFun : ∀ {n : ℕ} (h : 0 < n) (i : Fin (Composition.single n h).length), (Composition.single n h).blocksFun i = n
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.DTreeMap.foldrM f init t = Array.foldrM (fun a b => f a.1 a.2 b) init (Std.DTreeMap.Const.toArray t)
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.RightLift.w : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {s t : CategoryTheory.Bicategory.RightLift f g} (h : s ⟶ t),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight h.left f) t.counit = s.counit
-- Lean.DocString.Markdown
_private.Lean.DocString.Markdown.0.Lean.Doc.blockRendererForUnsafe : Lean.Name → Lean.CoreM (Option Lean.Doc.BlockMdRenderer)
-- Mathlib.Algebra.GroupWithZero.Opposite
AddOpposite.instMonoidWithZero : {α : Type u_1} → [MonoidWithZero α] → MonoidWithZero αᵃᵒᵖ
-- Mathlib.Analysis.Seminorm
Seminorm.mem_ball_self : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {x : E} {r : ℝ}, 0 < r → x ∈ p.ball x r
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
/-- The restriction of a linear map `f : M → M₂` to a submodule `p ⊆ M` gives a linear map
`p → M₂`.  -/
ContinuousLinearMap.domRestrict : {R₁ : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R₁ →+* R₂} →
          {M₁ : Type u_4} →
            {M₂ : Type u_5} →
              [inst_2 : TopologicalSpace M₁] →
                [inst_3 : AddCommMonoid M₁] →
                  [inst_4 : Module R₁ M₁] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : AddCommMonoid M₂] →
                        [inst_7 : Module R₂ M₂] → (M₁ →SL[σ₁₂] M₂) → (p : Submodule R₁ M₁) → ↥p →SL[σ₁₂] M₂
-- Init.Data.List.Lemmas
List.get_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → ∃ n, l.get n = a
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.associator_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q R : C),
  (CategoryTheory.Limits.biprod.associator P Q R).inv =
    CategoryTheory.Limits.biprod.lift
      (CategoryTheory.Limits.biprod.lift CategoryTheory.Limits.biprod.fst
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.fst))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd CategoryTheory.Limits.biprod.snd)
-- Mathlib.Analysis.Convex.Deriv
/-- Reformulation of `ConvexOn.le_slope_of_hasDerivWithinAt_Ioi` using `derivWithin`.  -/
ConvexOn.rightDeriv_le_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConvexOn ℝ S f →
    x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f (Set.Ioi x) x → derivWithin f (Set.Ioi x) x ≤ slope f x y
-- Mathlib.NumberTheory.SiegelsLemma
_private.Mathlib.NumberTheory.SiegelsLemma.0.Int.Matrix.termP : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂)[k] = t₁[k]
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.ediam_union_le`.

---

If two sets have nonempty intersection, then the extended diameter of their union
is estimated from above by the sum of their union.  -/
EMetric.diam_union' : ∀ {X : Type u_2} {s t : Set X} [inst : PseudoEMetricSpace X],
  (s ∩ t).Nonempty → Metric.ediam (s ∪ t) ≤ Metric.ediam s + Metric.ediam t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XYIdeal'.congr_simp : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} {x x_1 : F} (e_x : x = x_1) {y y_1 : F} (e_y : y = y_1)
  (h : W.Nonsingular x y),
  WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h = WeierstrassCurve.Affine.CoordinateRing.XYIdeal' ⋯
-- Mathlib.Analysis.Calculus.Deriv.Add
hasDerivAtFilter_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (L : Filter (𝕜 × 𝕜)), HasDerivAtFilter Neg.neg (-1) L
-- Mathlib.Data.Vector.Defs
/-- Map a vector under a function.  -/
List.Vector.map : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → (α → β) → List.Vector α n → List.Vector β n
-- Mathlib.Probability.CondVar
ProbabilityTheory.stronglyMeasurable_condVar : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  MeasureTheory.StronglyMeasurable (ProbabilityTheory.condVar m X μ)
-- Mathlib.Analysis.Normed.Group.Basic
norm_ne_zero_iff' : ∀ {E : Type u_5} [inst : NormedGroup E] {a : E}, ‖a‖ ≠ 0 ↔ a ≠ 1
-- Mathlib.Order.Defs.Unbundled
MinimalFor.eq_1 : ∀ {ι : Sort u_1} {α : Type u_2} [inst : LE α] (P : ι → Prop) (f : ι → α) (i : ι),
  MinimalFor P f i = (P i ∧ ∀ ⦃j : ι⦄, P j → f j ≤ f i → f i ≤ f j)
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.flip_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P}
  (f : M →+ N →+ P) (x_3 : M) (y : N), (f.flip y) x_3 = (f x_3) y
-- Init.Data.Nat.Dvd
Nat.div_mul_cancel : ∀ {n m : ℕ}, n ∣ m → m / n * n = m
-- Lean.Class
Lean.instInhabitedClassState : Inhabited Lean.ClassState
-- Mathlib.Topology.Bornology.Basic
OrderDual.isCobounded_preimage_toDual : ∀ {α : Type u_2} [inst : Bornology α] {s : Set αᵒᵈ},
  Bornology.IsCobounded (⇑OrderDual.toDual ⁻¹' s) ↔ Bornology.IsCobounded s
-- Mathlib.Data.EReal.Basic
EReal.instInhabited : Inhabited EReal
-- Lean.Data.Json.Basic
Lean.instHashableJsonNumber.hash : Lean.JsonNumber → UInt64
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.instCoeSortType : CoeSort TopCommRingCat (Type u)
-- Std.Sat.AIG.Basic
/-- Get the gate.
 -/
Std.Sat.AIG.Fanin.gate : Std.Sat.AIG.Fanin → ℕ
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.coe_of : ∀ (R : Type u) [inst : Ring R], ↑(RingCat.of R) = R
-- Mathlib.Data.Nat.WithBot
Nat.WithBot.add_eq_one_iff : ∀ {n m : WithBot ℕ}, n + m = 1 ↔ n = 0 ∧ m = 1 ∨ n = 1 ∧ m = 0
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.card_typein_toType_lt : ∀ (c : Cardinal.{u_1}) (x : c.ord.ToType), ((Ordinal.typein fun x1 x2 => x1 < x2).toRelEmbedding x).card < c
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
_private.Lean.Meta.Tactic.Simp.Arith.Int.Basic.0.Lean.Meta.Simp.Arith.Int.ToLinear.toLinearExpr.visit : Lean.Expr → Lean.Meta.Simp.Arith.Int.ToLinear.M Int.Internal.Linear.Expr
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.le_iff : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {L₁ L₂ : IntermediateField.Lifts F E K},
  L₁ ≤ L₂ ↔ ∃ (h : L₁.carrier ≤ L₂.carrier), L₂.emb.comp (IntermediateField.inclusion h) = L₁.emb
-- Mathlib.Order.Iterate
Monotone.le_iterate_comp_of_le : ∀ {α : Type u_1} [inst : Preorder α] {f : α → α} {β : Type u_2} {g : β → β} {h : β → α},
  Monotone f → h ∘ g ≤ f ∘ h → ∀ (n : ℕ), h ∘ g^[n] ≤ f^[n] ∘ h
-- Mathlib.Data.Multiset.MapFold
Multiset.map_eq_map_of_bij_of_nodup : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → γ) (g : β → γ) {s : Multiset α} {t : Multiset β},
  s.Nodup →
    t.Nodup →
      ∀ (i : (a : α) → a ∈ s → β),
        (∀ (a : α) (ha : a ∈ s), i a ha ∈ t) →
          (∀ (a₁ : α) (ha₁ : a₁ ∈ s) (a₂ : α) (ha₂ : a₂ ∈ s), i a₁ ha₁ = i a₂ ha₂ → a₁ = a₂) →
            (∀ b ∈ t, ∃ a, ∃ (ha : a ∈ s), i a ha = b) →
              (∀ (a : α) (ha : a ∈ s), f a = g (i a ha)) → Multiset.map f s = Multiset.map g t
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticSeverity.hint : Lean.Lsp.DiagnosticSeverity
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_eq_zero_of_infinite : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s : Set α},
  (s ∩ Function.support f).Infinite → ∑ᶠ (i : α) (_ : i ∈ s), f i = 0
-- Mathlib.Data.Part
Part.right_dom_of_union_dom : ∀ {α : Type u_1} [inst : Union α] {a b : Part α}, (a ∪ b).Dom → b.Dom
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Adj.edges_toWalk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (h : G.Adj u v), h.toWalk.edges = [s(u, v)]
-- Mathlib.Data.W.Constructions
/-- The constructors for the naturals  -/
WType.Natα : Type
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.setIntegral_eq : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [MeasureTheory.SigmaFiniteFiltration μ ℱ],
  MeasureTheory.Martingale f ℱ μ →
    ∀ {i j : ι}, i ≤ j → ∀ {s : Set Ω}, MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ = ∫ (ω : Ω) in s, f j ω ∂μ
-- Mathlib.Topology.Algebra.Constructions
Units.topology_eq_inf : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M],
  Units.instTopologicalSpaceUnits =
    TopologicalSpace.induced Units.val inst ⊓ TopologicalSpace.induced (fun u => ↑u⁻¹) inst
-- Mathlib.Algebra.Group.Prod
MulHom.coprod.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : CommSemigroup P] (f : M →ₙ* P)
  (g : N →ₙ* P), f.coprod g = f.comp (MulHom.fst M N) * g.comp (MulHom.snd M N)
-- Mathlib.Topology.MetricSpace.Dilation
/-- Every isometry is a dilation of ratio `1`.  -/
Isometry.toDilation : {α : Type u_1} →
  {β : Type u_2} → [inst : PseudoEMetricSpace α] → [inst_1 : PseudoEMetricSpace β] → (f : α → β) → Isometry f → α →ᵈ β
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.get.match_1.splitter : {α : Type u_1} →
  {δ : Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive :
            (t : Std.DTreeMap.Internal.Impl α fun x => δ) → Std.DTreeMap.Internal.Impl.contains k t = true → Sort u_3) →
          (t : Std.DTreeMap.Internal.Impl α fun x => δ) →
            (hlk : Std.DTreeMap.Internal.Impl.contains k t = true) →
              ((size : ℕ) →
                  (k' : α) →
                    (v' : δ) →
                      (l r : Std.DTreeMap.Internal.Impl α fun x => δ) →
                        (hlk :
                            Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
                              true) →
                          motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r) hlk) →
                motive t hlk
-- Init.Data.SInt.Lemmas
Int64.eq_sub_iff_add_eq : ∀ {a b c : Int64}, a = c - b ↔ a + b = c
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.mk : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [toIsCancelMulZero : IsCancelMulZero α]
  [toIsWellFounded : IsWellFounded α DvdNotUnit], (∀ {a : α}, Irreducible a ↔ Prime a) → UniqueFactorizationMonoid α
-- Std.Async.Basic
Std.Async.EAsync.instMonadAsyncAsyncTaskError : Std.Async.MonadAsync Std.Async.AsyncTask (Std.Async.EAsync IO.Error)
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.toEventualRanges_obj : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v))
  [inst_1 : CategoryTheory.IsCofilteredOrEmpty J] (j : J), F.toEventualRanges.obj j = ↑(F.eventualRange j)
-- Mathlib.Algebra.Group.Defs
/-- An alternative to `add_comm` which uses the mixin `IsAddCommutative` instead of bundled
commutative algebraic structures. In general, you should prefer `add_comm` unless you are working
with commutative subobjects in a noncommutative algebraic structure.  -/
add_comm' : ∀ {M : Type u_2} [inst : Add M] [IsAddCommutative M] (a b : M), a + b = b + a
-- Init.Data.Nat.Sqrt.Lemmas
_private.Init.Data.Nat.Sqrt.Lemmas.0.Nat.sqrt.iter_sq_le : ∀ (n guess : ℕ), Nat.sqrt.iter n guess * Nat.sqrt.iter n guess ≤ n
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.dsimprocCore : Bool → Lean.Meta.Simp.SimprocTree → Lean.PHashSet Lean.Name → Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.DStep
-- Init.Data.Order.PackageFactories
/-- Use this factory to conveniently define a linear order on a type `α` and all the associated
operations and instances given an `LE α` instance.

Creates a `LinearOrderPackage α` instance. Such an instance entails `LE α`, `LT α`, `BEq α`,
`Ord α`, `Min α` and `Max α` instances as well as an `IsLinearOrder α` instance and `LawfulOrder*`
instances proving the compatibility of the operations with the linear order.

In the presence of `LE α`, `DecidableLE α`, `Total (· ≤ ·)`, `Trans (· ≤ ·) (· ≤ ·) (· ≤ ·)` and
`Antisymm (· ≤ ·)` instances, no arguments are required and the factory can be used as in this
example:

```lean
public instance : LinearOrderPackage X := .ofLE X
```

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly
provide some arguments:

```lean
public instance : LinearOrderPackage X := .ofLE X {
  le_total := sorry
  le_trans := sorry
  le_antisymm := sorry }
```

It is also possible to do all of this by hand, without resorting to `LinearOrderPackage`. This
can be useful if, say, one wants to avoid specifying an `LT α` instance, which is not possible with
`LinearOrderPackage`.

**How the arguments are filled**

Lean tries to fill all of the fields of the `args : Packages.LinearOrderOfLEArgs α` parameter
automatically. If it fails, it is necessary to provide some of the fields manually.

* For the data-carrying typeclasses `LE`, `LT`, `BEq`, `Ord`, `Min` and `Max`, existing instances
  are always preferred. If no existing instances can be synthesized, it is attempted to derive an
  instance from the `LE` instance.
* Some proof obligations can be filled automatically if the data-carrying typeclasses have been
  derived from the `LE` instance. For example: If the `beq` field is omitted and no `BEq α` instance
  can be synthesized, it is derived from the `LE α` instance. In this case, `beq_iff_le_and_ge` can be
  omitted because Lean can infer that `BEq α` and `LE α` are compatible.
* Other proof obligations, namely `le_total`, `le_trans` and `le_antisymm`, can be omitted if
  `Total`, `Trans` and `Antisymm` instances can be synthesized.
 -/
Std.LinearOrderPackage.ofLE : (α : Type u) →
  autoParam (Std.Packages.LinearOrderOfLEArgs α) Std.LinearOrderPackage.ofLE._auto_1 → Std.LinearOrderPackage α
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.AdjoinSimple.coe_aeval_gen_apply : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E) (f : Polynomial F),
  ↑((Polynomial.aeval (IntermediateField.AdjoinSimple.gen F α)) f) = (Polynomial.aeval α) f
-- Mathlib.Order.Basic
LinearOrder.ext_lt : ∀ {α : Type u_2} {A B : LinearOrder α}, (∀ (x y : α), x < y ↔ x < y) → A = B
-- Mathlib.RingTheory.Length
Module.length_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Submodule R M},
  Module.length R (M ⧸ N) = Order.coheight N
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Iic_add_Iic_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [inst_2 : DecidableEq α] [AddLeftMono α] [AddRightMono α]
  [inst_5 : LocallyFiniteOrderBot α] (a b : α), Finset.Iic a + Finset.Iic b ⊆ Finset.Iic (a + b)
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.zsmul_neg' : ∀ {α : Type u_3} [self : LinearOrderedAddCommGroupWithTop α] (n : ℕ) (a : α), Int.negSucc n • a = -(↑n.succ • a)
-- Init.Data.List.Lemmas
List.concat_inj_left : ∀ {α : Type u_1} {l l' : List α} (a : α), l.concat a = l'.concat a ↔ l = l'
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.instModule : {𝕜 : Type u_2} →
  {E : Type u_4} →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] → [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → Module 𝕜 (WeakDual 𝕜 E)
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_comp : ∀ {R : Type u_1} [inst : Semiring R] (k l : ℕ),
  Polynomial.hasseDeriv k ∘ₗ Polynomial.hasseDeriv l = (k + l).choose k • Polynomial.hasseDeriv (k + l)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.lift.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g}
  (hs hs_1 : CategoryTheory.Limits.IsLimit s),
  hs = hs_1 →
    ∀ {W : C} (k k_1 : W ⟶ X) (e_k : k = k_1)
      (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g),
      CategoryTheory.Limits.Fork.IsLimit.lift hs k h = CategoryTheory.Limits.Fork.IsLimit.lift hs_1 k_1 ⋯
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_infty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M},
  ContMDiffWithinAt I I' (↑⊤) f s x ↔ ∀ (n : ℕ), ContMDiffWithinAt I I' (↑n) f s x
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.stoppedValue_hittingBtwn_mem : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] [WellFoundedLT ι]
  {u : ι → Ω → β} {s : Set β} {n m : ι} {ω : Ω},
  (∃ j ∈ Set.Icc n m, u j ω ∈ s) → MeasureTheory.stoppedValue u (fun ω => ↑(MeasureTheory.hittingBtwn u s n m ω)) ω ∈ s
-- Mathlib.NumberTheory.Height.MvPolynomial
Height.logHeight_sym2_le : ∀ (K : Type u_4) [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K],
  ∃ C,
    ∀ (a b c d : K),
      Height.logHeight ![a * c, a * d + b * c, b * d] ≤ C + Height.logHeight ![a, b] + Height.logHeight ![c, d]
-- Batteries.Data.List.Lemmas
List.findIdxs_eq_filterMap_zipIdx : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ},
  List.findIdxs p xs s = List.filterMap (fun ab => bif p ab.1 then some ab.2 else none) (xs.zipIdx s)
-- Mathlib.Topology.Constructions
IsClosed.trans : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {t : Set ↑s},
  IsClosed t → IsClosed s → IsClosed (Subtype.val '' t)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The (distinguished) triangles given by the natural transformations
`t.eTruncLT.obj i ⟶ 𝟭 C ⟶ t.eTruncGE.obj i ⟶ ...` for all `i : EInt`.  -/
CategoryTheory.Triangulated.TStructure.eTriangleLTGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} 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 EInt (CategoryTheory.Functor C (CategoryTheory.Pretriangulated.Triangle C))
-- Mathlib.Algebra.Group.Finsupp
/-- Bundle `Finsupp.embDomain f` as an additive map from `ι →₀ M` to `F →₀ M`.  -/
Finsupp.embDomain.addMonoidHom : {ι : Type u_1} → {F : Type u_2} → {M : Type u_3} → [inst : AddZeroClass M] → (ι ↪ F) → (ι →₀ M) →+ F →₀ M
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionLiteralSupport : Lean.ToJson Lean.Lsp.CodeActionLiteralSupport
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.inter_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp], t₁.inter t₂ = t₁ ∩ t₂
-- Mathlib.Topology.Category.TopCat.Limits.Konig
/-- Cofiltered limits of nonempty compact Hausdorff spaces are nonempty topological spaces.
 -/
TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system : ∀ {J : Type u} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TopCat)
  [CategoryTheory.IsCofilteredOrEmpty J] [∀ (j : J), Nonempty ↑(F.obj j)] [∀ (j : J), CompactSpace ↑(F.obj j)]
  [∀ (j : J), T2Space ↑(F.obj j)], Nonempty ↑(TopCat.limitCone F).pt
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex_X₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex✝ f n).X₂ =
    HomologicalComplex.homology L n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k k' : α}, cmp k k' = Ordering.eq → t.getKey! k = t.getKey! k'
-- Std.Http.Data.Body.Full
Std.Http.Body.instCoeAsyncResponseFullContextAsyncAny : Coe (Std.Async.Async (Std.Http.Response Std.Http.Body.Full))
  (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
`x + S`.  -/
QuotientAddGroup.instNorm : {M : Type u_1} → [inst : SeminormedAddCommGroup M] → {S : AddSubgroup M} → Norm (M ⧸ S)
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum.eq_1 : ∀ {α : Type u} {β : Type v} (M : Matroid α) (N : Matroid β),
  M.sum N =
    ((Matroid.sigma fun t => Bool.rec (M.mapEquiv Equiv.ulift.symm) (N.mapEquiv Equiv.ulift.symm) t).mapEquiv
          (Equiv.sumEquivSigmaBool (ULift.{v, u} α) (ULift.{u, v} β)).symm).mapEquiv
      (Equiv.ulift.sumCongr Equiv.ulift)
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- `IsScalarTower R'₂ R' N` implies `IsScalarTower R'₂ R' (M ⊗[R] N)`  -/
TensorProduct.isScalarTower_right : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] {R'₂ : Type u_22} [inst_8 : Monoid R'₂]
  [inst_9 : DistribMulAction R'₂ M] [inst_10 : SMulCommClass R R'₂ M] [inst_11 : SMul R'₂ R']
  [inst_12 : DistribMulAction R'₂ N] [inst_13 : DistribMulAction R' N] [TensorProduct.CompatibleSMul R R'₂ M N]
  [TensorProduct.CompatibleSMul R R' M N] [IsScalarTower R'₂ R' N], IsScalarTower R'₂ R' (TensorProduct R M N)
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceDocumentColorParams : Lean.Lsp.FileSource Lean.Lsp.DocumentColorParams
-- Mathlib.Order.CompleteLattice.PiLex
Pi.Lex.sInf_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] (s : Set (Lex ((i : ι) → (fun i => α i) i))) (i : ι), sInf s i = ⨅ e, ↑e i
-- Mathlib.Tactic.Translate.Core
/-- Check if the given constant exists in the environment, also checking for reserved names.
This function is based on `Lean.realizeGlobalName`.  -/
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.realizeGlobalConst : Lean.Name → Lean.CoreM Bool
-- Mathlib.Algebra.Order.Module.Defs
PosMulReflectLT.toPosSMulReflectLT : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : Mul α] [inst_2 : Preorder α] [PosMulReflectLT α], PosSMulReflectLT α α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.equiv_iff_keysArray_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap α Unit cmp},
  t₁.Equiv t₂ ↔ t₁.keysArray = t₂.keysArray