mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HahnSeries.PowerSeries
/-- The ring `R⟦σ →₀ ℕ⟧` is isomorphic to `MvPowerSeries σ R` for a `Finite` `σ`.
We take the index set of the hahn series to be `Finsupp` rather than `pi`,
even though we assume `Finite σ` as this is more natural for alignment with `MvPowerSeries`.
After importing `Mathlib/Algebra/Order/Pi.lean` the ring `R⟦σ → ℕ⟧` could be constructed
instead.
 -/
HahnSeries.toMvPowerSeries : {R : Type u_2} → [inst : Semiring R] → {σ : Type u_3} → [Finite σ] → HahnSeries (σ →₀ ℕ) R ≃+* MvPowerSeries σ R
-- Init.Data.Array.Lemmas
Array.contains_map : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {xs : Array α} {x : β} {f : α → β},
  (Array.map f xs).contains x = xs.any fun a => x == f a
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.isPrincipal_mul_of_le_two : ∀ {o : Ordinal.{u}}, o ≤ 2 → Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o
-- Mathlib.Algebra.GroupWithZero.Action.Basic
smulMonoidWithZeroHom_apply : ∀ {M₀ : Type u_5} {N₀ : Type u_6} [inst : MonoidWithZero M₀] [inst_1 : MulZeroOneClass N₀]
  [inst_2 : MulActionWithZero M₀ N₀] [inst_3 : IsScalarTower M₀ N₀ N₀] [inst_4 : SMulCommClass M₀ N₀ N₀] (a : M₀ × N₀),
  smulMonoidWithZeroHom a = (↑smulMonoidHom).toFun a
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.Hom.category : {B : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Bicategory C] →
      {F : B → C} → (X Y : CategoryTheory.Bicategory.InducedBicategory C F) → CategoryTheory.Category.{u_3, u_4} (X ⟶ Y)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_erase_le_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (cmp ((t.erase k).max he) (t.max ⋯)).isLE = true
-- Mathlib.Control.Monad.Cont
/-- Build a `ContT` from a function taking a continuation callback.  -/
ContT.mk : {r : Type u} → {m : Type u → Type v} → {α : Type w} → ((α → m r) → m r) → ContT r m α
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_hom_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.op =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (Opposite.op X)).inv
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.mkOfSucc_zero_eq_δ : SimplexCategory.mkOfSucc 0 = SimplexCategory.δ 2
-- Mathlib.Order.Iterate
Function.Commute.iterate_pos_le_iff_map_le : ∀ {α : Type u_1} [inst : LinearOrder α] {f g : α → α},
  Function.Commute f g → Monotone f → StrictMono g → ∀ {x : α} {n : ℕ}, 0 < n → (f^[n] x ≤ g^[n] x ↔ f x ≤ g x)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.ofArray_eq_ofList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} (a : Array ((a : α) × β a)),
  Std.DHashMap.ofArray a = Std.DHashMap.ofList a.toList
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Init.Data.List.Find
List.map_findSome? : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → Option β} {g : β → γ} {l : List α},
  Option.map g (List.findSome? f l) = List.findSome? (Option.map g ∘ f) l
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey!_modifyKey_beq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] [inst_4 : Inhabited α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β},
      (Std.Internal.List.minKey! (Std.Internal.List.Const.modifyKey k f l) == Std.Internal.List.minKey! l) = true
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_inter!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter! m₂).getKey? k = m₁.getKey? k
-- Lean.Server.CodeActions.Basic
/-- Passed as the `data?` field of `Lsp.CodeAction` to recover the context of the code action.  -/
Lean.Server.CodeActionResolveData : Type
-- Mathlib.Computability.Language
Language.reverse_surjective : ∀ {α : Type u_1}, Function.Surjective Language.reverse
-- Mathlib.Analysis.Subadditive
Subadditive.lim_le_div : ∀ {u : ℕ → ℝ} (h : Subadditive u), BddBelow (Set.range fun n => u n / ↑n) → ∀ {n : ℕ}, n ≠ 0 → h.lim ≤ u n / ↑n
-- Mathlib.Topology.Algebra.Algebra
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousAlgHom.Simps.apply : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (A →A[R] B) → A → B
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
zero_notMem_nonZeroDivisorsLeft : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [Nontrivial M₀], 0 ∉ nonZeroDivisorsLeft M₀
-- Init.Grind.ToInt
Lean.Grind.instLawfulBEqIntInterval : LawfulBEq Lean.Grind.IntInterval
-- Mathlib.Order.Types.Defs
OrderType.type_ne_zero : ∀ {α : Type u} [inst : LinearOrder α] [h : Nonempty α], OrderType.type α ≠ 0
-- Init.Data.Int.Gcd
Int.gcd_zero_left : ∀ (a : ℤ), Int.gcd 0 a = a.natAbs
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.monoidal_tensorUnit_comon_comul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.ComonObj.comul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.not_haveLebesgueDecomposition_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α),
  ¬s.HaveLebesgueDecomposition μ ↔
    ¬s.toJordanDecomposition.posPart.HaveLebesgueDecomposition μ ∨
      ¬s.toJordanDecomposition.negPart.HaveLebesgueDecomposition μ
