mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Characterizing the forward direction of the associator isomorphism
with respect to the unit transformations.  -/
CategoryTheory.MonoidalCategory.DayConvolution.associator_hom_unit_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  (H : CategoryTheory.Functor C V) [inst_5 : CategoryTheory.MonoidalCategory.DayConvolution G H]
  [inst_6 :
    CategoryTheory.MonoidalCategory.DayConvolution F (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)]
  [inst_7 :
    CategoryTheory.MonoidalCategory.DayConvolution (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H]
  [inst_8 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_9 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  (x y z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y)) (H.obj z))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.unit
              (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G) H).app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y, z))
        ((CategoryTheory.MonoidalCategory.DayConvolution.associator F G H).hom.app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) z))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj x) ((G, H).1.obj (y, z).1) ((G, H).2.obj (y, z).2)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x)
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit G H).app (y, z)))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit F
                (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).app
            (x, CategoryTheory.MonoidalCategoryStruct.tensorObj y z))
          ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F
                (CategoryTheory.MonoidalCategory.DayConvolution.convolution G H)).map
            (CategoryTheory.MonoidalCategoryStruct.associator (x, CategoryTheory.MonoidalCategoryStruct.tensorObj y z).1
                y z).inv)))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_sub_right : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α}, t.Nonempty → s.card ≤ (s - t).card
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instDecidableMem : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → {m : Std.HashSet.Raw α} → {a : α} → Decidable (a ∈ m)
-- Mathlib.Tactic.Ring.Common
/-- Equality test for expressions. This is not a `BEq` instance because it is heterogeneous.  -/
Mathlib.Tactic.Ring.Common.ExBase.eq : Mathlib.Tactic.Ring.Common.RingCompare Mathlib.Tactic.Ring.Common.btℕ →
  {u : Lean.Level} →
    {α : Q(Type u)} →
      {bt : Q(«$α») → Type} →
        {sα : Q(CommSemiring «$α»)} →
          Mathlib.Tactic.Ring.Common.RingCompare bt →
            {a b : Q(«$α»)} →
              Mathlib.Tactic.Ring.Common.ExBase bt sα a → Mathlib.Tactic.Ring.Common.ExBase bt sα b → Bool
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.symm_trans : ∀ {R : Type u_4} {S : Type u_5} {S' : Type u_6} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S]
  [inst_4 : Mul S'] [inst_5 : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S'), (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.mk.injEq : ∀ (symm : Bool) (proof type : Lean.Expr) (index : Lean.HeadIndex × ℕ)
  (mvarIds : Array (Lean.MVarId × Array Lean.LocalDecl)) (symm_1 : Bool) (proof_1 type_1 : Lean.Expr)
  (index_1 : Lean.HeadIndex × ℕ) (mvarIds_1 : Array (Lean.MVarId × Array Lean.LocalDecl)),
  ({ symm := symm, proof := proof, type := type, index := index, mvarIds := mvarIds } =
      { symm := symm_1, proof := proof_1, type := type_1, index := index_1, mvarIds := mvarIds_1 }) =
    (symm = symm_1 ∧ proof = proof_1 ∧ type = type_1 ∧ index = index_1 ∧ mvarIds = mvarIds_1)
-- Mathlib.Topology.Connected.Basic
Continuous.mapsTo_connectedComponent : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → ∀ (a : α), Set.MapsTo f (connectedComponent a) (connectedComponent (f a))
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The underlying topological space of `Proj`  -/
_private.Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme.0.AlgebraicGeometry.«termProj.T» : Lean.ParserDescr
-- Lean.Compiler.Specialize
/-- Marks a definition to always be specialized during code generation.

Specialization is an optimization in the code generator for generating variants of a function that
are specialized to specific parameter values. This is in particular useful for functions that take
other functions as parameters: Usually when passing functions as parameters, a closure needs to be
allocated that will then be called. Using `@[specialize]` prevents both of these operations by
using the provided function directly in the specialization of the inner function.

`@[specialize]` can take additional arguments for the parameter names or indices (starting at 1) of
the parameters that should be specialized. By default, instance and function parameters are
specialized.
 -/
Lean.Compiler.specializeAttr : Lean.ParametricAttribute (Array ℕ)
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.avgRisk_zero_right : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) (π : MeasureTheory.Measure Θ),
  ProbabilityTheory.avgRisk ℓ P 0 π = 0
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_C_mul_X_subset : ∀ {R : Type u} [inst : Semiring R] (c : R), (Polynomial.C c * Polynomial.X).support ⊆ {1}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k fallback : α}, (Std.ExtTreeMap.map f t).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.sylvester_map_map : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f g : Polynomial R) (m n : ℕ) (φ : R →+* S),
  (Polynomial.map φ f).sylvester (Polynomial.map φ g) m n = φ.mapMatrix (f.sylvester g m n)
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackZeroZeroIso X Y).inv
      (CategoryTheory.Limits.pullback.fst 0 0) =
    CategoryTheory.Limits.prod.fst
