mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeMap : {α β : Type u_1} → [DecidableEq β] → (s : Set α) → (f : α → β) → [Fintype ↑s] → Fintype ↑(f <$> s)
-- Mathlib.Algebra.Star.Unitary
Unitary.star_mem_iff : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {U : R}, star U ∈ unitary R ↔ U ∈ unitary R
-- Init.Data.BitVec.Lemmas
BitVec.toNat_smod : ∀ {w : ℕ} {x y : BitVec w},
  (x.smod y).toNat =
    match x.msb, y.msb with
    | false, false => (x.umod y).toNat
    | false, true =>
      have u := x.umod (-y);
      if u = 0#w then u.toNat else (u + y).toNat
    | true, false =>
      have u := (-x).umod y;
      if u = 0#w then u.toNat else (y - u).toNat
    | true, true => (-(-x).umod (-y)).toNat
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `add_right_cancel`. -/
add_right_cancel'' : ∀ {G : Type u_1} [inst : Add G] [IsRightCancelAdd G] {a b c : G}, a + b = c + b → a = c
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Sum.homInduction_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P : {x y : C ⊕ D} → (x ⟶ y) → Sort u_1} (inl : (x y : C) → (f : x ⟶ y) → P ((CategoryTheory.Sum.inl_ C D).map f))
  (inr : (x y : D) → (f : x ⟶ y) → P ((CategoryTheory.Sum.inr_ C D).map f)) {x y : D} (f : x ⟶ y),
  CategoryTheory.Sum.homInduction inl inr ((CategoryTheory.Sum.inr_ C D).map f) = inr x y f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to0.tr.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] {σ : Type u_3} [inst_1 : Inhabited σ]
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) (x : Γ) (snd : σ), Turing.TM1to0.tr M (none, snd) x = none
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instNonUnitalCommRing : {X : Type u_3} →
  {R : Type u_4} →
    [inst : Zero X] →
      [inst_1 : TopologicalSpace X] →
        [inst_2 : CommRing R] →
          [inst_3 : TopologicalSpace R] → [IsTopologicalRing R] → NonUnitalCommRing (ContinuousMapZero X R)
-- Mathlib.Order.Filter.Basic
Filter.iInf_eq_generate : ∀ {α : Type u} {ι : Sort x} (s : ι → Filter α), iInf s = Filter.generate (⋃ i, (s i).sets)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.Hom.id : {J : CategoryTheory.Limits.MultispanShape} → (A : CategoryTheory.Limits.WalkingMultispan J) → A.Hom A
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.superpolynomialDecay_iff_abs_isBoundedUnder : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k : α → β} (f : α → β) [inst : TopologicalSpace β] [inst_1 : Field β]
  [inst_2 : LinearOrder β] [IsStrictOrderedRing β] [OrderTopology β],
  Filter.Tendsto k l Filter.atTop →
    (Asymptotics.SuperpolynomialDecay l k f ↔
      ∀ (z : ℕ), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun a => |k a ^ z * f a|)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopic.equivalence : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Equivalence ContinuousMap.Homotopic
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.sInf_adj : ∀ {V : Type u} {a b : V} {s : Set (SimpleGraph V)}, (sInf s).Adj a b ↔ (∀ G ∈ s, G.Adj a b) ∧ a ≠ b
-- Mathlib.Tactic.CategoryTheory.Coherence.Basic
Mathlib.Tactic.BicategoryLike.mk_eq : ∀ {α : Type u_1} (a b a' b' : α), a = a' → b = b' → a' = b' → a = b
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.isDone : Lean.Elab.Term.CollectPatternVars.Context → Bool
-- Mathlib.Algebra.Order.Interval.Multiset
Multiset.map_add_right_Ico : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Multiset.map (fun x => x + c) (Multiset.Ico a b) = Multiset.Ico (a + c) (b + c)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
/-- The category of affine schemes locally of finite type over a fixed base scheme is essentially small.
TODO: extend this to (relatively) quasi-compact schemes.
 -/
