mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Arithmetic
Multiset.aemeasurable_prod : ∀ {M : Type u_2} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (l : Multiset (α → M)),
  (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable l.prod μ
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.restrictScalars₁₂_inj : ∀ {R : Type u_1} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_5} {N : Type u_7} {Pₗ : Type u_11}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid Pₗ] [inst_5 : Module R M]
  [inst_6 : Module S N] [inst_7 : Module R Pₗ] [inst_8 : Module S Pₗ] [inst_9 : SMulCommClass S R Pₗ] (R' : Type u_14)
  (S' : Type u_15) [inst_10 : Semiring R'] [inst_11 : Semiring S'] [inst_12 : Module R' M] [inst_13 : Module S' N]
  [inst_14 : Module R' Pₗ] [inst_15 : Module S' Pₗ] [inst_16 : SMulCommClass S' R' Pₗ] [inst_17 : SMul S' S]
  [inst_18 : IsScalarTower S' S N] [inst_19 : IsScalarTower S' S Pₗ] [inst_20 : SMul R' R]
  [inst_21 : IsScalarTower R' R M] [inst_22 : IsScalarTower R' R Pₗ] {B B' : M →ₗ[R] N →ₗ[S] Pₗ},
  LinearMap.restrictScalars₁₂ R' S' B = LinearMap.restrictScalars₁₂ R' S' B' ↔ B = B'
-- Mathlib.Tactic.Linarith.Lemmas
Mathlib.Tactic.Linarith.zero_lt_one : ∀ {α : Type u} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α], 0 < 1
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (A : adj.toComonad.Coalgebra) (B : C)
  [inst_2 : CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))]
  (f : (CategoryTheory.Comonad.comparison adj).obj B ⟶ A),
  (CategoryTheory.Comonad.ComonadicityInternal.comparisonRightAdjointHomEquiv adj A B) f =
    CategoryTheory.Limits.equalizer.lift ((adj.homEquiv B A.A) f.f) ⋯
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- Prefunctors commute with `homOfEq`.  -/
Prefunctor.homOfEq_map : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] (F : U ⥤q V) {X Y : U} (f : X ⟶ Y) {X' Y' : U}
  (hX : X = X') (hY : Y = Y'), F.map (Quiver.homOfEq f hX hY) = Quiver.homOfEq (F.map f) ⋯ ⋯
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₁_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C}
  {G H : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G)
  (μ : G ⟶ H),
  CategoryTheory.OverPresheafAux.YonedaCollection.map₁ (CategoryTheory.CategoryStruct.comp η μ) =
    CategoryTheory.OverPresheafAux.YonedaCollection.map₁ μ ∘ CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η
