mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.addConst_mul_card : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G), A.addConst B * ↑A.card = ↑(A + B).card
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_eq_getKeyD_default : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, m.getKey! a = m.getKeyD a default
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.forM_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit.{w + 1}},
  t₁.Equiv t₂ → forM t₁ f = forM t₂ f
-- Mathlib.Data.List.Basic
List.filter_attach : ∀ {α : Type u} (l : List α) (p : α → Bool),
  List.filter (fun x => p ↑x) l.attach = List.map (Subtype.map id ⋯) (List.filter p l).attach
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.readMCtx₁ : Aesop.EqualUpToIdsM Lean.MetavarContext
-- Mathlib.Order.CompactlyGenerated.Basic
/-- A compactness property for a complete lattice is that any `sup`-closed non-empty subset
contains its `sSup`.  -/
CompleteLattice.IsSupClosedCompact : (α : Type u_2) → [CompleteLattice α] → Prop
-- Qq.Macro
Qq.Impl.UnquoteState.mayPostpone : Qq.Impl.UnquoteState → Bool
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.p_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.Idempotents.Karoubi C}
  (f : P.Hom Q), CategoryTheory.CategoryStruct.comp P.p f.f = f.f
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_symm_apply_right : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (β : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk sq₁₃.π),
  ((adj₂.arrowHomEquiv sq₁₂ sq₁₃).symm β).right =
    adj₂.homEquiv.symm (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right β) sq₁₃.snd)
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
AddGroupLieAlgebra.bracket_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] (v w : AddGroupLieAlgebra I G),
  ⁅v, w⁆ = VectorField.mlieBracket I (addInvariantVectorField v) (addInvariantVectorField w) 0
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.epsilon_eq_deriv : ∀ (o : Ordinal.{u_1}), o.epsilon = Ordinal.deriv (fun a => Ordinal.omega0 ^ a) o
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.pi_bot : ∀ {ι : Type u_4} {M : ι → Type u_5} [inst : (i : ι) → AddZeroClass (M i)], (AddSubmonoid.pi Set.univ fun i => ⊥) = ⊥
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y Z : C),
  F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (F.obj Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
            (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))))
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.prod_top : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (s : AddSubsemigroup M),
  s.prod ⊤ = AddSubsemigroup.comap (AddHom.fst M N) s
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂'.eq_1 : ∀ (R : Type u_1) {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m],
  Matrix.toLinearMapₛₗ₂' R σ₁ σ₂ = (LinearMap.toMatrixₛₗ₂' R).symm
-- Mathlib.Algebra.Category.Grp.AB
instIsGrothendieckAbelianAddCommGrpCat : CategoryTheory.IsGrothendieckAbelian.{u, u, u + 1} AddCommGrpCat
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.prop_of_isLimit_fan : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderFiniteProducts] {J : Type u_2} [Finite J] {f : J → C} {F : CategoryTheory.Limits.Fan f}
  (hF : CategoryTheory.Limits.IsLimit F), (∀ (j : J), P (f j)) → P F.pt
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The two-variable Jacobi theta function,
`θ z τ = ∑' (n : ℤ), cexp (2 * π * I * n * z + π * I * n ^ 2 * τ)`.
 -/
jacobiTheta₂ : ℂ → ℂ → ℂ
-- Mathlib.Order.Hom.CompleteLattice
/-- Using `Set.image`, a function between types yields a `sSupHom` between their lattices of
subsets.

See also `CompleteLatticeHom.setPreimage`.  -/
sSupHom.setImage : {α : Type u_2} → {β : Type u_3} → (α → β) → sSupHom (Set α) (Set β)
-- Mathlib.Data.ENNReal.Inv
ENNReal.coe_zpow : ∀ {r : NNReal}, r ≠ 0 → ∀ (n : ℤ), ↑(r ^ n) = ↑r ^ n
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
HasSum.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (f : β → α) (a : α)
  (L : SummationFilter β), HasSum f a L = Filter.Tendsto (fun s => ∑ b ∈ s, f b) L.filter (nhds a)
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonUSize : Lean.FromJson USize
-- Mathlib.Algebra.Group.WithOne.Map
/-- Lift a map `f : α → β` to `WithZero α → WithZero β`. Implemented using `Option.map`.

