mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_counitIso_hom_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right]
  (X :
    CategoryTheory.Limits.Fork
      (I.fstPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))
      (I.sndPiMapOfIsLimit (CategoryTheory.Limits.limit.cone (CategoryTheory.Discrete.functor I.left))
        (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor I.right)))),
  (I.multiforkEquivPiFork.counitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Data.Option.NAry
Option.map₂_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {a : Option α} {b : Option β},
  Option.map₂ f a b = none ↔ a = none ∨ b = none
-- Init.Data.Array.Lemmas
List.filter_toArray' : ∀ {α : Type u_1} {p : α → Bool} {l : List α} {stop : ℕ},
  stop = l.length → Array.filter p l.toArray 0 stop = (List.filter p l).toArray
-- Mathlib.Topology.Algebra.UniformConvergence
instMulActionUniformFun : {α : Type u_1} → {β : Type u_2} → {M : Type u_5} → [inst : Monoid M] → [MulAction M β] → MulAction M (UniformFun α β)
-- Mathlib.Order.Interval.Finset.Defs
Iic_orderDual_def : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] (a : αᵒᵈ),
  Finset.Iic a = Finset.map OrderDual.toDual.toEmbedding (Finset.Ici (OrderDual.ofDual a))
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.empty_mul_empty : ∀ {α : Type u} {m' : Type uₘ} {o' : Type uₒ} [inst : NonUnitalNonAssocSemiring α] (A : Matrix m' (Fin 0) α)
  (B : Matrix (Fin 0) o' α), A * B = 0
-- Lean.Message
Lean.instToMessageDataSubarray : {α : Type} → [Lean.ToMessageData α] → Lean.ToMessageData (Subarray α)
-- Mathlib.Topology.Bornology.Hom
/-- The pullback of the `Bornology.cobounded` filter under the function is contained in the
cobounded filter. Equivalently, the function maps bounded sets to bounded sets.  -/
LocallyBoundedMap.comap_cobounded_le' : ∀ {α : Type u_6} {β : Type u_7} [inst : Bornology α] [inst_1 : Bornology β] (self : LocallyBoundedMap α β),
  Filter.comap self.toFun (Bornology.cobounded β) ≤ Bornology.cobounded α
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_bot_left : ∀ {G : Type u_1} [inst : Group G] (H₁ : Subgroup G), ⁅⊥, H₁⁆ = ⊥
-- Init.Data.SInt.Lemmas
Int8.toISize_lt : ∀ {a b : Int8}, a.toISize < b.toISize ↔ a < b
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Iio_add_one_eq_Iic : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrderBot α] [inst_3 : Add α]
  [SuccAddOrder α] [NoMaxOrder α] (b : α), Finset.Iio (b + 1) = Finset.Iic b
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- `LinearMap.compAlternatingMap` as an `S`-linear map.  -/
LinearMap.compAlternatingMapₗ : {R : Type u_1} →
  [inst : Semiring R] →
    {M : Type u_2} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_3} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                {ι : Type u_7} →
                  (S : Type u_10) →
                    {N₂ : Type u_11} →
                      [inst_5 : AddCommMonoid N₂] →
                        [inst_6 : Module R N₂] →
                          [inst_7 : Semiring S] →
                            [inst_8 : Module S N] →
                              [inst_9 : Module S N₂] →
                                [inst_10 : SMulCommClass R S N] →
                                  [inst_11 : SMulCommClass R S N₂] →
                                    [LinearMap.CompatibleSMul N N₂ S R] →
                                      (N →ₗ[R] N₂) → M [⋀^ι]→ₗ[R] N →ₗ[S] M [⋀^ι]→ₗ[R] N₂
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whisker_assoc_symm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
  (f : Y ⟶ Y') (Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y' Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) Z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z).hom h))
