mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.instMonoI : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.LeftHomologyData), CategoryTheory.Mono h.i
-- Mathlib.Order.Defs.Unbundled
antisymm_def : ∀ {α : Sort u_1} {r : α → α → Prop}, Std.Antisymm r ↔ ∀ ⦃a b : α⦄, r a b → r b a → a = b
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_or_compl_adj : ∀ {V : Type u} (G : SimpleGraph V) (u v : V), G.Reachable u v ∨ Gᶜ.Adj u v
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_single_one : ∀ (α : Type u_5) (n : Type u_6) [inst : Zero α] [inst_1 : One α] [inst_2 : DecidableEq n] [inst_3 : AddGroup n],
  Matrix.circulant (Pi.single 0 1) = 1
-- Mathlib.Algebra.GCDMonoid.Basic
Associated.gcd_eq_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {m n : α},
  Associated m n → ∀ (k : α), gcd k m = gcd k n
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.pack.match_1.congr_eq_3 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (x : Float.Model.UnpackedFloat)
  (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos))
  (s : Float.Model.UnpackedFloat.Sign),
  x = Float.Model.UnpackedFloat.zero s →
    (match x with
      | Float.Model.UnpackedFloat.notANumber => h_1 ()
      | Float.Model.UnpackedFloat.infinity s => h_2 s
      | Float.Model.UnpackedFloat.zero s => h_3 s
      | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) ≍
      h_3 s
-- Mathlib.Algebra.Order.GroupWithZero.Basic
StrictAnti.mul_const : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [inst_2 : Preorder α]
  {f : α → M₀} [MulPosStrictMono M₀], StrictAnti f → 0 < a → StrictAnti fun x => f x * a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Inhabited α] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeMap.unitOfList l cmp).getKey! k' = k
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essSurj_comp : ∀ {C : Type u₁} {D : Type u₂} {E : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.EssSurj] [G.EssSurj], (F.comp G).EssSurj
-- Std.Http.Data.URI.Basic
/-- Sets the URI scheme (e.g., "http", "https"). Panics if the scheme is invalid.
Use `setScheme?` if you need a safe option-returning version.
 -/
