mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι]
  {𝔸' : Type u_3} [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) →
    derivWithin (fun x => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x
-- Init.Internal.Order.Basic
/-- A function is monotone if it maps related elements to related elements.

This is intended to be used in the construction of `partial_fixpoint`, and not meant to be used otherwise.
 -/
Lean.Order.monotone : {α : Sort u} → [Lean.Order.PartialOrder α] → {β : Sort v} → [Lean.Order.PartialOrder β] → (α → β) → Prop
-- Mathlib.Topology.FiberBundle.Trivialization
OpenPartialHomeomorph.piecewise.congr_simp : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e e_1 : OpenPartialHomeomorph X Y) (e_e : e = e_1) (e' e'_1 : OpenPartialHomeomorph X Y) (e_e' : e' = e'_1)
  (s s_1 : Set X) (e_s : s = s_1) (t t_1 : Set Y) (e_t : t = t_1) {inst_2 : (x : X) → Decidable (x ∈ s)}
  [inst_3 : (x : X) → Decidable (x ∈ s_1)] {inst_4 : (y : Y) → Decidable (y ∈ t)}
  [inst_5 : (y : Y) → Decidable (y ∈ t_1)] (H : e.IsImage s t) (H' : e'.IsImage s t)
  (Hs : e.source ∩ frontier s = e'.source ∩ frontier s) (Heq : Set.EqOn (↑e) (↑e') (e.source ∩ frontier s)),
  e.piecewise e' s t H H' Hs Heq = e_1.piecewise e'_1 s_1 t_1 ⋯ ⋯ ⋯ ⋯
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.mkOfAdjoinEqTop'.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Module.Finite R S] [inst_4 : Module.Free R S] {α : S} (hα : R[α] = ⊤),
  IsAdjoinRootMonic.mkOfAdjoinEqTop' hα = IsAdjoinRootMonic.mkOfAdjoinEqTop' hα
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms,
this is the morphism `kernel (f ≫ g) ⟶ X ⊞ Y` which
"sends `x` to `(x, f(x))`".  -/
CategoryTheory.kernelCokernelCompSequence.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y Z : C} →
        (f : X ⟶ Y) → (g : Y ⟶ Z) → CategoryTheory.Limits.kernel (CategoryTheory.CategoryStruct.comp f g) ⟶ X ⊞ Y
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.leftUnitor_hom_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (η : F ⟶ G) (a : B),
  (CategoryTheory.Lax.LaxTrans.leftUnitor η).hom.as.app a = (CategoryTheory.Bicategory.leftUnitor (η.app a)).hom
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.RelevantArg.arg.sizeOf_spec : ∀ (n : ℕ), sizeOf (Mathlib.Tactic.Translate.RelevantArg.arg n) = 1 + sizeOf n
-- Lean.Parser.Types
Lean.Parser.ParserCache.parserCache : Lean.Parser.ParserCache → Std.HashMap Lean.Parser.ParserCacheKey Lean.Parser.ParserCacheEntry
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- The product over a sum can be written as a sum over the product of sets, `Finset.Pi`.
`Finset.prod_univ_sum` is an alternative statement when the product is over `univ`.  -/
Finset.prod_sum : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : DecidableEq ι] {κ : ι → Type u_5} (s : Finset ι)
  (t : (i : ι) → Finset (κ i)) (f : (i : ι) → κ i → R),
  ∏ a ∈ s, ∑ b ∈ t a, f a b = ∑ p ∈ s.pi t, ∏ x ∈ s.attach, f (↑x) (p ↑x ⋯)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whisker_assoc_symm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h)
        (CategoryTheory.Bicategory.associator f g' h).hom)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.isIso_iff_of_epi : ∀ {n m : SimplexCategory} (f : n ⟶ m) [hf : CategoryTheory.Epi f], CategoryTheory.IsIso f ↔ n.len = m.len
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version at a point.  -/
ContMDiffAt.mpullback_vectorField_preimage : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'],
  ContMDiffAt I' I'.tangent m (fun x => ⟨x, V x⟩) (f x₀) →
    ContMDiffAt I I' n f x₀ →
      (mfderiv% f x₀).IsInvertible →
        m + 1 ≤ n → ContMDiffAt I I.tangent m (fun x => ⟨x, VectorField.mpullback I I' f V x⟩) x₀
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_eq_headD_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.minKeyD fallback = t.keys.headD fallback
-- Mathlib.Data.Quot
Equivalence.quot_mk_eq_iff : ∀ {α : Type u_3} {r : α → α → Prop}, Equivalence r → ∀ (x y : α), Quot.mk r x = Quot.mk r y ↔ r x y
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- Every split mono `f` with a cokernel induces a binary bicone with `f` as its `inl` and
the cokernel map as its `snd`.
We will show in `isBilimitBinaryBiconeOfIsSplitMonoOfCokernel` that this binary bicone is in
fact already a biproduct.  -/
CategoryTheory.Limits.binaryBiconeOfIsSplitMonoOfCokernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          [CategoryTheory.IsSplitMono f] →
            {c : CategoryTheory.Limits.CokernelCofork f} →
              CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.BinaryBicone X c.pt
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableLocallyUniformlyOn.hasSumLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  SummableLocallyUniformlyOn f s → HasSumLocallyUniformlyOn f (fun x => ∑' (i : ι), f i x) s
-- Init.Data.BitVec.Bitblast
BitVec.getElem_srem : ∀ {w i : ℕ} {x y : BitVec w} (h : i < w),
  (x.srem y)[i] =
    match x.msb, y.msb with
    | false, false => (x % y)[i]
    | false, true => (x % -y)[i]
    | true, false => (-(-x % y))[i]
    | true, true => (-(-x % -y))[i]
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The qExpansion map as an additive group hom. to power series over `ℂ`.  -/
ModularForm.qExpansionAddHom : {Γ : Subgroup (GL (Fin 2) ℝ)} → {h : ℝ} → 0 < h → h ∈ Γ.strictPeriods → (k : ℤ) → ModularForm Γ k →+ PowerSeries ℂ
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.eval_map : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (R' : Type u_6)
  {M' : Type u_7} [inst_3 : CommRing R'] [inst_4 : AddCommGroup M'] [inst_5 : Module R' M'] [inst_6 : Module R M']
  [inst_7 : Algebra R R'] [IsScalarTower R R' M'] (f : M →ₗ[R] M') (q : PolynomialModule R M) (r : R),
  (PolynomialModule.eval ((algebraMap R R') r)) ((PolynomialModule.map R' f) q) = f ((PolynomialModule.eval r) q)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_iUnion_nonneg : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Countable β] {f : β → Set α} {M : Type u_4}
  [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [inst_2 : PartialOrder M] [IsOrderedAddMonoid M]
  [OrderClosedTopology M] {v : MeasureTheory.VectorMeasure α M},
  (∀ (i : β), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → (∀ (i : β), 0 ≤ v (f i)) → 0 ≤ v (⋃ i, f i)
-- Mathlib.MeasureTheory.Group.Arithmetic
Submonoid.instMeasurableConstSMul : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : Monoid M] [inst_2 : MulAction M α]
  [MeasurableConstSMul M α] (s : Submonoid M), MeasurableConstSMul (↥s) α
-- Mathlib.LinearAlgebra.LinearPMap
/-- The graph of `z • f` as a pushforward.  -/
LinearPMap.smul_graph : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] {M : Type u_7} [inst_4 : Monoid M] [inst_5 : DistribMulAction M F] [inst_6 : Module R F]
  [inst_7 : SMulCommClass R M F] (f : E →ₗ.[R] F) (z : M),
  (z • f).graph = Submodule.map (LinearMap.id.prodMap (z • LinearMap.id)) f.graph
-- Mathlib.Order.Rel.GaloisConnection
/-- `rightDual` maps any set `I` of elements of type `β` to the set `{a : α | ∀ b ∈ I, a ~[R] b}`
of elements `a` of type `α` such that `a ~[R] b` for every element `b` of `I`.  -/
SetRel.rightDual : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set β → Set α
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_ne_zero_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.leadingCoeff f ≠ 0 ↔ f ≠ 0
-- Mathlib.Order.Filter.AtTopBot.BigOperators
/-- **Alias** of `Filter.map_atTop_finsetSum_le_of_sum_eq`.

---

Let `f` and `g` be two maps to the same commutative additive monoid. This lemma
gives a sufficient condition for comparison of the filter `atTop.map (fun s ↦ ∑ b ∈ s, f b)` with
`atTop.map (fun s ↦ ∑ b ∈ s, g b)`. This is useful to compare the set of limit points of
`∑ b ∈ s, f b` as `s → atTop` with the similar set for `g`.  -/
Filter.map_atTop_finset_sum_le_of_sum_eq : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] {f : α → M} {g : β → M},
  (∀ (u : Finset β), ∃ v, ∀ (v' : Finset α), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∑ x ∈ u', g x = ∑ b ∈ v', f b) →
    Filter.map (fun s => ∑ b ∈ s, f b) Filter.atTop ≤ Filter.map (fun s => ∑ x ∈ s, g x) Filter.atTop
-- Mathlib.Order.Basic
/-- Transfer a `LinearOrder` on `β` to a `LinearOrder` on `α` using an injective
function `f : α → β`. This version autogenerates `min` and `max` fields. See `LinearOrder.lift`
for a version that takes `[Max α]` and `[Min α]`, then uses them as `max` and `min`. See
`LinearOrder.liftWithOrd'` for a version which does not auto-generate `compare` fields.
See note [reducible non-instances].  -/
LinearOrder.lift' : {α : Type u_2} → {β : Type u_3} → [LinearOrder β] → (f : α → β) → Function.Injective f → LinearOrder α
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `*` is a commutative magma, if it admits a surjective map that preserves
`*` from a commutative magma.  -/
Function.Injective.commMagma : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : CommMagma M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → CommMagma M₁
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
/-- The **Cayley-Hamilton Theorem** for f.g. modules over arbitrary rings states that for each
`R`-endomorphism `φ` of an `R`-module `M` generated by `n` elements such that `φ(M) ≤ I • M`
for some ideal `I`, there exist some `aᵢ ∈ Iⁱ` such that `φⁿ + a₁ φⁿ⁻¹ + ⋯ + aₙ = 0`.

This is the version in [Matsumura 2.1][matsumura1987], which is stronger than those in
[Eisenbud 4.3][Eisenbud1995] and [Atiyah-Macdonald 2.4][atiyah-macdonald].
 -/
LinearMap.exists_monic_and_natDegree_eq_and_coeff_mem_pow_and_aeval_eq_zero : ∀ {M : Type u_2} [inst : AddCommGroup M] (R : Type u_3) [inst_1 : CommRing R] [inst_2 : Module R M] [Module.Finite R M]
  (f : Module.End R M) (I : Ideal R),
  LinearMap.range f ≤ I • ⊤ →
    ∃ p,
      p.Monic ∧
        p.natDegree = ⊤.spanFinrank ∧ (∀ (k : ℕ), p.coeff k ∈ I ^ (p.natDegree - k)) ∧ (Polynomial.aeval f) p = 0
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- The saturation of an additive submonoid `s` is the intersection of all saturated submonoids
that contain `s`.

If `M` is a commutative additive monoid, then this is `{x : M | ∃ y : M, x + y ∈ s}`.  -/
AddSubmonoid.saturation : {M : Type u_1} → [inst : AddZeroClass M] → AddSubmonoid M → SaturatedAddSubmonoid M
-- Init.Data.List.Monadic
List.allM_pure : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → Bool} {as : List α},
  List.allM (fun x => pure (p x)) as = pure (as.all p)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet_iff_iIndepSets_singleton : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ι → Set Ω},
  (∀ (i : ι), MeasurableSet (f i)) → (ProbabilityTheory.iIndepSet f μ ↔ ProbabilityTheory.iIndepSets (fun i => {f i}) μ)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.uniformContinuous_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β], UniformContinuous fun x => x.1 ×ˢ x.2
-- Mathlib.Probability.Distributions.Geometric
ProbabilityTheory.stronglyMeasurable_geometricPMFReal : ∀ {p : ℝ}, MeasureTheory.StronglyMeasurable (ProbabilityTheory.geometricPMFReal p)
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.unit_smul_eq_smul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A) (r : Rˣ),
  spectrum R (r • a) = r • spectrum R a
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : (a : α) → β a → Bool}
  (h : t.WF), (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.toArray = Array.filter (fun p => f p.fst p.snd) t.toArray
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.coeff_sPolynomial_sup_eq_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
  MvPolynomial.coeff (m.degree f ⊔ m.degree g) (m.sPolynomial f g) = 0
-- Batteries.Data.Array.Match
/-- Inner loop for `mkPrefixTableOfStream`  -/
Array.mkPrefixTableOfStream.loop : {α : Type u_1} → {σ : Type u_2} → [BEq α] → [Std.Stream σ α] → Array.PrefixTable α → σ → Array.PrefixTable α
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Up to pre-composing with an equivalence of categories, `Pi.functor` is isomorphic to `lim`.  -/
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim : (α : Type w₂) →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] →
        (CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.comp CategoryTheory.Limits.lim ≅
          CategoryTheory.Limits.Pi.functor α
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- Sometimes, one may want to construct a charted space structure on a space which does not yet
have a topological structure, where the topology would come from the charts. For this, one needs
charts that are only partial equivalences, and continuity properties for their composition.
This is formalised in `ChartedSpaceCore`.  -/
ChartedSpaceCore : (H : Type u_5) → [TopologicalSpace H] → Type u_6 → Type (max u_5 u_6)
-- Mathlib.CategoryTheory.Subobject.Limits
/-- The morphism `imageSubobject (h ≫ f) ⟶ imageSubobject f`
is an epimorphism when `h` is an epimorphism.
In general this does not imply that `imageSubobject (h ≫ f) = imageSubobject f`,
although it will when the ambient category is abelian.
 -/
CategoryTheory.Limits.imageSubobject_comp_le_epi_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.HasEqualizers C] {X' : C}
  (h : X' ⟶ X) [CategoryTheory.Epi h] (f : X ⟶ Y) [inst_3 : CategoryTheory.Limits.HasImage f]
  [inst_4 : CategoryTheory.Limits.HasImage (CategoryTheory.CategoryStruct.comp h f)],
  CategoryTheory.Epi
    ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE
      (CategoryTheory.Limits.imageSubobject f) ⋯)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.associator.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) (g : b ⟶ c)
  (h : c ⟶ d),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.associator f g h) =
    1 + sizeOf a + sizeOf b + sizeOf c + sizeOf d + sizeOf f + sizeOf g + sizeOf h
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.bddAbove_of_small : ∀ {s : Set Cardinal.{u}} [h : Small.{u, u + 1} ↑s], BddAbove s
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_subset_Ioc_right : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b : α}, a₂ ≤ a₁ → Set.Ioc b a₂ ⊆ Set.Ioc b a₁
-- Mathlib.Order.Category.FinPartOrd
/-- Typecheck a `OrderHom` as a morphism in `FinPartOrd`.  -/
FinPartOrd.ofHom : {X Y : Type u} →
  [inst : PartialOrder X] →
    [inst_1 : Fintype X] →
      [inst_2 : PartialOrder Y] → [inst_3 : Fintype Y] → (X →o Y) → (FinPartOrd.of X ⟶ FinPartOrd.of Y)
