mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Image
Set.range_subset_range_iff_exists_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → γ} {g : β → γ}, Set.range f ⊆ Set.range g ↔ ∃ h, f = g ∘ h
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map_obj_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G)
  (X : CategoryTheory.Grothendieck F), ((CategoryTheory.Grothendieck.map α).obj X).base = X.base
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_setWidth_of_le : ∀ {w k l : ℕ} (x : BitVec w), k ≤ l → BitVec.setWidth k (BitVec.setWidth l x) = BitVec.setWidth k x
-- Mathlib.Order.Monotone.Monovary
monovaryOn_const_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] (f : ι → α) (b : β)
  (s : Set ι), MonovaryOn f (Function.const ι b) s
-- Mathlib.Order.Filter.Cocardinal
Filter.eventually_cocardinal_ne : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} (x : α), ∀ᶠ (a : α) in Filter.cocardinal α hreg, a ≠ x
-- Mathlib.CategoryTheory.Sites.CoverPreserving
/-- If `C` has pullbacks and `F : C ⥤ D` preserves pullbacks, any cover preserving
functor preserves all `1`-hypercovers.  -/
CategoryTheory.Functor.PreservesOneHypercovers.of_coverPreserving : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F],
  CategoryTheory.CoverPreserving J K F → F.PreservesOneHypercovers J K
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.X_sub_C_mul_divByMonic_eq_sub_modByMonic : ∀ {K : Type u_1} [inst : Ring K] (f : Polynomial K) (a : K),
  (Polynomial.X - Polynomial.C a) * (f /ₘ (Polynomial.X - Polynomial.C a)) = f - f %ₘ (Polynomial.X - Polynomial.C a)
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- Partially-applied version of `FractionalIdeal.ext_iff`.  -/
FractionalIdeal.coe_ext_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P}, I = J ↔ ↑I = ↑J
-- Mathlib.Order.Closure
LowerAdjoint.closure_sup_closure_left : ∀ {α : Type u_1} {β : Type u_4} [inst : SemilatticeSup α] [inst_1 : Preorder β] {u : β → α} (l : LowerAdjoint u)
  (x y : α), u (l.toFun (u (l.toFun x) ⊔ y)) = u (l.toFun (x ⊔ y))
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_inj_left : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, a ≤ b → a ≤ c → b - a = c - a → b = c
-- Mathlib.GroupTheory.Torsion
/-- A predicate on an additive monoid saying that all elements are of finite order.  -/
IsAddTorsion : (G : Type u_1) → [AddMonoid G] → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_lt_zero_iff : ∀ {x : ENNReal}, x.log < 0 ↔ x < 1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipSuffix?_eq_none_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.LawfulBackwardPattern pat] {s : String.Slice}, s.skipSuffix? pat = none ↔ s.endsWith pat = false
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.le_lim : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : CauSeq.IsComplete α abs] {f : CauSeq α abs} {x : α}, CauSeq.const abs x ≤ f → x ≤ f.lim
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.bddAbove_ord_image_iff : ∀ {s : Set Cardinal.{u_1}}, BddAbove (Cardinal.ord '' s) ↔ BddAbove s
-- Mathlib.Algebra.Quandle
/-- Show that `toEnvelGroup.mapAux` sends equivalent expressions to equal terms.
 -/
Rack.toEnvelGroup.mapAux.well_def : ∀ {R : Type u_1} [inst : Rack R] {G : Type u_2} [inst_1 : Group G] (f : ShelfHom R (Quandle.Conj G))
  {a b : Rack.PreEnvelGroup R} (a_1 : Rack.PreEnvelGroupRel' R a b),
  Rack.toEnvelGroup.mapAux f a = Rack.toEnvelGroup.mapAux f b
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.clift_apply_mk : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : FreeMonoid (M ⊕ N) →* P) (hM₁ : f (FreeMonoid.of (Sum.inl 1)) = 1) (hN₁ : f (FreeMonoid.of (Sum.inr 1)) = 1)
  (hM : ∀ (x y : M), f (FreeMonoid.of (Sum.inl (x * y))) = f (FreeMonoid.of (Sum.inl x) * FreeMonoid.of (Sum.inl y)))
  (hN : ∀ (x y : N), f (FreeMonoid.of (Sum.inr (x * y))) = f (FreeMonoid.of (Sum.inr x) * FreeMonoid.of (Sum.inr y)))
  (w : FreeMonoid (M ⊕ N)), (Monoid.Coprod.clift f hM₁ hN₁ hM hN) (Monoid.Coprod.mk w) = f w
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {j : n} {c : m → α} [inst : DecidableEq n]
  {j' : n}, M.updateCol j c i j' = if j' = j then c i else M i j'
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.mapObj_ext_iff : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X : CategoryTheory.GradedObject I C} {p : I → J} [inst_1 : X.HasMap p] {A : C} {j : J} {f g : X.mapObj p j ⟶ A},
  f = g ↔
    ∀ (i : I) (hij : p i = j),
      CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f =
        CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) g
