mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instAddGroupWithOne : {R : Type u_1} → [AddGroupWithOne R] → AddGroupWithOne (Lex R)
-- Mathlib.ModelTheory.Definability
/-- A subset of a finite Cartesian product of a structure is definable over a set `A` when
membership in the set is given by a first-order formula with parameters from `A`.  -/
Set.Definable : {M : Type w} → Set M → (L : FirstOrder.Language) → [L.Structure M] → {α : Type u₁} → Set (α → M) → Prop
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ofList_eq_foldl : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)}, Std.ExtHashMap.ofList l = List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfEquivalence.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasLimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasLimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F),
  CategoryTheory.Limits.HasLimit.isoOfEquivalence e w =
    (CategoryTheory.Limits.limit.isLimit F).conePointsIsoOfEquivalence (CategoryTheory.Limits.limit.isLimit G) e w
-- Std.Time.Time.PlainTime
/-- Adds nanoseconds to a `PlainTime`.
 -/
Std.Time.PlainTime.addNanoseconds : Std.Time.PlainTime → Std.Time.Nanosecond.Offset → Std.Time.PlainTime
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.findSomeM?_pure : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  [inst_2 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.Iterators.Finite α m] [Std.LawfulIteratorLoop α m m]
  {it : Std.IterM m β} {f : β → Option γ}, (it.findSomeM? fun x => pure (f x)) = it.findSome? f
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.image_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (f : P₁ ≃ᴬ[k] P₂) (s : Set P₂), ⇑f.symm '' s = ⇑f ⁻¹' s
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.add_iUnion₂ : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Add α] (s : Set α) (t : (i : ι) → κ i → Set α),
  s + ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s + t i j
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.mapDart_apply : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (d : G.Dart),
  f.mapDart d = { toProd := Prod.map (⇑f) (⇑f) d.toProd, adj := ⋯ }
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  {F : Type u_6} [inst_7 : FunLike F A B] [inst_8 : BialgHomClass F R A B] (f : F), ⇑↑f = ⇑f
-- Mathlib.Analysis.Complex.Basic
RCLike.hasSum_conj : ∀ {α : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] {L : SummationFilter α} {f : α → 𝕜} {x : 𝕜},
  HasSum (fun x => (starRingEnd 𝕜) (f x)) x L ↔ HasSum f ((starRingEnd 𝕜) x) L
-- Mathlib.Combinatorics.Matroid.Loop
/-- A version of `Matroid.isColoop_iff_forall_mem_closure_iff_mem` where we only quantify
over subsets of the ground set.  -/
Matroid.isColoop_iff_forall_mem_closure_iff_mem' : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e ↔ (∀ X ⊆ M.E, e ∈ M.closure X ↔ e ∈ X) ∧ e ∈ M.E
-- Mathlib.RingTheory.Flat.Basic
/-- If `M` is a flat module, then `𝟙 M ⊗ f` is injective for all injective linear maps `f`.  -/
Module.Flat.lTensor_preserves_injective_linearMap : ∀ {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] [Module.Flat R M] (f : N →ₗ[R] P),
  Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.mk_zero : Complex.UnitDisc.mk 0 Complex.UnitDisc.mk_zero._proof_1 = 0
-- Lean.Server.FileSource
Lean.Lsp.instFileSourceRpcReleaseParams : Lean.Lsp.FileSource Lean.Lsp.RpcReleaseParams
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.map_ofComp_ker : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι),
  Ideal.map (Q.ofComp P).toAlgHom (Q.comp P).ker = Q.ker
-- Mathlib.Data.List.Map2
List.zipLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, List.zipLeft = List.zipWithLeft Prod.mk
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.coeff_rename_eq_zero : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ),
  (∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → MvPolynomial.coeff u φ = 0) →
    MvPolynomial.coeff d ((MvPolynomial.rename f) φ) = 0
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cone `t` on `F` is a limit cone if each cone on `F` admits a unique
cone morphism to `t`.  -/
CategoryTheory.Limits.IsLimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cone F → Type (max (max u₁ u₃) v₃)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.prod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {γ : Type u_5} {δ : Type u_6} [inst : VAdd M α] [inst_1 : VAdd N γ]
  [inst_2 : VAdd N δ] {σ : M → N} (f : α →ₑ[σ] γ) (g : α →ₑ[σ] δ),
  f.prod g = { toFun := fun x => (f x, g x), map_vadd' := ⋯ }
-- Init.Data.Vector.MapIdx
Vector.mapIdx_eq_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Vector α 1} {f : ℕ → α → β} {b : β},
  Vector.mapIdx f xs = #v[b] ↔ ∃ a, xs = #v[a] ∧ f 0 a = b
-- Mathlib.Data.Multiset.MapFold
Multiset.sub_eq_fold_erase : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s - t = Multiset.foldl Multiset.erase s t
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.continuous_fderiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiff 𝕜 n f → n ≠ 0 → Continuous (fderiv 𝕜 f)
-- Mathlib.Control.Traversable.Basic
/-- An axiom for `traverse` involving `pure : β → Id β`.  -/
LawfulTraversable.traverse_eq_map_id : ∀ {t : Type u → Type u} {inst : Traversable t} [self : LawfulTraversable t] {α β : Type u} (f : α → β) (x : t α),
  traverse (pure ∘ f) x = pure (f <$> x)
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.lift.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {α : Type u_2} (f : M → α)
  (h : ∀ (a b : M), MulArchimedeanClass.mk a = MulArchimedeanClass.mk b → f a = f b),
  MulArchimedeanClass.lift f h = Quotient.lift f ⋯
-- Init.Data.List.ToArray
Array.sum.eq_1 : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] (as : Array α), as.sum = Array.foldr (fun x1 x2 => x1 + x2) 0 as
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_uSizeToNat : ∀ (n : USize), UInt64.ofNatLT n.toNat ⋯ = n.toUInt64
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.generalizeMatchDiscrs.withNewAltEqs.go : Array Lean.Expr →
  (Array Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr) →
    Array Lean.Expr → ℕ → Array Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesAt.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G}
  {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G},
  HasFPowerSeriesAt f p e → HasFPowerSeriesAt g q e → HasFPowerSeriesAt (fun x => (f x, g x)) (p.prod q) e
-- Mathlib.GroupTheory.Nilpotent
Group.nilpotencyClass_def : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G], Group.nilpotencyClass G = Nat.find ⋯
-- Init.Data.BitVec.Lemmas
BitVec.srem_one : ∀ {w : ℕ} {x : BitVec w}, x.srem 1#w = 0#w
-- Init.Data.Array.Erase
Array.erase_replicate : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a b : α},
  (Array.replicate n a).erase b = if (b == a) = true then Array.replicate (n - 1) a else Array.replicate n a
-- Std.Http.Data.URI.Encoding
/-- Encodes a raw string into an encoded path segment.
 -/
