mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- In a Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero, if `x` and `y` are
in the disk of convergence and commute, then
`NormedSpace.exp (x + y) = (NormedSpace.exp x) * (NormedSpace.exp y)`.  -/
NormedSpace.exp_add_of_commute_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] [CharZero 𝕂] {x y : 𝔸},
  Commute x y →
    x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
      y ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
        NormedSpace.exp (x + y) = NormedSpace.exp x * NormedSpace.exp y
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_sdiff_le_iff_le_add`. -/
MeasureTheory.measure_diff_le_iff_le_add : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → s ⊆ t → μ s ≠ ⊤ → ∀ {ε : ENNReal}, μ (t \ s) ≤ ε ↔ μ t ≤ μ s + ε
-- Plausible.Testable
Plausible.Bool.printableProp : {b : Bool} → Plausible.PrintableProp (b = true)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.neg_apply : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M) (a : A), (-D) a = -D a
-- Init.Data.Order.MinMaxOn
maxOn_eq_max : ∀ {α : Type u_1} {β : Type u_2} [inst : Max α] [inst_1 : LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMax α]
  [inst_4 : LE β] [inst_5 : DecidableLE β] {f : α → β} {a b : α}, (f b ≤ f a ↔ b ≤ a) → maxOn f a b = a ⊔ b
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sigma.isOpen_iff : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] (s : Set ((i : ι) × E i)),
  IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (i : ι) × E i), dist x y < ε → y ∈ s
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.Hom.hom'_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.ProjectiveResolution X} {X' : C} {R' : CategoryTheory.ProjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f) (n : ℤ) (m : ℕ) (h : -↑m = n),
  φ.hom'.f n =
    CategoryTheory.CategoryStruct.comp (R.cochainComplexXIso n m h).hom
      (CategoryTheory.CategoryStruct.comp (φ.hom.f m) (R'.cochainComplexXIso n m h).inv)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {k fallback : α}, (cmp k (t.minKeyD fallback)).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The indexing type of the cells of dimension `n`.  -/
Topology.RelCWComplex.cell : {X : Type u} →
  {inst : TopologicalSpace X} → (C : Set X) → {D : outParam (Set X)} → [self : Topology.RelCWComplex C D] → ℕ → Type u
-- Mathlib.GroupTheory.Coxeter.Basic
/-- The simple reflections of `W` generate `W` as a monoid.  -/
CoxeterSystem.submonoid_closure_range_simple : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W),
  Submonoid.closure (Set.range cs.simple) = ⊤
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_compQuasiMeasurePreserving : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} {f : α → β} (g : β →ₘ[ν] γ)
  (hf : MeasureTheory.Measure.QuasiMeasurePreserving f μ ν), ↑(g.compQuasiMeasurePreserving f hf) =ᵐ[μ] ↑g ∘ f
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.Hom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (hom : F.toFunctor ⟶ G.toFunctor)
  (isMonoidal :
    autoParam (CategoryTheory.NatTrans.IsMonoidal hom) CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal._autoParam)
  (hom_1 : F.toFunctor ⟶ G.toFunctor)
  (isMonoidal_1 :
    autoParam (CategoryTheory.NatTrans.IsMonoidal hom_1) CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal._autoParam),
  ({ hom := hom, isMonoidal := isMonoidal } = { hom := hom_1, isMonoidal := isMonoidal_1 }) = (hom = hom_1)
-- Mathlib.Lean.Expr.Basic
/-- Turn a `ConstantInfo` into a declaration.  -/
Lean.ConstantInfo.toDeclaration! : Lean.ConstantInfo → Lean.Declaration
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.Extension.comp_eq : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] {ψ : K →+* ℂ} [inst_2 : Algebra K L]
  (φ : NumberField.ComplexEmbedding.Extension L ψ), (↑φ).comp (algebraMap K L) = ψ
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalCommSemiring.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommSemigroup M],
  AddMonoidAlgebra.nonUnitalCommSemiring = { toNonUnitalSemiring := AddMonoidAlgebra.nonUnitalSemiring, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
/-- The underlying morphism in the first component.  -/
CategoryTheory.Limits.ColimitPresentation.Total.Hom.base : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u_1} →
      {I : J → Type u_2} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)] →
            {D : CategoryTheory.Functor J C} →
              {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)} →
                {k l : CategoryTheory.Limits.ColimitPresentation.Total P} → k.Hom l → (k.fst ⟶ l.fst)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isClosed_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y) {s : Set Y},
  IsClosed (⇑h ⁻¹' s) ↔ IsClosed s
-- Init.Data.String.Slice
/-- Creates a new slice that contains the suffix prefix of `s` for which `pat` matched
\(potentially repeatedly\).

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".toSlice.takeEndWhile Char.isLower == "blue".toSlice`

