mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.memLp_const_iff_enorm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε'' : Type u_8} [inst : TopologicalSpace ε'']
  [inst_1 : ESeminormedAddMonoid ε''] {p : ENNReal} {c : ε''},
  ‖c‖ₑ ≠ ⊤ → p ≠ 0 → p ≠ ⊤ → (MeasureTheory.MemLp (fun x => c) p μ ↔ ‖c‖ₑ = 0 ∨ μ Set.univ < ⊤)
-- Init.Data.SInt.Lemmas
ISize.toBitVec_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toBitVec = OfNat.ofNat n
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- A variant of `nnnorm_sub_mul_self_le` which uses `‖·‖` instead of `‖·‖₊`.  -/
CStarAlgebra.norm_sub_mul_self_le : ∀ {A : Type u_2} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {x y : A} (z : A),
  0 ≤ x → y ∈ Set.Icc x 1 → ∀ {c : ℝ}, 0 ≤ c → ‖star z * (1 - x) * z‖ ≤ c ^ 2 → ‖z - y * z‖ ≤ c
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmas.mk.injEq : ∀ (lemmas lemmas_1 : Lean.PHashMap Lean.Meta.AuxLemmaKey (Lean.Name × List Lean.Name)),
  ({ lemmas := lemmas } = { lemmas := lemmas_1 }) = (lemmas = lemmas_1)
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.unitOfArray.eq_1 : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (l : Array α),
  Std.DHashMap.Raw.Const.unitOfArray l = Std.DHashMap.Raw.Const.insertManyIfNewUnit ∅ l
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- Composing a multilinear map with a linear map gives again a multilinear map.  -/
LinearMap.compMultilinearMap : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        {M₃ : Type v₃} →
          [inst : Semiring R] →
            [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : (i : ι) → Module R (M₁ i)] →
                    [inst_5 : Module R M₂] →
                      [inst_6 : Module R M₃] → (M₂ →ₗ[R] M₃) → MultilinearMap R M₁ M₂ → MultilinearMap R M₁ M₃
-- Init.Omega.Constraint
/-- Flip a constraint.
This operation is not useful by itself, but is used to implement `neg` and `scale`.
 -/
Lean.Omega.Constraint.flip : Lean.Omega.Constraint → Lean.Omega.Constraint
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.foldlM_filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_of_ne_top : ∀ {x : EReal}, x ≠ ⊤ → x.toENNReal = ENNReal.ofReal x.toReal
-- Mathlib.CategoryTheory.Subobject.Comma
/-- If `A : S.obj B ⟶ T` is a costructured arrow for `S : C ⥤ D` and `T : D`, then we can
explicitly describe the quotients of `A` as the quotients `P` of `B` in `C` for which `A.hom`
factors through the image of `P` under `S`.  -/
CategoryTheory.CostructuredArrow.quotientEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} →
          {T : D} →
            [CategoryTheory.Limits.HasFiniteColimits C] →
              [CategoryTheory.Limits.PreservesFiniteColimits S] →
                (A : CategoryTheory.CostructuredArrow S T) →
                  CategoryTheory.Subobject (Opposite.op A) ≃o
                    { P // ∃ q, CategoryTheory.CategoryStruct.comp (S.map P.arrow.unop) q = A.hom }
-- Std.Http.Data.URI.Basic
/-- The host identifying the network location.
 -/
Std.Http.URI.Authority.host : Std.Http.URI.Authority → Std.Http.URI.Host
-- Mathlib.Algebra.Ring.Parity
Nat.not_odd_iff : ∀ {n : ℕ}, ¬Odd n ↔ n % 2 = 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instZSMul : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → SMul ℤ (SchwartzMap E F)
-- Mathlib.Topology.Algebra.Group.Basic
map_mul_left_nhds : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (x y : G),
  Filter.map (fun x_1 => x * x_1) (nhds y) = nhds (x * y)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inr_v_snd_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCocone.inr φ)).v p q hpq)
      ((CochainComplex.mappingCocone.snd φ).v q p ⋯) =
    CategoryTheory.CategoryStruct.id (L.X p)
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.getRootStr : Lean.Elab.ConfigEval.ConfigItem → String
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_inj : ∀ {a b : UInt8}, a.toUInt64 = b.toUInt64 ↔ a = b
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.index.sizeOf_spec : ∀ (imode : Aesop.IndexingMode), sizeOf (Aesop.Frontend.BuilderOption.index imode) = 1 + sizeOf imode
-- Mathlib.GroupTheory.Congruence.BigOperators
Con.coe_multisetProd : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] (c : Con M) (s : Multiset ι) (f : ι → M),
  ↑(Multiset.map f s).prod = (Multiset.map (fun i => ↑(f i)) s).prod
