mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β}, (m.alter k f).contains k = (f m[k]?).isSome
-- Mathlib.Order.Atoms
BooleanAlgebra.le_iff_atom_le_imp : ∀ {α : Type u_4} [inst : BooleanAlgebra α] [IsAtomic α] {x y : α}, x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_lt_preOmega : ∀ {o₁ o₂ : Ordinal.{u_1}}, Ordinal.preOmega o₁ < Ordinal.preOmega o₂ ↔ o₁ < o₂
-- Lean.Widget.UserWidget
Lean.Widget.addPanelWidgetLocal : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Widget.WidgetInstance → m Unit
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.Limits.pushout.associator_inv_naturality_right_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] {A B X Y Z W : C} {f : A ⟶ B} {g : X ⟶ Y}
  {h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z W ⟶ A},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z W Y).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h Y)
          (CategoryTheory.Limits.pushout.inr (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g)))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z W X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp h f) X)
        (CategoryTheory.Limits.pushout.inl (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g)))
-- Init.Data.SInt.Lemmas
Int64.ofInt_lt_iff_lt : ∀ {a b : ℤ},
  Int64.minValue.toInt ≤ a →
    a ≤ Int64.maxValue.toInt →
      Int64.minValue.toInt ≤ b → b ≤ Int64.maxValue.toInt → (Int64.ofInt a < Int64.ofInt b ↔ a < b)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.map_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β),
  MeasurableSpace.map (⇑e) inst = inst_1
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
  [inst_4 : S₃.HasLeftHomology] (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃),
  CategoryTheory.ShortComplex.cyclesMap (CategoryTheory.CategoryStruct.comp φ₁ φ₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap φ₁)
      (CategoryTheory.ShortComplex.cyclesMap φ₂)
-- Mathlib.Analysis.Complex.RealDeriv
/-- If a function `f : ℝ → ℝ` is differentiable at a (real) point `x`, then it is also
differentiable as a function `ℝ → ℂ`.  -/
HasDerivAt.ofReal_comp : ∀ {z : ℝ} {f : ℝ → ℝ} {u : ℝ}, HasDerivAt f u z → HasDerivAt (fun y => ↑(f y)) (↑u) z
-- Mathlib.FieldTheory.Minpoly.Basic
/-- The degree of a minimal polynomial is positive.  -/
minpoly.degree_pos : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B],
  IsIntegral A x → 0 < (minpoly A x).degree
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.mem_weightSpace : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [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] (χ : L → R)
  (m : M), m ∈ LieModule.weightSpace M χ ↔ ∀ (x : L), ⁅x, m⁆ = χ x • m
-- Init.Data.UInt.Bitwise
USize.xor_eq_zero_iff : ∀ {a b : USize}, a ^^^ b = 0 ↔ a = b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
/-- If `G` is a group object, then `Hom(-, G)` is a presheaf of groups.  -/
CategoryTheory.yonedaGrpObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (G : C) → [CategoryTheory.GrpObj G] → CategoryTheory.Functor Cᵒᵖ GrpCat
-- Mathlib.RingTheory.LocalRing.Quotient
IsLocalRing.quotient_span_eq_top_iff_span_eq_top : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalRing R] [Module.Finite R S] (s : Set S),
  Submodule.span (R ⧸ IsLocalRing.maximalIdeal R)
        (⇑(Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) '' s) =
      ⊤ ↔
    Submodule.span R s = ⊤
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey_le_maxKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k} {he : t ≠ ∅}, (cmp (t.maxKey he) ((t.insertIfNew k v).maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
CategoryTheory.Limits.IsTerminal.isTerminalOfObj.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) (X : C)
  [inst_2 : CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Functor.empty C) G]
  (l l_1 : CategoryTheory.Limits.IsTerminal (G.obj X)),
  l = l_1 →
    CategoryTheory.Limits.IsTerminal.isTerminalOfObj G X l = CategoryTheory.Limits.IsTerminal.isTerminalOfObj G X l_1
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.div2.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Mathlib.LinearAlgebra.TensorProduct.Basic
/-- This used to be an `@[ext]` lemma, but it fails very slowly when the `ext` tactic tries to apply
it in some cases, notably when one wants to show equality of two linear maps. The `@[ext]`
attribute is now added locally where it is needed. Using this as the `@[ext]` lemma instead of
`TensorProduct.ext'` allows `ext` to apply lemmas specific to `M →ₗ _` and `N →ₗ _`.

