mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Action.Limits
/-- `F : C ⥤ Action V G` preserves colimits of some size
if it does after postcomposing with the forgetful functor `Action V G ⥤ V`.  -/
Action.preservesColimitsOfSize_of_preserves : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} C] (F : CategoryTheory.Functor C (Action V G)),
  CategoryTheory.Limits.PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, u_1} (F.comp (Action.forget V G)) →
    CategoryTheory.Limits.PreservesColimitsOfSize.{w₂, w₁, v_2, v_1, u_3, max (max u_1 u_2) v_1} F
-- Init.Data.Nat.Basic
Nat.lt_pred_iff_succ_lt : ∀ {n : ℕ} {m : ℕ}, n < m.pred ↔ n.succ < m
-- Mathlib.Order.UpperLower.Relative
RelLowerSet.isRelLowerSet : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α] (l : RelLowerSet P), IsRelLowerSet (↑l) P
-- Batteries.Data.Range.Lemmas
Std.Legacy.Range.size_step_1 : ∀ (start stop : ℕ), [start:stop].size = stop - start
-- Init.Data.Nat.Gcd
Nat.gcd_sub_left_right_of_dvd : ∀ {m k : ℕ} (n : ℕ), m ≤ k → n ∣ k → n.gcd (k - m) = n.gcd m
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] [inst_2 : Inhabited β],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k =
          Std.DTreeMap.Internal.Impl.Const.get! t k
-- Mathlib.Order.Filter.Pointwise
Filter.mulLeftMono : ∀ {α : Type u_2} [inst : Mul α], MulLeftMono (Filter α)
-- Mathlib.Logic.Function.DependsOn
/-- A constant function does not depend on any variable.  -/
dependsOn_const : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (b : β), DependsOn (fun x => b) ∅
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
/-- Explicit formula for the Beta function when second argument is a positive integer.  -/
Complex.betaIntegral_eval_nat_add_one_right : ∀ {u : ℂ}, 0 < u.re → ∀ (n : ℕ), u.betaIntegral (↑n + 1) = ↑n.factorial / ∏ j ∈ Finset.range (n + 1), (u + ↑j)
-- Mathlib.FieldTheory.IsPerfectClosure
pNilradical_one : ∀ {R : Type u_1} [inst : CommSemiring R], pNilradical R 1 = ⊥
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.basis_apply : ∀ {R : Type u_1} (k : Type u_7) [inst : Semiring k] (r : R),
  (AddMonoidAlgebra.basis R k) r = AddMonoidAlgebra.single r 1
-- Mathlib.Data.ENNReal.Basic
ENNReal.toNNReal_coe : ∀ (r : NNReal), (↑r).toNNReal = r
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.inr_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] (h : Y ⟶ W) (k : Z ⟶ W)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.Limits.pushout.desc h k w) =
    k
-- Init.Core
of_iff_true : ∀ {a : Prop}, (a ↔ True) → a
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiable.clm_comp : ∀ {𝕜 : 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_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {g : M → F₁ →L[𝕜] F₃}
  {f : M → F₂ →L[𝕜] F₁}, MDiff g → MDiff f → MDiff fun x => g x ∘SL f x
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.nameLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Order.Nucleus
Nucleus.restrict_toFun : ∀ {X : Type u_1} [inst : Order.Frame X] (n : Nucleus X) (a : X), n.restrict a = Set.rangeFactorization (⇑n) a
-- Mathlib.Algebra.Group.Basic
neg_neg_sub_neg : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (a b : α), -(-a - -b) = a - b
-- Mathlib.Order.Filter.Cofinite
Filter.eventually_cofinite_ne : ∀ {α : Type u_2} (x : α), ∀ᶠ (a : α) in Filter.cofinite, a ≠ x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_comp_const_mul : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p]
  [ContinuousMapZero.UniqueHom R A] (r : R) (f : R → R) (a : A),
  autoParam (ContinuousOn f ((fun x => r * x) '' quasispectrum R a)) cfcₙ_comp_const_mul._auto_1 →
    autoParam (f 0 = 0) cfcₙ_comp_const_mul._auto_3 →
      autoParam (p a) cfcₙ_comp_const_mul._auto_5 → cfcₙ (fun x => f (r * x)) a = cfcₙ f (r • a)
