mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
/-- The function on the indexing sets.  -/
CategoryTheory.Limits.FormalCoproduct.Hom.f : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : CategoryTheory.Limits.FormalCoproduct C} → X.Hom Y → X.I → Y.I
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.piLocalizationToMaximal_surjective : ∀ (R : Type u_1) [inst : CommSemiring R], Function.Surjective ⇑(PrimeSpectrum.piLocalizationToMaximal R)
-- Mathlib.RingTheory.RingHom.OpenImmersion
RingHom.IsStandardOpenImmersion.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.IsStandardOpenImmersion
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_eraseKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.getValueD k (Std.Internal.List.eraseKey k l) fallback = fallback
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.ind₂ : ∀ {V : Type u} {G : SimpleGraph V} {β : G.ConnectedComponent → G.ConnectedComponent → Prop},
  (∀ (v w : V), β (G.connectedComponentMk v) (G.connectedComponentMk w)) → ∀ (c d : G.ConnectedComponent), β c d
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.map_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (self : PresheafOfModules R) {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : ModuleCat ↑(R.obj X)}
  (h :
    (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g)))).obj (self.obj Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp (self.map (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (self.map f)
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (self.map g))
        (CategoryTheory.CategoryStruct.comp
          ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                  (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
            (self.obj Z))
          h))
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.unit_app_tensor_comp_inverse_map_δ_functor : ∀ {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] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (e.unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (e.inverse.map (CategoryTheory.Functor.OplaxMonoidal.δ e.functor X Y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.unit.app X) (e.unitIso.hom.app Y))
      (CategoryTheory.Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y))
-- Mathlib.Data.Opposite
Opposite.op_unop : ∀ {α : Sort u} (x : αᵒᵖ), Opposite.op (Opposite.unop x) = x
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.rpcNeedsReconnect : Lean.JsonRpc.ErrorCode
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember : Type
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inr_comp_pushoutSymmetry_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.Limits.pushoutSymmetry f g).hom =
    CategoryTheory.Limits.pushout.inl g f
-- Mathlib.NumberTheory.NumberField.DirichletDensity
/-- The Dirichlet density of `S` as a real number, taking the junk value `0` when `S` has no
density. As with `tsum`, this value only has content when `S` has a density; the genuine statement
that `S` has density `0` is `HasDirichletDensity S 0`.  -/
NumberField.Set.dirichletDensity : {K : Type u_1} →
  [inst : Field K] → [NumberField K] → Set (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) → ℝ
-- Mathlib.NumberTheory.NumberField.Norm
RingOfIntegers.norm_norm : ∀ {L : Type u_1} (K : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : Type u_3)
  [inst_3 : Field F] [inst_4 : Algebra K F] [FiniteDimensional K F] [inst_6 : Algebra F L] [FiniteDimensional F L]
  [IsScalarTower K F L] (x : NumberField.RingOfIntegers L),
  (RingOfIntegers.norm K) ((RingOfIntegers.norm F) x) = (RingOfIntegers.norm K) x
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.coeq₃_condition₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ : C}
  (f g h : j₁ ⟶ j₂),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.coeq₃Hom f g h) =
    CategoryTheory.CategoryStruct.comp h (CategoryTheory.IsFiltered.coeq₃Hom f g h)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map_map_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G)
  {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y), ((CategoryTheory.Grothendieck.map α).map f).base = f.base
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_of_contains_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α}, (Std.TreeMap.filterMap f t).contains k = true → t.contains k = true
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_abs_right`. -/
Asymptotics.IsLittleO.of_abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
  (f =o[l] fun x => |u x|) → f =o[l] u
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The image of ring of integers `𝓞 K` in the Euclidean mixed space.  -/
NumberField.mixedEmbedding.euclidean.integerLattice : (K : Type u_1) → [inst : Field K] → [NumberField K] → Submodule ℤ (NumberField.mixedEmbedding.euclidean.mixedSpace K)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The semantics for `BVExpr`.
 -/
Std.Tactic.BVDecide.BVExpr.eval : {w : ℕ} → Std.Tactic.BVDecide.BVExpr.Assignment → Std.Tactic.BVDecide.BVExpr w → BitVec w
-- Init.Data.UInt.Lemmas
UInt8.toUSize_mod : ∀ (a b : UInt8), (a % b).toUSize = a.toUSize % b.toUSize
-- Mathlib.Topology.Compactness.CountablyCompact
/-- **Alias** of the reverse direction of `isCountablyCompact_iff_seq_clusterPt`.

---

A set is countably compact if and only if every sequence eventually in it has a cluster point
in it.  -/
IsCountablyCompact.of_seq_clusterPt : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E},
  (∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in Filter.atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a Filter.atTop x) → IsCountablyCompact A
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.id : Lean.Meta.Sym.Arith.Semiring → ℕ
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_tensor_left_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y)
            (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).hom)))
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsMulLeftInvariant.map_mul_left_eq_self : ∀ {G : Type u_1} {inst : MeasurableSpace G} {inst_1 : Mul G} {μ : MeasureTheory.Measure G} [self : μ.IsMulLeftInvariant]
  (g : G), MeasureTheory.Measure.map (fun x => g * x) μ = μ
-- Init.Data.SInt.Basic
/-- Decides whether two 32-bit signed integers are equal. Usually accessed via the `DecidableEq Int32`
instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Int32.decEq 123 123 = .isTrue rfl`
 * `(if ((-7) : Int32) = 7 then "yes" else "no") = "no"`
 * `show (7 : Int32) = 7 by decide`
 -/
