mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.IsSubordinate.toSmoothPartitionOfUnity : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} [inst_6 : T2Space M]
  [inst_7 : IsManifold I (↑⊤) M] {f : SmoothBumpCovering ι I M s} {U : M → Set M},
  f.IsSubordinate U → f.toSmoothPartitionOfUnity.IsSubordinate fun i => U (f.c i)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ofLeftInverse_symm_apply : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {g : N →+ G}
  (h : Function.LeftInverse ⇑g ⇑f) (x : ↥f.range), (AddMonoidHom.ofLeftInverse h).symm x = g ↑x
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addSemigroup : {M : Type u_1} → [inst : AddMonoid M] → [inst_1 : Preorder M] → [AddLeftStrictMono M] → AddSemigroup { x // 0 < x }
-- Mathlib.Data.EReal.Basic
EReal.bot_lt_zero : ⊥ < 0
-- Mathlib.Analysis.Calculus.TangentCone.Basic
UniqueDiffWithinAt.mono_nhds : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E},
  UniqueDiffWithinAt 𝕜 s x → nhdsWithin x s ≤ nhdsWithin x t → UniqueDiffWithinAt 𝕜 t x
-- Mathlib.Algebra.Order.Group.Abs
eq_of_mabs_div_le_one : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, |a / b|ₘ ≤ 1 → a = b
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNthEquiv_symm_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u) (p : Fin (n + 1)) (f : (i : Fin (n + 1)) → α i),
  (Fin.insertNthEquiv α p).symm f = (f p, p.removeNth f)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.ihom.ev_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.Closed A] {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A ((CategoryTheory.ihom A).map f))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app Y) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHom.eq_1 : ∀ (R : Type u_1) {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (f : M →+ N), AddMonoidAlgebra.mapDomainBialgHom R f = BialgHom.ofAlgHom (AddMonoidAlgebra.mapDomainAlgHom R R f) ⋯ ⋯
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is zero if and only if the angle with the order of the points reversed is
zero.  -/
EuclideanGeometry.oangle_eq_zero_iff_oangle_rev_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, EuclideanGeometry.oangle p₁ p₂ p₃ = 0 ↔ EuclideanGeometry.oangle p₃ p₂ p₁ = 0
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
meromorphicTrailingCoeffAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (x : 𝕜),
  meromorphicTrailingCoeffAt f x =
    if h₁ : MeromorphicAt f x then if h₂ : meromorphicOrderAt f x = ⊤ then 0 else ⋯.choose x else 0
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_functorPullback_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (U : CategoryTheory.Over X)
  (S : CategoryTheory.Sieve ((CategoryTheory.Over.map f).obj U)),
  (CategoryTheory.Sieve.overEquiv U) (CategoryTheory.Sieve.functorPullback (CategoryTheory.Over.map f) S) =
    (CategoryTheory.Sieve.overEquiv ((CategoryTheory.Over.map f).obj U)) S
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.instCategory : CategoryTheory.Category.{u_1, u_1 + 1} CommRingCat
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.instLaxBraidedForallPi : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [inst_2 : (i : I) → CategoryTheory.BraidedCategory (C i)] →
          {D : I → Type u₂} →
            [inst_3 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] →
              [inst_4 : (i : I) → CategoryTheory.MonoidalCategory (D i)] →
                [inst_5 : (i : I) → CategoryTheory.BraidedCategory (D i)] →
                  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) →
                    [(i : I) → (F i).LaxBraided] → (CategoryTheory.Functor.pi F).LaxBraided
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.powerlt_le : ∀ {a b c : Cardinal.{u}}, a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c
-- Batteries.Data.Fin.Coding
Fin.encodeFun.eq_1 : ∀ {n : ℕ} (x_2 : Fin 0 → Fin n), Fin.encodeFun x_2 = ⟨0, ⋯⟩
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.linearMap_ext_iff : ∀ {R : Type u} [inst : CommRing R] {n : ℕ} {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f g : ↥(⋀[R]^n M) →ₗ[R] N},
  f = g ↔ f.compAlternatingMap (exteriorPower.ιMulti R n) = g.compAlternatingMap (exteriorPower.ιMulti R n)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.e0_mul_e0 : ∀ {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.EquivEven.e0 Q * CliffordAlgebra.EquivEven.e0 Q = -1
-- Mathlib.Probability.Martingale.Centering
/-- Any `ℕ`-indexed stochastic process can be written as the sum of a martingale and a predictable
process. This is the predictable process. See `martingalePart` for the martingale.  -/
MeasureTheory.predictablePart : {Ω : Type u_1} →
  {E : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] →
        {m0 : MeasurableSpace Ω} → (ℕ → Ω → E) → MeasureTheory.Filtration ℕ m0 → MeasureTheory.Measure Ω → ℕ → Ω → E
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring is closed under negation.  -/
NonUnitalSubring.neg_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) {x : R}, x ∈ s → -x ∈ s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntTermInfo.mk.inj : ∀ {eToInt α he eToInt_1 α_1 he_1 : Lean.Expr},
  { eToInt := eToInt, α := α, he := he } = { eToInt := eToInt_1, α := α_1, he := he_1 } →
    eToInt = eToInt_1 ∧ α = α_1 ∧ he = he_1
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instCompleteSpace : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [ContinuousConstSMul 𝕜 F] [CompleteSpace F]
  [∀ (i : ι), IsTopologicalAddGroup (E i)] [SequentialSpace ((i : ι) → E i)],
  CompleteSpace (ContinuousMultilinearMap 𝕜 E F)
