mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Matrix.det_sum_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [Nontrivial R] [inst_2 : CommRing S] [inst_3 : LinearOrder S]
  [IsStrictOrderedRing S] {n : Type u_3} [inst_5 : Fintype n] [inst_6 : DecidableEq n] {ι : Type u_4} (s : Finset ι)
  {A : ι → Matrix n n R} {abv : AbsoluteValue R S} {x : S},
  (∀ (k : ι) (i j : n), abv (A k i j) ≤ x) →
    abv (∑ k ∈ s, A k).det ≤ (Fintype.card n).factorial • (s.card • x) ^ Fintype.card n
-- Mathlib.Algebra.Order.Kleene
kstar_one : ∀ {α : Type u_1} [inst : KleeneAlgebra α], KStar.kstar 1 = 1
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
/-- A class describing the property of reflecting finite effective epimorphic families.
 -/
CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} → [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.AlgebraicTopology.Reedy.Basic
HomotopicalAlgebra.ReedyStructure.unique : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [inst_1 : W₁.IsMultiplicative] [inst_2 : W₂.IsMultiplicative] {α : Type u_2} [inst_3 : LinearOrder α]
  [inst_4 : OrderBot α] [inst_5 : SuccOrder α] [inst_6 : WellFoundedLT α]
  (r : HomotopicalAlgebra.ReedyStructure W₁ W₂ α) {X Y : C} {f : X ⟶ Y} (fac fac' : W₁.MapFactorizationData W₂ f),
  ∃ (h : fac.Z = fac'.Z),
    fac.i = CategoryTheory.CategoryStruct.comp fac'.i (CategoryTheory.eqToHom ⋯) ∧
      fac.p = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h) fac'.p
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_mulRight₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : MeasurableSpace G₀] [inst_2 : MeasurableMul G₀] {g : G₀}
  (hg : g ≠ 0), (MeasurableEquiv.mulRight₀ g hg).symm = MeasurableEquiv.mulRight₀ g⁻¹ ⋯
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- A functorial choice of pullbacks along a morphism `f : Y ⟶ X` in `C` given by a functor
`Over X ⥤ Over Y` which is a right adjoint to the functor `Over.map f`.  -/
CategoryTheory.ChosenPullbacksAlong : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {Y X : C} → (Y ⟶ X) → Type (max u₁ v₁)
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.ι_mapBifunctorRightUnitor_hom_apply : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
  (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D)
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
          ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
      p]
  (j : J),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorMapObj F p X ((CategoryTheory.GradedObject.single₀ I).obj Y) j 0 j ⋯)
      ((CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X).hom j) =
    CategoryTheory.CategoryStruct.comp ((F.obj (X j)).map (CategoryTheory.GradedObject.singleObjApplyIso 0 Y).hom)
      (e.hom.app (X j))
-- Init.Data.List.MinMax
List.min_cons_cons : ∀ {α : Type u_1} [inst : Min α] {a b : α} {l : List α}, (a :: b :: l).min ⋯ = (a ⊓ b :: l).min ⋯
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1IsoOfIsTrivial_H1π_apply_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} [inst_2 : A.IsTrivial]
  (f : ↥(groupCohomology.cocycles₁ A)) (x : Additive G),
  ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1IsoOfIsTrivial A).hom)
        ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π A)) f))
      x =
    f (Additive.toMul x)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.AssociatorBimod.inv_hom_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U),
  CategoryTheory.CategoryStruct.comp (Bimod.AssociatorBimod.inv P Q L) (Bimod.AssociatorBimod.hom P Q L) =
    CategoryTheory.CategoryStruct.id (P.tensorBimod (Q.tensorBimod L)).X
