mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Basic
/-- An integer is non-negative if it is equal to a natural number.
 -/
Int.NonNeg : ℤ → Prop
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.hasColimit_iff_small_colimitType : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TopCat),
  CategoryTheory.Limits.HasColimit F ↔ Small.{u, max u v} (F.comp (CategoryTheory.forget TopCat)).ColimitType
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.vadd'.eq_1 : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] [inst_2 : VAdd S R]
  [inst_3 : VAdd S M] [inst_4 : VAddAssocClass S R M] (p : SubAddAction R M),
  p.vadd' = { vadd := fun c x => ⟨c +ᵥ ↑x, ⋯⟩ }
-- Mathlib.Data.Set.Sigma
Set.univ_sigma_univ : ∀ {ι : Type u_1} {α : ι → Type u_3} {i : ι}, (Set.univ.sigma fun x => Set.univ) = Set.univ
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instToSnapshotTreeTacticFinishedSnapshot : Lean.Language.ToSnapshotTree Lean.Elab.Tactic.TacticFinishedSnapshot
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_mono : Monotone Cardinal.ofENat
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.coeff_charpolyRev_eq_neg_trace : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.charpolyRev.coeff 1 = -M.trace
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CategoryTheory.Functor.mapCochainComplexPlus.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : F.PreservesZeroMorphisms], F.mapCochainComplexPlus = F_1.mapCochainComplexPlus
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.continuous_tan : Continuous fun x => Complex.tan ↑x
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsFinite.iff_isProper_and_isAffineHom : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.IsFinite f ↔ AlgebraicGeometry.IsProper f ∧ AlgebraicGeometry.IsAffineHom f
-- Mathlib.Topology.CompactOpen
ContinuousOn.compCM : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [LocallyCompactPair Y Z] {X' : Type u_6} [inst_4 : TopologicalSpace X']
  {g : X' → C(Y, Z)} {f : X' → C(X, Y)} {s : Set X'},
  ContinuousOn g s → ContinuousOn f s → ContinuousOn (fun x => (g x).comp (f x)) s
-- Mathlib.Data.Finset.Insert
Finset.insert_val' : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Finset α), (insert a s).val = (a ::ₘ s.val).dedup
-- Mathlib.Topology.UniformSpace.UniformEmbedding
completeSpace_iff_isComplete_range : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → (CompleteSpace α ↔ IsComplete (Set.range f))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_eq_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k fallback : α}, t.contains k = true → t.getD k fallback = k
-- Std.Http.Data.Headers
/-- Adds a header from string name and value.
Returns `none` if either the header name or value is invalid.
 -/
Std.Http.Headers.insert? : Std.Http.Headers → String → String → Option Std.Http.Headers
-- Lean.Meta.Basic
Lean.Meta.State.cache : Lean.Meta.State → Lean.Meta.Cache
-- Init.Data.UInt.Lemmas
UInt32.ofNatClamp_bitVecToNat : ∀ (n : BitVec 32), UInt32.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.Combinatorics.Pigeonhole
/-- The strong pigeonhole principle for finitely many pigeons and pigeonholes. There is a pigeonhole
with at most as many pigeons as the floor of the average number of pigeons across all pigeonholes.
 -/
Fintype.exists_card_fiber_lt_of_card_lt_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {b : M} [inst_3 : CommSemiring M] [inst_4 : LinearOrder M] [IsStrictOrderedRing M],
  ↑(Fintype.card α) < Fintype.card β • b → ∃ y, ↑{x | f x = y}.card < b
-- Lean.Parser.Command
Lean.Parser.Command.structImplicitBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.schur_complement_eq₂₂ : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : CommRing α] [inst_1 : StarRing α] [inst_2 : Fintype m]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (A : Matrix m m α) (B : Matrix m n α) {D : Matrix n n α} (x : m → α)
  (y : n → α) [Invertible D],
  D.IsHermitian →
    Matrix.vecMul (star (Sum.elim x y)) (Matrix.fromBlocks A B B.conjTranspose D) ⬝ᵥ Sum.elim x y =
      Matrix.vecMul (star ((D⁻¹ * B.conjTranspose).mulVec x + y)) D ⬝ᵥ ((D⁻¹ * B.conjTranspose).mulVec x + y) +
        Matrix.vecMul (star x) (A - B * D⁻¹ * B.conjTranspose) ⬝ᵥ x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.toSubmodule_eq_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S : NonUnitalSubalgebra R A}, S.toSubmodule = ⊤ ↔ S = ⊤
