mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.length_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp],
  (Std.ExtDTreeMap.Const.toList t).length = t.size
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- Expressing locally uniform convergence on a set using `dist`.  -/
Metric.tendstoLocallyUniformlyOn_iff : ∀ {α : Type u} {β : Type v} {ι : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : TopologicalSpace β] {F : ι → β → α}
  {f : β → α} {p : Filter ι} {s : Set β},
  TendstoLocallyUniformlyOn F f p s ↔
    ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, dist (f y) (F n y) < ε
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- The monoid hom between `PGL(n, R)` and `PGL(n, S)` induced by a
ring homomorphism `f : R →+* S`.  -/
Matrix.ProjGenLinGroup.map : {n : Type u_1} →
  {R : Type u_2} →
    [inst : Fintype n] →
      [inst_1 : DecidableEq n] →
        [inst_2 : CommRing R] →
          {S : Type u_4} → [inst_3 : CommRing S] → (R →+* S) → Matrix.ProjGenLinGroup n R →* Matrix.ProjGenLinGroup n S
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.rightUnitor_hom_unit_app : ∀ {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} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D} {inst_5 : CategoryTheory.MonoidalCategoryStruct D}
  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] (d : D) (y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).obj y)
        (CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.unitUnit C V D))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionExtensionUnit C V d
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).app
          (y, CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).map
              (CategoryTheory.MonoidalCategoryStruct.rightUnitor d).hom).app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor
          (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).obj y)).hom
      (((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d).map
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor y).inv)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.diagonal_conjTranspose : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoid α] [inst_2 : StarAddMonoid α] (v : n → α),
  (Matrix.diagonal v).conjTranspose = Matrix.diagonal (star v)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_erase : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (f : Π₀ (i : ι), β i),
  (DFinsupp.erase i f).support = f.support.erase i
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.injective : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), Function.Injective ⇑e
-- Mathlib.Tactic.CategoryTheory.Elementwise
/-- Given an equation `f = g` between morphisms `X ⟶ Y` in a category `C`
(possibly after a `∀` binder), produce the equation `∀ (x : X), f x = g x` or
`∀ FC CC _ [ConcreteCategory C FC] (x : X), f x = g x` as needed (after the `∀` binder), but
with compositions fully right associated and identities removed.

Returns the proof of the new theorem along with (optionally) a new level metavariable
for the first universe parameter to `ConcreteCategory`.

The `simpSides` option controls whether to simplify both sides of the equality, for simpNF
purposes.
 -/
Mathlib.Tactic.Elementwise.elementwiseExpr : Lean.Name → Lean.Expr → optParam Bool true → Lean.MetaM (Lean.Expr × Option (Lean.Level × Lean.Level))
-- Mathlib.Analysis.Complex.Exponential
Real.exp_nat_mul : ∀ (x : ℝ) (n : ℕ), Real.exp (↑n * x) = Real.exp x ^ n
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.one_top : ENNReal.HolderConjugate 1 ⊤
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, k ∈ t.insert k v
-- Mathlib.Data.Matrix.Mul
Matrix.vecMulVec_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m]
  (x : l → α) (y : m → α) (M : Matrix m n α), Matrix.vecMulVec x y * M = Matrix.vecMulVec x (Matrix.vecMul y M)
-- Mathlib.Order.Partition.Finpartition
Finpartition.card_bind : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α] {a : α}
  {P : Finpartition a} (Q : (i : α) → i ∈ P.parts → Finpartition i),
  (P.bind Q).parts.card = ∑ A ∈ P.parts.attach, (Q ↑A ⋯).parts.card
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_eq_bot : ∀ {M : Type u_2} [inst : Add M] {S : AddSubsemigroup M}, S.op = ⊥ ↔ S = ⊥
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Icc_succ_left_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] [NoMaxOrder α] (a b : α),
  Finset.Icc (Order.succ a) b = Finset.Ioc a b
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The polynomial algebra w.r.t. a family of generators modulo a family of relations.  -/
Algebra.Presentation.Quotient : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Presentation R S ι σ → Type (max w u)
-- Lean.LocalContext
/-- Participates fully in type class search, tactics, and is shown even if inaccessible.

For example: the `x` in `fun x => _` has the default kind.
 -/
