mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.CharP.Lemmas
/-- The iterated Frobenius map `x ↦ x ^ p ^ n`.  -/
iterateFrobenius : (R : Type u_3) → [inst : CommSemiring R] → (p : ℕ) → ℕ → [ExpChar R p] → R →+* R
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  {N : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} N] (p : CategoryTheory.Functor N C)
  [inst_3 : CategoryTheory.InitiallySmall N] {J : CategoryTheory.GrothendieckTopology C}
  [inst_4 : CategoryTheory.IsCofiltered N]
  (hp :
    ∀ ⦃X : C⦄,
      ∀ R ∈ J X,
        ∀ ⦃U : N⦄ (f : p.obj U ⟶ X),
          ∃ Y g,
            ∃ (_ : R.arrows g),
              ∃ V q a, CategoryTheory.CategoryStruct.comp a g = CategoryTheory.CategoryStruct.comp (p.map q) f)
  {A : Type u''} [inst_5 : CategoryTheory.Category.{v'', u''} A]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} A] (P : CategoryTheory.Functor Cᵒᵖ A),
  (CategoryTheory.GrothendieckTopology.Point.presheafFiberOfIsCofilteredCocone p hp P).pt =
    (CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered p hp).presheafFiber.obj P
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The angle between two vectors is `θ` if and only if they are nonzero and the second vector
is the first rotated by `θ` and scaled by the ratio of the norms, or `θ` and at least one of the
vectors are zero.  -/
Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V} (θ : Real.Angle),
  o.oangle x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • (o.rotation θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrp_obj_addGrp_add : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (A : CategoryTheory.AddGrp C),
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F A.X A.X)
      (F.map CategoryTheory.AddMonObj.add)
-- Mathlib.Data.Finset.Insert
Finset.singleton_subset_set_iff : ∀ {α : Type u_1} {s : Set α} {a : α}, ↑{a} ⊆ s ↔ a ∈ s
-- Mathlib.CategoryTheory.Sites.Closed
/-- A Grothendieck topology induces a natural family of closure operators on sieves.  -/
CategoryTheory.GrothendieckTopology.closureOperator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → (X : C) → ClosureOperator (CategoryTheory.Sieve X)
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.le_maxIdeal : ∀ (k : Type u) [inst : Field k], AlgebraicClosure.spanCoeffs k ≤ AlgebraicClosure.maxIdeal k
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  autoParam (CategoryTheory.LocallySmall.{w, v, u} C) CategoryTheory.IsGrothendieckAbelian.locallySmall._autoParam →
    ∀
      (hasFilteredColimitsOfSize :
        autoParam (CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C)
          CategoryTheory.IsGrothendieckAbelian.hasFilteredColimitsOfSize._autoParam),
      autoParam (CategoryTheory.AB5OfSize.{w, w, v, u} C) CategoryTheory.IsGrothendieckAbelian.ab5OfSize._autoParam →
        autoParam (CategoryTheory.HasSeparator C) CategoryTheory.IsGrothendieckAbelian.hasSeparator._autoParam →
          CategoryTheory.IsGrothendieckAbelian.{w, v, u} C
-- Init.Data.BitVec.Basic
/-- Converts a bitvector into a fixed-width hexadecimal number with enough digits to represent it.

If `n` is `0`, then one digit is returned. Otherwise, `⌊(n + 3) / 4⌋` digits are returned.
 -/
BitVec.toHex : {n : ℕ} → BitVec n → String
-- Lean.Data.Json.Basic
Lean.Json.instCoeNat : Coe ℕ Lean.Json
-- Mathlib.Analysis.Analytic.IteratedFDeriv
ContDiffWithinAt.domDomCongr_iteratedFDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {x : E},
  ContDiffWithinAt 𝕜 ⊤ f s x →
    UniqueDiffOn 𝕜 s →
      x ∈ s →
        ∀ {n : ℕ} (σ : Equiv.Perm (Fin n)),
          ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) = iteratedFDerivWithin 𝕜 n f s x
