mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a bundled additive monoid homomorphism `M₁ →+ M₂` from a function `f`
and a proof that it belongs to the closure of the range of the coercion from `M₁ →+ M₂` (or another
type of bundled homomorphisms that has an `AddMonoidHomClass` instance) to `M₁ → M₂`.  -/
addMonoidHomOfMemClosureRangeCoe : {M₁ : Type u_6} →
  {M₂ : Type u_7} →
    [inst : TopologicalSpace M₂] →
      [T2Space M₂] →
        [inst_2 : AddZeroClass M₁] →
          [inst_3 : AddZeroClass M₂] →
            [ContinuousAdd M₂] →
              {F : Type u_8} →
                [inst_5 : FunLike F M₁ M₂] →
                  [AddMonoidHomClass F M₁ M₂] → (f : M₁ → M₂) → f ∈ closure (Set.range fun f x => f x) → M₁ →+ M₂
-- Mathlib.Topology.Order.LeftRightLim
Monotone.leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β}, Monotone f → Monotone (Function.leftLim f)
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.algHom_ext : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_4}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] {f g : DividedPowerAlgebra R M →ₐ[R] A},
  (∀ (n : ℕ) (m : M), f (DividedPowerAlgebra.dp R n m) = g (DividedPowerAlgebra.dp R n m)) → f = g
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteLimits_comp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] {E : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E]
  [L.IsLocalization P.isoModSerre] [inst_7 : CategoryTheory.Preadditive D] [L.Additive]
  (G : CategoryTheory.Functor D E),
  CategoryTheory.Limits.PreservesFiniteLimits (L.comp G) ↔ CategoryTheory.Limits.PreservesFiniteLimits G
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.Quotient.mem_addSubgroup_orbit_iff' : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G}
  {x : AddAction.orbitRel.Quotient G α} {a b : ↑x.orbit} {c : α},
  ⟦a⟧ = ⟦b⟧ → (↑a ∈ AddAction.orbit (↥H) c ↔ ↑b ∈ AddAction.orbit (↥H) c)