Std.Http.URI.Builder.setScheme! : Std.Http.URI.Builder → String → Std.Http.URI.Builder
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' : α}, cmp k k' = Ordering.eq → (k ∈ t ↔ k' ∈ t)
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
/-- The canonical algebraic closure of a field, the direct limit of adding roots to the field for
each polynomial over the field.  -/
AlgebraicClosure : (k : Type u) → [Field k] → Type u
-- Mathlib.Data.FinEnum
FinEnum.Finset.finEnum : {α : Type u} → [FinEnum α] → FinEnum (Finset α)
-- Init.Data.String.Lemmas.TakeDrop
String.toList_copy_take : ∀ {s : String} {n : ℕ}, (s.take n).copy.toList = List.take n s.toList
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of `Topology.IsEmbedding.isOpenEmbedding_of_surjective`.

---

A surjective embedding is an `IsOpenEmbedding`.  -/
Topology.IsOpenEmbedding.of_isEmbedding : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → Function.Surjective f → Topology.IsOpenEmbedding f
-- Init.Data.List.Basic
List.tail_nil : ∀ {α : Type u}, [].tail = []
-- Mathlib.NumberTheory.Primorial
/-- The primorial `n#` of `n` is the product of the primes less than or equal to `n`.
 -/
primorial : ℕ → ℕ
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffOn.div₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : GroupWithZero G] [ContMDiffInv₀ I n G]
  [ContMDiffMul I n G] {E' : Type u_5} [inst_9 : NormedAddCommGroup E'] [inst_10 : NormedSpace 𝕜 E'] {H' : Type u_6}
  [inst_11 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {f g : M → G} {s : Set M},
  ContMDiffOn I' I n f s → ContMDiffOn I' I n g s → (∀ x ∈ s, g x ≠ 0) → ContMDiffOn I' I n (f / g) s
-- Mathlib.Analysis.ODE.Basic
IsIntegralCurveOn.isIntegralCurveAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {s : Set ℝ}
  {t₀ : ℝ}, IsIntegralCurveOn γ v s → s ∈ nhds t₀ → IsIntegralCurveAt γ v t₀
-- Mathlib.GroupTheory.OrderOfElement
RightCancelMonoid.finite_powers : ∀ {G : Type u_1} [inst : RightCancelMonoid G] {a : G}, (↑(Submonoid.powers a)).Finite ↔ IsOfFinOrder a
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.add_int_iff : ∀ {p x : ℝ} {m : ℤ}, LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
/-- The variables which have been *effectively eliminated*,
i.e. by running the elimination algorithm on that variable.  -/
Mathlib.Tactic.Linarith.PComp.effective : Mathlib.Tactic.Linarith.PComp → Std.TreeSet ℕ compare
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.preimageIso_inv_ι_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : CategoryTheory.IsIso f] (U : Y.Opens)
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.preimageIso f U).inv
      (CategoryTheory.CategoryStruct.comp ((TopologicalSpace.Opens.map f.base).obj U).ι
        (CategoryTheory.CategoryStruct.comp f h)) =
    CategoryTheory.CategoryStruct.comp U.ι h
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₀₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (self : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp self.v₀₁ self.v₁₂ = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forM_eq_forM_keysArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {m' : Type w → Type w'}
  [inst_2 : Monad m'] [LawfulMonad m'] {f : α → m' PUnit.{w + 1}},
  m.WF → Std.HashMap.Raw.forM (fun a x => f a) m = Array.forM f m.keysArray
-- Mathlib.Order.CountableSupClosed
finsetInf'_mem_countableInfClosure : ∀ {α : Type u_2} {s : Set α} {ι : Type u_4} [inst : SemilatticeInf α] {t : Finset ι} (ht : t.Nonempty) {f : ι → α},
  (∀ i ∈ t, f i ∈ s) → t.inf' ht f ∈ countableInfClosure s
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
/-- The functor `F.mapDerivedCategory` is induced
by `F.mapHomologicalComplex (ComplexShape.up ℤ)`.  -/
CategoryTheory.Functor.mapDerivedCategoryFactors : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [inst_1 : CategoryTheory.Abelian C₁] →
      [inst_2 : HasDerivedCategory C₁] →
        {C₂ : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_4 : CategoryTheory.Abelian C₂] →
              [inst_5 : HasDerivedCategory C₂] →
                (F : CategoryTheory.Functor C₁ C₂) →
                  [inst_6 : F.Additive] →
                    [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F] →
                      [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] →
                        DerivedCategory.Q.comp F.mapDerivedCategory ≅
                          (F.mapHomologicalComplex (ComplexShape.up ℤ)).comp DerivedCategory.Q
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.neZero : ∀ (n : ℕ) [NeZero n] (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [IsCyclotomicExtension {n} A B] [IsDomain B], NeZero ↑n
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparated_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.QuasiSeparated f ↔
    autoParam (AlgebraicGeometry.QuasiCompact (CategoryTheory.Limits.pullback.diagonal f))
      AlgebraicGeometry.QuasiSeparated.quasiCompact_diagonal._autoParam
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.mk.inj : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {E : Type u_2} {inst_1 : NormedAddCommGroup E}
  {inst_2 : NormedSpace 𝕜 E} {H : Type u_3} {inst_3 : TopologicalSpace H} {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  {inst_4 : TopologicalSpace M} {inst_5 : ChartedSpace H M} {F : Type u_5} {inst_6 : NormedAddCommGroup F}
  {inst_7 : NormedSpace 𝕜 F} {n : WithTop ℕ∞} {V : M → Type u_6} {inst_8 : TopologicalSpace (Bundle.TotalSpace F V)}
  {inst_9 : (x : M) → TopologicalSpace (V x)} {inst_10 : FiberBundle F V} {toFun : (x : M) → V x}
  {contMDiff_toFun : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, toFun x⟩} {toFun_1 : (x : M) → V x}
  {contMDiff_toFun_1 : ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, toFun_1 x⟩},
  { toFun := toFun, contMDiff_toFun := contMDiff_toFun } = { toFun := toFun_1, contMDiff_toFun := contMDiff_toFun_1 } →
    toFun = toFun_1
-- Mathlib.Data.TypeVec
TypeVec.prod.fst.eq_1 : ∀ (n : ℕ) (α β : TypeVec.{u} n.succ) (i : Fin2 n), TypeVec.prod.fst i.fs = TypeVec.prod.fst i
-- Mathlib.Probability.Moments.SubGaussian
/-- **Hoeffding's lemma**: with respect to a probability measure `μ`, if `X` is a random variable
that has expectation zero and is almost surely in `Set.Icc a b` for some `a ≤ b`, then `X` has a
sub-Gaussian moment-generating function with parameter `((b - a) / 2) ^ 2`.  -/
ProbabilityTheory.hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ}
  [MeasureTheory.IsProbabilityMeasure μ] {a b : ℝ},
  AEMeasurable X μ →
    (∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b) →
      ∫ (x : Ω), X x ∂μ = 0 → ProbabilityTheory.HasSubgaussianMGF X ((‖b - a‖₊ / 2) ^ 2) μ
-- Mathlib.Analysis.Normed.Group.Basic
coe_nnnorm : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a : E), ↑‖a‖₊ = ‖a‖
-- Init.GetElem
_private.Init.GetElem.0.GetElem?.match_1.eq_2 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match none with
    | some e => h_1 e
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.instMvFunctorObj : {n : ℕ} → (P : MvPFunctor.{u} n) → MvFunctor ↑P
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.withCaching : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `iteratedFDerivWithin_add_apply`

---

The iterated derivative of the sum of two functions is the sum of the iterated derivatives.
 -/
fun_iteratedFDerivWithin_add_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {x : E} {i : ℕ} {f g : E → F},
  ContDiffWithinAt 𝕜 (↑i) f s x →
    ContDiffWithinAt 𝕜 (↑i) g s x →
      UniqueDiffOn 𝕜 s →
        x ∈ s →
          iteratedFDerivWithin 𝕜 i (fun i => f i + g i) s x =
            iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x
-- Mathlib.Order.Sublattice
Sublattice.prodEquiv_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L : Sublattice α) (M : Sublattice β)
  (x : { a // (fun x => x ∈ ↑L) a } × { b // (fun x => x ∈ ↑M) b }), (RelIso.symm (L.prodEquiv M)) x = ⟨(↑x.1, ↑x.2), ⋯⟩
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.denote_mkBEqCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput},
  ⟦assign, aig.mkBEqCached input⟧ =
    (⟦assign, { aig := aig, ref := input.lhs }⟧ == ⟦assign, { aig := aig, ref := input.rhs }⟧)
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetOneRangeSpecialLinearGroupGeneralLinearGroupMapGL : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S], (Matrix.SpecialLinearGroup.mapGL S).range.HasDetOne
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.toCWComplex_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) [h : Topology.RelCWComplex C ∅],
  Topology.CWComplex.instRelCWComplex C = h
