mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lsingle_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι) (x : M i), (DFinsupp.lsingle i) x = fun₀ | i => x
-- Mathlib.Logic.Equiv.Basic
/-- Transporting dependent functions through an equivalence of the base,
expressed as a "simplification".
 -/
Equiv.piCongrLeft : {α : Sort u_1} → {β : Sort u_4} → (P : β → Sort w) → (e : α ≃ β) → ((a : α) → P (e a)) ≃ ((b : β) → P b)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.inspectOutParams : Lean.Expr → Lean.Expr → Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- `CategoryStruct` on `B ⥤ᵒᵖᴸ C` where the (1-)morphisms are given by oplax
transformations.  -/
CategoryTheory.Oplax.OplaxTrans.categoryStruct : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.CategoryStruct.{max (max (max u₁ v₁) v₂) w₂, max (max (max (max (max u₂ u₁) v₂) v₁) w₂) w₁}
          (CategoryTheory.OplaxFunctor B C)
-- Mathlib.NumberTheory.PellMatiyasevic
/-- The Pell `y` sequence, considered as an integer sequence.  -/
Pell.yz : {a : ℕ} → 1 < a → ℕ → ℤ
-- Mathlib.Order.OrderDual
OrderDual.toDual_lt : ∀ {α : Type u_1} [inst : LT α] {a : αᵒᵈ} {b : α}, OrderDual.toDual b < a ↔ OrderDual.ofDual a < b
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.isQF_bot : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ}, ⊥.IsQF
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.isCauSeq_nthHom : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)],
  (∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) →
    ∀ (r : R), IsCauSeq (padicNorm p) fun n => ↑(PadicInt.nthHom f r n)
-- Mathlib.Order.Interval.Basic
Interval.coe_subset_coe : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Interval α}, ↑s ⊆ ↑t ↔ s ≤ t
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapId'_inv_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ : B}
  {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryTheory.CategoryStruct.id b₀) (a : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.mapId' f hf).inv.toNatTrans.app X) ((F.map f).toFunctor.map a) =
    CategoryTheory.CategoryStruct.comp a ((F.mapId' f hf).inv.toNatTrans.app Y)
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRelO.swap : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Stream'.WSeq α → Stream'.WSeq β → Prop),
  Function.swap (Stream'.WSeq.LiftRelO R C) = Stream'.WSeq.LiftRelO (Function.swap R) (Function.swap C)
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- A helper function, providing the strong epi-mono factorization used construct to colimits.  -/
CategoryTheory.MonoOver.strongEpiMonoFactorisationSigmaDesc : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y : C} →
      [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
        [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] →
          {J : Type u₂} →
            [inst_3 : CategoryTheory.Category.{v₂, u₂} J] →
              (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)) →
                CategoryTheory.Limits.StrongEpiMonoFactorisation
                  (CategoryTheory.Limits.Sigma.desc fun i => (F.obj i).arrow)
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Constructor for cowedges.  -/
CategoryTheory.Limits.Cowedge.mk : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          (pt : C) →
            (ι : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ pt) →
              (∀ ⦃i j : J⦄ (f : i ⟶ j),
                  CategoryTheory.CategoryStruct.comp ((F.map f.op).app i) (ι i) =
                    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f) (ι j)) →
                CategoryTheory.Limits.Cowedge F
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.rightAdjointOfEquiv_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G_obj : D → C} (e : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G_obj Y))
  (he :
    ∀ (X' X : C) (Y : D) (f : X' ⟶ X) (g : F.obj X ⟶ Y),
      (e X' Y) (CategoryTheory.CategoryStruct.comp (F.map f) g) = CategoryTheory.CategoryStruct.comp f ((e X Y) g))
  {Y Y' : D} (g : Y ⟶ Y'),
  (CategoryTheory.Adjunction.rightAdjointOfEquiv e he).map g =
    (e (G_obj Y) Y')
      (CategoryTheory.CategoryStruct.comp ((e (G_obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G_obj Y))) g)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- A list containing every word that `w₁` reduces to.  -/
FreeGroup.Red.enum : {α : Type u_1} → [DecidableEq α] → List (α × Bool) → List (List (α × Bool))
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_post : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D]
  [inst_3 : CategoryTheory.Limits.HasColimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) j)
      (CategoryTheory.Limits.colimit.post F G) =
    G.map (CategoryTheory.Limits.colimit.ι F j)
-- Mathlib.Probability.Independence.Integration
/-- If `X` and `Y` are random variables and `B` is a continuous bilinear map
such that `∀ x y, c * ‖x‖ * ‖y‖ ≤ ‖B x y‖`, then
`∫ ω, B (f (X ω)) (g (Y ω)) ∂μ = B (∫ ω, f (X ω) ∂μ) (∫ ω, g (Y ω) ∂μ).`

The assumption on `B` allows to drop the integrability condition in
`IndepFun.integral_bilin_comp_comp`, which is useful for the versions where `B` is the scalar
multiplication or the multiplication.  -/
ProbabilityTheory.IndepFun.integral_bilin_comp_comp' : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3}
  {𝓨 : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst_1 : MeasurableSpace 𝓧] [inst_2 : MeasurableSpace 𝓨]
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 E] [CompleteSpace E]
  [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedSpace 𝕜 F] [CompleteSpace F]
  [inst_11 : NormedAddCommGroup G] [inst_12 : NormedSpace ℝ G] [inst_13 : NormedSpace 𝕜 G] [CompleteSpace G] {X : Ω → 𝓧}
  {Y : Ω → 𝓨} {f : 𝓧 → E} {g : 𝓨 → F},
  ProbabilityTheory.IndepFun X Y μ →
    AEMeasurable X μ →
      AEMeasurable Y μ →
        MeasureTheory.AEStronglyMeasurable f (MeasureTheory.Measure.map X μ) →
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map Y μ) →
            ∀ (B : E →L[𝕜] F →L[𝕜] G) (c : NNReal),
              c ≠ 0 →
                (∀ (x : E) (y : F), ↑c * ‖x‖ * ‖y‖ ≤ ‖(B x) y‖) →
                  ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardFactors_multiset_prod : ∀ {s : Multiset ℕ},
  s.prod ≠ 0 → ArithmeticFunction.cardFactors s.prod = (Multiset.map (⇑ArithmeticFunction.cardFactors) s).sum
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The polynomial `W(X, Y) := Y² + a₁XY + a₃Y - (X³ + a₂X² + a₄X + a₆)` associated to a Weierstrass
curve `W` over a ring `R` in affine coordinates.

For ease of polynomial manipulation, this is represented as a term of type `R[X][X]`, where the
inner variable represents `X` and the outer variable represents `Y`. For clarity, the alternative
notations `Y` and `R[X][Y]` are provided in the `Polynomial.Bivariate` scope to represent the outer
variable and the bivariate polynomial ring `R[X][X]` respectively.  -/
WeierstrassCurve.Affine.polynomial : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Affine R → Polynomial (Polynomial R)
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.left_inv : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.Equiv σ),
  Function.LeftInverse self.invFun (↑self).toFun
-- Mathlib.Algebra.Group.Units.Defs
/-- An element `a : M` of an `AddMonoid` is an `AddUnit` if it has a two-sided
additive inverse. The actual definition says that `a` is equal to some `u : AddUnits M`,
where `AddUnits M` is a bundled version of `IsAddUnit`.  -/
IsAddUnit : {M : Type u_1} → [AddMonoid M] → M → Prop
-- Std.Data.DHashMap.Basic
/-- Transforms the hash map into an array of mappings in some order.  -/
Std.DHashMap.toArray : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → Array ((a : α) × β a)
-- Mathlib.Order.Partition.Finpartition
Finpartition.card_atomise_le : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {F : Finset (Finset α)},
  (Finpartition.atomise s F).parts.card ≤ 2 ^ F.card
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.integralAgainstBilinCLM_ofSupportedIn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_6} {F₂ : Type u_7} {F₃ : Type u_8} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F₁]
  [inst_13 : NormedSpace ℝ F₃] [inst_14 : IsScalarTower ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂},
  MeasureTheory.LocallyIntegrableOn φ (↑Ω) μ →
    ∀ {K : TopologicalSpace.Compacts E} (K_sub_Ω : ↑K ⊆ ↑Ω) {f : ContDiffMapSupportedIn E F₁ n K},
      (TestFunction.integralAgainstBilinCLM B μ φ) (TestFunction.ofSupportedIn K_sub_Ω f) =
        (ContDiffMapSupportedIn.integralAgainstBilinCLM B μ φ) f
