mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type t}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{r, w} J] (F : CategoryTheory.Functor J C) {D : CategoryTheory.Limits.Cocone F}
  {i j : J} (x : CategoryTheory.ToType (F.obj i)) (y : CategoryTheory.ToType (F.obj j)),
  (∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map g)) y) →
    (CategoryTheory.ConcreteCategory.hom (D.ι.app i)) x = (CategoryTheory.ConcreteCategory.hom (D.ι.app j)) y
-- Mathlib.Analysis.Normed.Group.Uniform
SeparationQuotient.instNormedAddCommGroup : {E : Type u_2} → [inst : SeminormedAddCommGroup E] → NormedAddCommGroup (SeparationQuotient E)
-- Mathlib.NumberTheory.Real.Irrational
Nat.not_irrational : ∀ (m : ℕ), ¬Irrational ↑m
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.mk.inj : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {X Y : F.CoGrothendieck}
  {base : X.base ⟶ Y.base} {fiber : X.fiber ⟶ (F.map base.op.toLoc).toFunctor.obj Y.fiber} {base_1 : X.base ⟶ Y.base}
  {fiber_1 : X.fiber ⟶ (F.map base_1.op.toLoc).toFunctor.obj Y.fiber},
  { base := base, fiber := fiber } = { base := base_1, fiber := fiber_1 } → base = base_1 ∧ fiber ≍ fiber_1
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_0 : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) {X Y : A} (f : X ⟶ Y) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  (Λ.chainComplexMap f).f 0 =
    CategoryTheory.CategoryStruct.comp (Λ.chainComplexXZeroIso X).hom
      (CategoryTheory.CategoryStruct.comp (Λ.F.map f) (Λ.chainComplexXZeroIso Y).inv)
-- Mathlib.Algebra.Lie.Solvable
/-- The (solvable) radical of Lie algebra is the `sSup` of all solvable ideals.  -/
LieAlgebra.radical : (R : Type u) → (L : Type v) → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → LieIdeal R L
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} [inst : Inhabited β] {f : β → β},
  Std.DHashMap.Const.get! (Std.DHashMap.Const.modify m k f) k = (Option.map f (Std.DHashMap.Const.get? m k)).get!
-- Mathlib.RingTheory.Flat.CategoryTheory
Module.Flat.iff_preservesFiniteLimits_tensorLeft : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R),
  Module.Flat R ↑M ↔ CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorLeft M)
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- Every fractional ideal of a Noetherian integral domain is Noetherian.  -/
FractionalIdeal.isNoetherian : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K] [IsFractionRing R₁ K]
  [IsDomain R₁] [IsNoetherianRing R₁] (I : FractionalIdeal (nonZeroDivisors R₁) K), IsNoetherian R₁ ↥↑I
-- Mathlib.Data.Int.WithZero
/-- The map `toNNReal` is strictly monotone whenever `1 < e`.  -/
WithZeroMulInt.toNNReal_strictMono : ∀ {e : NNReal} (he : 1 < e), StrictMono ⇑(WithZeroMulInt.toNNReal ⋯)
-- Mathlib.Data.Vector.Defs
/-- Mapping two vectors under a curried function of two variables.  -/
List.Vector.map₂ : {α : Type u_1} →
  {β : Type u_2} → {φ : Type u_4} → {n : ℕ} → (α → β → φ) → List.Vector α n → List.Vector β n → List.Vector φ n
-- Mathlib.Order.CompleteBooleanAlgebra
sInf_sup_sInf : ∀ {α : Type u} [inst : Order.Coframe α] {s t : Set α}, sInf s ⊔ sInf t = ⨅ p ∈ s ×ˢ t, p.1 ⊔ p.2
-- Mathlib.CategoryTheory.Shift.Opposite
/-- The adjunction `adj`, seen as an adjunction between `OppositeShift.functor G`
and `OppositeShift.functor F`.
 -/
