mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.min_le_mk_mul : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (a b : M),
  min (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b) ≤ MulArchimedeanClass.mk (a * b)
-- Std.Http.Data.URI.Encoding
/-- Attempts to create an encoded path segment from raw bytes.
 -/
Std.Http.URI.EncodedSegment.ofByteArray? : ByteArray → Option Std.Http.URI.EncodedSegment
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.toMonoidWithZeroHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β], Function.Injective OrderMonoidWithZeroHom.toMonoidWithZeroHom
-- Mathlib.Analysis.RCLike.Basic
RCLike.im_le_neg_norm_iff_eq_neg_I_mul_norm : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, RCLike.im z ≤ -‖z‖ ↔ z = -(RCLike.I * ↑‖z‖)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.mk_zpow : ∀ {M : Type u_1} [inst : DivInvMonoid M] (a : M) (n : ℤ), DomMulAct.mk (a ^ n) = DomMulAct.mk a ^ n
-- Init.Internal.Order.Lemmas
Lean.Order.Array.monotone_mapFinIdxM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (xs : Array α)
  (f : γ → (i : ℕ) → α → i < xs.size → m β), Lean.Order.monotone f → Lean.Order.monotone fun x => xs.mapFinIdxM (f x)
-- Std.Tactic.Do.Syntax
Lean.Parser.Category.mcasesPat : Lean.Parser.Category
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The identity map of the `SubMulAction` of the `fixingSubgroup`
into the ambient set, as an equivariant map.  -/
SubMulAction.ofFixingSubgroup_equivariantMap : (M : Type u_1) →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] → (s : Set α) → ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[⇑(fixingSubgroup M s).subtype] α
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.map_objEquiv_op_apply : ∀ {X : SSet} {n : SimplexCategory} (x : X.obj (Opposite.op n)) {m : SimplexCategoryᵒᵖ}
  (y : (SSet.stdSimplex.obj n).obj m),
  (CategoryTheory.ConcreteCategory.hom (X.map (SSet.stdSimplex.objEquiv y).op)) x =
    (CategoryTheory.ConcreteCategory.hom ((SSet.yonedaEquiv.symm x).app m)) y
