mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.isIso_iCycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι),
  c.next i = j → K.d i j = 0 → ∀ [inst_2 : K.HasHomology i], CategoryTheory.IsIso (K.iCycles i)
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Preliminary statement of the comultiplication for a tensor product of comonoids.
This version is the definitional equality provided by transport, and not quite as good as
the version provided in `tensorObj_comul` below.
 -/
CategoryTheory.Comon.tensorObj_comul' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A B : C) [inst_3 : CategoryTheory.ComonObj A]
  [inst_4 : CategoryTheory.ComonObj B],
  CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.MonoidalCategory.tensorμ (Opposite.op A) (Opposite.op B) (Opposite.op A) (Opposite.op B)).unop
-- Std.Http.Data.Headers.Basic
/-- Checks whether the `Connection` header requests connection close semantics.
 -/
Std.Http.Header.Connection.shouldClose : Std.Http.Header.Connection → Bool
-- Mathlib.Data.Set.Order
AntitoneOn.union : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : β → Set α} {s : Set β},
  AntitoneOn f s → AntitoneOn g s → AntitoneOn (fun x => f x ∪ g x) s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_neg : ∀ (x : ℝ), ↑(-x) = -↑x
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.tendsto_partialSum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r →
    ∀ {y : E}, y ∈ Metric.eball 0 r → Filter.Tendsto (fun n => p.partialSum n y) Filter.atTop (nhds (f (x + y)))
-- Init.Data.UInt.IntToBitVec
UInt16.toBitVec32_toUSize : ∀ (n : UInt16) (h : System.Platform.numBits = 32), n.toUSize.toBitVec32 h = BitVec.setWidth 32 n.toBitVec
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- This instance is scoped, because it always applies (which makes linting and typeclass inference
potentially *a lot* slower).  -/
IsKleinFour.instFinite : ∀ {G : Type u_1} [inst : Group G] [IsKleinFour G], Finite G
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.Database.noConfusionType : Sort v✝ → Mathlib.CrossRef.Database → Mathlib.CrossRef.Database → Sort v✝
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.mk : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      {decls : Array (Std.Sat.AIG.Decl α)} →
        {idx : ℕ} →
          (max : ℕ) →
            (map : Std.HashMap α ℕ) →
              Std.Sat.AIG.RelabelNat.State.Inv1 max map →
                Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map → Std.Sat.AIG.RelabelNat.State α decls idx
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.rightUnitor_def : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R),
  CategoryTheory.MonoidalCategoryStruct.rightUnitor M = (TensorProduct.rid R ↑M).toModuleIso
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.toEven.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M),
  CliffordAlgebra.toEven Q =
    (CliffordAlgebra.lift Q)
      ⟨LinearMap.codRestrict (CliffordAlgebra.evenOdd (CliffordAlgebra.EquivEven.Q' Q) 0)
          (LinearMap.mulLeft R (CliffordAlgebra.EquivEven.e0 Q) ∘ₗ CliffordAlgebra.EquivEven.v Q) ⋯,
        ⋯⟩
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.agree_children : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} (x : PFunctor.Approx.CofixA F n.succ) (y : PFunctor.Approx.CofixA F (n.succ + 1))
  {i : F.B (PFunctor.Approx.head' x)} {j : F.B (PFunctor.Approx.head' y)},
  i ≍ j →
    PFunctor.Approx.Agree x y → PFunctor.Approx.Agree (PFunctor.Approx.children' x i) (PFunctor.Approx.children' y j)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.vadd_oreSub : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] (r : R) (x : X) (s : ↥S),
  r +ᵥ x -ₒ s = (AddOreLocalization.oreMin (r +ᵥ 0) s +ᵥ x) -ₒ AddOreLocalization.oreSubtra (r +ᵥ 0) s
-- Std.Time.DateTime
/-- Sets the `DateTime` to the specified `desiredWeekday`.
 -/
