mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Instances
/-- `(M →+ N)` is an `AddCommMonoid` if `N` is commutative.  -/
AddMonoidHom.instAddCommMonoid : {M : Type uM} → {N : Type uN} → [inst : AddZeroClass M] → [inst_1 : AddCommMonoid N] → AddCommMonoid (M →+ N)
-- Mathlib.Algebra.Notation.Indicator
Set.comp_indicator : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] (h : M → β) (f : α → M) {s : Set α} {x : α}
  [inst_1 : DecidablePred fun x => x ∈ s], h (s.indicator f x) = s.piecewise (h ∘ f) (Function.const α (h 0)) x
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.pderiv_inr_universalFactorizationMap_X : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin k) (j : Fin n),
  (MvPolynomial.pderiv (Sum.inr i))
      ((MvPolynomial.tensorEquivSum R (Fin m) (Fin k) R)
        ((MvPolynomial.universalFactorizationMap R n m k hn) (MvPolynomial.X j))) =
    if ↑j < ↑i then 0
    else if h : ↑j - ↑i < m then MvPolynomial.X (Sum.inl ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = m then 1 else 0
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
/-- Scalar multiplication by `𝕜` on `WeakBilin B` is continuous.  -/
WeakBilin.instContinuousSMul : ∀ {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [inst : TopologicalSpace 𝕜] [inst_1 : CommSemiring 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [ContinuousSMul 𝕜 𝕜], ContinuousSMul 𝕜 (WeakBilin B)
-- Lean.Meta.Tactic.Generalize
Lean.Meta.GeneralizeArg.mk.inj : ∀ {expr : Lean.Expr} {xName? hName? : Option Lean.Name} {expr_1 : Lean.Expr} {xName?_1 hName?_1 : Option Lean.Name},
  { expr := expr, xName? := xName?, hName? := hName? } = { expr := expr_1, xName? := xName?_1, hName? := hName?_1 } →
    expr = expr_1 ∧ xName? = xName?_1 ∧ hName? = hName?_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLimitConeOfIsRightKanExtension_lift : ∀ {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}
  (α : L.comp F' ⟶ F) [inst_3 : F'.IsRightKanExtension α] {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsLimit c) (s : CategoryTheory.Limits.Cone F'),
  (F'.isLimitConeOfIsRightKanExtension α hc).lift s =
    hc.lift { pt := s.1, π := CategoryTheory.CategoryStruct.comp (L.whiskerLeft s.π) α }
-- Init.Data.Slice.Notation
/-- Slices `carrier` from `range.lower` \(inclusive\) to `range.upper` \(exclusive\).
   -/
Std.Rco.Sliceable.mkSlice : {α : Type u} → {β : outParam (Type v)} → {γ : outParam (Type w)} → [self : Std.Rco.Sliceable α β γ] → α → Std.Rco β → γ
-- Mathlib.CategoryTheory.Limits.Creates
/-- The lifted cone has an image isomorphic to the original cone.  -/
CategoryTheory.liftedLimitMapsToOriginal : {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} →
                [inst_3 : CategoryTheory.CreatesLimit K F] →
                  {c : CategoryTheory.Limits.Cone (K.comp F)} →
                    (t : CategoryTheory.Limits.IsLimit c) → F.mapCone (CategoryTheory.liftLimit t) ≅ c
-- Std.Sync.Mutex
/-- Creates a new condition variable.  -/
Std.Condvar.new : BaseIO Std.Condvar
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
self_le_add_left : ∀ {α : Type u} [inst : Add α] [inst_1 : LE α] [CanonicallyOrderedAdd α] (a b : α), a ≤ b + a
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- A Mahler series whose coefficients tend to 0 is convergent.  -/
PadicInt.hasSum_mahlerSeries : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [inst_3 : IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E},
  Filter.Tendsto a Filter.atTop (nhds 0) → HasSum (fun n => PadicInt.mahlerTerm (a n) n) (PadicInt.mahlerSeries a)
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The second theorem that characterises the function `reduce`: the maximal reduction of a word
only reduces to itself.  -/
FreeGroup.reduce.min : ∀ {α : Type u_1} {L₁ L₂ : List (α × Bool)} [inst : DecidableEq α],
  FreeGroup.Red (FreeGroup.reduce L₁) L₂ → FreeGroup.reduce L₁ = L₂
-- Lean.Level
_private.Lean.Level.0.Lean.Level.isIMax.match_1.splitter : (motive : Lean.Level → Sort u_1) →
  (x : Lean.Level) →
    ((a a_1 : Lean.Level) → motive (a.imax a_1)) →
      ((x : Lean.Level) → (∀ (a a_1 : Lean.Level), x = a.imax a_1 → False) → motive x) → motive x
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.rIso_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {adj₁ adj₂ : a ⟶ b}
  (e : adj₁ ≅ adj₂), (CategoryTheory.Bicategory.Adj.rIso e).hom = e.inv.τr
-- Mathlib.Algebra.Group.Defs
sub_add_cancel : ∀ {G : Type u_1} [inst : AddGroup G] (a b : G), a - b + b = a
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
IsTranscendenceBasis.of_comp_algebraMap : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {A' : Type v'} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : CommRing A'] [inst_3 : Algebra R A] [inst_4 : Algebra R A'] [inst_5 : Algebra A A'] [IsScalarTower R A A']
  [FaithfulSMul A A'] {x : ι → A}, IsTranscendenceBasis R (⇑(algebraMap A A') ∘ x) → IsTranscendenceBasis R x
-- Mathlib.Topology.Category.Profinite.AsLimit
Profinite.isIso_asLimitCone_lift : ∀ (X : Profinite), CategoryTheory.IsIso ((Profinite.limitConeIsLimit X.diagram).lift X.asLimitCone)
-- Mathlib.Tactic.FunProp.Decl
/-- Discrimination tree for function properties.  -/
Mathlib.Meta.FunProp.FunPropDecls.decls : Mathlib.Meta.FunProp.FunPropDecls → Lean.Meta.DiscrTree Mathlib.Meta.FunProp.FunPropDecl
-- Mathlib.LinearAlgebra.Ray
/-- An equivalence between modules implies an equivalence between rays.  -/
Module.Ray.map : {R : Type u_1} →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} →
          [inst_3 : AddCommMonoid M] →
            [inst_4 : Module R M] →
              {N : Type u_3} →
                [inst_5 : AddCommMonoid N] → [inst_6 : Module R N] → (M ≃ₗ[R] N) → Module.Ray R M ≃ Module.Ray R N
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneRightOpOfCocone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cocone F),
  CategoryTheory.Limits.coneRightOpOfCocone c = { pt := Opposite.op c.pt, π := CategoryTheory.NatTrans.rightOp c.ι }
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurePreserving.aemeasurable_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μa : MeasureTheory.Measure α} {μb : MeasureTheory.Measure β} {f : α → β},
  MeasureTheory.MeasurePreserving f μa μb →
    MeasurableEmbedding f → ∀ {g : β → γ}, AEMeasurable (g ∘ f) μa ↔ AEMeasurable g μb
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Sheaf.interUnionPullbackConeLift_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X)
  (s :
    CategoryTheory.Limits.PullbackCone (F.obj.map (CategoryTheory.homOfLE ⋯).op)
      (F.obj.map (CategoryTheory.homOfLE ⋯).op)),
  CategoryTheory.CategoryStruct.comp (F.interUnionPullbackConeLift U V s) (F.obj.map (CategoryTheory.homOfLE ⋯).op) =
    s.snd
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose_one_right : ∀ (n : ℕ), n.multichoose 1 = n
-- Init.Data.List.Lemmas
List.contains_filterMap : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {l : List α} {x : β} {f : α → Option β},
  (List.filterMap f l).contains x = l.any fun a => Option.any (fun b => x == b) (f a)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.instInhabitedStep : Inhabited Lean.Meta.Simp.Step
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.SPolResult.mk.sizeOf_spec : ∀ (spol : Lean.Grind.CommRing.Poly) (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon),
  sizeOf { spol := spol, k₁ := k₁, m₁ := m₁, k₂ := k₂, m₂ := m₂ } =
    1 + sizeOf spol + sizeOf k₁ + sizeOf m₁ + sizeOf k₂ + sizeOf m₂
