mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ResidueField
/-- The isomorphism between residue fields of equal points.  -/
AlgebraicGeometry.Scheme.residueFieldCongr : {X : AlgebraicGeometry.Scheme} → {x y : ↥X} → x = y → (X.residueField x ≅ X.residueField y)
-- Mathlib.LinearAlgebra.Prod
LinearMap.prod_eq_inf_comap : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (p : Submodule R M) (q : Submodule R M₂),
  p.prod q = Submodule.comap (LinearMap.fst R M M₂) p ⊓ Submodule.comap (LinearMap.snd R M M₂) q
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_left_le_size_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t₁.size ≤ (t₁ ∪ t₂).size
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a fallback : α},
  a ∉ t → t.getD a fallback = fallback
-- Init.Data.List.Perm
List.Perm.filterMap : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) {l₁ l₂ : List α},
  l₁.Perm l₂ → (List.filterMap f l₁).Perm (List.filterMap f l₂)
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesHasSum.smul : ∀ {f : ℕ → ℂ} (c : ℂ) {s a : ℂ}, LSeriesHasSum f s a → LSeriesHasSum (c • f) s (c * a)
-- Mathlib.Order.Heyting.Basic
sdiff_le_inf_hnot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, b \ a ≤ b ⊓ ￢a
-- Mathlib.GroupTheory.Submonoid.Center
addUnitsCenterToCenterAddUnits.eq_1 : ∀ (M : Type u_1) [inst : AddMonoid M],
  addUnitsCenterToCenterAddUnits M =
    (AddUnits.map (AddSubmonoid.center M).subtype).codRestrict (AddSubmonoid.center (AddUnits M)) ⋯
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.ext_iff : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {S T : ↥L}, S = T ↔ ∀ (x : X), x ∈ S ↔ x ∈ T
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.ι_comp_colimitLeftOpIsoUnopLimit_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.leftOp j)
      (CategoryTheory.Limits.colimitLeftOpIsoUnopLimit F).hom =
    (CategoryTheory.Limits.limit.π F (Opposite.unop j)).unop
