mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_cert.match_1.congr_eq_3 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (p₁ p₂ : Int.Internal.Linear.Poly)
  (h_1 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k_1 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1))
  (h_2 :
    (k k_1 : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p))
  (h_3 : (c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
  (c₁ c₂ : ℤ),
  p₁ = Int.Internal.Linear.Poly.num c₁ →
    p₂ = Int.Internal.Linear.Poly.num c₂ →
      (match p₁, p₂ with
        | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_1 => h_1 k v p k_1
        | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_1 v p => h_2 k k_1 v p
        | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => h_3 c₁ c₂
        | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) ≍
        h_3 c₁ c₂
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
/-- If a precoverage satisfies `HasIsos`, `IsStableUnderBaseChange` and
`IsStableUnderComposition` (which is a slightly stronger condition as compared
to pretopologies), then in order to check that a pseudofunctor is a stack
it suffices to check that it is a stack for the presieves that are
part of the precoverage.  -/
CategoryTheory.Pseudofunctor.IsStack.of_precoverage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  [CategoryTheory.Limits.HasPullbacks C] {J : CategoryTheory.Precoverage C} [J.HasIsos] [J.IsStableUnderBaseChange]
  [J.IsStableUnderComposition], (∀ (S : C), ∀ R ∈ J.coverings S, F.IsStackFor R) → F.IsStack J.toGrothendieck
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- A finitely generated monoid with a single unit has finitely many irreducible elements.  -/
finite_irreducible : ∀ {M : Type u_1} [inst : CommMonoid M] [Subsingleton Mˣ] [Monoid.FG M], {p | Irreducible p}.Finite
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- **Alias** of the reverse direction of `AddSubgroup.normal_unop`. -/
AddSubgroup.Normal.unop : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup Gᵃᵒᵖ}, H.Normal → H.unop.Normal
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.δ_iso_of_coreflective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Coreflective R],
  CategoryTheory.IsIso (CategoryTheory.coreflectorAdjunction R).toComonad.δ
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a (Set.Ioi a)) (nhdsWithin a⁻¹ (Set.Iio a⁻¹))
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.mk_eq_of_ne_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B)
  [inst_2 : DecidablePred fun b => b = 0] (r s : A) (hr : f r ≠ 0) (hs : f s ≠ 0),
  MonoidWithZeroHom.ValueGroup₀.mk f r s = ↑(MonoidWithZeroHom.valueGroup.mk f r s hr hs)