See note [partially-applied ext lemmas].  -/
TensorProduct.ext : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring R₂] {σ₁₂ : R →+* R₂} {M : Type u_7}
  {N : Type u_8} {P₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : AddCommMonoid P₂]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R₂ P₂] {g h : TensorProduct R M N →ₛₗ[σ₁₂] P₂},
  (TensorProduct.mk R M N).compr₂ₛₗ g = (TensorProduct.mk R M N).compr₂ₛₗ h → g = h
-- Mathlib.Algebra.Module.StablyFree.Basic
/-- A module `M` over a ring `R` is called stably free if there exists a finite free `R`-module `N`
such that `M ⊕ N` is free.

The underlying constructor is marked as private. The intended constructor of `IsStablyFree` is
`IsStablyFree.of_free_prod`, and use `IsStablyFree.exist_free_prod` to extract the property from
`IsStablyFree`.  -/
Module.IsStablyFree : (R : Type u) → [inst : Ring R] → (M : Type u_1) → [inst_1 : AddCommGroup M] → [Module R M] → Prop
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.dual_injective_iff_surjective : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {A' : Type u_1} [inst_2 : AddCommGroup A']
  [inst_3 : Module R A] [inst_4 : Module R A'] {f : A →ₗ[R] A'},
  Function.Injective ⇑(CharacterModule.dual f) ↔ Function.Surjective ⇑f
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.commute_inl_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β]
  (m : α) (n : β), Commute ((OrderMonoidHom.inl α β) m) ((OrderMonoidHom.inr α β) n)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderiv_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F},
  fderiv 𝕜 Prod.snd p = ContinuousLinearMap.snd 𝕜 E F
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
/-- The submodule of compact continuous linear maps.  -/
compactOperator : {R₁ : Type u_1} →
  {R₄ : Type u_2} →
    [inst : Semiring R₁] →
      [inst_1 : CommSemiring R₄] →
        (σ₁₄ : R₁ →+* R₄) →
          (M₁ : Type u_3) →
            (M₄ : Type u_5) →
              [inst_2 : TopologicalSpace M₁] →
                [inst_3 : AddCommMonoid M₁] →
                  [inst_4 : TopologicalSpace M₄] →
                    [inst_5 : AddCommGroup M₄] →
                      [inst_6 : Module R₁ M₁] →
                        [inst_7 : Module R₄ M₄] →
                          [inst_8 : ContinuousConstSMul R₄ M₄] →
                            [inst_9 : IsTopologicalAddGroup M₄] → Submodule R₄ (M₁ →SL[σ₁₄] M₄)
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_self : ∀ {K : Type u_1} {L : Type u_2} [inst : CommRing K] [inst_1 : CommRing L] (i : K →+* L) (p : ℕ) [inst_2 : ExpChar K p]
  [inst_3 : ExpChar L p] [inst_4 : PerfectRing L p] [inst_5 : IsPerfectClosure i p],
  IsPerfectClosure.equiv i i p = RingEquiv.refl L
-- Init.Control.Lawful.Basic
/-- A functor satisfies the functor laws.

The `Functor` class contains the operations of a functor, but does not require that instances
prove they satisfy the laws of a functor. A `LawfulFunctor` instance includes proofs that the laws
are satisfied. Because `Functor` instances may provide optimized implementations of `mapConst`,
`LawfulFunctor` instances must also prove that the optimized implementation is equivalent to the
standard implementation.
 -/
