mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Types.Pushouts
/-- The constructed pushout cocone in the category of types.  -/
CategoryTheory.Limits.Types.Pushout.cocone : {S X₁ X₂ : Type u} → (f : S ⟶ X₁) → (g : S ⟶ X₂) → CategoryTheory.Limits.PushoutCocone f g
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_8 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) (fvarId : Lean.FVarId) (n : ℕ)
  (check persistent : Bool) (h : pu = Lean.Compiler.LCNF.Purity.impure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_8 fvarId n check persistent h
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.op_sInf : ∀ {G : Type u_2} [inst : Group G] (S : Set (Subgroup G)), (sInf S).op = sInf (Subgroup.unop ⁻¹' S)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instFiniteIndex : ∀ {G : Type u_1} [inst : AddGroup G] (H : FiniteIndexNormalAddSubgroup G), H.FiniteIndex
-- Batteries.Data.MLList.Basic
/-- Filter and transform a `MLList` using a function that returns values inside the monad.  -/
MLList.filterMapM : {m : Type u_1 → Type u_1} → {α β : Type u_1} → [Monad m] → (α → m (Option β)) → MLList m α → MLList m β
-- Lean.Util.Path
/-- Initialize Lean's search path given Lean's system root and an initial search path.
The system root can be obtained via `getBuildDir` (for internal use) or
`findSysroot` (for external users).  -/
Lean.initSearchPath : System.FilePath → optParam Lean.SearchPath ∅ → IO Unit
-- Mathlib.RingTheory.DedekindDomain.SInteger
Set.unit_valuation_eq_one : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R))
  (K : Type v) [inst_2 : Field K] [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (x : ↥(S.unit K))
  {v : IsDedekindDomain.HeightOneSpectrum R}, v ∉ S → (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑↑x = 1
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightAssocTensor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C × C × C}
  (f : X ⟶ Y),
  (CategoryTheory.MonoidalCategory.rightAssocTensor C).map f =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.1 (CategoryTheory.MonoidalCategoryStruct.tensorHom f.2.1 f.2.2)
-- Lean.Level
Lean.Level.Data.hasParam : Lean.Level.Data → Bool
-- Lean.Data.Position
Lean.MonadFileMap.getFileMap : {m : Type → Type} → [self : Lean.MonadFileMap m] → m Lean.FileMap
-- Mathlib.Data.Set.Lattice.Image
/-- Analogue of `iSup_prod` for sets.  -/
Set.iUnion_prod' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β × γ → Set α), ⋃ x, f x = ⋃ i, ⋃ j, f (i, j)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.neg_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : M),
  (LinearEquiv.neg R) x = -x
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.ColimitOfShape.colimitsOfShape : ∀ {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] {X : C} (h : P.ColimitOfShape J X), P.colimitsOfShape J X
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAlt0.eq_1 : ∀ {α : Type u} {m n : ℕ} (hm : m = n + n) (v : Fin m → α) (k : Fin n), Matrix.vecAlt0 hm v k = v ⟨↑k + ↑k, ⋯⟩
-- Init.Data.UInt.Lemmas
UInt64.mul_add : ∀ {a b c : UInt64}, a * (b + c) = a * b + a * c
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_starAe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R], ⇑QuaternionAlgebra.starAe = MulOpposite.op ∘ star
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
/-- Given two sets `s t : Set α`, the set `Set.orderSeparatingSet s t` is the set of points that
belong both to some `Set.ordConnectedComponent tᶜ x`, `x ∈ s`, and to some
`Set.ordConnectedComponent sᶜ x`, `x ∈ t`. In the case of two disjoint closed sets, this is the
union of all open intervals $(a, b)$ such that their endpoints belong to different sets.  -/
Set.ordSeparatingSet : {α : Type u_1} → [LinearOrder α] → Set α → Set α → Set α
-- Init.Data.BitVec.Folds
/-- Given a function `state` that provides the correct state for every potential iteration count and a
function that computes these states from the correct initial state, the result of applying
`BitVec.iunfoldr f` to the initial state is the state corresponding to the bitvector's width paired
with the bitvector that consists of each computed bit.

This theorem can be used to prove properties of functions that are defined using `BitVec.iunfoldr`.
 -/
