mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
CategoryTheory.Functor.IsPreFibered.mk : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮}, (∀ {a : 𝒳} {R : 𝒮} (f : R ⟶ p.obj a), ∃ b φ, p.IsCartesian f φ) → p.IsPreFibered
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getKeyDₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (a fallback : α), m.getKeyDₘ a fallback = (m.getKey?ₘ a).getD fallback
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
/-- When `X` satisfies `IsStrictSegal`, `X` is 2-coskeletal.  -/
SSet.StrictSegal.isCoskeletal' : ∀ {X : SSet} [X.IsStrictSegal], CategoryTheory.SimplicialObject.IsCoskeletal X 2
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a seminormed group from a multiplication-invariant pseudodistance.  -/
SeminormedCommGroup.ofMulDist : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : CommGroup E] →
      [inst_2 : PseudoMetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)) → SeminormedCommGroup E
-- Init.Data.String.Substring
/-- Splits a substring `s` on occurrences of the separator string `sep`. The default separator is `" "`.

When `sep` is empty, the result is `[s]`. When `sep` occurs in overlapping patterns, the first match
is taken. There will always be exactly `n+1` elements in the returned list if there were `n`
non-overlapping matches of `sep` in the string. The separators are not included in the returned
substrings, which are all substrings of `s`'s string.
 -/
Substring.Raw.splitOn : Substring.Raw → optParam String " " → List Substring.Raw
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inr_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inr X Y)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- The submonoid generated by an element of a monoid equals the set of natural number powers of
the element.  -/
Submonoid.mem_closure_singleton : ∀ {M : Type u_1} [inst : Monoid M] {x y : M}, y ∈ Submonoid.closure {x} ↔ ∃ n, x ^ n = y
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.subAt_append : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)) (x y : List A),
  Descriptive.Tree.subAt (Descriptive.Tree.subAt T x) y = Descriptive.Tree.subAt T (x ++ y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_pt : ∀ {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₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))]
  (h : CategoryTheory.Limits.IsTerminal Y₃),
  (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).pt = (G.obj (Opposite.op X₁)).obj X₃
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₁_ext_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G}
  {f₁ f₂ : ↥(groupCohomology.cocycles₁ A)}, f₁ = f₂ ↔ ∀ (g : G), f₁ g = f₂ g
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
intEquivOfZMultiplesEqTop.congr_simp : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : AddGroup G] (g g_1 : G) (e_g : g = g_1)
  (hg : AddSubgroup.zmultiples g = ⊤), intEquivOfZMultiplesEqTop g hg = intEquivOfZMultiplesEqTop g_1 ⋯
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedNotification : {a : Type u_1} → [Inhabited a] → Inhabited (Lean.JsonRpc.Notification a)
-- Batteries.Data.Fin.Fold
Fin.dfoldr_succ_last : ∀ {n : ℕ} {α : Fin (n + 2) → Type u_1} (f : (i : Fin (n + 1)) → α i.succ → α i.castSucc) (x : α (Fin.last (n + 1))),
  Fin.dfoldr (n + 1) α f x = Fin.dfoldr n (α ∘ Fin.castSucc) (fun x => f x.castSucc) (f (Fin.last n) x)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set β} {a : α}, s.Nonempty → (a +ᵥ s).Nonempty
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- `f ''ᵁ U` is notation for the image (as an open set) of `U` under an open immersion `f`.
The preferred name in lemmas is `image` and it should be treated as an infix.  -/
AlgebraicGeometry.«term_''ᵁ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.ker_eq_bot : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N), f.ker = ⊥ ↔ Function.Injective ⇑f
-- Mathlib.Condensed.Discrete.Characterization
LightCondSet.isDiscrete_tfae : ∀ (X : LightCondSet),
  [LightCondensed.IsDiscrete X, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X),
      (LightCondensed.discrete (Type u)).essImage X, LightCondSet.LocallyConstant.functor.essImage X,
      CategoryTheory.IsIso (LightCondSet.LocallyConstant.adjunction.counit.app X),
      ∀ (S : LightProfinite),
        Nonempty
          (CategoryTheory.Limits.IsColimit
            (X.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOpEquiv_functor_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : (CategoryTheory.Limits.Cone F)ᵒᵖ),
  CategoryTheory.Limits.coneOpEquiv.functor.obj c = (Opposite.unop c).op
-- Mathlib.Data.ENNReal.Basic
ENNReal.some_eq_coe' : ∀ (a : NNReal), ↑a = ↑a
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A `Submonoid` is either the trivial `Submonoid` or nontrivial.  -/
Submonoid.bot_or_nontrivial : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), S = ⊥ ∨ Nontrivial ↥S
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (A : CategoryTheory.Functor Cᵒᵖ (Type v))
  {X Y : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (g : X ⟶ Y),
  (CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver A).map g =
    CategoryTheory.CostructuredArrow.homMk (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ g) ⋯
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instWeakEquivalenceLeftOfOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] {X Y : CategoryTheory.Over S} (f : X ⟶ Y)
  [HomotopicalAlgebra.WeakEquivalence f], HomotopicalAlgebra.WeakEquivalence (CategoryTheory.Over.Hom.left f)
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The embedding of `FunSpace` into the space of continuous maps  -/
ODE.FunSpace.toContinuousMap : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {tmin tmax : ℝ} →
      {t₀ : ↑(Set.Icc tmin tmax)} → {x₀ : E} → {r L : NNReal} → ODE.FunSpace t₀ x₀ r L ↪ C(↑(Set.Icc tmin tmax), E)
