mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.hasColimit_of_locallyDirected : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange] [P.IsMultiplicative]
  {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (D : CategoryTheory.Functor J (P.Over ⊤ S)) (𝒰 : S.OpenCover) [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀]
  [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰],
  (∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij)) →
    ∀
      [∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
          CategoryTheory.Limits.PreservesColimitsOfShape J
            (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
      [∀ (i : 𝒰.I₀),
          CategoryTheory.Limits.HasColimit (D.comp (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (𝒰.f i)))]
      [Quiver.IsThin 𝒰.I₀] [Small.{u, u_2} 𝒰.I₀] [AlgebraicGeometry.IsZariskiLocalAtTarget P],
      CategoryTheory.Limits.HasColimit D
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_subset_support_append_left : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w), p.support ⊆ (p.append q).support
-- Mathlib.Order.CompleteLatticeIntervals
/-- `InfSet` structure on a nonempty subset `s` of a preorder with `InfSet`. This definition is
non-canonical (it uses `default s`); it should be used only as here, as an auxiliary instance in the
construction of the `ConditionallyCompleteLinearOrder` structure.  -/
subsetInfSet : {α : Type u_2} → (s : Set α) → [Preorder α] → [InfSet α] → [Inhabited ↑s] → InfSet ↑s
-- Mathlib.Algebra.Lie.Rank
LieModule.polyCharpoly_coeff_rank_ne_zero : ∀ (R : Type u_1) (L : Type u_3) (M : Type u_4) {ι : Type u_5} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : AddCommGroup M]
  [inst_6 : Module R M] [inst_7 : LieRingModule L M] [inst_8 : LieModule R L M] [inst_9 : Module.Finite R M]
  [inst_10 : Module.Free R M] [inst_11 : Fintype ι] (b : Module.Basis ι R L) [Nontrivial R] [inst_13 : DecidableEq ι],
  ((↑(LieModule.toEnd R L M)).polyCharpoly b).coeff (LieModule.rank R L M) ≠ 0
-- Init.Data.Vector.MapIdx
Vector.getElem?_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : ℕ → α → β} {xs : Vector α n} {i : ℕ},
  (Vector.mapIdx f xs)[i]? = Option.map (f i) xs[i]?
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
/-- If `g` is parabolic, this is the unique fixed point of `g` in `OnePoint K`.  -/
Matrix.GeneralLinearGroup.parabolicFixedPoint : {K : Type u_1} → [inst : Field K] → [DecidableEq K] → GL (Fin 2) K → OnePoint K
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_insertIfNew_le_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k} {km kmi : α},
  t.minKey? = some km → (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.diseq_split_resolve : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsLinearOrder α] [Lean.Grind.OrderedAdd α] (ctx : Lean.Grind.Linarith.Context α)
  (p₁ p₂ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.diseq_split_cert p₁ p₂ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ ≠ 0 →
      ¬Lean.Grind.Linarith.Poly.denote' ctx p₁ < 0 → Lean.Grind.Linarith.Poly.denote' ctx p₂ < 0
-- Init.Data.Int.Lemmas
Int.zero_mul : ∀ (a : ℤ), 0 * a = 0
-- Mathlib.Algebra.Group.Units.Equiv
/-- A version of `Equiv.addLeft a (-b)` that is defeq to `a - b`.  -/
Equiv.subLeft : {G : Type u_5} → [AddGroup G] → G → G ≃ G
-- Mathlib.RingTheory.WittVector.Defs
WittVector.peval.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {k : ℕ} (φ : MvPolynomial (Fin k × ℕ) ℤ) (x : Fin k → ℕ → R),
  WittVector.peval φ x = (MvPolynomial.aeval (Function.uncurry x)) φ
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.liftEquiv_symm_apply_coe : ∀ {S : Type u_1} {R : Type u} {M : Type v} [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M]
  [inst_7 : SMulCommClass R Rᵐᵒᵖ M] [inst_8 : IsScalarTower S R M] [inst_9 : IsScalarTower S Rᵐᵒᵖ M] {A : Type u_2}
  [inst_10 : Semiring A] [inst_11 : Algebra S A] (F : TrivSqZeroExt R M →ₐ[S] A),
  ↑(TrivSqZeroExt.liftEquiv.symm F) =
    (F.comp (TrivSqZeroExt.inlAlgHom S R M), F.toLinearMap ∘ₗ ↑S (TrivSqZeroExt.inrHom R M))
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.mul_const_lt_weak : ∀ {α : Type u_1} {b c : α} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α],
  b < c → ∀ {a : α}, 0 ≤ a → a * b ≤ a * c
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.exists_ne_zero_and_lt_and_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : WithZero α} [NoMinOrder α], x ≠ 0 → y ≠ 0 → ∃ z, z ≠ 0 ∧ z < x ∧ z < y
-- Mathlib.Data.Complex.Basic
/-- The inequality `s × t ⊆ s₁ × t₁` holds in `ℂ` iff it holds in `ℝ × ℝ`.  -/
Complex.reProdIm_subset_iff : ∀ {s s₁ t t₁ : Set ℝ}, s ×ℂ t ⊆ s₁ ×ℂ t₁ ↔ s ×ˢ t ⊆ s₁ ×ˢ t₁
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic.0.termY : Lean.ParserDescr
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Encode.0.Lean.Meta.RefinedDiscrTree.encodingStepAux : Lean.Expr → List Lean.FVarId → Bool → Lean.Meta.RefinedDiscrTree.LazyM✝ Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Analysis.Complex.HasPrimitives
Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E] {U : Set ℂ},
  IsOpen U → (Complex.IsConservativeOn f U ∧ ContinuousOn f U ↔ DifferentiableOn ℂ f U)
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.piIsoPi_hom_ker_subtype_apply : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : CategoryTheory.Limits.HasProduct Z] (i : ι)
  (x : ↑(∏ᶜ Z)),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.piIsoPi Z).hom) x i =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π Z i)) x
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_lineMap_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, x ∈ s → y ∉ s → ∀ {t : R}, 0 < t → s.SSameSide y ((AffineMap.lineMap x y) t)
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.minpoly.map_eq_prod : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsSeparable K L]
  [Normal K L] (c : ConjRootClass K L) [inst_5 : Fintype ↑c.carrier],
  Polynomial.map (algebraMap K L) c.minpoly = ∏ x ∈ c.carrier.toFinset, (Polynomial.X - Polynomial.C x)
