mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.ModularLattice
instIsWeakUpperModularLatticeOrderDual : ∀ {α : Type u_1} [inst : Lattice α] [IsWeakLowerModularLattice α], IsWeakUpperModularLattice αᵒᵈ
-- Aesop.Forward.State
/-- Remove the pattern substitution `subst` from `slot` and all later slots.
For each mapping `s ↦ e ↦ (ms, hs)` in `imap`, if `s ≥ slot`, then `subst` is
removed from `hs` and any matches containing `subst` are removed from `ms`.  -/
Aesop.InstMap.erasePatSubst : Aesop.InstMap → Aesop.Substitution → Aesop.SlotIndex → Aesop.InstMap
-- Lean.Server.Rpc.Basic
Lean.Lsp.instFromJsonRpcWireFormat : Lean.FromJson Lean.Lsp.RpcWireFormat
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instNonUnitalNonAssocSemiring : {α : Type u_1} →
  [DecidableEq α] →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : PartialOrder α] → [CanonicallyOrderedAdd α] → NonUnitalNonAssocSemiring (WithTop α)
-- Init.Data.UInt.Bitwise
UInt16.toUInt64_not : ∀ (a : UInt16), (~~~a).toUInt64 = ~~~a.toUInt64 % 65536
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.map_ofFixingAddSubgroupUnion_bijective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α},
  Function.Bijective ⇑(SubAddAction.map_ofFixingAddSubgroupUnion M s t)
-- Mathlib.RingTheory.Unramified.LocalStructure
HasStandardEtaleSurjectionOn.of_dvd : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f g : S},
  HasStandardEtaleSurjectionOn R f → f ∣ g → HasStandardEtaleSurjectionOn R g
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.instInhabitedPostponeBehavior : Inhabited Lean.Elab.Term.PostponeBehavior
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.reducible_notMem_factorSet : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] {p : Associates α},
  ¬Irreducible p → ∀ (s : Associates.FactorSet α), p ∉ s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The sine of `π / 3` is `√3 / 2`.  -/
