mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
/-- `isProp` is true if the parameter type is always a proposition.  -/
Lean.Meta.ParamInfo.isProp : Lean.Meta.ParamInfo → Bool
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A trivial block is a block.  -/
MulAction.IsTrivialBlock.isBlock : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsTrivialBlock B → MulAction.IsBlock G B
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
addRothNumber_map_add_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCancelCommMonoid α] (s : Finset α) (a : α),
  addRothNumber (Finset.map (addRightEmbedding a) s) = addRothNumber s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.instQuasiCompactGluedTo : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData), AlgebraicGeometry.QuasiCompact I.gluedTo
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleEquiv.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q n : ℤ} (h : p + n = q),
  CochainComplex.HomComplex.Cochain.toSingleEquiv h = CochainComplex.HomComplex.Cochain.toSingleEquiv h
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.ServerInfo.version? : Lean.Lsp.ServerInfo → Option String
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ_cons : ∀ (L : List ℕ) (a : ℕ) {m₁ m₂ : ℕ} (h : m₂ + (a :: L).length = m₁),
  SimplexCategoryGenRel.standardσ (a :: L) h =
    CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ L ⋯)
      (SimplexCategoryGenRel.σ (Fin.ofNat (m₂ + 1) a))
-- Lean.Meta.Eqns
Lean.Meta.GetUnfoldEqnFn : Type
-- Lean.Elab.Match
Lean.Elab.Term.reportMatcherResultErrors : List Lean.Meta.Match.AltLHS → Lean.Meta.Match.MatcherResult → Lean.Elab.TermElabM Unit
-- Mathlib.Probability.Distributions.Geometric
/-- Geometric distribution with success probability `p`.  -/
ProbabilityTheory.geometricPMF : {p : ℝ} → 0 < p → p ≤ 1 → PMF ℕ
-- Mathlib.Data.ENNReal.Inv
ENNReal.coe_inv' : ∀ {r : NNReal} [NeZero r], ↑r⁻¹ = (↑r)⁻¹
-- Mathlib.Order.Interval.Set.Defs
Set.mem_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ico a b ↔ a ≤ x ∧ x < b
-- Init.Data.Array.Lemmas
Array.set.eq_1 : ∀ {α : Type u_1} (xs : Array α) (i : ℕ) (v : α) (h : i < xs.size), xs.set i v h = { toList := xs.toList.set i v }
-- Mathlib.Probability.Distributions.Beta
ProbabilityTheory.isProbabilityMeasureBeta : ∀ {α β : ℝ}, 0 < α → 0 < β → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.betaMeasure α β)
-- Mathlib.Topology.Homotopy.Affine
ContinuousMap.Homotopy.evalAt_affine : ∀ {X : Type u_1} {E : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : IsTopologicalAddGroup E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] (f g : C(X, E)) (x : X),
  (ContinuousMap.Homotopy.affine f g).evalAt x = Path.segment (f x) (g x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_eq_some_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k k' : α},
  t.getKey? k = some k' ↔ ∃ (h : k ∈ t), t.getKey k h = k'
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v)[k] = v
-- Init.Data.SInt.Basic
/-- Converts a 64-bit signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.toInt : Int64 → ℤ
-- Init.Data.Array.Lemmas
Array.allM_toList : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {as : Array α},
  List.allM p as.toList = Array.allM p as
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- The inverse of an open partial homeomorphism `e` is an open map on `e.target`.  -/
OpenPartialHomeomorph.isOpen_image_symm_of_subset_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {t : Set Y}, IsOpen t → t ⊆ e.target → IsOpen (↑e.symm '' t)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Construct a morphism `M ⟶ N` of `Mon C` from a map `f : M ⟶ N` and
compatibilities with the unit and the multiplication.  -/
CategoryTheory.Mon.Hom.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.Mon C} →
        (f : M.X ⟶ N.X) →
          autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one f = CategoryTheory.MonObj.one)
              CategoryTheory.Mon.Hom.mk'._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul f =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f f)
                    CategoryTheory.MonObj.mul)
                CategoryTheory.Mon.Hom.mk'._auto_3 →
              M.Hom N
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.pathStar_apply : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) {u v : U} (p : Quiver.Path u v),
  φ.pathStar u (Quiver.PathStar.mk p) = Quiver.PathStar.mk (φ.mapPath p)