-- Mathlib.RingTheory.Flat.Stability
Module.Flat.of_isLocalizedModule : ∀ {R : Type u} {M : Type u_1} {Mp : Type u_2} (Rp : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring Rp] [inst_4 : Algebra R Rp] [inst_5 : AddCommMonoid Mp]
  [inst_6 : Module R Mp] [inst_7 : Module Rp Mp] [IsScalarTower R Rp Mp] [Module.Flat R M] (S : Submonoid R)
  [IsLocalization S Rp] (f : M →ₗ[R] Mp) [h : IsLocalizedModule S f], Module.Flat Rp Mp
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)} {he : (t.alter k f).isEmpty = false},
  (t.alter k f).minKey he = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalBoolExprCore : Lean.Expr → Lean.MetaM Bool
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
algebraMap_galRestrict_apply : ∀ (A : Type u_1) {K : Type u_2} {L : Type u_3} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : IsFractionRing A K]
  [inst_7 : Algebra K L] [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : Algebra B L]
  [inst_11 : IsScalarTower A B L] [inst_12 : IsIntegralClosure B A L] [inst_13 : Algebra.IsAlgebraic K L] (σ : Gal(L/K))
  (x : B), (algebraMap B L) (((galRestrict A K L B) σ) x) = σ ((algebraMap B L) x)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1SCLM_add_left : ∀ {α : 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 T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (f : ↥(α →₁ₛ[μ] E)),
  (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ ⋯) f =
    (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f + (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT') f
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.isOpen_of_isLowerSet : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α] [t : TopologicalSpace α]
  [Topology.IsScottHausdorff α D], IsLowerSet D → IsLowerSet s → IsOpen s
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The pullback of a height one prime in `B` to `A`.  -/
IsDedekindDomain.HeightOneSpectrum.under : (A : Type u_4) →
  [inst : CommRing A] →
    [IsDomain A] →
      {B : Type u_6} →
        [inst_2 : CommRing B] →
          [IsDomain B] →
            [inst_4 : Algebra A B] →
              [Algebra.IsIntegral A B] → IsDedekindDomain.HeightOneSpectrum B → IsDedekindDomain.HeightOneSpectrum A
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.instHasDimensionLTToSSetHorn : ∀ {n : ℕ} (i : Fin (n + 1)), (SSet.horn n i).toSSet.HasDimensionLT n
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_eq_getValueD : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α} {fallback : β}
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValue a l h = Std.Internal.List.getValueD a l fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.isEmpty = false
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.inductionOn : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} (f : l.Germ β) {p : l.Germ β → Prop}, (∀ (f : α → β), p ↑f) → p f
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.instIsCentralScalar : ∀ {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [inst_4 : Monoid R']
  [inst_5 : Semiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : DistribMulAction R' N]
  [inst_9 : ContinuousConstSMul R' N] [inst_10 : SMulCommClass A R' N] [inst_11 : DistribMulAction R'ᵐᵒᵖ N]
  [inst_12 : IsCentralScalar R' N], IsCentralScalar R' (M [⋀^ι]→L[A] N)
-- Init.Prelude
/-- Like `node` but for trailing parsers (which start with a nonterminal).
Assumes the lhs is already on the stack, and parses using `p`, then pops the
stack including the lhs to create a new node with kind `kind`.
The precedence `prec` and `lhsPrec` are used to determine whether the parser
should apply.  -/
Lean.ParserDescr.trailingNode : Lean.SyntaxNodeKind → ℕ → ℕ → Lean.ParserDescr → Lean.ParserDescr
-- Mathlib.RingTheory.Localization.AsSubring
Localization.subalgebra.ofField.eq_1 : ∀ {A : Type u_1} (K : Type u_2) [inst : CommRing A] (S : Submonoid A) (hS : S ≤ nonZeroDivisors A) [inst_1 : Field K]
  [inst_2 : Algebra A K] [inst_3 : IsFractionRing A K],
  Localization.subalgebra.ofField K S hS =
    (Localization.mapToFractionRing K S (Localization S) hS).range.copy
      {x | ∃ a s, ∃ (_ : s ∈ S), x = (algebraMap A K) a * ((algebraMap A K) s)⁻¹} ⋯
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.reflectsEpimorphisms_of_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Faithful], F.ReflectsEpimorphisms
-- Mathlib.Algebra.Order.ToIntervalMod
AddCommGroup.modEq_iff_forall_notMem_Ioo_mod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [hα : Archimedean α] {p : α},
  0 < p → ∀ {a b : α}, a ≡ b [PMOD p] ↔ ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.extension₂_coe_coe : ∀ {α : Type u_1} [inst : UniformSpace α] {β : Type u_2} [inst_1 : UniformSpace β] {γ : Type u_3}
  [inst_2 : UniformSpace γ] {f : α → β → γ} [T0Space γ],
  UniformContinuous₂ f → ∀ (a : α) (b : β), UniformSpace.Completion.extension₂ f ↑a ↑b = f a b
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- The composition of a meromorphic function in normal form and an analytic
function is meromorphic in normal form.
 -/
MeromorphicNFAt.comp_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {g : 𝕜 → 𝕜} {x : 𝕜},
  MeromorphicNFAt f (g x) → AnalyticAt 𝕜 g x → MeromorphicNFAt (f ∘ g) x
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_neBot : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  (MeasureTheory.ae (μ.restrict s)).NeBot ↔ μ s ≠ 0
-- Plausible.Gen
/-- Apply a function to the size parameter.  -/
Plausible.Gen.resize : {α : Type u_1} → (ℕ → ℕ) → Plausible.Gen α → Plausible.Gen α
-- Mathlib.Topology.Order.Basic
nhdsLE_basis_of_exists_lt : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a : α},
  (∃ u, u < a) → (nhdsWithin a (Set.Iic a)).HasBasis (fun u => u < a) fun u => Set.Ioc u a
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- An integral subalgebra of a division ring over a field is closed under inverses.  -/
Algebra.IsIntegral.inv_mem : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : DivisionRing S] [inst_2 : Algebra R S] {x : S}
  {A : Subalgebra R S} [Algebra.IsIntegral R ↥A], x ∈ A → x⁻¹ ∈ A
-- Mathlib.Data.Fin.SuccPred
Fin.coe_eq_castSucc : ∀ {n : ℕ} {a : Fin n}, ↑↑a = a.castSucc
-- Init.Grind.Config
Lean.Grind.NoopConfig.mk.inj : ∀ {toConfig toConfig_1 : Lean.Grind.Config},
  { toConfig := toConfig } = { toConfig := toConfig_1 } → toConfig = toConfig_1
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Choice.mk : List Lean.Meta.Grind.EMatch.Cnstr →
  ℕ → Array Lean.Expr → Lean.PHashSet Lean.Meta.Grind.EMatchDiagNode → Lean.Meta.Grind.EMatch.Choice
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, k ∉ t₂ → Std.DTreeMap.Const.get! (t₁ \ t₂) k = Std.DTreeMap.Const.get! t₁ k
-- Mathlib.Data.Sigma.Basic
Sigma.forall' : ∀ {α : Type u_1} {β : α → Type u_4} {p : (a : α) → β a → Prop},
  (∀ (a : α) (b : β a), p a b) ↔ ∀ (x : (a : α) × β a), p x.fst x.snd
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t'_iij : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J),
  D.t' i i j = (CategoryTheory.Limits.pullbackSymmetry (D.f i i) (D.f i j)).hom
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.compl_notMem_iff : ∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, sᶜ ∉ f ↔ s ∈ f
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toNonUnitalStarAlgHom_symm_ofNonUnitalStarAlgHom : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁]
  [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁] [inst_4 : NonUnitalNonAssocSemiring A₂]
  [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂] (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₁)
  (h₁ : g.comp f = NonUnitalStarAlgHom.id R A₁) (h₂ : f.comp g = NonUnitalStarAlgHom.id R A₂),
  (StarAlgEquiv.ofNonUnitalStarAlgHom f g h₁ h₂).symm.toNonUnitalStarAlgHom = g
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.image_insert_memberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] (𝒜 : Finset (Finset α)) (a : α),
  Finset.image (insert a) (Finset.memberSubfamily a 𝒜) = {s ∈ 𝒜 | a ∈ s}