Real.sin_pi_div_three : Real.sin (Real.pi / 3) = √3 / 2
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.nonempty : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} [M.RankPos], M.IsBase B → B.Nonempty
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- Promotes a bijective coalgebra homomorphism to a coalgebra equivalence.  -/
CoalgEquiv.ofBijective : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] →
                  [inst_6 : CoalgebraStruct R B] → {f : A →ₗc[R] B} → Function.Bijective ⇑f → A ≃ₗc[R] B
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The composition of the inverse of the isomorphism `pullbackSpecIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the first projection is
the morphism `Spec (S ⊗[R] T) ⟶ Spec S` obtained by applying `Spec.map` to the ring morphism
`s ↦ s ⊗ₜ[R] 1`.
 -/
AlgebraicGeometry.pullbackSpecIso_inv_fst_assoc : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of S) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
        h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom)) h
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
/-- The adjunction between `A ⊗ -` and `A ⟹ -`.  -/
CategoryTheory.ihom.adjunction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : C) →
        [inst_2 : CategoryTheory.Closed A] → CategoryTheory.MonoidalCategory.tensorLeft A ⊣ CategoryTheory.ihom A
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_le_omega_one : ∀ {o : Ordinal.{u}}, Ordinal.lift.{v, u} o ≤ Ordinal.omega 1 ↔ o ≤ Ordinal.omega 1
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- Make a morphism in `Truncated n` from a morphism in `SimplexCategory`. This
is equivalent to `@id (⦋a⦌ₙ ⟶ ⦋b⦌ₙ) f`.  -/
SimplexCategory.Truncated.Hom.tr : {n : ℕ} →
  {a b : SimplexCategory} →
    (a ⟶ b) →
      (ha : autoParam (a.len ≤ n) SimplexCategory.Truncated.Hom.tr._auto_1) →
        (hb : autoParam (b.len ≤ n) SimplexCategory.Truncated.Hom.tr._auto_3) →
          { obj := a, property := ha } ⟶ { obj := b, property := hb }
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Colim
/-- Given `S : ShortComplex (J ⥤ C)` and (colimit) cocones for `S.X₁`, `S.X₂`,
`S.X₃` equipped with suitable data, this is the induced
short complex `c₁.pt ⟶ c₂.pt ⟶ c₃.pt`.  -/
CategoryTheory.Limits.colim.mapShortComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} J] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (S : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) →
            {c₁ : CategoryTheory.Limits.Cocone S.X₁} →
              CategoryTheory.Limits.IsColimit c₁ →
                (c₂ : CategoryTheory.Limits.Cocone S.X₂) →
                  (c₃ : CategoryTheory.Limits.Cocone S.X₃) →
                    (f : c₁.pt ⟶ c₂.pt) →
                      (g : c₂.pt ⟶ c₃.pt) →
                        (∀ (j : J),
                            CategoryTheory.CategoryStruct.comp (c₁.ι.app j) f =
                              CategoryTheory.CategoryStruct.comp (S.f.app j) (c₂.ι.app j)) →
                          (∀ (j : J),
                              CategoryTheory.CategoryStruct.comp (c₂.ι.app j) g =
                                CategoryTheory.CategoryStruct.comp (S.g.app j) (c₃.ι.app j)) →
                            CategoryTheory.ShortComplex C
-- Mathlib.Order.BooleanAlgebra.Basic
disjoint_sdiff_self_left : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], Disjoint (y \ x) x
-- Init.Data.Option.Lemmas
Option.min_some_guard : ∀ {α : Type u_1} [inst : Min α] [Std.IdempotentOp min] {x : α} {p : α → Bool},
  some x ⊓ Option.guard p x = Option.guard p x
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.splitMin'.match_1.eq_1 : ∀ {α : Type u_1} (motive : α × Ordnode α → Sort u_2) (xm : α) (l' : Ordnode α)
  (h_1 : (xm : α) → (l' : Ordnode α) → motive (xm, l')),
  (match (xm, l') with
    | (xm, l') => h_1 xm l') =
    h_1 xm l'
-- Mathlib.Algebra.Order.Group.Defs
LinearOrderedAddCommGroup.to_noMinOrder : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Nontrivial α], NoMinOrder α
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_norm_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], ‖K.starProjection‖ ≤ 1
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X : C} {F : CategoryTheory.Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F),
  J.yonedaEquiv f =
    (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op X))) (CategoryTheory.CategoryStruct.id X)
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- Note that this instance also provides `Algebra R R[X]`.  -/
Polynomial.algebraOfAlgebra : {R : Type u} → {A : Type z} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Algebra R A] → Algebra R (Polynomial A)
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.comp_lift : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra.FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I)
  (g : A →ₐ[R] B ⧸ I), (Ideal.Quotient.mkₐ R I).comp (Algebra.FormallySmooth.lift I hI g) = g
-- Init.Data.Option.Attach
Option.isSome_attach : ∀ {α : Type u_1} (o : Option α), o.attach.isSome = o.isSome
-- Lean.Meta.Tactic.NormCast
/-- Classifies a declaration of type `ty` as a `norm_cast` rule.  -/
Lean.Meta.NormCast.classifyType : Lean.Expr → Lean.MetaM Lean.Meta.NormCast.Label
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.rangeRestrict_surjective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B), Function.Surjective ⇑f.rangeRestrict
-- Mathlib.NumberTheory.Real.Irrational
irrational_div_ratCast_iff : ∀ {q : ℚ} {x : ℝ}, Irrational (x / ↑q) ↔ q ≠ 0 ∧ Irrational x
-- Mathlib.Topology.Order
discreteTopology_bot : ∀ (α : Type u_2), DiscreteTopology α
-- Mathlib.Order.Category.BoolAlg
/-- Turn a `BoolAlg` into a `BddDistLat` by forgetting its complement operation.  -/
BoolAlg.toBddDistLat : BoolAlg → BddDistLat
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.zero_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : Zero 𝕜] [inst_1 : LE α] (a b : α), 0 a b = 0
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The automorphism of a root pairing given by a reflection.  -/
RootPairing.Equiv.reflection : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → ι → P.Aut
-- Mathlib.Analysis.Complex.Basic
RCLike.re_to_complex : ∀ {x : ℂ}, RCLike.re x = x.re
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Non-primitive corecursor for `Multiseries basis_hd basis_tl` allowing to use a friendly
operation in the tail of the corecursive definition.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.gcorec : {β : Type u_1} →
  {γ : Type u_2} →
    {basis_hd : ℝ → ℝ} →
      {basis_tl : Tactic.ComputeAsymptotics.Basis} →
        (β → Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl × γ × β)) →
          (op :
              γ →
                Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
                  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) →
            [Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op] →
              β → Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.isoMk_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  {Q : CategoryTheory.MorphismProperty C} [inst_2 : Q.IsMultiplicative] {F : CategoryTheory.Functor C D} {X : D}
  {A B : P.CostructuredArrow Q F X} (f : A.left ≅ B.left) (hf : Q f.hom) (hf' : Q f.inv)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f.hom) B.hom = A.hom)
      CategoryTheory.MorphismProperty.CostructuredArrow.isoMk._auto_1),
  (CategoryTheory.MorphismProperty.CostructuredArrow.isoMk f hf hf' w).hom =
    CategoryTheory.MorphismProperty.CostructuredArrow.homMk f.hom hf ⋯
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.mk.inj : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} {idxFun : ι → α ⊕ η} {proper : ∀ (e : η), ∃ i, idxFun i = Sum.inr e}
  {idxFun_1 : ι → α ⊕ η} {proper_1 : ∀ (e : η), ∃ i, idxFun_1 i = Sum.inr e},
  { idxFun := idxFun, proper := proper } = { idxFun := idxFun_1, proper := proper_1 } → idxFun = idxFun_1
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.associator : {B : Type u} →
  [inst : Quiver B] →
    {a b c d : CategoryTheory.FreeBicategory B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            CategoryTheory.FreeBicategory.Hom₂
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)
              (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      (Std.Internal.List.getKey? k l).pfilter fun x h => (f x (Std.Internal.List.getValueCast x l ⋯)).isSome
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanImportMetaKind : Lean.ToJson Lean.Lsp.LeanImportMetaKind
-- Mathlib.Data.Set.Insert
Set.ssubset_insert : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → s ⊂ insert a s
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.mem_iff_toAddUnits_mem_addUnits : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G) (x : G), toAddUnits x ∈ H.addUnits ↔ x ∈ H
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.ListSlice.toList_eq.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (h_1 : (stop : ℕ) → motive (some stop)) (h_2 : Unit → motive none),
  (match none with
    | some stop => h_1 stop
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Data.TypeVec
/-- predicate on a type vector to constrain only the last object  -/
TypeVec.PredLast' : {n : ℕ} → (α : TypeVec.{u_1} n) → {β : Type u_1} → (β → Prop) → (α ::: β).Arrow (TypeVec.repeat (n + 1) Prop)
-- Init.Data.Iterators.Combinators.Monadic.ULift
_private.Init.Data.Iterators.Combinators.Monadic.ULift.0.Std.Iterators.Types.ULiftIterator.instProductivenessRelation : {α : Type u} →
  {m : Type u → Type u'} →
    {n : Type (max u v) → Type v'} →
      {β : Type u} →
        {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} →
          [inst : Std.Iterator α m β] →
            [Std.Iterators.Productive α m] →
              [inst_2 : Monad n] →
                Std.Iterators.ProductivenessRelation (Std.Iterators.Types.ULiftIterator α m n β lift) n
-- Lean.Meta.Tactic.Grind.Arith.Util
Lean.Meta.Grind.Arith.CollectDecVars.State.visited : Lean.Meta.Grind.Arith.CollectDecVars.State → Std.HashSet UInt64
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` creates finite limits, then `F.unop : C ⥤ D` creates finite
colimits.  -/
CategoryTheory.Limits.createsFiniteColimitsUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteLimits F] → CategoryTheory.Limits.CreatesFiniteColimits F.unop
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.instInhabited : {M : Type u_1} →
  [inst : CommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → Inhabited (MulArchimedeanClass M)
-- Mathlib.Algebra.Group.Nat.Hom
multiplesAddHom_symm_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] (f : ℕ →+ M), (multiplesAddHom M).symm f = f 1
-- Mathlib.CategoryTheory.Yoneda
/-- Variant of `yonedaEquiv_naturality` with general `g`. This is technically strictly more general
than `yonedaEquiv_naturality`, but `yonedaEquiv_naturality` is sometimes preferable because it
can avoid the "motive is not type correct" error.  -/
CategoryTheory.yonedaEquiv_naturality' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (f : CategoryTheory.yoneda.obj (Opposite.unop X) ⟶ F) (g : X ⟶ Y),
  (CategoryTheory.ConcreteCategory.hom (F.map g)) (CategoryTheory.yonedaEquiv f) =
    CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g.unop) f)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.apply_mem_map_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {L : BooleanSubalgebra α}
  {f : BoundedLatticeHom α β} {a : α}, Function.Injective ⇑f → (f a ∈ BooleanSubalgebra.map f L ↔ a ∈ L)
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.projVandermonde_apply_of_ne_zero : ∀ {K : Type u_2} [inst : Field K] {n : ℕ} {v w : Fin (n + 1) → K} {i j : Fin (n + 1)},
  w i ≠ 0 → Matrix.projVandermonde v w i j = v i ^ ↑j * w i ^ n / w i ^ ↑j
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.ext : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] {e e' : P ≃ᵃⁱ[𝕜] P₂},
  (∀ (x : P), e x = e' x) → e = e'
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.acyclic_truncGE_iff : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_3, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : CochainComplex C ℤ)
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n₀ n₁ : ℤ),
  autoParam (n₀ + 1 = n₁) CochainComplex.acyclic_truncGE_iff._auto_1 →
    (HomologicalComplex.Acyclic (K.truncGE n₁) ↔ K.IsLE n₀)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union! m₂).getD k fallback = m₂.getD k fallback
