mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Reinterpret a formal `𝕜'`-multilinear series as a formal `𝕜`-multilinear series.  -/
FormalMultilinearSeries.restrictScalars : (𝕜 : Type u) →
  {𝕜' : Type u'} →
    {E : Type v} →
      {F : Type w} →
        [inst : Semiring 𝕜] →
          [inst_1 : AddCommMonoid E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : ContinuousAdd E] →
                  [inst_5 : ContinuousConstSMul 𝕜 E] →
                    [inst_6 : AddCommMonoid F] →
                      [inst_7 : Module 𝕜 F] →
                        [inst_8 : TopologicalSpace F] →
                          [inst_9 : ContinuousAdd F] →
                            [inst_10 : ContinuousConstSMul 𝕜 F] →
                              [inst_11 : Semiring 𝕜'] →
                                [inst_12 : SMul 𝕜 𝕜'] →
                                  [inst_13 : Module 𝕜' E] →
                                    [inst_14 : ContinuousConstSMul 𝕜' E] →
                                      [IsScalarTower 𝕜 𝕜' E] →
                                        [inst_16 : Module 𝕜' F] →
                                          [inst_17 : ContinuousConstSMul 𝕜' F] →
                                            [IsScalarTower 𝕜 𝕜' F] →
                                              FormalMultilinearSeries 𝕜' E F → FormalMultilinearSeries 𝕜 E F
-- Mathlib.Data.List.InsertIdx
List.take_insertIdx_eq_take_of_le : ∀ {α : Type u} (l : List α) (x : α) (i j : ℕ), i ≤ j → List.take i (l.insertIdx j x) = List.take i l
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
/-- The increment partition has energy greater than the original one by a known fixed amount.  -/
SzemerediRegularity.energy_increment : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {G : SimpleGraph α}
  [inst_2 : DecidableRel G.Adj] {ε : ℝ} [Nonempty α] (hP : P.IsEquipartition),
  7 ≤ P.parts.card →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
        ¬P.IsUniform G ε →
          0 ≤ ε → ε ≤ 1 → ↑(P.energy G) + ε ^ 5 / 4 ≤ ↑((SzemerediRegularity.increment hP G ε).energy G)
-- Mathlib.Topology.Order.UpperLowerSetTopology
/-- `ofLowerSet` is the identity function from the `WithLowerSet` of a type.  -/
Topology.WithLowerSet.ofLowerSet : {α : Type u_1} → Topology.WithLowerSet α ≃ α
-- Mathlib.Topology.Algebra.Monoid
continuous_finprod_cond : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : CommMonoid M] [ContinuousMul M] {f : ι → X → M} {p : ι → Prop},
  (∀ (i : ι), p i → Continuous (f i)) →
    (LocallyFinite fun i => Function.mulSupport (f i)) → Continuous fun x => ∏ᶠ (i : ι) (_ : p i), f i x
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateRow_mulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {ι : Type u_6} [inst : Fintype n] [inst_1 : NonUnitalNonAssocSemiring α]
  (M : Matrix m n α) (v : n → α), Matrix.replicateRow ι (M.mulVec v) = (M * Matrix.replicateCol ι v).transpose
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_zero_apply : ∀ (a : Ordinal.{u_1}), Ordinal.veblen 0 a = Ordinal.omega0 ^ a
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_succ_succ : ∀ {m n : ℤ}, ((m + 1)...n + 1).toArray = Array.map (fun x => x + 1) (m...n).toArray
-- Mathlib.RingTheory.MvPowerSeries.Inverse
/-- Auxiliary definition that unifies
the totalised inverse formal power series `(_)⁻¹` and
the inverse formal power series that depends on
an inverse of the constant coefficient `invOfUnit`.  -/
MvPowerSeries.inv.aux : {σ : Type u_1} → {R : Type u_2} → [Ring R] → R → MvPowerSeries σ R → MvPowerSeries σ R
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The action by a subsemiring is the action by the underlying semiring.  -/
Subsemiring.module : {R' : Type u_1} →
  {α : Type u_2} →
    [inst : Semiring R'] → [inst_1 : AddCommMonoid α] → [Module R' α] → (S : Subsemiring R') → Module (↥S) α
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.lt_of_le : ∀ {α : Type u_1} {a a' b b' : α} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  a ≤ b → a' + b < b' + a → a' < b'
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_right_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m : M}, Function.Injective (AddMonoidAlgebra.single m)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.instSmallComap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {F : CategoryTheory.Functor C D} (J : CategoryTheory.Precoverage D) [J.Small],
  (CategoryTheory.Precoverage.comap F J).Small
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) (n₀ n₁ : ℤ)
  (h : autoParam (n₀ + 1 = n₁) CochainComplex.g_shortComplexTruncLEX₃ToTruncGE._auto_1) {Z : CochainComplex C ℤ}
  (h_1 : K.truncGE n₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE n₀).g
      (CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLEX₃ToTruncGE n₀ n₁ h) h_1) =
    CategoryTheory.CategoryStruct.comp (K.πTruncGE n₁) h_1
-- Mathlib.Data.Seq.Basic
Stream'.Seq.map_comp : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : Stream'.Seq α),
  Stream'.Seq.map (g ∘ f) s = Stream'.Seq.map g (Stream'.Seq.map f s)
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.concreteCategory : CategoryTheory.ConcreteCategory TwoP fun X Y => X.toBipointed.HomSubtype Y.toBipointed
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.comp_toFunctor : ∀ {C D E : CategoryTheory.Cat} (F : C ⟶ D) (G : D ⟶ E),
  (CategoryTheory.CategoryStruct.comp F G).toFunctor = F.toFunctor.comp G.toFunctor
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_antitone : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G), Antitone S.lowerCentralSeries
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.linearMap_compatibleSMul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (N₁ : Type u_4) (N₂ : Type u_5) [inst_4 : AddCommMonoid N₁]
  [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₁] [inst_7 : Module R N₂] [inst_8 : Module S N₁]
  [inst_9 : Module S N₂] [IsScalarTower R S N₁] [IsScalarTower R S N₂], LinearMap.CompatibleSMul N₁ N₂ S R
-- Mathlib.Analysis.InnerProductSpace.OfNorm
_private.Mathlib.Analysis.InnerProductSpace.OfNorm.0.InnerProductSpaceable.rat_prop : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [InnerProductSpaceable E] (r : ℚ), InnerProductSpaceable.innerProp'✝ E ↑r
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instIsAlgClosureOfIsAlgebraic : ∀ (k : Type u) [inst : Field k] {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra k L] [Algebra.IsAlgebraic k L],
  IsAlgClosure k (AlgebraicClosure L)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.contains_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β},
  m.WF → (Std.DHashMap.Raw.Const.modify m k f).contains k' = m.contains k'
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- By definition, the uniformity of `α →ᵤ β` admits the family `{(f, g) | ∀ x, (f x, g x) ∈ V}`
for `V ∈ 𝓤 β` as a filter basis.  -/
UniformFun.hasBasis_uniformity : ∀ (α : Type u_1) (β : Type u_2) [inst : UniformSpace β],
  (uniformity (UniformFun α β)).HasBasis (fun x => x ∈ uniformity β) (UniformFun.gen α β)
-- Mathlib.CategoryTheory.Galois.Action
CategoryTheory.PreGaloisCategory.instFaithfulActionFintypeCatAutFunctorFunctorToAction : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (CategoryTheory.PreGaloisCategory.functorToAction F).Faithful
-- Mathlib.Control.LawfulFix
Pi.uncurry_curry_ωScottContinuous : ∀ {α : Type u_1} {β : α → Type u_2} {γ : (a : α) → β a → Type u_3}
  [inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)]
  {f : ((a : α) → (b : β a) → γ a b) → (a : α) → (b : β a) → γ a b} (hc : OmegaCompletePartialOrder.ωScottContinuous f),
  OmegaCompletePartialOrder.ωScottContinuous
    ⇑((Pi.monotoneUncurry α β γ).comp ({ toFun := f, monotone' := ⋯ }.comp (Pi.monotoneCurry α β γ)))
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.instAddCommMonoid : {σ : Type u_1} → {R : Type u_2} → [AddCommMonoid R] → AddCommMonoid (MvPowerSeries σ R)
-- Std.Http.Data.URI.Basic
/-- Asterisk-form request target (used with OPTIONS requests).
Example: `*`
 -/
Std.Http.RequestTarget.asteriskForm : Std.Http.RequestTarget
-- Init.Data.Sum.Basic
Sum.liftRel_inl_inl : ∀ {α : Type u_1} {γ : Type u_2} {r : α → γ → Prop} {β : Type u_3} {δ : Type u_4} {s : β → δ → Prop} {a : α} {c : γ},
  Sum.LiftRel r s (Sum.inl a) (Sum.inl c) ↔ r a c
-- Lean.Elab.BuiltinNotation
/-- Helper method for elaborating terms such as `(.+.)` where a constant name is expected.
This method is usually used to implement tactics that take function names as arguments
(e.g., `simp`).
 -/
Lean.Elab.Term.elabCDotFunctionAlias? : Lean.Term → Lean.Elab.TermElabM (Option Lean.Expr)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_getThenInsertIfNew? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {a : α} {b : β a},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(m.getThenInsertIfNew? a b).2).buckets).Perm
      (Std.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.denote_eq_cancel_eq : ∀ (ctx : Nat.Internal.Linear.Context) (m₁ m₂ : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.denote_eq ctx (m₁.cancel m₂) = Nat.Internal.Linear.Poly.denote_eq ctx (m₁, m₂)
-- Mathlib.SetTheory.ZFC.PSet
PSet.toSet_sUnion : ∀ (x : PSet.{u}), (⋃₀ x).toSet = ⋃₀ (PSet.toSet '' x.toSet)
-- Mathlib.GroupTheory.Nilpotent
Group.nilpotencyClass.eq_1 : ∀ (G : Type u_1) [inst : Group G], Group.nilpotencyClass G = if hG : Group.IsNilpotent G then Nat.find ⋯ else 0
-- Mathlib.Combinatorics.SetFamily.Intersecting
Set.Intersecting.mono : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {s t : Set α}, t ⊆ s → s.Intersecting → t.Intersecting
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse.  -/
EuclideanGeometry.dist_div_cos_oangle_left_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → dist p₁ p₂ / (EuclideanGeometry.oangle p₃ p₁ p₂).cos = dist p₁ p₃
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRciSlice : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] → Std.Rci.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RciSlice α β)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedSplitSource.default : Lean.Meta.Grind.SplitSource
-- Std.Http.Protocol.H1.Event
/-- Indicates a failure during parsing or processing.
 -/
Std.Http.Protocol.H1.Event.failed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Error → Std.Http.Protocol.H1.Event dir
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.lim_mem_Icc : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X),
  c.lim x ∈ Set.Icc 0 1
-- Std.Http.Transport
/-- Closes the mock server and client.
 -/
Std.Http.Internal.Mock.Client.close : Std.Http.Internal.Mock.Client → IO Unit
-- Mathlib.RingTheory.Congruence.Hom
/-- The homomorphism induced on the quotient of a ring by the kernel of a ring homomorphism.  -/
RingCon.kerLift : {M : Type u_1} →
  {P : Type u_3} →
    [inst : NonAssocSemiring M] → [inst_1 : NonAssocSemiring P] → (f : M →+* P) → (RingCon.ker f).Quotient →+* P
-- Init.Data.Nat.Lemmas
Nat.lt_of_lt_pred : ∀ {m n : ℕ}, m < n - 1 → m < n
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Prequotient.add.injEq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (a a_1 a_2 a_3 : RingCat.Colimits.Prequotient F), (a.add a_1 = a_2.add a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Logic.Embedding.Set
Function.Embedding.optionElim.congr_simp : ∀ {α : Type u_1} {β : Type u_2} (f f_1 : α ↪ β) (e_f : f = f_1) (x x_1 : β) (e_x : x = x_1) (h : x ∉ Set.range ⇑f),
  f.optionElim x h = f_1.optionElim x_1 ⋯
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatModInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Order.RelSeries
/-- For two preorders `α, β`, if `f : α → β` is surjective and strictly comonotonic, then a
strict series of `β` can be pulled back to a strict chain of `α` by
`b₀ < b₁ < ... < bₙ ↦ f⁻¹ b₀ < f⁻¹ b₁ < ... < f⁻¹ bₙ` where `f⁻¹ bᵢ` is an arbitrary element in the
preimage of `f⁻¹ {bᵢ}`.
 -/
LTSeries.comap : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        LTSeries β → (f : α → β) → (∀ ⦃x y : α⦄, f x < f y → x < y) → Function.Surjective f → LTSeries α
-- Mathlib.Topology.Ultrafilter
mapClusterPt_iff_ultrafilter : ∀ {X : Type u} {α : Type u_1} {x : X} [inst : TopologicalSpace X] {F : Filter α} {u : α → X},
  MapClusterPt x F u ↔ ∃ U, ↑U ≤ F ∧ Filter.Tendsto u (↑U) (nhds x)
-- Mathlib.Algebra.Order.Group.PosPart
one_le_leOnePart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : DivInvMonoid α] (a : α), 1 ≤ a⁻ᵐ
-- Init.Data.Option.Lemmas
Option.map_pbind : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {o : Option α} {f : (a : α) → o = some a → Option β} {g : β → γ},
  Option.map g (o.pbind f) = o.pbind fun a h => Option.map g (f a h)
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.utf8ByteSize'.eq_1 : ∀ (x : String), String.utf8ByteSize'✝ x = String.utf8ByteSize'.go✝ x.toList
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_natCast_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ) (a : R),
  Int.fract (↑n + a) = Int.fract a
-- Mathlib.Analysis.Complex.Polynomial.GaussLucas
/-- *Gauss-Lucas Theorem*: if $P$ is a nonconstant polynomial with complex coefficients,
then all zeros of $P'$ belong to the convex hull of the set of zeros of $P$.

See also `eq_centerMass_of_eval_derivative_eq_zero`
for a version that provides explicit coefficients of the convex combination.
 -/
Polynomial.rootSet_derivative_subset_convexHull_rootSet : ∀ {P : Polynomial ℂ}, 0 < P.degree → (Polynomial.derivative P).rootSet ℂ ⊆ (convexHull ℝ) (P.rootSet ℂ)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.orElse_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {x : ExceptT ε m α} {h : Unit → ExceptT ε m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps],
  (Std.Do.wp (OrElse.orElse x h)).apply Q = (Std.Do.wp x).apply (Q.1, fun x => (Std.Do.wp (h ())).apply Q, Q.2.2)
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.exists_lt_of_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [IsDirectedOrder α] {u : α → β} [inst_2 : Preorder β]
  [NoMaxOrder β], Filter.Tendsto u Filter.atTop Filter.atTop → ∀ (a : α) (b : β), ∃ a', a ≤ a' ∧ b < u a'
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- Nonzero fractional ideals contain a nonzero integer.  -/
FractionalIdeal.exists_ne_zero_mem_isInteger : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  {I : FractionalIdeal (nonZeroDivisors R) K} [Nontrivial R], I ≠ 0 → ∃ x, x ≠ 0 ∧ (algebraMap R K) x ∈ I