mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Subsemigroup.Center
/-- The center of a magma is commutative and associative.  -/
Subsemigroup.center.commSemigroup : {M : Type u_1} → [inst : Mul M] → CommSemigroup ↥(Subsemigroup.center M)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.Const.maxEntry!.eq_def : ∀ {α : Type u} {β : Type v} [inst : Inhabited (α × β)] (x : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.maxEntry! x =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.Const.maxEntry!" 839 13
        "Map is empty"
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => (k, v)
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      Std.DTreeMap.Internal.Impl.Const.maxEntry! r
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.instRefl : ∀ {n : ℕ}, Std.Refl n.ModEq
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.instIsStableUnderCompositionComap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.Precoverage D} [J.IsStableUnderComposition],
  (CategoryTheory.Precoverage.comap F J).IsStableUnderComposition
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- `f` is the equalizer of the two maps  -/
CategoryTheory.RegularMono.isLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (self : CategoryTheory.RegularMono f) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `IsUnit.mul_le_mul_right`. -/
IsUnit.le_of_mul_le_mul_right : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b c : M}, IsUnit c → a * c ≤ b * c → a ≤ b
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A short complex `S` has homology when there exists a `S.HomologyData`  -/
CategoryTheory.ShortComplex.HasHomology : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Prop
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.eq_1 : ∀ {α : Type u_2} (s : Set α) (r : α → α → Prop), s.PartiallyWellOrderedOn r = WellQuasiOrdered (Subrel r fun x => x ∈ s)
-- Init.Control.Lawful.MonadAttach.Instances
instWeaklyLawfulMonadAttachOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m], WeaklyLawfulMonadAttach m
-- Lean.AuxRecursor
Lean.mkCasesOnName : Lean.Name → Lean.Name
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.supported_mono : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  {s t : Set M}, s ⊆ t → AddMonoidAlgebra.supported R S s ≤ AddMonoidAlgebra.supported R S t
-- Std.Http.Data.Body.Full
Std.Http.Body.instCoeResponseFullAny : Coe (Std.Http.Response Std.Http.Body.Full) (Std.Http.Response Std.Http.Body.Any)
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_inverse_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑Y)ᵒᵖ C) (X_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).inverse.obj G).obj X_1 =
    G.obj (Opposite.op ((TopologicalSpace.Opens.map H.inv).obj (Opposite.unop X_1)))
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsType₂.δ_simplex : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N}
  (hx : SSet.prodStdSimplex.pairingCore.IsType₂ x) {d : ℕ} (hd : x.dim = d),
  (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.SimplicialObject.δ
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := m + 1 })
            (SSet.stdSimplex.obj { len := n }))
          (SSet.prodStdSimplex.pairingCore.min x hd).castSucc))
      (hx.simplex hd) =
    (x.cast hd).simplex
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- - `∏ x, f x` is notation for `Finset.prod Finset.univ f`. It is the product of `f x`,
  where `x` ranges over the finite domain of `f`.
- `∏ x ∈ s, f x` is notation for `Finset.prod s f`. It is the product of `f x`,
  where `x` ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
- `∏ x ∈ s with p x, f x` is notation for `Finset.prod (Finset.filter p s) f`.
- `∏ x ∈ s with h : p x, f x h` is notation for
  `Finset.prod s fun x ↦ if h : p x then f x h else 1`.
- `∏ (x ∈ s) (y ∈ t), f x y` is notation for `Finset.prod (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y)`.

These support destructuring, for example `∏ ⟨x, y⟩ ∈ s ×ˢ t, f x y`.

Notation: `"∏" bigOpBinders* ("with" (ident ":")? term)? "," term`  -/
BigOperators.bigprod : Lean.ParserDescr
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_eq_mk'_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : ↥S),
  IsLocalizedModule.mk' f m₁ s₁ = IsLocalizedModule.mk' f m₂ s₂ ↔ ∃ s, s • s₁ • m₂ = s • s₂ • m₁
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.of_biUnion_eq_of_finite : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  {U : Set S} (s : Set (Set S)),
  ⋃ t ∈ s, t = U → s.Finite → (∀ t ∈ s, IsCompactOpenCovered f t) → IsCompactOpenCovered f U