-- Mathlib.Order.Filter.CardinalInter
/-- `Filter.CardinalGenerateSets c g` is the (sets of the)
greatest `cardinalInterFilter c` containing `g`.  -/
Filter.CardinalGenerateSets : {α : Type u} → {c : Cardinal.{u}} → Set (Set α) → Set α → Prop
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- `J.Cover X` denotes the poset of covers of `X` with respect to the
Grothendieck topology `J`.  -/
CategoryTheory.GrothendieckTopology.Cover : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.GrothendieckTopology C → C → Type (max u v)
-- Mathlib.Analysis.Convex.Gauge
tendsto_gauge_nhds_zero : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], s ∈ nhds 0 → Filter.Tendsto (gauge s) (nhds 0) (nhds 0)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.toGroup.eq_1 : ∀ {G : Type u_3} [inst : Group G] (H : Subgroup G), H.toGroup = SubgroupClass.toGroup H
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wrepr.eq_1 : ∀ {F : Type u → Type v} [q : QPF F], QPF.Wrepr = QPF.recF (PFunctor.W.mk ∘ QPF.repr)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.lift_self : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] {T : Bundle.Trivialization F proj} {z : Z}, proj z ∈ T.baseSet → T.lift z (proj z) = z
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_univ_iff : ∀ {α : Type u}, Set.univ.Nontrivial ↔ Nontrivial α
-- Mathlib.Logic.Equiv.Prod
Equiv.arrowProdEquivProdArrow_apply : ∀ (α : Type u_9) (β : α → Type u_10) (γ : α → Type u_11) (f : (i : α) → β i × γ i),
  (Equiv.arrowProdEquivProdArrow α β γ) f = (fun c => (f c).1, fun c => (f c).2)
-- Aesop.Rule.Name
Aesop.instInhabitedPhaseName.default : Aesop.PhaseName
-- Mathlib.Probability.Kernel.Composition.RadonNikodym
/-- Auxiliary lemma for `rnDeriv_measure_compProd_left`.  -/
_private.Mathlib.Probability.Kernel.Composition.RadonNikodym.0.ProbabilityTheory.rnDeriv_measure_compProd_left_of_ac : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν →
    ∀ (κ : ProbabilityTheory.Kernel α β) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
      [ProbabilityTheory.IsFiniteKernel κ],
      (μ.compProd κ).rnDeriv (ν.compProd κ) =ᵐ[ν.compProd κ] fun p => μ.rnDeriv ν p.1
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.ofArchimedean_inj : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {R : Type u_2}
  [inst_3 : LinearOrder R] [inst_4 : CommRing R] [inst_5 : IsStrictOrderedRing R] [inst_6 : Archimedean R]
  (f : R →+*o K) {x y : R},
  (ArchimedeanClass.FiniteResidueField.ofArchimedean f) x = (ArchimedeanClass.FiniteResidueField.ofArchimedean f) y ↔
    x = y
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure_eq_self_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W.multiplicativeClosure = W ↔ W.IsMultiplicative
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_div : ∀ {a b : ℕ} (ha : a < 2 ^ 64) (hb : b < 2 ^ 64), UInt64.ofNatLT (a / b) ⋯ = UInt64.ofNatLT a ha / UInt64.ofNatLT b hb
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (curr : ℕ) → motive curr.succ),
  (match 0 with
    | 0 => h_1 ()
    | curr.succ => h_2 curr) =
    h_1 ()
-- Mathlib.Algebra.Group.Commute.Defs
IsAddRightRegular.addCommute_add_right_iff : ∀ {S : Type u_3} [inst : AddSemigroup S] {a b : S}, IsAddRightRegular a → (AddCommute (b + a) a ↔ AddCommute a b)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- additive version of `MeasureTheory.Measure.haar.haarProduct`  -/
MeasureTheory.Measure.haar.addHaarProduct : {G : Type u_1} → [AddGroup G] → [inst : TopologicalSpace G] → Set G → Set (TopologicalSpace.Compacts G → ℝ)
-- Lean.Parser.Command
Lean.Parser.Command.declModifiers.parenthesizer : Bool → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_mul : ∀ {R : Type u} [inst : Semiring R] (a b : AddMonoidAlgebra R ℕ),
  { toFinsupp := a * b } = { toFinsupp := a } * { toFinsupp := b }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- To check whether two morphisms are equalized by the maps of a pullback cone, it suffices to