-- Mathlib.Data.Finset.Sym
Finset.mem_sym_iff : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {n : ℕ} {m : Sym α n}, m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s
-- Mathlib.Data.Nat.Cast.Defs
Nat.cast_add_one : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] (n : ℕ), ↑(n + 1) = ↑n + 1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Inhabited α] {k k' : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k' (Std.Internal.List.modifyKey k f l) =
      if (k == k') = true then if Std.Internal.List.containsKey k l = true then k else default
      else Std.Internal.List.getKey! k' l
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.powerRevlex_k_eq_powerRevlex : ∀ (k₁ k₂ : ℕ), Lean.Grind.CommRing.powerRevlex_k k₁ k₂ = Lean.Grind.CommRing.powerRevlex k₁ k₂
-- Lean.Meta.Basic
/-- Pretty-print the given expression.  -/
Lean.Meta.ppExpr : Lean.Expr → Lean.MetaM Std.Format
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.prod_comp_prodMap : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_6}
  {N' : Type u_7} [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] [inst_4 : AddZeroClass P] (f : P →+ M)
  (g : P →+ N) (f' : M →+ M') (g' : N →+ N'), (f'.prodMap g').comp (f.prod g) = (f'.comp f).prod (g'.comp g)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instBoundedContinuousMapClass : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], BoundedContinuousMapClass (SchwartzMap E F) E F
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
AlgebraicGeometry.Scheme.instIsContinuousTopCatForgetToTopZariskiTopologyGrothendieckTopology : AlgebraicGeometry.Scheme.forgetToTop.IsContinuous AlgebraicGeometry.Scheme.zariskiTopology TopCat.grothendieckTopology
-- Mathlib.GroupTheory.Perm.Sign
/-- `signAux σ` is the sign of a permutation on `Fin n`, defined as the parity of the number of
pairs `(x₁, x₂)` such that `x₂ < x₁` but `σ x₁ ≤ σ x₂`  -/
Equiv.Perm.signAux : {n : ℕ} → Equiv.Perm (Fin n) → ℤˣ
-- Mathlib.Condensed.Module
/-- The free-forgetful adjunction for condensed abelian groups.  -/
Condensed.setAbAdjunction : Condensed.freeAb ⊣ Condensed.abForget
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instIsOpenImmersionMapSchemeLocallyRingedSpaceForgetToLocallyRingedSpace : ∀ {X Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.map f)
-- Mathlib.Data.List.Lattice
List.count_bagInter : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l₁ l₂ : List α},
  List.count a (l₁.bagInter l₂) = min (List.count a l₁) (List.count a l₂)
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.ContainsZero.exists_zero : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.ObjectProperty C} [self : P.ContainsZero],
  ∃ Z, CategoryTheory.Limits.IsZero Z ∧ P Z
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Given an ordered finpartition of `n+1`, with a leftmost atom different from `{0}`, remove `{0}`
from the atom that contains it, to form an ordered finpartition of `n`.  -/
OrderedFinpartition.eraseMiddle : {n : ℕ} → (c : OrderedFinpartition (n + 1)) → Set.range (c.emb 0) ≠ {0} → OrderedFinpartition n
-- Mathlib.Data.Nat.DvdSequence
IsDvdSequence.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : Dvd α] [inst_1 : CommMonoid β] {f g : α → β},
  IsDvdSequence f → IsDvdSequence g → IsDvdSequence (f * g)