-- Mathlib.RepresentationTheory.Submodule
Representation.asAlgebraHom_mem_of_forall_mem : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (p : Submodule k V),
  (∀ (g : G), ∀ v ∈ p, (ρ g) v ∈ p) → ∀ v ∈ p, ∀ (x : MonoidAlgebra k G), (ρ.asAlgebraHom x) v ∈ p
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Rotating the first vector by `θ` subtracts `θ` from the angle between two vectors.  -/
Orientation.oangle_rotation_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  x ≠ 0 → y ≠ 0 → ∀ (θ : Real.Angle), o.oangle ((o.rotation θ) x) y = o.oangle x y - θ
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The total mass of a finite measure depends continuously on the measure.  -/
MeasureTheory.FiniteMeasure.continuous_mass : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  Continuous fun μ => μ.mass
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csInf_sub : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M]
  {s t : Set M}, s.Nonempty → BddBelow s → t.Nonempty → BddAbove t → sInf (s - t) = sInf s - sSup t
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.Away.exists_isIntegral_mul_of_isIntegral_mk' : ∀ {R : Type u_5} {S : Type u_6} {Sₘ : Type u_7} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing Sₘ]
  [inst_3 : Algebra R S] [inst_4 : Algebra S Sₘ] [inst_5 : Algebra R Sₘ] [IsScalarTower R S Sₘ] {r : S},
  IsIntegral R r →
    ∀ [inst_7 : IsLocalization.Away r Sₘ] {x : S} {a : ↥(Submonoid.powers r)},
      IsIntegral R (IsLocalization.mk' Sₘ x a) → ∃ n, IsIntegral R (r ^ n * x)
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- Let `G` be a Type with addition, let `A B : Finset G` be finite subsets and
let `a0 b0 : G` be two elements.  `UniqueAdd A B a0 b0` asserts `a0 + b0` can be written in at
most one way as a sum of an element from `A` and an element from `B`.  -/
UniqueAdd : {G : Type u_1} → [Add G] → Finset G → Finset G → G → G → Prop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Bitwise or.
 -/
Std.Tactic.BVDecide.BVBinOp.or : Std.Tactic.BVDecide.BVBinOp
-- Mathlib.Topology.Instances.RealVectorSpace
/-- Reinterpret a continuous additive homomorphism between two real vector spaces
as a continuous real-linear map.  -/
AddMonoidHom.toRealLinearMap : {E : Type u_1} →
  [inst : AddCommGroup E] →
    [inst_1 : Module ℝ E] →
      [inst_2 : TopologicalSpace E] →
        [ContinuousSMul ℝ E] →
          {F : Type u_2} →
            [inst_4 : AddCommGroup F] →
              [inst_5 : Module ℝ F] →
                [inst_6 : TopologicalSpace F] →
                  [ContinuousSMul ℝ F] → [T2Space F] → (f : E →+ F) → Continuous ⇑f → E →L[ℝ] F
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- Given a finite measure supported on a compact set, there exists another finite measure which
integrates in the same way bounded continuous functions, and is regular.  -/
MeasureTheory.Measure.exists_innerRegular_eq_of_isCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [inst_2 : MeasurableSpace X] [BorelSpace X]
  (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] {K : Set X},
  IsCompact K →
    μ Kᶜ = 0 →
      ∃ ν,
        ν.InnerRegular ∧
          MeasureTheory.IsFiniteMeasure ν ∧
            ν Kᶜ = 0 ∧ ∀ (g : BoundedContinuousFunction X ℝ), ∫ (x : X), g x ∂μ = ∫ (x : X), g x ∂ν
-- Mathlib.Algebra.Category.ModuleCat.Images
/-- The inclusion of `image f` into the target  -/
ModuleCat.image.ι : {R : Type u} → [inst : Ring R] → {G H : ModuleCat R} → (f : G ⟶ H) → ModuleCat.image f ⟶ H
-- Mathlib.FieldTheory.IsPerfectClosure
pNilradical_eq_bot' : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ}, p ≤ 1 → pNilradical R p = ⊥
-- Mathlib.Topology.ContinuousOn
/-- If `f` is continuous on some neighbourhood `s'` of `s` and `f` maps `s` to `t`,
the preimage of a set neighbourhood of `t` is a set neighbourhood of `s`.  -/
ContinuousOn.tendsto_nhdsSet : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s s' : Set α}
  {t : Set β}, ContinuousOn f s' → s' ∈ nhdsSet s → Set.MapsTo f s t → Filter.Tendsto f (nhdsSet s) (nhdsSet t)
-- Mathlib.LinearAlgebra.StdBasis
/-- `Pi.basis (s : ∀ j, Basis (ιs j) R (Ms j))` is the `Σ j, ιs j`-indexed basis on `Π j, Ms j`
given by `s j` on each component.

For the standard basis over `R` on the finite-dimensional space `η → R` see `Pi.basisFun`.
 -/
Pi.basis : {R : Type u_2} →
  {η : Type u_4} →
    {ιs : η → Type u_5} →
      {Ms : η → Type u_6} →
        [inst : Semiring R] →
          [inst_1 : (i : η) → AddCommMonoid (Ms i)] →
            [inst_2 : (i : η) → Module R (Ms i)] →
              [Fintype η] → ((j : η) → Module.Basis (ιs j) R (Ms j)) → Module.Basis ((j : η) × ιs j) R ((j : η) → Ms j)
-- Mathlib.Topology.ContinuousOn
ContinuousOn.finInsertNth : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {X : Fin (n + 1) → Type u_5}
  [inst_1 : (i : Fin (n + 1)) → TopologicalSpace (X i)] (i : Fin (n + 1)) {f : α → X i}
  {g : α → (j : Fin n) → X (i.succAbove j)} {s : Set α},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun a => i.insertNth (f a) (g a)) s
