mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_eq_fallback : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} {fallback : β}, a ∉ m → m.getD a fallback = fallback
-- Init.Data.Array.Monadic
Array.forIn_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {init : γ} [inst : Monad m] [LawfulMonad m]
  {xs : Array α} {g : α → β} {f : β → γ → m (ForInStep γ)},
  forIn (Array.map g xs) init f = forIn xs init fun a y => f (g a) y
-- Lean.Data.NameTrie
Lean.NamePart.cmp : Lean.NamePart → Lean.NamePart → Ordering
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- To show `F` is a comonadic left adjoint, we can show it preserves and reflects `F`-split
equalizers, and `C` has them.
 -/
CategoryTheory.Comonad.comonadicOfHasPreservesReflectsFSplitEqualizers : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              [CategoryTheory.Comonad.HasEqualizerOfIsCosplitPair F] →
                [CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair F] →
                  [CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair F] → CategoryTheory.ComonadicLeftAdjoint F
-- Lean.Compiler.InitAttr
Lean.registerInitAttrUnsafe : Lean.Name → Bool → Lean.Name → IO (Lean.ParametricAttribute Lean.Name)
-- Lean.Server.GoTo
Lean.Server.locationLinksDefault : Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Init.Data.UInt.Lemmas
USize.toBitVec_ofBitVec : ∀ (n : BitVec System.Platform.numBits), { toBitVec := n }.toBitVec = n
-- Init.Data.Fin.Lemmas
Fin.pred_mk_succ' : ∀ {n : ℕ} (i : ℕ) (h₁ : i + 1 < n + 1 + 1) (h₂ : ⟨i + 1, h₁⟩ ≠ 0), ⟨i + 1, h₁⟩.pred h₂ = ⟨i, ⋯⟩
-- Lean.Meta.Sym.Pattern
/-- Collects `ProofInstInfo` for all function symbols occurring in `pattern`.

Only includes functions that have at least one proof or instance argument.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkProofInstInfoMapFor : Lean.Expr → Lean.MetaM (Lean.AssocList Lean.Name Lean.Meta.Sym.ProofInstInfo)
-- Mathlib.Algebra.Notation.Defs
/-- Type class for the `-ᵥ` notation.  -/
VSub : outParam (Type u_1) → Type u_2 → Type (max u_1 u_2)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeMap.unitOfList l cmp).getKeyD k' fallback = k
-- Init.Data.List.Monadic
List.zipWithM.loop.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (x : List α)
  (x_1 : List β) (x_2 : Array γ),
  List.zipWithM.loop f x x_1 x_2 =
    match x, x_1, x_2 with
    | a :: as, b :: bs, acc => do
      let __do_lift ← f a b
      List.zipWithM.loop f as bs (acc.push __do_lift)
    | x, x_3, acc => pure acc.toList
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.dvd_prod : ∀ {M : Type u_4} [inst : CommMonoid M] {a : M} {l : List M}, a ∈ l → a ∣ l.prod
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- See `card_le_card_mul_left` for a more convenient but less general version for types with a
left-cancellative multiplication.
 -/
Finset.card_le_card_mul_left_of_injective : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α} {a : α},
  a ∈ s → IsLeftRegular a → t.card ≤ (s * t).card
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.coe_mk' : ∀ {M : Type u_1} [inst : AddZeroClass M] {c : AddCon M}, ⇑c.mk' = AddCon.toQuotient
-- Mathlib.Data.FP.Basic
FP.FloatCfg.precPos : ∀ [self : FP.FloatCfg], 0 < FP.FloatCfg.prec
-- Mathlib.Algebra.MonoidAlgebra.Division
AddMonoidAlgebra.modOf_add_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G]
  (x : AddMonoidAlgebra k G) (g : G), x.modOf g + AddMonoidAlgebra.of' k G g * x.divOf g = x
-- Init.Data.List.Find
List.findFinIdx?_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool}, List.findFinIdx? p [a] = if p a = true then some ⟨0, ⋯⟩ else none
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.comp_d₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (self : CochainComplex.ConnectData K L),
  CategoryTheory.CategoryStruct.comp (K.d 1 0) self.d₀ = 0
