mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Given a presieve on `F(X)`, we can define a presieve on `X` by taking the preimage via `F`.  -/
CategoryTheory.Presieve.functorPullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → {X : C} → CategoryTheory.Presieve (F.obj X) → CategoryTheory.Presieve X
-- Mathlib.Logic.Equiv.Defs
/-- Equivalence between `Fin 0` and `PEmpty`.  -/
finZeroEquiv' : Fin 0 ≃ PEmpty.{u}
-- Mathlib.Topology.Algebra.InfiniteSum.Module
Summable.tsum_smul_const : ∀ {ι : Type u_5} {R : Type u_7} {M : Type u_9} [inst : Semiring R] [inst_1 : TopologicalSpace R]
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [ContinuousSMul R M] {f : ι → R}
  {L : SummationFilter ι} [T2Space M] [L.NeBot],
  Summable f L → ∀ (a : M), ∑'[L] (z : ι), f z • a = (∑'[L] (z : ι), f z) • a
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
ContMDiff.mdifferentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s : Set M}
  {n : WithTop ℕ∞}, ContMDiff I I' n f → n ≠ 0 → MDiffAt[s] f x
-- Init.Data.Array.Find
Array.idxOf?_eq_map_finIdxOf?_val : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {a : α}, xs.idxOf? a = Option.map (fun x => ↑x) (xs.finIdxOf? a)
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.ghostComponent_verschiebung : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [hp : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  (WittVector.ghostComponent (n + 1)) (WittVector.verschiebung x) = ↑p * (WittVector.ghostComponent n) x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Ring.powFn? : Lean.Meta.Grind.Arith.CommRing.Ring → Option Lean.Expr
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
Function.Injective.addActionHom_embedding_isInjective : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup H] [inst_3 : AddAction H β] {σ : G → H} {f : α →ₑ[σ] β} {ι : Type u_5}
  (hf : Function.Injective ⇑f), Function.Injective ⇑(Function.Injective.addActionHom_embedding ι hf)
-- Mathlib.Topology.Compactification.StoneCech
instTotallyDisconnectedSpaceUltrafilter : ∀ {α : Type u}, TotallyDisconnectedSpace (Ultrafilter α)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.union_vsub_inter_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s₁ s₂ t₁ t₂ : Set β}, s₁ ∪ s₂ -ᵥ t₁ ∩ t₂ ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)
-- Mathlib.Analysis.Analytic.Constructions
one_le_alternatingGeometricSeries_radius : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [Nontrivial A], 1 ≤ (alternatingGeometricSeries 𝕜 A).radius
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.restrict_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {M' : Submonoid M} {N' : Submonoid N}
  {f : M →* N} (h : Set.MapsTo ⇑f ↑M' ↑N'), Function.Injective ⇑f → Function.Injective ⇑(MonoidHom.restrict h)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.hom_ofHom : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : Ring X] [inst_2 : Algebra R X] [inst_3 : Ring Y]
  [inst_4 : Algebra R Y] (f : X →ₐ[R] Y), AlgCat.Hom.hom (AlgCat.ofHom f) = f
-- Aesop.Tree.Data
Aesop.Rapp.parent : Aesop.Rapp → Aesop.GoalRef
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.instMax : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → Max (L.BoundedFormula α n)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.type₂_simplex : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] (f : P.RankFunction ι)
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j),
  (SSet.Subcomplex.Pairing.RankFunction.Cell.type₂ f c).simplex =
    (CategoryTheory.ConcreteCategory.hom (c.ιSigmaStdSimplex.app (Opposite.op { len := c.dim })))
      (SSet.stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_insertMany_list_le : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)}, (m.insertMany l).size ≤ m.size + l.length
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sinc_le_one : ∀ (x : ℝ), Real.sinc x ≤ 1
-- Mathlib.Analysis.Calculus.TangentCone.Basic
tangentConeAt_closure : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s : Set E}
  {x : E} [ContinuousAdd E] [ContinuousConstSMul 𝕜 E], tangentConeAt 𝕜 (closure s) x = tangentConeAt 𝕜 s x
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddGroup.tendsto_nhds_zero : ∀ {α : Type u_2} {E : Type u_5} [inst : SeminormedAddGroup E] {f : α → E} {l : Filter α},
  Filter.Tendsto f l (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in l, ‖f x‖ < ε
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.prodLeftIsoPullback_inv_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  {Z_1 : C} (h : Z.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.snd) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd Y.hom Z.hom) h
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- We call *occurrence set* for pattern `p` and position `g` the set of configurations
in which a pattern `p` occurs at position `g`.

This proves that it is exactly the cylinder corresponding to the
pattern obtained by translating `p` by `g`.