Int32.decEq : (a b : Int32) → Decidable (a = b)
-- Init.Data.Iterators.Consumers.Loop
Std.instForInIterOfMonadOfIteratorLoopId : (α β : Type w) →
  (n : Type x → Type x') → [Monad n] → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id n] → ForIn n (Std.Iter β) β
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Spec is a faithful functor.  -/
AlgebraicGeometry.instFaithfulOppositeCommRingCatLocallyRingedSpaceToLocallyRingedSpace : AlgebraicGeometry.Spec.toLocallyRingedSpace.Faithful
-- Mathlib.NumberTheory.ModularForms.Basic
CuspFormClass.mk : ∀ {F : Type u_2} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} [inst : FunLike F UpperHalfPlane ℂ]
  [toSlashInvariantFormClass : SlashInvariantFormClass F Γ k],
  (∀ (f : F), MDiff ⇑f) → (∀ (f : F) {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt (⇑f) k) → CuspFormClass F Γ k
-- Mathlib.Logic.Function.CompTypeclasses
/-- Class of Id maps  -/
CompTriple.IsId : {M : Type u_1} → (M → M) → Prop
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousAt.inv : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Inv G]
  [ContinuousInv G] {f : X → G} {x : X}, ContinuousAt f x → ContinuousAt f⁻¹ x
-- Lean.Environment
_private.Lean.Environment.0.Lean.setImportedEntries.unsafe_4 : Array (Lean.PersistentEnvExtension Lean.EnvExtensionEntry Lean.EnvExtensionEntry Lean.EnvExtensionState) →
  ℕ → Array Lean.EnvExtensionState → Array Lean.EnvExtensionEntry → ℕ → Array Lean.EnvExtensionState
-- Mathlib.Geometry.Convex.Set
/-- A convex subset of a convex space is a convex space.  -/
Convexity.ConvexSpace.subtype : {R : Type u_3} →
  {X : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsStrictOrderedRing R] →
          [inst_3 : Convexity.ConvexSpace R X] → (s : Set X) → Convexity.IsConvexSet R s → Convexity.ConvexSpace R ↑s
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_mul_sub_toIocMod : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), ↑(toIocDiv hp a b) * p + toIocMod hp a b = b
-- Init.Data.UInt.Lemmas
UInt8.sub_mul : ∀ {a b c : UInt8}, (a - b) * c = a * c - b * c
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.toExpr : Lean.Meta.Grind.NewFact → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  {h₁ h₂ : CategoryTheory.AddMonObj X}, h₁ = h₂ ↔ CategoryTheory.AddMonObj.add = CategoryTheory.AddMonObj.add
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.get?ₘ_eq_getValue? : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α},
      Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a =
        Std.Internal.List.getValue? a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Lean.Environment
