mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An `OrderAddMonoidHom` can be made to an `OrderHom` between their
`ArchimedeanOrder`.  -/
ArchimedeanOrder.orderHom : {M : Type u_2} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        {N : Type u_3} →
          [inst_3 : AddCommGroup N] →
            [inst_4 : LinearOrder N] →
              [inst_5 : IsOrderedAddMonoid N] → (M →+o N) → ArchimedeanOrder M →o ArchimedeanOrder N
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.isOver_iff_eq_restrict : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] {f : X.PartialMap Y},
  AlgebraicGeometry.Scheme.PartialMap.IsOver S f ↔
    f.compHom (Y ↘ S) = (AlgebraicGeometry.Scheme.Hom.toPartialMap (X ↘ S)).restrict f.domain ⋯ ⋯
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.nu_ne_zero : ∀ {s : BoundingSieve} {d : ℕ}, d ∣ s.prodPrimes → s.nu d ≠ 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = (m.getKey? a).isSome
-- Mathlib.CategoryTheory.Localization.Monoidal.Functor
CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp_μIso_inv : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.MonoidalCategory D]
  [inst_5 : CategoryTheory.MonoidalCategory E] (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C)
  [inst_6 : L.IsLocalization W] [inst_7 : L.Monoidal] (F : CategoryTheory.Functor D E) (G : CategoryTheory.Functor C E)
  [inst_8 : G.Monoidal] [inst_9 : W.ContainsIdentities] [inst_10 : CategoryTheory.Localization.Lifting L W G F]
  (X Y : D),
  ((CategoryTheory.Localization.Monoidal.functorCoreMonoidalOfComp L W F G).μIso X Y).inv =
    ((CategoryTheory.Localization.Monoidal.curriedTensorPreIsoPost L W F G).inv.app X).app Y
-- Mathlib.LinearAlgebra.Isomorphisms
/-- Linear map from `p` to `p+p'/p'` where `p p'` are submodules of `R`  -/
LinearMap.subToSupQuotient : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (p p' : Submodule R M) → ↥p →ₗ[R] ↥(p ⊔ p') ⧸ Submodule.comap (p ⊔ p').subtype p'
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_fast_choose : Nat.choose = Nat.fast_choose
-- Mathlib.Order.Atoms
isCoatom_compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {a : α}, IsCoatom aᶜ ↔ IsAtom a
-- Mathlib.Algebra.Polynomial.RuleOfSigns
_private.Mathlib.Algebra.Polynomial.RuleOfSigns.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofExistsFiniteIsBase_E : ∀ {α : Type u_1} (E : Set α) (IsBase : Set α → Prop) (exists_finite_base : ∃ B, IsBase B ∧ B.Finite)
  (isBase_exchange : Matroid.ExchangeProperty IsBase) (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  (Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground).E = E
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_modify_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [inst_3 : Inhabited α] {k : α} {f : β k → β k}, m.WF → (m.modify k f).getKey! k = if k ∈ m then k else default
-- Mathlib.RingTheory.Length
Module.length_eq_finrank : ∀ (K : Type u_5) (M : Type u_6) [inst : DivisionRing K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [Module.Finite K M], Module.length K M = ↑(Module.finrank K M)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.restrict_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {H : Type u_6}
  [inst_6 : Monoid H] (π : ContRepresentation R G V) (φ : H →* G) (h : H), (π.restrict φ) h = π (φ h)
-- Mathlib.RingTheory.Smooth.Field
/-- Separably generated extensions are formally smooth.  -/
Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable : ∀ {K : Type u_1} {L : Type u_2} {ι : Type u_3} [inst : Field L] [inst_1 : Field K] [inst_2 : Algebra K L] {v : ι → L},
  AlgebraicIndependent K v →
    ∀ [Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range v))) L], Algebra.FormallySmooth K L
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
_private.Mathlib.LinearAlgebra.TensorProduct.Graded.External.0.TensorProduct.termℬ𝒜 : Lean.ParserDescr
-- Mathlib.Tactic.ProdAssoc
/-- IMPLEMENTATION: Syntax used in the implementation of `prod_assoc%`.
This elaborator postpones if there are metavariables in the expected type,
and to propagate the fact that this elaborator produces an `Equiv`,
the `prod_assoc%` macro sets things up with a type ascription.
This enables using `prod_assoc%` with, for example `Equiv.trans` dot notation.  -/
Lean.Expr.prodAssocStx : Lean.ParserDescr
-- Mathlib.Data.Sym.Sym2
Sym2.mem_pmap_iff : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (z : Sym2 α) (h : ∀ a ∈ z, P a) (b : β),
  b ∈ Sym2.pmap f z h ↔ ∃ a, ∃ (ha : a ∈ z), b = f a ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesLimitsOfShape_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D),
  Subsingleton (CategoryTheory.Limits.PreservesLimitsOfShape J F)