-- Mathlib.Analysis.Complex.CauchyIntegral
Complex.analyticOn_univ_iff_differentiable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E},
  AnalyticOn ℂ f Set.univ ↔ Differentiable ℂ f
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.tuple.sizeOf_spec : ∀ (ref : Lean.Syntax) (a : List Lean.Elab.Tactic.RCases.RCasesPatt),
  sizeOf (Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref a) = 1 + sizeOf ref + sizeOf a
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioc.instCancelCommMonoid : {R : Type u_2} →
  [inst : CommRing R] →
    [inst_1 : PartialOrder R] → [IsStrictOrderedRing R] → [IsDomain R] → CancelCommMonoid ↑(Set.Ioc 0 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.iso_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} (self : I.SymmStruct)
  (i j : ι) {Z : C} (h : I.right ((CategoryTheory.Limits.MultispanShape.prod ι).fst (j, i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.iso i j).hom (CategoryTheory.CategoryStruct.comp (I.fst (j, i)) h) =
    CategoryTheory.CategoryStruct.comp (I.snd (i, j)) h
-- Mathlib.Analysis.Normed.Field.Instances
NormedField.instCompletableTopField : ∀ {F : Type u_1} [inst : NormedField F], CompletableTopField F
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.elab : Lean.Syntax → Aesop.ElabM Aesop.Frontend.Feature
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.labelGraph_adj : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} {C : G.EdgeLabeling K} {k : K} (x y : V),
  (C.labelGraph k).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k
-- Lean.Server.References
/-- References from workers, overriding the corresponding ilean files  -/
Lean.Server.References.workers : Lean.Server.References → Lean.Server.WorkerRefMap
-- Init.Data.Option.Lemmas
Option.all_eq_false_iff_get : ∀ {α : Type u_1} (p : α → Bool) (x : Option α), Option.all p x = false ↔ ∃ (h : x.isSome = true), p (x.get h) = false
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C]
  (sieves : (X : C) → Set (CategoryTheory.Sieve X)) (top_mem' : ∀ (X : C), ⊤ ∈ sieves X)
  (pullback_stable' :
    ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X), S ∈ sieves X → CategoryTheory.Sieve.pullback f S ∈ sieves Y)
  (transitive' :
    ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
      S ∈ sieves X →
        ∀ (R : CategoryTheory.Sieve X),
          (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X),
  sizeOf { sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' } =
    1
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_natGeneratingSequence : ∀ (α : Type u_3) [m : MeasurableSpace α] [inst : MeasurableSpace.CountablyGenerated α],
  MeasurableSpace.generateFrom (Set.range (MeasurableSpace.natGeneratingSequence α)) = m
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalars.smul_def : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) {M : ModuleCat S} (r : R)
  (m : ↑((ModuleCat.restrictScalars f).obj M)),
  r • m =
    f r •
      have this := m;
      this
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Ψ_two : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ 2 = W.ψ₂
-- Init.Data.UInt.Bitwise
UInt32.ofBitVec_shiftLeft : ∀ (a : BitVec 32), ∀ b < 32, { toBitVec := a <<< b } = { toBitVec := a } <<< UInt32.ofNat b
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C}
  (toPreZeroHypercover : CategoryTheory.PreZeroHypercover S)
  (I₁ : toPreZeroHypercover.I₀ → toPreZeroHypercover.I₀ → Type w) (Y : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → I₁ i₁ i₂ → C)
  (p₁ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₁)
  (p₂ : ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ → (j : I₁ i₁ i₂) → Y j ⟶ toPreZeroHypercover.X i₂)
  (w :
    ∀ ⦃i₁ i₂ : toPreZeroHypercover.I₀⦄ (j : I₁ i₁ i₂),
      CategoryTheory.CategoryStruct.comp (p₁ j) (toPreZeroHypercover.f i₁) =
        CategoryTheory.CategoryStruct.comp (p₂ j) (toPreZeroHypercover.f i₂))
  (toPreZeroHypercover_1 : CategoryTheory.PreZeroHypercover S)
  (I₁_1 : toPreZeroHypercover_1.I₀ → toPreZeroHypercover_1.I₀ → Type w)
  (Y_1 : ⦃i₁ i₂ : toPreZeroHypercover_1.I₀⦄ → I₁_1 i₁ i₂ → C)
  (p₁_1 : ⦃i₁ i₂ : toPreZeroHypercover_1.I₀⦄ → (j : I₁_1 i₁ i₂) → Y_1 j ⟶ toPreZeroHypercover_1.X i₁)
  (p₂_1 : ⦃i₁ i₂ : toPreZeroHypercover_1.I₀⦄ → (j : I₁_1 i₁ i₂) → Y_1 j ⟶ toPreZeroHypercover_1.X i₂)
  (w_1 :
    ∀ ⦃i₁ i₂ : toPreZeroHypercover_1.I₀⦄ (j : I₁_1 i₁ i₂),
      CategoryTheory.CategoryStruct.comp (p₁_1 j) (toPreZeroHypercover_1.f i₁) =
        CategoryTheory.CategoryStruct.comp (p₂_1 j) (toPreZeroHypercover_1.f i₂)),
  ({ toPreZeroHypercover := toPreZeroHypercover, I₁ := I₁, Y := Y, p₁ := p₁, p₂ := p₂, w := w } =
      { toPreZeroHypercover := toPreZeroHypercover_1, I₁ := I₁_1, Y := Y_1, p₁ := p₁_1, p₂ := p₂_1, w := w_1 }) =
    (toPreZeroHypercover = toPreZeroHypercover_1 ∧ I₁ ≍ I₁_1 ∧ Y ≍ Y_1 ∧ p₁ ≍ p₁_1 ∧ p₂ ≍ p₂_1)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₂₁_single_one_fst : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G) (a : ↑A),
  ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A)) fun₀ | (1, g) => a) = fun₀ | 1 => a
