mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.val : Lean.Elab.Term.LetRecToLift → Lean.Expr
-- Mathlib.Algebra.Order.Field.Basic
/-- **Alias** of the reverse direction of `half_lt_self_iff`. -/
half_lt_self : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  0 < a → a / 2 < a
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.setIntegral : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsCondKernelCDF f κ ν →
    ∀ (a : α) {s : Set β}, MeasurableSet s → ∀ (x : ℝ), ∫ (b : β) in s, ↑(f (a, b)) x ∂ν a = (κ a).real (s ×ˢ Set.Iic x)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.bsize : ∀ {s : Substring.Raw}, s.Valid → s.bsize = String.utf8Len s.toString.toList
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.max_sum_le : ∀ {α : Type u_2} {M : Type u_3} [inst : AddMonoid M] (l : List α) (f g : α → M) [inst_1 : LinearOrder M] [AddLeftMono M]
  [AddRightMono M], max (List.map f l).sum (List.map g l).sum ≤ (List.map (fun i => max (f i) (g i)) l).sum
-- Mathlib.Order.ULift
ULift.instTransOrd_mathlib : ∀ {α : Type u} [inst : Ord α] [inst_1 : Std.TransOrd α], Std.TransOrd (ULift.{v, u} α)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_of_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α}, m.isEmpty = true → Std.DHashMap.Const.get? m a = none
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsCofibrantResolutionObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C)
  [HomotopicalAlgebra.IsCofibrant X],
  HomotopicalAlgebra.IsCofibrant (HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj X)
-- Mathlib.RepresentationTheory.Invariants
/-- The functor sending a representation to its submodule of invariants.  -/
Rep.invariantsFunctor : (k : Type u) →
  (G : Type v) → [inst : CommRing k] → [inst_1 : Group G] → CategoryTheory.Functor (Rep.{w, u, v} k G) (ModuleCat k)
-- Mathlib.NumberTheory.SmoothNumbers
/-- The product of two `n`-smooth numbers is an `n`-smooth number.  -/
Nat.mul_mem_smoothNumbers : ∀ {m₁ m₂ n : ℕ}, m₁ ∈ n.smoothNumbers → m₂ ∈ n.smoothNumbers → m₁ * m₂ ∈ n.smoothNumbers
-- Lean.Data.Json.Basic
Lean.Json.getInt? : Lean.Json → Except String ℤ
-- Std.Http.Data.Chunk
/-- The extension value string.
 -/
Std.Http.Chunk.ExtensionValue.value : Std.Http.Chunk.ExtensionValue → String
-- Mathlib.FieldTheory.Perfect
PerfectRing.mul : ∀ (M : Type u_1) (p q : ℕ) [inst : CommMonoid M] [PerfectRing M p] [PerfectRing M q], PerfectRing M (p * q)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile
Std.IterM.takeWhileWithPostcondition.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} (P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool))
  (it : Std.IterM m β), Std.IterM.takeWhileWithPostcondition P it = { internalState := { inner := it } }
-- Lean.Parser.Term
/-- A `sufficesDecl` represents everything that comes after the `suffices` keyword:
an optional `x :`, then a term `ty`, then `from val` or `by tac`.  -/
Lean.Parser.Term.sufficesDecl : Lean.Parser.Parser
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.eval_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h : a ⟶ b} {η η' : f ⟶ g} {θ θ' : g ⟶ h} {ι : f ⟶ h},
  η = η' → θ = θ' → CategoryTheory.CategoryStruct.comp η' θ' = ι → CategoryTheory.CategoryStruct.comp η θ = ι
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Metric.exists_isCompact_closedBall : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] [WeaklyLocallyCompactSpace α] (x : α),
  ∃ r, 0 < r ∧ IsCompact (Metric.closedBall x r)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.π
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) h₂.ι) =
    CategoryTheory.CategoryStruct.comp h₁.i h₂.p