-- Std.Http.Data.Body.Stream
/-- Sends a chunk, retrying if a select-mode consumer races and loses. If no consumer is ready,
installs the chunk as a pending producer and awaits acknowledgement from the receiver.
 -/
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.send' : Std.Http.Body.Stream → Std.Http.Chunk → Std.Async.Async Unit
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.liftAddHom_symm_apply_apply : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (F : (α →₀ M) →+ N)
  (x : α) (y : M), (Finsupp.liftAddHom.symm F x) y = F fun₀ | x => y
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ico_add_one_left_eq_Ioo : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] (a b : α), Finset.Ico (a + 1) b = Finset.Ioo a b
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.mul_rpow_of_nonneg : ∀ (x y : ENNReal) {z : ℝ}, 0 ≤ z → (x * y) ^ z = x ^ z * y ^ z
-- Mathlib.Algebra.Lie.Basis.Prod
/-- `LieAlgebra.Basis.prod` is equivalent to its left input algebra.  -/
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.prodEquivLeft : {ι₁ : Type u_1} →
  {ι₂ : Type u_2} →
    {L₁ : Type u_3} →
      {L₂ : Type u_4} →
        [inst : Finite ι₁] →
          [inst_1 : Finite ι₂] →
            (eι : ι₁ ≃ ι₂) →
              [inst_2 : LieRing L₁] →
                [inst_3 : LieRing L₂] →
                  {K : Type u_5} →
                    [inst_4 : Field K] →
                      [CharZero K] →
                        [inst_6 : LieAlgebra K L₁] →
                          [FiniteDimensional K L₁] →
                            {H₁ : LieSubalgebra K L₁} →
                              (b₁ : LieAlgebra.Basis ι₁ H₁) →
                                [inst_8 : LieAlgebra K L₂] →
                                  [FiniteDimensional K L₂] →
                                    {H₂ : LieSubalgebra K L₂} →
                                      (b₂ : LieAlgebra.Basis ι₂ H₂) →
                                        (Matrix.reindex eι eι) b₁.A = b₂.A →
                                          [LieAlgebra.IsSimple K L₂] → ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂) ≃ₗ⁅K⁆ L₁