-- Mathlib.Topology.Algebra.Module.ModuleTopology
/-- A semilinear surjection between modules with the module topology is a quotient map.
Equivalently, the pushforward of the module topology along a surjective semilinear map is
again the module topology.  -/
IsModuleTopology.isQuotientMap_of_surjectiveₛₗ : ∀ {R : Type u_1} {S : Type u_2} [τR : TopologicalSpace R] [τS : TopologicalSpace S] [inst : Ring R] [inst_1 : Ring S]
  {A : Type u_3} [inst_2 : AddCommGroup A] [inst_3 : Module R A] [inst_4 : TopologicalSpace A] [IsModuleTopology R A]
  {B' : Type u_5} [inst_6 : AddCommGroup B'] [inst_7 : Module S B'] [τB : TopologicalSpace B'] [IsModuleTopology S B']
  {σ : R →+* S}, IsOpenQuotientMap ⇑σ → ∀ (φ : A →ₛₗ[σ] B'), Function.Surjective ⇑φ → Topology.IsQuotientMap ⇑φ
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.eq_1 : ∀ {G : Type u_1} [inst : Monoid G] (x : G), IsOfFinOrder x = (1 ∈ Function.periodicPts fun x_1 => x * x_1)
-- Mathlib.Data.ENNReal.Basic
ENNReal.exists_nat_gt : ∀ {r : ENNReal}, r ≠ ⊤ → ∃ n, r < ↑n
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.topologicalSpaceFiber : {ι : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] → (Z : FiberBundleCore ι B F) → (x : B) → TopologicalSpace (Z.Fiber x)
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Mul-div-mul version.  -/
Finset.ruzsa_triangle_inequality_mul_div_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  B.card * (A * C).card ≤ (B / A).card * (B * C).card
-- Init.Data.SInt.Lemmas
ISize.toInt32_ofNat' : ∀ {n : ℕ}, (ISize.ofNat n).toInt32 = Int32.ofNat n
-- Init.Data.List.Attach
List.foldr_pmap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : List α} {P : α → Prop} {f : (a : α) → P a → β} (H : ∀ a ∈ l, P a)
  (g : β → γ → γ) (x : γ), List.foldr g x (List.pmap f l H) = List.foldr (fun a acc => g (f ↑a ⋯) acc) x l.attach
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instRespectsOfIsStableUnderComposition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderComposition], W.Respects W
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Any finite subset of an orthonormal family is an `OrthonormalBasis` for its span.  -/
OrthonormalBasis.span : {ι' : Type u_2} →
  {𝕜 : Type u_3} →
    [inst : RCLike 𝕜] →
      {E : Type u_4} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : DecidableEq E] →
              {v' : ι' → E} →
                Orthonormal 𝕜 v' → (s : Finset ι') → OrthonormalBasis (↥s) 𝕜 ↥(Submodule.span 𝕜 ↑(Finset.image v' s))
-- Mathlib.Algebra.Colimit.Finiteness
/-- The directed system of finitely generated submodules of a module.  -/
Module.fgSystem : (R : Type u_1) →
  (M : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (N₁ N₂ : { N // N.FG }) → N₁ ≤ N₂ → ↥↑N₁ →ₗ[R] ↥↑N₂
-- Lean.Meta.Transform
/-- Return expression without visiting any subexpressions.  -/
Lean.TransformStep.done : Lean.Expr → Lean.TransformStep
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_comm_of_commute : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N : AddSubmonoid R},
  (∀ m ∈ M, ∀ n ∈ N, Commute m n) → M * N = N * M
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrLeft_symm_apply : ∀ {ι : Type u_4} {ι' : Type u_5} {X : ι' → Type u_6} [inst : (j : ι') → UniformSpace (X j)] (e : ι ≃ ι'),
  ⇑(UniformEquiv.piCongrLeft e).symm = fun x1 x2 => x1 (e x2)
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContinuousLinearMap.hasCoeToContMDiffMap : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                (n : WithTop ℕ∞) →
                  Coe (E →L[𝕜] E') (ContMDiffMap (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') E E' n)
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
/-- The function `⟨x, y⟩ ↦ ⟪x, y⟫` bundled as a continuous sesquilinear map.  -/
CStarModule.innerSL : {A : Type u_1} →
  {E : Type u_2} →
    [inst : NonUnitalCStarAlgebra A] →
      [inst_1 : PartialOrder A] →
        [StarOrderedRing A] →
          [inst_3 : SMul A E] →
            [inst_4 : NormedAddCommGroup E] → [inst_5 : NormedSpace ℂ E] → [CStarModule A E] → E →L⋆[ℂ] E →L[ℂ] A
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.le_def : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X]
  [inst_3 : FaithfulSMul M X] (P Q : { P // IsLprojection X P }), P ≤ Q ↔ ↑P = ↑(P ⊓ Q)
-- Init.Data.SInt.Bitwise
instLawfulCommIdentityISizeHAndNegOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 &&& x2) (-1)
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.add_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommSemigroup α],
  Function.Periodic f c → ∀ (a : α), Function.Periodic (fun x => f (x + a)) c
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.brecOn.eq : ∀ {R : Type u} [inst : Rack R] {motive : (a a_1 : Rack.PreEnvelGroup R) → Rack.PreEnvelGroupRel' R a a_1 → Sort u_1}
  {a a_1 : Rack.PreEnvelGroup R} (t : Rack.PreEnvelGroupRel' R a a_1)
  (F_1 :
    (a a_2 : Rack.PreEnvelGroup R) →
      (t : Rack.PreEnvelGroupRel' R a a_2) → Rack.PreEnvelGroupRel'.below t → motive a a_2 t),
  Rack.PreEnvelGroupRel'.brecOn t F_1 = F_1 a a_1 t (Rack.PreEnvelGroupRel'.brecOn.go t F_1).2
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_mks : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {f : A → B} (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x y : A),
      { toFun := f, map_one' := h₁ }.toFun (x * y) =
        { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x y : A),
      (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
        (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x +
          (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y)
  (h₅ :
    ∀ (r : R),
      (↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
        (algebraMap R B) r),
  ⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ } = f
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_cast : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c d : E}
  (ω : E → E →L[𝕜] F) (γ : Path a b) (hc : c = a) (hd : d = b), ∫ᶜ (x : E) in γ.cast hc hd, ω x = ∫ᶜ (x : E) in γ, ω x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Cell.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.OrientedOrd α] [inst_2 : Std.LawfulEqOrd α] {k : α}
  (c c_1 : Std.DTreeMap.Internal.Cell α β (compare k)), c = c_1 → c.get? = c_1.get?
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.cg_of_fg : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] [h : FirstOrder.Language.Structure.FG L M],
  FirstOrder.Language.Structure.CG L M
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_neg_iff_of_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] [inst_5 : PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E]
  {f : k → E} {x y : k}, x ≤ y → (slope f x y < 0 ↔ f y < f x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The notation `\textf` for `WeierstrassCurve.VariableChange.baseChange C A`.  -/
WeierstrassCurve.VariableChange.«term_⁄_» : Lean.TrailingParserDescr
-- Init.Data.SInt.Lemmas
Int64.mod_zero : ∀ {a : Int64}, a % 0 = a
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instLieAddGroupOfNatWithTopENatOfIsTopologicalAddGroup : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [IsTopologicalAddGroup G],
  LieAddGroup I 0 G
-- Lean.Compiler.LCNF.Types
/-- `void` is used to identify uses of the state token from `BaseIO` which do no longer need
to be passed around etc. at this point in the pipeline.
 -/
Lean.Compiler.LCNF.ImpureType.void : Lean.Expr
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- The Galois group of a product maps into the product of the Galois groups.  -/
Polynomial.Gal.restrictProd : {F : Type u_1} → [inst : Field F] → (p q : Polynomial F) → (p * q).Gal →* p.Gal × q.Gal
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.all_eq_all_toListModel : ∀ {α : Type u} {β : α → Type v} {p : (a : α) → β a → Bool} {m : Std.DHashMap.Raw α β},
  m.all p = (Std.DHashMap.Internal.toListModel m.buckets).all fun x => p x.fst x.snd
-- Init.System.IO
IO.Process.SpawnArgs.toStdioConfig : IO.Process.SpawnArgs → IO.Process.StdioConfig
-- Mathlib.GroupTheory.GroupAction.Period
/-- If for some `n`, `(n • m) +ᵥ a = a`, then `0 < period m a`.  -/
AddAction.period_pos_of_fixed : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α} {n : ℕ},
  0 < n → n • m +ᵥ a = a → 0 < AddAction.period m a
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instZero : {α : Type u_1} → {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → [Zero β] → Zero C(α, β)
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- If `φ : a ⟶ b` lifts `f : R ⟶ S` and `φ` is an isomorphism, then so is `f`.  -/
CategoryTheory.IsHomLift.isIso_of_lift_isIso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ]
  [CategoryTheory.IsIso φ], CategoryTheory.IsIso f
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.ACM.Context.mk.sizeOf_spec : ∀ (opId : ℕ), sizeOf { opId := opId } = 1 + sizeOf opId
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).getKey? a = if cmp k a = Ordering.eq then none else t.getKey? a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_right_le_size_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₂.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_zsmul_add : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {a : G} {b : H} [inst_1 : AddCommGroup G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H a b] (f : F) (n : ℤ) (x : G), f (n • a + x) = f x + n • b
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Evaluate a `FieldSimp.NF M` object `l`, i.e. a list of pairs in `ℤ × M`, to an element of `M`,
by forming the "multiplicative linear combination" it specifies: raise each `M` term to the power of
the corresponding `ℤ` term, then multiply them all together.  -/
Mathlib.Tactic.FieldSimp.NF.eval : {M : Type u_1} → [GroupWithZero M] → Mathlib.Tactic.FieldSimp.NF M → M
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.step : {α : Type u_1} → {β : Type u_2} → Std.IterM Id (α × β) → Std.IterStep (Std.IterM Id (α × β)) (α × β)
-- Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
AlgebraicClosure.hasEnoughRootsOfUnity_pow : ∀ (F : Type u_1) [inst : Field F] (n k : ℕ) [NeZero ↑n], HasEnoughRootsOfUnity (AlgebraicClosure F) (n ^ k)
-- Init.Data.Int.Linear
Int.Internal.Linear.OrOver_cases_type.eq_2 : ∀ (p : ℕ → Prop) (fuel_1 : ℕ),
  Int.Internal.Linear.OrOver_cases_type fuel_1.succ p =
    (¬p (fuel_1 + 1) → Int.Internal.Linear.OrOver_cases_type fuel_1 p)
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k : α}, (m.insertMany l).contains k = (m.contains k || (List.map Prod.fst l).contains k)
-- Mathlib.Data.Fintype.Card
Finset.card_compl_add_card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α), sᶜ.card + s.card = Fintype.card α
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.instMonoMap'KernelCokernelCompSequenceOfNatNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.Mono
    ((CategoryTheory.kernelCokernelCompSequence f g).map' 0 1
      CategoryTheory.instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_2
      CategoryTheory.instMonoMap'KernelCokernelCompSequenceOfNatNat._proof_4)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit.eq_1 : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  c.isUnit =
    match c.clause with
    | [l] => some l
    | x => none
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toHom_symm_apply : ∀ {α : Type u_1} (a : α), Quiver.SingleObj.toHom.symm a = a
-- Std.Http.Protocol.H1.Writer
/-- Closes the writer, transitioning to the closed state.
 -/
Std.Http.Protocol.H1.Writer.close : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir
-- Mathlib.Algebra.Group.Submonoid.Support
Submonoid.IsMulSpanning.mem_or_inv_mem : ∀ {G : Type u_1} [inst : Group G] {M : Submonoid G}, M.IsMulSpanning → ∀ (a : G), a ∈ M ∨ a⁻¹ ∈ M
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.pow_apply_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α},
  f.IsCycleOn ↑s → a ∈ s → ∀ {n : ℕ}, (f ^ n) a = a ↔ s.card ∣ n
-- Mathlib.MeasureTheory.Measure.Dirac
/-- A measure on a countable type is a sum of Dirac measures.  -/
MeasureTheory.Measure.sum_smul_dirac : ∀ {α : Type u_1} [inst : MeasurableSpace α] [Countable α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure α),
  (MeasureTheory.Measure.sum fun a => μ {a} • MeasureTheory.Measure.dirac a) = μ
-- Std.Time.Date.Unit.Week
Std.Time.Week.instLEOffset : LE Std.Time.Week.Offset
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Summable.tsum_mul_right : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} [T2Space α] [L.NeBot] (a : α),
  Summable f L → ∑'[L] (i : ι), f i * a = (∑'[L] (i : ι), f i) * a
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- If `x` and `y` are two distinct vectors of norm at most `r`, then a convex combination of `x`
and `y` with positive coefficients has norm strictly less than `r`.  -/
norm_combo_lt_of_ne : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E} {a b r : ℝ},
  ‖x‖ ≤ r → ‖y‖ ≤ r → x ≠ y → 0 < a → 0 < b → a + b = 1 → ‖a • x + b • y‖ < r
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.map_inr_inv_coprodComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) {A B : C} [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct (F.obj A) (F.obj B)]
  [inst_4 : CategoryTheory.IsIso (CategoryTheory.Limits.coprodComparison F A B)],
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.coprod.inr)
      (CategoryTheory.inv (CategoryTheory.Limits.coprodComparison F A B)) =
    CategoryTheory.Limits.coprod.inr