-- Mathlib.Topology.Order.LeftRight
nhdsWithinLE_sup_nhdsWithinGT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {s : Set α} (a : α),
  nhdsWithin a (s ∩ Set.Iic a) ⊔ nhdsWithin a (s ∩ Set.Ioi a) = nhdsWithin a s
-- Init.Data.SInt.Bitwise
Int32.not_xor : ∀ {a b : Int32}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Mathlib.Order.Filter.Map
Filter.map_comap : ∀ {α : Type u_1} {β : Type u_2} (f : Filter β) (m : α → β),
  Filter.map m (Filter.comap m f) = f ⊓ Filter.principal (Set.range m)
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- Computable alternative to `AddMonoidHom.ofInjective`.  -/
AddMonoidHom.ofLeftInverse : {G : Type u_1} →
  [inst : AddGroup G] →
    {N : Type u_5} → [inst_1 : AddGroup N] → {f : G →+ N} → {g : N →+ G} → Function.LeftInverse ⇑g ⇑f → G ≃+ ↥f.range
-- Mathlib.Order.CountableSupClosed
CountableInfClosed.iInf_mem : ∀ {ι : Sort u_1} {α : Type u_2} {s : Set α} [inst : CompleteLattice α] [Countable ι] [Nonempty ι],
  CountableInfClosed s → ∀ {A : ι → α}, (∀ (n : ι), A n ∈ s) → ⨅ n, A n ∈ s
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_const_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ), ProbabilityTheory.covariance X (fun x => c) μ = 0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H1Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupCohomology.cocycles A 1)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H1Iso A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.π A 1)) x) =
    (groupCohomology.shortComplexH1 A).moduleCatToCycles.range.mkQ
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₁ A).hom) x)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.imageMonoIsoSource_hom_self_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f] {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageMonoIsoSource f).hom
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
-- Mathlib.SetTheory.Lists
/-- Subset relation for ZFA lists. Defined inductively.  -/
Lists'.Subset : {α : Type u_1} → Lists' α true → Lists' α true → Prop
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.isSeparated_iff_setRelIsSeparated : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s : Set X} {ε : ENNReal},
  Metric.IsSeparated ε s ↔ SetRel.IsSeparated {(x, y) | edist x y ≤ ε} s
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.isUnsafe : Lean.Elab.Command.AddAndFinalizeContext✝ → Bool
-- Mathlib.SetTheory.Ordinal.Notation
ONote.ofNat_succ : ∀ (n : ℕ), ↑n.succ = ONote.oadd 0 n.succPNat 0
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.nonempty_right : ∀ {G : Type u_1} [inst : AddGroup G] {S T : Set G}, AddSubgroup.IsComplement S T → T.Nonempty
-- Mathlib.Algebra.Torsor.Defs
/-- Dividing two points in the reverse order produces the inverse of dividing them.  -/
inv_sdiv_eq_sdiv_rev : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p₁ p₂ : P), (p₁ /ₛ p₂)⁻¹ = p₂ /ₛ p₁
-- Mathlib.Order.Category.FinBddDistLat
FinBddDistLat.ofHom_id : ∀ {X : Type u} [inst : DistribLattice X] [inst_1 : BoundedOrder X] [inst_2 : Fintype X],
  FinBddDistLat.ofHom (BoundedLatticeHom.id X) = CategoryTheory.CategoryStruct.id (FinBddDistLat.of X)
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.LocalizerMorphism.homMap_id : ∀ {C₁ : Type u_2} {C₂ : Type u_3} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_2, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D₁]
  [inst_3 : CategoryTheory.Category.{v_6, u_6} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  (L₁ : CategoryTheory.Functor C₁ D₁) [inst_4 : L₁.IsLocalization W₁] (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₂.IsLocalization W₂] (X : C₁),
  Φ.homMap L₁ L₂ (CategoryTheory.CategoryStruct.id (L₁.obj X)) =
    CategoryTheory.CategoryStruct.id (L₂.obj (Φ.functor.obj X))
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_atTop_zero_iff_le_of_antitone : ∀ {β : Type u_4} [Nonempty β] [inst : SemilatticeSup β] {f : β → ENNReal},
  Antitone f → (Filter.Tendsto f Filter.atTop (nhds 0) ↔ ∀ (ε : ENNReal), 0 < ε → ∃ n, f n ≤ ε)
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.tendsto_nhds_iff : ∀ {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z]
  {f : ι → Y} {l : Filter ι} {y : Y},
  Topology.IsEmbedding g → (Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y)))
