mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Control.EState
/-- Alternative orElse operator that allows callers to select which exception should be used when both
operations fail. The default is to use the first exception since the standard `orElse` uses the
second.
 -/
EStateM.orElse' : {ε σ α δ : Type u} → [EStateM.Backtrackable δ σ] → EStateM ε σ α → EStateM ε σ α → optParam Bool true → EStateM ε σ α
-- Init.Data.String.Lemmas.Pattern.Split.Pred
_private.Init.Data.String.Lemmas.Pattern.Split.Pred.0.String.Slice.Pattern.Model.split.eq_def : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.Model.StrictPatternModel pat] {s : String.Slice} (firstRejected curr : s.Pos)
  (hle : firstRejected ≤ curr),
  String.Slice.Pattern.Model.split pat firstRejected curr hle =
    if h : curr = s.endPos then [s.subslice firstRejected curr hle]
    else
      match hd : String.Slice.Pattern.Model.matchAt? pat curr with
      | some pos =>
        have this := ⋯;
        s.subslice firstRejected curr hle :: String.Slice.Pattern.Model.split pat pos pos ⋯
      | none => String.Slice.Pattern.Model.split pat firstRejected (curr.next h) ⋯
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.instFintypeOfDiscreteTopologyOfCompactSpace : {A : Type u_1} →
  [inst : Monoid A] →
    [inst_1 : TopologicalSpace A] → [DiscreteTopology A] → [CompactSpace A] → Fintype (PontryaginDual A)
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- For a presheaf `P`, consider the forgetful functor from the category of representable
presheaves over `P` to the category of presheaves. There is a tautological cocone over this
functor whose leg for a natural transformation `V ⟶ P` with `V` representable is just that
natural transformation.  -/
CategoryTheory.Presheaf.tautologicalCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type v₁)) →
      CategoryTheory.Limits.Cocone
        ((CategoryTheory.CostructuredArrow.proj CategoryTheory.yoneda P).comp CategoryTheory.yoneda)
-- Std.Time.Internal.Bounded
/-- Adjust the bounds of a `Bounded` by adding a constant value to both the lower and upper bounds.
 -/
Std.Time.Internal.Bounded.LE.addProven : {n m num : ℤ} →
  (bounded : Std.Time.Internal.Bounded.LE n m) → ↑bounded + num ≤ m → num ≥ 0 → Std.Time.Internal.Bounded.LE n m
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.hasDerivAt_cosh : ∀ (x : ℝ), HasDerivAt Real.cosh (Real.sinh x) x
-- Mathlib.Topology.Algebra.Group.Basic
/-- Given a compact set `K` inside an open set `U`, there is an open neighborhood `V` of
`0` such that `V + K ⊆ U`.  -/
compact_open_separated_add_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddZeroClass G] [ContinuousAdd G] {K U : Set G},
  IsCompact K → IsOpen U → K ⊆ U → ∃ V ∈ nhds 0, V + K ⊆ U
-- Mathlib.Algebra.Algebra.Hom.Rat
RingHom.equivRatAlgHom_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R →+* S), (RingHom.equivRatAlgHom R S) f = f.toRatAlgHom
-- Mathlib.Data.Seq.Defs
/-- Functorial action of the functor `Option (α × _)`  -/
Stream'.Seq.omap : {α : Type u} → {β : Type v} → {γ : Type w} → (β → γ) → Option (α × β) → Option (α × γ)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreCompInclusionIso_inv_app : ∀ {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 : CategoryTheory.Core C),
  F.coreCompInclusionIso.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X.of)
