mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `fallback` if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryGTD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → α × β → α × β
-- Lean.Parser.Command
Lean.Parser.Command.openScoped : Lean.Parser.Parser
-- Mathlib.NumberTheory.ModularForms.Derivative
/-- The derivative operator `D` preserves MDifferentiability.
If `F : ℍ → ℂ` is MDifferentiable, then `D F` is also MDifferentiable.
 -/
Derivative.normalizedDerivOfComplex_mdifferentiable : ∀ {F : UpperHalfPlane → ℂ}, MDiff F → MDiff (Derivative.normalizedDerivOfComplex F)
-- Mathlib.Algebra.Order.Field.Canonical
/-- Construct a `LinearOrderedCommGroupWithZero` from a canonically linear ordered semifield.  -/
CanonicallyOrderedAdd.toLinearOrderedCommGroupWithZero : {α : Type u_1} →
  [inst : Semifield α] → [inst_1 : LinearOrder α] → [CanonicallyOrderedAdd α] → LinearOrderedCommGroupWithZero α
-- Mathlib.Logic.Equiv.Defs
Equiv.subsingleton : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) [Subsingleton β], Subsingleton α
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.faceOppositeCentroid_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (S : AffineSubspace k P)
  (hS : affineSpan k (Set.range s.points) ≤ S) {i : Fin (n + 1)},
  ↑((s.restrict S hS).faceOppositeCentroid i) = s.faceOppositeCentroid i
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
measurableSet_Ioc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} [ClosedIicTopology α], MeasurableSet (Set.Ioc a b)
-- Mathlib.Topology.Order.NhdsSet
Ioi_mem_nhdsSet_Ici_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b : α},
  Set.Ioi a ∈ nhdsSet (Set.Ici b) ↔ a < b
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.id_hom_c_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C)
  (U : (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)ᵒᵖ),
  (CategoryTheory.CategoryStruct.id X).hom.c.app U = CategoryTheory.CategoryStruct.id (X.presheaf.obj U)
-- Lean.Elab.Util
Lean.Elab.MonadMacroAdapter.toMonadQuotation : {m : Type → Type} → [self : Lean.Elab.MonadMacroAdapter m] → Lean.MonadQuotation m
-- Init.Data.Nat.Basic
Nat.not_lt_eq : ∀ (a b : ℕ), (¬a < b) = (b ≤ a)
-- Mathlib.MeasureTheory.Measure.MeasuredSets
/-- The subtype of all measurable sets. We denote it as `MeasuredSets μ`, with an explicit but
unused parameter `μ`, to be able to define a distance on it given by `edist s t = μ (s ∆ t)`  -/
MeasureTheory.MeasuredSets : {α : Type u_1} → [mα : MeasurableSpace α] → MeasureTheory.Measure α → Type u_1
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), (-p).natDegree = p.natDegree
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
ContinuousLinearMap.integral_apply : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝕜 : Type u_6}
  [inst_1 : RCLike 𝕜] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E]
  {H : Type u_8} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {φ : X → H →L[𝕜] E},
  MeasureTheory.Integrable φ μ → ∀ (v : H), (∫ (x : X), φ x ∂μ) v = ∫ (x : X), (φ x) v ∂μ
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.LebesgueDecomposition.iSup_mem_measurableLE : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (f : ℕ → α → ENNReal),
  (∀ (n : ℕ), f n ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν) →
    ∀ (n : ℕ), (fun x => ⨆ k, ⨆ (_ : k ≤ n), f k x) ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν
-- Init.Data.Option.Lemmas
Option.pmap_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (o : Option α) (f : α → β) {p : β → Prop} (g : (b : β) → p b → γ)
  (H : ∀ (a : β), Option.map f o = some a → p a),
  Option.pmap g (Option.map f o) H = Option.pmap (fun a h => g (f a) h) o ⋯
-- Mathlib.Data.Fin.SuccPred
finCongr_symm : ∀ {n m : ℕ} (h : m = n), (finCongr h).symm = finCongr ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).size = if t.contains k = true then t.size - 1 else t.size
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.of_discreteTopology : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X)
  [DiscreteTopology E] [DiscreteTopology X], IsCoveringMap f
-- Mathlib.CategoryTheory.Galois.Basic
/-- The evaluation map on automorphisms is injective for connected objects.  -/
CategoryTheory.PreGaloisCategory.evaluation_aut_injective_of_isConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A : C)
  [CategoryTheory.PreGaloisCategory.IsConnected A] (a : (F.obj A).obj),
  Function.Injective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.hom)) a