* `"red green blue".toSlice.takeEndWhile 'e' == "e".toSlice`

* `"red green blue".toSlice.takeEndWhile (fun (_ : Char) => true) == "red green blue".toSlice`
 -/
String.Slice.takeEndWhile : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → String.Slice
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
/-- The restriction of an algebra norm in a scalar tower.  -/
AlgebraNorm.isScalarTower_restriction : {R : Type u_1} →
  [inst : SeminormedCommRing R] →
    {S : Type u_2} →
      [inst_1 : Ring S] →
        [inst_2 : Algebra R S] →
          {A : Type u_3} →
            [inst_3 : CommRing A] →
              [inst_4 : Algebra R A] →
                [inst_5 : Algebra A S] →
                  [IsScalarTower R A S] → Function.Injective ⇑(algebraMap A S) → AlgebraNorm R S → AlgebraNorm R A
-- Mathlib.Analysis.Normed.Algebra.DualNumber
DualNumber.exp_eps : ∀ {R : Type u_1} [inst : CommRing R] [Algebra ℚ R] [inst_2 : UniformSpace R] [inst_3 : IsTopologicalRing R] [T2Space R],
  NormedSpace.exp DualNumber.eps = 1 + DualNumber.eps
-- Mathlib.Analysis.SpecificLimits.Normed
hasSum_choose_mul_geometric_of_norm_lt_one' : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R},
  ‖r‖ < 1 → HasSum (fun n => ↑((n + k).choose k) * r ^ n) (Ring.inverse (1 - r) ^ (k + 1))
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.insert_erase : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} {a b : α} [inst : DecidableEq α],
  G.IsNClique n s → (∀ w ∈ s \ {b}, G.Adj a w) → b ∈ s → G.IsNClique n (insert a (s.erase b))
-- Mathlib.Algebra.Module.Presentation.DirectSum
Module.Presentation.finsupp_G : ∀ {A : Type u} [inst : Ring A] {N : Type v} [inst_1 : AddCommGroup N] [inst_2 : Module A N]
  (pres : Module.Presentation A N) (ι : Type w) [inst_3 : DecidableEq ι] [inst_4 : DecidableEq N],
  (pres.finsupp ι).G = ((i : ι) × pres.G)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.inv_tensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) [inst_2 : CategoryTheory.IsIso f] (g : Y ⟶ Z) [inst_3 : CategoryTheory.IsIso g],
  CategoryTheory.inv (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.inv f) (CategoryTheory.inv g)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.face_mono : ∀ {n : ℕ} {I J : BoxIntegral.Box (Fin (n + 1))}, I ≤ J → ∀ (i : Fin (n + 1)), I.face i ≤ J.face i
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.finite_of_finite : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : Algebra R S] [IsLocalHom (algebraMap R S)] [Module.Finite R S],
  Finite (IsLocalRing.ResidueField R) → Finite (IsLocalRing.ResidueField S)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- `ContinuousLinearMap.compContinuousAlternatingMap` as a bundled continuous bilinear map.

