mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.mk.inj : ∀ {declName? : Option Lean.Name} {options : Lean.Options} {openDecls : List Lean.OpenDecl}
  {macroStack : Lean.Elab.MacroStack} {errToSorry : Bool} {levelNames : List Lean.Name}
  {fixedTermElabs : Array Lean.Elab.Term.FixedTermElabRef} {declName?_1 : Option Lean.Name} {options_1 : Lean.Options}
  {openDecls_1 : List Lean.OpenDecl} {macroStack_1 : Lean.Elab.MacroStack} {errToSorry_1 : Bool}
  {levelNames_1 : List Lean.Name} {fixedTermElabs_1 : Array Lean.Elab.Term.FixedTermElabRef},
  { declName? := declName?, options := options, openDecls := openDecls, macroStack := macroStack,
        errToSorry := errToSorry, levelNames := levelNames, fixedTermElabs := fixedTermElabs } =
      { declName? := declName?_1, options := options_1, openDecls := openDecls_1, macroStack := macroStack_1,
        errToSorry := errToSorry_1, levelNames := levelNames_1, fixedTermElabs := fixedTermElabs_1 } →
    declName? = declName?_1 ∧
      options = options_1 ∧
        openDecls = openDecls_1 ∧
          macroStack = macroStack_1 ∧
            errToSorry = errToSorry_1 ∧ levelNames = levelNames_1 ∧ fixedTermElabs = fixedTermElabs_1
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- The skew polynomials over `R` is the type of univariate polynomials over `R`
endowed with a skewed convolution product.  -/
SkewPolynomial : (R : Type u_1) → [AddCommMonoid R] → Type (max u_1 0)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
Matrix.Nondegenerate.toBilin : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] {ι : Type u_6}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] {M : Matrix ι ι R₂},
  M.Nondegenerate → ∀ (b : Module.Basis ι R₂ M₂), ((Matrix.toBilin b) M).Nondegenerate
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_neg_iff : ∀ {z : ℂ}, z.arg < 0 ↔ z.im < 0
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ioo_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a : α i), Pi.single i '' Set.Ioo a 0 = Set.Ioo (Pi.single i a) 0
-- Mathlib.Data.Set.Prod
Set.prod_eq_univ : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Nonempty α] [Nonempty β],
  s ×ˢ t = Set.univ ↔ s = Set.univ ∧ t = Set.univ
-- Mathlib.Data.List.Sigma
List.kerase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α), List.kerase a = List.eraseP fun s => decide (a = s.fst)