-- Lean.Meta.Tactic.Util
/-- Throw a tactic exception with given tactic name if the given metavariable is assigned.  -/
Lean.MVarId.checkNotAssigned : Lean.MVarId → Lean.Name → Lean.MetaM Unit
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.TransitionSpec.julian.injEq : ∀ (day day_1 : Std.Time.Internal.Bounded.LE 1 365),
  (Std.Time.TimeZone.TransitionSpec.julian day = Std.Time.TimeZone.TransitionSpec.julian day_1) = (day = day_1)
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_antitone : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing 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]
  {p : M →ₗ[R] N →ₗ[R] R}, Antitone (PointedCone.dual p)
-- Mathlib.CategoryTheory.Functor.Basic
/-- `𝟭 C` is the identity functor on a category `C`.  -/
CategoryTheory.Functor.id : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C C
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instCoeCommMonCat.eq_1 : AddCommGrpCat.instCoeCommMonCat = { coe := (CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat).obj }
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_inter_le_size_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₁.size
-- Mathlib.CategoryTheory.Iso
/-- The forward direction of an isomorphism.  -/
CategoryTheory.Iso.hom : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ≅ Y) → (X ⟶ Y)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.differentiableWithinAt_arccos_Ici : ∀ {x : ℝ}, DifferentiableWithinAt ℝ Real.arccos (Set.Ici x) x ↔ x ≠ -1
-- Std.Sat.AIG.Relabel
_private.Std.Sat.AIG.Relabel.0.Std.Sat.AIG.Decl.relabel.match_1.eq_1 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (h_1 : Unit → motive Std.Sat.AIG.Decl.false)
  (h_2 : (a : α) → motive (Std.Sat.AIG.Decl.atom a))
  (h_3 : (lhs rhs : Std.Sat.AIG.Fanin) → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match Std.Sat.AIG.Decl.false with
    | Std.Sat.AIG.Decl.false => h_1 ()
    | Std.Sat.AIG.Decl.atom a => h_2 a
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs) =
    h_1 ()
-- Mathlib.LinearAlgebra.Multilinear.DirectSum
MultilinearMap.fromDirectSumEquiv.eq_1 : ∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M']
  [inst_5 : DecidableEq ι] [inst_6 : Finite ι], MultilinearMap.fromDirectSumEquiv = MultilinearMap.fromDFinsuppEquiv κ R
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.brecOn.go : {motive : (a : Tactic.ComputeAsymptotics.Basis) → Tactic.ComputeAsymptotics.BasisExtension a → Sort u} →
  {a : Tactic.ComputeAsymptotics.Basis} →
    (t : Tactic.ComputeAsymptotics.BasisExtension a) →
      ((a : Tactic.ComputeAsymptotics.Basis) →
          (t : Tactic.ComputeAsymptotics.BasisExtension a) →
            Tactic.ComputeAsymptotics.BasisExtension.below t → motive a t) →
        motive a t ×' Tactic.ComputeAsymptotics.BasisExtension.below t
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instZero : {R : Type u_1} → {a b : R} → [Zero R] → Zero (QuadraticAlgebra R a b)
-- Init.Data.Int.Order
Int.lt_iff_le_not_le : ∀ {a b : ℤ}, a < b ↔ a ≤ b ∧ ¬b ≤ a
-- Init.Data.List.Perm
/-- This theorem is a variant of `Perm.foldr_eq` defined in Mathlib which uses typeclasses rather
than the explicit `comm` argument.
 -/
