mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.deepTerms.threshold : Lean.Option ℕ
-- Mathlib.Data.Rat.Cast.Order
Rat.cast_le_natCast : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℚ} {n : ℕ}, ↑m ≤ ↑n ↔ m ≤ ↑n
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.starGraph_adj : ∀ {V : Type u_1} {r x y : V}, (SimpleGraph.starGraph r).Adj x y ↔ x ≠ y ∧ (x = r ∨ y = r)
-- Mathlib.Analysis.Convex.Basic
Convex.vadd : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E}, Convex 𝕜 s → ∀ (z : E), Convex 𝕜 (z +ᵥ s)
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.instDecidableIsNIndepSetOfDecidableEqOfDecidableRelAdj : {α : Type u_1} →
  (G : SimpleGraph α) →
    [DecidableEq α] → [DecidableRel G.Adj] → {n : ℕ} → {s : Finset α} → Decidable (G.IsNIndepSet n s)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- For a symmetric operator `T`, the function `fun x ↦ ⟪T x, x⟫` is real-valued.  -/
LinearMap.IsSymmetric.coe_reApplyInnerSelf_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, (↑T).IsSymmetric → ∀ (x : E), ↑(T.reApplyInnerSelf x) = inner 𝕜 (T x) x
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_mk : ∀ {R : Type u_1} {A : Type u_2} (x : R × A), (Unitization.mk x).toProd = x
-- Init.Meta.Defs
/-- Takes the string literal lexical syntax parsed by the parser and interprets it as a string.
This is where escape sequences are processed for example.
The string `s` is either a plain string literal or a raw string literal.

If it returns `none` then the string literal is ill-formed, which indicates a bug in the parser.
The function is not required to return `none` if the string literal is ill-formed.
 -/
Lean.Syntax.decodeStrLit : String → Option String
-- Init.Data.Option.Basic
Option.isSome_none : ∀ {α : Type u_1}, none.isSome = false
-- Init.Data.BitVec.Lemmas
BitVec.sle_eq_ule : ∀ {w : ℕ} {x y : BitVec w}, x.sle y = (x.msb != y.msb ^^ x.ule y)
-- Std.Http.Data.URI.Basic
/-- Returns the query as an array of (key, value) pairs. This is an identity function since Query is
already an array of pairs.
 -/
