mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousInv.measurableInv : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] [inst_3 : Inv γ]
  [ContinuousInv γ], MeasurableInv γ
-- Mathlib.Data.W.Constructions
WType.Listα.cons : {γ : Type u} → γ → WType.Listα γ
-- Mathlib.Algebra.Homology.Homotopy
/-- a variant of `Homotopy.compLeft` useful for dealing with homotopy equivalences.  -/
Homotopy.compLeftId : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            {f : D ⟶ D} →
              Homotopy f (CategoryTheory.CategoryStruct.id D) →
                (g : C ⟶ D) → Homotopy (CategoryTheory.CategoryStruct.comp g f) g
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerRight_rightUnitor_hom : ∀ {A : Type u_1} {B : Type u_2} (C : Type u_3) [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]
  (F : CategoryTheory.Functor A B),
  CategoryTheory.Join.mapWhiskerRight F.rightUnitor.hom (CategoryTheory.Functor.id C) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompLeft C F (CategoryTheory.Functor.id B)).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id C)).whiskerLeft CategoryTheory.Join.mapPairId.hom)
        (CategoryTheory.Join.mapPair F (CategoryTheory.Functor.id C)).rightUnitor.hom)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.zero_eval : ∀ (v : List ℕ), Turing.ToPartrec.Code.zero.eval v = pure [0]
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.instAddOfIsOrderedAddMonoid.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [inst_2 : AddCommMonoid β]
  [inst_3 : Preorder β] [inst_4 : IsOrderedAddMonoid β],
  OrderAddMonoidHom.instAddOfIsOrderedAddMonoid =
    {
      add := fun f g =>
        let __src := ↑f + ↑g;
        { toAddMonoidHom := __src, monotone' := ⋯ } }
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod_inv_inl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop
      CategoryTheory.Limits.coprod.inl.unop =
    CategoryTheory.Limits.prod.fst
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.isOpen_iff : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set α} {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → (IsOpen s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.bot_adj : ∀ {V : Type u} (v w : V), ⊥.Adj v w ↔ False
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.mem_pointwise_smul_iff_inv_smul_mem : ∀ {M : Type u_1} {R : Type u_2} [inst : Group M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Subring R} {x : R}, x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.Grp.hom_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (H : CategoryTheory.Grp C) [inst_3 : CategoryTheory.IsCommMonObj H.X],
  CategoryTheory.MonObj.one.hom.hom = CategoryTheory.MonObj.one
-- Aesop.Forward.State
Aesop.Hyp.mk : Option Lean.FVarId → Aesop.Substitution → Aesop.Hyp
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    k ∉ m →
      List.Pairwise (fun a b => (a == b) = false) l →
        k ∈ l → (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKey? k' = some k
-- Mathlib.Data.TypeVec
/-- append an arrow and a function for arbitrary source and target type vectors  -/
TypeVec.splitFun : {n : ℕ} →
  {α : TypeVec.{u_1} (n + 1)} → {α' : TypeVec.{u_2} (n + 1)} → α.drop.Arrow α'.drop → (α.last → α'.last) → α.Arrow α'
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.mk.injEq : ∀ (env : Lean.Environment) (cmdEnv? : Option Lean.Environment) (fileMap : Lean.FileMap) (mctx : Lean.MetavarContext)
  (options : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (ngen : Lean.NameGenerator)
  (env_1 : Lean.Environment) (cmdEnv?_1 : Option Lean.Environment) (fileMap_1 : Lean.FileMap)
  (mctx_1 : Lean.MetavarContext) (options_1 : Lean.Options) (currNamespace_1 : Lean.Name)
  (openDecls_1 : List Lean.OpenDecl) (ngen_1 : Lean.NameGenerator),
  ({ env := env, cmdEnv? := cmdEnv?, fileMap := fileMap, mctx := mctx, options := options,
        currNamespace := currNamespace, openDecls := openDecls, ngen := ngen } =
      { env := env_1, cmdEnv? := cmdEnv?_1, fileMap := fileMap_1, mctx := mctx_1, options := options_1,
        currNamespace := currNamespace_1, openDecls := openDecls_1, ngen := ngen_1 }) =
    (env = env_1 ∧
      cmdEnv? = cmdEnv?_1 ∧
        fileMap = fileMap_1 ∧
          mctx = mctx_1 ∧
            options = options_1 ∧ currNamespace = currNamespace_1 ∧ openDecls = openDecls_1 ∧ ngen = ngen_1)
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The `n`-th coefficient of the `k`-th power of a power series.  -/
PowerSeries.coeff_pow : ∀ {R : Type u_2} [inst : CommSemiring R] (k n : ℕ) (φ : PowerSeries R),
  (PowerSeries.coeff n) (φ ^ k) =
    ∑ l ∈ (Finset.range k).finsuppAntidiag n, ∏ i ∈ Finset.range k, (PowerSeries.coeff (l i)) φ
-- Mathlib.Analysis.Matrix.Order
/-- The kronecker product of two positive semi-definite matrices is positive semi-definite.  -/
Matrix.PosSemidef.kronecker : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [Finite n] {m : Type u_3} [Finite m] {x : Matrix n n 𝕜}
  {y : Matrix m m 𝕜}, x.PosSemidef → y.PosSemidef → (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y).PosSemidef
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
_private.Mathlib.Data.Nat.Factorial.DoubleFactorial.0.Nat.doubleFactorial.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ.succ => h_3 k) =
    h_2 ()
-- Mathlib.Analysis.Calculus.FDeriv.Basic
fderivWithin_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s t : Set E},
  t ∈ nhds x → fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x
-- Mathlib.Order.Category.BoolAlg
_private.Mathlib.Order.Category.BoolAlg.0.BoolAlg.Hom.mk.injEq : ∀ {X Y : BoolAlg} (hom' hom'_1 : BoundedLatticeHom ↑X ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Data.Sym.Sym2
Sym2.coe_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (z : Sym2 α), ↑(Sym2.map f z) = f '' ↑z
-- Mathlib.Data.Multiset.UnionInter
Multiset.sup_eq_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s ⊔ t = s ∪ t
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.instIsTorsionFree : ∀ {R : Type u_3} {Γ : Type u_6} {V : Type u_7} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup V]
  [inst_3 : AddCommMonoid Γ] [inst_4 : LinearOrder Γ] [inst_5 : IsOrderedCancelAddMonoid Γ] [inst_6 : Module R V]
  [Module.IsTorsionFree R V], Module.IsTorsionFree (HahnSeries Γ R) (HahnModule Γ R V)
-- Std.Data.ExtHashSet.Lemmas
/-- This is a restatement of `contains_insert` that is written to exactly match the proof
obligation in the statement of `get_insert`.  -/
Std.ExtHashSet.contains_of_contains_insert' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α}, (m.insert k).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.Algebra.Category.Grp.EpiMono
AddCommGrpCat.epi_iff_range_eq_top : ∀ {A B : AddCommGrpCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ (AddCommGrpCat.Hom.hom f).range = ⊤
-- Mathlib.Order.Interval.Finset.Defs
Finset.Icc_ofDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : αᵒᵈ),
  Finset.Icc (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Icc b a)
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.eq_of_not_disjoint : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} {a b : G},
  ¬Disjoint (DoubleCoset.doubleCoset a ↑H ↑K) (DoubleCoset.doubleCoset b ↑H ↑K) →
    DoubleCoset.doubleCoset a ↑H ↑K = DoubleCoset.doubleCoset b ↑H ↑K
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.naturality_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f g : b ⟶ c} {pf : a ⟶ c} {η : f ≅ g}
  (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf) (η_g : CategoryTheory.CategoryStruct.comp p g ≅ pf),
  CategoryTheory.Bicategory.whiskerLeftIso p η ≪≫ η_g = η_f →
    CategoryTheory.Bicategory.whiskerLeftIso p η.symm ≪≫ η_f = η_g
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.homeomorph_comp_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E] {Y : Type u_4} [inst_4 : TopologicalSpace Y] (φ : X ≃ₜ Y),
  IsAddQuotientCoveringMap (⇑φ ∘ f) G ↔ IsAddQuotientCoveringMap f G
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.norm_unit : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] (u : (↥(Valued.integer K))ˣ),
  ‖↑u‖ = 1
-- Init.Data.SInt.Lemmas
ISize.div_self : ∀ {a : ISize}, a / a = if a = 0 then 0 else 1
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot_mem_affineSpan_image_compl : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.altitudeFoot i ∈ affineSpan ℝ (s.points '' {i}ᶜ)
-- Mathlib.GroupTheory.CoprodI
One.toOfNat1.hcongr_2 : ∀ (α α' : Type u_1), α = α' → ∀ (inst : One α) (inst' : One α'), inst ≍ inst' → One.toOfNat1 ≍ One.toOfNat1
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.left_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g), h.left.i = h.i.left
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [inst_1 : X.HasMap p] {c : X.CofanMapObjFun p j}
  (hc : CategoryTheory.Limits.IsColimit c) (i : I) (hi : p i = j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩)
      (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).hom =
    X.ιMapObj p i j hi
-- Std.Sat.CNF.Basic
/-- Variable `v` occurs in `Clause` `c`.
 -/
Std.Sat.CNF.Clause.Mem : {α : Type u_1} → α → Std.Sat.CNF.Clause α → Prop
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.self_le_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k kmi : α},
  (t.insert k).max?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.Algebra.Field.GeomSum