-- Mathlib.Topology.ContinuousMap.Bounded.Star
BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply : ∀ {α : Type u} {β : Type v} (𝕜 : Type u_2) [inst : NormedField 𝕜] [inst_1 : TopologicalSpace α] [inst_2 : NormedRing β]
  [inst_3 : NormedAlgebra 𝕜 β] [inst_4 : StarAddMonoid β] [inst_5 : NormedStarGroup β]
  (f : BoundedContinuousFunction α β) (a : α), ((BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) f) a = f a
-- Mathlib.Algebra.Order.Monovary
monovary_neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {f : ι → α} {g : ι → β},
  Monovary (-f) (-g) ↔ Monovary f g
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.evaluation_naturality_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) {V : TopologicalSpace.Opens ↑Y.toTopCat}
  (x : ↥((TopologicalSpace.Opens.map f.base).obj V)) {Z : CommRingCat} (h : X.residueField ↑x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.evaluation ⟨(CategoryTheory.ConcreteCategory.hom f.base) ↑x, ⋯⟩)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.residueFieldMap f ↑x) h) =
    CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op V)) (CategoryTheory.CategoryStruct.comp (X.evaluation x) h)
-- Mathlib.Order.Sublattice
Sublattice.mem_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {f : LatticeHom α β} {a : α} {L : Sublattice β},
  a ∈ Sublattice.comap f L ↔ f a ∈ L
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- A polynomial equipped with a chain of rewrite steps that justifies its equality to the original input.
From an input polynomial `p`, we use equations (i.e., `EqCnstr`) as rewriting rules.
For example, consider the following sequence of rewrites for the input polynomial `x^2 + x*y`
using the equations `x - 1 = 0` (`c₁`) and `y - 2 = 0` (`c₂`).
```
2*x^2 + x*y                  | s₁ := .input (2*x^2 + x*y)
=           - 2*x*(x - 1)
(2*x + x*y)                  | s₂ := .step (2*x + x*y)  1 s₁ (-2) x c₁
=           - 2*1*(x - 1)
(x*y + 2)                    | s₃ := .step (x*y + 2) 1 s₂ (-2) 1 c₁
=           - 1*y*(x - 1)
(y + 2)                      | s₄ := .step (y+2) 1 s₃ (-1) y c₁
=           - 1*1*(y - 2)
4                            | s₅ := .step 4 1 s₄ 1 1 c₂
```
From the chain above, we build the certificate
```
(-2*x - y - 2)*(x-1) + (-1)*(y-2)
```
for
```
4 = (2*x^2 + x*y)
```
because `x-1 = 0` and `y-2=0`
 -/
Lean.Meta.Grind.Arith.CommRing.PolyDerivation : Type
-- Init.Data.ToString.Basic
instToStringString : ToString String
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.measurable_invFun : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β}
  [inst_2 : Nonempty α] (hf : MeasurableEmbedding f), Measurable hf.invFun
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Run a computation in the `OmegaM` monad, starting with no recorded atoms.  -/
Lean.Elab.Tactic.Omega.OmegaM.run : {α : Type} → Lean.Elab.Tactic.Omega.OmegaM α → Lean.Meta.Omega.OmegaConfig → Lean.MetaM α
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pullbackConeEquivBinaryFan_inverse_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X}
  (c : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)),
  CategoryTheory.Limits.pullbackConeEquivBinaryFan.inverse.obj c =
    CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left c.fst) (CategoryTheory.Over.Hom.left c.snd) ⋯
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₂.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (app₀ app₀_1 : f.obj' 0 _proof_245✝ ⟶ g.obj' 0 _proof_245✝) (e_app₀ : app₀ = app₀_1)
  (app₁ app₁_1 : f.obj' 1 _proof_246✝ ⟶ g.obj' 1 _proof_246✝) (e_app₁ : app₁ = app₁_1)
  (app₂ app₂_1 : f.obj' 2 _proof_247✝ ⟶ g.obj' 2 _proof_247✝) (e_app₂ : app₂ = app₂_1)
  (w₀ :
    CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝) app₁ =
      CategoryTheory.CategoryStruct.comp app₀ (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
  (w₁ :
    CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂ =
      CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_247✝)),
  CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁ =
    CategoryTheory.ComposableArrows.homMk₂ app₀_1 app₁_1 app₂_1 ⋯ ⋯
