mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.ForEachExpr
_private.Lean.Meta.ForEachExpr.0.Lean.Meta.forEachExpr'.visit : {m : Type → Type} →
  [Monad m] →
    [MonadControlT Lean.MetaM m] →
      (Lean.Expr → m Bool) →
        (x : STWorld IO.RealWorld m) →
          MonadLiftT (ST IO.RealWorld) m → Lean.Expr → Lean.MonadCacheT Lean.Expr Unit m Unit
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
_private.Mathlib.Combinatorics.Enumerative.IncidenceAlgebra.0.IncidenceAlgebra.mu'_apply_self : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a : α), (IncidenceAlgebra.mu'✝ 𝕜) a a = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasProducts_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoproducts C],
  CategoryTheory.Limits.HasProducts Cᵒᵖ
-- Mathlib.RingTheory.Flat.CategoryTheory
Module.Flat.instPreservesFiniteLimitsModuleCatTensorRightOfCarrier : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) [Module.Flat R ↑M],
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.MonoidalCategory.tensorRight M)
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_real : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsFiniteMeasure μ] (x y : ℝ),
  ((ProbabilityTheory.covarianceBilin μ) x) y = x * y * ProbabilityTheory.variance id μ
-- Mathlib.MeasureTheory.Function.Egorov
/-- Given some `ε > 0`, `notConvergentSeqLTIndex` provides the index such that
`notConvergentSeq` (intersected with a set of finite measure) has measure less than
`ε * 2⁻¹ ^ n`.

This definition is useful for Egorov's theorem.  -/
MeasureTheory.Egorov.notConvergentSeqLTIndex : {α : Type u_1} →
  {β : Type u_2} →
    {ι : Type u_3} →
      {m : MeasurableSpace α} →
        [inst : PseudoEMetricSpace β] →
          {μ : MeasureTheory.Measure α} →
            {s : Set α} →
              {ε : ℝ} →
                {f : ι → α → β} →
                  {g : α → β} →
                    [inst_1 : SemilatticeSup ι] →
                      [Nonempty ι] →
                        [Countable ι] →
                          0 < ε →
                            (∀ (n : ι), Measurable fun a => edist (f n a) (g a)) →
                              MeasurableSet s →
                                μ s ≠ ⊤ →
                                  (∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
                                    ℕ → ι
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.succMany? (pref.length + 1) r.lower).get ⋯
-- Mathlib.Tactic.TacticAnalysis
/-- Code to run in the context of the tactic, for example an alternative tactic.  -/
Mathlib.TacticAnalysis.ComplexConfig.test : (self : Mathlib.TacticAnalysis.ComplexConfig) →
  Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → self.ctx → Lean.MVarId → Lean.Elab.Command.CommandElabM self.out
-- Lean.Meta.Match.MVarRenaming
Lean.Meta.MVarRenaming.map : Lean.Meta.MVarRenaming → Lean.MVarIdMap Lean.MVarId
-- Mathlib.GroupTheory.SemidirectProduct
/-- The canonical map `G →* N ⋊[φ] G` sending `g` to `⟨1, g⟩`  -/
SemidirectProduct.inr : {N : Type u_1} → {G : Type u_2} → [inst : Group N] → [inst_1 : Group G] → {φ : G →* MulAut N} → G →* N ⋊[φ] G
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.coe_sSup_apply' : ∀ {E : Type u_3} [inst : Group E] {s : Set (GroupSeminorm E)},
  BddAbove s → ∀ {x : E}, (sSup s) x = sSup ((fun x_1 => x_1 x) '' s)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.preimage_toSnowflaking_eball : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : Metric.Snowflaking X α hα₀ hα₁)
  (d : ENNReal),
  ⇑Metric.Snowflaking.toSnowflaking ⁻¹' Metric.eball x d = Metric.eball (Metric.Snowflaking.ofSnowflaking x) (d ^ α⁻¹)
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChangeAux.congr_simp : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (M : Type u_10) [inst_12 : AddCommGroup M] [inst_13 : Module R M]
  [inst_14 : Module A M] [inst_15 : IsScalarTower R A M],
  Algebra.IsPushout.cancelBaseChangeAux R S A B M = Algebra.IsPushout.cancelBaseChangeAux R S A B M