-- Lean.Linter.UnusedVariables
/-- Visit an `Expr`, collecting all fvars in it into `fvarUses`  -/
_private.Lean.Linter.UnusedVariables.0.Lean.Linter.UnusedVariables.visitAssignments.visitExpr : IO.Ref (Std.HashSet USize) → IO.Ref (Std.HashSet Lean.FVarId) → Lean.Expr → Lean.MonadCacheT Lean.Expr Unit IO Unit
-- Lean.Elab.SyntheticMVars
/-- Execute `k`, and synthesize pending synthetic metavariables created while executing `k` are solved.
If `mayPostpone == false`, then all of them must be synthesized.
Remark: even if `mayPostpone == true`, the method still uses `synthesizeUsingDefault`  -/
Lean.Elab.Term.withSynthesize : {m : Type → Type u_1} →
  {α : Type} →
    [MonadFunctorT Lean.Elab.TermElabM m] →
      m α → optParam Lean.Elab.Term.PostponeBehavior Lean.Elab.Term.PostponeBehavior.no → m α
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  {c c' : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)} (f : c ⟶ c'),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).map f).hom = f.hom
-- Mathlib.Topology.Hom.ContinuousEvalConst
ContinuousWithinAt.eval_const : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z] {f : Z → F} {s : Set Z}
  {z : Z}, ContinuousWithinAt f s z → ∀ (x : α), ContinuousWithinAt (fun x_1 => (f x_1) x) s z