List.Perm.foldr_eq' : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → β} {l₁ l₂ : List α},
  l₁.Perm l₂ →
    (∀ x ∈ l₁, ∀ y ∈ l₁, ∀ (z : β), f y (f x z) = f x (f y z)) →
      ∀ (init : β), List.foldr f init l₁ = List.foldr f init l₂
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
ContinuousAlternatingMap.hasStrictFDerivAt_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {ι : Type u_2} {F : Type u_4} {G : Type u_5} {H : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] [inst_7 : Fintype ι] [inst_8 : DecidableEq ι]
  (fg : G [⋀^ι]→L[𝕜] H × (F →L[𝕜] G)),
  HasStrictFDerivAt (fun fg => fg.1.compContinuousLinearMap fg.2)
    (ContinuousAlternatingMap.compContinuousLinearMapCLM fg.2 ∘SL
        ContinuousLinearMap.fst 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G) +
      fg.1.fderivCompContinuousLinearMap fg.2 ∘SL ContinuousLinearMap.snd 𝕜 (G [⋀^ι]→L[𝕜] H) (F →L[𝕜] G))
    fg
-- Mathlib.Tactic.Hint
/-- Construct a suggestion for a tactic.
* Check the passed `MessageLog` for an info message beginning with "Try this: ".
* If found, use that as the suggestion.
* Otherwise use the provided syntax.
* Also, look for remaining goals and pretty print them after the suggestion.
 -/