-- Lean.DocString.Types
Lean.Doc.Inline.brecOn_1.go : {i : Type u} →
  {motive_1 : Lean.Doc.Inline i → Sort u_1} →
    {motive_2 : Array (Lean.Doc.Inline i) → Sort u_1} →
      {motive_3 : List (Lean.Doc.Inline i) → Sort u_1} →
        (t : Array (Lean.Doc.Inline i)) →
          ((t : Lean.Doc.Inline i) → t.below → motive_1 t) →
            ((t : Array (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_1 t → motive_2 t) →
              ((t : List (Lean.Doc.Inline i)) → Lean.Doc.Inline.below_2 t → motive_3 t) →
                motive_2 t ×' Lean.Doc.Inline.below_1 t
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.findMin.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) (k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α)
  (x : Batteries.BinomialHeap.Imp.Heap α) (x_1 : Batteries.BinomialHeap.Imp.FindMin α),
  Batteries.BinomialHeap.Imp.Heap.findMin le k x x_1 =
    match x, x_1 with
    | Batteries.BinomialHeap.Imp.Heap.nil, res => res
    | Batteries.BinomialHeap.Imp.Heap.cons r a c s, res =>
      Batteries.BinomialHeap.Imp.Heap.findMin le (k ∘ Batteries.BinomialHeap.Imp.Heap.cons r a c) s
        (if le res.val a = true then res else { before := k, val := a, node := c, next := s })
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.renameEquiv_trans : ∀ {σ : Type u_1} {τ : Type u_2} {γ : Type u_3} {R : Type u_4} [inst : CommSemiring R] (e : σ ≃ τ) (f : τ ≃ γ),
  (MvPowerSeries.renameEquiv R e).trans (MvPowerSeries.renameEquiv R f) = MvPowerSeries.renameEquiv R (e.trans f)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE Int8
-- Mathlib.NumberTheory.SmoothNumbers
Nat.roughNumbersUpTo.eq_1 : ∀ (N k : ℕ), N.roughNumbersUpTo k = {n ∈ Finset.range (N + 1) | n ≠ 0 ∧ n ∉ k.smoothNumbers}
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.brecOn.go : {B : Type u} →
  [inst : Quiver B] →
    {motive :
        {a b : CategoryTheory.FreeBicategory B} →
          (a_1 a_2 : a ⟶ b) → CategoryTheory.FreeBicategory.Hom₂ a_1 a_2 → Sort u_1} →
      {a b : CategoryTheory.FreeBicategory B} →
        {a_1 a_2 : a ⟶ b} →
          (t : CategoryTheory.FreeBicategory.Hom₂ a_1 a_2) →
            ({a b : CategoryTheory.FreeBicategory B} →
                (a_3 a_4 : a ⟶ b) →
                  (t : CategoryTheory.FreeBicategory.Hom₂ a_3 a_4) →
                    CategoryTheory.FreeBicategory.Hom₂.below t → motive a_3 a_4 t) →
              motive a_1 a_2 t ×' CategoryTheory.FreeBicategory.Hom₂.below t
-- Mathlib.Topology.DiscreteSubset
/-- **Alias** of `isDiscrete_iff_forall_mem_exists_isOpen`.

---

A set `s` is discrete iff for every `y ∈ s` there is an open `u` with `u ∩ s = {y}`.
See `isDiscrete_iff_forall_subset_exists_isOpen'` for a related version of this with subsets.  -/
isDiscrete_iff_forall_exists_isOpen : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] {s : Set Y}, IsDiscrete s ↔ ∀ y ∈ s, ∃ u, IsOpen u ∧ u ∩ s = {y}
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.liftOn_def : ∀ {K : Type u_1} [inst : CommRing K] {P : Sort u_2} (x : RatFunc K) (f : Polynomial K → Polynomial K → P)
  (H :
    ∀ {p q p' q' : Polynomial K},
      q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q'),
  x.liftOn f H = Localization.liftOn x.toFractionRing (fun p q => f p ↑q) ⋯
-- Aesop.RuleSet.Member
Aesop.LocalRuleSetMember.localNormSimpRule.injEq : ∀ (r r_1 : Aesop.LocalNormSimpRule),
  (Aesop.LocalRuleSetMember.localNormSimpRule r = Aesop.LocalRuleSetMember.localNormSimpRule r_1) = (r = r_1)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : Option β → Option β},
  m.WF →
    Std.DHashMap.Raw.Const.getD (Std.DHashMap.Raw.Const.alter m k f) k fallback =
      (f (Std.DHashMap.Raw.Const.get? m k)).getD fallback
-- Mathlib.Data.ZMod.Basic
ZMod.cast_sub_one : ∀ {R : Type u_1} [inst : Ring R] {n : ℕ} (k : ZMod n), (k - 1).cast = (if k = 0 then ↑n else k.cast) - 1
-- Std.Internal.Do.WP.Lemmas
EStateM.get.eq_1 : ∀ {ε σ : Type u} (s : σ), EStateM.get s = EStateM.Result.ok s s
-- Batteries.Lean.Meta.UnusedNames
_private.Batteries.Lean.Meta.UnusedNames.0.Lean.Name.parseIndexSuffix : String.Slice → Option ℕ
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (app : (X : C) → (Y : D) → P.obj X Y ⟶ Q.obj X Y)
  (naturality :
    autoParam
      (∀ ⦃X X' : C⦄ ⦃Y Y' : D⦄ (f : X ⟶ X') (g : Y ⟶ Y'),
        CategoryTheory.CategoryStruct.comp (P.map f g) (app X' Y) =
          CategoryTheory.CategoryStruct.comp (app X Y') (Q.map f g))
      CategoryTheory.ProfunctorCore.Hom.naturality._autoParam),
  sizeOf { app := app, naturality := naturality } = 1
-- Mathlib.Order.RelIso.Basic
RelHom.mk.inj : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} {toFun : α → β}
  {map_rel' : ∀ {a b : α}, r a b → s (toFun a) (toFun b)} {toFun_1 : α → β}
  {map_rel'_1 : ∀ {a b : α}, r a b → s (toFun_1 a) (toFun_1 b)},
  { toFun := toFun, map_rel' := map_rel' } = { toFun := toFun_1, map_rel' := map_rel'_1 } → toFun = toFun_1
-- Mathlib.Order.Defs.LinearOrder
eq_or_gt_of_not_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ¬a < b → a = b ∨ b < a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- Extensionality principle for morphisms in `CategoricalPullback F G`.  -/
CategoryTheory.Limits.CategoricalPullback.hom_ext : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} {f g : x ⟶ y}, f.fst = g.fst → f.snd = g.snd → f = g
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.take.match_1.eq_3 : ∀ {α : Type u_1} (motive : ℕ → List α → Sort u_2) (n : ℕ) (a : α) (as : List α) (h_1 : (x : List α) → motive 0 x)
  (h_2 : (n : ℕ) → motive n.succ []) (h_3 : (n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)),
  (match n.succ, a :: as with
    | 0, x => h_1 x
    | n.succ, [] => h_2 n
    | n.succ, a :: as => h_3 n a as) =
    h_3 n a as
-- Mathlib.Data.Set.CoeSort
Set.elem_mem : ∀ {σ : Type u_1} {α : Type u_2} [inst : Membership σ α] {S : α}, ↑{x | x ∈ S} = { x // x ∈ S }
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_comap : ∀ {K : Type u} [inst : Field K] {L : Type u_1} [inst_1 : Field L] {A : ValuationSubring L} {f : K →+* L} {x : K},
  x ∈ A.comap f ↔ f x ∈ A
-- Mathlib.Analysis.Analytic.Linear
analyticWithinAt_fst : ∀ {𝕜 : 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] {t : Set (E × F)}
  {p : E × F}, AnalyticWithinAt 𝕜 (fun p => p.1) t p
-- Mathlib.Topology.Bornology.Absorbs
absorbent_univ : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α],
  Absorbent G₀ Set.univ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- An disequality `a != 0` coming from the core. That is, `(a = 0) = False` in the core.  -/
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.core0 : Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.continuous_singleton : ∀ {α : Type u_1} [inst : TopologicalSpace α], Continuous fun x => {x}
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.rightUnitor_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : CategoryTheory.AddMon C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.hom =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.X).hom
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.funLike : {E : Type u_3} → [inst : Group E] → FunLike (GroupSeminorm E) E ℝ
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.RefIdentJsonRepr.c.sizeOf_spec : ∀ (m n : String), sizeOf (Lean.Lsp.RefIdent.RefIdentJsonRepr.c m n) = 1 + sizeOf m + sizeOf n
-- Mathlib.Geometry.Manifold.Immersion
/-- A `C^n` immersion at `x` is continuous at `x`.  -/
Manifold.IsImmersionAtOfComplement.continuousAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M},
  Manifold.IsImmersionAtOfComplement F I J n f x → ContinuousAt f x
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.coordChange_model_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_8} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (b b' x : F),
  (tangentBundleCore (modelWithCornersSelf 𝕜 F) F).coordChange (achart F b) (achart F b') x = 1
-- Mathlib.RingTheory.Coprime.Lemmas
Int.isCoprime_gcdB : ∀ {x y : ℤ}, IsCoprime x y → IsCoprime (x.gcdB y) x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_filter_not_contains_map_fst : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getValueCast k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) h₁ =
        Std.Internal.List.getValueCast k l₁ h₂
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instGroup : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [Group β] → Group (MeasureTheory.SimpleFunc α β)
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.instLieAlgebra : {𝕜 : 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} →
                {G : Type u_4} →
                  [inst_4 : TopologicalSpace G] →
                    [inst_5 : ChartedSpace H G] →
                      [inst_6 : Monoid G] →
                        [inst_7 : ContMDiffMul I (↑⊤) G] → LieAlgebra 𝕜 (LeftInvariantDerivation I G)
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.instMulActionWithZeroOfUniformContinuousConstSMul : {M : Type u_1} →
  {α : Type u_3} →
    [inst : UniformSpace α] →
      [inst_1 : MonoidWithZero M] →
        [inst_2 : Zero α] →
          [inst_3 : MulActionWithZero M α] →
            [UniformContinuousConstSMul M α] → MulActionWithZero M (UniformSpace.Completion α)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instDecidableEqBVBit.decEq : (x x_1 : Std.Tactic.BVDecide.BVBit) → Decidable (x = x_1)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.WeaklyRegular.zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α], MeasureTheory.Measure.WeaklyRegular 0
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.lift_comp_eqToHom_iff : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S S' : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (h : S = S'),
  p.IsHomLift (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) φ ↔ p.IsHomLift f φ
