mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.id_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B), (ContinuousAlgHom.id R B).comp f = f
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctor_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A] (M : A),
  (Φ.skyscraperSheafFunctor.obj M).obj = Φ.skyscraperPresheaf M
-- Mathlib.GroupTheory.OrderOfElement
/-- Every finite left cancellative additive monoid is an additive group.  -/
AddLeftCancelMonoid.addGroupOfFinite : {G : Type u_1} → [AddLeftCancelMonoid G] → [Finite G] → AddGroup G
-- Mathlib.Algebra.Group.Prod
Prod.instAddLeftCancelSemigroup : {G : Type u_1} →
  {H : Type u_2} → [AddLeftCancelSemigroup G] → [AddLeftCancelSemigroup H] → AddLeftCancelSemigroup (G × H)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- The set of boxes of a prepartition that contain `x` in their closures has cardinality
at most `2 ^ Fintype.card ι`.  -/
BoxIntegral.Prepartition.card_filter_mem_Icc_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [inst : Fintype ι] (x : ι → ℝ),
  {J ∈ π.boxes | x ∈ BoxIntegral.Box.Icc J}.card ≤ 2 ^ Fintype.card ι
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompInverseAssociator_hom_app_down_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : C),
  ((CategoryTheory.sum.inlCompInverseAssociator C D E).hom.app X).down.down = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.support_trinomial : ∀ {R : Type u} [inst : Semiring R] {k m n : ℕ},
  k < m →
    m < n →
      ∀ {x y z : R},
        x ≠ 0 →
          y ≠ 0 →
            z ≠ 0 →
              (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m +
                    Polynomial.C z * Polynomial.X ^ n).support =
                {k, m, n}
-- Mathlib.Algebra.RingQuot
/-- The quotient of a ring by an arbitrary relation.  -/
RingQuot : {R : Type uR} → [Semiring R] → (R → R → Prop) → Type uR
-- Init.Data.UInt.Lemmas
UInt32.left_eq_add : ∀ {a b : UInt32}, a = a + b ↔ b = 0
-- Init.Data.Int.DivMod.Bootstrap
Int.add_emod : ∀ (a b n : ℤ), (a + b) % n = (a % n + b % n) % n
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsSubApply : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], IsSubApply (SchwartzMap E F) E F
-- Init.Data.Array.Lemmas
Array.elem_eq_contains : ∀ {α : Type u_1} [inst : BEq α] {a : α} {xs : Array α}, Array.elem a xs = xs.contains a
-- Init.WF
/-- A value is accessible if for all `y` such that `r y x`, `y` is also accessible.
Note that if there exists no `y` such that `r y x`, then `x` is accessible. Such an `x` is called a
_base case_.
 -/
Acc.intro : ∀ {α : Sort u} {r : α → α → Prop} (x : α), (∀ (y : α), r y x → Acc r y) → Acc r x
-- Init.System.IO
/-- Returns the current working directory of the executing process.
 -/
IO.currentDir : IO System.FilePath
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Turn a morphism in `MonCat` back into a `MonoidHom`.  -/
MonCat.Hom.hom : {X Y : MonCat} → X.Hom Y → ↑X →* ↑Y
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Algebra.Ring.GeomSum
pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum : ∀ {R : Type u_1} [inst : CommRing R] {x : R} {m n : ℕ},
  (x ^ m - 1) * ∑ k ∈ Finset.range n, x ^ k = (x ^ n - 1) * ∑ k ∈ Finset.range m, x ^ k
-- Mathlib.Algebra.Order.Kleene
add_idem : ∀ {α : Type u_1} [inst : IdemSemiring α] (a : α), a + a = a
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.RingCompare.mk.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} (eq : {x y : Q(«$α»)} → BaseType x → BaseType y → Bool)
  (compare : {x y : Q(«$α»)} → BaseType x → BaseType y → Ordering)
  (eq_1 : {x y : Q(«$α»)} → BaseType x → BaseType y → Bool)
  (compare_1 : {x y : Q(«$α»)} → BaseType x → BaseType y → Ordering),
  ({ eq := eq, compare := compare } = { eq := eq_1, compare := compare_1 }) = (eq = eq_1 ∧ compare = compare_1)
