mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Cotangent.map_comp_h1Cotangentι : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P'),
  Algebra.Extension.Cotangent.map f ∘ₗ Algebra.Extension.h1Cotangentι =
    ↑S Algebra.Extension.h1Cotangentι ∘ₗ Algebra.Extension.H1Cotangent.map f
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.range_val : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  S.val.range = S
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.String.toBitVec_getElem_utf8EncodeChar_zero_of_utf8Size_eq_one : ∀ {c : Char} (h : c.utf8Size = 1), (String.utf8EncodeChar c)[0].toBitVec = 0#1 ++ BitVec.extractLsb' 0 7 c.val.toBitVec
-- Mathlib.Topology.Algebra.InfiniteSum.Field
HasProd.norm : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedCommRing E] [NormMulClass E] [NormOneClass E] {f : α → E} {x : E},
  HasProd f x → HasProd (fun x => ‖f x‖) ‖x‖
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mk.sizeOf_spec : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] [inst_1 : SizeOf R] (toNonUnitalSubsemiring : NonUnitalSubsemiring R)
  (neg_mem' : ∀ {x : R}, x ∈ toNonUnitalSubsemiring.carrier → -x ∈ toNonUnitalSubsemiring.carrier),
  sizeOf { toNonUnitalSubsemiring := toNonUnitalSubsemiring, neg_mem' := neg_mem' } = 1 + sizeOf toNonUnitalSubsemiring
-- Init.Data.Array.Lemmas
Array.foldlM_push : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α} {a : α}
  {f : β → α → m β} {b : β},
  Array.foldlM f b (xs.push a) = do
    let b ← Array.foldlM f b xs
    f b a
-- Mathlib.Algebra.BigOperators.Finprod
Multiset.sum_map_eq_finsum : ∀ {α : Type u_1} {M : Type u_2} [inst : DecidableEq α] [inst_1 : AddCommMonoid M] (s : Multiset α) (f : α → M),
  (Multiset.map f s).sum = ∑ᶠ (a : α), Multiset.count a s • f a
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.topologicalClosure_mono : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [inst_2 : SeparatelyContinuousMul M]
  {s t : Subsemigroup M}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- The inf of two submodules, the first finite-dimensional, is
finite-dimensional.  -/
Submodule.finiteDimensional_inf_left : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (S₁ S₂ : Submodule K V) [FiniteDimensional K ↥S₁], FiniteDimensional K ↥(S₁ ⊓ S₂)
-- Mathlib.CategoryTheory.Monoidal.Bimod
/-- The underlying morphism of the forward component of the associator isomorphism.  -/
Bimod.AssociatorBimod.hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Limits.HasCoequalizers C] →
        [inst_3 :
            ∀ (X : C),
              CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                (CategoryTheory.MonoidalCategory.tensorLeft X)] →
          [inst_4 :
              ∀ (X : C),
                CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
                  (CategoryTheory.MonoidalCategory.tensorRight X)] →
            {R S T U : CategoryTheory.Mon C} →
              (P : Bimod R S) →
                (Q : Bimod S T) →
                  (L : Bimod T U) → ((P.tensorBimod Q).tensorBimod L).X ⟶ (P.tensorBimod (Q.tensorBimod L)).X
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.locallyFinite : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] [inst_5 : FiniteDimensional ℝ E] {s : Set M} (fs : SmoothBumpCovering ι I M s),
  LocallyFinite fun i => Function.support ↑(fs.toFun i)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.zsmul_eq_iff : ∀ {ψ θ : Real.Angle} {z : ℤ}, z ≠ 0 → (z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑k • ↑(2 * Real.pi / ↑z))
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.C_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : CommSemiring R] {A : Type u_3}
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : IsTopologicalSemiring A] (r : R)
  (a : α), (ContinuousMap.C r) a = (algebraMap R A) r
-- Lean.Message
/-- A persistent array of messages.

