mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- A successor structure on a category consists of the
data of an object `succ X` for any `X : C`, a map `toSucc X : X ⟶ succ X`
(which does not need to be natural), and a zeroth object `X₀`.
 -/
CategoryTheory.SmallObject.SuccStruct : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_tsub_one_le_encard_sdiff_singleton`. -/
Set.encard_tsub_one_le_encard_diff_singleton : ∀ {α : Type u_1} (s : Set α) (x : α), s.encard - 1 ≤ (s \ {x}).encard
-- Init.Data.Dyadic.Basic
Dyadic.neg_ofOdd : ∀ {n k : ℤ} {hn : n % 2 = 1}, -Dyadic.ofOdd n k hn = Dyadic.ofOdd (-n) k ⋯
-- Mathlib.Algebra.Order.Group.Synonym
toLex_add : ∀ {α : Type u_1} [inst : Add α] (a b : α), toLex (a + b) = toLex a + toLex b
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- The constant term of `cyclotomic n R` is `1` if `2 ≤ n`.  -/
Polynomial.cyclotomic_coeff_zero : ∀ (R : Type u_1) [inst : CommRing R] {n : ℕ}, 1 < n → (Polynomial.cyclotomic n R).coeff 0 = 1
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.punitCoprod.eq_1 : ∀ (M : Type u_1) [inst : Monoid M], MulEquiv.punitCoprod M = Monoid.Coprod.snd.toMulEquiv Monoid.Coprod.inr ⋯ ⋯
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Given a colimit cocone, `F.cocones` is corepresentable by the point of the cocone.  -/
CategoryTheory.Limits.IsColimit.corepresentableBy : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} → CategoryTheory.Limits.IsColimit t → F.cocones.CorepresentableBy t.pt
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.NatTrans.whiskerRight_app_tensor_app_assoc : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  {F G F' G' : CategoryTheory.Functor J C} (α : F ⟶ F') (β : G ⟶ G') {X Y : J} (f : X ⟶ Y) (X' : J) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F'.obj Y) (G'.obj X') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (G.obj X'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app Y) (β.app X')) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (β.app X'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F'.map f) (G'.obj X')) h)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.ulift_f : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (x : ↥X), 𝒰.ulift.f x = 𝒰.f (𝒰.idx x)
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.changeOriginSeries.eq_1 : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F) (k l : ℕ), p.changeOriginSeries k l = ∑ s, p.changeOriginSeriesTerm k l ↑s ⋯
-- Init.Data.SInt.Bitwise
instCommutativeInt8HXor : Std.Commutative fun x1 x2 => x1 ^^^ x2
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.State.mk.injEq : ∀ (result? : Option Lean.Meta.AbstractMVarsResult) (generatorStack : Array Lean.Meta.SynthInstance.GeneratorNode)
  (resumeStack : Array (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer))
  (tableEntries : Std.HashMap Lean.Expr Lean.Meta.SynthInstance.TableEntry)
  (result?_1 : Option Lean.Meta.AbstractMVarsResult) (generatorStack_1 : Array Lean.Meta.SynthInstance.GeneratorNode)
  (resumeStack_1 : Array (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer))
  (tableEntries_1 : Std.HashMap Lean.Expr Lean.Meta.SynthInstance.TableEntry),
  ({ result? := result?, generatorStack := generatorStack, resumeStack := resumeStack, tableEntries := tableEntries } =
      { result? := result?_1, generatorStack := generatorStack_1, resumeStack := resumeStack_1,
        tableEntries := tableEntries_1 }) =
    (result? = result?_1 ∧
      generatorStack = generatorStack_1 ∧ resumeStack = resumeStack_1 ∧ tableEntries = tableEntries_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.objEquiv_symm_δ_notMem_horn_iff : ∀ {n : ℕ} (i j : Fin (n + 2)),
  SSet.stdSimplex.objEquiv.symm (SimplexCategory.δ i) ∉ (SSet.horn (n + 1) j).obj (Opposite.op { len := n }) ↔ i = j
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p q : MvPolynomial σ R},
  q.totalDegree < p.totalDegree → (q + p).totalDegree = p.totalDegree
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, a Localization map `F : M →* N` away from `x`, and a map of `CommMonoid`s
`g : M →* P` such that `g x` is invertible, the homomorphism induced from `N` to `P` sending
`z : N` to `g y * (g x)⁻ⁿ`, where `y : M, n : ℕ` are such that `z = F y * (F x)⁻ⁿ`.  -/
Submonoid.LocalizationMap.AwayMap.lift : {M : Type u_1} →
  [inst : CommMonoid M] →
    {N : Type u_2} →
      [inst_1 : CommMonoid N] →
        {P : Type u_3} →
          [inst_2 : CommMonoid P] →
            {g : M →* P} → (x : M) → Submonoid.LocalizationMap.AwayMap x N → IsUnit (g x) → N →* P
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  {x y : ArchimedeanClass.FiniteElement K},
  ArchimedeanClass.FiniteResidueField.mk x < ArchimedeanClass.FiniteResidueField.mk y → x < y
-- Mathlib.Analysis.Normed.Order.Lattice
norm_inf_le_add : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (x y : α),
  ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
-- Mathlib.Data.Finsupp.Pointwise
Finsupp.mul_apply : ∀ {α : Type u₁} {β : Type u₂} [inst : MulZeroClass β] {g₁ g₂ : α →₀ β} {a : α}, (g₁ * g₂) a = g₁ a * g₂ a
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : SizeOf C]
  (X : CategoryTheory.SimplicialObject C) (s : X.Splitting), sizeOf { X := X, s := s } = 1 + sizeOf X + sizeOf s
-- Mathlib.GroupTheory.Complement
Equiv.ofBijective.eq_1 : ∀ {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f),
  Equiv.ofBijective f hf = { toFun := f, invFun := Function.surjInv ⋯, left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instCommutativeHOr : Std.Commutative fun x1 x2 => x1 ||| x2
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β]
  [inst_2 : MulZeroOneClass γ] {g : β →*₀ γ} {f₁ f₂ : α →*₀ β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.IsSubnormal.below.top : ∀ {G : Type u_1} [inst : Group G] {motive : (a : Subgroup G) → a.IsSubnormal → Prop}, Subgroup.IsSubnormal.below ⋯
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.mapComon_map_hom : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] {X Y : CategoryTheory.Comon C} (f : X ⟶ Y),
  (F.mapComon.map f).hom = F.map f.hom
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.coweightHom_injective : ∀ {ι : 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),
  Function.Injective ⇑(RootPairing.Equiv.coweightHom P)
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
/-- For a box `I`, the hyperplanes passing through its center split `I` into `2 ^ card ι` boxes.
`BoxIntegral.Box.splitCenterBox I s` is one of these boxes. See also
`BoxIntegral.Partition.splitCenter` for the corresponding `BoxIntegral.Partition`.  -/
BoxIntegral.Box.splitCenterBox : {ι : Type u_1} → BoxIntegral.Box ι → Set ι → BoxIntegral.Box ι
-- Init.Data.String.Termination
String.Pos.map_toSlice_next? : ∀ {s : String} {p : s.Pos}, Option.map String.Pos.toSlice p.next? = p.toSlice.next?
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorHomMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C))
  (hom₁ hom₁_1 : A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₁)
  (e_hom₁ : hom₁ = hom₁_1)
  (hom₂ hom₂_1 : A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₂)
  (e_hom₂ : hom₂ = hom₂_1)
  (hom₃ hom₃_1 : A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₃)
  (e_hom₃ : hom₃ = hom₃_1)
  (comm₁ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂) hom₂ =
      CategoryTheory.CategoryStruct.comp hom₁ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂))
  (comm₂ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) hom₃ =
      CategoryTheory.CategoryStruct.comp hom₂ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃))
  (comm₃ :
    CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
        (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp hom₃ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)),
  CategoryTheory.Pretriangulated.Triangle.functorHomMk A B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃ =
    CategoryTheory.Pretriangulated.Triangle.functorHomMk A B hom₁_1 hom₂_1 hom₃_1 ⋯ ⋯ ⋯
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
IsAddCyclic.card_nsmul_eq_zero_le : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] [IsAddCyclic α] {n : ℕ},
  0 < n → {a | n • a = 0}.card ≤ n
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mul_mem_sup : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  {x y : A}, x ∈ S → y ∈ T → x * y ∈ S ⊔ T
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.IsAlt.neg : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B : LinearMap.BilinForm R₁ M₁}, B.IsAlt → (-B).IsAlt
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.aemeasurable_dirac : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [MeasurableSingletonClass α]
  {a : α} {f : α → β}, AEMeasurable f (MeasureTheory.Measure.dirac a)
-- Mathlib.Algebra.Opposites
AddOpposite.op_eq_one_iff : ∀ {α : Type u_1} [inst : One α] {a : α}, AddOpposite.op a = 1 ↔ a = 1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rcc_ne_nil_iff : ∀ {m n : ℤ}, (m...=n).toList ≠ [] ↔ m ≤ n
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.Compatible.anti_right : ∀ {α : Type u_1} {β : Type u_2} {G H H₁ : Graph α β}, H₁ ≤ H → G.Compatible H → G.Compatible H₁
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first output of the iterator, or `none` if no such output is found.

`O(|it|)` since the iterator may skip an unknown number of times before returning a result.
Short-circuits upon encountering the first result. Only the first element of `it` is examined.

If the iterator is not productive, this function might run forever. The variant
`it.ensureTermination.first?` always terminates after finitely many steps.

Examples:
* `([7, 6].iterM Id).first? = pure (some 7)`
* `([].iterM Id).first? = pure none`
 -/
Std.IterM.first? : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] → [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM m β → m (Option β)
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univBall_target : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) {r : ℝ},
  0 < r → (OpenPartialHomeomorph.univBall c r).target = Metric.ball c r
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_map_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄] (f : M →ₗ[R] M₂) (g : M₃ →ₗ[R] M₄)
  (S : Submodule R M) (S' : Submodule R M₃),
  Submodule.map (f.prodMap g) (S.prod S') = (Submodule.map f S).prod (Submodule.map g S')
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.dsimp : {m : Type → Type} → [self : Lean.Meta.MonadSimp m] → Lean.Expr → m Lean.Expr
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.typeHasRecFun : Lean.Expr → Array Lean.Expr → List Lean.Elab.Term.LetRecToLift → Option Lean.FVarId
-- Std.Data.HashMap.Raw
/-- Returns an array of all values present in the hash map in some order.  -/
Std.HashMap.Raw.valuesArray : {α : Type u} → {β : Type v} → Std.HashMap.Raw α β → Array β
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_injective_right : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α), Function.Injective fun b => Set.uIoc b a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.toArray_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp}, t.toList.toArray = t.toArray
-- Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup
Subgroup.properlyDiscontinuousSMul_iff : ∀ {Γ : Type u_1} {α : Type u_2} [inst : Group Γ] [inst_1 : TopologicalSpace α] [inst_2 : SMul Γ α] (S : Subgroup Γ),
  ProperlyDiscontinuousSMul (↥S) α ↔
    ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ S ∧ (g • K ∩ L).Nonempty}.Finite
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.IsTotallyReal.maximalRealSubfield_eq_top : ∀ {K : Type u_2} [inst : Field K] [NumberField.IsTotallyReal K], NumberField.maximalRealSubfield K = ⊤
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w : ℕ} → ℕ → aig.RefVec w → Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget aig w
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.mk.sizeOf_spec : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} [inst_4 : SizeOf ι] [inst_5 : SizeOf R] [inst_6 : SizeOf L]
  (A : Matrix ι ι ℤ) (h e f : ι → L) (cartan_eq_lieSpan : H = LieSubalgebra.lieSpan R L (Set.range h))
  (span_ef : LieSubalgebra.lieSpan R L (Set.range e ∪ Set.range f) = ⊤) (linInd : LinearIndependent R h)
  (nondegen : A.Nondegenerate) (sl2 : ∀ (i : ι), IsSl2Triple (h i) (e i) (f i)) (lie_h_h : ∀ (i j : ι), ⁅h i, h j⁆ = 0)
  (lie_h_e : ∀ (i j : ι), ⁅h j, e i⁆ = A i j • e i) (lie_h_f : ∀ (i j : ι), ⁅h j, f i⁆ = -A i j • f i)
  (lie_e_f_ne : ∀ (i j : ι), i ≠ j → ⁅e i, f j⁆ = 0),
  sizeOf
      { A := A, h := h, e := e, f := f, cartan_eq_lieSpan := cartan_eq_lieSpan, span_ef := span_ef, linInd := linInd,
        nondegen := nondegen, sl2 := sl2, lie_h_h := lie_h_h, lie_h_e := lie_h_e, lie_h_f := lie_h_f,
        lie_e_f_ne := lie_e_f_ne } =
    1 + sizeOf cartan_eq_lieSpan + sizeOf span_ef + sizeOf nondegen
-- Mathlib.Order.Interval.Set.OrdConnected
Set.OrdConnected.uIoc_subset : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α},
  s.OrdConnected → ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.uIoc x y ⊆ s
-- Mathlib.Data.Nat.ModEq
Nat.add_mul_modulus_modEq_iff : ∀ {n a b c : ℕ}, a + b * n ≡ c [MOD n] ↔ a ≡ c [MOD n]
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_map : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {f : F} {s : NonUnitalSubsemiring R} {y : S},
  y ∈ NonUnitalSubsemiring.map f s ↔ ∃ x ∈ s, f x = y
-- Mathlib.RingTheory.Invariant.Basic
MulSemiringAction.charpoly_eq : ∀ {B : Type u_2} (G : Type u_3) [inst : CommRing B] [inst_1 : Group G] [inst_2 : MulSemiringAction G B]
  [inst_3 : Fintype G] (b : B), MulSemiringAction.charpoly G b = ∏ g, (Polynomial.X - Polynomial.C (g • b))
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.vanishingIdeal_empty : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3},
  MvPolynomial.vanishingIdeal k ∅ = ⊤
-- Mathlib.GroupTheory.Torsion
/-- `g` lies in the additive `p`-primary component iff `p ^ k • g = 0` for some `k`.  -/
AddCommGroup.mem_primaryComponent : ∀ {G : Type u_1} [inst : AddCommGroup G] {p : ℕ} {g : G}, g ∈ AddCommGroup.primaryComponent G p ↔ ∃ k, p ^ k • g = 0
-- Mathlib.Analysis.Complex.Trigonometric
/-- The real hyperbolic cosine function, defined as the real part of the complex hyperbolic cosine
 -/
Real.cosh : ℝ → ℝ
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_def : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), a⁺ = cfcₙ (fun x => x⁺) a
-- Init.Control.ExceptCps
ExceptCpsT.runCatch_throw : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {a : α} [inst : Monad m], (throw a).runCatch = pure a
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.isBase_restrict_iff' : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, (M.restrict X).IsBase I ↔ M.IsBasis' I X
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.getConfig : Lean.Meta.Sym.DSimp.DSimpM Lean.Meta.Sym.DSimp.Config
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.mk.inj : ∀ {R : Type u} {A : Type v} {B : Type w} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Semiring B}
  {inst_3 : Algebra R A} {inst_4 : Algebra R B} {toEquiv : A ≃ B}
  {map_mul' : ∀ (x y : A), toEquiv.toFun (x * y) = toEquiv.toFun x * toEquiv.toFun y}
  {map_add' : ∀ (x y : A), toEquiv.toFun (x + y) = toEquiv.toFun x + toEquiv.toFun y}
  {commutes' : ∀ (r : R), toEquiv.toFun ((algebraMap R A) r) = (algebraMap R B) r} {toEquiv_1 : A ≃ B}
  {map_mul'_1 : ∀ (x y : A), toEquiv_1.toFun (x * y) = toEquiv_1.toFun x * toEquiv_1.toFun y}
  {map_add'_1 : ∀ (x y : A), toEquiv_1.toFun (x + y) = toEquiv_1.toFun x + toEquiv_1.toFun y}
  {commutes'_1 : ∀ (r : R), toEquiv_1.toFun ((algebraMap R A) r) = (algebraMap R B) r},
  { toEquiv := toEquiv, map_mul' := map_mul', map_add' := map_add', commutes' := commutes' } =
      { toEquiv := toEquiv_1, map_mul' := map_mul'_1, map_add' := map_add'_1, commutes' := commutes'_1 } →
    toEquiv = toEquiv_1
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Evaluation of the logarithmic counting function at zero yields zero.
 -/
ValueDistribution.logCounting_eval_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a : WithTop E},
  ValueDistribution.logCounting f a 0 = 0
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mem_sup_right : ∀ {M : Type u_2} [inst : Mul M] {S T : Subsemigroup M} {x : M}, x ∈ T → x ∈ S ⊔ T
-- Std.Data.Internal.List.Associative
Std.Internal.List.eraseList_perm_of_perm_first : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l1 l2 : List ((a : α) × β a)} {toErase : List α},
  l1.Perm l2 →
    Std.Internal.List.DistinctKeys l1 →
      (Std.Internal.List.eraseList l1 toErase).Perm (Std.Internal.List.eraseList l2 toErase)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- If a function is countably sub-multiplicative then it is binary sub-multiplicative  -/
rel_sup_mul : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} [inst_2 : CompleteLattice α]
  (m : α → M),
  m ⊥ = 1 →
    ∀ (R : M → M → Prop),
      (∀ (s : ℕ → α), R (m (⨆ i, s i)) (∏' (i : ℕ), m (s i))) → ∀ (s₁ s₂ : α), R (m (s₁ ⊔ s₂)) (m s₁ * m s₂)
-- Mathlib.Order.Interval.Set.Disjoint
IsGLB.biUnion_Ici_eq_Ioi : ∀ {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α}, IsGLB s a → a ∉ s → ⋃ x ∈ s, Set.Ici x = Set.Ioi a
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.coe_ofCLM : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (A : E →SL[σ] F),
  ⇑(ContinuousLinearMapWOT.ofCLM A) = ⇑A
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedPort.default : Std.Http.URI.Port
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.length_sub : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (s t : NonemptyInterval α), (s - t).length = s.length + t.length
-- Mathlib.Logic.Equiv.Set
Equiv.range_eq_univ : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), Set.range ⇑e = Set.univ
-- Mathlib.Analysis.Seminorm
/-- Let `p` and `q` be two seminorms on a vector space over a `NontriviallyNormedField`.
If we have `q x ≤ C * p x` on some shell of the form `{x | ε/‖c‖ ≤ p x < ε}` (where `ε > 0`
and `‖c‖ > 1`), then we also have `q x ≤ C * p x` for all `x` such that `p x ≠ 0`.  -/
Seminorm.bound_of_shell : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p q : Seminorm 𝕜 E) {ε C : ℝ},
  0 < ε → ∀ {c : 𝕜}, 1 < ‖c‖ → (∀ (x : E), ε / ‖c‖ ≤ p x → p x < ε → q x ≤ C * p x) → ∀ {x : E}, p x ≠ 0 → q x ≤ C * p x
-- Mathlib.Data.Real.Sign
Real.sign_of_neg : ∀ {r : ℝ}, r < 0 → r.sign = -1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
/-- Multiseries representing a constant.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.const : (basis : Tactic.ComputeAsymptotics.Basis) → ℝ → Tactic.ComputeAsymptotics.MultiseriesExpansion basis
-- Mathlib.Analysis.Distribution.Support
/-- The distributional support of `f` is the intersection of all closed sets `s` such that `f`
vanishes on the complement of `s`.

To make this definition work for all types of distributions, we define it for any function from
a `FunLike` type to a type with zero.  -/
Distribution.dsupport : {α : Type u_2} →
  {β : Type u_3} →
    {F : Type u_6} → {V : Type u_10} → [FunLike F α β] → [TopologicalSpace α] → [Zero β] → [Zero V] → (F → V) → Set α
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- To construct an isomorphism of algebras, it suffices to give an isomorphism of the As which
commutes with the structure morphisms.
 -/
CategoryTheory.Endofunctor.Algebra.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} →
        (h : A₀.a ≅ A₁.a) →
          autoParam
              (CategoryTheory.CategoryStruct.comp (F.map h.hom) A₁.str =
                CategoryTheory.CategoryStruct.comp A₀.str h.hom)
              CategoryTheory.Endofunctor.Algebra.isoMk._auto_1 →
            (A₀ ≅ A₁)
-- Mathlib.Topology.Spectral.Hom
/-- A function between topological spaces is spectral if it is continuous and the preimage of every
compact open set is compact open.  -/
IsSpectralMap : {α : Type u_2} → {β : Type u_3} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop