mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangleMap_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂),
  (CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₁ = a
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Given `f : β → ℝ`, if `f` sends `{i | p i}` to a set of positive numbers
accumulating to zero, then closed neighborhoods of the diagonal of sizes `{f i | p i}`
form a basis of `𝓤 α`.

Currently we have only one specific basis `uniformity_basis_dist_le` based on this constructor.
More can be easily added if needed in the future.  -/
Metric.mk_uniformity_basis_le : ∀ {α : Type u} [inst : PseudoMetricSpace α] {β : Type u_3} {p : β → Prop} {f : β → ℝ},
  (∀ (x : β), p x → 0 < f x) →
    (∀ (ε : ℝ), 0 < ε → ∃ x, p x ∧ f x ≤ ε) → (uniformity α).HasBasis p fun x => {p | dist p.1 p.2 ≤ f x}
-- Mathlib.Order.RelIso.Basic
RelIso.relHomCongr_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ →r s₁),
  (e₁.relHomCongr e₂) f₁ = e₂.toRelEmbedding.toRelHom.comp (f₁.comp e₁.symm.toRelEmbedding.toRelHom)
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The forgetful functor from `Bipointed` to `Pointed` which forgets about the first point.  -/
bipointedToPointedSnd : CategoryTheory.Functor Bipointed Pointed
-- Mathlib.Analysis.Normed.Group.Basic
ne_one_of_norm_ne_zero : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E}, ‖a‖ ≠ 0 → a ≠ 1
-- Init.Data.UInt.Lemmas
UInt8.ofNatLT_uInt16ToNat : ∀ (n : UInt16) (h : n.toNat < UInt8.size), UInt8.ofNatLT n.toNat h = n.toUInt8
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.instDecidablePreconnected : {V : Type u} → (G : SimpleGraph V) → [DecidableEq V] → [Fintype V] → [DecidableRel G.Adj] → Decidable G.Preconnected
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_insert : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} [inst_2 : DecidableEq β] {b : β}, (insert b s).lcm f = lcm (f b) (s.lcm f)
-- Init.Data.Order.Ord
Std.TransOrd.compareOfLessAndEq_of_lt_trans_of_lt_iff : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : DecidableEq α],
  (∀ {a b c : α}, a < b → b < c → a < c) →
    (∀ (x y : α), x < y ↔ ¬y < x ∧ x ≠ y) → Std.TransCmp fun x y => compareOfLessAndEq x y
-- Init.Data.UInt.Lemmas
BitVec.ofNat_uInt16ToNat : ∀ (n : UInt16), BitVec.ofNat 16 n.toNat = n.toBitVec
-- Mathlib.Data.TwoPointing
TwoPointing.instNonemptyOfNontrivial : ∀ {α : Type u_1} [Nontrivial α], Nonempty (TwoPointing α)
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.mk_SpecMap : ∀ {R S : CommRingCat} {f : R ⟶ S},
  Topology.IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) →
    (CommRingCat.Hom.hom f).SurjectiveOnStalks → AlgebraicGeometry.IsPreimmersion (AlgebraicGeometry.Spec.map f)
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instSupSet : {V : Type u} → {G : SimpleGraph V} → [Finite V] → SupSet G.Finsubgraph
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.colimitLeftOpIsoUnopLimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.colimitLeftOpIsoUnopLimit F =
    CategoryTheory.Limits.colimit.isoColimitCocone
      { cocone := CategoryTheory.Limits.coconeLeftOpOfCone (CategoryTheory.Limits.limit.cone F),
        isColimit := CategoryTheory.Limits.isColimitCoconeLeftOpOfCone F (CategoryTheory.Limits.limit.isLimit F) }
-- Mathlib.NumberTheory.NumberField.CMField
/-- The complex conjugation generates the Galois group of `K/K⁺`.
 -/
