mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.SmallHom
/-- The composition on `SmallHom W`.  -/
CategoryTheory.Localization.SmallHom.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {X Y Z : C} →
        [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] →
          [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W Y Z] →
            [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Z] →
              CategoryTheory.Localization.SmallHom W X Y →
                CategoryTheory.Localization.SmallHom W Y Z → CategoryTheory.Localization.SmallHom W X Z
-- Mathlib.Data.Multiset.MapFold
Multiset.inj_on_of_nodup_map : ∀ {α : Type u_1} {β : Type v} {f : α → β} {s : Multiset α},
  (Multiset.map f s).Nodup → ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.RawView.mk : {α : Type u} →
  {β : α → Type v} → (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl.RawView α β
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Indep.indep_isRestriction : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α}, M.Indep I → N.IsRestriction M → I ⊆ N.E → N.Indep I
-- Mathlib.RingTheory.Unramified.Dedekind
/-- A domain finite and unramified over a Dedekind domain is a Dedekind domain.  -/
isDedekindDomain.of_formallyUnramified : ∀ (A : Type u_1) (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [Module.Finite A B]
  [IsDedekindDomain A] [IsDomain B] [Algebra.FormallyUnramified A B], IsDedekindDomain B
-- Lean.Meta.Basic
/-- When `Config.univApprox := true`, this flag is set to `true` when there is no
progress processing universe constraints.
 -/
Lean.Meta.Context.univApprox : Lean.Meta.Context → Bool
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteEdges_le_of_le : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s s' : Set (Sym2 V)},
  s ⊆ s' → G'.deleteEdges s' ≤ G'.deleteEdges s
-- Mathlib.FieldTheory.Fixed
FixedPoints.smul : ∀ (M : Type u) [inst : Monoid M] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction M F] (m : M)
  (x : ↥(FixedPoints.subfield M F)), m • x = x
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.instCommSemiringOfCanonicallyOrderedAdd : {α : Type u_2} →
  [inst : CommSemiring α] → [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → CommSemiring (NonemptyInterval α)
-- Mathlib.Order.Minimal
Maximal.eq_of_ge : ∀ {α : Type u_2} {P : α → Prop} {x y : α} [inst : PartialOrder α], Maximal P x → P y → x ≤ y → y = x
-- Init.Data.Int.DivMod.Lemmas
Int.sub_mul_ediv_right : ∀ (a b : ℤ) {c : ℤ}, c ≠ 0 → (a - b * c) / c = a / c - b
-- Mathlib.Order.BooleanAlgebra.Basic
sup_sdiff_inf : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (x y : α), x \ y ⊔ x ⊓ y = x
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_pow : ∀ (a : USize) (n : ℕ) (h : System.Platform.numBits = 32), (a ^ n).toBitVec32 h = a.toBitVec32 h ^ n
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.symm_comp_self : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), ⇑h.symm ∘ ⇑h = id
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.CostructuredArrow.createsColimit : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {G : CategoryTheory.Functor A T} →
              {X : T} →
                (F : CategoryTheory.Functor J (CategoryTheory.CostructuredArrow G X)) →
                  [i : CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.CostructuredArrow.proj G X)) G] →
                    CategoryTheory.CreatesColimit F (CategoryTheory.CostructuredArrow.proj G X)
-- Mathlib.Algebra.Exact.Basic
LinearMap.exact_subtype_ker_map : ∀ {R : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Ring R] [inst_1 : AddCommGroup N] [inst_2 : AddCommGroup P]
  [inst_3 : Module R N] [inst_4 : Module R P] (g : N →ₗ[R] P), Function.Exact ⇑g.ker.subtype ⇑g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : Option β → Option β},
  (Std.ExtDTreeMap.Const.alter t k f).getKey! k =
    if (f (Std.ExtDTreeMap.Const.get? t k)).isSome = true then k else default
-- Mathlib.Order.Bounds.Basic
lowerBounds_le_upperBounds_of_nonempty_inter : ∀ {α : Type u_1} [inst : Preorder α] {s s' : Set α} {a b : α},
  (s ∩ s').Nonempty → a ∈ lowerBounds s → b ∈ upperBounds s' → a ≤ b
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.σ_objEquiv_symm_apply : ∀ {n : ℕ} {m : SimplexCategory} (f : { len := n } ⟶ m) (i : Fin (n + 1)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (SSet.stdSimplex.obj m) i))
      (SSet.stdSimplex.objEquiv.symm f) =
    SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ i) f)
