mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.mem_of_add_mem_left : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M},
  F.IsFaceOf C → ∀ {x y : M}, x ∈ C → y ∈ C → x + y ∈ F → x ∈ F
-- Lean.Meta.Order
/-- Given `inst : CCPO (t[x])` for some FVar `x`, constructs an instance
of the type `CCPO (∀ x, t[x])`.
Can handle `CompleteLattice` as well.
- -/
Lean.Meta.mkInstPiOfInstForall : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Finset.Lattice.Fold
/-- To rewrite from right to left, use `Finset.inf'_comp_eq_image`.  -/
Finset.inf'_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : DecidableEq β] {s : Finset γ}
  {f : γ → β} (hs : (Finset.image f s).Nonempty) (g : β → α), (Finset.image f s).inf' hs g = s.inf' ⋯ (g ∘ f)
-- Init.Data.Int.DivMod.Lemmas
Int.le_bmod : ∀ {x : ℤ} {m : ℕ}, 0 < m → -(↑m / 2) ≤ x.bmod m
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The multiplication morphism of a monoid object.  -/
CategoryTheory.MonObj.termμ : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.load.inj : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {a : Γ → σ → σ} {a_1 : Turing.TM1.Stmt Γ Λ σ} {a_2 : Γ → σ → σ}
  {a_3 : Turing.TM1.Stmt Γ Λ σ}, Turing.TM1.Stmt.load a a_1 = Turing.TM1.Stmt.load a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Data.Multiset.Functor
