mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.smul_sum : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {M : Type u_3} {R : Type u_4} [inst_1 : AddCommMonoid M]
  [inst_2 : DistribSMul R M] {v : SkewMonoidAlgebra k G} {c : R} {h : G → k → M},
  c • v.sum h = v.sum fun a b => c • h a b
-- Init.Data.String.Iterator
/-- Moves the iterator's position forward by one character, unconditionally.

This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.

It is only valid to call this function if the iterator is not at the end of the string (i.e.
if `Iterator.atEnd` is `false`); otherwise, the resulting iterator will be invalid.
 -/
String.Legacy.Iterator.next : String.Legacy.Iterator → String.Legacy.Iterator
-- Mathlib.Logic.Denumerable
Denumerable.pnat : Denumerable ℕ+
-- Mathlib.Dynamics.OmegaLimit
/-- The ω-limit of a nonempty set w.r.t. a nontrivial filter is nonempty.  -/
nonempty_omegaLimit_of_isCompact_absorbing : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  [f.NeBot] {c : Set β},
  IsCompact c → (∃ v ∈ f, closure (Set.image2 ϕ v s) ⊆ c) → s.Nonempty → (omegaLimit f ϕ s).Nonempty
-- Mathlib.GroupTheory.GroupAction.Basic
/-- An action is pretransitive if and only if the quotient by `MulAction.orbitRel` is a
subsingleton.  -/
MulAction.pretransitive_iff_subsingleton_quotient : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsPretransitive G α ↔ Subsingleton (MulAction.orbitRel.Quotient G α)
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise.eq_1 : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s : Finset ι) (f g : (i : ι) → π i) [inst : (j : ι) → Decidable (j ∈ s)] (i : ι),
  s.piecewise f g i = if i ∈ s then f i else g i
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_sub_const_Ici : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x - a) ⁻¹' Set.Ici b = Set.Ici (b + a)
-- Mathlib.Data.Multiset.Filter
Multiset.map_filter' : ∀ {α : Type u_1} {β : Type v} (p : α → Prop) [inst : DecidablePred p] {f : α → β},
  Function.Injective f →
    ∀ (s : Multiset α) [inst_1 : DecidablePred fun b => ∃ a, p a ∧ f a = b],
      Multiset.map f (Multiset.filter p s) = Multiset.filter (fun b => ∃ a, p a ∧ f a = b) (Multiset.map f s)
-- Mathlib.Data.W.Basic
WType.mk.inj : ∀ {α : Type u_1} {β : α → Type u_2} {a : α} {f : β a → WType β} {a_1 : α} {f_1 : β a_1 → WType β},
  WType.mk a f = WType.mk a_1 f_1 → a = a_1 ∧ f ≍ f_1
-- Mathlib.Algebra.Algebra.Pi
/-- A family of algebra equivalences `∀ i, (A₁ i ≃ₐ A₂ i)` generates a
multiplicative equivalence between `Π i, A₁ i` and `Π i, A₂ i`.

This is the `AlgEquiv` version of `Equiv.piCongrRight`, and the dependent version of
`AlgEquiv.arrowCongr`.
 -/
AlgEquiv.piCongrRight : {R : Type u_3} →
  {ι : Type u_4} →
    {A₁ : ι → Type u_5} →
      {A₂ : ι → Type u_6} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → Semiring (A₁ i)] →
            [inst_2 : (i : ι) → Semiring (A₂ i)] →
              [inst_3 : (i : ι) → Algebra R (A₁ i)] →
                [inst_4 : (i : ι) → Algebra R (A₂ i)] →
                  ((i : ι) → A₁ i ≃ₐ[R] A₂ i) → ((i : ι) → A₁ i) ≃ₐ[R] (i : ι) → A₂ i
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_swapEquiv_apply : ∀ {R : Type u_3} (c₁ c₃ : R) [inst : CommRing R] (t : QuaternionAlgebra R c₁ 0 c₃),
  ((QuaternionAlgebra.swapEquiv c₁ c₃) t).imJ = t.imI
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TriggerCondition.continue.sizeOf_spec : ∀ {ctx : Type u_1} [inst : SizeOf ctx] (context : ctx),
  sizeOf (Mathlib.TacticAnalysis.TriggerCondition.continue context) = 1 + sizeOf context
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `Section` of a group extension is a right inverse to `S.rightHom`.  -/
GroupExtension.Section : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] → [inst_1 : Group E] → [inst_2 : Group G] → GroupExtension N E G → Type (max u_2 u_3)
-- Mathlib.RingTheory.Jacobson.Ring
IsJacobsonRing.out : ∀ {R : Type u_3} [inst : CommRing R], IsJacobsonRing R → ∀ {I : Ideal R}, I.IsRadical → I.jacobson = I
-- Mathlib.SetTheory.ZFC.Class
instNonemptyClass : Nonempty Class.{u_1}
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atBot_basis : ∀ {α : Type u_6} [inst : Preorder α] [IsCodirectedOrder α] [Nonempty α], Filter.atBot.HasBasis (fun x => True) Set.Iic
-- Mathlib.Data.Sum.Basic
Sum.update_inr_comp_inl : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : β} {x : γ},
  Function.update f (Sum.inr i) x ∘ Sum.inl = f ∘ Sum.inl