-- Init.Data.UInt.Lemmas
USize.ofNat_uInt32ToNat : ∀ (n : UInt32), USize.ofNat n.toNat = n.toUSize
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_Ioo_succ : ∀ {n : ℕ} (i j : Fin n), Fin.succ ⁻¹' Set.Ioo i.succ j.succ = Set.Ioo i j
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instDistribMulActionOfSMulCommClass : {R : Type uR} →
  {S : Type uS} →
    {ι : Type uι} →
      {M₁ : ι → Type v₁} →
        {M₂ : Type v₂} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : (i : ι) → Module R (M₁ i)] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M₂] →
                    [inst_5 : Monoid S] →
                      [inst_6 : DistribMulAction S M₂] →
                        [SMulCommClass R S M₂] → DistribMulAction S (MultilinearMap R M₁ M₂)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.isSheaf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} (self : SheafOfModules R), CategoryTheory.Presheaf.IsSheaf J self.val.presheaf
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ordCompare_minKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtDTreeMap α (fun x => β) compare}
  {k : α} {f : β → β} {fallback : α},
  compare ((Std.ExtDTreeMap.Const.modify t k f).minKeyD fallback) (t.minKeyD fallback) = Ordering.eq
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.mk.inj : ∀ {R : Type u} {inst : CommRing R} {u : Rˣ} {r s t : R} {u_1 : Rˣ} {r_1 s_1 t_1 : R},
  { u := u, r := r, s := s, t := t } = { u := u_1, r := r_1, s := s_1, t := t_1 } →
    u = u_1 ∧ r = r_1 ∧ s = s_1 ∧ t = t_1
-- Mathlib.Analysis.Convex.Slope
/-- A function `f : 𝕜 → 𝕜` is strictly convex iff for any three points `x < y < z` the slope of
the secant line of `f` on `[x, y]` is strictly less than the slope of the secant line of `f` on
`[y, z]`.  -/
strictConvexOn_iff_slope_strict_mono_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.valued : (K : Type u_2) → [inst : Field K] → Valued (LaurentSeries K) (WithZero (Multiplicative ℤ))
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.testBit.match_1.eq_6 : ∀ (motive : PosNum → ℕ → Sort u_1) (p : PosNum) (n : ℕ) (h_1 : Unit → motive PosNum.one 0)
  (h_2 : (x : ℕ) → motive PosNum.one x) (h_3 : (a : PosNum) → motive a.bit0 0)
  (h_4 : (p : PosNum) → (n : ℕ) → motive p.bit0 n.succ) (h_5 : (a : PosNum) → motive a.bit1 0)
  (h_6 : (p : PosNum) → (n : ℕ) → motive p.bit1 n.succ),
  (match p.bit1, n.succ with
    | PosNum.one, 0 => h_1 ()
    | PosNum.one, x => h_2 x
    | a.bit0, 0 => h_3 a
    | p.bit0, n.succ => h_4 p n
    | a.bit1, 0 => h_5 a
    | p.bit1, n.succ => h_6 p n) =
    h_6 p n
-- Mathlib.Algebra.Category.ModuleCat.Tannaka
CategoryTheory.AdditiveFunctor.of.congr_simp : ∀ {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] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1) [inst_4 : F.Additive],
  CategoryTheory.AdditiveFunctor.of F = CategoryTheory.AdditiveFunctor.of F_1
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_subset_Ioc_union_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a ⊆ Set.Ioc a b ∪ Set.Ioi b
-- Mathlib.Tactic.ProxyType
/-- Configuration used by `mkProxyEquiv`.  -/
Mathlib.ProxyType.ProxyEquivConfig : Type
-- Batteries.Lean.Meta.Basic
/-- Check whether a metavariable is declared.
 -/
Lean.MVarId.isDeclared : {m : Type → Type} → [Monad m] → [Lean.MonadMCtx m] → Lean.MVarId → m Bool
-- Mathlib.Data.ENNReal.Inv
ENNReal.eq_div_iff : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → (b = c / a ↔ a * b = c)
-- Init.Data.Vector.Find
Vector.getElem?_zero_flatten : ∀ {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n}, xss.flatten[0]? = Vector.findSome? (fun xs => xs[0]?) xss
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_mul_right : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] (a : G),
  IsOpenMap fun x => x * a
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instIsAddApply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)), IsAddApply (UniformConvergenceCLM σ F 𝔖) E F
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimit_neg_mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (x : (j : J) × ↑(F.obj j)),
  -AddGrpCat.FilteredColimits.G.mk F x = AddGrpCat.FilteredColimits.G.mk F ⟨x.fst, -x.snd⟩
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- `ProfiniteGrp.limitCone` is a limit cone.  -/
ProfiniteGrp.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}) → CategoryTheory.Limits.IsLimit (ProfiniteGrp.limitCone F)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_add_of_le_of_lt : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightMono α] {a b c d : α},
  a ≤ b → c < d → a + c < b + d