Std.Http.URI.EncodedSegment.encode : String → Std.Http.URI.EncodedSegment
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_lt_im`. -/
Complex.frontier_setOf_lt_im : ∀ (a : ℝ), frontier {z | a < z.im} = {z | z.im = a}
-- Mathlib.Topology.Order.LiminfLimsup
/-- The `liminf` of a function `u` along a filter `f` is a cluster point of `u` along `f`.  -/
MapClusterPt.liminf : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] {u : β → α} {f : Filter β} [f.NeBot],
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f u) MapClusterPt.liminf._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) MapClusterPt.liminf._auto_3 →
      MapClusterPt (Filter.liminf u f) f u
-- Mathlib.Order.Circular
/-- The strict betweenness relation obtained from "looping around" `<`.
See note [reducible non-instances].  -/
LT.toSBtw : (α : Type u_1) → [LT α] → SBtw α
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.inseparable_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable ↑x ↑y ↔ Inseparable x y
-- Mathlib.Topology.Specialization
Specialization.toEquiv_symm : ∀ {α : Type u_1}, Specialization.toEquiv.symm = Specialization.ofEquiv
-- Mathlib.Algebra.Quaternion
Quaternion.coe_pow : ∀ {R : Type u_3} [inst : CommRing R] (x : R) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_one : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), Polynomial.reflect n 1 = Polynomial.X ^ n
-- Mathlib.Data.Sym.Basic
Sym.exists_eq_cons_of_succ : ∀ {α : Type u_1} {n : ℕ} (s : Sym α n.succ), ∃ a s', s = a ::ₛ s'
-- Mathlib.Algebra.Group.Hom.Basic
/-- A homomorphism from a group to a monoid is injective iff its kernel is trivial.
For the iff statement on the triviality of the kernel, see `injective_iff_map_eq_one'`.  -/
injective_iff_map_eq_one : ∀ {F : Type u_7} {G : Type u_8} {H : Type u_9} [inst : Group G] [inst_1 : MulOneClass H] [inst_2 : FunLike F G H]
  [MonoidHomClass F G H] (f : F), Function.Injective ⇑f ↔ ∀ (a : G), f a = 1 → a = 1
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instInhabited.eq_1 : ∀ (M : Type u_4) [inst : AddZero M], AddMonoid.End.instInhabited M = { default := 1 }
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_equivariantMap.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (s : Set α),
  SubAddAction.ofFixingAddSubgroup_equivariantMap M s = { toFun := fun x => ↑x, map_vadd' := ⋯ }
-- Mathlib.Topology.EMetricSpace.Basic
EMetric.inseparable_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α}, Inseparable x y ↔ edist x y = 0
-- Mathlib.Order.Interval.Basic
NonemptyInterval.setLike : {α : Type u_1} → [inst : PartialOrder α] → SetLike (NonemptyInterval α) α
-- Mathlib.Algebra.Order.GroupWithZero.Basic
monotone_mul_left_of_nonneg : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : Preorder M₀] {a : M₀} [PosMulMono M₀],
  0 ≤ a → Monotone fun x => a * x
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.ofGoalRef : Aesop.GoalRef → BaseIO Aesop.BestFirstQueue.ActiveGoal
-- Mathlib.Data.Set.Lattice
Set.iInf_eq_dif : ∀ {α : Type u_1} {p : Prop} [inst : Decidable p] (s : p → Set α), ⋂ (h : p), s h = if h : p then s h else Set.univ
-- Init.Data.List.Lemmas
List.forall_mem_iff_forall_getElem : ∀ {α : Type u_1} {P : α → Prop} {l : List α}, (∀ x ∈ l, P x) ↔ ∀ (i : ℕ) (hi : i < l.length), P l[i]
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.Equiv t₂ → t₁.getKeyD k fallback = t₂.getKeyD k fallback
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.liftRingHom_X : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {L : Type u_1} [inst_2 : Field L] (φ : Polynomial K →+* L)
  (hφ : nonZeroDivisors (Polynomial K) ≤ Submonoid.comap φ (nonZeroDivisors L)),
  (RatFunc.liftRingHom φ hφ) RatFunc.X = φ Polynomial.X
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.image_of_monotone_on : ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {r' : β → β → Prop} {f : α → β} {s : Set α},
  s.PartiallyWellOrderedOn r → (∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)) → (f '' s).PartiallyWellOrderedOn r'
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddRightInvariant.comap : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] {H : Type u_3} [inst_3 : AddGroup H]
  {mH : MeasurableSpace H} [MeasurableAdd H] (μ : MeasureTheory.Measure H) [μ.IsAddRightInvariant] {f : G →+ H},
  MeasurableEmbedding ⇑f → (MeasureTheory.Measure.comap (⇑f) μ).IsAddRightInvariant
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α}, k ∈ t → t.getKey? k = some k
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E}, U ⟂ V → V ⟂ U
-- Mathlib.Data.Nat.Prime.Defs
Nat.coprime_of_dvd : ∀ {m n : ℕ}, (∀ (k : ℕ), Nat.Prime k → k ∣ m → ¬k ∣ n) → m.Coprime n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_map : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  {f : α → β → γ},
  Std.DTreeMap.Internal.Impl.Const.toArray (Std.DTreeMap.Internal.Impl.map f t) =
    Array.map (fun p => (p.1, f p.1 p.2)) (Std.DTreeMap.Internal.Impl.Const.toArray t)
