mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- Let `K` be a field with an admissible family of absolute values (giving rise
to a logarithmic height).
Let `p` be a family (indexed by `ι'`) of homogeneous polynomials in variables indexed by
the finite type `ι` and of the same degree `N`. Then for any `x : ι →  K`,
the logarithmic height of `fun j : ι' ↦ eval x (p j)` is bounded by a constant
plus `N * logHeight x`.

The difference to `logHeight_eval_le` is that the constant is not made explicit.  -/
Height.logHeight_eval_le' : ∀ {K : Type u_4} [inst : Field K] {ι : Type u_5} {ι' : Type u_6} [inst_1 : Height.AdmissibleAbsValues K] [Finite ι']
  [Finite ι] {N : ℕ} {p : ι' → MvPolynomial ι K},
  (∀ (i : ι'), (p i).IsHomogeneous N) →
    ∃ C, ∀ (x : ι → K), (Height.logHeight fun j => (MvPolynomial.eval x) (p j)) ≤ C + ↑N * Height.logHeight x
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_toList_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {k : α} {v : β},
  (k, v) ∈ m.toList ↔ m[k]? = some v
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂) {Z : C}
  (h_1 :
    CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h)) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom h_1)
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- Given `Λ : LeftResolution ι`, the chain complex `Λ.chainComplex X`
identifies in degree `1` to `Λ.F.obj (kernel (Λ.π.app X))`.  -/
CategoryTheory.Abelian.LeftResolution.chainComplexXOneIso : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          (Λ : CategoryTheory.Abelian.LeftResolution ι) →
            (X : A) →
              [inst_2 : ι.Full] →
                [inst_3 : ι.Faithful] →
                  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] →
                    [inst_5 : CategoryTheory.Abelian A] →
                      (Λ.chainComplex X).X 1 ≅ Λ.F.obj (CategoryTheory.Limits.kernel (Λ.π.app X))
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.opensDiagram_obj : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (i : I)
  (U : (D.obj i).Opens) (j : CategoryTheory.Over i),
  (AlgebraicGeometry.opensDiagram D i U).obj j = ↑((TopologicalSpace.Opens.map (D.map j.hom).base).obj U)
-- Mathlib.Topology.Compactness.Lindelof
IsLindelof.countable : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s → DiscreteTopology ↑s → s.Countable
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.descResidueField.congr_simp : ∀ {K : Type u} [inst : Field K] {X : AlgebraicGeometry.Scheme} {x : ↥X} (f f_1 : X.presheaf.stalk x ⟶ CommRingCat.of K)
  (e_f : f = f_1) [inst_1 : IsLocalHom (CommRingCat.Hom.hom f)],
  AlgebraicGeometry.Scheme.descResidueField f = AlgebraicGeometry.Scheme.descResidueField f_1
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_inter' : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s t : Set M} {x : M}
  {n : WithTop ℕ∞}, t ∈ nhdsWithin x s → (ContMDiffWithinAt I I' n f (s ∩ t) x ↔ ContMDiffWithinAt I I' n f s x)
-- Mathlib.Topology.Order.SuccPred
AccPt.not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  {a : α} {s : Set α}, AccPt a (Filter.principal s) → ¬IsMax a
-- Init.Classical
Classical.byCases : ∀ {p q : Prop}, (p → q) → (¬p → q) → q
-- Mathlib.Tactic.Linarith.Frontend
/-- A configuration object for `linarith`.  -/
Mathlib.Tactic.Linarith.LinarithConfig : Type
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If M is the midpoint of the segment AB, then ∠AMB = π.  -/
EuclideanGeometry.angle_midpoint_eq_pi : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ : P), p₁ ≠ p₂ → EuclideanGeometry.angle p₁ (midpoint ℝ p₁ p₂) p₂ = Real.pi
-- Mathlib.Order.CompleteLattice.Defs
CompleteSemilatticeInf.toInfSet : {α : Type u_8} → [self : CompleteSemilatticeInf α] → InfSet α
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a family of compact subsets of `X`, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the topologies
of uniform convergence on `𝔖` and pointwise convergence on `⋃₀ 𝔖` induce the same topology on  `ι`.