-- Mathlib.Algebra.Order.Star.Basic
star_le_one_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R] {x : R},
  star x ≤ 1 ↔ x ≤ 1
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.map_g₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S T : J.Cover X} {I₁ I₂ : S.Arrow} (r : I₁.Relation I₂) (f : S ⟶ T), (r.map f).g₁ = r.g₁
-- Lean.Parser.Term
Lean.Parser.Term.basicFun : Lean.Parser.Parser
-- Mathlib.Data.List.Destutter
List.destutter'.eq_def : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (x : α) (x_1 : List α),
  List.destutter' R x x_1 =
    match x, x_1 with
    | a, [] => [a]
    | a, h :: l => if R a h then a :: List.destutter' R h l else List.destutter' R a l
-- Mathlib.Order.Atoms
/-- **Alias** of the forward direction of `covBy_top_iff`. -/
CovBy.isCoatom : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, a ⋖ ⊤ → IsCoatom a
-- Mathlib.Topology.UnitInterval
/-- Helper definition for `convexComb_assoc'`, giving one of the coefficients appearing
when we reassociate a convex combination in the reverse direction.
 -/
Set.Icc.convexComb_assoc_coeff₁' : ↑unitInterval → ↑unitInterval → ↑unitInterval
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_append_replicate_zero : ∀ {b k : ℕ} (l : List ℕ), Nat.ofDigits b (l ++ List.replicate k 0) = Nat.ofDigits b l
-- Mathlib.LinearAlgebra.Eigenspace.Pi
/-- A commuting family of triangularizable endomorphisms is simultaneously triangularizable.  -/
Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_iSup_maxGenEigenspace_eq_top_of_commute : ∀ {ι : Type u_1} {K : Type u_3} {M : Type u_4} [inst : Field K] [inst_1 : AddCommGroup M] [inst_2 : Module K M]
  [FiniteDimensional K M] (f : ι → Module.End K M),
  (Pairwise fun i j => Commute (f i) (f j)) →
    (∀ (i : ι), ⨆ μ, (f i).maxGenEigenspace μ = ⊤) → ⨆ χ, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.instIsKInjectiveExtendNatIntEmbeddingUpNatOfInjectiveX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℕ) [∀ (n : ℕ), CategoryTheory.Injective (K.X n)],
  CochainComplex.IsKInjective (HomologicalComplex.extend K ComplexShape.embeddingUpNat)
-- Mathlib.Geometry.Convex.ConvexSpace.Module
/-- `iConvexComb` in a module can be expressed as a sum.  -/
Convexity.iConvexComb_eq_sum : ∀ {R : Type u_2} {M : Type u_3} {I : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Convexity.ConvexSpace R M]
  [Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R I) (f : I → M),
  Convexity.iConvexComb w f = w.weights.sum fun i r => r • f i
-- Mathlib.Topology.Inseparable
Topology.IsInducing.specializes_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
  Topology.IsInducing f → (f x ⤳ f y ↔ x ⤳ y)
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- `LightCondSet.LocallyConstant.functor` is fully faithful.  -/
LightCondSet.LocallyConstant.functorFullyFaithful : LightCondSet.LocallyConstant.functor.FullyFaithful
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.ext : ∀ {R : Type u_1} [inst : Semiring R] {p q : SkewPolynomial R}, (∀ (n : ℕ), p.coeff n = q.coeff n) → p = q
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.val_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (x : (PreQuasiregular A)ˣ),
  ↑↑((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x) = 1 + ↑(PreQuasiregular.equiv.symm ↑x)
-- Std.Time.Internal.UnitVal
/-- Divides the `UnitVal` by an `Int`, resulting in a new `UnitVal` with an adjusted ratio.
 -/
Std.Time.Internal.UnitVal.div : {a : ℚ} → Std.Time.Internal.UnitVal a → (divisor : ℤ) → Std.Time.Internal.UnitVal (a * ↑divisor)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- The angle at the center of a circle equals twice the angle at the circumference, oriented angle
version.  -/
EuclideanGeometry.Sphere.oangle_center_eq_two_zsmul_oangle : ∀ {V : Type u_3} {P : Type u_4} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {s : EuclideanGeometry.Sphere P} {p₁ p₂ p₃ : P},
  p₁ ∈ s →
    p₂ ∈ s →
      p₃ ∈ s → p₂ ≠ p₁ → p₂ ≠ p₃ → EuclideanGeometry.oangle p₁ s.center p₃ = 2 • EuclideanGeometry.oangle p₁ p₂ p₃
-- Mathlib.Topology.Separation.Profinite
/-- Let `X` be a totally disconnected compact Hausdorff space, `D i ⊆ X` a finite family of clopens,
and `Z i ⊆ D i` closed. Assume that the `Z i` are pairwise disjoint. Then there exist clopens
`Z i ⊆ C i ⊆ D i` with the `C i` disjoint, and such that `∪ D i ⊆ ∪ C i`.  -/
exists_clopen_partition_of_clopen_cover : ∀ {X : Type u_4} {I : Type u_5} [inst : TopologicalSpace X] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X]
  [Finite I] {Z D : I → Set X},
  (∀ (i : I), IsClosed (Z i)) →
    (∀ (i : I), IsClopen (D i)) →
      (∀ (i : I), Z i ⊆ D i) →
        Set.univ.PairwiseDisjoint Z →
          ∃ C,
            (∀ (i : I), IsClopen (C i)) ∧
              (∀ (i : I), Z i ⊆ C i) ∧ (∀ (i : I), C i ⊆ D i) ∧ ⋃ i, D i ⊆ ⋃ i, C i ∧ Set.univ.PairwiseDisjoint C
