mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.NormalizedHom.cons.inj : ∀ {e : Mathlib.Tactic.BicategoryLike.Mor₁} {a : Mathlib.Tactic.BicategoryLike.NormalizedHom}
  {a_1 : Mathlib.Tactic.BicategoryLike.Atom₁} {e_1 : Mathlib.Tactic.BicategoryLike.Mor₁}
  {a_2 : Mathlib.Tactic.BicategoryLike.NormalizedHom} {a_3 : Mathlib.Tactic.BicategoryLike.Atom₁},
  Mathlib.Tactic.BicategoryLike.NormalizedHom.cons e a a_1 =
      Mathlib.Tactic.BicategoryLike.NormalizedHom.cons e_1 a_2 a_3 →
    e = e_1 ∧ a = a_2 ∧ a_1 = a_3
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.hsymm_zero : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ],
  MvPolynomial.hsymm σ R 0 = 1
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- `FactorSetMem p s` is the predicate that the irreducible `p` is a member of
`s : FactorSet α`.

If `p` is not irreducible, `p` is not a member of any `FactorSet`.  -/
Associates.FactorSetMem : {α : Type u_1} → [inst : CommMonoidWithZero α] → Associates.FactorSet α → Associates α → Prop
-- Std.Time.Format.Basic
Std.Time.FormatPart.string.sizeOf_spec : ∀ (val : String), sizeOf (Std.Time.FormatPart.string val) = 1 + sizeOf val
-- Init.Data.UInt.BasicAux
/-- Non-strict inequality of word-sized unsigned integers, defined as inequality of the corresponding
natural numbers. Usually accessed via the `≤` operator.
 -/
USize.le : USize → USize → Prop
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosed.card_aroots_eq_natDegree_of_leadingCoeff_ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Field B] [IsAlgClosed B] [inst_3 : Algebra A B]
  {p : Polynomial A}, (algebraMap A B) p.leadingCoeff ≠ 0 → (p.aroots B).card = p.natDegree
-- Mathlib.AlgebraicTopology.DoldKan.Projections
/-- For each `q`, `P q` is a natural transformation.  -/
AlgebraicTopology.DoldKan.natTransP : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      ℕ → (AlgebraicTopology.alternatingFaceMapComplex C ⟶ AlgebraicTopology.alternatingFaceMapComplex C)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_eq_isSome_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = m[a]?.isSome
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.mulShift.eq_1 : ∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : Monoid G] (p : SymbolicDynamics.FullShift.Pattern A G)
  (v h : G),
  p.mulShift v h =
    if hmem : h ∈ Finset.image (fun x => v * x) p.support then
      have ex := ⋯;
      p.config (Classical.choose ex)
    else default
-- Mathlib.Algebra.Group.Units.Defs
isUnit_iff_exists_inv : ∀ {M : Type u_1} [inst : Monoid M] [IsDedekindFiniteMonoid M] {a : M}, IsUnit a ↔ ∃ b, a * b = 1
-- Mathlib.Order.Filter.CardinalInter
/-- Construct a filter with cardinal `c` intersection property.
Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property.
Similarly to `Filter.ofCardinalInter`,
this constructor deduces some properties from the cardinal `c` intersection property
which becomes the cardinal `c` union property because we take complements of all sets.  -/
Filter.ofCardinalUnion : {α : Type u} →
  {c : Cardinal.{u}} →
    (l : Set (Set α)) →
      2 < c →
        (∀ (S : Set (Set α)), Cardinal.mk ↑S < c → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) → (∀ t ∈ l, ∀ s ⊆ t, s ∈ l) → Filter α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
addLECancellable_zero : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α], AddLECancellable 0
-- Mathlib.MeasureTheory.Measure.Restrict
mem_map_indicator_ae_iff_mem_map_restrict_ae_of_zero_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β] {t : Set β},
  0 ∈ t →
    MeasurableSet s →
      (t ∈ Filter.map (s.indicator f) (MeasureTheory.ae μ) ↔ t ∈ Filter.map f (MeasureTheory.ae (μ.restrict s)))
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- **Alias** of `ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prod`. -/
ProbabilityTheory.iIndepFun.charFunDual_map_finset_sum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : NormedSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (∑ i ∈ s, X i) P) =
        ∏ i ∈ s, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P)
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductCone_fst : ∀ (X Y : Type u), (CategoryTheory.Limits.Types.binaryProductCone X Y).fst = TypeCat.ofHom Prod.fst
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.le_succ_iff : ∀ {α : Type u_1} {a b : α} [inst : LinearOrder α] [inst_1 : SuccOrder α],
  Order.IsSuccPrelimit b → (b ≤ Order.succ a ↔ b ≤ a)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_mul : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (f g : E →ₗᵢ[R] E), ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Data.List.Sublists