Lean.AsyncConstantInfo.ofConstantInfo : Lean.ConstantInfo → Lean.AsyncConstantInfo
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax associativity.  -/
CategoryTheory.LaxFunctor.map₂_associator_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.LaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)),
  CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)) =
    CategoryTheory.CategoryStruct.comp ((self.mapComp g h).toNatTrans.app ((self.map f).toFunctor.obj X))
      ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- If `f` and `g` are in `X.PtSimplex n x`, then `RelStruct f g i.succ`
identifies to `MulStruct g .const f i`.  -/
SSet.PtSimplex.relStructSuccEquivMulStruct : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g : X.PtSimplex n x} → {i : Fin n} → f.RelStruct g i.succ ≃ g.MulStruct SSet.RelativeMorphism.const f i
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpaceCore.mem_chart_source : ∀ {H : Type u_5} [inst : TopologicalSpace H] {M : Type u_6} (self : ChartedSpaceCore H M) (x : M),
  x ∈ (self.chartAt x).source
-- Mathlib.Data.Nat.Choose.Basic
/-- `multichoose n k` is the number of multisets of cardinality `k` from a type of cardinality `n`.  -/
Nat.multichoose : ℕ → ℕ → ℕ
-- Mathlib.ModelTheory.Definability
/-- `TermDefinable₁` functions are closed under composition.  -/
Set.TermDefinable₁.comp : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {f g : M → M},
  Set.TermDefinable₁ L f → Set.TermDefinable₁ L g → Set.TermDefinable₁ L (f ∘ g)
