mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.shift_unop_opShiftFunctorEquivalence_counitIso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n : ℤ),
  (CategoryTheory.shiftFunctor C n).map
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X).unop =
    ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.hom.app
        (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_uIcc_addNat : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) ⁻¹' Set.uIcc (i.addNat m) (j.addNat m) = Set.uIcc i j
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffOn.add_section : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {u : Set M},
  ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) u →
    ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) u →
      ContMDiffOn I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (s + t) x⟩) u
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.fullChange : String → Lean.Lsp.TextDocumentContentChangeEvent
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (F : CategoryTheory.Functor I C) [inst_2 : CategoryTheory.Limits.HasColimit F] (i : I)
  {Z : CategoryTheory.Functor C (Type u₂)} (h : CategoryTheory.coyoneda.obj (F.op.obj (Opposite.op i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op) h
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.formatStringToFormat : Lean.TSyntax `str → Option (Lean.TSyntax `term) → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
/-- A measurable set of negative measure has a negative subset of negative measure.  -/
MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  s i < 0 →
    ∃ j,
      MeasurableSet j ∧
        j ⊆ i ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ s j < 0
-- Init.Data.BitVec.Lemmas
BitVec.neg_one_eq_allOnes : ∀ {w : ℕ}, -1#w = BitVec.allOnes w
-- Init.Data.UInt.Bitwise
USize.toUInt64_shiftRight : ∀ (a b : USize), (a >>> b).toUInt64 = a.toUInt64 >>> (b.toUInt64 % UInt64.ofNat System.Platform.numBits)
-- Mathlib.GroupTheory.PresentedGroup
/-- `FreeGroup α →* FreeGroup β` induces a homomorphism
`PresentedGroup s →* PresentedGroup t` if the image of `s` is contained in `t`.
 -/
PresentedGroup.map : {α : Type u_1} →
  {β : Type u_2} →
    (f : FreeGroup α →* FreeGroup β) →
      {s : Set (FreeGroup α)} → {t : Set (FreeGroup β)} → Set.MapsTo (⇑f) s t → PresentedGroup s →* PresentedGroup t
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
div_lt_arithGeom : ∀ {R : Type u_1} {a b u₀ : R} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R],
  0 < a → a ≠ 1 → b / (1 - a) < u₀ → ∀ (n : ℕ), b / (1 - a) < arithGeom a b u₀ n
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.MemLp.integrable_enorm_pow' : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [MeasureTheory.IsFiniteMeasure μ] {f : α → ε} {p : ℕ},
  MeasureTheory.MemLp f (↑p) μ → MeasureTheory.Integrable (fun x => ‖f x‖ₑ ^ p) μ
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_insert_of_mem : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v' : α} [Std.TransCmp cmp] (v : α) {t : RBTree.RBSet α cmp},
  v' ∈ t → v' ∈ t.insert v
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.snd_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : CategoryTheory.Mon C),
  (CategoryTheory.SemiCartesianMonoidalCategory.snd M N).hom = CategoryTheory.SemiCartesianMonoidalCategory.snd M.X N.X
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ) {ν k : ℕ},
  k < ν → Polynomial.eval 0 ((⇑Polynomial.derivative)^[k] (bernsteinPolynomial R n ν)) = 0
-- Mathlib.NumberTheory.NumberField.CMField
/-- A variant of the complex conjugation defined as an `AlgEquiv` on the ring of integers.
 -/
NumberField.IsCMField.ringOfIntegersComplexConj : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : CharZero K] →
      [NumberField.IsCMField K] →
        [Algebra.IsIntegral ℚ K] →
          NumberField.RingOfIntegers K ≃ₐ[NumberField.RingOfIntegers ↥(NumberField.maximalRealSubfield K)]
            NumberField.RingOfIntegers K
-- ImportGraph.Tools.FindHome
/-- When clicked, this widget component jumps to the source of the module `modName`,
assuming a source URI can be found for the module.  -/
GoToModuleLink : Lean.Widget.Module
-- Init.System.IO
IO.FileRight.mk.injEq : ∀ (user group other user_1 group_1 other_1 : IO.AccessRight),
  ({ user := user, group := group, other := other } = { user := user_1, group := group_1, other := other_1 }) =
    (user = user_1 ∧ group = group_1 ∧ other = other_1)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