-- Mathlib.RingTheory.Localization.Module
/-- An `R`-linear map between two `S⁻¹R`-modules is actually `S⁻¹R`-linear.  -/
LinearMap.extendScalarsOfIsLocalization : {R : Type u_3} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      (A : Type u_4) →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [IsLocalization S A] →
              {M : Type u_5} →
                {N : Type u_6} →
                  [inst_4 : AddCommMonoid M] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module A M] →
                        [IsScalarTower R A M] →
                          [inst_8 : AddCommMonoid N] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module A N] → [IsScalarTower R A N] → (M →ₗ[R] N) → M →ₗ[A] N
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.EqInfo.decSubsingleton.inj : ∀ {lhs rhs lhs_1 rhs_1 : Lean.FVarId},
  Lean.Meta.EqInfo.decSubsingleton✝ lhs rhs = Lean.Meta.EqInfo.decSubsingleton✝ lhs_1 rhs_1 → lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.strictLimitsClosureStep.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {α : Type t}
  (J : α → Type u') [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)],
  P.strictLimitsClosureStep J = P ⊔ ⨆ a, P.strictLimitsOfShape (J a)
-- Mathlib.Data.Set.Image
Set.preimage_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, Disjoint s (Set.range f) → f ⁻¹' s = ∅
-- Std.Sync.CancellationContext
/-- Cancels this context and all child contexts with the given reason.
 -/
Std.CancellationContext.cancel : Std.CancellationContext → Std.CancellationReason → BaseIO Unit
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestRevMatchAtChain_startPos_endPos_iff : ∀ {pat s : String.Slice},
  String.Slice.Pattern.Model.IsLongestRevMatchAtChain pat s.startPos s.endPos ↔
    ∃ n, s.copy = String.join (List.replicate n pat.copy)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.inclusion_inclusion : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S T U : Subalgebra R A} (hst : S ≤ T) (htu : T ≤ U) (x : ↥S),
  (Subalgebra.inclusion htu) ((Subalgebra.inclusion hst) x) = (Subalgebra.inclusion ⋯) x
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.BlockTriangular.det : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : CommRing R] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : DecidableEq α] [inst_4 : LinearOrder α],
  M.BlockTriangular b → M.det = ∏ a ∈ Finset.image b Finset.univ, (M.toSquareBlock b a).det
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_pos_of_neg : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a : α}, a < 0 → 0 < |a|
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_mul_cancel_left₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (b : G₀), a / (a * b) = b⁻¹
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.le_ae_join : ∀ {α : Type u_1} {mα : MeasurableSpace α} (m : MeasureTheory.Measure (MeasureTheory.Measure α)),
  (MeasureTheory.ae m).bind MeasureTheory.ae ≤ MeasureTheory.ae m.join
-- Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered
CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk_map : ∀ {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] {U V : N} (g : V ⟶ U),
  CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk (p.map g) =
    CategoryTheory.GrothendieckTopology.Point.ofIsCofiltered.fiberMk (CategoryTheory.CategoryStruct.id (p.obj U))
-- Mathlib.Topology.Semicontinuity.Basic
IsClosed.upperSemicontinuousOn_indicator : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {s t : Set α} {y : β} [inst_1 : Zero β]
  [inst_2 : Preorder β], IsClosed s → 0 ≤ y → UpperSemicontinuousOn (s.indicator fun _x => y) t
-- Mathlib.Algebra.Module.Submodule.Range
/-- Under the canonical linear map from a submodule `p` to the ambient space `M`, the image of the
maximal submodule of `p` is just `p`.  -/
Submodule.map_subtype_top : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p : Submodule R M), Submodule.map p.subtype ⊤ = p
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.instHasPullbacksOfHasPullbacks : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} [CategoryTheory.Limits.HasPullbacks C]
  (R : CategoryTheory.Presieve X) {Y : C} (f : Y ⟶ X), R.HasPullbacks f
-- Init.Data.Dyadic.Instances
Dyadic.instCommRing : Lean.Grind.CommRing Dyadic
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.coe_himp : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : T2Space α]
  (s t : TopologicalSpace.CompactOpens α), ↑(s ⇨ t) = ↑s ⇨ ↑t
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_compl_add_sum : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (s : Finset ι)
  (f : ι → M), ∑ i ∈ sᶜ, f i + ∑ i ∈ s, f i = ∑ i, f i
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.commSemiring : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → CommSemiring (R ⧸ I)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_rpow : ∀ {x y z : ℝ}, 0 ≤ x → x ≤ y → 0 ≤ z → x ^ z ≤ y ^ z
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_insertNth : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (i : Fin (n + 1)) (x : M) (p : Fin n → M),
  ∏ j, i.insertNth x p j = x * ∏ j, p j
-- Mathlib.Analysis.Complex.IntegerCompl
Complex.integerComplement.ne_zero : ∀ {x : ℂ}, x ∈ Complex.integerComplement → x ≠ 0
-- Init.Data.Vector.MapIdx
Array.mapFinIdx_toVector : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β},
  xs.toVector.mapFinIdx f = Vector.cast ⋯ (xs.mapFinIdx f).toVector
-- Std.Time.Time.HourMarker
Std.Time.instTransOrdHourMarker : Std.TransOrd Std.Time.HourMarker
-- Mathlib.Topology.Inseparable
Topology.IsInducing.specializingMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → StableUnderSpecialization (Set.range f) → SpecializingMap f
-- Mathlib.Topology.Separation.Basic
/-- In a (weakly) locally compact R₁ space, each point admits a compact closed neighborhood.  -/
exists_mem_nhds_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X),
  ∃ K ∈ nhds x, IsCompact K ∧ IsClosed K
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore.getDoubleIdx : String → ℕ → ℕ → ℕ
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in a commutative Banach algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has strict
Fréchet derivative `NormedSpace.exp x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`.  -/
hasStrictFDerivAt_exp : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : RCLike 𝕂] [inst_1 : NormedCommRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸] {x : 𝔸}, HasStrictFDerivAt NormedSpace.exp (NormedSpace.exp x • 1) x
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k : α} {fallback : γ},
  (Std.HashMap.filterMap f m).getD k fallback = (m[k]?.pbind fun x_2 h' => f (m.getKey k ⋯) x_2).getD fallback
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShift_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n : ℤ}
  (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n) (x : R),
  (x • γ).rightShift a n' hn' = x • γ.rightShift a n' hn'
-- Init.Data.Ord.Basic
Ordering.not_isNe_eq_isEq : ∀ {o : Ordering}, (!o.isNe) = o.isEq
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- Linear isometry equiv between a space and its lift to another universe.  -/
LinearIsometryEquiv.ulift : (R : Type u_1) →
  (E : Type u_5) →
    [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : Module R E] → ULift.{u_11, u_5} E ≃ₗᵢ[R] E
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmallerₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ : Std.DHashMap.Internal.Raw₀ α β)
  (m₂ : Std.DHashMap.Raw α β),
  m₁.interSmallerₘ m₂ =
    Std.DHashMap.Raw.fold (fun sofar k x => m₁.interSmallerFnₘ sofar k) Std.DHashMap.Internal.Raw₀.emptyWithCapacity m₂
-- Lean.Compiler.MetaAttr
/-- Marks in the environment extension that the given declaration has been declared by the user as `meta`.  -/
Lean.markMeta : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.Order.BooleanAlgebra.Defs
Bool.sup_eq_bor : (fun x1 x2 => max x1 x2) = or
-- Mathlib.Algebra.Field.Opposite
AddOpposite.instField : {α : Type u_1} → [Field α] → Field αᵃᵒᵖ
-- Init.Data.FloatArray.Basic
FloatArray.empty : FloatArray
-- Mathlib.CategoryTheory.Localization.Construction
/-- The obvious functor `C ⥤ W.Localization`  -/
CategoryTheory.MorphismProperty.Q : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) → CategoryTheory.Functor C W.Localization
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousLinearMap.continuous_postcomp_continuousMultilinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} {G : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜 G]
  [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜 G] (g : F →L[𝕜] G),
  Continuous g.compContinuousMultilinearMap
