mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given a commutative ring `A` with field of fractions `K`,
and an injective ring hom `g : A →+* L` where `L` is a field,
field hom induced from `K` to `L` maps `f x / f y` to `g x / g y` for all
`x : A, y ∈ NonZeroDivisors A`.  -/
IsFractionRing.lift_mk' : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] {L : Type u_7} [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {g : A →+* L} (hg : Function.Injective ⇑g) (x : A)
  (y : ↥(nonZeroDivisors A)), (IsFractionRing.lift hg) (IsLocalization.mk' K x y) = g x / g ↑y
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.coeFn_coe : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (f : LieDerivation R L M), ⇑↑f = ⇑f
-- Init.Omega.Constraint
Lean.Omega.Constraint.neg_sat : ∀ {c : Lean.Omega.Constraint} {v : ℤ}, c.sat v = true → c.neg.sat (-v) = true
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.instNeg : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        [inst : Ring k] →
          [inst_1 : AddCommGroup V1] →
            [inst_2 : Module k V1] →
              [inst_3 : AddTorsor V1 P1] → [inst_4 : AddCommGroup V2] → [inst_5 : Module k V2] → Neg (P1 →ᵃ[k] V2)
-- Init.Data.SInt.Lemmas
Int32.toInt8_ofInt : ∀ {n : ℤ}, (Int32.ofInt n).toInt8 = Int8.ofInt n
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version within a set at a point, but with full pullback.  -/
MDifferentiableWithinAt.mpullback_vectorField_preimage_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} {y₀ : M'} [inst_11 : IsManifold I 2 M]
  [inst_12 : IsManifold I' 2 M'] [CompleteSpace E],
  MDiffAt[t] (T% V) y₀ →
    ContMDiffAt I I' n f x₀ →
      (mfderiv% f x₀).IsInvertible →
        2 ≤ n → y₀ = f x₀ → (MDiffAt[f ⁻¹' t] fun x => ⟨x, VectorField.mpullback I I' f V x⟩) x₀
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ Dᵒᵖ` creates finite coproducts, then `F.leftOp : Cᵒᵖ ⥤ D` creates finite
products.  -/
CategoryTheory.Limits.createsFiniteProductsLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C Dᵒᵖ) →
          [CategoryTheory.Limits.CreatesFiniteCoproducts F] → CategoryTheory.Limits.CreatesFiniteProducts F.leftOp
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mk'.congr_simp : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s s_1 : Set R) (e_s : s = s_1) (sm sm_1 : Subsemigroup R)
  (e_sm : sm = sm_1) (sa sa_1 : AddSubgroup R) (e_sa : sa = sa_1) (hm : ↑sm = s) (ha : ↑sa = s),
  NonUnitalSubring.mk' s sm sa hm ha = NonUnitalSubring.mk' s_1 sm_1 sa_1 ⋯ ⋯
-- Mathlib.Topology.Separation.Hausdorff
/-- The smallest equivalence relation on a topological space giving a T2 quotient.  -/
t2Setoid : (X : Type u_1) → [TopologicalSpace X] → Setoid X
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.ennreal_smul_extend : ∀ {α : Type u_2} {P : α → Prop} (m : (s : α) → P s → ENNReal) {c : ENNReal},
  c ≠ 0 → c • MeasureTheory.extend m = MeasureTheory.extend fun s h => c • m s h
-- Mathlib.Data.Int.Cast.Basic
Nat.cast_sub : ∀ {R : Type u} [inst : AddGroupWithOne R] {m n : ℕ}, m ≤ n → ↑(n - m) = ↑n - ↑m
-- Mathlib.RingTheory.Artinian.Module
isArtinian_of_range_eq_ker : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} {N : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup P] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R P] [inst_6 : Module R N]
  [IsArtinian R M] [IsArtinian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P), f.range = g.ker → IsArtinian R N
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The opposite of the left homology functor is the right homology functor.  -/
CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasKernels C] →
        [inst_3 : CategoryTheory.Limits.HasCokernels C] →
          [inst_4 : CategoryTheory.Limits.HasKernels Cᵒᵖ] →
            [inst_5 : CategoryTheory.Limits.HasCokernels Cᵒᵖ] →
              (CategoryTheory.ShortComplex.leftHomologyFunctor C).op ≅
                (CategoryTheory.ShortComplex.opFunctor C).comp (CategoryTheory.ShortComplex.rightHomologyFunctor Cᵒᵖ)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_eq : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ : C₂} {X₃ : C₃},
  adj₂.homEquiv = (adj₂.adj X₁).homEquiv X₂ X₃
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.IsClosable.congr_simp : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] (f f_1 : E →ₗ.[R] F), f = f_1 → f.IsClosable = f_1.IsClosable
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
/-- The underlying isometry  -/
QuadraticModuleCat.Hom.toIsometry' : {R : Type u} → [inst : CommRing R] → {V W : QuadraticModuleCat R} → V.Hom W → V.form →qᵢ W.form
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.id : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_4} →
      [inst_1 : AddMonoid A] → [inst_2 : CategoryTheory.HasShift C A] → (CategoryTheory.Functor.id C).CommShift A
-- Mathlib.Algebra.Category.MonCat.Basic
/-- additive equivalences between `AddMonoid`s are the same
as (isomorphic to) isomorphisms in `AddMonCat`  -/
addEquivIsoAddMonCatIso : {X Y : Type u} → [inst : AddMonoid X] → [inst_1 : AddMonoid Y] → X ≃+ Y ≅ AddMonCat.of X ≅ AddMonCat.of Y
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.ofIsClopen_fiber_one : ∀ {X : Type u_5} [inst : TopologicalSpace X] {U : Set X} [inst_1 : (x : X) → Decidable (x ∈ U)] (hU : IsClopen U),
  ⇑(LocallyConstant.ofIsClopen hU) ⁻¹' {1} = Uᶜ
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.commute : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g} {x : B} {h : x ⟶ c}
  [self : CategoryTheory.Bicategory.LanLift.CommuteWith f g h],
  Nonempty ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h).IsKan
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat.injEq : ∀ (e thm : Lean.Expr) (d : ℕ) (a : Int.Internal.Linear.Expr) (e_1 thm_1 : Lean.Expr) (d_1 : ℕ)
  (a_1 : Int.Internal.Linear.Expr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat e thm d a =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat e_1 thm_1 d_1 a_1) =
    (e = e_1 ∧ thm = thm_1 ∧ d = d_1 ∧ a = a_1)
-- Init.Data.SInt.IntToBitVec
USize.toBitVec64_toISize : ∀ (n : USize) (h : System.Platform.numBits = 64), n.toISize.toBitVec64 h = n.toBitVec64 h
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.nameLitAux : String.Pos.Raw → Lean.Parser.ParserFn
-- Mathlib.Order.Preorder.Finite
/-- A strictly monotone self-map of a finite linear order is the identity.  -/
StrictMono.eq_id : ∀ {α : Type u_4} [inst : LinearOrder α] [Finite α] {f : α → α}, StrictMono f → f = id
-- Mathlib.Topology.EMetricSpace.Defs
Metric.mem_eball_comm : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {ε : ENNReal}, x ∈ Metric.eball y ε ↔ y ∈ Metric.eball x ε
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_prod_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (a : α) (b : β),
  Set.Iic a ×ˢ Set.Iic b = Set.Iic (a, b)
-- Init.Data.String.Subslice
String.Slice.endExclusive_toSubslice : ∀ {s : String.Slice}, s.toSubslice.endExclusive = s.endPos
-- Init.Data.List.Find
List.findIdx?_eq_bind_find?_idxOf? : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : List α} {p : α → Bool},
  List.findIdx? p xs = (List.find? p xs).bind fun a => List.idxOf? a xs
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofFiniteGrpHom.eq_1 : ∀ {G H : FiniteGrp.{u}} (f : G ⟶ H),
  ProfiniteGrp.ofFiniteGrpHom f =
    CategoryTheory.ConcreteCategory.ofHom { toMonoidHom := GrpCat.Hom.hom f.hom, continuous_toFun := ⋯ }
-- Mathlib.Data.Num.Bitwise
instOneNzsNum : One NzsNum
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonModuleHierarchyOptions : Lean.FromJson Lean.Lsp.ModuleHierarchyOptions