Std.Time.DateTime.withWeekday : Std.Time.DateTime → Std.Time.Weekday → Std.Time.DateTime
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Two vertices are *reachable* if there is a walk between them.
This is equivalent to `Relation.ReflTransGen` of `G.Adj`.
See `SimpleGraph.reachable_iff_reflTransGen`.  -/
SimpleGraph.Reachable : {V : Type u} → SimpleGraph V → V → V → Prop
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.sset.injEq : ∀ (x : Lean.IR.VarId) (i offset : ℕ) (y : Lean.IR.VarId) (ty : Lean.IR.IRType) (b : Lean.IR.FnBody)
  (x_1 : Lean.IR.VarId) (i_1 offset_1 : ℕ) (y_1 : Lean.IR.VarId) (ty_1 : Lean.IR.IRType) (b_1 : Lean.IR.FnBody),
  (Lean.IR.FnBody.sset x i offset y ty b = Lean.IR.FnBody.sset x_1 i_1 offset_1 y_1 ty_1 b_1) =
    (x = x_1 ∧ i = i_1 ∧ offset = offset_1 ∧ y = y_1 ∧ ty = ty_1 ∧ b = b_1)
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.pointwise_smul_def : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M}
  (S : Subring R), a • S = Subring.map (MulSemiringAction.toRingHom M R a) S
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.categoryStruct_id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (a : B),
  (CategoryTheory.CategoryStruct.id F).app a = (CategoryTheory.Lax.LaxTrans.id F).app a
-- Mathlib.Order.Concept
lowerPolar_iUnion₂ : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} {κ : ι → Sort u_5} (r : α → β → Prop) (f : (i : ι) → κ i → Set β),
  lowerPolar r (⋃ i, ⋃ j, f i j) = ⋂ i, ⋂ j, lowerPolar r (f i j)
-- Lean.Data.Lsp.Basic
/-- The text document's URI.  -/
Lean.Lsp.TextDocumentItem.uri : Lean.Lsp.TextDocumentItem → Lean.Lsp.DocumentUri
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.l_le_l_iff : ∀ {α : Type u} {β : Type v} {u : α → β} {l : β → α} [inst : Preorder α] [inst_1 : Preorder β]
  (gi : GaloisCoinsertion l u) {a b : β}, l b ≤ l a ↔ b ≤ a
-- Mathlib.Algebra.Order.AbsoluteValue.Euclidean
/-- The requirement of a Euclidean absolute value
that `abv` is monotone with respect to `≺`  -/
AbsoluteValue.IsEuclidean.map_lt_map_iff' : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {abv : AbsoluteValue R S}, abv.IsEuclidean → ∀ {x y : R}, abv x < abv y ↔ EuclideanDomain.r x y
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.getLast_digit_ne_zero : ∀ (b : ℕ) {m : ℕ} (hm : m ≠ 0), (b.digits m).getLast ⋯ ≠ 0
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicAbvDef.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b) (x : K),
  v.adicAbvDef hb x = (WithZeroMulInt.toNNReal ⋯) ((IsDedekindDomain.HeightOneSpectrum.valuation K v) x)
-- Init.Data.Array.Lemmas
Array.getElem?_replicate : ∀ {α : Type u_1} {n : ℕ} {v : α} {i : ℕ}, (Array.replicate n v)[i]? = if i < n then some v else none
-- Mathlib.Topology.Maps.Strict.Module
/-- A linear map `f : M → N` is strict if and only if the canonical isomorphism
`M ⧸ f.ker ≃ f.range` is a homeomorphism.  -/
LinearMap.isStrictMap_iff_isHomeomorph_quotKerEquivRange : ∀ {R : Type u_1} {M : Type u_3} {Nₗ : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup Nₗ]
  [inst_3 : Module R M] [inst_4 : Module R Nₗ] {fₗ : M →ₗ[R] Nₗ} [inst_5 : TopologicalSpace M]
  [inst_6 : TopologicalSpace Nₗ], Topology.IsStrictMap ⇑fₗ ↔ IsHomeomorph ⇑fₗ.quotKerEquivRange
-- Batteries.Data.HashMap.Basic
/-- Removes key `a` from the map. If it does not exist in the map, the map is returned unchanged.
```
def hashMap := ofList [("one", 1), ("two", 2)]
hashMap.erase "one" = {"two" => 2}
hashMap.erase "three" = {"one" => 1, "two" => 2}
```
 -/