-- Mathlib.Data.NNReal.Basic
NNReal.image_coe_Iio : ∀ (x : NNReal), NNReal.toReal '' Set.Iio x = Set.Ico 0 ↑x
-- Mathlib.Topology.Algebra.Monoid
ContinuousWithinAt.fun_nsmul : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : AddMonoid M]
  [ContinuousAdd M] {f : X → M} {x : X} {s : Set X},
  ContinuousWithinAt f s x → ∀ (n : ℕ), ContinuousWithinAt (fun i => n • f i) s x
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a co-Heyting homomorphism preserves the difference operation.  -/
CoheytingHom.map_sdiff' : ∀ {α : Type u_6} {β : Type u_7} [inst : CoheytingAlgebra α] [inst_1 : CoheytingAlgebra β] (self : CoheytingHom α β)
  (a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b
-- Lean.Elab.InfoTree.Types
Lean.Elab.UserWidgetInfo.mk.sizeOf_spec : ∀ (toWidgetInstance : Lean.Widget.WidgetInstance) (stx : Lean.Syntax),
  sizeOf { toWidgetInstance := toWidgetInstance, stx := stx } = 1 + sizeOf toWidgetInstance + sizeOf stx
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function respects the `≤` relation asymptotically.
 -/
Function.locallyFinsuppWithin.logCounting_eventuallyLE : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {f₁ f₂ : Function.locallyFinsupp E ℤ},
  f₁ ≤ f₂ → Function.locallyFinsuppWithin.logCounting f₁ ≤ᶠ[Filter.atTop] Function.locallyFinsuppWithin.logCounting f₂
-- Init.Sym.Lemmas
Lean.Sym.Int32.le_eq_false : ∀ (a b : Int32), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.Algebra.GCDMonoid.Basic
instCommutativeLcm : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α], Std.Commutative lcm
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.mk : {α : Type u_6} →
  [inst : NonUnitalNonAssocSemiring α] →
    (toAddMonoidHom : α →+ α) →
      (∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = a * (↑toAddMonoidHom).toFun b) →
        (∀ (a b : α), (↑toAddMonoidHom).toFun (a * b) = (↑toAddMonoidHom).toFun a * b) → CentroidHom α
-- Mathlib.RingTheory.Polynomial.ContentIdeal
/-- The polynomial `p` is primitive if and only if the coefficients of `p` generate the whole ring.
 -/
Polynomial.isPrimitive_iff_contentIdeal_eq_top : ∀ {R : Type u_3} [inst : CommSemiring R] [IsBezout R] (p : Polynomial R), p.IsPrimitive ↔ p.contentIdeal = ⊤
-- Mathlib.Data.Nat.Factorial.SuperFactorial
_private.Mathlib.Data.Nat.Factorial.SuperFactorial.0.Nat.superFactorial.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Combinatorics.Matroid.Basic
_private.Mathlib.Combinatorics.Matroid.Basic.0.Matroid.inter_right_subset_ground : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, X ⊆ M.E → X ∩ Y ⊆ M.E
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The associator isomorphism can be passed through a map by swapping the order.  -/
CategoryTheory.Limits.biprod.associator_inv_natural : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h))
      (CategoryTheory.Limits.biprod.associator X Y Z).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).inv
      (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h)
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- **Alias** of `IsAddUnit.addSubmonoid.coe_neg`. -/
AddSubmonoid.IsUnit.Submonoid.coe_neg : ∀ {M : Type u_1} [inst : AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)), ↑(-x) = ↑(-IsAddUnit.addUnit ⋯)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.coe_rpow : ∀ (x : NNReal) (y : ℝ), ↑(x ^ y) = ↑x ^ y
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], k ∈ m₂ → (m₁ ∩ m₂).get! k = m₁.get! k
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_div_id_eq_one : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : Div α] [MulDivCancelClass α]
  {s : Finset α} {a : α}, a ∈ s → a ≠ 0 → (s.gcd fun b => b / s.gcd id) = 1
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_map_toList : ∀ {ι : Type u_2} {M : Type u_3} [inst : CommMonoid M] (s : Multiset ι) (f : ι → M),
  (List.map f s.toList).prod = (Multiset.map f s).prod
-- Lean.Environment
/-- Environment extension state for the language server.  -/
Lean.OLeanLevel.server : Lean.OLeanLevel
-- Mathlib.Data.PNat.Xgcd
/-- `bp` is a variable which changes through the algorithm.  -/
PNat.XgcdType.bp : PNat.XgcdType → ℕ
-- Init.Data.Nat.Fold
Nat.dfold_add : ∀ {n m : ℕ} {α : (i : ℕ) → autoParam (i ≤ n + m) Nat.dfold_add._auto_5 → Type u}
  (f : (i : ℕ) → (h : i < n + m) → α i ⋯ → α (i + 1) ⋯) (init : α 0 ⋯),
  (n + m).dfold f init = m.dfold (fun i h => f (n + i) ⋯) (n.dfold (fun i h => f i ⋯) init)
-- Mathlib.Algebra.Group.Prod
/-- Given magmas `M`, `N`, the natural projection homomorphism from `M × N` to `M`.  -/
MulHom.fst : (M : Type u_3) → (N : Type u_4) → [inst : Mul M] → [inst_1 : Mul N] → M × N →ₙ* M
-- Mathlib.RingTheory.FormalGroup.Basic
FormalGroup.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : SizeOf R] (toPowerSeries : MvPowerSeries (Fin 2) R)
  (zero_constantCoeff : MvPowerSeries.constantCoeff toPowerSeries = 0)
  (lin_coeff_X : (MvPowerSeries.coeff fun₀ | 0 => 1) toPowerSeries = 1)
  (lin_coeff_Y : (MvPowerSeries.coeff fun₀ | 1 => 1) toPowerSeries = 1)
  (assoc :
    MvPowerSeries.subst ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] toPowerSeries, MvPowerSeries.X 2]
        toPowerSeries =
      MvPowerSeries.subst
        ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] toPowerSeries] toPowerSeries),
  sizeOf
      { toPowerSeries := toPowerSeries, zero_constantCoeff := zero_constantCoeff, lin_coeff_X := lin_coeff_X,
        lin_coeff_Y := lin_coeff_Y, assoc := assoc } =
    1 + sizeOf zero_constantCoeff + sizeOf lin_coeff_X + sizeOf lin_coeff_Y + sizeOf assoc
-- Mathlib.Algebra.Group.Basic
mul_div_cancel : ∀ {G : Type u_3} [inst : CommGroup G] (a b : G), a * (b / a) = b
-- Std.Async.UDP
/-- Gets the local address of the UDP socket.
 -/
Std.Async.UDP.Socket.getSockName : Std.Async.UDP.Socket → IO Std.Net.SocketAddress
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.const_div : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Div γ] [MeasurableDiv γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ (c : γ), ProbabilityTheory.IdentDistrib (fun x => c / f x) (fun x => c / g x) μ ν
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getEntry : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → (a : α) → (l : List ((a : α) × β a)) → Std.Internal.List.containsKey a l = true → (a : α) × β a
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.conj : ∀ {G : Type u} [inst : Group G] {B : GroupFilterBasis G} (x₀ : G) {U : Set G},
  U ∈ B → ∃ V ∈ B, V ⊆ (fun x => x₀ * x * x₀⁻¹) ⁻¹' U
-- Mathlib.LinearAlgebra.Projectivization.Action
Projectivization.matrixSpecialLinearGroup_smul_def : ∀ {ι : Type u_4} {F : Type u_5} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : Field F]
  (g : Matrix.SpecialLinearGroup ι F) (x : Projectivization F (ι → F)),
  g • x = Matrix.SpecialLinearGroup.toLin'_equiv g • x
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The proposition that the function preserves 0  -/
DistribMulActionHom.map_zero' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_10}
  [inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_11} [inst_4 : AddMonoid B]
  [inst_5 : DistribMulAction N B] (self : A →ₑ+[φ] B), self.toFun 0 = 0