-- Mathlib.Data.Finset.Image
Finset.subtype_mem_eq_attach : ∀ {α : Type u_1} (s : Finset α) [inst : DecidablePred fun x => x ∈ s], Finset.subtype (fun x => x ∈ s) s = s.attach
-- Init.Data.Order.Lemmas
Std.trichotomous_of_rel_or_eq_or_rel_swap : ∀ {α : Sort u_1} {r : α → α → Prop}, (∀ {a b : α}, r a b ∨ a = b ∨ r b a) → Std.Trichotomous r
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.bilinearComp_zero_right : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  {E' : Type u_11} {F' : Type u_12} [inst_9 : SeminormedAddCommGroup E'] [inst_10 : SeminormedAddCommGroup F']
  {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [inst_11 : NontriviallyNormedField 𝕜₁'] [inst_12 : NontriviallyNormedField 𝕜₂']
  [inst_13 : NormedSpace 𝕜₁' E'] [inst_14 : NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}
  {σ₂₃' : 𝕜₂' →+* 𝕜₃} [inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃']
  [inst_17 : RingHomIsometric σ₂₃] [inst_18 : RingHomIsometric σ₁₃'] [inst_19 : RingHomIsometric σ₂₃']
  {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gE : E' →SL[σ₁'] E}, f.bilinearComp gE 0 = 0
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_single_zero : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (a : α) (c : γ),
  (fun₀ | a => c).sumElim 0 = fun₀ | Sum.inl a => c
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_iConvexComb : ∀ {R : Type u_1} {I : Type u_6} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  (w : Convexity.StdSimplex R I) (f : I → Convexity.StdSimplex R I),
  (Convexity.iConvexComb w f).weights = w.weights.sum fun i r => r • (f i).weights
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.instNonempty : ∀ {α : Type u} [inst : TopologicalSpace α] [Nonempty α], Nonempty (ConnectedComponents α)
-- Lean.Meta.CollectMVars
Lean.Meta.getMVarsAtDecl : Lean.Declaration → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.Tactic.FunProp.Theorems
/-- Extensions for transition or morphism theorems  -/
Mathlib.Meta.FunProp.GeneralTheoremsExt : Type
-- Mathlib.RingTheory.Algebraic.Integral
/-- Transitivity of algebraicity for algebras over domains.  -/
Algebra.IsAlgebraic.trans : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [Algebra.IsAlgebraic R S] [alg : Algebra.IsAlgebraic S A], Algebra.IsAlgebraic R A
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryLT!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited ((a : α) × β a)],
          Std.DTreeMap.Internal.Impl.getEntryLT! k t₁ = Std.DTreeMap.Internal.Impl.getEntryLT! k t₂
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.NatTrans.rightDerived_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] (n : ℕ),
  CategoryTheory.NatTrans.rightDerived (CategoryTheory.CategoryStruct.id F) n =
    CategoryTheory.CategoryStruct.id (F.rightDerived n)
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.liftIsometry_tprodL : ∀ {ι : 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)],
  (PiTensorProduct.liftIsometry 𝕜 E (PiTensorProduct 𝕜 fun i => E i)) (PiTensorProduct.tprodL 𝕜) =
    ContinuousLinearMap.id 𝕜 (PiTensorProduct 𝕜 fun i => E i)