-- Mathlib.Order.WithBot
WithBot.forall_le_coe_iff_le : ∀ {α : Type u_1} [inst : Preorder α] {x y : WithBot α} [NoBotOrder α], (∀ (a : α), y ≤ ↑a → x ≤ ↑a) ↔ x ≤ y
-- Init.Data.Nat.Div.Basic
Nat.div_zero : ∀ (n : ℕ), n / 0 = 0
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHomComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          [Mathlib.Tactic.BicategoryCoherence.LiftHom f] →
            [Mathlib.Tactic.BicategoryCoherence.LiftHom g] →
              Mathlib.Tactic.BicategoryCoherence.LiftHom (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffOn_const : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {c : F}
  {s : Set E}, ContDiffOn 𝕜 n (fun x => c) s
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioo_ofDual : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : αᵒᵈ),
  Finset.Ioo (OrderDual.ofDual a) (OrderDual.ofDual b) = Finset.map OrderDual.ofDual.toEmbedding (Finset.Ioo b a)
-- Mathlib.Order.Hom.Basic
/-- `Prod.fst` as an `OrderHom`.  -/
OrderHom.fst : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α × β →o α
-- Mathlib.CategoryTheory.Pi.Monoidal
/-- When each `C i` is a symmetric monoidal category,
the natural pointwise monoidal structure on `∀ i, C i`
is also symmetric.
 -/
