mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
/-- Turns a `MetaM MessageData` into a `MessageData.lazy` which will run the monadic value.
The optional array of expressions is used to set the `hasSyntheticSorry` fields, and should
comprise the expressions that are included in the message data.
 -/
Lean.MessageData.ofLazyM : Lean.MetaM Lean.MessageData → optParam (Array Lean.Expr) #[] → Lean.MessageData
-- Mathlib.RepresentationTheory.Rep.Iso
Rep.diagonal_succ_projective : ∀ {k : Type u} [inst : CommRing k] {G : Type u} [inst_1 : Group G] {n : ℕ},
  CategoryTheory.Projective (Rep.diagonal k G (n + 1))
-- Mathlib.Algebra.Ring.Units
RingHom.isUnit_map : ∀ {α : Type u} {β : Type v} [inst : Semiring α] [inst_1 : Semiring β] (f : α →+* β) {a : α}, IsUnit a → IsUnit (f a)
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.isometry_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace β] (s : Set α),
  Isometry (⇑UniformFun.ofFun ∘ s.domRestrict ∘ ⇑(UniformOnFun.toFun {s}))
-- Mathlib.RingTheory.Finiteness.Subalgebra
Subalgebra.finite_bot : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], Module.Finite R ↥⊥
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosedIn.algebraMap_eq_of_integral : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsIntegrallyClosedIn R A] {x : A}, IsIntegral R x → ∃ y, (algebraMap R A) y = x
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.coeff.linearMap_apply : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_6} [inst : PartialOrder Γ] [inst_1 : Semiring R] [inst_2 : AddCommMonoid V]
  [inst_3 : Module R V] (g : Γ) (a : HahnSeries Γ V),
  (HahnSeries.coeff.linearMap g) a = (↑(HahnSeries.coeff.addMonoidHom g)).toFun a
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.errorName.inj : ∀ {stx partialId stx_1 partialId_1 : Lean.Syntax},
  Lean.Elab.CompletionInfo.errorName stx partialId = Lean.Elab.CompletionInfo.errorName stx_1 partialId_1 →
    stx = stx_1 ∧ partialId = partialId_1
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- **Alias** of `dimH_subsingleton`. -/
Set.Subsingleton.dimH_zero : ∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Subsingleton → dimH s = 0
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_mul_single_subset : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] [inst_2 : DecidableEq G] (x : AddMonoidAlgebra k G)
  (r : k) (a : G), (x * AddMonoidAlgebra.single a r).coeff.support ⊆ Finset.image (fun x => x + a) x.coeff.support
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
SpectrumRestricts.nnreal_iff_nnnorm : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A} {t : NNReal},
  IsSelfAdjoint a → ‖a‖₊ ≤ t → (SpectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ‖(algebraMap ℝ A) ↑t - a‖₊ ≤ t)
