mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G],
  (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).IsLeftKanExtension
    (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRic : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Ric α)
-- Init.Data.Iterators.Lemmas.Combinators.ULift
Std.Iter.uLift_eq_toIter_uLift_toIterM : ∀ {α β : Type u} {it : Std.Iter β}, it.uLift = (it.toIterM.uLift Id).toIter
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.isLeftDescent_iff_not_isLeftDescent_mul : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {w : W} {i : B},
  cs.IsLeftDescent w i ↔ ¬cs.IsLeftDescent (cs.simple i * w) i
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerveApp_hom_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (n : SimplexCategoryᵒᵖ) (i : CategoryTheory.ToType (Opposite.unop n)),
  CategoryTheory.CategoryStruct.comp (U.cechIsoCechNerveApp hT n).hom
      (CategoryTheory.Limits.WidePullback.π
        (fun x => (CategoryTheory.Limits.FormalCoproduct.isTerminalIncl T hT).from U) i) =
    U.powerπ i
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inr_comp_tensorHom : ∀ {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} (f₁ : x₁ ⟶ y₁) (f₂ : x₂ ⟶ y₂),
  CategoryTheory.CategoryStruct.comp (x₁.inr x₂) (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) =
    CategoryTheory.CategoryStruct.comp f₂ (y₁.inr y₂)
-- Mathlib.Data.List.Pairwise
List.Pairwise.cons_cons_of_trans : ∀ {α : Type u_1} {R : α → α → Prop} [IsTrans α R] {l : List α} {a b : α},
  R a b → List.Pairwise R (b :: l) → List.Pairwise R (a :: b :: l)
-- Mathlib.Analysis.Normed.Group.Basic
norm_ne_zero_iff : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a : E}, ‖a‖ ≠ 0 ↔ a ≠ 0
-- Mathlib.Analysis.MellinTransform
/-- If `f` is a locally integrable real-valued function which is `O(x ^ (-b))` at `0`, then for any
`b < s`, its Mellin transform converges on some right neighbourhood of `0`.  -/
mellin_convergent_zero_of_isBigO : ∀ {b : ℝ} {f : ℝ → ℝ},
  MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0)) →
    (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) →
      ∀ {s : ℝ},
        b < s → ∃ c, 0 < c ∧ MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioc 0 c) MeasureTheory.volume
-- Mathlib.Data.NNReal.Defs
NNReal.coe_nsmul : ∀ (r : NNReal) (n : ℕ), ↑(n • r) = n • ↑r
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_zero : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B], selfZPow x B 0 = 1
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.ColimitType.instAdd : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → Add (RingCat.Colimits.ColimitType F)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.mk.inj : ∀ {term? : Option Lean.Term} {phase? : Option Aesop.PhaseName} {priority? : Option Aesop.Frontend.Priority}
  {builder? : Option Aesop.Frontend.DBuilderName} {builderOptions : Aesop.RuleBuilderOptions}
  {ruleSets : Aesop.Frontend.RuleSets} {term?_1 : Option Lean.Term} {phase?_1 : Option Aesop.PhaseName}
  {priority?_1 : Option Aesop.Frontend.Priority} {builder?_1 : Option Aesop.Frontend.DBuilderName}
  {builderOptions_1 : Aesop.RuleBuilderOptions} {ruleSets_1 : Aesop.Frontend.RuleSets},
  { term? := term?, phase? := phase?, priority? := priority?, builder? := builder?, builderOptions := builderOptions,
        ruleSets := ruleSets } =
      { term? := term?_1, phase? := phase?_1, priority? := priority?_1, builder? := builder?_1,
        builderOptions := builderOptions_1, ruleSets := ruleSets_1 } →
    term? = term?_1 ∧
      phase? = phase?_1 ∧
        priority? = priority?_1 ∧ builder? = builder?_1 ∧ builderOptions = builderOptions_1 ∧ ruleSets = ruleSets_1