Lean.LocalDeclKind.default : Lean.LocalDeclKind
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1π_eq_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x y : ↥(groupCohomology.cocycles₁ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π A)) x =
      (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π A)) y ↔
    ⇑x - ⇑y ∈ groupCohomology.coboundaries₁ A
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inr_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inr X Y)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    h
-- Mathlib.RingTheory.Polynomial.Morse
/-- If the roots of `f` in `S` have at most one collision modulo each maximal ideal `m`, and if a
group `G` acting transitively on the roots in `S` is generated by inertia subgroups, then `G`
surjects onto the symmetric group `S_n`.

Such polynomials are called *Morse functions* in Section 4.4 of [serre-galois].  -/
Polynomial.Splits.surjective_toPermHom_of_iSup_inertia_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain S]
  {G : Type u_3} [inst_4 : Group G] [inst_5 : MulSemiringAction G S] [inst_6 : SMulCommClass G R S] {f : Polynomial R},
  (Polynomial.map (algebraMap R S) f).Splits →
    ∀ [MulAction.IsPretransitive G ↑(f.rootSet S)],
      (∀ (m : MaximalSpectrum S), (f.rootSet S).ncard ≤ (f.rootSet (S ⧸ m.asIdeal)).ncard + 1) →
        ⨆ m, Ideal.inertia G m.asIdeal = ⊤ → Function.Surjective ⇑(MulAction.toPermHom G ↑(f.rootSet S))
-- Mathlib.Combinatorics.Additive.Convolution
/-- Given finite subsets `A` and `B` of an additive group `G`,
convolution of `A` and `B` is a map `G → ℕ` that maps `x ∈ G` to the number of distinct
representations of `x` in the form `x = a + b`, where `a ∈ A`, `b ∈ B`.  -/
Finset.addConvolution : {G : Type u_1} → [AddGroup G] → [DecidableEq G] → Finset G → Finset G → G → ℕ
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- `P⁺⁺` is always a sheaf.  -/
CategoryTheory.GrothendieckTopology.Plus.isSheaf_plus_plus : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.Presheaf.IsSheaf J (J.plusObj (J.plusObj P))
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {n : ℕ} {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)}
  [inst_1 : SizeOf C] {k k' : ℕ} (hk : k < n) (hk' : k' < n) (j : (X k hk).fst) (j' : (X k' hk').fst)
  (a a_1 : (X k hk).snd j ⟶ (X k' hk').snd j'),
  sizeOf (CategoryTheory.IsCofiltered.CofilteredClosureSmall.InductiveStep.eq✝ hk hk' j j' a a_1) =
    1 + sizeOf k + sizeOf k' + sizeOf hk + sizeOf hk' + sizeOf j + sizeOf j' + sizeOf a + sizeOf a_1
-- Mathlib.Computability.Primrec.Basic
Primrec.and : Primrec₂ and
-- Lean.Level
Lean.Level.depth : Lean.Level → ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inr_opIso_inv_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P Q : C) [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct P Q] {Z : Cᵒᵖ} (h : Opposite.op (P ⊞ Q) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.opIso P Q).inv h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd.op h
-- Mathlib.Algebra.Homology.ConcreteCategory
HomologicalComplex.i_cyclesMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Abelian C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [inst_6 : (CategoryTheory.forget₂ C Ab).PreservesHomology]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι}
  (x : ↑((CategoryTheory.forget₂ C Ab).obj (K.X i))) (j : ι) (hj : c.next i = j)
  (hx : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (K.d i j))) x = 0),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map (K.iCycles i))) (K.cyclesMk x j hj hx) = x
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.continuous_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : TopologicalSpace X],
  Continuous ⇑Metric.Snowflaking.ofSnowflaking
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_add_zero_inv_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a : A) (X : C),
  (CategoryTheory.shiftFunctorAdd C a 0).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.eqToHom ⋯)
-- Std.Http.Server.Config
/-- Maximum number of leading empty lines (bare CRLF) to skip before a request-line
(RFC 9112 §2.2 robustness). Default: 8.
 -/
Std.Http.Config.maxLeadingEmptyLines : Std.Http.Config → ℕ
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.preservesColimitsOfSize_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D),
  Subsingleton (CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_nonempty : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set β} {a : α}, (a • s).Nonempty ↔ s.Nonempty
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_add : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {n : ℕ} {x y : A},
  x ∈ I → y ∈ I → self.dpow n (x + y) = ∑ k ∈ Finset.HasAntidiagonal.antidiagonal n, self.dpow k.1 x * self.dpow k.2 y
