mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.uncurry_add : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → Add (γ a b)]
  (x y : (a : α) → (b : β a) → γ a b), Sigma.uncurry (x + y) = Sigma.uncurry x + Sigma.uncurry y
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.neg_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommGroup N₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂}
  (f : M →ₛₗ[σ₁₂] N₂) (x : M), (-f) x = -f x
-- Mathlib.Analysis.Seminorm
Seminorm.lt_def : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  {p q : Seminorm 𝕜 E}, p < q ↔ p ≤ q ∧ ∃ x, p x < q x
-- Mathlib.Data.ENNReal.Basic
ENNReal.lt_iff_exists_coe : ∀ {a b : ENNReal}, a < b ↔ ∃ p, a = ↑p ∧ ↑p < b
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates colimits, and `D` has all colimits, then `C` has all colimits.  -/
CategoryTheory.hasColimits_of_hasColimits_createsColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₂, u₂} D]
  [CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.HasColimitsOfSize.{w, w', v₁, u₁} C
-- Mathlib.Algebra.Category.Ring.Constructions
/-- The constructed pullback cone is indeed the limit.  -/
CommRingCat.pullbackConeIsLimit : {A B C : CommRingCat} → (f : A ⟶ C) → (g : B ⟶ C) → CategoryTheory.Limits.IsLimit (CommRingCat.pullbackCone f g)
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearMap.antilipschitz_of_comap_nhds_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [h : RingHomIsometric σ₁₂] (f : E →ₛₗ[σ₁₂] F),
  Filter.comap (⇑f) (nhds 0) ≤ nhds 0 → ∃ K, AntilipschitzWith K ⇑f
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.irreducible : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [CharP k p], Irreducible ↑p
-- Mathlib.Tactic.SetNotationForOrder
UsesSetNotationForOrder.mk : {α : Type u_1} → UsesSetNotationForOrder α
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.mulLeft_apply : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulLeftMono α] (a x : α), (OrderIso.mulLeft a) x = a * x
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.PullbackCone.combine_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} (f : F ⟶ H) (g : G ⟶ H)
  (c : (X : D) → CategoryTheory.Limits.PullbackCone (f.app X) (g.app X))
  (hc : (X : D) → CategoryTheory.Limits.IsLimit (c X)) (j : CategoryTheory.Limits.WalkingCospan),
  (CategoryTheory.Limits.PullbackCone.combine f g c hc).π.app j =
    Option.rec (CategoryTheory.CategoryStruct.comp { app := fun X => (c X).fst, naturality := ⋯ } f)
      (fun val =>
        CategoryTheory.Limits.WalkingPair.rec { app := fun X => (c X).fst, naturality := ⋯ }
          { app := fun X => (c X).snd, naturality := ⋯ } val)
      j