-- Lean.Data.Lsp.InitShutdown
/-- Whether the client supports interactive widgets. When true, in order to improve performance
the server may cease including information which can be retrieved interactively in some standard
LSP messages. Defaults to false.  -/
Lean.Lsp.InitializationOptions.hasWidgets? : Lean.Lsp.InitializationOptions → Option Bool
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atTop_of_add_le_const : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  (∃ C, ∀ (x : α), g x ≤ C) → Filter.Tendsto (fun x => f x + g x) l Filter.atTop → Filter.Tendsto f l Filter.atTop
-- Mathlib.Algebra.DualQuaternion
Quaternion.imJ_fst_dualNumberEquiv : ∀ {R : Type u_1} [inst : CommRing R] (q : Quaternion (DualNumber R)),
  (TrivSqZeroExt.fst (Quaternion.dualNumberEquiv q)).imJ = TrivSqZeroExt.fst q.imJ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₁_le_cocycles₁ : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{max u u_1, u, u} k G),
  groupCohomology.coboundaries₁ A ≤ groupCohomology.cocycles₁ A
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- `limSeq f`, for `f` a Cauchy sequence of `p`-adic numbers, is a sequence of rationals with the
same limit point as `f`.  -/
Padic.limSeq : {p : ℕ} → [inst : Fact (Nat.Prime p)] → CauSeq ℚ_[p] ⇑padicNormE → ℕ → ℚ
-- Init.Data.Vector.Lemmas
/-- A vector of length `0` is the empty vector.  -/
Vector.eq_empty : ∀ {α : Type u_1} {xs : Vector α 0}, xs = #v[]
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.totalSpaceMk_preimage_source : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B),
  Bundle.TotalSpace.mk b ⁻¹' (a.pretrivializationAt b).source = Set.univ
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin_ofNat : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (s : Set 𝕜) (n : ℕ) [inst_3 : OfNat F n], derivWithin (OfNat.ofNat n) s = 0
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalUInt64_qq : Lean.Meta.ReduceEval UInt64
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_mul_X : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [IsDomain R], (f * Polynomial.X).Splits ↔ f.Splits
-- Std.Data.Iterators.Combinators.Monadic.Zip
Std.Iterators.Types.Zip.right : {α₁ : Type w} →
  {m : Type w → Type w'} →
    {β₁ : Type w} →
      [inst : Std.Iterator α₁ m β₁] → {α₂ β₂ : Type w} → Std.Iterators.Types.Zip α₁ m α₂ β₂ → Std.IterM m β₂
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceTextDocumentPositionParams : Lean.Lsp.FileSource Lean.Lsp.TextDocumentPositionParams
-- Mathlib.Condensed.Light.Basic
/-- Light condensed sets. Because `LightProfinite` is an essentially small category, we don't need the
same universe bump as in `CondensedSet`.
 -/
LightCondSet : Type (u + 1)
-- Mathlib.CategoryTheory.Linear.Basic
/-- A category is called `R`-linear if `P ⟶ Q` is an `R`-module such that composition is
`R`-linear in both variables.  -/
CategoryTheory.Linear : (R : Type w) →
  [Semiring R] →
    (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Preadditive C] → Type (max (max u v) w)
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- Constructor for morphisms from the fiber of a presheaf.  -/
CategoryTheory.GrothendieckTopology.Point.presheafFiberDesc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
              {P : CategoryTheory.Functor Cᵒᵖ A} →
                {T : A} →
                  (φ : (X : C) → Φ.fiber.obj X → (P.obj (Opposite.op X) ⟶ T)) →
                    autoParam
                        (∀ ⦃X Y : C⦄ (f : X ⟶ Y) (x : Φ.fiber.obj X),
                          CategoryTheory.CategoryStruct.comp (P.map f.op) (φ X x) =
                            φ Y ((CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f)) x))
                        _auto_48✝ →
                      (Φ.presheafFiber.obj P ⟶ T)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.toGraph_adj : ∀ {α : Type u_1} {V : Type u_2} {A : Matrix V V α} [inst : MulZeroOneClass α] [inst_1 : Nontrivial α]
  (h : A.IsAdjMatrix) (i j : V), h.toGraph.Adj i j = (A i j = 1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [Inhabited α] {k fallback : α} {f : Option β → Option β},
  (m.alter k f).getKeyD k fallback = if (f m[k]?).isSome = true then k else fallback
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.iff_dvd_total : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R], ValuationRing R ↔ Std.Total fun x1 x2 => x1 ∣ x2
-- Mathlib.Algebra.Order.Disjointed
disjointed_add_one : ∀ {α : Type u_1} {ι : Type u_2} [inst : GeneralizedBooleanAlgebra α] [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrderBot ι] [inst_3 : Add ι] [inst_4 : One ι] [SuccAddOrder ι] [NoMaxOrder ι] (f : ι → α)
  (i : ι), disjointed f (i + 1) = f (i + 1) \ (partialSups f) i
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonUnit : Lean.FromJson Unit
-- Mathlib.Algebra.Group.Subgroup.Map
MulEquiv.mapSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Type u_6} [inst_1 : Group H] (f : G ≃* H),
  f.mapSubgroup =
    { toFun := Subgroup.map ↑f, invFun := Subgroup.map ↑f.symm, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ShowDocumentClientCapabilities : Type
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The equivalence that exhibits `SimplexCategory` as skeleton
of `NonemptyFinLinOrd`  -/
SimplexCategory.skeletalEquivalence : SimplexCategory ≌ NonemptyFinLinOrd
-- Mathlib.MeasureTheory.Measure.OpenPos
MeasureTheory.Measure.isOpenPosMeasure_smul : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  {c : ENNReal}, c ≠ 0 → (c • μ).IsOpenPosMeasure
-- Mathlib.Analysis.ODE.Gronwall
gronwallBound_x0 : ∀ (δ K ε : ℝ), gronwallBound δ K ε 0 = δ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.diff_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ \ m₂).Equiv (m₁ \ m₃)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] (X Y : C)
  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m : M),
  CategoryTheory.Localization.HasSmallLocalizedHom W X ((CategoryTheory.shiftFunctor C m).obj Y)