-- Mathlib.RingTheory.Congruence.Hom
/-- The diagram described by the universal property for quotients of rings, when
the ring congruence relation is the kernel of the homomorphism, commutes.  -/
RingCon.kerLift_mk : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {f : M →+* P} (x : M),
  (RingCon.kerLift f) ↑x = f x
-- Mathlib.Algebra.Order.Module.Defs
/-- **Alias** of `lt_of_smul_lt_smul_right`. -/
lt_of_smul_lt_smul_of_nonneg_right : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero β] [SMulPosReflectLT α β], a₁ • b < a₂ • b → 0 ≤ b → a₁ < a₂
-- Mathlib.Data.NNRat.Defs
NNRat.coe_natCast : ∀ (n : ℕ), ↑↑n = ↑n
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.mem_pi : ∀ {η : Type u_7} {f : η → Type u_8} [inst : (i : η) → Group (f i)] (I : Set η) {H : (i : η) → Subgroup (f i)}
  {p : (i : η) → f i}, p ∈ Subgroup.pi I H ↔ ∀ i ∈ I, p i ∈ H i
-- Init.Data.Option.Lemmas
Option.isSome_join : ∀ {α : Type u_1} {x : Option (Option α)}, x.join.isSome = Option.any Option.isSome x
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.instOrderBotOfIsDomain : {R : Type u} → [inst : CommSemiring R] → [IsDomain R] → OrderBot (PrimeSpectrum R)
-- Mathlib.Algebra.Ring.Parity
Nat.even_div : ∀ {m n : ℕ}, Even (m / n) ↔ m % (2 * n) / n = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filterMap!_le_size : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  {f : (a : α) → β a → Option (γ a)}, t.WF → (Std.DTreeMap.Internal.Impl.filterMap! f t).size ≤ t.size
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.map_map_assoc_symm : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9}
  {T : Type u_10} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P]
  [inst_4 : AddCommMonoid Q] [inst_5 : AddCommMonoid S] [inst_6 : AddCommMonoid T] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R Q] [inst_10 : Module R S] [inst_11 : Module R T] [inst_12 : Module R P]
  (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T) (x : TensorProduct R M (TensorProduct R N P)),
  (TensorProduct.map (TensorProduct.map f g) h) ((TensorProduct.assoc R M N P).symm x) =
    (TensorProduct.assoc R Q S T).symm ((TensorProduct.map f (TensorProduct.map g h)) x)
-- Mathlib.Algebra.GroupWithZero.Action.ConjAct
ConjAct.smulCommClass₀ : ∀ {α : Type u_1} {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : SMul α G₀] [SMulCommClass α G₀ G₀]
  [IsScalarTower α G₀ G₀], SMulCommClass α (ConjAct G₀) G₀
-- Mathlib.Probability.Independence.InfinitePi
/-- Consider `((Xᵢⱼ)ⱼ)ᵢ` a family of families of random variables.
Assume that for any `i`, the random variables `(Xᵢⱼ)ⱼ` are independent.
Assume furthermore that the random variables `((Xᵢⱼ)ⱼ)ᵢ` are independent.
Then the random variables `(Xᵢⱼ)` indexed by pairs `(i, j)` are independent.

This is a non-dependent version of `iIndepFun_uncurry`.  -/
ProbabilityTheory.iIndepFun_uncurry' : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {κ : Type u_4}
  {𝓧 : ι → κ → Type u_5} {m𝓧 : (i : ι) → (j : κ) → MeasurableSpace (𝓧 i j)} {X : (i : ι) → (j : κ) → Ω → 𝓧 i j},
  (∀ (i : ι) (j : κ), Measurable (X i j)) →
    ProbabilityTheory.iIndepFun (fun i ω x => X i x ω) P →
      (∀ (i : ι), ProbabilityTheory.iIndepFun (X i) P) → ProbabilityTheory.iIndepFun (fun p ω => X p.1 p.2 ω) P
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- A concrete version of the multiequalizer, to be used below.  -/
CategoryTheory.Meq : {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)] →
                [CategoryTheory.ConcreteCategory D FD] →
                  {X : C} → CategoryTheory.Functor Cᵒᵖ D → J.Cover X → Type (max 0 (max t u) v)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.forCodeM : {m : Type → Type u_1} →
  {pu : Lean.Compiler.LCNF.Purity} →
    [Monad m] → (Lean.Compiler.LCNF.Code pu → m Unit) → Lean.Compiler.LCNF.DeclValue pu → m Unit
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ext : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f g : α →ᵈ β},
  (∀ (x : α), f x = g x) → f = g
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp_toGerm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α →ₘ[μ] β),
  (MeasureTheory.AEEqFun.comp g hg f).toGerm = Filter.Germ.map g f.toGerm
