mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
GenContFract.fib_le_of_contsAux_b : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K],
  n ≤ 1 ∨ ¬(GenContFract.of v).TerminatedAt (n - 2) → ↑(Nat.fib n) ≤ ((GenContFract.of v).contsAux n).b
-- Mathlib.Algebra.Group.Pi.Lemmas
Set.piecewise_inv : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Inv (f i)] (s : Set I) [inst_1 : (i : I) → Decidable (i ∈ s)]
  (f₁ g₁ : (i : I) → f i), s.piecewise f₁⁻¹ g₁⁻¹ = (s.piecewise f₁ g₁)⁻¹
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ F).app X =
    F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.instEpiGShortComplexObj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), CategoryTheory.Epi (Φ.shortComplexObj X).g
-- Mathlib.Tactic.Basic
/-- Given two arrays of `FVarId`s, one from an old local context and the other from a new local
context, pushes `FVarAliasInfo`s into the info tree for corresponding pairs of `FVarId`s.
Recall that variables linked this way should be considered to be semantically identical.

The effect of this is, for example, the unused variable linter will see that variables
from the first array are used if corresponding variables in the second array are used.  -/
Mathlib.Tactic.pushFVarAliasInfo : {m : Type → Type} →
  [Monad m] → [Lean.Elab.MonadInfoTree m] → Array Lean.FVarId → Array Lean.FVarId → Lean.LocalContext → m Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder_map : ∀ (ι : Type w) [inst : LinearOrder ι]
  {x y : CategoryTheory.Limits.WalkingMultispan (CategoryTheory.Limits.MultispanShape.ofLinearOrder ι)} (f : x ⟶ y),
  (CategoryTheory.Limits.WalkingMultispan.inclusionOfLinearOrder ι).map f =
    match x, y, f with
    | x, .(x), CategoryTheory.Limits.WalkingMultispan.Hom.id .(x) =>
      CategoryTheory.CategoryStruct.id
        (match x with
        | CategoryTheory.Limits.WalkingMultispan.left a => CategoryTheory.Limits.WalkingMultispan.left ↑a
        | CategoryTheory.Limits.WalkingMultispan.right b => CategoryTheory.Limits.WalkingMultispan.right b)
    | .(CategoryTheory.Limits.WalkingMultispan.left b),
      .(CategoryTheory.Limits.WalkingMultispan.right ((CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).fst b)),
      CategoryTheory.Limits.WalkingMultispan.Hom.fst b => CategoryTheory.Limits.WalkingMultispan.Hom.fst ↑b
    | .(CategoryTheory.Limits.WalkingMultispan.left b),
      .(CategoryTheory.Limits.WalkingMultispan.right ((CategoryTheory.Limits.MultispanShape.ofLinearOrder ι).snd b)),
      CategoryTheory.Limits.WalkingMultispan.Hom.snd b => CategoryTheory.Limits.WalkingMultispan.Hom.snd ↑b
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.Fix.dest_mk : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: MvQPF.Fix F α)),
  (MvQPF.Fix.mk x).dest = x
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instInfClosedSubgroup.eq_1 : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G],
  ClosedSubgroup.instInfClosedSubgroup G = { min := fun U V => { toSubgroup := ↑U ⊓ ↑V, isClosed' := ⋯ } }
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.pullbackObjIso_hom_comp_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPullbacks C] (f : F ⟶ H) (g : G ⟶ H) (d : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackObjIso f g d).hom
      (CategoryTheory.Limits.pullback.snd (f.app d) (g.app d)) =
    (CategoryTheory.Limits.pullback.snd f g).app d
-- Init.Data.List.Monadic
List.flatMapM_loop_eq : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m (List β)}
  {l : List α} {acc : List (List β)},
  List.flatMapM.loop f l acc = (fun x => acc.reverse.flatten ++ x) <$> List.flatMapM.loop f l []
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_singleton_le_iff_mem : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M)
  (p : Submodule R M), R ∙ m ≤ p ↔ m ∈ p
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_mul_left : ∀ {β : Type u_3} {α : Type u_5} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {a : α}, (s.gcd fun x => a * f x) = normalize a * s.gcd f
-- Mathlib.Data.Matrix.Mul
Matrix.mul_vecMulVec : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype m]
  (M : Matrix l m α) (x : m → α) (y : n → α), M * Matrix.vecMulVec x y = Matrix.vecMulVec (M.mulVec x) y