-- Mathlib.Data.Set.Card.Arithmetic
Set.encard_iUnion_le_of_finite : ∀ {α : Type u_1} {ι : Type u_2} [Finite ι] (s : ι → Set α), (⋃ i, s i).encard ≤ ∑ᶠ (i : ι), (s i).encard
-- Init.Omega.IntList
/-- The dot product of two `IntList`s.  -/
Lean.Omega.IntList.dot : Lean.Omega.IntList → Lean.Omega.IntList → ℤ
-- Mathlib.Data.Stream.Init
Stream'.cons_append_stream : ∀ {α : Type u} (a : α) (l : List α) (s : Stream' α), a :: l ++ₛ s = Stream'.cons a (l ++ₛ s)
-- Mathlib.Order.Filter.Basic
Filter.frequently_or_distrib : ∀ {α : Type u} {f : Filter α} {p q : α → Prop},
  (∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.update_sub : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Sub (f i)] [inst_1 : DecidableEq I] (f₁ f₂ : (i : I) → f i) (i : I)
  (x₁ x₂ : f i), Function.update (f₁ - f₂) i (x₁ - x₂) = Function.update f₁ i x₁ - Function.update f₂ i x₂
-- Init.Data.Dyadic.Basic
instDecidableEqDyadic.decEq : (x x_1 : Dyadic) → Decidable (x = x_1)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
PowerBasis.equivAdjoinSimple_gen : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (pb : PowerBasis K L),
  pb.equivAdjoinSimple (IntermediateField.AdjoinSimple.gen K pb.gen) = pb.gen