-- Mathlib.Algebra.Order.Group.Finset
Finset.sup'_pow : ∀ {ι : Type u_1} {M : Type u_3} [inst : LinearOrder M] [inst_1 : Monoid M] [MulLeftMono M] [MulRightMono M]
  (s : Finset ι) (f : ι → M) (n : ℕ) (hs : s.Nonempty), s.sup' hs f ^ n = s.sup' hs fun a => f a ^ n
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.mk.injEq : ∀ {α : Type u_4} (vertexSet : Set α) (edgeSet : Set (Set α))
  (subset_vertexSet_of_mem_edgeSet' : ∀ ⦃e : Set α⦄, e ∈ edgeSet → e ⊆ vertexSet) (vertexSet_1 : Set α)
  (edgeSet_1 : Set (Set α)) (subset_vertexSet_of_mem_edgeSet'_1 : ∀ ⦃e : Set α⦄, e ∈ edgeSet_1 → e ⊆ vertexSet_1),
  ({ vertexSet := vertexSet, edgeSet := edgeSet,
        subset_vertexSet_of_mem_edgeSet' := subset_vertexSet_of_mem_edgeSet' } =
      { vertexSet := vertexSet_1, edgeSet := edgeSet_1,
        subset_vertexSet_of_mem_edgeSet' := subset_vertexSet_of_mem_edgeSet'_1 }) =
    (vertexSet = vertexSet_1 ∧ edgeSet = edgeSet_1)
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.restrictScalars_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {A B : AlgCat S} (g : A ⟶ B),
  (AlgCat.restrictScalars f).map g = AlgCat.ofHom (AlgHom.restrictScalars R (AlgCat.Hom.hom g))
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_add : ∀ {w acc' : ℕ} {x : BitVec w} {acc n : ℕ}, x.cpopNatRec n (acc + acc') = x.cpopNatRec n acc + acc'
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeTR.go.eq_1 : ∀ {α : Type u_1} (l : List α) (a : ℕ) (a_1 : Array α), List.takeTR.go✝ l [] a a_1 = l
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substAlgHom_X : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S} (ha : PowerSeries.HasSubst a), (PowerSeries.substAlgHom ha) PowerSeries.X = a
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.smul_measure : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μa : MeasureTheory.Measure α}
  {μb : MeasureTheory.Measure β} {f : α → β} {R : Type u_5} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal],
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb →
    ∀ (c : R), MeasureTheory.Measure.QuasiMeasurePreserving f (c • μa) (c • μb)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.isMultiplicative : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), F.relativelyRepresentable.IsMultiplicative
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The top subsemigroup is isomorphic to the semigroup.  -/
Subsemigroup.topEquiv : {M : Type u_1} → [inst : Mul M] → ↥⊤ ≃* M
-- Std.Time.Format.Modifier
Std.Time.Modifier.b.injEq : ∀ (presentation presentation_1 : Std.Time.Text),
  (Std.Time.Modifier.b presentation = Std.Time.Modifier.b presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.isWellFounded : ∀ {R : Type u} [inst : EuclideanDomain R], IsWellFounded R fun x1 x2 => EuclideanDomain.r x1 x2
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- Map an ideal `I` to a fractional ideal by forgetting `I` is integral.

This is a bundled version of `IsLocalization.coeSubmodule : Ideal R → Submodule R P`,
which is not to be confused with the `coe : FractionalIdeal S P → Submodule R P`,
also called `coeToSubmodule` in theorem names.

This map is available as a ring hom, called `FractionalIdeal.coeIdealHom`.
 -/
FractionalIdeal.instCoeTCIdeal : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → CoeTC (Ideal R) (FractionalIdeal S P)
-- Mathlib.Data.Prod.Basic
Prod.Lex.decidable : {α : Type u_1} →
  {β : Type u_2} →
    [DecidableEq α] →
      (r : α → α → Prop) → (s : β → β → Prop) → [DecidableRel r] → [DecidableRel s] → DecidableRel (Prod.Lex r s)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- The differential on the complex of morphisms between cochain complexes, as a linear map.  -/
CochainComplex.HomComplex.δ_hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (R : Type u_1) →
        [inst_2 : Ring R] →
          [inst_3 : CategoryTheory.Linear R C] →
            (F G : CochainComplex C ℤ) →
              (n m : ℤ) → CochainComplex.HomComplex.Cochain F G n →ₗ[R] CochainComplex.HomComplex.Cochain F G m
-- Lean.Server.References
Lean.Server.References.mk : Lean.Server.ILeanMap → Lean.Server.WorkerRefMap → Lean.Server.References
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotientInfEquivSupQuotient_surjective : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M),
  Function.Surjective ⇑(LinearMap.quotientInfToSupQuotient p p')
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_roo : ∀ {a b : ℕ}, (a<...b).size = b - a - 1
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
fderivWithin_iteratedFDerivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {n : ℕ},
  fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s =
    ⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ iteratedFDerivWithin 𝕜 (n + 1) f s
-- Mathlib.Dynamics.Flow
Flow.IsSemiconjugacy.surj : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddMonoid τ]
  {β : Type u_3} [inst_3 : TopologicalSpace β] {π : α → β} {ϕ : Flow τ α} {ψ : Flow τ β},
  Flow.IsSemiconjugacy π ϕ ψ → Function.Surjective π