-- Mathlib.Analysis.Convex.Function
ConcaveOn.right_le_of_le_left' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : SMul 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f →
    ∀ {x y : E} {a b : 𝕜}, x ∈ s → y ∈ s → 0 ≤ a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ f x → f y ≤ f (a • x + b • y)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.inv_hom_h₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : F.I₀) {Z : C} (h : F.X (e.hom.s₀ (e.inv.s₀ i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.inv.h₀ i) (CategoryTheory.CategoryStruct.comp (e.hom.h₀ (e.inv.s₀ i)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
-- Mathlib.Data.Setoid.Basic
/-- Two equivalence relations are equal iff their underlying binary operations are equal.  -/
Setoid.eq_iff_rel_eq : ∀ {α : Type u_1} {r₁ r₂ : Setoid α}, r₁ = r₂ ↔ ⇑r₁ = ⇑r₂
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn_eq_add_of_root_eq_add : ∀ {ι : 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} {S : Type u_6}
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [FaithfulSMul S R] [inst_8 : P.IsValuedIn S] {i j k l : ι},
  P.root k = P.root i + P.root l → P.pairingIn S k j = P.pairingIn S i j + P.pairingIn S l j
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.lift : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)} {β : Type v} [inst : Group β] {f : α → β},
  FreeGroup.Red.Step L₁ L₂ → FreeGroup.Lift.aux f L₁ = FreeGroup.Lift.aux f L₂
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Multiplying by an almost-everywhere nonzero scalar *function* preserves a.e. strong
measurability. This is the varying-scalar analogue of `aestronglyMeasurable_const_smul_iff₀`.  -/
aestronglyMeasurable_smul_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {G₀ : Type u_7} [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ β] [inst_3 : TopologicalSpace G₀]
  [ContinuousInv₀ G₀] [TopologicalSpace.MetrizableSpace G₀] [ContinuousSMul G₀ β] {c : α → G₀},
  MeasureTheory.AEStronglyMeasurable c μ →
    (∀ᵐ (x : α) ∂μ, c x ≠ 0) →
      (MeasureTheory.AEStronglyMeasurable (fun x => c x • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ)
-- Mathlib.Data.Set.Image
Function.Injective.mem_range_iff_existsUnique : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ {b : β}, b ∈ Set.range f ↔ ∃! a, f a = b
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The family of seminorms that induce the weak operator topology, namely `‖y (A x)‖` for
all `x` and `y`.  -/
ContinuousLinearMapWOT.seminormFamily : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          (E : Type u_3) →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [inst_9 : ContinuousConstSMul 𝕜₂ F] → SeminormFamily 𝕜₂ (E →SWOT[σ] F) (E × StrongDual 𝕜₂ F)
-- Init.Data.Slice.Array.Iterator
SubarrayIterator.step.eq_1 : ∀ {α : Type u} {m : Type u → Type u_1} (xs : Subarray α),
  SubarrayIterator.step { internalState := { xs := xs } } =
    if h : xs.start < xs.stop then
      have this := ⋯;
      have this := ⋯;
      Std.IterStep.yield
        {
          internalState :=
            {
              xs :=
                {
                  internalRepresentation :=
                    { array := xs.array, start := xs.start + 1, stop := xs.stop, start_le_stop := ⋯,
                      stop_le_array_size := ⋯ } } } }
        xs.array[xs.start]
    else Std.IterStep.done
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_le_pow : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {a b : M},
  a ≤ b → 1 ≤ b → ∀ {m n : ℕ}, m ≤ n → a ^ m ≤ b ^ n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_max?_eq_not_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.max?.isSome = !t.isEmpty
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.comp_f_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {L L' L'' : Φ.LeftResolution X₂} (φ : L ⟶ L') (ψ : L' ⟶ L'') {Z : C₁} (h : L''.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ ψ).f h =
    CategoryTheory.CategoryStruct.comp φ.f (CategoryTheory.CategoryStruct.comp ψ.f h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
CategoryTheory.Limits.equalizerPullbackMapIso_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S)
  {Z : C} (h : CategoryTheory.Limits.pullback s v ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerPullbackMapIso hf hg v).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.equalizer.ι f g)
          (CategoryTheory.Limits.pullback.fst s v))
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.equalizer.ι
        (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
        (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
      h
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned
matrix with the rows of the initial matrix conjugate transposed to become columns.  -/
Matrix.conjTranspose_fromRows_eq_fromCols_conjTranspose : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [inst : Star R] (A₁ : Matrix m₁ n R)
  (A₂ : Matrix m₂ n R), (A₁.fromRows A₂).conjTranspose = A₁.conjTranspose.fromCols A₂.conjTranspose
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableAt_prod_module_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_17} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_18} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂] {x : M}
  (f : M → F₁ × F₂), MDiffAt f x ↔ MDiffAt (Prod.fst ∘ f) x ∧ MDiffAt (Prod.snd ∘ f) x
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count.instSigmaFinite : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [Countable α],
  MeasureTheory.SigmaFinite MeasureTheory.Measure.count
-- Mathlib.CategoryTheory.MorphismProperty.Quotient
CategoryTheory.MorphismProperty.HasQuotient.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  {homRel : HomRel C} [inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel]
  [inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel],
  (∀ ⦃X Y : C⦄ ⦃f g : X ⟶ Y⦄, homRel f g → (W f ↔ W g)) → W.HasQuotient homRel
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_surjective : ∀ {M : Type u_1} [inst : Monoid M], Function.Surjective Associates.mk
-- Mathlib.Analysis.Convex.BetweenList
List.sbtw_iff_triplewise_and_ne_pair : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {l : List P},
  List.Sbtw R l ↔ List.Triplewise (Sbtw R) l ∧ ∀ (a : P), l ≠ [a, a]
-- Mathlib.Probability.StrongLaw
/-- **Strong law of large numbers**, Lᵖ version: if `X n` is a sequence of independent
identically distributed random variables in Lᵖ, then `n⁻¹ • ∑ i ∈ range n, X i`
converges in `Lᵖ` to `𝔼[X 0]`.  -/
ProbabilityTheory.strong_law_Lp : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : MeasurableSpace E] [BorelSpace E] {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      ∀ (X : ℕ → Ω → E),
        MeasureTheory.MemLp (X 0) p μ →
          Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
            (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
              Filter.Tendsto
                (fun n =>
                  MeasureTheory.eLpNorm (fun ω => (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω - ∫ (x : Ω), X 0 x ∂μ) p μ)
                Filter.atTop (nhds 0)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → t.min! ∈ t
-- Mathlib.Combinatorics.Additive.Dissociation
MulDissociated.subset : ∀ {α : Type u_1} [inst : CommGroup α] {s t : Set α}, s ⊆ t → MulDissociated t → MulDissociated s
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- A Jordan decomposition provides a Hahn decomposition.  -/
MeasureTheory.JordanDecomposition.exists_compl_positive_negative : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
  ∃ S,
    MeasurableSet S ∧
      MeasureTheory.VectorMeasure.restrict j.toSignedMeasure S ≤ MeasureTheory.VectorMeasure.restrict 0 S ∧
        MeasureTheory.VectorMeasure.restrict 0 Sᶜ ≤ MeasureTheory.VectorMeasure.restrict j.toSignedMeasure Sᶜ ∧
          j.posPart S = 0 ∧ j.negPart Sᶜ = 0
-- Lean.Syntax
Lean.mkListNode : Array Lean.Syntax → Lean.Syntax
-- Mathlib.Topology.Order.Category.AlexDisc
alexDiscEquivPreord_inverse_map : ∀ {X Y : Preord} (f : X ⟶ Y),
  alexDiscEquivPreord.inverse.map f =
    CategoryTheory.ConcreteCategory.ofHom (Topology.WithUpperSet.map (Preord.Hom.hom f))
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.postAdjunctionLeft_counit_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X : C} {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (a : F ⊣ G)
  (X_1 : CategoryTheory.Over ((CategoryTheory.Functor.id D).obj (F.obj X))),
  ((CategoryTheory.Over.postAdjunctionLeft a).counit.app X_1).left =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.pullback.fst (G.map X_1.hom) (a.unit.app X)))
      (a.counit.app X_1.left)
-- Mathlib.Data.List.Destutter
/-- If the elements of a list `l` are related pairwise by an antisymmetric relation `r`, then
destuttering `l` by disequality produces the same result as deduplicating `l`.
This is most useful when `r` is a strict or weak ordering.
 -/
List.Pairwise.destutter_eq_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {r : α → α → Prop} [Std.Antisymm r] {l : List α},
  List.Pairwise r l → List.destutter (fun x1 x2 => x1 ≠ x2) l = l.dedup
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition with a linear isometry equiv on the left preserves the norm of the iterated
derivative.  -/
LinearIsometryEquiv.norm_iteratedFDeriv_comp_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (g : F ≃ₗᵢ[𝕜] G) (f : E → F) (x : E) (i : ℕ),
  ‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
-- Mathlib.Analysis.Calculus.Monotone
/-- A monotone function is almost everywhere differentiable, with derivative equal to the
Radon-Nikodym derivative of the associated Stieltjes measure with respect to Lebesgue.  -/
Monotone.ae_hasDerivAt : ∀ {f : ℝ → ℝ} (hf : Monotone f),
  ∀ᵐ (x : ℝ), HasDerivAt f (hf.stieltjesFunction.measure.rnDeriv MeasureTheory.volume x).toReal x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n) (Z : C) (m p : ℕ)
  (h : n + m = p), α.comp 0 h = 0
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.below.mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  {motive : (a a_1 : CommRingCat.Colimits.Prequotient F) → CommRingCat.Colimits.Relation F a a_1 → Prop} (j : J)
  (x y : ↑(F.obj j)), CommRingCat.Colimits.Relation.below ⋯
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State.found : Lean.Util.ParamMinimizer.State✝ → Bool
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_pow_le_mul_norm : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E} {n : ℕ}, ‖a ^ n‖₊ ≤ ↑n * ‖a‖₊
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_self : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [inst : DecidableEq n],
  M.updateCol j c i j = c i
-- Lean.Expr
Lean.Nat.mkInstPow : Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instUniformSpace : {A : Type u_3} → {E : Type u_4} → [u : UniformSpace E] → UniformSpace (WithCStarModule A E)