-- Mathlib.Algebra.Homology.QuasiIso
exactAt_iff_of_quasiIsoAt : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [QuasiIsoAt f i], K.ExactAt i ↔ L.ExactAt i
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem:
Weak convergence of probability measures implies that the liminf of the measures of any open set
is at least the measure of the open set under the limit probability measure.
 -/
MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto : ∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [inst_2 : OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω}
  {μs : ι → MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs L (nhds μ) → ∀ {G : Set Ω}, IsOpen G → ↑μ G ≤ Filter.liminf (fun i => ↑(μs i) G) L
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α β} {l : List ((a : α) × β a)}
  (h : t₁.WF),
  (↑(t₁.insertMany l ⋯)).Equiv (List.foldl (fun acc p => Std.DTreeMap.Internal.Impl.insert! p.fst p.snd acc) t₁ l)
-- Mathlib.Topology.Homotopy.Contractible
ContinuousMap.nullhomotopic_of_constant : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (y : Y),
  (ContinuousMap.const X y).Nullhomotopic
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.uniqueUpToIso`.

---

a concrete equivalence of any two subobject classifiers  -/
CategoryTheory.Classifier.uniqueUpToIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C) → 𝒞₁.Ω ≅ 𝒞₂.Ω
-- Std.Data.DTreeMap.Basic
/-- Creates a new empty tree map. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree map. `simp` replaces
`empty` with `∅`.
 -/
Std.DTreeMap.empty : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] {f : M → N} {a : M} {r : R},
  MonoidAlgebra.mapDomain f (MonoidAlgebra.single a r) = MonoidAlgebra.single (f a) r
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rco_succ_right_eq_append : ∀ {m n : ℕ}, m ≤ n → (m...n + 1).toList = (m...n).toList ++ [n]
-- Mathlib.CategoryTheory.Limits.Fubini
/-- For each map, a map of cocones.  -/
CategoryTheory.Limits.DiagramOfCocones.map : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              (self : CategoryTheory.Limits.DiagramOfCocones F) →
                {j j' : J} →
                  (f : j ⟶ j') → self.obj j ⟶ (CategoryTheory.Limits.Cocone.precompose (F.map f)).obj (self.obj j')
-- Init.Data.Fin.Lemmas
Fin.eq_or_lt_of_le : ∀ {n : ℕ} {a b : Fin n}, a ≤ b → a = b ∨ a < b
-- Mathlib.Topology.Connected.TotallyDisconnected
/-- A version of `IsPreconnected.constant_of_mapsTo` that assumes that the codomain is nonempty and
proves that `f` is equal to `const α y` on `S` for some `y ∈ T`.  -/
IsPreconnected.eqOn_const_of_mapsTo : ∀ {α : Type u} [inst : TopologicalSpace α] {S : Set α},
  IsPreconnected S →
    ∀ {β : Type u_3} [inst_1 : TopologicalSpace β] {T : Set β},
      IsDiscrete T →
        ∀ {f : α → β}, ContinuousOn f S → Set.MapsTo f S T → T.Nonempty → ∃ y ∈ T, Set.EqOn f (Function.const α y) S
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f : ℝ → ℝ` be a differentiable function. If `C < f'`, then `f` grows faster than
`C * x`, i.e., `C * (y - x) < f y - f x` whenever `x < y`.  -/
mul_sub_lt_image_sub_of_lt_deriv : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → ∀ {C : ℝ}, (∀ (x : ℝ), C < deriv f x) → ∀ ⦃x y : ℝ⦄, x < y → C * (y - x) < f y - f x
-- Lean.DocString.Syntax
/-- A description of an item  -/
Lean.Parser.Category.desc_item : Lean.Parser.Category
-- Lean.Environment
Lean.instLEOLeanLevel : LE Lean.OLeanLevel
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A type `M` is a `CancelCommMonoidWithZero` if it is a commutative monoid with zero element,
`0` is left and right absorbing,
and left/right multiplication by a non-zero element is injective.  -/
CancelCommMonoidWithZero : Type u_2 → Type u_2
-- Mathlib.Algebra.Module.Submodule.Union
Submodule.exists_forall_notMem_of_forall_ne_top : ∀ {ι : Type u_1} {K : Type u_2} {M : Type u_3} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [Finite ι] [Infinite K] (p : ι → Submodule K M), (∀ (i : ι), p i ≠ ⊤) → ∃ x, ∀ (i : ι), x ∉ p i
-- Mathlib.LinearAlgebra.Matrix.Kronecker
/-- The Kronecker tensor product. This is just a shorthand for `kroneckerMap (⊗ₜ)`.
Prefer the notation `⊗ₖₜ` rather than this definition.  -/
Kronecker.«term_⊗ₖₜ_» : Lean.TrailingParserDescr
-- Init.System.IOError
IO.Error.mkIllegalOperation : UInt32 → String → IO.Error
-- Mathlib.RingTheory.IntegralDomain
/-- **Alias** of `isCyclic_subgroup_units`.