-- Lean.Meta.Hint
/-- A code action suggestion associated with a hint in a message.

Refer to `TryThis.Suggestion`. This extends that structure with several fields specific to inline
hints.
 -/
Lean.Meta.Hint.Suggestion : Type
-- Init.GrindInstances.ToInt
Lean.Grind.instSubNatCiOfNatInt : Lean.Grind.ToInt.Sub ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
OpenPartialHomeomorph.subtypeRestr_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : TopologicalSpace.Opens X} (hs : Nonempty ↥s),
  (e.subtypeRestr hs).source = Subtype.val ⁻¹' e.source
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain.eq_1 : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (x : AddMonoidAlgebra R M),
  AddMonoidAlgebra.mapDomain f x = AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain f x.coeff)
-- Lean.Parser.Basic
Lean.Parser.setExpected : List String → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_of_two_le : ∀ {R : Type u_1} [inst : CommRing R] (k : ℕ) (a : R) {n : ℕ},
  2 ≤ n →
    Polynomial.dickson k a n =
      Polynomial.X * Polynomial.dickson k a (n - 1) - Polynomial.C a * Polynomial.dickson k a (n - 2)
-- Init.Data.UInt.Bitwise
UInt8.toUInt64_shiftLeft : ∀ (a b : UInt8), (a <<< b).toUInt64 = a.toUInt64 <<< (b % 8).toUInt64 % 256
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.hasPullback_of_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z), CategoryTheory.Limits.HasPullback g f
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The limit cone.  -/
LightDiagram.cone : (self : LightDiagram) → CategoryTheory.Limits.Cone (self.diagram.comp FintypeCat.toProfinite)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.rotate.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α × List α → Sort u_2) (l₁ l₂ : List α) (h_1 : (l₁ l₂ : List α) → motive (l₁, l₂)),
  (match (l₁, l₂) with
    | (l₁, l₂) => h_1 l₁ l₂) =
    h_1 l₁ l₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.fin3_def_ext : ∀ {R : Type r} (a b c : R), ![a, b, c] 0 = a ∧ ![a, b, c] 1 = b ∧ ![a, b, c] 2 = c
-- Mathlib.Analysis.Real.Hyperreal
/-- A hyperreal number is infinitesimal if its standard part is 0.
**Do not use.** Write `0 < ArchimedeanClass.mk x` instead.  -/
Hyperreal.Infinitesimal : ℝ* → Prop
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.EAdj.inter_nonempty : ∀ {α : Type u_1} {e f : Set α} {H : Hypergraph α}, H.EAdj e f → (e ∩ f).Nonempty
-- Mathlib.RingTheory.Unramified.Field
Algebra.FormallyUnramified.isRadical_map_isMaximal : ∀ (A : Type u_2) [inst : CommRing A] (B : Type u_4) [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Algebra.EssFiniteType A B] [Algebra.FormallyUnramified A B] (p : Ideal A) [p.IsMaximal],
  (Ideal.map (algebraMap A B) p).IsRadical
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instCompleteSpace : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : UniformSpace K] [IsUniformAddGroup K]
  [IsNonarchimedeanLocalField K], CompleteSpace K
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_comp_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z),
  CategoryTheory.CartesianMonoidalCategory.lift
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z))
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.snd Y Z)) =
    f
-- Mathlib.RingTheory.Filtration
Ideal.stableFiltration_N : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (N : Submodule R M) (i : ℕ), (I.stableFiltration N).N i = I ^ i • N
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.rTensorEquivAlgEquiv.eq_1 : ∀ (R : Type u_1) {M : Type u_2} (S : Type u_4) (A : Type u_5) (B : Type u_6) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : AddCommMonoid M],
  AddMonoidAlgebra.rTensorEquivAlgEquiv R S A B =
    AlgEquiv.restrictScalars S
      (AlgEquiv.ofAlgHom
        (Algebra.TensorProduct.lift
          ((IsScalarTower.toAlgHom A (TensorProduct R A B) (AddMonoidAlgebra (TensorProduct R A B) M)).comp
            Algebra.TensorProduct.includeLeft)
          (AddMonoidAlgebra.mapAlgHom M Algebra.TensorProduct.includeRight) ⋯)
        AddMonoidAlgebra.rTensorEquivAlgEquiv.invFun ⋯ ⋯)
