mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.ofBraided_η_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  (CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Center.ofBraided C)).f =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Center.ofBraided C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).fst
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
SimpleGraph.triangleRemovalBound_pos : ∀ {ε : ℝ}, 0 < ε → 0 < SimpleGraph.triangleRemovalBound ε
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.instFintypeElemFinset : (α : Type u_1) → (n : ℕ) → [Fintype α] → Fintype ↑(Set.powersetCard α n)
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.summable_iff_summable_coeff : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_3}
  {f : ι → MvPowerSeries σ R}, Summable f ↔ ∀ (d : σ →₀ ℕ), Summable fun i => (MvPowerSeries.coeff d) (f i)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
CategoryTheory.Bicategory.OplaxTrans.ComonadBicat.mkOfComonad_counit : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a : B} (t : a ⟶ a) [inst_1 : CategoryTheory.Bicategory.Comonad t],
  CategoryTheory.Bicategory.Comonad.counit = CategoryTheory.Bicategory.Comonad.counit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} {fallback : β k} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.getD k fallback = (Option.filter (f k) (t.get? k)).getD fallback
-- Mathlib.Topology.UniformSpace.Basic
mem_uniformity_of_uniformContinuous_invariant : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : SetRel β β} {f : α → α → β},
  (UniformContinuous fun p => f p.1 p.2) →
    s ∈ uniformity β → ∃ u ∈ uniformity α, ∀ (a b c : α), (a, b) ∈ u → (f a c, f b c) ∈ s
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.mk.sizeOf_spec : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {X : C} {data : F.OneHypercoverDenseData J₀ J X} {X₀ : C₀}
  {f : F.obj X₀ ⟶ X} {Y₀ : C₀} {g : Y₀ ⟶ X₀} [inst_2 : SizeOf C₀] [inst_3 : SizeOf C] (i₀ : data.I₀)
  (q : F.obj Y₀ ⟶ F.obj (data.X i₀))
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp q (data.f i₀) = CategoryTheory.CategoryStruct.comp (F.map g) f)
      CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac._autoParam),
  sizeOf { i₀ := i₀, q := q, fac := fac } = 1 + sizeOf i₀ + sizeOf q + sizeOf fac
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.IsCycle.existsUnique_cycle : ∀ {α : Type u_1} [Finite α] [inst : DecidableEq α] {f : Equiv.Perm α},
  f.IsCycle → ∃! s, ∃ (h : s.Nodup), s.formPerm h = f
-- Mathlib.Algebra.Homology.Homotopy
/-- Homotopy to zero for maps constructed with `nullHomotopicMap'`  -/
Homotopy.nullHomotopy' : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            (h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)) → Homotopy (Homotopy.nullHomotopicMap' h) 0
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.mulVec_injective_of_det_ne_zero : ∀ {m : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Fintype m] [inst_2 : DecidableEq m] {M : Matrix m m R}
  [NoZeroDivisors R], M.det ≠ 0 → Function.Injective M.mulVec
-- Mathlib.Algebra.Algebra.Hom
/-- Ring homomorphisms are the same as `ℕ`-algebra homomorphisms.  -/
RingHom.equivNatAlgHom : (R : Type u_1) → (S : Type u_2) → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) ≃ (R →ₐ[ℕ] S)
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- Partial homeomorphisms, defined on subsets of the space  -/
PartialHomeomorph : (X : Type u_7) → (Y : Type u_8) → [TopologicalSpace X] → [TopologicalSpace Y] → Type (max u_7 u_8)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddHom.map_srange : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : Add P] (g : N →ₙ+ P)
  (f : M →ₙ+ N), AddSubsemigroup.map g f.srange = (g.comp f).srange
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
/-- Note: this assumes `[IsLeftUniformGroup β] [IsRightUniformGroup β]` instead of the more typical
(and equivalent) `[IsUniformGroup β]` because this is used in the proof of said equivalence.  -/
tendsto_conj_nhds_one : ∀ {β : Type u_2} [inst : UniformSpace β] [inst_1 : Group β] [IsLeftUniformGroup β] [IsRightUniformGroup β],
  Filter.Tendsto (fun gx => gx.1 * gx.2 * gx.1⁻¹) (Filter.comap Prod.snd (nhds 1)) (nhds 1)