-- Mathlib.Analysis.InnerProductSpace.LinearMap
InnerProductSpace.rankOne_def' : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x : E) (y : F),
  ((InnerProductSpace.rankOne 𝕜) x) y = ContinuousLinearMap.toSpanSingleton 𝕜 x ∘SL (innerSL 𝕜) y
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.mem_piAntidiag : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] {s : Finset ι} {n : μ} {f : ι → μ},
  f ∈ s.piAntidiag n ↔ s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.inv_op_smul_set_distrib₀ : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (s : Set α), (MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
-- Mathlib.Probability.Density
/-- A random variable that `HasPDF` transformed under a `QuasiMeasurePreserving`
map also `HasPDF` if `(map g (map X ℙ)).HaveLebesgueDecomposition μ`.

`quasiMeasurePreserving_hasPDF` is more useful in the case we are working with a
probability measure and a real-valued random variable.  -/
MeasureTheory.pdf.quasiMeasurePreserving_hasPDF : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {F : Type u_3} [inst_1 : MeasurableSpace F] {ν : MeasureTheory.Measure F} (X : Ω → E)
  [MeasureTheory.HasPDF X ℙ μ] {g : E → F},
  MeasureTheory.Measure.QuasiMeasurePreserving g μ ν →
    (MeasureTheory.Measure.map g (MeasureTheory.Measure.map X ℙ)).HaveLebesgueDecomposition ν →
      MeasureTheory.HasPDF (g ∘ X) ℙ ν
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.collectedBasis.eq_1 : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} (h : DirectSum.IsInternal A) {α : ι → Type u_2}
  (v : (i : ι) → Module.Basis (α i) R ↥(A i)),
  h.collectedBasis v =
    {
      repr :=
        ((LinearEquiv.ofBijective (DirectSum.coeLinearMap A) h).symm ≪≫ₗ
            DFinsupp.mapRange.linearEquiv fun i => (v i).repr) ≪≫ₗ
          (sigmaFinsuppLequivDFinsupp R).symm }
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_not : ∀ {a : USize} (h : System.Platform.numBits = 64), (~~~a).toBitVec64 h = ~~~a.toBitVec64 h
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.ExceptT.run_bind.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (x : α) → motive (Except.ok x))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok x => h_1 x
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.Algebra.Lie.SerreConstruction
_private.Mathlib.Algebra.Lie.SerreConstruction.0.CartanMatrix.Relations.termE : Lean.ParserDescr
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.mk.congr_simp : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (toStarSubalgebra toStarSubalgebra_1 : StarSubalgebra ℂ (H →L[ℂ] H))
  (e_toStarSubalgebra : toStarSubalgebra = toStarSubalgebra_1)
  (centralizer_centralizer' : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier),
  { toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer' } =
    { toStarSubalgebra := toStarSubalgebra_1, centralizer_centralizer' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPairHom.comp_id : ∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (f : CategoryTheory.Limits.WalkingParallelPairHom X Y),
  f.comp (CategoryTheory.Limits.WalkingParallelPairHom.id Y) = f
-- Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace
Besicovitch.card_le_multiplicity_of_δ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {s : Finset E},
  (∀ c ∈ s, ‖c‖ ≤ 2) →
    (∀ c ∈ s, ∀ d ∈ s, c ≠ d → 1 - Besicovitch.goodδ E ≤ ‖c - d‖) → s.card ≤ Besicovitch.multiplicity E
-- Mathlib.Algebra.Group.Defs
div_mul_cancel : ∀ {G : Type u_1} [inst : Group G] (a b : G), a / b * b = a
-- Mathlib.RingTheory.Perfection
PreTilt.valAux.eq_1 : ∀ (K : Type u₁) [inst : Field K] (v : Valuation K NNReal) (O : Type u₂) [inst_1 : CommRing O] [inst_2 : Algebra O K]
  (p : ℕ) [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p] (f : PreTilt O p),
  PreTilt.valAux K v O p f =
    if h : ∃ n, (PreTilt.coeff n) f ≠ 0 then ModP.preVal K v O p ((PreTilt.coeff (Nat.find h)) f) ^ p ^ Nat.find h
    else 0
-- Init.Data.BitVec.Bitblast
BitVec.getElem_add : ∀ {w i : ℕ} (i_lt : i < w) (x y : BitVec w), (x + y)[i] = (x[i] ^^ (y[i] ^^ BitVec.carry i x y false))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.norm_expMapBasis : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K),
  NumberField.mixedEmbedding.norm
      (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x)) =
    Real.exp (x NumberField.Units.dirichletUnitTheorem.w₀) ^ Module.finrank ℚ K
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- An alternative version of `contMDiffWithinAt_iff_of_mem_maximalAtlas` which takes a
chart `e'` in the target in the maximal atlas, but uses the preferred chart on the domain.  -/
contMDiffWithinAt_iff_of_mem_maximalAtlas' : ∀ {𝕜 : 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'] {e' : OpenPartialHomeomorph M' H'}
  {f : M → M'} {s : Set M} {x : M} {n : WithTop ℕ∞},
  e' ∈ IsManifold.maximalAtlas I' n M' →
    f x ∈ e'.source →
      (ContMDiffWithinAt I I' n f s x ↔
        ContinuousWithinAt f s x ∧
          ContDiffWithinAt 𝕜 n (↑(e'.extend I') ∘ f ∘ ↑(extChartAt I x).symm)
            (↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I) (↑(extChartAt I x) x))
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
/-- the map `(limᵢ Gᵢ) ⊗ M → limᵢ (Gᵢ ⊗ M)` from the bilinear map `limᵢ Gᵢ → M → limᵢ (Gᵢ ⊗ M)` given
by the family of maps `Gᵢ → M → limᵢ (Gᵢ ⊗ M)` where `gᵢ ↦ m ↦ [gᵢ ⊗ m]`
 -/
TensorProduct.toDirectLimit : {R : Type u_1} →
  [inst : CommSemiring R] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] →
        [inst_2 : Preorder ι] →
          {G : ι → Type u_3} →
            [inst_3 : (i : ι) → AddCommMonoid (G i)] →
              [inst_4 : (i : ι) → Module R (G i)] →
                (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                  (M : Type u_4) →
                    [inst_5 : AddCommMonoid M] →
                      [inst_6 : Module R M] →
                        TensorProduct R (Module.DirectLimit G f) M →ₗ[R]
                          Module.DirectLimit (fun x => TensorProduct R (G x) M) fun i j h =>
                            LinearMap.rTensor M (f i j h)
-- Mathlib.Dynamics.Minimal
AddAction.IsMinimal.mk : ∀ {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α],
  (∀ (x : α), Dense (AddAction.orbit M x)) → AddAction.IsMinimal M α
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.dropPrefix?_prop_eq_dropPrefix?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.dropPrefix? p = s.dropPrefix? fun x => decide (p x)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instSigmaFiniteVolume : MeasureTheory.SigmaFinite MeasureTheory.volume
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.sup_primeHeight_of_maximal_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R], ↑(⨆ I, ⨆ (x : I.IsMaximal), Ideal.primeHeight✝ I) = ringKrullDim R
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.isStrictlyPositive_iff_eq_star_mul_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [StarOrderedRing A] [inst_5 : Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A}, IsStrictlyPositive a ↔ ∃ b, IsUnit b ∧ a = star b * b
-- Mathlib.Analysis.BoxIntegral.Basic
/-- If `f` is integrable on `I`, then `fun J ↦ integral J l f vol` is box-additive on subboxes of
`I`: if `π₁`, `π₂` are two prepartitions of `I` covering the same part of `I`, the sum of integrals
of `f` over the boxes of `π₁` is equal to the sum of integrals of `f` over the boxes of `π₂`.

See also `BoxIntegral.Integrable.sum_integral_congr` for an unbundled version.  -/
BoxIntegral.Integrable.toBoxAdditive : {ι : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ F] →
              {I : BoxIntegral.Box ι} →
                [inst_4 : Fintype ι] →
                  {l : BoxIntegral.IntegrationParams} →
                    {f : (ι → ℝ) → E} →
                      {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} →
                        [CompleteSpace F] → BoxIntegral.Integrable I l f vol → BoxIntegral.BoxAdditiveMap ι F ↑I
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousOn.mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (f * g) s
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instModule : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      {V : Type u_5} →
        [inst : AddCommMonoid Γ] →
          [inst_1 : PartialOrder Γ] →
            [inst_2 : IsOrderedCancelAddMonoid Γ] →
              [inst_3 : PartialOrder Γ'] →
                [inst_4 : AddAction Γ Γ'] →
                  [IsOrderedCancelVAdd Γ Γ'] →
                    [inst_6 : AddCommMonoid V] →
                      [inst_7 : Semiring R] → [inst_8 : Module R V] → Module (HahnSeries Γ R) (HahnModule Γ' R V)
-- Mathlib.Data.Sym.Sym2
Set.sym2_singleton : ∀ {α : Type u_1} (a : α), {a}.sym2 = {s(a, a)}
-- Init.Core
instSubsingletonEmpty : Subsingleton Empty
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.mem_quotToDoubleCoset_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (i : DoubleCoset.Quotient ↑H ↑K) (a : G),
  a ∈ DoubleCoset.quotToDoubleCoset H K i ↔ DoubleCoset.mk H K a = i
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
OpenNormalSubgroup.toFiniteIndexNormalSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : CompactSpace G] [inst_3 : ContinuousMul G]
  (H : OpenNormalSubgroup G), H.toFiniteIndexNormalSubgroup = FiniteIndexNormalSubgroup.ofSubgroup ↑H.toOpenSubgroup
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
norm_cfc_lt_iff : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜)
  (a : A) {c : ℝ},
  0 < c →
    autoParam (ContinuousOn f (spectrum 𝕜 a)) norm_cfc_lt_iff._auto_1 →
      autoParam (p a) norm_cfc_lt_iff._auto_3 → (‖cfc f a‖ < c ↔ ∀ x ∈ spectrum 𝕜 a, ‖f x‖ < c)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCoseparator.hasSeparator_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.HasCoseparator C],
  CategoryTheory.HasSeparator Cᵒᵖ
-- Mathlib.Data.List.Chain
List.IsChain.infix : ∀ {α : Type u_1} {R : α → α → Prop} {l l₁ : List α}, List.IsChain R l → l₁ <:+: l → List.IsChain R l₁
-- Mathlib.Data.Nat.Nth
Nat.nth_eq_zero : ∀ {p : ℕ → Prop} {n : ℕ}, Nat.nth p n = 0 ↔ p 0 ∧ n = 0 ∨ ∃ (hf : (Set.ofPred p).Finite), hf.toFinset.card ≤ n
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDeriv_succ_apply_left : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {n : ℕ} (m : Fin (n + 1) → E),
  (iteratedFDeriv 𝕜 (n + 1) f x) m = ((fderiv 𝕜 (iteratedFDeriv 𝕜 n f) x) (m 0)) (Fin.tail m)
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoalParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.PlainTermGoalParams
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.le_rightCont : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : PartialOrder ι] (𝓕 : MeasureTheory.Filtration ι m),
  𝓕 ≤ 𝓕.rightCont
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftComp_hom_app_left : ∀ {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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ L₃ : CategoryTheory.Functor A T} (l : L₁ ⟶ L₂) (l' : L₂ ⟶ L₃) (X : CategoryTheory.Comma L₃ R),
  ((CategoryTheory.Comma.mapLeftComp R l l').hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  {F : S₁.X ⟶ S₂.X} {f : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n}
  {comm :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F.app (Opposite.op { len := n })) =
          CategoryTheory.CategoryStruct.comp (f n) (S₂.s.ι n))
      CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam}
  {F_1 : S₁.X ⟶ S₂.X} {f_1 : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n}
  {comm_1 :
    autoParam
      (∀ (n : ℕ),
        CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F_1.app (Opposite.op { len := n })) =
          CategoryTheory.CategoryStruct.comp (f_1 n) (S₂.s.ι n))
      CategoryTheory.SimplicialObject.Split.Hom.comm._autoParam},
  { F := F, f := f, comm := comm } = { F := F_1, f := f_1, comm := comm_1 } → F = F_1 ∧ f = f_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel_a₃_eq : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] (W : WeierstrassCurve K)
  [hW : WeierstrassCurve.IsIntegral R W], (algebraMap R K) (WeierstrassCurve.integralModel R W).a₃ = W.a₃
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.instFunLike : {R : Type u} →
  {S : Type u₁} →
    [inst : Monoid R] →
      [inst_1 : Monoid S] →
        (φ : R →* S) →
          (A : Type v) →
            (B : Type w) →
              [inst_2 : NonUnitalNonAssocSemiring A] →
                [inst_3 : DistribMulAction R A] →
                  [inst_4 : NonUnitalNonAssocSemiring B] → [inst_5 : DistribMulAction S B] → FunLike (A →ₛₙₐ[φ] B) A B
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasStrictFDerivAt_list_prod_attach' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸 : Type u_6} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {l : List ι} {x : { i // i ∈ l } → 𝔸},
  HasStrictFDerivAt (fun x => (List.map x l.attach).prod)
    (∑ i,
      (List.map x (List.take (↑i) l.attach)).prod •
        MulOpposite.op (List.map x (List.drop (↑i).succ l.attach)).prod •
          ContinuousLinearMap.proj l.attach[Fin.cast ⋯ i])
    x