-- Init.Data.Int.Lemmas
Int.add_right_inj : ∀ {i j : ℤ} (k : ℤ), k + i = k + j ↔ i = j
-- Mathlib.Analysis.Convex.Radon
/-- **Helly's theorem** for finite families of convex sets in its classical form.

If `F` is a family of `n` convex sets in a vector space of finite dimension `d`, with `n ≥ d + 1`,
and any `d + 1` sets of `F` intersect nontrivially, then all sets of `F` intersect nontrivially.  -/
Convex.helly_theorem : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [FiniteDimensional 𝕜 E] {F : ι → Set E} {s : Finset ι},
  Module.finrank 𝕜 E + 1 ≤ s.card →
    (∀ i ∈ s, Convex 𝕜 (F i)) →
      (∀ I ⊆ s, I.card = Module.finrank 𝕜 E + 1 → (⋂ i ∈ I, F i).Nonempty) → (⋂ i ∈ s, F i).Nonempty
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncLT : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt), (t.eTruncLT.obj i).Additive
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The subsemigroup `M` of the magma `M`.  -/
Subsemigroup.instTop : {M : Type u_1} → [inst : Mul M] → Top (Subsemigroup M)
-- Std.Data.HashSet.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.HashSet.all : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → Std.HashSet α → (α → Bool) → Bool
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.ImportData.errors : Lean.Meta.LazyDiscrTree.ImportData → IO.Ref (Array Lean.Meta.LazyDiscrTree.ImportFailure)
-- Mathlib.Data.PFun
Part.restrict.congr_simp : ∀ {α : Type u_1} (p p_1 : Prop) (e_p : p = p_1) (o o_1 : Part α) (e_o : o = o_1) (H : p → o.Dom),
  Part.restrict p o H = Part.restrict p_1 o_1 ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k : α} {h' : k ∈ Std.ExtDTreeMap.Const.insertManyIfNewUnit t l} (contains : k ∈ t),
  (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).getKey k h' = t.getKey k contains
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minEntry?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (xs : List ((a : α) × β a)), Std.Internal.List.minEntry? xs = xs.min?
-- Mathlib.CategoryTheory.Enriched.Basic
/-- A type synonym for `C`, which should come equipped with a `V`-enriched category structure.
In a moment we will equip this with the `W`-enriched category structure
obtained by applying the functor `F : LaxMonoidalFunctor V W` to each hom object.
 -/
CategoryTheory.TransportEnrichment : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {W : Type v'} →
        [inst_2 : CategoryTheory.Category.{w', v'} W] →
          [inst_3 : CategoryTheory.MonoidalCategory W] →
            (F : CategoryTheory.Functor V W) → [F.LaxMonoidal] → Type u₁ → Type u₁
-- Mathlib.Analysis.Convex.Between
sbtw_const_add_iff : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V} (v : V), Sbtw R (v + x) (v + y) (v + z) ↔ Sbtw R x y z
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- Two finite Borel measures are equal if the integrals of all non-negative bounded continuous
functions with respect to both agree.  -/
MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω] [BorelSpace Ω]
  {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  (∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν) → μ = ν
-- Mathlib.Data.Matrix.Basis
Matrix.liftLinear.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} {β : Type u_8} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Semiring R] [inst_5 : Semiring S]
  [inst_6 : AddCommMonoid α] [inst_7 : AddCommMonoid β] [inst_8 : Module R α] [inst_9 : Module R β]
  [inst_10 : Module S β] [inst_11 : SMulCommClass R S β],
  Matrix.liftLinear S =
    (LinearEquiv.piCongrRight fun x => LinearMap.lsum R (fun a => α) S) ≪≫ₗ LinearMap.lsum R (fun i => n → α) S ≪≫ₗ
      LinearEquiv.congrLeft β S (Matrix.ofLinearEquiv R)
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.inv_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (e : F ≅ G) (X : C), CategoryTheory.inv (e.hom.app X) = e.inv.app X
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.hsum.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α), s.hsum = { coeff := fun g => ∑ᶠ (i : α), (s i).coeff g, isPWO_support' := ⋯ }
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_range_map_map : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  Submodule.map (ExteriorAlgebra.map f).toLinearMap (ExteriorAlgebra.ι R).range =
    Submodule.map (ExteriorAlgebra.ι R) f.range
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS_toPolyS_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (e : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Poly.denoteS ctx e.toPolyS_nc = Lean.Grind.CommRing.Expr.denoteS ctx e
-- Mathlib.Data.List.Zip
List.reverse_revzip : ∀ {α : Type u} (l : List α), l.revzip.reverse = l.reverse.revzip
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_div_const_uIcc : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α},
  a ≠ 0 → ∀ (b c : α), (fun x => x / a) ⁻¹' Set.uIcc b c = Set.uIcc (b * a) (c * a)
-- Batteries.Data.AssocList
/-- Returns true if every entry in the list satisfies `p`.  -/
Batteries.AssocList.All : {α : Type u_1} → {β : Type u_2} → (α → β → Prop) → Batteries.AssocList α β → Prop
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instMonoFKernelSequenceCyclesE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₂₃ : i₁ ⟶ i₃) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ) (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂), CategoryTheory.Mono (X.kernelSequenceCyclesE f₁ f₂ f₃ f₂₃ h₂₃ n₀ n₁ n₂ hn₁ hn₂).f
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.finTwoArrow_symm_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X], ⇑Homeomorph.finTwoArrow.symm = fun x => ![x.1, x.2]
-- Init.Data.Array.Lemmas
Array.back_filter_of_pos : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} (w : 0 < xs.size) (h : p (xs.back w) = true),
  (Array.filter p xs).back ⋯ = xs.back w
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {l : List α} {k : α}, k ∉ m → l.contains k = false → (m.insertMany l).get! k = default
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_one : UInt16.toBitVec 1 = 1#16
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_lt_top_iff : ∀ {a b : ENNReal}, a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_castAddEmb_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.castAddEmb m) (Finset.Icc i j) = Finset.Icc (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.isSubterminal_of_isTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  CategoryTheory.IsSubterminal T
-- Init.Data.Order.Classes
Std.LawfulOrderLeftLeaningMax.mk : ∀ {α : Type u} [inst : Max α] [inst_1 : LE α],
  (∀ (a b : α), b ≤ a → a ⊔ b = a) → (∀ (a b : α), ¬b ≤ a → a ⊔ b = b) → Std.LawfulOrderLeftLeaningMax α
-- Lean.MetavarContext
Lean.MetavarContext.isAnonymousMVar : Lean.MetavarContext → Lean.MVarId → Bool
-- Mathlib.RingTheory.TensorProduct.IsBaseChangeHom
IsBaseChange.linearMapLeftRightHom_toMatrix : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {P : Type u_5} [inst_7 : AddCommMonoid P] [inst_8 : Module R P] {Q : Type u_6} [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] [inst_11 : Module S P] [inst_12 : IsScalarTower R S P] [inst_13 : Module S Q]
  [inst_14 : IsScalarTower R S Q] {α : M →ₗ[R] P} {β : N →ₗ[R] Q} (ibcM : IsBaseChange S α) (ibcN : IsBaseChange S β)
  {ι : Type u_7} {θ : Type u_8} [inst_15 : DecidableEq ι] [inst_16 : Fintype ι] [inst_17 : Finite θ]
  (b : Module.Basis ι R M) (c : Module.Basis θ R N) (f : M →ₗ[R] N),
  (LinearMap.toMatrix (IsBaseChange.basis b ibcM) (IsBaseChange.basis c ibcN)) ((ibcM.linearMapLeftRightHom β) f) =
    ((LinearMap.toMatrix b c) f).map ⇑(algebraMap R S)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is algebraic, then `E` is purely inseparable over the
separable closure of `F` in `E`.  -/
separableClosure.isPurelyInseparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsAlgebraic F E],
  IsPurelyInseparable (↥(separableClosure F E)) E
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.MkPreResultResult.success.sizeOf_spec : ∀ (mvarsToCheckType instMVars : Array Lean.MVarId),
  sizeOf (Lean.Meta.Sym.MkPreResultResult.success✝ mvarsToCheckType instMVars) =
    1 + sizeOf mvarsToCheckType + sizeOf instMVars
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressParams.mk : Option Lean.Lsp.ProgressToken → Lean.Lsp.WorkDoneProgressParams
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm
/-- Extract the certificate from the `vec` found by `Linarith.SimplexAlgorithm.findPositiveVector`.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.postprocess : Array ℚ → Std.HashMap ℕ ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.ofSigmaCoforkFunctor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  {K₁ K₂ : CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc)} (f : K₁ ⟶ K₂),
  ((I.ofSigmaCoforkFunctor hc).map f).hom = f.hom