-- Mathlib.Topology.UniformSpace.AbstractCompletion
_private.Mathlib.Topology.UniformSpace.AbstractCompletion.0.AbstractCompletion.termMap : Lean.ParserDescr
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.smul_toFun : ∀ {t : Tactic.ComputeAsymptotics.Monomial} {basis : Tactic.ComputeAsymptotics.Basis} (c : ℝ),
  (t.smul c).toFun basis = c • t.toFun basis
-- Mathlib.Algebra.Polynomial.OfFn
/-- If `i < n` the `i`-th coefficient of `ofFn n v` is `v i`.  -/
Polynomial.ofFn_coeff_eq_val_of_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] {n i : ℕ} (v : Fin n → R) (hi : i < n),
  ((Polynomial.ofFn n) v).coeff i = v ⟨i, hi⟩
-- Std.Data.TreeSet.Basic
/-- Removes all elements from the tree set for which the given function returns `false`.  -/
Std.TreeSet.filter : {α : Type u} → {cmp : α → α → Ordering} → (α → Bool) → Std.TreeSet α cmp → Std.TreeSet α cmp
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_algEquiv : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B) (x : A),
  Polynomial.aeval (f x) = (↑f).comp (Polynomial.aeval x)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.colimitsOfShape_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.op.colimitsOfShape J = (P.limitsOfShape Jᵒᵖ).op
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.AffineZariskiSite.basicOpen.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (U : X.AffineZariskiSite) (f : ↑(X.presheaf.obj (Opposite.op U.toOpens))),
  U.basicOpen f = ⟨X.basicOpen f, ⋯⟩
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.then_eq : ∀ (o₁ o₂ : Ordering), o₁.then o₂ = Ordering.eq ↔ o₁ = Ordering.eq ∧ o₂ = Ordering.eq
-- Init.Data.String.Basic
ByteArray.validateUTF8_eq_true_iff : ∀ {b : ByteArray}, b.validateUTF8 = true ↔ b.IsValidUTF8
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} [MeasureTheory.IsFiniteMeasure μ] [ProbabilityTheory.IsFiniteKernel κ],
  MeasureTheory.IsFiniteMeasure (μ.bind ⇑κ)
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDerivAux.congr_simp : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ κ_1 : ProbabilityTheory.Kernel α γ),
  κ = κ_1 →
    ∀ (η η_1 : ProbabilityTheory.Kernel α γ),
      η = η_1 → ∀ (a a_1 : α), a = a_1 → ∀ (x x_1 : γ), x = x_1 → κ.rnDerivAux η a x = κ_1.rnDerivAux η_1 a_1 x_1
