mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorObjImpl_rel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (X.tensorObjImpl Y).rel =
    (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst)).obj
        X.rel ⊓
      (CategoryTheory.Subobject.pullback
            (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)).obj
        Y.rel
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eraseKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValue? a (Std.Internal.List.eraseKey k l) =
      if (k == a) = true then none else Std.Internal.List.getValue? a l
-- Lean.Elab.SyntheticMVars
/-- Auxiliary function used to implement `synthesizeSyntheticMVars`.  -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.resumeElabTerm : Lean.Syntax → Option Lean.Expr → optParam Bool true → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Logic.Equiv.Set
Equiv.Set.sumDiffSubset.congr_simp : ∀ {α : Type u_3} {s t : Set α} (h : s ⊆ t) [inst : DecidablePred fun x => x ∈ s],
  Equiv.Set.sumDiffSubset h = Equiv.Set.sumDiffSubset h
-- Mathlib.Algebra.Order.Monoid.Units
Units.instOrd.eq_1 : ∀ {α : Type u_1} [inst : Monoid α] [inst_1 : Ord α], Units.instOrd = { compare := fun a b => compare ↑a ↑b }
-- Lean.Util.CollectAxioms
/-- Collect all axioms transitively used by a constant.  -/
Lean.collectAxioms : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Array Lean.Name)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Hom.codRestrict_toFun_coe : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (p : L.Substructure N) (f : L.Hom M N) (h : ∀ (c : M), f c ∈ p) (c : M),
  ↑((FirstOrder.Language.Hom.codRestrict p f h) c) = f c
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inrX_sndX_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι) {Z : C} (h : G.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ i) h) =
    h
-- Mathlib.Data.Set.Card
Set.encard_preimage_of_injective_subset_range : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β},
  Function.Injective f → t ⊆ Set.range f → (f ⁻¹' t).encard = t.encard
-- Mathlib.Geometry.Euclidean.Basic
/-- The inner product of two vectors given with `weightedVSub`, in
terms of the pairwise distances.  -/
EuclideanGeometry.inner_weightedVSub : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ι₁ : Type u_3} {s₁ : Finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P),
  ∑ i ∈ s₁, w₁ i = 0 →
    ∀ {ι₂ : Type u_4} {s₂ : Finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P),
      ∑ i ∈ s₂, w₂ i = 0 →
        inner ℝ ((s₁.weightedVSub p₁) w₁) ((s₂.weightedVSub p₂) w₂) =
          (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'App_hom_naturality : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) {M N : ModuleCat R₃} (φ : M ⟶ N),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars gf).map φ)
      (ModuleCat.restrictScalarsComp'App f g gf hgf N).hom =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsComp'App f g gf hgf M).hom
      ((ModuleCat.restrictScalars f).map ((ModuleCat.restrictScalars g).map φ))
-- Mathlib.Logic.Function.FromTypes
/-- Constant `n`-ary function with value `t`.  -/
Function.FromTypes.const : {n : ℕ} → (p : Fin n → Type u) → {τ : Type u} → τ → Function.FromTypes p τ
-- Mathlib.Order.RelClasses
/-- Inducts on a well-founded `<` relation.  -/
WellFoundedLT.induction : ∀ {α : Type u} [inst : LT α] [WellFoundedLT α] {motive : α → Prop} (a : α),
  (∀ (x : α), (∀ y < x, motive y) → motive x) → motive a
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Parse all imports in a text file at `path` and return just their names:
this is just a thin wrapper around `Lean.parseImports'`.
Omit `Init` (which is part of the prelude).  -/
findImports : System.FilePath → IO (Array Lean.Name)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.hasReturn : Lean.Elab.Term.Do.Code → Bool
-- Mathlib.Algebra.Polynomial.Laurent
/-- The semiring of Laurent polynomials with coefficients in the semiring `R`.
We denote it by `R[T;T⁻¹]`.
The ring homomorphism `C : R →+* R[T;T⁻¹]` includes `R` as the constant polynomials.  -/
LaurentPolynomial : (R : Type u_3) → [Semiring R] → Type (max u_3 0)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {f : β → β},
  (t.modify k f).isEmpty = false → (t.modify k f).maxKey! = if cmp t.maxKey! k = Ordering.eq then k else t.maxKey!
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.filterMap.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
CategoryTheory.Preadditive.RightFreyd.Candidate.desc.eq_1 : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts V] {u v : CategoryTheory.Arrow V} (f : u ⟶ v)
  {w : CategoryTheory.Arrow V} (g : v ⟶ w)
  (h : CategoryTheory.Arrow.RightHomotopy (CategoryTheory.CategoryStruct.comp f g) 0),
  CategoryTheory.Preadditive.RightFreyd.Candidate.desc f g h =
    CategoryTheory.Arrow.homMk (CategoryTheory.Limits.biprod.desc (CategoryTheory.Arrow.Hom.left g) h.hom)
      (CategoryTheory.Arrow.Hom.right g) ⋯