-- Init.Data.Vector.Basic
/-- Maps elements of a vector using the function `f`, which also receives the index of the element.  -/
Vector.mapIdx : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → (ℕ → α → β) → Vector α n → Vector β n
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.subtype_toEquiv_inclusion : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N} (h : f ≤ g),
  g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (FirstOrder.Language.Substructure.inclusion ⋯)) =
    f.cod.subtype.comp f.toEquiv.toEmbedding
-- Aesop.Tree.State
Aesop.Goal.isIrrelevantNoCache : Aesop.Goal → BaseIO Bool
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc_g : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq' pq'' : κ) (i₀' i₀ i₁ i₂ i₃ : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯)
  (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc X data r r' hrr' hr pq' pq'' i₀' i₀ i₁ i₂ i₃
        hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' hn₁ hn₂).g =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD X data r pq' pq'' ⋯
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.counit_comp_dFinsuppCoeFnLinearMap : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : n → Type u_3}
  [inst_3 : (i : n) → AddCommMonoid (A i)] [inst_4 : (i : n) → Module R (A i)]
  [inst_5 : (i : n) → CoalgebraStruct R (A i)],
  CoalgebraStruct.counit ∘ₗ DFinsupp.coeFnLinearMap R = CoalgebraStruct.counit
-- Mathlib.Computability.NFA
NFA.stepSet_singleton : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (s : σ) (a : α), M.stepSet {s} a = M.step s a
-- Mathlib.Order.Filter.AtTopBot.Field
/-- The function `fun x ↦ f x * r` tends to infinity along a nontrivial filter
if and only if `r > 0` and `f` tends to infinity or `r < 0` and `f` tends to negative infinity.  -/
Filter.tendsto_mul_const_atTop_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto (fun x => f x * r) l Filter.atTop ↔
    0 < r ∧ Filter.Tendsto f l Filter.atTop ∨ r < 0 ∧ Filter.Tendsto f l Filter.atBot
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.one_vle_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] {x : R}, 1 ≤ᵥ x ↔ 1 ≤ v x
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- The hom-set equivalence exhibiting the adjunction.  -/
ProfiniteGrp.ProfiniteCompletion.homEquiv : (G : GrpCat) →
  (P : ProfiniteGrp.{u}) → (ProfiniteGrp.ProfiniteCompletion.completion G ⟶ P) ≃ (G ⟶ GrpCat.of ↑P.toProfinite.toTop)
-- Std.Data.HashMap.Lemmas
Std.HashMap.equiv_of_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : BEq β] [LawfulBEq α]
  [LawfulBEq β], (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.Algebra.Group.Action.TypeTags
ofMul_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (a : α) (b : β), Additive.ofMul a +ᵥ b = a • b
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_add : Primrec₂ fun x1 x2 => x1 + x2
-- Mathlib.Topology.UniformSpace.Real
NNReal.continuous_coe : Continuous NNReal.toReal
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.gamma_ne_zero : ∀ {o : Ordinal.{u}}, o.gamma ≠ 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XYIdeal.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x : R) (y : Polynomial R),
  WeierstrassCurve.Affine.CoordinateRing.XYIdeal W' x y =
    Ideal.span {WeierstrassCurve.Affine.CoordinateRing.XClass W' x, WeierstrassCurve.Affine.CoordinateRing.YClass W' y}
-- Mathlib.RingTheory.Localization.AtPrime.Extension
/-- The following diagram where the vertical maps are the algebra maps and the horizontal maps are
`Localization.AtPrime.equivQuotMaximalIdeal.symm` and
`Localization.AtPrime.equivQuotientMapOfIsMaximal.symm` commutes:
```
Rₚ ⧸ 𝓂 ──▶ R ⧸ p
  │         │
Sₚ ⧸ 𝒫 ──▶ S ⧸ P
```
Here, `𝓂` denotes the maximal ideal of `Rₚ` and `𝒫` the image of `P` in `Sₚ`.
Note that result is stated in that direction since this is the formulation needed for the proof
of `Localization.AtPrime.inertiaDeg_map_eq_inertiaDeg`.
 -/
IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (Rₚ : Type u_3) [inst_4 : CommRing Rₚ] [inst_5 : Algebra R Rₚ]
  [inst_6 : IsLocalization.AtPrime Rₚ p] [inst_7 : IsLocalRing Rₚ] (Sₚ : Type u_4) [inst_8 : CommRing Sₚ]
  [inst_9 : Algebra S Sₚ] [inst_10 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ]
  [inst_11 : Algebra Rₚ Sₚ] (P : Ideal S) [hPp : P.LiesOver p] [inst_12 : Algebra R Sₚ] [IsScalarTower R S Sₚ]
  [IsScalarTower R Rₚ Sₚ] [inst_15 : p.IsMaximal] [inst_16 : P.IsMaximal]
  [inst_17 : (Ideal.map (algebraMap S Sₚ) P).LiesOver (IsLocalRing.maximalIdeal Rₚ)]
  (x : Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ),
  (algebraMap (R ⧸ p) (S ⧸ P)) ((IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ).symm x) =
    (IsLocalization.AtPrime.equivQuotientMapOfIsMaximal p Sₚ P).symm
      ((algebraMap (Rₚ ⧸ IsLocalRing.maximalIdeal Rₚ) (Sₚ ⧸ Ideal.map (algebraMap S Sₚ) P)) x)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- A non-unital subsemiring is isomorphic to its image under an injective function  -/
NonUnitalSubsemiring.equivMapOfInjective : {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] →
              (s : NonUnitalSubsemiring R) → (f : F) → Function.Injective ⇑f → ↥s ≃+* ↥(NonUnitalSubsemiring.map f s)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.coe_nnreal_ennreal : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → NNReal}, Measurable f → Measurable fun x => ↑(f x)
-- Mathlib.Logic.Function.Basic
Function.invFun_eq_of_injective_of_rightInverse : ∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β} {g : β → α},
  Function.Injective f → Function.RightInverse g f → Function.invFun f = g
-- Mathlib.RepresentationTheory.Intertwining
/-- The `Equiv` between representations induced from `TensorProduct.rid`.  -/
Representation.TensorProduct.rid : (A : Type u_1) →
  {G : Type u_2} →
    {W : Type u_4} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] → (σ : Representation A G W) → (σ.tprod (Representation.trivial A G A)).Equiv σ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], (m.erase k).get! k = default
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- An ordinal regarded as a term of `I`.  -/
Profinite.NobelingProof.term : (I : Type u) →
  [inst : LinearOrder I] → [inst_1 : WellFoundedLT I] → {o : Ordinal.{u}} → (o < Ordinal.type fun x1 x2 => x1 < x2) → I
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.natDegree_multiset_sum_le : ∀ {S : Type u_1} [inst : Semiring S] (l : Multiset (Polynomial S)),
  l.sum.natDegree ≤ Multiset.foldr max 0 (Multiset.map Polynomial.natDegree l)