---

A finite subgroup of the units of an integral domain is cyclic.  -/
subgroup_units_cyclic : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (S : Subgroup Rˣ) [Finite ↥S], IsCyclic ↥S
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
FreeNonUnitalNonAssocAlgebra.lift_unique : ∀ (R : Type u_1) {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (f : X → A)
  (F : FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] A),
  ⇑F ∘ FreeNonUnitalNonAssocAlgebra.of R = f ↔ F = (FreeNonUnitalNonAssocAlgebra.lift R) f
-- Mathlib.Order.Monotone.Basic
strictMono_nat_of_lt_succ : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f n < f (n + 1)) → StrictMono f
-- Mathlib.Control.Fold
Traversable.toList_spec : ∀ {α : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] (xs : t α),
  Traversable.toList xs = FreeMonoid.toList (Traversable.foldMap FreeMonoid.of xs)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The bijection `(unit R ⟶ M) ≃ M.sections` for `M : PresheafOfModules R`.  -/
PresheafOfModules.unitHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → (M : PresheafOfModules R) → (PresheafOfModules.unit R ⟶ M) ≃ M.sections
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.le_iff_compatible_subset_subset : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β},
  G ≤ H ↔ G.Compatible H ∧ G.vertexSet ⊆ H.vertexSet ∧ G.edgeSet ⊆ H.edgeSet
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
/-- The condition that a commutative square is a pushout square.  -/
CategoryTheory.Square.IsPushout : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → Prop
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.below.of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → CategoryTheory.MorphismProperty.sourceLocalClosure K P x → Prop} {X Y X' Y' : C}
  (f : X ⟶ Y) (g : X' ⟶ Y') (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g)
  (a : CategoryTheory.MorphismProperty.sourceLocalClosure K P f),
  CategoryTheory.MorphismProperty.sourceLocalClosure.below a →
    motive f a → CategoryTheory.MorphismProperty.sourceLocalClosure.below ⋯
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.isProbabilityMeasure_geometricMeasure : ∀ {p : ↑unitInterval}, MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.geometricMeasure p)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The bijection `(unit R ⟶ M) ≃ M.sections` for `M : SheafOfModules R`.  -/
SheafOfModules.unitHomEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} → (M : SheafOfModules R) → (SheafOfModules.unit R ⟶ M) ≃ M.sections
-- Mathlib.Order.Partition.Finpartition
/-- There's a unique partition of an atom.  -/
IsAtom.uniqueFinpartition : {α : Type u_1} →
  [inst : Lattice α] → [inst_1 : OrderBot α] → {a : α} → {P : Finpartition a} → IsAtom a → Unique (Finpartition a)