/-- If the `σ`-algebra of the codomain of a null measurable function is countably generated,
then the function is a.e.-measurable.  -/
MeasureTheory.NullMeasurable.aemeasurable : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : α → β} [hc : MeasurableSpace.CountablyGenerated β], MeasureTheory.NullMeasurable f μ → AEMeasurable f μ
-- Mathlib.ModelTheory.Definability
Set.Definable.map_expansion : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {s : Set (α → M)}
  {L' : FirstOrder.Language} [inst_1 : L'.Structure M],
  A.Definable L s → ∀ (φ : L →ᴸ L') [φ.IsExpansionOn M], A.Definable L' s
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.instMonoidalFunctorOppositePresheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [inst_2 : CategoryTheory.MonoidalCategory A] →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [CategoryTheory.LocallySmall.{w, v, u} C] →
                  [∀ (X : A),
                        CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
                          (CategoryTheory.MonoidalCategory.tensorLeft X)] →
                    [∀ (X : A),
                          CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
                            (CategoryTheory.MonoidalCategory.tensorRight X)] →
                      Φ.presheafFiber.Monoidal
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.den_eq_conts_b : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K], g.dens n = (g.conts n).b
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMap_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology]
  [inst_4 : S₃.HasRightHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
  CategoryTheory.ShortComplex.opcyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ₁)
      (CategoryTheory.ShortComplex.opcyclesMap φ₂)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedDiagnostics : Inhabited Lean.Meta.Simp.Diagnostics
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_assoc' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α),
  Associated (gcd (gcd m n) k) (gcd m (gcd n k))
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair.mk : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          ({A B : C} →
              (f g : A ⟶ B) →
                [F.IsCosplitPair f g] → CategoryTheory.CreatesLimit (CategoryTheory.Limits.parallelPair f g) F) →
            CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair F
-- Mathlib.Data.Set.Basic
Set.instNonemptyTop : ∀ {α : Type u} [Nonempty α], Nonempty ↑⊤
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l).get k' h = k
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.mapA.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.map_add_right : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {M₂ : Type u_12} {N₂ : Type u_14} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R M] [inst_7 : Module R N]
  [inst_8 : Module R₂ M₂] [inst_9 : Module R₂ N₂] (f : M →ₛₗ[σ₁₂] M₂) (g₁ g₂ : N →ₛₗ[σ₁₂] N₂),
  TensorProduct.map f (g₁ + g₂) = TensorProduct.map f g₁ + TensorProduct.map f g₂
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is twice differentiable on `ℝ`, and `f''` is nonpositive on `ℝ`,
then `f` is concave on `ℝ`.  -/
concaveOn_univ_of_deriv2_nonpos : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → Differentiable ℝ (deriv f) → (∀ (x : ℝ), deriv^[2] f x ≤ 0) → ConcaveOn ℝ Set.univ f
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- A submodule over `S` which is stable under scalar multiplication by elements of `M` is a
submodule over `S[M]`  -/
MonoidAlgebra.submoduleOfSMulMem : {S : Type u_2} →
  {M : Type u_3} →
    [inst : CommSemiring S] →
      [inst_1 : Monoid M] →
        {V : Type u_7} →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module S V] →
              [inst_4 : Module (MonoidAlgebra S M) V] →
                [IsScalarTower S (MonoidAlgebra S M) V] →
                  (W : Submodule S V) →
                    (∀ (g : M), ∀ v ∈ W, (MonoidAlgebra.of S M) g • v ∈ W) → Submodule (MonoidAlgebra S M) V
-- Mathlib.Topology.Spectral.Hom
SpectralMap.mk.injEq : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (toFun : α → β)
  (spectral' : IsSpectralMap toFun) (toFun_1 : α → β) (spectral'_1 : IsSpectralMap toFun_1),
  ({ toFun := toFun, spectral' := spectral' } = { toFun := toFun_1, spectral' := spectral'_1 }) = (toFun = toFun_1)
-- Mathlib.RingTheory.Perfection
Perfection.coeffMonoidHom_pow_p' : ∀ {M : Type u_1} [inst : CommMonoid M] {p : ℕ} (f : Perfection M p) (n : ℕ),
  (Perfection.coeffMonoidHom M p (n + 1)) f ^ p = (Perfection.coeffMonoidHom M p n) f
-- Init.Data.Nat.Control
_private.Init.Data.Nat.Control.0.Nat.foldM.loop : {α : Type u} → {m : Type u → Type v} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → α → m α) → (i : ℕ) → i ≤ n → α → m α
-- Mathlib.Algebra.Module.Hom
AddMonoid.End.isScalarTower : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : AddCommMonoid A]
  [inst_3 : DistribMulAction R A] [inst_4 : DistribMulAction S A] [inst_5 : SMul R S] [IsScalarTower R S A],
  IsScalarTower R S (AddMonoid.End A)