-- Lean.Meta.Tactic.Grind.Proof
/-- Given two applications `a` and `b`, finds the common prefix.
Returns `some (f, n)` if `a` and `b` are of the form
- `f a_1 ... a_n`
- `f b_1 ... b_n`

and `none` otherwise.
 -/
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.findCommonPrefix : Lean.Expr → Lean.Expr → Option (Lean.Expr × ℕ)
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- `symm` is `true` when rewriting from right to left  -/
Mathlib.Tactic.LibraryRewrite.Rewrite.symm : Mathlib.Tactic.LibraryRewrite.Rewrite → Bool
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instHasZeroMorphisms.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Grp.instHasZeroMorphisms = { zero := CategoryTheory.Grp.instZeroHom, comp_zero := ⋯, zero_comp := ⋯ }
-- Batteries.Lean.Expr
/-- Like `getAppArgs` but ignores metadata.  -/
Lean.Expr.getAppArgs' : Lean.Expr → Array Lean.Expr
-- Mathlib.Data.Nat.Bits
Nat.shiftLeft_sub : ∀ (m : ℕ) {n k : ℕ}, k ≤ n → m <<< (n - k) = m <<< n >>> k
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_antitoneOn : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M],
  AntitoneOn MulArchimedeanClass.mk (Set.Ici 1)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- The integrals along a decreasing approximating sequence to the indicator of a closed set