-- Init.Grind.Interactive
/-- `any_goals tac` applies the tactic `tac` to every goal,
concatenating the resulting goals for successful tactic applications.
If the tactic fails on all of the goals, the entire `any_goals` tactic fails.

This tactic is like `all_goals try tac` except that it fails if none of the applications of `tac` succeeds.
 -/
Lean.Parser.Tactic.Grind.anyGoals : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instIsUniformAddGroup : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : UniformSpace F]
  [inst_7 : IsUniformAddGroup F], IsUniformAddGroup (ContinuousMultilinearMap 𝕜 E F)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalStringExprCore : Lean.Expr → Lean.MetaM String
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.loopWf_eq : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] [LawfulMonad n] (γ : Type u) {lift : (γ δ : Type u) → (γ → n δ) → Id γ → n δ}
  [instLawfulMonadLiftFunction : Std.Internal.LawfulMonadLiftBindFunction lift] (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxi.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (acc : γ) (next : α)
  (h : LargeEnough next) (f : (out : α) → LargeEnough out → (c : γ) → n { s // Pl out c s }),
  Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc next h f = do
    let __do_lift ← f next h acc
    match __do_lift with
      | ⟨ForInStep.yield acc', property⟩ =>
        Std.IterM.DefaultConsumers.forIn' lift γ Pl { internalState := { next := Std.PRange.succ? next } } acc'
          { internalState := { next := Std.PRange.succ? next } }.IsPlausibleIndirectOutput ⋯ fun next' h_1 acc' =>
          f next' ⋯ acc'
      | ⟨ForInStep.done acc', property⟩ => pure acc'
-- Mathlib.Order.SuccPred.Archimedean
Pred.rec_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] [IsPredArchimedean α] (p : α → Prop),
  p ⊤ → (∀ (a : α), p a → p (Order.pred a)) → ∀ (a : α), p a
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Let `f` be a measurable function integrable on `a..b`. The function `(u, v) ↦ ∫ x in u..v, f x`
has derivative `(u, v) ↦ v • f b - u • f a` within `s × t` at `(a, b)`, where
`s ∈ {Iic a, {a}, Ici a, univ}` and `t ∈ {Iic b, {b}, Ici b, univ}` provided that `f` tends to
`f a` and `f b` at the filters `la` and `lb` from the following table. In most cases this assumption
is definitionally equal `ContinuousAt f _` or `ContinuousWithinAt f _ _`.

| `s`     | `la`     | `t`     | `lb`     |
| ------- | ----     | ---     | ----     |
| `Iic a` | `𝓝[≤] a` | `Iic b` | `𝓝[≤] b` |
| `Ici a` | `𝓝[>] a` | `Ici b` | `𝓝[>] b` |
| `{a}`   | `⊥`      | `{b}`   | `⊥`      |
| `univ`  | `𝓝 a`    | `univ`  | `𝓝 b`    |
 -/
intervalIntegral.integral_hasFDerivWithinAt : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E}
  {la lb : Filter ℝ} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f la MeasureTheory.volume →
      StronglyMeasurableAtFilter f lb MeasureTheory.volume →
        ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter a (nhdsWithin a s) la]
          [intervalIntegral.FTCFilter b (nhdsWithin b t) lb],
          Filter.Tendsto f la (nhds (f a)) →
            Filter.Tendsto f lb (nhds (f b)) →
              HasFDerivWithinAt (fun p => ∫ (x : ℝ) in p.1..p.2, f x)
                ((ContinuousLinearMap.snd ℝ ℝ ℝ).smulRight (f b) - (ContinuousLinearMap.fst ℝ ℝ ℝ).smulRight (f a))
                (s ×ˢ t) (a, b)
