mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Fin.OverflowAware
Fin.addNat?_eq_some_iff : ∀ {n m : ℕ} {j i : Fin n}, i.addNat? m = some j ↔ ↑i + m < n ∧ ↑j = ↑i + m
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State.emap : Lean.Meta.AbstractMVars.State → Std.HashMap Lean.MVarId Lean.Expr
-- Mathlib.Topology.Order
instDiscreteTopologyEmpty : DiscreteTopology Empty
-- Mathlib.Data.Multiset.MapFold
Multiset.map_lt_map : ∀ {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α}, s < t → Multiset.map f s < Multiset.map f t
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.instHasColimitsOfShapeOppositeType : ∀ {N : Type u'} [inst : CategoryTheory.Category.{v', u'} N] [CategoryTheory.InitiallySmall N],
  CategoryTheory.Limits.HasColimitsOfShape Nᵒᵖ (Type w)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.Sorted.tail : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}, ms.Sorted → ms.tail.Sorted
-- Mathlib.Algebra.Homology.Homotopy
_private.Mathlib.Algebra.Homology.Homotopy.0.Homotopy.mkInductiveAux₂.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Order.Partition.Finpartition
Finpartition.sum_ofPairwiseDisjoint_eq_sum : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {parts : Finset α}
  (hdisjoint : (↑parts).PairwiseDisjoint id) {X : Type u_2} [inst_3 : AddCommMonoid X] {f : α → X},
  f ⊥ = 0 → ∑ p ∈ (Finpartition.ofPairwiseDisjoint parts hdisjoint).parts, f p = ∑ p ∈ parts, f p