Equivalently, `p.mulOccursInAt x g` iff on every translated site
`g * w` (with `w ∈ p.support`)
the configuration `x` agrees with the translated pattern `Pattern.mulShift p g`.

(This uses `[IsLeftCancelMul G]` to identify the preimage along left-multiplication by `g`.)  -/
SymbolicDynamics.FullShift.mulOccursInAt_eq_cylinder : ∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : Monoid G] [IsLeftCancelMul G]
  (p : SymbolicDynamics.FullShift.Pattern A G) (g : G),
  {x | p.mulOccursInAt x g} =
    SymbolicDynamics.FullShift.cylinder (Finset.image (fun x => g * x) p.support) (p.mulShift g)
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- The evaluation at a point as a linear map.  -/
Derivation.evalAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      (x : M) →
                        Derivation 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤)
                            (ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) M 𝕜 ↑⊤) →ₗ[PointedContMDiffMap 𝕜 I M (↑⊤) x]
                          PointDerivation I x
-- Mathlib.Algebra.Group.AddChar
/-- The additive characters on a commutative additive group form a commutative group.  -/
AddChar.instAddCommGroup : {A : Type u_1} → {M : Type u_2} → [inst : AddCommGroup A] → [inst_1 : CommMonoid M] → AddCommGroup (AddChar A M)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Comon_EquivMon_OpOp_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Comon.Comon_EquivMon_OpOp C).functor = CategoryTheory.Comon.ComonToMonOpOp C
-- Mathlib.Data.Nat.Digits.Defs
Nat.coe_ofDigits : ∀ (α : Type u_1) [inst : Semiring α] (b : ℕ) (L : List ℕ), ↑(Nat.ofDigits b L) = Nat.ofDigits (↑b) L
-- Std.Time.Internal.Bounded
/-- A `Bounded` is represented by an `Int` that is constrained by a lower and higher bounded using some
relation `rel`. It includes all the integers that `rel lo val ∧ rel val hi`.
 -/
Std.Time.Internal.Bounded : (ℤ → ℤ → Prop) → ℤ → ℤ → Type
-- Mathlib.Topology.ContinuousMap.Basic
/-- Combine a collection of bundled continuous maps `C(X i, Y i)` into a bundled continuous map
`C(∀ i, X i, ∀ i, Y i)`.  -/
ContinuousMap.piMap : {I : Type u_5} →
  {X : I → Type u_7} →
    {Y : I → Type u_8} →
      [inst : (i : I) → TopologicalSpace (X i)] →
        [inst_1 : (i : I) → TopologicalSpace (Y i)] → ((i : I) → C(X i, Y i)) → C((i : I) → X i, (i : I) → Y i)
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
AlgebraicGeometry.HasRingHomProperty.descendsAlong_flat : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange]
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] => Q],
  (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] =>
      RingHom.FaithfullyFlat) →
    P.DescendsAlong (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- The (real) logarithm of a natural number `n` is bounded by a multiple of every power of `n`
with positive exponent.  -/
Real.log_natCast_le_rpow_div : ∀ (n : ℕ) {ε : ℝ}, 0 < ε → Real.log ↑n ≤ ↑n ^ ε / ε
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limit.lift_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (H : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimit H]
  (c : CategoryTheory.Limits.Cone H) (j : J) (k : K),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit.lift H c).app k)
      ((CategoryTheory.Limits.limit.π H j).app k) =
    (c.π.app j).app k
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_alter_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {k : α} {fallback : β k},
  (↑m).WF → ∀ {f : Option (β k) → Option (β k)}, (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback
-- Mathlib.LinearAlgebra.TensorPower.Pairing
TensorPower.pairingDual.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ),
  TensorPower.pairingDual R M n = PiTensorProduct.lift (TensorPower.multilinearMapToDual R M n)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_add : ∀ (o₁ o₂ : Ordinal.{u_1}), (o₁ + o₂).card = o₁.card + o₂.card
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.natDegree_coeff_Φ_ofNat : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ),
  (W.Φ ↑n).natDegree ≤ n ^ 2 ∧ (W.Φ ↑n).coeff (n ^ 2) = 1
-- Mathlib.Algebra.Free
FreeAddMagma.of : {α : Type u} → α → FreeAddMagma α
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.tAux.eq_1 : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J] (i j : J),
  AlgebraicGeometry.Scheme.IsLocallyDirected.tAux F i j =
    AlgebraicGeometry.Scheme.Cover.glueMorphisms
      (AlgebraicGeometry.Scheme.Opens.iSupOpenCover fun k => AlgebraicGeometry.Scheme.Hom.opensRange (F.map k.snd.1))
      (fun k =>
        CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoOpensRange (F.map k.snd.1)).inv
          (F.map k.snd.2))
      ⋯
-- Init.Data.BitVec.Basic
/-- Transforms a bitvector of length `w` into a bitvector of length `v`, padding with `0` as needed.

The specific behavior depends on the relationship between the starting width `w` and the final width
`v`:
 * If `v > w`, it is zero-extended; the high bits are padded with zeroes until the bitvector has `v`
   bits.
 * If `v = w`, the bitvector is returned unchanged.
 * If `v < w`, the high bits are truncated.

`BitVec.setWidth`, `BitVec.zeroExtend`, and `BitVec.truncate` are aliases for this operation.

SMT-LIB name: `zero_extend`.
 -/
BitVec.setWidth : {w : ℕ} → (v : ℕ) → BitVec w → BitVec v
-- Mathlib.Data.Set.Card
Set.InjOn.encard_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.InjOn f s → (f '' s).encard = s.encard
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasAdditiveReduction.mk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K}
  [toIsMinimal : WeierstrassCurve.IsMinimal R W],
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.Δ < 1 →
    (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal R)) W.c₄ < 1 →
      WeierstrassCurve.HasAdditiveReduction R W
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.OverflowInput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} (w : ℕ) (vec : aig.BinaryRefVec w)
  (cin : aig.Ref) (w_1 : ℕ) (vec_1 : aig.BinaryRefVec w_1) (cin_1 : aig.Ref),
  ({ w := w, vec := vec, cin := cin } = { w := w_1, vec := vec_1, cin := cin_1 }) =
    (w = w_1 ∧ vec ≍ vec_1 ∧ cin = cin_1)
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod.congr_simp : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f f_1 : M →* P) (e_f : f = f_1) (g g_1 : N →* P) (e_g : g = g_1) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)),
  f.noncommCoprod g comm = f_1.noncommCoprod g_1 ⋯
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.instSubsingleton : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  Subsingleton (CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- (Implementation): The structure morphisms of the covering objects of `cylinder f g`.  -/
CategoryTheory.PreOneHypercover.cylinderf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
            (f g : E.Hom F) →
              {i : E.I₀} → (k : F.I₁ (f.s₀ i) (g.s₀ i)) → CategoryTheory.PreOneHypercover.cylinderX f g k ⟶ S
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.charZero : ∀ {α : Type u} [inst : AddMonoidWithOne α] [CharZero α], CharZero (WithBot α)
-- Mathlib.Analysis.Normed.Lp.WithLp
LinearEquiv.withLpCongr_symm : ∀ (p : ENNReal) {K : Type u_1} {K' : Type u_2} {V : Type u_4} {V' : Type u_5} [inst : Semiring K] [inst_1 : Semiring K']
  {σ : K →+* K'} {σ' : K' →+* K} [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] [inst_4 : AddCommGroup V]
  [inst_5 : Module K V] [inst_6 : AddCommGroup V'] [inst_7 : Module K' V'] (f : V ≃ₛₗ[σ] V'),
  (LinearEquiv.withLpCongr p f).symm = LinearEquiv.withLpCongr p f.symm
-- Mathlib.Order.Filter.Basic
Filter.principal_empty : ∀ {α : Type u}, Filter.principal ∅ = ⊥
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.mem_closure : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {x : M},
  x ∈ SemigroupIdeal.closure s ↔ ∀ (p : SemigroupIdeal M), s ⊆ ↑p → x ∈ p
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryGT! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap α (fun x => β) cmp → α → α × β
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_le : ∀ {a b : Int32}, a ≤ b → a.toNatClampNeg ≤ b.toNatClampNeg
-- Std.Data.HashMap.Lemmas
Std.HashMap.ofList_equiv_foldl : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {l : List (α × β)},
  (Std.HashMap.ofList l).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.mk : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} →
                                (toContinuousLinearMap : V →L[R] W) →
                                  (∀ (g : G), toContinuousLinearMap ∘SL π₁ g = π₂ g ∘SL toContinuousLinearMap) →
                                    ContIntertwiningMap π₁ π₂
-- Init.Data.String.Basic
/-- Constructs a valid position on `s` from a position, returning `none` if the position is not valid.  -/
String.pos? : (s : String) → String.Pos.Raw → Option s.Pos
-- Lean.Elab.Syntax
_private.Lean.Elab.Syntax.0.Lean.Elab.Command.elabSyntaxAux : Lean.Elab.Command.CommandElab
-- Mathlib.Topology.Homotopy.Lifting
/-- A continuous map `f` from a simply-connected, locally path-connected space `A` to another
space `X` lifts uniquely through a covering map `p : E → X`, after specifying any lift
`e₀ : E` of any point `a₀ : A`.  -/
IsCoveringMap.existsUnique_continuousMap_lifts : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X},
  IsCoveringMap p →
    ∀ [SimplyConnectedSpace A] [LocallyPathConnectedSpace A] (f : C(A, X)) (a₀ : A) (e₀ : E),
      p e₀ = f a₀ → ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.rightDualIso_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (p : CategoryTheory.ExactPairing X Y), CategoryTheory.rightDualIso p p = CategoryTheory.Iso.refl Y
-- Init.SizeOf
sizeOf_thunk : ∀ {α : Sort u_1} [inst : SizeOf α] (f : Unit → α), sizeOf f = sizeOf (f ())
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.Stmt.peek : {K : Type u_1} →
  {Γ : K → Type u_2} →
    {Λ : Type u_3} → {σ : Type u_4} → (k : K) → (σ → Option (Γ k) → σ) → Turing.TM2.Stmt Γ Λ σ → Turing.TM2.Stmt Γ Λ σ
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Generalization of `Finsupp.add_sum_erase`: if `g` maps a second argument of 0
to 0, then its sum over `f : α →₀ M` is the same as adding the value on any element
`y : α` to the sum over `erase y f`.  -/
Finsupp.add_sum_erase' : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α →₀ M) (y : α)
  (g : α → M → N), (∀ (i : α), g i 0 = 0) → g y (f y) + (Finsupp.erase y f).sum g = f.sum g
-- Mathlib.MeasureTheory.Integral.MeanInequalities
ENNReal.lintegral_mul_le_Lp_mul_Lq_of_ne_zero_of_eq_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p q : ℝ},
  0 < p →
    0 ≤ q →
      ∀ {f g : α → ENNReal},
        ∫⁻ (a : α), f a ^ p ∂μ = ⊤ →
          ∫⁻ (a : α), g a ^ q ∂μ ≠ 0 →
            ∫⁻ (a : α), (f * g) a ∂μ ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), g a ^ q ∂μ) ^ (1 / q)
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin_i₁ : ∀ (l : ℕ) (pq : ℤ × Fin l), (CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin l).i₁ pq = pq.2.castSucc
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.instLawfulForwardPatternModelChar : ∀ {c : Char}, String.Slice.Pattern.Model.LawfulForwardPatternModel c
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.ext_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f g : X.PartialIso Y),
  f = g ↔ ∃ (e : f.source = g.source) (e' : g.target = f.target), f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e'
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instSubNegZeroMonoidOfAddOpposite : {M : Type u_1} → [SubNegZeroMonoid Mᵃᵒᵖ] → SubNegZeroMonoid Mᵈᵃᵃ
-- Init.Data.Float.Model.Unpacked.Operations.OfNat
/-- Converts an `Int64` to an `UnpackedFloat`, returning positive zero on zero.  -/
Float.Model.UnpackedFloat.ofInt64 : Float.Model.Format → Int64 → Float.Model.UnpackedFloat
-- Init.SimpLemmas
and_not_self : ∀ {a : Prop}, ¬(a ∧ ¬a)
-- Mathlib.Data.Setoid.Partition
IndexedPartition.mem_iff_index_eq : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) {x : α} {i : ι}, x ∈ s i ↔ hs.index x = i
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_zero_iff : ∀ {z : ℂ}, z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Coercion of a `MonoidHom` into a function is itself a `MonoidHom`.

See also `MonoidHom.eval`.  -/
MonoidHom.coeFn : (α : Type u_5) → (β : Type u_6) → [inst : MulOneClass α] → [inst_1 : CommMonoid β] → (α →* β) →* α → β
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.hom_ext_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : StandardEtalePair R} {f g : P.Ring →ₐ[R] S}, f = g ↔ f P.X = g P.X
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.subtype.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- The transpose of a matrix is row stochastic matrix if it is column stochastic.  -/
Matrix.transpose_mem_rowStochastic_iff_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M.transpose ∈ Matrix.rowStochastic R n ↔ M ∈ Matrix.colStochastic R n
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiring.ofClass_carrier : ∀ {S : Type u_1} {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike S R]
  [inst_2 : NonUnitalSubsemiringClass S R] (s : S), ↑(NonUnitalSubsemiring.ofClass s) = ↑s
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.instDiv.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : One M] [inst_1 : DivisionMonoid N],
  OneHom.instDiv = { div := fun f g => { toFun := fun m => f m / g m, map_one' := ⋯ } }
-- Mathlib.Data.PNat.Xgcd
PNat.gcd_eq : ∀ (a b : ℕ+), a.gcdD b = a.gcd b
-- Mathlib.Topology.Compactification.StoneCech
/-- Every ultrafilter `u` on `Ultrafilter α` converges to a unique
point of `Ultrafilter α`, namely `joinM u`.  -/
ultrafilter_converges_iff : ∀ {α : Type u} {u : Ultrafilter (Ultrafilter α)} {x : Ultrafilter α}, ↑u ≤ nhds x ↔ x = joinM u
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs : BEq Mathlib.Meta.FunProp.LambdaTheoremArgs