-- Mathlib.Algebra.Order.Field.Basic
div_neg_of_pos_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  0 < a → b < 0 → a / b < 0
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.posSemidef_matrix_measure_inter : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Type u_5} [Finite ι] {s : ι → Set α},
  (∀ (j : ι), MeasurableSet (s j)) →
    autoParam (∀ (j : ι), μ (s j) ≠ ⊤) MeasureTheory.posSemidef_matrix_measure_inter._auto_1 →
      (Matrix.of fun i j => μ.real (s i ∩ s j)).PosSemidef
-- Mathlib.Topology.Order.LeftRightNhds
nhdsLT_basis : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α),
  (nhdsWithin a (Set.Iio a)).HasBasis (fun x => x < a) fun x => Set.Ioo x a
-- Lean.Server.References
Lean.Server.LoadedILean.mk : Lean.Lsp.DocumentUri →
  System.FilePath → Lean.Server.DirectImports → Lean.Lsp.ModuleRefs → Lean.Lsp.Decls → Lean.Server.LoadedILean
-- Mathlib.RingTheory.Radical.Basic
/-- An irreducible `a` divides the radical of `b` if and only if it divides `b` itself.
Note this generalises to radical elements `a`, see `UniqueFactorizationMonoid.dvd_radical_iff`.
 -/
UniqueFactorizationMonoid.dvd_radical_iff_of_irreducible : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M}, Irreducible a → b ≠ 0 → (a ∣ UniqueFactorizationMonoid.radical b ↔ a ∣ b)
-- Mathlib.RingTheory.PicardGroup
/-- If `f : M →ₗ[R] N` and `g : N →ₗ[R] M` where `M` and `N` are invertible `R`-modules, and `f` is
a right inverse of `g`, then in fact `f` is also the left inverse of `g`, and we promote this to
an `R`-module isomorphism.  -/
Module.Invertible.linearEquivOfRightInverse : {R : Type u} →
  {M : Type v} →
    {N : Type u_1} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] →
              [inst_4 : Module R N] →
                [Module.Invertible R M] →
                  [Module.Invertible R N] → {f : M →ₗ[R] N} → {g : N →ₗ[R] M} → Function.RightInverse ⇑f ⇑g → M ≃ₗ[R] N
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_eq_zero_iff_isEmpty : ∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r], Ordinal.type r = 0 ↔ IsEmpty α
-- Mathlib.Topology.Closure
/-- If a closed property holds for a dense subset, it holds for the whole space.  -/
Dense.induction : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  Dense s → ∀ {P : X → Prop}, (∀ x ∈ s, P x) → IsClosed {x | P x} → ∀ (x : X), P x
-- Mathlib.Algebra.Group.Hom.Defs
/-- `1` is the homomorphism sending all elements to `1`.  -/
instOneOneHom : {M : Type u_4} → {N : Type u_5} → [inst : One M] → [inst_1 : One N] → One (OneHom M N)
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.five_le_of_ne_two_of_ne_three : ∀ {p : ℕ}, Nat.Prime p → p ≠ 2 → p ≠ 3 → 5 ≤ p
-- Mathlib.GroupTheory.Solvable
/-- A group `G` is solvable if its derived series is eventually trivial. We use this definition
because it's the most convenient one to work with.  -/
Group.IsSolvable : (G : Type u_1) → [Group G] → Prop
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.orderIsoMatrix_apply_ringCon_r : ∀ {R : Type u_1} {n : Type u_2} [inst : NonAssocRing R] [inst_1 : Fintype n] [inst_2 : Nonempty n]
  [inst_3 : DecidableEq n] (I : TwoSidedIdeal R) (M N : Matrix n n R),
  (TwoSidedIdeal.orderIsoMatrix I).ringCon.toSetoid M N = ∀ (i j : n), I.ringCon (M i j) (N i j)