-- Mathlib.GroupTheory.Subgroup.Simple
AddEquiv.isSimpleAddGroup_congr : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_3} [inst_1 : AddGroup H] (e : G ≃+ H),
  IsSimpleAddGroup G ↔ IsSimpleAddGroup H
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.algebraMap_eq_zero_iff : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] (x : R), (algebraMap R (FreeAlgebra R X)) x = 0 ↔ x = 0
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a commutative subtraction monoid under pointwise operations if `α` is.  -/
Filter.subtractionCommMonoid : {α : Type u_2} → [SubtractionCommMonoid α] → SubtractionCommMonoid (Filter α)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.lift₃_p₃ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] [inst_4 : F.Faithful] {Z : C} (x₁ : Z ⟶ A₁)
  (x₂ : Z ⟶ A₂) (x₃ : Z ⟶ A₃)
  (h₁₂ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₂) f₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp (F.map x₁) f₁ = CategoryTheory.CategoryStruct.comp (F.map x₃) f₃),
  CategoryTheory.CategoryStruct.comp (hf₁.lift₃ f₂ f₃ x₁ x₂ x₃ h₁₂ h₁₃)
      (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₃ hf₁ f₂ f₃) =
    x₃
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.succ_pred_eq_iff_not_isSuccPrelimit : ∀ {o : Ordinal.{u_4}}, Order.succ o.pred = o ↔ ¬Order.IsSuccPrelimit o
-- Mathlib.GroupTheory.Submonoid.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is a commutative monoid.  -/
Submonoid.closureCommMonoidOfComm : (M : Type u_1) → [inst : Monoid M] → {s : Set M} → (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → CommMonoid ↥(Submonoid.closure s)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.addConvolution_comm : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} [inst : AddCommMonoid M] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid E] [inst_3 : Module S E] [inst_4 : TopologicalSpace E] (L : E →ₗ[S] E →ₗ[S] E) (f g : M → E),
  (∀ (x y : E), (L x) y = (L y) x) → DiscreteConvolution.addConvolution L f g = DiscreteConvolution.addConvolution L g f
-- Mathlib.CategoryTheory.Products.Basic
/-- Similar to `prod`, but both functors start from the same category `A`  -/
CategoryTheory.Functor.prod' : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            CategoryTheory.Functor A B → CategoryTheory.Functor A C → CategoryTheory.Functor A (B × C)
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.left.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {a a_1 : C}, CategoryTheory.Join.left a = CategoryTheory.Join.left a_1 → a = a_1
-- Mathlib.Data.Multiset.Interval
Multiset.card_Iic : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α),
  (Finset.Iic s).card = ∏ i ∈ s.toFinset, (Multiset.count i s + 1)
-- Mathlib.Order.Filter.AtTopBot.BigOperators
/-- Let `f` and `g` be two maps to the same commutative additive monoid. This lemma
gives a sufficient condition for comparison of the filter `atTop.map (fun s ↦ ∑ b ∈ s, f b)` with
`atTop.map (fun s ↦ ∑ b ∈ s, g b)`. This is useful to compare the set of limit points of
`∑ b ∈ s, f b` as `s → atTop` with the similar set for `g`.  -/
Filter.map_atTop_finsetSum_le_of_sum_eq : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {f : α → M} {g : β → M},
  (∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b) →
    Filter.map (fun s => ∑ b ∈ s, f b) Filter.atTop ≤ Filter.map (fun s => ∑ x ∈ s, g x) Filter.atTop
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.rootSpan_dualAnnihilator_map_eq_iInf_ker_root' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  Submodule.map (↑P.flip.toPerfPair.symm) (P.rootSpan R).dualAnnihilator = ⨅ i, LinearMap.ker (P.root' i)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_dite : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} {p : ι → Prop} [inst_1 : DecidablePred p]
  (f : (x : ι) → p x → M) (g : (x : ι) → ¬p x → M),
  (∑ x ∈ s, if hx : p x then f x hx else g x hx) = ∑ x, f ↑x ⋯ + ∑ x, g ↑x ⋯