CategoryTheory.OppositeShift.adjunction : {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] →
        (A : Type u_3) →
          [inst_2 : AddMonoid A] →
            [inst_3 : CategoryTheory.HasShift C A] →
              [inst_4 : CategoryTheory.HasShift D A] →
                {F : CategoryTheory.Functor C D} →
                  {G : CategoryTheory.Functor D C} →
                    (F ⊣ G) → (CategoryTheory.OppositeShift.functor A G ⊣ CategoryTheory.OppositeShift.functor A F)
-- Mathlib.Data.Set.NAry
Set.image2_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s : Set α} {t : Set β},
  Set.image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.GroupWithZero.Action.Units
Units.instSMulZeroClass : {M : Type u_3} → {α : Type u_4} → [inst : Monoid M] → [inst_1 : Zero α] → [SMulZeroClass M α] → SMulZeroClass Mˣ α
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.nilradical_eq_iInf : ∀ (R : Type u_1) [inst : CommRing R] [IsArtinianRing R], nilradical R = iInf MaximalSpectrum.asIdeal
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionLiteralSupportValueSet.mk : Array Lean.Lsp.CodeActionKind → Lean.Lsp.CodeActionLiteralSupportValueSet
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_mul_apply : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : NonAssocSemiring α] (f : l ≃. m) (i : l) (j : n) (M : Matrix m n α),
  (f.toMatrix * M) i j = Option.casesOn (f i) 0 fun fi => M fi j
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The `ℤ`-basis of the lattice determined by a pair of periods.  -/
PeriodPair.latticeBasis : (L : PeriodPair) → Module.Basis (Fin 2) ℤ ↥L.lattice
-- Mathlib.RingTheory.Flat.Rank
/-- The rank of a ring homomorphism `f : R →+* S` at a prime `x` of `R` is the rank of
`S` as an `R`-module at the stalk of `x`.  -/
RingHom.finrank : {R : Type u_3} → {S : Type u_4} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → PrimeSpectrum R → ℕ
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `FaithfulVAdd` across an `Equiv`

See `FaithfulVAdd.of_injective` for the general statement not about transferring.  -/
Equiv.faithfulVAdd : ∀ (M : Type u_1) {α : Type u_4} {β : Type u_5} [inst : VAdd M β] (e : α ≃ β) [FaithfulVAdd M β], FaithfulVAdd M α
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.pointwiseLeftKanExtensionCompIsoOfPreserves_hom_fac : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [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]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesPointwiseLeftKanExtension F L]
  [inst_5 : L.HasPointwiseLeftKanExtension F],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (L.pointwiseLeftKanExtensionUnit F) G)
      (CategoryTheory.CategoryStruct.comp (L.associator (L.pointwiseLeftKanExtension F) G).hom
        (L.whiskerLeft (G.pointwiseLeftKanExtensionCompIsoOfPreserves F L).hom)) =
    L.pointwiseLeftKanExtensionUnit (F.comp G)