-- Mathlib.Data.ENNReal.Basic
ENNReal.natCast_lt_top : ∀ (n : ℕ), ↑n < ⊤
-- Mathlib.NumberTheory.Primorial
primorial_one : primorial 1 = 1
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
Nat.doubleFactorial.eq_3 : ∀ (k : ℕ), k.succ.succ.doubleFactorial = (k + 2) * k.doubleFactorial
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
/-- The action of `SL(2, ℝ)` on `ℍ` is jointly continuous.  -/
UpperHalfPlane.instContinuousSMulSL2R : ContinuousSMul (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane
-- Mathlib.Analysis.Normed.Group.Defs
ENormedAddMonoid.enorm_eq_zero : ∀ {E : Type u_8} {inst : TopologicalSpace E} [self : ENormedAddMonoid E] (x : E), ‖x‖ₑ = 0 ↔ x = 0
-- Mathlib.Data.List.Cycle
List.next_getLast_eq_head : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (h : l ≠ []), l.Nodup → l.next (l.getLast h) ⋯ = l.head h
-- Init.Meta.Defs
Lean.Meta.Omega.OmegaConfig.mk : Bool → Bool → Bool → Bool → Lean.Meta.Omega.OmegaConfig
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_maxKey?_modify_eq_isSome : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β}, (t.modify k f).maxKey?.isSome = t.maxKey?.isSome
-- Lean.Data.Lsp.Utf16
Lean.String.codepointPosToUtf16Pos : String → ℕ → ℕ
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.equivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.ULift.equivalence.functor = CategoryTheory.ULift.upFunctor
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Construct a bundled `MonCat` from the underlying type and typeclass.  -/
MonCat.of : (M : Type u) → [Monoid M] → MonCat
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.lt_slope_of_hasDerivWithinAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivWithinAt f f' S y → f' < slope f x y
-- Init.Data.SInt.Lemmas
Int16.toBitVec_div : ∀ {a b : Int16}, (a / b).toBitVec = a.toBitVec.sdiv b.toBitVec
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.not_bddBelow_of_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder β] {l : Filter α} [l.NeBot] {f : α → β} [NoMinOrder β],
  Filter.Tendsto f l Filter.atBot → ¬BddBelow (Set.range f)
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is of the form `Nat`  -/
Lean.Meta.Grind.Arith.isNatType : Lean.Expr → Bool
-- Lean.Elab.Term.TermElabM
/-- Execute `x` without heeding the `elab_as_elim` attribute. Useful when there is
no expected type (so `elabAppArgs` would fail), but expect that the user wants
to use such constants.
 -/
Lean.Elab.Term.withoutHeedElabAsElim : {m : Type → Type u_1} → {α : Type} → [MonadFunctorT Lean.Elab.TermElabM m] → m α → m α
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
_private.Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree.0.WeierstrassCurve.natDegree_coeff_ΨSq_ofNat : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ),
  (W.ΨSq ↑n).natDegree ≤ n ^ 2 - 1 ∧ (W.ΨSq ↑n).coeff (n ^ 2 - 1) = ↑(↑n ^ 2)
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.NullMeasurableSet.const_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {s : Set E},
  MeasureTheory.NullMeasurableSet s μ → ∀ (r : ℝ), MeasureTheory.NullMeasurableSet (r • s) μ
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_dvd_tdiv : ∀ {a b c : ℤ}, a ∣ b → b ∣ c → b.tdiv a ∣ c.tdiv a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Unsigned Less Than
 -/