Multiset.map_comp_coe : ∀ {α β : Type u_1} (h : α → β), Functor.map h ∘ Multiset.ofList = Multiset.ofList ∘ Functor.map h
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.val_neg_addUnitsTypeEquivIsAddUnitAddSubmonoid_symm_apply : ∀ {M : Type u_4} [inst : AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)),
  ↑(-AddSubmonoid.addUnitsTypeEquivIsAddUnitAddSubmonoid.symm x) = ↑(-Classical.choose ⋯)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_zero : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b : M}, a ≡ b [PMOD 0] ↔ a = b
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.mk_apply : ∀ (R : Type uR) [inst : CommSemiring R] (A : Type u_1) (M : Type u_2) (N : Type u_3) [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module A M] [inst_5 : SMulCommClass R A M]
  [inst_6 : AddCommMonoid N] [inst_7 : Module R N] (m : M),
  (TensorProduct.AlgebraTensorModule.mk R A M N) m = { toFun := fun x2 => m ⊗ₜ[R] x2, map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Meta.Basic
Lean.Meta.instBEqSynthInstanceCacheKey : BEq Lean.Meta.SynthInstanceCacheKey
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {fallback : α}, t.get! (t.minD fallback) = t.minD fallback
-- Init.Data.Nat.Internal.Linear
_private.Init.Data.Nat.Internal.Linear.0.Nat.Internal.Linear.Expr.toPoly.go.match_1.eq_4 : ∀ (motive : Nat.Internal.Linear.Expr → Sort u_1) (k : ℕ) (a : Nat.Internal.Linear.Expr)
  (h_1 : (k : ℕ) → motive (Nat.Internal.Linear.Expr.num k))
  (h_2 : (i : Nat.Internal.Linear.Var) → motive (Nat.Internal.Linear.Expr.var i))
  (h_3 : (a b : Nat.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (k : ℕ) → (a : Nat.Internal.Linear.Expr) → motive (Nat.Internal.Linear.Expr.mulL k a))
  (h_5 : (a : Nat.Internal.Linear.Expr) → (k : ℕ) → motive (a.mulR k)),
  (match Nat.Internal.Linear.Expr.mulL k a with
    | Nat.Internal.Linear.Expr.num k => h_1 k
    | Nat.Internal.Linear.Expr.var i => h_2 i
    | a.add b => h_3 a b
    | Nat.Internal.Linear.Expr.mulL k a => h_4 k a
    | a.mulR k => h_5 a k) =
    h_4 k a
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- `backwardRfl` is true if `proof` is by a `@[backward_defeq]` theorem (i.e. rfl at default,
but not instance, transparency). Honored by `dsimp` only when
`backward.defeqAttrib.useBackward` is set.
 -/
Lean.Meta.SimpTheorem.backwardRfl : Lean.Meta.SimpTheorem → Bool
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.lift.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  [inst_5 : F.Additive], CategoryTheory.Mat_.lift F = CategoryTheory.Mat_.lift F_1
-- Mathlib.Algebra.Algebra.Spectrum.Basic
_private.Mathlib.Algebra.Algebra.Spectrum.Basic.0.«term↑ₐ» : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- **Alias** of the forward direction of `dvd_neg`.

---

An element `a` of a semigroup with a distributive negation divides the negation of an element
`b` iff `a` divides `b`.  -/
Dvd.dvd.of_neg_right : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : HasDistribNeg α] {a b : α}, a ∣ -b → a ∣ b
-- Mathlib.GroupTheory.IsSubnormal
/-- Subnormality is transitive.

This version involves an explicit `subtype`; the version `IsSubnormal.trans` does not.
 -/
Subgroup.IsSubnormal.trans' : ∀ {G : Type u_1} [inst : Group G] {K : Subgroup G} {H : Subgroup ↥K},
  H.IsSubnormal → K.IsSubnormal → (Subgroup.map K.subtype H).IsSubnormal
-- Mathlib.Data.Matrix.Basic
Matrix.piRingEquiv_symm_apply : ∀ {n : Type u_3} {ι : Type u_14} {β : ι → Type u_15} [inst : (i : ι) → AddCommMonoid (β i)]
  [inst_1 : (i : ι) → Mul (β i)] [inst_2 : Fintype n] (f : (i : ι) → Matrix n n (β i)),
  Matrix.piRingEquiv.symm f = Matrix.of fun j k i => f i j k
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_toLinearMap : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (f : A →ₐc[R] B), ⇑↑f = ⇑f
-- Mathlib.Order.Interval.Set.WithBotTop
WithBot.Ico_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico ↑b ↑a = WithBot.some '' Set.Ico b a
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_bot : ∀ {R : Type u_2} [inst : NonAssocRing R], ⊥.unop = ⊥
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_add_mul_I : ∀ (x y : ℂ),
  Complex.cos (x + y * Complex.I) = Complex.cos x * Complex.cosh y - Complex.sin x * Complex.sinh y * Complex.I
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ofList_cons : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {hd : α} {tl : List α},
  Std.ExtTreeSet.ofList (hd :: tl) cmp = (∅.insert hd).insertMany tl
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexRange_self : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι) (h : optParam (b i ∈ Set.range ⇑b) ⋯), b.reindexRange ⟨b i, h⟩ = b i
-- Lean.Data.Lsp.Basic
/-- Options for `CreateFile` and `RenameFile`.  -/
Lean.Lsp.CreateFile.Options : Type
-- Mathlib.Data.TypeVec
TypeVec.append1_drop_last : ∀ {n : ℕ} (α : TypeVec.{u_1} (n + 1)), α.drop ::: α.last = α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.equiv_iff_toList_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ ↔ Std.DTreeMap.Const.toList t₁ = Std.DTreeMap.Const.toList t₂
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffWithinAt_finsetSum' : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
  {f : ι → M → G}, (∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) → ContMDiffWithinAt I' I n (∑ i ∈ t, f i) s x
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- If a monotone function `u : ι → α` tends to `atTop` along *some* non-trivial filter `l`, then
it tends to `atTop` along `atTop`.  -/
Filter.tendsto_atTop_of_monotone_of_filter : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] [inst_1 : Preorder α] {l : Filter ι} {u : ι → α},
  Monotone u → ∀ [l.NeBot], Filter.Tendsto u l Filter.atTop → Filter.Tendsto u Filter.atTop Filter.atTop
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- **Alias** of the forward direction of `contDiffWithinAt_insert`. -/
ContDiffWithinAt.of_insert : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {y : E}, ContDiffWithinAt 𝕜 n f (insert y s) x → ContDiffWithinAt 𝕜 n f s x
-- Init.Data.Format.Basic
/-- Either all `Format.line`s in the group will be newlines, or all of them will be spaces.
 -/
