mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.fst_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B]
  [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : Star C] (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C),
  (StarAlgHom.fst R B C).comp (f.prod g) = f
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.Equivalence.sheafCongr.functor_map_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D) (e : C ≌ D) (A : Type u₃)
  [inst_2 : CategoryTheory.Category.{v₃, u₃} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite K J e.inverse]
  {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongr.functor J K e A).map f).hom.app X_1 =
    f.hom.app (Opposite.op (e.inverse.obj (Opposite.unop X_1)))
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem.0.MvPolynomial.supDegree_monic_esymm : ∀ {R : Type u_3} {m : ℕ} [inst : CommSemiring R] [Nontrivial R] {i : ℕ} (him : i < m),
  AddMonoidAlgebra.supDegree (⇑toLex) (MvPolynomial.esymm (Fin m) R (i + 1)) =
      toLex (Finsupp.indicator (Finset.Iic ⟨i, him⟩) fun x x_1 => 1) ∧
    AddMonoidAlgebra.Monic (⇑toLex) (MvPolynomial.esymm (Fin m) R (i + 1))
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.liftCover_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {ι : Type u_5} {S : ι → Set α}
  {φ : (i : ι) → C(↑(S i), β)}
  {hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩}
  {hS : ∀ (x : α), ∃ i, S i ∈ nhds x} {i : ι}, ContinuousMap.restrict (S i) (ContinuousMap.liftCover S φ hφ hS) = φ i
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
  ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | 1 => x) = 0
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Disc
Matrix.discr_conj : ∀ {R : Type u_1} {n : Type u_2} [inst : CommRing R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (g : GL n R)
  (m : Matrix n n R), (↑g * m * (↑g)⁻¹).discr = m.discr
-- Mathlib.Topology.Connected.PathComponentOne
OpenNormalSubgroup.pathComponentOne_carrier : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyPathConnectedSpace G], ↑(OpenNormalSubgroup.pathComponentOne G) = pathComponent 1
-- Lean.Structure
/-- Returns the name of the auxiliary definition for a default value for the field, even if inherited, if any such definition exists.
 -/
Lean.getEffectiveDefaultFnForField? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.rightOp_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ D) (X : Dᵒᵖ), e.rightOp.counitIso.hom.app X = (e.counitIso.inv.app (Opposite.unop X)).op
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_map_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {δ : Type u_4} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β) {f : β → γ}
  {g : β → δ}, Measurable g → (κ.map fun x => (f x, g x)).fst = κ.map f
-- Mathlib.Topology.NhdsWithin
/-- **Alias** of `sdiff_mem_nhdsWithin_sdiff`. -/
diff_mem_nhdsWithin_diff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s t : Set α},
  s ∈ nhdsWithin x t → ∀ (t' : Set α), s \ t' ∈ nhdsWithin x (t \ t')
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.isGround.sizeOf_spec : ∀ (bvarIdx : ℕ), sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.isGround bvarIdx) = 1 + sizeOf bvarIdx
-- Mathlib.Algebra.CharP.Two
CharTwo.ofNat_eq_mod : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharP R 2] (n : ℕ) [inst_2 : n.AtLeastTwo],
  OfNat.ofNat n = ↑(OfNat.ofNat n % 2)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Given two functors `L : C ⥤ D` and `F : C ⥤ H`, this is the category of functors
`F' : D ⥤ H` equipped with a natural transformation `F ⟶ L ⋙ F'`.  -/
CategoryTheory.Functor.LeftExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            CategoryTheory.Functor C D →
              CategoryTheory.Functor C H → Type (max (max (max (max u_3 u_4) v_3) v_4) u_1 v_3)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.diff_eq_diffₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.diff m₂ = m₁.diffₘ m₂
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- An instance of the `CooperSplitPred` at `k`.
 -/
Lean.Meta.Grind.Arith.Cutsat.CooperSplit : Type
-- Lean.Parser.Term
Lean.Parser.Term.idbg.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Order.Ord
Array.instLawfulEqOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.LawfulEqOrd α], Std.LawfulEqOrd (Array α)
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
/-- the coercion from two-sided-ideals to sets is an order embedding
 -/