-- Std.Data.HashSet.Basic
Std.HashSet.mk.inj : ∀ {α : Type u} {inst : BEq α} {inst_1 : Hashable α} {inner inner_1 : Std.HashMap α Unit},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rio_eq_self : ∀ {n i : ℕ}, i < n → (*...n).toList[i]! = i
-- Std.Http.Data.Headers.Value
Std.Http.Header.instInhabitedValue : Inhabited Std.Http.Header.Value
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- Any function in `ℒp` can be approximated by bounded continuous functions when `p < ∞`,
version in terms of `eLpNorm`.  -/
MeasureTheory.MemLp.exists_boundedContinuous_eLpNorm_sub_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} {p : ENNReal} [NormedSpace ℝ E] [μ.WeaklyRegular],
  p ≠ ⊤ →
    ∀ {f : α → E},
      MeasureTheory.MemLp f p μ →
        ∀ {ε : ENNReal}, ε ≠ 0 → ∃ g, MeasureTheory.eLpNorm (f - ⇑g) p μ ≤ ε ∧ MeasureTheory.MemLp (⇑g) p μ
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.smul_eq' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (z : CategoryTheory.CatCenter C) {X Y : C} (f : X ⟶ Y),
  z • f = CategoryTheory.CategoryStruct.comp (z.app X) f
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_fun_def_field : ∀ {k : Type u_1} [inst : Field k] (f : k → k) (a : k), slope f a = fun b => (f b - f a) / (b - a)
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_one : ∀ {α : Type u_1} [inst : One α], ofColex 1 = 1
-- Mathlib.Data.ENNReal.Operations
/-- This lemma has an abbreviated name because it is used frequently.  -/
ENNReal.cancel_coe : ∀ {a : NNReal}, AddLECancellable ↑a
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.range'TR.go.match_1.eq_1 : ∀ (motive : ℕ → ℕ → List ℕ → Sort u_1) (x : ℕ) (acc : List ℕ) (h_1 : (x : ℕ) → (acc : List ℕ) → motive 0 x acc)
  (h_2 : (n e : ℕ) → (acc : List ℕ) → motive n.succ e acc),
  (match 0, x, acc with
    | 0, x, acc => h_1 x acc
    | n.succ, e, acc => h_2 n e acc) =
    h_1 x acc
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.objEquiv_symm_notMem_horn_of_isIso : ∀ {n : ℕ} (i : Fin (n + 1)) {d : SimplexCategory} (f : d ⟶ { len := n }) [CategoryTheory.IsIso f],
  SSet.stdSimplex.objEquiv.symm f ∉ (SSet.horn n i).obj (Opposite.op d)
-- Mathlib.Data.Matrix.Basis
Matrix.diag_single_same : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Zero α] (i : n) (c : α),
  (Matrix.single i i c).diag = Pi.single i c
-- Init.Data.Array.Lemmas
Array.getElem_extract_loop_lt : ∀ {α : Type u_1} {i : ℕ} {xs ys : Array α} {size start : ℕ} (hlt : i < ys.size)
  (h : optParam (i < (Array.extract.loop xs size start ys).size) ⋯), (Array.extract.loop xs size start ys)[i] = ys[i]
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyMapIso'_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  (CategoryTheory.ShortComplex.leftHomologyMapIso' e h₁ h₂).inv =
    CategoryTheory.ShortComplex.leftHomologyMap' e.inv h₂ h₁
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.jointly_surjective₃' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  [CategoryTheory.IsCofiltered C] [CategoryTheory.InitiallySmall C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {cR : CategoryTheory.Limits.Cocone R} {hcR : CategoryTheory.Limits.IsColimit cR} {M : PresheafOfModules R}
  {cM : CategoryTheory.Limits.Cocone M.presheaf} {hcM : CategoryTheory.Limits.IsColimit cM} {M' : PresheafOfModules R}
  {cM' : CategoryTheory.Limits.Cocone M'.presheaf} {hcM' : CategoryTheory.Limits.IsColimit cM'} (r : ↑cR.pt)
  (m₁ : PresheafOfModules.ModuleColimit hcR hcM) (m₂ : PresheafOfModules.ModuleColimit hcR hcM'),
  ∃ U a x₁ x₂,
    (PresheafOfModules.ModuleColimit.ιR cR) a = r ∧
      PresheafOfModules.ModuleColimit.ιM x₁ = m₁ ∧ PresheafOfModules.ModuleColimit.ιM x₂ = m₂
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- A subalgebra is a sub(semi)ring that includes the range of `algebraMap`.  -/
Subalgebra : (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Type v
-- Mathlib.Order.Interval.Set.Monotone
MonotoneOn.Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  MonotoneOn f s → MonotoneOn (fun x => Set.Iio (f x)) s
-- Mathlib.Order.Filter.Map
Filter.pure_le_principal : ∀ {α : Type u_1} {s : Set α} (a : α), pure a ≤ Filter.principal s ↔ a ∈ s
-- Mathlib.Data.Fintype.Card
Bool.instWellFoundedGT : WellFoundedGT Bool