-- Init.Data.Int.Pow
Int.pow_nonneg : ∀ {n : ℤ} {m : ℕ}, 0 ≤ n → 0 ≤ n ^ m
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → k ∉ t₁ \ t₂
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intAdicAbv_eq_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b) (r : R), (v.intAdicAbv hb) r = 1 ↔ r ∉ v.asIdeal
-- Mathlib.Geometry.Manifold.Notation
/-- `MDiffAt f x` elaborates to `MDifferentiableAt I J f x`,
trying to determine `I` and `J` from the local context.
The argument `x` can be omitted.  -/
Manifold.termMDiffAt__ : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Ray
SameRay.of_subsingleton : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Subsingleton M] (x y : M), SameRay R x y
-- Mathlib.Analysis.Convex.Topology
Convex.nhdsWithin_sdiff_eq_nhdsGT : ∀ {𝕜 : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜},
  Convex 𝕜 s →
    ∀ {a : 𝕜},
      a ∈ closure s → s ∩ Set.Iio a = ∅ → (s ∩ Set.Ioi a).Nonempty → nhdsWithin a (s \ {a}) = nhdsWithin a (Set.Ioi a)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.coe_lTensorHom : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P], ⇑(LinearMap.lTensorHom M) = LinearMap.lTensor M
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.ediam_image : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (s : Set E), Metric.ediam (⇑f '' s) = Metric.ediam s
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.MemLp.prodLp_snd : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => (f x).snd) p μ
-- Mathlib.Analysis.Normed.Group.Real
Real.enorm_abs : ∀ (r : ℝ), ‖|r|‖ₑ = ‖r‖ₑ
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A convex cone is blunt if it doesn't include `0`.  -/
ConvexCone.Blunt : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → ConvexCone R M → Prop
-- Mathlib.Order.Bounds.Basic
/-- In a codirected order, the union of bounded below sets is bounded below.  -/
BddBelow.union : ∀ {α : Type u_1} [inst : Preorder α] [IsCodirectedOrder α] {s t : Set α}, BddBelow s → BddBelow t → BddBelow (s ∪ t)
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.instIsStableUnderCompositionQcPrecoverage : AlgebraicGeometry.Scheme.qcPrecoverage.IsStableUnderComposition
-- Mathlib.Order.CompleteLattice.Defs
/-- In a linearly ordered type, we assume the order relations are all decidable.  -/
CompleteLinearOrder.toDecidableLT : {α : Type u_8} → [self : CompleteLinearOrder α] → DecidableLT α
-- Mathlib.Data.Finset.Grade
CovBy.card_multiset : ∀ {α : Type u_1} {s t : Multiset α}, s ⋖ t → s.card ⋖ t.card
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_inter_le' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrderBot α] {s t : Set α},
  autoParam (BddAbove s) csSup_inter_le'._auto_1 →
    autoParam (BddAbove t) csSup_inter_le'._auto_3 → sSup (s ∩ t) ≤ min (sSup s) (sSup t)
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageMetaData.notification : String → Lean.JsonRpc.MessageMetaData
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxView.induct : ∀ {α : Type u} {β : α → Type v}
  (motive :
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced → r.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Prop),
  (∀ (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced)
      (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size Std.DTreeMap.Internal.Impl.leaf.size),
      motive k v l Std.DTreeMap.Internal.Impl.leaf hl hr hlr) →
    (∀ (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (size : ℕ) (k' : α) (v' : β k')
        (l' r' : Std.DTreeMap.Internal.Impl α β) (hr : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
        (hlr :
          Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size)
        (dk : α) (dv : β dk) (dt : Std.DTreeMap.Internal.Impl α β) (hdt : dt.Balanced)
        (hdt' : dt.size = l'.size + r'.size),
        Std.DTreeMap.Internal.Impl.maxView k' v' l' r' ⋯ ⋯ ⋯ =
            { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } →
          motive k' v' l' r' ⋯ ⋯ ⋯ → motive k v l (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hr hlr) →
      ∀ (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced) (hr : r.Balanced)
        (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size), motive k v l r hl hr hlr
-- Init.Data.BitVec.Bootstrap
BitVec.toNat_ofBool : ∀ (b : Bool), (BitVec.ofBool b).toNat = b.toNat
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.next_stop : ∀ {l m r : List Char} {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → s.next { byteIdx := String.utf8Len m } = { byteIdx := String.utf8Len m }
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_natCast : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ), ‖↑n‖ = ↑n
-- Std.Data.HashMap.Basic
Std.HashMap.mk.inj : ∀ {α : Type u} {β : Type v} {inst : BEq α} {inst_1 : Hashable α} {inner inner_1 : Std.DHashMap α fun x => β},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x : W'.CoordinateRing),
  ∃ p q, p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W') Polynomial.X = x
-- Mathlib.Analysis.Normed.Algebra.Spectrum
_private.Mathlib.Analysis.Normed.Algebra.Spectrum.0.spectrum.«term↑ₐ_1» : Lean.ParserDescr
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.unzero_lt_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithZero α} {b : α} (hx : x ≠ 0), WithZero.unzero hx < b ↔ x < ↑b
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.stalk_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] [inst_1 : CategoryTheory.Limits.HasColimits C]
  (x : ↑↑X.toPresheafedSpace), CategoryTheory.IsIso (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f.hom x)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.getSimpCongrTheorems : Lean.CoreM Lean.Meta.SimpCongrTheorems
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getValue.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a : α) (l : List ((_ : α) × β))
  (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValue a l h = (Std.Internal.List.getValue? a l).get ⋯
-- Mathlib.Topology.Order
coinduced_compose : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [tα : TopologicalSpace α] {f : α → β} {g : β → γ},
  TopologicalSpace.coinduced g (TopologicalSpace.coinduced f tα) = TopologicalSpace.coinduced (g ∘ f) tα
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeRightOpOfCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ C} (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.coconeRightOpOfCone c = { pt := Opposite.op c.pt, ι := CategoryTheory.NatTrans.rightOp c.π }
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Top α] [inst_2 : Min β] [inst_3 : Top β]
  [inst_4 : Min γ] [inst_5 : Top γ] {g₁ g₂ : InfTopHom β γ} {f : InfTopHom α β},
  Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_iUnion_le_sum_mk_lift : ∀ {α : Type u} {ι : Type v} {f : ι → Set α},
  Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ i, f i)) ≤ Cardinal.sum fun i => Cardinal.mk ↑(f i)