-- Mathlib.Order.SupIndep
Finset.SupIndep.union : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α] [inst_3 : DecidableEq ι]
  {s t : Finset ι} {f : ι → α}, s.SupIndep f → t.SupIndep f → Disjoint (s.sup f) (t.sup f) → (s ∪ t).SupIndep f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_le_size_insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) {ρ : Type w}
  [inst_2 : ForIn Id ρ α] [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {l : ρ}, (↑m).size ≤ (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).size
-- Init.Data.Nat.Lemmas
_private.Init.Data.Nat.Lemmas.0.Nat.allLTTR.loop.match_1.eq_1 : ∀ (n : ℕ) (motive : (x : ℕ) → x ≤ n → Sort u_1) (x : 0 ≤ n) (h_1 : (x : 0 ≤ n) → motive 0 x)
  (h_2 : (i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.unicodeSymbolNoAntiquot.formatter : String → String → Bool → Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
/-- `midpoint x y` is the midpoint of the segment `[x, y]`.  -/
midpoint : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_4} →
      [inst : Ring R] → [Invertible 2] → [inst_2 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → P → P → P
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.Core.withConsistentCtx : {α : Type} → Lean.CoreM α → Lean.CoreM α
-- ProofWidgets.Cancellable
/-- Maps the ID of each currently executing request to its task.  -/
ProofWidgets.runningRequests : IO.Ref (ProofWidgets.RequestId × Std.HashMap ProofWidgets.RequestId ProofWidgets.CancellableTask)
-- Lean.Declaration
Lean.mkReducibilityHintsRegularEx : UInt32 → Lean.ReducibilityHints
-- Lean.Environment
_private.Lean.Environment.0.Lean.runInitAttrs : Lean.Environment → Lean.Options → IO Unit
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- If a short complex `S` is such that `S.f = 0` and that the kernel of `S.g` is preserved
by a functor `F`, then `F` preserves the right homology of `S`.  -/
CategoryTheory.Functor.preservesRightHomology_of_zero_f : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C),
  S.f = 0 →
    ∀ [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair S.g 0) F], F.PreservesRightHomologyOf S
-- Mathlib.Data.List.Duplicate
List.decidableDuplicate : {α : Type u_1} → [DecidableEq α] → (x : α) → (l : List α) → Decidable (List.Duplicate x l)
-- Init.Data.Int.Basic
/-- Negation of natural numbers.

Examples:
* `Int.negOfNat 6 = -6`
* `Int.negOfNat 0 = 0`
 -/
Int.negOfNat : ℕ → ℤ
-- Mathlib.Algebra.Module.SpanRank
Submodule.FG.spanRank_le_iff : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.FG → ∀ (n : ℕ), p.spanRank ≤ ↑n ↔ p.spanFinrank ≤ n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertMany_empty_list : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).size = l.length
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.ofList_cons : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {k : α} {v : β k} {tl : List ((a : α) × β a)},
  Std.DHashMap.ofList (⟨k, v⟩ :: tl) = (∅.insert k v).insertMany tl
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_piCongrLeft : ∀ {δ : Type u_4} {δ' : Type u_5} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] (f : δ' ≃ δ),
  Measurable ⇑(Equiv.piCongrLeft X f)
-- Mathlib.NumberTheory.Height.NumberField
_private.Mathlib.NumberTheory.Height.NumberField.0.NumberField.absNorm_mul_finprod_finitePlace_eq_one_aux : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {ι : Type u_2} [Finite ι]
  {x : ι → NumberField.RingOfIntegers K} [Nonempty ι],
  (∀ (i : ι), x i ≠ 0) →
    ↑(Ideal.absNorm (Ideal.span (Set.range x))) * ∏ᶠ (v : NumberField.FinitePlace K), ⨆ i, v ↑(x i) = 1
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.multiplicity_le_multiplicity_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Monoid β] {a b : α} {c d : β},
  FiniteMultiplicity a b →
    FiniteMultiplicity c d → (multiplicity a b ≤ multiplicity c d ↔ ∀ (n : ℕ), a ^ n ∣ b → c ^ n ∣ d)
-- Mathlib.Data.EReal.Basic
/-- The canonical inclusion from reals to ereals. Registered as a coercion.  -/
Real.toEReal : ℝ → EReal
-- Mathlib.Topology.Connected.Basic
IsConnected.union : ∀ {α : Type u} [inst : TopologicalSpace α] {s t : Set α},
  (s ∩ t).Nonempty → IsConnected s → IsConnected t → IsConnected (s ∪ t)
-- Mathlib.Order.RelSeries
RelSeries.ofLE_toFun : ∀ {α : Type u_1} {r : SetRel α α} (x : RelSeries r) {s : SetRel α α} (h : r ⊆ s) (a : Fin (x.length + 1)),
  (x.ofLE h).toFun a = x.toFun a
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : sInfHom α β) (f' : α → β) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.comp_assoc : ∀ {V : Type u_1} {W : Type u_2} {X : Type u_3} {Y : Type u_4} {G : SimpleGraph V} {G' : SimpleGraph W}
  {G'' : SimpleGraph X} {G''' : SimpleGraph Y} (f : G'' →g G''') (g : G' →g G'') (h : G →g G'),
  f.comp (g.comp h) = (f.comp g).comp h
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k : α} {v : β}, (m.insert k v)[k] = v
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.le_comap_of_subsingleton : ∀ {V : Type u_1} {W : Type u_2} (G : SimpleGraph V) (G' : SimpleGraph W) (f : V → W) [Subsingleton V],
  G ≤ SimpleGraph.comap f G'
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.obj.neg_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] {G : C} [inst_5 : CategoryTheory.AddGrpObj G],
  CategoryTheory.AddGrpObj.neg = F.map CategoryTheory.AddGrpObj.neg
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.comm₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  φ₁.τ₃ = self.h₃ + CategoryTheory.CategoryStruct.comp self.h₂ S₂.g + φ₂.τ₃
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.match_1.eq_2 : ∀ (s : String) (motive : Char → Option (s.Pos × ℕ) → Sort u_1) (x : Char) (x_1 : Option (s.Pos × ℕ))
  (h_1 : (q : s.Pos) → (v : ℕ) → x_1 = some (q, v) → motive 'U' (some (q, v)))
  (h_2 : (x : Char) → (x_2 : Option (s.Pos × ℕ)) → x_1 = x_2 → motive x x_2),
  (∀ (q : s.Pos) (v : ℕ), x = 'U' → x_1 = some (q, v) → False) →
    (match x, h₃ : x_1 with
      | 'U', some (q, v) => h_1 q v h₃
      | x, x_3 => h_2 x x_3 h₃) =
      h_2 x x_1 ⋯