-- Init.Data.Iterators.Basic
Std.IterM.mk_internalState : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} (it : Std.IterM m β),
  { internalState := it.internalState } = it
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.filter f t) k =
    (Std.ExtDTreeMap.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.fold_filterM : ∀ {ps : Std.Do.PostShape} {α β δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Std.Do.WPMonad n ps] [inst_7 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n]
  {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → δ} {init : δ} {it : Std.Iter β} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← f b
          pure (if __do_lift.down = true then g d b else d))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.Iter.filterM f it) ⦃Q⦄
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.full_sheafPushforwardContinuous : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] [inst_3 : CategoryTheory.Functor.IsDenseSubsite J K G],
  (G.sheafPushforwardContinuous A J K).Full
-- Lean.Level
Lean.Level.updateMax! : Lean.Level → Lean.Level → Lean.Level → Lean.Level
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model on a `TangentBundle`  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromTangentBundle : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.rootSet_maps_to' : ∀ {T : Type w} [inst : CommRing T] {p : Polynomial T} {S : Type u_1} {S' : Type u_2} [inst_1 : CommRing S]
  [inst_2 : IsDomain S] [inst_3 : Algebra T S] [inst_4 : CommRing S'] [inst_5 : IsDomain S'] [inst_6 : Algebra T S'],
  (Polynomial.map (algebraMap T S') p = 0 → Polynomial.map (algebraMap T S) p = 0) →
    ∀ (f : S →ₐ[T] S'), Set.MapsTo (⇑f) (p.rootSet S) (p.rootSet S')
-- Mathlib.Data.Fin.Tuple.Reflection
_private.Mathlib.Data.Fin.Tuple.Reflection.0.FinVec.seq.match_1.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (motive : (x : ℕ) → (Fin x → α → β) → (Fin x → α) → Sort u_1) (x : Fin 0 → α → β)
  (x_1 : Fin 0 → α) (h_1 : (x : Fin 0 → α → β) → (x_2 : Fin 0 → α) → motive 0 x x_2)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → α → β) → (v : Fin (n + 1) → α) → motive n.succ f v),
  (match 0, x, x_1 with
    | 0, x, x_2 => h_1 x x_2
    | n.succ, f, v => h_2 n f v) =
    h_1 x x_1
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.lof_coprodIsoDirectSum_inv_apply : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : DecidableEq ι]
  [inst_2 : CategoryTheory.Limits.HasCoproduct Z] (i : ι) (x : ↑(Z i)),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.coprodIsoDirectSum Z).inv)
      ((DirectSum.lof R ι (fun i => ↑(Z i)) i) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι Z i)) x
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.zeroLocus_isClosed : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op U))), IsClosed (X.zeroLocus s)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndependent.span_repr_eq : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (hv : LinearIndependent R v) [inst_3 : Nontrivial R] (x : ↥(Submodule.span R (Set.range v))),
  Span.repr R (Set.range v) x = Finsupp.equivMapDomain (Equiv.ofInjective v ⋯) (hv.repr x)
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Do not use this. Use `_root_.mul_le_mul_of_nonneg_right` instead.  -/
MulPosMono.mul_le_mul_of_nonneg_right : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : Zero α} {inst_2 : Preorder α} [self : MulPosMono α] ⦃c : α⦄,
  0 ≤ c → ∀ ⦃a b : α⦄, a ≤ b → a * c ≤ b * c
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.term.sizeOf_spec : ∀ (term : Lean.Term) (expr : Lean.Expr), sizeOf (Aesop.ElabRuleTerm.term term expr) = 1 + sizeOf term + sizeOf expr
-- Mathlib.CategoryTheory.Monad.Limits
/-- If `C` has colimits of shape `J` then any reflective subcategory has colimits of shape `J`.  -/
CategoryTheory.hasColimitsOfShape_of_reflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type u} [inst_2 : CategoryTheory.Category.{v, u} J] (R : CategoryTheory.Functor D C)
  [CategoryTheory.Reflective R] [CategoryTheory.Limits.HasColimitsOfShape J C],
  CategoryTheory.Limits.HasColimitsOfShape J D
