mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
mem_selfAdjointMatricesSubmodule : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J A₁ : Matrix n n R)
  [inst_2 : DecidableEq n], A₁ ∈ selfAdjointMatricesSubmodule J ↔ J.IsSelfAdjoint A₁
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
/-- the natural transformation between the underlying functors  -/
CategoryTheory.LaxMonoidalFunctor.Hom.hom : {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 G : CategoryTheory.LaxMonoidalFunctor C D} → F.Hom G → (F.toFunctor ⟶ G.toFunctor)
-- Mathlib.RingTheory.Invariant.Basic
/-- This theorem will be made redundant by `IsFractionRing.stabilizerHom_surjective`.  -/
_private.Mathlib.RingTheory.Invariant.Basic.0.fixed_of_fixed1 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (G : Type u_3)
  [inst_3 : Group G] [Finite G] [inst_5 : MulSemiringAction G B] [inst_6 : SMulCommClass G A B] (P : Ideal A)
  (Q : Ideal B) [Q.IsPrime] [inst_8 : Q.LiesOver P] (K : Type u_4) (L : Type u_5) [inst_9 : Field K] [inst_10 : Field L]
  [inst_11 : Algebra (A ⧸ P) K] [inst_12 : Algebra (B ⧸ Q) L] [inst_13 : Algebra (A ⧸ P) L]
  [IsScalarTower (A ⧸ P) (B ⧸ Q) L] [inst_15 : Algebra K L] [IsScalarTower (A ⧸ P) K L] [Algebra.IsInvariant A B G]
  [Module.IsTorsionFree (B ⧸ Q) L] (f : Gal(L/K)) (b : B ⧸ Q),
  (∀ (g : ↥(MulAction.stabilizer G Q)), ((Ideal.Quotient.stabilizerHom Q P G) g) b = b) →
    f ((algebraMap (B ⧸ Q) L) b) = (algebraMap (B ⧸ Q) L) b
-- Mathlib.Data.Matrix.Composition
/-- `Matrix.comp` as `AlgEquiv`  -/
Matrix.compAlgEquiv : (I : Type u_1) →
  (J : Type u_2) →
    (R : Type u_5) →
      (K : Type u_7) →
        [inst : CommSemiring K] →
          [inst_1 : Semiring R] →
            [inst_2 : Fintype I] →
              [inst_3 : Fintype J] →
                [inst_4 : Algebra K R] →
                  [inst_5 : DecidableEq I] →
                    [inst_6 : DecidableEq J] → Matrix I I (Matrix J J R) ≃ₐ[K] Matrix (I × J) (I × J) R
-- Init.Data.Vector.Lex
Vector.lt_of_le_of_lt : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] [Std.IsLinearOrder α]
  {xs ys zs : Vector α n}, xs ≤ ys → ys < zs → xs < zs
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homology₀ε.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C],
  X.homology₀ε R =
    CategoryTheory.CategoryStruct.comp (X.homology₀Iso R).hom
      (CategoryTheory.Limits.Sigma.desc fun x => CategoryTheory.CategoryStruct.id R)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.map_neg : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {S : Type u_1} [inst_1 : Ring S] (f : R →+* S),
  Polynomial.map f (-p) = -Polynomial.map f p
