mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Core
/-- The disjoint union of types `α` and `β`, ordinarily written `α ⊕ β`.

An element of `α ⊕ β` is either an `a : α` wrapped in `Sum.inl` or a `b : β` wrapped in `Sum.inr`.
`α ⊕ β` is not equivalent to the set-theoretic union of `α` and `β` because its values include an
indication of which of the two types was chosen. The union of a singleton set with itself contains
one element, while `Unit ⊕ Unit` contains distinct values `inl ()` and `inr ()`.
 -/
Sum : Type u → Type v → Type (max u v)
-- Mathlib.Data.Finset.Prod
Finset.disjoint_product : ∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t t' : Finset β},
  Disjoint (s ×ˢ t) (s' ×ˢ t') ↔ Disjoint s s' ∨ Disjoint t t'
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedAuthority.default : Std.Http.URI.Authority
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
/-- The forwards edge of `coherentIso`.  -/
SSet.coherentIso.hom : SSet.Edge SSet.coherentIso.x₀ SSet.coherentIso.x₁
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_empty : ∀ {V : Type u}, SimpleGraph.fromEdgeSet ∅ = ⊥
-- Mathlib.Order.SymmDiff
symmDiff_hnot_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), symmDiff a (￢a) = ⊤
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_succ_right_eq_append_map : ∀ {m n : ℕ}, m ≤ n → (m<...=n + 1).toArray = #[m + 1] ++ Array.map (fun x => x + 1) (m<...=n).toArray
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_inter!_le_size_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → (m₁.inter! m₂).size ≤ m₂.size
-- Mathlib.LinearAlgebra.Projectivization.Collinear
Projectivization.IsCollinear_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (S : Set (Projectivization K V)),
  Projectivization.IsCollinear S ↔
    ∃ M,
      Module.Finite K ↥(Projectivization.Subspace.submodule M) ∧
        Module.finrank K ↥(Projectivization.Subspace.submodule M) ≤ 2 ∧ S ⊆ ↑M
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_diff!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} [inst_1 : Inhabited (β k)],
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff! m₂).get! k = default
-- Init.PropLemmas
if_false_right : ∀ {p q : Prop} [h : Decidable p], (if p then q else False) ↔ p ∧ q
-- Mathlib.Data.List.MinMax
/-- The maximum value in a non-empty `List`.  -/
List.maximum_of_length_pos : {α : Type u_1} → [LinearOrder α] → {l : List α} → 0 < l.length → α
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- If `s` is a dense set in a magma `M`, `Subsemigroup.closure s = ⊤`, then in order to prove that
some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x ∈ s`,
and verify that `p x` and `p y` imply `p (x * y)`.  -/
Subsemigroup.dense_induction : ∀ {M : Type u_1} [inst : Mul M] {p : M → Prop} (s : Set M),
  Subsemigroup.closure s = ⊤ → (∀ x ∈ s, p x) → (∀ (x y : M), p x → p y → p (x * y)) → ∀ (x : M), p x
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- The right regular action of a group on itself is transitive.  -/
MulAction.Regular.isPretransitive_mulOpposite : ∀ {G : Type u_2} [inst : Group G], MulAction.IsPretransitive Gᵐᵒᵖ G
-- Mathlib.Topology.Separation.NotNormal
IsClosed.mk_lt_two_pow_mk_dense : ∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] {s d : Set X},
  IsClosed s → ∀ [DiscreteTopology ↑s], Dense d → Cardinal.mk ↑s < 2 ^ Cardinal.mk ↑d
-- Mathlib.SetTheory.ZFC.PSet
PSet.empty_subset : ∀ (x : PSet.{u}), ∅ ⊆ x
-- Mathlib.Topology.Instances.Discrete
/-- **Alias** of `LinearOrder.bot_topologicalSpace_eq_preorderTopology`. -/
LinearOrder.bot_topologicalSpace_eq_generateFrom : ∀ {α : Type u_2} [inst : LinearOrder α] [PredOrder α] [SuccOrder α], ⊥ = Preorder.topology α
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_insert_self : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α}, (m.insert k).contains k = true
-- Mathlib.RingTheory.WittVector.InitTail
WittVector.init_pow : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (m : ℕ) (x : WittVector p R) (n : ℕ),
  WittVector.init n (x ^ m) = WittVector.init n (WittVector.init n x ^ m)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingularLift_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [Nontrivial R], W'.NonsingularLift ⟦![1, 1, 0]⟧
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.op_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.op.h₂ = h.h₁.op
-- Mathlib.Algebra.Polynomial.Derivation
/-- A form of the chain rule: if `f` is a polynomial over `R`
and `d : A → M` is an `R`-derivation then for all `a : A` we have
$$ d(f(a)) = f' (a) d a. $$
The equation is in `M`. For the same equation in `Module.AEval R M a`,
see `Derivation.compAEval_eq`.
 -/
Derivation.comp_aeval_eq : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M] [IsScalarTower R A M] (a : A)
  (d : Derivation R A M) (f : Polynomial R),
  d ((Polynomial.aeval a) f) = (Polynomial.aeval a) (Polynomial.derivative f) • d a
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.instZero : {α : Type u_2} →
  {β : Type u_3} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → Zero (α →ₙ+* β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getKeyD k fallback = fallback
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.isHomogeneous_homogeneousComponent : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (f : MvPowerSeries σ R) (p : ℕ),
  ((MvPowerSeries.homogeneousComponent p) f).IsHomogeneous p
-- Init.Data.Vector.Lemmas
Vector.instDecidableForallForallMemOfDecidablePred : {α : Type u_1} → {n : ℕ} → {xs : Vector α n} → {p : α → Prop} → [DecidablePred p] → Decidable (∀ x ∈ xs, p x)
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Injective
CategoryTheory.Injective.injective_iff_preservesEpimorphisms_preadditiveYoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (J : C),
  CategoryTheory.Injective J ↔ (CategoryTheory.preadditiveYoneda.obj J).PreservesEpimorphisms
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_eq_back?_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp], t.WF → t.max? = t.toArray.back?
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.eq_bot_iff_verts_eq_empty : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph), G' = ⊥ ↔ G'.verts = ∅
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.instIsLocalizationCompFibrantObjectιFibrantObjectWeakEquivalences : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{u_2, u_1} D] (L : CategoryTheory.Functor (HomotopicalAlgebra.FibrantObject C) D)
  [L.IsLocalization (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.FibrantObject C))],
  (HomotopicalAlgebra.BifibrantObject.ιFibrantObject.comp L).IsLocalization
    (HomotopicalAlgebra.weakEquivalences (HomotopicalAlgebra.BifibrantObject C))
-- Mathlib.Data.Num.ZNum
ZNum.cmp_to_int : ∀ (m n : ZNum), Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (discr discr_1 : aig.Ref),
  discr = discr_1 →
    ∀ (lhs lhs_1 : aig.RefVec w),
      lhs = lhs_1 →
        ∀ (rhs rhs_1 : aig.RefVec w),
          rhs = rhs_1 →
            ∀ (s s_1 : aig.RefVec curr),
              s = s_1 →
                Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s =
                  Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr_1 lhs_1 rhs_1 s_1
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_prod_right : ∀ {𝕜 : 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'] {x₀ : M} {y₀ : M'},
  (mfderiv% fun y => (x₀, y)) y₀ = ContinuousLinearMap.inr 𝕜 (TangentSpace I x₀) (TangentSpace I' y₀)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.vle_iff_le : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] {x y : R}, x ≤ᵥ y ↔ v x ≤ v y
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_lt_iff_lt_rpow_of_base_lt_one : ∀ {b x y : ℝ}, 0 < b → b < 1 → 0 < x → (Real.logb b x < y ↔ b ^ y < x)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.asymm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [Std.Asymm s], Std.Asymm r
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- For a functor `F : C ⥤ D` and an object `d : D`, we obtain a contravariant functor from the
category of structured arrows `d ⟶ F.obj c` to the category of costructured arrows
`F.op.obj c ⟶ (op d)`.
 -/
CategoryTheory.StructuredArrow.toCostructuredArrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (d : D) →
            CategoryTheory.Functor (CategoryTheory.StructuredArrow d F)ᵒᵖ
              (CategoryTheory.CostructuredArrow F.op (Opposite.op d))
-- Mathlib.Tactic.Widget.CongrM
/-- Rpc function for the congrm widget.  -/
CongrMSelectionPanel.rpc : SelectInsertParams → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toRingEquiv_symm : ∀ {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₂), e.toRingEquiv.symm = e.symm.toRingEquiv
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.toSignedMeasure_neg : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
  (-j).toSignedMeasure = -j.toSignedMeasure
-- Mathlib.Topology.Algebra.IsOpenUnits
instIsOpenUnitsOfContinuousInv : ∀ {M : Type u_1} [inst : Group M] [inst_1 : TopologicalSpace M] [ContinuousInv M], IsOpenUnits M
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.IsCoseparator.of_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : C}, CategoryTheory.IsCoseparator G → ∀ (α : C ≌ D), CategoryTheory.IsCoseparator (α.functor.obj G)
-- Init.Data.Vector.Lemmas
Vector.getElem?_map : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {xs : Vector α n} {i : ℕ},
  (Vector.map f xs)[i]? = Option.map f xs[i]?
-- Mathlib.Analysis.Normed.Operator.Basic
/-- **Alias** of the forward direction of `ContinuousLinearMap.opNorm_le_iff_lipschitz`. -/
ContinuousLinearMap.lipschitzWith_of_opNorm_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {f : E →SL[σ₁₂] F}
  {K : NNReal}, ‖f‖ ≤ ↑K → LipschitzWith K ⇑f
-- Mathlib.Order.SupClosed
IsSublattice.mk : ∀ {α : Type u_3} [inst : Lattice α] {s : Set α}, SupClosed s → InfClosed s → IsSublattice s
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_of_right_mem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} (x : P) {y : P}, y ∈ s → s.WSameSide x y
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.up_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : InfSet α] (f : ι → α), { down := ⨅ i, f i } = ⨅ i, { down := f i }
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ₂Sq.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R),
  W.Ψ₂Sq =
    Polynomial.C 4 * Polynomial.X ^ 3 + Polynomial.C W.b₂ * Polynomial.X ^ 2 + Polynomial.C (2 * W.b₄) * Polynomial.X +
      Polynomial.C W.b₆
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.removeNeutrals.match_1.eq_2 : ∀ (motive : List ℕ → Sort u_1) (ys : List ℕ) (h_1 : Unit → motive []) (h_2 : (ys : List ℕ) → motive ys),
  (ys = [] → False) →
    (match ys with
      | [] => h_1 ()
      | ys => h_2 ys) =
      h_2 ys
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidates_nonneg : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {f : GromovHausdorff.ProdSpaceFun✝ X Y}
  {x y : X ⊕ Y}, f ∈ GromovHausdorff.candidates X Y → 0 ≤ f (x, y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.coe_eq_zero_iff : ∀ {x : ℝ}, ↑x = 0 ↔ ∃ n, n • (2 * Real.pi) = x
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.instReprInt : Repr ℤ
-- Mathlib.Topology.ClusterPt
/-- `x` is a cluster point of a set `s` if every neighbourhood of `x` meets `s` on a nonempty
set. See also `mem_closure_iff_clusterPt`.  -/
clusterPt_principal_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X},
  ClusterPt x (Filter.principal s) ↔ ∀ U ∈ nhds x, (U ∩ s).Nonempty
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.proofs : Lean.Option Bool
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.toPoly'.go.match_1.eq_6 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (a : Int.Internal.Linear.Expr) (k : ℤ)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_2 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_3 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b))
  (h_5 : (k : ℤ) → (a : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k a))
  (h_6 : (a : Int.Internal.Linear.Expr) → (k : ℤ) → motive (a.mulR k))
  (h_7 : (a : Int.Internal.Linear.Expr) → motive a.neg),
  (match a.mulR k with
    | Int.Internal.Linear.Expr.num k => h_1 k
    | Int.Internal.Linear.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Int.Internal.Linear.Expr.mulL k a => h_5 k a
    | a.mulR k => h_6 a k
    | a.neg => h_7 a) =
    h_6 a k
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.toFlat : ∀ {R : Type u} {M : Type v} {inst : CommRing R} {inst_1 : AddCommGroup M} {inst_2 : Module R M}
  [self : Module.FaithfullyFlat R M], Module.Flat R M
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.eq_of_add : ∀ {α : Type u_1} {a a' b b' : α} [inst : AddGroup α], a = b → a' - b' - (a - b) = 0 → a' = b'
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatClamp n).toUInt64 = UInt64.ofNatLT n ⋯
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- When a function is `C^n` in a set `s` of unique differentiability, it admits
`ftaylorSeriesWithin 𝕜 f s` as a Taylor series up to order `n` in `s`.  -/
ContDiffOn.ftaylorSeriesWithin : ∀ {𝕜 : 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} {n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f s → UniqueDiffOn 𝕜 s → HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
-- Mathlib.RingTheory.Derivation.ToSquareZero
liftOfDerivationToSquareZero_mk_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (I : Ideal B) [inst_5 : Algebra A B] (hI : I ^ 2 = ⊥)
  [inst_6 : IsScalarTower R A B] (d : Derivation R A ↥I) (x : A),
  (Ideal.Quotient.mk I) ((liftOfDerivationToSquareZero I hI d) x) = (algebraMap A (B ⧸ I)) x
-- Init.SimpLemmas
heq_eq_eq : ∀ {α : Sort u_1} (a b : α), (a ≍ b) = (a = b)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.prodComm_apply : ∀ (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 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (a : P₁ × P₂), (AffineEquiv.prodComm k P₁ P₂) a = a.swap
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.Hom.comp_app : ∀ {X : AlgebraicGeometry.Scheme} {M N K : X.Modules} {U : X.Opens} (φ : M ⟶ N) (ψ : N ⟶ K),
  AlgebraicGeometry.Scheme.Modules.Hom.app (CategoryTheory.CategoryStruct.comp φ ψ) U =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.Hom.app φ U)
      (AlgebraicGeometry.Scheme.Modules.Hom.app ψ U)
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValue? k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
          (Std.Internal.List.getValue? k l).bind fun x => f k' x
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.transpose : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : LT α] [inst_1 : Zero R],
  M.BlockTriangular b → M.transpose.BlockTriangular (⇑OrderDual.toDual ∘ b)
-- Aesop.RulePattern.Cache
Aesop.RulePatternCache.map : Aesop.RulePatternCache → Std.HashMap Lean.Expr Aesop.RulePatternCache.Entry
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapComp'.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (h : CategoryTheory.CategoryStruct.comp f g = fg), F.mapComp' f g fg h = F.mapComp' f g fg h
-- Std.Sync.Mutex
Std.instNonemptyMutex : ∀ {α : Type} [Nonempty α], Nonempty (Std.Mutex α)
-- Mathlib.Tactic.Simproc.Factors
Mathlib.Meta.Simproc.FactorsHelper.singleton : ∀ (n : ℕ) {a : ℕ}, a.blt n = true → Mathlib.Meta.NormNum.IsNat n.minFac n → Mathlib.Meta.Simproc.FactorsHelper n a [n]
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.measureReal_le_one : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsZeroOrProbabilityMeasure μ]
  {s : Set α}, μ.real s ≤ 1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rcc : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toList[i]? = if i < (n + 1 - m).toNat then some (m + ↑i) else none
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.card_points_eq_card_lines : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [Configuration.ProjectivePlane P L] [inst : Fintype P]
  [inst_1 : Fintype L], Fintype.card P = Fintype.card L
-- Mathlib.Analysis.BoundedVariation
LocallyBoundedVariationOn.mul : ∀ {α : Type u_2} [inst : LinearOrder α] {f g : α → ℝ} {s : Set α},
  LocallyBoundedVariationOn f s → LocallyBoundedVariationOn g s → LocallyBoundedVariationOn (f * g) s
-- Mathlib.Topology.VectorBundle.Basic
/-- In a vector bundle, a trivialization in the fiber (which is a priori only linear)
is in fact a continuous linear equiv between the fibers and the model fiber.  -/
Bundle.Trivialization.continuousLinearEquivAt : (R : Type u_1) →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)] →
                      [inst_7 : (x : B) → TopologicalSpace (E x)] →
                        [FiberBundle F E] →
                          (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                            [Bundle.Trivialization.IsLinear R e] → (b : B) → b ∈ e.baseSet → E b ≃L[R] F
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_inv_of_lt_inv₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a b : G₀}, 0 < a → a < b⁻¹ → b < a⁻¹
-- Init.Data.Float.Float32
/-- Converts a floating-point number to a 32-bit unsigned integer.

If the given `Float32` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `UInt32`. Returns `0` if the `Float32` is negative or `NaN`, and returns
the largest `UInt32` value (i.e. `UInt32.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float32.Model`.
 -/
Float32.toUInt32 : Float32 → UInt32
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g] (hf : S.f = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).ι = CategoryTheory.Limits.kernel.ι S.g
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
/-- The isomorphism `(extendToSucc hj F τ).obj ⟨Order.succ j, _⟩ ≅ X`.  -/
CategoryTheory.SmallObject.SuccStruct.extendToSuccObjSuccIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] →
          {j : J} →
            (hj : ¬IsMax j) →
              (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                {X : C} →
                  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) →
                    (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).obj ⟨Order.succ j, ⋯⟩ ≅ X
-- Mathlib.Control.Monad.Cont
ExceptT.callCC.eq_1 : ∀ {m : Type u → Type v} [inst : Monad m] {ε : Type u} [inst_1 : MonadCont m] {α β : Type u}
  (f : MonadCont.Label α (ExceptT ε m) β → ExceptT ε m α),
  ExceptT.callCC f = ExceptT.mk (MonadCont.callCC fun x => (f (ExceptT.mkLabel x)).run)
-- Std.Data.Internal.List.Associative
Std.Internal.List.perm_of_beqModel : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : (k : α) → BEq (β k)]
  [∀ (k : α), LawfulBEq (β k)] {l₁ l₂ : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.DistinctKeys l₂ → Std.Internal.List.beqModel l₁ l₂ = true → l₁.Perm l₂
-- Init.Data.Vector.Attach
Vector.pmap.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {P : α → Prop} (f : (a : α) → P a → β) (xs : Vector α n) (H : ∀ a ∈ xs, P a),
  Vector.pmap f xs H = Vector.mk (Array.pmap f xs.toArray ⋯) ⋯