-- Std.Internal.Do.ExceptPost
Std.Internal.Do.EPost.Nil.mk.sizeOf_spec : sizeOf epost⟨⟩ = 1
-- Mathlib.NumberTheory.ADEInequality
ADEInequality.Admissible.one_lt_sumInv : ∀ {pqr : Multiset ℕ+}, ADEInequality.Admissible pqr → 1 < ADEInequality.sumInv pqr
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {km : α},
  t.min? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Algebra.Colimit.DirectLimit
/-- `map₀` as a `MonoidHom`.  -/
DirectLimit.map₀MonoidHom : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [inst_4 : Nonempty ι] →
                  [inst_5 : (i : ι) → MulOneClass (G i)] →
                    [inst_6 : ∀ (i j : ι) (h : i ≤ j), MonoidHomClass (T h) (G i) (G j)] →
                      ((i : ι) → G i) →* DirectLimit G f
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.defEvalConfigItem.visitStruct : Lean.Ident →
  Lean.Elab.ConfigEval.HandlerTrie✝ →
    Lean.Name → Lean.Name → Bool → Lean.Elab.ConfigEval.M✝ Lean.Elab.ConfigEval.HandlerTrie✝
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- The top additive subsemigroup is isomorphic to the additive semigroup.  -/
AddSubsemigroup.topEquiv : {M : Type u_1} → [inst : Add M] → ↥⊤ ≃+ M
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy
CategoryTheory.Arrow.RightHomotopy.compLeftId_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f : v ⟶ v}
  (h : CategoryTheory.Arrow.RightHomotopy f (CategoryTheory.CategoryStruct.id v)) (g : u ⟶ v),
  (h.compLeftId g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right g) h.hom
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.mk : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D : HomologicalComplex V c} →
            (hom : C ⟶ D) →
              (inv : D ⟶ C) →
                Homotopy (CategoryTheory.CategoryStruct.comp hom inv) (CategoryTheory.CategoryStruct.id C) →
                  Homotopy (CategoryTheory.CategoryStruct.comp inv hom) (CategoryTheory.CategoryStruct.id D) →
                    HomotopyEquiv C D
-- Aesop.Index.RulePattern
/-- An entry of the rule pattern index.  -/
Aesop.RulePatternIndex.Entry : Type
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_inverse_map_hom_app : ∀ {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] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  {X Y : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A} (f : X ⟶ Y) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).inverse.map f).hom.app X_1 =
    f.hom.app (Opposite.op (e.functor.obj (Opposite.unop X_1)))
-- Lean.Meta.DiscrTree.Util
/-- Extract the values stored in a `DiscrTree`.
 -/
Lean.Meta.DiscrTree.values : {α : Type} → Lean.Meta.DiscrTree α → Array α
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- A *simple continued fraction* (scf) is a generalized continued fraction (gcf) whose partial
numerators are equal to one.
$$
  h + \dfrac{1}
            {b_0 + \dfrac{1}
                         {b_1 + \dfrac{1}
                                      {b_2 + \dfrac{1}
                                                   {b_3 + \dots}}}}
$$
For convenience, one often writes `[h; b₀, b₁, b₂,...]`.
It is encoded as the subtype of gcfs that satisfy `GenContFract.IsSimpContFract`.
 -/