-- Mathlib.CategoryTheory.Yoneda
/-- The curried version of yoneda lemma when `C` is small.  -/
CategoryTheory.curriedYonedaLemma' : {C : Type u₁} →
  [inst : CategoryTheory.SmallCategory C] →
    CategoryTheory.yoneda.comp
        ((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor Cᵒᵖ (Type u₁))ᵒᵖ (Type u₁)).obj
          CategoryTheory.yoneda.op) ≅
      CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ (Type u₁))
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.foldMatchingM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} →
    {β : Type u_4} →
      {σ : Type u_1} →
        [Monad m] → (cmp : α → α → Ordering) → Lean.PrefixTreeNode α β cmp → List α → σ → (β → σ → m σ) → m σ
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.hoFunctor.unitHomEquiv_eq : ∀ (X : SSet) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet ⟶ X),
  (SSet.hoFunctor.unitHomEquiv X) x =
    (CategoryTheory.Functor.LaxMonoidal.ε SSet.hoFunctor).toFunctor.comp (SSet.hoFunctor.map x).toFunctor
-- Mathlib.Algebra.Algebra.Defs
/-- Creating an algebra from a morphism to a commutative semiring.
See note [reducible non-instances].

*Warning:* In general this should not be used if `S` already has a `SMul R S`
instance, since this creates another `SMul R S` instance from the supplied `RingHom` and
this will likely create a diamond.  -/
RingHom.toAlgebra : {R : Type u_1} → {S : Type u_2} → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → (R →+* S) → Algebra R S
-- Mathlib.Algebra.Algebra.Tower
AlgEquiv.extendScalarsOfSurjective_symm : ∀ {R : Type u} {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (h : Function.Surjective ⇑(algebraMap R S)) (f : A ≃ₐ[R] B),
  ((AlgEquiv.extendScalarsOfSurjective h) f).symm = (AlgEquiv.extendScalarsOfSurjective h) f.symm
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.Stained.name.inj : ∀ {a a_1 : Lean.Name}, Mathlib.Linter.Flexible.Stained.name✝ a = Mathlib.Linter.Flexible.Stained.name✝ a_1 → a = a_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {km : α}, t.maxKey? = some km → t.getKey! km = km
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.CokernelCofork.IsColimit.isIso_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (hc : CategoryTheory.Limits.IsColimit c),
  f = 0 → CategoryTheory.IsIso (CategoryTheory.Limits.Cofork.π c)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSlice.instToIterator : {α : Type u_1} →
  {β : Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RioSliceData α β)) Id
        (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxoIterator α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
          pure (b.fst, b.snd))
        (α × β)
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.instUnitizationRing : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] → [IsScalarTower 𝕜 A A] → [SMulCommClass 𝕜 A A] → Ring (WithLp 1 (Unitization 𝕜 A))
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- **Alias** of `Submodule.toLinearMap_orthogonalProjectionOnto_eq_projectionOnto`. -/
Submodule.toLinearMap_orthogonalProjection_eq_linearProjOfIsCompl : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection], ↑K.orthogonalProjectionOnto = K.projectionOnto Kᗮ ⋯
-- Mathlib.Logic.Equiv.Sum
/-- An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. Compare
with `Equiv.sumSigmaDistrib` which is indexed by sums.  -/
Equiv.sigmaSumDistrib : {ι : Type u_11} → (α : ι → Type u_9) → (β : ι → Type u_10) → (i : ι) × (α i ⊕ β i) ≃ (i : ι) × α i ⊕ (i : ι) × β i
-- Mathlib.CategoryTheory.GuitartExact.Basic
CategoryTheory.TwoSquare.equivalenceJ_unitIso : ∀ {C₁ : Type u₁} {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₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) {X₂ : C₂}
  {X₃ : C₃} (g : R.obj X₂ ⟶ B.obj X₃),
  (w.equivalenceJ g).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (w.StructuredArrowRightwards g))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {h' : a ∈ m.erase k}, (m.erase k)[a] = m[a]
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.insert : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} {a : α} [inst : DecidableEq α],
  G.IsNClique n s → (∀ b ∈ s, G.Adj a b) → G.IsNClique (n + 1) (insert a s)
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.instEpiTopCatBaseCommRingCatFromGlued : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover), CategoryTheory.Epi (AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰).base
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
QuotientAddGroup.borelSpace : ∀ {G : Type u_3} [inst : TopologicalSpace G] [PolishSpace G] [inst_2 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {N : AddSubgroup G} [N.Normal] [IsClosed ↑N], BorelSpace (G ⧸ N)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.isDecompOn' : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (self : Equidecomp X G),
  ∃ S, Equidecomp.IsDecompOn (↑self.toPartialEquiv) self.source S
-- Mathlib.RingTheory.Flat.Localization
Module.flat_iff_of_isLocalization : ∀ {R : Type u_1} (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (p : Submonoid R) [IsLocalization p S] (M : Type u_3) [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : Module S M] [IsScalarTower R S M], Module.Flat S M ↔ Module.Flat R M
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_injective : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι),
  Function.Injective (RestrictedProduct.single A i)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.decidableMemKer.eq_1 : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] [inst_2 : DecidableEq M] (f : G →* M) (x : G),
  f.decidableMemKer x = decidable_of_iff (f x = 1) ⋯
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- A continuous function on a compact space has automatically compact support. This is not an
instance to avoid type class loops.  -/
CompactlySupportedContinuousMapClass.of_compactSpace : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : TopologicalSpace β]
  (G : Type u_5) [inst_3 : FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α],
  CompactlySupportedContinuousMapClass G α β
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- Swapping the `o`-th coordinate to `true`.  -/
Profinite.NobelingProof.SwapTrue : {I : Type u} → [inst : LinearOrder I] → [WellFoundedLT I] → Ordinal.{u} → (I → Bool) → I → Bool
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adj.unit_naturality_assoc : ∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₁.obj} (f : X ⟶ Y) {Z : ↑C₁.obj}
  (h : α.r.toFunctor.obj (α.l.toFunctor.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.adj.unit.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp (α.r.toFunctor.map (α.l.toFunctor.map f)) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (α.adj.unit.toNatTrans.app Y) h)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.reflQuiver_Hom : ∀ (S : SSet.Truncated 2)
  (x₀ x₁ : S.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })),
  (x₀ ⟶ x₁) = SSet.Truncated.Edge x₀ x₁
