mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.SuccPred.Basic
/-- Proof of interaction between `succ` and maximal element  -/
SuccOrder.max_of_succ_le : ∀ {α : Type u_3} {inst : Preorder α} [self : SuccOrder α] {a : α}, SuccOrder.succ a ≤ a → IsMax a
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderIso.setOfPredMinimalIsoSetOfPredMaximal`.

---

If two sets are antitonically order isomorphic, their minimals/maximals are too.  -/
OrderIso.setOfMinimalIsoSetOfMaximal : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        {s : Set α} →
          {t : Set β} →
            ↑s ≃o (↑t)ᵒᵈ → ↑{x | Minimal (fun x => x ∈ s) x} ≃o ↑{x | Maximal (fun x => x ∈ t) (OrderDual.ofDual x)}
-- Mathlib.Analysis.Normed.Group.Basic
enorm_multisetSum_le : ∀ {ε : Type u_9} [inst : TopologicalSpace ε] [inst_1 : ESeminormedAddCommMonoid ε] (m : Multiset ε),
  ‖m.sum‖ₑ ≤ (Multiset.map (fun x => ‖x‖ₑ) m).sum
-- Mathlib.Topology.Inseparable
specializes_iff_clusterPt : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ ClusterPt y (pure x)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piFunctor_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] (X : C)
  (α : Type wᵒᵖ), (CategoryTheory.Limits.piFunctor.obj X).obj α = ∏ᶜ fun t => X
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.total.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K L : HomologicalComplex₂ C c₁ c₂}
  (φ : K ⟶ L) (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : K.HasTotal c₁₂] [inst_5 : L.HasTotal c₁₂],
  (HomologicalComplex.forget C c₁₂).map (HomologicalComplex₂.total.map φ c₁₂) =
    CategoryTheory.GradedObject.mapMap (HomologicalComplex₂.toGradedObjectMap φ) (c₁.π c₂ c₁₂)
-- Mathlib.Order.Hom.Basic
OrderEmbedding.ofIsEmpty_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : IsEmpty α] (a : α),
  OrderEmbedding.ofIsEmpty a = isEmptyElim a
-- Mathlib.Data.DFinsupp.BigOperators
/-- The `DFinsupp` version of `Finsupp.liftAddHom_singleAddHom`  -/
DFinsupp.liftAddHom_singleAddHom : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)],
  DFinsupp.liftAddHom (DFinsupp.singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)
-- Mathlib.Logic.Equiv.Sum
Equiv.prodSumDistrib_apply_right : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α) (c : γ),
  (Equiv.prodSumDistrib α β γ) (a, Sum.inr c) = Sum.inr (a, c)
-- Init.Data.Vector.Basic
Vector.zip : {α : Type u_1} → {n : ℕ} → {β : Type u_2} → Vector α n → Vector β n → Vector (α × β) n
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_two_mul : ∀ (x : ℝ), Real.cos (2 * x) = 2 * Real.cos x ^ 2 - 1
-- Init.Data.Option.Lemmas
Option.filter_filter : ∀ {α : Type u_1} {q p : α → Bool} {o : Option α},
  Option.filter q (Option.filter p o) = Option.filter (fun x => p x && q x) o
-- Mathlib.CategoryTheory.SingleObj
MonCat.toCat.eq_1 : MonCat.toCat =
  { obj := fun x => CategoryTheory.Cat.of (CategoryTheory.SingleObj ↑x),
    map := fun {x y} f => ((CategoryTheory.SingleObj.mapHom ↑x ↑y) (MonCat.Hom.hom f)).toCatHom,
    map_id := MonCat.toCat._proof_1, map_comp := @MonCat.toCat._proof_2 }
-- Mathlib.Order.Heyting.Basic
sup_compl_le_himp : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, b ⊔ aᶜ ≤ a ⇨ b
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.usedTheorems : Lean.Meta.Simp.State → Lean.Meta.Simp.UsedSimps
-- Mathlib.CategoryTheory.Triangulated.Adjunction
/-- Constructor for `Adjunction.IsTriangulated`.
 -/
CategoryTheory.Adjunction.IsTriangulated.mk' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) [inst_12 : F.CommShift ℤ] [inst_13 : G.CommShift ℤ] [adj.CommShift ℤ] [F.IsTriangulated],
  adj.IsTriangulated
-- Mathlib.Data.Set.Countable
/-- A set `s : Set α` is countable if and only if there exists a function `α → ℕ` injective
on `s`.  -/
Set.countable_iff_exists_injOn : ∀ {α : Type u} {s : Set α}, s.Countable ↔ ∃ f, Set.InjOn f s
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Additive submonoids of an additive monoid `A` are isomorphic to
multiplicative submonoids of `Multiplicative A`.  -/
AddSubmonoid.toSubmonoid : {A : Type u_4} → [inst : AddZeroClass A] → AddSubmonoid A ≃o Submonoid (Multiplicative A)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If `f` is meromorphic on a compact set `U` and `V ⊆ U`, then the divisor of `f` on `V` has finite
support.
 -/
MeromorphicOn.divisor_support_finite_of_subset : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {V : Set 𝕜},
  MeromorphicOn f U → IsCompact U → V ⊆ U → (MeromorphicOn.divisor f V).support.Finite
-- Mathlib.Algebra.Order.Floor.Ring
natCast_ceil_eq_intCast_ceil : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R}, 0 ≤ a → ↑⌈a⌉₊ = ↑⌈a⌉
-- Mathlib.LinearAlgebra.Vandermonde
/-- A matrix with rows all having the form `[b^(n-1), a * b^(n-2), ..., a ^ (n-1)]`  -/
Matrix.rectVandermonde : {R : Type u_1} → [CommRing R] → {α : Type u_3} → (α → R) → (α → R) → (n : ℕ) → Matrix α (Fin n) R
-- Mathlib.Data.Sigma.Lex
Sigma.Lex.mono_right : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s₁ s₂ : (i : ι) → α i → α i → Prop},
  (∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) → ∀ {a b : (i : ι) × α i}, Sigma.Lex r s₁ a b → Sigma.Lex r s₂ a b
-- Mathlib.Order.Heyting.Hom
CoheytingHom.instInhabited : {α : Type u_2} → [inst : CoheytingAlgebra α] → Inhabited (CoheytingHom α α)
-- Init.Data.Nat.Basic
Nat.sub_zero : ∀ (n : ℕ), n - 0 = n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_sub_right : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (d : ℝ),
  ∫ (x : ℝ) in a..b, f (x - d) = ∫ (x : ℝ) in a - d..b - d, f x
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_integral_add : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] ⦃f g : β × γ → E⦄,
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable g ((κ.compProd η) a) →
      ∫ (x : β), ∫ (y : γ), f (x, y) + g (x, y) ∂η (a, x) ∂κ a =
        ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a + ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.adjunction_left_triangle : ∀ (P : TopCat → Prop) [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_3 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  [inst_4 : CompHausLike.HasExplicitFiniteCoproducts P] (X : Type (max u w)),
  CategoryTheory.CategoryStruct.comp
      (CompHausLike.LocallyConstant.functorToPresheaves.map ((CompHausLike.LocallyConstant.unit P hs).app X))
      ((CompHausLike.LocallyConstant.counit P hs).app ((CompHausLike.LocallyConstant.functor P hs).obj X)).hom =
    CategoryTheory.CategoryStruct.id (CompHausLike.LocallyConstant.functorToPresheaves.obj X)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
CategoryTheory.Limits.PreservesLimitsOfShape.overPost : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {X : C} {F : CategoryTheory.Functor C D}
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.WithTerminal J) F],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Over.post F)
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- `B.F` agrees with the L-series of `zetaMul χ` on `1 < s.re`.  -/
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.F_eq_LSeries : ∀ {N : ℕ} [inst : NeZero N] (B : DirichletCharacter.BadChar✝ N) {s : ℂ},
  1 < s.re → DirichletCharacter.BadChar.F✝ B s = LSeries (⇑(DirichletCharacter.BadChar.χ✝ B).zetaMul) s
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixedPoints_le_of_le : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H H' : Subgroup G) [inst_5 : SMulCommClass G K L],
  H ≤ H' → FixedPoints.intermediateField ↥H' ≤ FixedPoints.intermediateField ↥H
-- Mathlib.Analysis.Convex.StdSimplex
/-- The standard one-dimensional simplex in `ℝ² = Fin 2 → ℝ`
is homeomorphic to the unit interval.  -/
stdSimplexHomeomorphUnitInterval : ↑(stdSimplex ℝ (Fin 2)) ≃ₜ ↑unitInterval
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.add_apply : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] [inst_7 : IsOrderedAddMonoid E₂] (f g : E₁ →ₚ[R] E₂) (x : E₁), (f + g) x = f x + g x
-- Init.Data.List.Nat.Basic
List.getElem?_intersperse : ∀ {α : Type u_1} {l : List α} {sep : α} {i : ℕ},
  (List.intersperse sep l)[i]? = if i % 2 = 0 then l[i / 2]? else if i < 2 * l.length - 1 then some sep else none
-- Mathlib.Geometry.Manifold.Submersion
_private.Mathlib.Geometry.Manifold.Submersion.0.Manifold.IsSubmersionAt.eq_1 : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] (I : ModelWithCorners 𝕜 E H)
  (J : ModelWithCorners 𝕜 E'' G) {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N)
  (x : M), Manifold.IsSubmersionAt I J n f x = ∃ F x_1 x_2, Manifold.IsSubmersionAtOfComplement F I J n f x
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.IsGaussian.integrable_dual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  (μ : MeasureTheory.Measure E) [ProbabilityTheory.IsGaussian μ] (L : StrongDual ℝ E), MeasureTheory.Integrable (⇑L) μ
-- Mathlib.Combinatorics.KatonaCircle
Numbering.prefixed.eq_1 : ∀ {X : Type u_1} [inst : Fintype X] [inst_1 : DecidableEq X] (s : Finset X), Numbering.prefixed s = {f | f.IsPrefix s}
-- Mathlib.Data.Set.Finite.Basic
Finite.Set.finite_sep : ∀ {α : Type u} (s : Set α) (p : α → Prop) [Finite ↑s], Finite ↑{a | a ∈ s ∧ p a}
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.inter_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {R S : CategoryTheory.Sieve X} {Y : C} (f : Y ⟶ X),
  (R ⊓ S).arrows f ↔ R.arrows f ∧ S.arrows f
-- Init.Data.Range.Polymorphic.Basic
Std.Ric.mem_iff : ∀ {α : Type u} {r : Std.Ric α} {a : α} [inst : LE α], a ∈ r ↔ a ≤ r.upper
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k a : α} {v : β}, (t.insertIfNew k v)[a]! = if cmp k a = Ordering.eq ∧ k ∉ t then v else t[a]!
-- Init.Data.Float.Float
/-- Checks whether a floating-point number is a positive or negative infinite number, but not a finite
number or `NaN`.

This function has a logical model in terms of `Float.Model`. It is compiled to the C operator `isinf`.
 -/
Float.isInf : Float → Bool
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOnFilter.prodMk : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α} {ι' : Type u_5} {β' : Type u_6} [inst_1 : UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'}
  {q : Filter ι'},
  TendstoUniformlyOnFilter F f p p' →
    TendstoUniformlyOnFilter F' f' q p' →
      TendstoUniformlyOnFilter (fun i a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ q) p'
-- Mathlib.Algebra.Group.Action.Defs
mul_smul_one : ∀ {M : Type u_9} {N : Type u_10} [inst : MulOneClass N] [inst_1 : SMul M N] [SMulCommClass M N N] (x : M) (y : N),
  y * x • 1 = x • y
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.Mon_tensor_mul_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : C) [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul))
        (CategoryTheory.MonoidalCategoryStruct.tensorObj M N))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
            (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_mul_iff_one_lt_left' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LT α] [MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b : α},
  a < b * a ↔ 1 < b
-- Mathlib.Algebra.Notation.Defs
dite_div_dite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Div α] (a : P → α) (b : ¬P → α) (c : P → α) (d : ¬P → α),
  ((if h : P then a h else b h) / if h : P then c h else d h) = if h : P then a h / c h else b h / d h
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.smul_comp : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (a : A) (f : σ.IntertwiningMap τ) (g : ρ.IntertwiningMap σ), (a • f).comp g = a • f.comp g
-- Mathlib.Data.Vector.Basic
List.Vector.get_append_cons_zero : ∀ {α : Type u_1} {m n : ℕ} {x : α} (xs : List.Vector α n) (ys : List.Vector α m), (x ::ᵥ xs ++ ys).get 0 = x
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.indep : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → M.Indep B
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- See `finiteDimensional_iSup_of_finset'` for a stronger version,
that was the one used in mathlib3.  -/
IntermediateField.finiteDimensional_iSup_of_finset : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type u_5}
  {t : ι → IntermediateField K L} {s : Finset ι} [∀ (i : ι), FiniteDimensional K ↥(t i)],
  FiniteDimensional K ↥(⨆ i ∈ s, t i)