-- Mathlib.Data.Fintype.Pi
Set.iUnion_fin_add_one_eq_iUnion_castSucc : ∀ {α : Type u_1} {n : ℕ} (f : Fin (n + 1) → Set α), ⋃ i, f i = Set.iUnion (f ∘ Fin.castSucc) ∪ f (Fin.last n)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec.injEq : ∀ (h h_1 : Lean.FVarId),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec h = Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec h_1) = (h = h_1)
-- Mathlib.Algebra.Jordan.Basic
/-- A (commutative) Jordan multiplication is also a Jordan multiplication  -/
IsCommJordan.toIsJordan : ∀ (A : Type u_1) [inst : CommMagma A] [IsCommJordan A], IsJordan A
-- Mathlib.Analysis.Asymptotics.Defs
/-- Definition of `IsBigO` in terms of filters, with a positive constant.  -/
Asymptotics.isBigO_iff' : ∀ {α : Type u_1} {E : Type u_3} {E''' : Type u_12} [inst : Norm E] [inst_1 : SeminormedAddGroup E'''] {f : α → E}
  {l : Filter α} {g : α → E'''}, f =O[l] g ↔ ∃ c > 0, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
-- Init.Data.Fin.Lemmas
Fin.zero_add : ∀ {n : ℕ} [inst : NeZero n] (k : Fin n), 0 + k = k
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- Given the data of the constructible set `s`, build the data of the constructible set
`{I | {x | φ x ∈ I} ∈ s}`.  -/
PrimeSpectrum.BasicConstructibleSetData.map : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        (R →+* S) → PrimeSpectrum.BasicConstructibleSetData R → PrimeSpectrum.BasicConstructibleSetData S
-- Mathlib.Topology.Algebra.Support
mulTSupport_comp_eq_of_range_subset : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} [inst : One α] [inst_1 : TopologicalSpace X] [inst_2 : One β] {g : α → β}
  {f : X → α}, (∀ {x : α}, x ∈ Set.range f → (g x = 1 ↔ x = 1)) → mulTSupport (g ∘ f) = mulTSupport f
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_lt : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {x y : α},
  CauSeq.const abs x < CauSeq.const abs y ↔ x < y
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.fromSubtype_π : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p]
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p)
      (CategoryTheory.Limits.biproduct.π f j) =
    if h : p j then CategoryTheory.Limits.biproduct.π (Subtype.restrict p f) ⟨j, h⟩ else 0
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.orbitRel_le_fst : ∀ (G : Type u_1) (α : Type u_2) (β : Type u_3) [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MulAction G β],
  MulAction.orbitRel G (α × β) ≤ Setoid.comap Prod.fst (MulAction.orbitRel G α)
-- Mathlib.Order.Circular
/-- **Alias** of `sbtw_cyclic_left`. -/
SBtw.sbtw.cyclic_left : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → sbtw b c a
-- Mathlib.Analysis.Convex.Combination
convexHull_sub : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s t : Set E),
  (convexHull R) (s - t) = (convexHull R) s - (convexHull R) t
