mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.IntermediateValue
intermediate_value_Ico : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a b : α}, a ≤ b → ∀ {f : α → δ}, ContinuousOn f (Set.Icc a b) → Set.Ico (f a) (f b) ⊆ f '' Set.Ico a b
-- Mathlib.Analysis.InnerProductSpace.Calculus
DifferentiableAt.inner : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : NormedSpace ℝ E] {G : Type u_4} [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G] {f g : G → E}
  {x : G}, DifferentiableAt ℝ f x → DifferentiableAt ℝ g x → DifferentiableAt ℝ (fun x => inner 𝕜 (f x) (g x)) x
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the natural
transformation `F ⟶ H` is componentwise monic iff the natural transformation `G ⋙ F ⟶ G ⋙ H`
obtained from the units and counits of the adjunctions is.
Note that unlike `epi_rightToLeft_app_iff`, this equivalence does not make sense
on a per-object basis because the components of the two natural transformations are indexed by
different categories.  -/
CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful],
  (∀ (X : C), CategoryTheory.Mono (t.leftToRight.app X)) ↔
    ∀ (X : D), CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp (t.adj₁.counit.app X) (t.adj₂.unit.app X))
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instSub : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) → (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Sub (AdicCompletion I M)
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.TZifV1.mk.inj : ∀ {header : Std.Time.TimeZone.TZif.Header} {transitionTimes : Array ℤ} {transitionIndices : Array UInt8}
  {localTimeTypes : Array Std.Time.TimeZone.TZif.LocalTimeType} {abbreviations : Array String}
  {leapSeconds : Array Std.Time.TimeZone.TZif.LeapSecond} {stdWallIndicators utLocalIndicators : Array Bool}
  {header_1 : Std.Time.TimeZone.TZif.Header} {transitionTimes_1 : Array ℤ} {transitionIndices_1 : Array UInt8}
  {localTimeTypes_1 : Array Std.Time.TimeZone.TZif.LocalTimeType} {abbreviations_1 : Array String}
  {leapSeconds_1 : Array Std.Time.TimeZone.TZif.LeapSecond} {stdWallIndicators_1 utLocalIndicators_1 : Array Bool},
  { header := header, transitionTimes := transitionTimes, transitionIndices := transitionIndices,
        localTimeTypes := localTimeTypes, abbreviations := abbreviations, leapSeconds := leapSeconds,
        stdWallIndicators := stdWallIndicators, utLocalIndicators := utLocalIndicators } =
      { header := header_1, transitionTimes := transitionTimes_1, transitionIndices := transitionIndices_1,
        localTimeTypes := localTimeTypes_1, abbreviations := abbreviations_1, leapSeconds := leapSeconds_1,
        stdWallIndicators := stdWallIndicators_1, utLocalIndicators := utLocalIndicators_1 } →
    header = header_1 ∧
      transitionTimes = transitionTimes_1 ∧
        transitionIndices = transitionIndices_1 ∧
          localTimeTypes = localTimeTypes_1 ∧
            abbreviations = abbreviations_1 ∧
              leapSeconds = leapSeconds_1 ∧
                stdWallIndicators = stdWallIndicators_1 ∧ utLocalIndicators = utLocalIndicators_1
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inr_snd_f_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι) {Z : C} (h : L.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.snd.f i) h) =
    h
-- Mathlib.NumberTheory.LucasLehmer
mersenne_le_mersenne : ∀ {p q : ℕ}, mersenne p ≤ mersenne q ↔ p ≤ q
-- Lean.CoreM
/-- Creates a new name for use as an auxiliary declaration that can be assumed to be globally unique.

Uniqueness is guaranteed for the current branch of elaboration. When entering parallelism and other
branching elaboration steps, `mkChild` must be used (automatically done in `wrapAsync*`).
 -/