CategoryTheory.Pi.symmetricCategory : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] →
        [(i : I) → CategoryTheory.SymmetricCategory (C i)] → CategoryTheory.SymmetricCategory ((i : I) → C i)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.image_symm_image : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) (S : Set B), ⇑e '' ⇑e.symm '' S = S
-- Mathlib.CategoryTheory.Category.KleisliCat
CategoryTheory.KleisliCat.id_def : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (α : CategoryTheory.KleisliCat m),
  CategoryTheory.CategoryStruct.id α = pure
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.ofIsTerminal_fst : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₃ Y₃ : C₃}
  (f₃ : X₃ ⟶ Y₃)
  [inst_3 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op X₁))]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (G.obj (Opposite.op Y₁))]
  (h : CategoryTheory.Limits.IsTerminal Y₃),
  (CategoryTheory.Functor.PullbackObjObj.ofIsTerminal G f₁ f₃ h).fst =
    CategoryTheory.CategoryStruct.id ((G.obj (Opposite.op X₁)).obj X₃)
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries.0.Pentagonal.tendsto_order_pow_mul_prod_one_sub_pow : ∀ (R : Type u_1) [inst : CommRing R] (k : ℕ),
  Filter.Tendsto
    (fun n => (PowerSeries.X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - PowerSeries.X ^ (k + i + 1))).order)
    Filter.atTop (nhds ⊤)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.lt_log_of_lt_opow : ∀ {b x c : Ordinal.{u_1}}, c ≠ 0 → x < b ^ c → Ordinal.log b x < c
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_compl_self : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f {x}ᶜ x ↔ ContDiffAt 𝕜 n f x
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.metadataBlock.opener : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- More general form of `Subalgebra.algebra`.