-- Mathlib.Order.CountableSupClosed
inf_mem_countableInfClosure : ∀ {α : Type u_2} {s : Set α} {a b : α} [inst : SemilatticeInf α], a ∈ s → b ∈ s → a ⊓ b ∈ countableInfClosure s
-- Lean.Attributes
Lean.instInhabitedEnumAttributes : {a : Type} → Inhabited (Lean.EnumAttributes a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.isEmpty_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ → t₁.isEmpty = t₂.isEmpty
-- Mathlib.Algebra.Order.Group.Abs
le_of_abs_le : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G}, |a| ≤ b → a ≤ b
-- Lean.Meta.AppBuilder
_private.Lean.Meta.AppBuilder.0.Lean.Meta.throwAppBuilderException : {α : Type} → Lean.Name → Lean.MessageData → Lean.MetaM α
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_of_notMem_CNF : ∀ {b o e : Ordinal.{u_1}}, e ∉ List.map Prod.fst (Ordinal.CNF b o) → (Ordinal.CNF.coeff b o) e = 0
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- Use `eLpNorm_smul_measure_of_ne_top` instead.  -/
_private.Mathlib.MeasureTheory.Function.LpSeminorm.Basic.0.MeasureTheory.eLpNorm_smul_measure_of_ne_zero_of_ne_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {p : ENNReal},
  p ≠ 0 →
    p ≠ ⊤ →
      ∀ {f : α → ε} (c : ENNReal), MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.injectiveDimension_le_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ),
  CategoryTheory.injectiveDimension X ≤ ↑n ↔ CategoryTheory.HasInjectiveDimensionLE X n
-- Mathlib.Algebra.Polynomial.Eval.Algebra
Polynomial.eval₂_pow' : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (x : S)
  (p : Polynomial R) (n : ℕ), Polynomial.eval₂ (algebraMap R S) x (p ^ n) = Polynomial.eval₂ (algebraMap R S) x p ^ n
-- Mathlib.Algebra.Field.Basic
half_sub : ∀ {K : Type u_1} [inst : DivisionRing K] [NeZero 2] (a : K), a / 2 - a = -(a / 2)
-- Mathlib.Analysis.InnerProductSpace.Harmonic.HarmonicContOnCl
/-- Eta-expanded form of `InnerProductSpace.HarmonicContOnCl.neg` -/
InnerProductSpace.HarmonicContOnCl.fun_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicContOnCl f s → InnerProductSpace.HarmonicContOnCl (fun i => -f i) s
-- Mathlib.Algebra.Group.End
AddAut.congr_symm_apply : ∀ {G : Type u_3} [inst : AddGroup G] {H : Type u_7} [inst_1 : AddGroup H] (ϕ : G ≃+ H) (f : AddAut H),
  (AddAut.congr ϕ).symm f = ϕ.trans (AddEquiv.trans f ϕ.symm)