-- Mathlib.Data.FinEnum
FinEnum.instUInt16 : FinEnum UInt16
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.instInhabitedMat : (x : Type u_1) → Inhabited (CategoryTheory.Mat x)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.terminalIsoIsTerminal_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] {P : C}
  (t : CategoryTheory.Limits.IsTerminal P),
  (CategoryTheory.Limits.terminalIsoIsTerminal t).inv = CategoryTheory.Limits.terminalIsTerminal.from P
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.surjective : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), Function.Surjective ⇑h
-- Mathlib.Algebra.DirectSum.Module
DirectSum.lequivProdDirectSum_apply : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {α : Option ι → Type w} [inst_1 : (i : Option ι) → AddCommMonoid (α i)]
  [inst_2 : (i : Option ι) → Module R (α i)] (a : DirectSum (Option ι) fun i => α i),
  (DirectSum.lequivProdDirectSum R) a = DirectSum.addEquivProdDirectSum.toFun a
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_inl_inr : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N],
  Monoid.Coprod.lift Monoid.Coprod.inl Monoid.Coprod.inr = MonoidHom.id (Monoid.Coprod M N)
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_le_sum_map : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] {s : Multiset α} [AddLeftMono α] (f : α → α),
  (∀ x ∈ s, x ≤ f x) → s.sum ≤ (Multiset.map f s).sum
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The homotopy between `π₀ K ≫ ι K` and `𝟙 K.pathObject`.  -/
HomologicalComplex.pathObject.π₀CompιHomotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasPathObject] →
                  (∀ (i : α), ∃ j, c.Rel i j) →
                    Homotopy
                      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.π₀ K)
                        (HomologicalComplex.pathObject.ι K))
                      (CategoryTheory.CategoryStruct.id K.pathObject)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_inv_snd : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).inv
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
        (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 f_deg ⋯))
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.HasCountableCoproducts.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C],
  (∀ (J : Type) [Countable J], CategoryTheory.Limits.HasCoproductsOfShape J C) →
    CategoryTheory.Limits.HasCountableCoproducts C
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_eq_fastFib : Nat.fib = Nat.fastFib
-- Init.Data.List.Lemmas
List.any_reverse : ∀ {α : Type u_1} {f : α → Bool} {l : List α}, l.reverse.any f = l.any f
-- Mathlib.Order.WithBot
WithTop.untop_inj : ∀ {α : Type u_1} {a b : WithTop α} (ha : a ≠ ⊤) (hb : b ≠ ⊤), a.untop ha = b.untop hb ↔ a = b
-- Mathlib.Topology.Constructions
comap_nhdsWithin_range : ∀ {α : Type u_5} {β : Type u_6} [inst : TopologicalSpace β] (f : α → β) (y : β),
  Filter.comap f (nhdsWithin y (Set.range f)) = Filter.comap f (nhds y)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termL₁ : Lean.ParserDescr
-- Mathlib.Computability.RecursiveIn
RecursiveIn.some : ∀ {α : Type u_1} [inst : Primcodable α] {O : Set (ℕ →. ℕ)}, RecursiveIn O Part.some
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.step.match_1.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Cfg Γ Λ σ → Sort u_5) (var : σ)
  (stk : (k : K) → List (Γ k))
  (h_1 : (var : σ) → (stk : (k : K) → List (Γ k)) → motive { l := none, var := var, stk := stk })
  (h_2 : (l : Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive { l := some l, var := v, stk := S }),
  (match { l := none, var := var, stk := stk } with
    | { l := none, var := var, stk := stk } => h_1 var stk
    | { l := some l, var := v, stk := S } => h_2 l v S) =
    h_1 var stk
-- Mathlib.Data.Countable.Defs
instCountableQuotient : ∀ {α : Sort u} [Countable α] {s : Setoid α}, Countable (Quotient s)
-- Mathlib.SetTheory.Cardinal.Subfield
_private.Mathlib.SetTheory.Cardinal.Subfield.0.Subfield.operate : {α : Type u} →
  (s : Set α) →
    [inst : DivisionRing α] →
      (n : Fin 6 ⊕ ↑s) × (Subfield.Operands✝ s n → ↥(Subfield.closure s)) → ↥(Subfield.closure s)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.homogeneousLocalizationToStalk_stalkToFiberRingHom : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ↑(ProjectiveSpectrum.top 𝒜))
  (z : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.stalk x)),
  AlgebraicGeometry.homogeneousLocalizationToStalk 𝒜 x
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.stalkToFiberRingHom 𝒜 x)) z) =
    z
-- Init.Coe
Coe.mk : {α : semiOutParam (Sort u)} → {β : Sort v} → (α → β) → Coe α β
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.imp_keq_certC : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → ℤ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → ℕ → Bool
-- Mathlib.Order.GaloisConnection.Defs
GaloisCoinsertion.mk.injEq : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {l : α → β} {u : β → α}
  (choice : (x : β) → x ≤ l (u x) → α) (gc : GaloisConnection l u) (u_l_le : ∀ (x : α), u (l x) ≤ x)
  (choice_eq : ∀ (a : β) (h : a ≤ l (u a)), choice a h = u a) (choice_1 : (x : β) → x ≤ l (u x) → α)
  (gc_1 : GaloisConnection l u) (u_l_le_1 : ∀ (x : α), u (l x) ≤ x)
  (choice_eq_1 : ∀ (a : β) (h : a ≤ l (u a)), choice_1 a h = u a),
  ({ choice := choice, gc := gc, u_l_le := u_l_le, choice_eq := choice_eq } =
      { choice := choice_1, gc := gc_1, u_l_le := u_l_le_1, choice_eq := choice_eq_1 }) =
    (choice = choice_1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k a : α} {fallback : β a},
  (t.erase k).getD a fallback = if cmp k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- A Weierstrass equation over the fraction field `K` is integral if
it has coefficients in the ring `R`.  -/
WeierstrassCurve.IsIntegral : (R : Type u_1) → [inst : CommRing R] → {K : Type u_2} → [inst_1 : Field K] → [Algebra R K] → WeierstrassCurve K → Prop
-- Init.Data.String.PosRaw
String.Pos.Raw.mk_le_mk : ∀ {i₁ i₂ : ℕ}, { byteIdx := i₁ } ≤ { byteIdx := i₂ } ↔ i₁ ≤ i₂
-- Mathlib.GroupTheory.OrderOfElement
/-- See also `injective_pow_iff_not_isOfFinOrder`.  -/
not_isOfFinOrder_of_injective_pow : ∀ {G : Type u_1} [inst : Monoid G] {x : G}, (Function.Injective fun n => x ^ n) → ¬IsOfFinOrder x
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_naturality_middle : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
  (f : Y ⟶ Y') (Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) Z)
      (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_lt_mul_iff_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LT α] [MulRightStrictMono α] [MulRightReflectLT α] (a : α) {b c : α},
  b * a < c * a ↔ b < c
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift.congr_simp : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮}
  {a : ↑(F.obj { as := Opposite.op S })} (f : R ⟶ S) {a' : F.CoGrothendieck} (g g_1 : a'.base ⟶ R) (e_g : g = g_1)
  (φ' φ'_1 : a' ⟶ { base := S, fiber := a }) (e_φ' : φ' = φ'_1)
  [inst_1 :
    (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'],
  CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift f g φ' =
    CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift f g_1 φ'_1
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (unit : CategoryTheory.Functor.id C ⟶ F.comp G) (counit : G.comp F ⟶ CategoryTheory.Functor.id D)
  (left_triangle_components :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (F.map (unit.app X)) (counit.app (F.obj X)) =
          CategoryTheory.CategoryStruct.id (F.obj X))
      CategoryTheory.Adjunction.left_triangle_components._autoParam)
  (right_triangle_components :
    autoParam
      (∀ (Y : D),
        CategoryTheory.CategoryStruct.comp (unit.app (G.obj Y)) (G.map (counit.app Y)) =
          CategoryTheory.CategoryStruct.id (G.obj Y))
      CategoryTheory.Adjunction.right_triangle_components._autoParam),
  sizeOf
      { unit := unit, counit := counit, left_triangle_components := left_triangle_components,
        right_triangle_components := right_triangle_components } =
    1 + sizeOf unit + sizeOf counit
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T U : CategoryTheory.Over X} (f : R ⟶ S) (g : T ⟶ U) {Z : C} (h : U.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd S.hom U.hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd R.hom T.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left g) h)
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Creates a `SimpTheorem` from a definitional equality.   -/
Lean.Meta.mkDSimpTheorem : Lean.Meta.Origin →
  Array Lean.Name →
    Lean.Expr →
      optParam Bool true →
        optParam ℕ 1000 → optParam Lean.Meta.ConfigWithKey Lean.Meta.simpGlobalConfig → Lean.MetaM Lean.Meta.SimpTheorem
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.isIso_counit_app_iff_mem_essImage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Faithful] [L.Full] {X : D},
  CategoryTheory.IsIso (h.counit.app X) ↔ L.essImage X