-- Mathlib.Topology.Algebra.Module.PerfectPairing
LinearMap.IsContPerfPair.bijective_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {inst : CommRing R} {inst_1 : TopologicalSpace R}
  {inst_2 : AddCommGroup M} {inst_3 : Module R M} {inst_4 : TopologicalSpace M} {inst_5 : AddCommGroup N}
  {inst_6 : Module R N} {inst_7 : TopologicalSpace N} (p : M →ₗ[R] N →ₗ[R] R) [self : p.IsContPerfPair],
  Function.Bijective fun y => { toLinearMap := p.flip y, cont := ⋯ }
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.fromSaturateOfHasPullbacks_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] {i j : E.saturate.I₀} (k : E.saturate.I₁ i j),
  E.fromSaturateOfHasPullbacks.h₁ k = CategoryTheory.Limits.pullback.lift k.fst k.snd ⋯
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize.eq_1 : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (x : V), NormedSpace.normalize x = ‖x‖⁻¹ • x
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.Pair.mk.injEq : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (head : M i) (tail : Monoid.CoprodI.Word M)
  (fstIdx_ne : tail.fstIdx ≠ some i) (head_1 : M i) (tail_1 : Monoid.CoprodI.Word M)
  (fstIdx_ne_1 : tail_1.fstIdx ≠ some i),
  ({ head := head, tail := tail, fstIdx_ne := fstIdx_ne } =
      { head := head_1, tail := tail_1, fstIdx_ne := fstIdx_ne_1 }) =
    (head = head_1 ∧ tail = tail_1)
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.nnnorm_self_mul_star : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [CStarRing E] {x : E}, ‖x * star x‖₊ = ‖x‖₊ * ‖x‖₊
-- Mathlib.MeasureTheory.Covering.OneDim
Real.Icc_mem_vitaliFamily_at_right : ∀ {x y : ℝ}, x < y → Set.Icc x y ∈ (IsUnifLocDoublingMeasure.vitaliFamily MeasureTheory.volume 1).setsAt x
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prod_le_top_prod : ∀ {X Y : SSet} (A : X.Subcomplex) (B : Y.Subcomplex), A.prod B ≤ ⊤.prod B
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.ForgetEnrichment.homOf_comp : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] {X Y Z : C}
  (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ X ⟶[W] Y)
  (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ Y ⟶[W] Z),
  CategoryTheory.ForgetEnrichment.homOf W
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit W)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
          (CategoryTheory.eComp W X Y Z))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ForgetEnrichment.homOf W f)
      (CategoryTheory.ForgetEnrichment.homOf W g)
-- Mathlib.SetTheory.Cardinal.UnivLE
/-- Together with transitivity, this shows `UnivLE` is a total preorder.  -/
univLE_total : UnivLE.{u, v} ∨ UnivLE.{v, u}
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mem_zeroLocus : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ProjectiveSpectrum 𝒜) (s : Set A),
  x ∈ ProjectiveSpectrum.zeroLocus 𝒜 s ↔ s ⊆ ↑x.asHomogeneousIdeal
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.insertListIfNew.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (k : α) (v : β k)
  (l_1 : List ((a : α) × β a)),
  Std.Internal.List.insertListIfNew l (⟨k, v⟩ :: l_1) =
    Std.Internal.List.insertListIfNew (Std.Internal.List.insertEntryIfNew k v l) l_1
-- Aesop.Util.Basic
Aesop.forEachExprInLCtx : {ω : Type} →
  {m : Type → Type} →
    [STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] →
          [MonadControlT Lean.MetaM m] → [MonadLiftT Lean.MetaM m] → Lean.MVarId → (Lean.Expr → m Unit) → m Unit