-- Mathlib.Order.SuccPred.Limit
Order.not_isPredPrelimit_pred : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] [NoMinOrder α] (a : α), ¬Order.IsPredPrelimit (Order.pred a)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.reflectionPerm_inv : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  (P.reflectionPerm i)⁻¹ = P.reflectionPerm i
-- Lean.Meta.Tactic.Generalize
Lean.Meta.GeneralizeArg.mk.sizeOf_spec : ∀ (expr : Lean.Expr) (xName? hName? : Option Lean.Name),
  sizeOf { expr := expr, xName? := xName?, hName? := hName? } = 1 + sizeOf expr + sizeOf xName? + sizeOf hName?
-- Init.Data.BitVec.Bootstrap
BitVec.eq_of_getLsbD_eq : ∀ {w : ℕ} {x y : BitVec w}, (∀ i < w, x.getLsbD i = y.getLsbD i) → x = y
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- The non-Archimedean subgroup basis lemmas cannot be instances because some instances
(such as `MeasureTheory.AEEqFun.instAddMonoid` or `IsTopologicalAddGroup.toContinuousAdd`)
cause the search for `@IsTopologicalAddGroup β ?m1 ?m2`, i.e. a search for a topological group where
the topology/group structure are unknown.  -/
LibraryNote.«non-Archimedean_non-instances» : Batteries.Util.LibraryNote
-- Mathlib.Analysis.Convex.Integral
ConcaveOn.average_mem_hypograph : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} {g : E → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  [NeZero μ],
  ConcaveOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        (∀ᵐ (x : α) ∂μ, f x ∈ s) →
          MeasureTheory.Integrable f μ →
            MeasureTheory.Integrable (g ∘ f) μ →
              (⨍ (x : α), f x ∂μ, ⨍ (x : α), g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getInt32Value? : Lean.Expr → OptionT Id Int32
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sieve₁'_eq_sieve₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) (i₁ i₂ : E.I₀)
  [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)],
  E.sieve₁' i₁ i₂ =
    E.sieve₁ (CategoryTheory.Limits.pullback.fst (E.f i₁) (E.f i₂))
      (CategoryTheory.Limits.pullback.snd (E.f i₁) (E.f i₂))
-- Mathlib.Algebra.AddConstMap.Basic
/-- An `AddConstMap` satisfies `f (x + a) = f x + b`. Use `map_add_const` instead.  -/
AddConstMap.map_add_const' : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (self : AddConstMap G H a b) (x : G),
  self.toFun (x + a) = self.toFun x + b
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.not_mem_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → k ∉ t₁ \ t₂
-- Mathlib.Data.Set.Subset
Set.image_val_sdiff : ∀ {α : Type u_2} {A : Set α} {D E : Set ↑A}, Subtype.val '' (D \ E) = Subtype.val '' D \ Subtype.val '' E
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- Half of **Jordan's inequality** for absolute values.  -/
Real.mul_abs_le_abs_sin : ∀ {x : ℝ}, |x| ≤ Real.pi / 2 → 2 / Real.pi * |x| ≤ |Real.sin x|
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instCompleteLattice : {α : Type u_2} → [inst : TopologicalSpace α] → CompleteLattice (TopologicalSpace.Opens α)
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumLeft.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₁ : Type v₁}
  [inst_3 : DecidableEq ι₁] (M₁ : ι₁ → Type w₁) (M₂' : Type w₂') [inst_4 : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)]
  [inst_5 : AddCommMonoid M₂'] [inst_6 : (i₁ : ι₁) → Module R (M₁ i₁)] [inst_7 : Module R M₂']
  [inst_8 : (i₁ : ι₁) → Module S (M₁ i₁)] [inst_9 : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)],
  TensorProduct.directSumLeft R S M₁ M₂' =
    (TensorProduct.AlgebraTensorModule.congr 1 (DirectSum.lid R M₂' PUnit.{1}).symm ≪≫ₗ
        TensorProduct.directSum R S M₁ fun x => M₂') ≪≫ₗ
      DirectSum.lequivCongrLeft S (Equiv.prodUnique ι₁ Unit)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- A finite sum of functions monotone on `u` is monotone on `u`.  -/
MonotoneOn.finsetSum : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {s : Finset ι} [AddLeftMono N]
  {γ : Type u_9} [inst_3 : Preorder γ] {u : Set γ} {f : ι → γ → N},
  (∀ i ∈ s, MonotoneOn (f i) u) → MonotoneOn (fun x => ∑ i ∈ s, f i x) u
-- Mathlib.Order.SuccPred.Basic
Order.pred_ne_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : OrderTop α] [Nontrivial α] (a : α),
  Order.pred a ≠ ⊤
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.isUniformInducing_coeFn : ∀ {𝕜₁ : 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 : UniformSpace F] [inst_8 : IsUniformAddGroup F]
  (𝔖 : Set (Set E)), IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ DFunLike.coe)
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.instFromJsonCancelParams : Lean.FromJson Lean.Lsp.CancelParams
-- Mathlib.Analysis.Calculus.FDeriv.Pow
hasStrictFDerivAt_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] (n : ℕ) {x : 𝔸},
  HasStrictFDerivAt (fun x => x ^ n) ((n • x ^ (n - 1)) • ContinuousLinearMap.id 𝕜 𝔸) x