BitVec.iunfoldr_replace : ∀ {w : ℕ} {α : Type u_1} {f : Fin w → α → α × Bool} (state : ℕ → α) (value : BitVec w) (a : α),
  state 0 = a → (∀ (i : Fin w), f i (state ↑i) = (state (↑i + 1), value[↑i])) → BitVec.iunfoldr f a = (state w, value)
-- Mathlib.Topology.Connected.PathConnected
pathConnectedSpace_iff_zerothHomotopy : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  PathConnectedSpace X ↔ Nonempty (ZerothHomotopy X) ∧ Subsingleton (ZerothHomotopy X)
-- Mathlib.Analysis.InnerProductSpace.Coalgebra
/-- The comultiplication on `n → 𝕜` corresponds to the Euclidean space adjoint of the
multiplication map.  -/
Pi.comul_eq_adjoint : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {n : Type u_3} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  CoalgebraStruct.comul =
    TensorProduct.map ↑↑(EuclideanSpace.equiv n 𝕜) ↑↑(EuclideanSpace.equiv n 𝕜) ∘ₗ
      LinearMap.adjoint
          (↑↑(EuclideanSpace.equiv n 𝕜).symm ∘ₗ
            LinearMap.mul' 𝕜 (n → 𝕜) ∘ₗ TensorProduct.map ↑↑(EuclideanSpace.equiv n 𝕜) ↑↑(EuclideanSpace.equiv n 𝕜)) ∘ₗ
        ↑↑(EuclideanSpace.equiv n 𝕜).symm
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R},
  f ≠ 0 ↔ ∃ n d, (MvPowerSeries.coeff d) f ≠ 0 ∧ (Finsupp.weight w) d = n
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.maxKey he ∈ t
-- Mathlib.Algebra.Group.TypeTags.Hom
AddMonoidHom.toMultiplicativeRight_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] (f : Additive α →+ β) (a : α),
  (AddMonoidHom.toMultiplicativeRight f) a = Multiplicative.ofAdd (f (Additive.ofMul a))
-- Mathlib.Order.Hom.CompleteLattice
instCoeTCCompleteLatticeHomOfCompleteLatticeHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : CompleteLattice α] →
          [inst_2 : CompleteLattice β] → [CompleteLatticeHomClass F α β] → CoeTC F (CompleteLatticeHom α β)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.trim_mkMetric : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [BorelSpace X] (m : ENNReal → ENNReal),
  (MeasureTheory.OuterMeasure.mkMetric m).trim = MeasureTheory.OuterMeasure.mkMetric m
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
card_rootsOfUnity_eq_iff_exists_isPrimitiveRoot : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {n : ℕ} [NeZero n],
  Nat.card ↥(rootsOfUnity n R) = n ↔ ∃ ζ, IsPrimitiveRoot ζ n
-- Batteries.Data.List.Basic
/-- `idxOfNth a xs n` returns the index of the `n`th instance of `a` in `xs`, counting from `0`.

For example:
```
idxOfNth 1 [5, 1, 3, 2, 4, 0, 1, 4] 1 = 6
```
 -/
List.idxOfNth : {α : Type u_1} → [BEq α] → α → List α → ℕ → ℕ
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `fallback` if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyGTD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → α → α
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.ofHom_hom : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y : TopModuleCat R} (f : X.Hom Y),
  TopModuleCat.ofHom f.hom = f
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.mk : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : TopologicalSpace R] →
        [inst_2 : AddCommGroup M] →
          [inst_3 : Module R M] →
            (toAddGroupFilterBasis : AddGroupFilterBasis M) →
              (∀ {U : Set M},
                  U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ nhds 0, ∃ W ∈ toAddGroupFilterBasis.sets, V • W ⊆ U) →
                (∀ (x₀ : R) {U : Set M},
                    U ∈ toAddGroupFilterBasis.sets → ∃ V ∈ toAddGroupFilterBasis.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U) →
                  (∀ (m₀ : M) {U : Set M}, U ∈ toAddGroupFilterBasis.sets → ∀ᶠ (x : R) in nhds 0, x • m₀ ∈ U) →
                    ModuleFilterBasis R M
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_le_one : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (f : R → R) (a : A),
  (∀ x ∈ spectrum R a, f x ≤ 1) → cfc f a ≤ 1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_tensor_left_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).hom h))))
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The functor `EInt ⥤ C ⥤ C` which sends `⊥` to `𝟭 C`,
`n : ℤ` to `t.truncGE n` and `⊤` to the zero functor.  -/
CategoryTheory.Triangulated.TStructure.eTruncGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → CategoryTheory.Functor EInt (CategoryTheory.Functor C C)
-- Mathlib.Algebra.Group.Units.Basic
mul_ne_one : ∀ {α : Type u} [inst : CommMonoid α] [Subsingleton αˣ] {a b : α}, a * b ≠ 1 ↔ a ≠ 1 ∨ b ≠ 1
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.nondegenerate_iff_det_ne_zero : ∀ {R : Type u_1} {M₁ : Type u_6} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [IsDomain R] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] (b : Module.Basis m R M₁) {B : M₁ →ₗ[R] M₁ →ₗ[R] R},
  B.Nondegenerate ↔ ((LinearMap.toMatrix₂ b b) B).det ≠ 0