-- Mathlib.RingTheory.SurjectiveOnStalks
RingHom.SurjectiveOnStalks.of_comp : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {T : Type u_3} [inst_2 : CommRing T]
  {g : S →+* T} {f : R →+* S}, (g.comp f).SurjectiveOnStalks → g.SurjectiveOnStalks
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.smul_fst : ∀ {R : Type u_1} {A : Type u_2} {E : Type u_3} {F : Type u_4} [inst : SMul R E] [inst_1 : SMul R F]
  (x : WithCStarModule A (E × F)) (c : R), (c • x).1 = c • x.1
-- Mathlib.Data.FunLike.Basic
DFunLike.ext' : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, ⇑f = ⇑g → f = g
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheorems.mk.inj : ∀
  {theorems theorems_1 :
    Std.HashMap (Lean.Name × Mathlib.Meta.FunProp.LambdaTheoremType) (Array Mathlib.Meta.FunProp.LambdaTheorem)},
  { theorems := theorems } = { theorems := theorems_1 } → theorems = theorems_1
-- Mathlib.AlgebraicGeometry.FunctionField
AlgebraicGeometry.instIsAffineXSchemeAffineCover : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X), AlgebraicGeometry.IsAffine (X.affineCover.X x)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.lt_lt_combine : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.lt_lt_combine_cert p₁ p₂ p₃ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ < 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ < 0 → Lean.Grind.Linarith.Poly.denote' ctx p₃ < 0
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
CategoryTheory.Functor.partialLeftAdjointHomEquiv_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D C) {X Y : F.PartialLeftAdjointSource} (f : X ⟶ Y),
  F.partialLeftAdjointHomEquiv (F.partialLeftAdjointMap f) =
    CategoryTheory.CategoryStruct.comp f.hom
      (F.partialLeftAdjointHomEquiv (CategoryTheory.CategoryStruct.id (F.partialLeftAdjointObj Y)))
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanIndex_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] (d : (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).L),
  (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z).fst d = (↑d.snd).1
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioc_symm : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioc a b ∪ Set.Ioc b a = Set.Ioc (min a b) (max a b)
-- Init.Data.Vector.Monadic
Vector.allM_pure : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → Bool} {xs : Vector α n},
  Vector.allM (fun x => pure (p x)) xs = pure (xs.all p)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.norm_approxOn_zero_le : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [inst_3 : OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} (h₀ : 0 ∈ s)
  [inst_4 : TopologicalSpace.SeparableSpace ↑s] (x : β) (n : ℕ),
  ‖(MeasureTheory.SimpleFunc.approxOn f hf s 0 h₀ n) x‖ ≤ ‖f x‖ + ‖f x‖
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
/-- The power series expansion of `Complex.arctan`, valid on the open unit disc.  -/
Complex.hasSum_arctan : ∀ {z : ℂ}, ‖z‖ < 1 → HasSum (fun n => (-1) ^ n * z ^ (2 * n + 1) / ↑(2 * n + 1)) z.arctan
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.contains'.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α → Ordering) (size : ℕ) (k' : α) (v : β k')
  (l_2 r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.contains' k (Std.DTreeMap.Internal.Impl.inner size k' v l_2 r) =
    match k k' with
    | Ordering.lt => Std.DTreeMap.Internal.Impl.contains' k l_2
    | Ordering.gt => Std.DTreeMap.Internal.Impl.contains' k r
    | Ordering.eq => true
-- Mathlib.Topology.Separation.Hausdorff
separated_by_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T2Space Y] {f : X → Y},
  Continuous f → ∀ {x y : X}, f x ≠ f y → ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v
-- Mathlib.Data.Int.Cast.Lemmas
zmultiplesAddHom_symm_apply : ∀ (β : Type u_4) [inst : AddCommGroup β] (f : ℤ →+ β), (zmultiplesAddHom β).symm f = f 1
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.lift_obj_functor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  (H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂) (X : C),
  (CategoryTheory.Quotient.lift r F H).obj ((CategoryTheory.Quotient.functor r).obj X) = F.obj X
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- A component of a transposed form of the conjugation definition.  -/
CategoryTheory.conjugateEquiv_counit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (α : L₂ ⟶ L₁) (d : D),
  CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.conjugateEquiv adj₁ adj₂) α).app d))
      (adj₂.counit.app d) =
    CategoryTheory.CategoryStruct.comp (α.app (R₁.obj d)) (adj₁.counit.app d)