Note: the definition previously known as `WithZero.map` is now called `WithZero.mapAddHom`.  -/
WithZero.map : {α : Type u_1} → {β : Type u_2} → (α → β) → WithZero α → WithZero β
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.cokernelBiproductFromSubtypeIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {K : Type}
  [inst_2 : Finite K] [inst_3 : CategoryTheory.Limits.HasFiniteBiproducts C] (f : K → C) (p : K → Prop),
  (CategoryTheory.Limits.cokernelBiproductFromSubtypeIso f p).hom =
    CategoryTheory.Limits.colimit.desc
      (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.biproduct.fromSubtype f p) 0)
      (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biproduct.toSubtype f pᶜ) ⋯)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.sections_property : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (s : M.sections) {X Y : Cᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (M.map f)) (↑s X) = ↑s Y
-- Batteries.Data.Array.Scan
Array.getElem?_scanl_zero : ∀ {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {f : β → α → β}, (Array.scanl f init as)[0]? = some init
-- Std.Http.Data.Headers.Name
/-- Standard Content-Type header name
 -/
Std.Http.Header.Name.contentType : Std.Http.Header.Name
-- Lean.Meta.MkIffOfInductiveProp
/-- Auxiliary data associated with a single constructor of an inductive declaration.
 -/
_private.Lean.Meta.MkIffOfInductiveProp.0.Lean.Meta.Shape : Type
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.atEnd : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} →
        [inst : String.Slice.Pattern.ToForwardSearcher pat σ] → String.Slice.SplitInclusiveIterator pat s
-- Std.Data.ExtTreeMap.Lemmas
/-- Variant of `getElem?_map` that holds without `LawfulEqCmp`.  -/
Std.ExtTreeMap.getElem?_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α}, (Std.ExtTreeMap.map f t)[k]? = Option.pmap (fun v h' => f (t.getKey k h') v) t[k]? ⋯
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.eq_trivialization : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [i : MemTrivializationAtlas e],
  e = Bundle.Trivial.trivialization B F
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanServerCapabilities : Type
-- Mathlib.Analysis.SpecialFunctions.Log.InvLog
Real.not_continuousAt_inv_log_neg_one : ¬ContinuousAt (fun x => (Real.log x)⁻¹) (-1)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.isPell_nat : ∀ {a : ℕ} (a1 : 1 < a) {x y : ℕ}, Pell.IsPell { re := ↑x, im := ↑y } ↔ x * x - Pell.d✝ a1 * y * y = 1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ext_iff : ∀ {X : AlgebraicGeometry.Scheme} {I J : X.IdealSheafData}, I = J ↔ I.ideal = J.ideal
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- The Mellin transform of `f` is well-defined and equal to `P.Λ s`, for all `s`.  -/
IsStrongFEPair.hasMellin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → ∀ (s : ℂ), HasMellin P.f s (P.Λ s)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.splitMax'.eq_def : ∀ {α : Type u_1} (x : Ordnode α) (x_1 : α) (x_2 : Ordnode α),
  x.splitMax' x_1 x_2 =
    match x, x_1, x_2 with
    | l, x, Ordnode.nil => (l, x)
    | l, x, Ordnode.node size rl rx rr =>
      match rl.splitMax' rx rr with
      | (r', xm) => (l.balanceL x r', xm)
-- Mathlib.Lean.Expr.Basic
/-- If an `Expr` has the form `Type u`, then return `some u`, otherwise `none`.  -/
Lean.Expr.type? : Lean.Expr → Option Lean.Level
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.unitsEquiv_finite_valued_eq_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (a : (IsDedekindDomain.FiniteAdeleRing R K)ˣ),
  ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite,
    Valued.v ↑(((RestrictedProduct.unitsEquiv (IsDedekindDomain.HeightOneSpectrum.adicCompletion K)) a) v) = 1
-- Mathlib.Analysis.Normed.Group.Constructions
ULift.seminormedAddGroup.eq_1 : ∀ {E : Type u_2} [inst : SeminormedAddGroup E],
  ULift.seminormedAddGroup =
    SeminormedAddGroup.induced (ULift.{u_5, u_2} E) E { toFun := ULift.down, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Maps.Basic
/-- The topology induced under an inclusion `f : X → Y` from a discrete topological space `Y`
is the discrete topology on `X`.

See also `DiscreteTopology.of_continuous_injective`.  -/
Topology.IsEmbedding.discreteTopology : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [DiscreteTopology Y], Topology.IsEmbedding f → DiscreteTopology X
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.tag : {α : Type u} → α → Lean.Widget.TaggedText α → Lean.Widget.TaggedText α
-- Mathlib.Control.Traversable.Basic
instTraversableId : Traversable Id
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_ofFin : ∀ (n : Fin (2 ^ 16)), { toBitVec := { toFin := n } } = UInt16.ofFin n
-- Mathlib.Algebra.Group.Shrink
Shrink.addEquiv.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : Add α], Shrink.addEquiv = (equivShrink α).symm.addEquiv
-- Mathlib.Data.Num.Bitwise
/-- This is a nonzero (and "non minus one") version of `SNum`.
See the documentation of `SNum` for more details.  -/
NzsNum : Type
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofAlgHom_toAlgHom : ∀ {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₂] (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁)
  (h₁ : (↑f).comp g = AlgHom.id R A₂) (h₂ : g.comp ↑f = AlgHom.id R A₁), AlgEquiv.ofAlgHom (↑f) g h₁ h₂ = f