-- Init.Data.Int.Order
Int.nonpos_of_mul_nonpos_right : ∀ {a b : ℤ}, a * b ≤ 0 → 0 < a → b ≤ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_alter_eq_self_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  k ∈ t → (f (t.get? k)).isSome = true → (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.size = t.size
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.uliftFunctorForgetIso_hom_app_hom_apply : ∀ (R : Type u) [inst : Ring R] (X : ModuleCat R)
  (a : ((ModuleCat.uliftFunctor.{v', u_1, u} R).comp (CategoryTheory.forget (ModuleCat R))).obj X),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.uliftFunctorForgetIso R).hom.app X)) a = a
-- Mathlib.Algebra.Ring.GeomSum
/-- $x^n-y^n = (x-y) \sum x^ky^{n-1-k}$ reformulated without `-` signs.  -/
geom_sum₂_mul_add : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (n : ℕ),
  (∑ i ∈ Finset.range n, (x + y) ^ i * y ^ (n - 1 - i)) * x + y ^ n = (x + y) ^ n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_some_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α} {fallback : β}, a ∈ t → Std.ExtDTreeMap.Const.get? t a = some (Std.ExtDTreeMap.Const.getD t a fallback)
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (toLinearPreorderOfOrdArgs : Std.Packages.LinearPreorderOfOrdArgs α)
  (eq_of_compare :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      ∀ (a b : α), compare a b = Ordering.eq → a = b)
      Std.Packages.LinearOrderOfOrdArgs.eq_of_compare._autoParam)
  (min :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      Min α)
      Std.Packages.LinearOrderOfOrdArgs.min._autoParam)
  (max :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      Max α)
      Std.Packages.LinearOrderOfOrdArgs.max._autoParam)
  (min_eq :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      let this_2 := min;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊓ b = if (compare a b).isLE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.min_eq._autoParam)
  (max_eq :
    autoParam
      (let this := toLinearPreorderOfOrdArgs.ord;
      let this_1 := toLinearPreorderOfOrdArgs.le;
      let this_2 := max;
      have this_3 := ⋯;
      ∀ (a b : α), a ⊔ b = if (compare a b).isGE = true then a else b)
      Std.Packages.LinearOrderOfOrdArgs.max_eq._autoParam),
  sizeOf
      { toLinearPreorderOfOrdArgs := toLinearPreorderOfOrdArgs, eq_of_compare := eq_of_compare, min := min, max := max,
        min_eq := min_eq, max_eq := max_eq } =
    1 + sizeOf toLinearPreorderOfOrdArgs + sizeOf min + sizeOf max
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_eq_indicator : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M} {a : α} {t : Set β} {g : β → M}
  {b : β}, (a ∈ s ↔ b ∈ t) → f a = g b → s.indicator f a = t.indicator g b
-- Mathlib.Order.Atoms
instIsStronglyCoatomicElemOfOrdConnected : ∀ {α : Type u_4} [inst : Preorder α] [IsStronglyCoatomic α] {s : Set α} [h : s.OrdConnected], IsStronglyCoatomic ↑s
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Empty
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Empty.0.Std.IterM.forIn'_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.yield c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_1 c
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- The canonical isomorphism `(A_f)₀ ≅ Γ(Proj A, D₊(f))`
when `f` is homogeneous of positive degree.  -/
AlgebraicGeometry.Proj.basicOpenIsoAway : {σ : Type u_1} →
  {A : Type u} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                {m : ℕ} →
                  f ∈ 𝒜 m →
                    0 < m →
                      (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f) ≅
                        (AlgebraicGeometry.Proj 𝒜).presheaf.obj (Opposite.op (AlgebraicGeometry.Proj.basicOpen 𝒜 f)))
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Poly.mulMon_denote : ∀ (ctx : Nat.Internal.Linear.Context) (p : Nat.Internal.SOM.Poly) (k : ℕ) (m : Nat.Internal.SOM.Mon),
  Nat.Internal.SOM.Poly.denote ctx (p.mulMon k m) =
    Nat.Internal.SOM.Poly.denote ctx p * k * Nat.Internal.SOM.Mon.denote ctx m
-- Mathlib.Combinatorics.Graph.Basic
/-- The unary incidence predicate of `G`. `G.Inc e x` means that the vertex `x`
is one or both of the ends of the edge `e`.
In the `Inc` namespace, we use `edge` and `vertex` to refer to `e` and `x`.  -/
Graph.Inc : {α : Type u_1} → {β : Type u_2} → Graph α β → β → α → Prop
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sub : ∀ {n : ℕ} (x y : BitVec n), (x - y).toNat = (2 ^ n - y.toNat + x.toNat) % 2 ^ n
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.inv_one_sub_inv : ∀ {a : ENNReal}, a ≤ 1 → a⁻¹.HolderConjugate (1 - a)⁻¹
-- Init.Data.SInt.Lemmas
Int64.toFin_toBitVec : ∀ (x : Int64), x.toBitVec.toFin = x.toUInt64.toFin
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_inv_naturality_left_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f' g) h ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g h).inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h) h_1)
-- Mathlib.Algebra.Group.Finsupp
/-- If `M` is the trivial monoid, then the monoid of finitely supported functions `ι →₀ M` is
is isomorphic to `M`.  -/
Finsupp.uniqueAddEquiv : {ι : Type u_1} → {M : Type u_3} → [inst : AddZeroClass M] → ι → [Subsingleton ι] → (ι →₀ M) ≃+ M
-- Lean.LibrarySuggestions.Basic
/-- A premise whose `type.getForallBody.getAppFn` is a constant that has one of these prefixes is not retrieved.

Use `run_cmd modifyEnv fun env => typePrefixDenyListExt.addEntry env typePrefix` to add a type prefix to the deny list.
 -/
Lean.LibrarySuggestions.typePrefixDenyListExt : Lean.SimplePersistentEnvExtension Lean.Name (List Lean.Name)
-- Lean.Elab.DefView
/-- State before elaboration of a mutual definition.  -/
Lean.Elab.DefParsed : Type
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.toCategory : {obj : Type u} → [self : CategoryTheory.Groupoid obj] → CategoryTheory.Category.{v, u} obj
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.instPreservesLimitsOfShapeForgetOfHasLimitsOfShape : ∀ {J : Type w} [inst : CategoryTheory.Category.{v_1, w} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.Mon.forget C)
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionMain.succNthDefiningPoly.congr_simp : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ)
  (a₁ a₁_1 : WittVector p k),
  a₁ = a₁_1 →
    ∀ (a₂ a₂_1 : WittVector p k),
      a₂ = a₂_1 →
        ∀ (bs bs_1 : Fin (n + 1) → k),
          bs = bs_1 →
            WittVector.RecursionMain.succNthDefiningPoly p n a₁ a₂ bs =
              WittVector.RecursionMain.succNthDefiningPoly p n a₁_1 a₂_1 bs_1
-- Mathlib.CategoryTheory.Triangulated.WeakKernels
/-- If `T` is a distinguished triangle, then `T.mor₁` defines a kernel fork for `T.mor₂`.  -/
CategoryTheory.Pretriangulated.kernelForkOfDistTriangle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (T : CategoryTheory.Pretriangulated.Triangle C) →
                T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → CategoryTheory.Limits.KernelFork T.mor₂
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_add : ∀ (a b : UInt16), (a + b).toUInt32 = (a.toUInt32 + b.toUInt32) % 65536
-- Mathlib.Tactic.Linarith.Frontend
_private.Mathlib.Tactic.Linarith.Frontend.0.Mathlib.Tactic.instEvalExprLinarithConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.Linarith.LinarithConfig
-- Lean.Meta.Tactic.Apply
/-- Custom `isDefEq` for the `apply` tactic  -/
_private.Lean.Meta.Tactic.Apply.0.Lean.Meta.isDefEqApply : Bool → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Group.Conj
addConj_add : ∀ {α : Type u} [inst : AddGroup α] {a b c : α}, b + a + -b + (b + c + -b) = b + (a + c) + -b
-- Lean.Meta.Basic
Lean.Meta.map2MetaM : {m : Type → Type u_1} →
  {β : Sort u_2} →
    {γ : Sort u_3} →
      [MonadControlT Lean.MetaM m] →
        [Monad m] → ({α : Type} → (β → γ → Lean.MetaM α) → Lean.MetaM α) → {α : Type} → (β → γ → m α) → m α
-- Mathlib.Algebra.Module.NatInt
instSMulWithZeroNat : {M : Type u_3} → [inst : AddMonoid M] → SMulWithZero ℕ M
-- Lean.CoreM
Lean.Core.InstantiateLevelCache : Type
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_eq_getD_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {fallback : α},
  t.minD fallback = t.toArray.getD 0 fallback
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- If `φ : S₁ ⟶ S₂` is a morphism of short complexes such that `φ.τ₁` is epi, `φ.τ₂` is an iso
and `φ.τ₃` is mono, then a homology data for `S₁` induces a homology data for `S₂`.
The inverse construction is `ofEpiOfIsIsoOfMono'`.  -/
CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          S₁.HomologyData →
            [CategoryTheory.Epi φ.τ₁] → [CategoryTheory.IsIso φ.τ₂] → [CategoryTheory.Mono φ.τ₃] → S₂.HomologyData