-- Mathlib.Condensed.Functors
instFaithfulCompHausCondensedSetCompHausToCondensed : compHausToCondensed.Faithful
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {f : σ → R} (n : ℕ),
  (MvPolynomial.eval f) (p ^ n) = (MvPolynomial.eval f) p ^ n
-- Mathlib.Order.KrullDimension
Order.krullDim_le_one_iff_forall_isMin : ∀ {α : Type u_3} [inst : PartialOrder α] [inst_1 : OrderTop α], Order.krullDim α ≤ 1 ↔ ∀ (x : α), x ≠ ⊤ → IsMin x
-- Mathlib.Topology.Sober
genericPoints.closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSober α], closure (genericPoints α) = Set.univ
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.add_pos : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g : CauSeq α abs},
  f.Pos → g.Pos → (f + g).Pos
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.equivalenceOfIsTerminal_unitIso : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.Over.equivalenceOfIsTerminal hX).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun Y =>
        CategoryTheory.Over.isoMk
          (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Over X)).obj Y).left) ⋯)
      ⋯
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
/-- The distance between any two adjacent vertices is 1.  -/
SimpleGraph.UnitDistEmbedding.unit_dist : ∀ {V : Type u_1} {G : SimpleGraph V} {E : Type u_3} [inst : MetricSpace E] (self : G.UnitDistEmbedding E) {u v : V},
  G.Adj u v → dist (self.p u) (self.p v) = 1