-- Mathlib.Order.LiminfLimsup
Filter.limsup_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteBooleanAlgebra α] (f : Filter β) (u : β → α),
  (Filter.limsup u f)ᶜ = Filter.liminf (compl ∘ u) f
-- Mathlib.Analysis.Calculus.LocalExtr.LineDeriv
IsExtrFilter.lineDeriv_eq_zero : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {f : E → ℝ} {a b : E} {l : Filter E},
  IsExtrFilter f l a → Filter.Tendsto (fun t => a + t • b) (nhds 0) l → lineDeriv ℝ f a b = 0
-- Mathlib.RingTheory.Support
/-- `Supp(M/IM) = Supp(M) ∩ Z(I)`.  -/
Module.support_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  (I : Ideal R), Module.support R (M ⧸ I • ⊤) = Module.support R M ∩ PrimeSpectrum.zeroLocus ↑I
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_sSup : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Set (Subsemiring R)), (sSup S).op = sSup (Subsemiring.unop ⁻¹' S)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k fallback : α},
  (List.map Prod.fst l).contains k = false → (Std.DHashMap.Const.ofList l).getKeyD k fallback = fallback
-- Std.Data.ExtHashSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise panics.
If no panic occurs the result is guaranteed to be pointer equal to the key in the set.
 -/
Std.ExtHashSet.get! : {α : Type u} →
  {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → [Inhabited α] → Std.ExtHashSet α → α → α
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_le_of_le_add : ∀ (f : CircleDeg1Lift) {z : ℝ}, (∀ (x : ℝ), f x ≤ x + z) → f.translationNumber ≤ z
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_eq_getLast_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey he = t.keys.getLast ⋯
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- `Ideal.quotient.lift` as an `AlgHom`.  -/
Ideal.Quotient.liftₐ : {R₁ : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R₁] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R₁ A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R₁ B] →
                (I : Ideal A) → [inst_5 : I.IsTwoSided] → (f : A →ₐ[R₁] B) → (∀ a ∈ I, f a = 0) → A ⧸ I →ₐ[R₁] B
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_add_emod : ∀ (a b : ℤ), b * (a / b) + a % b = a
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.mk.sizeOf_spec : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {S : C} [inst_2 : SizeOf C₀] [inst_3 : SizeOf C] (I₀ : Type w) (X : I₀ → C₀)
  (f : (i : I₀) → F.obj (X i) ⟶ S) (I₁ : I₀ → I₀ → Type w) (Y : ⦃i₁ i₂ : I₀⦄ → I₁ i₁ i₂ → C₀)
  (p₁ : ⦃i₁ i₂ : I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ X i₁) (p₂ : ⦃i₁ i₂ : I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ X i₂)
  (w :
    ∀ ⦃i₁ i₂ : I₀⦄ (j : I₁ i₁ i₂),
      CategoryTheory.CategoryStruct.comp (F.map (p₁ j)) (f i₁) =
        CategoryTheory.CategoryStruct.comp (F.map (p₂ j)) (f i₂)),
  sizeOf { I₀ := I₀, X := X, f := f, I₁ := I₁, Y := Y, p₁ := p₁, p₂ := p₂, w := w } = 1 + sizeOf I₀
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order
/-- `a ↦ a ^ p` is operator concave for `p ∈ [0,1]`.  -/
CFC.concaveOn_nnrpow : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {p : NNReal},
  p ∈ Set.Icc 0 1 → ConcaveOn ℝ (Set.Ici 0) fun a => a ^ p
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- If a function is continuous outside of a countable set, then it is strongly measurable.  -/
MeasureTheory.StronglyMeasurable.of_countable_not_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [OpensMeasurableSpace α]
  [MeasurableSingletonClass α] [inst_4 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β]
  [h : SecondCountableTopologyEither α β] {f : α → β},
  {x | ¬ContinuousAt f x}.Countable → MeasureTheory.StronglyMeasurable f
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- The second projection from the pullback.  -/
TopCat.pullbackSnd : {X Y Z : TopCat} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      TopCat.of { p // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 } ⟶ Y
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.postcomp_shiftIso_hom_app : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E] {A : Type u_5}
  [inst_3 : AddMonoid A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : CategoryTheory.HasShift E A]
  (F : CategoryTheory.SingleFunctors C D A) (G : CategoryTheory.Functor D E) [inst_6 : G.CommShift A] (n a a' : A)
  (ha' : n + a = a') (X : C),
  ((F.postcomp G).shiftIso n a a' ha').hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G n).inv.app ((F.functor a').obj X))
      (G.map ((F.shiftIso n a a' ha').hom.app X))
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.bialgEquivOfSubsingleton.eq_1 : ∀ {R : Type u_1} (M : Type u_8) [inst : CommSemiring R] [inst_1 : Monoid M] [inst_2 : Subsingleton M],
  MonoidAlgebra.bialgEquivOfSubsingleton M =
    { toCoalgHom := (Bialgebra.counitBialgHom R (MonoidAlgebra R M)).toCoalgHom,
      invFun := ⇑(algebraMap R (MonoidAlgebra R M)), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.freeMap.eq_1 : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y : TopCat} (f : X ⟶ Y),
  TopModuleCat.freeMap R f =
    CategoryTheory.ConcreteCategory.ofHom { toLinearMap := Finsupp.lmapDomain R R ⇑(TopCat.Hom.hom f), cont := ⋯ }
-- Init.Data.AC
Lean.Data.AC.norm : {α : Sort u_1} → [info : Lean.Data.AC.ContextInformation α] → α → Lean.Data.AC.Expr → List ℕ
-- Mathlib.Data.Set.Finite.Basic
/-- A `Fintype` instance for set intersection where the left set has a `Fintype` instance.  -/
Set.fintypeInterOfLeft : {α : Type u} → (s t : Set α) → [Fintype ↑s] → [DecidablePred fun x => x ∈ t] → Fintype ↑(s ∩ t)
-- Std.Data.DHashMap.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Equiv.inner : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β},
  m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.Order.Filter.Basic
Filter.inf_eq_bot_iff : ∀ {α : Type u} {f g : Filter α}, f ⊓ g = ⊥ ↔ ∃ U ∈ f, ∃ V ∈ g, U ∩ V = ∅
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.pointwise_smul_le_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : AddMonoid A] [inst_1 : GroupWithZero G₀] [inst_2 : DistribMulAction G₀ A]
  {S T : AddSubmonoid A} {a : G₀}, a ≠ 0 → (a • S ≤ T ↔ S ≤ a⁻¹ • T)
-- Init.Data.UInt.Lemmas
USize.toNat_lt_size : ∀ (a : USize), a.toNat < USize.size