-- Mathlib.RingTheory.Support
LocalizedModule.subsingleton_iff_support_subset : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : R},
  Subsingleton (LocalizedModule.Away f M) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.mulActionFinset.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Monoid α] [inst_2 : MulAction α β],
  Finset.mulActionFinset = Function.Injective.mulAction SetLike.coe ⋯ ⋯
-- Init.Data.SInt.Lemmas
Int16.toNatClampNeg_lt : ∀ (x : Int16), x.toNatClampNeg < 2 ^ 15
-- Init.Core
instInhabitedTrue.default : True
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_comp_comp : ∀ {β : Type ub} {V W M : SetRel β β} [W.IsSymm] {p : β × β},
  p ∈ (V.comp M).comp W ↔ (UniformSpace.ball p.1 V ×ˢ UniformSpace.ball p.2 W ∩ M).Nonempty
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_edist_eq_sup : ∀ {α : Type u_2} {β : Type u_3} [inst : EDist α] [inst_1 : EDist β] (f g : WithLp ⊤ (α × β)),
  edist f g = max (edist f.fst g.fst) (edist f.snd g.snd)
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl)
The natural transformation given by the coalgebra structure maps, used to construct a cone `c` with
point `limit (D ⋙ forget T)`.
 -/
CategoryTheory.Comonad.ForgetCreatesLimits'.γ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          {D : CategoryTheory.Functor J T.Coalgebra} → D.comp T.forget ⟶ (D.comp T.forget).comp T.toFunctor
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.mulRec.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (s : ℕ) → motive s.succ),
  (match 0 with
    | 0 => h_1 ()
    | s.succ => h_2 s) =
    h_1 ()
-- Mathlib.Topology.Order.LeftRightNhds
nhdsGT_basis : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] (a : α),
  (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioo a)
-- Std.Time.Date.Unit.Week
Std.Time.Week.Aligned.instTransOrdOrdinal : Std.TransOrd Std.Time.Week.Aligned.Ordinal
-- Mathlib.RingTheory.Localization.Ideal
IsLocalization.mk'_mem_map_algebraMap_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (I : Ideal R) (x : R) (s : ↥M),
  IsLocalization.mk' S x s ∈ Ideal.map (algebraMap R S) I ↔ ∃ s ∈ M, s * x ∈ I
-- Init.Data.UInt.Lemmas
UInt8.toFin_toUInt64 : ∀ (n : UInt8), n.toUInt64.toFin = Fin.castLE UInt8.toFin_toUInt64._proof_1 n.toFin
-- Std.Time.Date.Unit.Day
Std.Time.Day.instTransOrdOrdinal : Std.TransOrd Std.Time.Day.Ordinal
-- Mathlib.SetTheory.Lists
Finsets.instInhabited : {α : Type u_1} → Inhabited (Finsets α)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc'_trunc'_pow : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] {n : σ →₀ ℕ} {k : ℕ},
  1 ≤ k →
    ∀ (φ : MvPowerSeries σ R),
      (MvPowerSeries.trunc' R n) (↑((MvPowerSeries.trunc' R n) φ) ^ k) = (MvPowerSeries.trunc' R n) (φ ^ k)