-- Mathlib.CategoryTheory.RepresentedBy
CategoryTheory.Functor.IsRepresentedBy.map_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {x : F.obj (Opposite.op X)},
  F.IsRepresentedBy x → ∀ {Y : C}, Function.Bijective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f.op)) x
-- Mathlib.Topology.Order.LeftRightNhds
nhdsGT_basis_Ioc_of_exists_gt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a : α},
  (∃ b, a < b) → (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioc a)
-- Std.Data.ExtDTreeMap.Lemmas
/-- Simpler variant of `get?_filterMap` when `LawfulEqCmp` is available.  -/
Std.ExtDTreeMap.Const.get?_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.filterMap f t) k = (Std.ExtDTreeMap.Const.get? t k).bind fun x => f k x
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.upFunctor_obj_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (down : C),
  (CategoryTheory.ULift.upFunctor.obj down).down = down
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- Avoid using this. Use the isomorphism `AlgebraicGeometry.Scheme.Modules.restrictAppIso`
instead.  -/
AlgebraicGeometry.Scheme.Modules.restrict_obj : ∀ {X Y : AlgebraicGeometry.Scheme} (M : Y.Modules) (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↥X),
  (M.restrict f).presheaf.obj (Opposite.op U) =
    M.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))
-- Mathlib.Topology.MetricSpace.Gluing
Metric.inhabitedLeft : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : Nonempty Z] →
        [inst_1 : MetricSpace Z] →
          [inst_2 : MetricSpace X] →
            [inst_3 : MetricSpace Y] →
              {Φ : Z → X} →
                {Ψ : Z → Y} → (hΦ : Isometry Φ) → (hΨ : Isometry Ψ) → [Inhabited X] → Inhabited (Metric.GlueSpace hΦ hΨ)
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- The empty component of a sheaf is terminal.  -/
TopCat.Sheaf.isTerminalOfEmpty : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : TopCat} → (F : TopCat.Sheaf C X) → CategoryTheory.Limits.IsTerminal (F.obj.obj (Opposite.op ⊥))