-- Mathlib.Tactic.Order.Graph.Basic
Mathlib.Tactic.Order.instToStringEdge : ToString Mathlib.Tactic.Order.Edge
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquivClass.mk : ∀ {F : Type u_1} {A : outParam (Type u_2)} {B : outParam (Type u_3)} [inst : Add A] [inst_1 : Mul A] [inst_2 : Star A]
  [inst_3 : Add B] [inst_4 : Mul B] [inst_5 : Star B] [inst_6 : EquivLike F A B]
  [toRingEquivClass : RingEquivClass F A B], (∀ (f : F) (a : A), f (star a) = star (f a)) → StarRingEquivClass F A B
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_limit : ∀ {a b : Ordinal.{u_1}}, a ≠ 0 → Order.IsSuccLimit b → a ^ b = ⨆ x, a ^ ↑x
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom₂.ext : ∀ {B : Type u_1} {C : Type u_2} {inst : CategoryTheory.Bicategory C} {F : B → C}
  {X Y : CategoryTheory.Bicategory.InducedBicategory C F} {f g : X ⟶ Y}
  {x y : CategoryTheory.Bicategory.InducedBicategory.Hom₂ f g}, x.hom = y.hom → x = y
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_neg : ∀ (x : ℂ), Complex.tan (-x) = -Complex.tan x
-- Lean.Meta.Tactic.Grind.Types
/-- Returns a proof that `a = Bool.true`.
It assumes `a` and `Bool.true` are in the same equivalence class.
 -/
Lean.Meta.Grind.mkEqBoolTrueProof : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Data.Finset.NAry
/-- If each partial application of `f` is injective, and images of `t` under those partial
applications are disjoint (but not necessarily distinct!), then the size of `s` divides the size of
`Finset.image₂ f s t`.  -/
Finset.card_dvd_card_image₂_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  (∀ b ∈ t, Function.Injective fun a => f a b) →
    ((fun b => Finset.image (fun a => f a b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (Finset.image₂ f s t).card
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- Let `M` be an `R`-module, and `f` an `R`-linear endomorphism of `M`,
and let `μ : R` and `k : ℕ∞` be given.
Then `x : M` satisfies `HasUnifEigenvector f μ k x` if
`x ∈ f.genEigenspace μ k` and `x ≠ 0`.

For `k = 1`, this means that `x` is an eigenvector of `f` with eigenvalue `μ`.  -/
Module.End.HasUnifEigenvector : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → ℕ∞ → M → Prop
-- Mathlib.Order.PropInstances
Prop.linearOrder : LinearOrder Prop
-- Mathlib.Data.W.Constructions
/-- `WType.Listα` is equivalent to `γ` with an extra point.
This is useful when considering the associated polynomial endofunctor
 -/
WType.ListαEquivPUnitSum : (γ : Type u) → WType.Listα γ ≃ PUnit.{v + 1} ⊕ γ
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.tsupport_subset_symm_image_closedBall : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) [inst_5 : FiniteDimensional ℝ E] [T2Space M],
  tsupport ↑f ⊆ ↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I)
-- Mathlib.Algebra.Field.Defs
/-- `a ^ -(n + 1) = (a ^ (n + 1))⁻¹`  -/
Semifield.zpow_neg' : ∀ {K : Type u_2} [self : Semifield K] (n : ℕ) (a : K), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β},
  (k, v) ∈ Std.DHashMap.Const.toArray m ↔ m.getKey? k = some k ∧ Std.DHashMap.Const.get? m k = some v
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.DHashMap.Const.get! (Std.DHashMap.Const.insertMany m l) k = Std.DHashMap.Const.get! m k
-- Mathlib.Algebra.Group.End
Equiv.Perm.equivUnitsEnd_symm_apply_apply : ∀ {α : Type u_4} (u : (Function.End α)ˣ), ⇑(Equiv.Perm.equivUnitsEnd.symm u) = ↑u
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.symm_reindexAlgEquiv : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n), (Matrix.reindexAlgEquiv R A e).symm = Matrix.reindexAlgEquiv R A e.symm
-- Init.Data.Fin.Lemmas
Fin.addNat_subNat : ∀ {n m : ℕ} {i : Fin (n + m)} (h : m ≤ ↑i), (Fin.subNat m i h).addNat m = i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The natural inclusion of the `n`-cycles `Zₙ(G, A)` into the `n`-chains `Cₙ(G, A).`  -/
groupHomology.iCycles : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (n : ℕ) → groupHomology.cycles A n ⟶ (groupHomology.inhomogeneousChains A).X n
-- Init.SimpLemmas
Lean.false_arrow : ∀ (p : Prop), Lean.Arrow False p = True
-- Mathlib.Analysis.Complex.Exponential
Complex.exp_sum : ∀ {α : Type u_1} (s : Finset α) (f : α → ℂ), Complex.exp (∑ x ∈ s, f x) = ∏ x ∈ s, Complex.exp (f x)
-- Init.Data.Dyadic.Basic
Dyadic.roundDown_eq_self_of_le : ∀ {x : Dyadic} {prec : ℤ}, x.precision ≤ some prec → x.roundDown prec = x
-- Mathlib.Algebra.Torsor.Defs
/-- Scalar multiplying the result of dividing another point produces that point.  -/
sdiv_smul : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p₁ p₂ : P), (p₁ /ₛ p₂) • p₂ = p₁
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.FullSubcategory.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C}
  {x y : P.FullSubcategory}, x.obj = y.obj → x = y
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Given a coalgebra morphism whose carrier part is an isomorphism, we get a coalgebra isomorphism.
 -/