Std.Http.URI.Query.toArray : Std.Http.URI.Query → Array (Std.Http.URI.EncodedQueryParam × Option Std.Http.URI.EncodedQueryParam)
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_map_mkHom_homMk_homMk : ∀ {X Y : SSet.Truncated 2}
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e : SSet.Truncated.Edge x₀ x₁)
  {y₀ y₁ : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })}
  (e' : SSet.Truncated.Edge y₀ y₁),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).map
      (CategoryTheory.Prod.mkHom (SSet.Truncated.HomotopyCategory.homMk e) (SSet.Truncated.HomotopyCategory.homMk e')) =
    SSet.Truncated.HomotopyCategory.homMk (e.tensor e')
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
summable_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α]
  {L : SummationFilter β} [ContinuousAdd α] {f : γ → β → α} {s : Finset γ},
  (∀ i ∈ s, Summable (f i) L) → Summable (fun b => ∑ i ∈ s, f i b) L
-- Mathlib.RingTheory.WittVector.MulP
_private.Mathlib.RingTheory.WittVector.MulP.0.WittVector.wittMulN.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WOppSide.nonempty : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.WOppSide x y → (↑s).Nonempty
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.coe_comp_inclusion : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖),
  DFunLike.coe ∘ RestrictedProduct.inclusion R A h = DFunLike.coe
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.hom_inv_h₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S} (e : E ≅ F)
  (i : E.I₀) {Z : C} (h : E.X (e.inv.s₀ (e.hom.s₀ i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.hom.h₀ i) (CategoryTheory.CategoryStruct.comp (e.inv.h₀ (e.hom.s₀ i)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Mathlib.Algebra.Star.Subalgebra
Subalgebra.starClosure_eq_adjoin : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] (S : Subalgebra R A),
  S.starClosure = StarAlgebra.adjoin R ↑S
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj_map_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} (p : I₁ × I₂ × I₃ → J) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  [inst_4 :
    ∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
      ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p]
  {X₂ Y₂ : CategoryTheory.GradedObject I₂ C₂} (φ : X₂ ⟶ Y₂) (X₃ : CategoryTheory.GradedObject I₃ C₃) (i : J),
  ((CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj F p X₁).map φ).app X₃ i =
    CategoryTheory.GradedObject.mapTrifunctorMapMap F p (CategoryTheory.CategoryStruct.id X₁) φ
      (CategoryTheory.CategoryStruct.id X₃) i
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Any space is a `ChartedSpace` modelled over itself, by just using the identity chart.  -/
chartedSpaceSelf : (H : Type u_5) → [inst : TopologicalSpace H] → ChartedSpace H H
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- **Alias** of `MonoidHom.ker_domRestrict`. -/
MonoidHom.ker_restrict : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M),
  (f.domRestrict K).ker = f.ker.subgroupOf K
-- Mathlib.Order.UpperLower.Closure
upperClosure_eq_top_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, upperClosure s = ⊤ ↔ s = ∅
-- Mathlib.Data.PEquiv
PEquiv.mem_trans : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α ≃. β) (g : β ≃. γ) (a : α) (c : γ),
  c ∈ (f.trans g) a ↔ ∃ b ∈ f a, c ∈ g b
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.builtinVersoDocStrings : IO.Ref (Lean.NameMap Lean.VersoDocString)
-- Mathlib.Order.Booleanisation
/-- The embedding from a generalised Boolean algebra to its generated Boolean algebra.  -/
Booleanisation.liftLatticeHom : {α : Type u_1} → [inst : GeneralizedBooleanAlgebra α] → LatticeHom α (Booleanisation α)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.le_opNorm_mul_prod_of_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} {b : ι → ℝ},
  (∀ (i : ι), ‖m i‖ ≤ b i) → ‖f m‖ ≤ ‖f‖ * ∏ i, b i
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_diff_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Mathlib.Order.Compare
Ordering.compares_swap : ∀ {α : Type u_1} [inst : LT α] {a b : α} {o : Ordering}, o.swap.Compares a b ↔ o.Compares b a
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.mk.inj : ∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms V} {c : ComplexShape ι} {X : ι → V} {d : (i j : ι) → X i ⟶ X j}
  {shape : autoParam (∀ (i j : ι), ¬c.Rel i j → d i j = 0) HomologicalComplex.shape._autoParam}
  {d_comp_d' :
    autoParam (∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d i j) (d j k) = 0)
      HomologicalComplex.d_comp_d'._autoParam}
  {X_1 : ι → V} {d_1 : (i j : ι) → X_1 i ⟶ X_1 j}
  {shape_1 : autoParam (∀ (i j : ι), ¬c.Rel i j → d_1 i j = 0) HomologicalComplex.shape._autoParam}
  {d_comp_d'_1 :
    autoParam (∀ (i j k : ι), c.Rel i j → c.Rel j k → CategoryTheory.CategoryStruct.comp (d_1 i j) (d_1 j k) = 0)
      HomologicalComplex.d_comp_d'._autoParam},
  { X := X, d := d, shape := shape, d_comp_d' := d_comp_d' } =
      { X := X_1, d := d_1, shape := shape_1, d_comp_d' := d_comp_d'_1 } →
    X = X_1 ∧ d ≍ d_1
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLinkLocation.mk.inj : ∀ {module : Lean.Name} {range : Lean.Syntax.Range} {module_1 : Lean.Name} {range_1 : Lean.Syntax.Range},
  { module := module, range := range } = { module := module_1, range := range_1 } → module = module_1 ∧ range = range_1
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.IsVertexCover.vertexCoverNum_le : ∀ {V : Type u_1} {G : SimpleGraph V} {c : Set V}, G.IsVertexCover c → G.vertexCoverNum ≤ c.encard
-- Mathlib.Data.Fin.Tuple.Reflection
/-- Expand `v` to `![v 0, v 1, ...]`  -/
FinVec.etaExpand : {α : Type u_1} → {m : ℕ} → (Fin m → α) → Fin m → α
-- Mathlib.Order.Interval.Finset.Defs
Set.toFinset_Icc : ∀ {α : Type u_3} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α) [inst_2 : Fintype ↑(Set.Icc a b)],
  (Set.Icc a b).toFinset = Finset.Icc a b
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.below.root : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1}
  {motive :
    (a : RBTree.RBNode.Path α) →
      (a_1 : RBTree.RBColor) → (a_2 : ℕ) → RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop},
  RBTree.RBNode.Path.Balanced.below ⋯