LawfulFunctor : (f : Type u → Type v) → [Functor f] → Prop
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveGoal.pretty : Lean.Widget.InteractiveGoal → Std.Format
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Icc_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a b : Fin n),
  ∏ i ∈ Finset.Icc (Fin.cast h a) (Fin.cast h b), f i = ∏ i ∈ Finset.Icc a b, f (Fin.cast h i)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.prod_coe : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ),
  ↑(e.prod e') = fun p => (↑e p.1, ↑e' p.2)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_filter_eq_size_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  m.WF →
    ((Std.DHashMap.Raw.filter f m).size = m.size ↔
      ∀ (a : α) (h : a ∈ m), f (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = true)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.instSetLike : {α : Type u_2} → [inst : TopologicalSpace α] → SetLike (TopologicalSpace.IrreducibleCloseds α) α
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- The distance on `X ⊕ Y` as a candidate  -/
GromovHausdorff.candidatesBDist : (X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [CompactSpace X] →
        [Nonempty X] → [inst_3 : MetricSpace Y] → [CompactSpace Y] → [Nonempty Y] → GromovHausdorff.Cb✝ X Y
-- Mathlib.Data.List.NodupEquivFin
/-- If `l` is a list sorted w.r.t. `(<)`, then `List.get` defines an order isomorphism between
`Fin (length l)` and the set of elements of `l`.  -/
List.SortedLT.getIso : {α : Type u_1} → [inst : Preorder α] → [DecidableEq α] → (l : List α) → l.SortedLT → Fin l.length ≃o { x // x ∈ l }
-- Lean.Meta.Tactic.Simp.Attr
Lean.Meta.simpExtension : Lean.Meta.SimpExtension
-- Std.Http.Data.URI.Basic
/-- Returns a new URI with the scheme replaced.
 -/
Std.Http.URI.withScheme! : Std.Http.URI → String → Std.Http.URI
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.FindMin.mk.injEq : ∀ {α : Type u_1} (before : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α) (val : α)
  (node : Batteries.BinomialHeap.Imp.HeapNode α) (next : Batteries.BinomialHeap.Imp.Heap α)
  (before_1 : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α) (val_1 : α)
  (node_1 : Batteries.BinomialHeap.Imp.HeapNode α) (next_1 : Batteries.BinomialHeap.Imp.Heap α),
  ({ before := before, val := val, node := node, next := next } =
      { before := before_1, val := val_1, node := node_1, next := next_1 }) =
    (before = before_1 ∧ val = val_1 ∧ node = node_1 ∧ next = next_1)
-- Mathlib.Topology.Algebra.GroupCompletion
instZeroCompletion : {α : Type u_3} → [inst : UniformSpace α] → [Zero α] → Zero (UniformSpace.Completion α)
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- Given injective resolutions `I` and `I'` of two objects `Z` and `Z'`,
and a morphism `f : Z ⟶ Z'`, this structure contains the data of a morphism
`I.cocomplex ⟶ I'.cocomplex` which is compatible with `f`  -/
CategoryTheory.InjectiveResolution.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          CategoryTheory.InjectiveResolution Z → {Z' : C} → CategoryTheory.InjectiveResolution Z' → (Z ⟶ Z') → Type v
-- Mathlib.Algebra.Homology.Augment
ChainComplex.augmentTruncate_inv_f_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) (i : ℕ), C.augmentTruncate.inv.f (i + 1) = CategoryTheory.CategoryStruct.id (C.X (i + 1))
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.instCategoryI₀Cover : {S : AlgebraicGeometry.Scheme} →
  {𝒰 : S.OpenCover} →
    [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀] →
      [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
        (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰) →
          [inst_2 : Small.{u, u_1} 𝒰.I₀] → [inst_3 : Quiver.IsThin 𝒰.I₀] → CategoryTheory.Category.{u_2, u_1} d.cover.I₀
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.iSup_generateFrom : ∀ {α : Type u_1} {ι : Sort u_6} (s : ι → Set (Set α)),
  ⨆ i, MeasurableSpace.generateFrom (s i) = MeasurableSpace.generateFrom (⋃ i, s i)
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.mk.injEq : ∀ (hour : Std.Time.Hour.Ordinal) (minute : Std.Time.Minute.Ordinal) (second : Std.Time.Second.Ordinal true)
  (nanosecond : Std.Time.Nanosecond.Ordinal) (hour_1 : Std.Time.Hour.Ordinal) (minute_1 : Std.Time.Minute.Ordinal)
  (second_1 : Std.Time.Second.Ordinal true) (nanosecond_1 : Std.Time.Nanosecond.Ordinal),
  ({ hour := hour, minute := minute, second := second, nanosecond := nanosecond } =
      { hour := hour_1, minute := minute_1, second := second_1, nanosecond := nanosecond_1 }) =
    (hour = hour_1 ∧ minute = minute_1 ∧ second = second_1 ∧ nanosecond = nanosecond_1)
-- Mathlib.Algebra.Order.Star.Basic
star_left_conjugate_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a : R}, 0 ≤ a → ∀ (c : R), 0 ≤ star c * a * c
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₀_comp_assoc : ∀ {X Y : SSet} (f : X ⟶ Y) {Z : SSet}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y (SSet.stdSimplex.obj { len := 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (SSet.stdSimplex.obj { len := 1 })) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp SSet.ι₀ h)
-- Mathlib.Algebra.Ring.Int.Defs
Int.instMulDivCancelClass : MulDivCancelClass ℤ
-- Mathlib.Data.Set.Functor
/-- This is `Set` but with a `Monad` instance.  -/
SetM : Type u → Type u
-- Init.Data.Vector.Lemmas
Vector.reflBEq_iff : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [NeZero n], ReflBEq (Vector α n) ↔ ReflBEq α
-- Mathlib.Analysis.Meromorphic.Order
/-- The order is additive in products of meromorphic functions.
 -/
meromorphicOrderAt_fun_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {ι : Type u_5} {s : Finset ι} {f : ι → 𝕜 → 𝕜'},
  (∀ i ∈ s, MeromorphicAt (f i) x) →
    meromorphicOrderAt (fun a => ∏ i ∈ s, f i a) x = ∑ i ∈ s, meromorphicOrderAt (f i) x
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.algebra : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {N : Type u_6} →
                  [inst_4 : TopologicalSpace N] →
                    [inst_5 : ChartedSpace H N] →
                      {n : WithTop ℕ∞} →
                        {A : Type u_10} →
                          [inst_6 : NormedRing A] →
                            [inst_7 : NormedAlgebra 𝕜 A] →
                              [inst_8 : ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] →
                                Algebra 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A n)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.Nonsingular.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) (P : Fin 3 → R),
  W'.Nonsingular P =
    (W'.Equation P ∧
      ((MvPolynomial.eval P) W'.polynomialX ≠ 0 ∨
        (MvPolynomial.eval P) W'.polynomialY ≠ 0 ∨ (MvPolynomial.eval P) W'.polynomialZ ≠ 0))
-- Init.Data.List.Scan.Lemmas
List.scanr_singleton : ∀ {α : Type u_1} {β : Type u_2} {b : β} {a : α} {f : α → β → β}, List.scanr f b [a] = [f a b, b]
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.instIsMulLeftInvariantHausdorffMeasureOfIsIsometricSMul : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {d : ℝ} [inst_3 : Group X]
  [IsIsometricSMul X X], (MeasureTheory.Measure.hausdorffMeasure d).IsMulLeftInvariant
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.insert : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'},
  g =o[nhdsWithin x s] g' → g x = 0 → g =o[nhdsWithin x (insert x s)] g'
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- Version of `ContMDiffWithinAt.congr` where `x` need not be contained in `s`,
but `f` and `f₁` are equal on a set containing both.  -/
ContMDiffWithinAt.congr' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s t : Set M} {x : M}
  {n : WithTop ℕ∞},
  ContMDiffWithinAt I I' n f s x → (∀ y ∈ t, f₁ y = f y) → s ⊆ t → x ∈ t → ContMDiffWithinAt I I' n f₁ s x
-- Mathlib.NumberTheory.Padics.Measure.Basic
AbstractMeasure.prodMk'_apply : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (μ : AbstractMeasure X R R)
  (ν : AbstractMeasure Y R R) [inst_5 : LocallyCompactSpace X] [inst_6 : LocallyCompactSpace Y] (f : C(X × Y, R)),
  ((AbstractMeasure.prodMk' μ) ν) f = μ ((AbstractMeasure.contractSnd ν) f)
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageActionItem.title : Lean.Lsp.MessageActionItem → String
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk.congr_simp : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (x x_1 : ↥X) (e_x : x = x_1) (y y_1 : ↥Y) (e_y : y = y_1)
  (s s_1 : ↥S) (e_s : s = s_1) (hx : f x = s) (hy : g y = s),
  { x := x, y := y, s := s, hx := hx, hy := hy } = { x := x_1, y := y_1, s := s_1, hx := ⋯, hy := ⋯ }
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The identity morphism of an algebra of endofunctor `F`  -/
CategoryTheory.Endofunctor.Coalgebra.Hom.id : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} → (V : CategoryTheory.Endofunctor.Coalgebra F) → V.Hom V
-- Init.Data.SInt.Lemmas
Int16.sub_eq_add_neg : ∀ (a b : Int16), a - b = a + -b
-- Init.Data.SInt.Lemmas
Int16.ofInt_iSizeToInt : ∀ (x : ISize), Int16.ofInt x.toInt = x.toInt16
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.le : ∀ {m : ℕ} {L : List ℕ}, SimplexCategoryGenRel.IsAdmissible m L → ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} [inst : Fintype α],
  G.Colorable (Fintype.card α) → (G.chromaticNumber = ↑(Fintype.card α) ↔ ∀ (C : G.Coloring α), Function.Surjective ⇑C)
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
/-- If `P` and `P'` are properties of objects such that `P ≤ P'`, there is
an induced functor `P.FullSubcategory ⥤ P'.FullSubcategory`.  -/
CategoryTheory.ObjectProperty.ιOfLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P P' : CategoryTheory.ObjectProperty C} → P ≤ P' → CategoryTheory.Functor P.FullSubcategory P'.FullSubcategory
-- Lean.Util.Diff
Lean.Diff.instHashableAction : Hashable Lean.Diff.Action
-- Lean.Level
Lean.Level.isZero : Lean.Level → Bool
-- Lean.Structure
/-- We use an environment extension to cache resolution orders.
These are not expensive to compute, but worth caching, and we save olean storage space.
 -/
Lean.structureResolutionExt : Lean.EnvExtension Lean.StructureResolutionState
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- An isomorphism in the language of rings is a ring isomorphism  -/
FirstOrder.Ring.languageEquivEquivRingEquiv : {R : Type u_2} →
  {S : Type u_3} →
    [inst : NonAssocRing R] →
      [inst_1 : NonAssocRing S] →
        [inst_2 : FirstOrder.Ring.CompatibleRing R] →
          [inst_3 : FirstOrder.Ring.CompatibleRing S] → FirstOrder.Language.ring.Equiv R S ≃ (R ≃+* S)
-- Lean.Expr
Lean.Expr.updateForallE! : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Init.Data.Vector.Lemmas
Vector.all_toArray : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.toArray.all p = xs.all p
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.saturate_of_superset : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (K : CategoryTheory.Coverage C) {X : C}
  {S T : CategoryTheory.Sieve X}, S ≤ T → K.Saturate X S → K.Saturate X T
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_of_get?_eq_some : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a a' : α}, m.get? a = some a' → a' ∈ m
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The special case where the vector field is independent of time  -/
IsPicardLindelof.of_time_independent : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : E → E} {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E}
  {a r L K : NNReal},
  (∀ x ∈ Metric.closedBall x₀ ↑a, ‖f x‖ ≤ ↑L) →
    LipschitzOnWith K f (Metric.closedBall x₀ ↑a) →
      ↑L * max (tmax - ↑t₀) (↑t₀ - tmin) ≤ ↑a - ↑r → IsPicardLindelof (fun x => f) t₀ x₀ a r L K
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_next : ∀ {s : String} (p : s.Pos) (hp : p ≠ s.endPos),
  (p.next hp).Splits ((s.sliceTo p).copy ++ String.singleton (p.get hp)) (s.sliceFrom (p.next hp)).copy
-- Mathlib.GroupTheory.PGroup
IsPGroup.powEquiv_apply : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (hG : IsPGroup p G) {n : ℕ} (hn : p.Coprime n) (g : G),
  (hG.powEquiv hn) g = g ^ n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqExpr.beq : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Bool