_private.Mathlib.Data.List.Sublists.0.List.sublistsLenAux.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : ℕ → List α → (List α → β) → List β → Sort u_3) →
      (x : ℕ) →
        (x_1 : List α) →
          (x_2 : List α → β) →
            (x_3 : List β) →
              ((x : List α) → (f : List α → β) → (r : List β) → motive 0 x f r) →
                ((n : ℕ) → (x : List α → β) → (r : List β) → motive n.succ [] x r) →
                  ((n : ℕ) → (a : α) → (l : List α) → (f : List α → β) → (r : List β) → motive n.succ (a :: l) f r) →
                    motive x x_1 x_2 x_3
-- Mathlib.Logic.Function.DependsOn
DependsOn.eq_1 : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : Type u_3} (f : ((i : ι) → α i) → β) (s : Set ι),
  DependsOn f s = ∀ ⦃x y : (i : ι) → α i⦄, (∀ i ∈ s, x i = y i) → f x = f y
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_equivMapDomain : ∀ {α : Type u_1} (R : Type u_5) [inst : Semiring R] {α' : Type u_7} {M' : Type u_8} [inst_1 : AddCommMonoid M']
  [inst_2 : Module R M'] {v' : α' → M'} (f : α ≃ α') (l : α →₀ R),
  (Finsupp.linearCombination R v') (Finsupp.equivMapDomain f l) = (Finsupp.linearCombination R (v' ∘ ⇑f)) l
-- Mathlib.Topology.Inseparable
/-- A subset `S` of a topological space is stable under specialization
if `x ∈ S → y ∈ S` for all `x ⤳ y`.  -/
StableUnderSpecialization : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.SetTheory.Cardinal.Free
instCountableFreeAddGroup : ∀ (α : Type u) [Countable α], Countable (FreeAddGroup α)
-- Mathlib.Algebra.Star.Basic
/-- `star` as an `AddEquiv`  -/
starAddEquiv : {R : Type u} → [inst : AddMonoid R] → [StarAddMonoid R] → R ≃+ R
-- Mathlib.Topology.Order.OrderClosed
isClosed_Icc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {a b : α},
  IsClosed (Set.Icc a b)
-- Mathlib.Logic.IsEmpty.Basic
not_nonempty_iff : ∀ {α : Sort u_1}, ¬Nonempty α ↔ IsEmpty α
-- Init.Data.Range.Polymorphic.Basic
/-- Returns the number of elements starting from `lo` that satisfy the given upper bound.  -/
Std.Rxo.HasSize.size : {α : Type u} → [self : Std.Rxo.HasSize α] → α → α → ℕ
-- Mathlib.AlgebraicTopology.DoldKan.Compatibility
AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso_inv_app : ∀ {A : Type u_1} {A' : Type u_2} {B' : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] [inst_2 : CategoryTheory.Category.{v_4, u_4} B'] {eA : A ≌ A'}
  {e' : A' ≌ B'} {F : CategoryTheory.Functor A B'} (hF : eA.functor.comp e'.functor ≅ F) (X : B'),
  (AlgebraicTopology.DoldKan.Compatibility.equivalence₁CounitIso hF).inv.app X =
    CategoryTheory.CategoryStruct.comp (e'.counitIso.inv.app X)
      (CategoryTheory.CategoryStruct.comp (e'.functor.map (eA.counitIso.inv.app (e'.inverse.obj X)))
        (hF.hom.app (eA.inverse.obj (e'.inverse.obj X))))
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsClosedSubgraph.instIsPartialOrder : ∀ {α : Type u_1} {β : Type u_2}, IsPartialOrder (Graph α β) fun x1 x2 => x1.IsClosedSubgraph x2
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
/-- An open normal subgroup of a compact topological group has finite index.  -/
OpenNormalSubgroup.toFiniteIndexNormalSubgroup : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [CompactSpace G] → [ContinuousMul G] → OpenNormalSubgroup G → FiniteIndexNormalSubgroup G
-- Mathlib.Data.Ordering.Lemmas
cmpUsing_eq_eq : ∀ {α : Type u} {lt : α → α → Prop} [inst : DecidableRel lt] (a b : α), cmpUsing lt a b = Ordering.eq ↔ ¬lt a b ∧ ¬lt b a
-- Std.Sync.CancellationToken
Std.CancellationToken.State.mk.sizeOf_spec : ∀ (reason : Option Std.CancellationReason) (consumers : Std.Queue Std.CancellationToken.Consumer),
  sizeOf { reason := reason, consumers := consumers } = 1 + sizeOf reason + sizeOf consumers
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {rs : List R},
  RingTheory.Sequence.IsRegular M rs → ∀ (N : Submodule R M), Nontrivial (M ⧸ Ideal.ofList rs • N)
-- Mathlib.Order.Cover
wcovBy_congr_left : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (a ⩿ c ↔ b ⩿ c)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_lt_two_pow : ∀ {x i : ℕ}, x < 2 ^ i → x.testBit i = false
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_iSup₂_iff : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] {a : α} {f : (i : ι) → κ i → LowerSet α},
  a ∈ ⨆ i, ⨆ j, f i j ↔ ∃ i j, a ∈ f i j
-- Lean.Meta.MethodSpecs
Lean.MethodSpecsAttrData.mk : Lean.Name → Bool → Lean.MethodSpecsAttrData
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
IsStrongFEPair.hf₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {P : WeakFEPair E},
  IsStrongFEPair P → P.f₀ = 0
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a fallback : α}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.sum_lt_sum_of_nonempty : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α]
  [AddLeftStrictMono α] {s : Multiset ι} {f g : ι → α},
  s ≠ ∅ → (∀ i ∈ s, f i < g i) → (Multiset.map f s).sum < (Multiset.map g s).sum
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.forM_eq_forM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → m PUnit.{w + 1}},
  (forM t fun a => f a.fst) = t.keys.forM f
