mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Module.Defs
inv_smul_le_iff_of_pos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b₁ b₂ : β} [inst : GroupWithZero α] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : MulAction α β] [PosSMulMono α β] [PosSMulReflectLE α β], 0 < a → (a⁻¹ • b₁ ≤ b₂ ↔ b₁ ≤ a • b₂)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpenIsoSpec_inv_ι_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Proj 𝒜 ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpenIsoSpec 𝒜 f f_deg hm).inv
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.basicOpen 𝒜 f).ι h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm) h
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.restrictScalarsEquiv_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : Ring S] [inst_4 : SMul S R] [inst_5 : Module S M] [inst_6 : IsScalarTower S R M] (P : Submodule R M)
  (x : M), (Submodule.Quotient.restrictScalarsEquiv S P) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.fundCircuit_eq_of_notMem_ground : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {e : α}, e ∉ M.E → M.fundCircuit e X = {e}
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  t.alter k f ≠ ∅ → ((t.alter k f).minKey! = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Batteries.Data.Array.Basic
/-- Find the first minimal element of an array. If the array is empty, `none` is
returned. If `start` and `stop` are given, only the subarray `xs[start...stop]` is
considered.
 -/
Array.rangeMin? : {α : Type u_1} → [ord : Ord α] → (xs : Array α) → optParam ℕ 0 → optParam ℕ xs.size → Option α
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_coeff_natDegree : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.eraseLead.coeff f.natDegree = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Extract an isomorphism
`(pointwiseLeftKanExtension L F) ⋙ G ≅ pointwiseLeftKanExtension L (F ⋙ G)` when `G` preserves
left Kan extensions.  -/
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves : {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.PreservesPointwiseLeftKanExtension F L] →
                        [inst_5 : L.HasPointwiseLeftKanExtension F] →
                          (L.pointwiseLeftKanExtension F).comp G ≅ L.pointwiseLeftKanExtension (F.comp G)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.exists_pos_forall_lt_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  IsCompact s → IsClosed t → Disjoint s t → ∃ r, 0 < r ∧ ∀ x ∈ s, ∀ y ∈ t, ↑r < edist x y
-- Init.Prelude
/-- Unsigned 16-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 16-bit value
rather than wrapping a `BitVec 16`.
 -/
UInt16 : Type
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.forget_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : CategoryTheory.CommMon C} (f : X ⟶ Y),
  (CategoryTheory.CommMon.forget C).map f = f.hom.hom
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.symm_trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁), (p.symm.trans p).Homotopic (Path.refl x₁)
-- Mathlib.Order.Basic
Prod.lt_of_le_of_lt : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {x y : α × β}, x.1 ≤ y.1 → x.2 < y.2 → x < y
-- Mathlib.Topology.ContinuousMap.Compact
BoundedContinuousFunction.mkOfCompact.congr_simp : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : CompactSpace α]
  (f f_1 : C(α, β)), f = f_1 → BoundedContinuousFunction.mkOfCompact f = BoundedContinuousFunction.mkOfCompact f_1
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.isPullback_morphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens),
  CategoryTheory.IsPullback (f ∣_ U) ((TopologicalSpace.Opens.map f.base).obj U).ι U.ι f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.HashMap.Raw.ofList l).getKeyD k' fallback = k
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_sum_of_fintype : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : Fintype α] (f : α → M), ∑ᶠ (i : α), f i = ∑ i, f i
-- Mathlib.LinearAlgebra.Matrix.Invertible
Matrix.transposeInvertibleEquivInvertible_apply : ∀ {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring α] (A : Matrix n n α)
  [inst_3 : Invertible A.transpose], A.transposeInvertibleEquivInvertible inst_3 = A.invertibleOfInvertibleTranspose
-- Init.System.ST
ST.Prim.Ref.modify : {σ α : Type} → ST.Ref σ α → (α → α) → ST σ Unit
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
measurableEmbedding_mulLeft : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [MeasurableMul G] (g : G),
  MeasurableEmbedding fun x => g * x
-- Mathlib.Analysis.Convex.Gauge
_private.Mathlib.Analysis.Convex.Gauge.0.bddBelow_gauge_set : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E}, BddBelow {r | 0 < r ∧ x ∈ r • s}
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.homology ⟶ Z)
  (x : ↑S.moduleCatLeftHomologyData.K),
  (CategoryTheory.ConcreteCategory.hom h)
      ((CategoryTheory.ConcreteCategory.hom S.homologyπ)
        ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.inv) x)) =
    (CategoryTheory.ConcreteCategory.hom h)
      ((CategoryTheory.ConcreteCategory.hom S.moduleCatHomologyIso.inv)
        ((CategoryTheory.ConcreteCategory.hom S.moduleCatLeftHomologyData.π) x))