-- Mathlib.Data.List.Perm.Basic
List.rel_perm : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop},
  Relator.BiUnique r →
    Relator.LiftFun (List.Forall₂ r) (Relator.LiftFun (List.Forall₂ r) fun x1 x2 => x1 ↔ x2) List.Perm List.Perm
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldlM.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type u_1} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (init : δ), Std.DTreeMap.Internal.Impl.foldlM f init Std.DTreeMap.Internal.Impl.leaf = pure init
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasDerivAt.tendsto_nhdsNE : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x → f' ≠ 0 → Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhdsWithin (f x) {f x}ᶜ)
-- Mathlib.Topology.Homotopy.TopCat.Path
/-- The bijection between `TopCat.Path X x y` and `_root_.Path x y`.  -/
TopCat.pathEquiv : {X : TopCat} → {x y : ↑X} → X.Path x y ≃ Path x y
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_max : ∀ (x y : ℝ), ↑(max x y) = max ↑x ↑y
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.algebraMap_apply : ∀ {ι : 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 𝒜] {x : Submonoid A} (y : HomogeneousLocalization 𝒜 x),
  (algebraMap (HomogeneousLocalization 𝒜 x) (Localization x)) y = y.val
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Homotopy group of finite index, denoted as `π_n` within the Topology namespace.  -/
HomotopyGroup.Pi : ℕ → (X : Type u_3) → [TopologicalSpace X] → X → Type u_3
-- Init.Data.SInt.Bitwise
Int32.toUInt32_xor : ∀ (a b : Int32), (a ^^^ b).toUInt32 = a.toUInt32 ^^^ b.toUInt32
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.self_comp_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β), ⇑e ∘ ⇑e.symm = id
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_eq_of_row_eq : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] {A : Matrix n n R}
  {p q : n}, p ≠ q → A.row p = A.row q → ∀ (s : optParam ℤˣ 1) (t : optParam ℤˣ (-1)), Matrix.detp s A = Matrix.detp t A
-- Init.PropLemmas
nonempty_prop : ∀ {p : Prop}, Nonempty p ↔ p
-- Std.Time.Time.Unit.Minute
/-- `Ordinal` represents a bounded value for minutes, ranging from 0 to 59. This is useful for representing the minute component of a time.
 -/
Std.Time.Minute.Ordinal : Type
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst.inj : ∀ {x : Lean.Grind.Linarith.Var} {c₁ c₂ : Lean.Meta.Grind.Arith.Linear.EqCnstr} {x_1 : Lean.Grind.Linarith.Var}
  {c₁_1 c₂_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr},
  Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Linear.EqCnstrProof.subst x_1 c₁_1 c₂_1 →
    x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Data.Set.Operations
/-- The image of a binary function `f : α → β → γ` as a function `Set α → Set β → Set γ`.
Mathematically this should be thought of as the image of the corresponding function `α × β → γ`.  -/
Set.image2 : {α : Type u} → {β : Type v} → {γ : Type w} → (α → β → γ) → Set α → Set β → Set γ
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.NoetherianSpace.range : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [TopologicalSpace.NoetherianSpace α] (f : α → β), Continuous f → TopologicalSpace.NoetherianSpace ↑(Set.range f)
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.toSurjectiveOnStalks : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsPreimmersion f],
  AlgebraicGeometry.SurjectiveOnStalks f
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Indep.cardinalMk_le_isBasis' : ∀ {α : Type u} {M : Matroid α} {I J X : Set α} [M.InvariantCardinalRank],
  M.Indep I → M.IsBasis' J X → I ⊆ X → Cardinal.mk ↑I ≤ Cardinal.mk ↑J
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.withPreservedCache : {α : Type} → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.linMulLin_compRight : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : M →ₗ[R] R} (r : M →ₗ[R] M),
  (LinearMap.BilinForm.linMulLin f g).compRight r = LinearMap.BilinForm.linMulLin f (g ∘ₗ r)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Request.method : {α : Type u} → Lean.JsonRpc.Request α → String
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α], (↑m).WF → (Std.DHashMap.Raw.Const.toArray ↑m).isEmpty = (↑m).isEmpty
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.foldr_eq_foldr_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {α_1 : Type u_2} {f : α → α_1 → α_1} {init : α_1} {t : RBTree.RBSet α cmp},
  RBTree.RBSet.foldr f init t = List.foldr f init t.toList
