mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
LaurentPolynomial.antipode_C : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (a : A),
  (HopfAlgebraStruct.antipode R) (LaurentPolynomial.C a) = LaurentPolynomial.C ((HopfAlgebraStruct.antipode R) a)
-- Lean.Data.Options
Lean.OptionDecl.mk.inj : ∀ {name : Lean.Name} {declName : autoParam Lean.Name Lean.OptionDecl.declName._autoParam} {defValue : Lean.DataValue}
  {descr : String} {deprecation? : Option Lean.OptionDeprecation} {name_1 : Lean.Name}
  {declName_1 : autoParam Lean.Name Lean.OptionDecl.declName._autoParam} {defValue_1 : Lean.DataValue}
  {descr_1 : String} {deprecation?_1 : Option Lean.OptionDeprecation},
  { name := name, declName := declName, defValue := defValue, descr := descr, deprecation? := deprecation? } =
      { name := name_1, declName := declName_1, defValue := defValue_1, descr := descr_1,
        deprecation? := deprecation?_1 } →
    name = name_1 ∧ declName = declName_1 ∧ defValue = defValue_1 ∧ descr = descr_1 ∧ deprecation? = deprecation?_1
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.ratio_pow : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (f : α →ᵈ α) (n : ℕ), Dilation.ratio (f ^ n) = Dilation.ratio f ^ n
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.le_minDegree_induce_of_support_subset : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj], G.support ⊆ s → G.minDegree ≤ (SimpleGraph.induce s G).minDegree
-- Mathlib.Analysis.Convex.Topology
/-- **Alias** of the reverse direction of `Real.convex_iff_isPreconnected`. -/
IsPreconnected.convex : ∀ {s : Set ℝ}, IsPreconnected s → Convex ℝ s
-- Mathlib.Topology.Algebra.Module.Basic
/-- A topological module over a ring has continuous negation.

This cannot be an instance, because it would cause search for `[Module ?R M]` with unknown `R`.  -/
ContinuousNeg.of_continuousConstSMul : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [ContinuousConstSMul R M], ContinuousNeg M
-- Mathlib.Algebra.Notation.Defs
Star.mk : {R : Type u} → (R → R) → Star R
-- Std.Data.HashMap.Basic
/-- Partition a hash map into two hash map based on a predicate.  -/
Std.HashMap.partition : {α : Type u} →
  {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → (α → β → Bool) → Std.HashMap α β → Std.HashMap α β × Std.HashMap α β
-- Mathlib.CategoryTheory.Generator.Presheaf
CategoryTheory.Presheaf.freeYoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (X : C) (M : A) (Y : Cᵒᵖ),
  (CategoryTheory.Presheaf.freeYoneda X M).obj Y = ∐ fun i => M
-- Lean.Parser.Term
Lean.Parser.Term.letPosOpt.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.compSubConstCLM_comp : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  (f : SchwartzMap E F) (a b : E),
  (SchwartzMap.compSubConstCLM 𝕜 b) ((SchwartzMap.compSubConstCLM 𝕜 a) f) = (SchwartzMap.compSubConstCLM 𝕜 (a + b)) f
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.toEnd_def : ∀ (M : Type u) [inst : Monoid M] (x : M), (CategoryTheory.SingleObj.toEnd M) x = x
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- The family of functions forming the partition of unity.  -/
SmoothPartitionOfUnity.toFun : {ι : 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 : optParam (Set M) Set.univ} →
                      SmoothPartitionOfUnity ι I M s → ι → ContMDiffMap I (modelWithCornersSelf ℝ ℝ) M ℝ ↑⊤
-- Mathlib.Probability.HasLaw
ProbabilityTheory.HasLaw.measurePreserving : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {X : Ω → 𝓧}
  {μ : MeasureTheory.Measure 𝓧} {P : MeasureTheory.Measure Ω},
  ProbabilityTheory.HasLaw X μ P → Measurable X → MeasureTheory.MeasurePreserving X P μ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (t.insertMany l).getKeyD k' fallback = k
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- Right-exactness of tensor product  -/
lTensor_mkQ : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Q : Type u_5)
  [inst_3 : AddCommGroup Q] [inst_4 : Module R Q] (N : Submodule R M),
  (LinearMap.lTensor Q N.mkQ).ker = (LinearMap.lTensor Q N.subtype).range