-- Init.Data.Vector.Basic
Vector.Mem.val : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {a : α}, xs.Mem a → a ∈ xs.toArray
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (hom : S₁ ⟶ S₂) (inv : S₂ ⟶ S₁)
  (homotopyHomInvId :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp hom inv)
      (CategoryTheory.CategoryStruct.id S₁))
  (homotopyInvHomId :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp inv hom)
      (CategoryTheory.CategoryStruct.id S₂))
  (hom_1 : S₁ ⟶ S₂) (inv_1 : S₂ ⟶ S₁)
  (homotopyHomInvId_1 :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp hom_1 inv_1)
      (CategoryTheory.CategoryStruct.id S₁))
  (homotopyInvHomId_1 :
    CategoryTheory.ShortComplex.Homotopy (CategoryTheory.CategoryStruct.comp inv_1 hom_1)
      (CategoryTheory.CategoryStruct.id S₂)),
  ({ hom := hom, inv := inv, homotopyHomInvId := homotopyHomInvId, homotopyInvHomId := homotopyInvHomId } =
      { hom := hom_1, inv := inv_1, homotopyHomInvId := homotopyHomInvId_1, homotopyInvHomId := homotopyInvHomId_1 }) =
    (hom = hom_1 ∧ inv = inv_1 ∧ homotopyHomInvId ≍ homotopyHomInvId_1 ∧ homotopyInvHomId ≍ homotopyInvHomId_1)
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalAddGroup.tendstoUniformly_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddGroup G] [u : UniformSpace G]
  [inst_1 : IsTopologicalAddGroup G] (F : ι → α → G) (f : α → G) (p : Filter ι),
  IsTopologicalAddGroup.rightUniformSpace G = u →
    (TendstoUniformly F f p ↔ ∀ u_1 ∈ nhds 0, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a - f a ∈ u_1)
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.String.Slice.contains.match_1.eq_1 : ∀ (s : String.Slice) (motive : String.Slice.Pattern.SearchStep s → Sort u_1) (startPos endPos : s.Pos)
  (h_1 : (startPos endPos : s.Pos) → motive (String.Slice.Pattern.SearchStep.matched startPos endPos))
  (h_2 : (x : String.Slice.Pattern.SearchStep s) → motive x),
  (match String.Slice.Pattern.SearchStep.matched startPos endPos with
    | String.Slice.Pattern.SearchStep.matched startPos endPos => h_1 startPos endPos
    | x => h_2 x) =
    h_1 startPos endPos
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.dist_top : ∀ {V : Type u_1} {u v : V} [inst : DecidableEq V], ⊤.dist u v = if u = v then 0 else 1
-- Mathlib.Order.Heyting.Hom
/-- Composition of `CoheytingHom`s as a `CoheytingHom`.  -/
CoheytingHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : CoheytingAlgebra α] →
        [inst_1 : CoheytingAlgebra β] →
          [inst_2 : CoheytingAlgebra γ] → CoheytingHom β γ → CoheytingHom α β → CoheytingHom α γ
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.closure_mul_le : ∀ {G : Type u_2} [inst : Group G] (S T : Set G), Subgroup.closure (S * T) ≤ Subgroup.closure S ⊔ Subgroup.closure T
-- Mathlib.Control.ULiftable
/-- A version of `down` for a `PUnit` return type.  -/
ULiftable.down' : {f : Type u₀ → Type u₁} → {g : Type v₀ → Type v₁} → [ULiftable f g] → g PUnit.{v₀ + 1} → f PUnit.{u₀ + 1}
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.map_comap_incl : ∀ {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 N' : LieSubmodule R L M),
  LieSubmodule.map N.incl (LieSubmodule.comap N.incl N') = N ⊓ N'
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.bot : ∀ {R : Type u_1} [inst : CommRing R] (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M], IsAdicComplete ⊥ M
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
SSet.prodStdSimplex.nonDegenerateEquiv₁_fst : ∀ {p : ℕ} (i : Fin (p + 1)),
  (↑(SSet.prodStdSimplex.nonDegenerateEquiv₁ i)).1 = SSet.stdSimplex.objEquiv.symm (SimplexCategory.σ i)
-- Mathlib.Algebra.BigOperators.Finprod
/-- If `f a = 1`, then the product of `f i` over `i ∈ insert a s` equals the product of `f i` over
`i ∈ s`.  -/
finprod_mem_insert_one : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a : α} {s : Set α},
  f a = 1 → ∏ᶠ (i : α) (_ : i ∈ insert a s), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Init.Data.Vector.Lemmas
Vector.contains_flatMap : ∀ {β : Type u_1} {α : Type u_2} {n m : ℕ} [inst : BEq β] {xs : Vector α n} {f : α → Vector β m} {x : β},
  (xs.flatMap f).contains x = xs.any fun a => (f a).contains x
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_apply_apply_mk : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B},
  b ∈ e.baseSet → ∀ (y : E b), e.symm b (↑e ⟨b, y⟩).2 = y