-- Mathlib.Order.Circular
CircularPreorder.mk : {α : Type u_1} →
  [toBtw : Btw α] →
    [toSBtw : SBtw α] →
      (∀ (a : α), btw a a a) →
        (∀ {a b c : α}, btw a b c → btw b c a) →
          autoParam (∀ {a b c : α}, sbtw a b c ↔ btw a b c ∧ ¬btw c b a)
              CircularPreorder.sbtw_iff_btw_not_btw._autoParam →
            (∀ {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d c) → CircularPreorder α
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.lt_pred_iff : ∀ {α : Type u_1} {a b : α} [inst : PartialOrder α] [inst_1 : PredOrder α],
  Order.IsPredPrelimit b → (b < Order.pred a ↔ b < a)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSMul₂.toMeasurableSMul : ∀ {M : Type u_2} {X : Type u_3} [inst : MeasurableSpace X] [inst_1 : SMul M X] [inst_2 : MeasurableSpace M]
  [MeasurableSMul₂ M X], MeasurableSMul M X
-- Mathlib.Algebra.Order.Monoid.Lex
MonoidHom.inl_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  StrictMono ⇑(MonoidHom.inl α β)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
/-- Euclidean center of the circle with center `z` and radius `r` in the hyperbolic metric.  -/
UpperHalfPlane.center : UpperHalfPlane → ℝ → UpperHalfPlane
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [Inhabited α] {k k' : α} {f : β k → β k} {hc : k' ∈ t.modify k f},
  (t.modify k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.FindMin.WF.mk.sizeOf_spec : ∀ {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α} [inst : SizeOf α] (rank : ℕ)
  (before :
    ∀ {s : Batteries.BinomialHeap.Imp.Heap α},
      Batteries.BinomialHeap.Imp.Heap.WF le rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s))
  (node : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node rank)
  (next : Batteries.BinomialHeap.Imp.Heap.WF le (rank + 1) res.next),
  sizeOf { rank := rank, before := before, node := node, next := next } = 1 + sizeOf rank + sizeOf node + sizeOf next
-- Mathlib.Analysis.Normed.Operator.Mul
/-- Multiplication on the left in a non-unital normed algebra `R` as a non-unital algebra
homomorphism into the algebra of *continuous* linear maps. This is the left regular representation
of `A` acting on itself.

This has more algebraic structure than `ContinuousLinearMap.mul`, but there is no longer continuity
bundled in the first coordinate.  An alternative viewpoint is that this upgrades
`NonUnitalAlgHom.lmul` from a homomorphism into linear maps to a homomorphism into *continuous*
linear maps.  -/
NonUnitalAlgHom.Lmul : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    (R : Type u_3) →
      [inst_1 : NonUnitalSeminormedRing R] →
        [inst_2 : NormedSpace 𝕜 R] → [IsScalarTower 𝕜 R R] → [SMulCommClass 𝕜 R R] → R →ₙₐ[𝕜] R →L[𝕜] R
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.pow : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] [IsTopologicalRing S]
  [IsLinearTopology S S] (x : σ → S), MvPowerSeries.HasEval x → ∀ {p : ℕ}, 0 < p → MvPowerSeries.HasEval (x ^ p)
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.instFaithfulModuleCatLightCondensedDiscrete : ∀ (R : Type u) [inst : Ring R], (LightCondensed.discrete (ModuleCat R)).Faithful
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts.isClosedUnderColimitsOfShape : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P : CategoryTheory.ObjectProperty C}
  [self : P.IsClosedUnderFiniteCoproducts] (J : Type) [Finite J],
  P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete J)
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.v.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M),
  CliffordAlgebra.EquivEven.v Q = CliffordAlgebra.ι (CliffordAlgebra.EquivEven.Q' Q) ∘ₗ LinearMap.inl R M R
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α},
  (Std.ExtDHashMap.filter f m).getKey? k = (m.getKey? k).pfilter fun x_2 h' => f x_2 (m.get x_2 ⋯)