-- Aesop.Search.RuleSelection
Aesop.selectSafeRules : {Q : Type} → [inst : Aesop.Queue Q] → Aesop.Goal → Aesop.SearchM Q (Array (Aesop.IndexMatchResult Aesop.SafeRule))
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation'.d_app : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ' : S' ⟶ R} (d : M.Derivation' φ')
  {X : Dᵒᵖ} (a : ↑(S'.obj X)), d.d ((CategoryTheory.ConcreteCategory.hom (φ'.app X)) a) = 0
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.isoClosure_iSup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Sort u_1} (P : α → CategoryTheory.ObjectProperty C),
  (⨆ a, P a).isoClosure = ⨆ a, (P a).isoClosure
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.lift_insepDegree_bot' : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Cardinal.lift.{v, w} (Field.insepDegree F ↥⊥) = Cardinal.lift.{w, v} (Field.insepDegree F E)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ofMeasurable.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : (s : Set α) → MeasurableSet s → ENNReal) (m0 : m ∅ ⋯ = 0)
  (mU :
    ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
      Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯),
  MeasureTheory.Measure.ofMeasurable m m0 mU =
    { toOuterMeasure := MeasureTheory.inducedOuterMeasure m ⋯ m0, m_iUnion := ⋯, trim_le := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.uniqueHomFromTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (A : CategoryTheory.Mon C) → Unique (CategoryTheory.Mon.trivial C ⟶ A)
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
expNegInvGlue.zero : expNegInvGlue 0 = 0
-- Mathlib.Data.List.Defs
List.permutations'.eq_1 : ∀ {α : Type u_1}, [].permutations' = [[]]
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBase.encard_eq_eRank : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → B.encard = M.eRank
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Restriction of an AddSemigroup hom to an `AddSubsemigroup` of the domain.  -/
AddHom.domRestrict : {M : Type u_1} →
  {σ : Type u_4} →
    [inst : Add M] →
      {N : Type u_5} →
        [inst_1 : Add N] → [inst_2 : SetLike σ M] → [inst_3 : AddMemClass σ M] → (M →ₙ+ N) → (S : σ) → ↥S →ₙ+ N
-- Init.Data.Nat.Lemmas
Nat.pow_le_pow_iff_left : ∀ {a b n : ℕ}, n ≠ 0 → (a ^ n ≤ b ^ n ↔ a ≤ b)
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.LimitBicone.mk : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {F : J → C} → (bicone : CategoryTheory.Limits.Bicone F) → bicone.IsBilimit → CategoryTheory.Limits.LimitBicone F
-- Mathlib.Order.SuccPred.Basic
Order.isMin_iterate_pred_of_eq_of_ne : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α} {n m : ℕ},
  Order.pred^[n] a = Order.pred^[m] a → n ≠ m → IsMin (Order.pred^[n] a)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} (h : t.WF),
  (Std.DTreeMap.Raw.filterMap f t).getKey? k = (t.getKey? k).pfilter fun x h' => (f x (t.get x ⋯)).isSome
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_diffₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑m₂ →
      (Std.DHashMap.Internal.toListModel (↑(m₁.diffₘ m₂)).buckets).Perm
        (List.filter (fun k => !(List.map Sigma.fst (Std.DHashMap.Internal.toListModel (↑m₂).buckets)).contains k.fst)
          (Std.DHashMap.Internal.toListModel (↑m₁).buckets))
-- Mathlib.Order.Filter.IsBounded
Filter.IsCoboundedUnder.of_frequently_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : LinearOrder α] {f : Filter ι} {u : ι → α} {a : α},
  (∃ᶠ (x : ι) in f, u x ≤ a) → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f u
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_tsum : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable β]
  {f : β → α → ENNReal},
  (∀ (i : β), AEMeasurable (f i) μ) → ∫⁻ (a : α), ∑' (i : β), f i a ∂μ = ∑' (i : β), ∫⁻ (a : α), f i a ∂μ
-- Mathlib.NumberTheory.Padics.ValuativeRel
Padic.instCompatibleWithZeroMultiplicativeIntMulValuation : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Padic.mulValuation.Compatible
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.rightRegular_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (s t : G) (f : G → k),
  (TannakaDuality.FiniteGroup.rightRegular s) f t = f (t * s)
