mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.CommaMorphism.mk.sizeOf_spec : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L R} [inst_3 : SizeOf A] [inst_4 : SizeOf B]
  [inst_5 : SizeOf T] (left : X.left ⟶ Y.left) (right : X.right ⟶ Y.right)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L.map left) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R.map right))
      CategoryTheory.CommaMorphism.w._autoParam),
  sizeOf { left := left, right := right, w := w } = 1 + sizeOf left + sizeOf right + sizeOf w
-- Mathlib.Algebra.Order.Kleene
kstar_le_of_mul_le_right : ∀ {α : Type u_1} [inst : KleeneAlgebra α] {a b : α}, 1 ≤ b → a * b ≤ b → KStar.kstar a ≤ b
-- Mathlib.Topology.Order.Lattice
ContinuousOn.finset_inf'_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {t : Set X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => s.inf' hne fun x => f x a) t
-- Mathlib.Logic.Denumerable
Nat.Subtype.ofNat.eq_def : ∀ (s : Set ℕ) [inst : DecidablePred fun x => x ∈ s] [inst_1 : Infinite ↑s] (x : ℕ),
  Nat.Subtype.ofNat s x =
    match x with
    | 0 => ⊥
    | n.succ => Nat.Subtype.succ (Nat.Subtype.ofNat s n)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerRight_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G H : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) (a : B),
  (CategoryTheory.Oplax.OplaxTrans.whiskerRight Γ ι).as.app a =
    CategoryTheory.Bicategory.whiskerRight (Γ.as.app a) (ι.app a)
-- Std.Sync.CancellationContext
Std.CancellationContext.State : Type
-- Mathlib.Analysis.Convex.Basic
Set.OrdConnected.convex_of_chain : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] {s : Set E},
  s.OrdConnected → IsChain (fun x1 x2 => x1 ≤ x2) s → Convex 𝕜 s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insert_eq_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {p : α × β}, insert p m = m.insert p.1 p.2
-- Mathlib.FieldTheory.Separable
Polynomial.separable_X_sub_C : ∀ {R : Type u} [inst : CommRing R] {x : R}, (Polynomial.X - Polynomial.C x).Separable
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.modify₀ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  {h : 0 < m.buckets.size} {a : α} {f : β a → β a}, m.WF → (↑(Std.DHashMap.Internal.Raw₀.modify ⟨m, h⟩ a f)).WF
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The completed L-function of a function `Φ : ZMod N → ℂ`.

This is only mathematically meaningful if `Φ` is either even, or odd; here we extend this to all `Φ`
by linearity.
 -/
ZMod.completedLFunction : {N : ℕ} → [NeZero N] → (ZMod N → ℂ) → ℂ → ℂ
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Given a point in an affine subspace, a vector is in its direction if and only if it results from
subtracting that point on the right.  -/
AffineSubspace.mem_direction_iff_eq_vsub_right : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ∀ (v : V), v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p₂ -ᵥ p
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.mapIso_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (e : A ≅ B),
  (CategoryTheory.MonoOver.mapIso e).functor = CategoryTheory.MonoOver.map e.hom
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- Pointwise unions of upper hemicontinuous maps are upper hemicontinuous.  -/
UpperHemicontinuousOn.union : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → Set β} {s : Set α},
  UpperHemicontinuousOn f s → UpperHemicontinuousOn g s → UpperHemicontinuousOn (fun x => f x ∪ g x) s
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.mul_subset : ∀ {G : Type u_2} [inst : Group G] {s t : Set G} {H : Subgroup G}, s ⊆ ↑H → t ⊆ ↑H → s * t ⊆ ↑H
-- Init.Data.String.Pattern.Char
String.Slice.Pattern.Char.instToForwardSearcherCharDefaultForwardSearcherForallBoolBeq : {c : Char} →
  String.Slice.Pattern.ToForwardSearcher c
    (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher fun x => x == c)
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- The forgetful functor from schemes étale over `X` to schemes over `X`.  -/
AlgebraicGeometry.Scheme.Etale.forget : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Functor X.Etale (CategoryTheory.Over X)
-- Batteries.Util.Cache
/-- A type synonym for a `DeclCache` containing a pair of discrimination trees.
The first will store declarations in the current file,
the second will store declarations from imports (and will hopefully be "read-only" after creation).
 -/
Batteries.Tactic.DiscrTreeCache : Type → Type
-- Init.Data.Int.Order
Int.natAbs_eq_zero : ∀ {a : ℤ}, a.natAbs = 0 ↔ a = 0
-- Lean.Elab.Binders
Lean.Elab.Term.LetConfig.setFrom : Lean.Elab.Term.LetConfig → Lean.Syntax → Bool → Lean.Elab.Term.LetConfig
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.mem_iff : ∀ {α : Type u_1} {n : ℕ} {s : Finset α}, s ∈ Set.powersetCard α n ↔ s.card = n
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.ringHom_ext_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {I : Ideal R} [inst_2 : I.IsPrime]
  {f g : I.ResidueField →+* S}, f = g ↔ f.comp (algebraMap R I.ResidueField) = g.comp (algebraMap R I.ResidueField)