-- Lean.Server.Rpc.Basic
Lean.Server.rpcReleaseRef : Lean.Lsp.RpcRef → StateM Lean.Server.RpcObjectStore Bool
-- Mathlib.Order.Max
IsMin.eq_1 : ∀ {α : Type u_1} [inst : LE α] (a : α), IsMin a = ∀ ⦃b : α⦄, b ≤ a → a ≤ b
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.comp_preimage : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (U : Z.Opens),
  (TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.comp f g).base).obj U =
    (TopologicalSpace.Opens.map f.base).obj ((TopologicalSpace.Opens.map g.base).obj U)
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- We may bind the basic open sets of an open affine cover to form an affine cover that is also
a basis.  -/
AlgebraicGeometry.Scheme.affineBasisCover : (X : AlgebraicGeometry.Scheme) → X.OpenCover
-- Mathlib.Data.Fintype.Sum
Finset.toRight_eq_univ : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype β] {u : Finset (α ⊕ β)},
  u.toRight = Finset.univ ↔ Finset.map Function.Embedding.inr Finset.univ ⊆ u
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- Any module is the direct limit of its finitely generated submodules  -/
Submodule.FG.directLimit : (R : Type u) →
  [inst : Semiring R] →
    (M : Type u_1) →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [inst_3 : DecidableEq { P // P.FG }] →
            (Module.DirectLimit (fun P => ↥↑P) fun ⦃P Q⦄ h => Submodule.inclusion h) ≃ₗ[R] M
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.trivialOn.eq_1 : ∀ {α : Type u_1} (f : Set α),
  Hypergraph.trivialOn f = { vertexSet := f, edgeSet := ∅, subset_vertexSet_of_mem_edgeSet' := ⋯ }
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- `ContinuousLinearMap.inl` has a continuous left inverse.  -/
ContinuousLinearMap.HasLeftInverse.inl : ∀ {R : Type u_1} [inst : Semiring R] {F : Type u_4} {G : Type u_6} [inst_1 : TopologicalSpace F]
  [inst_2 : AddCommMonoid F] [inst_3 : Module R F] [inst_4 : TopologicalSpace G] [inst_5 : AddCommMonoid G]
  [inst_6 : Module R G], (ContinuousLinearMap.inl R F G).HasLeftInverse
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- If `A` is a commutative ring of prime characteristic `p` and `I` is an ideal such that
`I^p = 0`, then `I` admits a divided power structure.  -/
DividedPowers.IsNilpotent.dividedPowers : {A : Type u_1} →
  [inst : CommRing A] →
    {p : ℕ} →
      [Fact (Nat.Prime p)] →
        IsNilpotent ↑p → {I : Ideal A} → [DecidablePred fun x => x ∈ I] → I ^ p = 0 → DividedPowers I
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_insertMany_list : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List ((a : α) × β a)}, (m.insertMany l).isEmpty = (m.isEmpty && l.isEmpty)
-- Std.Http.Data.URI.Basic
/-- Builds a complete URI from the builder state, encoding all components. Defaults to "https" scheme if
none is specified.
 -/
Std.Http.URI.Builder.build : Std.Http.URI.Builder → Std.Http.URI
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CStarAlgebra.instPosPart : {A : Type u_1} →
  [inst : NonUnitalRing A] →
    [inst_1 : Module ℝ A] →
      [inst_2 : SMulCommClass ℝ A A] →
        [inst_3 : IsScalarTower ℝ A A] →
          [inst_4 : StarRing A] →
            [inst_5 : TopologicalSpace A] → [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] → PosPart A
-- Mathlib.Algebra.Order.ToIntervalMod
/-- **Alias** of the forward direction of `AddCommGroup.modEq_iff_toIocMod_eq_right`. -/
AddCommGroup.ModEq.toIcoMod_eq_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α}, a ≡ b [PMOD p] → toIocMod hp a b = a + p
-- Mathlib.Algebra.BigOperators.Balance
Fintype.balance_add : ∀ {ι : Type u_1} {G : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup G] [inst_2 : Module ℚ≥0 G] (f g : ι → G),
  Fintype.balance (f + g) = Fintype.balance f + Fintype.balance g
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_option_succ : ∀ {α : Type u_1} [inst : Encodable α] (n : ℕ), Encodable.decode n.succ = Option.map some (Encodable.decode n)
-- Mathlib.Data.Ineq
Mathlib.Ineq.ofNat : ℕ → Mathlib.Ineq
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.dense_target : ∀ {X Y : AlgebraicGeometry.Scheme} (self : X.PartialIso Y), Dense ↑self.target
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.category_id_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {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}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'),
  (CategoryTheory.CategoryStruct.id ψ).left = CategoryTheory.CategoryStruct.id ψ.left
-- Mathlib.RingTheory.Jacobson.Radical
/-- A product of modules with trivial Jacobson radical (e.g. simple modules) also has trivial
Jacobson radical.  -/
Module.jacobson_pi_eq_bot : ∀ (R : Type u_1) [inst : Ring R] {ι : Type u_6} (M : ι → Type u_5) [inst_1 : (i : ι) → AddCommGroup (M i)]
  [inst_2 : (i : ι) → Module R (M i)], (∀ (i : ι), Module.jacobson R (M i) = ⊥) → Module.jacobson R ((i : ι) → M i) = ⊥
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.exists₁ : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} (ac : e₁.AreComplementary e₂) {i₁ : ι₁},
  e₁.BoundaryLE i₁ → ∃ i₂, ac.Boundary i₁ i₂
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.ofSupportedInCLM.congr_simp : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n : ℕ∞} [inst_6 : SMulCommClass ℝ 𝕜 F]
  {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω),
  TestFunction.ofSupportedInCLM 𝕜 K_sub_Ω = TestFunction.ofSupportedInCLM 𝕜 K_sub_Ω