Lean.mkAuxDeclName : {m : Type → Type} →
  [Monad m] → [Lean.MonadEnv m] → [Lean.MonadDeclNameGenerator m] → optParam Lean.Name `_aux → m Lean.Name
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- In a locally path connected space, each path component is an open set.  -/
IsOpen.pathComponent : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X] (x : X), IsOpen (pathComponent x)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiable_pi'' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_6} {F' : ι → Type u_7} [inst_3 : (i : ι) → NormedAddCommGroup (F' i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {Φ : E → (i : ι) → F' i},
  (∀ (i : ι), Differentiable 𝕜 fun x => Φ x i) → Differentiable 𝕜 Φ
-- Mathlib.Data.Rel.Separated
SetRel.IsSeparated.singleton : ∀ {X : Type u_1} {R : SetRel X X} {x : X}, R.IsSeparated {x}
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.toFinsupp.eq_1 : ∀ {X : Type u_1}, FreeAbelianGroup.toFinsupp = FreeAbelianGroup.lift fun x => fun₀ | x => 1
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The topology of `𝔖`-convergence is the infimum, for `S ∈ 𝔖`, of topology induced by the map
of `S.domRestrict : (α →ᵤ[𝔖] β) → (↥S →ᵤ β)` of restriction to `S`, where `↥S →ᵤ β` is endowed with
the topology of uniform convergence.  -/
UniformOnFun.topologicalSpace_eq : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)),
  UniformOnFun.topologicalSpace α β 𝔖 =
    ⨅ s ∈ 𝔖,
      TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖))
        (UniformFun.topologicalSpace (↑s) β)
-- Lean.Parser.Level
Lean.Parser.Level.ident.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.ModuleCat.Topology.Homology
TopModuleCat.kerι_apply : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {M N : TopModuleCat R} (φ : M ⟶ N)
  (x : (fun X => ↑X.toModuleCat) (TopModuleCat.ker φ)),
  (CategoryTheory.ConcreteCategory.hom (TopModuleCat.kerι φ)) x = ↑x
-- Mathlib.NumberTheory.Height.MvPolynomial
_private.Mathlib.NumberTheory.Height.MvPolynomial.0.Height.hasFiniteMulSupport_iSup_max_iSup_one : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K] [Finite ι'],
  Nonempty ι' →
    ∀ (p : ι' → MvPolynomial ι K),
      Function.HasFiniteMulSupport fun v => ⨆ j, max (⨆ s, ↑v (MvPolynomial.coeff (↑s) (p j))) 1
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_sum_disjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [ContinuousAdd α]
  {ι : Type u_4} (s : Finset ι) {t : ι → Set β} {a : ι → α},
  (↑s).Pairwise (Function.onFun Disjoint t) →
    (∀ i ∈ s, HasSum (f ∘ Subtype.val) (a i)) → HasSum (f ∘ Subtype.val) (∑ i ∈ s, a i)
-- Init.Data.Repr
instReprChar : Repr Char
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.forget_grp_preserves_mono : (CategoryTheory.forget GrpCat).PreservesMonomorphisms
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofFiniteAddGrpHom.eq_1 : ∀ {G H : FiniteAddGrp.{u}} (f : G ⟶ H),
  ProfiniteAddGrp.ofFiniteAddGrpHom f =
    CategoryTheory.ConcreteCategory.ofHom { toAddMonoidHom := AddGrpCat.Hom.hom f.hom, continuous_toFun := ⋯ }
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.neg_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b : X ⟶ Y), -(a + b) = -a - b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.Hom.mk : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {x y : CategoryTheory.Limits.CategoricalPullback F G} →
                  (fst : x.fst ⟶ y.fst) →
                    (snd : x.snd ⟶ y.snd) →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp (F.map fst) y.iso.hom =
                            CategoryTheory.CategoryStruct.comp x.iso.hom (G.map snd))
                          CategoryTheory.Limits.CategoricalPullback.Hom.w._autoParam →
                        x.Hom y
-- Init.Data.String.Defs
/-- Checks whether a slice is empty.

Empty slices have {name}`utf8ByteSize` {lean}`0`.

Examples:
* {lean}`"".toSlice.isEmpty = true`
* {lean}`" ".toSlice.isEmpty = false`
 -/
String.Slice.isEmpty : String.Slice → Bool
-- Mathlib.RepresentationTheory.Action
Representation.LinearizeMonoidal.η_ε : ∀ (k : Type u) (G : Type v) [inst : Monoid G] [inst_1 : Semiring k],
  (Representation.LinearizeMonoidal.η k G).comp (Representation.LinearizeMonoidal.ε k G) =
    Representation.IntertwiningMap.id (Representation.trivial k G k)
-- Mathlib.Algebra.Notation.Indicator
Set.piecewise_eq_indicator : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M} [inst_1 : DecidablePred fun x => x ∈ s],
  s.piecewise f 0 = s.indicator f
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.tendsto_atTop_add_right_of_le : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G] (l : Filter α)
  {f g : α → G} (C : G),
  Filter.Tendsto f l Filter.atTop → (∀ (x : α), C ≤ g x) → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Mathlib.Data.Matrix.Mul
Matrix.sub_mul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n]
  (M M' : Matrix m n α) (N : Matrix n o α), (M - M') * N = M * N - M' * N
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  Disjoint s₁ s₂ →
    MeasurableSet s₂ →
      autoParam (μ s₁ ≠ ⊤) MeasureTheory.measureReal_union._auto_1 →
        autoParam (μ s₂ ≠ ⊤) MeasureTheory.measureReal_union._auto_3 → μ.real (s₁ ∪ s₂) = μ.real s₁ + μ.real s₂
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `pos_of_ne_zero`.

---

**Alias** of the reverse direction of `pos_iff_ne_zero`. -/
Ne.pos : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≠ 0 → 0 < a
-- Init.Data.List.MinMaxOn
List.le_apply_maxOn_append_right : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (h : ys ≠ []), f (List.maxOn f ys h) ≤ f (List.maxOn f (xs ++ ys) ⋯)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- If `X` is a paracompact normal topological space and `U` is an open covering of a closed set
`s`, then there exists a `SmoothPartitionOfUnity ι M s` that is subordinate to `U`.  -/
SmoothPartitionOfUnity.exists_isSubordinate : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [T2Space M] [SigmaCompactSpace M]
  {s : Set M}, IsClosed s → ∀ (U : ι → Set M), (∀ (i : ι), IsOpen (U i)) → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.extend_source : ∀ {𝕜 : 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}, (f.extend I).source = f.source
-- Mathlib.Data.Vector.Basic
/-- Erasing an element after inserting an element, at different indices.  -/
List.Vector.eraseIdx_insertIdx' : ∀ {α : Type u_1} {n : ℕ} {a : α} {v : List.Vector α (n + 1)} {i : Fin (n + 1)} {j : Fin (n + 2)},
  List.Vector.eraseIdx (j.succAbove i) (List.Vector.insertIdx a j v) =
    List.Vector.insertIdx a (i.predAbove j) (List.Vector.eraseIdx i v)
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- Equivalence between Young diagrams and weakly decreasing lists of positive natural numbers.
A Young diagram `μ` is equivalent to a list of row lengths.  -/
YoungDiagram.equivListRowLens : YoungDiagram ≃ { w // w.SortedGE ∧ ∀ x ∈ w, 0 < x }
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x` is a semigroup if `β` is a semigroup.  -/
FunLike.semigroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Mul F] → [inst_2 : Semigroup β] → [IsMulApply F α β] → Semigroup F
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The left-hand side of the diagram commutes.  -/
AddGroupExtension.Equiv.inl_comm : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G}
  (self : S.Equiv S'), ⇑self.toAddEquiv ∘ ⇑S.inl = ⇑S'.inl
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.stoppedAbove.eq_1 : ∀ {ι : Type u_1} {Ω : Type u_2} {β : Type u_3} [inst : LinearOrder ι] [inst_1 : OrderBot ι] [inst_2 : InfSet ι]
  [inst_3 : Preorder β] (f : ι → Ω → β) (r : β),
  MeasureTheory.stoppedAbove f r = MeasureTheory.stoppedProcess f (MeasureTheory.leastGE f r)
-- Mathlib.Algebra.FiveLemma
/-- One four lemma in terms of groups. For a diagram explaining the variables,
see the module docstring.  -/
MonoidHom.surjective_of_surjective_of_surjective_of_injective : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8}
  {N₄ : Type u_9} [inst : Group M₁] [inst_1 : Group M₂] [inst_2 : Group M₃] [inst_3 : Group M₄] [inst_4 : Group N₁]
  [inst_5 : Group N₂] [inst_6 : Group N₃] [inst_7 : Group N₄] (f₁ : M₁ →* M₂) (f₂ : M₂ →* M₃) (f₃ : M₃ →* M₄)
  (g₁ : N₁ →* N₂) (g₂ : N₂ →* N₃) (g₃ : N₃ →* N₄) (i₁ : M₁ →* N₁) (i₂ : M₂ →* N₂) (i₃ : M₃ →* N₃) (i₄ : M₄ →* N₄),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      g₃.comp i₃ = i₄.comp f₃ →
        Function.MulExact ⇑f₂ ⇑f₃ →
          Function.MulExact ⇑g₁ ⇑g₂ →
            Function.MulExact ⇑g₂ ⇑g₃ →
              Function.Surjective ⇑i₁ → Function.Surjective ⇑i₃ → Function.Injective ⇑i₄ → Function.Surjective ⇑i₂
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_top : ∀ {α : Type u_1} [inst : HeytingAlgebra α], ↑⊤ = ⊤
-- Mathlib.Analysis.Convex.Measure
/-- A convex set in a finite-dimensional real vector space is null measurable with respect to an
additive Haar measure on this space.  -/
Convex.nullMeasurableSet : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {s : Set E},
  Convex ℝ s → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Order.Preorder.Chain