-- Init.Data.BitVec.Lemmas
BitVec.lt_allOnes_iff : ∀ {w : ℕ} {x : BitVec w}, x < BitVec.allOnes w ↔ x ≠ BitVec.allOnes w
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.blocksFun.eq_1 : ∀ {n : ℕ} (c : Composition n), c.blocksFun = c.blocks.get
-- Mathlib.RingTheory.DedekindDomain.Different
conductor_mul_differentIdeal : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [IsScalarTower A K L] [IsScalarTower A B L] [inst_11 : IsDomain A] [IsFractionRing A K]
  [FiniteDimensional K L] [Algebra.IsSeparable K L] [IsIntegralClosure B A L] [IsIntegrallyClosed A]
  [inst_17 : IsDedekindDomain B] [inst_18 : Module.IsTorsionFree A B] (x : B),
  K[(algebraMap B L) x] = ⊤ →
    conductor A x * differentIdeal A B = Ideal.span {(Polynomial.aeval x) (Polynomial.derivative (minpoly A x))}
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst_2 : Inhabited α], t ≠ ∅ → ∀ {km : α}, t.max! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Algebra.Quandle
Rack.op_invAct_op_eq : ∀ {R : Type u_1} [inst : Rack R] {x y : R},
  Rack.invAct (MulOpposite.op x) (MulOpposite.op y) = MulOpposite.op (Shelf.act x y)
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.modEq_digits_sum : ∀ (b b' : ℕ), b' % b = 1 → ∀ (n : ℕ), n ≡ (b'.digits n).sum [MOD b]
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.go.eq_def : ∀ (acc s : String) (a : List String),
  String.intercalate.go✝ acc s a =
    match a with
    | a :: as => String.intercalate.go✝ (acc ++ s ++ a) s as
    | [] => acc
-- Aesop.Tree.State
Aesop.Goal.isUnprovableNoCache : Aesop.Goal → BaseIO Bool
-- Init.Data.Array.Find
Array.findSome?_empty : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1}, Array.findSome? f #[] = none
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceBmod : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPair.one : CategoryTheory.Limits.WalkingParallelPair
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite : ∀ {α : Type u_1} {G : SimpleGraph α} {r : ℕ} [inst : DecidableEq α],
  Maximal (fun H => H.CliqueFree (r + 2)) G →
    ¬G.IsCompleteMultipartite → ∃ v w₁ w₂ s t, G.IsFiveWheelLike r (s ∩ t).card v w₁ w₂ s t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insert!_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {kmi : α},
  (Std.DTreeMap.Internal.Impl.insert! k v t).minKey?.get ⋯ = kmi → (compare kmi k).isLE = true
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.antisymm : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H.IsSubgraph G → G.IsSubgraph H → H = G