-- Aesop.Rule
Aesop.instOrdSafeRuleInfo : Ord Aesop.SafeRuleInfo
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_Ioi : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : α), ↑(Finset.Ioi a) = Set.Ioi a
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_le_of_map_zero : ∀ (f : CircleDeg1Lift) (x : ℝ), f x ≤ f 0 + ↑⌈x⌉
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.oppositeLeftAction_actionObj_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj (Opposite.op c) (Opposite.op d) =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesLimitEval : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c))
  [∀ (n : ι), CategoryTheory.Limits.HasLimit (F.comp (HomologicalComplex.eval C c n))] (n : ι),
  CategoryTheory.Limits.PreservesLimit F (HomologicalComplex.eval C c n)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.whiskerRight_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R S T : CategoryTheory.Over X} (f : S ⟶ T),
  CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.whiskerRight f R) =
    CategoryTheory.Limits.pullback.map S.hom R.hom T.hom R.hom (CategoryTheory.Over.Hom.left f)
      (CategoryTheory.CategoryStruct.id R.left) (CategoryTheory.CategoryStruct.id X) ⋯ ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipSuffixWhile_eq_revSkipWhile_endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  s.skipSuffixWhile pat = s.endPos.revSkipWhile pat
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.bcount.eq_def : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)] (p : { a // Irreducible a })
  (x : Associates.FactorSet α),
  Associates.bcount p x =
    match x with
    | none => 0
    | some s => Multiset.count p s
-- Mathlib.Algebra.Group.Pointwise.Set.ListOfFn
Set.mem_nsmul : ∀ {α : Type u_1} [inst : AddMonoid α] {s : Set α} {a : α} {n : ℕ}, a ∈ n • s ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.pseudofunctorOfIsLocallyDiscrete_mapId : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory B]
  [inst_1 : CategoryTheory.Bicategory.IsLocallyDiscrete B] [inst_2 : CategoryTheory.Bicategory C] (obj : B → C)
  (map : {b b' : B} → (b ⟶ b') → (obj b ⟶ obj b'))
  (mapId : (b : B) → map (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.CategoryStruct.id (obj b))
  (mapComp :
    {b₀ b₁ b₂ : B} →
      (f : b₀ ⟶ b₁) →
        (g : b₁ ⟶ b₂) →
          map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (map f) (map g))
  (map₂_associator :
    autoParam
      (∀ {b₀ b₁ b₂ b₃ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (h : b₂ ⟶ b₃),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapComp f g).hom (map h))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (map f) (map g) (map h)).hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapComp g h).inv)
                  (mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv))) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_1)
  (map₂_left_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp (CategoryTheory.CategoryStruct.id b₀) f).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (mapId b₀).hom (map f))
              (CategoryTheory.Bicategory.leftUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_3)
  (map₂_right_unitor :
    autoParam
      (∀ {b₀ b₁ : B} (f : b₀ ⟶ b₁),
        CategoryTheory.CategoryStruct.comp (mapComp f (CategoryTheory.CategoryStruct.id b₁)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (map f) (mapId b₁).hom)
              (CategoryTheory.Bicategory.rightUnitor (map f)).hom) =
          CategoryTheory.eqToHom ⋯)
      CategoryTheory.pseudofunctorOfIsLocallyDiscrete._auto_5)
  (b : B),
  (CategoryTheory.pseudofunctorOfIsLocallyDiscrete obj map mapId mapComp map₂_associator map₂_left_unitor
          map₂_right_unitor).mapId
      b =
    mapId b
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.instOne : {R : Type u_3} → {c₁ c₂ c₃ : R} → [Zero R] → [One R] → One (QuaternionAlgebra R c₁ c₂ c₃)
-- Mathlib.Algebra.Torsor.Defs
Torsor.nonempty : ∀ {G : outParam (Type u_1)} {P : Type u_2} {inst : Group G} [self : Torsor G P], Nonempty P
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.fieldId.sizeOf_spec : ∀ (stx : Lean.Syntax) (id : Option Lean.Name) (lctx : Lean.LocalContext) (structName : Lean.Name),
  sizeOf (Lean.Elab.CompletionInfo.fieldId stx id lctx structName) =
    1 + sizeOf stx + sizeOf id + sizeOf lctx + sizeOf structName