SimpContFract : (α : Type u_1) → [One α] → Type (max 0 u_1)
-- Mathlib.Computability.Halting
ComputablePred.eq_1 : ∀ {α : Type u_1} [inst : Primcodable α] (p : α → Prop), ComputablePred p = ∃ x, Computable fun a => decide (p a)
-- Mathlib.Data.Nat.Cast.Commute
SemiconjBy.natCast_mul_left : ∀ {α : Type u_1} [inst : Semiring α] {a x y : α}, SemiconjBy a x y → ∀ (n : ℕ), SemiconjBy (↑n * a) x y
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.simple_sq : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.simple i ^ 2 = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.homMk.eq_1 : ∀ {V : SSet.Truncated 2} {x₀ x₁ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  (e : SSet.Truncated.Edge x₀ x₁),
  SSet.Truncated.HomotopyCategory.homMk e =
    (SSet.Truncated.HomotopyCategory.quotientFunctor V).map (CategoryTheory.Cat.FreeRefl.homMk e)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.sup_mem_closed_subalgebra : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)),
  IsClosed ↑A → ∀ (f g : ↥A), ↑f ⊔ ↑g ∈ A
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.EssImageSubcategory.toUnit_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Full] [inst_5 : F.Faithful]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteProducts F] (X : F.EssImageSubcategory),
  CategoryTheory.SemiCartesianMonoidalCategory.toUnit X =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X.obj)
-- Init.Data.String.Slice
String.Slice.SplitIterator.operating : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} →
        [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
          s.Pos → Std.Iter (String.Slice.Pattern.SearchStep s) → String.Slice.SplitIterator pat s
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_neg : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p : Polynomial R), (-p).roots = p.roots
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_Ioc : ∀ {n : ℕ} (a b : Fin n), (Finset.Ioc ↑a ↑b).attachFin ⋯ = Finset.Ioc a b
-- Lean.HeadIndex
Lean.HeadIndex.lit.sizeOf_spec : ∀ (litVal : Lean.Literal), sizeOf (Lean.HeadIndex.lit litVal) = 1 + sizeOf litVal
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.Simprocs.addCore : Lean.Meta.Simprocs →
  Array Lean.Meta.SimpTheoremKey →
    Lean.Name → Bool → Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc → Lean.Meta.Simprocs
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.div_tendsto_atBot_of_degree_gt' : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q.degree < P.degree →
    P.leadingCoeff / Q.leadingCoeff < 0 →
      Filter.Tendsto (fun x => Polynomial.eval x P / Polynomial.eval x Q) Filter.atTop Filter.atBot
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.instBraidedCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.BraidedCategory (CategoryTheory.AddGrp C)
-- Lean.Meta.Tactic.Grind.Types
/-- Abstracts nested proofs in `e`. This is a preprocessing step performed before internalization.
 -/
Lean.Meta.Grind.abstractNestedProofs : Lean.Expr → Lean.Meta.Grind.GrindM Lean.Expr
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.dual_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sSupHom α β) (a : αᵒᵈ),
  (sSupHom.dual f) a = (⇑OrderDual.toDual ∘ ⇑f ∘ ⇑OrderDual.ofDual) a
-- Init.System.IO
/-- Runs `act` in a separate `Task`, with priority `prio`. Because `IO` actions may throw an exception
of type `IO.Error`, the result of the task is an `Except IO.Error α`.

Running the resulting `BaseIO` action causes the task to be started eagerly. Pure accesses to the
`Task` do not influence the impure `act`. Because `IO` actions may throw an exception of type
`IO.Error`, the result of the task is an `Except IO.Error α`.

Unlike pure tasks created by `Task.spawn`, tasks created by this function will run even if the last
reference to the task is dropped. The `act` should explicitly check for cancellation via
`IO.checkCanceled` if it should be terminated or otherwise react to the last reference being
dropped.
 -/
IO.asTask : {α : Type} → IO α → optParam Task.Priority Task.Priority.default → BaseIO (Task (Except IO.Error α))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_of_mem_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k : α},
      k ∈ Std.DHashMap.Raw.Const.insertMany m l → (List.map Prod.fst l).contains k = false → k ∈ m