-- Mathlib.Logic.Equiv.Defs
Equiv.min_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : Min β] (a b : α), a ⊓ b = e.symm (e a ⊓ e b)
-- Mathlib.Algebra.Polynomial.Div
Irreducible.not_isRoot_of_natDegree_ne_one : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} [IsDomain R],
  Irreducible p → p.natDegree ≠ 1 → ∀ {x : R}, ¬p.IsRoot x
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The `i`-th component of an isomorphism of chain complexes.  -/
HomologicalComplex.Hom.isoApp : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → {C₁ C₂ : HomologicalComplex V c} → (C₁ ≅ C₂) → (i : ι) → C₁.X i ≅ C₂.X i
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.smul_mem_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Subring R} {x : R}, a • x ∈ a • S ↔ x ∈ S
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.T_pow_mul_apply_one : ∀ (n : ℤ) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), ↑(ModularGroup.T ^ n * g) 1 = ↑g 1
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.cliqueNum_le_chromaticNumber : ∀ {V : Type u} {G : SimpleGraph V}, ↑G.cliqueNum ≤ G.chromaticNumber
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.isoMkFunctor_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor (CategoryTheory.Join C D) E)
  (x : CategoryTheory.Join C D),
  (CategoryTheory.Join.isoMkFunctor F).inv.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.Join.left x))
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.Join.right x))
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- A Gaussian measure is a probability measure.  -/
ProbabilityTheory.IsGaussian.toIsProbabilityMeasure : ∀ {E : Type u_1} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] {mE : MeasurableSpace E}
  (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ], MeasureTheory.IsProbabilityMeasure μ
-- Mathlib.Topology.Connected.LocallyConnected
/-- A product of spaces is locally connected iff it is empty, or every factor is locally
connected and all but finitely many factors are preconnected.  -/
Pi.locallyConnectedSpace_iff : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)],
  LocallyConnectedSpace ((i : ι) → X i) ↔
    IsEmpty ((i : ι) → X i) ∨ (∀ (i : ι), LocallyConnectedSpace (X i)) ∧ {i | ¬PreconnectedSpace (X i)}.Finite
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isLongestMatch_iff_isLongestMatch_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch p pos ↔
    String.Slice.Pattern.Model.IsLongestMatch (fun x => decide (p x)) pos
-- Mathlib.Analysis.Complex.Basic
Complex.neg_ofReal_mem_slitPlane : ∀ {x : ℝ}, -↑x ∈ Complex.slitPlane ↔ x < 0
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.ins.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode.Path α) →
      (x_1 : RBTree.RBNode α) →
        ((t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t) →
          ((parent : RBTree.RBNode.Path α) →
              (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a) →
            ((a : RBTree.RBNode α) →
                (y : α) →
                  (parent : RBTree.RBNode.Path α) →
                    (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b) →
              ((parent : RBTree.RBNode.Path α) →
                  (y : α) →
                    (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a) →
                ((a : RBTree.RBNode α) →
                    (y : α) →
                      (parent : RBTree.RBNode.Path α) →
                        (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b) →
                  motive x x_1
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions
/-- Bicoloring of a path graph  -/
SimpleGraph.pathGraph.bicoloring : (n : ℕ) → (SimpleGraph.pathGraph n).Coloring Bool
-- Lean.Elab.InfoTree.Types
Lean.Elab.MonadInfoTree.modifyInfoState : {m : Type → Type} → [self : Lean.Elab.MonadInfoTree m] → (Lean.Elab.InfoState → Lean.Elab.InfoState) → m Unit
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.mem_canonicalEquiv_apply : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (P' : Type u_3) [inst_3 : CommRing P'] [inst_4 : Algebra R P'] [inst_5 : IsLocalization S P]
  [inst_6 : IsLocalization S P'] {I : FractionalIdeal S P} {x : P'},
  x ∈ (FractionalIdeal.canonicalEquiv S P P') I ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {a : α}
  {h' : (Std.DHashMap.Raw.Const.get? m a).isSome = true},
  (Std.DHashMap.Raw.Const.get? m a).get h' = Std.DHashMap.Raw.Const.get m a ⋯
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : β → β}, m.WF → (m.modify k f).size = m.size
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.eval₂_T_n : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] (f : R →+* S) (x : Sˣ) (n : ℕ),
  (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.T ↑n) = ↑x ^ n
-- Mathlib.GroupTheory.Sylow
Sylow.instPartialOrder : {p : ℕ} → {G : Type u_1} → [inst : Group G] → PartialOrder (Sylow p G)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_rco : ∀ {m n i fallback : ℕ}, (m...n).toArray.getD i fallback = if i < n - m then m + i else fallback
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.tail.eq_1 : ∀ {α : Type u} (s : Stream'.WSeq α),
  s.tail = Stream'.WSeq.flatten ((fun o => Option.recOn o Stream'.WSeq.nil Prod.snd) <$> s.destruct)
-- Lean.LocalContext
/-- Gets the declaration for expression `e` in the local context.
If `e` is not a free variable or not present then panics.  -/
Lean.LocalContext.getFVar! : Lean.LocalContext → Lean.Expr → Lean.LocalDecl
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Preimage of a non-unital subalgebra under an algebra homomorphism.  -/
NonUnitalSubalgebra.comap : {F : Type v'} →
  {R : Type u} →
    {A : Type v} →
      {B : Type w} →
        [inst : CommSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring A] →
            [inst_2 : NonUnitalNonAssocSemiring B] →
              [inst_3 : Module R A] →
                [inst_4 : Module R B] →
                  [inst_5 : FunLike F A B] →
                    [NonUnitalAlgHomClass F R A B] → F → NonUnitalSubalgebra R B → NonUnitalSubalgebra R A
-- Mathlib.Data.FunLike.Embedding
/-- The coercion to functions must produce injective functions.  -/
EmbeddingLike.injective' : ∀ {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (Sort u_3)} {inst : FunLike F α β} [self : EmbeddingLike F α β]
  (f : F), Function.Injective ⇑f
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVecEntry.vec : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] →
      [inst_2 : DecidableEq α] → {w : ℕ} → (self : Std.Sat.AIG.RefVecEntry α w) → self.aig.RefVec w
-- Mathlib.RingTheory.Trace.Basic
/-- Let $L/K$ be a finite extension of fields. If $L/K$ is separable,
then `traceForm` is nondegenerate.  -/
traceForm_nondegenerate : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L]
  [Algebra.IsSeparable K L], (Algebra.traceForm K L).Nondegenerate
-- Mathlib.CategoryTheory.Shift.Basic
/-- When shifts are indexed by an additive commutative monoid, then shifts commute.  -/
CategoryTheory.shiftComm : {C : Type u} →
  {A : Type u_1} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          (X : C) →
            (i j : A) →
              (CategoryTheory.shiftFunctor C j).obj ((CategoryTheory.shiftFunctor C i).obj X) ≅
                (CategoryTheory.shiftFunctor C i).obj ((CategoryTheory.shiftFunctor C j).obj X)
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.coe_of : ∀ (X : Type u) [inst : TopologicalSpace X], ↑(TopCat.of X) = X
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasProd_strict_mono : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {f g : ι → α} {a₁ a₂ : α},
  HasProd f a₁ → HasProd g a₂ → f < g → a₁ < a₂
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- The coefficients `ℕ →₀ M` of an element of the additive monoid algebra `M[X]`.  -/
PolynomialModule.coeff : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → PolynomialModule R M → ℕ →₀ M
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- A monomorphism `i : Δ' ⟶ Δ` induces a morphism `K.X Δ.len ⟶ K.X Δ'.len` which
is the identity if `Δ = Δ'`, the differential on the complex `K` if `i = δ 0`, and
zero otherwise.  -/
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (K : ChainComplex C ℕ) →
        {Δ' Δ : SimplexCategory} → (i : Δ' ⟶ Δ) → [CategoryTheory.Mono i] → K.X Δ.len ⟶ K.X Δ'.len
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_srem : ∀ (a b : BitVec 8), Int8.ofBitVec (a.srem b) = Int8.ofBitVec a % Int8.ofBitVec b
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsPlot.dSmooth : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  Diffeology.IsPlot p → Diffeology.DSmooth p
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.one_apply_eq_zero_iff : ∀ {M₀ : Type u_7} {N₀ : Type u_8} [inst : MulZeroOneClass M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : DecidablePred fun x => x = 0] [inst_3 : Nontrivial M₀] [inst_4 : NoZeroDivisors M₀] [Nontrivial N₀]
  {x : M₀}, 1 x = 0 ↔ x = 0
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- `p` is a Taylor series of `f` up to `n+1` if and only if `p.shift` is a Taylor series up to `n`
for `p 1`, which is a derivative of `f`. Version for `n : ℕ`.  -/
hasFTaylorSeriesUpToOn_succ_nat_iff_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {n : ℕ},
  HasFTaylorSeriesUpToOn (↑(n + 1)) f p s ↔
    (∀ x ∈ s, (p x 0).curry0 = f x) ∧
      (∀ x ∈ s, HasFDerivWithinAt (fun y => p y 0) (p x 1).curryLeft s x) ∧
        HasFTaylorSeriesUpToOn (↑n) (fun x => (continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) (fun x => (p x).shift) s
-- Mathlib.RingTheory.Localization.FractionRing
/-- The image of `IsFractionRing.lift` is the subfield generated by the image
of the ring hom.  -/
IsFractionRing.lift_fieldRange : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g),
  (IsFractionRing.lift hg).fieldRange = Subfield.closure ↑g.range
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stmts₁.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stmts₁ (Turing.TM2.Stmt.push k a q) = insert (Turing.TM2.Stmt.push k a q) (Turing.TM2.stmts₁ q)
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.const_pow : ∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
  [inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {g : α → γ},
  AEMeasurable g μ → ∀ (c : β), AEMeasurable (fun x => c ^ g x) μ
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.eq_top_iff : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] (I : HomogeneousIdeal 𝒜),
  I = ⊤ ↔ I.toIdeal = ⊤
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.leftUnitor_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.Mon C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.X).hom
-- Mathlib.MeasureTheory.Integral.SetToL1
/-- Auxiliary lemma for `setToFun_congr_measure`: the function sending `f : α →₁[μ] G` to
`f : α →₁[μ'] G` is continuous when `μ' ≤ c' • μ` for `c' ≠ ∞`.  -/
MeasureTheory.continuous_L1_toL1 : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] {m : MeasurableSpace α} {μ μ' : MeasureTheory.Measure α}
  (c' : ENNReal) (hc' : c' ≠ ⊤) (hμ'_le : μ' ≤ c' • μ), Continuous fun f => MeasureTheory.Integrable.toL1 ↑↑f ⋯
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.connectedComponentsLift_apply_coe : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TotallyDisconnectedSpace β] {f : α → β} (h : Continuous f) (x : α),
  h.connectedComponentsLift (ConnectedComponents.mk x) = f x
-- Mathlib.Order.Category.Preord
Preord.coe_comp : ∀ {X Y Z : Preord} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_le_arctan_iff : ∀ {x y : ℝ}, Real.arctan x ≤ Real.arctan y ↔ x ≤ y
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_diff_of_contains_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF → (↑m₂).WF → ∀ {k : α}, m₂.contains k = true → Std.DHashMap.Internal.Raw₀.Const.get! (m₁.diff m₂) k = default
-- Mathlib.Analysis.Calculus.ContDiff.Defs
Filter.EventuallyEq.congr_contDiffWithinAt_of_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → (ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x)
-- Mathlib.Tactic.Translate.ToDual
/-- Maps names to their dual counterparts.  -/
Mathlib.Tactic.ToDual.translations : Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_top_const_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_7} [inst : TopologicalSpace ε']
  [inst_1 : ContinuousENorm ε'] {c : ε'}, ‖c‖ₑ ≠ ⊤ → MeasureTheory.MemLp (fun x => c) ⊤ μ
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms a list of keys into a tree map.  -/
Std.DTreeMap.Raw.Const.unitOfList : {α : Type u} →
  List α →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw.Const.unitOfList._auto_1) →
      Std.DTreeMap.Raw α (fun x => Unit) cmp
-- Mathlib.Data.Int.NatPrime
Int.Prime.dvd_natAbs_of_coe_dvd_sq : ∀ {p : ℕ}, Nat.Prime p → ∀ (k : ℤ), ↑p ∣ k ^ 2 → p ∣ k.natAbs
-- Mathlib.NumberTheory.Padics.ValuativeRel
Padic.instIsRankLeOne : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ValuativeRel.IsRankLeOne ℚ_[p]
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.rightInvSeq.eq_1 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W), cs.rightInvSeq [] = []
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
/-- `toAut` is injective, if only the identity acts trivially on every fiber.  -/
CategoryTheory.PreGaloisCategory.toAut_injective_of_non_trivial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1)
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj]
  [inst_3 : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G],
  (∀ (g : G), (∀ (X : C) (x : (F.obj X).obj), g • x = x) → g = 1) →
    Function.Injective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.tsum_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  [CompleteSpace α] [T0Space α] {f : β → γ → α},
  Summable (Function.uncurry f) → ∑' (c : γ) (b : β), f b c = ∑' (b : β) (c : γ), f b c
-- Init.Data.BEq
equivBEq_of_iff_apply_eq : ∀ {α : Type u_1} {β : Sort u_2} [inst : BEq α] (f : α → β), (∀ (a b : α), (a == b) = true ↔ f a = f b) → EquivBEq α
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.symm_addMonoidHomCongrRight : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N₁]
  [inst_2 : AddCommMonoid N₂] (e : N₁ ≃+ N₂), e.addMonoidHomCongrRight.symm = e.symm.addMonoidHomCongrRight