-- Mathlib.Tactic.NormNum.Abs
/-- The `norm_num` extension which identifies expressions of the form `|a|`,
such that `norm_num` successfully recognises `a`.  -/
Mathlib.Meta.NormNum.evalAbs : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.Order.WithBot
WithTop.forall_coe_le_iff_le : ∀ {α : Type u_1} [inst : Preorder α] {x y : WithTop α} [NoTopOrder α], (∀ (a : α), ↑a ≤ y → ↑a ≤ x) ↔ y ≤ x
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instInhabited : (α : Type u_2) → [inst : Max α] → [inst_1 : Bot α] → Inhabited (SupBotHom α α)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trAux.match_1.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → σ → Sort u_4) (a : Γ → σ → Γ)
  (q : Turing.TM1.Stmt Γ Λ σ) (v : σ)
  (h_1 : (d : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.move d q) v)
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.write a q) v)
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.load a q) v)
  (h_4 : (p : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → motive (Turing.TM1.Stmt.goto l) v) (h_6 : (v : σ) → motive Turing.TM1.Stmt.halt v),
  (match Turing.TM1.Stmt.write a q, v with
    | Turing.TM1.Stmt.move d q, v => h_1 d q v
    | Turing.TM1.Stmt.write a q, v => h_2 a q v
    | Turing.TM1.Stmt.load a q, v => h_3 a q v
    | Turing.TM1.Stmt.branch p q₁ q₂, v => h_4 p q₁ q₂ v
    | Turing.TM1.Stmt.goto l, v => h_5 l v
    | Turing.TM1.Stmt.halt, v => h_6 v) =
    h_2 a q v
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.isFiniteMeasure_withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (a : α), f a ∂μ ≠ ⊤ → MeasureTheory.IsFiniteMeasure (μ.withDensity f)
-- Mathlib.CategoryTheory.Category.Cat.Limit
CategoryTheory.Cat.HasLimits.limitConeX_α : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J CategoryTheory.Cat),
  ↑(CategoryTheory.Cat.HasLimits.limitConeX F) = CategoryTheory.Limits.limit (F.comp CategoryTheory.Cat.objects)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.Limits.IsZero Y → ∀ (f : X ⟶ Y), CategoryTheory.IsIso f
-- Mathlib.Data.List.Lex
List.lex_singleton_iff : ∀ {α : Type u} {r : α → α → Prop} (a b : α), List.Lex r [a] [b] ↔ r a b
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.lower.eq_1 : ∀ (α : Type u_1) [inst : Preorder α], Topology.lower α = TopologicalSpace.generateFrom {s | ∃ a, (Set.Ici a)ᶜ = s}
-- Mathlib.CategoryTheory.Monoidal.Opposite.Mon
MonObj.mopMonObj_one_unmop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M], CategoryTheory.MonObj.one.unmop = CategoryTheory.MonObj.one
-- Init.Tactics
/-- `mframe` infers which hypotheses from the stateful context can be moved into the pure context.
This is useful because pure hypotheses "survive" the next application of modus ponens
(`Std.Do.SPred.mp`) and transitivity (`Std.Do.SPred.entails.trans`).

It is used as part of the `mspec` tactic.

```lean
example (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
  mintro _
  mframe
  /- `h : p ∧ q ∧ r ∧ s ∧ t` in the pure context -/
  mcases h with hP
  mexact h
```
 -/
Lean.Parser.Tactic.mframeMacro : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.entryAtIdxD.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → α × β → Sort u_3) (x : ℕ)
  (fallback : α × β) (h_1 : (x : ℕ) → (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf x fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (n : ℕ) → (fallback : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, x, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => h_1 x fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback => h_2 size k v l r n fallback) =
    h_1 x fallback
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- the map between the apices  -/
CategoryTheory.Span.Hom.hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      {c c' : C} → {S₁ S₂ : CategoryTheory.Span Wₗ Wᵣ c c'} → S₁.Hom S₂ → (S₁.apex ⟶ S₂.apex)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.subtypeVal : ∀ {α : Type u_2} [inst : AddCommMonoid α] {n : ℕ} {S : Type u_5} [inst_1 : SetLike S α] [inst_2 : AddSubmonoidClass S α]
  {s : S}, IsAddFreimanHom n Set.univ Set.univ Subtype.val