-- Mathlib.Algebra.Group.Defs
nsmulRecAuto.eq_1 : ∀ {M : Type u_2} [inst : AddSemigroup M] [inst_1 : Zero M] (k : ℕ) (m : M), nsmulRecAuto k m = nsmulRec k m
-- Init.Data.Slice.Array.Basic
instSliceableArrayNatSubarray_6 : {α : Type u} → Std.Ric.Sliceable (Array α) ℕ (Subarray α)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
le_of_mul_le_right : ∀ {α : Type u} [inst : Mul α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] {a b c : α}, a * b ≤ c → b ≤ c
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.traceAux.congr_simp : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w}
  {inst_3 : DecidableEq ι} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι] (b b_1 : Module.Basis ι R M),
  b = b_1 → LinearMap.traceAux R b = LinearMap.traceAux R b_1
-- Init.Data.Int.Order
Int.neg_pos : ∀ {a : ℤ}, 0 < -a ↔ a < 0
-- Mathlib.Data.Matrix.Diagonal
Matrix.map_natCast : ∀ {n : Type u_3} {α : Type v} {β : Type w} [inst : DecidableEq n] [inst_1 : AddMonoidWithOne α] [inst_2 : Zero β]
  {f : α → β}, f 0 = 0 → ∀ (d : ℕ), (↑d).map f = Matrix.diagonal fun x => f ↑d
-- Mathlib.Data.NNRat.Defs
/-- **Alias** of the reverse direction of `Rat.toNNRat_eq_zero`. -/
Rat.toNNRat_of_nonpos : ∀ {q : ℚ}, q ≤ 0 → q.toNNRat = 0
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Comonad.comparison_faithful_of_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} [L.Faithful] (h : L ⊣ R),
  (CategoryTheory.Comonad.comparison h).Faithful
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressEnd.message? : Lean.Lsp.WorkDoneProgressEnd → Option String
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_subset_div_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t
-- Lean.Meta.Instances
Lean.Meta.InstanceEntry.val : Lean.Meta.InstanceEntry → Lean.Expr
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_bi_mul_le_r : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), b (AkraBazziRecurrence.min_bi b) / 2 * ↑n ≤ ↑(r i n)
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_ofSubtype : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] {p : α → Prop} [inst_2 : DecidablePred p]
  [inst_3 : Fintype (Subtype p)] (f : Equiv.Perm (Subtype p)),
  Equiv.Perm.sign (Equiv.Perm.ofSubtype f) = Equiv.Perm.sign f
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.instIsRightKanExtensionRightKanExtensionRightKanExtensionCounit : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasRightKanExtension F],
  (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- Expresses the integral over `Ioi 0` of `t ^ (a - 1) * exp (-(r * t))`, for positive real `r`,
in terms of the Gamma function.  -/
Real.integral_rpow_mul_exp_neg_mul_Ioi : ∀ {a r : ℝ}, 0 < a → 0 < r → ∫ (t : ℝ) in Set.Ioi 0, t ^ (a - 1) * Real.exp (-(r * t)) = (1 / r) ^ a * Real.Gamma a
-- Mathlib.Topology.Sober
/-- A space is quasi-sober if it can be covered by open quasi-sober subsets.  -/
quasiSober_of_open_cover : ∀ {α : Type u_1} [inst : TopologicalSpace α] (S : Set (Set α)),
  (∀ (s : ↑S), IsOpen ↑s) → ∀ [∀ (s : ↑S), QuasiSober ↑↑s], ⋃₀ S = ⊤ → QuasiSober α
-- Mathlib.MeasureTheory.VectorMeasure.WithDensity
MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) {f : α → ℝ},
  MeasureTheory.Integrable f μ →
    ∀ {i : Set α}, MeasurableSet i → ((μ.withDensityᵥ f).trim hm) i = ∫ (x : α) in i, f x ∂μ
-- Mathlib.Tactic.Translate.Core
/-- Insert only one direction of a translation.  -/
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.insertTranslation.insertTranslationAux : Lean.Name →
  Lean.Syntax →
    Lean.Name → Mathlib.Tactic.Translate.TranslateData → Mathlib.Tactic.Translate.TranslationInfo → Lean.CoreM Unit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.differentiableOn_arcsin : DifferentiableOn ℝ Real.arcsin {-1, 1}ᶜ
