mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.App
/-- The resultant expression being built.  -/
Lean.Elab.Term.ElabElim.State.f : Lean.Elab.Term.ElabElim.State → Lean.Expr
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.val_inv_det_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : GL n R),
  ↑(Matrix.GeneralLinearGroup.det A)⁻¹ = (↑A⁻¹).det
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d.eq_4 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (a a_1 : ℕ),
  h.d (Int.ofNat a) (Int.negSucc a_1) = 0
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instModuleQuotientCotangent : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Module (R ⧸ I) I.Cotangent
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- Endowing the space `PiLp p β` with the `L^p` edistance. We register this instance
separate from `pi_Lp.pseudo_emetric` since the latter requires the type class hypothesis
`[Fact (1 ≤ p)]` in order to prove the triangle inequality.

Registering this separately allows for a future emetric-like structure on `PiLp p β` for `p < 1`
satisfying a relaxed triangle inequality. The terminology for this varies throughout the
literature, but it is sometimes called a *quasi-metric* or *semi-metric*.  -/
PiLp.instEDist : (p : ENNReal) → {ι : Type u_2} → (β : ι → Type u_4) → [Fintype ι] → [(i : ι) → EDist (β i)] → EDist (PiLp p β)
-- Mathlib.Topology.Constructions.SumProd
/-- The hypotheses on `f` are slightly weaker here compared to `mem_map_closure₂`. That
lemma requires `f` to be jointly continuous, whereas here we only require continuity in each
variable separately.  -/
map_mem_closure₂' : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y → Z} {x : X} {y : Y} {s : Set X} {t : Set Y} {u : Set Z},
  (∀ (x : X), Continuous (f x)) →
    (∀ (y : Y), Continuous fun x => f x y) →
      x ∈ closure s → y ∈ closure t → (∀ a ∈ s, ∀ b ∈ t, f a b ∈ u) → f x y ∈ closure u
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
CategoryTheory.Limits.instIsIsoProdComparison : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X Y : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (G.obj X) (G.obj Y)]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison G X Y)
-- Mathlib.Data.Fin.Tuple.Basic
/-- Adding an element at the beginning of a tuple and then updating it amounts to adding it
directly.  -/
Fin.update_snoc_last : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (z : α (Fin.last n)),
  Function.update (Fin.snoc p x) (Fin.last n) z = Fin.snoc p z
-- Mathlib.Topology.Spectral.Basic
SpectralSpace.toQuasiSober : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : SpectralSpace X], QuasiSober X
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.mul_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R), φ * 0 = 0
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.equivalenceOfReindexing_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cocone.equivalenceOfReindexing e α).inverse =
    (CategoryTheory.Limits.Cocone.precompose α.hom).comp
      ((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
        (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv))
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EvalTactic.skip : Lean.Meta.Grind.EvalTactic
-- Mathlib.Algebra.RingQuot
RingQuot.lift_mkRingHom_apply : ∀ {R : Type uR} [inst : Semiring R] {T : Type uT} [inst_1 : Semiring T] (f : R →+* T) {r : R → R → Prop}
  (w : ∀ ⦃x y : R⦄, r x y → f x = f y) (x : R), (RingQuot.lift ⟨f, w⟩) ((RingQuot.mkRingHom r) x) = f x
-- Mathlib.LinearAlgebra.Complex.Module
/-- The scalar action of `ℝ` on a `ℂ`-module `E` induced by `Module.complexToReal` associates with
another scalar action of `M` on `E` whenever the action of `ℂ` associates with the action of `M`.  -/
IsScalarTower.complexToReal : ∀ {M : Type u_1} {E : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℂ M] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ E] [inst_4 : SMul M E] [IsScalarTower ℂ M E], IsScalarTower ℝ M E
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.foldl_toList : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {f : γ → β → γ} {init : γ} {it : Std.Iter β},
  List.foldl f init it.toList = Std.Iter.fold f init it
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonAssocRing : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → [MulOneClass M] → NonAssocRing (MonoidAlgebra R M)
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instRxcLawfulHasSize : ∀ {n : ℕ}, Std.Rxc.LawfulHasSize (BitVec n)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_finite_biUnion : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {s : Set β},
  s.Finite →
    ∀ {t : β → Set α}, MeasureTheory.IntegrableOn f (⋃ i ∈ s, t i) μ ↔ ∀ i ∈ s, MeasureTheory.IntegrableOn f (t i) μ