-- Mathlib.Analysis.Convex.Body
/-- **Alias** of `ConvexBody.hausdorffEDist_ne_top`. -/
ConvexBody.hausdorffEdist_ne_top : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] {K L : ConvexBody V},
  Metric.hausdorffEDist ↑K ↑L ≠ ⊤
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.iUnion_compl : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : Finite ι] (π : BoxIntegral.Prepartition I),
  π.compl.iUnion = ↑I \ π.iUnion
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instEpiHomologyπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  CategoryTheory.Epi (K.homologyπ i)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coe_truncLTLinearMap : ∀ {Γ : Type u_1} (R : Type u_3) {V : Type u_6} [inst : PartialOrder Γ] [inst_1 : Semiring R] [inst_2 : AddCommMonoid V]
  [inst_3 : Module R V] [inst_4 : DecidableLT Γ] (c : Γ), ⇑(HahnSeries.truncLTLinearMap R c) = ⇑(HahnSeries.truncLT c)
-- Mathlib.Algebra.Group.Torsion
pow_eq_one_iff_left : ∀ {M : Type u_1} [inst : Monoid M] [IsMulTorsionFree M] {n : ℕ} {a : M}, n ≠ 0 → (a ^ n = 1 ↔ a = 1)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.subNegZeroMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → SubNegZeroMonoid (f i)],
  Pi.subNegZeroMonoid = { toSubNegMonoid := Pi.subNegMonoid, neg_zero := ⋯ }