-- Mathlib.Data.Part
Part.map_some : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (a : α), Part.map f (Part.some a) = Part.some (f a)
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- The sum of the weights for the centroid indexed by a `Fintype`.  -/
Finset.sum_centroidWeightsIndicator : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [inst_1 : Fintype ι],
  ∑ i, Finset.centroidWeightsIndicator k s i = ∑ i ∈ s, Finset.centroidWeights k s i
-- Std.Tactic.Do.Syntax
/-- `mconstructor` is like `constructor`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by
  mintro HQ
  mconstructor <;> mexact HQ
```
 -/
Lean.Parser.Tactic.mconstructor : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.preprocess : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAt.div_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : DivInvMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffMul I n G]
  {E' : Type u_5} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {f : M → G} {x : M} (c : G),
  ContMDiffAt I' I n f x → ContMDiffAt I' I n (fun x => f x / c) x
-- Mathlib.MeasureTheory.Order.Lattice
MeasurableSup₂.mk : ∀ {M : Type u_1} [inst : MeasurableSpace M] [inst_1 : Max M],
  autoParam (Measurable fun p => p.1 ⊔ p.2) MeasurableSup₂.measurable_sup._autoParam → MeasurableSup₂ M
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceClientCapabilities.workspaceEdit? : Lean.Lsp.WorkspaceClientCapabilities → Option Lean.Lsp.WorkspaceEditClientCapabilities
-- Mathlib.ModelTheory.Substructures
/-- A first-order hom `f : M → N` whose values lie in a substructure `p ⊆ N` can be restricted to a
hom `M → p`.  -/
FirstOrder.Language.Hom.codRestrict : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] → (p : L.Substructure N) → (f : L.Hom M N) → (∀ (c : M), f c ∈ p) → L.Hom M ↥p
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.integral_toReal_rnDeriv' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.SigmaFinite ν],
  ∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν = μ.real Set.univ - (μ.singularPart ν).real Set.univ
-- Mathlib.RingTheory.WittVector.Verschiebung
/-- The 0th Verschiebung polynomial is 0. For `n > 0`, the `n`th Verschiebung polynomial is the
variable `X (n-1)`.
 -/
WittVector.verschiebungPoly : ℕ → MvPolynomial ℕ ℤ
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.consₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a),
  m.consₘ a b =
    ⟨{ size := (↑m).size + 1,
        buckets :=
          Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a fun l => Std.DHashMap.Internal.AssocList.cons a b l },
      ⋯⟩
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.star_mk : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] (x y : R), star { re := x, im := y } = { re := x + b * y, im := -y }
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- An adjunction of monoidal functors lifts to an adjunction of their lifts to additive
monoid objects.  -/
CategoryTheory.Adjunction.mapAddMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (a : F ⊣ G) →
                  [inst_4 : F.Monoidal] → [inst_5 : G.LaxMonoidal] → [a.IsMonoidal] → F.mapAddMon ⊣ G.mapAddMon
-- Mathlib.Topology.Order.Basic
pi_Iic_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι]
  {a' x' : ι → α}, (∀ (i : ι), x' i < a' i) → Set.Iic a' ∈ nhds x'
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- Given three graded objects `X₁`, `X₂`, `X₃` in `GradedObject I C`, this is the
assumption that for all `i₁ : I` and `i₂₃ : I`, the tensor product functor `X₁ i₁ ⊗ -`
commutes with the coproduct of the objects `X₂ i₂ ⊗ X₃ i₃` such that `i₂ + i₃ = i₂₃`.  -/
CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ : {I : Type u} →
  [AddMonoid I] →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [CategoryTheory.MonoidalCategory C] →
          CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → Prop
-- Lean.LocalContext
Lean.LocalContext.numIndices : Lean.LocalContext → ℕ
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- A lax monoidal functor takes additive monoid objects to additive monoid objects.

That is, a lax monoidal functor `F : C ⥤ D` induces a functor `AddMon C ⥤ AddMon D`.
 -/
CategoryTheory.Functor.mapAddMon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.LaxMonoidal] → CategoryTheory.Functor (CategoryTheory.AddMon C) (CategoryTheory.AddMon D)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_unop_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex Cᵒᵖ), S.unop.Exact ↔ S.Exact
-- Mathlib.Computability.Encoding
/-- An `Encoding` of `Bool` in `Bool`.  -/
Computability.encodingBoolBool : Computability.Encoding Bool Bool
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A}
  {x : A}, x ∈ S.toSubsemiring ↔ x ∈ S
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.fst_mapId_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (x : B × C),
  ((CategoryTheory.Bicategory.Prod.fst B C).mapId x).hom =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.1)
-- Init.Data.List.Sublist
List.prefix_replicate_iff : ∀ {α : Type u_1} {n : ℕ} {a : α} {l : List α}, l <+: List.replicate n a ↔ l.length ≤ n ∧ l = List.replicate l.length a
-- Mathlib.Data.Int.Log
Int.lt_zpow_succ_log_self : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, 1 < b → ∀ (r : R), r < ↑b ^ (Int.log b r + 1)
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_keys_eq_length : ∀ {α : Type u} {β : α → Type v} (l : List ((a : α) × β a)), (Std.Internal.List.keys l).length = l.length
-- Mathlib.Tactic.Widget.GCongr
/-- Display a widget panel allowing to generate a `gcongr` call with holes specified by selecting
subexpressions in the goal.  -/
tacticGcongr? : Lean.ParserDescr
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Topology.NhdsSet
subset_of_mem_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, t ∈ nhdsSet s → s ⊆ t
-- Mathlib.Topology.Neighborhoods
isOpen_iff_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsOpen s ↔ ∀ x ∈ s, nhds x ≤ Filter.principal s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.singleton_eq_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {p : α}, {p} = ∅.insert p
-- Init.Data.UInt.Lemmas
UInt64.toUSize_ofNatLT : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatLT n hn).toUSize = USize.ofNat n
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instIsScalarTower : ∀ (M : Type v) (N : Type w) (X : Type x) [inst : UniformSpace X] [inst_1 : SMul M X] [inst_2 : SMul N X]
  [inst_3 : SMul M N] [UniformContinuousConstSMul M X] [UniformContinuousConstSMul N X] [IsScalarTower M N X],
  IsScalarTower M N (UniformSpace.Completion X)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.subsingleton_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], Subsingleton (TopologicalSpace.Compacts α) ↔ IsEmpty α
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The image of an `AddSubsemigroup` along an `AddSemigroup` homomorphism is
an `AddSubsemigroup`.  -/
AddSubsemigroup.map : {M : Type u_1} → {N : Type u_2} → [inst : Add M] → [inst_1 : Add N] → (M →ₙ+ N) → AddSubsemigroup M → AddSubsemigroup N
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.pairwise_disjoint_supp_connectedComponent : ∀ {V : Type u} (G : SimpleGraph V), Pairwise fun c c' => Disjoint c.supp c'.supp
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.comap_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) (y : Y),
  Filter.comap (⇑h) (nhds y) = nhds (h.symm y)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `isCofinal_of_isCofinal_sUnion`. -/
Cardinal.unbounded_of_unbounded_sUnion : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set (Set α)},
  IsCofinal (⋃₀ s) → Cardinal.mk ↑s < Order.cof α → ∃ x ∈ s, IsCofinal x
-- Lean.Meta.Tactic.Grind.OrderInsts
Lean.Meta.Grind.mkIsLinearOrderInst? : Lean.Level → Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)