-- Init.Data.UInt.Bitwise
USize.zero_xor : ∀ {a : USize}, 0 ^^^ a = a
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.coeff_smul_left : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ']
  [inst_2 : VAdd Γ Γ'] [inst_3 : IsOrderedCancelVAdd Γ Γ'] [inst_4 : AddCommMonoid V] [inst_5 : Zero R]
  [inst_6 : SMulWithZero R V] {x : HahnSeries Γ R} {y : HahnModule Γ' R V} {a : Γ'} {s : Set Γ} (hs : s.IsPWO),
  x.support ⊆ s →
    ((HahnModule.of R).symm (x • y)).coeff a =
      ∑ ij ∈ Finset.VAddAntidiagonal a ⋯, x.coeff ij.1 • ((HahnModule.of R).symm y).coeff ij.2
-- Lean.Meta.Tactic.Simp.Main
/-- If `e` is a raw Nat literal and `OfNat.ofNat` is not in the list of declarations to unfold,
return an `OfNat.ofNat`-application.
 -/
Lean.Meta.Simp.foldRawNatLit : Lean.Expr → Lean.Meta.SimpM Lean.Expr
-- Mathlib.Data.Nat.Prime.Defs
Nat.not_prime_zero : ¬Nat.Prime 0
-- Mathlib.Analysis.Normed.Lp.lpSpace
PreLp.zero_apply : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {i : α}, 0 i = 0
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.instIsMarkovKernelCondDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} [inst_4 : MeasurableSpace β],
  ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.condDistrib Y X μ)
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
`[Nontrivial R]` is needed, otherwise for `l = []` we have `⊥` in the LHS and `0` in the RHS.
 -/
Polynomial.degree_list_prod : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] [Nontrivial R] (l : List (Polynomial R)),
  l.prod.degree = (List.map Polynomial.degree l).sum
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the second commutative square of a triangle morphism  -/
CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (self : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂),
  CategoryTheory.CategoryStruct.comp T₁.mor₂ self.hom₃ = CategoryTheory.CategoryStruct.comp self.hom₂ T₂.mor₂