-- Lean.Level
Lean.Level.max.sizeOf_spec : ∀ (a a_1 : Lean.Level), sizeOf (a.max a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.RingTheory.Ideal.Prod
RingHom.ker_prodMap : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {T : Type u_1} {U : Type u_2}
  [inst_2 : Semiring T] [inst_3 : Semiring U] (f : R →+* S) (g : T →+* U),
  RingHom.ker (f.prodMap g) = (RingHom.ker f).prod (RingHom.ker g)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.eq_1 : ∀ {α : Type u} {β : α → Type v} (x : ℕ), Std.DTreeMap.Internal.Impl.leaf.entryAtIdx? x = none
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.differentiable_fourierChar_neg_bilinear_left : ∀ {V : Type u_1} {W : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : NormedAddCommGroup W]
  [inst_3 : NormedSpace ℝ W] (L : V →L[ℝ] W →L[ℝ] ℝ) (w : W), Differentiable ℝ fun v => ↑(Real.fourierChar (-(L v) w))
-- Init.Internal.Order.Basic
Lean.Order.coind_not : ∀ {α : Sort u_1} [inst : Lean.Order.PartialOrder α] (f₁ : α → Prop),
  Lean.Order.monotone f₁ → Lean.Order.monotone fun x => ¬f₁ x
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps.mk.inj : ∀ {embeds : Array (String × ProofWidgets.Html)} {dsl sty sub : String} {maxOptSteps : ℕ}
  {embeds_1 : Array (String × ProofWidgets.Html)} {dsl_1 sty_1 sub_1 : String} {maxOptSteps_1 : ℕ},
  { embeds := embeds, dsl := dsl, sty := sty, sub := sub, maxOptSteps := maxOptSteps } =
      { embeds := embeds_1, dsl := dsl_1, sty := sty_1, sub := sub_1, maxOptSteps := maxOptSteps_1 } →
    embeds = embeds_1 ∧ dsl = dsl_1 ∧ sty = sty_1 ∧ sub = sub_1 ∧ maxOptSteps = maxOptSteps_1
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for objects.  -/
Mathlib.Tactic.BicategoryLike.Obj : Type
-- Mathlib.Analysis.Normed.Group.Pointwise
sphere_zero_sub_singleton : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), Metric.sphere 0 δ - {x} = Metric.sphere (-x) δ
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_neg_iff : ∀ {R : Type u_1} [inst : Ring R] {f : Polynomial R}, (-f).Splits ↔ f.Splits
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep_pair_le_toReal_inf : ∀ {α : Type u_1} [inst : EDist α] {x y : α}, x ≠ y → {x, y}.infsep ≤ (min (edist x y) (edist y x)).toReal
-- Mathlib.Algebra.Lie.LieTheorem
_private.Mathlib.Algebra.Lie.LieTheorem.0.LieModule.exists_forall_lie_eq_smul_of_isSolvable_of_finite : ∀ (k : Type u_1) [inst : Field k] (V : Type u_3) [inst_1 : AddCommGroup V] [inst_2 : Module k V] [CharZero k]
  [Module.Finite k V] [Nontrivial V] (L : Type u_4) [inst_6 : LieRing L] [inst_7 : LieAlgebra k L]
  [inst_8 : LieRingModule L V] [inst_9 : LieModule k L V] [LieAlgebra.IsSolvable L] [LieModule.IsTriangularizable k L V]
  [Module.Finite k L], ∃ χ, Nontrivial ↥(LieModule.weightSpace V ⇑χ)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_of_isEmpty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited β] {a : α}, m.isEmpty = true → m[a]! = default
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_2 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.instReprFunIndInfo : Repr Lean.Meta.FunIndInfo
-- Lean.Meta.Tactic.Simp.Main
_private.Lean.Meta.Tactic.Simp.Main.0.Lean.Meta.Simp.dsimpReduce : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.mk_div : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : Field R] [inst_2 : IsOrderedRing R] (x y : R),
  ArchimedeanClass.mk (x / y) = ArchimedeanClass.mk x - ArchimedeanClass.mk y
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_whisker_right_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) (X : ↑(self.obj a)) {Z : ↑(self.obj c)}
  (h_1 : (self.map (CategoryTheory.CategoryStruct.comp g h)).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.whiskerRight η h)).toNatTrans.app X) h_1 =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f h).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.map₂ η).toNatTrans.app X))
        (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).inv.toNatTrans.app X) h_1))
-- Mathlib.Order.WithBot
WithBot.forall_coe_lt : ∀ {α : Type u_1} {a : α} [inst : Preorder α] {p : WithBot α → Prop},
  (∀ (x : WithBot α), ↑a < x → p x) ↔ ∀ (b : α), a < b → p ↑b
-- Mathlib.GroupTheory.IsPerfect
Group.IsPerfect.range : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (f : G →* G') [Group.IsPerfect G],
  Group.IsPerfect ↥f.range