-- Init.Data.Option.Monadic
Option.forM_eq_forM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m], Option.forM = forM
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- There is a unique monoid homomorphism between two monoids with a unique element.  -/
ContinuousMulEquiv.instUnique : {M : Type u_3} →
  {N : Type u_4} →
    [Unique M] →
      [Unique N] →
        [inst : Mul M] →
          [inst_1 : Mul N] → [inst_2 : TopologicalSpace M] → [inst_3 : TopologicalSpace N] → Unique (M ≃ₜ* N)
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- A sequence of functors from `ComposableArrows ι 1` to the abelian category.
The image of `mk₁ f` will be referred to as `H^n(f)` in the documentation.  -/
CategoryTheory.Abelian.SpectralObject.H : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι → ℤ → CategoryTheory.Functor (CategoryTheory.ComposableArrows ι 1) C
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomial_sorted : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {n : ℕ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomial basis_hd basis_tl n).Sorted
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.intCast_im : ∀ (x : GaussianInt), ↑x.im = (GaussianInt.toComplex x).im
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.ext_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] {s t : ContMDiffSection I F n V},
  s = t ↔ ∀ (x : M), s x = t x
-- Init.Data.SInt.Basic
instSubInt8 : Sub Int8
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemContKind.noConfusionType : Sort v✝ → Lean.Elab.Do.DoElemContKind → Lean.Elab.Do.DoElemContKind → Sort v✝
-- Init.Data.Nat.Mod
Nat.lt_of_mul_lt_mul_right : ∀ {a b c : ℕ}, b * a < c * a → b < c
-- Mathlib.Algebra.Notation.Prod
Prod.pow_def : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : Pow α E] [inst_1 : Pow β E] (p : α × β) (c : E),
  p ^ c = (p.1 ^ c, p.2 ^ c)
-- Mathlib.SetTheory.Ordinal.Topology
/-- An ordinal is an accumulation point of a set of ordinals if it is positive and there
are elements in the set arbitrarily close to the ordinal from below.  -/
Ordinal.IsAcc : Ordinal.{u_1} → Set Ordinal.{u_1} → Prop
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.UnderMorphism.ext_iff : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Under X} {f g : U ⟶ V},
  f = g ↔ CategoryTheory.Under.Hom.right f = CategoryTheory.Under.Hom.right g