-- Mathlib.Data.Int.Fib.Lemmas
/-- **Catalan's identity**: `fib (x + a) ^ 2 - fib x * fib (x + 2 * a) = (-1) ^ |x| * fib a ^ 2`.  -/
Int.fib_add_sq_sub_fib_mul_fib_add_two_mul : ∀ (x a : ℤ), Int.fib (x + a) ^ 2 - Int.fib x * Int.fib (x + 2 * a) = (-1) ^ x.natAbs * Int.fib a ^ 2
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivRangeS.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (c : RingCon M) (f : N →+* M)
  {d : RingCon N} (hcd : d = c.comap f), c.comapQuotientEquivRangeS f hcd = c.comapQuotientEquivRangeS f hcd
-- Mathlib.Dynamics.Ergodic.Action.Basic
ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq : ∀ {G : Type u_1} {α : Type u_2} {inst : SMul G α} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [self : ErgodicSMul G α μ] {s : Set α},
  MeasurableSet s → (∀ (g : G), (fun x => g • x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.Data.Stream.Init
_private.Mathlib.Data.Stream.Init.0.Stream'.take.match_1.eq_2 : ∀ {α : Type u_1} (motive : ℕ → Stream' α → Sort u_2) (n : ℕ) (s : Stream' α) (h_1 : (x : Stream' α) → motive 0 x)
  (h_2 : (n : ℕ) → (s : Stream' α) → motive n.succ s),
  (match n.succ, s with
    | 0, x => h_1 x
    | n.succ, s => h_2 n s) =
    h_2 n s
-- Mathlib.Order.BooleanAlgebra.Basic
compl_injective : ∀ {α : Type u} [inst : BooleanAlgebra α], Function.Injective compl
-- Mathlib.Analysis.Convex.Basic
Convex.starConvex_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E} {x : E} [ZeroLEOneClass 𝕜], Convex 𝕜 s → s.Nonempty → (StarConvex 𝕜 x s ↔ x ∈ s)
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_add_ball_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), {x} + Metric.ball 0 δ = Metric.ball x δ
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holderL_apply_apply : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (p q r : ENNReal) [hpqr : p.HolderTriple q r] [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G)
  [inst_7 : Fact (1 ≤ p)] [inst_8 : Fact (1 ≤ q)] [inst_9 : Fact (1 ≤ r)] (x : ↥(MeasureTheory.Lp E p μ))
  (g : ↥(MeasureTheory.Lp F q μ)), ((ContinuousLinearMap.holderL μ p q r B) x) g = ContinuousLinearMap.holder r B x g
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
/-- The Proximity Function of Value Distribution Theory

If `f : ℂ → E` is meromorphic and `a : WithTop E` is any value, the proximity function is a
logarithmically weighted measure quantifying how well a meromorphic function `f` approximates the
constant function `a` on the circle of radius `R` in the complex plane.  In the special case where
`a = ⊤`, it quantifies how well `f` approximates infinity.
 -/
ValueDistribution.proximity : {E : Type u_1} → [NormedAddCommGroup E] → (ℂ → E) → WithTop E → ℝ → ℝ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.foldr_eq_foldr_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} [inst : Std.TransCmp cmp]
  {f : α → δ → δ} {init : δ}, Std.ExtTreeMap.foldr (fun a x d => f a d) init t = List.foldr f init t.keys