-- Mathlib.Analysis.RCLike.Basic
RCLike.instMulPosReflectLE : ∀ {K : Type u_1} [inst : RCLike K], MulPosReflectLE K
-- Mathlib.Data.Finset.Finsupp
Finsupp.pi.eq_1 : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (f : ι →₀ Finset α), f.pi = f.support.finsupp ⇑f
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.toCompl_apply : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [inst_2 : IsUniformAddGroup α] (a : α),
  UniformSpace.Completion.toCompl a = ↑a
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.mul_empty : ∀ {α : Type u} {m' : Type uₘ} {n' : Type uₙ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n']
  (A : Matrix m' n' α) (B : Matrix n' (Fin 0) α), A * B = Matrix.of fun x => ![]
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_congr : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {a b : α}, (a == b) = true → m[a]! = m[b]!
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.ushiftRight_zero' : ∀ {w w' : ℕ} (n : BitVec w), n >>> 0#w' = n
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.unorderedListIndicator : Lean.Doc.Parser.UnorderedListType → Lean.Parser.ParserFn
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.UTLocal.ut.sizeOf_spec : sizeOf Std.Time.TimeZone.UTLocal.ut = 1
-- Mathlib.Topology.Constructions.SumProd
isClosed_range_inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsClosed (Set.range Sum.inr)
-- Mathlib.Algebra.Order.Hom.Basic
/-- The map is invariant under inversion of its argument.  -/
GroupSeminormClass.map_inv_eq_map : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Group α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : GroupSeminormClass F α β] (f : F) (a : α), f a⁻¹ = f a
-- Mathlib.Analysis.Calculus.MeanValue
/-- If two continuous functions on `[a, b]` have the same right derivative and are equal at `a`,
then they are equal everywhere on `[a, b]`.  -/
eq_of_has_deriv_right_eq : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {f' g : ℝ → E},
  (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt g (f' x) (Set.Ici x) x) →
      ContinuousOn f (Set.Icc a b) → ContinuousOn g (Set.Icc a b) → f a = g a → ∀ y ∈ Set.Icc a b, f y = g y
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.mkD_eq_self : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : Zero X] {f g : ContinuousMapZero X R}, ContinuousMapZero.mkD (⇑f) g = f
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.pincerRecursion.match_1.splitter : (motive : ℕ → ℕ → Sort u_1) →
  (x x_1 : ℕ) →
    ((m : ℕ) → motive m 0) →
      ((n : ℕ) → (n = 0 → False) → motive 0 n) → ((n n_1 : ℕ) → motive n.succ n_1.succ) → motive x x_1
-- Mathlib.Data.Set.Image
Subtype.coe_image_univ : ∀ {α : Type u_1} (s : Set α), Subtype.val '' Set.univ = s
-- Mathlib.Algebra.Ring.Ext
NonUnitalCommSemiring.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : NonUnitalCommSemiring R⦄, HAdd.hAdd = HAdd.hAdd → HMul.hMul = HMul.hMul → inst₁ = inst₂
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsWide.mk : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  (∀ (c : C), CategoryTheory.CategoryStruct.id c ∈ S.arrows c c) → S.IsWide
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_fun_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {f : α → β × γ}, Measurable f ↔ (Measurable fun a => (f a).1) ∧ Measurable fun a => (f a).2
-- Lean.Compiler.ExternAttr
Lean.ExternEntry.standard.sizeOf_spec : ∀ (backend : Lean.Name) (fn : String), sizeOf (Lean.ExternEntry.standard backend fn) = 1 + sizeOf backend + sizeOf fn
-- Mathlib.RingTheory.Ideal.Nonunits
Submonoid.mem_nonunits_iff : ∀ {α : Type u_2} {C : Type u_4} [inst : SetLike C α] [inst_1 : Group α] [inst_2 : SubmonoidClass C α] {S : C} {a : ↥S},
  a ∈ nonunits ↥S ↔ (↑a)⁻¹ ∉ S
-- Mathlib.RingTheory.Algebraic.Defs
/-- An algebra is algebraic if all its elements are algebraic.  -/
Algebra.IsAlgebraic : (R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : Ring A] → [Algebra R A] → Prop
-- Mathlib.Topology.Closure
closure_inter_open_nonempty_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen t → ((closure s ∩ t).Nonempty ↔ (s ∩ t).Nonempty)
-- Mathlib.Combinatorics.Quiver.Push
Quiver.instPush : {V : Type u_1} → [Quiver V] → {W : Type u_2} → (σ : V → W) → Quiver (Quiver.Push σ)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mker_prod_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {M' : Type u_5} {N' : Type u_6}
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ N) (g : M' →+ N'),
  AddMonoidHom.mker (f.prodMap g) = (AddMonoidHom.mker f).prod (AddMonoidHom.mker g)
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMap.toFun_eq_coe : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (f : AddConstMap G H a b), f.toFun = ⇑f
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `c < b`, the point `(c, f c)` is non-strictly above the
segment `[(a, f a), (b, f b)]` if and only if `slope f c b ≤ slope f a b`.  -/
lineMap_le_map_iff_slope_le_slope_right : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module k E] [IsStrictOrderedModule k E]
  [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  0 < (1 - r) * (b - a) →
    ((AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔
      slope f ((AffineMap.lineMap a b) r) b ≤ slope f a b)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_isColimit₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).isColimit₁ =
    CategoryTheory.Limits.coproductIsCoproduct fun i => A i.i
-- Init.Data.List.ToArray
List.eraseIdx_toArray : ∀ {α : Type u_1} (l : List α) (i : ℕ) (h : i < l.toArray.size), l.toArray.eraseIdx i h = (l.eraseIdx i).toArray
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.merge.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (xs : List α) (h_1 : (ys : List α) → motive [] ys)
  (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (xs = [] → False) →
    (match xs, [] with
      | [], ys => h_1 ys
      | xs, [] => h_2 xs
      | x :: xs, y :: ys => h_3 x xs y ys) =
      h_2 xs
-- Batteries.Data.List.Lemmas
List.dropSuffix?_nil : ∀ {α : Type u_1} [inst : BEq α] {s : List α}, s.dropSuffix? [] = some s
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.sections.mk.sizeOf_spec : ∀ {J : CategoryTheory.Limits.MulticospanShape} {I : CategoryTheory.Limits.MulticospanIndex J (Type u)}
  (val : (i : J.L) → I.left i)
  (property :
    ∀ (r : J.R),
      (CategoryTheory.ConcreteCategory.hom (I.fst r)) (val (J.fst r)) =
        (CategoryTheory.ConcreteCategory.hom (I.snd r)) (val (J.snd r))),
  sizeOf { val := val, property := property } = 1
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.instIsPreorderIsContained : ∀ {α : Type u_4}, IsPreorder (SimpleGraph α) SimpleGraph.IsContained
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso_hom_app_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Functor C (CategoryTheory.Mon D)) (X_1 : C),
  ((CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.counitIso.hom.app X).app X_1).hom =
    CategoryTheory.CategoryStruct.id (X.obj X_1).X
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.whiskeringRight_preservesLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [CategoryTheory.Limits.PreservesLimitsOfShape J F],
  CategoryTheory.Limits.PreservesLimitsOfShape J ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.prod_const' : ∀ (ι : Type u) (a : Cardinal.{u}), (Cardinal.prod fun x => a) = a ^ Cardinal.mk ι
-- Init.Data.String.Basic
String.Slice.Pos.nextn.induct_unfolding : ∀ {s : String.Slice} (motive : s.Pos → ℕ → s.Pos → Prop),
  (∀ (p : s.Pos), motive p 0 p) →
    (∀ (p : s.Pos) (n : ℕ) (h : p ≠ s.endPos),
        motive (p.next h) n ((p.next h).nextn n) → motive p n.succ ((p.next h).nextn n)) →
      (∀ (p : s.Pos) (n : ℕ), ¬p ≠ s.endPos → motive p n.succ p) → ∀ (p : s.Pos) (n : ℕ), motive p n (p.nextn n)
-- Mathlib.Algebra.Order.Hom.Monoid
/-- For two ordered monoid morphisms `f` and `g`, their product is the ordered monoid morphism
sending `a` to `f a * g a`.  -/
OrderMonoidHom.instMulOfIsOrderedMonoid : {α : Type u_2} →
  {β : Type u_3} →
    [inst : CommMonoid α] →
      [inst_1 : Preorder α] → [inst_2 : CommMonoid β] → [inst_3 : Preorder β] → [IsOrderedMonoid β] → Mul (α →*o β)
-- Mathlib.Algebra.Free
FreeAddSemigroup.instDecidableEq.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (x x_1 : FreeAddSemigroup α),
  x.instDecidableEq x_1 = decidable_of_iff' (x.head = x_1.head ∧ x.tail = x_1.tail) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.toLinearOrder_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  (I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C) [inst_1 : LinearOrder ι]
  (j : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).L), I.toLinearOrder.fst j = I.fst ↑j