-- Mathlib.RingTheory.IdealFilter.Topology
/-- An `IdealFilter` on a ring `A` is uniform if and only if its ideals form a `RingFilterBasis`
for `A`.  -/
IdealFilter.isUniform_iff_exists_ringFilterBasis : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A}, F.IsUniform ↔ ∃ B, B.sets = {x | ∃ I ∈ F, ↑I = x}
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- A map to `E →SLₚₜ[σ] F` is continuous if for every `x : E` the evaluation `g · x` is
continuous.  -/
PointwiseConvergenceCLM.continuous_of_continuous_eval : ∀ {α : Type u_1} [inst : TopologicalSpace α] {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst_1 : NormedField 𝕜₁]
  [inst_2 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7} {F : Type u_8} [inst_3 : AddCommGroup E]
  [inst_4 : TopologicalSpace E] [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : Module 𝕜₁ E] [inst_9 : Module 𝕜₂ F] {g : α → E →SLₚₜ[σ] F},
  (∀ (x : E), Continuous fun x_1 => (g x_1) x) → Continuous g
-- Mathlib.Order.Interval.Basic
NonemptyInterval.map₂_pure : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : α → β → γ) (h₀ : ∀ (b : β), Monotone fun a => f a b) (h₁ : ∀ (a : α), Monotone (f a)) (a : α) (b : β),
  NonemptyInterval.map₂ f h₀ h₁ (NonemptyInterval.pure a) (NonemptyInterval.pure b) = NonemptyInterval.pure (f a b)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.length_dropUntil_le_length : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).length ≤ p.length
-- Mathlib.Analysis.Normed.Module.FiniteDimension
isOpen_setOfPred_nat_le_rank : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  (n : ℕ), IsOpen {f | ↑n ≤ (↑f).rank}
-- Mathlib.Analysis.Calculus.FDeriv.Prod
/-- A variant of `hasStrictFDerivAt_finCons` where the derivative variables are free on the RHS
instead.  -/
hasStrictFDerivAt_finCons' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ} {φ' : E →L[𝕜] F' 0} {φs' : E →L[𝕜] (i : Fin n) → F' i.succ},
  HasStrictFDerivAt (fun x => Fin.cons (φ x) (φs x)) (φ'.finCons φs') x ↔
    HasStrictFDerivAt φ φ' x ∧ HasStrictFDerivAt φs φs' x
-- Mathlib.Data.Set.Insert
Set.Nonempty.subset_pair_iff_eq : ∀ {α : Type u_1} {s : Set α} {a b : α}, s.Nonempty → (s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b})
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.keyAtIdx?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ},
  t₁.Equiv t₂ → t₁.keyAtIdx? i = t₂.keyAtIdx? i
-- Lean.Parser.Term
Lean.Parser.Term.show.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.val_eq_coe : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), ↑I = ↑I
-- Mathlib.RingTheory.Kaehler.Basic
/-- The module of Kähler differentials (Kahler differentials, Kaehler differentials).
This is implemented as `I / I ^ 2` with `I` the kernel of the multiplication map `S ⊗[R] S →ₐ[R] S`.
To view elements as a linear combination of the form `s • D s'`, use
`KaehlerDifferential.tensorProductTo_surjective` and `Derivation.tensorProductTo_tmul`.

We also provide the notation `Ω[S⁄R]` for `KaehlerDifferential R S`.
Note that the slash is `\textfractionsolidus`.
 -/
«termΩ[_⁄_]» : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instInhabited : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Inhabited (LieSubmodule R L M)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.uniqueAddEquiv_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (i : ι) [inst_1 : Subsingleton ι] (f : ι →₀ M),
  (Finsupp.uniqueAddEquiv i) f = f i