-- Mathlib.Data.Fintype.Defs
Fintype.decidableLeftInverseFintype : {α : Type u_1} →
  {β : Type u_2} → [DecidableEq β] → [Fintype β] → (f : α → β) → (g : β → α) → Decidable (Function.LeftInverse f g)
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_of_fintype : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} [inst_1 : Fintype ↑s],
  s.einfsep = s.offDiag.toFinset.inf (Function.uncurry edist)
-- Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian
CategoryTheory.Idempotents.DoldKan.Γ_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.IsIdempotentComplete C] [inst_3 : CategoryTheory.Limits.HasFiniteCoproducts C]
  (X : ChainComplex C ℕ) {X_1 Y : SimplexCategoryᵒᵖ} (θ : X_1 ⟶ Y),
  (CategoryTheory.Idempotents.DoldKan.Γ.obj X).map θ = AlgebraicTopology.DoldKan.Γ₀.Obj.map X θ
-- Mathlib.Analysis.Normed.Operator.NormedSpace
Submodule.norm_subtypeL : ∀ {𝕜 : Type u_1} {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (K : Submodule 𝕜 E) [Nontrivial ↥K], ‖K.subtypeL‖ = 1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getKeyₘ_eq_getKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β} (h : Std.Internal.List.containsKey k t.toListModel = true)
  {h' : (t.getKey?ₘ k).isSome = true}, t.Ordered → t.getKeyₘ k h' = Std.Internal.List.getKey k t.toListModel h
-- Mathlib.Data.Fintype.BigOperators
Fintype.sum_prod_type_right : ∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : AddCommMonoid γ]
  (f : α₁ × α₂ → γ), ∑ x, f x = ∑ y, ∑ x, f (x, y)