CategoryTheory.Comonad.coalgebra_iso_of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) {A B : G.Coalgebra}
  (f : A ⟶ B) [CategoryTheory.IsIso f.f], CategoryTheory.IsIso f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.MemP.eq_1 : ∀ {α : Type u_1} (cut : α → Ordering) (t : RBTree.RBNode α),
  RBTree.RBNode.MemP cut t = RBTree.RBNode.Any (fun x => cut x = Ordering.eq) t
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.LetRecClosure.mk.inj : ∀ {ref : Lean.Syntax} {localDecls : Array Lean.LocalDecl} {closed : Lean.Expr} {toLift : Lean.Elab.Term.LetRecToLift}
  {ref_1 : Lean.Syntax} {localDecls_1 : Array Lean.LocalDecl} {closed_1 : Lean.Expr}
  {toLift_1 : Lean.Elab.Term.LetRecToLift},
  { ref := ref, localDecls := localDecls, closed := closed, toLift := toLift } =
      { ref := ref_1, localDecls := localDecls_1, closed := closed_1, toLift := toLift_1 } →
    ref = ref_1 ∧ localDecls = localDecls_1 ∧ closed = closed_1 ∧ toLift = toLift_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.le_of_add_le_add_right : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [inst_1 : LE α] [AddRightReflectLE α], z ≠ ⊤ → x + z ≤ y + z → x ≤ y
-- Batteries.Data.String.Lemmas
String.splitAux_of_valid : ∀ (p : Char → Bool) (l m r : List Char) (acc : List String),
  (String.ofList (l ++ m ++ r)).splitAux p { byteIdx := String.utf8Len l }
      { byteIdx := String.utf8Len l + String.utf8Len m } acc =
    acc.reverse ++ List.map String.ofList (List.splitOnPPrepend p r m.reverse)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.brecOn_2.eq : ∀ {motive_1 : Lean.Lsp.Ipc.CallHierarchy → Sort u} {motive_2 : Array Lean.Lsp.Ipc.CallHierarchy → Sort u}
  {motive_3 : List Lean.Lsp.Ipc.CallHierarchy → Sort u} (t : List Lean.Lsp.Ipc.CallHierarchy)
  (F_1 : (t : Lean.Lsp.Ipc.CallHierarchy) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_2 t → motive_3 t),
  Lean.Lsp.Ipc.CallHierarchy.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.Lsp.Ipc.CallHierarchy.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.neg_coroot_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [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) (i : ι),
  -P.coroot i ∈ Set.range ⇑P.coroot
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.hom_ext_iff : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] {f g : AddMonoid.Coprod M N →+ P},
  f = g ↔
    f.comp AddMonoid.Coprod.inl = g.comp AddMonoid.Coprod.inl ∧
      f.comp AddMonoid.Coprod.inr = g.comp AddMonoid.Coprod.inr
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `IsPrimePow n`, `n ≠ 2` and `Irreducible (cyclotomic n K)` (in particular for
`K = ℚ`), then the norm of `ζ - 1` is `n.minFac`.  -/
IsPrimitiveRoot.sub_one_norm_isPrimePow : ∀ {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L],
  IsPrimitiveRoot ζ n →
    IsPrimePow n →
      ∀ [IsCyclotomicExtension {n} K L],
        Irreducible (Polynomial.cyclotomic n K) → n ≠ 2 → (Algebra.norm K) (ζ - 1) = ↑n.minFac
-- Mathlib.Data.Finsupp.Interval
Finsupp.mem_rangeIcc_apply_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] {f g : ι →₀ α} {i : ι} {a : α}, a ∈ (f.rangeIcc g) i ↔ f i ≤ a ∧ a ≤ g i