mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Graph.Basic
Graph.mk.sizeOf_spec : ∀ {α : Type u_3} {β : Type u_4} [inst : SizeOf α] [inst_1 : SizeOf β] (vertexSet : Set α) (IsLink : β → α → α → Prop)
  (edgeSet : Set β) (isLink_symm : ∀ ⦃e : β⦄, e ∈ edgeSet → Std.Symm (IsLink e))
  (eq_or_eq_of_isLink_of_isLink : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w)
  (edge_mem_iff_exists_isLink :
    autoParam (∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y) Graph.edge_mem_iff_exists_isLink._autoParam)
  (left_mem_of_isLink :
    autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet) Graph.left_mem_of_isLink._autoParam),
  sizeOf
      { vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink, left_mem_of_isLink := left_mem_of_isLink } =
    1
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddCommMonCat.FilteredColimits.colimitCoconeIsColimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommMonCat),
  AddCommMonCat.FilteredColimits.colimitCoconeIsColimit F =
    CategoryTheory.Limits.isColimitOfReflects (CategoryTheory.forget₂ AddCommMonCat AddMonCat)
      (AddMonCat.FilteredColimits.colimitCoconeIsColimit (F.comp (CategoryTheory.forget₂ AddCommMonCat AddMonCat)))
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_tmul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (g : E →L[𝕜] F) (m : G) (n : E),
  (ContinuousLinearMap.lTensor G g) (m ⊗ₜ[𝕜] n) = m ⊗ₜ[𝕜] g n
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.InducingFunctorData.whiskerRight_eq : ∀ {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.MonoidalCategoryStruct D]
  {F : CategoryTheory.Functor D C} (self : CategoryTheory.Monoidal.InducingFunctorData F) {X₁ X₂ : D} (f : X₁ ⟶ X₂)
  (Y : D),
  F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y) =
    CategoryTheory.CategoryStruct.comp (self.μIso X₁ Y).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj Y))
        (self.μIso X₂ Y).hom)
-- Mathlib.Analysis.Normed.Algebra.Exponential
Pi.coe_exp : ∀ {ι : Type u_3} {𝔸 : ι → Type u_4} [Finite ι] [inst : (i : ι) → NormedRing (𝔸 i)] [(i : ι) → NormedAlgebra ℚ (𝔸 i)]
  [∀ (i : ι), CompleteSpace (𝔸 i)] (x : (i : ι) → 𝔸 i) (i : ι), NormedSpace.exp x i = NormedSpace.exp (x i)
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapRange_finsetSum : ∀ {α : Type u_1} {ι : Type u_4} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  {F : Type u_12} [inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] (f : F) (s : Finset ι) (g : ι → α →₀ M),
  Finsupp.mapRange ⇑f ⋯ (∑ x ∈ s, g x) = ∑ x ∈ s, Finsupp.mapRange ⇑f ⋯ (g x)
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.reflection.congr_simp : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s s_1 : AffineSubspace 𝕜 P)
  (e_s : s = s_1) [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection],
  EuclideanGeometry.reflection s = EuclideanGeometry.reflection s_1
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.mk : {X : SSet} →
  {n : ℕ} →
    (concat :
        (x : X.obj (Opposite.op { len := 1 })) →
          (s : X.obj (Opposite.op { len := n })) →
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
                (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s →
              X.obj (Opposite.op { len := n + 1 })) →
      (∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
          (h :
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
              (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
          (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) (concat x s h) = x) →
        (∀ (x : X.obj (Opposite.op { len := 1 })) (s : X.obj (Opposite.op { len := n }))
            (h :
              (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
                (CategoryTheory.ConcreteCategory.hom (X.map ({ len := 0 }.const { len := n } 0).op)) s),
            (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) (concat x s h) = s) →
          (∀ {x y : X.obj (Opposite.op { len := n + 1 })},
              (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) x =
                  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc 0).op)) y →
                (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) x =
                    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ X 0)) y →
                  x = y) →
            X.StrictSegalCore n