-- Mathlib.Data.List.Shortlex
/-- **Alias** of the reverse direction of `List.shortlex_cons_iff`. -/
List.Shortlex.cons : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] {a : α} {s t : List α},
  List.Shortlex r s t → List.Shortlex r (a :: s) (a :: t)
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- A function on the upper half plane that is given everywhere by a convergent `q`-expansion with
non-negative exponents, `f τ = ∑' m, c m * 𝕢 h τ ^ m`, is bounded at `i∞`. This is a converse to
`hasSum_qExpansion`: there, boundedness is a hypothesis used to produce the `q`-expansion, while
here convergence of the `q`-expansion is enough to deduce boundedness.  -/
UpperHalfPlane.isBoundedAtImInfty_of_hasSum_qExpansion : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ} {c : ℕ → ℂ},
  0 < h →
    (∀ (τ : UpperHalfPlane), HasSum (fun m => c m • Function.Periodic.qParam h ↑τ ^ m) (f τ)) →
      UpperHalfPlane.IsBoundedAtImInfty f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.neg_negPart_le : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  {a : A}, autoParam (IsSelfAdjoint a) CFC.neg_negPart_le._auto_1 → -a⁻ ≤ a
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.twoCocycle.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.Cohomology.twoCocycle R L M = (LieModule.Cohomology.d₂₃ R L M).ker
-- Mathlib.Analysis.Calculus.MeanValue
/-- The mean value theorem on a convex set: if the derivative of a function is bounded by `C`,
then the function is `C`-Lipschitz. Version with `fderiv`.  -/
Convex.norm_image_sub_le_of_norm_fderiv_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G} {C : ℝ} {s : Set E} {x y : E},
  (∀ x ∈ s, DifferentiableAt 𝕜 f x) →
    (∀ x ∈ s, ‖fderiv 𝕜 f x‖ ≤ C) → Convex ℝ s → x ∈ s → y ∈ s → ‖f y - f x‖ ≤ C * ‖y - x‖
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.applyPartition_eq_apply_toListModel : ∀ {α : Type u} {β : α → Type v} {δ : Type w} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α]
  [inst_3 : Std.LawfulBEqOrd α] {k : α} {l : Std.DTreeMap.Internal.Impl α β},
  l.Ordered →
    ∀
      {f :
        List ((a : α) × β a) →
          (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
            (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → List ((a : α) × β a) → δ}
      (g :
        (ll : List ((a : α) × β a)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → Std.Internal.List.containsKey k ll = true) → δ),
      (∀ {ll rr : List ((a : α) × β a)} {c : Std.DTreeMap.Internal.Cell α β (compare k)}
          {h₁ : Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true},
          List.Pairwise (fun a b => compare a.fst b.fst = Ordering.lt) (ll ++ c.inner.toList ++ rr) →
            (∀ p ∈ ll, compare k p.fst = Ordering.gt) →
              (∀ p ∈ rr, compare k p.fst = Ordering.lt) → f ll c h₁ rr = g (ll ++ c.inner.toList ++ rr) ⋯) →
        Std.DTreeMap.Internal.Impl.applyPartition (compare k) l f = g l.toListModel ⋯
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.InferControlInfo.ofSeq : Lean.DoSeq → Lean.Elab.TermElabM Lean.Elab.Do.ControlInfo
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Equivalence.mapCommMon_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D] (e : C ≌ D)
  [inst_6 : e.functor.Braided] [inst_7 : e.inverse.Braided] [inst_8 : e.IsMonoidal],
  e.mapCommMon.inverse = e.inverse.mapCommMon
-- Mathlib.Tactic.Order.Preprocessing
Mathlib.Tactic.Order.OrderType.lin.sizeOf_spec : sizeOf Mathlib.Tactic.Order.OrderType.lin = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.walkingCospanOpEquiv_inverse_obj : ∀ (X : CategoryTheory.Limits.WidePushoutShape CategoryTheory.Limits.WalkingPair),
  CategoryTheory.Limits.walkingCospanOpEquiv.inverse.obj X = Opposite.op X
-- Mathlib.Algebra.Symmetrized
SymAlg.instCommMagmaOfInvertibleOfNat : {α : Type u_1} → [inst : Ring α] → [Invertible 2] → CommMagma αˢʸᵐ
-- LeanSearchClient.Syntax
LeanSearchClient.instReprSearchResult : Repr LeanSearchClient.SearchResult
-- Init.Data.Nat.Basic
Nat.mul_left_comm : ∀ (n m k : ℕ), n * (m * k) = m * (n * k)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic.0.Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((m : ℕ) → motive m.succ) → motive n
-- Init.Data.UInt.Lemmas
UInt16.toFin_mod : ∀ (a b : UInt16), (a % b).toFin = a.toFin % b.toFin
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- The `p`-adic valuation on `ℚ` lifts to `PadicSeq p`.
`Valuation f` is defined to be the valuation of the (`ℚ`-valued) stationary point of `f`.  -/
PadicSeq.valuation : {p : ℕ} → [Fact (Nat.Prime p)] → PadicSeq p → ℤ
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.sum_incMatrix_apply_of_notMem_edgeSet : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : NonAssocSemiring R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {e : Sym2 α} [inst_3 : Fintype α],
  e ∉ G.edgeSet → ∑ a, SimpleGraph.incMatrix R G a e = 0
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.toOuterMeasure_top : ∀ {α : Type u_1} {x : MeasurableSpace α}, ⊤.toOuterMeasure = ⊤
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- The logarithmic counting function of a constant function is zero.
 -/
ValueDistribution.logCounting_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {c : E} {e : WithTop E},
  ValueDistribution.logCounting (fun x => c) e = 0
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.finset_logSizeBallSeq_subset_logSizeBallSeq_init : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T] (hJ : J.Nonempty)
  (i : ℕ), (PairReduction.logSizeBallSeq J hJ a c i).finset ⊆ J
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization : ∀ {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] {P : Ideal R} [inst_4 : P.IsPrime] [inst_5 : Algebra S T] [inst_6 : Algebra R T]
  [IsScalarTower R S T],
  IsLocalization (Algebra.algebraMapSubmonoid T (Algebra.algebraMapSubmonoid S P.primeCompl))
    (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coroot_eq_neg_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {i j : ι},
  P.coroot i = -P.coroot j ↔ i = (P.reflectionPerm j) j
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.commute_monodromyPerm_toPermFiber : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {g : G} {x : X}
  {γ : FundamentalGroup X x}, Commute ((⋯.monodromyPerm x) γ) ((hp.toPermFiber x) g)
-- Batteries.Data.UInt
UInt8.ext : ∀ {x y : UInt8}, x.toNat = y.toNat → x = y
-- Mathlib.Algebra.Group.Action.Pi
/-- Non-dependent version of `Pi.smulCommClass`. Lean gets confused by the dependent instance if
this is not present.  -/
Function.smulCommClass : ∀ {ι : Type u_1} {M : Type u_2} {N : Type u_3} {α : Type u_7} [inst : SMul M α] [inst_1 : SMul N α]
  [SMulCommClass M N α], SMulCommClass M N (ι → α)
-- Mathlib.CategoryTheory.Limits.Creates
/-- the isomorphism expressing that `liftedCone` lifts the given cone  -/
CategoryTheory.LiftableCone.validLift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                {c : CategoryTheory.Limits.Cone (K.comp F)} →
                  (self : CategoryTheory.LiftableCone K F c) → F.mapCone self.liftedCone ≅ c
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.size_eq_match_roc : ∀ {α : Type u} {r : Std.Roo α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α],
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some next => if next < r.upper then (next<...r.upper).size + 1 else 0
-- Mathlib.Tactic.Observe
/-- `observe hp : p` asserts the proposition `p` as a hypothesis named `hp`, and tries to prove it
using `exact?`.
If no proof is found, the tactic fails.
In other words, this tactic is equivalent to `have hp : p := by exact?`.

* `observe : p` uses the name `this` for the new hypothesis.
* `observe? hp : p` will emit a trace message of the form `have hp : p := proof_term`.
  This may be particularly useful to speed up proofs.
 -/
Mathlib.Tactic.LibrarySearch.observe : Lean.ParserDescr
-- Mathlib.Data.NNRat.Defs
NNRat.divNat_zero : ∀ (n : ℕ), NNRat.divNat n 0 = 0
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃.congr_simp : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  (D D_1 : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ),
  D = D_1 →
    ∀ (m₁ m₁_1 : J),
      m₁ = m₁_1 →
        CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃ D m₁ =
          CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₃ D_1 m₁_1
-- Mathlib.Topology.Constructions
continuousAt_codRestrict_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {t : Set Y}
  (h1 : ∀ (x : X), f x ∈ t) {x : X}, ContinuousAt (Set.codRestrict f t h1) x ↔ ContinuousAt f x
-- Mathlib.RingTheory.RingHomProperties
RingHom.CodescendsAlong.algebraMap_tensorProduct : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  (Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) (R S T : Type u)
  [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T],
  (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => P) fun {R S} [CommRing R] [CommRing S] => Q) →
    Q (algebraMap R S) → P (algebraMap S (TensorProduct R S T)) → P (algebraMap R T)
-- Mathlib.Data.Rel.Separated
SetRel.IsSeparated.empty : ∀ {X : Type u_1} {R : SetRel X X}, R.IsSeparated ∅
-- Mathlib.Algebra.Star.Basic
star_pow : ∀ {R : Type u} [inst : Monoid R] [inst_1 : StarMul R] (x : R) (n : ℕ), star (x ^ n) = star x ^ n
-- Std.Sat.CNF.Basic
Std.Sat.CNF.eval_empty : ∀ {α : Type u_1} (a : α → Bool), Std.Sat.CNF.eval a Std.Sat.CNF.empty = true
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
DiscreteMeasurableSpace.mk : ∀ {α : Type u_7} [inst : MeasurableSpace α], (∀ (s : Set α), MeasurableSet s) → DiscreteMeasurableSpace α
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_subset_Ioc_left : ∀ {α : Type u_2} {a₁ a₂ b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ ≤ a₂ → Finset.Ioc a₂ b ⊆ Finset.Ioc a₁ b
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- a bijection between the types of morphisms  -/
CategoryTheory.CoreSmallCategoryOfSet.homEquiv : {Ω : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (self : CategoryTheory.CoreSmallCategoryOfSet Ω C) →
        {X Y : ↑self.obj} → ↑(self.hom X Y) ≃ (self.objEquiv X ⟶ self.objEquiv Y)
-- Mathlib.Algebra.Algebra.Unitization
DistribMulActionHom.mk.congr_simp : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_10}
  [inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_11} [inst_4 : AddMonoid B]
  [inst_5 : DistribMulAction N B] (toMulActionHom toMulActionHom_1 : A →ₑ[⇑φ] B)
  (e_toMulActionHom : toMulActionHom = toMulActionHom_1) (map_zero' : toMulActionHom.toFun 0 = 0)
  (map_add' : ∀ (x y : A), toMulActionHom.toFun (x + y) = toMulActionHom.toFun x + toMulActionHom.toFun y),
  { toMulActionHom := toMulActionHom, map_zero' := map_zero', map_add' := map_add' } =
    { toMulActionHom := toMulActionHom_1, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
/-- The `SubAddAction` generated by a set `s`.  -/
SubAddAction.closure : (R : Type u_1) → {M : Type u_2} → [inst : VAdd R M] → Set M → SubAddAction R M
-- Mathlib.Order.SuccPred.Archimedean
Set.OrdConnected.isSuccArchimedean : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (s : Set α)
  [inst_3 : s.OrdConnected], IsSuccArchimedean ↑s
-- Lean.Parser.Term
Lean.Parser.Term.falseVal.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.takeWhile_char_eq_takeWhile_beq : ∀ {c : Char} {s : String.Slice}, s.takeWhile c = s.takeWhile fun x => x == c
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_affine_Ico : ∀ {K : Type u_2} [inst : DivisionSemiring K] [inst_1 : PartialOrder K] [PosMulReflectLT K] [IsOrderedCancelAddMonoid K]
  [ExistsAddOfLE K] {a : K},
  0 < a → ∀ (b c d : K), (fun x => a * x + b) '' Set.Ico c d = Set.Ico (a * c + b) (a * d + b)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.Char.toNat_le : ∀ {c : Char}, c.toNat ≤ 1114111
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : β → β}, (m.modify k f).contains k' = m.contains k'
-- Mathlib.RingTheory.Spectrum.Prime.Topology
Algebra.IsIntegral.comap_surjective : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] [FaithfulSMul R S], Function.Surjective (PrimeSpectrum.comap (algebraMap R S))
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerRight_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {G H K : CategoryTheory.Functor C D} (α : G ⟶ H)
  (β : H ⟶ K) (F : CategoryTheory.Functor D E),
  CategoryTheory.Functor.whiskerRight (CategoryTheory.CategoryStruct.comp α β) F =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α F)
      (CategoryTheory.Functor.whiskerRight β F)
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.remaining : Lean.Meta.MatcherApp → Array Lean.Expr
-- Mathlib.Algebra.Group.Units.Defs
inv_eq_one_divp : ∀ {α : Type u} [inst : Monoid α] (u : αˣ), ↑u⁻¹ = 1 /ₚ u
-- Mathlib.Data.PNat.Xgcd
/-- `y` satisfies `b / d = z + y` at the final step.  -/
PNat.XgcdType.y : PNat.XgcdType → ℕ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.coe_projKerOfRightInverse_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Ring R₁] [inst_1 : Ring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] {M₁ : Type u_4} {M₂ : Type u_5} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : Module R₁ M₁] [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommGroup M₂]
  [inst_8 : Module R₂ M₂] [inst_9 : IsTopologicalAddGroup M₁] (f₁ : M₁ →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M₁)
  (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : M₁), ↑((f₁.projKerOfRightInverse f₂ h) x) = x - f₂ (f₁ x)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.toUniformSpace : {α : Type u} → [self : PseudoMetricSpace α] → UniformSpace α
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- We redeclare this instance to get keys
`SMul (@Subtype (MulOpposite _) (@Membership.mem (MulOpposite _)
  (Subgroup (MulOpposite _) _) _ (@Subgroup.op _ _ _))) _`