-- Init.Data.List.Basic
List.isEqv_nil_cons : ∀ {α : Type u} {a : α} {as : List α} {eqv : α → α → Bool}, [].isEqv (a :: as) eqv = false
-- Mathlib.Algebra.Group.Defs
AddCommMonoid.toAddMonoid : {M : Type u} → [self : AddCommMonoid M] → AddMonoid M
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp},
  Std.TreeMap.Raw.empty.Equiv t ↔ t.isEmpty = true
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go_get_aux : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr)
  (hfoo :
    aig.decls.size ≤
      (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).vec.get idx ⋯ =
    (s.get idx hidx).cast hfoo
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Auxiliary lemma in the proof of `integral_eq_sub_of_hasDeriv_right_of_le`.  -/
intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le : ∀ {g' g φ : ℝ → ℝ} {a b : ℝ},
  a ≤ b →
    ContinuousOn g (Set.Icc a b) →
      (∀ x ∈ Set.Ioo a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
        MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume →
          (∀ x ∈ Set.Ioo a b, φ x ≤ g' x) → ∫ (y : ℝ) in a..b, φ y ≤ g b - g a
-- Mathlib.CategoryTheory.Limits.Cones
/-- Change a cocone on `F.rightOp : J ⥤ Cᵒᵖ` to a cone on `F : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.coneOfCoconeRightOp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor Jᵒᵖ C} → CategoryTheory.Limits.Cocone F.rightOp → CategoryTheory.Limits.Cone F
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.StrongTrans F G) {a b c : B} (f : a ⟶ b)
  (g : b ⟶ c) {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (self.app a) (CategoryTheory.CategoryStruct.comp (G.map f) (G.map g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).inv
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).hom h)))))
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] {Z : AlgebraicGeometry.SheafedSpace C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict f).hom
      (CategoryTheory.CategoryStruct.comp (Y.ofRestrict ⋯) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
TensorProduct.Algebra.eq_of_fg_of_subtype_eq' : ∀ {R : Type u_1} {S : Type u_2} {N : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {A : Subalgebra R S},
  A.FG →
    ∀ {t : TensorProduct R (↥A) N} {A' : Subalgebra R S},
      A'.FG →
        ∀ {t' : TensorProduct R (↥A') N},
          (LinearMap.rTensor N A.val.toLinearMap) t = (LinearMap.rTensor N A'.val.toLinearMap) t' →
            ∃ B,
              ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
                B.FG ∧
                  (LinearMap.rTensor N (Subalgebra.inclusion hAB).toLinearMap) t =
                    (LinearMap.rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'
-- Mathlib.Data.Finset.Max
Finset.min'_pair : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), {a, b}.min' ⋯ = min a b
-- Std.Time.Internal.Bounded
/-- Convert a `Nat` to a `Bounded.LE`.
 -/
Std.Time.Internal.Bounded.LE.ofNat : {hi : ℕ} → (val : ℕ) → val ≤ hi → Std.Time.Internal.Bounded.LE 0 ↑hi
-- Init.Data.UInt.Bitwise
UInt32.ofNatLT_xor : ∀ (a b : ℕ) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32),
  UInt32.ofNatLT (a ^^^ b) ⋯ = UInt32.ofNatLT a ha ^^^ UInt32.ofNatLT b hb
-- Mathlib.Order.RelIso.Basic
/-- The induced relation on a subtype is an embedding under the natural inclusion.  -/
Subtype.relEmbedding : {X : Type u_5} → (r : X → X → Prop) → (p : X → Prop) → Subtype.val ⁻¹'o r ↪r r
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.inter_I₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S)
  (F : CategoryTheory.PreOneHypercover S)
  [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)]
  [inst_2 :
    ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
      CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
        (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))]
  (i j : (E.inter F.toPreZeroHypercover).I₀), (E.inter F).I₁ i j = (E.I₁ i.1 j.1 × F.I₁ i.2 j.2)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instNonUnitalRingOfIsTopologicalRing : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : NonUnitalRing β] → [IsTopologicalRing β] → NonUnitalRing C(α, β)
-- Mathlib.MeasureTheory.Order.Lattice
Measurable.inf_const : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f : α → M} [inst_1 : Min M]
  [MeasurableInf M], Measurable f → ∀ (c : M), Measurable fun x => f x ⊓ c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  (self : CategoryTheory.Limits.ChosenPullback f₁ f₂),
  CategoryTheory.CategoryStruct.comp self.p₁ f₁ = CategoryTheory.CategoryStruct.comp self.p₂ f₂
-- Init.Data.UInt.Basic
instShiftLeftUInt8 : ShiftLeft UInt8
-- Mathlib.Analysis.Normed.Module.Complemented
Submodule.IsCompl.isTopCompl_of_isClosed : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {p q : Subspace 𝕜 E},
  IsCompl p q → IsClosed ↑p → IsClosed ↑q → Submodule.IsTopCompl p q
-- Mathlib.RingTheory.WittVector.WittPolynomial
constantCoeff_wittPolynomial : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [hp : Fact (Nat.Prime p)] (n : ℕ),
  MvPolynomial.constantCoeff (wittPolynomial p R n) = 0
-- Mathlib.SetTheory.Ordinal.Notation
/-- The fast growing hierarchy for ordinal notations `< ε₀`. This is a sequence of functions `ℕ → ℕ`
indexed by ordinals, with the definition:

* `f_0(n) = n + 1`
* `f_(α + 1)(n) = f_α^[n](n)`
* `f_α(n) = f_(α[n])(n)` where `α` is a limit ordinal and `α[i]` is the fundamental sequence
  converging to `α`  -/
ONote.fastGrowing : ONote → ℕ → ℕ
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
/-- A property of objects satisfies `P.IsClosedUnderLimitsOfShape J` if it
is stable by limits of shape `J`.  -/
CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.ObjectProperty C → (J : Type u') → [CategoryTheory.Category.{v', u'} J] → Prop
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measurableSet_of_continuousAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {β : Type u_6}
  [inst_3 : PseudoEMetricSpace β] (f : α → β), MeasurableSet {x | ContinuousAt f x}
-- Lean.Parser.Basic
Lean.Parser.RecoveryContext.mk.sizeOf_spec : ∀ (initialPos : String.Pos.Raw) (initialSize : ℕ),
  sizeOf { initialPos := initialPos, initialSize := initialSize } = 1 + sizeOf initialPos + sizeOf initialSize
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Turn an element of a type `F` satisfying `OrderIsoClass F α β` and `AddEquivClass F α β`
into an actual `OrderAddMonoidIso`.
This is declared as the default coercion from `F` to `α ≃+o β`.  -/
OrderMonoidIsoClass.toOrderAddMonoidIso : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : AddZeroClass α] →
            [inst_3 : AddZeroClass β] →
              [inst_4 : EquivLike F α β] → [OrderIsoClass F α β] → [AddEquivClass F α β] → F → α ≃+o β
-- Init.Data.Nat.ToString
Nat.digitChar_eq_d : ∀ {n : ℕ}, n.digitChar = 'd' ↔ n = 13
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Presieve.CoverByImageStructure.fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {V U : D} {f : V ⟶ U}
  (self : CategoryTheory.Presieve.CoverByImageStructure G f) {Z : D} (h : U ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.lift (CategoryTheory.CategoryStruct.comp self.map h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Algebra.Group.Ext
AddLeftCancelMonoid.ext : ∀ {M : Type u} ⦃m₁ m₂ : AddLeftCancelMonoid M⦄, HAdd.hAdd = HAdd.hAdd → m₁ = m₂
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.IsExtremePt.map_le_of_mem_of_lt : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {y : α},
  ChainCompletePartialOrder.IsExtremePt x f y → ∀ {z : α}, z ∈ ChainCompletePartialOrder.bot x f → z < y → f z ≤ y
-- Mathlib.Order.Filter.Map
Filter.comap_sSup : ∀ {α : Type u_1} {β : Type u_2} {s : Set (Filter β)} {m : α → β}, Filter.comap m (sSup s) = ⨆ f ∈ s, Filter.comap m f
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM : Type → Type
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- The closure of a `PreAbstractSimplicialComplex` to an `AbstractSimplicialComplex` by adding
all singletons.  -/
PreAbstractSimplicialComplex.addSingletons : (ι : Type u_1) → PreAbstractSimplicialComplex ι → AbstractSimplicialComplex ι
-- Mathlib.Algebra.Lie.Weights.Killing
/-- The restriction of the Killing form to a Cartan subalgebra, as a linear equivalence to the
dual.  -/
LieAlgebra.IsKilling.cartanEquivDual : {K : Type u_2} →
  {L : Type u_3} →
    [inst : LieRing L] →
      [inst_1 : Field K] →
        [inst_2 : LieAlgebra K L] →
          [FiniteDimensional K L] →
            (H : LieSubalgebra K L) → [H.IsCartanSubalgebra] → [LieAlgebra.IsKilling K L] → ↥H ≃ₗ[K] Module.Dual K ↥H
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitorNatIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategory.rightUnitorNatIso C).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.SubobjectRepresentableBy.iso`.

---

`h.iso m` is the isomorphism between `m` and the pullback of `Ω₀`
along the characteristic map of `m`.  -/
CategoryTheory.Classifier.SubobjectRepresentableBy.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) →
          {U X : C} →
            (m : U ⟶ X) →
              [inst_2 : CategoryTheory.Mono m] →
                CategoryTheory.MonoOver.mk m ≅
                  CategoryTheory.Subobject.representative.obj ((CategoryTheory.Subobject.pullback (h.χ m)).obj h.Ω₀)
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.sum_eq_one : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s) {x : M}, x ∈ s → ∑ᶠ (i : ι), (f i) x = 1
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : Fintype ι] [inst_1 : Fintype ι'] (X : ι ⊕ ι' → Type u_4)
  [inst_2 : (i : ι ⊕ ι') → MeasureTheory.MeasureSpace (X i)]
  [∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X).symm) MeasureTheory.volume MeasureTheory.volume
-- Mathlib.Order.SetDissipate
Set.iInter_subset_dissipate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : LE α] (x : α), ⋂ i, s i ⊆ Set.dissipate s x
-- Mathlib.NumberTheory.LSeries.RiemannZeta
differentiableOn_riemannZeta : DifferentiableOn ℂ riemannZeta {1}ᶜ
-- Mathlib.Data.Finset.Powerset
Finset.mem_powerset : ∀ {α : Type u_1} {s t : Finset α}, s ∈ t.powerset ↔ s ⊆ t
-- Mathlib.Algebra.Opposites
AddOpposite.unop_inv : ∀ {α : Type u_1} [inst : Inv α] (a : αᵃᵒᵖ), AddOpposite.unop a⁻¹ = (AddOpposite.unop a)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.mk : {D : Type u_1} →
  {D' : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] →
        {F : CategoryTheory.Functor D D'} →
          {C : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.MonoidalCategory C] →
                [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
                  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] →
                    [toLaxLeftLinear : F.LaxLeftLinear C] →
                      [toOplaxLeftLinear : F.OplaxLeftLinear C] →
                        (∀ (c : C) (d : D),
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d)
                                (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d) =
                              CategoryTheory.CategoryStruct.id
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c (F.obj d))) →
                          (∀ (c : C) (d : D),
                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxLeftLinear.δₗ F c d)
                                  (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d) =
                                CategoryTheory.CategoryStruct.id
                                  (F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d))) →
                            F.LeftLinear C
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_fst : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  ↑(ContinuousAlgHom.fst R A B) = AlgHom.fst R A B
-- Mathlib.Algebra.Ring.Subring.Order
/-- The inclusion `S → R` of a subring, as an ordered ring homomorphism.  -/
Subring.orderedSubtype : {R : Type u_1} → [inst : Ring R] → [inst_1 : PartialOrder R] → (s : Subring R) → ↥s →+*o R
-- Batteries.Recycling.RBTree.WF
/-- The red-red invariant is monotonic in `p`.  -/
RBTree.RBNode.RedRed.imp : ∀ {p q : Prop} {α : Type u_1} {t : RBTree.RBNode α} {n : ℕ},
  (p → q) → RBTree.RBNode.RedRed p t n → RBTree.RBNode.RedRed q t n