-- Init.System.IOError
/-- The operation failed due to a hardware problem, such as an I/O error.

This corresponds to the POSIX error `EIO`.
 -/
IO.Error.hardwareFault : UInt32 → String → IO.Error
-- Mathlib.Algebra.Ring.Subsemiring.Defs
SubsemiringClass.nontrivial : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : SetLike S R] [hSR : SubsemiringClass S R] (s : S)
  [Nontrivial R], Nontrivial ↥s
-- Mathlib.Data.List.Sigma
List.kunion.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (x x_1 : List (Sigma β)),
  x.kunion x_1 =
    match x, x_1 with
    | [], l₂ => l₂
    | s :: l₁, l₂ => s :: l₁.kunion (List.kerase s.fst l₂)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
/-- The associator for tensor, `(X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z)` in `Dial C`.  -/
CategoryTheory.Dial.associatorImpl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] →
      [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
        (X Y Z : CategoryTheory.Dial C) → (X.tensorObjImpl Y).tensorObjImpl Z ≅ X.tensorObjImpl (Y.tensorObjImpl Z)
-- Init.Data.List.Perm
List.Perm.prod_nat : ∀ {l₁ l₂ : List ℕ}, l₁.Perm l₂ → l₁.prod = l₂.prod
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.commonNeighbors_subset_neighborSet_right : ∀ {V : Type u} (G : SimpleGraph V) (v w : V), G.commonNeighbors v w ⊆ G.neighborSet w
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.mem_domain_baseEmbedding : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) {x : M}
  {c : FiniteArchimedeanClass M}, x ∈ seed.stratum c → x ∈ seed.baseEmbedding.domain
-- Init.Data.Ord.UInt
UInt32.instOrd : Ord UInt32
-- Mathlib.Probability.Kernel.Composition.CompNotation
MeasureTheory.Measure.deterministic_comp_eq_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β} (hf : Measurable f), μ.bind ⇑(ProbabilityTheory.Kernel.deterministic f hf) = MeasureTheory.Measure.map f μ
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.mem_cutMap_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : DivisionRing β] {a : α} {b : β},
  b ∈ LinearOrderedField.cutMap β a ↔ ∃ q, ↑q < a ∧ ↑q = b