NumberField.IsCMField.zpowers_complexConj_eq_top : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K], Subgroup.zpowers (NumberField.IsCMField.complexConj K) = ⊤
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalizer_empty : ∀ {G : Type u_1} [inst : Group G], Subgroup.normalizer ∅ = ⊤
-- Init.Data.List.Count
List.boole_getElem_le_countP : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {i : ℕ} (h : i < l.length),
  (if p l[i] = true then 1 else 0) ≤ List.countP p l
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Ordinal.cof_type`. -/
Ordinal.cof_type_lt : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α],
  (Ordinal.type fun x1 x2 => x1 < x2).cof = Order.cof α
-- Init.Data.BEq
BEq.trans : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {a b c : α}, (a == b) = true → (b == c) = true → (a == c) = true
-- Init.Data.Dyadic.Basic
Dyadic.zero_mul : ∀ (x : Dyadic), 0 * x = 0
-- Mathlib.Analysis.Convex.Star
StarConvex.linear_preimage : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {x : E} {s : Set F} (f : E →ₗ[𝕜] F),
  StarConvex 𝕜 (f x) s → StarConvex 𝕜 x (⇑f ⁻¹' s)
-- Mathlib.Algebra.Group.End
MonoidHom.toHomPerm_apply_apply : ∀ {α : Type u_4} {G : Type u_7} [inst : Group G] (f : G →* Function.End α) (x : G), ⇑(f.toHomPerm x) = f x
-- Init.Data.Vector.Basic
/-- Map a monadic function over a vector.  -/
Vector.mapM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → {n : ℕ} → [Monad m] → (α → m β) → Vector α n → m (Vector β n)
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_add_ofNat : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (a : R) (n : ℕ)
  [inst_4 : n.AtLeastTwo], Int.fract (a + OfNat.ofNat n) = Int.fract a
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.opComp_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (X : Cᵒᵖ),
  (F.opComp G).hom.app X = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj (F.obj (Opposite.unop X))))
-- Mathlib.Order.Antisymmetrization
Mathlib.Tactic.GCongr.AntisymmRel.left : ∀ {α : Type u_3} {a b : α} {r : α → α → Prop}, AntisymmRel r a b → r a b
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (sz : ℕ) (k' : α) (v' : β k')
  (l' r' : Std.DTreeMap.Internal.Impl α β) (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  Std.DTreeMap.Internal.Impl.insert k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr_1 =
    match compare k k' with
    | Ordering.lt =>
      match Std.DTreeMap.Internal.Impl.insert k v l' ⋯ with
      | { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balanceL k' v' d r' ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
    | Ordering.gt =>
      match Std.DTreeMap.Internal.Impl.insert k v r' ⋯ with
      | { impl := d, balanced_impl := hd, lb_le_size_impl := hd₁, size_impl_le_ub := hd₂ } =>
        { impl := Std.DTreeMap.Internal.Impl.balanceR k' v' l' d ⋯ ⋯ ⋯, balanced_impl := ⋯, lb_le_size_impl := ⋯,
          size_impl_le_ub := ⋯ }
    | Ordering.eq =>
      { impl := Std.DTreeMap.Internal.Impl.inner sz k v l' r', balanced_impl := ⋯, lb_le_size_impl := ⋯,
        size_impl_le_ub := ⋯ }
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.coe_trans : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃}, ↑(e₁₂.trans e₂₃) = ↑e₂₃ ∘ₛₗ ↑e₁₂
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Translating the argument as a continuous linear map on Schwartz space.  -/
SchwartzMap.compSubConstCLM : (𝕜 : Type u_2) →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              [inst_4 : RCLike 𝕜] → [inst_5 : NormedSpace 𝕜 F] → E → SchwartzMap E F →L[𝕜] SchwartzMap E F
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₁_quotientGroupMk'_epi : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (S : Subgroup G) [inst_2 : S.Normal]
  [inst_3 : Representation.IsTrivial (MonoidHom.comp A.ρ S.subtype)],
  CategoryTheory.Epi (groupHomology.mapCycles₁ (QuotientGroup.mk' S) (A.resOfQuotientIso S).inv)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- Refining each component of a `0`-hypercover yields a refined `0`-hypercover of the base.  -/
CategoryTheory.Precoverage.ZeroHypercover.bind : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {T : C} →
        [J.IsStableUnderComposition] →
          (E : J.ZeroHypercover T) → ((i : E.I₀) → J.ZeroHypercover (E.X i)) → J.ZeroHypercover T
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.ZNum.zNeg.match_1.eq_2 : ∀ (motive : ZNum → Sort u_1) (a : PosNum) (h_1 : Unit → motive ZNum.zero) (h_2 : (a : PosNum) → motive (ZNum.pos a))
  (h_3 : (a : PosNum) → motive (ZNum.neg a)),
  (match ZNum.pos a with
    | ZNum.zero => h_1 ()
    | ZNum.pos a => h_2 a
    | ZNum.neg a => h_3 a) =
    h_2 a
-- Init.Core
/-- If the right type in a sum is inhabited then the sum is inhabited.

This is not an instance to avoid non-canonical instances when both the left and right types are
inhabited.
 -/
PSum.inhabitedRight : {α : Sort u_1} → {β : Sort u_2} → [Inhabited β] → Inhabited (α ⊕' β)
-- Mathlib.Topology.PartitionOfUnity
PartitionOfUnity.mk.sizeOf_spec : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ} [inst_1 : SizeOf ι]
  [inst_2 : SizeOf X] [inst_3 : (a : X) → SizeOf (s a)] (toFun : ι → C(X, ℝ))
  (locallyFinite' : LocallyFinite fun i => Function.support ⇑(toFun i)) (nonneg' : 0 ≤ toFun)
  (sum_eq_one' : ∀ x ∈ s, ∑ᶠ (i : ι), (toFun i) x = 1) (sum_le_one' : ∀ (x : X), ∑ᶠ (i : ι), (toFun i) x ≤ 1),
  sizeOf
      { toFun := toFun, locallyFinite' := locallyFinite', nonneg' := nonneg', sum_eq_one' := sum_eq_one',
        sum_le_one' := sum_le_one' } =
    1
-- Mathlib.Analysis.Calculus.FDeriv.Pi
hasFDerivAt_single : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type u_3}
  [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {i : ι} (y : E i),
  HasFDerivAt (Pi.single i) (ContinuousLinearMap.pi (Pi.single i (ContinuousLinearMap.id 𝕜 (E i)))) y
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_toNatTrans_app : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] {a b : CategoryTheory.Cat} {f g : a ⟶ b} (x : f ⟶ g)
  (x_1 : CategoryTheory.Join (↑a) D),
  ((CategoryTheory.Join.pseudofunctorLeft D).map₂ x).toNatTrans.app x_1 =
    match x_1 with
    | CategoryTheory.Join.left x_2 => (CategoryTheory.Join.inclLeft (↑b) D).map (x.toNatTrans.app x_2)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_iff_tendsto_subseq_of_monotone : ∀ {ι₁ : Type u_3} {ι₂ : Type u_4} {α : Type u_5} [inst : SemilatticeSup ι₁] [inst_1 : Preorder ι₂] [Nonempty ι₁]
  [inst_3 : TopologicalSpace α] [inst_4 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [NoMaxOrder α]
  {f : ι₂ → α} {φ : ι₁ → ι₂} {l : α},
  Monotone f →
    Filter.Tendsto φ Filter.atTop Filter.atTop →
      (Filter.Tendsto f Filter.atTop (nhds l) ↔ Filter.Tendsto (f ∘ φ) Filter.atTop (nhds l))
-- Mathlib.Order.Hom.Bounded
BotHom.instLE : {α : Type u_2} → {β : Type u_3} → [inst : Bot α] → [LE β] → [inst_2 : Bot β] → LE (BotHom α β)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Ici_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ioo a b ⊆ Finset.Ici a
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorHomMk'_app_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} {mor₁ : obj₁ ⟶ obj₂}
  {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (hom₁ : obj₁ ⟶ obj₁') (hom₂ : obj₂ ⟶ obj₂')
  (hom₃ : obj₃ ⟶ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp hom₃ mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorHomMk' hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₃ = hom₃.app j
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_periodic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), Function.Periodic (toIocMod hp a) p
-- Mathlib.Algebra.Group.Action.Defs
/-- Let `Q / P / N / M` be a tower. If `P / N / M`, `Q / N / M` and `Q / P / M` are
scalar towers, then `Q / P / N` is also a scalar tower.
 -/
IsScalarTower.to₂₃₄ : ∀ (M : Type u_9) (N : Type u_10) (P : Type u_11) (Q : Type u_12) [inst : SMul M N] [inst_1 : SMul M P]
  [inst_2 : SMul M Q] [inst_3 : SMul P Q] [inst_4 : Monoid N] [inst_5 : MulAction N P] [inst_6 : MulAction N Q]
  [IsScalarTower M N P] [IsScalarTower M N Q] [IsScalarTower M P Q],
  (Function.Surjective fun m => m • 1) → IsScalarTower N P Q
-- Mathlib.Algebra.Ring.Pi
/-- `Function.const` as a `RingHom`.  -/
Pi.constRingHom : (α : Type u_1) → (β : Type u_2) → [inst : NonAssocSemiring β] → β →+* α → β
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.δ₀Iter_σ_assoc : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (hi : autoParam (n + (i + 1) = m + 1) SimplexCategory.δ₀Iter_σ._auto_1),
  autoParam (↑j ≤ i) SimplexCategory.δ₀Iter_σ._auto_3 →
    ∀ {Z : SimplexCategory} (h : { len := m } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter (i + 1) hi)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.δ₀Iter i ⋯) h
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_le_size_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)}, m.size ≤ (Std.ExtDHashMap.Const.insertMany m l).size
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.prodEquiv.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] (X₁ X₂ : C)
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct X₁ X₂]
  [inst_4 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X₁ X₂) (CategoryTheory.forget C)],
  CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂ = CategoryTheory.Limits.Concrete.prodEquiv X₁ X₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insert_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF),
  t.isEmpty = false →
    ∀ {k : α} {v : β k} {fallback : α},
      (compare ((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_of_norm_sub_le : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f₀ f₁ : α → β} {g : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f₁ μ →
    MeasureTheory.Integrable f₀ μ →
      MeasureTheory.Integrable g μ → (∀ᵐ (a : α) ∂μ, ‖f₀ a - f₁ a‖ ≤ g a) → MeasureTheory.Integrable f₁ μ
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyLemma.mk.inj : ∀ {name name_1 : Mathlib.Tactic.ClickSuggestions.Premise}, { name := name } = { name := name_1 } → name = name_1
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lTensor_mul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (f₁ f₂ : N →ₗ[R] N),
  (TensorProduct.AlgebraTensorModule.lTensor A M) (f₁ * f₂) =
    (TensorProduct.AlgebraTensorModule.lTensor A M) f₁ * (TensorProduct.AlgebraTensorModule.lTensor A M) f₂
-- Mathlib.Logic.Nontrivial.Defs
Function.nontrivial_of_nontrivial : ∀ (α : Type u_3) (β : Type u_4) [Nontrivial (α → β)], Nontrivial β
-- Mathlib.Combinatorics.Colex
/-- The equivalence between `ℕ` and `Finset ℕ` that maps `∑ i ∈ s, 2^i` to `s`.  -/
Finset.equivBitIndices : ℕ ≃ Finset ℕ
-- Mathlib.Topology.Order.Compact
/-- The **extreme value theorem**: if a continuous function `f` is smaller than a value in its range
away from compact sets, then it has a global maximum.  -/
Continuous.exists_forall_ge' : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] {f : β → α},
  Continuous f → ∀ (x₀ : β), (∀ᶠ (x : β) in Filter.cocompact β, f x ≤ f x₀) → ∃ x, ∀ (y : β), f y ≤ f x
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.powFn? : Lean.Meta.Sym.Arith.Semiring → Option Lean.Expr
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- This is the scheme `Proj(A)` for any `ℕ`-graded ring `A`.
 -/
AlgebraicGeometry.Proj : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] → [inst_2 : AddSubgroupClass σ A] → (𝒜 : ℕ → σ) → [GradedRing 𝒜] → AlgebraicGeometry.Scheme
-- Init.Data.Int.Order
Int.min_add_right : ∀ (a b c : ℤ), min (a + c) (b + c) = min a b + c
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The canonical map from a component to the direct limit.  -/
DirectLimit.Module.of : (R : Type u_1) →
  (ι : Type u_2) →
    [inst : Preorder ι] →
      (G : ι → Type u_3) →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : Semiring R] →
                    [inst_5 : (i : ι) → AddCommMonoid (G i)] →
                      [inst_6 : (i : ι) → Module R (G i)] →
                        [inst_7 : ∀ (i j : ι) (h : i ≤ j), LinearMapClass (T h) R (G i) (G j)] →
                          [inst_8 : Nonempty ι] → (i : ι) → G i →ₗ[R] DirectLimit G f
-- Mathlib.Algebra.Order.Group.PosPart
posPart_sub_negPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] [AddLeftMono α] (a : α), a⁺ - a⁻ = a
-- Mathlib.RingTheory.Ideal.Maps
RingHom.liftOfSurjective_comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Ring A] [inst_1 : Ring B] [inst_2 : Ring C] (f : A →+* B)
  (hf : Function.Surjective ⇑f) (g : { g // RingHom.ker f ≤ RingHom.ker g }), ((f.liftOfSurjective hf) g).comp f = ↑g
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasurableEmbedding.aestronglyMeasurable_map_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {γ : Type u_5} {mγ : MeasurableSpace γ}
  {mα : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ},
  MeasurableEmbedding f →
    ∀ {g : α → β},
      MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) ↔
        MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_Icc : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], (Finset.Icc a b).Nonempty ↔ a ≤ b
-- Mathlib.MeasureTheory.Order.Lattice
/-- We say that a type has `MeasurableSup₂` if `uncurry (· ⊔ ·)` is a measurable functions.
For a typeclass assuming measurability of `(c ⊔ ·)` and `(· ⊔ c)` see `MeasurableSup`.  -/
MeasurableSup₂ : (M : Type u_1) → [MeasurableSpace M] → [Max M] → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGet_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α} {hk : k ∈ t₁} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂),
  Std.DTreeMap.Raw.Const.get t₁ k hk = Std.DTreeMap.Raw.Const.get t₂ k ⋯
-- Mathlib.GroupTheory.Subgroup.Simple
IsSimpleGroup.toNontrivial : ∀ {G : Type u_1} {inst : Group G} [self : IsSimpleGroup G], Nontrivial G
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- The units of the stalk at `x` of the sheaf of smooth functions from `M` to `𝕜`, considered as a
sheaf of commutative rings, are the functions whose values at `x` are nonzero.  -/
smoothSheafCommRing.isUnit_stalk_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] {x : M}
  (f : ↑((smoothSheafCommRing IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜).presheaf.stalk x)),
  IsUnit f ↔ f ∉ RingHom.ker (smoothSheafCommRing.eval IM (modelWithCornersSelf 𝕜 𝕜) M 𝕜 x)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.Adj.fst_mem : ∀ {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {u v : V}, H.Adj u v → u ∈ H.verts
-- Lean.Compiler.IR.CompilerM
Lean.IR.findDecl : Lean.Name → Lean.IR.CompilerM (Option Lean.IR.Decl)
-- Init.Data.Int.Gcd
Int.lcm_eq_zero_iff : ∀ {m n : ℤ}, m.lcm n = 0 ↔ m = 0 ∨ n = 0