-- Mathlib.Probability.Distributions.Exponential
/-- A negative exponential function is integrable on intervals in `R≥0`  -/
ProbabilityTheory.exp_neg_integrableOn_Ioc : ∀ {b x : ℝ}, 0 < b → MeasureTheory.IntegrableOn (fun x => Real.exp (-(b * x))) (Set.Ioc 0 x) MeasureTheory.volume
-- Init.Data.List.Lemmas
List.insert.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α) (l : List α), List.insert a l = if l.contains a = true then l else a :: l
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_maxKey?_iff_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  (Std.Internal.List.maxKey? l).isSome = true ↔ l.isEmpty = false
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp.instBraided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            [inst_4 : CategoryTheory.BraidedCategory C] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (F : CategoryTheory.Functor C D) → [inst_6 : F.Braided] → F.mapAddGrp.Braided
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.forget_map : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (f : A ⟶ B),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget (CommAlgCat R)).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The image of a subobject classifier under an equivalence of categories is a subobject classifier.
 -/
CategoryTheory.Subobject.Classifier.ofEquivalence : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        CategoryTheory.Subobject.Classifier C → (C ≌ D) → CategoryTheory.Subobject.Classifier D
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_monadLift_trans_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m n o : Type u → Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : (α : Type u) → Std.Internal.Do.WP (o α) α Pred EPred]
  {α : Type u} {post : α → Pred} {epost : EPred} [inst_3 : MonadLift n o] [inst_4 : MonadLiftT m n] (x : m α),
  Std.Internal.Do.wp (monadLift x) post epost = Std.Internal.Do.wp (MonadLift.monadLift (monadLift x)) post epost
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_mul_eq_iff : ∀ {F : Type u} [inst : Field F] (f g : Polynomial F),
  (f * g).natSepDegree = f.natSepDegree + g.natSepDegree ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g