-- Mathlib.RingTheory.EuclideanDomain
EuclideanDomain.isCoprime_of_dvd : ∀ {α : Type u_1} [inst : EuclideanDomain α] {x y : α},
  ¬(x = 0 ∧ y = 0) → (∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬z ∣ y) → IsCoprime x y
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.coe_copy : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  (f : ZeroAtInftyContinuousMap α β) (f' : α → β) (h : f' = ⇑f), ⇑(f.copy f' h) = f'
-- Init.Data.Option.List
Option.toList_min : ∀ {α : Type u_1} [inst : Min α] {o o' : Option α}, (o ⊓ o').toList = List.zipWith min o.toList o'.toList
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_map_of_injective : ∀ {R : Type u} {S : Type v} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R) [inst_1 : CommSemiring S]
  {f : R →+* S}, Function.Injective ⇑f → ((MvPolynomial.map f) p).vars = p.vars
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly
Matrix.minpoly_dvd_charpoly : ∀ {n : Type v} [inst : DecidableEq n] [inst_1 : Fintype n] {K : Type u_1} [inst_2 : Field K] (M : Matrix n n K),
  minpoly K M ∣ M.charpoly
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasProd.prod_range_mul : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m : M} [ContinuousMul M] {f : ℕ → M} {k : ℕ},
  HasProd (fun n => f (n + k)) m → HasProd f ((∏ i ∈ Finset.range k, f i) * m)
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem:
Assuming that for all Borel sets E whose boundary ∂E carries no probability mass under a
candidate limit probability measure μ we have convergence of the measures μsᵢ(E) to μ(E),
then for all closed sets F we have the limsup condition limsup μsᵢ(F) ≤ μ(F).  -/
MeasureTheory.limsup_measure_closed_le_of_forall_tendsto_measure : ∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [TopologicalSpace.PseudoMetrizableSpace Ω] [OpensMeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {μs : ι → MeasureTheory.Measure Ω},
  (∀ {E : Set Ω}, MeasurableSet E → μ (frontier E) = 0 → Filter.Tendsto (fun i => (μs i) E) L (nhds (μ E))) →
    ∀ (F : Set Ω), IsClosed F → Filter.limsup (fun i => (μs i) F) L ≤ μ F
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.rel.congr_simp : ∀ {I : Type u} {inst : DecidableEq I} [inst_1 : DecidableEq I] (R : Type v) [inst_2 : CommSemiring R] (A : I → Type w)
  [inst_3 : (i : I) → Semiring (A i)] [inst_4 : (i : I) → Algebra R (A i)]
  (a a_1 : LinearAlgebra.FreeProduct.FreeTensorAlgebra R A),
  a = a_1 →
    ∀ (a_2 a_3 : LinearAlgebra.FreeProduct.FreeTensorAlgebra R A),
      a_2 = a_3 → LinearAlgebra.FreeProduct.rel R A a a_2 = LinearAlgebra.FreeProduct.rel R A a_1 a_3
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.le_add_mul : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ} {K : NNReal},
  LipschitzWith K f → ∀ (x y : α), f x ≤ f y + ↑K * dist x y
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveCodeProps.mk.inj : ∀ {fmt fmt_1 : Lean.Widget.CodeWithInfos}, { fmt := fmt } = { fmt := fmt_1 } → fmt = fmt_1
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_eq_real_add_ite : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {a : 𝕜},
  RCLike.sqrt a =
    ↑√((‖a‖ + RCLike.re a) / 2) + (if 0 ≤ RCLike.im a then 1 else -1) * ↑√((‖a‖ - RCLike.re a) / 2) * RCLike.I
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.instPathConnectedSpaceCarrierObjTopCatToTop₀ : ∀ (n : SimplexCategory), PathConnectedSpace ↑(SimplexCategory.toTop₀.obj n)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.singleton_mul_subgroup : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G} {h : G}, h ∈ H → {h} * ↑H = ↑H
-- Mathlib.Data.Nat.GCD.Basic
Nat.gcd_mul_of_coprime_of_dvd : ∀ {a b c : ℕ}, a.Coprime c → b ∣ c → (a * b).gcd c = b
-- Mathlib.Logic.Basic
Ne.ne_or_ne : ∀ {α : Sort u_1} {x y : α} (z : α), x ≠ y → x ≠ z ∨ y ≠ z
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct A₁ B₁] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A₂ B₂]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) (CategoryTheory.Limits.coprod.map h k) =
    CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_symm_naturality_one : ∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {X₂ : C₂} {X₃ : C₃}
  (f₁ : X₁ ⟶ Y₁) (g : X₂ ⟶ (G.obj (Opposite.op Y₁)).obj X₃),
  adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp g ((G.map f₁.op).app X₃)) =
    CategoryTheory.CategoryStruct.comp ((F.map f₁).app X₂) (adj₂.homEquiv.symm g)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_le_maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {he : t.isEmpty = false},
  (compare (t.maxKey he) ((Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.maxKey ⋯)).isLE = true
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DefinitionParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Mathlib.Order.Interval.Multiset
Multiset.mem_Ioo : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Multiset.Ioo a b ↔ a < x ∧ x < b
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.contractSnd_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (ν : AbstractMeasure Y R R)
  (f : C(X × Y, R)) (x : X),
  ((AbstractMeasure.contractSnd ν) f) x = ν { toFun := fun y => f (x, y), continuous_toFun := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.elim c_1 → c = c_1
-- Init.Tactics
/-- After `with`, there is an optional tactic that runs on all branches, and
then a list of alternatives.
 -/
Lean.Parser.Tactic.inductionAlts : Lean.ParserDescr
-- Mathlib.CategoryTheory.Presentable.Limits
CategoryTheory.isCardinalPresentable_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {K : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} K] [CategoryTheory.Limits.HasLimitsOfShape Kᵒᵖ (Type w)]
  {Y : CategoryTheory.Functor K C} (c : CategoryTheory.Limits.Cocone Y) (hc : CategoryTheory.Limits.IsColimit c)
  (κ : Cardinal.{w}) [inst_4 : Fact κ.IsRegular],
  HasCardinalLT (CategoryTheory.Arrow K) κ →
    ∀ [∀ (k : K), CategoryTheory.IsCardinalPresentable (Y.obj k) κ], CategoryTheory.IsCardinalPresentable c.pt κ
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquivClass.mk : ∀ {F : Type u_9} {A : outParam (Type u_10)} {B : outParam (Type u_11)} [inst : Mul A] [inst_1 : Mul B]
  [inst_2 : EquivLike F A B], (∀ (f : F) (a b : A), f (a * b) = f a * f b) → MulEquivClass F A B
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.instL1SeminormedAddCommGroup : {R : Type u_3} →
  {M : Type u_4} → [SeminormedRing R] → [SeminormedAddCommGroup M] → SeminormedAddCommGroup (TrivSqZeroExt R M)
-- Mathlib.Order.Grade
isMin_grade_iff : ∀ {𝕆 : Type u_1} {α : Type u_3} [inst : Preorder 𝕆] [inst_1 : Preorder α] [inst_2 : GradeMinOrder 𝕆 α] {a : α},
  IsMin (grade 𝕆 a) ↔ IsMin a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The chosen convolution between the functors.  -/
CategoryTheory.MonoidalCategory.DayConvolution.unit : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {V : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            (F G : CategoryTheory.Functor C V) →
              [self : CategoryTheory.MonoidalCategory.DayConvolution F G] →
                CategoryTheory.MonoidalCategory.externalProduct F G ⟶
                  (CategoryTheory.MonoidalCategory.tensor C).comp
                    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
-- Lean.Util.ShareCommon
Lean.ShareCommon.ShareCommonM : Type u_1 → Type u_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.add_le_add_iff_right : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Add α] [IsAddCommutative α] [AddLeftMono α] {a b c : α},
  AddLECancellable a → (b + a ≤ c + a ↔ b ≤ c)
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.inv_add : ∀ {R : Type u_1} [inst : CommSemiring R] {b₁ b₂ : R} {a₁ a₂ : ℕ}, ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂
-- Mathlib.Algebra.Order.UpperLower
LowerSet.addCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  LowerSet.addCommSemigroup = Function.Injective.addCommSemigroup SetLike.coe ⋯ ⋯
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
/-- `b < sSup s` when there is an element `a` in `s` with `b < a`, when `s` is bounded above.
This is essentially an iff, except that the assumptions for the two implications are
slightly different (one needs boundedness above for one direction, nonemptiness and linear
order for the other one), so we formulate separately the two implications, contrary to
the `CompleteLattice` case.  -/
DirectedOn.lt_csSup_of_lt : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} {a b : α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → BddAbove s → a ∈ s → b < a → b < sSup s
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIic_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {b x : α}, b ≤ x → Set.projIic b x = ⟨b, ⋯⟩
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toAddSubgroup_sup : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SeparatelyContinuousAdd G]
  (U V : OpenAddSubgroup G), ↑(U ⊔ V) = ↑U ⊔ ↑V
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokensOptions : Lean.FromJson Lean.Lsp.SemanticTokensOptions
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- We can turn any limit cone over a pair into a bilimit bicone.  -/
CategoryTheory.Limits.binaryBiconeIsBilimitOfLimitConeOfIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {t : CategoryTheory.Limits.Cone (CategoryTheory.Limits.pair X Y)} →
          (ht : CategoryTheory.Limits.IsLimit t) → (CategoryTheory.Limits.BinaryBicone.ofLimitCone ht).IsBilimit
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_dist_tendsto' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  Filter.Tendsto (fun n => ‖↑(newton_cau_seq✝ hnorm) n - a‖) Filter.atTop (nhds ‖soln_gen✝ hnorm - a‖)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- The projective object `p` of this presentation  -/
CategoryTheory.ProjectivePresentation.p : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → CategoryTheory.ProjectivePresentation X → C
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.isSquare_of_isNNRat_rat : ∀ (a : ℚ) (n d : ℕ), IsSquare n → IsSquare d → Mathlib.Meta.NormNum.IsNNRat a n d → IsSquare a
-- Mathlib.Algebra.Category.MonCat.Basic
AddEquiv.toAddMonCatIso.eq_1 : ∀ {X Y : Type u} [inst : AddMonoid X] [inst_1 : AddMonoid Y] (e : X ≃+ Y),
  e.toAddMonCatIso =
    { hom := AddMonCat.ofHom e.toAddMonoidHom, inv := AddMonCat.ofHom e.symm.toAddMonoidHom, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The additive negation is a polynomial function on Witt vectors.  -/
WittVector.negIsPoly : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], WittVector.IsPoly p fun R x => Neg.neg
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
isMIntegralCurve_comp_sub : ∀ {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] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {dt : ℝ}, IsMIntegralCurve (γ ∘ fun x => x - dt) v ↔ IsMIntegralCurve γ v
-- Std.Time.Time.PlainTime
/-- Subtracts hours from a `PlainTime`.
 -/
Std.Time.PlainTime.subHours : Std.Time.PlainTime → Std.Time.Hour.Offset → Std.Time.PlainTime
-- Mathlib.Analysis.Seminorm
Seminorm.ball_eq_metric : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E]
  (p : Seminorm 𝕜 E) {x : E} {r : ℝ}, p.ball x r = Metric.ball x r
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
DerivedCategory.Plus.isZero_homology_of_isGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : DerivedCategory.Plus C) (n : ℤ) [X.IsGE n],
  ∀ i < n, CategoryTheory.Limits.IsZero ((DerivedCategory.Plus.homologyFunctor C i).obj X)