-- Mathlib.RingTheory.Polynomial.RationalRoot
scaleRoots_aeval_eq_zero_of_aeval_mk'_eq_zero : ∀ {A : Type u_1} {S : Type u_4} [inst : CommRing A] [inst_1 : CommRing S] {M : Submonoid A} [inst_2 : Algebra A S]
  [inst_3 : IsLocalization M S] {p : Polynomial A} {r : A} {s : ↥M},
  (Polynomial.aeval (IsLocalization.mk' S r s)) p = 0 → (Polynomial.aeval ((algebraMap A S) r)) (p.scaleRoots ↑s) = 0
-- Mathlib.Algebra.Module.Torsion.Basic
/-- **Alias** of `isAddTorsion_iff_isTorsion_int`. -/
AddMonoid.isTorsion_iff_isTorsion_int : ∀ {M : Type u_2} [inst : AddCommGroup M], IsAddTorsion M ↔ Module.IsTorsion ℤ M
-- Mathlib.RingTheory.MatrixAlgebra
/-- (Implementation detail).
The function underlying `(A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A`,
as an `R`-linear map.
 -/
MatrixEquivTensor.toFunLinear : (n : Type u_3) →
  (R : Type u_5) →
    (A : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [inst_2 : Algebra R A] → TensorProduct R A (Matrix n n R) →ₗ[R] Matrix n n A
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given two functors which have equivalent categories of cocones,
we can transport a colimiting cocone across the equivalence.
 -/
CategoryTheory.Limits.IsColimit.ofCoconeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              {D : Type u₄} →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} D] →
                  {G : CategoryTheory.Functor K D} →
                    (h : CategoryTheory.Limits.Cocone G ≌ CategoryTheory.Limits.Cocone F) →
                      {c : CategoryTheory.Limits.Cocone G} →
                        CategoryTheory.Limits.IsColimit (h.functor.obj c) ≃ CategoryTheory.Limits.IsColimit c
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.div_zero : ∀ {R : Type u} [inst : EuclideanDomain R] (a : R), a / 0 = 0
-- Mathlib.Data.Set.Insert
Set.union_singleton : ∀ {α : Type u_1} {s : Set α} {a : α}, s ∪ {a} = insert a s
-- Mathlib.Algebra.FreeMonoid.Symbols
/-- The set of unique symbols in an additive free monoid element  -/
FreeAddMonoid.symbols : {α : Type u_1} → [DecidableEq α] → FreeAddMonoid α → Finset α
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.ofHom.eq_1 : ∀ {X Y : Type u} [inst : AddSemigroup X] [inst_1 : AddSemigroup Y] (f : X →ₙ+ Y),
  AddSemigrp.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainNonUnitalRingHom_id : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : Mul M],
  MonoidAlgebra.mapDomainNonUnitalRingHom R (MulHom.id M) = NonUnitalRingHom.id (MonoidAlgebra R M)
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
_private.Mathlib.Analysis.FunctionalSpaces.SobolevInequality.0.«term#_» : Lean.ParserDescr
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
/-- The `vonMangoldt` function is the function on natural numbers that returns `log p` if the input can
be expressed as `p^k` for a prime `p`.
In the case when `n` is a prime power, `Nat.minFac` will give the appropriate prime, as it is the
smallest prime factor.

In the `ArithmeticFunction` locale, we have the notation `Λ` for this function.
This is also available in the `ArithmeticFunction.vonMangoldt` locale, allowing for selective
access to the notation.
 -/