-- Init.Data.Int.Gcd
Int.lcm_natCast_natCast : ∀ (a b : ℕ), (↑a).lcm ↑b = a.lcm b
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCochain_v_descCochain_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K L : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain K F m) (β : CochainComplex.HomComplex.Cochain K G n) {n' m' : ℤ}
  (α' : CochainComplex.HomComplex.Cochain F L m') (β' : CochainComplex.HomComplex.Cochain G L n') (h : n + 1 = m)
  (h' : m' + 1 = n') (p : ℤ) (hp : n + n' = p) (p₁ p₂ p₃ : ℤ) (h₁₂ : p₁ + n = p₂) (h₂₃ : p₂ + n' = p₃) (q : ℤ)
  (hq : p₁ + m = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.liftCochain φ α β h).v p₁ p₂ h₁₂)
      ((CochainComplex.mappingCone.descCochain φ α' β' h').v p₂ p₃ h₂₃) =
    CategoryTheory.CategoryStruct.comp (α.v p₁ q hq) (α'.v q p₃ ⋯) +
      CategoryTheory.CategoryStruct.comp (β.v p₁ p₂ h₁₂) (β'.v p₂ p₃ h₂₃)
-- Mathlib.Algebra.Homology.Homotopy
_private.Mathlib.Algebra.Homology.Homotopy.0.Homotopy.mkInductiveAux₁.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_2 ()
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.comp_mem_paths_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y Z : C}
  {p : Quiver.Path X Y} {q : Quiver.Path Y Z}, W.paths (p.comp q) ↔ W.paths p ∧ W.paths q
-- Mathlib.Data.Sym.Sym2.Order
Sym2.inf_le_sup : ∀ {α : Type u_1} [inst : Lattice α] (s : Sym2 α), s.inf ≤ s.sup
-- Lean.Data.JsonRpc
Lean.JsonRpc.instBEqRequest : {α : Type u_1} → [BEq α] → BEq (Lean.JsonRpc.Request α)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyData.map_g' : ∀ {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.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h.IsPreservedBy F],
  (h.map F).g' = F.map h.g'
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.maxD_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    t.isEmpty = false → ∀ {k fallback : α}, (cmp (t.maxD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_insert_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {kmi : α}, (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi k).isLE = true
-- Mathlib.Data.Multiset.FinsetOps
Multiset.coe_ndinter : ∀ {α : Type u_1} [inst : DecidableEq α] (l₁ l₂ : List α), (↑l₁).ndinter ↑l₂ = ↑(l₁ ∩ l₂)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, a ∉ t → t.getD a fallback = fallback
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_iUnion_fintype : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {ι : Type u_7} [inst_6 : Fintype ι] {s : ι → Set X},
  (∀ (i : ι), MeasurableSet (s i)) →
    Pairwise (Function.onFun Disjoint s) →
      (∀ (i : ι), μ.IntegrableOn f (s i)) → ∫ᵛ (x : X) in ⋃ i, s i, f x ∂[B; μ] = ∑ i, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.TheoremForm.noConfusionType : Sort v✝ → Mathlib.Meta.FunProp.TheoremForm → Mathlib.Meta.FunProp.TheoremForm → Sort v✝
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Consumer.mk.injEq : ∀ {α : Type} (promise : IO.Promise Bool) (waiter : Option (Std.Async.Waiter (Option α))) (promise_1 : IO.Promise Bool)
  (waiter_1 : Option (Std.Async.Waiter (Option α))),
  ({ promise := promise, waiter := waiter } = { promise := promise_1, waiter := waiter_1 }) =
    (promise = promise_1 ∧ waiter = waiter_1)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso_toHom : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X.toSheafedSpace ⟶ Y.toSheafedSpace)
  [inst : CategoryTheory.IsIso f], (AlgebraicGeometry.LocallyRingedSpace.homOfSheafedSpaceHomOfIsIso f).toHom = f.hom
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.sum'_ground_eq : ∀ {α : Type u_1} {ι : Type u_2} (M : ι → Matroid α), (Matroid.sum' M).E = ⋃ i, Prod.mk i '' (M i).E
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.PointedGaloisObject.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        (obj : C) →
          (F.obj obj).obj →
            autoParam (CategoryTheory.PreGaloisCategory.IsGalois obj)
                CategoryTheory.PreGaloisCategory.PointedGaloisObject.isGalois._autoParam →
              CategoryTheory.PreGaloisCategory.PointedGaloisObject F
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.State.mk.injEq : ∀ (structs : Array Lean.Meta.Grind.AC.Struct) (opIdOf : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToOpIds : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ)) (steps : ℕ) (structs_1 : Array Lean.Meta.Grind.AC.Struct)
  (opIdOf_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ))
  (exprToOpIds_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (List ℕ)) (steps_1 : ℕ),
  ({ structs := structs, opIdOf := opIdOf, exprToOpIds := exprToOpIds, steps := steps } =
      { structs := structs_1, opIdOf := opIdOf_1, exprToOpIds := exprToOpIds_1, steps := steps_1 }) =
    (structs = structs_1 ∧ opIdOf = opIdOf_1 ∧ exprToOpIds = exprToOpIds_1 ∧ steps = steps_1)
-- Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FieldSimp.DenomCondition.positive.injEq : ∀ {v : Lean.Level} {M : Q(Type v)} {iM : Q(GroupWithZero «$M»)} (iM' : Q(PartialOrder «$M»))
  (iM'' : Q(PosMulStrictMono «$M»)) (iM''' : Q(PosMulReflectLT «$M»)) (iM'''' : Q(ZeroLEOneClass «$M»))
  (iM'_1 : Q(PartialOrder «$M»)) (iM''_1 : Q(PosMulStrictMono «$M»)) (iM'''_1 : Q(PosMulReflectLT «$M»))
  (iM''''_1 : Q(ZeroLEOneClass «$M»)),
  (Mathlib.Tactic.FieldSimp.DenomCondition.positive iM' iM'' iM''' iM'''' =
      Mathlib.Tactic.FieldSimp.DenomCondition.positive iM'_1 iM''_1 iM'''_1 iM''''_1) =
    (iM' = iM'_1 ∧ iM'' = iM''_1 ∧ iM''' = iM'''_1 ∧ iM'''' = iM''''_1)
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.eraseₘ : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Topology.Order.IntermediateValue
/-- A preconnected set in a conditionally complete linear order is either one of the intervals
`[Inf s, Sup s]`, `[Inf s, Sup s)`, `(Inf s, Sup s]`, `(Inf s, Sup s)`, `[Inf s, +∞)`,
`(Inf s, +∞)`, `(-∞, Sup s]`, `(-∞, Sup s)`, `(-∞, +∞)`, or `∅`. The converse statement requires
`α` to be densely ordered.  -/
IsPreconnected.mem_intervals : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {s : Set α},
  IsPreconnected s →
    s ∈
      {Set.Icc (sInf s) (sSup s), Set.Ico (sInf s) (sSup s), Set.Ioc (sInf s) (sSup s), Set.Ioo (sInf s) (sSup s),
        Set.Ici (sInf s), Set.Ioi (sInf s), Set.Iic (sSup s), Set.Iio (sSup s), Set.univ, ∅}
-- Init.Data.Option.Lemmas
Option.isSome_of_isSome_pfilter : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool}, (o.pfilter p).isSome = true → o.isSome = true
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.fst'.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {Y : D} {b : C} {f' : F.obj b ⟶ Y} (hf' : F.relativelyRepresentable f') {a : C}
  (g : F.obj a ⟶ Y) [inst_2 : F.Full], hf'.fst' g = hf'.fst' g
-- Lean.Expr
/-- Like `getAppNumArgs` but ignores metadata.  -/
Lean.Expr.getAppNumArgs' : Lean.Expr → ℕ
-- Mathlib.Probability.Process.HittingTime
/-- **Alias** of `MeasureTheory.Adapted.isStoppingTime_hittingBtwn`.

---

A discrete hitting time is a stopping time.  -/
MeasureTheory.hittingBtwn_isStoppingTime : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [WellFoundedLT ι] [Countable ι] {x : MeasurableSpace β} {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {s : Set β}
  {n n' : ι},
  MeasureTheory.Adapted f u →
    MeasurableSet s → MeasureTheory.IsStoppingTime f fun ω => ↑(MeasureTheory.hittingBtwn u s n n' ω)
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.coe_of : ∀ (R : Type u) [inst : Semigroup R], ↑(Semigrp.of R) = R
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsLocalizedEquivalence.mk : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂},
  (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence → Φ.IsLocalizedEquivalence
-- Mathlib.Topology.Order.Basic
isOpen_lt' : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] (a : α), IsOpen {b | a < b}
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.tendsto_exp_comp_atTop : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
  Filter.Tendsto (fun x => Real.exp (f x)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
-- Mathlib.Algebra.Category.Ring.Limits
/-- A choice of limit cone for a functor into `RingCat`.
(Generally, you'll just want to use `limit F`.)
 -/
RingCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J RingCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.instHasIterationOfShapeElemIic : ∀ {J : Type w} [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasIterationOfShape J C] [SuccOrder J] [WellFoundedLT J] (j : J),
  CategoryTheory.Limits.HasIterationOfShape (↑(Set.Iic j)) C
-- Mathlib.RingTheory.Etale.StandardEtale
/-- There is a map from a standard etale algebra `R[X][Y]/⟨f, Yg-1⟩` to `S` sending `X` to `x` iff
`f(x) = 0` and `g(x)` is invertible. Also see `StandardEtalePair.homEquiv`.  -/
StandardEtalePair.HasMap : {R : Type u_1} →
  {S : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → StandardEtalePair R → S → Prop
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.killCompl_C : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {f : σ → τ} (hf : Function.Injective f) (r : R),
  (MvPolynomial.killCompl hf) (MvPolynomial.C r) = MvPolynomial.C r
-- Mathlib.Topology.Compactness.Compact
/-- Sets of subtype are compact iff the image under a coercion is.  -/
Subtype.isCompact_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop} {s : Set { x // p x }},
  IsCompact s ↔ IsCompact (Subtype.val '' s)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instNeg : {R : Type u_1} →
  [inst : CommRing R] →
    {A : Type u_2} →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {M : Type u_3} →
            [inst_3 : AddCommGroup M] → [inst_4 : Module A M] → [inst_5 : Module R M] → Neg (Derivation R A M)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
PresheafOfModules.freeAdjunctionUnit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat)
  (F : CategoryTheory.Functor Cᵒᵖ (Type u)) (X : Cᵒᵖ),
  (PresheafOfModules.freeAdjunctionUnit R F).app X = TypeCat.ofHom fun x => ModuleCat.freeMk x
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The second simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_σ_of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    CategoryTheory.CategoryStruct.comp (X.σ j.succ) (X.δ i.castSucc) =
      CategoryTheory.CategoryStruct.comp (X.δ i) (X.σ j)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
/-- `Submodule.subtype` as a `ContinuousLinearMap`.  -/
Submodule.subtypeL : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommMonoid M] → [inst_3 : Module R M] → (p : Submodule R M) → ↥p →L[R] M
-- Mathlib.Data.Set.Function
Set.surjOn_univ : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Set.SurjOn f Set.univ Set.univ ↔ Function.Surjective f
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeWhileTR.go.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (x : Array α) (h_1 : (x : Array α) → motive [] x)
  (h_2 : (a : α) → (as : List α) → (acc : Array α) → motive (a :: as) acc),
  (match [], x with
    | [], x => h_1 x
    | a :: as, acc => h_2 a as acc) =
    h_1 x
-- Mathlib.Order.SymmDiff
bihimp_eq : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp a b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ)
-- Std.Internal.Do.WP.Frame
/-- The framed spec `vcgen` applies for `x`, when each `op r` preserves `Sup`: framing `x` by `F`
makes `op F (wp x (fun a => PreservesSup.upperAdjoint (op F) (Q a)))` a precondition for `wp x Q`.  -/
Std.Internal.Do.WP.Frames.op_wp_upperAdjoint_le_wp : ∀ {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {R : Type t}
  (op : R → Pred → Pred) [∀ (r : R), Lean.Order.PreservesSup (op r)] {x : Prog} {F : R},
  Std.Internal.Do.WP.Frames op x F →
    ∀ (Q : Value → Pred) (E : EPred),
      Lean.Order.PartialOrder.rel
        (op F (Std.Internal.Do.wp x (fun a => Lean.Order.PreservesSup.upperAdjoint (op F) (Q a)) E))
        (Std.Internal.Do.wp x Q E)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.pow_vlt_pow : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {a b : R}, a <ᵥ b → ∀ {n : ℕ}, n ≠ 0 → a ^ n <ᵥ b ^ n
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheck.mk.sizeOf_spec : ∀ (site : Lean.Doc.DeferredCheckSite) (index : ℕ) (sourceString : String) (imports : Array Lean.Name)
  (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (options : Lean.Options) (check : Dynamic),
  sizeOf
      { site := site, index := index, sourceString := sourceString, imports := imports, currNamespace := currNamespace,
        openDecls := openDecls, options := options, check := check } =
    1 + sizeOf site + sizeOf index + sizeOf sourceString + sizeOf imports + sizeOf currNamespace + sizeOf openDecls +
        sizeOf options +
      sizeOf check
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multicospanIndexEnd_right : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : (CategoryTheory.Limits.multicospanShapeEnd J).R),
  (CategoryTheory.Limits.multicospanIndexEnd F).right f =
    (F.obj (Opposite.op (CategoryTheory.Arrow.left f))).obj (CategoryTheory.Arrow.right f)
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.termFace_ : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_roo_eq_some : ∀ {m n i : ℕ}, i < n - (m + 1) → (m<...n).toList[i]? = some (m + 1 + i)
-- Init.Data.Range.Polymorphic.Basic
/-- This typeclass ensures that a `HasSize` instance returns the correct size for all ranges.
 -/
Std.Rxc.LawfulHasSize : (α : Type u) → [LE α] → [Std.PRange.UpwardEnumerable α] → [Std.Rxc.HasSize α] → Prop
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- A real function whose derivative tends to infinity from the left at a point is not
differentiable on the left at that point  -/
not_differentiableWithinAt_of_deriv_tendsto_atTop_Iio : ∀ (f : ℝ → ℝ) {a : ℝ},
  Filter.Tendsto (deriv f) (nhdsWithin a (Set.Iio a)) Filter.atTop → ¬DifferentiableWithinAt ℝ f (Set.Iio a) a
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformlyOn.hasSumUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α], SummableUniformlyOn f s → HasSumUniformlyOn f (fun x => ∑' (i : ι), f i x) s
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono_ae_real : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] {f : α → F} {g : α → ℝ},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ g x) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Mathlib.MeasureTheory.Constructions.SubmoduleQuotient
Submodule.Quotient.instDiscreteMeasurableSpaceQuotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  [inst_3 : MeasurableSpace M] [DiscreteMeasurableSpace M], DiscreteMeasurableSpace (M ⧸ p)
-- Mathlib.Analysis.PSeries
Real.summable_one_div_nat_add_rpow : ∀ (a s : ℝ), (Summable fun n => 1 / |↑n + a| ^ s) ↔ 1 < s
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- `N`-conjugacy is reflexive.  -/
AddGroupExtension.IsAddConj.refl : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  (S : AddGroupExtension N E G) (s : S.Splitting), S.IsAddConj s s
-- Mathlib.Topology.Instances.ZMultiples
/-- This is a special case of `NormedSpace.discreteTopology_zmultiples`. It exists only to simplify
dependencies.  -/
Int.instDiscreteTopologySubtypeRealMemAddSubgroupZmultiples : ∀ {a : ℝ}, DiscreteTopology ↥(AddSubgroup.zmultiples a)
-- Init.Data.Nat.Gcd
Nat.gcd_eq_left_iff_dvd : ∀ {m n : ℕ}, m.gcd n = m ↔ m ∣ n
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Isomorphic presheaves have isomorphic `piOpens` for any cover `U`.  -/
TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens.isoOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        {F : TopCat.Presheaf C X} →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              {G : TopCat.Presheaf C X} →
                (F ≅ G) →
                  (TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens F U ≅
                    TopCat.Presheaf.SheafConditionEqualizerProducts.piOpens G U)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.ofList_nil : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α}, Std.DHashMap.ofList [] = ∅