mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.withDensitySMulLI_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {E : Type u_8} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : α → NNReal} (f_meas : Measurable f)
  (u : ↥(MeasureTheory.Lp E 1 (μ.withDensity fun x => ↑(f x)))),
  (MeasureTheory.withDensitySMulLI μ f_meas) u = MeasureTheory.MemLp.toLp (fun x => f x • ↑↑u x) ⋯
-- Mathlib.CategoryTheory.Limits.Cones
/-- Whiskering by an equivalence gives an equivalence between categories of cones.
 -/
CategoryTheory.Limits.Cocone.whiskeringEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (e : K ≌ J) → CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone (e.functor.comp F)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.ofIso_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X : C} [inst_2 : CategoryTheory.GrpObj G] (e : G ≅ X),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.inv e.inv)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom)
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Avoiding a fixed family of patterns is a closed condition (in the product topology on `G → A`).

Since each occurrence set `{ x | p.mulOccursInAt x v }` is open (when `A` is discrete),
its complement `{ x | ¬ p.mulOccursInAt x v }` is closed; `forbidden F` is the intersection
of these closed sets over `p ∈ F` and `v ∈ G`.  -/
SymbolicDynamics.FullShift.isClosed_mulForbidden : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : Monoid G]
  [IsLeftCancelMul G] [DiscreteTopology A] (F : Set (SymbolicDynamics.FullShift.Pattern A G)),
  IsClosed (SymbolicDynamics.FullShift.mulForbidden F)
-- Lean.Elab.Tactic.Omega.Core
/-- Walk through the equalities, finding either the first equality with minimal coefficient `±1`,
or otherwise the equality with minimal `(r.minNatAbs, r.maxNatAbs)` (ordered lexicographically).

Returns the coefficients of the equality, along with the value of `minNatAbs`.

Although we don't need to run a termination proof here, it's nevertheless important that we use this
ordering so the algorithm terminates in practice!
 -/
Lean.Elab.Tactic.Omega.Problem.selectEquality : Lean.Elab.Tactic.Omega.Problem → Option (Lean.Omega.Coeffs × ℕ)
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.pickNonNone : Lean.Parser.SyntaxStack → Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- For any pair objects `F (0: X ⟶ Y) = (0 : F X ⟶ F Y)`  -/
CategoryTheory.Functor.PreservesZeroMorphisms.map_zero : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D}
  {F : CategoryTheory.Functor C D} [self : F.PreservesZeroMorphisms] (X Y : C), F.map 0 = 0
-- Mathlib.Data.Sign.Defs
SignType.pos_eq_one : SignType.pos = 1
-- Mathlib.Algebra.GroupWithZero.Units.Basic
zpow_one_sub_natCast₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → ∀ (n : ℕ), a ^ (1 - ↑n) = a / a ^ n
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof → Sort u}
  (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof) → t.below → motive_2 t),
  t.brecOn F_1 F_2 = F_2 t (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.brecOn.go t F_1 F_2).2
-- Mathlib.Topology.MetricSpace.Gluing
/-- A metric space structure on the disjoint union `Σ i, E i`.
We embed isometrically each factor, set the basepoints at distance 1, arbitrarily,
and say that the distance from `a` to `b` is the sum of the distances of `a` and `b` to
their respective basepoints, plus the distance 1 between the basepoints.
Since there is an arbitrary choice in this construction, it is not an instance by default.  -/
Metric.Sigma.metricSpace : {ι : Type u_1} → {E : ι → Type u_2} → [(i : ι) → MetricSpace (E i)] → MetricSpace ((i : ι) × E i)
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- To bound the Hausdorff measure of a set, one may use coverings with maximum diameter tending
to `0`, indexed by any sequence of countable types.  -/
MeasureTheory.Measure.hausdorffMeasure_le_liminf_tsum : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {β : Type u_4}
  {ι : β → Type u_5} [∀ (n : β), Countable (ι n)] (d : ℝ) (s : Set X) {l : Filter β} (r : β → ENNReal),
  Filter.Tendsto r l (nhds 0) →
    ∀ (t : (n : β) → ι n → Set X),
      (∀ᶠ (n : β) in l, ∀ (i : ι n), Metric.ediam (t n i) ≤ r n) →
        (∀ᶠ (n : β) in l, s ⊆ ⋃ i, t n i) →
          (MeasureTheory.Measure.hausdorffMeasure d) s ≤
            Filter.liminf (fun n => ∑' (i : ι n), Metric.ediam (t n i) ^ d) l
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.indep_iSup_limsup : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4}
  {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) →
            (∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.Kernel.Indep (⨆ n, s n) (Filter.limsup s f) κ μα
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The image of `g` is the opposite of the image of `g.unop.`  -/
CategoryTheory.imageUnopUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B : Cᵒᵖ} → (g : A ⟶ B) → Opposite.unop (CategoryTheory.Limits.image g) ≅ CategoryTheory.Limits.image g.unop
-- Plausible.Testable
/-- Combine the test result for properties `p` and `q` to create a test for their disjunction.  -/
Plausible.TestResult.or : {p q : Prop} → Plausible.TestResult p → Plausible.TestResult q → Plausible.TestResult (p ∨ q)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.edgeSet_mapLe_eq_edgeSet : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p : G.Walk u v),
  (SimpleGraph.Walk.mapLe h p).edgeSet = p.edgeSet
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.topologicalClosure_coe : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (s : Subalgebra R A), ↑s.topologicalClosure = closure ↑s
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso'_eq_mapHomologyIso : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S.HasHomology]
  [inst_6 : F.PreservesLeftHomologyOf S] [inst_7 : F.PreservesRightHomologyOf S],
  S.mapHomologyIso' F = S.mapHomologyIso F