ArithmeticFunction.vonMangoldt : ArithmeticFunction ℝ
-- Mathlib.Topology.Compactness.Lindelof
/-- **Alias** of `isLindelof_iff_lindelofSpace`. -/
isLindelof_iff_LindelofSpace : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsLindelof s ↔ LindelofSpace ↑s
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.apply_eq_true_of_lt_skipWhile_bool : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos},
  pos ≤ pos' → ∀ (h₂ : pos' < pos.skipWhile p), p (pos'.get ⋯) = true
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.scientificLitNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The type of continuous monoid homomorphisms from `A` to `B`. -/
ContinuousMonoidHom.«term_→ₜ+_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Enriched.EnrichedCat
/-- Composition of `V`-enriched functors is associative up to isomorphism.  -/
CategoryTheory.EnrichedCat.associator : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₁} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {E : Type u₂} →
                [inst_4 : CategoryTheory.EnrichedCategory V E] →
                  {E' : Type u₃} →
                    [inst_5 : CategoryTheory.EnrichedCategory V E'] →
                      (F : CategoryTheory.EnrichedFunctor V C D) →
                        (G : CategoryTheory.EnrichedFunctor V D E) →
                          (H : CategoryTheory.EnrichedFunctor V E E') →
                            CategoryTheory.EnrichedFunctor.comp V (CategoryTheory.EnrichedFunctor.comp V F G) H ≅
                              CategoryTheory.EnrichedFunctor.comp V F (CategoryTheory.EnrichedFunctor.comp V G H)
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientiInfSubgroupOfEmbedding_apply_mk : ∀ {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α) (g : ↥H) (i : ι),
  (Subgroup.quotientiInfSubgroupOfEmbedding f H) (↑g) i = ↑g
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_functor_obj_toTwoPointing_toProd : ∀ (X : TwoP), (TwoP.swapEquiv.functor.obj X).toTwoPointing.toProd = (X.toTwoPointing.toProd.2, X.toTwoPointing.toProd.1)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.ae_eq_set_pi : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {I : Set ι}
  {s t : (i : ι) → Set (α i)}, (∀ i ∈ I, s i =ᵐ[μ i] t i) → I.pi s =ᵐ[MeasureTheory.Measure.pi μ] I.pi t
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_braiding_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g) (β_ Y X).inv =
    CategoryTheory.CartesianMonoidalCategory.lift g f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.leibnizPushout_map_app : ∀ {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₃)) [inst_3 : CategoryTheory.Limits.HasPushouts C₃]
  {X Y : CategoryTheory.Arrow C₁} (sq : X ⟶ Y) (f₂ : CategoryTheory.Arrow C₂),
  (F.leibnizPushout.map sq).app f₂ =
    (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F X.hom f₂.hom).mapArrowLeft
      (CategoryTheory.Functor.PushoutObjObj.ofHasPushout F Y.hom f₂.hom) sq
-- Mathlib.Order.WellFoundedSet
Set.Finite.isWF : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.Finite → s.IsWF
-- Mathlib.Tactic.FunProp.Types
/-- General theorem about a function property used for transition and morphism theorems  -/
Mathlib.Meta.FunProp.GeneralTheorem : Type
-- Mathlib.Order.Category.Lat
Lat.ofHom_hom : ∀ {X Y : Lat} (f : X ⟶ Y), Lat.ofHom (Lat.Hom.hom f) = f
-- Mathlib.Order.Interval.Finset.Fin
Fin.card_Ioo : ∀ {n : ℕ} (a b : Fin n), (Finset.Ioo a b).card = ↑b - ↑a - 1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun x => Opposite.op (Z x)}
  (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) (b : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).inv (c.inj b).op = f.proj b
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.closure_eq_of_le : ∀ {M : Type u_1} [inst : Mul M] {s : Set M} {S : Subsemigroup M},
  s ⊆ ↑S → S ≤ Subsemigroup.closure s → Subsemigroup.closure s = S
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.integrable_of_bilin_of_bdd_right : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) {f : α → E} {g : α → F} (C : ℝ),
  MeasureTheory.Integrable f μ →
    MeasureTheory.AEStronglyMeasurable g μ →
      (∀ᵐ (a : α) ∂μ, ‖g a‖ ≤ C) → MeasureTheory.Integrable (fun x => (B (f x)) (g x)) μ