In particular, pointwise convergence and compact convergence coincide on an equicontinuous
subset of `X → α`.

This is a consequence of `EquicontinuousOn.comap_uniformOnFun_eq` stated in terms of `IsInducing`
for convenience.  -/
EquicontinuousOn.inducing_uniformOnFun_iff_pi' : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : TopologicalSpace ι] {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    (∀ K ∈ 𝔖, EquicontinuousOn F K) →
      (Topology.IsInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Topology.IsInducing ((⋃₀ 𝔖).domRestrict ∘ F))
-- Mathlib.Data.Set.Restrict
Set.surjective_mapsTo_image_restrict : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Function.Surjective (Set.MapsTo.restrict f s (f '' s) ⋯)
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.add_right : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : MeasureTheory.Measure α},
  μ.MutuallySingular ν₁ → μ.MutuallySingular ν₂ → μ.MutuallySingular (ν₁ + ν₂)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Define a morphism between right lifts by cancelling the whiskered identities.  -/
CategoryTheory.Bicategory.RightLift.whiskerIdCancel : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (t :
              CategoryTheory.Bicategory.RightLift f
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)) →
            {s : CategoryTheory.Bicategory.RightLift f g} →
              (s.whisker (CategoryTheory.CategoryStruct.id c) ⟶ t) → (s ⟶ t.ofIdComp)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The equivalence between the rational points on an elliptic curve `E` and the set of pairs