-- Mathlib.Algebra.Module.Torsion.Basic
/-- Unexpander for `torsionBy`.  -/
AddSubgroup.torsionByUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.mapIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f] {X' Y' : C} (f' : X' ⟶ Y')
  [inst_3 : CategoryTheory.Limits.HasCokernel f'] (p : X ≅ X') (q : Y ≅ Y')
  (w : CategoryTheory.CategoryStruct.comp f q.hom = CategoryTheory.CategoryStruct.comp p.hom f'),
  (CategoryTheory.Limits.cokernel.mapIso f f' p q w).inv = CategoryTheory.Limits.cokernel.map f' f p.inv q.inv ⋯
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Connected.exists_walk_length_eq_dist : ∀ {V : Type u_1} {G : SimpleGraph V}, G.Connected → ∀ (u v : V), ∃ p, p.length = G.dist u v
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.lift.congr_simp : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (S : AddSubgroup M) (f f_1 : NormedAddGroupHom M N) (e_f : f = f_1) (hf : ∀ s ∈ S, f s = 0),
  NormedAddGroupHom.lift S f hf = NormedAddGroupHom.lift S f_1 ⋯
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.iterate_monotone : ∀ (n : ℕ), Monotone fun f => (⇑f)^[n]
-- Mathlib.RingTheory.Algebraic.Basic
Subalgebra.algebra_isAlgebraic_bot_left_iff : ∀ {R : Type u} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Function.Injective ⇑(algebraMap R S) → (Algebra.IsAlgebraic (↥⊥) S ↔ Algebra.IsAlgebraic R S)
-- Mathlib.RingTheory.WittVector.IsPoly
/-- The function that is constantly zero on Witt vectors is a polynomial function.  -/
WittVector.zeroIsPoly : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], WittVector.IsPoly p fun x x_1 x_2 => 0
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.inv_eq_zero : ∀ {k : Type u_2} [inst : Field k] {φ : PowerSeries k}, φ⁻¹ = 0 ↔ PowerSeries.constantCoeff φ = 0
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Schwartz functions as bounded continuous functions  -/
SchwartzMap.toBoundedContinuousFunction : {E : Type u_5} →
  {F : Type u_6} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → SchwartzMap E F → BoundedContinuousFunction E F
-- Init.Data.BitVec.Lemmas
BitVec.reverse_cast : ∀ {w v : ℕ} (h : w = v) (x : BitVec w), (BitVec.cast h x).reverse = BitVec.cast h x.reverse
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.mk.sizeOf_spec : ∀ {B : Type u_1} {M : CoxeterMatrix B} {W : Type u_2} [inst : Group W] [inst_1 : SizeOf B] [inst_2 : SizeOf W]
  (mulEquiv : W ≃* M.Group), sizeOf { mulEquiv := mulEquiv } = 1 + sizeOf mulEquiv
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- `cell C n` is finite for every `n`.  -/
Topology.RelCWComplex.FiniteType.finite_cell : ∀ {X : Type u} {inst : TopologicalSpace X} {C D : Set X} {inst_1 : Topology.RelCWComplex C D}
  [self : Topology.RelCWComplex.FiniteType C] (n : ℕ), Finite (Topology.RelCWComplex.cell C n)
-- Mathlib.Algebra.CharP.Defs
CharP.mk : ∀ {R : Type u_2} [inst : AddMonoidWithOne R] {p : outParam ℕ}, (∀ (x : ℕ), ↑x = 0 ↔ p ∣ x) → CharP R p
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.one_mul : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a : FreeAlgebra.Pre R X}, FreeAlgebra.Rel R X (1 * a) a
-- Mathlib.Data.Vector.Mem
List.Vector.head_mem : ∀ {α : Type u_1} {n : ℕ} (v : List.Vector α (n + 1)), v.head ∈ v.toList
-- Mathlib.Probability.Process.LocalProperty
_private.Mathlib.Probability.Process.LocalProperty.0.ProbabilityTheory.mkStrictMonoAux_strictMono : ∀ (x : ℕ → ℕ), StrictMono (ProbabilityTheory.mkStrictMonoAux✝ x)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
fderiv_sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → fderiv ℝ (fun x => Real.sinh (f x)) x = Real.cosh (f x) • fderiv ℝ f x
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNatClamp n).toUInt8 = UInt8.ofNat n
-- Mathlib.Data.List.Cycle
List.prev_infix_of_mem_tail : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α} (ha : a ∈ l), a ≠ l.head ⋯ → [l.prev a ha, a] <:+: l
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.extractAndExtendAux.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n' : ℕ) (h_1 : n'.succ = 0 → motive 0)
  (h_2 : (n'_1 : ℕ) → n'.succ = n'_1.succ → motive n'_1.succ),
  (match hwi : n'.succ with
    | 0 => h_1 hwi
    | n'_1.succ => h_2 n'_1 hwi) =
    h_2 n' ⋯
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_ne_one_iff`. -/
Ideal.ramificationIdx_ne_one_iff : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  {P : Ideal S}, Ideal.map (algebraMap R S) p ≤ P → (p.ramificationIdx' P ≠ 1 ↔ Ideal.map (algebraMap R S) p ≤ P ^ 2)
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tsnd_id : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α β : Type u},
  Bitraversable.tsnd pure = pure
-- Mathlib.Logic.Encodable.Basic
Quotient.rep_spec : ∀ {α : Type u_1} {s : Setoid α} [inst : DecidableRel fun x1 x2 => x1 ≈ x2] [inst_1 : Encodable α] (q : Quotient s),
  ⟦q.rep⟧ = q
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_toSubalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (s : IntermediateField K L)
  (x : L), x ∈ s.toSubalgebra ↔ x ∈ s
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RccSliceData.range : {α : Type u} → {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RccSliceData α β → Std.Rcc α