mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
aemeasurable_restrict_of_antitoneOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  [inst_2 : TopologicalSpace β] {mβ : MeasurableSpace β} [BorelSpace β] [inst_4 : LinearOrder α] [OrderTopology α]
  [SecondCountableTopology α] [inst : LinearOrder β] [OrderClosedTopology β] {μ : MeasureTheory.Measure β} {s : Set β},
  MeasurableSet s → ∀ {f : β → α}, AntitoneOn f s → AEMeasurable f (μ.restrict s)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_inv_eq_germ_apply : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V) (y : ↑(X.presheaf.obj (Opposite.op (h.functor.obj V)))),
  (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).inv)
      ((CategoryTheory.ConcreteCategory.hom
          (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯))
        y) =
    (CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) y
-- Mathlib.Algebra.Group.AddChar
AddChar.ne_zero_iff : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] {ψ : AddChar A M}, ψ ≠ 0 ↔ ∃ x, ψ x ≠ 1
-- Mathlib.Order.Hom.Basic
/-- Order isomorphism between the space of monotone maps to `β × γ` and the product of the spaces
of monotone maps to `β` and `γ`.  -/
OrderHom.prodIso : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Preorder γ] → (α →o β × γ) ≃o (α →o β) × (α →o γ)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.descCochain.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cochain K M m),
  α = α_1 →
    ∀ (β β_1 : CochainComplex.HomComplex.Cochain L M n),
      β = β_1 →
        ∀ (h : m + 1 = n) (T : CochainComplex.HomComplex.Triplet m),
          CochainComplex.mappingCocone.descCochain φ α β h T = CochainComplex.mappingCocone.descCochain φ α_1 β_1 h T
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_natTrailingDegree : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → u ≠ 0 → (Polynomial.trinomial k m n u v w).natTrailingDegree = k
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.id_homEquiv_symm_apply : ∀ (X : Type v) (x : X) (a : PUnit.{v + 1}),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.CorepresentableBy.id.homEquiv.symm x)) a = x
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
Real.posLog.eq_1 : ∀ (r : ℝ), r.posLog = max 0 (Real.log r)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract.congr_simp : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b b_1 : Module.Basis ι K E),
  b = b_1 →
    ∀ [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K] [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m m_1 : E),
      m = m_1 → ZSpan.fract b m = ZSpan.fract b_1 m_1
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.eventually_finsupport_subset : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (ρ : SmoothPartitionOfUnity ι I M s) (x₀ : M),
  ∀ᶠ (y : M) in nhds x₀, ρ.finsupport y ⊆ ρ.fintsupport x₀
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ChangeAnnotationSupport.mk : Option Bool → Lean.Lsp.ChangeAnnotationSupport
-- Mathlib.Order.Interval.Set.Fin
Fin.range_castAdd : ∀ {m n : ℕ} [inst : NeZero m], Set.range (Fin.castAdd m) = Set.Iio (Fin.natAdd n 0)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.isEmpty = false → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α} {h : a ∈ t}, Std.ExtDTreeMap.Const.get t a h = Std.ExtDTreeMap.Const.get! t a
-- Mathlib.Data.Rel
SetRel.instIsIrreflOfPredProdMatch_1PropOfIrrefl : ∀ {α : Type u_1} {R : α → α → Prop} [Std.Irrefl R], SetRel.IsIrrefl {(a, b) | R a b}
-- Mathlib.Combinatorics.Enumerative.Composition
CompositionAsSet.mk.congr_simp : ∀ {n : ℕ} (boundaries boundaries_1 : Finset (Fin n.succ)) (e_boundaries : boundaries = boundaries_1)
  (zero_mem : 0 ∈ boundaries) (getLast_mem : Fin.last n ∈ boundaries),
  { boundaries := boundaries, zero_mem := zero_mem, getLast_mem := getLast_mem } =
    { boundaries := boundaries_1, zero_mem := ⋯, getLast_mem := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_sub_one : ∀ {x : NNReal}, x ≠ 0 → ∀ (y : ℝ), x ^ (y - 1) = x ^ y / x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instCoeTC : {F : Type u_1} →
  {α : Type u} →
    {β : Type v} →
      [inst : TopologicalSpace α] →
        [inst_1 : TopologicalSpace β] →
          [inst_2 : Zero β] →
            [inst_3 : FunLike F α β] → [ZeroAtInftyContinuousMapClass F α β] → CoeTC F (ZeroAtInftyContinuousMap α β)
-- Mathlib.Order.SupClosed
isSublattice_singleton : ∀ {α : Type u_3} [inst : Lattice α] {a : α}, IsSublattice {a}
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.isSheaf_coherent_of_projective_of_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A) {B : Type u₄}
  [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.Preregular C]
  [inst_4 : CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X]
  [CategoryTheory.Limits.ReflectsFiniteProducts s],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s) →
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.apply_eq_true_of_skipSuffixWhile_le_bool : ∀ {p : Char → Bool} {s : String} {pos : s.Pos},
  s.skipSuffixWhile p ≤ pos → ∀ (h' : pos < s.endPos), p (pos.get ⋯) = true
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
differentiableWithinAtProp_self_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_5 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {f : E → H'} {s : Set E} {x : E},
  DifferentiableWithinAtProp (modelWithCornersSelf 𝕜 E) I' f s x ↔ DifferentiableWithinAt 𝕜 (↑I' ∘ f) s x
-- Lean.Compiler.ExportAttr
Lean.isExport : Lean.Environment → Lean.Name → Bool
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- The indexed supremum of a function is bounded below by the value taken at one point  -/
le_ciSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {f : ι → α},
  BddAbove (Set.range f) → ∀ (c : ι), f c ≤ iSup f
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- If the submodule generated by a set `s` is dense in the ambient module, then two continuous
linear maps equal on `s` are equal.  -/
ContinuousLinearMap.ext_on : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [T2Space M₂] {s : Set M₁},
  Dense ↑(Submodule.span R₁ s) → ∀ {f g : M₁ →SL[σ₁₂] M₂}, Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.mul_homogeneous_element_mem_of_mem : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜]
  {I : Ideal A} (r x : A), SetLike.IsHomogeneousElem 𝒜 x → x ∈ I → ∀ (j : ι), (GradedRing.proj 𝒜 j) (r * x) ∈ I