Given a continuous linear map `g : F →L[𝕜] G` and a continuous alternating map `f : E [⋀^ι]→L[𝕜] F`,
it returns the continuous alternating map `g ∘ f`.
This function is continuous in `f` (for each `g`)
and in `g` (as a function taking values in continuous linear maps).
Note that for a general topological vector space,
the map is not guaranteed to be continuous in `(g, f)`.
 -/
ContinuousLinearMap.compContinuousAlternatingMapCLM : (𝕜 : Type u_1) →
  (E : Type u_2) →
    (F : Type u_3) →
      (G : Type u_4) →
        (ι : Type u_5) →
          [inst : NormedField 𝕜] →
            [inst_1 : AddCommGroup E] →
              [inst_2 : Module 𝕜 E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : Module 𝕜 F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : IsTopologicalAddGroup F] →
                          [inst_8 : ContinuousConstSMul 𝕜 F] →
                            [inst_9 : AddCommGroup G] →
                              [inst_10 : Module 𝕜 G] →
                                [inst_11 : TopologicalSpace G] →
                                  [inst_12 : IsTopologicalAddGroup G] →
                                    [inst_13 : ContinuousConstSMul 𝕜 G] →
                                      (F →L[𝕜] G) →L[𝕜] E [⋀^ι]→L[𝕜] F →L[𝕜] E [⋀^ι]→L[𝕜] G
-- Std.Data.Iterators.Combinators.Monadic.StepSize
Std.Iterators.Types.StepSizeIterator.instIterator : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorAccess α m] → [Monad m] → Std.Iterator (Std.Iterators.Types.StepSizeIterator α m β) m β
-- Mathlib.Data.Set.Lattice
Set.BijOn.iUnion_congr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set β} {t : Set γ} (f : β → Set α) (g : γ → Set α) {h : β → γ},
  Set.BijOn h s t → (∀ (x : β), g (h x) = f x) → ⋃ x ∈ s, f x = ⋃ y ∈ t, g y
-- Mathlib.Algebra.BigOperators.Group.Finset.Interval
Finset.prod_Icc_succ_eq_mul_endpoints : ∀ {R : Type u_1} [inst : CommGroup R] (f : ℤ → R) {N : ℕ},
  ∏ m ∈ Finset.Icc (-(↑N + 1)) (↑N + 1), f m = f (↑N + 1) * f (-(↑N + 1)) * ∏ m ∈ Finset.Icc (-↑N) ↑N, f m
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex
/-- If `X` is a Kan complex and `f : ∀ (j : Fin (n + 2)) (_ : j ≠ i), Δ[n] ⟶ X`
is a compatible family of morphisms (which defines a morphism `Λ[n + 1, i] ⟶ X`),
then this is a lifting `Δ[n + 1] ⟶ X`.  -/
SSet.horn.IsCompatible.liftOfKanComplex : {X : SSet} →
  {n : ℕ} →
    {i : Fin (n + 2)} →
      {f : (j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)} →
        [X.KanComplex] → SSet.horn.IsCompatible f → (SSet.stdSimplex.obj { len := n + 1 } ⟶ X)
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.mem_twoCocycle_iff_of_trivial : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [LieModule.IsTrivial L M] (a : ↥(LieModule.Cohomology.twoCochain R L M)),
  a ∈ LieModule.Cohomology.twoCocycle R L M ↔ ∀ (x y z : L), (a x) ⁅y, z⁆ = (a ⁅x, y⁆) z + (a y) ⁅x, z⁆
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.star_apply' : ∀ {R : Type u_1} [inst : CommRing R] [Finite Rˣ] (χ : MulChar R ℂ) (a : R), star (χ a) = χ⁻¹ a
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.toInvSubmonoid.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S], IsLocalization.toInvSubmonoid M S = IsLocalization.toInvSubmonoid M S
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.zero_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {x : ℝ}, x ≠ 0 → CFC.rpow 0 x = 0
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.coe_copy_eq : ∀ {M : Type u_4} {N : Type u_5} {x : Add M} {x_1 : Add N} (f : M →ₙ+ N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Control.Fix
_private.Mathlib.Control.Fix.0.Part.Fix.approx.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (i : ℕ) → motive i.succ),
  (match 0 with
    | 0 => h_1 ()
    | i.succ => h_2 i) =
    h_1 ()