geom_sum₂_Ico : ∀ {K : Type u_2} [inst : Field K] {x y : K},
  x ≠ y → ∀ {m n : ℕ}, m ≤ n → ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i) = (x ^ n - y ^ (n - m) * x ^ m) / (x - y)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderTactic.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- the predicate of objects that are `≥ n` for `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.ge : {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] →
              CategoryTheory.Triangulated.TStructure C → ℤ → CategoryTheory.ObjectProperty C
-- Mathlib.Lean.Expr.Basic
/-- Check that an expression contains no metavariables (after instantiation).  -/
Lean.Expr.ensureHasNoMVars : Lean.Expr → Lean.MetaM Unit
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- `Res(f(x + r), g(x + r)) = Res(f, g)`.  -/
Polynomial.resultant_taylor : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (r : R),
  ((Polynomial.taylor r) f).resultant ((Polynomial.taylor r) g) = f.resultant g
-- Init.Data.Slice.List.Lemmas
List.mkSlice_rii_eq_mkSlice_rci : ∀ {α : Type u_1} {xs : List α}, Std.Rii.Sliceable.mkSlice xs *...* = Std.Rci.Sliceable.mkSlice xs 0...*
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx?.eq_def : ∀ {α : Type u} {β : Type v} (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : ℕ),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdx? x x_1 =
    match x, x_1 with
    | Std.DTreeMap.Internal.Impl.leaf, x => none
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n =>
      match compare n l.size with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx? l n
      | Ordering.eq => some (k, v)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.entryAtIdx? r (n - l.size - 1)
-- Init.Data.UInt.Lemmas
USize.eq_of_toFin_eq : ∀ {a b : USize}, a.toFin = b.toFin → a = b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback fallback' : α}, t.getD (t.maxD fallback) fallback' = t.maxD fallback
-- Mathlib.GroupTheory.Coxeter.Basic
/-- A group is a Coxeter group if it admits a Coxeter system for some Coxeter matrix `M`.  -/
IsCoxeterGroup : (W : Type u) → [Group W] → Prop
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abv_nonneg : ∀ {S : Type u_5} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_6} [inst_2 : Semiring R] (abv : R → S)
  [IsAbsoluteValue abv] (x : R), 0 ≤ abv x
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.holderConjugate_div_div : ∀ {p q r : ℝ}, p.HolderTriple q r → (p / r).HolderConjugate (q / r)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapRingHom_comp_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Monoid M]
  (f : R →+* S),
  (MonoidAlgebra.mapRingHom M f).comp (algebraMap R (MonoidAlgebra R M)) = (algebraMap S (MonoidAlgebra S M)).comp f
-- Mathlib.Analysis.SpecialFunctions.Log.Deriv
HasStrictFDerivAt.log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {f' : StrongDual ℝ E},
  HasStrictFDerivAt f f' x → f x ≠ 0 → HasStrictFDerivAt (fun x => Real.log (f x)) ((f x)⁻¹ • f') x
-- Mathlib.LinearAlgebra.Pi
/-- The linear map defeq to `Matrix.vecEmpty`  -/
LinearMap.vecEmpty : {R : Type u} →
  {M : Type v} →
    {M₃ : Type y} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₃] → [inst_3 : Module R M] → [inst_4 : Module R M₃] → M →ₗ[R] Fin 0 → M₃
-- Std.Http.Data.URI.Basic
Std.Http.URI.Path.mk.injEq : ∀ (segments : Array Std.Http.URI.EncodedSegment) (absolute : Bool) (segments_1 : Array Std.Http.URI.EncodedSegment)
  (absolute_1 : Bool),
  ({ segments := segments, absolute := absolute } = { segments := segments_1, absolute := absolute_1 }) =
    (segments = segments_1 ∧ absolute = absolute_1)
-- Mathlib.Data.Finset.PImage
/-- Rewrite `s.pimage f` in terms of `Finset.filter`, `Finset.attach`, and `Finset.image`.  -/
Finset.pimage_eq_image_filter : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom]
  {s : Finset α}, Finset.pimage f s = Finset.image (fun x => (f ↑x).get ⋯) {x ∈ s | (f x).Dom}.attach
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerveFunctor.full : CategoryTheory.nerveFunctor.Full
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.PrimeSpectrum.Top.eq_1 : ∀ (R : Type u) [inst : CommRing R], AlgebraicGeometry.PrimeSpectrum.Top R = TopCat.of (PrimeSpectrum R)
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.BindStruct.hg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Presieve X}
  {R : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → S f → CategoryTheory.Presieve Y} {Z : C} {h : Z ⟶ X} (self : S.BindStruct R h),
  R ⋯ self.g
-- Mathlib.RingTheory.Coalgebra.Basic
Pi.comul_coe_finsupp : ∀ {R : Type u_1} {n : Type u_2} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M : Type u_4}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : CoalgebraStruct R M] (x : n →₀ M),
  CoalgebraStruct.comul ⇑x = (TensorProduct.map Finsupp.lcoeFun Finsupp.lcoeFun) (CoalgebraStruct.comul x)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Hom.sum_apply : ∀ {V : Type u_3} {V' : Type u_4} {W : Type u_5} {W' : Type u_6} {G : SimpleGraph V} {H : SimpleGraph W}
  {G' : SimpleGraph V'} {H' : SimpleGraph W'} (f : G →g G') (g : H →g H') (a : V ⊕ W), (f.sum g) a = Sum.map (⇑f) (⇑g) a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} (h h' : CategoryTheory.MonoidalCategory.DayConvolution F G)
  {Z : CategoryTheory.Functor (C × C) V}
  (h_1 :
    (CategoryTheory.MonoidalCategory.tensor C).comp (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.tensor C).whiskerLeft (h.uniqueUpToIso h').hom) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayConvolution.unit F G) h_1
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_fun_neg_right : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg F],
  (f =o[𝕜; l] fun x => -g x) ↔ f =o[𝕜; l] g
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.instUniqueHomΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {c : CategoryTheory.Subobject.Classifier C} → (Y : C) → Unique (Y ⟶ c.Ω₀)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.mapIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : W ≅ Y) (g : X ≅ Z), (CategoryTheory.Limits.prod.mapIso f g).hom = CategoryTheory.Limits.prod.map f.hom g.hom
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableWithinAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {z : M} {f : M → E'} {s : Set M}, MDiffAt[s] f z → MDiffAt[s] (-f) z
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.liftOn₂_mk : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : Sort u_4} (f : M → ↥S → M → ↥S → p)
  (H :
    ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
      (AddLocalization.r S) (a, b) (a', b') → (AddLocalization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d')
  (a c : M) (b d : ↥S), (AddLocalization.mk a b).liftOn₂ (AddLocalization.mk c d) f H = f a b c d
-- Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskerLeft_app_snd : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  (F₁ : CategoryTheory.Functor J C) {F₂ F₂' : CategoryTheory.Functor J C} (g : F₂ ⟶ F₂') (j : J),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.whiskerLeft F₁ g).app j)
      (CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂'.obj j)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd (F₁.obj j) (F₂.obj j))
      (g.app j)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instIsAddApplyForall : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  [inst_7 : ContinuousAdd M₂], IsAddApply (ContinuousMultilinearMap R M₁ M₂) ((i : ι) → M₁ i) M₂
-- Init.System.IO
/-- Everything that was written to the process's standard error.  -/
IO.Process.Output.stderr : IO.Process.Output → String
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.map_evalRingHom_eval : ∀ {R : Type u_1} [inst : CommSemiring R] (x y : R) (p : Polynomial (Polynomial R)),
  Polynomial.eval y (Polynomial.map (Polynomial.evalRingHom x) p) = Polynomial.evalEval x y p
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subRight.eq_1 : ∀ {G : Type u_5} [inst : AddGroup G] (a : G),
  Equiv.subRight a = { toFun := fun b => b - a, invFun := fun b => b + a, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Analysis.Normed.Ring.Units
/-- In a normed ring with summable geometric series, the coercion from `Rˣ` (equipped with the
induced topology from the embedding in `R × R`) to `R` is an open map.  -/
Units.isOpenMap_val : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R], IsOpenMap Units.val
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instSub : {ι : Type u_1} → {G : ι → Type u_4} → [(i : ι) → Sub (G i)] → Sub ((i : ι) → G i)
-- Lean.Elab.Attributes
Lean.Elab.Attribute.kind : Lean.Elab.Attribute → Lean.AttributeKind
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.support.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (P P_1 : RingPreordering R) (e_P : P = P_1) [inst_1 : P.HasIdealSupport],
  P.support = P_1.support
-- Mathlib.ModelTheory.Definability
Set.Definable.compl : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {s : Set (α → M)},
  A.Definable L s → A.Definable L sᶜ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- A measurable embedding is a measurable function.  -/
MeasurableEmbedding.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : α → β},
  MeasurableEmbedding f → Measurable f
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
/-- An object admits a projective resolution.
 -/
CategoryTheory.HasProjectiveResolution : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → Prop