-- Aesop.RuleTac.Tactic
Aesop.RuleTac.tacGenImpl : Lean.Name → Aesop.RuleTac
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If a function is `C^n` with `n ≥ 1`, then it is differentiable.  -/
ContDiff.differentiable : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiff 𝕜 n f → n ≠ 0 → Differentiable 𝕜 f
-- Std.Http.Data.Body.Basic
/-- Returns `true` when the body stream is closed.
 -/
Std.Http.Body.isClosed : {α : Type} → [self : Std.Http.Body α] → α → Std.Async.Async Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
/-- If `F ⋙ G` preserves finite products and `G` reflects finite products, then `F` preserves
finite products.
 -/
CategoryTheory.Limits.preservesFiniteProducts_of_reflects_of_preserves : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesFiniteProducts (F.comp G)]
  [CategoryTheory.Limits.ReflectsFiniteProducts G], CategoryTheory.Limits.PreservesFiniteProducts F
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.RenameParams : Type
-- Mathlib.Topology.Order.Basic
/-- Consider a disjoint family of intervals `(x, y)` with `x < y` in a second-countable space.
Then the family is countable.
This is not a straightforward consequence of second-countability as some of these intervals might be
empty (but in fact this can happen only for countably many of them).  -/
Set.PairwiseDisjoint.countable_of_Ioo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {y : α → α} {s : Set α}, (s.PairwiseDisjoint fun x => Set.Ioo x (y x)) → (∀ x ∈ s, x < y x) → s.Countable
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey! k = default
-- Std.Do.SPred.Notation
/-- Unexpander that reconstructs `spred(... → ...)⌝` syntax from applications of `SPred.imp`, lifting
nested applications of `spred(...)` from the arguments.
 -/
Std.Do.SPred.Notation.unexpandImp : Lean.PrettyPrinter.Unexpander
-- Mathlib.Data.Set.Function
Set.SurjOn.congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β},
  Set.SurjOn f₁ s t → Set.EqOn f₁ f₂ s → Set.SurjOn f₂ s t
-- Mathlib.Algebra.Category.Ring.Limits
CommRingCat.forget₂CommSemiRing_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ CommRingCat CommSemiRingCat)
-- Init.Meta.Defs
Lean.Syntax.isNatLit? : Lean.Syntax → Option ℕ
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.coe_srange : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F), ↑(NonUnitalRingHom.srange f) = Set.range ⇑f
-- Lean.Meta.Tactic.Simp.Arith.Int.Simp
Lean.Meta.Simp.Arith.Int.simpRel? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Data.Matrix.DMatrix
/-- `DMatrix.row u` is the row matrix whose entries are given by `u`.  -/
DMatrix.row : {n : Type u_2} → {α : n → Type v} → ((j : n) → α j) → DMatrix Unit n fun _i j => α j
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.irrelevant_le_map_comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {σ : Type u_4} {τ : Type u_5} {ω : Type u_6} {ι : Type u_7}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ω C] [inst_6 : AddSubmonoidClass σ A] [inst_7 : AddSubmonoidClass τ B]
  [inst_8 : AddSubmonoidClass ω C] [inst_9 : DecidableEq ι] [inst_10 : AddCommMonoid ι] [inst_11 : PartialOrder ι]
  [inst_12 : CanonicallyOrderedAdd ι] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ω} [inst_13 : GradedRing 𝒜]
  [inst_14 : GradedRing ℬ] [inst_15 : GradedRing 𝒞] {f : 𝒜 →+*ᵍ ℬ} {g : ℬ →+*ᵍ 𝒞},
  HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜) →
    HomogeneousIdeal.irrelevant 𝒞 ≤ HomogeneousIdeal.map g (HomogeneousIdeal.irrelevant ℬ) →
      HomogeneousIdeal.irrelevant 𝒞 ≤ HomogeneousIdeal.map (g.comp f) (HomogeneousIdeal.irrelevant 𝒜)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalars_isEquivalence_of_ringEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S),
  (ModuleCat.restrictScalars e.toRingHom).IsEquivalence
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.id_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.CategoryStruct.id S).τ₃ = CategoryTheory.CategoryStruct.id S.X₃
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.mulCayley_singleton_one : ∀ {M : Type u_1} [inst : MulOneClass M], SimpleGraph.mulCayley {1} = ⊥