-- Mathlib.Topology.Sheaves.Functors
TopCat.Sheaf.instIsLeftAdjointPullback : ∀ {X Y : TopCat} (f : X ⟶ Y) (A : Type u_1) [inst : CategoryTheory.Category.{w, u_1} A] {FA : A → A → Type u_2}
  {CA : A → Type w} [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_2 : CategoryTheory.ConcreteCategory A FA] [inst_3 : CategoryTheory.Limits.HasColimits A]
  [inst_4 : CategoryTheory.Limits.HasLimits A]
  [inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget A)]
  [inst_6 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget A)]
  [inst_7 : (CategoryTheory.forget A).ReflectsIsomorphisms], (TopCat.Sheaf.pullback A f).IsLeftAdjoint
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instModule : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          {R : Type u_4} →
            [inst_2 : Semiring R] →
              [inst_3 : Module R M] →
                [ContinuousConstSMul R M] → [inst_5 : ContinuousAdd M] → Module R (MeasureTheory.VectorMeasure α M)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_spec`. -/
Ideal.ramificationIdx_spec : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  {n : ℕ}, Ideal.map (algebraMap R S) p ≤ P ^ n → ¬Ideal.map (algebraMap R S) p ≤ P ^ (n + 1) → p.ramificationIdx' P = n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {v : β k} {h₁ : a ∈ t.insertIfNew k v},
  (t.insertIfNew k v).get a h₁ = if h₂ : cmp k a = Ordering.eq ∧ k ∉ t then cast ⋯ v else t.get a ⋯
-- Mathlib.Order.CompleteLattice.Basic
iSup₂_le_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (κ : ι → Sort u_8) (f : ι → α), ⨆ i, ⨆ x, f i ≤ ⨆ i, f i
-- Init.Grind.Ordered.Linarith
/-- Converts the given expression into a polynomial, and then normalizes it.  -/
Lean.Grind.Linarith.Expr.norm : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Poly
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertManyIfNewUnit.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ α] (m m_1 : Std.ExtHashMap α Unit),
  m = m_1 → ∀ (l l_1 : ρ), l = l_1 → m.insertManyIfNewUnit l = m_1.insertManyIfNewUnit l_1
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.isAlgebraic : ∀ (k : Type u) [inst : Field k], Algebra.IsAlgebraic k (AlgebraicClosure k)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- The family of morphisms from the pullback cover to the original cover.  -/
AlgebraicGeometry.Scheme.Cover.pullbackHom : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] →
      {X W : AlgebraicGeometry.Scheme} →
        (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
          (f : W ⟶ X) →
            (i : 𝒰.toPreZeroHypercover.1) →
              [inst_2 : ∀ (x : 𝒰.I₀), CategoryTheory.Limits.HasPullback f (𝒰.f x)] →
                (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).X i ⟶ 𝒰.X i
-- Mathlib.Algebra.Order.Quantale
Quantale.mul_bot : ∀ {α : Type u_3} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α] {x : α}, x * ⊥ = ⊥
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negAddY_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P Q : Fin 3 → R},
  W'.Equation Q → Q 2 = 0 → W'.negAddY P Q = (-(Q 0 * P 2)) ^ 3 * W'.negY P
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₁ ⟶ X₀) (d₁ : X₂ ⟶ X₁) (s : CategoryTheory.CategoryStruct.comp d₁ d₀ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' CategoryTheory.CategoryStruct.comp d₂ S.f = 0),
  ChainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ =
    ChainComplex.of (fun n => (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).X₃)
      (fun n => (ChainComplex.mkAux X₀ X₁ X₂ d₀ d₁ s succ n).g) ⋯
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.sphere_subset_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {r R : ℝ}, r < R → Metric.sphere x r ⊆ Metric.ball x R
-- Init.Data.Option.Lemmas
Option.le.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (val : α), Option.le r (some val) none = False
-- Mathlib.FieldTheory.Separable
/-- If `F` is of characteristic `p` and `p ∤ n`, then `X ^ n - a` is separable for any `a ≠ 0`.  -/
Polynomial.separable_X_pow_sub_C' : ∀ {F : Type u} [inst : Field F] (p n : ℕ) (a : F) [CharP F p],
  ¬p ∣ n → a ≠ 0 → (Polynomial.X ^ n - Polynomial.C a).Separable
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- The bimonoid morphism from the trivial bimonoid to any bimonoid.  -/
CategoryTheory.Bimon.trivialTo : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (A : CategoryTheory.Bimon C) → CategoryTheory.Bimon.trivial C ⟶ A
-- Mathlib.Logic.Function.Basic
Function.Bijective.of_comp_left : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : γ → α},
  Function.Bijective (f ∘ g) → Function.Injective f → Function.Bijective g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.IsPullback.app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasPullbacks D] {F₁ F₂ F₃ F₄ : CategoryTheory.Functor C D} {f₁ : F₁ ⟶ F₂} {f₂ : F₁ ⟶ F₃}
  {f₃ : F₂ ⟶ F₄} {f₄ : F₃ ⟶ F₄},
  CategoryTheory.IsPullback f₁ f₂ f₃ f₄ →
    ∀ (X : C), CategoryTheory.IsPullback (f₁.app X) (f₂.app X) (f₃.app X) (f₄.app X)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- Taking the product under `h` is an additive homomorphism of finsupps, if `h` is an
additive homomorphism on the support. This is a more general version of
`Finsupp.sum_add_index'`; the latter has simpler hypotheses.  -/
Finsupp.sum_add_index : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : DecidableEq α] [inst_1 : AddZeroClass M]
  [inst_2 : AddCommMonoid N] {f g : α →₀ M} {h : α → M → N},
  (∀ a ∈ f.support ∪ g.support, h a 0 = 0) →
    (∀ a ∈ f.support ∪ g.support, ∀ (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f + g).sum h = f.sum h + g.sum h
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cocone.cocone_iso_of_hom_iso`.

---

Given a cocone morphism whose object part is an isomorphism, produce an
isomorphism of cocones.
 -/
CategoryTheory.Limits.Cocones.cone_iso_of_hom_iso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {K : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cocone K} (f : d ⟶ c) [i : CategoryTheory.IsIso f.hom],
  CategoryTheory.IsIso f
-- Mathlib.Topology.Algebra.Order.Field
/-- If `g` tends to `atTop` and there exist constants `b B : 𝕜` such that eventually
`b ≤ f x| ≤ B`, then the quotient `f / g` tends to zero.  -/
tendsto_bdd_div_atTop_nhds_zero : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {b B : 𝕜},
  (∀ᶠ (x : α) in l, b ≤ f x) →
    (∀ᶠ (x : α) in l, f x ≤ B) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x / g x) l (nhds 0)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- **Alias** of the reverse direction of `orthogonalFamily_iff_pairwise`. -/
OrthogonalFamily.of_pairwise : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {V : ι → Submodule 𝕜 E},
  Pairwise (Function.onFun (fun x1 x2 => x1 ⟂ x2) V) → OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.comp_PInfty_eq_zero_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] {Z : C} {n : ℕ} (f : Z ⟶ X.obj (Opposite.op { len := n })),
  CategoryTheory.CategoryStruct.comp f (AlgebraicTopology.DoldKan.PInfty.f n) = 0 ↔
    CategoryTheory.CategoryStruct.comp f
        (s.πSummand (CategoryTheory.SimplicialObject.Splitting.IndexSet.id (Opposite.op { len := n }))) =
      0
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.mul_isLittleO : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] {S : Type u_17} [inst_1 : NormedRing S] [NormMulClass S]
  {l : Filter α} {f₁ f₂ : α → R} {g₁ g₂ : α → S},
  f₁ =O[l] g₁ → f₂ =o[l] g₂ → (fun x => f₁ x * f₂ x) =o[l] fun x => g₁ x * g₂ x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : SizeOf C] (val : PresheafOfModules R.obj)
  (isSheaf : CategoryTheory.Presheaf.IsSheaf J val.presheaf), sizeOf { val := val, isSheaf := isSheaf } = 1 + sizeOf val
-- Mathlib.Algebra.Lie.Nilpotent
lieModule_lcs_map_le : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] {L₂ : Type u_1}
  {M₂ : Type u_2} [inst_7 : LieRing L₂] [inst_8 : LieAlgebra R L₂] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : LieRingModule L₂ M₂] {f : L →ₗ⁅R⁆ L₂} {g : M →ₗ[R] M₂},
  (∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) →
    ∀ (k : ℕ), Submodule.map g ↑(LieModule.lowerCentralSeries R L M k) ≤ ↑(LieModule.lowerCentralSeries R L₂ M₂ k)
-- Mathlib.Order.Heyting.Basic
CoheytingAlgebra.toOrderTop : {α : Type u_4} → [self : CoheytingAlgebra α] → OrderTop α
-- Lean.Language.Lean.Types
Lean.Language.Lean.instToSnapshotTreeCommandResultSnapshot : Lean.Language.ToSnapshotTree Lean.Language.Lean.CommandResultSnapshot
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.isCoprime_num_denom : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), IsCoprime x.num x.denom
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.refl_homotopyInvHomId : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} (C : HomologicalComplex V c), (HomotopyEquiv.refl C).homotopyInvHomId = Homotopy.ofEq ⋯
-- Mathlib.Algebra.Order.Floor.Ring
/-- The fractional part of `a` is positive if and only if `a ≠ ⌊a⌋`.  -/
Int.fract_pos : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R} [IsOrderedRing R],
  0 < Int.fract a ↔ a ≠ ↑⌊a⌋
-- Mathlib.Analysis.Seminorm
SeminormClass.mk : ∀ {F : Type u_12} {𝕜 : outParam (Type u_13)} {E : outParam (Type u_14)} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E]
  [inst_2 : SMul 𝕜 E] [inst_3 : FunLike F E ℝ] [toAddGroupSeminormClass : AddGroupSeminormClass F E ℝ],
  (∀ (f : F) (a : 𝕜) (x : E), f (a • x) = ‖a‖ * f x) → SeminormClass F 𝕜 E
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Multiset.one_le_prod : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulMono R]
  {s : Multiset R}, (∀ a ∈ s, 1 ≤ a) → 1 ≤ s.prod
-- Mathlib.Topology.Bornology.Constructions
Bornology.isBounded_image_subtype_val : ∀ {α : Type u_1} [inst : Bornology α] {p : α → Prop} {s : Set { x // p x }},
  Bornology.IsBounded (Subtype.val '' s) ↔ Bornology.IsBounded s
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- A point is centroid if and only if the sum of vectors from the point to all vertices is zero.  -/
Affine.Simplex.eq_centroid_iff_sum_vsub_eq_zero : ∀ {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 : ℕ} [CharZero k] {s : Affine.Simplex k P n} {p : P},
  p = s.centroid ↔ ∑ i, (s.points i -ᵥ p) = 0
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instSemiring : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} →
          [inst : SMul M X] →
            [inst_1 : Monoid N] → [inst_2 : Semiring Y] → [inst_3 : MulSemiringAction N Y] → Semiring (X →ₑ[σ] Y)
-- Mathlib.Data.TypeVec
TypeVec.dropFun_comp : ∀ {n : ℕ} {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)} (f₀ : α₀.Arrow α₁)
  (f₁ : α₁.Arrow α₂), TypeVec.dropFun (TypeVec.comp f₁ f₀) = TypeVec.comp (TypeVec.dropFun f₁) (TypeVec.dropFun f₀)
-- Init.Data.Vector.Extract
Vector.set_eq_push_extract_append_extract : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n) {a : α},
  xs.set i a h = Vector.cast ⋯ ((xs.extract 0 i).push a ++ xs.extract (i + 1))
-- Init.Prelude
/-- Constructs a pair. This is usually written `(x, y)` instead of `Prod.mk x y`.


Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. -/
Prod.mk : {α : Type u} → {β : Type v} → α → β → α × β
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- If `i + 1 < j`, `mkOfSucc i ≫ δ j` is the morphism `⦋1⦌ ⟶ ⦋n⦌` that
sends `0` and `1` to `i` and `i + 1`, respectively.  -/
SimplexCategory.mkOfSucc_δ_lt : ∀ {n : ℕ} {i : Fin n} {j : Fin (n + 2)},
  i.succ.castSucc < j →
    CategoryTheory.CategoryStruct.comp (SimplexCategory.mkOfSucc i) (SimplexCategory.δ j) =
      SimplexCategory.mkOfSucc i.castSucc
-- Init.Data.Iterators.Lemmas.Combinators.ULift
_private.Init.Data.Iterators.Lemmas.Combinators.ULift.0.Std.IterM.step_uLift.match_1.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it' out h
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.toEquiv_homeomorph : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : TopologicalSpace X],
  Metric.Snowflaking.homeomorph.toEquiv = Metric.Snowflaking.ofSnowflaking
-- Std.Http.Data.Method
Std.Http.Method.mkcol.sizeOf_spec : sizeOf Std.Http.Method.mkcol = 1
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- **Alias** of `Convexity.convexCombPair_one`.

---

A binary convex combination with weight 1 on the first point returns the first point.  -/
Convexity.convexComboPair_one : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {x y : M}, Convexity.convexCombPair 1 0 ⋯ ⋯ ⋯ x y = x
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Canonical factors are meromorphic in normal form.
 -/
Complex.meromorphicNFOn_canonicalFactor : ∀ {R : ℝ} {w : ℂ}, w ∈ Metric.ball 0 R → MeromorphicNFOn (Complex.canonicalFactor R w) Set.univ
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The image of a divided power morphism from `I` to `J` is a sub-dp-ideal of `J`.  -/
DividedPowers.isSubDPIdeal_map : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} [inst_1 : CommSemiring B]
  {J : Ideal B} {hJ : DividedPowers J} {f : A →+* B}, hI.IsDPMorphism hJ f → hJ.IsSubDPIdeal (Ideal.map f I)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.typeParameter : Lean.Lsp.SymbolKind
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- If `Fₙ` tends uniformly to `f` on a set `s`, and `gₙ` tends to `x` within `s`, then `Fₙ gₙ`
tends to `f x` if `f` is continuous at `x` within `s`.  -/
TendstoUniformlyOn.tendsto_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α},
  TendstoUniformlyOn F f p s →
    ContinuousWithinAt f s x → Filter.Tendsto g p (nhdsWithin x s) → Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.instIsSplitMonoComp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ Y}
  [hf : CategoryTheory.IsSplitMono f] [hg : CategoryTheory.IsSplitMono g],
  CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The quadratic character as a multiplicative character.  -/
quadraticChar : (F : Type u_1) → [inst : Field F] → [Fintype F] → [DecidableEq F] → MulChar F ℤ
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.dirichletUnitTheorem.seq.eq_2 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ}
  (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B)
  (n : ℕ), NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n.succ = ⟨⋯.choose, ⋯⟩
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_inv_hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b : CategoryTheory.Bicategory.InducedBicategory C F} (x : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor x).inv.hom = (CategoryTheory.Bicategory.rightUnitor x.hom).inv
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.braiding_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (P Q : C),
  (CategoryTheory.Limits.coprod.braiding P Q).hom =
    CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl
-- Mathlib.GroupTheory.Commutator.Finite
Subgroup.rank_commutator_le_card : ∀ (G : Type u_1) [inst : Group G] [inst_1 : Finite ↑(commutatorSet G)],
  Group.rank ↥(commutator G) ≤ Nat.card ↑(commutatorSet G)
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_eq_one : ∀ {c : Cardinal.{u}}, Cardinal.toNat c = 1 ↔ c = 1
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.isIntegral_root : ∀ {K : Type u_5} [inst : Field K] {f : Polynomial K}, f ≠ 0 → IsIntegral K (AdjoinRoot.root f)
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_star : ∀ {d : ℤ} (z : ℤ√d), (star z).im = -z.im
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- The parts of a Turán-maximal graph form an equipartition.  -/
SimpleGraph.IsTuranMaximal.isEquipartition : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r)
  [inst_2 : DecidableEq V], h.finpartition.IsEquipartition
-- Mathlib.Order.Filter.Ultrafilter.Basic
/-- **Alias** of `Filter.compl_mem_hyperfilter_of_finite`. -/
Set.Finite.compl_mem_hyperfilter : ∀ {α : Type u} [inst : Infinite α] {s : Set α}, s.Finite → sᶜ ∈ Filter.hyperfilter α