Std.Tactic.BVDecide.BVBinPred.ult : Std.Tactic.BVDecide.BVBinPred
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.forInUncurried_eq_forIn_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Monad m] [LawfulMonad m] {f : α × β → δ → m (ForInStep δ)}
  {init : δ}, Std.DTreeMap.Raw.Const.forInUncurried f init t = forIn (Std.DTreeMap.Raw.Const.toArray t) init f
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.mk.injEq : ∀ {G : Type u_1} [inst : CommGroup G] (toSubmonoid : Submonoid G)
  (eq_one_of_mem_of_inv_mem' : ∀ {a : G}, a ∈ toSubmonoid.carrier → a⁻¹ ∈ toSubmonoid.carrier → a = 1)
  (toSubmonoid_1 : Submonoid G)
  (eq_one_of_mem_of_inv_mem'_1 : ∀ {a : G}, a ∈ toSubmonoid_1.carrier → a⁻¹ ∈ toSubmonoid_1.carrier → a = 1),
  ({ toSubmonoid := toSubmonoid, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem' } =
      { toSubmonoid := toSubmonoid_1, eq_one_of_mem_of_inv_mem' := eq_one_of_mem_of_inv_mem'_1 }) =
    (toSubmonoid = toSubmonoid_1)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- If `k` is algebraically closed, then every nonconstant polynomial has a root.
 -/
IsAlgClosed.exists_root : ∀ {k : Type u} [inst : Field k] [IsAlgClosed k] (p : Polynomial k), p.degree ≠ 0 → ∃ x, p.IsRoot x
-- Mathlib.Data.Set.Card
Set.BijOn.ncard_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {t : Set β}, Set.BijOn f s t → s.ncard = t.ncard
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.transpose_eq_iff : ∀ {μ ν : YoungDiagram}, μ.transpose = ν.transpose ↔ μ = ν
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.instIsHomLiftIdObj : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) (a : 𝒳),
  p.IsHomLift (CategoryTheory.CategoryStruct.id (p.obj a)) (CategoryTheory.CategoryStruct.id a)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_sub_ofNat : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  [inst_4 : Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R) (n : ℕ) [inst_7 : n.AtLeastTwo],
  ⌊a - OfNat.ofNat n⌋₊ = ⌊a⌋₊ - OfNat.ofNat n
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_zero_ratCast : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : Zero R] [inst_3 : RatCast R]
  (q : ℚ), (HahnSeries.single 0) ↑q = ↑q
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.pairwise_toList_le : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [LT α] [inst_3 : Std.PRange.UpwardEnumerable α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_6 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => a ≤ b) r.toList
-- Batteries.Data.Vector.Basic
Vector.uset.congr_simp : ∀ {α : Type u_1} {n : ℕ} (xs xs_1 : Vector α n),
  xs = xs_1 →
    ∀ (i i_1 : USize) (e_i : i = i_1) (v v_1 : α), v = v_1 → ∀ (h : i.toNat < n), xs.uset i v h = xs_1.uset i_1 v_1 ⋯
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.antidiagonalOfLocallyFinite.eq_1 : ∀ {A : Type u_2} [inst : AddCommMonoid A] [inst_1 : PartialOrder A] [inst_2 : CanonicallyOrderedAdd A]
  [inst_3 : LocallyFiniteOrderBot A] [inst_4 : DecidableEq A],
  Finset.HasAntidiagonal.antidiagonalOfLocallyFinite =
    { antidiagonal := fun n => {uv ∈ Finset.Iic n ×ˢ Finset.Iic n | uv.1 + uv.2 = n}, mem_antidiagonal := ⋯ }
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- Isomorphic monoids have isomorphic monoid algebras.  -/
MonoidAlgebra.domCongrBialgEquiv : (R : Type u_1) →
  (A : Type u_3) →
    {M : Type u_8} →
      {N : Type u_9} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Bialgebra R A] →
              [inst_3 : Monoid M] → [inst_4 : Monoid N] → M ≃* N → MonoidAlgebra A M ≃ₐc[R] MonoidAlgebra A N
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instAddCommMonoid.eq_1 : ∀ {A : Type u_2} {E : Type u_6} [inst : AddMonoid A] [inst_1 : TopologicalSpace A] [inst_2 : AddCommMonoid E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E],
  ContinuousAddMonoidHom.instAddCommMonoid =
    { add := fun f g => (ContinuousAddMonoidHom.add E).comp (f.prod g), add_assoc := ⋯,
      toZero := ContinuousAddMonoidHom.instZero A E, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto,
      nsmul_zero := ⋯, nsmul_succ := ⋯, add_comm := ⋯ }