-- Mathlib.Algebra.Ring.Parity
Nat.odd_iff : ∀ {n : ℕ}, Odd n ↔ n % 2 = 1
-- Mathlib.Analysis.Normed.Lp.LpEquiv
/-- The canonical `AddEquiv` between `lp E p` and `PiLp p E` when `E : α → Type u` with
`[Finite α]`.  -/
AddEquiv.lpPiLp : {α : Type u_1} →
  {E : α → Type u_2} → [inst : (i : α) → NormedAddCommGroup (E i)] → {p : ENNReal} → [Finite α] → ↥(lp E p) ≃+ PiLp p E
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_union_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k fallback : α}, m₁.contains k = false → (m₁.union m₂).getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The image of a subring along a ring homomorphism is a subring.  -/
Subring.map : {R : Type u} → {S : Type v} → [inst : NonAssocRing R] → [inst_1 : NonAssocRing S] → (R →+* S) → Subring R → Subring S
-- Mathlib.Topology.UniformSpace.Ultra.Basic
IsUltraUniformity.mk_of_hasBasis : ∀ {X : Type u_1} [inst : UniformSpace X] {ι : Type u_2} {p : ι → Prop} {s : ι → SetRel X X},
  (uniformity X).HasBasis p s → (∀ (i : ι), p i → (s i).IsSymm) → (∀ (i : ι), p i → (s i).IsTrans) → IsUltraUniformity X
-- Init.Data.UInt.IntToBitVec
UInt64.toBitVec32_toUSize : ∀ (n : UInt64) (h : System.Platform.numBits = 32), n.toUSize.toBitVec32 h = BitVec.setWidth 32 n.toBitVec
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.of_tendsto : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} {x : β},
  Filter.Tendsto f l (pure x) → Filter.EventuallyConst f l
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bsup_congr : ∀ {o₁ o₂ : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}) (ho : o₁ = o₂),
  o₁.bsup f = o₂.bsup fun a h => f a ⋯
