mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.range_dualMap_eq_dualAnnihilator_ker_of_surjective : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  Function.Surjective ⇑f → f.dualMap.range = f.ker.dualAnnihilator
-- Mathlib.Data.Setoid.Partition
Setoid.IsPartition.finpartition_parts : ∀ {α : Type u_1} {c : Finset (Set α)} (hc : Setoid.IsPartition ↑c), hc.finpartition.parts = c
-- Std.Data.HashSet.Basic
/-- Carries out a monadic action on each element in the hash set in some order.  -/
Std.HashSet.forM : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} → {m : Type v → Type w} → [Monad m] → (α → m PUnit.{v + 1}) → Std.HashSet α → m PUnit.{v + 1}
-- Mathlib.Topology.Algebra.InfiniteSum.Real
not_summable_iff_tendsto_nat_atTop_of_nonneg : ∀ {f : ℕ → ℝ},
  (∀ (n : ℕ), 0 ≤ f n) → (¬Summable f ↔ Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop Filter.atTop)
-- Mathlib.Algebra.Group.Defs
nsmulRec.eq_def : ∀ {M : Type u_1} [inst : Zero M] [inst_1 : Add M] (x : ℕ) (x_1 : M),
  nsmulRec x x_1 =
    match x, x_1 with
    | 0, x => 0
    | n.succ, a => nsmulRec n a + a
-- Std.Internal.Do.WP.Lemmas
ExceptT.adapt.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} [inst : Monad m] {ε' α : Type u} (f : ε → ε') (x : ExceptT ε m α),
  ExceptT.adapt f x = ExceptT.mk (Except.mapError f <$> x)
-- Mathlib.Algebra.Category.ModuleCat.Ext.DimensionShifting
/-- The connection maps in the covariant long exact sequence of `Ext` are surjective if
the middle term of the short exact sequence is injective.  -/
postcomp_extClass_surjective_of_projective_X₂ : ∀ {R : Type u} [inst : Ring R] [inst_1 : Small.{v, u} R] {S : CategoryTheory.ShortComplex (ModuleCat R)}
  (h : S.ShortExact) (M : ModuleCat R) (n : ℕ) [CategoryTheory.Injective S.X₂],
  Function.Surjective ⇑(h.extClass.postcomp M ⋯)
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.mem_disjointed_spanningSetsIndex : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ] (x : α),
  x ∈ disjointed (MeasureTheory.spanningSets μ) (MeasureTheory.spanningSetsIndex μ x)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of a finite subset of an affinely independent
family has dimension one less than its cardinality.  -/
AffineIndependent.finrank_vectorSpan_image_finset : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : DecidableEq P] {p : ι → P},
  AffineIndependent k p →
    ∀ {s : Finset ι} {n : ℕ}, s.card = n + 1 → Module.finrank k ↥(vectorSpan k ↑(Finset.image p s)) = n
-- Mathlib.Topology.Category.TopCat.GrothendieckTopology
TopCat.instRespectsIsoIsOpenEmbedding : TopCat.isOpenEmbedding.RespectsIso
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.instIsMonHomInvOfIsCommMonObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {G : C}
  [inst_2 : CategoryTheory.GrpObj G] [inst_3 : CategoryTheory.BraidedCategory C] [CategoryTheory.IsCommMonObj G],
  CategoryTheory.IsMonHom CategoryTheory.GrpObj.inv
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.coeff_C_succ : ∀ {R : Type u_1} [inst : Semiring R] {r : R} {n : ℕ}, (SkewPolynomial.C r).coeff (n + 1) = 0
-- Mathlib.Data.Finsupp.ToDFinsupp
/-- `Finsupp.toDFinsupp` and `DFinsupp.toFinsupp` together form an equiv.  -/
finsuppEquivDFinsupp : {ι : Type u_1} →
  {M : Type u_3} → [DecidableEq ι] → [inst : Zero M] → [(m : M) → Decidable (m ≠ 0)] → (ι →₀ M) ≃ Π₀ (x : ι), M
-- Mathlib.Data.Nat.Factors
Nat.prime_of_mem_primeFactorsList : ∀ {n p : ℕ}, p ∈ n.primeFactorsList → Nat.Prime p
-- Mathlib.Data.Quot
Quotient.liftOn'_mk : ∀ {α : Sort u_1} {β : Sort u_2} {s : Setoid α} (x : α) (f : α → β) (h : ∀ (a b : α), s a b → f a = f b),
  ⟦x⟧.liftOn' f h = f x
-- Mathlib.RingTheory.DedekindDomain.Instances
_private.Mathlib.RingTheory.DedekindDomain.Instances.0.termF : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.entryAtIdx : {α : Type u} →
  {β : α → Type v} → (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → (n : ℕ) → n < t.size → (a : α) × β a
-- Mathlib.Analysis.Analytic.Constructions
/-- A function is analytic at a point iff it is analytic after multiplication
with a non-vanishing analytic function.  -/
analyticAt_iff_analytic_mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f g : E → 𝕝}
  {z : E}, AnalyticAt 𝕜 f z → f z ≠ 0 → (AnalyticAt 𝕜 g z ↔ AnalyticAt 𝕜 (f * g) z)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_X_same : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (i : σ), MvPolynomial.coeff (fun₀ | i => 1) (MvPolynomial.X i) = 1