-- Mathlib.Analysis.Normed.Group.Constructions
PUnit.norm_eq_zero : ∀ (x : PUnit.{u_5 + 1}), ‖x‖ = 0
-- Mathlib.Combinatorics.SetFamily.Compression.Down
Finset.memberSubfamily_union_nonMemberSubfamily : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)),
  Finset.memberSubfamily a 𝒜 ∪ Finset.nonMemberSubfamily a 𝒜 = Finset.image (fun s => s.erase a) 𝒜
-- Mathlib.LinearAlgebra.TensorProduct.Defs
IsAddUnit.tmul_right : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] {m : M},
  IsAddUnit m → ∀ (n : N), IsAddUnit (m ⊗ₜ[R] n)
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.map_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5} [inst_3 : NormedAddCommGroup E]
  [inst_4 : NormedSpace ℝ E] [inst_5 : FiniteDimensional ℝ E] [inst_6 : TopologicalSpace H] {I : ModelWithCorners ℝ E H}
  (s : SingularManifold X k I) {φ : X → Y} {ψ : Y → Z} (hφ : Continuous φ) (hψ : Continuous ψ),
  ((s.map hφ).map hψ).f = (ψ ∘ φ) ∘ s.f
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits of shape `Jᵒᵖ`, then `F.unop : C ⥤ D` creates limits of
shape `J`.  -/
CategoryTheory.Limits.createsLimitsOfShapeUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
              [CategoryTheory.CreatesColimitsOfShape Jᵒᵖ F] → CategoryTheory.CreatesLimitsOfShape J F.unop
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
/-- Given a tower `A / ↥U / S / R` of algebras, where `U` is an `S`-subalgebra of `A`, reinterpret
`U` as an `R`-subalgebra of `A`.  -/
Subalgebra.restrictScalars : (R : Type u) →
  {S : Type v} →
    {A : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra S A] → [inst_5 : Algebra R A] → [IsScalarTower R S A] → Subalgebra S A → Subalgebra R A
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.instTensorProduct : ∀ {R : Type u} {A : Type v} {B : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallyEtale R A],
  Algebra.FormallyEtale B (TensorProduct R B A)
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.constSDiv.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalTorsor P] (p : P),
  Homeomorph.constSDiv p = { toEquiv := Equiv.constSDiv p, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Order.Antichain
IsAntichain.not_lt : ∀ {α : Type u_1} {s : Set α} {a b : α} [inst : Preorder α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) s → a ∈ s → b ∈ s → ¬a < b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_comp_isoCocycles₁_hom_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↑(groupCohomology.cocycles A 1)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₁ B).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesMap f φ 1)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₁ f φ))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₁ A).hom) x)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.instMonoidalProject : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v', u'} D] →
      [inst_1 : CategoryTheory.MonoidalCategory D] →
        (f : C → D) → (CategoryTheory.FreeMonoidalCategory.project f).Monoidal
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.lastDart_eq_getLast_darts : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : ¬p.Nil), p.lastDart hnil = p.darts.getLast ⋯
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.instBEqErrorContext.beq : Mathlib.Linter.TextBased.ErrorContext✝ → Mathlib.Linter.TextBased.ErrorContext✝ → Bool
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_pos_iff_of_base_lt_one : ∀ {b x : ℝ}, 0 < b → b < 1 → 0 < x → (0 < Real.logb b x ↔ x < 1)
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
HasFibers.proj_eq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} [inst_2 : HasFibers p] {S : 𝒮} (a : HasFibers.Fib p S),
  p.obj ((HasFibers.ι S).obj a) = S