AlgebraicGeometry.essentiallySmall_costructuredArrow_Spec : ∀ {X : AlgebraicGeometry.Scheme},
  ∀ P ≤ @AlgebraicGeometry.LocallyOfFiniteType,
    ∀ [P.RespectsIso],
      CategoryTheory.EssentiallySmall.{u, u, u + 1} (P.CostructuredArrow ⊤ AlgebraicGeometry.Scheme.Spec X)
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.factor_eq_factor : ∀ {R : Type u_1} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided] [inst_2 : J.IsTwoSided] (h : I ≤ J)
  (x : R ⧸ I), (Submodule.factor h) x = (Ideal.Quotient.factor h) x
-- Mathlib.Topology.Subpath
/-- Alternative to `Path.Homotopy.concatSubpath` in terms of `Path.Homotopic`.  -/
Path.Homotopic.concat_subpath : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} {n : ℕ} (γ : Path a b) (t : Fin (n + 1) → ↑unitInterval),
  (Path.concat (⇑γ ∘ t) fun k => γ.subpath (t k.castSucc) (t k.succ)).Homotopic (γ.subpath (t 0) (t (Fin.last n)))
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.ext : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  ⦃f g : L.Equiv M N⦄, (∀ (x : M), f x = g x) → f = g
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minView.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (hr : r.Balanced) (size : ℕ)
  (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hl_2 : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
  (hlr_2 : Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size r.size),
  Std.DTreeMap.Internal.Impl.minView k v (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') r hl_2 hr hlr_2 =
    match Std.DTreeMap.Internal.Impl.minView k' v' l' r' ⋯ ⋯ ⋯ with
    | { k := dk, v := dv, tree := { impl := dt, balanced_impl := hdt, size_impl := hdt' } } =>
      { k := dk, v := dv,
        tree :=
          { impl := Std.DTreeMap.Internal.Impl.balanceRErase k v dt r ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ } }
-- Init.Data.String.Defs
String.Slice.Pos.le_iff : ∀ {s : String.Slice} {l r : s.Pos}, l ≤ r ↔ l.offset ≤ r.offset
-- Mathlib.Topology.Inseparable
StableUnderGeneralization.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  StableUnderGeneralization s → Continuous f → StableUnderGeneralization (f ⁻¹' s)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_union_add_inter₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasureTheory.NullMeasurableSet t μ → μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The `k`-linear `G`-representation on `k[Gⁿ]`, induced by left multiplication.  -/
Rep.diagonal : (k : Type u) → (G : Type v) → [inst : Ring k] → [inst_1 : Monoid G] → ℕ → Rep.{max u v, u, v} k G
-- Init.Data.String.Lemmas.FindPos
String.posGE_eq_pos : ∀ {s : String} {p : String.Pos.Raw} (h : String.Pos.Raw.IsValid s p), s.posGE p ⋯ = s.pos p h
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.Pos.skipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Init.Data.Subtype.Order
Subtype.instLE : {α : Type u} → [LE α] → {P : α → Prop} → LE (Subtype P)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintTooltip : Type
-- Mathlib.FieldTheory.Extension
IntermediateField.Lifts.instPartialOrder : {F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] →
            [inst_3 : Algebra F E] → [inst_4 : Algebra F K] → PartialOrder (IntermediateField.Lifts F E K)
-- Mathlib.Analysis.Convex.Cone.Dual
PointedCone.isClosed_dual : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : TopologicalSpace R] [ClosedIciTopology R] [inst_4 : IsOrderedRing R] [inst_5 : AddCommGroup M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R M] [inst_8 : Module R N] [inst_9 : TopologicalSpace N]
  {p : M →ₗ[R] N →ₗ[R] R} {s : Set M}, (∀ (x : M), Continuous ⇑(p x)) → IsClosed ↑(PointedCone.dual p s)
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_three_eq_top : SimpleGraph.cycleGraph 3 = ⊤
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
MonoidHom.isUniformEmbedding_of_isEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {Hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : Group β] [IsUniformGroup β] [inst_6 : FunLike Hom α β] [MonoidHomClass Hom α β]
  {f : Hom}, Topology.IsEmbedding ⇑f → IsUniformEmbedding ⇑f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_eq_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k fallback : α}, k ∈ t → t.getKeyD k fallback = k
-- Lean.DocString.Types
Lean.Doc.Block.code.sizeOf_spec : ∀ {i : Type u} {b : Type v} [inst : SizeOf i] [inst_1 : SizeOf b] (content : String),
  sizeOf (Lean.Doc.Block.code content) = 1 + sizeOf content
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.faithful_whiskeringLeft_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D],
  ((CategoryTheory.Functor.whiskeringLeft C (CategoryTheory.Quotient r) D).obj
      (CategoryTheory.Quotient.functor r)).Faithful
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_comp_mk₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) {n : ℕ}
  (α : CategoryTheory.Abelian.Ext Z T n),
  (CategoryTheory.Abelian.Ext.mk₀ f).comp ((CategoryTheory.Abelian.Ext.mk₀ g).comp α ⋯) ⋯ =
    (CategoryTheory.Abelian.Ext.mk₀ (CategoryTheory.CategoryStruct.comp f g)).comp α ⋯
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.support_weights_nonempty : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} [Nontrivial R]
  (w : Convexity.StdSimplex R M), w.weights.support.Nonempty
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_smul : ∀ {A : Type u_1} {B : Type u_2} (a : A) (b : B) (C : Type u_3) [inst : SMul A B] [inst_1 : CommSemiring B]
  [inst_2 : Semiring C] [inst_3 : Algebra B C] [inst_4 : SMul A C] [IsScalarTower A B C], ↑(a • b) = a • ↑b