-- Mathlib.Order.Filter.IsBounded
Filter.Tendsto.isBoundedUnder_le_atBot : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [Nonempty α] {f : Filter β} {u : β → α},
  Filter.Tendsto u f Filter.atBot → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u
-- Mathlib.Data.PNat.Basic
PNat.sub_coe : ∀ (a b : ℕ+), ↑(a - b) = if b < a then ↑a - ↑b else 1
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Permuting the rows changes the sign of the determinant.  -/
Matrix.det_permute' : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (σ : Equiv.Perm n)
  (M : Matrix n n R), (M.submatrix id ⇑σ).det = ↑↑(Equiv.Perm.sign σ) * M.det
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.comp' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A₁ A₂ A₃ : CategoryTheory.Grp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Analysis.LocallyConvex.Separation
RCLike.geometric_hahn_banach_point_open : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {t : Set E}
  {x : E} [inst_3 : RCLike 𝕜] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E], Convex ℝ t → IsOpen t → x ∉ t → ∃ f, ∀ b ∈ t, RCLike.re (f x) < RCLike.re (f b)
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- A choice of chart on the domain `M` of the local property `P` of `f` at `x`:
w.r.t. this chart and `codChart`, `f` has the local property `P` at `x`.  -/
Manifold.LocalPresentationAt.domChart : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_4} →
      {H : Type u_6} →
        {G : Type u_8} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : NormedSpace 𝕜 E] →
                [inst_3 : NormedAddCommGroup F] →
                  [inst_4 : NormedSpace 𝕜 F] →
                    [inst_5 : TopologicalSpace H] →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 F G} →
                            {M : Type u_10} →
                              {N : Type u_12} →
                                [inst_7 : TopologicalSpace M] →
                                  [inst_8 : ChartedSpace H M] →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} →
                                          {f : M → N} →
                                            {x : M} →
                                              {P :
                                                  (M → N) →
                                                    OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop} →
                                                Manifold.LocalPresentationAt I J n f x P → OpenPartialHomeomorph M H
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.instInhabitedSimpM : {α : Type} → Inhabited (Lean.Meta.Sym.Simp.SimpM α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableOn.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {s : Set E},
  DifferentiableOn ℝ f s → DifferentiableOn ℝ g s → (∀ x ∈ s, f x ≠ 0) → DifferentiableOn ℝ (fun x => f x ^ g x) s
-- Mathlib.Topology.UniformSpace.Equicontinuity
uniformEquicontinuousOn_unique : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} [uα : UniformSpace α] [uβ : UniformSpace β] [inst : Unique ι]
  {F : ι → β → α} {S : Set β}, UniformEquicontinuousOn F S ↔ UniformContinuousOn (F default) S
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.isLocalizing_of_iso : ∀ {R : CommRingCat} {M N : TopCat.Sheaf (ModuleCat ↑R) ↑(AlgebraicGeometry.Spec R).toPresheafedSpace} (φ : M ≅ N),
  AlgebraicGeometry.IsLocalizing M → AlgebraicGeometry.IsLocalizing N
