mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.Hom.toPartialMap_compHom : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  (AlgebraicGeometry.Scheme.Hom.toPartialMap f).compHom g =
    AlgebraicGeometry.Scheme.Hom.toPartialMap (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_sumElim : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι → M)
  (g : κ → M), ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instMonadMacroAdapterTermElabM : Lean.Elab.MonadMacroAdapter Lean.Elab.TermElabM
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularEpi.fac : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularEpi f] (k : X ⟶ Z)
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.left f) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.IsRegularEpi.right f) k),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsRegularEpi.desc f k h) = k
-- Init.Data.Nat.Lcm
Nat.lcm_dvd_mul_self_right_iff_dvd_mul : ∀ {k m n : ℕ}, n.lcm k ∣ m * k ↔ n ∣ m * k
-- Mathlib.Data.Finsupp.Defs
Finsupp.support_subset_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] {s : Set α} {f : α →₀ M}, ↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformContinuousOn_iff_le : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {s : Set α},
  UniformContinuousOn f s ↔ ∀ ε > 0, ∃ δ > 0, ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ δ → dist (f x) (f y) ≤ ε
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_of_containsKey_insertListIfNewUnit : ∀ {α : Type u} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α},
  toInsert.contains k = false →
    Std.Internal.List.containsKey k (Std.Internal.List.insertListIfNewUnit l toInsert) = true →
      Std.Internal.List.containsKey k l = true
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.TacticNode.mk : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → Bool → Mathlib.TacticAnalysis.TacticNode
-- Mathlib.Data.Option.Basic
Option.pmap_bind : ∀ {α β γ : Type u_5} {x : Option α} {g : α → Option β} {p : β → Prop} {f : (b : β) → p b → γ}
  (H : ∀ (a : β), x >>= g = some a → p a) (H' : ∀ (a : α), ∀ b ∈ g a, b ∈ x >>= g),
  Option.pmap f (x >>= g) H = do
    let a ← x
    Option.pmap f (g a) ⋯
-- Init.Data.String.Slice
/-- If `pat` matches a prefix of `s`, returns the remainder. Returns `none` otherwise.

Use `String.Slice.dropPrefix` to return the slice
unchanged when `pat` does not match a prefix.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".toSlice.dropPrefix? "red " == some "green blue".toSlice`

* `"red green blue".toSlice.dropPrefix? "reed " == none`

* `"red green blue".toSlice.dropPrefix? 'r' == some "ed green blue".toSlice`

* `"red green blue".toSlice.dropPrefix? Char.isLower == some "ed green blue".toSlice`
 -/
String.Slice.dropPrefix? : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Option String.Slice
-- Mathlib.RingTheory.PicardGroup
/-- Picard group as a functor from the category of commutative semirings to
the category of abelian groups.  -/
CommRing.Pic.functor : CategoryTheory.Functor CommSemiRingCat CommGrpCat
-- Init.Omega.IntList
Lean.Omega.IntList.combo_eq_smul_add_smul : ∀ (a : ℤ) (xs : Lean.Omega.IntList) (b : ℤ) (ys : Lean.Omega.IntList),
  Lean.Omega.IntList.combo a xs b ys = a * xs + b * ys
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Ideal.Quotient.factor_ker : ∀ {R : Type u_1} [inst : Ring R] {I J : Ideal R} (H : I ≤ J) [inst_1 : I.IsTwoSided] [inst_2 : J.IsTwoSided],
  RingHom.ker (Ideal.Quotient.factor H) = Ideal.map (Ideal.Quotient.mk I) J
-- Lean.Environment
Lean.Environment.hasUnsafe : Lean.Environment → Lean.Expr → Bool
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.keyAtIdx? : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ℕ → Option α
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj_self : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} (a : ℕ),
  ProbabilityTheory.Kernel.partialTraj κ a a = ProbabilityTheory.Kernel.id