-- Init.Data.Nat.Lemmas
Nat.lt_of_add_lt_add_right : ∀ {k m n : ℕ}, k + n < m + n → k < m
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.mul_div_lipschitzWith : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E}, AntilipschitzWith Kf f → LipschitzWith Kg (g / f) → Kg < Kf⁻¹ → AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g
-- Mathlib.CategoryTheory.DinatTrans
CategoryTheory.DinatTrans.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} [inst_2 : SizeOf C] [inst_3 : SizeOf D]
  (app : (X : C) → (F.obj (Opposite.op X)).obj X ⟶ (G.obj (Opposite.op X)).obj X)
  (dinaturality :
    autoParam
      (∀ {X Y : C} (f : X ⟶ Y),
        CategoryTheory.CategoryStruct.comp ((F.map f.op).app X)
            (CategoryTheory.CategoryStruct.comp (app X) ((G.obj (Opposite.op X)).map f)) =
          CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op Y)).map f)
            (CategoryTheory.CategoryStruct.comp (app Y) ((G.map f.op).app Y)))
      CategoryTheory.DinatTrans.dinaturality._autoParam),
  sizeOf { app := app, dinaturality := dinaturality } = 1
-- Mathlib.Algebra.Torsor.Basic
smul_sdiv_smul_comm : ∀ {G : Type u_1} {P : Type u_2} [inst : CommGroup G] [inst_1 : Torsor G P] (v₁ v₂ : G) (p₁ p₂ : P),
  v₁ • p₁ /ₛ v₂ • p₂ = v₁ / v₂ * (p₁ /ₛ p₂)
-- Mathlib.Probability.HasLaw
/-- The predicate `HasLaw X μ P` registers the fact that the random variable `X` has law `μ` under
the measure `P`, in other words that `P.map X = μ`. We also require `X` to be `AEMeasurable`,
to allow for nice interactions with operations on the codomain of `X`. See for instance
`HasLaw.comp`, `IndepFun.hasLaw_mul` and `IndepFun.hasLaw_add`.  -/
ProbabilityTheory.HasLaw : {Ω : Type u_1} →
  {𝓧 : Type u_2} →
    {mΩ : MeasurableSpace Ω} →
      {m𝓧 : MeasurableSpace 𝓧} →
        (Ω → 𝓧) → MeasureTheory.Measure 𝓧 → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.HasLaw._auto_1 → Prop
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → k ∉ t₁ \ t₂
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.isPrime : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : IsDedekindDomain S] (P : ↥(UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p)).toFinset),
  (↑P).IsPrime
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.measurableSet_sigmaFiniteSetWRT : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, MeasurableSet (μ.sigmaFiniteSetWRT ν)
-- Mathlib.Order.Hom.Lattice
InfHom.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : Min β] → FunLike (InfHom α β) α β
-- Mathlib.Order.Interval.Basic
Interval.partialOrder : {α : Type u_1} → [inst : PartialOrder α] → PartialOrder (Interval α)
-- Init.Data.SInt.Lemmas
Int64.toInt8_toInt16 : ∀ (n : Int64), n.toInt16.toInt8 = n.toInt8
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.RotateLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {aig : Std.Sat.AIG α} (input : aig.RefVec w)
  (distance curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go input distance curr hcurr s =
    if hcurr1 : curr < w then
      if hcurr2 : curr < distance % w then
        have ref := input.get (w - distance % w + curr) ⋯;
        have s := s.push ref;
        Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go input distance (curr + 1) ⋯ s
      else
        have ref := input.get (curr - distance % w) ⋯;
        have s := s.push ref;
        Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateLeft.go input distance (curr + 1) ⋯ s
    else
      have hcurr := ⋯;
      hcurr ▸ s
-- Mathlib.Data.Fintype.Inv
Function.Injective.invFun_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β} (hf : Function.Injective f)
  [inst_2 : Nonempty α], (Set.range f).domRestrict (Function.invFun f) = hf.invOfMemRange