-- Mathlib.Data.Nat.Digits.Defs
_private.Mathlib.Data.Nat.Digits.Defs.0.Nat.ofDigits.match_1.eq_2 : ∀ (motive : List ℕ → Sort u_1) (h : ℕ) (t : List ℕ) (h_1 : Unit → motive [])
  (h_2 : (h : ℕ) → (t : List ℕ) → motive (h :: t)),
  (match h :: t with
    | [] => h_1 ()
    | h :: t => h_2 h t) =
    h_2 h t
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- Given a nonnegative nonarchimedean function `α → R` such that `f 0 = 0`, a function `g : β → α`
and a finset `t : Finset β`, we can always find `b : β`, belonging to `t` if `t` is nonempty,
such that `f (t.sum g) ≤ f (g b)` .  -/
IsNonarchimedean.finset_image_add : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {α : Type u_2} {β : Type u_3} [inst_2 : AddCommMonoid α]
  [Nonempty β] {f : α → R},
  f 0 = 0 →
    (∀ (x : α), 0 ≤ f x) →
      IsNonarchimedean f → ∀ (g : β → α) (t : Finset β), ∃ i, (t.Nonempty → i ∈ t) ∧ f (t.sum g) ≤ f (g i)
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- Given `E` and `F` two topological vector spaces and `𝔖 : Set (Set E)`, then
`UniformConvergenceCLM σ F 𝔖` (denoted `E →SLᵤ[σ, 𝔖] F`) is a type synonym of `E →SL[σ] F` equipped
with the "topology of uniform convergence on the elements of `𝔖`".

If the continuous linear image of any element of `𝔖` is bounded, this makes `E →SL[σ] F` a
topological vector space.  -/
UniformConvergenceCLM.«term_→Lᵤ[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
le_addRothNumber_product : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : AddMonoid α] [inst_2 : DecidableEq β]
  [inst_3 : AddMonoid β] (s : Finset α) (t : Finset β), addRothNumber s * addRothNumber t ≤ addRothNumber (s ×ˢ t)
-- Lean.Server.Utils
/-- Returns the document contents with the change applied.  -/
Lean.Server.applyDocumentChange : Lean.FileMap → Lean.Lsp.TextDocumentContentChangeEvent → Lean.FileMap
-- Mathlib.MeasureTheory.Measure.Regular
/-- If a measure is inner regular (using closed or compact sets) for open sets, then every
measurable set of finite measure can be approximated by a (closed or compact) subset.  -/
MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set α → Prop}
  [inst_1 : TopologicalSpace α] [μ.OuterRegular],
  μ.InnerRegularWRT p IsOpen →
    (∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)) → μ.InnerRegularWRT p fun s => MeasurableSet s ∧ μ s ≠ ⊤