-- Mathlib.Combinatorics.SimpleGraph.Prod
_private.Mathlib.Combinatorics.SimpleGraph.Prod.0.SimpleGraph.sum.match_1.eq_3 : ∀ {V : Type u_1} {W : Type u_2} (motive : V ⊕ W → V ⊕ W → Sort u_3) (x x_1 : V ⊕ W)
  (h_1 : (u v : V) → motive (Sum.inl u) (Sum.inl v)) (h_2 : (u v : W) → motive (Sum.inr u) (Sum.inr v))
  (h_3 : (x x_2 : V ⊕ W) → motive x x_2),
  (∀ (u v : V), x = Sum.inl u → x_1 = Sum.inl v → False) →
    (∀ (u v : W), x = Sum.inr u → x_1 = Sum.inr v → False) →
      (match x, x_1 with
        | Sum.inl u, Sum.inl v => h_1 u v
        | Sum.inr u, Sum.inr v => h_2 u v
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.Logic.Equiv.Fin.Basic
finSumFinEquiv_apply_left : ∀ {m n : ℕ} (i : Fin m), finSumFinEquiv (Sum.inl i) = Fin.castAdd n i
-- Mathlib.Algebra.Group.UniqueProds.Basic
Prod.instUniqueProds : ∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] [UniqueProds G] [UniqueProds H], UniqueProds (G × H)
-- Mathlib.Algebra.Category.Grp.Basic
/-- An alias for `AddGrpCat.{max u v}`, to deal around unification issues.  -/
GrpMaxAux : Type ((max u1 u2) + 1)
-- Mathlib.Data.ENNReal.Basic
ENNReal.not_top_le_coe : ∀ {r : NNReal}, ¬⊤ ≤ ↑r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α} {v : β k}, (cmp (t.insertIfNew k v).minKey! k).isLE = true
-- Mathlib.Algebra.GroupWithZero.Action.Units
Units.instDistribSMulUnits : {M : Type u_3} → {α : Type u_4} → [inst : Monoid M] → [inst_1 : AddZeroClass α] → [DistribSMul M α] → DistribSMul Mˣ α
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.mapsTo : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → Set.MapsTo (↑e) (e.source ∩ s) (e.target ∩ t)
-- Mathlib.Analysis.RCLike.Basic
/-- The priority must be set at 900 to ensure that coercions are tried in the right order.
See Note [coercion into rings], or `Mathlib/Data/Nat/Cast/Basic.lean` for more details.  -/
RCLike.algebraMapCoe : {K : Type u_1} → [RCLike K] → CoeTC ℝ K
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape_snd : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) (j : data.I₁'),
  data.multicospanShape.snd j = j.fst.2
-- Init.Data.String.TakeDrop
String.Slice.trimLeft : String.Slice → String.Slice
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ContinuousWithinAt.extChartAt_symm_preimage_inter_range_eventuallyEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} {E' : Type u_5} {M' : Type u_6} {H' : Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M] {I : ModelWithCorners 𝕜 E H}
  [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] [inst_7 : TopologicalSpace H']
  [inst_8 : TopologicalSpace M'] {I' : ModelWithCorners 𝕜 E' H'} {s : Set M} [inst_9 : ChartedSpace H M]
  [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M},
  ContinuousWithinAt f s x →
    ↑(extChartAt I x).symm ⁻¹' s ∩ Set.range ↑I =ᶠ[nhds (↑(extChartAt I x) x)]
      (extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' (f x)).source)
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.Ioo_ae_eq_Ico : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, Set.Ioo a b =ᵐ[μ] Set.Ico a b
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendSingleIso_inv_f_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : DecidableEq ι] (e : c.Embedding c') (X : C)
  [inst_4 : DecidableEq ι'] (i : ι) (i' : ι') (h : e.f i = i') {Z : C}
  (h_1 : (((HomologicalComplex.single C c i).obj X).extend e).X i' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((HomologicalComplex.extendSingleIso e X i i' h).inv.f i') h_1 =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c' i' X).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c i X).inv
        (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c i).obj X).extendXIso e h).inv h_1))
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.sum_pi_single'`.  -/
Fintype.sum_pi_single' : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι) (a : M),
  ∑ j, Pi.single i a j = a
-- Mathlib.Order.Atoms
isStronglyCoatomic_dual_iff_is_stronglyAtomic : ∀ {α : Type u_4} [inst : Preorder α], IsStronglyCoatomic αᵒᵈ ↔ IsStronglyAtomic α
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.app_idem : ∀ {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] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C))
  (X : J), CategoryTheory.CategoryStruct.comp (P.p.app X) (P.p.app X) = P.p.app X
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCancelMonoidOfAddOpposite : {M : Type u_1} → [AddCancelMonoid Mᵃᵒᵖ] → AddCancelMonoid Mᵈᵃᵃ
-- Mathlib.Analysis.Seminorm
Seminorm.coe_sSup_eq : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set (Seminorm 𝕜 E)}, BddAbove s → ⇑(sSup s) = ⨆ p, ⇑↑p
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.xa_pow_four : ∀ {n : ℕ} (i : ZMod (2 * n)), QuaternionGroup.xa i ^ 4 = 1
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.MatchResult.covered.injEq : ∀ (f : Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Elab.Term.Quotation.Alt) (exhaustive : Bool)
  (f_1 : Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM Lean.Elab.Term.Quotation.Alt) (exhaustive_1 : Bool),
  (Lean.Elab.Term.Quotation.MatchResult.covered f exhaustive =
      Lean.Elab.Term.Quotation.MatchResult.covered f_1 exhaustive_1) =
    (f = f_1 ∧ exhaustive = exhaustive_1)