-- Mathlib.Analysis.InnerProductSpace.Basic
real_inner_smul_right : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F) (r : ℝ),
  inner ℝ x (r • y) = r * inner ℝ x y
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
_private.Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization.0.termAt_ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.liftOfSurjective.eq_1 : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (hf : Function.Surjective ⇑f), f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) ⋯
-- Mathlib.Order.WithBot
WithTop.some_eq_coe : ∀ {α : Type u_1} (a : α), some a = ↑a
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanShape_R : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C], (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).R = Unit
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.precomposeEquivalence_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} (α : F ≅ G),
  (CategoryTheory.Limits.Cocone.precomposeEquivalence α).inverse = CategoryTheory.Limits.Cocone.precompose α.hom
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.instHomeomorphClass : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂],
  HomeomorphClass (P₁ ≃ᴬ[k] P₂) P₁ P₂
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.of_isKan_whisker : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] (t : CategoryTheory.Bicategory.LeftLift f g) {x : B}
  (h : x ⟶ c) (H : (t.whisker h).IsKan) (i : t.whisker h ≅ (CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h),
  CategoryTheory.Bicategory.LanLift.CommuteWith f g h
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.mk : {M : Type u_1} → [inst : MulOneClass M] → (toSubmonoid : Submonoid M) → toSubmonoid.MulSaturated → SaturatedSubmonoid M
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.brecOn.eq : ∀ {motive_1 : Lean.Elab.Tactic.RCases.RCasesPatt → Sort u} {motive_2 : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u}
  (t : Lean.Elab.Tactic.RCases.RCasesPatt) (F_1 : (t : Lean.Elab.Tactic.RCases.RCasesPatt) → t.below → motive_1 t)
  (F_2 : (t : List Lean.Elab.Tactic.RCases.RCasesPatt) → Lean.Elab.Tactic.RCases.RCasesPatt.below_1 t → motive_2 t),
  t.brecOn F_1 F_2 = F_1 t (Lean.Elab.Tactic.RCases.RCasesPatt.brecOn.go t F_1 F_2).2
-- Lean.Expr
/-- `.app f a` is now the preferred form.
 -/
Lean.mkApp : Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Order.Filter.Defs
/-- Two functions `f` and `g` are *eventually equal* along a filter `l` if the set of `x` such that
`f x = g x` belongs to `l`.  -/
Filter.EventuallyEq : {α : Type u_1} → {β : Type u_2} → Filter α → (α → β) → (α → β) → Prop
-- Lean.Elab.MutualDef
/-- Return `some [a, b, c]` if the given `views` are representing a declaration of the form
```
example a b c : Nat := ...
```
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.isExampleParams? : Array Lean.Elab.DefView → Option (List Lean.Name)
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.tensorProductEquivOfMapIncludeRight_tmul : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_9)
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (M : Submonoid A) (B : Type u_10) [inst_5 : CommSemiring B]
  [inst_6 : Algebra R B] [inst_7 : Algebra A B] [inst_8 : IsScalarTower R A B] [inst_9 : IsLocalization M B]
  (C : Type u_11) [inst_10 : CommSemiring C] [inst_11 : Algebra S C] [inst_12 : Algebra (TensorProduct R S A) C]
  [inst_13 : IsScalarTower S (TensorProduct R S A) C]
  [inst_14 : IsLocalization (Submonoid.map Algebra.TensorProduct.includeRight M) C] (x : S) (a : A),
  (IsLocalization.tensorProductEquivOfMapIncludeRight R S M B C) (x ⊗ₜ[R] (algebraMap A B) a) =
    (algebraMap (TensorProduct R S A) C) (x ⊗ₜ[R] a)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.brecOn_2.eq : ∀ {pu : Lean.Compiler.LCNF.Purity} {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u}
  {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u}
  {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u}
  {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} (t : List (Lean.Compiler.LCNF.Alt pu))
  (F_1 : (t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t)
  (F_2 : (t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t)
  (F_3 : (t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t)
  (F_4 : (t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t)
  (F_5 : (t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t)
  (F_6 : (t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t),
  Lean.Compiler.LCNF.Alt.brecOn_2 t F_1 F_2 F_3 F_4 F_5 F_6 =
    F_6 t (Lean.Compiler.LCNF.Alt.brecOn_2.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_neg : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a (-b) = -(toIcoDiv hp (-a) b + 1)
-- Mathlib.Topology.ContinuousMap.Defs
ContinuousMap.ext_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)},
  f = g ↔ ∀ (a : X), f a = g a