-- Std.Net.Addr
Std.Net.SocketAddressV6.addr : Std.Net.SocketAddressV6 → Std.Net.IPv6Addr
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_zero_iff`. -/
ModularForm.coe_eq_zero_iff : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β] (f : F), ⇑f = 0 ↔ f = 0
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2to1.trStmts₁.match_1.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (f : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k f q))
  (h_2 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k f q))
  (h_3 : (k : K) → (f : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k f q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (x : Turing.TM2.Stmt Γ Λ σ) → motive x),
  (match Turing.TM2.Stmt.branch a q₁ q₂ with
    | Turing.TM2.Stmt.push k f q => h_1 k f q
    | Turing.TM2.Stmt.peek k f q => h_2 k f q
    | Turing.TM2.Stmt.pop k f q => h_3 k f q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | x => h_6 x) =
    h_5 a q₁ q₂
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.support_scaleRoots_eq : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) {s : R},
  s ∈ nonZeroDivisors R → (p.scaleRoots s).support = p.support
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.nondegenerate_zero : ∀ (X : SSet), X.nonDegenerate 0 = Set.univ
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_le : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ H₃ : Subgroup G}, ⁅H₁, H₂⁆ ≤ H₃ ↔ ∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ H₃
-- Lean.Parser.Extension
/-- All builtin parser categories are Pratt's parsers  -/
_private.Lean.Parser.Extension.0.Lean.Parser.addBuiltinParserCategory : Lean.Name → Lean.Name → Lean.Parser.LeadingIdentBehavior → IO Unit
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.X_dvd_mul_iff : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {i : σ} {p q : MvPolynomial σ R} [IsCancelMulZero R],
  MvPolynomial.X i ∣ p * q ↔ MvPolynomial.X i ∣ p ∨ MvPolynomial.X i ∣ q
-- Mathlib.CategoryTheory.Sites.LocalSite
CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] [inst_2 : J.IsLocalSite] (A : Type u')
  [inst_3 : CategoryTheory.Category.{v', u'} A] [inst_4 : CategoryTheory.Limits.HasProducts A],
  CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A =
    (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).skyscraperSheafFunctor
-- Mathlib.Order.BoundedOrder.Lattice
sup_bot_eq : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (a : α), a ⊔ ⊥ = a
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.instSeminormedRing : {α : Type u_2} → [SeminormedRing α] → SeminormedRing αᵐᵒᵖ
-- Batteries.Recycling.RBTree.Basic
/-- Run monadic function `f` on each element of the tree (in increasing order).  -/
RBTree.RBNode.forM : {m : Type u_1 → Type u_2} → {α : Type u_3} → [Monad m] → (α → m PUnit.{u_1 + 1}) → RBTree.RBNode α → m PUnit.{u_1 + 1}
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemTag.ofNat_ctorIdx : ∀ (x : Lean.Lsp.CompletionItemTag), Lean.Lsp.CompletionItemTag.ofNat x.ctorIdx = x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- The infinite sum of `k`-th iterated derivative of the complex exponential multiplied by a
function that grows polynomially is absolutely and uniformly convergent.  -/
summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp : ∀ (k l : ℕ) {f : ℕ → ℂ} {p : ℝ},
  0 < p →
    (f =O[Filter.atTop] fun n => ↑n ^ l) →
      SummableLocallyUniformlyOn
        (fun n =>
          f n •
            iteratedDerivWithin k (fun z => Complex.exp (2 * ↑Real.pi * Complex.I * z / ↑p) ^ n)
              UpperHalfPlane.upperHalfPlaneSet)
        UpperHalfPlane.upperHalfPlaneSet
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsModuleFiltration.toGradedSMul : ∀ {ι : Type u_1} {ιM : Type u_2} {R : Type u_3} {M : Type u_4} {σ : Type u_5} {σM : Type u_6} {inst : AddMonoid ι}
  {inst_1 : PartialOrder ι} {inst_2 : PartialOrder ιM} {inst_3 : VAdd ι ιM} {inst_4 : Preorder σ} {inst_5 : Semiring R}
  {inst_6 : SetLike σ R} {inst_7 : Preorder σM} {inst_8 : AddCommMonoid M} {inst_9 : Module R M}
  {inst_10 : SetLike σM M} {F : ι → σ} {F_lt : outParam (ι → σ)} {inst_11 : IsRingFiltration F F_lt} {F' : ιM → σM}
  {F'_lt : outParam (ιM → σM)} [self : IsModuleFiltration F F_lt F' F'_lt], SetLike.GradedSMul F F'
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.BirationalOver.trans : ∀ {S X Y Z : AlgebraicGeometry.Scheme} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S},
  AlgebraicGeometry.Scheme.BirationalOver sX sY →
    AlgebraicGeometry.Scheme.BirationalOver sY sZ → AlgebraicGeometry.Scheme.BirationalOver sX sZ
-- Mathlib.Tactic.Positivity.Core
/-- Converts a `MetaM Strictness` which can fail
into one that never fails and returns `.none` instead.  -/
Mathlib.Meta.Positivity.catchNone : {u : Lean.Level} →
  {α : Q(Type u)} →
    {zα : Q(Zero «$α»)} →
      {e : Q(«$α»)} →
        {pα? : Option Q(PartialOrder «$α»)} →
          Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?) →
            Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.hasSum_one_geometricMeasure : ∀ {p : ↑unitInterval}, p ≠ 0 → HasSum (fun n => (1 - ↑p) ^ n * ↑p) 1
-- Mathlib.Analysis.Calculus.ImplicitFunction.ProdDomain
HasStrictFDerivAt.implicitFunctionOfProdDomain.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂]
  [inst_5 : NormedSpace 𝕜 E₂] [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : CompleteSpace F] {u u_1 : E₁ × E₂} (e_u : u = u_1) {f f_1 : E₁ × E₂ → F}
  (e_f : f = f_1) {f'u f'u_1 : E₁ × E₂ →L[𝕜] F} (e_f'u : f'u = f'u_1) (dfu : HasStrictFDerivAt f f'u u)
  (if₂u : (f'u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible) (a a_1 : E₁),
  a = a_1 → dfu.implicitFunctionOfProdDomain if₂u a = ⋯.implicitFunctionOfProdDomain ⋯ a_1
-- Mathlib.Order.SupClosed
SupClosed.biSup_mem : ∀ {α : Type u_3} [inst : CompleteLattice α] {s : Set α} {ι : Type u_5} {t : Set ι} {f : ι → α},
  SupClosed s → t.Finite → ⊥ ∈ s → (∀ i ∈ t, f i ∈ s) → ⨆ i ∈ t, f i ∈ s
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- `(F'Uε_X, otherMap X)` is a reflexive pair: in particular if `A` has reflexive coequalizers then
this pair has a coequalizer.
 -/
CategoryTheory.LiftLeftAdjoint.instIsReflexivePairMapAppCounitOtherMap : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {U : CategoryTheory.Functor B C} {F : CategoryTheory.Functor C B} (R : CategoryTheory.Functor A B)
  (F' : CategoryTheory.Functor C A) (adj₁ : F ⊣ U) (adj₂ : F' ⊣ R.comp U) (X : B),
  CategoryTheory.IsReflexivePair (F'.map (U.map (adj₁.counit.app X)))
    (CategoryTheory.LiftLeftAdjoint.otherMap R F' adj₁ adj₂ X)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The weights for the reflection of the circumcenter in an edge of a
simplex.  This definition is only valid with `i₁ ≠ i₂`.  -/
Affine.Simplex.reflectionCircumcenterWeightsWithCircumcenter : {n : ℕ} → Fin (n + 1) → Fin (n + 1) → Affine.Simplex.PointsWithCircumcenterIndex n → ℝ
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.coveringNumber_anti : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε δ : NNReal},
  ε ≤ δ → Metric.coveringNumber δ A ≤ Metric.coveringNumber ε A
-- Init.Omega.Int
Lean.Omega.Int.mul_congr_left : ∀ {a b : ℤ}, a = b → ∀ (c : ℤ), a * c = b * c
-- Mathlib.Topology.Order.T5
/-- A linear order with order topology is a completely normal Hausdorff topological space.  -/
OrderTopology.completelyNormalSpace : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X], CompletelyNormalSpace X
-- Mathlib.Data.List.Lattice
List.singleton_bagInter : ∀ {α : Type u_1} {l₁ : List α} [inst : DecidableEq α] (a : α), [a].bagInter l₁ = if a ∈ l₁ then [a] else []
-- Mathlib.MeasureTheory.Group.Arithmetic
Multiset.measurable_fun_sum : ∀ {M : Type u_2} {α : Type u_4} [inst : AddCommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} (s : Multiset (α → M)),
  (∀ f ∈ s, Measurable f) → Measurable fun x => (Multiset.map (fun f => f x) s).sum
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertList.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l toInsert : List ((a : α) × β a)),
  Std.Internal.List.insertList l toInsert =
    match toInsert with
    | [] => l
    | ⟨k, v⟩ :: toInsert => Std.Internal.List.insertList (Std.Internal.List.insertEntry k v l) toInsert
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.allM.eq_2 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool) (a : α) (as : List α),
  List.allM p (a :: as) = do
    let __do_lift ← p a
    match __do_lift with
      | true => List.allM p as
      | false => pure false
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.val_step_takeWhile.match_3.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder c) = 1 + sizeOf c
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).getKey! k = if k ∈ m₂ then default else m₁.getKey! k
-- Mathlib.Data.PFunctor.Multivariate.W
/-- Constructor for `W`  -/
MvPFunctor.wMk : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) → {α : TypeVec.{u} n} → (a : P.A) → (P.drop.B a).Arrow α → (P.last.B a → P.W α) → P.W α
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- The inverse of `f : LinearPMap` is closed if and only if `f` is closed.  -/
LinearPMap.inverse_closed_iff : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  {f : E →ₗ.[R] F}, f.toFun.ker = ⊥ → (f.inverse.IsClosed ↔ f.IsClosed)
-- Init.Data.UInt.Lemmas
UInt32.ofNat_lt_iff : ∀ {n : UInt32} {m : ℕ}, m < UInt32.size → (UInt32.ofNat m < n ↔ m < n.toNat)
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuous.isOpen_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → β} [inst_1 : Preorder β],
  UpperSemicontinuous f → ∀ (y : β), IsOpen (f ⁻¹' Set.Iio y)
-- Aesop.Tree.Data
Aesop.RappId.mk.sizeOf_spec : ∀ (toNat : ℕ), sizeOf { toNat := toNat } = 1 + sizeOf toNat
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.denote.match_1.eq_1 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (match Lean.Grind.Linarith.Poly.nil with
    | Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add k v p => h_2 k v p) =
    h_1 ()
-- Lean.Meta.Tactic.Grind.CollectParams
_private.Lean.Meta.Tactic.Grind.CollectParams.0.Lean.Meta.Grind.Collector.pushParam : Lean.Meta.Grind.TParam → Lean.Meta.Grind.Collector.Collect✝ Unit
-- Mathlib.Algebra.Order.Field.Basic
abs_inv : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α), |a⁻¹| = |a|⁻¹
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- If `G : Cocone F ⥤ Cocone F'` preserves initial objects, it preserves colimit cocones.  -/
CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {D : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                {F : CategoryTheory.Functor J C} →
                  {F' : CategoryTheory.Functor K D} →
                    (G : CategoryTheory.Functor (CategoryTheory.Limits.Cocone F) (CategoryTheory.Limits.Cocone F')) →
                      [CategoryTheory.Limits.PreservesColimit
                            (CategoryTheory.Functor.empty (CategoryTheory.Limits.Cocone F)) G] →
                        {c : CategoryTheory.Limits.Cocone F} →
                          CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit (G.obj c)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddGroup.addConjugatesOfSet_mono : ∀ {G : Type u_1} [inst : AddGroup G] {s t : Set G},
  s ⊆ t → AddGroup.addConjugatesOfSet s ⊆ AddGroup.addConjugatesOfSet t
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- `MultilinearMap.domDomCongr` as a `LinearEquiv`.  -/
MultilinearMap.domDomCongrLinearEquiv : (R : Type uR) →
  (S : Type uS) →
    (M₂ : Type v₂) →
      (M₃ : Type v₃) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : Module R M₂] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M₃] →
                  [inst_5 : Module S M₃] →
                    [inst_6 : Module R M₃] →
                      [inst_7 : SMulCommClass R S M₃] →
                        {ι₁ : Type u_1} →
                          {ι₂ : Type u_2} →
                            ι₁ ≃ ι₂ → MultilinearMap R (fun x => M₂) M₃ ≃ₗ[S] MultilinearMap R (fun x => M₂) M₃
-- Lean.Server.References
/-- References loaded from ilean files  -/
Lean.Server.References.ileans : Lean.Server.References → Lean.Server.ILeanMap
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
pinGroup.coe_star : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : ↥(pinGroup Q)}, ↑(star x) = star ↑x
-- Mathlib.Analysis.Complex.Tietze
Set.instTietzeExtensionUnitBall : ∀ {𝕜 : Type v} [inst : RCLike 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [FiniteDimensional 𝕜 E], TietzeExtension ↑(Metric.ball 0 1)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.inv_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c)
  [inst_1 : CategoryTheory.IsIso η],
  CategoryTheory.inv (CategoryTheory.Bicategory.whiskerRight η h) =
    CategoryTheory.Bicategory.whiskerRight (CategoryTheory.inv η) h
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_one : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, (f.genEigenspace μ) 1 = (f - μ • 1).ker
-- Mathlib.Order.Sublattice
Sublattice.map_iSup : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β)
  (L : ι → Sublattice α), Sublattice.map f (⨆ i, L i) = ⨆ i, Sublattice.map f (L i)