-- Mathlib.Data.Set.Prod
Set.graphOn_insert : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) (s : Set α),
  Set.graphOn f (insert x s) = insert (x, f x) (Set.graphOn f s)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs c = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.divCoeffs c_1) =
    (c = c_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.IsBilimit.ext_iff : ∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {B : CategoryTheory.Limits.Bicone F}
  {x y : B.IsBilimit}, x = y ↔ x.isLimit = y.isLimit ∧ x.isColimit = y.isColimit
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.continue.inj : ∀ {pat pat_1 : Lean.Expr},
  Lean.Meta.Grind.EMatch.Cnstr.continue pat = Lean.Meta.Grind.EMatch.Cnstr.continue pat_1 → pat = pat_1
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.mkOfCompact_neg : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : CompactSpace α]
  (f : C(α, β)), BoundedContinuousFunction.mkOfCompact (-f) = -BoundedContinuousFunction.mkOfCompact f
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `spectralNorm K L x = 0`, then `x = 0`.  -/
eq_zero_of_map_spectralNorm_eq_zero : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L},
  spectralNorm K L x = 0 → IsAlgebraic K x → x = 0
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_sSup : ∀ {M : Type u_2} [inst : AddZeroClass M] (S : Set (AddSubmonoid M)), (sSup S).op = sSup (AddSubmonoid.unop ⁻¹' S)
-- Mathlib.Order.Interval.Finset.Defs
/-- The finset $(a, b]$ of elements `x` such that `a < x` and `x ≤ b`. Basically `Set.Ioc a b` as a
finset.  -/
Finset.Ioc : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrder α] → α → α → Finset α
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.hasSum_lintegral_measure : ∀ {α : Type u_1} {ι : Type u_4} {x : MeasurableSpace α} (f : α → ENNReal) (μ : ι → MeasureTheory.Measure α),
  HasSum (fun i => ∫⁻ (a : α), f a ∂μ i) (∫⁻ (a : α), f a ∂MeasureTheory.Measure.sum μ)
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.instAddActionSubtypeMem : {M' : Type u_1} →
  {α : Type u_2} →
    {S' : Type u_4} →
      [inst : SetLike S' M'] →
        (s : S') → [inst_1 : AddMonoid M'] → [inst_2 : AddSubmonoidClass S' M'] → [AddAction M' α] → AddAction (↥s) α
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Composition on the right as a `MonoidHom`. Similar to `MonoidHom.compHom'`.  -/
ContinuousMap.compMonoidHom' : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        {γ : Type u_3} →
          [inst_2 : TopologicalSpace γ] →
            [inst_3 : MulOneClass γ] → [inst_4 : ContinuousMul γ] → C(α, β) → C(β, γ) →* C(α, γ)
-- Mathlib.GroupTheory.Torsion
CommGroup.freeRank_eq_zero_of_finite : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : Finite G], CommGroup.freeRank G = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k},
      Std.Internal.List.maxKey (Std.Internal.List.insertEntry k v l) ⋯ =
        (Std.Internal.List.maxKey? l).elim k fun k' => if (compare k' k).isLE = true then k else k'
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq m] (M : Matrix m n α) (i : m) (b : n → α),
  M.updateRow i b = Matrix.of (Function.update M i b)
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.toList_iter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β}, m.iter.toList = m.toList
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_congr_ae : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {q : ℝ} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  {f g : α → ε}, f =ᵐ[μ] g → MeasureTheory.eLpNorm' f q μ = MeasureTheory.eLpNorm' g q μ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.all_eq_not_any_not : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {p : (a : α) → β a → Bool},
  (↑m).all p = !(↑m).any fun a b => !p a b
-- Mathlib.Data.Nat.Squarefree
Nat.primeFactors_prod : ∀ {s : Finset ℕ}, (∀ p ∈ s, Nat.Prime p) → (∏ p ∈ s, p).primeFactors = s
-- Mathlib.Topology.LocallyConstant.Algebra
/-- `DFunLike.coe` as an `AddMonoidHom`.  -/
LocallyConstant.coeFnAddMonoidHom : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : AddZeroClass Y] → LocallyConstant X Y →+ X → Y
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_six : ∀ {M : Type u_2} [inst : CommMonoid M] (f : Fin 6 → M), ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5
-- Mathlib.Algebra.Order.Floor.Div
smul_ceilDiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : MulActionWithZero α β] [inst_5 : CeilDiv α β] {a : α} [PosSMulMono α β]
  [PosSMulReflectLE α β], 0 < a → ∀ (b : β), a • b ⌈/⌉ a = b