-- Init.Data.Nat.Fold
Nat.foldRev_zero : ∀ {α : Type u} (f : (i : ℕ) → i < 0 → α → α) (init : α), Nat.foldRev 0 f init = init
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.mapEquivMonic_symm_map_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (n : ℕ) (p : Polynomial.MonicDegreeEq S n) [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T],
  (MvPolynomial.mapEquivMonic R T n).symm (p.map (algebraMap S T)) =
    (IsScalarTower.toAlgHom R S T).comp ((MvPolynomial.mapEquivMonic R S n).symm p)
-- Mathlib.Logic.Function.Basic
Function.update_eq_const_of_subsingleton : ∀ {α : Sort u} {α' : Sort w} [inst : DecidableEq α] [Subsingleton α] (a : α) (v : α') (f : α → α'),
  Function.update f a v = Function.const α v
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.List.forIn'_cons.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.yield b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_2 b
-- Lean.Expr
Lean.FVarIdSet.ofArray : Array Lean.FVarId → Lean.FVarIdSet
-- Init.Data.Vector.Count
Vector.countP_true : ∀ {α : Type u_1} {n : ℕ}, (Vector.countP fun x => true) = fun x => n
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.eq) (h_2 : Unit → motive Ordering.lt)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.eq => h_1 ()
    | Ordering.lt => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddMonoid : {α : Type u_2} → [inst : Small.{v, u_2} α] → [AddMonoid α] → AddMonoid (Shrink.{v, u_2} α)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instInhabited.eq_1 : ∀ {α : Type u} [inst : AddMonoid α], AddUnits.instInhabited = { default := 0 }
-- Mathlib.Algebra.CubicDiscriminant
Cubic.c_of_eq : ∀ {R : Type u_1} {P Q : Cubic R} [inst : Semiring R], P.toPoly = Q.toPoly → P.c = Q.c
-- Init.Data.String.Iterate
String.Slice.RevPosIterator.mk.inj : ∀ {s : String.Slice} {currPos currPos_1 : s.Pos},
  { currPos := currPos } = { currPos := currPos_1 } → currPos = currPos_1
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.continuous_mk' : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : TopologicalSpace 𝕜],
  Continuous ⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p))
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If there is a primitive `n`-th root of unity in `K`, then `cyclotomic' n K` comes from a
monic polynomial with integer coefficients.  -/
Polynomial.int_coeff_of_cyclotomic' : ∀ {K : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] {ζ : K} {n : ℕ},
  IsPrimitiveRoot ζ n →
    ∃ P,
      Polynomial.map (Int.castRingHom K) P = Polynomial.cyclotomic' n K ∧
        P.degree = (Polynomial.cyclotomic' n K).degree ∧ P.Monic
-- Init.Data.SInt.Bitwise
Int16.neg_one_and : ∀ {a : Int16}, -1 &&& a = a
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : C} (f : X ⟶ Y), CategoryTheory.Epi (L.map f) ↔ P.epiModSerre f
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
LinearMap.BilinForm.orthogonal_eq_bot_iff : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {B : LinearMap.BilinForm K V} {W : Submodule K V},
  B.IsRefl → (B.restrict W).Nondegenerate → B.Nondegenerate → (B.orthogonal W = ⊥ ↔ W = ⊤)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCoconeEquiv_functor_map_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} {Y X : (CategoryTheory.Limits.Cocone F)ᵒᵖ} (f : Y ⟶ X),
  (CategoryTheory.Limits.coneRightOpOfCoconeEquiv.functor.map f).hom = f.unop.hom.op
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.iSup_labelGraph : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K), ⨆ k, C.labelGraph k = G
-- Init.Data.UInt.Lemmas
UInt8.toNat_mod_uInt16Size : ∀ (n : UInt8), n.toNat % UInt16.size = n.toNat
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.w_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {s t : CategoryTheory.Bicategory.LeftExtension f g} (η : s ⟶ t) {Z : a ⟶ c}
  (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.StructuredArrow.right t) ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.unit
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.StructuredArrow.Hom.right η)) h) =
    CategoryTheory.CategoryStruct.comp t.unit h
-- Mathlib.Order.Filter.Pointwise
Filter.pure_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {g : Filter β} {a : α}, pure a +ᵥ g = Filter.map (fun x => a +ᵥ x) g
-- Mathlib.Data.PNat.Basic
PNat.mk_ofNat : ∀ (n : ℕ) (h : 0 < n), ⟨OfNat.ofNat n, h⟩ = OfNat.ofNat n
-- Mathlib.Data.Vector3
/-- Get the tail of a nonempty vector.  -/
Vector3.tail : {α : Type u_1} → {n : ℕ} → Vector3 α (n + 1) → Vector3 α n
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.rightDual : (K : Type u) → [inst : Field K] → (V : FGModuleCat K) → CategoryTheory.HasRightDual V
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.ofSubsingleton_symm_apply_apply : ∀ (R : Type u_1) [inst : Semiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} [inst_5 : Subsingleton ι] (i : ι) (f : M [⋀^ι]→ₗ[R] N)
  (x : M), ((AlternatingMap.ofSubsingleton R M N i).symm f) x = f fun x_1 => x
-- Mathlib.Order.Filter.Extr
IsExtrFilter.neg : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α}
  {l : Filter α}, IsExtrFilter f l a → IsExtrFilter (fun x => -f x) l a
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.f_int_ofNat : ∀ (k : ℕ) {a : ℝ},
  0 ≤ a → ∀ (t : ℝ) (n : ℕ), HurwitzKernelBounds.f_int k a t (Int.ofNat n) = HurwitzKernelBounds.f_nat k a t n
-- Mathlib.Data.Stream.Init
Stream'.tail_drop : ∀ {α : Type u} (n : ℕ) (s : Stream' α), (Stream'.drop n s).tail = Stream'.drop n s.tail
-- Mathlib.Topology.Semicontinuity.Defs
Semicontinuous.isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop},
  Semicontinuous r → ∀ (b : β), IsOpen {x | r x b}
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- The measure of sets  -/
MeasureTheory.VectorMeasure.measureOf' : {α : Type u_3} →
  [inst : MeasurableSpace α] →
    {M : Type u_4} →
      [inst_1 : AddCommMonoid M] → [inst_2 : TopologicalSpace M] → MeasureTheory.VectorMeasure α M → Set α → M