-- Mathlib.Data.List.Sigma
List.dlookup_kerase_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {l : List (Sigma β)},
  a ≠ a' → List.dlookup a (List.kerase a' l) = List.dlookup a l
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulDysonETransform_snd : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.mulDysonETransform e x).2 = x.2 ∩ e⁻¹ • x.1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_map_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] [inst : Inhabited γ] {f : α → β → γ} {k k' : α},
  t.getKey? k = some k' →
    Std.DTreeMap.Const.get! (Std.DTreeMap.map f t) k = (Option.map (f k') (Std.DTreeMap.Const.get? t k)).get!
-- Init.Data.BitVec.Bitblast
BitVec.extractAndExtendAux.congr_simp : ∀ {w : ℕ} (k len : ℕ) (x x_1 : BitVec w),
  x = x_1 →
    ∀ (acc acc_1 : BitVec (k * len)),
      acc = acc_1 →
        ∀ (hle : k ≤ w), BitVec.extractAndExtendAux k len x acc hle = BitVec.extractAndExtendAux k len x_1 acc_1 hle
-- Std.Async.Basic
Std.Async.EAsync.instMonad : {ε : Type} → Monad (Std.Async.EAsync ε)
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_id : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁),
  (LinearMap.toMatrixAlgEquiv v₁) LinearMap.id = 1
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.symm_comp : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), (↑e.symm).comp ↑e = AlgHom.id R A₁
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  List.find? (fun x => cmp x.1 k == Ordering.eq) t.toList = none ↔ t.contains k = false
-- Std.Sat.AIG.CachedGatesLemmas
/-- Encoding of BEq as boolean expression in AIG form.
 -/
_private.Std.Sat.AIG.CachedGatesLemmas.0.Std.Sat.AIG.beq_as_aig : ∀ (a b : Bool), (!(a && !b) && !(!a && b)) = (a == b)
-- Mathlib.CategoryTheory.Preadditive.Injective.InjectiveObject
/-- The full subcategory of injective objects in a category `C`.  -/
CategoryTheory.InjectiveObject : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type u
-- Mathlib.Analysis.Analytic.Binomial
binomialSeries_apply : ∀ {𝕂 : Type u} [inst : Field 𝕂] [inst_1 : CharZero 𝕂] (𝔸 : Type v) [inst_2 : Ring 𝔸] [inst_3 : Algebra 𝕂 𝔸]
  [inst_4 : TopologicalSpace 𝔸] [inst_5 : IsTopologicalRing 𝔸] (a : 𝕂) {n : ℕ} (v : Fin n → 𝔸),
  (binomialSeries 𝔸 a n) v = Ring.choose a n • (List.ofFn v).prod
-- Mathlib.Order.Cover
wcovBy_iff_Ioo_eq : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⩿ b ↔ a ≤ b ∧ Set.Ioo a b = ∅
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : { w // w.IsComplex }), ((NumberField.mixedEmbedding.stdBasis K).repr x) (Sum.inr (w, 1)) = (x.2 w).im
-- Mathlib.Tactic.NormNum.Basic
/-- The `norm_num` extension which identifies expressions of the form `Nat.mod a b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalNatMod : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Topology.CantorBendixson
CantorBendixson.perfectKernel_subset : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), CantorBendixson.perfectKernel s ⊆ s
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- This instance is provided instead of `StarHomClass` to avoid type class inference loops.
See note [lower instance priority]  -/
WeakDual.Complex.instStarHomClass : ∀ {F : Type u_1} {A : Type u_2} [inst : CStarAlgebra A] [inst_1 : FunLike F A ℂ] [hF : AlgHomClass F ℂ A ℂ],
  StarHomClass F A ℂ
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_prod_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (a : α × β),
  Set.Ici a = Set.Ici a.1 ×ˢ Set.Ici a.2
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.innerSL.congr_simp : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A]
  [inst_3 : SMul A E] [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace ℂ E] [inst_6 : CStarModule A E],
  CStarModule.innerSL = CStarModule.innerSL
-- Mathlib.AlgebraicTopology.SimplexCategory.Truncated
SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero_assoc : ∀ {n : ℕ} (hn : autoParam ({ len := n }.len ≤ 2) SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero._auto_1)
  (hn' : autoParam ({ len := n + 1 }.len ≤ 2) SimplexCategory.Truncated.δ₂_one_comp_σ₂_zero._auto_3)
  {Z : CategoryTheory.ObjectProperty.FullSubcategory fun a => a.len ≤ 2}
  (h : { obj := { len := n }, property := hn } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.δ₂ 1 hn hn')
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.σ₂ 0 hn' hn) h) =
    h
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_withDensity : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [inst : ProbabilityTheory.IsFiniteKernel κ]
  {f : α → γ → ENNReal} [ProbabilityTheory.IsFiniteKernel (κ.withDensity f)],
  Measurable (Function.uncurry f) → ∀ (a : α), (κ.withDensity f).rnDeriv κ a =ᵐ[κ a] f a
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.equivSigma_symm_apply_hom : ∀ (T : Type u) [inst : CategoryTheory.Category.{v, u} T] (x : (X : T) × (Y : T) × (X ⟶ Y)),
  ((CategoryTheory.Arrow.equivSigma T).symm x).hom = x.snd.snd
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.fundamentalDomain : {ι : Type u_3} → {s : Set (ι → ℕ)} → IsProperLinearSet s → [Finite ι] → Set (ι → ℕ)
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.le.injEq : ∀ (lhs rhs : ℕ) (proof : Lean.Expr) (lhs_1 rhs_1 : ℕ) (proof_1 : Lean.Expr),
  (Mathlib.Tactic.Order.AtomicFact.le lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.le lhs_1 rhs_1 proof_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.support_toPath_subset_support : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] (p : G.Walk u v), (↑p.toPath).support ⊆ p.support
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- For a tangent line to a sphere, the angle between the line and the radius at the tangent point
equals `π / 2`.  -/
EuclideanGeometry.Sphere.IsTangentAt.angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → q ∈ as → EuclideanGeometry.angle q p s.center = Real.pi / 2
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.integrable_poissonMeasure_iff : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {r : NNReal} {f : ℕ → E},
  MeasureTheory.Integrable f (ProbabilityTheory.poissonMeasure r) ↔
    Summable fun n => Real.exp (-↑r) * ↑r ^ n / ↑n.factorial * ‖f n‖
-- Mathlib.Algebra.Torsor.Defs
/-- Cancellation dividing the results of two divisions.  -/
sdiv_div_sdiv_cancel_right : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p₁ p₂ p₃ : P), (p₁ /ₛ p₃) / (p₂ /ₛ p₃) = p₁ /ₛ p₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.j.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic], W.j = ↑W.Δ'⁻¹ * W.c₄ ^ 3
-- Mathlib.Algebra.MvPolynomial.Basic
/-- `MvPolynomial.coeff m` but promoted to an `AddMonoidHom`.  -/
MvPolynomial.coeffAddMonoidHom : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → (σ →₀ ℕ) → MvPolynomial σ R →+ R
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.not_superset`.

---

Set notation form of `LT.lt.not_ge` -/
LT.lt.not_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → ¬b ⊆ a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a `Semigroup` under pointwise operations if `α` is.  -/
Finset.semigroup : {α : Type u_2} → [DecidableEq α] → [Semigroup α] → Semigroup (Finset α)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
GaloisConnection.l_csSup' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] [inst_1 : ConditionallyCompleteLattice β]
  {l : α → β} {u : β → α}, GaloisConnection l u → ∀ {s : Set α}, s.Nonempty → BddAbove s → l (sSup s) = sSup (l '' s)
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearEquiv.isBigO_sub_rev : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (e : E ≃SL[σ₁₂] F) [RingHomIsometric σ₂₁]
  (l : Filter E) (x : E), (fun x' => x' - x) =O[l] fun x' => e (x' - x)
-- Mathlib.Algebra.Category.Ring.Under.Basic
/-- Make an object of `Under R` from an `R`-algebra.  -/
CommRingCat.mkUnder : (R : CommRingCat) → (A : Type u) → [inst : CommRing A] → [Algebra (↑R) A] → CategoryTheory.Under R
-- Mathlib.Analysis.Distribution.TemperedDistribution
/-- The distributional Laplacian and the classical Laplacian coincide on `𝓢(E, F)`.  -/
TemperedDistribution.laplacian_toTemperedDistributionCLM_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℂ F]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] (f : SchwartzMap E F),
  Laplacian.laplacian ((SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) f) =
    (SchwartzMap.toTemperedDistributionCLM E F MeasureTheory.volume) (Laplacian.laplacian f)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {fallback : β k} {f : Option (β k) → Option (β k)},
      (t.alter k f).getD k fallback = (f (t.get? k)).getD fallback
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasurableSpace.generateFrom {s | MeasurableSet s} = inst
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.isLUB_ciSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] [Nonempty ι] {f : ι → α},
  Directed (fun x1 x2 => x1 ≤ x2) f → BddAbove (Set.range f) → IsLUB (Set.range f) (⨆ i, f i)