-- Mathlib.Order.Ideal
Order.Cofinal.mk.injEq : ∀ {P : Type u_2} [inst : Preorder P] (carrier : Set P) (isCofinal : IsCofinal carrier) (carrier_1 : Set P)
  (isCofinal_1 : IsCofinal carrier_1),
  ({ carrier := carrier, isCofinal := isCofinal } = { carrier := carrier_1, isCofinal := isCofinal_1 }) =
    (carrier = carrier_1)
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.image_symm : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β),
  Set.image ⇑h.symm = Set.preimage ⇑h
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.Finite.toFinset_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Set α} (hs : s.Finite) (ht : t.Finite)
  (hf : optParam (s * t).Finite ⋯), hf.toFinset = hs.toFinset * ht.toFinset
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.map_lift_equalizerComparison : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.Limits.HasEqualizer f g] [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)]
  {Z : C} {h : Z ⟶ X} (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.equalizer.lift h w))
      (CategoryTheory.Limits.equalizerComparison f g G) =
    CategoryTheory.Limits.equalizer.lift (G.map h) ⋯
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCancelCommMonoid : {α : Type u_1} → [CancelCommMonoid α] → CancelCommMonoid (Lex α)
-- Mathlib.Order.RelIso.Basic
RelIso.instFunLike : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → FunLike (r ≃r s) α β
-- Mathlib.Algebra.Algebra.Defs
/-- The identity map inducing an `Algebra` structure.  -/
Algebra.id : (R : Type u) → [inst : CommSemiring R] → Algebra R R
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centerToMulOpposite_symm_apply_coe : ∀ {R : Type u} [inst : NonAssocSemiring R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)),
  ↑(Subsemiring.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
-- Init.Data.String.Lemmas.Modify
String.map_id : ∀ {s : String}, String.map id s = s
-- Mathlib.Algebra.GroupWithZero.Action.Opposite
MulOpposite.instDistribMulAction : {M : Type u_1} →
  {α : Type u_2} → [inst : Monoid M] → [inst_1 : AddMonoid α] → [DistribMulAction M α] → DistribMulAction M αᵐᵒᵖ
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.signAux2.eq_def : ∀ {α : Type u} [inst : DecidableEq α] (x : List α) (x_1 : Equiv.Perm α),
  Equiv.Perm.signAux2 x x_1 =
    match x, x_1 with
    | [], x => 1
    | x :: l, f => if x = f x then Equiv.Perm.signAux2 l f else -Equiv.Perm.signAux2 l (Equiv.swap x (f x) * f)
-- Mathlib.SetTheory.Ordinal.Arithmetic
_private.Mathlib.SetTheory.Ordinal.Arithmetic.0.Ordinal.add_lt_add_iff_left' : ∀ (a : Ordinal.{u_4}) {b c : Ordinal.{u_4}}, a + b < a + c ↔ b < c
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The Legendre symbol `legendreSym p a = 1` if there is a solution in `ℤ/pℤ`
of the equation `x^2 - a*y^2 = 0` with `y ≠ 0`.  -/
legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {a : ℤ},
  ↑a ≠ 0 → ∀ {x y : ZMod p}, y ≠ 0 → x ^ 2 - ↑a * y ^ 2 = 0 → legendreSym p a = 1
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.generatedBy_eq : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} {tY : TopologicalSpace Y}
  [Topology.IsGeneratedBy X Y], TopologicalSpace.generatedBy X = tY
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.id.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A),
  M.id = { hom := CategoryTheory.CategoryStruct.id M.X, isModHom := ⋯ }
-- Mathlib.FieldTheory.NormalizedTrace
Algebra.normalizedTrace_algebraMap : ∀ (F : Type u_3) (E : Type u_4) (K : Type u_5) [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra E K] [inst_5 : Algebra F K] [inst_6 : IsScalarTower F E K]
  [inst_7 : Algebra.IsIntegral F E] [inst_8 : Algebra.IsIntegral F K] [inst_9 : CharZero F],
  Algebra.normalizedTrace F K ∘ₗ ↑F (Algebra.linearMap E K) = Algebra.normalizedTrace F E