In the Lean elaborator, we use a fresh message log per command but may also report diagnostics at
various points inside a command, which will empty `unreported` and move its messages to `reported`.
Reported messages are preserved for some specific "lookback" operations such as `hasError` that
should consider the entire message history of the current command; most other functions such as
`add` and `toList` will only operate on unreported messages.
 -/
Lean.MessageLog : Type
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.forEligibleDeclsWithCancellationM : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [MonadLiftT Lean.MetaM m] →
        [Lean.Server.MonadCancellable m] → (Lean.Name → Lean.Server.Completion.EligibleDecl → m PUnit.{1}) → m PUnit.{1}
-- Mathlib.Data.PFun
PFun.mem_res : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (a : α) (b : β), b ∈ PFun.res f s a ↔ a ∈ s ∧ f a = b
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.two_le_chromaticNumber_of_adj : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → 2 ≤ G.chromaticNumber
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.of_hasBasis_nhds : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set (Set α)},
  (∀ (a : α), (nhds a).HasBasis (fun t => t ∈ s ∧ a ∈ t) id) → TopologicalSpace.IsTopologicalBasis s
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef.mk.inj : ∀ {α : Type} {ref ref_1 : IO.Ref (Lean.Meta.RefinedDiscrTree α)}, { ref := ref } = { ref := ref_1 } → ref = ref_1
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.State.writingBodyFixed.sizeOf_spec : ∀ (n : ℕ), sizeOf (Std.Http.Protocol.H1.Writer.State.writingBodyFixed n) = 1 + sizeOf n
-- Mathlib.MeasureTheory.Function.ConvergenceInMeasure
/-- If `f` is a sequence of functions which converges in measure to `g`, then there exists a
subsequence of `f` which converges a.e. to `g`.  -/
MeasureTheory.TendstoInMeasure.exists_seq_tendsto_ae : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : PseudoEMetricSpace E]
  {f : ℕ → α → E} {g : α → E},
  MeasureTheory.TendstoInMeasure μ f Filter.atTop g →
    ∃ ns, StrictMono ns ∧ ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => f (ns i) x) Filter.atTop (nhds (g x))
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNRealRingHom_apply : ⇑ENat.toENNRealRingHom = ENat.toENNReal
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- The syntax of the flexible tactic that caused the stain  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.stx : Mathlib.Linter.Flexible.StainData✝ → Lean.Syntax
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The projection `S.X₂ ⟶ S.opcycles`.  -/
CategoryTheory.ShortComplex.pOpcycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → [inst_2 : S.HasRightHomology] → S.X₂ ⟶ S.opcycles
-- Init.Data.Nat.Sqrt.Lemmas
Nat.sqrt.eq_1 : ∀ (n : ℕ), n.sqrt = if n ≤ 1 then n else Nat.sqrt.iter n (1 <<< (n.log2 / 2 + 1))
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toRingHom_toAddMonoidHom : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), ↑↑f = ↑f
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `le_sub_iff_add_le'`. -/
le_sub_left_of_add_le : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a + b ≤ c → b ≤ c - a
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.comp_inv : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] {φ : M →* N} {ψ : N →* M},
  Function.RightInverse ⇑φ ⇑ψ → ∀ {χ : M →* M} [MonoidHom.CompTriple.IsId χ], φ.CompTriple ψ χ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.diff_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ \ m₃).Equiv (m₂ \ m₃)
-- Mathlib.Data.SetLike.Basic
SetLike.mk : {A : Type u_1} → {B : outParam (Type u_2)} → (coe : A → Set B) → Function.Injective coe → SetLike A B
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.shortestPrefixDiff.eq_1 : ∀ {E : ℕ → Type u_2} (x : (n : ℕ) → E n) (s : Set ((n : ℕ) → E n)),
  PiNat.shortestPrefixDiff x s = if h : ∃ n, Disjoint s (PiNat.cylinder x n) then Nat.find h else 0