-- Mathlib.FieldTheory.Normal.Defs
Normal.of_algEquiv : ∀ {F : Type u_1} [inst : Field F] {E : Type u_3} [inst_1 : Field E] [inst_2 : Algebra F E] {E' : Type u_4}
  [inst_3 : Field E'] [inst_4 : Algebra F E'] [h : Normal F E] (f : E ≃ₐ[F] E'), Normal F E'
-- Init.Data.List.Nat.Modify
List.modify_eq_set : ∀ {α : Type u_1} [inst : Inhabited α] (f : α → α) (i : ℕ) (l : List α), l.modify i f = l.set i (f (l[i]?.getD default))
-- Mathlib.CategoryTheory.CommSq
/-- The commutative square associated to a commutative square in the opposite category.  -/
CategoryTheory.CommSq.unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z}, CategoryTheory.CommSq f g h i → CategoryTheory.CommSq i.unop h.unop g.unop f.unop
-- Mathlib.Data.ZMod.Basic
ZModModule.char_nsmul_eq_zero : ∀ (n : ℕ) {G : Type u_2} [inst : AddCommGroup G] [Module (ZMod n) G] (x : G), n • x = 0
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- A ring with a valuative relation is discrete if its value group-with-zero
has a maximal element `< 1`.  -/
ValuativeRel.IsDiscrete : (R : Type u_1) → [inst : Semiring R] → [ValuativeRel R] → Prop
-- Mathlib.Analysis.Complex.Basic
Complex.nndist_conj_conj : ∀ (z w : ℂ), nndist ((starRingEnd ℂ) z) ((starRingEnd ℂ) w) = nndist z w
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- If
* `p : ι' → MvPolynomial ι K` is a family of polynomials (which in practice will be homogeneous
  of the same degree `N`),
* `q : ι × ι' → MvPolynomial ι K` is a family of homogeneous polynomials of the same degree `M`,
* `x : ι → K` is such that for all `k : ι`,
  `∑ j, (q (k, j)).eval x * (p j).eval x = (x k) ^ (M + N)`,

then the multiplicative height of `fun j ↦ (p j).eval x` is bounded below by a positive
constant depending only on `q` times the `N`th power of the multiplicative height of `x`.

The difference to `mulHeight_eval_ge` is that the constant is not made explicit.  -/
Height.mulHeight_eval_ge' : ∀ {K : Type u_6} [inst : Field K] {ι : Type u_7} {ι' : Type u_8} [inst_1 : Fintype ι']
  [inst_2 : Height.AdmissibleAbsValues K] [Finite ι] {M N : ℕ} {q : ι × ι' → MvPolynomial ι K},
  (∀ (a : ι × ι'), (q a).IsHomogeneous M) →
    ∃ C > 0,
      ∀ (p : ι' → MvPolynomial ι K) {x : ι → K},
        (∀ (k : ι), ∑ j, (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) →
          C * Height.mulHeight x ^ N ≤ Height.mulHeight fun j => (MvPolynomial.eval x) (p j)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_mem_coeffs : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.coeff n ≠ 0 → p.coeff n ∈ p.coeffs
-- Mathlib.Analysis.Convex.Strict
/-- A set is strictly convex if the open segment between any two distinct points lies is in its
interior. This basically means "convex and not flat on the boundary".  -/
StrictConvex : (𝕜 : Type u_6) →
  {E : Type u_7} →
    [Semiring 𝕜] → [PartialOrder 𝕜] → [TopologicalSpace E] → [AddCommMonoid E] → [SMul 𝕜 E] → Set E → Prop
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instInv : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Inv β] → Inv (MeasureTheory.SimpleFunc α β)