Batteries.HashMap.erase : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → Batteries.HashMap α β → α → Batteries.HashMap α β
-- Mathlib.Order.Filter.Map
Filter.comap_map : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {m : α → β}, Function.Injective m → Filter.comap m (Filter.map m f) = f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_of_contains_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, (Std.DHashMap.map f m).contains k = true → m.contains k = true
-- Init.Data.Nat.Lemmas
Nat.mul_mod : ∀ (a b n : ℕ), a * b % n = a % n * (b % n) % n
-- Lean.Elab.PreDefinition.WF.Unfold
/-- Generates a theorem of the form
```
matcherArgPusher params motive {α} {β} (f : ∀ (x : α), β x) rel alt1 .. x1 x2
  :
  matcher params (motive := fun x1 x2 => ((y : α) → rel x1 x2 y → β y) → motive x1 x2)
    (alt1 := fun z1 z2 z2 f => alt1 z1 z2 z2 f) …
    x1 x2
    (fun y _h => f y)
  =
  matcher params (motive := motive)
    (alt1 := fun z1 z2 z2 => alt1 z1 z2 z2 (fun y _ => f y)) …
    x1 x2
```
 -/
_private.Lean.Elab.PreDefinition.WF.Unfold.0.Lean.Elab.WF.mkMatchArgPusher : Lean.Name → Lean.Meta.MatcherInfo → Lean.MetaM Lean.Name
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_f_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (q n : ℕ)
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) {Z : C}
  (h : (AlgebraicTopology.AlternatingFaceMapComplex.obj Y).X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n }))
      (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n) h) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.P q).f n)
      (CategoryTheory.CategoryStruct.comp (f.app (Opposite.op { len := n })) h)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasFDerivAt_fst : ∀ {𝕜 : 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] {p : E × F},
  HasFDerivAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_le_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α} (hc : k ∈ t),
  (cmp (t.min ⋯) k).isLE = true
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKeyD_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) k).isLE = true
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_prod_of_fintype : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] [inst_1 : Fintype α] (f : α → M), ∏ᶠ (i : α), f i = ∏ i, f i
-- Mathlib.Algebra.Group.Equiv.Finite
Fintype.decidableEqAddEquivFintype.eq_1 : ∀ {α : Type u_4} {β : Type u_5} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Add α] [inst_3 : Add β]
  (a b : α ≃+ β), Fintype.decidableEqAddEquivFintype a b = decidable_of_iff (⇑a = ⇑b) ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.exists_neg_mem : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α} {p : α → Prop}, (∃ x, -x ∈ s ∧ p x) ↔ ∃ x ∈ s, p (-x)
-- Init.Data.List.Monadic
List.flatMapM.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α),
  List.flatMapM f as = List.flatMapM.loop f as []
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.Context.mk.inj : ∀ {red : Lean.Meta.TransparencyMode} {evalAtom : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result}
  {red_1 : Lean.Meta.TransparencyMode} {evalAtom_1 : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result},
  { red := red, evalAtom := evalAtom } = { red := red_1, evalAtom := evalAtom_1 } → red = red_1 ∧ evalAtom = evalAtom_1
-- Mathlib.Tactic.ToDual
le_of_le_of_eq'' : ∀ {α : Type u_1} {a b c : α} [inst : LE α], b ≤ a → b = c → c ≤ a
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- If `a ≠ 0` then the cosine zeta function is entire.  -/
HurwitzZeta.differentiable_cosZeta_of_ne_zero : ∀ {a : UnitAddCircle}, a ≠ 0 → Differentiable ℂ (HurwitzZeta.cosZeta a)
-- Init.Data.String.Subslice
String.Slice.Subslice.cast_rfl : ∀ {s : String.Slice}, String.Slice.Subslice.cast ⋯ = id
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The copy from a subgraph to the supergraph.  -/
SimpleGraph.Copy.ofLE : {V : Type u_1} → (G₁ G₂ : SimpleGraph V) → G₁ ≤ G₂ → G₁.Copy G₂
-- Mathlib.RingTheory.Extension.Presentation.Core
/-- The `r`-th relation of `P` as a polynomial in `R₀`. This is the (arbitrary) choice of a
pre-image under the map `R₀[X] → R[X]`.  -/
Algebra.Presentation.relationOfHasCoeffs : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              {P : Algebra.Presentation R S ι σ} →
                (R₀ : Type u_5) →
                  [inst_3 : CommRing R₀] →
                    [inst_4 : Algebra R₀ R] →
                      [inst_5 : Algebra R₀ S] →
                        [inst_6 : IsScalarTower R₀ R S] → [P.HasCoeffs R₀] → σ → MvPolynomial ι R₀