-- Mathlib.Analysis.Real.Hyperreal
/-- Hyperreal numbers on the ultrafilter extending the cofinite filter.  -/
Hyperreal.«termℝ*» : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.keysArray_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {f : α → Bool},
  (Std.DTreeMap.filter (fun k x => f k) t).keysArray = Array.filter f t.keysArray
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.iUnion_cellFrontier_subset_skeleton`. -/
Topology.CWComplex.iUnion_cellFrontier_subset_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D] (l : ℕ),
  ⋃ j, Topology.RelCWComplex.cellFrontier l j ⊆ ↑(Topology.RelCWComplex.skeleton C ↑l)
-- Mathlib.Algebra.DualNumber
/-- When applied to `ε`, `DualNumber.lift` produces the element of `B` that squares to 0.  -/
DualNumber.lift_apply_eps : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { fe // fe.2 * fe.2 = 0 ∧ ∀ (a : A), Commute fe.2 (fe.1 a) }),
  (DualNumber.lift fe) DualNumber.eps = (↑fe).2
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.monoCoprod_of_preservesCoprod_of_reflectsMono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.MonoCoprod D]
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F]
  [F.ReflectsMonomorphisms], CategoryTheory.Limits.MonoCoprod C
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.nil_iff : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {f : ℝ → ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
        f).Approximates ↔
    f =ᶠ[Filter.atTop] 0
-- Mathlib.Tactic.ProdAssoc
/-- This function should act as the "reverse" of `ProdTree.unpack`, constructing
a term of the iterated product out of a list of terms of the types appearing in the product.  -/
Lean.Expr.ProdTree.pack : List Lean.Expr → Lean.Expr.ProdTree → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_sub_const_fun : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} (c : F), (deriv fun x => f x - c) = deriv f
-- Std.Http.Data.URI.Basic
Std.Http.URI.mk : Std.Http.URI.Scheme →
  Option Std.Http.URI.Authority → Std.Http.URI.Path → Std.Http.URI.Query → Option String → Std.Http.URI
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDeriv_prodMk : ∀ {𝕜 : 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 : E → G},
  ContDiffAt 𝕜 n f x →
    ContDiffAt 𝕜 n g x →
      ∀ {i : ℕ},
        ↑i ≤ n → iteratedFDeriv 𝕜 i (fun x => (f x, g x)) x = (iteratedFDeriv 𝕜 i f x).prod (iteratedFDeriv 𝕜 i g x)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.Normal.map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup G},
  H.Normal → ∀ (f : G →+ N), Function.Surjective ⇑f → (AddSubgroup.map f H).Normal
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
/-- If some `r` is strictly larger than the Riemannian edistance between two points, there exists
a path between these two points of length `< r`. Here, we get such a path on an arbitrary interval
`[a, b]` with `a < b`, and moreover we ensure that the path is locally constant around `a` and `b`,
which is convenient for gluing purposes.  -/
Manifold.exists_lt_locally_constant_of_riemannianEDist_lt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)] {x y : M} {r : ENNReal}
  {a b : ℝ},
  Manifold.riemannianEDist I x y < r →
    a < b →
      ∃ γ,
        γ a = x ∧
          γ b = y ∧
            ContMDiff (modelWithCornersSelf ℝ ℝ) I 1 γ ∧
              Manifold.pathELength I γ a b < r ∧ (γ =ᶠ[nhds a] fun x_1 => x) ∧ γ =ᶠ[nhds b] fun x => y
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instCreatesColimitsTopCatToTopCat : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] → CategoryTheory.CreatesColimits GeneratedByTopCat.toTopCat
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionOptions.mk : Option (Array String) → Option (Array String) → Bool → Lean.Lsp.CompletionOptions
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.defEq.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheoremKey : Type
-- Mathlib.Algebra.Group.Submonoid.Saturation
AddSubmonoid.AddSaturated.add_mem_iff : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : AddSubmonoid M}, s.AddSaturated → ∀ {x y : M}, x + y ∈ s ↔ x ∈ s ∧ y ∈ s
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- `single` as a `DistribMulActionSemiHom`.

See also `lsingle` for the version as a linear map.  -/
SkewMonoidAlgebra.DistribMulActionHom.single : {R : Type u_3} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : DistribMulAction R M] → {α : Type u_6} → α → M →+[R] SkewMonoidAlgebra M α
-- Std.Sync.StreamMap
Std.AnyAsyncStream.getSelector : {α : Type} → Std.AnyAsyncStream α → Std.Async.Selector α × IO Unit
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_const_eq' : ∀ (α : Type u_1) {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (b : β), ∃ b', ↑(MeasureTheory.AEEqFun.const α b) = fun x => b'
-- Mathlib.Data.Matrix.DMatrix
/-- `DMatrix m n` is the type of dependently typed matrices
whose rows are indexed by the type `m` and
whose columns are indexed by the type `n`.

In most applications `m` and `n` are finite types.  -/
DMatrix : (m : Type u) → (n : Type u') → (m → n → Type v) → Type (max u u' v)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.asIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.asIso f).inv = CategoryTheory.inv f
-- Mathlib.Topology.Order.SuccPred
PredOrder.nhds_top : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  [inst_5 : OrderTop α], nhds ⊤ = pure ⊤
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.neg_apply : ∀ (G : Type v) [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G]
  [inst_3 : IsIsometricVAdd Gᵃᵒᵖ G] (a : G), (IsometryEquiv.neg G) a = -a
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobian.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P P_1 : Algebra.PreSubmersivePresentation R S ι σ), P = P_1 → ∀ [inst_3 : Finite σ], P.jacobian = P_1.jacobian
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instIsNegApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsNegApply (ModularForm Γ k) UpperHalfPlane ℂ