-- Mathlib.Topology.Connected.Basic
connectedSpace_iff_univ : ∀ {α : Type u} [inst : TopologicalSpace α], ConnectedSpace α ↔ IsConnected Set.univ
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity.sizeOf_spec : ∀ {A B : GrpCat} {f : A ⟶ B}, sizeOf GrpCat.SurjectiveOfEpiAuxs.XWithInfinity.infinity = 1
-- Mathlib.Topology.Algebra.Group.Basic
continuousInv_sInf : ∀ {G : Type w} [inst : Inv G] {ts : Set (TopologicalSpace G)}, (∀ t ∈ ts, ContinuousInv G) → ContinuousInv G
-- Mathlib.Analysis.Convex.Quasiconvex
Monotone.quasiconvexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : PartialOrder β] [inst_6 : Module 𝕜 E] [PosSMulMono 𝕜 E]
  {f : E → β}, Monotone f → QuasiconvexOn 𝕜 Set.univ f
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instInhabited.eq_1 : CommMonCat.instInhabited = { default := CommMonCat.of PUnit.{u_1 + 1} }
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.exists_isoModSerre_comp_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y),
  (∃ X' s, ∃ (_ : P.isoModSerre s), CategoryTheory.CategoryStruct.comp s f = 0) ↔ P (CategoryTheory.Abelian.image f)