-- Lean.Environment
Lean.EnvExtension.AsyncMode.sync.sizeOf_spec : sizeOf Lean.EnvExtension.AsyncMode.sync = 1
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.isStronglyCartesian_homCartesianLift : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {R S : 𝒮}
  (a : ↑(F.obj { as := Opposite.op S })) (f : R ⟶ S),
  (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsStronglyCartesian f
    (CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift a f)
-- Init.Data.Vector.Lemmas
Vector.sum_reverse : ∀ {α : Type u_1} {n : ℕ} [inst : Zero α] [inst_1 : Add α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.Commutative fun x1 x2 => x1 + x2] [Std.LawfulLeftIdentity (fun x1 x2 => x1 + x2) 0] (xs : Vector α n),
  xs.reverse.sum = xs.sum
-- Mathlib.Topology.Category.DeltaGenerated
/-- **Alias** of `TopCat.toDeltaGenerated`.

---

The faithful (but not full) functor taking each topological space to its delta-generated
coreflection.  -/
DeltaGenerated.topToDeltaGenerated : CategoryTheory.Functor TopCat DeltaGenerated
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.getVert_cons_succ : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {n : ℕ} (p : G.Walk v w) (h : G.Adj u v),
  (SimpleGraph.Walk.cons h p).getVert (n + 1) = p.getVert n
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.encard_sdiff_add_encard_of_subset`. -/
Set.encard_diff_add_encard_of_subset : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → (t \ s).encard + s.encard = t.encard
-- Init.Internal.Order.Basic
Lean.Order.monotone_exceptTRun : ∀ {γ : Sort u_1} {m : Type u_2 → Type u_3} {ε α : Type u_2} [inst : Lean.Order.PartialOrder γ] [Monad m]
  [inst_2 : (α : Type u_2) → Lean.Order.PartialOrder (m α)] (f : γ → ExceptT ε m α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => (f x).run
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- The equiv `FractionalIdeal R⁰ K ≃+* FractionalIdeal S⁰ L`
induced by a ring isomorphism `f : R ≃+* S`.  -/
FractionalIdeal.ringEquivOfRingEquiv : {R : Type u_5} →
  {S : Type u_6} →
    (K : Type u_7) →
      (L : Type u_8) →
        [inst : CommRing R] →
          [IsDomain R] →
            [inst_2 : CommRing S] →
              [IsDomain S] →
                [inst_4 : CommRing K] →
                  [inst_5 : CommRing L] →
                    [inst_6 : Algebra R K] →
                      [inst_7 : Algebra S L] →
                        [IsFractionRing R K] →
                          [IsFractionRing S L] →
                            R ≃+* S → FractionalIdeal (nonZeroDivisors R) K ≃+* FractionalIdeal (nonZeroDivisors S) L
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.finrank_eq_pow : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [ExpChar F q]
  [IsPurelyInseparable F E] [FiniteDimensional F E], ∃ n, Module.finrank F E = q ^ n
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The property of being `C^n`, initially defined in terms of the Fréchet derivative, can be
reformulated in terms of the one-dimensional derivative.  -/
contDiff_nat_iff_iteratedDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ},
  ContDiff 𝕜 (↑n) f ↔ (∀ m ≤ n, Continuous (iteratedDeriv m f)) ∧ ∀ m < n, Differentiable 𝕜 (iteratedDeriv m f)
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
le_emultiplicity_iff_replicate_subperm_primeFactorsList : ∀ {a b n : ℕ}, Nat.Prime a → b ≠ 0 → (↑n ≤ emultiplicity a b ↔ (List.replicate n a).Subperm b.primeFactorsList)
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_le_toZ : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i j : ι}, toZ i0 i ≤ toZ i0 j ↔ i ≤ j
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.EqCnstr.pp : Lean.Meta.Grind.Arith.Cutsat.EqCnstr → Lean.Meta.Grind.GoalM Lean.MessageData
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.int_sub : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (m : ℤ), LiouvilleWith p (↑m - x)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- Any functor out of the WalkingReflexivePair yields a reflexive pair  -/
CategoryTheory.Limits.reflexivePair.to_isReflexivePair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C},
  CategoryTheory.IsReflexivePair (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
    (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)
-- Lean.Data.Lsp.Diagnostics
/-- Extension: whether this diagnostic should not be displayed as a regular diagnostic in the editor.
In VS Code, this means that the diagnostic does not have a squiggly and is not displayed in
the InfoView under 'All Messages', but it is still displayed under 'Messages'.
Defaults to `false`.
 -/
Lean.Lsp.DiagnosticWith.isSilent? : {α : Type} → Lean.Lsp.DiagnosticWith α → Option Bool
-- Mathlib.SetTheory.Cardinal.Finsupp
Cardinal.mk_finsupp_of_infinite : ∀ (α β : Type u) [Infinite α] [inst : Zero β] [Nontrivial β], Cardinal.mk (α →₀ β) = max (Cardinal.mk α) (Cardinal.mk β)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_some_get!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {a : α},
  t.contains a = true → t.get? a = some (t.get! a)
-- Mathlib.CategoryTheory.Abelian.Images
/-- The projection onto the coimage.  -/
CategoryTheory.Abelian.coimage.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] →
              P ⟶ CategoryTheory.Abelian.coimage f
-- Init.Meta.Defs
Lean.Syntax.instEmptyCollectionSepArray : {sep : String} → EmptyCollection (Lean.Syntax.SepArray sep)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_diff_iff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ \ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∈ t₂
-- Mathlib.LinearAlgebra.Complex.Module
/-- A universal property of the complex numbers, providing a unique `ℂ →ₐ[ℝ] A` for every element
of `A` which squares to `-1`.

This can be used to embed the complex numbers in the `Quaternion`s.

This isomorphism is named to match the very similar `Zsqrtd.lift`.  -/
Complex.lift : {A : Type u_1} → [inst : Ring A] → [inst_1 : Algebra ℝ A] → { I' // I' * I' = -1 } ≃ (ℂ →ₐ[ℝ] A)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- In a topological vector space, the topology is generated by a single seminorm `p` iff
the unit ball for this seminorm is a bounded neighborhood of `0`.  -/
withSeminorms_iff_mem_nhds_isVonNBounded : ∀ {𝕜 : Type u_2} {E : Type u_6} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {p : Seminorm 𝕜 E},
  (WithSeminorms fun x => p) ↔ p.ball 0 1 ∈ nhds 0 ∧ Bornology.IsVonNBounded 𝕜 (p.ball 0 1)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.epi_δ_of_isZero : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (n : ℕ),
  CategoryTheory.Limits.IsZero (groupHomology X.X₂ n) → CategoryTheory.Epi (groupHomology.δ hX (n + 1) n ⋯)
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.stdout : Lean.Lsp.Ipc.IpcM IO.FS.Stream
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.FourierMotzkinData.mk.inj : ∀ {var : ℕ} {irrelevant : List Lean.Elab.Tactic.Omega.Fact}
  {lowerBounds upperBounds : List (Lean.Elab.Tactic.Omega.Fact × ℤ)} {lowerExact upperExact : Bool} {var_1 : ℕ}
  {irrelevant_1 : List Lean.Elab.Tactic.Omega.Fact}
  {lowerBounds_1 upperBounds_1 : List (Lean.Elab.Tactic.Omega.Fact × ℤ)} {lowerExact_1 upperExact_1 : Bool},
  { var := var, irrelevant := irrelevant, lowerBounds := lowerBounds, upperBounds := upperBounds,
        lowerExact := lowerExact, upperExact := upperExact } =
      { var := var_1, irrelevant := irrelevant_1, lowerBounds := lowerBounds_1, upperBounds := upperBounds_1,
        lowerExact := lowerExact_1, upperExact := upperExact_1 } →
    var = var_1 ∧
      irrelevant = irrelevant_1 ∧
        lowerBounds = lowerBounds_1 ∧
          upperBounds = upperBounds_1 ∧ lowerExact = lowerExact_1 ∧ upperExact = upperExact_1
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Subshift.mk.inj : ∀ {A : Type u_1} {inst : TopologicalSpace A} {G : Type u_2} {inst_1 : AddMonoid G} {carrier : Set (G → A)}
  {isClosed : IsClosed carrier} {mapsTo : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.shift g) carrier carrier}
  {carrier_1 : Set (G → A)} {isClosed_1 : IsClosed carrier_1}
  {mapsTo_1 : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.shift g) carrier_1 carrier_1},
  { carrier := carrier, isClosed := isClosed, mapsTo := mapsTo } =
      { carrier := carrier_1, isClosed := isClosed_1, mapsTo := mapsTo_1 } →
    carrier = carrier_1
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr_trans_hom : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} {x y z : AlgebraicGeometry.Scheme.Pullback.Triplet f g}
  (e : x = y) (e' : y = z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).hom
      (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e').hom =
    (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr ⋯).hom
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Universal property of the intersection of two pre-`1`-hypercovers.  -/
CategoryTheory.PreOneHypercover.interLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          [inst_1 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
            [inst_2 :
                ∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
                  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
                    (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] →
              {G : CategoryTheory.PreOneHypercover S} → G.Hom E → G.Hom F → G.Hom (E.inter F)
-- Mathlib.RepresentationTheory.Submodule
Representation.invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) [Nontrivial V], Nontrivial ↥ρ.invtSubmodule
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_toList : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.toList.isEmpty = t.isEmpty