Std.Format.FlattenBehavior.allOrNone : Std.Format.FlattenBehavior
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtComplexPlaces_apply_isReal : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.mixedEmbedding.mixedSpace K} (w : { w // w.IsReal }),
  NumberField.mixedEmbedding.normAtComplexPlaces x ↑w = x.1 w
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.hom_ext : ∀ {X Y : AddGrpCat} {f g : X ⟶ Y}, AddGrpCat.Hom.hom f = AddGrpCat.Hom.hom g → f = g
-- Lean.Elab.Match
Lean.Elab.Term.ToDepElimPattern.State.patternVars : Lean.Elab.Term.ToDepElimPattern.State → Array Lean.Expr
-- Mathlib.MeasureTheory.Constructions.Cylinders
/-- Given a finite set `s` of indices, a square cylinder is the product of a set `S` of
`∀ i : s, α i` and of `univ` on the other indices. The set `S` is a product of sets `t i` such that
for all `i : s`, `t i ∈ C i`.
`squareCylinders` is the set of all such square cylinders.  -/
MeasureTheory.squareCylinders : {ι : Type u_1} → {α : ι → Type u_2} → ((i : ι) → Set (Set (α i))) → Set (Set ((i : ι) → α i))
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
/-- Given `Φ : LocalizerMorphism W₁ W₂`, `L : C₂ ⥤ D` a localization functor for `W₂` and
a morphism `y : L.obj X₂ ⟶ X₃`, this is the functor which sends `R : Φ.RightResolution d` to
`(isoOfHom L W₂ R.w R.hw).inv ≫ y` in the category `w.CostructuredArrowDownwards y`
where `w` is `TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 _) (Functor.rightUnitor _).inv`.  -/
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.Constructor.fromRightResolution : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              {D : Type u_3} →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
                  (L : CategoryTheory.Functor C₂ D) →
                    [L.IsLocalization W₂] →
                      {X₂ : C₂} →
                        {X₃ : D} →
                          (y : L.obj X₂ ⟶ X₃) →
                            CategoryTheory.Functor (Φ.RightResolution X₂)
                              ((CategoryTheory.TwoSquare.mk Φ.functor (Φ.functor.comp L) L (CategoryTheory.Functor.id D)
                                    (Φ.functor.comp L).rightUnitor.inv).CostructuredArrowDownwards
                                y)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofChoiceInfo : Lean.Elab.ChoiceInfo → Lean.Elab.Info
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_subset_comm : ∀ {α : Type u_1} {s t : Set α}, sᶜ ⊆ t ↔ tᶜ ⊆ s
-- Mathlib.CategoryTheory.Equivalence
/-- Construct an isomorphism `G.inverse ⋙ F ≅ H` from an isomorphism `F ≅ G.functor ⋙ H`.  -/
CategoryTheory.Iso.inverseCompIso : {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] →
            {F : CategoryTheory.Functor C E} →
              {H : CategoryTheory.Functor D E} → {G : C ≌ D} → (F ≅ G.functor.comp H) → (G.inverse.comp F ≅ H)
-- Mathlib.Topology.Separation.Basic
compl_singleton_mem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x y : X}, y ≠ x → {x}ᶜ ∈ nhds y
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.det_mul_corner_pow : ∀ {S : Type u_2} {m : Type u_5} [inst : CommRing S] (M : Matrix m m S) [inst_1 : DecidableEq m] (k : m)
  [inst_2 : Fintype m],
  M.det * M k k ^ (Fintype.card m - 1) =
    M k k * ((M * Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun x => x = k) False).det
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.mk_comp_mkInv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W Y X]
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W Y Y] (f : Y ⟶ X) (hf : W f),
  (CategoryTheory.Localization.SmallHom.mk W f).comp (CategoryTheory.Localization.SmallHom.mkInv f hf) =
    CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id Y)