-- Mathlib.Order.Interval.Basic
Interval.coe_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ↑⊤ = Set.univ
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_inv_eq_one : ∀ {α : Type u} [inst : DivisionMonoid α] {a b : α}, IsUnit b → (a * b⁻¹ = 1 ↔ a = b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- In a category, given a morphism `f : A ⟶ B` and an object `X`,
this is the obvious pullback diagram:
```
A ⨯ X ⟶ A
  |     |
  v     v
B ⨯ X ⟶ B
```
 -/
CategoryTheory.IsPullback.of_prod_fst_with_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C} (f : A ⟶ B) (X : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct B X],
  CategoryTheory.IsPullback CategoryTheory.Limits.prod.fst
    (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id X)) f CategoryTheory.Limits.prod.fst
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.himp : {α : Type u_1} → [inst : HeytingAlgebra α] → HImp (Heyting.Regular α)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- The total variation of a signed measure.  -/
MeasureTheory.SignedMeasure.totalVariation : {α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α → MeasureTheory.Measure α
-- Lean.Elab.Term.TermElabM
/-- Elaborate `x` with `stx` on the macro stack  -/
Lean.Elab.Term.withPushMacroExpansionStack : {α : Type} → Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM α → Lean.Elab.TermElabM α
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.hom_ext_iff : ∀ {S : SSet.Truncated 2} {x y : SSet.OneTruncation₂ S} {f g : x ⟶ y}, f = g ↔ f.edge = g.edge
-- Mathlib.Topology.Sequences
compactSpace_iff_seqCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X],
  CompactSpace X ↔ SeqCompactSpace X
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.SharedState.mk.inj : ∀ {clientToServer serverToClient clientToServer_1 serverToClient_1 : Std.CloseableChannel ByteArray},
  { clientToServer := clientToServer, serverToClient := serverToClient } =
      { clientToServer := clientToServer_1, serverToClient := serverToClient_1 } →
    clientToServer = clientToServer_1 ∧ serverToClient = serverToClient_1
-- Mathlib.Data.ULift
ULift.map_surjective : ∀ {α : Type u} {β : Type v} {f : α → β}, Function.Surjective (ULift.map f) ↔ Function.Surjective f
-- Mathlib.Util.Superscript
_private.Mathlib.Util.Superscript.0.Mathlib.Tactic.Superscript.isValid.scripted : Lean.SyntaxNodeKind → Bool
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_mono_left : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → ∀ (s : Set α), μ s ≤ ν s
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- A version of the Bird determinant algorithm that is stated in terms of `Matrix`.  -/
BirdDet.Spec.birdDet : {R : Type u_1} → [CommRing R] → {n : ℕ} → Matrix (Fin n) (Fin n) R → R
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.pure_bindOnSupport : ∀ {α : Type u_1} {β : Type u_2} (a : α) (f : (a' : α) → a' ∈ (PMF.pure a).support → PMF β),
  (PMF.pure a).bindOnSupport f = f a ⋯
-- Mathlib.Algebra.Quaternion
Quaternion.normSq_def' : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R),
  Quaternion.normSq a = a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleSuccessorOf.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (it' it : Std.IterM m β),
  it'.IsPlausibleSuccessorOf it = ∃ step, step.successor = some it' ∧ it.IsPlausibleStep step
-- Mathlib.MeasureTheory.Function.JacobianOneDim
MeasureTheory.integrableOn_Icc_deriv_smul_iff_of_deriv_nonpos : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f f' : ℝ → ℝ} {a b : ℝ} {g : ℝ → F},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) →
      (∀ x ∈ Set.Ioo a b, f' x ≤ 0) →
        a ≤ b →
          (MeasureTheory.IntegrableOn (fun x => f' x • g (f x)) (Set.Icc a b) MeasureTheory.volume ↔
            MeasureTheory.IntegrableOn g (Set.Icc (f b) (f a)) MeasureTheory.volume)
-- Mathlib.Order.RelSeries
RelSeries.head_reverse : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.reverse.head = p.last
-- Mathlib.Logic.Function.Basic
Function.not_injective_const : ∀ {α : Type u_4} {β : Type u_5} [Nontrivial α] {b : β}, ¬Function.Injective fun x => b
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_uInt16ToBitVec : ∀ (n : UInt16), { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64
-- Mathlib.Order.Northcott
Northcott.exists_min_image : ∀ {α : Type u_1} {β : Type u_2} (h : α → β) [inst : LinearOrder β] [Northcott h] (s : Set α),
  s.Nonempty → ∃ a ∈ s, ∀ a' ∈ s, h a ≤ h a'
-- Mathlib.Algebra.Order.Monoid.Defs
instOrderedAddOfIsOrderedCancelAddMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α],
  Lean.Grind.OrderedAdd α