-- Mathlib.Data.Seq.Basic
Stream'.Seq.get?_set_of_terminatedAt : ∀ {α : Type u} (x : α) {s : Stream'.Seq α} {n : ℕ}, s.TerminatedAt n → (s.set n x).get? n = none
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∈ m₂ → Std.DTreeMap.Raw.Const.getD (m₁ \ m₂) k fallback = fallback
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cocycle.toCochainAddMonoidHom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ) (x : CochainComplex.HomComplex.Cocycle K L n),
  (CochainComplex.HomComplex.Cocycle.toCochainAddMonoidHom K L n) x = ↑x
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- If a ring is equivalent to a DVR, it is itself a DVR.  -/
IsDiscreteValuationRing.RingEquivClass.isDiscreteValuationRing : ∀ {A : Type u_2} {B : Type u_3} {E : Type u_4} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : CommRing B]
  [inst_3 : IsDomain B] [IsDiscreteValuationRing A] [inst_5 : EquivLike E A B] [RingEquivClass E A B] (e : E),
  IsDiscreteValuationRing B
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.exists_path_of_stronglyConnectedComponent_eq : ∀ {V : Type u_2} [inst : Quiver V] {a b : V},
  Quiver.StronglyConnectedComponent.mk a = Quiver.StronglyConnectedComponent.mk b →
    Nonempty (Quiver.Path a b) ∧ Nonempty (Quiver.Path b a)
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.limitAddCommGroup : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] →
            AddCommGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (ModuleCat R)))).pt
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.id_tensorHom : ∀ (x : AugmentedSimplexCategory) {y₁ y₂ : AugmentedSimplexCategory} (f : y₁ ⟶ y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id x) f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft x f
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- This is a version of `summable_norm_mul_geometric_of_norm_lt_one` for more general codomains. We
keep the original one due to import restrictions.  -/
summable_norm_mul_geometric_of_norm_lt_one' : ∀ {F : Type u_1} [inst : NormedRing F] [NormOneClass F] [NormMulClass F] {k : ℕ} {r : F},
  ‖r‖ < 1 → ∀ {u : ℕ → F}, (u =O[Filter.atTop] fun n => ↑(n ^ k)) → Summable fun n => ‖u n * r ^ n‖
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- The map applying a vector to Hom-valued Schwartz function as a continuous linear map.  -/
SchwartzMap.evalCLM : (𝕜 : Type u_2) →
  (E : Type u_5) →
    {F : Type u_6} →
      (G : Type u_7) →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                [inst_4 : NormedField 𝕜] →
                  [inst_5 : NormedAddCommGroup G] →
                    [inst_6 : NormedSpace ℝ G] →
                      [inst_7 : NormedSpace 𝕜 G] →
                        [inst_8 : SMulCommClass ℝ 𝕜 G] → F → SchwartzMap E (F →L[ℝ] G) →L[𝕜] SchwartzMap E G
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.getKey!_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {a : α}, m.getKey! a = Std.DHashMap.Internal.Raw₀.getKey! ⟨m, ⋯⟩ a
-- Mathlib.Order.Filter.AtTopBot.Prod
Filter.tendsto_atTop_diagonal : ∀ {α : Type u_3} [inst : Preorder α], Filter.Tendsto (fun a => (a, a)) Filter.atTop Filter.atTop
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.disjointSum.eq_1 : ∀ {α : Type u_1} (M N : Matroid α) (h : Disjoint M.E N.E),
  M.disjointSum N h = ((M.restrictSubtype M.E).sum (N.restrictSubtype N.E)).mapEmbedding (Function.Embedding.sumSet h)
-- Mathlib.NumberTheory.MulChar.Duality
/-- Let `N` be a submonoid of `M` group and let `R` be a ring with enough roots of unity.
Then any `R`-value multiplicative character of `N` can be extended to a multiplicative
character of `M`.
 -/