-- Init.Data.SInt.Bitwise
instAssociativeInt8HOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.le_inf_support_coeff_mul : ∀ {R : Type u_1} {A : Type u_3} {T : Type u_4} [inst : SemilatticeInf T] [inst_1 : OrderTop T] [inst_2 : Semiring R]
  [inst_3 : Add A] [inst_4 : Add T] [AddLeftMono T] [AddRightMono T] {degt : A → T},
  (∀ (a b : A), degt a + degt b ≤ degt (a + b)) →
    ∀ (f g : AddMonoidAlgebra R A), f.coeff.support.inf degt + g.coeff.support.inf degt ≤ (f * g).coeff.support.inf degt
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.isTerminalPUnit_from_apply : ∀ {X : Type u} (x : X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.isTerminalPUnit.from X)) x = PUnit.unit
-- Init.Prelude
/-- Make an opaque reference to a `Methods`.  -/
Lean.Macro.mkMethods : Lean.Macro.Methods → Lean.Macro.MethodsRef
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasTerminal_of_hasInitial_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial Cᵒᵖ],
  CategoryTheory.Limits.HasTerminal C
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.ofEpi_s : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M N : SheafOfModules R} (σ : M.GeneratingSections) (p : M ⟶ N)
  [inst_3 : CategoryTheory.Epi p] (i : σ.I), (σ.ofEpi p).s i = SheafOfModules.sectionsMap p (σ.s i)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.canLiftCardinalType : CanLift Cardinal.{u} (Type u) Cardinal.mk fun x => True
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_comp_equiv_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (j : K →+* M) (k : K →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : ExpChar L p] [inst_7 : PerfectRing L p] [inst_8 : IsPerfectClosure i p]
  [inst_9 : PerfectRing M p] [inst_10 : IsPerfectClosure j p] [inst_11 : ExpChar N p] [inst_12 : PerfectRing N p]
  [inst_13 : IsPerfectClosure k p] (x : L),
  (IsPerfectClosure.equiv j k p) ((IsPerfectClosure.equiv i j p) x) = (IsPerfectClosure.equiv i k p) x
-- Mathlib.Algebra.Lie.Abelian
LieModule.instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.IsTrivial L ↥(LieModule.maxTrivSubmodule R L M)
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_zero : ↑0 = 0
-- Mathlib.Analysis.MeanInequalities
/-- **Hölder inequality**: the scalar product of two functions is bounded by the product of their
`L^p` and `L^q` norms when `p` and `q` are conjugate exponents. A version for `NNReal`-valued
functions. For an alternative version, convenient if the infinite sums are not already expressed as
`p`-th powers, see `inner_le_Lp_mul_Lq_tsum`.  -/
NNReal.inner_le_Lp_mul_Lq_hasSum : ∀ {ι : Type u} {f g : ι → NNReal} {A B : NNReal} {p q : ℝ},
  p.HolderConjugate q →
    HasSum (fun i => f i ^ p) (A ^ p) → HasSum (fun i => g i ^ q) (B ^ q) → ∃ C ≤ A * B, HasSum (fun i => f i * g i) C
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
/-- Given a locally bijective morphism `α : R₀ ⟶ R.val` where `R₀` is a presheaf of rings
and `R` a sheaf of rings (i.e. `R` identifies to the sheafification of `R₀`), this is
the associated sheaf of modules functor `PresheafOfModules.{v} R₀ ⥤ SheafOfModules.{v} R`.  -/
PresheafOfModules.sheafification : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [CategoryTheory.Presheaf.IsLocallySurjective J α] →
                [J.WEqualsLocallyBijective AddCommGrpCat] →
                  [CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
                    CategoryTheory.Functor (PresheafOfModules R₀) (SheafOfModules R)
-- Mathlib.RingTheory.ChainOfDivisors
DivisorChain.first_of_chain_isUnit : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {q : Associates M} {n : ℕ}
  {c : Fin (n + 1) → Associates M}, StrictMono c → (∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) → IsUnit (c 0)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {fallback : α}
  {hc : t.minD fallback ∈ t}, t.get (t.minD fallback) hc = t.minD fallback
-- Mathlib.Algebra.Order.Group.OrderIso
/-- **Alias** of the forward direction of `neg_le`. -/
neg_le_of_neg_le : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] [AddRightMono α] {a b : α}, -a ≤ b → -b ≤ a
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc.injEq : ∀ (toErase toErase_1 : Lean.Name),
  (Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc toErase =
      Lean.Elab.Tactic.ElabSimpArgResult.eraseSimproc toErase_1) =
    (toErase = toErase_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_eq_lineMap_iff : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] [IsDomain k] [Module.IsTorsionFree k V1] {p₀ p₁ : P1} {c₁ c₂ : k},
  (AffineMap.lineMap p₀ p₁) c₁ = (AffineMap.lineMap p₀ p₁) c₂ ↔ p₀ = p₁ ∨ c₁ = c₂