-- Mathlib.Order.Filter.Pointwise
/-- The negation of a filter is the pointwise preimage under `-` of its sets.  -/
Filter.instNeg : {α : Type u_2} → [Neg α] → Neg (Filter α)
-- Std.Async.Basic
/-- Handles errors in an `EAsync` computation by running a handler if one occurs.
 -/
Std.Async.EAsync.tryCatch : {ε α : Type} →
  Std.Async.EAsync ε α →
    (ε → Std.Async.EAsync ε α) →
      optParam Task.Priority Task.Priority.default → optParam Bool false → Std.Async.EAsync ε α
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.const_obj_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.SimplicialObject.Augmented.const.obj X).right = X
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_iSup_of_directed : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
  [Nonempty ι] (S : ι → Submodule R M), Directed (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ iSup S ↔ ∃ i, x ∈ S i
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))) (X : C)
  (R : F.RepresentableBy X),
  (CategoryTheory.Functor.RepresentableBy.equivUliftYonedaIso F X) R =
    CategoryTheory.NatIso.ofComponents (fun X_1 => equivEquivIso (Equiv.ulift.trans R.homEquiv)) ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
tprod_int_eq_zero_mul_tprod_pnat_sq : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G] [CompleteSpace G] [T2Space G]
  {f : ℤ → G}, Function.Even f → Multipliable f → ∏' (n : ℤ), f n = f 0 * (∏' (n : ℕ+), f ↑↑n) ^ 2
-- Mathlib.Data.Fintype.OfMap
/-- If `f : α → β` is a bijection and `α` is a fintype, then `β` is also a fintype.  -/
Fintype.ofBijective : {α : Type u_1} → {β : Type u_2} → [Fintype α] → (f : α → β) → Function.Bijective f → Fintype β
-- Init.Data.Array.Basic
/-- Returns the index of the first element equal to `a`, or the size of the array if no element is equal
to `a`.

Examples:
 * `#["carrot", "potato", "broccoli"].idxOf "carrot" = 0`
 * `#["carrot", "potato", "broccoli"].idxOf "broccoli" = 2`
 * `#["carrot", "potato", "broccoli"].idxOf "tomato" = 3`
 * `#["carrot", "potato", "broccoli"].idxOf "anything else" = 3`
 -/
Array.idxOf : {α : Type u} → [BEq α] → α → Array α → ℕ
-- Mathlib.Order.Filter.AtTopBot.Finset
/-- `Finset.card` tends to `atTop` along `atTop` on `Finset α`, when `α` is infinite.  -/
Filter.tendsto_card_atTop_atTop : ∀ {α : Type u_3} [Infinite α], Filter.Tendsto Finset.card Filter.atTop Filter.atTop
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instNeg : {R : Type u_1} → [inst : NegZeroClass R] → Neg (ArithmeticFunction R)
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_right_pure_floor : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [OrderClosedTopology α] (x : α), Filter.Tendsto Int.floor (nhdsWithin x (Set.Ici x)) (pure ⌊x⌋)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_prod_perm : ∀ {α : Type u_1} {l₁ l₂ : List (Equiv.Perm α)}, List.Pairwise Equiv.Perm.Disjoint l₁ → l₁.Perm l₂ → l₁.prod = l₂.prod
-- Mathlib.Data.Finset.Powerset
/-- The union of all `r`-element subsets of `s` is `s`, provided `1 ≤ r ≤ #s`.  -/
Finset.powersetCard_biUnion : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {r : ℕ},
  r ≠ 0 → r ≤ s.card → (Finset.powersetCard r s).biUnion id = s
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- A recursor for `WithUpperSet`. Use as `induction x`.  -/
Topology.WithUpperSet.rec : {α : Type u_1} →
  {motive : Topology.WithUpperSet α → Sort u_4} →
    ((a : α) → motive (Topology.WithUpperSet.toUpperSet a)) → (a : Topology.WithUpperSet α) → motive a
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_singleton : ∀ (x : ZFSet.{u_1}), {x}.rank = Order.succ x.rank
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsInaccessible.ne_zero : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → c ≠ 0
-- Mathlib.Order.Bounds.Basic
isGLB_lt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {a b : α}, IsGLB s a → (a < b ↔ ∃ c ∈ s, c < b)