Mathlib.Tactic.Hint.suggestion : Lean.TSyntax `tactic →
  Lean.PersistentArray Lean.Elab.InfoTree → Lean.Elab.Tactic.TacticM Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.CategoryTheory.Sites.CompatiblePlus
CategoryTheory.GrothendieckTopology.ι_plusCompIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D) [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_8 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F] (X : Cᵒᵖ)
  (W : (J.Cover (Opposite.unop X))ᵒᵖ),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.colimit.ι (J.diagram P (Opposite.unop X)) W))
      ((J.plusCompIso F P).hom.app X) =
    CategoryTheory.CategoryStruct.comp ((J.diagramCompIso F P (Opposite.unop X)).hom.app W)
      (CategoryTheory.Limits.colimit.ι (J.diagram (P.comp F) (Opposite.unop X)) W)
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.postponed.inj : ∀ {result result_1 : Aesop.PostponedSafeRule},
  Aesop.SafeRuleResult.postponed result = Aesop.SafeRuleResult.postponed result_1 → result = result_1
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexCellsEquiv_symm_apply_k_simplex : ∀ {X : SSet} (s : X.N), (SSet.relativeCellComplexCellsEquiv.symm s).k.simplex = s.simplex
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.toFinset_sum_count_nsmul_eq : ∀ {ι : Type u_1} [inst : DecidableEq ι] (s : Multiset ι), ∑ a ∈ s.toFinset, Multiset.count a s • {a} = s
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.pushout_inl_tensorProdObjIsoPushoutObj_inv_right : ∀ {R S : CommRingCat} [inst : Algebra ↑R ↑S] (A : CategoryTheory.Under R),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl A.hom (CommRingCat.ofHom (algebraMap ↑R ↑S)))
      (CategoryTheory.Under.Hom.right (CommRingCat.tensorProdObjIsoPushoutObj S A).inv) =
    CommRingCat.ofHom Algebra.TensorProduct.includeRight.toRingHom
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_η_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {C' : Type u₁'}
  [inst_4 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal]
  (G : CategoryTheory.Functor D C'),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.η F))
      (G.map (CategoryTheory.Functor.LaxMonoidal.ε F)) =
    CategoryTheory.CategoryStruct.id (G.obj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coalgebraEquivOver_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C],
  (CategoryTheory.coalgebraEquivOver X).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.Over.isoMk
          (CategoryTheory.Iso.refl
            (((CategoryTheory.overToCoalgebra X).comp (CategoryTheory.coalgebraToOver X)).obj f).left)
          ⋯)
      ⋯
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.incl_apply : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N), N.incl m = ↑m
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_le_iff_comap : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R₂ M₂}, f.range ≤ p ↔ Submodule.comap f p = ⊤
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpoint.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (signs : Finset (Fin (n + 1)))
  (i : Fin (n + 1)), s.touchpoint signs i = ↑((s.faceOpposite i).orthogonalProjectionSpan (s.excenter signs))
-- Mathlib.Topology.Sheaves.MayerVietoris
Opens.coe_mayerVietorisSquare_X₄ : ∀ {T : Type u} [inst : TopologicalSpace T] (U V : TopologicalSpace.Opens T),
  ↑(Opens.mayerVietorisSquare U V).X₄ = ↑U ∪ ↑V
-- Mathlib.Order.CompactlyGenerated.Basic
/-- **Alias** of the reverse direction of `CompleteLattice.wellFoundedGT_iff_isSupFiniteCompact`. -/
CompleteLattice.IsSupFiniteCompact.wellFoundedGT : ∀ (α : Type u_2) [inst : CompleteLattice α], CompleteLattice.IsSupFiniteCompact α → WellFoundedGT α
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.gcorec_some : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {F : β → Option (α × γ × β)} {op : γ → Stream'.Seq α → Stream'.Seq α}
  [inst : Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass op] {b : β} {a : α} {c : γ} {b' : β},
  F b = some (a, c, b') →
    Tactic.ComputeAsymptotics.Seq.gcorec F op b =
      Stream'.Seq.cons a (op c (Tactic.ComputeAsymptotics.Seq.gcorec F op b'))
-- Mathlib.Topology.Compactness.Compact
/-- **Alexander's subbasis theorem**. Suppose `X` is a topological space with a subbasis `S` and `s` is
a subset of `X`. Then `s` is compact if for any open cover of `s` with all elements taken from `S`,
there is a finite subcover.
 -/
isCompact_generateFrom : ∀ {X : Type u} [T : TopologicalSpace X] {S : Set (Set X)},
  T = TopologicalSpace.generateFrom S → ∀ {s : Set X}, (∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q) → IsCompact s
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_subset_of_le : ∀ {a b : Ordinal.{u}}, a ≤ b → ZFSet.vonNeumann a ⊆ ZFSet.vonNeumann b
-- Plausible.Arbitrary
/-- The `Arbitrary` typeclass represents types for which there exists a
random generator suitable for property-based testing.
- This is the equivalent of Haskell QuickCheck's `Arbitrary` typeclass.
- In QuickChick, this typeclass is called `Gen`, but `Gen` is already
a reserved keyword in Plausible, so we call this typeclass `Arbitrary`
following the Haskell QuickCheck convention).  -/
Plausible.Arbitrary : Type u → Type u
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_sInf : ∀ {G : Type u_2} [inst : AddGroup G] (S : Set (AddSubgroup G)), (sInf S).op = sInf (AddSubgroup.unop ⁻¹' S)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The natural labelling of `RootPairing.EmbeddedG2.allRoots`.  -/
RootPairing.EmbeddedG2.indexEquivAllRoots : {ι : 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) →
                    [inst_5 : P.EmbeddedG2] →
                      [Finite ι] →
                        [CharZero R] →
                          [IsDomain R] → [P.IsIrreducible] → ι ≃ ↥(RootPairing.EmbeddedG2.allRoots P).toFinset
-- Mathlib.Topology.Homotopy.Equiv
Homeomorph.refl_toHomotopyEquiv : ∀ (X : Type u) [inst : TopologicalSpace X], (Homeomorph.refl X).toHomotopyEquiv = ContinuousMap.HomotopyEquiv.refl X
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasTerminal_op_of_hasInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasInitial C],
  CategoryTheory.Limits.HasTerminal Cᵒᵖ
-- Init.Data.Format.Basic
Std.Format.instInhabitedFlattenBehavior : Inhabited Std.Format.FlattenBehavior
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_measure_zero' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {f : α → E} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → μ s = 0) → MeasureTheory.setToFun μ T hT f = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.insert k).max?.isSome = true
-- Mathlib.Topology.Category.Compactum
_private.Mathlib.Topology.Category.Compactum.0.Compactum.basic_inter : ∀ {X : Compactum} (A B : Set X.A), Compactum.basic✝ (A ∩ B) = Compactum.basic✝ A ∩ Compactum.basic✝ B
-- Mathlib.Algebra.Colimit.DirectLimit
/-- The canonical map from a component to the direct limit.  -/
DirectLimit.Algebra.of : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      (G : ι → Type u_3) →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : CommSemiring R] →
                    [inst_5 : (i : ι) → Semiring (G i)] →
                      [inst_6 : (i : ι) → Algebra R (G i)] →
                        [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] →
                          [inst_8 : Nonempty ι] → (i : ι) → G i →ₐ[R] DirectLimit G f
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.count_span_normalizedFactors_eq_of_normUnit : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] [inst_4 : DecidableEq R] {r X : R},
  r ≠ 0 →
    normUnit X = 1 →
      Prime X →
        Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) =
          Multiset.count X (UniqueFactorizationMonoid.normalizedFactors r)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonUnitalNonAssocCommSemiringOfNonUnitalRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalNonAssocCommSemiring (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                      NonUnitalNonAssocCommSemiring (DirectLimit G f)
-- Mathlib.Algebra.Category.Grp.Basic
/-- The category of additive groups and group morphisms.  -/
AddCommGrpCat : Type (u + 1)
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.PublishDiagnosticsParams.mk : Lean.Lsp.DocumentUri → Option ℤ → Option Bool → Array Lean.Lsp.Diagnostic → Lean.Lsp.PublishDiagnosticsParams
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.erase_emptyc : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {k : α}, ∅.erase k = ∅
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nat_mul_two_pi_add_pi : ∀ (n : ℕ), Real.cos (↑n * (2 * Real.pi) + Real.pi) = -1
-- Mathlib.Topology.Perfect
/-- In a T1 space, being preperfect is equivalent to having perfect closure.  -/
preperfect_iff_perfect_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [T1Space α], Preperfect C ↔ Perfect (closure C)
-- Init.Data.UInt.Lemmas
UInt8.toNat_mod_uInt32Size : ∀ (n : UInt8), n.toNat % UInt32.size = n.toNat
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHom₂WhiskerRight : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f g : a ⟶ b} →
        (η : f ⟶ g) →
          [inst_1 : Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
            [inst_2 : Mathlib.Tactic.BicategoryCoherence.LiftHom g] →
              [Mathlib.Tactic.BicategoryCoherence.LiftHom₂ η] →
                {h : b ⟶ c} →
                  [inst_4 : Mathlib.Tactic.BicategoryCoherence.LiftHom h] →
                    Mathlib.Tactic.BicategoryCoherence.LiftHom₂ (CategoryTheory.Bicategory.whiskerRight η h)
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator.operating.injEq : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  [inst : String.Slice.Pattern.ToForwardSearcher pat σ] (currPos : s.Pos)
  (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) (currPos_1 : s.Pos)
  (searcher_1 : Std.Iter (String.Slice.Pattern.SearchStep s)),
  (String.Slice.SplitInclusiveIterator.operating currPos searcher =
      String.Slice.SplitInclusiveIterator.operating currPos_1 searcher_1) =
    (currPos = currPos_1 ∧ searcher = searcher_1)
-- Batteries.Recycling.RBTree.WF
/-- `O(n)`. Map a function on every value in the set.
This requires `IsMonotone` on the function in order to preserve the order invariant.
If the function is not monotone, use `RBSet.map` instead.
 -/
RBTree.RBSet.mapMonotone : {α : Type u_1} →
  {β : Type u_2} →
    {cmpα : α → α → Ordering} →
      {cmpβ : β → β → Ordering} →
        (f : α → β) → [RBTree.RBNode.IsMonotone cmpα cmpβ f] → RBTree.RBSet α cmpα → RBTree.RBSet β cmpβ