-- Aesop.Percent
Aesop.Percent : Type
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.abs_le_right_of_norm : ∀ (m n : ℤ), ↑|m| ≤ ‖![n, m]‖
-- Mathlib.Probability.Moments.SubGaussian
_private.Mathlib.Probability.Moments.SubGaussian.0.ProbabilityTheory.HasSubgaussianMGF.sum_of_iIndepFun_of_forall_aemeasurable : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ},
  ProbabilityTheory.iIndepFun X μ →
    ∀ {c : ι → NNReal},
      (∀ (i : ι), AEMeasurable (X i) μ) →
        ∀ {s : Finset ι},
          (∀ i ∈ s, ProbabilityTheory.HasSubgaussianMGF (X i) (c i) μ) →
            ProbabilityTheory.HasSubgaussianMGF (fun ω => ∑ i ∈ s, X i ω) (∑ i ∈ s, c i) μ
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_mk : ∀ (n : ℕ), { byteIdx := n }.byteIdx = n
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapWithPostcondition_mapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [inst_7 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n γ} {g : γ → Std.Iterators.PostconditionT o δ}
  {it : Std.IterM m β},
  (Std.IterM.mapWithPostcondition g (Std.IterM.mapWithPostcondition f it)).toListRev =
    (Std.IterM.mapWithPostcondition (fun x => liftM (f x) >>= g) it).toListRev
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.of.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M],
  Algebra.GrothendieckAddGroup.of = (AddLocalization.addMonoidOf ⊤).toAddMonoidHom
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- This is the reverse direction of the equivalence we're constructing.  -/
CategoryTheory.OverPresheafAux.costructuredArrowPresheafToOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      CategoryTheory.Functor
        (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
        (CategoryTheory.Over A)
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.State.mk.sizeOf_spec : ∀ (items : Array Lean.Lsp.ResolvableCompletionItem), sizeOf { items := items } = 1 + sizeOf items
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.continuous_norm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], Continuous ⇑NumberField.mixedEmbedding.norm
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_mem_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α} {a b : α}, a ∈ s → b ∈ t → a - b ∈ s - t
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMap_comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorObjLeft f πX)
      (CategoryTheory.SmallObject.functorMapTgt f τ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMapSrc f τ)
      (CategoryTheory.SmallObject.functorObjLeft f πY)
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasLeftInverse.isClosed_range : ∀ {R : Type u_7} {E : Type u_8} {F : Type u_10} [inst : Ring R] [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommGroup F] [inst_6 : Module R F] {f : E →L[R] F}
  [T1Space F], f.HasLeftInverse → ∀ [IsTopologicalAddGroup F], IsClosed (Set.range ⇑f)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.le_eRk_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {n : ℕ∞}, n ≤ M.eRk X ↔ ∃ I ⊆ X, M.Indep I ∧ I.encard = n
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.WhiskerLeft.brecOn.eq : ∀ {motive : Mathlib.Tactic.BicategoryLike.WhiskerLeft → Sort u} (t : Mathlib.Tactic.BicategoryLike.WhiskerLeft)
  (F_1 :
    (t : Mathlib.Tactic.BicategoryLike.WhiskerLeft) → Mathlib.Tactic.BicategoryLike.WhiskerLeft.below t → motive t),
  Mathlib.Tactic.BicategoryLike.WhiskerLeft.brecOn t F_1 =
    F_1 t (Mathlib.Tactic.BicategoryLike.WhiskerLeft.brecOn.go t F_1).2
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- The Gelfand transform is spectrum-preserving.  -/
spectrum.gelfandTransform_eq : ∀ {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] (a : A),
  spectrum ℂ ((WeakDual.gelfandTransform ℂ A) a) = spectrum ℂ a
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.instBEqSimpKind : BEq Lean.Elab.Tactic.SimpKind
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.eq_1 : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} (s1 s2 : Set (Set Ω))
  (κ : ProbabilityTheory.Kernel α Ω) (μ : MeasureTheory.Measure α),
  ProbabilityTheory.Kernel.IndepSets s1 s2 κ μ =
    ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