TwoSidedIdeal.coeOrderEmbedding : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → TwoSidedIdeal R ↪o Set R
-- Mathlib.Algebra.Ring.Basic
AddMonoidHom.coe_mul : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R], ⇑AddMonoidHom.mul = AddMonoidHom.mulLeft
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_X_pow_sub_C : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] {n : ℕ},
  0 < n → ∀ (a : R), (Polynomial.X ^ n - Polynomial.C a).degree = ↑n
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_nsmul : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (n : ℕ) (a : M) (b : ↥S),
  n • AddLocalization.mk a b = AddLocalization.mk (n • a) (n • b)
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The colimit cocone over any functor from a finite diagram into a `SemilatticeSup` with `OrderBot`.
 -/
CategoryTheory.Limits.CompleteLattice.finiteColimitCocone : {α : Type u} →
  {J : Type w} →
    [inst : CategoryTheory.SmallCategory J] →
      [CategoryTheory.FinCategory J] →
        [inst_2 : SemilatticeSup α] →
          [OrderBot α] → (F : CategoryTheory.Functor J α) → CategoryTheory.Limits.ColimitCocone F
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} {fallback : β}, (t₁ ∩ t₂).getD k fallback = if k ∈ t₂ then t₁.getD k fallback else fallback
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
/-- The cardinality of even permutations of given `cycleType`  -/
AlternatingGroup.card_of_cycleType_mul_eq : ∀ (α : Type u_1) [inst : Fintype α] [inst_1 : DecidableEq α] (m : Multiset ℕ),
  {g | (↑g).cycleType = m}.card *
      ((Fintype.card α - m.sum).factorial * m.prod * ∏ n ∈ m.toFinset, (Multiset.count n m).factorial) =
    if (m.sum ≤ Fintype.card α ∧ ∀ a ∈ m, 2 ≤ a) ∧ Even (m.sum + m.card) then (Fintype.card α).factorial else 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.minKey_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {h' : t₁.isEmpty = false} (h : t₁.Equiv t₂), t₁.minKey h' = t₂.minKey ⋯
-- Mathlib.Analysis.Complex.Norm
Complex.norm_le_sqrt_two_mul_max : ∀ (z : ℂ), ‖z‖ ≤ √2 * max |z.re| |z.im|
-- Init.Data.Array.Lemmas
List.take_toArray : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.toArray.take i = (List.take i l).toArray
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofNatLT : ∀ {n : ℕ} (h : n < UInt32.size), (UInt32.ofNatLT n h).toUInt64 = UInt64.ofNatLT n ⋯
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.instInhabitedRewriteLemma : Inhabited Mathlib.Tactic.LibraryRewrite.RewriteLemma
-- Mathlib.Algebra.Ring.NonZeroDivisors
isRightRegular_iff_mem_nonZeroDivisorsRight : ∀ {R : Type u_1} [inst : Ring R] {r : R}, IsRightRegular r ↔ r ∈ nonZeroDivisorsRight R
-- Mathlib.Tactic.Linter.TextBased
/-- A line contains trailing whitespace.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.trailingWhitespace : Mathlib.Linter.TextBased.StyleError✝
-- Init.Data.BitVec.Lemmas
BitVec.flattenList_zero_length : ∀ (vs : List (BitVec 0)), BitVec.flattenList vs = 0
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.toFn.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), Polynomial.toFn n = LinearMap.pi fun i => Polynomial.lcoeff R ↑i
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.aemeasurable_lintegral : ∀ {α : Type u_1} {mα : MeasurableSpace α} {m : MeasureTheory.Measure (MeasureTheory.Measure α)} {f : α → ENNReal},
  AEMeasurable f m.join → AEMeasurable (fun μ => ∫⁻ (a : α), f a ∂μ) m