This instance should have low priority since it is slow to fail:
before failing, it will cause a search through all `SMul R' R` instances,
which can quickly get expensive.
 -/
Subalgebra.algebra' : {R' : Type u'} →
  {R : Type u} →
    {A : Type v} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            (S : Subalgebra R A) →
              [inst_3 : CommSemiring R'] →
                [inst_4 : SMul R' R] → [inst_5 : Algebra R' A] → [IsScalarTower R' R A] → Algebra R' ↥S
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisorAt.mod'.congr_simp : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {I I_1 : Ideal A} (e_I : I = I_1)
  (H : g.IsWeierstrassDivisorAt I) [inst_1 : IsAdicComplete I A], H.mod' = ⋯.mod'
-- Init.Data.BitVec.Lemmas
BitVec.neg_eq_iff_eq_neg : ∀ {w : ℕ} {x y : BitVec w}, -x = y ↔ x = -y
-- Mathlib.Algebra.Algebra.Pi
AlgHom.pi_evalAlgHom : ∀ {ι : Type u_1} (R : Type u_2) (A : ι → Type u_3) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)], AlgHom.pi (Pi.evalAlgHom R A) = AlgHom.id R ((i : ι) → A i)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.mk.sizeOf_spec : ∀ (lhs rhs : Lean.Grind.AC.Seq) (h : Lean.Meta.Grind.AC.EqCnstrProof) (id : ℕ),
  sizeOf { lhs := lhs, rhs := rhs, h := h, id := id } = 1 + sizeOf lhs + sizeOf rhs + sizeOf h + sizeOf id
-- Mathlib.Order.Filter.Extr
/-- If `f` has a minimum and a maximum both given by `f a` along the filter `l`, then it is
eventually equal to `f a` along the filter.  -/
eventuallyEq_of_isMinFilter_of_isMaxFilter : ∀ {α : Type u} {l : Filter α} {a : α} {β : Type u_1} [inst : PartialOrder β] {f : α → β},
  IsMinFilter f l a → IsMaxFilter f l a → f =ᶠ[l] fun x => f a