-- Mathlib.Data.Seq.Computation
/-- bisimilarity relation  -/
_private.Mathlib.Data.Seq.Computation.0.Computation.«term_~_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.tmul_one_tmul_one_tmul : ∀ (R : Type u_3) (A : Type u_4) (B : Type u_5) (C : Type u_6) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (x : A) (y : C), x ⊗ₜ[R] 1 ⊗ₜ[A] (1 ⊗ₜ[R] y) = 1 ⊗ₜ[A] (x ⊗ₜ[R] y)
-- Lean.Parser.Syntax
/-- `infixl:prec "op" => f` is equivalent to `notation:prec x:prec "op" y:prec1 => f x y`, where `prec1 := prec + 1`.
 -/
Lean.Parser.Command.infixl : Lean.Parser.Parser
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_rfl : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x : R}, x ≤ᵥ x
-- Mathlib.RingTheory.Ideal.GoingDown
/-- [Stacks Tag 00HX](https://stacks.math.columbia.edu/tag/00HX) -/
Algebra.HasGoingDown.trans : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_5)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] [Algebra.HasGoingDown R S]
  [Algebra.HasGoingDown S T], Algebra.HasGoingDown R T
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_X : ∀ {R : Type u_1} [inst : Semiring R] (k : ℕ), 1 < k → (Polynomial.hasseDeriv k) Polynomial.X = 0
-- Mathlib.SetTheory.Ordinal.Notation
ONote.instInhabited : Inhabited ONote
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a unital magma inherits a unital magma structure.  -/
SubmonoidClass.toMulOneClass : {M : Type u_4} →
  [inst : MulOneClass M] → {A : Type u_5} → [inst_1 : SetLike A M] → [SubmonoidClass A M] → (S : A) → MulOneClass ↥S
-- Std.Http.Data.Status
/-- 502 Bad Gateway
 -/
Std.Http.Status.badGateway : Std.Http.Status
-- Mathlib.Order.WellQuasiOrder
Finite.wellQuasiOrdered : ∀ {α : Type u_1} (r : α → α → Prop) [Finite α] [Std.Refl r], WellQuasiOrdered r
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- Given an arbitrary function on a subset of sets, we can define the outer measure corresponding
to it (this is the unique maximal outer measure that is at most `m` on the domain of `m`).  -/
MeasureTheory.inducedOuterMeasure : {α : Type u_1} →
  {P : Set α → Prop} → (m : (s : Set α) → P s → ENNReal) → (P0 : P ∅) → m ∅ P0 = 0 → MeasureTheory.OuterMeasure α