-- Mathlib.Order.Antichain
IsStrongAntichain.subsingleton : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsDirected α r], IsStrongAntichain r s → s.Subsingleton
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.one_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.one.mul x) x
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₁_comp : ∀ {X Y : TopCat} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp TopCat.ι₁ (CategoryTheory.MonoidalCategoryStruct.whiskerRight f TopCat.I) =
    CategoryTheory.CategoryStruct.comp f TopCat.ι₁
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The data of a term in `MapFactorizationData W₁ W₂ f` for any morphism `f`.  -/
CategoryTheory.MorphismProperty.FactorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Type (max u_1 v_1)
-- Init.Data.Option.Lemmas
Option.isEqSome.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (x a : α), (some a).isEqSome x = (a == x)
-- Mathlib.Topology.Algebra.Group.Basic
/-- The map `(x, y) ↦ (x, x * y)` as a homeomorphism. This is a shear mapping.  -/
Homeomorph.shearMulRight : (G : Type w) → [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → G × G ≃ₜ G × G
-- Mathlib.Topology.Constructions.SumProd
isInducing_prodMkLeft : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (y : Y),
  Topology.IsInducing fun x => (x, y)
-- Mathlib.Analysis.Complex.Order
Complex.zero_lt_real : ∀ {x : ℝ}, 0 < ↑x ↔ 0 < x
-- Mathlib.RingTheory.RingHom.Surjective
/-- `R →+* S` is surjective if there exists a set `{ r }` that spans `R` such that
`Rᵣ →+* Sᵣ` is surjective.  -/
RingHom.surjective_ofLocalizationSpan : RingHom.OfLocalizationSpan fun {X Y} [CommRing X] [CommRing Y] f => Function.Surjective ⇑f
-- Mathlib.Analysis.Convex.Star
StarConvex.mem_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {x : E} {s : Set E},
  StarConvex 𝕜 0 s → x ∈ s → ∀ {t : 𝕜}, 1 ≤ t → x ∈ t • s
-- Init.Data.UInt.Lemmas
UInt8.ofNat_uSizeToNat : ∀ (n : USize), UInt8.ofNat n.toNat = n.toUInt8
-- Mathlib.Algebra.Algebra.Equiv
LinearEquiv.algEquivOfRing_symm_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (e : R ≃ₗ[R] A)
  (x : A), e.algEquivOfRing.symm x = e.symm (e 1 * x)
-- Mathlib.ModelTheory.LanguageMap
_private.Mathlib.ModelTheory.LanguageMap.0.FirstOrder.Language.constantsOnFunc.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.liftNCRingHom.eq_1 : ∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : AddMonoid G] [inst_2 : Semiring R]
  (f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ (x : k) (y : Multiplicative G), Commute (f x) (g y)),
  AddMonoidAlgebra.liftNCRingHom f g h_comm =
    { toFun := (↑(AddMonoidAlgebra.liftNC ↑f ⇑g)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- If `n % 4 = 3`, then `χ₄ n = -1`.  -/
ZMod.χ₄_int_three_mod_four : ∀ {n : ℤ}, n % 4 = 3 → ZMod.χ₄ ↑n = -1
-- Mathlib.Data.Rat.Defs
Rat.divInt_ne_zero_of_ne_zero : ∀ {n d : ℤ}, n ≠ 0 → d ≠ 0 → Rat.divInt n d ≠ 0
-- Mathlib.Data.PNat.Prime
Nat.Primes.coePNat : Coe Nat.Primes ℕ+
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The morphism in the category of `ProfiniteAddGrp` from a profinite additive group
`P` to the projective limit of its quotients by open normal subgroups ordered by inclusion  -/
ProfiniteAddGrp.toLimit : (P : ProfiniteAddGrp.{u}) → P ⟶ ProfiniteAddGrp.limit P.diagram
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
/-- `MeasureTheory.Lp.const` as a `ContinuousLinearMap`.  -/
MeasureTheory.Lp.constL : {α : Type u_1} →
  {E : Type u_2} →
    {m : MeasurableSpace α} →
      (p : ENNReal) →
        (μ : MeasureTheory.Measure α) →
          [inst : NormedAddCommGroup E] →
            [MeasureTheory.IsFiniteMeasure μ] →
              (𝕜 : Type u_3) →
                [inst_2 : NormedRing 𝕜] →
                  [inst_3 : Module 𝕜 E] →
                    [inst_4 : IsBoundedSMul 𝕜 E] → [inst_5 : Fact (1 ≤ p)] → E →L[𝕜] ↥(MeasureTheory.Lp E p μ)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.biprodAddEquiv_apply_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X₁ X₂ Y : C} {n : ℕ} (e : CategoryTheory.Abelian.Ext (X₁ ⊞ X₂) Y n),
  (CategoryTheory.Abelian.Ext.biprodAddEquiv e).2 =
    (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.inr).comp e ⋯
-- Mathlib.Topology.Order
/-- The only open sets in the indiscrete topology are the empty set and the whole space.  -/
IndiscreteTopology.isOpen_iff : ∀ {α : Type u_1} {t₂ : TopologicalSpace α} [IndiscreteTopology α] (U : Set α), IsOpen U ↔ U = ∅ ∨ U = Set.univ
-- Mathlib.FieldTheory.SeparableDegree
/-- The separable degree of an irreducible polynomial divides its degree.  -/
Irreducible.natSepDegree_dvd_natDegree : ∀ {F : Type u} [inst : Field F] {f : Polynomial F}, Irreducible f → f.natSepDegree ∣ f.natDegree
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_discard : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsMarkovKernel κ], (ProbabilityTheory.Kernel.discard β).comp κ = ProbabilityTheory.Kernel.discard α
-- Mathlib.Topology.Bornology.Basic
/-- A finite space is bounded.  -/
BoundedSpace.of_finite : ∀ {α : Type u_4} [inst : Bornology α] [Finite α], BoundedSpace α
-- Mathlib.Order.OrderDual
OrderDual.instOrd : (α : Type u_2) → [h : Ord α] → Ord αᵒᵈ
-- Mathlib.CategoryTheory.Sums.Associator
/-- The associator functor `(C ⊕ D) ⊕ E ⥤ C ⊕ (D ⊕ E)` for sums of categories.
 -/