-- Mathlib.Data.Fintype.EquivFin
Fintype.finite : ∀ {α : Type u_4} (_inst : Fintype α), Finite α
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegrable_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, CurveIntegrable ω γ.symm ↔ CurveIntegrable ω γ
-- Mathlib.Analysis.Convex.Exposed
IsExposed.inter : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] [IsOrderedRing 𝕜] [ContinuousAdd 𝕜]
  {A B C : Set E}, IsExposed 𝕜 A B → IsExposed 𝕜 A C → IsExposed 𝕜 A (B ∩ C)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- This lemma is superseded by `MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le`
which does not require measurability.  -/
MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le_of_meas : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α → β},
  MeasureTheory.MemLp f 1 μ →
    MeasureTheory.StronglyMeasurable f →
      ∀ {ε : ℝ}, 0 < ε → ∃ M, 0 ≤ M ∧ ∫⁻ (x : α), ‖{x | M ≤ ↑‖f x‖₊}.indicator f x‖ₑ ∂μ ≤ ENNReal.ofReal ε
-- Mathlib.Data.Nat.Cast.Order.Basic
Nat.ofNat_lt : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α]
  {m n : ℕ} [inst_5 : n.AtLeastTwo] [inst_6 : m.AtLeastTwo],
  OfNat.ofNat m < OfNat.ofNat n ↔ OfNat.ofNat m < OfNat.ofNat n
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.condIndep : ∀ {Ω : Type u_1} {m' m₁ m₂ mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {p1 p2 : Set (Set Ω)},
  m₁ ≤ mΩ →
    m₂ ≤ mΩ →
      IsPiSystem p1 →
        IsPiSystem p2 →
          m₁ = MeasurableSpace.generateFrom p1 →
            m₂ = MeasurableSpace.generateFrom p2 →
              ProbabilityTheory.CondIndepSets m' hm' p1 p2 μ → ProbabilityTheory.CondIndep m' m₁ m₂ hm' μ
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.decidableMemCenter : {M : Type u_1} →
  [inst : AddMonoid M] → (a : M) → [Decidable (∀ (b : M), b + a = a + b)] → Decidable (a ∈ AddSubmonoid.center M)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Projection to `ContinuousMultilinearMap`s.  -/
ContinuousAlternatingMap.toContinuousMultilinearMap : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] → M [⋀^ι]→L[R] N → ContinuousMultilinearMap R (fun x => M) N
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty_inter_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.Data.List.Sigma
List.kreplace_self : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)},
  l.NodupKeys → ⟨a, b⟩ ∈ l → List.kreplace a b l = l
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eq_const_cons : ∀ {R : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M] {r : R} (m : M)
  {n : M} {l : Mathlib.Tactic.Module.NF R M}, 0 = r → n = l.eval → n = ((r, m) ::ᵣ l).eval