-- Init.WF
PSigma.lexNdep : {α : Sort u} → {β : Sort v} → (α → α → Prop) → (β → β → Prop) → (_ : α) ×' β → (_ : α) ×' β → Prop
-- Init.Data.Nat.Basic
Nat.pred_lt : ∀ {n : ℕ}, n ≠ 0 → n.pred < n
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_one : Ordinal.card 1 = 1
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α},
  ∅[a]? = none
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_congr : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f₁ f₂ : M} {g₁ g₂ : R}
  {U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)} {hu : U ≤ PrimeSpectrum.basicOpen g₁},
  f₁ = f₂ →
    ∀ (hg : g₁ = g₂),
      AlgebraicGeometry.StructureSheaf.const f₁ g₁ U hu = AlgebraicGeometry.StructureSheaf.const f₂ g₂ U ⋯
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
interior, and `f''` is nonpositive on the interior, then `f` is concave on `D`.  -/
concaveOn_of_hasDerivWithinAt2_nonpos : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f f' f'' : ℝ → ℝ},
      ContinuousOn f D →
        (∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) →
          (∀ x ∈ interior D, HasDerivWithinAt f' (f'' x) (interior D) x) →
            (∀ x ∈ interior D, f'' x ≤ 0) → ConcaveOn ℝ D f
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instContinuousFourierInv : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F], ContinuousFourierInv (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.Algebra.MonoidAlgebra.Support
MonoidAlgebra.support_coeff_mul_single_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] [inst_2 : DecidableEq G] (x : MonoidAlgebra k G)
  (r : k) (a : G), (x * MonoidAlgebra.single a r).coeff.support ⊆ Finset.image (fun x => x * a) x.coeff.support
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.hasDerivAt_sin : ∀ (x : ℝ), HasDerivAt Real.sin (Real.cos x) x
-- Mathlib.RingTheory.RegularLocalRing.Defs
IsRegularRing.of_ringEquiv : ∀ {R : Type u_1} [inst : CommRing R] {R' : Type u_2} [inst_1 : CommRing R'] (e : R ≃+* R') [IsRegularRing R],
  IsRegularRing R'
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for monotonicity of multiplication on the left,
namely `b₁ ≤ b₂ → a * b₁ ≤ a * b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedMonoid`.  -/
MulLeftMono : (M : Type u_1) → [Mul M] → [LE M] → Prop
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.limitCone_cone_pt : ∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α), (CategoryTheory.Limits.CompleteLattice.limitCone F).cone.pt = iInf F.obj
-- Mathlib.RingTheory.EssentialFiniteness
RingHom.EssFiniteType.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.EssFiniteType = Algebra.EssFiniteType R S
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_two : ↑2 = 2
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.inv_single : ∀ {R : Type u_2} [inst : Semifield R] {a b : R}, a⁻¹ = b → (a + 0)⁻¹ = b + 0
-- Mathlib.Order.CompleteBooleanAlgebra
_private.Mathlib.Order.CompleteBooleanAlgebra.0.Order.Coframe.MinimalAxioms.sup_sInf_eq : ∀ {α : Type u} (s : Set α) (a : α) [inst : CompleteLattice α],
  Order.Coframe.MinimalAxioms α → a ⊔ sInf s = ⨅ b ∈ s, a ⊔ b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k a : α},
  (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Values of Hurwitz zeta functions at (strictly) negative integers.

TODO: This formula is also correct for `k = 0`; but our current proof does not work in this
case.  -/
HurwitzZeta.hurwitzZeta_neg_nat : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.hurwitzZeta (↑x) (-↑k) =
        -1 / (↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (k + 1)))
-- Mathlib.RingTheory.Coalgebra.TensorProduct
TensorProduct.instIsCocomm : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid B] [inst_4 : Algebra R S] [inst_5 : Module R A]
  [inst_6 : Module S A] [inst_7 : Module R B] [inst_8 : IsScalarTower R S A] [inst_9 : Coalgebra R B]
  [inst_10 : Coalgebra S A] [Coalgebra.IsCocomm S A] [Coalgebra.IsCocomm R B],
  Coalgebra.IsCocomm S (TensorProduct R A B)