IsChain.mono_rel : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {r' : α → α → Prop},
  IsChain r s → (∀ (x y : α), r x y → r' x y) → IsChain r' s
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polarBilin_apply_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (m y : M),
  (Q.polarBilin m) y = QuadraticMap.polar (⇑Q) m y
-- Mathlib.Analysis.Analytic.Order
AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  AnalyticAt 𝕜 f x → deriv f x ≠ 0 → analyticOrderAt (fun x_1 => f x_1 - f x) x = 1
-- Mathlib.Analysis.Convex.Star
StarConvex.add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x y : E} {s t : Set E}, StarConvex 𝕜 x s → StarConvex 𝕜 y t → StarConvex 𝕜 (x + y) (s + t)
-- Mathlib.Order.Fin.Tuple
Fin.insertNth_mem_Icc : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i}
  {p : (j : Fin n) → α (i.succAbove j)} {q₁ q₂ : (j : Fin (n + 1)) → α j},
  i.insertNth x p ∈ Set.Icc q₁ q₂ ↔
    x ∈ Set.Icc (q₁ i) (q₂ i) ∧ p ∈ Set.Icc (fun j => q₁ (i.succAbove j)) fun j => q₂ (i.succAbove j)
-- Mathlib.Analysis.Calculus.TangentCone.Basic
tangentConeAt_of_mem_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} {x : E}
  [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousAdd E], s ∈ nhds x → tangentConeAt 𝕜 s x = Set.univ
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.coe_symm_measurableEquivPiIoc : ∀ {ι : Type u_2} (b : ι → ℝ), ⇑(UnitAddTorus.measurableEquivPiIoc b).symm = fun x i => ↑(↑x i)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instInf : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : TopologicalSpace M] → [inst_3 : Module R M] → Min (ClosedSubmodule R M)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.inf_neBot_iff : ∀ {α : Type u} {f : Ultrafilter α} {g : Filter α}, (↑f ⊓ g).NeBot ↔ ↑f ≤ g
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.differentiableAt_sqrt : ∀ {z : ℂ}, z ∈ Complex.slitPlane → DifferentiableAt ℂ Complex.sqrt z
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.W_eq_inverseImage_isomorphisms_of_adjunction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  {G : CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)}
  (adj : G ⊣ CategoryTheory.sheafToPresheaf J A),
  J.W = (CategoryTheory.MorphismProperty.isomorphisms (CategoryTheory.Sheaf J A)).inverseImage G
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionHomologyIso_inv_homologyι : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (i j k : ι) (hi : c.prev j = i)
  (hk : c.next j = k) {i' j' k' : ι'} (hi' : e.f i = i') (hj' : e.f j = j') (hk' : e.f k = k') (hi'' : c'.prev j' = i')
  (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j'] [inst_4 : (K.restriction e).HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv
      ((K.restriction e).homologyι j) =
    CategoryTheory.CategoryStruct.comp (K.homologyι j') (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofan_inj_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C}
  (i : 𝒜) (x : (f i).I),
  ((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).φ x = CategoryTheory.CategoryStruct.id ((f i).obj x)
-- Mathlib.Algebra.Order.Group.End
RelIso.apply_inv_self : ∀ {α : Type u_1} {r : α → α → Prop} (e : r ≃r r) (x : α), e (e⁻¹ x) = x
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorObj_instCoalgebra : ∀ (R : Type u) [inst : CommRing R] (X Y : CoalgCat R),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).instCoalgebra = inferInstance
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_neg : ∀ {a : USize} (h : System.Platform.numBits = 64), (-a).toBitVec64 h = -a.toBitVec64 h
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.instDecidableRankGT : {α : Type u_1} → {s : Batteries.BinomialHeap.Imp.Heap α} → {n : ℕ} → Decidable (s.rankGT n)
-- Init.Control.Lawful.Instances
EStateM.run_bind : ∀ {ε σ α β : Type u_1} {s : σ} (x : EStateM ε σ α) (f : α → EStateM ε σ β),
  (x >>= f).run s =
    match x.run s with
    | EStateM.Result.ok x s => (f x).run s
    | EStateM.Result.error e s => EStateM.Result.error e s
-- Mathlib.ModelTheory.Definability
/-- Shows that definability is closed under finite projections.  -/
Set.Definable.image_comp_embedding : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1}
  {s : Set (β → M)}, A.Definable L s → ∀ (f : α ↪ β) [Finite β], A.Definable L ((fun g => g ∘ ⇑f) '' s)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.forIn_eq_forIn_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {δ : Type v} {m' : Type v → Type w}
  [inst_2 : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  m.WF → Std.HashSet.Raw.forIn (fun a d => f a d) init m = forIn m.toArray init f
-- Mathlib.Data.Finsupp.MonomialOrder
/-- `toSyn` is monotone  -/
MonomialOrder.toSyn_monotone : ∀ {σ : Type u_1} (self : MonomialOrder σ), Monotone ⇑self.toSyn
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- The truncated simplex category.  -/
SimplexCategory.Truncated : ℕ → Type
-- Mathlib.Data.Fin.Fin2
Fin2.toFin_ofFin : ∀ {n : ℕ} (i : Fin n), (Fin2.ofFin i).toFin = i
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw₀.getD.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m m_1 : Std.DHashMap.Internal.Raw₀ α β),
  m = m_1 → ∀ (a : α) (fallback fallback_1 : β a), fallback = fallback_1 → m.getD a fallback = m_1.getD a fallback_1
-- Mathlib.Analysis.Calculus.DSlope
continuousOn_dslope : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a : 𝕜} {s : Set 𝕜},
  s ∈ nhds a → (ContinuousOn (dslope f a) s ↔ ContinuousOn f s ∧ DifferentiableAt 𝕜 f a)
-- Mathlib.Algebra.GroupWithZero.TransferInstance
/-- Transfer `SemigroupWithZero` across an `Equiv`  -/
Equiv.semigroupWithZero : {α : Type u} → {β : Type v} → α ≃ β → [SemigroupWithZero β] → SemigroupWithZero α
-- Plausible.Testable
/-- Try to find a counter-example of `p`.  -/
Plausible.Testable.runSuite : (p : Prop) → [Plausible.Testable p] → optParam Plausible.Configuration { } → Plausible.Gen (Plausible.TestResult p)
-- Init.Data.SInt.Bitwise
Int8.ofBitVec_and : ∀ (a b : BitVec 8), Int8.ofBitVec (a &&& b) = Int8.ofBitVec a &&& Int8.ofBitVec b
-- Mathlib.Data.PNat.Prime
PNat.prime_two : PNat.Prime 2
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.cone_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F],
  (CategoryTheory.Limits.limit.cone F).π.app = CategoryTheory.Limits.limit.π F
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.proofWidgetsJsxChild.quot : Lean.ParserDescr
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Suprema of `X`-generated topologies are `X`-generated.  -/
Topology.IsGeneratedBy.iSup : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type u_1} {κ : Sort u_2}
  {t : κ → TopologicalSpace Y}, (∀ (k : κ), Topology.IsGeneratedBy X Y) → Topology.IsGeneratedBy X Y