-- Mathlib.Order.Filter.NAry
/-- The other direction does not hold because of the `f-f` cross terms on the RHS.  -/
Filter.map₂_distrib_le_left : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9}
  {f : Filter α} {g : Filter β} {h : Filter γ} {m : α → δ → ε} {n : β → γ → δ} {m₁ : α → β → β'} {m₂ : α → γ → γ'}
  {n' : β' → γ' → ε},
  (∀ (a : α) (b : β) (c : γ), m a (n b c) = n' (m₁ a b) (m₂ a c)) →
    Filter.map₂ m f (Filter.map₂ n g h) ≤ Filter.map₂ n' (Filter.map₂ m₁ f g) (Filter.map₂ m₂ f h)
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.const.get_map : ∀ {n : ℕ} {A : Type u} {α β : TypeVec.{u} n} (f : α.Arrow β) (x : ↑(MvPFunctor.const n A) α),
  MvPFunctor.const.get (MvFunctor.map f x) = MvPFunctor.const.get x
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.preimageIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} [inst_2 : F.Full] [inst_3 : F.Faithful] (f : F.obj X ≅ F.obj Y),
  (F.preimageIso f).hom = F.preimage f.hom
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : Add α],
  OrderAddMonoidIso.instInhabited α = { default := OrderAddMonoidIso.refl α }
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.instFaithfulPresheafOfModulesObjFunctorOppositeRingCatIsSheafForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  (R : CategoryTheory.Sheaf J RingCat), (SheafOfModules.forget R).Faithful
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k
-- Lean.Elab.Level
Lean.Elab.Level.State.levelNames : Lean.Elab.Level.State → List Lean.Name
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.le_mul_right : ∀ (a : Ordinal.{u_4}) {b : Ordinal.{u_4}}, 0 < b → a ≤ b * a
-- Lean.Elab.AuxDef
/-- Declares an auxiliary definition with an automatically generated name.
For example, `aux_def foo : Nat := 42` creates a definition
with an internal, unused name based on the suggestion `foo`.
 -/
Lean.Elab.Command.aux_def : Lean.ParserDescr
-- Mathlib.Data.Sign.Basic
sign_mul_self : ∀ {α : Type u} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (x : α), ↑(SignType.sign x) * x = |x|
-- Lean.Meta.Closure
Lean.Meta.Closure.State : Type
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Insert key-value pair `(k, v)` into the tree.  -/
RBTree.RBMap.insert : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → β → RBTree.RBMap α β cmp
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
IsValuativeTopology.mem_nhds_zero_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R]
  (s : Set R), s ∈ nhds 0 ↔ ∃ γ, {x | (ValuativeRel.valuation R) x < ↑γ} ⊆ s
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOfCoconeLeftOp_π_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J Cᵒᵖ} (c : CategoryTheory.Limits.Cocone F.leftOp) (X : J),
  (CategoryTheory.Limits.coneOfCoconeLeftOp c).π.app X = (c.ι.app (Opposite.op X)).op
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk₀ : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type w'}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂}
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂)
  (eY : Φ.functor.obj Y₁ ≅ Y₂) [W₁.IsCompatibleWithShift M] [W₂.IsCompatibleWithShift M] (m₀ : M) (hm₀ : m₀ = 0)
  (f : X₁ ⟶ Y₁),
  Φ.smallShiftedHomMap eX eY (CategoryTheory.Localization.SmallShiftedHom.mk₀ W₁ m₀ hm₀ f) =
    CategoryTheory.Localization.SmallShiftedHom.mk₀ W₂ m₀ hm₀
      (CategoryTheory.CategoryStruct.comp eX.inv (CategoryTheory.CategoryStruct.comp (Φ.functor.map f) eY.hom))
-- Mathlib.Algebra.Ring.Pointwise.Finset
Finset.mul_add_subset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Distrib α] (s t u : Finset α), s * (t + u) ⊆ s * t + s * u
-- Init.Data.Float.Float
/-- Subtracts 64-bit floating-point numbers according to IEEE 754. Typically used via the `-` operator.

This function has a logical model in terms of `Float.Model`. It is compiled to the C subtraction operator.
 -/