-- Mathlib.Data.Finsupp.Fintype
Finsupp.infinite_of_left : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [Nontrivial α] [Infinite ι], Infinite (ι →₀ α)
-- Mathlib.AlgebraicGeometry.Gluing
/-- The open cover of the colimit of a locally directed diagram by the components.  -/
AlgebraicGeometry.Scheme.IsLocallyDirected.openCover : {J : Type w} →
  [inst : CategoryTheory.Category.{v, w} J] →
    (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) →
      [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] →
        [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] →
          [inst_3 : Quiver.IsThin J] → [inst_4 : Small.{u, w} J] → (CategoryTheory.Limits.colimit F).OpenCover
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.isOpen : ∀ {α : Type u} [t : TopologicalSpace α] {s : Set α} {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → s ∈ b → IsOpen s
-- Mathlib.Tactic.Simproc.Factors
Mathlib.Meta.Simproc.FactorsHelper.singleton_self : ∀ (a : ℕ), Mathlib.Meta.Simproc.FactorsHelper a a [a]
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.degree_le' : ∀ {V : Type u} {G : SimpleGraph V} (G' G'' : G.Subgraph),
  G' ≤ G'' →
    ∀ (v : V) [inst : Fintype ↑(G'.neighborSet v)] [inst_1 : Fintype ↑(G''.neighborSet v)], G'.degree v ≤ G''.degree v
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.addGrpObj_add : ∀ {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.Monoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.AddGrpObj (F.obj X)],
  CategoryTheory.AddMonObj.add =
    hF.preimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.AddMonObj.add)
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.stdSimplex.le_boundary_iff : ∀ {n : ℕ} (A : (SSet.stdSimplex.obj { len := n }).Subcomplex), A ≤ SSet.boundary n ↔ A ≠ ⊤
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.prependNode.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Node α β → Sort u_3) (keys : Array α) (vals : Array β)
  (hsz : keys.size = vals.size)
  (h_1 :
    (es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      motive (Lean.PersistentHashMap.Node.entries es))
  (h_2 :
    (keys : Array α) →
      (vals : Array β) → (hsz : keys.size = vals.size) → motive (Lean.PersistentHashMap.Node.collision keys vals hsz)),
  (match Lean.PersistentHashMap.Node.collision keys vals hsz with
    | Lean.PersistentHashMap.Node.entries es => h_1 es
    | Lean.PersistentHashMap.Node.collision keys vals hsz => h_2 keys vals hsz) =
    h_2 keys vals hsz
-- Mathlib.Data.Nat.Factors
Nat.primeFactorsList.eq_1 : Nat.primeFactorsList 0 = []
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOfEquivOfLe.eq_1 : ∀ {G : Type u_7} [inst : Group G] {H K : Subgroup G} (h : H ≤ K),
  Subgroup.subgroupOfEquivOfLe h =
    { toFun := fun g => ⟨↑↑g, ⋯⟩, invFun := fun g => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Ring.Defs
/-- Multiplication is left distributive over addition  -/
Distrib.left_distrib : ∀ {R : Type u_1} [self : Distrib R] (a b c : R), a * (b + c) = a * b + a * c
-- Mathlib.GroupTheory.NoncommCoprod
MulHom.noncommCoprod_apply : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Semigroup P] (f : M →ₙ* P)
  (g : N →ₙ* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (mn : M × N),
  (f.noncommCoprod g comm) mn = f mn.1 * g mn.2
-- Mathlib.Order.Lattice.Nat
Nat.iSup_lt_succ : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
  ⨆ k, ⨆ (_ : k < n + 1), u k = (⨆ k, ⨆ (_ : k < n), u k) ⊔ u n
-- Init.Data.Nat.Fold
Nat.any_eq_anyTR : Nat.any = Nat.anyTR
-- Lean.Elab.Tactic.Omega.OmegaM
/-- An intermediate layer in the `OmegaM` monad.  -/
Lean.Elab.Tactic.Omega.OmegaM' : Type → Type
-- Init.Data.Range.Polymorphic.Basic
Std.Rxo.size_eq_zero_iff_not_le : ∀ {α : Type u} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxo.HasSize α]
  [Std.Rxo.LawfulHasSize α] {lo hi : α}, Std.Rxo.HasSize.size lo hi = 0 ↔ ¬lo < hi
-- Init.Data.Array.BinSearch
_private.Init.Data.Array.BinSearch.0.Array.binInsertAux.match_1.splitter : {α : Type u_1} →
  (lt : α → α → Bool) →
    (as : Array α) →
      (k : α) →
        (motive : (x x_1 : Fin as.size) → ↑x ≤ ↑x_1 → lt as[x] k = true → Sort u_2) →
          (x x_1 : Fin as.size) →
            (x_2 : ↑x ≤ ↑x_1) →
              (x_3 : lt as[x] k = true) →
                ((lo hi : Fin as.size) → (h : ↑lo ≤ ↑hi) → (w : lt as[lo] k = true) → motive lo hi h w) →
                  motive x x_1 x_2 x_3
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.D₂.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (j j' : ι₄)
  [inst_23 : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄],
  HomologicalComplex.mapBifunctor₂₃.D₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ j j' =
    HomologicalComplex.mapBifunctor₂₃.mapBifunctor₂₃Desc c₁₂ fun i₁ i₂ i₃ x =>
      HomologicalComplex.mapBifunctor₂₃.d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- **Integration by parts**. Special case of `integral_mul_deriv_eq_deriv_mul_of_hasDeriv_right`
where the functions have a two-sided derivative in the interior of the interval.  -/
intervalIntegral.integral_mul_deriv_eq_deriv_mul_of_hasDerivAt : ∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  ContinuousOn u (Set.uIcc a b) →
    ContinuousOn v (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt u (u' x) x) →
        (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt v (v' x) x) →
          IntervalIntegrable u' MeasureTheory.volume a b →
            IntervalIntegrable v' MeasureTheory.volume a b →
              ∫ (x : ℝ) in a..b, u x * v' x = u b * v b - u a * v a - ∫ (x : ℝ) in a..b, u' x * v x
-- Mathlib.FieldTheory.Minpoly.Field
minpoly.eq_of_irreducible_of_monic : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B]
  {p : Polynomial A}, Irreducible p → (Polynomial.aeval x) p = 0 → p.Monic → p = minpoly A x
-- Init.Grind.Module.OfNatModule
Lean.Grind.IntModule.OfNatModule.of_eq : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] {a b : α} {a' b' : Lean.Grind.IntModule.OfNatModule.Q α},
  Lean.Grind.IntModule.OfNatModule.toQ a = a' → Lean.Grind.IntModule.OfNatModule.toQ b = b' → a = b → a' = b'
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.instIsScalarTowerSubtypeMem : ∀ {M' : Type u_1} {α : Type u_2} {β : Type u_3} {S' : Type u_4} [inst : SetLike S' M'] (s : S') [inst_1 : SMul α β]
  [inst_2 : SMul M' α] [inst_3 : SMul M' β] [IsScalarTower M' α β], IsScalarTower (↥s) α β