-- Init.Data.List.Count
List.boole_getElem_le_count : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α} {i : ℕ} (h : i < l.length),
  (if (l[i] == a) = true then 1 else 0) ≤ List.count a l
-- Mathlib.Data.PNat.Prime
PNat.instFactPrimeValOfPrime : ∀ {p : ℕ+} [h : Fact p.Prime], Fact (Nat.Prime ↑p)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g] (hf : S.f = 0),
  (CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel S hf).H = CategoryTheory.Limits.kernel S.g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (Std.ExtDTreeMap.ofList l cmp).getKeyD k fallback = fallback
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_ne_zero_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [CanonicallyOrderedAdd α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  Summable f → (∑' (i : ι), f i ≠ 0 ↔ ∃ x, f x ≠ 0)
-- Mathlib.Data.Fintype.Card
Fintype.card_subtype_eq : ∀ {α : Type u_1} (y : α) [inst : Fintype { x // x = y }], Fintype.card { x // x = y } = 1
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.cocomplex_exactAt_succ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (I : CategoryTheory.InjectiveResolution Z) (n : ℕ),
  HomologicalComplex.ExactAt I.cocomplex (n + 1)
-- Lean.Meta.Tactic.Grind.EMatch
/-- Performs one round of E-matching using the giving theorems, and returns `true` if new instances were generated.  -/
Lean.Meta.Grind.ematchOnly : Array Lean.Meta.Grind.EMatchTheorem → Lean.Meta.Grind.GoalM Bool
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.map_sum₂ : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  {ι : Type u_14} (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (t : Finset ι) (x : ι → M) (y : N),
  (f (∑ i ∈ t, x i)) y = ∑ i ∈ t, (f (x i)) y
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `Y' ≅ Y`, then `X x Y` also is the product of `X` and `Y'`.  -/
CategoryTheory.Limits.BinaryFan.isLimitCompRightIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Y' : C} →
      (c : CategoryTheory.Limits.BinaryFan X Y) →
        (f : Y ⟶ Y') →
          [CategoryTheory.IsIso f] →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsLimit
                (CategoryTheory.Limits.BinaryFan.mk c.fst (CategoryTheory.CategoryStruct.comp c.snd f))
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adj.counit_naturality_assoc : ∀ {C₁ C₂ : CategoryTheory.Bicategory.Adj CategoryTheory.Cat} (α : C₁ ⟶ C₂) {X Y : ↑C₂.obj} (f : X ⟶ Y) {Z : ↑C₂.obj}
  (h : (CategoryTheory.CategoryStruct.id C₂.obj).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.l.toFunctor.map (α.r.toFunctor.map f))
      (CategoryTheory.CategoryStruct.comp (α.adj.counit.toNatTrans.app Y) h) =
    CategoryTheory.CategoryStruct.comp (α.adj.counit.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousAt_iff_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  UpperHemicontinuousAt f x ↔
    ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
-- Batteries.Data.List.Lemmas
List.disjoint_append_left : ∀ {α : Type u_1} {l₁ l₂ l : List α}, (l₁ ++ l₂).Disjoint l ↔ l₁.Disjoint l ∧ l₂.Disjoint l
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  k ∈ Std.DTreeMap.filterMap f t ↔ ∃ (h : k ∈ t), (f k (t.get k h)).isSome = true
-- Init.Data.List.Basic
/-- Rotates the elements of `xs` to the left, moving `i % xs.length` elements from the start of the list
to the end.

`O(|xs|)`.

Examples:
* `[1, 2, 3, 4, 5].rotateLeft 3 = [4, 5, 1, 2, 3]`
* `[1, 2, 3, 4, 5].rotateLeft 5 = [1, 2, 3, 4, 5]`
* `[1, 2, 3, 4, 5].rotateLeft 1 = [2, 3, 4, 5, 1]`
 -/
List.rotateLeft : {α : Type u} → List α → optParam ℕ 1 → List α
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- The support of the Euler characteristic summand equals the finite rank support,
because the sign `c.χ i` is always nonzero (it's a unit).  -/
_private.Mathlib.Algebra.Homology.EulerCharacteristic.0.GradedObject.support_eulerChar_summand : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} (c : ComplexShape ι) [inst_1 : c.EulerCharSigns]
  (X : CategoryTheory.GradedObject ι (ModuleCat R)),
  (Function.support fun i => ↑(c.χ i) * ↑(Module.finrank R ↑(X i))) = GradedObject.finrankSupport X
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.coe_ofClass : ∀ {S : Type u_3} {M : Type u_4} [inst : Monoid M] [inst_1 : SetLike S M] [inst_2 : SubmonoidClass S M] (s : S),
  ↑(Submonoid.ofClass s) = ↑s
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.lift_mk : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  {φ : G →+ M} (HN : N ≤ φ.ker) (g : G), (QuotientAddGroup.lift N φ HN) ↑g = φ g
-- Lean.DocString.Types
/-- An empty block with no content.  -/
Lean.Doc.Block.empty : {i : Type u_1} → {b : Type u_2} → Lean.Doc.Block i b
-- Mathlib.Data.Seq.Computation
Computation.get_think : ∀ {α : Type u} (s : Computation α) [h : s.Terminates], s.think.get = s.get
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.map_iInf : ∀ {F : Type u_1} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] [inst_7 : IsScalarTower R A A] [inst_8 : SMulCommClass R A A] {ι : Sort u_2}
  [Nonempty ι] [inst_10 : IsScalarTower R B B] [inst_11 : SMulCommClass R B B] (f : F),
  Function.Injective ⇑f →
    ∀ (S : ι → NonUnitalSubalgebra R A), NonUnitalSubalgebra.map f (⨅ i, S i) = ⨅ i, NonUnitalSubalgebra.map f (S i)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.refl : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F), CommRingCat.Colimits.Relation F x x
-- Mathlib.RingTheory.Regular.RegularSequence
Ideal.ofList_cons : ∀ {R : Type u_1} [inst : Semiring R] (r : R) (rs : List R), Ideal.ofList (r :: rs) = Ideal.span {r} ⊔ Ideal.ofList rs
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.shortComplexTruncLE_X₃_isSupportedOutside : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Abelian C] (K : HomologicalComplex C c')
  (e : c.Embedding c') [inst_2 : e.IsTruncLE], (K.shortComplexTruncLE e).X₃.IsSupportedOutside e
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (producers : Std.Queue (α × IO.Promise Bool))
  (consumers : Std.Queue (Std.CloseableChannel.Consumer✝ α)) (closed : Bool),
  sizeOf { producers := producers, consumers := consumers, closed := closed } =
    1 + sizeOf producers + sizeOf consumers + sizeOf closed
-- Mathlib.Algebra.Order.Floor.Ring
Int.preimage_Ioi : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] {a : R},
  Int.cast ⁻¹' Set.Ioi a = Set.Ioi ⌊a⌋
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_univ : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s : Set α}, s =ᵐ[μ] Set.univ ↔ μ sᶜ = 0
-- Mathlib.Combinatorics.Matroid.Closure
/-- The property of being a flat gives rise to a `ClosureOperator` on the subsets of `M.E`,
in which the `IsClosed` sets correspond to flats.
(We can't define such an operator on all of `Set α`,
since this would incorrectly force `univ` to always be a flat.)  -/
Matroid.subtypeClosure : {α : Type u_2} → (M : Matroid α) → ClosureOperator ↑(Set.Iic M.E)
-- Mathlib.Probability.Moments.ComplexMGF
/-- `complexMGF X μ` is holomorphic on the vertical strip
`{z | z.re ∈ interior (integrableExpSet X μ)}`.  -/
ProbabilityTheory.differentiableOn_complexMGF : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  DifferentiableOn ℂ (ProbabilityTheory.complexMGF X μ) {z | z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ)}
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.minValueSealed : Int16
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.ExtTreeMap.getEntryGE! : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtTreeMap α β cmp → α → α × β
-- Init.Data.String.Lemmas.Search
String.front_toSlice : ∀ {s : String}, s.toSlice.front = s.front
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A morphism `f` has a kernel if the functor `ParallelPair f 0` has a limit.  -/
CategoryTheory.Limits.HasKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → {X Y : C} → (X ⟶ Y) → Prop
-- Init.Data.SInt.Lemmas
Int32.toInt_toISize : ∀ (x : Int32), x.toISize.toInt = x.toInt
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.hasIntegral_congr : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : Fintype ι] (I : BoxIntegral.Box ι)
  (l : BoxIntegral.IntegrationParams) {f₁ f₂ : (ι → ℝ) → E} {vol₁ vol₂ : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  Set.EqOn f₁ f₂ (BoxIntegral.Box.Icc I) →
    Set.EqOn (⇑vol₁) (⇑vol₂) (Set.Iic I) →
      ∀ (y : F), BoxIntegral.HasIntegral I l f₁ vol₁ y ↔ BoxIntegral.HasIntegral I l f₂ vol₂ y
-- Mathlib.RingTheory.Adjoin.Polynomial.Bivariate
Polynomial.Bivariate.Transcendental.algEquivAdjoin.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x : A}
  (hx : Transcendental R x),
  Polynomial.Bivariate.Transcendental.algEquivAdjoin hx =
    Polynomial.mapAlgEquiv (Polynomial.algEquivOfTranscendental R x hx)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∈ t₂ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsBasis'.contract_isBasis'_sdiff_of_subset`. -/
Matroid.IsBasis'.contract_isBasis'_diff_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis' I X → J ⊆ I → (M.contract J).IsBasis' (I \ J) X
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.natCast_lt_gamma : ∀ {o : Ordinal.{u}} (n : ℕ), ↑n < o.gamma
-- Mathlib.Data.Sym.Basic
/-- Mapping an equivalence `α ≃ β` using `Sym.map` gives an equivalence between `Sym α n` and
`Sym β n`.  -/
Sym.equivCongr : {α : Type u_1} → {β : Type u_2} → {n : ℕ} → α ≃ β → Sym α n ≃ Sym β n
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_iff_faithful_yoneda_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : C),
  CategoryTheory.IsCoseparator G ↔ (CategoryTheory.yoneda.obj G).Faithful
-- Mathlib.Topology.Algebra.Support
notMem_tsupport_iff_eventuallyEq : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : Zero β] {f : α → β} {x : α},
  x ∉ tsupport f ↔ f =ᶠ[nhds x] 0