-- Mathlib.NumberTheory.Real.Irrational
not_irrational_one : ¬Irrational 1
-- Mathlib.Algebra.Ring.Int.Defs
Int.cast_pow : ∀ {R : Type u_1} [inst : Ring R] (n : ℤ) (m : ℕ), ↑(n ^ m) = ↑n ^ m
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
/-- Returns the ring id for the given type if there is a `Ring` instance for it.
This function is invoked only when `getCommRingId?` returns `none`.
 -/
Lean.Meta.Grind.Arith.CommRing.getNonCommRingId? : Lean.Expr → Lean.Meta.Grind.GoalM (Option ℕ)
-- Mathlib.RingTheory.WittVector.Compare
WittVector.toZModPow.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (k : ℕ),
  WittVector.toZModPow p k = (TruncatedWittVector.zmodEquivTrunc p k).symm.toRingHom.comp (WittVector.truncate k)
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_le_of_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, 0 < n → n • x = 0 → addOrderOf x ≤ n
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.bot_eq_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {B : C}, ⊥ = CategoryTheory.Subobject.mk 0
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- `P` as a morphism property respects isomorphisms  -/
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.respectsIso : ∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty} [self : P.IsLocal], P.toProperty.RespectsIso
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isIso_of_isEmpty : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsEmpty ↥Y], CategoryTheory.IsIso f
-- Mathlib.Analysis.CStarAlgebra.Multiplier
DoubleCentralizer.instNormedAlgebra : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → NormedAlgebra 𝕜 (DoubleCentralizer 𝕜 A)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Let `f` be a measurable function integrable on `a..b`. The function `(u, v) ↦ ∫ x in u..v, f x`
has derivative `(u, v) ↦ v • cb - u • ca` within `s × t` at `(a, b)`, where
`s ∈ {Iic a, {a}, Ici a, univ}` and `t ∈ {Iic b, {b}, Ici b, univ}` provided that `f` tends to `ca`
and `cb` almost surely at the filters `la` and `lb` from the following table.

| `s`     | `la`     | `t`     | `lb`     |
| ------- | ----     | ---     | ----     |
| `Iic a` | `𝓝[≤] a` | `Iic b` | `𝓝[≤] b` |
| `Ici a` | `𝓝[>] a` | `Ici b` | `𝓝[>] b` |
| `{a}`   | `⊥`      | `{b}`   | `⊥`      |
| `univ`  | `𝓝 a`    | `univ`  | `𝓝 b`    |
 -/
intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {ca cb : E}
  {la lb : Filter ℝ} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) la]
      [intervalIntegral.FTCFilter b (nhdsWithin b t) lb],
      StronglyMeasurableAtFilter f la MeasureTheory.volume →
        StronglyMeasurableAtFilter f lb MeasureTheory.volume →
          Filter.Tendsto f (la ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds ca) →
            Filter.Tendsto f (lb ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds cb) →
              HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x)
                ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight cb - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t)
                (a, b)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeffEquiv_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (self : AddMonoidAlgebra R M),
  AddMonoidAlgebra.coeffEquiv self = self.coeff
-- Std.Async.Basic
/-- Create an `ETask` that resolves to the pure value of the promise `x`. If the promise gets dropped then it
panics.
 -/
Std.Async.ETask.ofPurePromise : {α ε : Type} → IO.Promise α → Std.Async.ETask ε α
-- Aesop.Index.Basic
Aesop.IndexingMode.unindexed : Aesop.IndexingMode
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_addEquiv_lpPiLp : ∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} [inst_1 : Finite α]
  (f : ↥(lp E p)), (AddEquiv.lpPiLp f).ofLp = ↑f
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_entry_le_entrywise_sup_norm : ∀ {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : SeminormedAddCommGroup α] (A : Matrix m n α) {i : m} {j : n}, ‖A i j‖ ≤ ‖A‖
-- Mathlib.Data.Finsupp.Fin
Finsupp.tail.eq_1 : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] (s : Fin (n + 1) →₀ M), s.tail = Finsupp.equivFunOnFinite.symm (Fin.tail ⇑s)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addX_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R) (u v : R),
  W'.addX (u • P) (v • Q) = (u * v) ^ 2 * W'.addX P Q