CategoryTheory.sum.associator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) → [inst_2 : CategoryTheory.Category.{v₃, u₃} E] → CategoryTheory.Functor ((C ⊕ D) ⊕ E) (C ⊕ D ⊕ E)
-- Mathlib.Data.Fintype.BigOperators
/-- Sum over a sigma type equals the repeated sum, curried version.
This version is useful to rewrite from right to left.  -/
Fintype.sum_sigma' : ∀ {ι : Type u_9} {α : ι → Type u_7} {M : Type u_8} [inst : Fintype ι] [inst_1 : (i : ι) → Fintype (α i)]
  [inst_2 : AddCommMonoid M] (f : (i : ι) → α i → M), ∑ x, f x.fst x.snd = ∑ x, ∑ y, f x y
-- Std.Do.PostCond
Std.Do.ExceptConds.and_false : ∀ {ps : Std.Do.PostShape} {x : Std.Do.ExceptConds ps}, (x ∧ₑ Std.Do.ExceptConds.false).entails Std.Do.ExceptConds.false
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingAfter_eq_sInf : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CompleteLattice ι] {u : ι → Ω → β} {s : Set β}
  [inst_1 : (ω : Ω) → Decidable (∃ j, u j ω ∈ s)] (ω : Ω),
  MeasureTheory.hittingAfter u s ⊥ ω = if ∃ j, u j ω ∈ s then ↑(sInf {i | u i ω ∈ s}) else ⊤
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelopeIter_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] {n m n' : ℕ},
  autoParam (n = n' + 1) CategoryTheory.ObjectProperty.triangEnvelopeIter_add._auto_1 →
    P.triangEnvelopeIter (n + m) = ((P.triangEnvelopeIter n').extensionProduct (P.triangEnvelopeIter m)).retractClosure
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_insert : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E) {s : Set E},
  Bornology.IsVonNBounded 𝕜 (insert x s) ↔ Bornology.IsVonNBounded 𝕜 s
-- Lean.Parser.Do
Lean.Parser.Term.doCatchMatch : Lean.Parser.Parser
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_toUInt8 : ∀ (n : UInt64), n.toUInt8.toUInt16 = n.toUInt16 % 256
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_iInter : ∀ {V : Type u} {ι : Sort u_2} {f : ι → Set (Sym2 V)},
  SimpleGraph.fromEdgeSet (⋂ i, f i) = ⨅ i, SimpleGraph.fromEdgeSet (f i)
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isMatch_iff : ∀ {pat s : String.Slice} {pos : s.Pos}, String.Slice.Pattern.Model.IsMatch pat pos ↔ (s.sliceTo pos).copy = pat.copy
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.d₁₂_comp_d₂₃_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u_1, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k (G × G × G → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.d₁₂ A)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.d₂₃ A) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_inj : ∀ {α : Type u_1} {M₁ M₂ : Matroid α}, M₁✶ = M₂✶ ↔ M₁ = M₂
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.dvd_iff_eq : ∀ {p a : ℕ}, Nat.Prime p → a ≠ 1 → (a ∣ p ↔ p = a)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.sum_const' : ∀ (ι : Type u) (a : Cardinal.{u}), (Cardinal.sum fun x => a) = Cardinal.mk ι * a
-- Std.Sync.Broadcast
/-- Maximum number of messages that can be buffered before producers block.
 -/
_private.Std.Sync.Broadcast.0.Std.Bounded.State.capacity : {α : Type} → Std.Bounded.State✝ α → { x // 0 < x }
-- Mathlib.Topology.UniformSpace.UniformEmbedding
/-- **Alias** of the forward direction of `isUniformInducing_iff_uniformSpace`. -/
IsUniformInducing.comap_uniformSpace : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β},
  IsUniformInducing f → UniformSpace.comap f inst_1 = inst
-- Init.MetaTypes
Lean.Meta.ExtractLetsConfig.mk : Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Lean.Meta.ExtractLetsConfig
-- Std.Time.Date.Unit.Week
Std.Time.Week.instOrdOffset : Ord Std.Time.Week.Offset
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback_hom_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C}
  (h_1 : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp h.isoPullback.hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h_1) =
    CategoryTheory.CategoryStruct.comp fst h_1
-- Lean.Parser.Extension
Lean.Parser.ParserAliasInfo : Type
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.beqModel.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : (k : α) → BEq (β k)]
  (l₁ l₂ : List ((a : α) × β a)),
  Std.Internal.List.beqModel l₁ l₂ =
    if l₁.length ≠ l₂.length then false else l₁.all fun x => Std.Internal.List.getValueCast? x.fst l₂ == some x.snd
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Let `t i` be a nonempty directed subfamily of `𝔖`
such that every `s ∈ 𝔖` is included in some `t i`.
Let `V` bounded by `p` be a basis of entourages of `β`.