-- Mathlib.FieldTheory.NormalizedTrace
_private.Mathlib.FieldTheory.NormalizedTrace.0.Algebra.normalizedTrace_trans_apply_aux : ∀ (F : Type u_3) (E : Type u_4) (K : Type u_5) [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra E K] [inst_5 : Algebra F K] [IsScalarTower F E K]
  [inst_7 : Algebra.IsIntegral F E] [inst_8 : Algebra.IsIntegral F K] [inst_9 : CharZero F] [FiniteDimensional F E]
  [inst_11 : Algebra.IsIntegral E K] [inst_12 : CharZero E] (a : K),
  (Algebra.normalizedTrace F E) ((Algebra.normalizedTrace E K) a) = (Algebra.normalizedTrace F K) a
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.ι_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.ι f g)
      (CategoryTheory.kernelCokernelCompSequence.φ f g) =
    0
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.isoOfEq.congr_simp : ∀ (X : AlgebraicGeometry.Scheme) {U V : X.Opens} (e : U = V), X.isoOfEq e = X.isoOfEq e
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.forkOfIsColimit_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {S : C} (E : CategoryTheory.PreOneHypercover S) {c : CategoryTheory.Limits.Cofan E.X}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan E.Y'}
  (hd : CategoryTheory.Limits.IsColimit d) (F : CategoryTheory.Functor Cᵒᵖ A),
  (E.forkOfIsColimit hc hd F).pt = F.obj (Opposite.op S)
-- Mathlib.Order.Fin.Basic
/-- `Fin.natAdd` as an `OrderEmbedding`.

`natAddOrderEmb n i` adds `n` to `i` "on the left".  -/
Fin.natAddOrderEmb : {m : ℕ} → (n : ℕ) → Fin m ↪o Fin (n + m)
-- Mathlib.Probability.Independence.Integration
ProbabilityTheory.IndepFun.integral_fun_mul_eq_mul_integral : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → 𝕜},
  ProbabilityTheory.IndepFun X Y μ →
    MeasureTheory.AEStronglyMeasurable X μ →
      MeasureTheory.AEStronglyMeasurable Y μ → ∫ (ω : Ω), X ω * Y ω ∂μ = (∫ (x : Ω), X x ∂μ) * ∫ (x : Ω), Y x ∂μ