-- Mathlib.Algebra.Homology.ImageToKernel
image_le_kernel : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g],
  CategoryTheory.CategoryStruct.comp f g = 0 →
    CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g
-- Mathlib.Condensed.EffectiveEpi
instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed : compHausToCondensed.PreservesEpimorphisms
-- Mathlib.Topology.Clopen
IsClopen.compl : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClopen s → IsClopen sᶜ
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelopeIter_le_triangEnvelope : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (n : ℕ), P.triangEnvelopeIter n ≤ P.triangEnvelope
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.Entry.ext.injEq : ∀ (declName declName_1 : Lean.Name),
  (Lean.Meta.Grind.Entry.ext declName = Lean.Meta.Grind.Entry.ext declName_1) = (declName = declName_1)
-- Mathlib.Data.Set.Card
Set.ncard_exchange' : ∀ {α : Type u_1} {s : Set α} {a b : α}, a ∉ s → b ∈ s → (insert a s \ {b}).ncard = s.ncard
-- Mathlib.Order.Category.DistLat
DistLat.inv_hom_apply : ∀ {X Y : DistLat} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.comp_l : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {X Y Z : CategoryTheory.Bicategory.Adj B}
  (f : CategoryTheory.Bicategory.Adj.Hom X.obj Y.obj) (g : CategoryTheory.Bicategory.Adj.Hom Y.obj Z.obj),
  (CategoryTheory.CategoryStruct.comp f g).l = CategoryTheory.CategoryStruct.comp f.l g.l
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conj_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : CategoryTheory.End X),
  α.conj (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (α.conj f) (α.conj g)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`.  -/
Orientation.oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [hd2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  o.oangle x y = ↑(Real.pi / 2) → o.oangle (x + y) y = ↑(Real.arctan (‖x‖ / ‖y‖))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.sum_eq_zero_of_mem_span_completeFamily : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.realSpace K},
  x ∈ Submodule.span ℝ (Set.range fun w => NumberField.mixedEmbedding.fundamentalCone.completeFamily K ↑w) →
    ∑ w, x w = 0
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.map_id : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] (f : A),
  HomogeneousLocalization.Away.map (GradedRingHom.id 𝒜) f = RingHom.id (HomogeneousLocalization.Away 𝒜 f)
-- Batteries.Data.Array.Scan
Array.scanl_eq_singleton_iff : ∀ {β : Type u_1} {α : Type u_2} {init : β} {as : Array α} {f : β → α → β} (c : β),
  Array.scanl f init as = #[c] ↔ c = init ∧ as = #[]
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_sSup' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set (Submodule R M)), Submodule.span R ↑(sSup s) = sSup s
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {F : CategoryTheory.Functor C C} {V : C} {str : V ⟶ F.obj V}
  {V_1 : C} {str_1 : V_1 ⟶ F.obj V_1}, { V := V, str := str } = { V := V_1, str := str_1 } → V = V_1 ∧ str ≍ str_1
-- Mathlib.GroupTheory.CommutingProbability
commProb_def' : ∀ (G : Type u_2) [inst : Group G], commProb G = ↑(Nat.card (ConjClasses G)) / ↑(Nat.card G)
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.Types.binaryCoproductIso_inl_comp_inv_apply : ∀ (X Y : Type u) (x : X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryCoproductIso X Y).inv) (Sum.inl x) =
    (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.coprod.inl) x
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.mk.inj : ∀ {α : Type} {tries : Array (Lean.Meta.LazyDiscrTree.Trie α)}
  {roots : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex}
  {tries_1 : Array (Lean.Meta.LazyDiscrTree.Trie α)}
  {roots_1 : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex},
  { tries := tries, roots := roots } = { tries := tries_1, roots := roots_1 } → tries = tries_1 ∧ roots = roots_1
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.of_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_3 : CategoryTheory.Limits.PreservesFiniteColimits F], (CategoryTheory.ExactFunctor.of F).obj = F
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₈_of_isCharTwoJEqZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2], W.b₈ = W.a₄ ^ 2
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycle_inv : ∀ {α : Type u_2} {f : Equiv.Perm α}, f⁻¹.IsCycle ↔ f.IsCycle
-- Init.PropLemmas
imp_or_left_iff_true : ∀ {P Q : Prop}, P → P ∨ Q ↔ True
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_inter!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter! m₂).get? k = none
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- The underlying function of an `OrderHom` is monotone.  -/
PositiveLinearMap.monotone' : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] (self : E₁ →ₚ[R] E₂), Monotone self.toFun
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.prod.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass P] (f : M →+ N) (g : M →+ P),
  f.prod g = { toFun := Function.prod ⇑f ⇑g, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balancedAtRoot_one_zero : Std.DTreeMap.Internal.Impl.BalancedAtRoot 1 0
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instPowISizeSintNumBits : Lean.Grind.ToInt.Pow ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
-- Mathlib.Data.Ordmap.Ordset
/-- An `Ordset α` is a finite set of values, represented as a tree. The operations on this type
maintain that the tree is balanced and correctly stores subtree sizes at each level. The
correctness property of the tree is baked into the type, so all operations on this type are correct
by construction.  -/
Ordset : (α : Type u_2) → [Preorder α] → Type (max 0 u_2)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Sheaf.interUnionPullbackConeLift.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X)
  (s :
    CategoryTheory.Limits.PullbackCone (F.obj.map (CategoryTheory.homOfLE ⋯).op)
      (F.obj.map (CategoryTheory.homOfLE ⋯).op)),
  F.interUnionPullbackConeLift U V s =
    CategoryTheory.CategoryStruct.comp
      (⋯.some.lift
        { pt := s.pt,
          π :=
            {
              app := fun X_1 =>
                Opposite.casesOn X_1 fun unop =>
                  CategoryTheory.Pairwise.casesOn unop
                    (fun a => ULift.casesOn a fun down => CategoryTheory.Limits.WalkingPair.casesOn down s.fst s.snd)
                    fun a a_1 =>
                    ULift.casesOn a fun down =>
                      CategoryTheory.Limits.WalkingPair.casesOn down
                        (CategoryTheory.CategoryStruct.comp s.fst (F.obj.map (CategoryTheory.homOfLE ⋯).op))
                        (CategoryTheory.CategoryStruct.comp s.snd (F.obj.map (CategoryTheory.homOfLE ⋯).op)),
              naturality := ⋯ } })
      (F.obj.map (CategoryTheory.eqToHom ⋯).op)
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.unitIso_inv_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  (X : CategoryTheory.Sheaf J A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongr.unitIso J K e A).inv.app X).hom.app X_1 =
    X.obj.map (e.unitIso.hom.app (Opposite.unop X_1)).op
-- Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology
/-- For a precoherent category, any sieve that contains an `EffectiveEpiFamily` is a sieve of the
coherent topology.
Note: This is one direction of `mem_sieves_iff_hasEffectiveEpiFamily`, but is needed for the proof.
 -/
CategoryTheory.coherentTopology.mem_sieves_of_hasEffectiveEpiFamily : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Precoherent C] {X : C}
  (S : CategoryTheory.Sieve X),
  (∃ α, ∃ (_ : Finite α), ∃ Y π, CategoryTheory.EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)) →
    S ∈ (CategoryTheory.coherentTopology C) X
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.mul_smul : ∀ {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)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (r r' : ↑(R.obj.obj X)) (m : ↑(A.obj.obj X)),
  PresheafOfModules.Sheafify.smul α φ (r * r') m =
    PresheafOfModules.Sheafify.smul α φ r (PresheafOfModules.Sheafify.smul α φ r' m)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.congr_left : ∀ {α : Type u} {m₁ m₂ m₃ : Std.HashSet.Raw α}, m₁.Equiv m₂ → (m₁.Equiv m₃ ↔ m₂.Equiv m₃)
-- Init.Data.String.Subslice
String.Slice.instInhabitedSubslice : {s : String.Slice} → Inhabited s.Subslice
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
/-- The first projection from the pullback.  -/
TopCat.pullbackFst : {X Y Z : TopCat} →
  (f : X ⟶ Z) →
    (g : Y ⟶ Z) →
      TopCat.of { p // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 } ⟶ X
-- Mathlib.Data.Multiset.Count
Multiset.ext' : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, (∀ (a : α), Multiset.count a s = Multiset.count a t) → s = t
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.ofFn.go.match_1.splitter : {n : ℕ} →
  (motive : (x : ℕ) → x ≤ n → Sort u_1) →
    (x : ℕ) → (x_1 : x ≤ n) → ((i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h) → ((x : 0 ≤ n) → motive 0 x) → motive x x_1
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instInhabited : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → Inhabited (MeasureTheory.FiniteMeasure Ω)
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
/-- A family of 1-hypercovers generates the topology if any covering sieve
contains the sieve generated by the underlying covering of one of these 1-hypercovers.
See `OneHypercoverFamily.isSheaf_iff` for the characterization of sheaves.  -/
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsGenerating : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {J : CategoryTheory.GrothendieckTopology C} → J.OneHypercoverFamily → Prop
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
_private.Mathlib.RingTheory.DedekindDomain.SelmerGroup.0.«term_/__1» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- A morphism version of the `le_inf` axiom.  -/
CategoryTheory.MonoOver.leInf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {A : C} →
        (f g h : CategoryTheory.MonoOver A) → (h ⟶ f) → (h ⟶ g) → (h ⟶ (CategoryTheory.MonoOver.inf.obj f).obj g)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_alter_eq_add_one : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∉ t → (f t[k]?).isSome = true → (t.alter k f).size = t.size + 1
-- Mathlib.Data.Finsupp.SMul
Finsupp.filter_smul : ∀ {α : Type u_1} {M : Type u_3} {R : Type u_6} {p : α → Prop} [inst : DecidablePred p] [inst_1 : Zero M]
  [inst_2 : SMulZeroClass R M] {b : R} {v : α →₀ M}, Finsupp.filter p (b • v) = b • Finsupp.filter p v
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.pow_apply : ∀ {M : Type uM} {N : Type uN} [inst : One M] [inst_1 : Monoid N] (f : OneHom M N) (n : ℕ) (x : M), (f ^ n) x = f x ^ n
-- Init.MetaTypes
/-- Unfolds reducible, `[instance_reducible]`, and `[implicit_reducible]` constants.
Used for checking definitional equality of implicit and instance-implicit arguments.
 -/
Lean.Meta.TransparencyMode.implicit : Lean.Meta.TransparencyMode
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_liftSupQuotQuotMkₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ⇑(DoubleQuot.liftSupQuotQuotMkₐ R I J) = ⇑(DoubleQuot.liftSupQuotQuotMk I J)
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.of_isCompact_of_forall_exists_isCompactOpenCovered : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  [inst_1 : TopologicalSpace S] {U : Set S},
  IsCompact U → (∀ x ∈ U, ∃ t ⊆ U, x ∈ t ∧ IsOpen t ∧ IsCompactOpenCovered f t) → IsCompactOpenCovered f U
-- Mathlib.Data.Sigma.Basic
Sigma.eta : ∀ {α : Type u_1} {β : α → Type u_4} (x : (a : α) × β a), ⟨x.fst, x.snd⟩ = x
-- Mathlib.Topology.Constructions.SumProd
Prod.instNeBotNhdsWithinIoi : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder X]
  [inst_3 : Preorder Y] {x : X × Y} [hx₁ : (nhdsWithin x.1 (Set.Ioi x.1)).NeBot]
  [hx₂ : (nhdsWithin x.2 (Set.Ioi x.2)).NeBot], (nhdsWithin x (Set.Ioi x)).NeBot
-- Init.Data.Nat.Coprime
Nat.Coprime.coprime_dvd_right : ∀ {n m k : ℕ}, n ∣ m → k.Coprime m → k.Coprime n
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.apply_lie_eq_sub : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [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]
  (D : LieDerivation R L M) (a b : L), D ⁅a, b⁆ = ⁅a, D b⁆ - ⁅b, D a⁆
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.sheafedSpaceMap_hom_c_app : ∀ {R S : CommRingCat} (f : R ⟶ S)
  (U : (TopologicalSpace.Opens ↑↑(AlgebraicGeometry.Spec.sheafedSpaceObj R).toPresheafedSpace)ᵒᵖ),
  (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom.c.app U =
    CommRingCat.ofHom
      (AlgebraicGeometry.StructureSheaf.comap (CommRingCat.Hom.hom f) (Opposite.unop U)
        ((TopologicalSpace.Opens.map (AlgebraicGeometry.Spec.topMap f)).obj (Opposite.unop U)) ⋯)
-- Lean.Elab.DeclModifiers
Lean.linter.redundantVisibility : Lean.Option Bool
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.IsPushout.isIntegral' : ∀ (R : Type u_1) (A : Type u_2) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing S]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] [int : Algebra.IsIntegral R S] (SA : Type u_5) [inst_5 : CommRing SA]
  [inst_6 : Algebra R SA] [inst_7 : Algebra S SA] [inst_8 : Algebra A SA] [inst_9 : IsScalarTower R S SA]
  [inst_10 : IsScalarTower R A SA] [Algebra.IsPushout R A S SA], Algebra.IsIntegral A SA
-- Mathlib.NumberTheory.Divisors
Nat.Prime.prod_divisors : ∀ {α : Type u_1} [inst : CommMonoid α] {p : ℕ} {f : ℕ → α}, Nat.Prime p → ∏ x ∈ p.divisors, f x = f p * f 1