MulChar.domRestrictHom_surjective : ∀ (M : Type u_1) (R : Type u_2) [inst : CommMonoid M] [inst_1 : CommRing R] [Finite M]
  [HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] (N : Submonoid M), Function.Surjective ⇑(MulChar.domRestrictHom N R)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If two functions are equal in the relevant interval, their interval integrals are also equal.  -/
intervalIntegral.integral_congr : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : ℝ → E} {μ : MeasureTheory.Measure ℝ}
  {a b : ℝ}, Set.EqOn f g (Set.uIcc a b) → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_top : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {c d : C} (f : c ⟶ d), f ∈ ⊤.arrows c d
-- Init.Data.List.Lemmas
List.length_flatMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β},
  (List.flatMap f l).length = (List.map (fun a => (f a).length) l).sum
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.toPreAbstractSimplicialComplex_le_iff : ∀ {ι : Type u_1} {K L : AbstractSimplicialComplex ι},
  K.toPreAbstractSimplicialComplex ≤ L.toPreAbstractSimplicialComplex ↔ K ≤ L
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- Changing coordinates between two elements of the maximal atlas gives rise to an element
of the structure groupoid.  -/
StructureGroupoid.compatible_of_mem_maximalAtlas : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e e' : OpenPartialHomeomorph M H},
  e ∈ StructureGroupoid.maximalAtlas M G → e' ∈ StructureGroupoid.maximalAtlas M G → e.symm.trans e' ∈ G
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanServerCapabilities.mk.injEq : ∀ (moduleHierarchyProvider? : Option Lean.Lsp.ModuleHierarchyOptions) (rpcProvider? : Option Lean.Lsp.RpcOptions)
  (moduleHierarchyProvider?_1 : Option Lean.Lsp.ModuleHierarchyOptions) (rpcProvider?_1 : Option Lean.Lsp.RpcOptions),
  ({ moduleHierarchyProvider? := moduleHierarchyProvider?, rpcProvider? := rpcProvider? } =
      { moduleHierarchyProvider? := moduleHierarchyProvider?_1, rpcProvider? := rpcProvider?_1 }) =
    (moduleHierarchyProvider? = moduleHierarchyProvider?_1 ∧ rpcProvider? = rpcProvider?_1)
-- Mathlib.Order.Cover
covBy_congr_right : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (c ⋖ a ↔ c ⋖ b)
-- Lean.Elab.Tactic.SolveByElim
/-- Wrapper for `solveByElim` that processes a list of `Term`s
that specify the lemmas to use.  -/
Lean.Elab.Tactic.SolveByElim.processSyntax : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } →
  Bool → Bool → List Lean.Term → List Lean.Term → Array Lean.Ident → List Lean.MVarId → Lean.MetaM (List Lean.MVarId)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse_obj_left_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Under.forget c).comp F) G),
  ((CategoryTheory.StructuredArrow.ofCommaSndEquivalenceInverse F G c).obj Y).left.as = PUnit.unit
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_map_subtype_le : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (n : ℕ),
  AddSubgroup.map H.subtype (⊤.lowerCentralSeries n) ≤ ⊤.lowerCentralSeries n
-- Mathlib.Algebra.Order.Interval.Basic
Interval.length_neg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α] (s : Interval α),
  (-s).length = s.length
-- Mathlib.Order.TypeTags
WithBot.recBotCoe.eq_2 : ∀ {α : Type u_1} {C : WithBot α → Sort u_2} (bot : C ⊥) (coe : (a : α) → C ↑a) (a : α),
  WithBot.recBotCoe bot coe (some a) = coe a
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.add_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b : α}, a + b ≠ ⊤ ↔ a ≠ ⊤ ∧ b ≠ ⊤
-- Mathlib.Order.CompleteLattice.Chain
chainClosure_empty : ∀ {α : Type u_1} {r : α → α → Prop}, ChainClosure r ∅
-- Mathlib.Data.Matrix.Basic
/-- `Matrix.diagonal` as a `RingHom`.  -/
Matrix.diagonalRingHom : (n : Type u_3) →
  (α : Type u_11) →
    [inst : NonAssocSemiring α] → [inst_1 : Fintype n] → [inst_2 : DecidableEq n] → (n → α) →+* Matrix n n α