-- Mathlib.Topology.Algebra.UniformConvergence
instGroupUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [Group β] → Group (UniformOnFun α β 𝔖)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∈ Std.ExtDTreeMap.Const.insertManyIfNewUnit t l ↔ k ∈ t ∨ l.contains k = true
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.toENat_cRk_eq : ∀ {α : Type u} (M : Matroid α) (X : Set α), Cardinal.toENat (M.cRk X) = M.eRk X
-- Mathlib.NumberTheory.LSeries.Convergence
LSeries.abscissaOfAbsConv.eq_1 : ∀ (f : ℕ → ℂ), LSeries.abscissaOfAbsConv f = sInf (Real.toEReal '' {x | LSeriesSummable f ↑x})
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.subsingleton_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S], Subsingleton S ↔ 0 ∈ M
-- Mathlib.Algebra.Group.Basic
ne_iff_ne_of_add_eq_add : ∀ {α : Type u_1} [inst : AddCancelCommMonoid α] {a b c d : α}, a + b = c + d → (a ≠ c ↔ b ≠ d)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.ext : ∀ {α : Type u_2} {inst : MeasurableSpace α} {x y : MeasureTheory.JordanDecomposition α},
  x.posPart = y.posPart → x.negPart = y.negPart → x = y
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instMonadBacktrackSavedStateDoElabM : Lean.MonadBacktrack Lean.Elab.Do.SavedState Lean.Elab.Do.DoElabM
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_pow : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (f : E →L[𝕜] E)
  (g : F →L[𝕜] F) (n : ℕ), TensorProduct.mapL f g ^ n = TensorProduct.mapL (f ^ n) (g ^ n)
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates the limit of `K` and `F ≅ G`, then `G` creates the limit of `K`.  -/
CategoryTheory.createsLimitOfNatIso : {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] →
            {K : CategoryTheory.Functor J C} →
              {F G : CategoryTheory.Functor C D} →
                (F ≅ G) → [CategoryTheory.CreatesLimit K F] → CategoryTheory.CreatesLimit K G
-- Mathlib.Order.LiminfLimsup
sSupHom.apply_blimsup_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u : β → α}
  [inst_1 : CompleteLattice γ] (g : sSupHom α γ), g (Filter.blimsup u f p) ≤ Filter.blimsup (⇑g ∘ u) f p
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- **Alias** of `MeasureTheory.SignedMeasure.of_sdiff_eq_zero_of_symmDiff_eq_zero_negative`.

---

If the symmetric difference of two negative sets is a null-set, then so are the differences
between the two sets.  -/
MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_negative : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u →
        MeasureTheory.VectorMeasure.restrict s v ≤ MeasureTheory.VectorMeasure.restrict 0 v →
          s (symmDiff u v) = 0 → s (u \ v) = 0 ∧ s (v \ u) = 0
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.expand_monomial : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (d : ℕ) (r : R),
  (PowerSeries.expand p hp) ((PowerSeries.monomial d) r) = (PowerSeries.monomial (p * d)) r
-- Mathlib.NumberTheory.SmoothNumbers
Nat.factoredNumbers_empty : Nat.factoredNumbers ∅ = {1}
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_sub_right : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ (c : ℝ),
      autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_sub_right._auto_1 →
        IntervalIntegrable (fun x => f (x - c)) MeasureTheory.volume (a + c) (b + c)
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.Balanced.at_root : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
AddChar.coe_complexBasis : ∀ (α : Type u_1) [inst : AddCommGroup α] [inst_1 : Finite α], ⇑(AddChar.complexBasis α) = DFunLike.coe
-- Std.Sat.AIG.CNF
/-- Convert an AIG into CNF, starting at some entry node.
 -/