-- Mathlib.NumberTheory.LSeries.Deriv
/-- The derivative of the terms of an L-series.  -/
LSeries.hasDerivAt_term : ∀ (f : ℕ → ℂ) (n : ℕ) (s : ℂ), HasDerivAt (fun z => LSeries.term f z n) (-LSeries.term (LSeries.logMul f) s n) s
-- Mathlib.Lean.MessageData.ForExprs
Lean.MessageData.Exprs.mk.inj : ∀ {msg msg_1 : Lean.MessageData}, { msg := msg } = { msg := msg_1 } → msg = msg_1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.app_invApp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑Y) {Z : C}
  (h :
    Y.presheaf.obj
        (Opposite.op
          ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj
            ((TopologicalSpace.Opens.map f.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U)) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticOn.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E}, AnalyticOn 𝕜 f s → DifferentiableOn 𝕜 f s
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.of_sub_left : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 (s - t) → t.Nonempty → Bornology.IsVonNBounded 𝕜 s
-- Init.Data.List.Monadic
List.foldrM_attachWith : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α} {q : α → Prop}
  (H : ∀ a ∈ l, q a) {f : { x // q x } → β → m β} {b : β},
  List.foldrM f b (l.attachWith q H) = List.foldrM (fun a acc => f ⟨↑a, ⋯⟩ acc) b l.attach
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.prod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (s : Subsemigroup M) (t : Subsemigroup N),
  s.prod t = { carrier := ↑s ×ˢ ↑t, mul_mem' := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.toClosedSubmodule_injective : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H],
  Function.Injective StandardSubspace.toClosedSubmodule
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.map_stabilizer_le : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (f : G →+ H) (s : Set G),
  AddSubgroup.map f (AddAction.stabilizer G s) ≤ AddAction.stabilizer H (⇑f '' s)
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι}
  {p' : Filter α} [p.NeBot] {L : ι → β} {ℓ : β},
  TendstoUniformlyOnFilter F f p p' →
    (∀ᶠ (i : ι) in p, Filter.Tendsto (F i) p' (nhds (L i))) → Filter.Tendsto L p (nhds ℓ) → Filter.Tendsto f p' (nhds ℓ)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.minKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (xs : List ((a : α) × β a)),
  Std.Internal.List.minKey? xs = Option.map Sigma.fst (Std.Internal.List.minEntry? xs)
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.instHasAffinePropertyDiagonalSchemeDiagonal : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) {Q : AlgebraicGeometry.AffineTargetMorphismProperty}
  [AlgebraicGeometry.HasAffineProperty P Q], AlgebraicGeometry.HasAffineProperty P.diagonal Q.diagonal
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_injective_of_injective : ∀ {n : ℕ} {α : Type u_2} {x₀ : α} {x : Fin n → α},
  Function.Injective x → x₀ ∉ Set.range x → Function.Injective (Fin.snoc x x₀)
-- Mathlib.Data.Vector.Basic
List.Vector.nodup_iff_injective_get : ∀ {α : Type u_1} {n : ℕ} {v : List.Vector α n}, v.toList.Nodup ↔ Function.Injective v.get
-- Init.Omega.IntList
Lean.Omega.IntList.add_nil : ∀ (xs : Lean.Omega.IntList), xs + [] = xs
-- Mathlib.Algebra.Opposites
AddOpposite.unop_comp_op : ∀ {α : Type u_1}, AddOpposite.unop ∘ AddOpposite.op = id
-- Mathlib.Data.Finset.Image
Finset.image_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → β), Finset.image f ∅ = ∅
-- Mathlib.Order.WithBot
WithTop.le_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithTop αᵒᵈ} {y : WithBot α}, y ≤ WithTop.ofDual x ↔ x ≤ WithBot.toDual y
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.notMem_of_notMem_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {P : R}, P ∉ NonUnitalSubsemiring.closure s → P ∉ s
-- Mathlib.RingTheory.Localization.FractionRing
/-- Given a `MulSemiringAction G B`, extend the action of `G` on `B` to a `MulSemiringAction G L`
on the fraction field `L` of `B`.  -/
IsFractionRing.mulSemiringAction : (G : Type u_10) →
  (B : Type u_12) →
    (L : Type u_14) →
      [inst : Group G] →
        [inst_1 : CommRing B] →
          [MulSemiringAction G B] →
            [inst_3 : Field L] → [inst_4 : Algebra B L] → [IsFractionRing B L] → MulSemiringAction G L
-- Init.Data.Array.DecidableEq
/-- Equality with `#[]` is decidable even if the underlying type does not have decidable equality.
 -/
Array.instDecidableEqEmp : {α : Type u_1} → (xs : Array α) → Decidable (xs = #[])
-- Mathlib.ModelTheory.Definability
Set.empty_definableFun_iff : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {f : (α → M) → M},
  Set.DefinableFun L ∅ f ↔ ∃ φ, Function.tupleGraph f = Set.ofPred φ.Realize
-- Mathlib.MeasureTheory.Order.Lattice
/-- Eta-expanded form of `Measurable.sup` -/
Measurable.fun_sup : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {f g : α → M} [inst_1 : Max M]
  [MeasurableSup₂ M], Measurable f → Measurable g → Measurable fun i => f i ⊔ g i
-- Init.Data.Array.Lemmas
Array.toList_snd_unzip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array (α × β)}, xs.unzip.2.toList = xs.toList.unzip.2
-- Mathlib.FieldTheory.Galois.Abelian
instIsAbelianGaloisSubtypeMemIntermediateFieldBot : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L], IsAbelianGalois K ↥⊥
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_zero_C : ∀ {R : Type u_1} [inst : Semiring R] (a : R), (PowerSeries.coeff 0) (PowerSeries.C a) = a
-- Lean.Compiler.IR.CompilerM
Lean.IR.logDecls : Lean.Name → Array Lean.IR.Decl → Lean.IR.CompilerM Unit
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.quot_map_mk : ∀ {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → List (β × Bool))
  (H : Relator.LiftFun FreeAddGroup.Red.Step FreeAddGroup.Red.Step f f),
  Quot.map f H (FreeAddGroup.mk L) = FreeAddGroup.mk (f L)
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.instCoeSortType : CoeSort GrpWithZero (Type u_1)
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coe_inj : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} ⦃f g : 𝒜 →+*ᵍ ℬ⦄, ⇑f = ⇑g → f = g
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.boundedBy_eq : ∀ {α : Type u_1} {m : Set α → ENNReal} (s : Set α),
  m ∅ = 0 →
    (∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t) →
      (∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)) → (MeasureTheory.OuterMeasure.boundedBy m) s = m s
-- Init.WF
WellFounded.val_wrap : ∀ {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α), ↑(h.wrap x) = x
-- Mathlib.Algebra.Lie.SemiDirect
/-- The semi-direct sum of two Lie algebras `K` and `L` over `R`, relative to a Lie algebra homomorphism
`ψ: L → LieDerivation R K K`. As a set, it is just `K × L`, however the Lie bracket is twisted by
`ψ`.
 -/
LieAlgebra.«term_⋊⁅_⁆_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.add_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
  {v : MeasureTheory.VectorMeasure α M} {w₁ w₂ : MeasureTheory.VectorMeasure α N} [T2Space M]
  [inst_5 : ContinuousAdd N], v.MutuallySingular w₁ → v.MutuallySingular w₂ → v.MutuallySingular (w₁ + w₂)