-- Mathlib.Algebra.Group.Action.Sum
Sum.instSMul : {M : Type u_1} → {α : Type u_3} → {β : Type u_4} → [SMul M α] → [SMul M β] → SMul M (α ⊕ β)
-- Mathlib.Topology.Bornology.Constructions
instBoundedSpaceMultiplicative : ∀ {α : Type u_1} [inst : Bornology α] [BoundedSpace α], BoundedSpace (Multiplicative α)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.OuterMeasure.le_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] {m : (i : ι) → MeasureTheory.OuterMeasure (α i)}
  {n : MeasureTheory.OuterMeasure ((i : ι) → α i)},
  n ≤ MeasureTheory.OuterMeasure.pi m ↔
    ∀ (s : (i : ι) → Set (α i)), (Set.univ.pi s).Nonempty → n (Set.univ.pi s) ≤ ∏ i, (m i) (s i)
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.not_prime_mul_of_ble : ∀ (a b n : ℕ), a * b = n → a.ble 1 = false → b.ble 1 = false → ¬Nat.Prime n
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.id_apply : ∀ (M : Type u_1) [inst : Monoid M] {A : Type u_4} [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (x : A),
  (DistribMulActionHom.id M) x = x
-- Batteries.Control.AlternativeMonad
/-- `LawfulAlternative m` means that the `failure` operation on `m` behaves naturally
with respect to `map`, `seq`, and `orElse` operators.  -/
LawfulAlternative : (m : Type u_1 → Type u_2) → [Alternative m] → Prop
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instIsBoundedSMul : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [inst_3 : IsBoundedSMul 𝕜 E]
  [inst_4 : Fact (1 ≤ p)], IsBoundedSMul 𝕜 ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'Map_f_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i'] {i : ι} (hi : ¬e.BoundaryGE i)
  {i' : ι'} (h : e.f i = i'),
  (HomologicalComplex.truncGE'Map φ e).f i =
    CategoryTheory.CategoryStruct.comp (K.truncGE'XIso e h hi).hom
      (CategoryTheory.CategoryStruct.comp (φ.f i') (L.truncGE'XIso e h hi).inv)
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.symm_constVSub : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (p : P),
  (AffineIsometryEquiv.constVSub 𝕜 p).symm =
    (LinearIsometryEquiv.neg 𝕜).toAffineIsometryEquiv.trans (AffineIsometryEquiv.vaddConst 𝕜 p)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.eta_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g), t.eta.inv.hom = CategoryTheory.CategoryStruct.id t.pt
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.AEEqFun.integrable_iff_mem_L1 : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f : α →ₘ[μ] β}, f.Integrable ↔ f ∈ MeasureTheory.Lp β 1 μ
-- Mathlib.Data.Fintype.Sets
Fintype.finsetEquivSet_symm_apply : ∀ {α : Type u_1} [inst : Fintype α] (s : Set α) [inst_1 : Fintype ↑s], Fintype.finsetEquivSet.symm s = s.toFinset
-- Mathlib.Algebra.CharP.Two
CharTwo.sub_eq_add : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2] (x y : R), x - y = x + y
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_one_iff_enorm_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {f : α → E} {a : Filter α},
  Filter.Tendsto f a (nhds 1) ↔ Filter.Tendsto (fun x => ‖f x‖ₑ) a (nhds 0)
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- In a linearly ordered group with zero element adjoined, `U` is a neighbourhood of `0` if and
only if there exists a nonzero element `γ₀` such that `Iio γ₀ ⊆ U`.  -/
WithZeroTopology.hasBasis_nhds_zero : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀], (nhds 0).HasBasis (fun γ => γ ≠ 0) Set.Iio
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₂Rel.snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {z₁ z₂ : W.LeftFraction₂ X Y},
  CategoryTheory.MorphismProperty.LeftFraction₂Rel z₁ z₂ → CategoryTheory.MorphismProperty.LeftFractionRel z₁.snd z₂.snd
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 401 status code.
 -/
Std.Http.Response.unauthorized : Std.Http.Response.Builder
-- Mathlib.Order.Partition.Finpartition
Finpartition.combine_parts : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {ι : Type u_2} {I : Finset ι} {a : ι → α} (P : (i : ι) → Finpartition (a i)) (ha : I.SupIndep a),
  (Finpartition.combine P ha).parts = I.biUnion fun i => (P i).parts
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.adjugate_fin_two_of : ∀ {α : Type w} [inst : CommRing α] (a b c d : α), !![a, b; c, d].adjugate = !![d, -b; -c, a]
-- Mathlib.LinearAlgebra.Matrix.Permanent
/-- If `n` has only one element, the permanent of an `n` by `n` matrix is just that element.
Although `Unique` implies `DecidableEq` and `Fintype`, the instances might
not be syntactically equal. Thus, we need to fill in the args explicitly.  -/
Matrix.permanent_unique : ∀ {R : Type u_2} [inst : CommSemiring R] {n : Type u_3} [inst_1 : Unique n] [inst_2 : DecidableEq n]
  [inst_3 : Fintype n] (A : Matrix n n R), A.permanent = A default default
-- Mathlib.RingTheory.Regular.Category
LinearMap.exact_lsmul_mkQ_smul_top : ∀ {R : Type u} [inst : CommRing R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R),
  Function.Exact ⇑((LinearMap.lsmul R M) r) ⇑(r • ⊤).mkQ
-- Mathlib.CategoryTheory.Abelian.Injective.Extend
CategoryTheory.InjectiveResolution.cochainComplex_d_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Preadditive C] {X : C} (R : CategoryTheory.InjectiveResolution X) (n₁ n₂ : ℤ) (k₁ k₂ : ℕ)
  (h₁ : ↑k₁ = n₁) (h₂ : ↑k₂ = n₂) {Z : C} (h : R.cochainComplex.X n₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (R.cochainComplex.d n₁ n₂) h =
    CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n₁ k₁ h₁).hom
      (CategoryTheory.CategoryStruct.comp (R.cocomplex.d k₁ k₂)
        (CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n₂ k₂ h₂).inv h))