Then `UniformOnFun.gen 𝔖 (t i) (V j)` bounded by `p j` is a basis of entourages of `α →ᵤ[𝔖] β`.  -/
UniformOnFun.hasBasis_uniformity_of_covering_of_basis : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] (𝔖 : Set (Set α)) {ι : Type u_5} {ι' : Type u_6} [Nonempty ι]
  {t : ι → Set α} {p : ι' → Prop} {V : ι' → Set (β × β)},
  (∀ (i : ι), t i ∈ 𝔖) →
    Directed (fun x1 x2 => x1 ⊆ x2) t →
      (∀ s ∈ 𝔖, ∃ i, s ⊆ t i) →
        (uniformity β).HasBasis p V →
          (uniformity (UniformOnFun α β 𝔖)).HasBasis (fun i => p i.2) fun i => UniformOnFun.gen 𝔖 (t i.1) (V i.2)
-- Std.Data.HashSet.Lemmas
Std.HashSet.equiv_iff_toList_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
-- Mathlib.Data.Sym.Sym2
Sym2.mk.eq_1 : ∀ {α : Type u_4} (a b : α), s(a, b) = Quot.mk (Sym2.Rel α) (a, b)
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.toSemiring_apply : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R] (f : (i : ι) → A i →+ R)
  (hone : (f 0) GradedMonoid.GOne.one = 1)
  (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj)
  (a : DirectSum ι fun i => A i), (DirectSum.toSemiring f hone hmul) a = (DirectSum.toAddMonoid f) a
-- Mathlib.Order.Interval.Finset.Basic
Finset.mem_uIcc' : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c : α},
  a ∈ Finset.uIcc b c ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b
-- Mathlib.Order.Fin.Tuple
monotone_vecEmpty : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Monotone ![a]
-- Mathlib.Analysis.Calculus.ContDiff.Basic
iteratedFDeriv_const_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ},
  n ≠ 0 → ∀ (c : F), (iteratedFDeriv 𝕜 n fun x => c) = 0
-- Mathlib.Combinatorics.Quiver.Path.Weight
/-- The additive weight of a path, where the weight of an edge is
defined by a function on its endpoints.  -/
Quiver.Path.addWeightOfEPs : {V : Type u_1} → [inst : Quiver V] → {R : Type u_2} → [AddMonoid R] → (V → V → R) → {i j : V} → Quiver.Path i j → R
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instAddOffset : Add Std.Time.Nanosecond.Offset
-- Mathlib.Data.Set.Pairwise.Basic
Set.Subsingleton.pairwise : ∀ {α : Type u_1} {s : Set α}, s.Subsingleton → ∀ (r : α → α → Prop), s.Pairwise r
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.instCoeTypeForall_3 : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.Topology.NhdsSet
/-- A proposition is true on a set neighborhood of `s` iff it is true on a larger open set  -/
eventually_nhdsSet_iff_exists : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {p : X → Prop},
  (∀ᶠ (x : X) in nhdsSet s, p x) ↔ ∃ t, IsOpen t ∧ s ⊆ t ∧ ∀ x ∈ t, p x