Float.sub : Float → Float → Float
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseRightKanExtensionCompIsoOfPreserves_hom_fac_assoc : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseRightKanExtension F L]
  [inst_5 : L.HasPointwiseRightKanExtension F] {Z : CategoryTheory.Functor A D} (h : F.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.pointwiseRightKanExtensionCompIsoOfPreserves F L).hom)
      (CategoryTheory.CategoryStruct.comp (L.pointwiseRightKanExtensionCounit (F.comp G)) h) =
    CategoryTheory.CategoryStruct.comp (L.associator (L.pointwiseRightKanExtension F) G).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.pointwiseRightKanExtensionCounit F) G)
        h)
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The category of sheaves taking values in `A` on a Grothendieck topology.  -/
CategoryTheory.Sheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.GrothendieckTopology C →
      (A : Type u₂) → [CategoryTheory.Category.{v₂, u₂} A] → Type (max (max (max u₂ v₂) u₁) v₁)
-- Mathlib.Algebra.Star.Basic
star_one : ∀ (R : Type u) [inst : MulOneClass R] [inst_1 : StarMul R], star 1 = 1
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_eq_inter_iff_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t
-- Mathlib.Analysis.Normed.Ring.Basic
/-- Normed ring structure on the product of two normed rings, using the sup norm.  -/
Prod.normedRing : {α : Type u_2} → {β : Type u_3} → [NormedRing α] → [NormedRing β] → NormedRing (α × β)
-- Mathlib.Topology.Compactness.Compact
/-- If `s` and `t` are compact sets and `n` is an open neighborhood of `s × t`, then there exist
open neighborhoods `u ⊇ s` and `v ⊇ t` such that `u × v ⊆ n`.

See also `IsCompact.nhdsSet_prod_eq`.  -/
generalized_tube_lemma : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X},
  IsCompact s →
    ∀ {t : Set Y},
      IsCompact t → ∀ {n : Set (X × Y)}, IsOpen n → s ×ˢ t ⊆ n → ∃ u v, IsOpen u ∧ IsOpen v ∧ s ⊆ u ∧ t ⊆ v ∧ u ×ˢ v ⊆ n
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectIso_comp_image_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X}
  [inst_1 : CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g]
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso (CategoryTheory.Arrow.mk f).hom).hom
      (CategoryTheory.Limits.image.map sq) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq)
      (CategoryTheory.Limits.imageSubobjectIso g).hom
-- Mathlib.Order.UpperLower.Prod
UpperSet.top_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (t : UpperSet β), ⊤ ×ˢ t = ⊤
-- Mathlib.Data.Finsupp.Order
Finsupp.sum_le_sum : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ h₂ : ι → α → β},
  (∀ i ∈ f.support, h₁ i (f i) ≤ h₂ i (f i)) → f.sum h₁ ≤ f.sum h₂
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_fromEdgeSet_fromRel_eq_reflTransGen : ∀ {V : Type u} {r : V → V → Prop} (sym : Std.Symm r),
  (SimpleGraph.fromEdgeSet (Sym2.fromRel sym)).Reachable = Relation.ReflTransGen r
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommMonoidWithTop.toLinearOrder : {α : Type u_3} → [self : LinearOrderedAddCommMonoidWithTop α] → LinearOrder α
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.tendsto_coe_atTop : ∀ {α : Type u_2} {f : Filter α} {m : α → NNReal},
  Filter.Tendsto (fun a => ↑(m a)) f Filter.atTop ↔ Filter.Tendsto m f Filter.atTop
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_natAdd_Ioi : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.image (Fin.natAdd m) (Finset.Ioi i) = Finset.Ioi (Fin.natAdd m i)
-- Lean.Parser.Types
Lean.Parser.mkIdent : Lean.SourceInfo → Substring.Raw → Lean.Name → Lean.Syntax
-- Init.Prelude
instMinUInt32 : Min UInt32
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.absNorm_relNorm : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] (S : Type u_3) [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S]
  [inst_11 : Module.Free ℤ R] [inst_12 : Module.Free ℤ S] [Module.Finite ℤ S] [PerfectField (FractionRing R)]
  (I : Ideal S), Ideal.absNorm ((Ideal.relNorm R) I) = Ideal.absNorm I