-- Mathlib.Algebra.Group.Equiv.TypeTags
/-- Reinterpret `G ≃* H` as `Additive G ≃+ Additive H`.  -/
MulEquiv.toAdditive : {G : Type u_2} →
  {H : Type u_3} → [inst : MulOneClass G] → [inst_1 : MulOneClass H] → G ≃* H ≃ (Additive G ≃+ Additive H)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex✝ f n).X₁ =
    HomologicalComplex.homology K n
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportKind.isAll : Lean.Lsp.LeanImportKind → Bool
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureInt_vars : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] [inst : Fintype idx] (Φ : MvPolynomial idx ℤ) (n : ℕ),
  (wittStructureInt p Φ n).vars ⊆ Finset.univ ×ˢ Finset.range (n + 1)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanMap.match_1.splitter : {C₀ : Type u_4} →
  {C : Type u_5} →
    [inst : CategoryTheory.Category.{u_2, u_4} C₀] →
      [inst_1 : CategoryTheory.Category.{u_3, u_5} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {X : C} →
            (data : F.PreOneHypercoverDenseData X) →
              (motive : CategoryTheory.Limits.WalkingMulticospan data.multicospanShape → Sort u_6) →
                (x : CategoryTheory.Limits.WalkingMulticospan data.multicospanShape) →
                  ((i : data.multicospanShape.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i)) →
                    ((j : data.multicospanShape.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right j)) →
                      motive x
-- Mathlib.Topology.Convenient.GeneratedBy
/-- Any topology coinduced by an `X`-generated topology is `X`-generated.  -/
Topology.IsGeneratedBy.coinduced : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  {Z : Type v'} [Topology.IsGeneratedBy X Y] (f : Y → Z), Topology.IsGeneratedBy X Z
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
MvPolynomial.irreducible_sumSMulX : ∀ {n : Type u_1} {R : Type u_2} [inst : CommRing R] (c : n →₀ R) [IsDomain R],
  c.support.Nonempty → (∀ (r : R), (∀ (i : n), r ∣ c i) → IsUnit r) → Irreducible (MvPolynomial.sumSMulX c)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.arg.mkNamedNoParen : ℕ → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Mathlib.Combinatorics.Additive.RuzsaCovering
/-- **Ruzsa's covering lemma** for sets. See also `Finset.ruzsa_covering_mul`.  -/
Set.ruzsa_covering_mul : ∀ {G : Type u_1} [inst : Group G] {K : ℝ} {A B : Set G},
  A.Finite →
    B.Finite →
      B.Nonempty → ↑(Nat.card ↑(A * B)) ≤ K * ↑(Nat.card ↑B) → ∃ F ⊆ A, ↑(Nat.card ↑F) ≤ K ∧ A ⊆ F * (B / B) ∧ F.Finite
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.fg_iff_structure_fg : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.Substructure M),
  S.FG ↔ FirstOrder.Language.Structure.FG L ↥S
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.one_mul : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] (x : OreLocalization S R),
  1 * x = x
-- Mathlib.Algebra.Group.PUnit
PUnit.commGroup : CommGroup PUnit.{u_1 + 1}
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.toTrivialization_apply : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : E} [inst_3 : Nonempty I] (h : IsEvenlyCovered f (f x) I),
  (↑h.toTrivialization x).2 = ⟨x, ⋯⟩
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.length.eq_2 : ∀ {V : Type u} [inst : Quiver V] {a : V} (x b : V) (p : Quiver.Path a b) (a_1 : b ⟶ x),
  (p.cons a_1).length = p.length + 1
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0)
  (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  (CategoryTheory.ShortComplex.Homotopy.ofNullHomotopic S₁ S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).h₁ = h₁