-- Init.Data.List.Zip
List.getElem?_zipWithAll : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {as : List α} {bs : List β} {f : Option α → Option β → γ} {i : ℕ},
  (List.zipWithAll f as bs)[i]? =
    match as[i]?, bs[i]? with
    | none, none => none
    | a?, b? => some (f a? b?)
-- Mathlib.Geometry.Convex.Cone.Basic
Convex.toCone.eq_1 : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] (s : Set M) (hs : Convex 𝕜 s),
  Convex.toCone s hs = { carrier := ⋃ c, ⋃ (_ : 0 < c), c • s, smul_mem' := ⋯, add_mem' := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Applying `affineCombination` with given weights.  This is for the
case where a result involving a default base point is OK (for example,
when that base point will cancel out later); a more typical use case
for `affineCombination` would involve selecting a preferred base
point with
`affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one` and
then using `weightedVSubOfPoint_apply`.  -/
Finset.affineCombination_apply : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
  (Finset.affineCombination k s p) w = (s.weightedVSubOfPoint p (Classical.choice ⋯)) w +ᵥ Classical.choice ⋯
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.GammaAux_recurrence2 : ∀ (s : ℂ) (n : ℕ), -s.re < ↑n → Complex.GammaAux✝ n s = Complex.GammaAux✝ (n + 1) s
-- Mathlib.Algebra.Category.Grp.Basic
/-- The (unbundled) group of automorphisms of a type is `MulEquiv` to the (unbundled) group
of permutations.  -/
CategoryTheory.Aut.mulEquivPerm : {α : Type u} → CategoryTheory.Aut α ≃* Equiv.Perm α
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.Context.mk : Lean.Elab.Term.ElabElimInfo → Lean.Expr → Lean.Elab.Term.ElabElim.Context
-- Std.Sync.Mutex
_private.Std.Sync.Mutex.0.Std.Mutex.mk.inj : ∀ {α : Type} {ref : IO.Ref α} {mutex : Std.BaseMutex} {ref_1 : IO.Ref α} {mutex_1 : Std.BaseMutex},
  { ref := ref, mutex := mutex } = { ref := ref_1, mutex := mutex_1 } → ref = ref_1 ∧ mutex = mutex_1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RcoSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Rco α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.Order.Hom.Basic
OrderIso.equivEmbeddingSurjective_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (f : α ≃o β),
  OrderIso.equivEmbeddingSurjective f = ⟨RelIso.toRelEmbedding f, ⋯⟩
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.flip_surjective_iff₂ : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₂],
  Function.Surjective ⇑B.flip ↔ Function.Injective ⇑B
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.minKeyD fallback ∈ t
-- Lean.Parser.Term
Lean.Parser.Term.optExprPrecedence.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.QuotientGroup.Defs
Con.mk.congr_simp : ∀ {M : Type u_1} [inst : Mul M] (toSetoid toSetoid_1 : Setoid M) (e_toSetoid : toSetoid = toSetoid_1)
  (mul' : ∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w * y) (x * z)),
  { toSetoid := toSetoid, mul' := mul' } = { toSetoid := toSetoid_1, mul' := ⋯ }
-- Init.Data.Array.Basic
/-- Applies a function to each element of the array along with the index at which that element is found,
returning the array of results.

`Array.mapFinIdx` is a variant that additionally provides the function with a proof that the index
is valid.
 -/
Array.mapIdx : {α : Type u} → {β : Type v} → (ℕ → α → β) → Array α → Array β
-- Mathlib.Probability.Distributions.Gamma
/-- The gamma pdf is nonnegative  -/
ProbabilityTheory.gammaPDFReal_nonneg : ∀ {a r : ℝ}, 0 < a → 0 < r → ∀ (x : ℝ), 0 ≤ ProbabilityTheory.gammaPDFReal a r x
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.of_addEquivOfAddEquiv_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {T : AddSubmonoid P} {Q : Type u_4} [inst_3 : AddCommMonoid Q]
  {k : T.LocalizationMap Q} {j : M ≃+ P} (H : AddSubmonoid.map j.toAddMonoidHom S = T) (x : M),
  (f.ofAddEquivOfLocalizations (f.addEquivOfAddEquiv k H)) x = k (j x)
-- Mathlib.Order.OrderDual
OrderDual.instMinOfMax.eq_1 : ∀ (α : Type u_2) [h : Max α], OrderDual.instMinOfMax α = { min := fun a b => a ⊔ b }
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.lastEditTimestamp? : Lean.Server.FileWorker.InlayHintState → Option ℕ
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {r : HomRel C} {x y : CategoryTheory.Quotient r},
  x = y ↔ x.as = y.as
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- The *exponent* of a purely inseparable extension is the smallest
natural number `e` such that `a ^ ringExpChar K ^ e ∈ K` for all `a ∈ L`.  -/
IsPurelyInseparable.exponent : (K : Type u_2) →
  (L : Type u_3) →
    [inst : CommRing K] → [inst_1 : Ring L] → [inst_2 : Algebra K L] → [IsPurelyInseparable.HasExponent K L] → ℕ
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- **Alias** of the forward direction of `Filter.eventually_atBot`. -/
Filter.Eventually.exists_forall_of_atBot : ∀ {α : Type u_3} [inst : Preorder α] [IsCodirectedOrder α] {p : α → Prop} [Nonempty α],
  (∀ᶠ (x : α) in Filter.atBot, p x) → ∃ a, ∀ b ≤ a, p b
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- This is the nondependent eliminator for `K'`, but we use it specifically here in order to
represent the stack data as four lists rather than as a function `K' → List Γ'`, because this makes
rewrites easier. The theorems `K'.elim_update_main` et. al. show how such a function is updated
after an `update` to one of the components.  -/
Turing.PartrecToTM2.K'.elim : List Turing.PartrecToTM2.Γ' →
  List Turing.PartrecToTM2.Γ' →
    List Turing.PartrecToTM2.Γ' → List Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.K' → List Turing.PartrecToTM2.Γ'
-- Mathlib.Topology.Compactness.Compact
/-- If `s : Set (X × Y)` belongs to `𝓝 x ×ˢ l` for all `x` from a compact set `K`,
then it belongs to `(𝓝ˢ K) ×ˢ l`,
i.e., there exist an open `U ⊇ K` and `t ∈ l` such that `U ×ˢ t ⊆ s`.  -/
IsCompact.mem_nhdsSet_prod_of_forall : ∀ {X : Type u} [inst : TopologicalSpace X] {K : Set X} {Y : Type u_2} {l : Filter Y} {s : Set (X × Y)},
  IsCompact K → (∀ x ∈ K, s ∈ nhds x ×ˢ l) → s ∈ nhdsSet K ×ˢ l
-- Init.Data.List.MinMaxOn
List.minOn_replicate : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {n : ℕ} {a : α}
  {f : α → β} (h : List.replicate n a ≠ []), List.minOn f (List.replicate n a) h = a
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.span_coroot_support : ∀ {ι : 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} (b : P.Base),
  Submodule.span R (⇑P.coroot '' ↑b.support) = P.corootSpan R
-- Mathlib.Computability.Language
/-- `1 : Language α` contains only one element `[]`.  -/
Language.instOne : {α : Type u_1} → One (Language α)
-- Mathlib.CategoryTheory.ObjectProperty.Local
CategoryTheory.MorphismProperty.isColocal_antitone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W W' : CategoryTheory.MorphismProperty C},
  W ≤ W' → W'.isColocal ≤ W.isColocal