-- Mathlib.Algebra.Module.Torsion.Basic
/-- An `a`-torsion module is a module whose `a`-torsion submodule is the full space.  -/
Module.isTorsionBy_iff_torsionBy_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a : R),
  Module.IsTorsionBy R M a ↔ Submodule.torsionBy R M a = ⊤
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mk : {G : Type u_3} →
  [inst : Group G] →
    (toSubmonoid : Submonoid G) → (∀ {x : G}, x ∈ toSubmonoid.carrier → x⁻¹ ∈ toSubmonoid.carrier) → Subgroup G
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {he : t.isEmpty = false}, (cmp (t.maxKey he) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.approximates_deriv_on_open_nhds : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E},
  HasStrictFDerivAt f (↑f') a → ∃ s, a ∈ s ∧ IsOpen s ∧ ApproximatesLinearOn f (↑f') s (‖↑f'.symm‖₊⁻¹ / 2)
-- Lean.Meta.Sym.Apply
/-- Indices of arguments that become new subgoals, ordered with
non-dependent goals first.  -/
Lean.Meta.Sym.BackwardRule.resultPos : Lean.Meta.Sym.BackwardRule → List ℕ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.revSkipWhile_eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String.Slice} {pos : s.Pos},
  pos.revSkipWhile pat = (String.Slice.Pattern.Model.revMatchAt? pat pos).elim pos fun x => x.revSkipWhile pat
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt32.size), (UInt32.ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯
-- Mathlib.Algebra.Category.Ring.Colimits
/-- Evidence that the proposed colimit is the colimit.  -/
RingCat.Colimits.colimitIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → CategoryTheory.Limits.IsColimit (RingCat.Colimits.colimitCocone F)
-- Mathlib.Algebra.Order.Star.Basic
instPosSMulStrictMono : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : NonUnitalSemiring A] [inst_5 : StarRing A] [inst_6 : PartialOrder A] [StarOrderedRing A]
  [inst_8 : Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] [IsDomain R] [IsCancelAdd A]
  [Module.IsTorsionFree R A], PosSMulStrictMono R A
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.mk.sizeOf_spec : ∀ {α : Type u_4} [inst : TopologicalSpace α] [inst_1 : SizeOf α] (toCompacts : TopologicalSpace.Compacts α)
  (interior_nonempty' : (interior toCompacts.carrier).Nonempty),
  sizeOf { toCompacts := toCompacts, interior_nonempty' := interior_nonempty' } =
    1 + sizeOf toCompacts + sizeOf interior_nonempty'
-- Mathlib.Algebra.Group.Basic
/-- Version of `add_right_iterate` that is fully applied, for `rw`.  -/
add_right_iterate_apply : ∀ {M : Type u_4} [inst : AddMonoid M] {n : ℕ} (a b : M), (fun x => x + a)^[n] b = b + n • a
-- Mathlib.Data.Bool.Basic
Bool.self_ne_not : ∀ (b : Bool), b ≠ !b
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
/-- The right lifting property with respect to all epimorphisms  -/
CategoryTheory.StrongMono.rlp : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P Q : C} {f : P ⟶ Q} [self : CategoryTheory.StrongMono f]
  ⦃X Y : C⦄ (z : X ⟶ Y) [CategoryTheory.Epi z], CategoryTheory.HasLiftingProperty z f
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
_private.Mathlib.MeasureTheory.Function.ConvergenceInMeasure.0.MeasureTheory.ExistsSeqTendstoAe.seqTendstoAeSeq.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Tactic.Simps.Basic
Simps.ParsedProjectionData.mk.sizeOf_spec : ∀ (strName : Lean.Name) (strStx : Lean.Syntax) (newName : Lean.Name) (newStx : Lean.Syntax) (isDefault isPrefix : Bool)
  (expr? : Option Lean.Expr) (projNrs : Array ℕ) (isCustom : Bool),
  sizeOf
      { strName := strName, strStx := strStx, newName := newName, newStx := newStx, isDefault := isDefault,
        isPrefix := isPrefix, expr? := expr?, projNrs := projNrs, isCustom := isCustom } =
    1 + sizeOf strName + sizeOf strStx + sizeOf newName + sizeOf newStx + sizeOf isDefault + sizeOf isPrefix +
          sizeOf expr? +
        sizeOf projNrs +
      sizeOf isCustom
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_comap : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β))
  (U : TopologicalSpace.Opens β), ↑((TopologicalSpace.Opens.comap f) U) = ⇑f ⁻¹' ↑U
-- Mathlib.Data.Set.Card.Arithmetic
Set.ncard_iUnion_le_of_finite : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] (s : ι → Set α), (⋃ i, s i).ncard ≤ ∑ᶠ (i : ι), (s i).ncard
-- Lean.Data.SSet
Lean.SSet.insert : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SSet α → α → Lean.SSet α