-- Mathlib.Algebra.Homology.CochainComplexPlus
CategoryTheory.Functor.mapCochainComplexPlus_map_hom_f : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : F.PreservesZeroMorphisms] {X Y : CochainComplex.Plus C} (f : X ⟶ Y) (i : ℤ),
  (F.mapCochainComplexPlus.map f).hom.f i = F.map (f.hom.f i)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- If `F i → f` in `L1`, then `∫ x, F i x ∂μ → ∫ x, f x ∂μ`.  -/
MeasureTheory.tendsto_integral_of_L1' : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {ι : Type u_6} (f : α → G),
  MeasureTheory.AEStronglyMeasurable f μ →
    ∀ {F : ι → α → G} {l : Filter ι},
      (∀ᶠ (i : ι) in l, MeasureTheory.Integrable (F i) μ) →
        Filter.Tendsto (fun i => MeasureTheory.eLpNorm (F i - f) 1 μ) l (nhds 0) →
          Filter.Tendsto (fun i => ∫ (x : α), F i x ∂μ) l (nhds (∫ (x : α), f x ∂μ))
-- Mathlib.Data.Num.ZNum
PosNum.sub'.eq_def : ∀ (x x_1 : PosNum),
  x.sub' x_1 =
    match x, x_1 with
    | a, PosNum.one => a.pred'.toZNum
    | PosNum.one, b => b.pred'.toZNumNeg
    | a.bit0, b.bit0 => (a.sub' b).bit0
    | a.bit0, b.bit1 => (a.sub' b).bitm1
    | a.bit1, b.bit0 => (a.sub' b).bit1
    | a.bit1, b.bit1 => (a.sub' b).bit0
-- Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
/-- If `colim` on each fiber `F.obj c` of a functor `F : C ⥤ Cat` preserves limits of shape `J`,
then the fiberwise colimit of the limit of a functor `K : J ⥤ Grothendieck F ⥤ H` is naturally
isomorphic to taking the limit of the composition `K ⋙ fiberwiseColim F H`.  -/
CategoryTheory.Limits.fiberwiseColimitLimitIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {H : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
        {J : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} J] →
            {F : CategoryTheory.Functor C CategoryTheory.Cat} →
              (K : CategoryTheory.Functor J (CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)) →
                [inst_3 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H] →
                  [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J H] →
                    [∀ (c : C), CategoryTheory.Limits.PreservesLimitsOfShape J CategoryTheory.Limits.colim] →
                      CategoryTheory.Limits.fiberwiseColimit (CategoryTheory.Limits.limit K) ≅
                        CategoryTheory.Limits.limit (K.comp (CategoryTheory.Limits.fiberwiseColim F H))
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.mk : {P : TopCat → Prop} →
  (toTop : TopCat) → [is_compact : CompactSpace ↑toTop] → [is_hausdorff : T2Space ↑toTop] → P toTop → CompHausLike P
-- Mathlib.Analysis.Normed.Group.Submodule
/-- If `x` is an element of a submodule `s` of a normed group `E`, its norm in `s` is equal to its
norm in `E`.  -/
Submodule.coe_norm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Submodule 𝕜 E} (x : ↥s), ‖x‖ = ‖↑x‖
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_apply_self : ∀ {α : Sort u_1} [inst : DecidableEq α] (i j a : α), (Equiv.swap i j) ((Equiv.swap i j) a) = a
-- Mathlib.Analysis.CStarAlgebra.Projection
isStarProjection_iff_spectrum_subset_and_isSelfAdjoint : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℝ A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {p : A},
  IsStarProjection p ↔ spectrum ℝ p ⊆ {0, 1} ∧ IsSelfAdjoint p
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.mkGenHEqPattern : List Lean.Level → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.GroupTheory.Congruence.Hom
Con.coe_mk' : ∀ {M : Type u_1} [inst : MulOneClass M] {c : Con M}, ⇑c.mk' = Con.toQuotient
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The `X` field of the homological complex `homotopyCofiber φ`.  -/
HomologicalComplex.homotopyCofiber.X : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) → [HomologicalComplex.HasHomotopyCofiber φ] → [DecidableRel c.Rel] → ι → C
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The isomorphism `Z^n(𝟙 _, f) ≅ H^n(f)`.  -/
CategoryTheory.Abelian.SpectralObject.cyclesIsoH : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i₀ i₁ : ι} →
              (f : i₀ ⟶ i₁) →
                (n₀ n₁ : ℤ) →
                  autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIsoH._auto_1 →
                    (X.cycles (CategoryTheory.CategoryStruct.id i₀) f n₀ ≅
                      (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.Topology.ExtremallyDisconnected
/-- A preirreducible space is extremally disconnected.  -/
instExtremallyDisconnectedOfPreirreducibleSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [h : PreirreducibleSpace X], ExtremallyDisconnected X
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.continuous_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a →
    ∀ [inst_3 : UniformSpace R] [DiscreteUniformity R] [inst_5 : UniformSpace S] [DiscreteUniformity S],
      Continuous (MvPowerSeries.subst a)
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.toIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.WalkingIso C),
  (CategoryTheory.WalkingIso.toIso F).inv = F.map CategoryTheory.WalkingIso.iso.inv
-- Std.Data.HashMap.Lemmas
Std.HashMap.get_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : (m.getKey? a).isSome = true}, (m.getKey? a).get h = m.getKey a ⋯
-- Init.Data.Vector.Lemmas
Vector.flatMap_singleton' : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, (xs.flatMap fun x => #v[x]) = Vector.cast ⋯ xs
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.containsThenInsert!_snd : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.containsThenInsert! k v t).2 = Std.DTreeMap.Internal.Impl.insert! k v t
-- Lean.Meta.Tactic.Grind.ForallProp
_private.Lean.Meta.Tactic.Grind.ForallProp.0.Lean.Meta.Grind.addLocalEMatchTheorems : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.Bounds.Basic
/-- Adding a point to a set preserves its boundedness below.  -/
bddBelow_insert : ∀ {α : Type u_1} [inst : Preorder α] [IsCodirectedOrder α] {s : Set α} {a : α}, BddBelow (insert a s) ↔ BddBelow s
-- Mathlib.Geometry.Manifold.Submersion
isOpen_isSubmersionAt : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  IsOpen {x | Manifold.IsSubmersionAt I J n f x}
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.mixAssigns.eq_1 : ∀ {aig : Std.Sat.AIG ℕ} (assign1 : ℕ → Bool) (assign2 : Fin aig.decls.size → Bool) (var : ℕ),
  Std.Sat.AIG.toCNF.mixAssigns✝ assign1 assign2 var =
    if h : var < aig.decls.size then assign2 ⟨var, h⟩ else assign1 (var - aig.decls.size)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α] (h : t.WF) {k k' : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getKey! k' =
    if compare k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else default else t.getKey! k'
-- Mathlib.Order.Fin.Basic
Fin.instBoundedOrder : {n : ℕ} → [NeZero n] → BoundedOrder (Fin n)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadIso.toNatIso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C} (h : M ≅ N),
  (CategoryTheory.ComonadIso.toNatIso h).hom = (CategoryTheory.comonadToFunctor C).map h.hom
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Preserving limits at any universe level implies preserving limits in universe `0`.  -/
CategoryTheory.Limits.preservesSmallestLimits_of_preservesLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{v₃, u₃, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabChar : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair.ext_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C}
  (zero : F.obj CategoryTheory.Limits.WalkingParallelPair.zero ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.zero)
  (one : F.obj CategoryTheory.Limits.WalkingParallelPair.one ≅ G.obj CategoryTheory.Limits.WalkingParallelPair.one)
  (left :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.left) one.hom =
        CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.left))
      CategoryTheory.Limits.parallelPair.ext._auto_1)
  (right :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) one.hom =
        CategoryTheory.CategoryStruct.comp zero.hom (G.map CategoryTheory.Limits.WalkingParallelPairHom.right))
      CategoryTheory.Limits.parallelPair.ext._auto_3)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Limits.parallelPair.ext zero one left right).inv.app X =
    (CategoryTheory.Limits.WalkingParallelPair.rec zero one X).inv
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f g : β → α} {a b : α}
  {L : SummationFilter β} [ContinuousMul α], HasProd f a L → HasProd g b L → HasProd (fun b => f b * g b) (a * b) L
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_sigma : ∀ {α : Type u_5} {E : α → Type u_4}, IsEmpty (Sigma E) ↔ ∀ (a : α), IsEmpty (E a)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : β k → β k}, (m.modify k f).getKey? k = if k ∈ m then some k else none
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.mapBilinear_apply : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ}
  [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : IsScalarTower R A M]
  [inst_9 : AddCommMonoid N] [inst_10 : Module R N] [inst_11 : AddCommMonoid P] [inst_12 : Module R P]
  [inst_13 : Module A P] [inst_14 : IsScalarTower R A P] [inst_15 : AddCommMonoid Q] [inst_16 : Module R Q]
  [inst_17 : Module B P] [inst_18 : IsScalarTower R B P] [inst_19 : SMulCommClass A B P] (f : M →ₗ[A] P)
  (g : N →ₗ[R] Q),
  ((TensorProduct.AlgebraTensorModule.mapBilinear R A B M N P Q) f) g = TensorProduct.AlgebraTensorModule.map f g
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.isEmpty_filter_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {f : α → β → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter f m)).isEmpty = true ↔
      ∀ (k : α) (h : m.contains k = true), f (m.getKey k h) (Std.DHashMap.Internal.Raw₀.Const.get m k h) = false)