-- Mathlib.RingTheory.LaurentSeries
/-- The following lemma shows that for every `d` smaller than the minimum between the integers
produced in `Cauchy.exists_lb_eventual_support` and `Cauchy.exists_lb_support`, for almost all
series in `ℱ` the `d`th coefficient coincides with the `d`th coefficient of `Cauchy.coeff hℱ`.  -/
LaurentSeries.Cauchy.exists_lb_coeff_ne : ∀ {K : Type u_2} [inst : Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ),
  ∃ N, ∀ᶠ (f : LaurentSeries K) in ℱ, ∀ d < N, LaurentSeries.Cauchy.coeff hℱ d = f.coeff d
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_add : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x y : K},
  0 ≤ ArchimedeanClass.mk x →
    0 ≤ ArchimedeanClass.mk y →
      ArchimedeanClass.stdPart (x + y) = ArchimedeanClass.stdPart x + ArchimedeanClass.stdPart y
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
AddCommGrpCat.uliftZMultiplesAddEquiv_apply : ∀ (G : AddCommGrpCat) (a : AddCommGrpCat.of (ULift.{u_1, 0} ℤ) ⟶ G),
  G.uliftZMultiplesAddEquiv a = (AddEquiv.mk' (uliftZMultiplesHom ↑G) ⋯).symm (AddCommGrpCat.homAddEquiv a)
-- Init.Sym.Lemmas
Lean.Sym.UInt8.eq_eq_false : ∀ (a b : UInt8), decide (a = b) = false → (a = b) = False
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rTensor_id : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N],
  (TensorProduct.AlgebraTensorModule.rTensor R N) LinearMap.id = LinearMap.id
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_nnqsmul : ∀ {R : Type u_1} [inst : Field R] [inst_1 : StarRing R] (q : ℚ≥0) (x : ↥(selfAdjoint R)), ↑(q • x) = q • ↑x
-- Mathlib.Topology.Covering.Quotient
/-- Fibers of a quotient covering map by an additive group G is a G-torsor.  -/
IsAddQuotientCoveringMap.fiberEquivAddGroup : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {G : Type u_3} →
            [inst_2 : AddGroup G] →
              [inst_3 : AddAction G E] → IsAddQuotientCoveringMap f G → {x : X} → ↑(f ⁻¹' {x}) → ↑(f ⁻¹' {x}) ≃ G
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_pow : ∀ {R : Type u} [inst : Semiring R] (s : R) [(Ideal.span {s}).IsTwoSided] (n : ℕ),
  Ideal.span {s} ^ n = Ideal.span {s ^ n}
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.toBoolAlg : FinBoolAlg → BoolAlg
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.sumElim_of_tower : ∀ {ι : Type u_1} {R : Type u_3} {S : Type u} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A],
  AlgebraicIndependent R x →
    ∀ {ι' : Type u_4} {y : ι' → A},
      Set.range x ⊆ Set.range ⇑(algebraMap S A) → AlgebraicIndependent S y → AlgebraicIndependent R (Sum.elim y x)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffWithinAt.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → ContDiffWithinAt ℝ n (fun x => Real.sin (f x)) s x
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `FunLike.coe_smul`. -/
Seminorm.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSomeM?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) → ((b : β) → motive (some b)) → (Unit → motive none) → motive __do_lift
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mrange_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange AddMonoid.Coprod.mk = ⊤
-- Mathlib.Data.Set.Image
Set.compl_image_ofPred : ∀ {α : Type u_1} {p : Set α → Prop}, compl '' {s | p s} = {s | p sᶜ}
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_zpow : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (f : α →ₘ[μ] γ) (n : ℤ), ↑(f ^ n) =ᵐ[μ] ↑f ^ n
-- Mathlib.Logic.Equiv.Defs
Equiv.existsUnique_congr_right : ∀ {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β), (∃! a, q (e a)) ↔ ∃! b, q b
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.domRestrict_mrange : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N),
  AddMonoidHom.mrange (f.domRestrict S) = AddSubmonoid.map f S