compared to the keys for `Submonoid.smul`
`SMul (@Subtype _ (@Membership.mem _ (Submonoid _ _) _ _)) _`  -/
Subgroup.instSMul : {G : Type u_2} → [inst : Group G] → (H : Subgroup G) → SMul (↥H.op) G
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.C_apply : ∀ {R : Type u_1} [inst : Semiring R] (t : R) (n : ℤ), (LaurentPolynomial.C t).coeff n = if n = 0 then t else 0
-- Mathlib.CategoryTheory.SmallObject.Basic
/-- If `I : MorphismProperty C` permits the small object argument,
then the class of morphisms that have the left lifting property with respect to
the maps that have the right lifting property with respect to `I` are
exactly the retracts of transfinite compositions (indexed by `I.smallObjectκ.ord.ToType`)
of pushouts of coproducts of morphisms in `C`.  -/
CategoryTheory.MorphismProperty.llp_rlp_of_hasSmallObjectArgument' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C)
  [inst_1 : I.HasSmallObjectArgument],
  I.rlp.llp =
    ((CategoryTheory.MorphismProperty.coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape
        I.smallObjectκ.ord.ToType).retracts
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.mulEquivOfLocalizations_right_inv : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (k : S.LocalizationMap P),
  f.ofMulEquivOfLocalizations (f.mulEquivOfLocalizations k) = k
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.hom_ext_of_isLeftKanExtension : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [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]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [F'.IsLeftKanExtension α] {G : CategoryTheory.Functor D H} (γ₁ γ₂ : F' ⟶ G),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft γ₁) = CategoryTheory.CategoryStruct.comp α (L.whiskerLeft γ₂) →
    γ₁ = γ₂