-- Init.Grind.ToInt
/-- The embedding takes modulo to modulo (without needing to wrap into the range interval).
One might expect a `wrap` on the right hand side,
but in practice this stronger statement is usually true.
 -/
Lean.Grind.ToInt.Mod.toInt_mod : ∀ {α : Type u} {inst : Mod α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.Mod α I] (x y : α), ↑(x % y) = ↑x % ↑y
-- Qq.Match
_private.Qq.Match.0.Qq.Impl.getPatVars.mkMVar : Lean.Syntax → Array Lean.Term → StateT (Array Qq.Impl.PatternVar) Lean.Elab.TermElabM Lean.Term
-- Std.Net.Addr
/-- Obtain the `AddressFamily` associated with a `SocketAddress`.
 -/
Std.Net.SocketAddress.family : Std.Net.SocketAddress → Std.Net.AddressFamily
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.euc : ∀ {x : PSet.{u_1}} {y : PSet.{u_2}} {z : PSet.{u_3}}, x.Equiv y → z.Equiv y → x.Equiv z
-- Mathlib.Tactic.SwapVar
/-- The parser for swap rules  -/
Mathlib.Tactic.swapRule : Lean.ParserDescr
-- Mathlib.Topology.Sequences
/-- A sequentially compact set in a uniform space with countably generated uniformity filter
is complete.  -/
IsSeqCompact.isComplete : ∀ {X : Type u_1} [inst : UniformSpace X] {s : Set X} [(uniformity X).IsCountablyGenerated],
  IsSeqCompact s → IsComplete s
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.iter_eq_iterFromIdx : ∀ {β : Type w} {array : Array β}, array.iter = array.iterFromIdx 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.instFullOverTopOverForget : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) (X : T),
  (CategoryTheory.MorphismProperty.Over.forget P ⊤ X).Full
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.forall_smul_mem_iff : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : SetLike S M]
  [SMulMemClass S R M] {N : S} {x : M}, (∀ (a : R), a • x ∈ N) ↔ x ∈ N
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.limitConeIsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}),
  ProfiniteGrp.limitConeIsLimit F =
    {
      lift := fun cone =>
        ProfiniteGrp.ofHom
          (let __src :=
            TopCat.Hom.hom
              ((Profinite.limitConeIsLimit (F.comp (CategoryTheory.forget₂ ProfiniteGrp.{max u v} Profinite))).lift
                  ((CategoryTheory.forget₂ ProfiniteGrp.{max u v} Profinite).mapCone cone)).hom;
          { toFun := __src.toFun, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }),
      fac := ⋯, uniq := ⋯ }
-- Mathlib.Control.Monad.Cont
MonadCont : (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.Data.Int.Cast.Lemmas
SemiconjBy.intCast_mul_right : ∀ {α : Type u_3} [inst : Ring α] {a x y : α}, SemiconjBy a x y → ∀ (n : ℤ), SemiconjBy a (↑n * x) (↑n * y)
-- Mathlib.Algebra.Group.Prod
AddEquiv.uniqueProd.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : Unique N],
  AddEquiv.uniqueProd = { toEquiv := Equiv.uniqueProd M N, map_add' := ⋯ }
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- A list of parenthesized binders  -/
BigOperators.bigOpBinderCollection : Lean.ParserDescr