-- Mathlib.Topology.Basic
Filter.limUnder.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_3} [inst_1 : Nonempty X] (f : Filter α) (g : α → X),
  f.limUnder g = (Filter.map g f).lim
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.unescapeStr : String → String
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_null : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {n : ℕ} {x : A},
  x ∉ I → self.dpow n x = 0
-- Mathlib.Order.Defs.PartialOrder
instTransLTLE : {α : Type u_1} → [inst : Preorder α] → Trans LT.lt LE.le LT.lt
-- Init.Data.Rat.Basic
/-- Rational numbers, implemented as a pair of integers `num / den` such that the
denominator is positive and the numerator and denominator are coprime.
 -/
Rat : Type
-- Lean.Setup
/-- Abstract structure of an `import` statement.  -/
Lean.Import : Type
-- Mathlib.Data.Sum.Order
Sum.Lex.toLexRelIsoLT_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β], ⇑Sum.Lex.toLexRelIsoLT = ⇑toLex
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.listProd : ∀ {α : Type u_1} {R : Type u_13} {𝕜 : Type u_15} [inst : SeminormedRing R] [inst_1 : NormedDivisionRing 𝕜]
  {l : Filter α} {ι : Type u_17} {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜},
  (∀ i ∈ L, f i =O[l] g i) →
    (∃ i ∈ L, f i =o[l] g i) →
      (fun x => (List.map (fun x_1 => f x_1 x) L).prod) =o[l] fun x => (List.map (fun x_1 => g x_1 x) L).prod
-- Mathlib.Logic.Embedding.Basic
/-- A subtype `{x // p x ∨ q x}` over a disjunction of `p q : α → Prop` can be injectively split
into a sum of subtypes `{x // p x} ⊕ {x // q x}` such that `¬ p x` is sent to the right.  -/
subtypeOrLeftEmbedding : {α : Type u_1} → (p q : α → Prop) → [DecidablePred p] → { x // p x ∨ q x } ↪ { x // p x } ⊕ { x // q x }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_inter_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false →
        Std.DTreeMap.Internal.Impl.Const.get! (m₁.inter m₂ ⋯) k = default
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftKanExtensionUnique_hom : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (F'' : CategoryTheory.Functor D H) (α' : F ⟶ L.comp F'')
  [inst_4 : F''.IsLeftKanExtension α'], (F'.leftKanExtensionUnique α F'' α').hom = F'.descOfIsLeftKanExtension α F'' α'
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.uniformContinuous_eval_const : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] (x : (i : ι) → E i), UniformContinuous fun f => f x
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.volumeIoiPow.eq_1 : ∀ (n : ℕ),
  MeasureTheory.Measure.volumeIoiPow n =
    (MeasureTheory.Measure.comap Subtype.val MeasureTheory.volume).withDensity fun r => ENNReal.ofReal (↑r ^ n)
-- Mathlib.Algebra.Order.Ring.Abs
abs_neg_one_pow : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] (n : ℕ), |(-1) ^ n| = 1
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.isValuedIn_iff_mem_range : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {S : Type u_6}
  [inst_5 : CommRing S] [inst_6 : Algebra S R],
  P.IsValuedIn S ↔ ∀ (i j : ι), P.pairing i j ∈ Set.range ⇑(algebraMap S R)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mul_nonempty : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α}, (s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Mathlib.Data.ENat.Lattice
ENat.iInf_add_iInf : ∀ {ι : Sort u_2} {f g : ι → ℕ∞}, (∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j) → iInf f + iInf g = ⨅ a, f a + g a
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
/-- Technical lemma to control the addition of functions in `L^p` even for `p < 1`: Given `δ > 0`,
there exists `η` such that two functions bounded by `η` in `L^p` have a sum bounded by `δ`. One
could take `η = δ / 2` for `p ≥ 1`, but the point of the lemma is that it works also for `p < 1`.
 -/
MeasureTheory.exists_Lp_half : ∀ {α : Type u_1} (ε : Type u_3) {m : MeasurableSpace α} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddMonoid ε]
  (μ : MeasureTheory.Measure α) (p : ENNReal) {δ : ENNReal},
  δ ≠ 0 →
    ∃ η,
      0 < η ∧
        ∀ (f g : α → ε),
          MeasureTheory.AEStronglyMeasurable f μ →
            MeasureTheory.AEStronglyMeasurable g μ →
              MeasureTheory.eLpNorm f p μ ≤ η → MeasureTheory.eLpNorm g p μ ≤ η → MeasureTheory.eLpNorm (f + g) p μ < δ