-- Aesop.Search.SearchM
Aesop.NormSimpContext : Type
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.isPullback_aux : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (f : X ⟶ Y) (y : CategoryTheory.Subobject Y),
  ∃ φ, CategoryTheory.IsPullback φ ((CategoryTheory.Subobject.pullback f).obj y).arrow y.arrow f
-- ProofWidgets.Data.Html
Lean.Parser.Category.proofWidgetsJsxAttr : Lean.Parser.Category
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommAddMonObj.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X : C} [inst_3 : CategoryTheory.AddMonObj X],
  autoParam
      (CategoryTheory.CategoryStruct.comp (β_ X X).hom CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add)
      CategoryTheory.IsCommAddMonObj.add_comm._autoParam →
    CategoryTheory.IsCommAddMonObj X
-- Init.Internal.Order.MonadTail
Lean.Order.instCCPOSTOfNonempty : {α σ : Type} → [Nonempty α] → Lean.Order.CCPO (ST σ α)
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- Auxiliary definition used to define `liftOfRightInverse`  -/
MonoidHom.liftOfRightInverseAux : {G₁ : Type u_5} →
  {G₂ : Type u_6} →
    {G₃ : Type u_7} →
      [inst : Group G₁] →
        [inst_1 : Group G₂] →
          [inst_2 : Group G₃] →
            (f : G₁ →* G₂) →
              (f_inv : G₂ → G₁) → Function.RightInverse f_inv ⇑f → (g : G₁ →* G₃) → f.ker ≤ g.ker → G₂ →* G₃
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.le_def : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (f g : E →L[𝕜] E), f ≤ g ↔ (g - f).IsPositive
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
Module.End.ker_aeval_ring_hom'_unit_polynomial : ∀ {R : Type v} {M : Type w} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) (c : (Polynomial R)ˣ), LinearMap.ker ((Polynomial.aeval f) ↑c) = ⊥
-- Mathlib.Topology.Algebra.Order.Group
ContinuousOn.mabs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G} {s : Set X},
  ContinuousOn f s → ContinuousOn (fun x => |f x|ₘ) s
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} (eqv : C ≌ D)
  {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [inst_2 : eqv.functor.IsContinuous J K]
  [inst_3 : eqv.inverse.IsContinuous K J] (φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R)
  (ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S)
  (H₁ :
    CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.counit) R.obj =
      CategoryTheory.CategoryStruct.comp ψ.hom (eqv.inverse.op.whiskerLeft φ.hom))
  (H₂ :
    CategoryTheory.CategoryStruct.comp φ.hom
        (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.hom)
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.obj)) =
      CategoryTheory.CategoryStruct.id S.obj)
  (M : SheafOfModules R) (U : Dᵒᵖ) (x : ↑(((CategoryTheory.Functor.id (SheafOfModules R)).obj M).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom
        (((SheafOfModules.pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).unit.app M).val.app U))
      x =
    (CategoryTheory.ConcreteCategory.hom (M.val.map (eqv.counit.app (Opposite.unop U)).op)) x
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_dvd1_cert.eq_1 : ∀ (p₂ p' : Int.Internal.Linear.Poly) (b k : ℤ),
  Int.Internal.Linear.cooper_dvd_right_split_dvd1_cert p₂ p' b k =
    (b.beq' p₂.leadCoeff).and' (p'.beq' (p₂.tail.addConst_k k))
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set in dimension 1: if the derivative of a function is
bounded by `C` on `s`, then the function is `C`-Lipschitz on `s`.
Version with `derivWithin` and `LipschitzOnWith`.  -/
Convex.lipschitzOnWith_of_nnnorm_derivWithin_le : ∀ {𝕜 : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f : 𝕜 → G}
  {s : Set 𝕜} {C : NNReal},
  Convex ℝ s → DifferentiableOn 𝕜 f s → (∀ x ∈ s, ‖derivWithin f s x‖₊ ≤ C) → LipschitzOnWith C f s