-- Init.Data.Vector.InsertIdx
Vector.getElem_insertIdx_of_gt : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α} {i k : ℕ} (w : k ≤ n) (h : k > i), (xs.insertIdx i x ⋯)[k] = xs[k - 1]
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.FunctorPushforwardStructure.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} {S : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X} [inst_2 : SizeOf C]
  [inst_3 : SizeOf D] [inst_4 : ⦃Y : C⦄ → (a : Y ⟶ X) → SizeOf (S a)] (preobj : C) (premap : preobj ⟶ X)
  (lift : Y ⟶ F.obj preobj) (cover : S premap) (fac : f = CategoryTheory.CategoryStruct.comp lift (F.map premap)),
  sizeOf { preobj := preobj, premap := premap, lift := lift, cover := cover, fac := fac } =
    1 + sizeOf preobj + sizeOf premap + sizeOf lift + sizeOf cover + sizeOf fac
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List α}, (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).isEmpty = (m.isEmpty && l.isEmpty)
-- Mathlib.RingTheory.Ideal.Prime
/-- The prime ideal is not the entire ring.  -/
Ideal.IsPrime.ne_top' : ∀ {α : Type u} {inst : Semiring α} {I : Ideal α} [self : I.IsPrime], I ≠ ⊤
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.coe_mapAlgHom : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), ⇑(Polynomial.mapAlgHom f) = Polynomial.map ↑f
-- Mathlib.Algebra.Lie.Subalgebra
/-- An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is
preserved under addition, scalar multiplication and the Lie bracket, then `p` holds for all
elements of the Lie algebra spanned by `s`.  -/
LieSubalgebra.lieSpan_induction : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L}
  {p : (x : L) → x ∈ LieSubalgebra.lieSpan R L s → Prop},
  (∀ (x : L) (h : x ∈ s), p x ⋯) →
    p 0 ⋯ →
      (∀ (x y : L) (hx : x ∈ LieSubalgebra.lieSpan R L s) (hy : y ∈ LieSubalgebra.lieSpan R L s),
          p x hx → p y hy → p (x + y) ⋯) →
        (∀ (a : R) (x : L) (hx : x ∈ LieSubalgebra.lieSpan R L s), p x hx → p (a • x) ⋯) →
          ∀ {x : L},
            (∀ (x y : L) (hx : x ∈ LieSubalgebra.lieSpan R L s) (hy : y ∈ LieSubalgebra.lieSpan R L s),
                p x hx → p y hy → p ⁅x, y⁆ ⋯) →
              ∀ (hx : x ∈ LieSubalgebra.lieSpan R L s), p x hx
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
CategoryTheory.JointlyReflectIsomorphisms.quasiIsoAt_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{v_2, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  CategoryTheory.JointlyReflectIsomorphisms F →
    ∀ [inst_2 : CategoryTheory.Abelian C] [inst_3 : (i : I) → CategoryTheory.Abelian (D i)]
      [inst_4 : CategoryTheory.CategoryWithHomology C]
      [inst_5 : ∀ (i : I), CategoryTheory.Limits.PreservesFiniteLimits (F i)]
      [∀ (i : I), CategoryTheory.Limits.PreservesFiniteColimits (F i)] {α : Type u_4} {c : ComplexShape α}
      {K L : HomologicalComplex C c} (f : K ⟶ L) (a : α),
      QuasiIsoAt f a ↔ ∀ (i : I), QuasiIsoAt (((F i).mapHomologicalComplex c).map f) a
-- Mathlib.Order.Defs.LinearOrder
not_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
-- Init.Meta.Defs
Lean.Syntax.decodeQuotedChar : String → String.Pos.Raw → Option (Char × String.Pos.Raw)
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- Delaborate a projection primitive. These do not usually occur in
user code, but are pretty-printed when e.g. `#print`ing a projection
function.
 -/
Lean.PrettyPrinter.Delaborator.delabProj : Lean.PrettyPrinter.Delaborator.Delab
-- Std.Do.WP.SimpLemmas
Std.Do.WP.modify_MonadStateOf : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} {Q : Std.Do.PostCond PUnit.{u + 1} ps}
  [inst : Std.Do.WP m ps] [inst_1 : MonadStateOf σ m] (f : σ → σ),
  (Std.Do.wp (modify f)).apply Q = (Std.Do.wp (MonadStateOf.modifyGet fun s => (PUnit.unit, f s))).apply Q
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.isOpen_iff : ∀ {α : Type u_1} {s : Set α} {D : Set (Set α)} [inst : Preorder α] [t : TopologicalSpace α]
  [Topology.IsScottHausdorff α D],
  IsOpen s ↔
    ∀ ⦃d : Set α⦄,
      d ∈ D →
        d.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) d → ∀ ⦃a : α⦄, IsLUB d a → a ∈ s → ∃ b ∈ d, Set.Ici b ∩ d ⊆ s
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Subgroup.subgroupOfContinuousMulEquivOfLe_symm_apply : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {H K : Subgroup G} (hHK : H ≤ K) (g : ↥H),
  (Subgroup.subgroupOfContinuousMulEquivOfLe hHK).symm g = ⟨⟨↑g, ⋯⟩, ⋯⟩
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.StringSliceInvariant.eq_1 : ∀ (s : String.Slice) (β Pred : Type u), Std.Internal.Do.StringSliceInvariant s β Pred = (s.Pos → β → Pred)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.divisionCommMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → DivisionCommMonoid (f i)],
  Pi.divisionCommMonoid = { toDivisionMonoid := Pi.divisionMonoid, mul_comm := ⋯ }
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.isDPMorphism_def : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) (f : A →+* B),
  hI.IsDPMorphism hJ f ↔ Ideal.map f I ≤ J ∧ ∀ {n : ℕ}, ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
-- Mathlib.Topology.Separation.Hausdorff
/-- If `s` and `t` are compact sets in a T₂ space, then the set neighborhoods filter of `s ∩ t`
is the infimum of set neighborhoods filters for `s` and `t`.

For general sets, only the `≤` inequality holds, see `nhdsSet_inter_le`.  -/
IsCompact.nhdsSet_inter_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {s t : Set X},
  IsCompact s → IsCompact t → nhdsSet (s ∩ t) = nhdsSet s ⊓ nhdsSet t
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category_id_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.CategoryStruct.id sq).τ₃ = CategoryTheory.CategoryStruct.id sq.X₃