-- Mathlib.Analysis.Seminorm
/-- The seminorm of a scalar multiplication is the product of the absolute value of the scalar
and the original seminorm.  -/
Seminorm.smul' : ∀ {𝕜 : Type u_12} {E : Type u_13} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  (self : Seminorm 𝕜 E) (a : 𝕜) (x : E), self.toFun (a • x) = ‖a‖ * self.toFun x
-- Mathlib.Combinatorics.Quiver.Path.Vertices
Quiver.Path.getElem_vertices_zero : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), p.vertices[0] = a
-- Init.Data.List.Find
List.findIdx_getElem?_eq_getElem_of_exists : ∀ {α : Type u_1} {p : α → Bool} {xs : List α} (h : ∃ x ∈ xs, p x = true),
  xs[List.findIdx p xs]? = some xs[List.findIdx p xs]
-- Mathlib.Order.WithBotTop
WithBotTop.coe_strictMono : ∀ {ι : Type u_1} [inst : Preorder ι], StrictMono WithBotTop.coe
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- The right unitor isomorphism for categorical cospan transformations.  -/
CategoryTheory.Limits.CatCospanTransform.rightUnitor : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      {A' : Type u₄} →
        {B' : Type u₅} →
          {C' : Type u₆} →
            [inst : CategoryTheory.Category.{v₁, u₁} A] →
              [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
                  {F : CategoryTheory.Functor A B} →
                    {G : CategoryTheory.Functor C B} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                (φ : CategoryTheory.Limits.CatCospanTransform F G F' G') →
                                  φ.comp (CategoryTheory.Limits.CatCospanTransform.id F' G') ≅ φ
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.get? : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → Std.DTreeMap α β cmp → (a : α) → Option (β a)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.tactic : Lean.Syntax → Lean.Elab.CompletionInfo
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
denselyOrdered_iff_denselyOrdered_units_and_nontrivial_units : ∀ {α : Type u_1} [inst : LinearOrderedCommGroupWithZero α], DenselyOrdered α ↔ Nontrivial αˣ ∧ DenselyOrdered αˣ
-- Mathlib.Data.Nat.Choose.Factorization
/-- A binomial coefficient is the product of its prime factors, which are at most `n`.  -/
Nat.prod_pow_factorization_choose : ∀ (n k : ℕ), k ≤ n → ∏ p ∈ Finset.range (n + 1), p ^ (n.choose k).factorization p = n.choose k
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.IsSubDPIdeal.dpow_mem : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J : Ideal A},
  hI.IsSubDPIdeal J → ∀ (n : ℕ), n ≠ 0 → ∀ {j : A}, j ∈ J → hI.dpow n j ∈ J
-- Mathlib.GroupTheory.Subsemigroup.Center
Subsemigroup.decidableMemCenter.eq_1 : ∀ {M : Type u_1} [inst : Semigroup M] (a : M) [inst_1 : Decidable (∀ (b : M), b * a = a * b)],
  Subsemigroup.decidableMemCenter a = decidable_of_iff' (∀ (g : M), g * a = a * g) ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Congr
differentiableOn_congr : ∀ {𝕜 : 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 f₁ : E → F} {s : Set E},
  (∀ x ∈ s, f₁ x = f x) → (DifferentiableOn 𝕜 f₁ s ↔ DifferentiableOn 𝕜 f s)
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.uint8 : Lean.IR.IRType