-- Mathlib.Topology.Closure
Dense.interior_compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Dense s → interior sᶜ = ∅
-- Mathlib.Order.Category.HeytAlg
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
HeytAlg.Hom.Simps.hom : (X Y : HeytAlg) → X.Hom Y → HeytingHom ↑X ↑Y
-- Mathlib.CategoryTheory.Localization.Prod
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prod_fac : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {E : Type u₅} [inst_2 : CategoryTheory.Category.{v₅, u₅} E]
  (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) [inst_3 : W₁.ContainsIdentities]
  [inst_4 : W₂.ContainsIdentities],
  (W₁.Q.prod W₂.Q).comp (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift F hF) = F
-- Init.Grind.Module.Basic
Lean.Grind.AddCommMonoid.toAdd : {M : Type u} → [self : Lean.Grind.AddCommMonoid M] → Add M
-- Mathlib.RingTheory.Unramified.LocalRing
/-- [Stacks Tag 00UW](https://stacks.math.columbia.edu/tag/00UW) ((2)) -/
Algebra.instIsSeparableResidueFieldOfFormallyUnramified : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [inst_4 : IsLocalRing S] [inst_5 : IsLocalHom (algebraMap R S)] [Algebra.EssFiniteType R S]
  [Algebra.FormallyUnramified R S], Algebra.IsSeparable (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.instAdd : Add Lean.Omega.LinearCombo
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, local version for any measure.

Let filters `l` and `l'` be related by `[intervalIntegral.FTCFilter a l l']`; let `μ` be a locally
finite measure.  If `f` has a finite limit `c` at `l' ⊓ ae μ`, then
`∫ x in u..v, f x ∂μ = -μ (Set.Ioc v u) • c + o(μ(Set.Ioc v u))` as both `u` and `v` tend to `l`.

See also `measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge'` for a version that also works,
e.g., for `l = l' = Filter.atTop`.  -/
intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {c : E}
  {l l' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ]
  [CompleteSpace E] [intervalIntegral.FTCFilter a l l'],
  StronglyMeasurableAtFilter f l' μ →
    Filter.Tendsto f (l' ⊓ MeasureTheory.ae μ) (nhds c) →
      Filter.Tendsto u lt l →
        Filter.Tendsto v lt l →
          v ≤ᶠ[lt] u →
            (fun t => ∫ (x : ℝ) in u t..v t, f x ∂μ + μ.real (Set.Ioc (v t) (u t)) • c) =o[lt] fun t =>
              μ.real (Set.Ioc (v t) (u t))
-- Mathlib.Order.InitialSeg
/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≼i s` is an order
embedding whose `Set.range` is a lower set. That is, whenever `b < f a` in `β` then `b` is in the
range of `f`.  -/
InitialSeg.«term_≼i_» : Lean.TrailingParserDescr
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  List.Pairwise (fun a b => (a == b) = false) l → (Std.HashSet.Raw.ofList l).size = l.length
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.exists_fixed_point.match_1.splitter : {α : Type u_3} →
  {β : Type u_1} →
    {γ : Type u_2} →
      (motive : Option (α × γ × β) → Sort u_4) →
        (x : Option (α × γ × β)) →
          (Unit → motive none) → ((a : α) → (c : γ) → (b' : β) → motive (some (a, c, b'))) → motive x
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instAddSubmonoidClass : ∀ {M : Type u_1} [inst : AddZeroClass M], AddSubmonoidClass (AddSubmonoid M) M
-- Mathlib.Order.Filter.IsBounded
Filter.isCobounded_ge_of_top : ∀ {α : Type u_1} [inst : LE α] [OrderTop α] {f : Filter α}, Filter.IsCobounded (fun x1 x2 => x2 ≤ x1) f
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.norm_compContinuousLinearMap_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : F [⋀^ι]→L[𝕜] G) (g : E →L[𝕜] F), ‖f.compContinuousLinearMap g‖ ≤ ‖f‖ * ‖g‖ ^ Fintype.card ι
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- The results of the theorems that successfully applied.  -/
Mathlib.Tactic.ClickSuggestions.SectionState.results : {α : Type} → Mathlib.Tactic.ClickSuggestions.SectionState α → Array (Mathlib.Tactic.ClickSuggestions.Result α)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.IsDecompOn.comp : ∀ {X : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : MulAction G X] {g f : X → X} {B A : Set X} {T S : Finset G},
  Equidecomp.IsDecompOn g B T → Equidecomp.IsDecompOn f A S → Set.MapsTo f A B → Equidecomp.IsDecompOn (g ∘ f) A (T * S)
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_sdiff_add_inter`. -/
MeasureTheory.measureReal_diff_add_inter : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_sdiff_add_inter._auto_1 → μ.real (s \ t) + μ.real (s ∩ t) = μ.real s
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.below : {O : Set (ℕ →. ℕ)} → {motive : (a : ℕ →. ℕ) → Nat.RecursiveIn O a → Prop} → {a : ℕ →. ℕ} → Nat.RecursiveIn O a → Prop
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.smul_add : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMulCommClass R R' M] (r : R') (x y : TensorProduct R M N),
  r • (x + y) = r • x + r • y
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.unit_of_mem_ofUnits_spec_mem : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M} {h : x ∈ S.ofUnits}, S.unit_of_mem_ofUnits h ∈ S
-- Mathlib.Data.Multiset.UnionInter
Multiset.inter_add_sub_of_add_eq_add : ∀ {α : Type u_1} [inst : DecidableEq α] {M N P Q : Multiset α}, M + N = P + Q → N ∩ Q + (P - M) = N
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Icc : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x * a) ⁻¹' Set.Icc b c = Set.Icc (b / a) (c / a)
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolAlg_sdiff : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : AsBoolAlg α), ofBoolAlg (a \ b) = ofBoolAlg a * (1 + ofBoolAlg b)
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.coe_inducedOrderRingIso`. -/
LinearOrderedField.coe_inducedOrderRingIso : ∀ (β : Type u_3) (γ : Type u_4) [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : IsStrictOrderedRing β] [inst_3 : Field γ] [inst_4 : ConditionallyCompleteLinearOrder γ]
  [inst_5 : IsStrictOrderedRing γ],
  ⇑(ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β γ) =
    ConditionallyCompleteLinearOrderedField.inducedMap β γ
-- Mathlib.CategoryTheory.EssentiallySmall
/-- The (noncomputable) categorical equivalence between
an essentially small category and its small model.
 -/
CategoryTheory.equivSmallModel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EssentiallySmall.{w, v, u} C] → C ≌ CategoryTheory.SmallModel.{w, v, u} C
-- Lean.Environment
Lean.Environment.allImportedModuleNames : Lean.Environment → Array Lean.Name
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β}, k ∈ m.alter k f ↔ (f m[k]?).isSome = true
-- Mathlib.Order.SymmDiff
Pi.bihimp_def : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → GeneralizedHeytingAlgebra (π i)] (a b : (i : ι) → π i),
  bihimp a b = fun i => bihimp (a i) (b i)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f.op g.op).unop h
-- Mathlib.RingTheory.DividedPowers.DPMorphism
/-- The composition of two divided power morphisms as a `DPMorphism`.  -/
DividedPowers.DPMorphism.comp : {A : Type u_3} →
  {B : Type u_4} →
    {C : Type u_5} →
      [inst : CommSemiring A] →
        [inst_1 : CommSemiring B] →
          [inst_2 : CommSemiring C] →
            {I : Ideal A} →
              {J : Ideal B} →
                {K : Ideal C} →
                  {hI : DividedPowers I} →
                    {hJ : DividedPowers J} →
                      {hK : DividedPowers K} → hJ.DPMorphism hK → hI.DPMorphism hJ → hI.DPMorphism hK
-- Lean.Expr
/-- Similar to `Lean.Expr.instantiate`, but considers only the substitutions `subst` in the range `[beginIdx, endIdx)`.
Function panics if `beginIdx <= endIdx <= subst.size` does not hold.

This function is equivalent to `instantiate e (subst.extract beginIdx endIdx)`, but it does not allocate a new array.

This instantiates with the "backwards" indexing scheme.
See also `Lean.Expr.instantiateRevRange`, which instantiates with the "forwards" indexing scheme.
 -/
Lean.Expr.instantiateRange : Lean.Expr → ℕ → ℕ → Array Lean.Expr → Lean.Expr
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.HashMap.ofList l).getKeyD k' fallback = k
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_homOfLE_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U V : Y.Opens) (e : U ≤ V) {Z : AlgebraicGeometry.Scheme} (h : ↑V ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f ∣_ U) (CategoryTheory.CategoryStruct.comp (Y.homOfLE e) h) =
    CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) (CategoryTheory.CategoryStruct.comp (f ∣_ V) h)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.ofEquivFun.congr_simp : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (e e_1 : M ≃ₗ[R] ι → R), e = e_1 → Module.Basis.ofEquivFun e = Module.Basis.ofEquivFun e_1
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.quotientKerEquivOfRightInverse_apply : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (f : M →+ P) (g : P → M)
  (hf : Function.RightInverse g ⇑f) (a : (AddCon.ker f).Quotient),
  (AddCon.quotientKerEquivOfRightInverse f g hf) a = (AddCon.kerLift f) a
-- Std.Sync.CancellationContext
/-- A cancellation context that allows multiple consumers to wait until cancellation is requested. Forms
a tree structure where cancelling a parent cancels all children.
 -/
Std.CancellationContext : Type
-- Mathlib.Topology.Compactification.StoneCech
Ultrafilter.topologicalSpace : {α : Type u} → TopologicalSpace (Ultrafilter α)
-- Mathlib.Computability.Language
Language.mem_kstar : ∀ {α : Type u_1} {l : Language α} {x : List α}, x ∈ KStar.kstar l ↔ ∃ L, x = L.flatten ∧ ∀ y ∈ L, y ∈ l
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition with a linear isometry on the left preserves the norm of the iterated
derivative.  -/
LinearIsometry.norm_iteratedFDeriv_comp_left : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : E} {n : WithTop ℕ∞} {f : E → F} (g : F →ₗᵢ[𝕜] G),
  ContDiffAt 𝕜 n f x → ∀ {i : ℕ}, ↑i ≤ n → ‖iteratedFDeriv 𝕜 i (⇑g ∘ f) x‖ = ‖iteratedFDeriv 𝕜 i f x‖
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.splitEpiBiprodComparison_section_ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [inst_6 : F.PreservesZeroMorphisms],
  (F.splitEpiBiprodComparison X Y).section_ = F.biprodComparison' X Y
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.relationOfHasCoeffs.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P P_1 : Algebra.Presentation R S ι σ} (e_P : P = P_1) (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (r r_1 : σ),
  r = r_1 → Algebra.Presentation.relationOfHasCoeffs R₀ r = Algebra.Presentation.relationOfHasCoeffs R₀ r_1
-- Init.Data.UInt.Lemmas
UInt16.toNat_toUSize : ∀ (x : UInt16), x.toUSize.toNat = x.toNat
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
dist_pi_def : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)]
  (f g : (b : β) → X b), dist f g = ↑(Finset.univ.sup fun b => nndist (f b) (g b))
-- Mathlib.Order.RelIso.Basic
RelEmbedding.isWellFounded : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : r ↪r s) [IsWellFounded β s],
  IsWellFounded α r
-- Mathlib.Algebra.GroupWithZero.Commute
Ring.inverse_pow : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] (r : M₀) (n : ℕ), Ring.inverse r ^ n = Ring.inverse (r ^ n)
-- Mathlib.RingTheory.AdicCompletion.Functoriality
AdicCompletion.AdicCauchySequence.map_id : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  AdicCompletion.AdicCauchySequence.map I LinearMap.id = LinearMap.id
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdx?.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.eq_1 : ∀ {α : Type u} (s : Set α), s.Subsingleton = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y
-- Mathlib.Combinatorics.Quiver.Path
/-- The image of a path under a prefunctor.  -/
Prefunctor.mapPath : {V : Type u₁} →
  [inst : Quiver V] →
    {W : Type u₂} → [inst_1 : Quiver W] → (F : V ⥤q W) → {a b : V} → Quiver.Path a b → Quiver.Path (F.obj a) (F.obj b)
-- Mathlib.Probability.Martingale.OptionalSampling
MeasureTheory.Martingale.condExp_stoppedValue_stopping_time_ae_eq_restrict_le : ∀ {Ω : Type u_1} {E : Type u_2} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {ι : Type u_3} [inst_3 : LinearOrder ι] [LocallyFiniteOrder ι]
  [inst_5 : OrderBot ι] [inst_6 : TopologicalSpace ι] [DiscreteTopology ι] [inst_8 : MeasurableSpace ι] [BorelSpace ι]
  [inst_10 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] {ℱ : MeasureTheory.Filtration ι m}
  {τ σ : Ω → WithTop ι} {f : ι → Ω → E} {i : ι},
  MeasureTheory.Martingale f ℱ μ →
    MeasureTheory.IsStoppingTime ℱ τ →
      ∀ (hσ : MeasureTheory.IsStoppingTime ℱ σ) [MeasureTheory.SigmaFinite (μ.trim ⋯)],
        (∀ (x : Ω), τ x ≤ ↑i) →
          μ[MeasureTheory.stoppedValue f τ | hσ.measurableSpace] =ᵐ[μ.restrict {x | τ x ≤ σ x}]
            MeasureTheory.stoppedValue f τ
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableWithinAt.smul : ∀ {𝕜 : 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] {s : Set M} {x : M} {V : Type u_18}
  [inst_6 : NormedAddCommGroup V] [inst_7 : NormedSpace 𝕜 V] {f : M → 𝕜} {g : M → V},
  MDiffAt[s] f x → MDiffAt[s] g x → (MDiffAt[s] fun p => f p • g p) x
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.mkVarCore : {m : Type → Type} →
  [MonadLiftT Lean.Meta.Grind.GoalM m] →
    [Monad m] →
      [Lean.Meta.Grind.Arith.CommRing.MonadRing m] →
        [Lean.Meta.Grind.Arith.CommRing.MonadSetTermId m] → Lean.Expr → m Lean.Grind.CommRing.Var
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_throw_StateT_lift_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {ε : Type u_3} {m : Type u → Type v} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] [inst_4 : MonadExceptOf ε m] {σ α : Type u} {post : α → σ → Pred}
  {epost : EPred} (err : ε),
  Std.Internal.Do.wp (MonadExceptOf.throw err) post epost =
    Std.Internal.Do.wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom_piSingle : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (i : ι) (φ : β i →+ γ),
  DFinsupp.sumAddHom (Pi.single i φ) = φ.comp (DFinsupp.evalAddMonoidHom i)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] (s : Finset α), s - ∅ = ∅
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- The natural inclusion from multivariate polynomials into multivariate formal power series.  -/
MvPolynomial.toMvPowerSeries : {σ : Type u_1} → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → MvPowerSeries σ R
-- Mathlib.RingTheory.HopfAlgebra.Quotient
Ideal.IsHopfIdeal.mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : HopfAlgebraStruct R A] {I : Ideal A}
  [toIsCoideal : (Submodule.restrictScalars R I).IsCoideal],
  (∀ ⦃x : A⦄, x ∈ I → (HopfAlgebraStruct.antipode R) x ∈ I) → Ideal.IsHopfIdeal R I
-- Mathlib.LinearAlgebra.Ray
units_smul_eq_self_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [Module.IsTorsionFree R M] {u : Rˣ} {v : Module.Ray R M},
  u • v = v ↔ 0 < ↑u
-- Mathlib.CategoryTheory.Types.Basic
equivIsoIso_inv : ∀ {X Y : Type u}, equivIsoIso.inv = TypeCat.ofHom fun i => i.toEquiv