-- Mathlib.Data.Countable.Defs
instInfiniteOfUncountable : ∀ {α : Sort u} [Uncountable α], Infinite α
-- Mathlib.Data.Finset.Card
Finset.two_lt_card : ∀ {α : Type u_1} {s : Finset α}, 2 < s.card ↔ ∃ a ∈ s, ∃ b ∈ s, ∃ c ∈ s, a ≠ b ∧ a ≠ c ∧ b ≠ c
-- Lean.Meta.Order
/-- Given CCPO instances `inst₁ : CCPO α₁` and `inst₂ : CCPO α₂`,
constructs an instance of the type `CCPO (α₁ × α₂)`.
 -/
Lean.Meta.mkInstCCPOPProd : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.irreducible.sizeOf_spec : sizeOf Lean.ReducibilityStatus.irreducible = 1
-- Lean.Elab.Binders
Lean.Elab.Term.FunBinders.State.fvars : Lean.Elab.Term.FunBinders.State → Array Lean.Expr
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- Expression of `tensorIteratedFDerivTwo` in terms of `iteratedFDeriv`.
 -/
tensorIteratedFDerivTwo_eq_iteratedFDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (e e₁ e₂ : E), (tensorIteratedFDerivTwo 𝕜 f e) (e₁ ⊗ₜ[𝕜] e₂) = (iteratedFDeriv 𝕜 2 f e) ![e₁, e₂]
-- Mathlib.Order.Filter.CardinalInter
Filter.CardinalGenerateSets.below.basic : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} {motive : (a : Set α) → Filter.CardinalGenerateSets g a → Prop}
  {s : Set α} (a : s ∈ g), Filter.CardinalGenerateSets.below ⋯
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.reindex_over_assoc : ∀ {n m : Type u} (i : m → n) (S : AlgebraicGeometry.Scheme) {Z : AlgebraicGeometry.Scheme} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex i S)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace m S ↘ S) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S ↘ S) h
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceToNat : Lean.Meta.Simp.DSimproc
-- Lean.DocString.Parser
/-- Parses a name and zero or more arguments to a role, directive, command, or code block.  -/
Lean.Doc.Parser.nameAndArgs : optParam (Option ℕ) none → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- First projection from the intersection of two pre-`1`-hypercovers.  -/
CategoryTheory.PreOneHypercover.interFst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        (F : CategoryTheory.PreOneHypercover S) →
          [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
            [inst_2 :
                ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
                  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
                    (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] →
              (E.inter F).Hom E
-- Mathlib.Analysis.MellinTransform
MellinConvergent.comp_mul_left : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {s : ℂ} {a : ℝ},
  0 < a → (MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.congr_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashMap α β},
  m₁.Equiv m₂ → (m₃.Equiv m₁ ↔ m₃.Equiv m₂)
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given finite sets `s` and `t`, the sum of `f i` over `i ∈ s ∪ t` plus the sum of
`f i` over `i ∈ s ∩ t` equals the sum of `f i` over `i ∈ s` plus the sum of `f i`
over `i ∈ t`.  -/
finsum_mem_union_inter : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
  s.Finite →
    t.Finite →
      ∑ᶠ (i : α) (_ : i ∈ s ∪ t), f i + ∑ᶠ (i : α) (_ : i ∈ s ∩ t), f i =
        ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Order.Defs.PartialOrder
/-- **Alias** of `not_lt_of_ge`. -/
LE.le.not_gt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ≤ b → ¬b < a
-- Batteries.Data.BinomialHeap.Basic
/-- A node containing a single element `a`.  -/
Batteries.BinomialHeap.Imp.HeapNode.singleton : {α : Type u_1} → α → Batteries.BinomialHeap.Imp.HeapNode α
-- Mathlib.Data.Sigma.Basic
Sigma.exists : ∀ {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop}, (∃ x, p x) ↔ ∃ a b, p ⟨a, b⟩
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.instFullCompPre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) [F.Full], (CategoryTheory.StructuredArrow.pre S F G).Full
-- Init.Data.List.MinMax
List.max?_nil : ∀ {α : Type u_1} [inst : Max α], [].max? = none
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_minValue : ISize.minValue.toNatClampNeg = 0
-- Std.Http.Data.Body.Empty
/-- Closes an empty body (no-op).
 -/
Std.Http.Body.Empty.close : Std.Http.Body.Empty → Std.Async.Async Unit
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_dvd_finrank_bot : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B : IntermediateField F E),
  A.relfinrank B ∣ Module.finrank F ↥B
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_add_one : ∀ (o : Ordinal.{u_1}), (o + 1).card = o.card + 1
-- Mathlib.Data.Part
Part.bind.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : Part α) (g : α → Part β), f.bind g = Part.assert f.Dom fun b => g (f.get b)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_add_add_eq_append : ∀ {m n : ℕ}, (*...=m + n).toList = (*...m).toList ++ (m...=m + n).toList
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.hComp_iff_of_essSurj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {T₂ : CategoryTheory.Functor C₂ C₃}
  {B₂ : CategoryTheory.Functor D₂ D₃} {V₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂)
  [B₁.EssSurj] [w.GuitartExact], (w.hComp w').GuitartExact ↔ w'.GuitartExact
-- Init.Data.Int.DivMod.Lemmas
Int.neg_mul_fmod_right : ∀ (a b : ℤ), (-(a * b)).fmod a = 0
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassPExceptSeries_hasSum : ∀ (L : PeriodPair) (l₀ z x : ℂ),
  (∀ (l : ↥L.lattice), ↑l ≠ l₀ → ‖z - x‖ < ‖↑l - x‖) →
    HasSum (fun i => (L.weierstrassPExceptSeries l₀ x).coeff i * (z - x) ^ i) (L.weierstrassPExcept l₀ z)
-- Mathlib.Probability.Process.Adapted
/-- A continuous and strongly adapted process is strongly progressive.  -/
MeasureTheory.StronglyAdapted.isStronglyProgressive_of_continuous : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u : ι → Ω → β} [inst_2 : TopologicalSpace ι]
  [TopologicalSpace.MetrizableSpace ι] [SecondCountableTopology ι] [inst_5 : MeasurableSpace ι] [OpensMeasurableSpace ι]
  [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.StronglyAdapted f u → (∀ (ω : Ω), Continuous fun i => u i ω) → MeasureTheory.IsStronglyProgressive f u
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.compRight_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} {e f : C ⟶ D} (h : Homotopy e f) (g : D ⟶ E) (i j : ι),
  (h.compRight g).hom i j = CategoryTheory.CategoryStruct.comp (h.hom i j) (g.f j)
-- Lean.Elab.AutoBound
Lean.Elab.relaxedAutoImplicit : Lean.Option Bool
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeasSubgroupToLpTrim_sub : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f g : ↥(MeasureTheory.lpMeasSubgroup F m p μ)),
  MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (f - g) =
    MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f - MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm g
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The bound on the degree of the polynomials used to describe the constructible set appearing in
the case of `C : R → R[X₁, ..., Xₘ]` of Chevalley's theorem with complexity bound.  -/
ChevalleyThm.MvPolynomialC.degBound : ℕ → (ℕ → ℕ) → ℕ → ℕ
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The identity function on Witt vectors is a polynomial function.  -/
WittVector.idIsPoly : ∀ (p : ℕ), WittVector.IsPoly p fun x x_1 => id
-- Std.Sat.CNF.RelabelFin
Std.Sat.CNF.of_maxLiteral_eq_none : ∀ (f : Std.Sat.CNF ℕ), f.maxLiteral = none → ∀ (lit : ℕ), ¬Std.Sat.CNF.VarMem lit f
-- Mathlib.Topology.ContinuousMap.Basic
map_continuousAt : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : FunLike F α β] [ContinuousMapClass F α β] (f : F) (a : α), ContinuousAt (⇑f) a
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.forward : Aesop.RuleTerm → Aesop.UnorderedArraySet Aesop.PremiseIndex → Bool → Aesop.RuleTacDescr
-- Init.Data.List.Count
List.filter_beq : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l : List α} (a : α),
  List.filter (fun x => x == a) l = List.replicate (List.count a l) a