-- Init.Data.List.Lemmas
List.replace_take : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l : List α} {i : ℕ},
  (List.take i l).replace a b = List.take i (l.replace a b)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.HasFundamentalDomain.mk : ∀ {G : Type u_6} {α : Type u_7} [inst : One G] [inst_1 : SMul G α] [inst_2 : MeasurableSpace α]
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.HasFundamentalDomain._auto_1},
  (∃ s, MeasureTheory.IsFundamentalDomain G s ν) → MeasureTheory.HasFundamentalDomain G α ν
-- Mathlib.Probability.IdentDistrib
/-- In a second countable topology, the first function in an identically distributed pair is a.e.
strongly measurable. So is the second function, but use `h.symm.aestronglyMeasurable_fst` as
`h.aestronglyMeasurable_snd` has a different meaning.  -/
ProbabilityTheory.IdentDistrib.aestronglyMeasurable_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : TopologicalSpace γ] [TopologicalSpace.PseudoMetrizableSpace γ] [OpensMeasurableSpace γ]
  [SecondCountableTopology γ], ProbabilityTheory.IdentDistrib f g μ ν → MeasureTheory.AEStronglyMeasurable f μ
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.matcherLevels : Lean.Meta.MatcherApp → Array Lean.Level
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`.  -/
AddSubmonoid.list_sum_mem : ∀ {M : Type u_1} [inst : AddMonoid M] (s : AddSubmonoid M) {l : List M}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.Faithful.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  autoParam (∀ {X Y : C}, Function.Injective F.map) CategoryTheory.Functor.Faithful.map_injective._autoParam →
    F.Faithful
-- Mathlib.Order.Category.CompleteLat
CompleteLat.instLargeCategory : CategoryTheory.LargeCategory CompleteLat
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algebraMap_apply : ∀ {R : Type u} {A : Type z} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (algebraMap R (Polynomial A)) r = Polynomial.C ((algebraMap R A) r)
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Composing on the left by a uniformly continuous function preserves
uniform Cauchy sequences  -/
UniformContinuous.comp_uniformCauchySeqOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α}
  {p : Filter ι} [inst_1 : UniformSpace γ] {g : β → γ},
  UniformContinuous g → UniformCauchySeqOn F p s → UniformCauchySeqOn (fun n => g ∘ F n) p s
-- Mathlib.Data.Fintype.Defs
Fintype.nodup_map_univ_iff_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {f : α → β},
  (Multiset.map f Finset.univ.val).Nodup ↔ Function.Injective f
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.Measure.sigmaFiniteSet.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α), μ.sigmaFiniteSet = μ.sigmaFiniteSetWRT μ
-- Mathlib.RingTheory.Derivation.Lie
/-- Let `σ : A → A'` be a an homomorphism. A derivation `d : A → A` and a derivation
`d' : A' → A'` are called compatible if `d' ∘ σ = σ ∘ d`. Couples of derivations
with this property form a Lie subalgebra of all couples of derivations.  -/
Derivation.couple : (R : Type u_1) →
  [inst : CommRing R] →
    (A : Type u_2) →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          (A' : Type u_3) →
            [inst_3 : CommRing A'] →
              [inst_4 : Algebra R A'] →
                [inst_5 : Algebra A A'] →
                  [IsScalarTower R A A'] → LieSubalgebra R (Derivation R A' A' × Derivation R A A)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerRight.of.inj : ∀ {η η_1 : Mathlib.Tactic.BicategoryLike.Atom},
  Mathlib.Tactic.BicategoryLike.WhiskerRight.of η = Mathlib.Tactic.BicategoryLike.WhiskerRight.of η_1 → η = η_1
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` preserves limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits.  -/
CategoryTheory.Limits.preservesColimits_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesLimits F.unop],
  CategoryTheory.Limits.PreservesColimits F
-- Init.Data.BitVec.Lemmas
/-- The absolute value of `x : BitVec w` is a case split on the sign of `x`, when `x ≠ intMin w`.
This is a variant of `toInt_abs_eq_ite`.
 -/
BitVec.toInt_abs_eq_ite_of_ne_intMin : ∀ {w : ℕ} {x : BitVec w}, x ≠ BitVec.intMin w → x.abs.toInt = if x.msb = true then -x.toInt else x.toInt
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.assoc_symm_tmul : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} {D : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Semiring A] [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring C] [inst_8 : Semiring D] [inst_9 : Bialgebra S C]
  [inst_10 : Bialgebra R D] [inst_11 : Algebra R C] [inst_12 : IsScalarTower R S C] (x : A) (y : C) (z : D),
  (Bialgebra.TensorProduct.assoc R S A C D).symm (x ⊗ₜ[S] (y ⊗ₜ[R] z)) = x ⊗ₜ[S] y ⊗ₜ[R] z
-- Mathlib.Topology.Separation.Basic
/-- Two inseparable points in a T₀ space are equal.  -/
T0Space.t0 : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T0Space X] ⦃x y : X⦄, Inseparable x y → x = y
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.algebraMap_eq_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂) {y : R} {x : A₁},
  (algebraMap R A₂) y = e x ↔ (algebraMap R A₁) y = x
-- Lean.Parser.Syntax
Lean.Parser.precedence.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.Comparable
instTransAntisymmRelLeCompRel : {α : Type u_1} →
  [inst : Preorder α] →
    Trans (AntisymmRel fun x1 x2 => x1 ≤ x2) (CompRel fun x1 x2 => x1 ≤ x2) (CompRel fun x1 x2 => x1 ≤ x2)
-- Init.Data.Array.Basic
/-- See comment at `forIn'Unsafe`  -/
Array.foldrMUnsafe : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} → [Monad m] → (α → β → m β) → β → (as : Array α) → optParam ℕ as.size → optParam ℕ 0 → m β
-- Mathlib.Topology.Compactness.Compact
/-- The comap of the cocompact filter on `Y` by a continuous function `f : X → Y` is less than or
equal to the cocompact filter on `X`.
This is a reformulation of the fact that images of compact sets are compact.  -/
Filter.comap_cocompact_le : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Filter.comap f (Filter.cocompact Y) ≤ Filter.cocompact X
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft_eq_zipWithLeftTR.go : ∀ (α : Type u_3) (β : Type u_2) (γ : Type u_1) (f : α → Option β → γ) (acc : Array γ) (as : List α) (bs : List β),
  List.zipWithLeftTR.go f as bs acc = acc.toList ++ List.zipWithLeft f as bs
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch.stackPos_le_size : ∀ {pat s : ByteArray} {needlePos stackPos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos → stackPos ≤ s.size
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_def : ∀ {𝔸 : Type u_3} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] (x : 𝔸),
  NormedSpace.exp x = if h : Nonempty (Algebra ℚ 𝔸) then (NormedSpace.expSeries ℚ 𝔸).sum x else 1
-- Plausible.Functions
Plausible.TotalFunction.Pi.sampleableExt : {α : Type u} →
  {β : Type v} →
    [Plausible.SampleableExt α] →
      [Plausible.SampleableExt β] → [DecidableEq α] → [Repr α] → Plausible.SampleableExt (α → β)
-- Mathlib.RingTheory.IdealFilter.Basic
/-- Characterization of Gabriel filters via `IsUniform` and idempotence of
`gabrielComposition`.  -/
IdealFilter.isGabriel_iff : ∀ {A : Type u_1} [inst : Ring A] (F : IdealFilter A), F.IsGabriel ↔ F.IsUniform ∧ F.gabrielComposition F = F
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.instInhabitedNormalExpr : Inhabited Mathlib.Tactic.Abel.NormalExpr
-- Mathlib.Tactic.Widget.SelectPanelUtils
instRpcEncodableSelectInsertParams : Lean.Server.RpcEncodable SelectInsertParams
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.conjugator.nil : ∀ {α : Type u} [inst : DecidableEq α], FreeAddGroup.reduceCyclically.conjugator [] = []
-- Init.Data.Nat.Div.Basic
Nat.le_div_iff_mul_le : ∀ {k x y : ℕ}, 0 < k → (x ≤ y / k ↔ x * k ≤ y)
-- Lean.Environment
Lean.PersistentEnvExtension.mk : {α β σ : Type} →
  Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ) →
    Lean.Name →
      (Array (Array α) → Lean.ImportM σ) →
        (σ → β → σ) →
          (Lean.Environment → σ → Lean.OLeanEntries (Array α)) → (σ → Std.Format) → Lean.PersistentEnvExtension α β σ
-- Mathlib.Order.CompleteLattice.Basic
iSup_iSup_eq_left : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {b : β} {f : (x : β) → x = b → α},
  ⨆ x, ⨆ (h : x = b), f x h = f b ⋯
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.nextCoeff_mul : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.Monic → q.Monic → (p * q).nextCoeff = p.nextCoeff + q.nextCoeff
-- Mathlib.Order.Hom.Bounded
BotHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β] (f : BotHom α β) (f' : α → β) (h : f' = ⇑f),
  f.copy f' h = f