-- Mathlib.Algebra.Homology.Factorizations.CM5a
CochainComplex.Plus.modelCategoryQuillen.cm5a_cof : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [CategoryTheory.EnoughInjectives C] (n : ℤ) [K.IsStrictlyGE n]
  [L.IsStrictlyGE n] [CategoryTheory.Mono f],
  ∃ K',
    ∃ (_ : K'.IsStrictlyGE n),
      ∃ ι π,
        CategoryTheory.Mono ι ∧
          QuasiIso ι ∧ CochainComplex.degreewiseEpiWithInjectiveKernel π ∧ CategoryTheory.CategoryStruct.comp ι π = f
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.lcm_eq_mul : ∀ {m n : ℕ}, m.Coprime n → m.lcm n = m * n
-- Mathlib.NumberTheory.Padics.Complex
/-- The norm on `PadicAlgCl p` is the spectral norm induced by the `p`-adic norm on `ℚ_[p]`.  -/
PadicAlgCl.spectralNorm_eq : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p), spectralNorm ℚ_[p] (PadicAlgCl p) x = ‖x‖
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.  -/
VectorFourier.integral_fourierIntegral_smul_eq_flip : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {F : Type u_5}
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace ℂ F] [inst_8 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜]
  [inst_10 : TopologicalSpace V] [BorelSpace V] [inst_12 : TopologicalSpace W] [inst_13 : MeasurableSpace W]
  [BorelSpace W] {e : AddChar 𝕜 Circle} {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜}
  {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν]
  [SecondCountableTopologyEither W V] [CompleteSpace F] {f : V → ℂ} {g : W → F},
  Continuous ⇑e →
    (Continuous fun p => (L p.1) p.2) →
      MeasureTheory.Integrable f μ →
        MeasureTheory.Integrable g ν →
          ∫ (ξ : W), VectorFourier.fourierIntegral e μ L f ξ • g ξ ∂ν =
            ∫ (x : V), f x • VectorFourier.fourierIntegral e ν L.flip g x ∂μ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toList_rio_eq : ∀ {n i : ℕ}, ((*...n).toList[i]?.isNone = true) = (n ≤ i)
-- Init.Data.Int.Gcd
Int.gcd_ne_zero_left : ∀ {a b : ℤ}, a ≠ 0 → a.gcd b ≠ 0
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- `μ` has finite spanning sets in `C` if there is a countable sequence of sets in `C` that have
finite measures. This structure is a type, which is useful if we want to record extra properties
about the sets, such as that they are monotone.
`SigmaFinite` is defined in terms of this: `μ` is σ-finite if there exists a sequence of
finite spanning sets in the collection of all measurable sets.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn : {α : Type u_1} → {m0 : MeasurableSpace α} → MeasureTheory.Measure α → Set (Set α) → Type u_1