mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The sum of a function over `PointsWithCircumcenterIndex`.  -/
Affine.Simplex.sum_pointsWithCircumcenter : ∀ {α : Type u_3} [inst : AddCommMonoid α] {n : ℕ} (f : Affine.Simplex.PointsWithCircumcenterIndex n → α),
  ∑ i, f i =
    ∑ i, f (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex i) +
      f Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex
-- Mathlib.Topology.UniformSpace.Separation
isClosed_of_spaced_out : ∀ {α : Type u} [inst : UniformSpace α] [T0Space α] {V₀ : Set (α × α)},
  V₀ ∈ uniformity α → ∀ {s : Set α}, (s.Pairwise fun x y => (x, y) ∉ V₀) → IsClosed s
-- Init.Prelude
/-- Converts an `Array Syntax` to a `TSyntaxArray`, without reallocation.  -/
Lean.TSyntaxArray.mk : {ks : Lean.SyntaxNodeKinds} → Array Lean.Syntax → Lean.TSyntaxArray ks
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.IsZeroAtImInfty.cuspFunction_apply_zero : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ}, UpperHalfPlane.IsZeroAtImInfty f → 0 < h → UpperHalfPlane.cuspFunction h f 0 = 0
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue.0.MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk' : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : MeasureTheory.SignedMeasure α} (μ : MeasureTheory.Measure α)
  {f : α → ℝ},
  Measurable f →
    MeasureTheory.Integrable f μ →
      MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
        s = t + μ.withDensityᵥ f → s.HaveLebesgueDecomposition μ
-- Lean.LocalContext
Lean.LocalContext.setType : Lean.LocalContext → Lean.FVarId → Lean.Expr → Lean.LocalContext
-- Mathlib.Order.CompleteLattice.Basic
Antitone.le_map_iInf₂ : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_6} [inst : CompleteLattice α]
  [inst_1 : CompleteLattice β] {f : α → β},
  Antitone f → ∀ (s : (i : ι) → κ i → α), ⨆ i, ⨆ j, f (s i j) ≤ f (⨅ i, ⨅ j, s i j)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.mkLetRecClosures : Array Lean.Expr →
  Array Lean.FVarId →
    Array Lean.FVarId →
      Array Lean.Elab.Term.LetRecToLift → Lean.Elab.TermElabM (List Lean.Elab.Term.MutualClosure.LetRecClosure)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} RingCat
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.le_maxD_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → ∀ {fallback : α}, (cmp k (t.maxD fallback)).isLE = true
-- Std.Sat.AIG.Basic
/-- A `Ref` into `aig1` is also valid for `aig2` if `aig1` is smaller than `aig2`.
 -/
Std.Sat.AIG.Ref.cast : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig1 aig2 : Std.Sat.AIG α} → aig1.Ref → aig1.decls.size ≤ aig2.decls.size → aig2.Ref
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.instEffectiveEpiOfEffectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B X : C} (f : X ⟶ B)
  [CategoryTheory.EffectiveEpiFamily (fun x => X) fun x => f], CategoryTheory.EffectiveEpi f
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLEMk_comp_ofMkLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A : C} (X : CategoryTheory.Subobject B) (f : A ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (Y : CategoryTheory.Subobject B) (h₁ : X ≤ CategoryTheory.Subobject.mk f)
  (h₂ : CategoryTheory.Subobject.mk f ≤ Y),
  CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁) (CategoryTheory.Subobject.ofMkLE f Y h₂) = X.ofLE Y ⋯
-- Init.Data.Fin.Lemmas
Fin.succRecOn_zero : ∀ {motive : (n : ℕ) → Fin n → Sort u_1} {zero : (n : ℕ) → motive (n + 1) 0}
  {succ : (n : ℕ) → (i : Fin n) → motive n i → motive n.succ i.succ} (n : ℕ), Fin.succRecOn 0 zero succ = zero n
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableWithinAt_insert_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f (insert x s) x ↔ DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Algebra.Ring.TransferInstance
/-- An equivalence `e : α ≃ β` gives a ring equivalence `α ≃+* β`
where the ring structure on `α` is
the one obtained by transporting a ring structure on `β` back along `e`.
 -/
Equiv.ringEquiv : {α : Type u_1} →
  {β : Type u_2} →
    (e : α ≃ β) →
      [inst : Add β] →
        [inst_1 : Mul β] →
          have add := e.add;
          have mul := e.mul;
          α ≃+* β
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.Context : Type
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.comp_id : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), f.comp (MulHom.id M) = f
-- Lean.Util.Trace
Lean.modifyTraces : {m : Type → Type} →
  [Lean.MonadTrace m] → (Lean.PersistentArray Lean.TraceElem → Lean.PersistentArray Lean.TraceElem) → m Unit
-- Batteries.Tactic.Congr
/-- Recursive core of `rcongr`. Calls `ext pats <;> congr` and then itself recursively,
unless `ext pats <;> congr` made no progress.
 -/