-- Init.Data.Nat.Basic
Nat.add_sub_cancel_left : ∀ (n m : ℕ), n + m - n = m
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.absolutelyContinuous_posterior : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω] {ν : MeasureTheory.Measure 𝓧} [MeasureTheory.SFinite ν],
  (∀ᵐ (ω : Ω) ∂μ, (κ ω).AbsolutelyContinuous ν) →
    ∀ᵐ (b : 𝓧) ∂μ.bind ⇑κ, ((ProbabilityTheory.posterior κ μ) b).AbsolutelyContinuous μ
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.hasOne : {R : Type u_1} → [inst : CommMonoid R] → {R' : Type u_2} → [inst_1 : CommMonoidWithZero R'] → One (MulChar R R')
-- Std.Time.Zoned
/-- Converts a `DateTime` to a `PlainTime`
 -/
Std.Time.DateTime.toPlainTime : Std.Time.DateTime → Std.Time.PlainTime
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_add : ∀ (p : ENNReal) {V : Type u_4} [inst : AddCommGroup V] (x y : WithLp p V), (x + y).ofLp = x.ofLp + y.ofLp
-- Mathlib.Data.FunLike.Group
FunLike.addCommMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Zero F]
  [inst_3 : SMul ℕ F] [inst_4 : AddCommMonoid β] [inst_5 : IsZeroApply F α β] [inst_6 : IsAddApply F α β]
  [inst_7 : IsSMulApply ℕ F α β], FunLike.addCommMonoid = Function.Injective.addCommMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