-- Batteries.Data.List.Lemmas
List.findIdxNth_eq_findIdxNth_iff : ∀ {α : Type u_1} {p : α → Bool} {n m : ℕ} {xs : List α},
  List.findIdxNth p xs n = List.findIdxNth p xs m ↔ (List.countP p xs ≤ m ∨ n ≤ m) ∧ (List.countP p xs ≤ n ∨ m ≤ n)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- `AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)`  -/
AddMemClass : (S : Type u_3) → (M : outParam (Type u_4)) → [Add M] → [SetLike S M] → Prop
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
WeakBilin.instModule : {𝕜 : Type u_3} →
  {𝕝 : Type u_1} →
    {E : Type u_2} →
      {F : Type u_4} →
        [inst : CommSemiring 𝕜] →
          [inst_1 : AddCommMonoid E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : AddCommMonoid F] →
                [inst_4 : Module 𝕜 F] →
                  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) → [inst_5 : CommSemiring 𝕝] → [Module 𝕝 E] → Module 𝕝 (WeakBilin B)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.isUnit_iff_singleton : ∀ {α : Type u_2} [inst : Group α] {s : Set α}, IsUnit s ↔ ∃ a, s = {a}
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.pow_smul_top_le_ker_eval : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), I ^ n • ⊤ ≤ (AdicCompletion.eval I M n).ker
-- Mathlib.Algebra.Lie.Nilpotent
/-- Given a non-trivial nilpotent Lie module `M` with lower central series
`M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥`, this is the `k-1`th term in the lower central series (the last
non-trivial term).

For a trivial or non-nilpotent module, this is the bottom submodule, `⊥`.  -/
LieModule.lowerCentralSeriesLast : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [LieAlgebra R L] →
            [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → LieSubmodule R L M
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} (h' : k ∈ t), t.getKey k h' = k
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mk.inj : ∀ {ι : Type u_2} {lower upper : ι → ℝ} {lower_lt_upper : ∀ (i : ι), lower i < upper i} {lower_1 upper_1 : ι → ℝ}
  {lower_lt_upper_1 : ∀ (i : ι), lower_1 i < upper_1 i},
  { lower := lower, upper := upper, lower_lt_upper := lower_lt_upper } =
      { lower := lower_1, upper := upper_1, lower_lt_upper := lower_lt_upper_1 } →
    lower = lower_1 ∧ upper = upper_1
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.isLink_congr : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β},
  x ∈ H.vertexSet → y ∈ H.vertexSet → H.IsInducedSubgraph G → (H.IsLink e x y ↔ G.IsLink e x y)
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
RingHom.IsIntegralElem.neg_iff : ∀ {R : Type u_1} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {x : S},
  f.IsIntegralElem (-x) ↔ f.IsIntegralElem x
-- Mathlib.Algebra.Free
FreeMagma.mul : {α : Type u} → FreeMagma α → FreeMagma α → FreeMagma α
-- Mathlib.GroupTheory.GroupAction.Hom
DistriMulActionHom.instZero : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_11} →
            [inst_2 : AddMonoid A] →
              [inst_3 : DistribMulAction M A] →
                {B : Type u_12} → [inst_4 : AddMonoid B] → [inst_5 : DistribMulAction N B] → Zero (A →ₑ+[φ] B)
-- Mathlib.CategoryTheory.Abelian.Subcategory
CategoryTheory.ObjectProperty.instAbelianFullSubcategoryOfContainsZeroOfIsClosedUnderKernelsOfIsClosedUnderCokernelsOfIsClosedUnderFiniteProducts : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.ObjectProperty C) →
      [inst_1 : CategoryTheory.Abelian C] →
        [P.ContainsZero] →
          [P.IsClosedUnderKernels] →
            [P.IsClosedUnderCokernels] → [P.IsClosedUnderFiniteProducts] → CategoryTheory.Abelian P.FullSubcategory
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber.eq_1 : ∀ {V : Type u} (G : SimpleGraph V), G.chromaticNumber = ⨅ n ∈ Set.ofPred G.Colorable, ↑n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_pi_div_two : Real.sin (Real.pi / 2) = 1
-- Init.Data.UInt.Lemmas
instCommutativeUInt8HMul : Std.Commutative fun x1 x2 => x1 * x2
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.addRightStrictMono : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddMonoid N] [inst_2 : LinearOrder N]
  [AddRightStrictMono N], AddRightStrictMono (Colex (α →₀ N))