-- Aesop.Rule.Name
Aesop.RuleName.instToString : ToString Aesop.RuleName
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comap_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), ⊤.comap f = ⊤
-- Mathlib.Data.Fin.Basic
Fin.natCast_eq_zero : ∀ {a n : ℕ} [inst : NeZero n], ↑a = 0 ↔ n ∣ a
-- Mathlib.Data.Matrix.ColumnRowPartitioned
/-- A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block
matrix.  -/
Matrix.fromRows_mul_fromCols : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [inst : Semiring R]
  [inst_1 : Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R),
  A₁.fromRows A₂ * B₁.fromCols B₂ = Matrix.fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.mk.injEq : ∀ (ref : Lean.Syntax) (fvarId : Lean.FVarId) (attrs : Array Lean.Elab.Attribute) (shortDeclName declName : Lean.Name)
  (parentName? : Option Lean.Name) (lctx : Lean.LocalContext) (localInstances : Lean.LocalInstances)
  (type val : Lean.Expr) (mvarId : Lean.MVarId) (termination : Lean.Elab.TerminationHints) (binders : Lean.Syntax)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (ref_1 : Lean.Syntax) (fvarId_1 : Lean.FVarId)
  (attrs_1 : Array Lean.Elab.Attribute) (shortDeclName_1 declName_1 : Lean.Name) (parentName?_1 : Option Lean.Name)
  (lctx_1 : Lean.LocalContext) (localInstances_1 : Lean.LocalInstances) (type_1 val_1 : Lean.Expr)
  (mvarId_1 : Lean.MVarId) (termination_1 : Lean.Elab.TerminationHints) (binders_1 : Lean.Syntax)
  (docString?_1 : Option (Lean.TSyntax `Lean.Parser.Command.docComment)),
  ({ ref := ref, fvarId := fvarId, attrs := attrs, shortDeclName := shortDeclName, declName := declName,
        parentName? := parentName?, lctx := lctx, localInstances := localInstances, type := type, val := val,
        mvarId := mvarId, termination := termination, binders := binders, docString? := docString? } =
      { ref := ref_1, fvarId := fvarId_1, attrs := attrs_1, shortDeclName := shortDeclName_1, declName := declName_1,
        parentName? := parentName?_1, lctx := lctx_1, localInstances := localInstances_1, type := type_1, val := val_1,
        mvarId := mvarId_1, termination := termination_1, binders := binders_1, docString? := docString?_1 }) =
    (ref = ref_1 ∧
      fvarId = fvarId_1 ∧
        attrs = attrs_1 ∧
          shortDeclName = shortDeclName_1 ∧
            declName = declName_1 ∧
              parentName? = parentName?_1 ∧
                lctx = lctx_1 ∧
                  localInstances = localInstances_1 ∧
                    type = type_1 ∧
                      val = val_1 ∧
                        mvarId = mvarId_1 ∧
                          termination = termination_1 ∧ binders = binders_1 ∧ docString? = docString?_1)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Context : Type
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (s : LowerSet α),
  ↑((LowerSet.map f) s) = ⇑f '' ↑s
-- Std.Data.DTreeMap.Basic
/-- Folds the given function over the mappings in the map in ascending order.  -/
Std.DTreeMap.foldl : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → {δ : Type w} → (δ → (a : α) → β a → δ) → δ → Std.DTreeMap α β cmp → δ
-- Mathlib.Topology.MetricSpace.DilationEquiv
IsometryEquiv.toDilationEquiv_toDilation : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (e : X ≃ᵢ Y),
  e.toDilationEquiv.toDilation = Isometry.toDilation ⇑e ⋯
-- Init.Data.String.Pattern.Char
String.Slice.Pattern.Char.instStrictBackwardPatternChar : ∀ {c : Char}, String.Slice.Pattern.StrictBackwardPattern c
-- Batteries.Classes.Order
Std.TransCmp.lt_of_lt_of_le : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {x y z : α},
  cmp x y = Ordering.lt → cmp y z ≠ Ordering.gt → cmp x z = Ordering.lt
-- Mathlib.Data.Finset.Pi
Finset.mem_piDiag : ∀ {α : Type u_1} {ι : Type u_2} [inst : DecidableEq (ι → α)] {s : Finset α} {f : ι → α},
  f ∈ s.piDiag ι ↔ ∃ a ∈ s, Function.const ι a = f
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.smul_prod : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] {R : Type u_4}
  [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E] {f : α → R} {g : β → E},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g ν → MeasureTheory.Integrable (fun z => f z.1 • g z.2) (μ.prod ν)
-- Mathlib.RingTheory.WittVector.WittPolynomial
wittPolynomial_zero : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R], wittPolynomial p R 0 = MvPolynomial.X 0
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.section_comp_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsReflexivePair f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.commonSection f g) f = CategoryTheory.CategoryStruct.id B
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.mul_le_dist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (x y : α), ↑K⁻¹ * dist x y ≤ dist (f x) (f y)
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atBot_pure : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] (f : α → β),
  Filter.Tendsto f Filter.atBot (pure (f ⊥))
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.HomologyData.exact_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData), S.Exact ↔ CategoryTheory.Limits.IsZero h.left.H
-- Mathlib.Data.Set.MemPartition
mem_memPartitionSet : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ) (a : α), a ∈ memPartitionSet f n a
-- Mathlib.Order.RelClasses
/-- Set notation form of `LT.lt.le` -/
LT.lt.subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b → a ⊆ b
-- Mathlib.Data.Int.NatAbs
Int.natAbs_natCast_sub_natCast_of_le : ∀ {a b : ℕ}, a ≤ b → (↑a - ↑b).natAbs = b - a
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.closure_map_eq_mapEquiv_closure : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N) [inst_7 : ContinuousAdd N] [inst_8 : ContinuousConstSMul R N]
  [inst_9 : ContinuousAdd M] [inst_10 : ContinuousConstSMul R M] (s : Submodule R M),
  (Submodule.map (↑↑f) s).closure = (ClosedSubmodule.mapEquiv f) s.closure
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.isColimitEquiv_symm_apply_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} {t : CategoryTheory.Limits.Cocone K}
  (t_1 : CategoryTheory.Limits.IsColimit t)
  (s : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)),
  (CategoryTheory.WithInitial.isColimitEquiv.symm t_1).desc s =
    ((CategoryTheory.WithInitial.coconeEquiv.toAdjunction.homEquiv' s t)
        (t_1.descCoconeMorphism (CategoryTheory.WithInitial.coconeEquiv.inverse.obj s))).hom
-- Mathlib.Order.Heyting.Basic
Prod.instBiheytingAlgebra : {α : Type u_2} → {β : Type u_3} → [BiheytingAlgebra α] → [BiheytingAlgebra β] → BiheytingAlgebra (α × β)
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.Precoverage.monotone_morphismProperty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C], Monotone CategoryTheory.Precoverage.morphismProperty
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encodeCode.eq_6 : ∀ (cf cg : Nat.Partrec.Code), (cf.comp cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode + 1) + 4
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcomp₁_map_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H)
  {X Y :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L')}
  (φ : X ⟶ Y),
  ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).map φ).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_ofFinsupp : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {x : S} {p : AddMonoidAlgebra R ℕ},
  Polynomial.eval₂ f x { toFinsupp := p } = (AddMonoidAlgebra.liftNC ↑f ⇑((powersHom S) x)) p
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.commRing : {X Y : AlgebraicGeometry.Scheme} → {f : X ⟶ Y} → (self : AlgebraicGeometry.ValuativeCommSq f) → CommRing self.R
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.middle_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  {S : J.Cover X} {T : (I : S.Arrow) → J.Cover I.Y} (I : (S.bind T).Arrow),
  CategoryTheory.CategoryStruct.comp I.toMiddleHom I.fromMiddleHom = I.f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ENodeMap : Type
-- Init.Data.List.Lemmas
List.map_inj : ∀ {α : Type u_1} {α_1 : Type u_2} {f g : α → α_1}, List.map f = List.map g ↔ f = g