-- Mathlib.LinearAlgebra.Multilinear.Pi
MultilinearMap.pi_ext_iff : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [inst : Semiring R]
  [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_2 : AddCommMonoid N]
  [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_4 : Module R N] [Finite ι] [∀ (i : ι), Finite (κ i)]
  [inst_7 : (i : ι) → DecidableEq (κ i)] {f g : MultilinearMap R (fun i => (j : κ i) → M i j) N},
  f = g ↔
    ∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => LinearMap.single R (M i) (p i)) =
        g.compLinearMap fun i => LinearMap.single R (M i) (p i)
-- Mathlib.Algebra.Category.Ring.Limits
CommRingCat.limitCommRing : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommRingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommRingCat)).sections] →
        CommRing (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget CommRingCat))).pt
-- Mathlib.Order.Minimal
not_maximal_iff_exists_gt : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : Preorder α], P x → (¬Maximal P x ↔ ∃ y, x < y ∧ P y)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.UnsatProof.lt : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Lean.Meta.Grind.Arith.Linear.UnsatProof
-- Lean.Server.Completion.EligibleHeaderDecls
Lean.Server.Completion.EligibleDecl.tags : Lean.Server.Completion.EligibleDecl → Lean.MetaM (Array Lean.Lsp.CompletionItemTag)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.mk.sizeOf_spec : ∀ {X Y : AlgebraicGeometry.Scheme} (domain : X.Opens) (dense_domain : Dense ↑domain) (hom : ↑domain ⟶ Y),
  sizeOf { domain := domain, dense_domain := dense_domain, hom := hom } = 1 + sizeOf domain + sizeOf hom
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
intervalIntegral.mul_integral_comp_sub_mul : ∀ {a b : ℝ} {f : ℝ → ℝ} (c d : ℝ), c * ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
-- Init.Data.List.Nat.Modify
List.take_modifyHead : ∀ {α : Type u_1} {f : α → α} {l : List α} {i : ℕ}, List.take i (List.modifyHead f l) = List.modifyHead f (List.take i l)
-- Mathlib.Data.W.Basic
_private.Mathlib.Data.W.Basic.0.WType.encodable_zero : {α : Type u_1} → {β : α → Type u_2} → [inst : (a : α) → Fintype (β a)] → Encodable (WType.WType'✝ β 0)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.isVertexCover_bot : ∀ {V : Type u_1} (c : Set V), ⊥.IsVertexCover c
-- Mathlib.RingTheory.Ideal.Operations
Ideal.pow_le_self : ∀ {R : Type u} [inst : Semiring R] {I : Ideal R} {n : ℕ}, n ≠ 0 → I ^ n ≤ I
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the monadic predicate `p` returns `true` for
all element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are
examined in order of iteration.

This variant terminates after finitely mall steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.allM`.
 -/
Std.Iter.Total.allM : {α β : Type w} →
  {m : Type → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id m] → [Std.Iterators.Finite α Id] → (β → m Bool) → Std.Iter.Total β → m Bool
-- Init.Data.Range.Polymorphic.PRange
/-- This type class ensures that right-open ranges \(i.e., for bounds `a` and `b`,
`a...b`, `a<...b` and `*...b`\) are always finite.
This is a prerequisite for many functions and instances, such as
`Rco.toList` or `ForIn'`.
 -/
Std.Rxo.IsAlwaysFinite : (α : Type u) → [Std.PRange.UpwardEnumerable α] → [LT α] → Prop
-- Mathlib.FieldTheory.RatFunc.Basic
/-- Subtraction of rational functions.  -/
RatFunc.sub : {K : Type u_1} → [inst : CommRing K] → RatFunc K → RatFunc K → RatFunc K
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
/-- An orthonormal basis of a finite-dimensional real inner product space `E` induces an
orthonormal basis of `⋀[ℝ]^n E`, indexed by `n`-element subsets of the index type.  -/
OrthonormalBasis.exteriorPower : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [inst_2 : FiniteDimensional ℝ E] →
        {I : Type u_2} →
          [inst_3 : Fintype I] →
            [LinearOrder I] → OrthonormalBasis I ℝ E → (n : ℕ) → OrthonormalBasis ↑(Set.powersetCard I n) ℝ ↥(⋀[ℝ]^n E)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffOn.csin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℂ n f s → ContDiffOn ℂ n (fun x => Complex.sin (f x)) s