-- Mathlib.Algebra.Module.Submodule.Ker
LinearMap.ker_sup_ker_le_ker_comp_of_commute : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {f g : M →ₗ[R] M},
  Commute f g → f.ker ⊔ g.ker ≤ (f ∘ₗ g).ker
-- Mathlib.LinearAlgebra.Dimension.RankNullity
LinearMap.lift_rank_quot_map_le : ∀ {R : Type u_1} {M : Type u} {M' : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M']
  [inst_3 : Module R M] [inst_4 : Module R M'] [HasRankNullity.{v, u_1} R] {f : M →ₗ[R] M'} (p : Submodule R M),
  Cardinal.lift.{u, v} (Module.rank R (M' ⧸ Submodule.map f p)) ≤
    Cardinal.lift.{u, v} (Module.rank R (M' ⧸ f.range)) + Cardinal.lift.{v, u} (Module.rank R (M ⧸ p))
-- Mathlib.Tactic.NormNum.Result
/-- If `a = b` and we can evaluate `b`, then we can evaluate `a`.  -/
Mathlib.Meta.NormNum.Result.eqTrans : {u : Lean.Level} →
  {α : Q(Type u)} → {a b : Q(«$α»)} → Q(«$a» = «$b») → Mathlib.Meta.NormNum.Result b → Mathlib.Meta.NormNum.Result a
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Imp.trans : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ θ : L.BoundedFormula α n},
  T.Imp φ ψ → T.Imp ψ θ → T.Imp φ θ
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_empty : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Preorder ι] [inst_1 : InfSet ι] {u : ι → Ω → β} (n m : ι),
  MeasureTheory.hittingBtwn u ∅ n m = fun x => m
-- Lean.Expr
Lean.Int.mkInstNeg : Lean.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eq_none_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  Std.Internal.List.minKey? l = none ↔ l.isEmpty = true
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesFiniteColimitsEvalOfHasFiniteColimits : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteColimits C] (n : ι),
  CategoryTheory.Limits.PreservesFiniteColimits (HomologicalComplex.eval C c n)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_add_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R}
  [IsStrictOrderedRing R], 0 ≤ a → ⌈a + 1⌉₊ = ⌈a⌉₊ + 1
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : DecidableEq σ] [inst_2 : CommSemiring R]
  (f : MvPowerSeries σ R), Filter.Tendsto (fun d => ↑((MvPowerSeries.trunc' R d) f)) Filter.atTop (nhds f)
-- Mathlib.Algebra.Group.Conj
IsAddConj.trans : ∀ {α : Type u} [inst : AddMonoid α] {a b c : α}, IsAddConj a b → IsAddConj b c → IsAddConj a c
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.symm_mapRingEquiv : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R ≃+* S) (p : Polynomial R)
  (q : Polynomial S) (h : Associated (Polynomial.map (↑f) p) q),
  (AdjoinRoot.mapRingEquiv f p q h).symm = AdjoinRoot.mapRingEquiv f.symm q p ⋯
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- If `f : X → Y` is Lipschitz in a neighborhood of each point `x : X`, then the Hausdorff
dimension of `range f` is at most the Hausdorff dimension of `X`.  -/
dimH_range_le_of_locally_lipschitzOn : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] [SecondCountableTopology X]
  {f : X → Y}, (∀ (x : X), ∃ C, ∃ s ∈ nhds x, LipschitzOnWith C f s) → dimH (Set.range f) ≤ dimH Set.univ
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {P : CategoryTheory.ProjectiveResolution Z} {Z' : C}
  {P' : CategoryTheory.ProjectiveResolution Z'} {f : Z ⟶ Z'} (hom : P.complex ⟶ P'.complex)
  (hom_f_zero_comp_π_f_zero :
    CategoryTheory.CategoryStruct.comp (hom.f 0) (P'.π.f 0) =
      CategoryTheory.CategoryStruct.comp (P.π.f 0) (((ChainComplex.single₀ C).map f).f 0))
  (hom_1 : P.complex ⟶ P'.complex)
  (hom_f_zero_comp_π_f_zero_1 :
    CategoryTheory.CategoryStruct.comp (hom_1.f 0) (P'.π.f 0) =
      CategoryTheory.CategoryStruct.comp (P.π.f 0) (((ChainComplex.single₀ C).map f).f 0)),
  ({ hom := hom, hom_f_zero_comp_π_f_zero := hom_f_zero_comp_π_f_zero } =
      { hom := hom_1, hom_f_zero_comp_π_f_zero := hom_f_zero_comp_π_f_zero_1 }) =
    (hom = hom_1)
-- Init.Data.Slice.List.Lemmas
ListSlice.mkSlice_roc_eq_mkSlice_roo : ∀ {α : Type u_1} {xs : ListSlice α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1
-- Aesop.Stats.Report
Aesop.StatsReport.default : Aesop.StatsReport
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.essentiallySmall_iff_objectPropertyEssentiallySmall_top : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.EssentiallySmall.{w, v, u} C ↔ CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} ⊤
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → Bool} {k : α}, (Std.ExtTreeMap.filter (fun k x => f k) t).getKey? k = Option.filter f (t.getKey? k)
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_coe_unitary : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] [Nontrivial E] (U : ↥(unitary E)), ‖↑U‖ = 1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_eq_zero_iff_of_le_of_nonneg_ae : ∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  a ≤ b →
    0 ≤ᵐ[μ.restrict (Set.Ioc a b)] f →
      IntervalIntegrable f μ a b → (∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Set.Ioc a b)] 0)
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.isNilpotent_of_le : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M]
  (M₁ M₂ : LieSubmodule R L M), M₁ ≤ M₂ → ∀ [LieModule.IsNilpotent L ↥M₂], LieModule.IsNilpotent L ↥M₁
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.SemaphoreState.mk.inj : ∀ {permits : ℕ} {waiters : Std.Queue (IO.Promise Unit)} {permits_1 : ℕ} {waiters_1 : Std.Queue (IO.Promise Unit)},
  { permits := permits, waiters := waiters } = { permits := permits_1, waiters := waiters_1 } →
    permits = permits_1 ∧ waiters = waiters_1
-- Mathlib.Order.LiminfLimsup
/-- See also `Filter.blimsup_or_eq_sup`.  -/
Filter.blimsup_sup_le_or : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  Filter.blimsup u f p ⊔ Filter.blimsup u f q ≤ Filter.blimsup u f fun x => p x ∨ q x
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.ParentKind.regular.sizeOf_spec : sizeOf Lean.Meta.Grind.NormalizePattern.ParentKind.regular✝ = 1
-- Lean.Language.Basic
Lean.Language.instNonemptySnapshotTask : ∀ {α : Type} [Nonempty α], Nonempty (Lean.Language.SnapshotTask α)
-- Mathlib.Analysis.Normed.Group.Basic
enorm_sub_rev : ∀ {E : Type u_8} [inst : SeminormedAddGroup E] (a b : E), ‖a - b‖ₑ = ‖b - a‖ₑ
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.Core.run_liftIOCore : ∀ {α : Type} (x : IO α) (r : Lean.Core.Context),
  ReaderT.run (Lean.Core.liftIOCore x) r =
    StateRefT'.lift
      (EIO.adapt (fun err => Lean.Exception.error r.ref (Lean.MessageData.ofFormat (Std.format (toString err)))) x)
-- Mathlib.Data.Finset.Insert
Finset.pairwise_cons' : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {a : α} (ha : a ∉ s) (r : β → β → Prop) (f : α → β),
  Pairwise (Function.onFun r fun a_1 => f ↑a_1) ↔
    Pairwise (Function.onFun r fun a => f ↑a) ∧ ∀ b ∈ s, r (f a) (f b) ∧ r (f b) (f a)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.sub_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f g : M₁ ⟶ M₂) (X : Cᵒᵖ), (f - g).app X = f.app X - g.app X
-- Mathlib.Data.Stream.Init
Stream'.head_drop : ∀ {α : Type u} (a : Stream' α) (n : ℕ), (Stream'.drop n a).head = a.get n
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_mul_span' : ∀ {R : Type u} [inst : Semiring R] (S T : Set R) [(Ideal.span S).IsTwoSided],
  Ideal.span S * Ideal.span T = Ideal.span (S * T)