-- Mathlib.GroupTheory.Congruence.Defs
/-- In order to define a function `(Con.Quotient c)ˣ → α` on the units of `Con.Quotient c`,
where `c : Con M` is a multiplicative congruence on a monoid, it suffices to define a function `f`
that takes elements `x y : M` with proofs of `c (x * y) 1` and `c (y * x) 1`, and returns an element
of `α` provided that `f x y _ _ = f x' y' _ _` whenever `c x x'` and `c y y'`.  -/
Con.liftOnUnits : {M : Type u_1} →
  {α : Type u_4} →
    [inst : Monoid M] →
      {c : Con M} →
        c.Quotientˣ →
          (f : (x y : M) → c (x * y) 1 → c (y * x) 1 → α) →
            (∀ (x y : M) (hxy : c (x * y) 1) (hyx : c (y * x) 1) (x' y' : M) (hxy' : c (x' * y') 1)
                (hyx' : c (y' * x') 1), c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx') →
              α
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.mk : {G : Type u_6} →
  [inst : Group G] →
    (toFun : G → ℝ) →
      toFun 1 = 0 →
        (∀ (x y : G), toFun (x * y) ≤ toFun x + toFun y) → (∀ (x : G), toFun x⁻¹ = toFun x) → GroupSeminorm G
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
ContinuousLinearMap.iInf_rayleigh_eq_iInf_rayleigh_sphere : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (T : E →L[𝕜] E) {r : ℝ}, 0 < r → ⨅ x, T.rayleighQuotient ↑x = ⨅ x, T.rayleighQuotient ↑x
-- Mathlib.Probability.Kernel.Basic
/-- Kernel given by the restriction of the measures in the image of a kernel to a set.  -/
ProbabilityTheory.Kernel.restrict : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {s : Set β} → ProbabilityTheory.Kernel α β → MeasurableSet s → ProbabilityTheory.Kernel α β
-- Init.Data.UInt.Lemmas
UInt8.le_ofNat_iff : ∀ {n : UInt8} {m : ℕ}, m < UInt8.size → (n ≤ UInt8.ofNat m ↔ n.toNat ≤ m)
-- Mathlib.Logic.IsEmpty.Basic
Function.surjective_iff_isEmpty : ∀ {α : Type u_4} {β : Type u_5} [IsEmpty α] (f : α → β), Function.Surjective f ↔ IsEmpty β
-- Mathlib.Order.Hom.BoundedLattice
/-- `InfTopHomClass F α β` states that `F` is a type of finitary infimum-preserving morphisms.

You should extend this class when you extend `SupBotHom`.  -/
InfTopHomClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [Min α] → [Min β] → [Top α] → [Top β] → [FunLike F α β] → Prop
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.op_X' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y), φ.op.X' = Opposite.op φ.Y'
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.sound : ∀ {G : Type u} [inst : Group G] (N : Subgroup G) [nN : N.Normal] (U : Set (G ⧸ N)) (g : ↥N.op),
  g • ⇑(QuotientGroup.mk' N) ⁻¹' U = ⇑(QuotientGroup.mk' N) ⁻¹' U
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.elim.eq_3 : ∀ (a b c d : List Turing.PartrecToTM2.Γ'), Turing.PartrecToTM2.K'.elim a b c d Turing.PartrecToTM2.K'.aux = c
-- Mathlib.Order.Sublattice
Sublattice.coe_inclusion : ∀ {α : Type u_2} [inst : Lattice α] {L M : Sublattice α} (h : L ≤ M), ⇑(Sublattice.inclusion h) = Set.inclusion h
-- Mathlib.Topology.Maps.Proper.Basic
/-- An injective continuous and closed map is proper.  -/
isProperMap_of_isClosedMap_of_inj : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → Function.Injective f → IsClosedMap f → IsProperMap f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
Complex.cot_eq_exp_ratio : ∀ (z : ℂ), z.cot = (Complex.exp (2 * Complex.I * z) + 1) / (Complex.I * (1 - Complex.exp (2 * Complex.I * z)))
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.foldlM_list_const_inv : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : List α} {init : β} {f : β → α → m β} {inv : β → Pred}
  {epost : EPred},
  (∀ (hd : α) (b : β), ⦃ inv b ⦄ f b hd ⦃ fun b' => inv b'; epost ⦄) → ⦃ inv init ⦄ List.foldlM f init xs ⦃ inv; epost ⦄
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_preimage_of_notMem : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (s : Set α) (f : α → M) {t : Set M},
  0 ∉ t → s.indicator f ⁻¹' t = f ⁻¹' t ∩ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffine_some : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {X Y : F} (h : W.Nonsingular ![X, Y, 1]),
  WeierstrassCurve.Jacobian.Point.toAffine W ![X, Y, 1] = WeierstrassCurve.Affine.Point.some X Y ⋯
-- Mathlib.Topology.Instances.EReal.Lemmas
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_swap : ∀ {a b : EReal}, ContinuousAt (fun p => p.1 * p.2) (a, b) → ContinuousAt (fun p => p.1 * p.2) (b, a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {he : t.isEmpty = false} {hc : Std.DTreeMap.Internal.Impl.contains (t.maxKey he) t = true},
      t.getKey (t.maxKey he) hc = t.maxKey he
-- Mathlib.Analysis.BoxIntegral.Integrability
/-- If `f : ℝⁿ → E` is Bochner integrable w.r.t. a locally finite measure `μ` on a rectangular box
`I`, then it is McShane integrable on `I` with the same integral.  -/
MeasureTheory.IntegrableOn.hasBoxIntegral : ∀ {ι : Type u} {E : Type v} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [CompleteSpace E] {f : (ι → ℝ) → E} {μ : MeasureTheory.Measure (ι → ℝ)}
  [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] {I : BoxIntegral.Box ι},
  MeasureTheory.IntegrableOn f (↑I) μ →
    ∀ (l : BoxIntegral.IntegrationParams),
      l.bRiemann = false → BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.mapsTo_closedEBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  LipschitzWith K f → ∀ (x : α) (r : ENNReal), Set.MapsTo f (Metric.closedEBall x r) (Metric.closedEBall (f x) (↑K * r))
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.toIsQuotientMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E], IsQuotientCoveringMap f G → Topology.IsQuotientMap f
-- Std.Sync.SharedMutex
/-- `mutex.tryAtomically k` tries to lock `mutex` for exclusive write access and runs `k` with read
and write access to the mutex's state if it succeeds. If successful, it returns the value of `k`
as `some`, otherwise `none`.

Calling `mutex.tryAtomically` while already holding the underlying `BaseSharedMutex` in the same
thread is undefined behavior.
 -/
Std.SharedMutex.tryAtomically : {m : Type → Type} →
  {α β : Type} →
    [Monad m] → [MonadLiftT BaseIO m] → [MonadFinally m] → Std.SharedMutex α → Std.AtomicT α m β → m (Option β)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.isGround.inj : ∀ {bvarIdx bvarIdx_1 : ℕ},
  Lean.Meta.Grind.EMatchTheoremConstraint.isGround bvarIdx =
      Lean.Meta.Grind.EMatchTheoremConstraint.isGround bvarIdx_1 →
    bvarIdx = bvarIdx_1
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- `E →ₗ[𝕜] E` is a star algebra with the adjoint as the star operation.  -/
LinearMap.instStarId : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → [FiniteDimensional 𝕜 E] → Star (E →ₗ[𝕜] E)
-- Mathlib.Topology.Sober
genericPoints.isGenericPoint_ofComponent : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] (x : ↑(irreducibleComponents α)),
  IsGenericPoint ↑(genericPoints.ofComponent x) ↑x
-- Mathlib.Data.Matrix.Mul
Matrix.mul_neg : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalNonAssocRing α] [inst_1 : Fintype n]
  (M : Matrix m n α) (N : Matrix n o α), M * -N = -(M * N)
-- Init.Data.BitVec.Lemmas
BitVec.or_not_self : ∀ {w : ℕ} (x : BitVec w), x ||| ~~~x = BitVec.allOnes w
-- Mathlib.LinearAlgebra.Determinant
/-- The determinant of a map vanishes iff the map is not injective.  -/
LinearMap.det_eq_zero_iff_ker_ne_bot : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.Free R M] [Module.Finite R M] {f : M →ₗ[R] M}, LinearMap.det f = 0 ↔ f.ker ≠ ⊥
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- **Alias** of `SimpleGraph.colorable_iff_forall_connectedComponent`. -/
SimpleGraph.colorable_iff_forall_connectedComponents : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.Colorable n ↔ ∀ (c : G.ConnectedComponent), c.toSimpleGraph.Colorable n
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.coe_mul : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {x y : ℚ}, ↑(x * y) = ↑x * ↑y
-- Mathlib.Topology.Constructions.SumProd
Topology.IsOpenEmbedding.sumElim : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z},
  Topology.IsOpenEmbedding f →
    Topology.IsOpenEmbedding g → Function.Injective (Sum.elim f g) → Topology.IsOpenEmbedding (Sum.elim f g)
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- On local sites, the global sections functor `Γ` is left-adjoint to the coconstant functor.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.ΓCoconstantSheafAdj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_2 : J.IsLocalSite] →
          (A : Type u') →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [inst_5 : CategoryTheory.Limits.HasProducts A] →
                  [inst_6 : CategoryTheory.HasWeakSheafify J A] →
                    CategoryTheory.Sheaf.Γ J A ⊣ CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Pretty-prints the parameters of a `forall`. The pretty-printed parameters are passed to
`delabForall` at the end.
 -/
Lean.PrettyPrinter.Delaborator.delabForallParamsWithSignature : {α : Type} →
  (Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder → Lean.Term → Lean.PrettyPrinter.Delaborator.DelabM α) →
    Lean.PrettyPrinter.Delaborator.DelabM α
-- Std.Data.HashSet.Basic
/-- Computes the intersection of the given hash sets. The result will only contain entries from the first map.

This function always iterates through the smaller set, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.HashSet.inter : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → Std.HashSet α → Std.HashSet α → Std.HashSet α
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.hom_inv_id_hom_app_assoc : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (e : F ≅ G) (n : A) (X : C) {Z : D}
  (h : (F.functor n).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((e.hom.hom n).app X)
      (CategoryTheory.CategoryStruct.comp ((e.inv.hom n).app X) h) =
    h
-- Mathlib.LinearAlgebra.StdBasis
/-- The product of finitely many free modules is free.  -/
Module.Free.pi : ∀ {ι : Type u_1} (R : Type u_2) [inst : Semiring R] (M : ι → Type u_4) [Finite ι]
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Free R (M i)],
  Module.Free R ((i : ι) → M i)
-- Mathlib.CategoryTheory.Enriched.Basic
/-- A `V`-functor `F` between `V`-enriched categories
has a `V`-morphism from `X ⟶[V] Y` to `F.obj X ⟶[V] F.obj Y`,
satisfying the usual axioms.
 -/
CategoryTheory.EnrichedFunctor : (V : Type v) →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (C : Type u₁) →
        [CategoryTheory.EnrichedCategory V C] →
          (D : Type u₂) → [CategoryTheory.EnrichedCategory V D] → Type (max (max u₁ u₂) w)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_toArray_rcc : ∀ {m n : ℕ}, (m...=n).toArray.toList = (m...=n).toList
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.toSheafification_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] (P : CategoryTheory.Functor Cᵒᵖ D),
  (J.toSheafification D).app P = J.toSheafify P
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_append : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {a : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr a} {a_1 : ℕ}
  {rhs : Std.Tactic.BVDecide.BVExpr a_1} {h : a + a_1 = a + a_1},
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.append rhs h) =
    Std.Tactic.BVDecide.BVExpr.eval assign lhs ++ Std.Tactic.BVDecide.BVExpr.eval assign rhs
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The Tate norm connecting complexes of inhomogeneous chains and cochains.  -/
tateComplexConnectData : {R G : Type u} →
  [inst : CommRing R] →
    [inst_1 : Group G] →
      [Fintype G] →
        (M : Rep.{u, u, u} R G) →
          CochainComplex.ConnectData (groupHomology.inhomogeneousChains M) (groupCohomology.inhomogeneousCochains M)
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.map_add : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S) (x y : R), f (x + y) = f x + f y
-- Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
/-- If `A` is a family of enough low-degree polynomials over a finite ring,
there is a pair of elements in `A` (with different indices but not necessarily
distinct), such that their difference has small degree.  -/
Polynomial.exists_approx_polynomial_aux : ∀ {Fq : Type u_1} [inst : Fintype Fq] [inst_1 : Ring Fq] {d m : ℕ},
  Fintype.card Fq ^ d ≤ m →
    ∀ (b : Polynomial Fq) (A : Fin m.succ → Polynomial Fq),
      (∀ (i : Fin m.succ), (A i).degree < b.degree) → ∃ i₀ i₁, i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < ↑(b.natDegree - d)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_associator' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X)
              (CategoryTheory.Functor.OplaxMonoidal.δ F Y Z)))))
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.exists_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (x : X), ∃ n, x ∈ K n
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono
PresheafOfModules.mono_of_injective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} {f : M₁ ⟶ M₂},
  (∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (f.app X))) → CategoryTheory.Mono f