-- Mathlib.Analysis.Complex.ReImTopology
Complex.closure_setOfPred_re_lt : ∀ (a : ℝ), closure {z | z.re < a} = {z | z.re ≤ a}
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balanced_inner_iff : ∀ {α : Type u} {β : α → Type v} {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Balanced ↔
    l.Balanced ∧ r.Balanced ∧ Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size ∧ sz = l.size + 1 + r.size
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsStationary.of_not_isCofinal_compl : ∀ {α : Type v} {s : Set α} [inst : LinearOrder α], ¬IsCofinal sᶜ → IsStationary s
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
ClosedSubmodule.involutive_mulI : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [ipc : InnerProductSpace ℂ H], Function.Involutive ClosedSubmodule.mulI
-- Mathlib.SetTheory.Ordinal.Notation
NONote.repr_mul : ∀ (a b : NONote), (a * b).repr = a.repr * b.repr
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.foldl.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} (f : δ → (α : α) → β α → δ) (init : δ)
  (as : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.foldl f init as =
    (Std.DHashMap.Internal.AssocList.foldlM (fun x1 x2 x3 => pure (f x1 x2 x3)) init as).run
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- The `Derivation` associated with the ring.  -/
Differential.«term_′» : Lean.TrailingParserDescr
-- Mathlib.Topology.MetricSpace.Bounded
/-- **Alias** of the forward direction of `Metric.isBounded_iff_ediam_ne_top`.

---

Characterize the boundedness of a set in terms of the finiteness of its emetric.diameter.  -/
Bornology.IsBounded.ediam_ne_top : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], Bornology.IsBounded s → Metric.ediam s ≠ ⊤
-- Mathlib.Topology.Order
TopologicalSpace.nhds_generateFrom : ∀ {α : Type u} {g : Set (Set α)} {a : α}, nhds a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, Filter.principal s
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_range_self : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] {f : α → ZFSet.{u}} (a : α), f a ∈ ZFSet.range f
-- Init.Data.UInt.Lemmas
UInt16.eq_iff_toBitVec_eq : ∀ {a b : UInt16}, a = b ↔ a.toBitVec = b.toBitVec
-- Lean.Meta.Tactic.Grind.AC.Types
/-- Mapping from operators to its "operator id". We cache failures using `none`.
`opIdOf[op]` is `some id`, then `id < structs.size`.  -/
Lean.Meta.Grind.AC.State.opIdOf : Lean.Meta.Grind.AC.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.instAddCommMonoid : {ι : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] → {I₀ : WithTop (BoxIntegral.Box ι)} → AddCommMonoid (BoxIntegral.BoxAdditiveMap ι M I₀)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Removal
SimpleGraph.triangleRemovalBound.eq_1 : ∀ (ε : ℝ),
  SimpleGraph.triangleRemovalBound ε =
    min (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ ((1 - min 1 ε / 4) * (ε / (16 * ↑(SzemerediRegularity.bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (p : Lean.Grind.CommRing.Poly)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p))
  (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p_1 : Lean.Grind.CommRing.Poly),
  p = Lean.Grind.CommRing.Poly.add k m p_1 →
    (match p with
      | Lean.Grind.CommRing.Poly.num k => h_1 k
      | Lean.Grind.CommRing.Poly.add k m p => h_2 k m p) ≍
      h_2 k m p_1
-- Init.Data.Array.GetLit
Array.toArrayLit : {α : Type u_1} → (xs : Array α) → (n : ℕ) → xs.size = n → Array α
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.mapL_coe : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {E' : ι → Type u_5}
  [inst_4 : (i : ι) → SeminormedAddCommGroup (E' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (E' i)]
  (f : (i : ι) → E i →L[𝕜] E' i), ↑(PiTensorProduct.mapL f) = PiTensorProduct.map fun i => ↑(f i)