tend to the measure of the closed set.  -/
HasOuterApproxClosed.tendsto_lintegral_apprSeq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F)
  [inst_2 : MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ],
  Filter.Tendsto (fun n => ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ) Filter.atTop (nhds (μ F))
-- Mathlib.Algebra.BigOperators.Expect
/-- `Fintype.expect_bijective` is a variant of `Finset.expect_bij` that accepts
`Function.Bijective`.

See `Function.Bijective.expect_comp` for a version without `h`.  -/
Fintype.expect_bijective : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : Fintype ι] [inst_1 : Fintype κ] [inst_2 : AddCommMonoid M]
  [inst_3 : Module ℚ≥0 M] (e : ι → κ),
  Function.Bijective e →
    ∀ (f : ι → M) (g : κ → M),
      (∀ (i : ι), f i = g (e i)) → (Finset.univ.expect fun i => f i) = Finset.univ.expect fun i => g i
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Summable.nsmul : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [ContinuousAdd α], Summable f L → ∀ (n : ℕ), Summable (fun x => n • f x) L
-- Mathlib.Computability.Reduce
/-- **Alias** of `stdRefl_oneOneReducible`. -/
reflexive_oneOneReducible : ∀ {α : Type u_1} [inst : Primcodable α], Std.Refl OneOneReducible
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.instCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      {c c' : C} → CategoryTheory.Category.{v_1, max u_1 v_1} (CategoryTheory.Span Wₗ Wᵣ c c')
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Reflective.comparison_essSurj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective R],
  (CategoryTheory.Monad.comparison (CategoryTheory.reflectorAdjunction R)).EssSurj
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_const : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q : ℚ), PadicSeq.norm (CauSeq.const (padicNorm p) q) = padicNorm p q
-- Mathlib.Data.Finset.Sum
Finset.card_toLeft_add_card_toRight : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)}, u.toLeft.card + u.toRight.card = u.card
-- Mathlib.SetTheory.Cardinal.NatCard
Set.card_strictMono : ∀ {α : Type u_1} [Finite α], StrictMono (Nat.card ∘ Set.Elem)
-- Mathlib.Logic.Equiv.Basic
Equiv.symm_trans_swap_trans : ∀ {α : Sort u_1} {β : Sort u_4} [inst : DecidableEq α] [inst_1 : DecidableEq β] (a b : α) (e : α ≃ β),
  (e.symm.trans (Equiv.swap a b)).trans e = Equiv.swap (e a) (e b)
-- Mathlib.Algebra.Category.Grp.Zero
CommGrpCat.isZero_of_iff_subsingleton : ∀ {G : Type u_1} [inst : CommGroup G], CategoryTheory.Limits.IsZero (CommGrpCat.of G) ↔ Subsingleton G
-- Mathlib.Topology.DiscreteSubset
IsDiscrete.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  IsDiscrete s → ContinuousOn f (f ⁻¹' s) → Function.Injective f → IsDiscrete (f ⁻¹' s)
-- Init.Grind.Config
/-- Maximum term generation for local theorems (e.g., hypotheses).
See `gen`.
 -/
Lean.Grind.Config.genLocal : Lean.Grind.Config → ℕ