check it for `fst t` and `snd t`  -/
CategoryTheory.Limits.PullbackCone.equalizer_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (t : CategoryTheory.Limits.PullbackCone f g) {W : C} {k l : W ⟶ t.pt},
  CategoryTheory.CategoryStruct.comp k t.fst = CategoryTheory.CategoryStruct.comp l t.fst →
    CategoryTheory.CategoryStruct.comp k t.snd = CategoryTheory.CategoryStruct.comp l t.snd →
      ∀ (j : CategoryTheory.Limits.WalkingCospan),
        CategoryTheory.CategoryStruct.comp k (t.π.app j) = CategoryTheory.CategoryStruct.comp l (t.π.app j)
-- Mathlib.Topology.Order.NhdsSet
Icc_mem_nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a < b → c < d → Set.Icc a d ∈ nhdsSet (Set.Icc b c)
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- `botSet` is the set of all bottom elements.  -/
botSet : {R : Type u_1} → [LinearOrder R] → Set R
-- Mathlib.Data.Set.Sups
Set.image_subset_infs_right : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t : Set α} {a : α}, a ∈ s → (fun x => a ⊓ x) '' t ⊆ s ⊼ t
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a rank `j` cell `c` for a rank function `f` for a proper
pairing of a subcomplex of a simplicial set, this is
the nondegenerate simplex in `f.sigmaStdSimplex j`
not in the image of `f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j`
which corresponds to `c.ιSigmaStdSimplex`.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.type₁ : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          (f : P.RankFunction ι) → [inst_1 : P.IsProper] → {j : ι} → f.Cell j → (SSet.Subcomplex.range (f.m j)).N
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mem_coe : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) {x : ι → ℝ}, x ∈ ↑I ↔ x ∈ I
-- Lean.DocString.Types
Lean.Doc.instBEqDescItem : {α : Type u_1} → {β : Type u_2} → [BEq α] → [BEq β] → BEq (Lean.Doc.DescItem α β)
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensorUnit_β : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (U : C),
  (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Center C)).snd.β U =
    CategoryTheory.MonoidalCategoryStruct.leftUnitor U ≪≫ (CategoryTheory.MonoidalCategoryStruct.rightUnitor U).symm
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
AddMonoidHom.map_multiset_sum : ∀ {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : M →+ N) (s : Multiset M),
  f s.sum = (Multiset.map (⇑f) s).sum
-- Mathlib.Algebra.Group.Defs
/-- A commutative semigroup is a type with an associative commutative `(*)`.  -/
CommSemigroup : Type u → Type u
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The map of a Gaussian distribution by multiplication by a constant is a Gaussian.  -/
ProbabilityTheory.gaussianReal_map_const_mul : ∀ {μ : ℝ} {v : NNReal} (c : ℝ),
  MeasureTheory.Measure.map (fun x => c * x) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (c * μ) (NNReal.mk (c ^ 2) ⋯ * v)
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Mono.of_binaryCoproductDisjoint_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [CategoryTheory.Limits.BinaryCoproductDisjoint X Y]
  {Z : C} {f : X ⟶ Z} (g : Y ⟶ Z) (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)),
  CategoryTheory.Mono f
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Ineq.WithStrictness.le.sizeOf_spec : sizeOf Mathlib.Ineq.WithStrictness.le = 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonWaitForILeansParams.fromJson : Lean.Json → Except String Lean.Lsp.WaitForILeansParams
-- Lean.Meta.Basic
Lean.Meta.DefEqCacheKey.lhs : Lean.Meta.DefEqCacheKey → Lean.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey_eq_maxKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)} {he : l.isEmpty = false},
  Std.Internal.List.maxKey l he = Std.Internal.List.maxKey! l
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_const_add_Ioc : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => a + x) '' Set.Ioc b c = Set.Ioc (a + b) (a + c)
-- Lean.Server.CodeActions.Basic
Lean.Server.LazyCodeAction.lazy? : Lean.Server.LazyCodeAction → Option (IO Lean.Lsp.CodeAction)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Equivalence.toAdjunction_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.toAdjunction.counit = e.counit
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grind_ref_ : Lean.ParserDescr
-- Mathlib.Data.Seq.Parallel
_private.Mathlib.Data.Seq.Parallel.0.Computation.parallel.aux2.match_1.eq_1 : ∀ {α : Type u_1} (motive : α ⊕ List (Computation α) → Sort u_2) (a : α) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (ls : List (Computation α)) → motive (Sum.inr ls)),
  (match Sum.inl a with
    | Sum.inl a => h_1 a
    | Sum.inr ls => h_2 ls) =
    h_1 a
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit.unitIso =
    CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso C