Batteries.Tactic.rcongrCore : Lean.MVarId →
  Batteries.Tactic.Congr.Config →
    List (Lean.TSyntax `rcasesPat) → Array Lean.MVarId → Lean.Elab.TermElabM (Array Lean.MVarId)
-- Mathlib.GroupTheory.Transfer
/-- Given `ϕ : H →+ A` from `H : AddSubgroup G` to an additive commutative group `A`,
the transfer homomorphism is `transfer ϕ : G →+ A`.  -/
AddMonoidHom.transfer : {G : Type u_1} →
  [inst : AddGroup G] →
    {H : AddSubgroup G} → {A : Type u_2} → [inst_1 : AddCommGroup A] → (↥H →+ A) → [H.FiniteIndex] → G →+ A
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.min? = some k' → (cmp k k').isLE = true) ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Init.Data.List.Basic
List.filter.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α),
  List.filter p (a :: as) =
    match p a with
    | true => a :: List.filter p as
    | false => List.filter p as
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.ofPrime_bot : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K), A.ofPrime ⊥ = ⊤
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp],
  t.WF → ∀ {l : List (α × β)} {k : α}, (List.map Prod.fst l).contains k = false → (t.insertMany l)[k]? = t[k]?
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Limit.π_mk : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasLimit F] (x : (j : J) → F.obj j)
  (h : ∀ (j j' : J) (f : j ⟶ j'), (CategoryTheory.ConcreteCategory.hom (F.map f)) (x j) = x j') (j : J),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j))
      (CategoryTheory.Limits.Types.Limit.mk F x h) =
    x j
-- Mathlib.Data.Int.Init
Int.neg_eq_neg : ∀ {a b : ℤ}, -a = -b → a = b
-- Mathlib.Algebra.Order.Module.Defs
neg_of_smul_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : LinearOrder α] [inst_4 : LinearOrder β] [PosSMulMono α β] [SMulPosMono α β], 0 < a • b → b ≤ 0 → a < 0
-- Mathlib.Data.Num.Basic
/-- Modulus of `PosNum`s.  -/
PosNum.mod' : PosNum → PosNum → Num
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_modify_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : β → β}, m.WF → (m.modify k f)[k]? = Option.map f m[k]?
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The points in the affine span of a (possibly empty) set of points. Use `affineSpan` instead to
get an `AffineSubspace k P`.  -/
spanPoints : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} → [inst : Ring k] → [inst_1 : AddCommGroup V] → [Module k V] → [AddTorsor V P] → Set P → Set P
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.functor_obj : ∀ (R : CommRingCat) (M : ModuleCat ↑R), (AlgebraicGeometry.tilde.functor R).obj M = AlgebraicGeometry.tilde M
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_mem_smul_set_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {a : α},
  a ≠ 0 → ∀ (A : Set β) (x : β), a • x ∈ a • A ↔ x ∈ A
-- Mathlib.Data.List.Pairwise
List.Pairwise.forall : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} [Std.Symm R],
  List.Pairwise R l → ∀ ⦃a : α⦄, a ∈ l → ∀ ⦃b : α⦄, b ∈ l → a ≠ b → R a b
-- Mathlib.Data.Multiset.Powerset
Multiset.zero_mem_powerset : ∀ {α : Type u_1} (s : Multiset α), 0 ∈ s.powerset
-- Mathlib.Topology.Category.Compactum
Compactum.isClosed_iff : ∀ {X : Compactum} (S : Set X.A), IsClosed S ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
-- Lean.Meta.Sym.SymM
/-- Configuration options for the symbolic computation framework.  -/
Lean.Meta.Sym.Config : Type
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.HomComplex.Cocycle.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (z z_1 : CochainComplex.HomComplex.Cochain F G n) (e_z : z = z_1) (m m_1 : ℤ)
  (e_m : m = m_1) (hnm : n + 1 = m) (h : CochainComplex.HomComplex.δ n m z = 0),
  CochainComplex.HomComplex.Cocycle.mk z m hnm h = CochainComplex.HomComplex.Cocycle.mk z_1 m_1 ⋯ ⋯
-- Mathlib.RingTheory.Localization.Basic
Localization.coe_algEquiv : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S],
  ↑(Localization.algEquiv M S) = IsLocalization.map S (RingHom.id R) ⋯
-- Mathlib.Topology.Sober
/-- The closed irreducible subsets of a sober space bijects with the points of the space.  -/
irreducibleSetEquivPoints : {α : Type u_1} →
  [inst : TopologicalSpace α] → [QuasiSober α] → [inst_2 : T0Space α] → TopologicalSpace.IrreducibleCloseds α ≃o α
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.prodMap_def : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_6} {N' : Type u_7}
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N'),
  f.prodMap g = (f.comp (AddMonoidHom.fst M N)).prod (g.comp (AddMonoidHom.snd M N))
-- Mathlib.Data.TypeVec
TypeVec.appendFun_comp' : ∀ {n : ℕ} {α₀ : TypeVec.{u_1} n} {α₁ : TypeVec.{u_2} n} {α₂ : TypeVec.{u_3} n} {β₀ : Type u_1} {β₁ : Type u_2}
  {β₂ : Type u_3} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂),
  TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀) = (TypeVec.comp f₁ f₀ ::: g₁ ∘ g₀)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The condition for a point to be in the affine span, in terms of `vectorSpan`.  -/
mem_affineSpan_iff_exists : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p : P} {s : Set P}, p ∈ affineSpan k s ↔ ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, p = v +ᵥ p₁
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.IsDecompOn.mono : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] {f f' : X → X} {A A' : Set X} {S : Finset G},
  Equidecomp.IsDecompOn f A S → A' ⊆ A → Set.EqOn f f' A' → Equidecomp.IsDecompOn f' A' S
-- Mathlib.Analysis.Convex.StrictConvexSpace
StrictConvexSpace.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E], (∀ (r : ℝ), 0 < r → StrictConvex 𝕜 (Metric.closedBall 0 r)) → StrictConvexSpace 𝕜 E
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.congr_fun : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {f g : M [⋀^ι]→ₗ[R] N},
  f = g → ∀ (x : ι → M), f x = g x
-- Mathlib.Data.Sigma.Basic
/-- Convert a product type to a Σ-type.  -/
Prod.toSigma : {α : Type u_7} → {β : Type u_8} → α × β → (_ : α) × β