Std.Sat.AIG.toCNF : Std.Sat.AIG.Entrypoint ℕ → Std.Sat.CNF ℕ
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.opHomeomorph_apply : ∀ {M : Type u_1} [inst : TopologicalSpace M] (a : M), MulOpposite.opHomeomorph a = MulOpposite.op a
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_15.splitter : (C : Type u_1) →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3) →
      (x y : CategoryTheory.WithTerminal Cᵒᵖ) →
        (f : x ⟶ y) →
          ((x y : C) →
              (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
                motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y))
                  f) →
            ((unop : C) →
                (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
                  motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x) →
              ((x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
                  motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x) →
                motive x y f
-- Mathlib.Data.Finset.Sym
Finset.symInsertEquiv_symm_apply_coe : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α] {n : ℕ} (h : a ∉ s)
  (m : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))), ↑((Finset.symInsertEquiv h).symm m) = Sym.fill a m.fst ↑m.snd
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
Std.IterM.fold_empty : ∀ {m : Type u_1 → Type u_2} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] {init : γ} {f : γ → β → γ},
  Std.IterM.fold f init (Std.IterM.empty m β) = pure init
-- Mathlib.Analysis.Fourier.Notation
FourierModule.mk.injEq : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : Add E] [inst_1 : Add F] [inst_2 : SMul R E]
  [inst_3 : SMul R F] (toFourierTransform : FourierTransform E F)
  (fourier_add :
    ∀ (f g : E), FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g)
  (fourier_smul : ∀ (r : R) (f : E), FourierTransform.fourier (r • f) = r • FourierTransform.fourier f)
  (toFourierTransform_1 : FourierTransform E F)
  (fourier_add_1 :
    ∀ (f g : E), FourierTransform.fourier (f + g) = FourierTransform.fourier f + FourierTransform.fourier g)
  (fourier_smul_1 : ∀ (r : R) (f : E), FourierTransform.fourier (r • f) = r • FourierTransform.fourier f),
  ({ toFourierTransform := toFourierTransform, fourier_add := fourier_add, fourier_smul := fourier_smul } =
      { toFourierTransform := toFourierTransform_1, fourier_add := fourier_add_1, fourier_smul := fourier_smul_1 }) =
    (toFourierTransform = toFourierTransform_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.any.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (t : Std.DTreeMap α β cmp) (p : (a : α) → β a → Bool),
  t.any p = t.inner.any p
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.isPeriodicPt_smul_iff : ∀ {α : Type v} {M : Type u} [inst : Monoid M] [inst_1 : MulAction M α] {m : M} {a : α} {n : ℕ},
  Function.IsPeriodicPt (fun x => m • x) n a ↔ m ^ n • a = a
-- Mathlib.Order.Nucleus
/-- `NucleusClass F X` states that F is a type of nuclei.  -/
NucleusClass : (F : Type u_2) → (X : Type u_3) → [SemilatticeInf X] → [FunLike F X X] → Prop
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.forget₂Comon_obj_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommComon C),
  ((CategoryTheory.CommComon.forget₂Comon C).obj A).X = A.X
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.of_lift : ∀ {α β : Type u_2} [inst : Mathlib.Tactic.Ring.CSLift α β] {a b : α} {a' b' : β}
  [h1 : Mathlib.Tactic.Ring.CSLiftVal a a'] [h2 : Mathlib.Tactic.Ring.CSLiftVal b b'], a' = b' → a = b
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `N` is flat, then for any submodule `M'` of `M`,
`M'` and `N` are also linearly disjoint.  -/
Submodule.LinearDisjoint.of_le_left_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → ∀ {M' : Submodule R S}, M' ≤ M → ∀ [Module.Flat R ↥N], M'.LinearDisjoint N
-- Lean.Attributes
Lean.registerEnumAttributes : {α : Type} →
  List (Lean.Name × String × α) →
    (optParam (Lean.Name → α → Lean.AttrM Unit) fun x x_1 => pure ()) →
      optParam Lean.AttributeApplicationTime Lean.AttributeApplicationTime.afterTypeChecking →
        autoParam Lean.Name Lean.registerEnumAttributes._auto_1 → IO (Lean.EnumAttributes α)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.existsUnique : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X),
  CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g →
    ∃! l, CategoryTheory.CategoryStruct.comp l (CategoryTheory.Limits.equalizer.ι f g) = k