-- Mathlib.Topology.Homeomorph.Lemmas
/-- The codomain of a homeomorphism is a locally compact space if and only if
the domain is a locally compact space.  -/
Homeomorph.locallyCompactSpace_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  LocallyCompactSpace X ↔ LocallyCompactSpace Y
-- Init.Data.Fin.Lemmas
Fin.induction_succ : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} (zero : motive 0) (succ : (i : Fin n) → motive i.castSucc → motive i.succ)
  (i : Fin n), Fin.induction zero succ i.succ = succ i (Fin.induction zero succ i.castSucc)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map_id_comp_H0Iso_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B : Rep.{u, u, u} k G} (f : A ⟶ B) {Z : ModuleCat k}
  (h : (Rep.coinvariantsFunctor k G).obj B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.map (MonoidHom.id G) f 0)
      (CategoryTheory.CategoryStruct.comp (groupHomology.H0Iso B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.H0Iso A).hom
      (CategoryTheory.CategoryStruct.comp ((Rep.coinvariantsFunctor k G).map f) h)
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The functor `(Φ.LeftResolution X₂)ᵒᵖ ⥤ Φ.op.RightResolution (Opposite.op X₂)`.  -/
CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              (X₂ : C₂) → CategoryTheory.Functor (Φ.LeftResolution X₂)ᵒᵖ (Φ.op.RightResolution (Opposite.op X₂))
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_lt_top_of_ae_enorm_bound : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε}
  {C : NNReal}, (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ ↑C) → MeasureTheory.eLpNormEssSup f μ < ⊤
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instSub : {R : Type u} → [inst : Ring R] → Sub (Polynomial R)
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ιOfLE_η : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C}
  [inst_3 : P'.IsMonoidal] (h : P ≤ P'),
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.ObjectProperty.ιOfLE h) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.ObjectProperty.ιOfLE h).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit P.FullSubcategory))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
/-- A version of `Commute.cfc` or `IsSelfAdjoint.commute_cfc` which does not require any interaction
with `star` when the base ring is `ℝ≥0`.  -/
Commute.cfc_nnreal : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : Algebra ℝ A] [inst_3 : TopologicalSpace A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [IsTopologicalRing A] [T2Space A] [inst_7 : PartialOrder A]
  [inst_8 : NonnegSpectrumClass ℝ A] [inst_9 : StarOrderedRing A] {a b : A},
  Commute a b → ∀ (f : NNReal → NNReal), Commute (cfc f a) b
-- Qq.SortLocalDecls
Qq.SortLocalDecls.State.mk : Lean.NameSet → Array Lean.LocalDecl → Qq.SortLocalDecls.State
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.mk'_carrier : ∀ {α : Type u_1} [inst : CompleteLattice α] (carrier : Set α)
  (sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier)
  (sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier),
  (CompleteSublattice.mk' carrier sSupClosed' sInfClosed').carrier = carrier
-- Mathlib.Topology.Order.OrderClosed
frontier_le_subset_eq : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f g : β → α}
  [inst_3 : TopologicalSpace β], Continuous f → Continuous g → frontier {b | f b ≤ g b} ⊆ {b | f b = g b}
-- Std.Time.DateTime
/-- Subtract `Year.Offset` from a `DateTime`, rolling over excess days.
 -/
Std.Time.DateTime.subYearsRollOver : Std.Time.DateTime → Std.Time.Year.Offset → Std.Time.DateTime
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace.eq_1 : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R), f.genEigenspace μ = { toFun := fun k => ⨆ l, ⨆ (_ : ↑l ≤ k), ((f - μ • 1) ^ l).ker, monotone' := ⋯ }