-- Lean.Meta.IndPredBelow
/-- Inductive eliminates into any universe  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.largeElim : Lean.Meta.IndPredBelow.Context✝ → Bool
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
WithTop.iInf_coe_eq_top : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {f : ι → α}, ⨅ x, ↑(f x) = ⊤ ↔ IsEmpty ι
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.id_image : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor (CategoryTheory.CategoryStruct.id X)).obj U = U
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.mk.inj : ∀ {α : Type u_4} {inst : TopologicalSpace α} {toCompacts : TopologicalSpace.Compacts α}
  {nonempty' : toCompacts.carrier.Nonempty} {toCompacts_1 : TopologicalSpace.Compacts α}
  {nonempty'_1 : toCompacts_1.carrier.Nonempty},
  { toCompacts := toCompacts, nonempty' := nonempty' } = { toCompacts := toCompacts_1, nonempty' := nonempty'_1 } →
    toCompacts = toCompacts_1
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.pairwise_aedisjoint_of_aedisjoint_forall_ne_one : ∀ {G : Type u_5} {α : Type u_6} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {s : Set α},
  (∀ (g : G), g ≠ 1 → MeasureTheory.AEDisjoint μ (g • s) s) →
    (∀ (g : G), MeasureTheory.Measure.QuasiMeasurePreserving (fun x => g • x) μ μ) →
      Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g • s)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_inv_naturality_middle : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h))
      (CategoryTheory.Bicategory.associator f g' h).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.not_isInducedSubgraph_iff : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β},
  H ≤ G → (¬H.IsInducedSubgraph G ↔ ∃ e x y, G.IsLink e x y ∧ x ∈ H.vertexSet ∧ y ∈ H.vertexSet ∧ e ∉ H.edgeSet)
-- Mathlib.Algebra.Order.Antidiag.FinsuppEquiv
Finset.finsuppAntidiagEquivSubtype_symm_apply_coe : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] (s : Finset ι) (n : μ) (f : { P // (P.sum fun x => id) = n }),
  ↑((s.finsuppAntidiagEquivSubtype n).symm f) = (↑f).extendDomain
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If each component of the unit is a split epimorphism, then the left adjoint is full.  -/
CategoryTheory.Adjunction.full_L_of_isSplitEpi_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R)
  [∀ (X : C), CategoryTheory.IsSplitEpi (h.unit.app X)], L.Full
-- Mathlib.Probability.Kernel.Basic
/-- See `swap_apply` for a partially applied version of this lemma.  -/
ProbabilityTheory.Kernel.swap_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (ab : α × β) {s : Set (β × α)},
  MeasurableSet s → ((ProbabilityTheory.Kernel.swap α β) ab) s = s.indicator 1 ab.swap
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
aeconst_of_dense_aestabilizer_vadd : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [ContinuousNeg G] {X : Type u_2}
  [inst_3 : TopologicalSpace X] [R1Space X] [inst_5 : MeasurableSpace X] [BorelSpace X] [inst_7 : AddAction G X]
  [ContinuousVAdd G X] {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular]
  [inst_11 : ErgodicVAdd G X μ] {s : Set X},
  MeasureTheory.NullMeasurableSet s μ →
    Dense ↑(AddAction.aestabilizer G μ s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.Tactic.NormNum.Core
/-- `@[norm_num e]`, where `e` is an expression (optionally with `_`s) adds the tagged definition,
of type `NormNumExt`, to the set of normalization procedures used by the `norm_num` tactic, such
that it will fire on expressions matching the form `e`. Use holes in `e` to indicate arbitrary
subexpressions, for example `@[norm_num _ + _]` will match any addition.

* `@[norm_num e1, e2, ...]` will match either `e1` or `e2` or ...

Example:
```lean
@[norm_num -_] def evalNeg : NormNumExt where eval {u α} e := do
  let .app (f : Q($α → $α)) (a : Q($α)) ← whnfR e | failure
  let ra ← derive a
  let rα ← inferRing α
  ra.neg
```
 -/
norm_num : Lean.ParserDescr
-- Mathlib.Algebra.Lie.Basic
IsLieTower.leibniz_lie : ∀ {L₁ : Type u_1} {L₂ : Type u_2} {M : Type u_3} {inst : Bracket L₁ L₂} {inst_1 : Bracket L₁ M} {inst_2 : Bracket L₂ M}
  {inst_3 : Add M} [self : IsLieTower L₁ L₂ M] (x : L₁) (y : L₂) (m : M), ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkLineEq.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.Modification.vcomp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {η θ ι : F ⟶ G} (Γ : CategoryTheory.Lax.OplaxTrans.Modification η θ)
  (Δ : CategoryTheory.Lax.OplaxTrans.Modification θ ι) (a : B),
  (Γ.vcomp Δ).app a = CategoryTheory.CategoryStruct.comp (Γ.app a) (Δ.app a)
-- Mathlib.Algebra.Group.Defs
NegZeroClass.neg_zero : ∀ {G : Type u_2} [self : NegZeroClass G], -0 = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insertMany_empty_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] {l : List ((a : α) × β a)} {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l →
        ∀ {h' : Std.DTreeMap.Internal.Impl.contains k' ↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯) = true},
          (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getKey k' h' = k
-- Init.Data.Vector.Find
Vector.find?_pmap : ∀ {α β : Type} {n : ℕ} {P : α → Prop} {f : (a : α) → P a → β} {xs : Vector α n} (H : ∀ a ∈ xs, P a) {p : β → Bool},
  Vector.find? p (Vector.pmap f xs H) =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      (Vector.find?
        (fun x =>
          match x with
          | ⟨a, m⟩ => p (f a ⋯))
        xs.attach)
-- Lean.Elab.Term.TermElabM
/-- The docstring, if present. Docstring processing is deferred until the declaration is added to
the environment (needed for Verso docstrings to work).  -/
Lean.Elab.Term.LetRecToLift.docString? : Lean.Elab.Term.LetRecToLift → Option (Lean.TSyntax `Lean.Parser.Command.docComment)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor that preserves biproducts of a pair preserves binary biproducts.  -/
CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBiproducts : ∀ {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) [inst_4 : F.PreservesZeroMorphisms]
  [CategoryTheory.Limits.PreservesBiproductsOfShape CategoryTheory.Limits.WalkingPair F],
  CategoryTheory.Limits.PreservesBinaryBiproducts F
-- Mathlib.Data.NNReal.Basic
/-- This lemma is needed for the `norm_cast` simp set. Outside of this use case `Nat.coe_sub`
should be used.  -/
NNReal.coe_sub_of_lt : ∀ {a b : NNReal}, a < b → ↑(b - a) = ↑b - ↑a
-- Mathlib.GroupTheory.Torsion
/-- Torsion submonoids are torsion.  -/
CommMonoid.torsion.isMulTorsion : ∀ {G : Type u_1} [inst : CommMonoid G], IsMulTorsion ↥(CommMonoid.torsion G)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.isEquivalenceMap₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  [F.IsEquivalence] [G.Faithful] [G.Full] [CategoryTheory.IsIso α] [CategoryTheory.IsIso β],
  (CategoryTheory.CostructuredArrow.map₂ α β).IsEquivalence
-- Init.Data.Order.Ord
Std.LawfulBEqCmp.reflBEq : ∀ {α : Type u} [inst : BEq α] {cmp : α → α → Ordering} [inst_1 : Std.LawfulBEqCmp cmp] [Std.ReflCmp cmp], ReflBEq α
-- Batteries.Util.Pickle
/-- Load an object from disk and run some continuation on it, freeing memory afterwards.  -/
withUnpickle : {m : Type → Type u_1} → [Monad m] → [MonadLiftT IO m] → {α β : Type} → System.FilePath → (α → m β) → m β