-- Mathlib.Analysis.Normed.Group.CocompactMap
CocompactMapClass.norm_le : ∀ {E : Type u_2} {F : Type u_3} {𝓕 : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : 𝓕}
  [ProperSpace F] [inst_3 : FunLike 𝓕 E F] [CocompactMapClass 𝓕 E F] (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.partialMatch_zero : ∀ {pat s : ByteArray} {stackPos : ℕ},
  stackPos ≤ s.size → String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s 0 stackPos
-- Init.System.IOError
/-- The operation failed because a file already exists.

This corresponds to POSIX errors `EEXIST`, `EINPROGRESS`, and `EISCONN`.
 -/
IO.Error.alreadyExists : Option String → UInt32 → String → IO.Error
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.CosimplicialObject.σ_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X' X : CategoryTheory.CosimplicialObject C} (f : X ⟶ X')
  {n : ℕ} (i : Fin (n + 1)),
  CategoryTheory.CategoryStruct.comp (X.σ i) (f.app { len := n }) =
    CategoryTheory.CategoryStruct.comp (f.app { len := n + 1 }) (X'.σ i)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_mono : ∀ {α : Type u_1} [inst : MeasurableSpace α], Monotone MeasureTheory.OuterMeasure.trim
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.End_toSemigroup_toMul_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A] (φ₁ φ₂ : A →ₐc[R] A), φ₁ * φ₂ = φ₁.comp φ₂
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_natCast_ite : ∀ {R : Type u_1} {m n : ℕ} [inst : Semiring R] [MulSemiringAction (Multiplicative ℕ) R],
  (↑m).coeff n = ↑(if n = 0 then m else 0)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_lt_self_iff`. -/
sub_lt_self : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] (a : α) {b : α}, 0 < b → a - b < a
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_injective : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι),
  Function.Injective (RestrictedProduct.mulSingle A i)
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.eventually_atTop_prod_self' : ∀ {α : Type u_3} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {p : α × α → Prop},
  (∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ a, ∀ k ≥ a, ∀ l ≥ a, p (k, l)
-- Mathlib.Data.Set.Card
Set.ncard_union_lt : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.ncard_union_lt._auto_1 →
    autoParam t.Finite Set.ncard_union_lt._auto_3 → ¬Disjoint s t → (s ∪ t).ncard < s.ncard + t.ncard
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.pairwise_sub_notMem_range' : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : AddCommGroup G] [inst_1 : LinearOrder S]
  [inst_2 : InvolutiveNeg ι] [inst_3 : AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G),
  (∀ (i : ι), v (-i) = -v i) →
    ∀ (f : G →+ S),
      (∀ (i : ι), f (v i) ≠ 0) →
        ∀ s ⊆ {j | IsAddIndecomposable v {i | 0 < f (v i)} j}, s.Pairwise fun i j => v i - v j ∉ Set.range v
-- Init.Data.List.Basic
List.Sublist.cons₂ : ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁.Sublist l₂ → (a :: l₁).Sublist (a :: l₂)
-- Mathlib.Data.Vector.Defs
/-- A vector of length `0` is a `nil` vector.  -/
List.Vector.eq_nil : ∀ {α : Type u_1} (v : List.Vector α 0), v = List.Vector.nil
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_le_op_iff : ∀ {M : Type u_2} [inst : Add M] {S₁ S₂ : AddSubsemigroup M}, S₁.op ≤ S₂.op ↔ S₁ ≤ S₂
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.move.eq_2 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (a : Γ) (L R : Turing.ListBlank Γ),
  Turing.Tape.move Turing.Dir.right { head := a, left := L, right := R } =
    { head := R.head, left := Turing.ListBlank.cons a L, right := R.tail }
-- Mathlib.FieldTheory.IsSepClosed
IsSepClosure.separable : ∀ {k : Type u} {inst : Field k} {K : Type v} {inst_1 : Field K} {inst_2 : Algebra k K} [self : IsSepClosure k K],
  Algebra.IsSeparable k K
-- Init.Data.List.Basic
List.Pairwise.below.cons : ∀ {α : Type u} {R : α → α → Prop} {motive : (a : List α) → List.Pairwise R a → Prop} {a : α} {l : List α}
  (a_1 : ∀ a' ∈ l, R a a') (a_2 : List.Pairwise R l), List.Pairwise.below a_2 → motive l a_2 → List.Pairwise.below ⋯