-- Mathlib.Topology.Separation.Basic
t1Space_TFAE : ∀ (X : Type u) [inst : TopologicalSpace X],
  [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of,
      ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ nhds x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ nhds x, y ∉ s,
      ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (nhds x) (pure y),
      ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (nhds y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
-- Mathlib.Algebra.Star.Module
algebraMap_star_comm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarMul A]
  [inst_4 : Algebra R A] [StarModule R A] (r : R), (algebraMap R A) (star r) = star ((algebraMap R A) r)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.addEquivBoundedOfCompact.congr_simp : ∀ (α : Type u_1) (β : Type u_2) [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  [inst_3 : AddMonoid β] [inst_4 : LipschitzAdd β],
  ContinuousMap.addEquivBoundedOfCompact α β = ContinuousMap.addEquivBoundedOfCompact α β
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm.eq_1 : ∀ {α : Type u_1} {E : Type u_4} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] (f : α → E) (p : ENNReal)
  (μ : MeasureTheory.Measure α),
  MeasureTheory.lpNorm f p μ =
    if MeasureTheory.AEStronglyMeasurable f μ then (MeasureTheory.eLpNorm f p μ).toReal else 0
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.instIsZariskiLocalAtTargetTopologicallyGeneralizingMap : AlgebraicGeometry.IsZariskiLocalAtTarget
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => GeneralizingMap)
-- Batteries.Recycling.RBTree.WF
/-- The property of a map function `f` which ensures the `map` operation is valid.  -/
RBTree.RBNode.IsMonotone : {α : Type u_1} → {β : Type u_2} → (α → α → Ordering) → (β → β → Ordering) → (α → β) → Prop
-- Lean.Meta.Basic
Lean.Meta.isExprDefEqGuarded : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Init.Data.Vector.Int
Vector.prod_append_int : ∀ {n m : ℕ} {as₁ : Vector ℤ n} {as₂ : Vector ℤ m}, (as₁ ++ as₂).prod = as₁.prod * as₂.prod
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.isoMk_hom_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreOneHypercover S}
  (s₀ : E.I₀ ≃ F.I₀) (h₀ : (i : E.I₀) → E.X i ≅ F.X (s₀ i)) (s₁ : ⦃i j : E.I₀⦄ → E.I₁ i j ≃ F.I₁ (s₀ i) (s₀ j))
  (h₁ : ⦃i j : E.I₀⦄ → (k : E.I₁ i j) → E.Y k ≅ F.Y (s₁ k))
  (w₀ :
    autoParam (∀ (i : E.I₀), CategoryTheory.CategoryStruct.comp (h₀ i).hom (F.f (s₀ i)) = E.f i)
      CategoryTheory.PreOneHypercover.isoMk._auto_1)
  (w₁₁ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (h₀ i).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_3)
  (w₁₂ :
    autoParam
      (∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k).hom (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (h₀ j).hom)
      CategoryTheory.PreOneHypercover.isoMk._auto_5)
  (i : E.I₀), (CategoryTheory.PreOneHypercover.isoMk s₀ h₀ s₁ h₁ w₀ w₁₁ w₁₂).hom.h₀ i = (h₀ i).hom
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lsum_symm_apply : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R₂ N] {σ : R →+* R₂} [inst_7 : Module S N] [inst_8 : SMulCommClass R₂ S N]
  (f : (α →₀ M) →ₛₗ[σ] N) (x : α), (Finsupp.lsum S).symm f x = f ∘ₛₗ Finsupp.lsingle x
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instMonadLiftBaseIO : MonadLift BaseIO Std.Async.ContextAsync
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_mul' : ∀ {R : Type u_1} [inst : CommRing R] {f g : Polynomial R} [IsDomain R],
  (f * g).Splits ↔ (f.Splits ∨ g = 0) ∧ (g.Splits ∨ f = 0)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.nhds_top_basis : (nhds ⊤).HasBasis (fun a => a < ⊤) fun a => Set.Ioi a
-- Mathlib.Algebra.CharP.Pi
CharP.pi' : ∀ (ι : Type u) [Nonempty ι] (R : Type v) [inst : CommRing R] (p : ℕ) [CharP R p], CharP (ι → R) p
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
IsSymmetricAlgebra.comp_equiv : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (e : SymmetricAlgebra R M ≃ₐ[R] A),
  IsSymmetricAlgebra (e.toLinearMap ∘ₗ SymmetricAlgebra.ι R M)
-- Mathlib.NumberTheory.Divisors
Nat.one_mem_properDivisors_iff_one_lt : ∀ {n : ℕ}, 1 ∈ n.properDivisors ↔ 1 < n