-- Mathlib.Data.Matrix.DMatrix
DMatrix.map_sub : ∀ {m : Type u_1} {n : Type u_2} {α : m → n → Type v} [inst : (i : m) → (j : n) → AddGroup (α i j)] {β : m → n → Type w}
  [inst_1 : (i : m) → (j : n) → AddGroup (β i j)] (f : ⦃i : m⦄ → ⦃j : n⦄ → α i j →+ β i j) (M N : DMatrix m n α),
  ((M - N).map fun i j => ⇑f) = (M.map fun i j => ⇑f) - N.map fun i j => ⇑f
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- If for every cell either `A ∩ openCell n j` is empty or `A ∩ closedCell n j` is closed then
`A` is closed.  -/
Topology.CWComplex.isClosed_of_disjoint_openCell_or_isClosed_inter_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : Topology.CWComplex C] [T2Space X] {A : Set X},
  A ⊆ C →
    (∀ (n : ℕ),
        0 < n →
          ∀ (j : Topology.RelCWComplex.cell C n),
            Disjoint A (Topology.RelCWComplex.openCell n j) ∨ IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) →
      IsClosed A
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.finMeasSupp_iff : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : Zero β] {μ : MeasureTheory.Measure α}
  {f : MeasureTheory.SimpleFunc α β}, f.FinMeasSupp μ ↔ ∀ (y : β), y ≠ 0 → μ (⇑f ⁻¹' {y}) < ⊤
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Turn a bijection `γ ≃ α` into a uniform isomorphism
`(γ →ᵤ β) ≃ᵤ (α →ᵤ β)` by pre-composing.  -/
UniformFun.congrLeft : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → [inst : UniformSpace β] → γ ≃ α → UniformFun γ β ≃ᵤ UniformFun α β
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- The unique eigenvalue of a parabolic matrix (junk if `m` is not parabolic).  -/
Matrix.parabolicEigenvalue : {K : Type u_1} → [Field K] → Matrix (Fin 2) (Fin 2) K → K