`⟨x, y⟩` satisfying `E.Equation x y` with zero.  -/
WeierstrassCurve.Affine.pointEquiv : {R : Type r} →
  [inst : CommRing R] →
    (W' : WeierstrassCurve.Affine R) →
      [Nontrivial R] → [WeierstrassCurve.IsElliptic W'] → W'.Point ≃ WithZero { xy // W'.Equation xy.1 xy.2 }
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHomEq_hom_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} {f g : T₁ ⟶ T₂} (h : f = g)
  (X : T₂.Algebra),
  ((CategoryTheory.Monad.algebraFunctorOfMonadHomEq h).hom.app X).f =
    (CategoryTheory.Iso.refl ((CategoryTheory.Monad.algebraFunctorOfMonadHom f).obj X).A).hom
-- Lean.Meta.DiscrTree.Main
/-- Find values that match `e` in `d`.
 -/
Lean.Meta.DiscrTree.getMatch : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → Lean.MetaM (Array α)
-- Init.Data.List.Count
List.count_le_length : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, List.count a l ≤ l.length
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.Scheme.Modules.map_smul_Spec : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {U V : (AlgebraicGeometry.Spec R).Opens}
  (hUV : Opposite.op V ⟶ Opposite.op U) (f : ↑R) (x : ↑(M.presheaf.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (M.presheaf.map hUV)) (f • x) =
    f • (CategoryTheory.ConcreteCategory.hom (M.presheaf.map hUV)) x
-- Mathlib.Data.Finset.Lattice.Prod
Finset.inf_sup_inf : ∀ {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [inst : DistribLattice α] [inst_1 : OrderTop α] (s : Finset ι)
  (t : Finset κ) (f : ι → α) (g : κ → α), s.inf f ⊔ t.inf g = (s ×ˢ t).inf fun i => f i.1 ⊔ g i.2
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nndist_toLp_single_same : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b₁ b₂ : β i),
  nndist (WithLp.toLp p (Pi.single i b₁)) (WithLp.toLp p (Pi.single i b₂)) = nndist b₁ b₂
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mk_mem_iff : ∀ {x y : PSet.{u_1}}, ZFSet.mk x ∈ ZFSet.mk y ↔ x ∈ y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.iteratedDeriv_add_one_sin : ∀ (n : ℕ), iteratedDeriv (n + 1) Complex.sin = iteratedDeriv n Complex.cos
-- Mathlib.CategoryTheory.Endomorphism
/-- Assist the typechecker by expressing an endomorphism `f : CategoryTheory.End X` as a term of
`X ⟶ X`.  -/
CategoryTheory.End.asHom : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → {X : C} → CategoryTheory.End X → (X ⟶ X)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ ∩ m₂},
  (m₁ ∩ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.Order.Interval.Finset.Fin
Fin.Ico_add_one_eq_Icc : ∀ {n : ℕ} {a b : Fin n}, ↑b + 1 < n → Finset.Ico a (b + 1) = Finset.Icc a b
-- Mathlib.Control.Traversable.Instances
Sum.traverse_eq_map_id : ∀ {σ α β : Type u} (f : α → β) (x : σ ⊕ α), Sum.traverse (pure ∘ f) x = pure (f <$> x)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntry.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.isEmpty = false → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : x.isEmpty = false) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                    (x :
                        (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
                      motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β) →
                            (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                              (h :
                                  (Std.DTreeMap.Internal.Impl.inner size k v l
                                        (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
                                    false) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v l
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                  h) →
              motive x x_1
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The map `R[X₁, ..., Xₙ] → S` factors via `T`, because the `bᵢ` are in `I`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.hom : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D →ₐ[R] S
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.comp₁ : ∀ {n : ℕ} (f : ℕ →. ℕ) {g : List.Vector ℕ n → ℕ},
  (Nat.Partrec' fun v => f v.head) → Nat.Partrec' ↑g → Nat.Partrec' fun v => f (g v)
-- Mathlib.Order.SupClosed
supClosed_pi : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → SemilatticeSup (α i)] {s : Set ι} {t : (i : ι) → Set (α i)},
  (∀ i ∈ s, SupClosed (t i)) → SupClosed (s.pi t)
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lcongr_symm : ∀ {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ : R →+* R₂}
  {σ_inv : R₂ →+* R} [inst_6 : RingHomInvPair σ σ_inv] [inst_7 : RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10}
  (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N), (Finsupp.lcongr e₁ e₂).symm = Finsupp.lcongr e₁.symm e₂.symm
-- Mathlib.Algebra.GroupWithZero.InjSurj
Function.Injective.isLeftCancelMulZero : ∀ {M₀ : Type u_1} {M₀' : Type u_3} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : Mul M₀'] [inst_3 : Zero M₀']
  (f : M₀ → M₀'),
  Function.Injective f →
    f 0 = 0 → (∀ (x y : M₀), f (x * y) = f x * f y) → ∀ [IsLeftCancelMulZero M₀'], IsLeftCancelMulZero M₀
-- Lean.Parser.Term
Lean.Parser.Term.binrel_no_prop.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- Hausdorff measure on an (e)metric space.  -/
MeasureTheory.«termμH[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Interval.Set.Instances
/-- The coercion from `Set.Ico 0 1` as a `MulHom`.  -/
Set.Ico.coeMulHom : {R : Type u_1} → [inst : Semiring R] → [inst_1 : PartialOrder R] → [inst_2 : IsOrderedRing R] → ↑(Set.Ico 0 1) →ₙ* R
-- Mathlib.Algebra.Free
FreeAddMagma.instInhabited : {α : Type u} → [Inhabited α] → Inhabited (FreeAddMagma α)
-- Lean.Elab.App
/-- If the eliminator is over-applied, we "revert" the extra arguments.
Returns the function with the reverted arguments applied and the new generalized expected type.
 -/
Lean.Elab.Term.ElabElim.revertArgs : List Lean.Elab.Term.Arg → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)
-- Lean.Class
Lean.ClassState.addEntry : Lean.ClassState → Lean.ClassEntry → Lean.ClassState
-- Std.Http.Protocol.H1
/-- Classifies hard request start-line parse failures into protocol-level errors.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.classifyStartLineHardError : Std.Internal.Parsec.Error → Std.Http.Protocol.H1.Error
-- Mathlib.Algebra.RingQuot
RingQuot.instCommSemiring : {R : Type uR} → [inst : CommSemiring R] → (r : R → R → Prop) → CommSemiring (RingQuot r)
-- Init.Data.Order.Ord
Std.instOrientedCmpCompareLex : ∀ {α : Type u_1} {cmp₁ cmp₂ : α → α → Ordering} [Std.OrientedCmp cmp₁] [Std.OrientedCmp cmp₂],
  Std.OrientedCmp (compareLex cmp₁ cmp₂)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtension_of_iso : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {F' F'' : CategoryTheory.Functor D H} (e : F' ≅ F'') {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F) (α' : L.comp F'' ⟶ F),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft e.hom) α' = α →
    ∀ [F'.IsRightKanExtension α], F''.IsRightKanExtension α'
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.instPartialOrder : {α : Type u_1} → [inst : HeytingAlgebra α] → PartialOrder (Heyting.Regular α)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The type (I) simplices of `h : A.PairingCore`, as a family indexed by `h.ι`.  -/
SSet.Subcomplex.PairingCore.type₁ : {X : SSet} → {A : X.Subcomplex} → (h : A.PairingCore) → h.ι → A.N
-- Mathlib.Tactic.Push.Attr
/-- Checks if the theorem is suitable for the `pull` tactic. That is,
check if it is of the form `x = f ...` where `x` contains the head `f`,
but `f` is not the head of `x`.
 -/
Mathlib.Tactic.Push.isPullThm : Lean.Name → Bool → Lean.MetaM (Option Mathlib.Tactic.Push.Head)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
Differentiable.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F), Differentiable 𝕜 f = ∀ (x : E), DifferentiableAt 𝕜 f x
-- Mathlib.SetTheory.ZFC.Class
Class.coe_union : ∀ (x y : ZFSet.{u}), ↑(x ∪ y) = ↑x ∪ ↑y
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitUnopIsoUnopColimit_inv_comp_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUnopIsoUnopColimit F).inv
      (CategoryTheory.Limits.limit.π F.unop j) =
    (CategoryTheory.Limits.colimit.ι F (Opposite.op j)).unop
-- Init.Data.Ord.Basic
Ordering.isLT_eq_beq_lt : ∀ {o : Ordering}, o.isLT = (o == Ordering.lt)
-- Mathlib.CategoryTheory.Types.Basic
/-- Composition of `Fun`s.  -/
TypeCat.Fun.comp : {X : Type u_1} → {Y : Type u_2} → {Z : Type u_3} → TypeCat.Fun Y Z → TypeCat.Fun X Y → TypeCat.Fun X Z
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.localize.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S} (H : φ.IsArithFrobAt Q) [inst_3 : Q.IsPrime],
  H.localize = { toRingHom := Localization.localRingHom Q Q ↑φ ⋯, commutes' := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.NormPow
enorm_fderiv_norm_rpow_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {F : Type u_2}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {f : F → E},
  Differentiable ℝ f →
    ∀ {x : F} {p : NNReal}, 1 < p → ‖fderiv ℝ (fun x => ‖f x‖ ^ ↑p) x‖ₑ ≤ ↑p * ‖f x‖ₑ ^ (↑p - 1) * ‖fderiv ℝ f x‖ₑ
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.instMulActionElemFinset.eq_1 : ∀ (G : Type u_1) [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  Set.powersetCard.instMulActionElemFinset G =
    { smul := Set.powersetCard.instMulActionElemFinset._aux_1 G, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
/-- If a function `f` vanishes outside of a finite set `s`, then it `HasSum`
`∑ b ∈ s, f b`.  -/
hasSum_sum_of_ne_finset_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  {f : β → α} {s : Finset β}, (∀ b ∉ s, f b = 0) → ∀ [L.LeAtTop], HasSum f (∑ b ∈ s, f b) L
-- Init.Data.Range.Basic
Std.Legacy.Range.mk.sizeOf_spec : ∀ (start stop step : ℕ) (step_pos : 0 < step),
  sizeOf [start:stop:step] = 1 + sizeOf start + sizeOf stop + sizeOf step + sizeOf step_pos
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_inj' : ∀ {m n : ℕ}, 1 < n ∨ 1 < m → (n.factorial = m.factorial ↔ n = m)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.tendsto_approxOn_L1_enorm : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  [inst_3 : OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s)
  [inst_4 : TopologicalSpace.SeparableSpace ↑s] {μ : MeasureTheory.Measure β},
  (∀ᵐ (x : β) ∂μ, f x ∈ closure s) →
    MeasureTheory.HasFiniteIntegral (fun x => f x - y₀) μ →
      Filter.Tendsto (fun n => ∫⁻ (x : β), ‖(MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x - f x‖ₑ ∂μ)
        Filter.atTop (nhds 0)
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
SimpleGraph.deleteEdges_eq_inter_edgeSet : ∀ {V : Type u_1} {G : SimpleGraph V} (s : Set (Sym2 V)), G.deleteEdges s = G.deleteEdges (s ∩ G.edgeSet)
-- Mathlib.Analysis.SpecificLimits.Basic
tendsto_factorial_div_pow_self_atTop : Filter.Tendsto (fun n => ↑n.factorial / ↑n ^ n) Filter.atTop (nhds 0)
-- Lean.Util.ShareCommon
Lean.ShareCommon.ShareCommonT.withShareCommon : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → α → Lean.ShareCommon.ShareCommonT m α
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.descFunLift.eq_5 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (s : CategoryTheory.Limits.Cocone F) (x_1 y : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.descFunLift F s (x_1.add y) =
    RingCat.Colimits.descFunLift F s x_1 + RingCat.Colimits.descFunLift F s y
-- Mathlib.CategoryTheory.Preadditive.SingleObj
CategoryTheory.instPreadditiveSingleObj : {α : Type u_1} → [inst : Ring α] → CategoryTheory.Preadditive (CategoryTheory.SingleObj α)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1))),
  s.ExcenterExists signs = (∑ i, s.excenterWeightsUnnorm signs i ≠ 0)
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.neg_apply : ∀ {R₁ : Type u_4} {M₁ : Type u_5} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  (B₁ : LinearMap.BilinForm R₁ M₁) (x y : M₁), ((-B₁) x) y = -(B₁ x) y
-- Mathlib.Data.ZMod.Basic
ZMod.val_intCast : ∀ {n : ℕ} (a : ℤ) [NeZero n], ↑(↑a).val = a % ↑n
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.productMap_range : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : CommSemiring S] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R S]
  (f : A →ₐ[R] S) (g : B →ₐ[R] S), (Algebra.TensorProduct.productMap f g).range = f.range ⊔ g.range
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.map_surjective : ∀ {S : Type u_2} {T : Type u_3} [inst : Semiring S] [inst_1 : Semiring T] (f : S →+* T),
  Function.Surjective ⇑f → Function.Surjective ⇑(PowerSeries.map f)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff_nsmul : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] {x : HahnSeries Γ R} {n : ℕ},
  (n • x).coeff = n • x.coeff
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.ofRingCon.injEq : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (ringCon ringCon_1 : RingCon R),
  ({ ringCon := ringCon } = { ringCon := ringCon_1 }) = (ringCon = ringCon_1)
-- Mathlib.Order.Category.PartOrdEmb
_private.Mathlib.Order.Category.PartOrdEmb.0.PartOrdEmb.Hom.mk : {X Y : PartOrdEmb} → ↑X ↪o ↑Y → X.Hom Y