-- Mathlib.Topology.Order.Compact
IsCompact.exists_sInf_image_eq_and_le : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [inst_2 : TopologicalSpace β] [ClosedIicTopology α] {s : Set β},
  IsCompact s → s.Nonempty → ∀ {f : β → α}, ContinuousOn f s → ∃ x ∈ s, sInf (f '' s) = f x ∧ ∀ y ∈ s, f x ≤ f y
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedEMatchDiagInfo.default : Lean.Meta.Grind.EMatchDiagInfo
-- Mathlib.Order.Ideal
Order.Ideal.isProper_of_notMem : ∀ {P : Type u_1} [inst : LE P] {I : Order.Ideal P} {p : P}, p ∉ I → I.IsProper
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.mk_eq_one : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] {g : GL n R},
  Matrix.ProjGenLinGroup.mk g = 1 ↔ g ∈ Subgroup.center (GL n R)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.preimage_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] (a : α) (t : Set β),
  (fun x => a +ᵥ x) ⁻¹' t = -a +ᵥ t
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, panicking if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryLE! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap.Raw α (fun x => β) cmp → α → α × β
-- Mathlib.LinearAlgebra.Prod
LinearMap.fst_comp_inl : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], LinearMap.fst R M M₂ ∘ₗ LinearMap.inl R M M₂ = LinearMap.id
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_eq_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → ∀ {fallback : α}, t.maxKeyD fallback = Std.Internal.List.maxKeyD t.toListModel fallback
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p : ℤ) {Z : C}
  (h : ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj (CochainComplex.mappingCone.triangle φ).obj₁).X p ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
      (CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.triangle φ).mor₃.f p) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Data.Multiset.AddSub
Multiset.le_cons_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (a : α), s ≤ a ::ₘ s.erase a
-- Init.Data.List.Attach
List.count_attachWith : ∀ {α : Type u_1} [inst : BEq α] {p : α → Prop} {l : List α} (H : ∀ a ∈ l, p a) {a : { x // p x }},
  List.count a (l.attachWith p H) = List.count (↑a) l
-- Mathlib.Computability.Partrec
/-- Computable functions `α → β → σ` between `Primcodable` types  -/
Computable₂ : {α : Type u_1} →
  {β : Type u_2} → {σ : Type u_3} → [Primcodable α] → [Primcodable β] → [Primcodable σ] → (α → β → σ) → Prop
-- Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
/-- EGA IV₁, 1.4.7.1  -/
Module.Finite.exists_free_surjective : ∀ (R : Type u) (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Finite R S],
  ∃ S' x x_1,
    ∃ (_ : Module.Finite R S') (_ : Module.Free R S') (_ : Algebra.FinitePresentation R S'), ∃ f, Function.Surjective ⇑f
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.exponent_eq_card : ∀ {α : Type u_1} [inst : Group α] [IsCyclic α], Monoid.exponent α = Nat.card α
-- Mathlib.Order.Hom.Bounded
/-- Turn an element of a type `F` satisfying `BoundedOrderHomClass F α β` into an actual
`BoundedOrderHom`. This is declared as the default coercion from `F` to `BoundedOrderHom α β`.  -/
BoundedOrderHomClass.toBoundedOrderHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Preorder α] →
          [inst_2 : Preorder β] →
            [inst_3 : BoundedOrder α] →
              [inst_4 : BoundedOrder β] → [BoundedOrderHomClass F α β] → F → BoundedOrderHom α β
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.comp_mul_comm : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (T S : CentroidHom α) (a b : α),
  (⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)
-- Mathlib.Algebra.Order.Star.Basic
mul_star_self_pos : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [Nontrivial R] {x : R}, IsRegular x → 0 < x * star x
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_unique : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Unique α] (l : α →₀ R) (v : α → M), (Finsupp.linearCombination R v) l = l default • v default
-- Mathlib.Data.Set.Image
Nat.mem_range_succ : ∀ (i : ℕ), i ∈ Set.range Nat.succ ↔ 0 < i
-- Mathlib.Order.Category.BddLat
BddLat.Iso.mk_inv : ∀ {α β : BddLat} (e : ↑α.toLat ≃o ↑β.toLat),
  (BddLat.Iso.mk e).inv =
    BddLat.ofHom
      (have __src := { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯ };
      { toFun := ⇑e.symm, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ })
-- Mathlib.Algebra.GroupWithZero.Divisibility
dvd_and_not_dvd_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {x y : α}, x ∣ y ∧ ¬y ∣ x ↔ DvdNotUnit x y
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_insert_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  t.isEmpty = true → (t.insert k).min? = some k
-- Mathlib.Data.Rel
Function.mem_graph : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : α} {b : β}, (a, b) ∈ Function.graph f ↔ f a = b
-- Mathlib.Data.Sigma.Lex
Sigma.instReflLex : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [∀ (i : ι), Std.Refl (s i)],
  Std.Refl (Sigma.Lex r s)
-- Mathlib.Topology.Category.Sequential
/-- Constructor for objects of the category `Sequential`.  -/
Sequential.of : (X : Type u) → [inst : TopologicalSpace X] → [SequentialSpace X] → Sequential
-- Mathlib.Probability.Kernel.MeasurableLIntegral
ProbabilityTheory.Kernel.measurable_kernel_prodMk_left : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {t : Set (α × β)}, MeasurableSet t → Measurable fun a => (κ a) (Prod.mk a ⁻¹' t)
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib.congr_simp : ∀ {α : Type u_5} {β : Type u_6} {Ω : Type u_7} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {x : MeasurableSpace α} [inst_3 : MeasurableSpace β] (Y Y_1 : α → Ω),
  Y = Y_1 →
    ∀ (X X_1 : α → β),
      X = X_1 →
        ∀ (μ μ_1 : MeasureTheory.Measure α) (e_μ : μ = μ_1) [inst_4 : MeasureTheory.IsFiniteMeasure μ],
          ProbabilityTheory.condDistrib Y X μ = ProbabilityTheory.condDistrib Y_1 X_1 μ_1
-- Mathlib.Analysis.Normed.Module.Bases
/-- Coordinate functionals.  -/
GeneralSchauderBasis.coord : {β : Type u_3} →
  {𝕜 : Type u_4} →
    {X : Type u_5} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup X] →
          [inst_2 : NormedSpace 𝕜 X] → {L : SummationFilter β} → GeneralSchauderBasis β 𝕜 X L → β → StrongDual 𝕜 X
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.nonDegenerate_top_dim : ∀ (n : ℕ),
  (SSet.stdSimplex.obj { len := n }).nonDegenerate n =
    {SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op { len := n })))}
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_erase_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).size ≤ t.size
-- Mathlib.Analysis.CStarAlgebra.Spectrum
spectrum.norm_eq_one_of_unitary : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : NormedRing E] [inst_2 : StarRing E] [CStarRing E]
  [inst_4 : NormedAlgebra 𝕜 E] [CompleteSpace E] {u : E}, u ∈ unitary E → ∀ ⦃z : 𝕜⦄, z ∈ spectrum 𝕜 u → ‖z‖ = 1
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multispanIndexCoend_fst : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) (f : (CategoryTheory.Limits.multispanShapeCoend J).L),
  (CategoryTheory.Limits.multispanIndexCoend F).fst f =
    (F.map (CategoryTheory.Arrow.hom f).op).app (CategoryTheory.Arrow.left f)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroSMulDivisors_iff : ∀ {M₀ : Type u_1} {M : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Zero M] [inst_2 : MulAction M₀ M] {x : M₀},
  x ∈ nonZeroSMulDivisors M₀ M ↔ ∀ (m : M), x • m = 0 → m = 0
-- Mathlib.Probability.Distributions.Uniform
PMF.toOuterMeasure_ofMultiset_apply : ∀ {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) (t : Set α),
  (PMF.ofMultiset s hs).toOuterMeasure t =
    (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x => x ∈ t) s))) / ↑s.card
-- Mathlib.Order.RelSeries
RelSeries.snoc_self_eraseLast : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (h : p.length ≠ 0), p.eraseLast.snoc p.last ⋯ = p
-- Mathlib.Topology.Order.LawsonTopology
Topology.WithLawson.to_Lawson_symm_eq : ∀ {α : Type u_1}, Topology.WithLawson.toLawson.symm = Topology.WithLawson.ofLawson
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_nat_eq_descFactorial : ∀ (a b : ℕ), Polynomial.eval a (ascPochhammer ℕ b) = (a + b - 1).descFactorial b
-- Init.Data.Iterators.Basic
/-- Every iterator is a plausible indirect successor of itself.  -/
Std.IterM.IsPlausibleIndirectSuccessorOf.refl : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] (it : Std.IterM m β),
  it.IsPlausibleIndirectSuccessorOf it
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_sup : ∀ {R : Type u} [inst : LinearOrder R] (x y : Tropical R),
  Tropical.untrop (max x y) = max (Tropical.untrop x) (Tropical.untrop y)
-- Init.Data.BitVec.Lemmas
BitVec.sub_eq_add_neg : ∀ {n : ℕ} (x y : BitVec n), x - y = x + -y
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_of_nonpos_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c : R} [ExistsAddOfLE R] [PosMulMono R] [AddRightMono R]
  [AddRightReflectLE R], b ≤ a → c ≤ 0 → c * a ≤ c * b