mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasure_comap : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} [mβ : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (f : β → α) [MeasureTheory.IsFiniteMeasure μ], MeasureTheory.IsFiniteMeasure (MeasureTheory.Measure.comap f μ)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_filter_le_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [Std.TransCmp cmp] {f : α → β → Bool},
  (Std.ExtTreeMap.filter f t).size ≤ t.size
-- Mathlib.Logic.Function.Basic
/-- A relation `r : α → β → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some function `f`.  -/
forall_existsUnique_iff' : ∀ {α : Sort u_1} {β : Sort u_2} {r : α → β → Prop}, (∀ (a : α), ∃! b, r a b) ↔ ∃ f, r = fun x1 x2 => f x1 = x2
-- Mathlib.Tactic.SwapVar
/-- `swap_var swap_rule₁, swap_rule₂, ⋯` applies `swap_rule₁` then `swap_rule₂` then `⋯`.

A `swap_rule` is of the form `x y` or `x ↔ y`, and "applying it" means swapping the variable name
`x` by `y` and vice-versa on all hypotheses and the goal.

```lean
example {P Q : Prop} (q : P) (p : Q) : P ∧ Q := by
  swap_var p ↔ q
  exact ⟨p, q⟩
```
 -/
Mathlib.Tactic.«tacticSwap_var__,,» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.balanceLErase_eq_balance : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced} {hlr : Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size},
  Std.DTreeMap.Internal.Impl.balanceLErase k v l r hlb hrb hlr = Std.DTreeMap.Internal.Impl.balance k v l r hlb hrb ⋯
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.subtype_injective : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G],
  Function.Injective ⇑↑H
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.map_constants_comp_sumInl : ∀ (L : FirstOrder.Language) {α : Type w'} {β : Type u_1} {f : α → β},
  (L.lhomWithConstantsMap f).comp FirstOrder.Language.LHom.sumInl = L.lhomWithConstants β
-- Batteries.Data.String.Lemmas
String.find_of_valid : ∀ (p : Char → Bool) (s : String),
  String.Legacy.find s p = { byteIdx := String.utf8Len (List.takeWhile (fun x => !p x) s.toList) }
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.min : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f g : β → α}
  {b : Filter β} {a₁ a₂ : α},
  Filter.Tendsto f b (nhds a₁) →
    Filter.Tendsto g b (nhds a₂) → Filter.Tendsto (fun b => min (f b) (g b)) b (nhds (min a₁ a₂))
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndInfo.mk.sizeOf_spec : ∀ (funName funIndName : Lean.Name) (levelMask : Array Bool) (params : Array Lean.Meta.FunIndParamKind),
  sizeOf { funName := funName, funIndName := funIndName, levelMask := levelMask, params := params } =
    1 + sizeOf funName + sizeOf funIndName + sizeOf levelMask + sizeOf params
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
Ideal.map_height_le_one_of_mem_minimalPrimes : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {I p : Ideal R} {x : R},
  p ∈ (I ⊔ Ideal.span {x}).minimalPrimes → (Ideal.map (Ideal.Quotient.mk I) p).height ≤ 1
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.exists_mem_closure_of_ge : ∀ (s : Set ℕ), ∃ n, ∀ m ≥ n, Nat.setGcd s ∣ m → m ∈ AddSubmonoid.closure s
-- Mathlib.Analysis.Calculus.LocalExtr.Polynomial
/-- The number of roots of a real polynomial `p` is at most the number of roots of its derivative
that are not roots of `p` plus one.  -/
Polynomial.card_roots_toFinset_le_card_roots_derivative_sdiff_roots_succ : ∀ (p : Polynomial ℝ), p.roots.toFinset.card ≤ ((Polynomial.derivative p).roots.toFinset \ p.roots.toFinset).card + 1
-- Lean.Language.Basic
/-- Trace data produced by this step. Currently used only by `trace.profiler.output`, otherwise we
depend on the elaborator adding traces to `diagnostics` eventually.
 -/
Lean.Language.Snapshot.traces : Lean.Language.Snapshot → Lean.TraceState
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.image_eball : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : α)
  (r : ENNReal), ⇑h '' Metric.eball x r = Metric.eball (h x) r
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.mk : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (toEquiv : M ≃ N) →
            autoParam
                (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
                  toEquiv.toFun (FirstOrder.Language.Structure.funMap f x) =
                    FirstOrder.Language.Structure.funMap f (toEquiv.toFun ∘ x))
                FirstOrder.Language.Equiv.map_fun'._autoParam →
              autoParam
                  (∀ {n : ℕ} (r : L.Relations n) (x : Fin n → M),
                    FirstOrder.Language.Structure.RelMap r (toEquiv.toFun ∘ x) ↔
                      FirstOrder.Language.Structure.RelMap r x)
                  FirstOrder.Language.Equiv.map_rel'._autoParam →
                L.Equiv M N
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.instDecidableIsSymmOfEqTranspose : {α : Type u_1} → {n : Type u_3} → (A : Matrix n n α) → [Decidable (A.transpose = A)] → Decidable A.IsSymm
-- Lean.Declaration
Lean.OpaqueVal.mk : Lean.ConstantVal → Lean.Expr → Bool → List Lean.Name → Lean.OpaqueVal
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_sup_le_and_aux_right : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  Filter.bliminf u f q ≤ Filter.bliminf u f fun x => p x ∧ q x
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- The instance `Algebra R A[M]` whenever we have `Algebra R A`.

In particular this provides the instance `Algebra R R[M]`.  -/
MonoidAlgebra.algebra : {R : Type u_1} →
  {A : Type u_4} →
    {M : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] → [Algebra R A] → [inst_3 : Monoid M] → Algebra R (MonoidAlgebra A M)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.Icc_add_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α}
  {a b c : α},
  a ≤ b →
    b ≤ c →
      b ∈ s → eVariationOn f (s ∩ Set.Icc a b) + eVariationOn f (s ∩ Set.Icc b c) = eVariationOn f (s ∩ Set.Icc a c)
-- Mathlib.NumberTheory.Divisors
/-- This lemma justifies its existence from its utility in crystallographic root system theory.  -/
Int.mul_mem_one_two_three_iff : ∀ {a b : ℤ},
  a * b ∈ {1, 2, 3} ↔
    (a, b) ∈ {(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
-- Mathlib.Topology.Separation.Basic
/-- If `t` is a subset of `s`, except for one point,
then `insert x s` is a neighborhood of `x` within `t`.  -/
insert_mem_nhdsWithin_of_subset_insert : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X} {s t : Set X},
  t ⊆ insert y s → insert x s ∈ nhdsWithin x t
-- Mathlib.Analysis.Real.Sqrt
Real.map_sqrt_atTop : Filter.map (fun x => √x) Filter.atTop = Filter.atTop
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatters_of_forall_subset : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {s : Finset α}, (∀ t ⊆ s, t ∈ 𝒜) → 𝒜.Shatters s
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.superpose?.go : Lean.Grind.AC.Seq →
  Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Option (Lean.Grind.AC.Seq × Lean.Grind.AC.Seq × Lean.Grind.AC.Seq)
-- Mathlib.NumberTheory.PellMatiyasevic
/-- The property of being a solution to the Pell equation, expressed
as a property of elements of `ℤ√d`.  -/
Pell.IsPell : {d : ℤ} → ℤ√d → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_minKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.isEmpty = false → t.getKey! t.minKey! = t.minKey!
-- Mathlib.Algebra.Category.Ring.FinitePresentation
CommRingCat.isFinitelyPresentable_hom : ∀ {R S : CommRingCat} (f : R ⟶ S),
  (CommRingCat.Hom.hom f).FinitePresentation → CategoryTheory.MorphismProperty.isFinitelyPresentable CommRingCat f
-- Mathlib.CategoryTheory.Linear.Basic
/-- The linear equivalence `(X ⟶ Y) ≃+ (F X ⟶ F Y)` when `F : D → C` and
`C` is a `R`-linear category.  -/
CategoryTheory.InducedCategory.homLinearEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {R : Type w} →
        [inst_2 : Semiring R] →
          [inst_3 : CategoryTheory.Linear R C] →
            {D : Type u'} → {F : D → C} → {X Y : CategoryTheory.InducedCategory C F} → (X ⟶ Y) ≃ₗ[R] F X ⟶ F Y
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_insertMany_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)}, (m.insertMany l).size ≤ m.size + l.length
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.instMulActionQuotient : {S : Type u_2} →
  (M : Type u_3) → [inst : Monoid S] → [inst_1 : MulAction S M] → (c : SMulCon S M) → MulAction S (SMulCon.Quotient M c)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
/-- This is a technical result: quite often, we want to impose conditions at all infinite places
but one and choose the value at the remaining place so that we can apply
`exists_ne_zero_mem_ringOfIntegers_lt`.  -/
NumberField.mixedEmbedding.adjust_f : ∀ (K : Type u_1) [inst : Field K] {f : NumberField.InfinitePlace K → NNReal} [inst_1 : NumberField K]
  {w₁ : NumberField.InfinitePlace K} (B : NNReal),
  (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → f w ≠ 0) →
    ∃ g, (∀ (w : NumberField.InfinitePlace K), w ≠ w₁ → g w = f w) ∧ ∏ w, g w ^ w.mult = B
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_prod_le : ∀ {ι : Type u_3} {E : Type u_5} [inst : SeminormedCommGroup E] (s : Finset ι) (f : ι → E),
  ‖∏ a ∈ s, f a‖₊ ≤ ∑ a ∈ s, ‖f a‖₊
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  (S : J.MayerVietorisSquare), S.shortComplex.ShortExact
-- Mathlib.Topology.UnitInterval
unitInterval.le_one : ∀ (x : ↑unitInterval), ↑x ≤ 1
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleMatch : Type
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.mk 0 x = 0
-- Init.Data.Nat.Lemmas
Nat.le_iff_ne_zero_of_dvd : ∀ {a b : ℕ}, a ≠ 0 → a ∣ b → (a ≤ b ↔ b ≠ 0)
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.mk.sizeOf_spec : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] [inst_1 : SizeOf I]
  [inst_2 : (a : I) → SizeOf (C a)] {i : I} {X Y : C i} (a : X ⟶ Y),
  sizeOf (CategoryTheory.Sigma.SigmaHom.mk a) = 1 + sizeOf i + sizeOf X + sizeOf Y + sizeOf a
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.toConvexCone_map : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] [inst_5 : AddCommMonoid F] [inst_6 : Module R F]
  (C : PointedCone R E) (f : E →ₗ[R] F), ↑(PointedCone.map f C) = ConvexCone.map f ↑C
-- Mathlib.Analysis.Convex.Basic
Monotone.convex_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Monotone f → ∀ (r : β), Convex 𝕜 {x | f x ≤ r}
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (Topology.WithUpper α)
-- Mathlib.Algebra.Category.BoolRing
BoolRing.of.injEq : ∀ (carrier : Type u) [booleanRing : BooleanRing carrier] (carrier_1 : Type u) (booleanRing_1 : BooleanRing carrier_1),
  ({ carrier := carrier, booleanRing := booleanRing } = { carrier := carrier_1, booleanRing := booleanRing_1 }) =
    (carrier = carrier_1 ∧ booleanRing ≍ booleanRing_1)
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (a b : α) (xs : List α) (le : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match a :: b :: xs, le with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_3 a b xs le
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- The map between neighbor sets induced by a homomorphism.  -/
SimpleGraph.Hom.mapNeighborSet : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} → {G' : SimpleGraph W} → (f : G →g G') → (v : V) → ↑(G.neighborSet v) → ↑(G'.neighborSet (f v))
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
Mathlib.Tactic.ClickSuggestions.ApplyAtLemma.mk.injEq : ∀ (name name_1 : Mathlib.Tactic.ClickSuggestions.Premise), ({ name := name } = { name := name_1 }) = (name = name_1)
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.String.pushHex.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.smul_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M]
  [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst_6 : DistribSMul S M₂] [inst_7 : SMulCommClass R₂ S M₂] (a : S)
  (f : M →ₛₗ[σ₁₂] M₂) (x : M), (a • f) x = a • f x
-- Mathlib.RepresentationTheory.Irreducible
Representation.IsIrreducible.instIsSimpleModuleMonoidAlgebraAsModule : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Field k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] {ρ : Representation k G V} [ρ.IsIrreducible], IsSimpleModule (MonoidAlgebra k G) ρ.asModule
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_one : ∀ {X : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : One X], Metric.ediam 1 = 0
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalHorizontalComp_cons_nil : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {f f' g g' h i : C} {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i} {β : f' ≅ g'}
  {η₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj g g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj h g'}
  {ηs₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj h g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i g'}
  {η₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj g g' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i g'}
  {η₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj f f' ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj i g'},
  CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl g).hom
          (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Iso.refl h).hom))
        g' =
      η₁ →
    CategoryTheory.MonoidalCategoryStruct.whiskerRight ηs g' = ηs₁ →
      CategoryTheory.CategoryStruct.comp η₁ ηs₁ = η₂ →
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorIso α β).hom η₂ = η₃ →
          CategoryTheory.MonoidalCategoryStruct.tensorHom
              (CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp η ηs)) β.hom =
            η₃
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.liftRight.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x)),
  IsUnit.liftRight f hf = Units.liftRight f (fun x => ⋯.unit) ⋯
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.filter_roots_map_range_eq_map_roots : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : IsDomain B]
  {f : A →+* B} [inst_4 : DecidablePred fun x => x ∈ f.range],
  Function.Injective ⇑f →
    ∀ (p : Polynomial A), Multiset.filter (fun x => x ∈ f.range) (Polynomial.map f p).roots = Multiset.map (⇑f) p.roots
-- Lean.Language.Basic
Lean.Language.ProcessingContext.mk : Lean.Parser.InputContext → Lean.Language.ProcessingContext
-- Mathlib.Data.Finset.Card
Finset.card.eq_1 : ∀ {α : Type u_1} (s : Finset α), s.card = s.val.card
-- Mathlib.Order.Hom.Order
OrderHom.coe_sup : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : SemilatticeSup β] (f g : α →o β), ⇑(f ⊔ g) = ⇑f ⊔ ⇑g
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
AlgebraicGeometry.PresheafedSpace.colimit_presheaf : ∀ {J : Type u'} [inst : CategoryTheory.Category.{v', u'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat]
  [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)]
  (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)),
  (AlgebraicGeometry.PresheafedSpace.colimit F).presheaf =
    CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp
-- Init.Data.Vector.Lemmas
Vector.foldl.eq_1 : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} (f : β → α → β) (b : β) (xs : Vector α n),
  Vector.foldl f b xs = Array.foldl f b xs.toArray
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forIn_eq_forIn_toArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ},
  m.WF → Std.DHashMap.Raw.forIn f init m = forIn m.toArray init fun a b => f a.fst a.snd b
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.mul_inv_rev : ∀ {R : Type u} {M : Type v} [inst : DivisionSemiring R] [inst_1 : AddCommGroup M] [inst_2 : Module Rᵐᵒᵖ M]
  [inst_3 : Module R M] [SMulCommClass R Rᵐᵒᵖ M] (a b : TrivSqZeroExt R M), (a * b)⁻¹ = b⁻¹ * a⁻¹
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.prodMap : ∀ {α₁ : Type u_5} {α₂ : Type u_6} {β₁ : Type u_7} {β₂ : Type u_8} [inst : CommMonoid α₁] [inst_1 : CommMonoid α₂]
  [inst_2 : CommMonoid β₁] [inst_3 : CommMonoid β₂] {A₁ : Set α₁} {A₂ : Set α₂} {B₁ : Set β₁} {B₂ : Set β₂}
  {f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {n : ℕ},
  IsMulFreimanIso n A₁ B₁ f₁ → IsMulFreimanIso n A₂ B₂ f₂ → IsMulFreimanIso n (A₁ ×ˢ A₂) (B₁ ×ˢ B₂) (Prod.map f₁ f₂)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.withSeminorms_of_hasBasis : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [t : TopologicalSpace E] [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι),
  (nhds 0).HasBasis (fun s => s ∈ p.basisSets) id → WithSeminorms p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- the first projection  -/
CategoryTheory.Functor.PullbackObjObj.fst : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₃ Y₃ : C₃} →
                    {f₃ : X₃ ⟶ Y₃} → (self : G.PullbackObjObj f₁ f₃) → self.pt ⟶ (G.obj (Opposite.op X₁)).obj X₃
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_diff_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.diff m₂ ⋯).getKey? k = none
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.πs_apply_apply : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u})
  (g : LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ) (a : ↑C),
  ((Profinite.NobelingProof.πs C o) g) a =
    g (Profinite.NobelingProof.ProjRestrict C (fun x => Profinite.NobelingProof.ord I x < o) a)
-- Init.Data.String.Modify
/-- Replaces each character in `s` with the result of applying `Char.toLower` to it.

`Char.toLower` has no effect on characters outside of the range `'A'`–`'Z'`.

Examples:
* `"ORANGE".toLower = "orange"`
* `"Orange".toLower = "orange"`
* `"ABc123".toLower = "abc123"`
 -/
String.toLower : String → String
-- Mathlib.Topology.EMetricSpace.Basic
/-- A compact set in a pseudo emetric space is separable, i.e., it is a subset of the closure of a
countable set.  -/
EMetric.subset_countable_closure_of_compact : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, IsCompact s → ∃ t ⊆ s, t.Countable ∧ s ⊆ closure t
-- Init.Data.String.Decode
ByteArray.validateUTF8At_eq_isSome_utf8DecodeChar? : ∀ {b : ByteArray} {i : ℕ}, b.validateUTF8At i = (b.utf8DecodeChar? i).isSome
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'} (e : S' ≅ S)
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w :
    ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) e.hom)
  {β : ι → ι'} {q' : (i : ι) → X i ⟶ X' (β i)}
  (w' :
    ∀ (i : ι), CategoryTheory.CategoryStruct.comp (q' i) (f' (β i)) = CategoryTheory.CategoryStruct.comp (f i) e.inv),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctorEquivalence F e w w').functor =
    CategoryTheory.Pseudofunctor.DescentData.pullFunctor F w
-- Mathlib.Topology.Compactness.Compact
/-- The neighborhood filter of a compact set is disjoint with a filter `l` if and only if the
neighborhood filter of each point of this set is disjoint with `l`.  -/
IsCompact.disjoint_nhdsSet_left : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {l : Filter X},
  IsCompact s → (Disjoint (nhdsSet s) l ↔ ∀ x ∈ s, Disjoint (nhds x) l)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.forall_fin_succ_pi : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} {P : ((i : Fin (n + 1)) → α i) → Prop},
  (∀ (x : (i : Fin (n + 1)) → α i), P x) ↔ ∀ (a : α 0) (v : (i : Fin n) → α i.succ), P (Fin.cons a v)
-- Mathlib.Topology.Order.LocalExtr
IsLocalMin.sup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SemilatticeSup β] {f g : α → β} {a : α},
  IsLocalMin f a → IsLocalMin g a → IsLocalMin (fun x => f x ⊔ g x) a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {w len : ℕ} {x : aig.RefVec (len * w)}
  {h : 0 < len} {len_1 : ℕ} {x_1 : aig.RefVec (len_1 * w)} {h_1 : 0 < len_1},
  { len := len, x := x, h := h } = { len := len_1, x := x_1, h := h_1 } → len = len_1 ∧ x ≍ x_1
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.ofSubsingleton_σ' : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : Subsingleton S]
  (x : S), (Algebra.SubmersivePresentation.ofSubsingleton R S).σ' x = 1