-- Std.Internal.Do.Order.PreservesSup
/-- `upperAdjoint f b` is the least upper bound of `{x | f x ⊑ b}` by definition.  -/
Lean.Order.PreservesSup.upperAdjoint_spec : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (f : α → α) (b : α),
  Lean.Order.is_sup (fun x => Lean.Order.PartialOrder.rel (f x) b) (Lean.Order.PreservesSup.upperAdjoint f b)
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `(Σ i, X i) × Y` is homeomorphic to `Σ i, (X i × Y)`.  -/
Homeomorph.sigmaProdDistrib : {Y : Type u_2} →
  [inst : TopologicalSpace Y] →
    {ι : Type u_7} →
      {X : ι → Type u_8} → [inst_1 : (i : ι) → TopologicalSpace (X i)] → ((i : ι) × X i) × Y ≃ₜ (i : ι) × X i × Y
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.ofBijective_apply : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective ⇑f) (a : A₁),
  (AlgEquiv.ofBijective f hf) a = f a
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- Given a t-structure `t` on a pretriangulated category `C` and `n : ℤ`, this
is the `≤ n`-truncation functor. See also the natural transformation `truncLEι`.  -/
CategoryTheory.Triangulated.TStructure.truncLE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → ℤ → CategoryTheory.Functor C C
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.equivalence_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (x : ULift.{u₂, u₁} C),
  CategoryTheory.ULift.equivalence.counitIso.hom.app x =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ULift.downFunctor.comp CategoryTheory.ULift.upFunctor).obj x)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth.eq_def : ∀ (o : Ordinal.{u}), Cardinal.preBeth o = ⨆ a, 2 ^ Cardinal.preBeth ↑a
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.rec.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Sort u}
  (f : (a : M) → (b : ↥S) → p (Localization.mk a b))
  (H : ∀ {a c : M} {b d : ↥S} (h : (Localization.r S) (a, b) (c, d)), ⋯ ▸ f a b = f c d) (x : Localization S),
  Localization.rec f H x = Quot.rec (fun y => f y.1 y.2) ⋯ x
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalAux.d₂_eq' : ∀ {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 : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' →
    ∀ (i₁₂ : I₁₂),
      K.d₂ c₁₂ i₁ i₂ i₁₂ =
        c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
          CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂')
            (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂)
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.compl_bot : ∀ {α : Type u_1} [inst : LE α], ⊥.compl = ⊥
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
/-- The canonical `HomologyData` of a short complex `S` in an abelian category.  -/
CategoryTheory.ShortComplex.HomologyData.ofAbelian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex C) → S.HomologyData
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderiv_mul` -/
mvfderiv_fun_mul : ∀ {𝕜 : 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 g : M → 𝕜} {x : M},
  MDiffAt f x → MDiffAt g x → (d% fun i => f i * g i) x = f x • d% g x + g x • d% f x
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.isIntertwining_assoc : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Semiring 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)
  {f : ρ.IntertwiningMap σ} (g : G) (l : U →ₗ[A] V), f.toLinearMap ∘ₗ ρ g ∘ₗ l = σ g ∘ₗ f.toLinearMap ∘ₗ l
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.maxKey!_modify_eq_maxKey! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).maxKey! = t.maxKey!
-- Mathlib.GroupTheory.OrderOfElement
sum_card_addOrderOf_eq_card_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {n : ℕ} [inst_1 : Fintype G] [inst_2 : DecidableEq G],
  n ≠ 0 → ∑ m ∈ n.divisors, {x | addOrderOf x = m}.card = {x | n • x = 0}.card
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- Given a 2-morphism between `f` and `g` in the free bicategory, we have the equality
`normalizeAux p f = normalizeAux p g`.
 -/
CategoryTheory.FreeBicategory.normalizeAux_congr : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (p : Quiver.Path a b) {f g : CategoryTheory.FreeBicategory.Hom b c}
  (η : f ⟶ g), CategoryTheory.FreeBicategory.normalizeAux p f = CategoryTheory.FreeBicategory.normalizeAux p g
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.homeomorphOfImageSubsetSource_symm_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  {s : Set X} {t : Set Y} (hs : s ⊆ e.source) (ht : ↑e '' s = t) (a : ↑t),
  (e.homeomorphOfImageSubsetSource hs ht).symm a = Set.MapsTo.restrict (↑e.symm) t s ⋯ a