-- Init.Data.ByteArray.Bootstrap
_private.Init.Data.ByteArray.Bootstrap.0.List.toByteArray.match_1.eq_1 : ∀ (motive : List UInt8 → ByteArray → Sort u_1) (r : ByteArray) (h_1 : (r : ByteArray) → motive [] r)
  (h_2 : (b : UInt8) → (bs : List UInt8) → (r : ByteArray) → motive (b :: bs) r),
  (match [], r with
    | [], r => h_1 r
    | b :: bs, r => h_2 b bs r) =
    h_1 r
-- Init.Data.Array.MinMax
Array.max?_eq_some_max : ∀ {α : Type u_1} [inst : Max α] {xs : Array α} (h : xs ≠ #[]), xs.max? = some (xs.max h)
-- Init.PropLemmas
Decidable.imp_iff_not_or : ∀ {a b : Prop} [Decidable a], a → b ↔ ¬a ∨ b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} (h' : k ∈ t), t.getKey k h' = k
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.negPart_neg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [T2Space A] (a : A), (-a)⁻ = a⁺
-- Mathlib.Algebra.DirectSum.Module
DirectSum.instIsScalarTower : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {S : Type u_1} [inst_3 : Semiring S] [inst_4 : SMul R S]
  [inst_5 : (i : ι) → Module S (M i)] [∀ (i : ι), IsScalarTower R S (M i)], IsScalarTower R S (DirectSum ι fun i => M i)
-- Mathlib.Data.Set.Piecewise
Set.piecewise_singleton : ∀ {α : Type u_1} {β : Type u_2} (x : α) [inst : (y : α) → Decidable (y ∈ {x})] [inst_1 : DecidableEq α] (f g : α → β),
  {x}.piecewise f g = Function.update g x (f x)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_eq_top_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  InformationTheory.klDiv μ ν = ⊤ ↔ μ.AbsolutelyContinuous ν → ¬MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termG₂_1 : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- The iterated derivative of an analytic function, on vectors `(y, ..., y)`, is given by `n!`
times the `n`-th term in the power series. For a more general result giving the full iterated
derivative as a sum over the permutations of `Fin n`, see
`HasFPowerSeriesOnBall.iteratedFDeriv_eq_sum`.  -/
HasFPowerSeriesOnBall.factorial_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r →
    ∀ (y : E) [CompleteSpace F] (n : ℕ), (n.factorial • (p n) fun x => y) = (iteratedFDeriv 𝕜 n f x) fun x => y
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkSyntax : Lean.Linter.MissingDocs.SimpleHandler
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.ofNat_ctorIdx : ∀ (x : Lean.Meta.Simp.DischargeResult), Lean.Meta.Simp.DischargeResult.ofNat x.ctorIdx = x
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'AddMonoidHom_apply : ∀ {o : Type u_4} (m' : o → Type u_7) (n' : o → Type u_8) (α : Type u_12) [inst : DecidableEq o]
  [inst_1 : AddZeroClass α] (M : (i : o) → Matrix (m' i) (n' i) α),
  (Matrix.blockDiagonal'AddMonoidHom m' n' α) M = Matrix.blockDiagonal' M
-- Mathlib.Data.List.Lookmap
_private.Mathlib.Data.List.Lookmap.0.List.lookmap.go.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((b : α) → motive (some b)) → (Unit → motive none) → motive x
-- Lean.Server.Requests
Lean.Language.SnapshotTree.foldSnaps.Control.proceed.inj : ∀ {foldChildren foldChildren_1 : Bool},
  Lean.Language.SnapshotTree.foldSnaps.Control.proceed foldChildren =
      Lean.Language.SnapshotTree.foldSnaps.Control.proceed foldChildren_1 →
    foldChildren = foldChildren_1
-- Init.Data.Rat.Basic
Rat.instDecidableLe : (a b : ℚ) → Decidable (a ≤ b)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_le_minKey_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (cmp (t.minKey ⋯) ((t.erase k).minKey he)).isLE = true
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  (CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₃ = Z
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.instIsMonHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} [inst_3 : CategoryTheory.IsCommMonObj H.X]
  [inst_4 : CategoryTheory.IsCommMonObj G.X] (f : G ⟶ H), CategoryTheory.IsMonHom f
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.instCoeTCSetForallReal : {ι : Type u_1} → CoeTC (BoxIntegral.Box ι) (Set (ι → ℝ))
-- Mathlib.CategoryTheory.Action.Basic
/-- `Functor.mapAction` is functorial in the functor.  -/
CategoryTheory.Functor.mapActionComp : {V : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    {W : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} W] →
        (G : Type u_3) →
          [inst_2 : Monoid G] →
            {T : Type u_4} →
              [inst_3 : CategoryTheory.Category.{v_3, u_4} T] →
                (F : CategoryTheory.Functor V W) →
                  (F' : CategoryTheory.Functor W T) → (F.comp F').mapAction G ≅ (F.mapAction G).comp (F'.mapAction G)
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.instForInOfMonad : {α : Type u_1} →
  [inst : BEq α] → [inst_1 : Hashable α] → {m : Type u_2 → Type u_3} → [Monad m] → ForIn m (Aesop.OrderedHashSet α) α
-- Mathlib.CategoryTheory.Presentable.Type
CategoryTheory.Types.isCardinalPresentable_iff : ∀ {X : Type u} (κ : Cardinal.{u}) [inst : Fact κ.IsRegular],
  CategoryTheory.IsCardinalPresentable X κ ↔ HasCardinalLT X κ
-- Mathlib.Data.Fintype.Card
Finite.to_wellFoundedGT : ∀ {α : Type u_1} [Finite α] [inst : Preorder α], WellFoundedGT α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] {k : α} {f : Option β → Option β} (h : m.WF) {hc : k ∈ m.alter k f},
  (m.alter k f)[k] = (f m[k]?).get ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (w : ℕ) (lhs rhs : aig.RefVec w)
  (cin : aig.Ref),
  Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit aig { w := w, vec := { lhs := lhs, rhs := rhs }, cin := cin } =
    Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs 0 cin
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- The cosine zeta function, i.e. the meromorphic function of `s` which agrees
with `∑' (n : ℕ), cos (2 * π * a * n) / n ^ s` for `1 < re s`.  -/
HurwitzZeta.cosZeta : UnitAddCircle → ℂ → ℂ
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.symm_i₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A), P.symm.i₀ = P.i₁
-- Mathlib.Topology.Convenient.Category
/-- The functor `ContinuousGeneratedByCat X ⥤ GeneratedByTopCat X` which is
part of the equivalence `ContinuousGeneratedByCat.equivalence`.  -/
ContinuousGeneratedByCat.toGeneratedByTopCat : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      CategoryTheory.Functor (ContinuousGeneratedByCat X) (GeneratedByTopCat X)
-- Batteries.Recycling.MonadSatisfying.Basic
/-- `SatisfiesM` distributes over `<*>`, weakest precondition version 2.
(Use this when `f` and the goal are known and `x` is a subgoal.)
 -/
SatisfiesM.seq_pre' : ∀ {m : Type u_1 → Type u_2} {α α_1 : Type u_1} {p₁ : (α → α_1) → Prop} {f : m (α → α_1)} {q : α_1 → Prop}
  [inst : Applicative m] [LawfulApplicative m] {x : m α},
  SatisfiesM p₁ f → SatisfiesM (fun a => ∀ {f : α → α_1}, p₁ f → q (f a)) x → SatisfiesM q (f <*> x)
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The expression of the relation.  -/
Mathlib.Tactic.ClickSuggestions.GrwPos.relation : Mathlib.Tactic.ClickSuggestions.GrwPos → Lean.Expr
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The image under a semigroup hom of the subsemigroup generated by a set equals the subsemigroup
generated by the image of the set.  -/
MulHom.map_mclosure : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N) (s : Set M),
  Subsemigroup.map f (Subsemigroup.closure s) = Subsemigroup.closure (⇑f '' s)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- `liminf` over a general filter is measurable. See `Measurable.liminf` for the version over `ℕ`.
 -/
Measurable.liminf' : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Type u_5} {ι' : Type u_6} {f : ι → δ → α} {v : Filter ι},
  (∀ (i : ι), Measurable (f i)) →
    ∀ {p : ι' → Prop} {s : ι' → Set ι},
      v.HasCountableBasis p s → (∀ (j : ι'), (s j).Countable) → Measurable fun x => Filter.liminf (fun x_1 => f x_1 x) v
-- Init.Data.List.Sublist
List.IsSuffix.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ → l₁ ⊆ l₂
-- Lean.DocString.Parser
/-- Parses a footnote reference target.
 -/
Lean.Doc.Parser.footnoteRef : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn