mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.Basic
/-- Instance needed to define star-linear maps over a commutative star ring
(ex: conjugate-linear maps when R = ℂ).  -/
RingHomInvPair.instStarRingEnd : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : StarRing R], RingHomInvPair (starRingEnd R) (starRingEnd R)
-- Mathlib.Algebra.Homology.Single
ChainComplex.toSingle₀Equiv_symm_apply_f_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {C : ChainComplex V ℕ} {X : V} (f : C.X 0 ⟶ X)
  (hf : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0), ((C.toSingle₀Equiv X).symm ⟨f, hf⟩).f 0 = f
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.mapCoeffs.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A],
  Differential.mapCoeffs = PolynomialModule.equivPolynomialSelf.compDer Differential.deriv.mapCoeffs
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Metric.cauchy_iff : ∀ {α : Type u} [inst : PseudoMetricSpace α] {f : Filter α},
  Cauchy f ↔ f.NeBot ∧ ∀ ε > 0, ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, dist x y < ε
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVPred.eval_bin : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {a : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr a}
  {op : Std.Tactic.BVDecide.BVBinPred} {rhs : Std.Tactic.BVDecide.BVExpr a},
  Std.Tactic.BVDecide.BVPred.eval assign (Std.Tactic.BVDecide.BVPred.bin lhs op rhs) =
    op.eval (Std.Tactic.BVDecide.BVExpr.eval assign lhs) (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
-- Init.Sym.DSimp.DSimprocDSL
/-- Pre-processing simproc chain.  -/
Lean.Parser.Command.symDSimpFieldPre : Lean.ParserDescr
-- Mathlib.Order.SuccPred.Limit
Order.not_isSuccPrelimit_of_isSuccArchimedean : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] [NoMinOrder α],
  ¬Order.IsSuccPrelimit a
-- Mathlib.Data.Set.Function
Set.mapsTo_iff_image_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.MapsTo f s t ↔ f '' s ⊆ t
-- Mathlib.Algebra.Order.Quantale
Quantale.mul_iSup_distrib : ∀ {α : Type u_1} {ι : Type u_2} {x : α} {f : ι → α} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α],
  x * ⨆ i, f i = ⨆ i, x * f i
-- Init.Data.Int.Order
Int.le_add_one : ∀ {a b : ℤ}, a ≤ b → a ≤ b + 1
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.of.sizeOf_spec : ∀ (carrier : Type u) [semiring : Semiring carrier],
  sizeOf (SemiRingCat.of carrier) = 1 + sizeOf carrier + sizeOf semiring
-- Mathlib.Algebra.Module.Submodule.Finsupp
/-- In a ring, sets acts on submodules.  -/
Submodule.pointwiseSetDistribMulAction : {R : Type u_2} →
  {M : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → [SMulCommClass R R M] → DistribMulAction (Set R) (Submodule R M)
-- Lean.OriginalConstKind
/-- Returns the kind of the declaration as originally declared instead of as exported. This information
is stored by `Lean.addDecl` and may be inaccurate if that function was circumvented. Returns `none`
if the declaration was not found.
 -/
Lean.getOriginalConstKind? : Lean.Environment → Lean.Name → Option Lean.ConstantKind
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (S : AddSubsemigroup N),
  AddSubsemigroup.comap f S = { carrier := ⇑f ⁻¹' ↑S, add_mem' := ⋯ }
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x`, `0 x = 0`, and
`(n • f) x = n • f x` is a commutative additive monoid if `β` is a commutative additive monoid.  -/
FunLike.addCommMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : AddCommMonoid β] →
                [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply ℕ F α β] → AddCommMonoid F
-- Mathlib.Data.Nat.Find
Nat.find_eq_iff : ∀ {m : ℕ} {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), Nat.find h = m ↔ p m ∧ ∀ n < m, ¬p n
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- Use the more general result `emultiplicity_map_eq_ramificationIdx'_mul`.
This is a helper lemma.  -/
_private.Mathlib.NumberTheory.RamificationInertia.Ramification.0.Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx'_mul_of_prime : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  [IsDedekindDomain R] [FaithfulSMul R S] {v : Ideal R} {w : Ideal S} {p : Ideal R},
  Irreducible v →
    Prime p →
      Irreducible w →
        w ≠ ⊥ →
          ∀ [w.LiesOver v], emultiplicity w (Ideal.map (algebraMap R S) p) = ↑(v.ramificationIdx' w) * emultiplicity v p
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instSetLike : {α : Type u_1} → [inst : LE α] → SetLike (UpperSet α) α
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.RestrictionCoextensionAdj.counit'_app : ∀ {R : Type u₁} {S : Type u₂} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S) (X : ModuleCat R),
  (ModuleCat.RestrictionCoextensionAdj.counit' f).app X =
    ModuleCat.ofHom { toFun := fun g => ((ModuleCat.CoextendScalars.equiv f X) g) 1, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.dist.eq_3 : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (x_2 : X) (y : Y),
  Metric.Sum.dist (Sum.inl x_2) (Sum.inr y) = dist x_2 ⋯.some + 1 + dist ⋯.some y
-- Mathlib.Order.Closure
LowerAdjoint.closure_iUnion₂_closure : ∀ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α]
  (l : LowerAdjoint SetLike.coe) (f : (i : ι) → κ i → α),
  l.toFun (⋃ i, ⋃ j, ↑(l.toFun ↑(f i j))) = l.toFun (⋃ i, ⋃ j, ↑(f i j))
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.comp_homologyπ_eq_zero_iff_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C} {A : C} (z₂ : A ⟶ S.cycles),
  CategoryTheory.CategoryStruct.comp z₂ S.homologyπ = 0 ↔
    ∃ A' π,
      ∃ (_ : CategoryTheory.Epi π),
        ∃ x₁, CategoryTheory.CategoryStruct.comp π z₂ = CategoryTheory.CategoryStruct.comp x₁ S.toCycles
-- Mathlib.Order.Filter.Map
Filter.seq_mono : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : Filter (α → β)} {g₁ g₂ : Filter α}, f₁ ≤ f₂ → g₁ ≤ g₂ → f₁.seq g₁ ≤ f₂.seq g₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_vsub_midpoint : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ p₂ p₃ p₄ : P),
  midpoint R p₁ p₂ -ᵥ midpoint R p₃ p₄ = midpoint R (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatchAt_iff_isLongestMatchAt_beq : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt c pos pos' ↔
    String.Slice.Pattern.Model.IsLongestMatchAt (fun x => x == c) pos pos'
-- Init.Data.Int.Basic
Int.ofNat_eq_natCast : ∀ (n : ℕ), Int.ofNat n = ↑n
-- Lean.Data.JsonRpc
/-- Generic version of `Message.notification`.

A notification message. A processed notification message must not send a response back. They work like events.

- [JSON-RPC](https://www.jsonrpc.org/specification#notification)
- [LSP](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#notificationMessage).
 -/
Lean.JsonRpc.Notification : Type u → Type u
-- Mathlib.Order.Disjoint
isComplemented_top : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α], IsComplemented ⊤
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.contains_eq_isSome_get?ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [Std.LawfulBEqOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → Std.DTreeMap.Internal.Impl.contains k t = (t.get?ₘ k).isSome
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.finset_sum : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid β] {ι : Type u_9} {s : Finset ι}
  {f : ι → α → β}, (∀ i ∈ s, HasCompactSupport (f i)) → HasCompactSupport (∑ i ∈ s, f i)
-- Mathlib.Order.SuccPred.Limit
Order.mem_range_pred_or_isPredPrelimit : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] (a : α),
  a ∈ Set.range Order.pred ∨ Order.IsPredPrelimit a
-- Mathlib.SetTheory.ZFC.Class
/-- **Alias** of `Class.coe_sdiff`. -/
Class.coe_diff : ∀ (x y : ZFSet.{u}), ↑(x \ y) = ↑x \ ↑y
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.quasicategory_of_from_innerFibrations : ∀ (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X), SSet.innerFibrations (t.from S) → S.Quasicategory
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsMatching.map : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {M : G.Subgraph} (f : G →g G'),
  Function.Injective ⇑f → M.IsMatching → (SimpleGraph.Subgraph.map f M).IsMatching
-- Init.Data.Vector.Nat
Vector.sum_eq_zero_iff_forall_eq_nat : ∀ {n : ℕ} {xs : Vector ℕ n}, xs.sum = 0 ↔ ∀ x ∈ xs, x = 0
-- Mathlib.RingTheory.Ideal.GoingDown
/-- An `R`-algebra `S` has the going down property if and only if generalizations lift
along `Spec S → Spec R`.  -/
Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.HasGoingDown R S ↔ GeneralizingMap (PrimeSpectrum.comap (algebraMap R S))
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
/-- The function on `(Fin 2 → ℤ)` whose sum defines an Eisenstein series.  -/
EisensteinSeries.eisSummand : ℤ → (Fin 2 → ℤ) → UpperHalfPlane → ℂ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_minKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t → t.minKey?.isSome = true
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_set_iInter_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VAdd α β] (a : α) (t : ι → Set β), a +ᵥ ⋂ i, t i ⊆ ⋂ i, a +ᵥ t i
-- Mathlib.Data.Nat.Bits
Nat.div2_val : ∀ (n : ℕ), n.div2 = n / 2
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Set
_private.Std.Data.Iterators.Lemmas.Consumers.Monadic.Set.0.Std.IterM.toExtTreeSet.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] [inst_2 : Std.IteratorLoop α m m]
  (it : Std.IterM m β) (cmp : β → β → Ordering) [inst_3 : Std.TransCmp cmp],
  it.toExtTreeSet cmp = Std.IterM.fold (fun acc a => acc.insert a) ∅ it
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.one_le_extendedHom_iff : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [inst_12 : Algebra K L]
  [inst_13 : Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsDedekindDomain A]
  [IsDedekindDomain B], I ≠ 0 → (1 ≤ (FractionalIdeal.extendedHom L B) I ↔ 1 ≤ I)
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_ssubset_toFinset : ∀ {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite}, hs.toFinset ⊂ ht.toFinset ↔ s ⊂ t
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousAt.lowerHemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α}
  (s : Set α), LowerHemicontinuousAt f x → LowerHemicontinuousWithinAt f s x
-- Mathlib.Algebra.Category.CoalgCat.Monoidal
CoalgCat.tensorObj_isModule : ∀ (R : Type u) [inst : CommRing R] (X Y : CoalgCat R),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).isModule = TensorProduct.instModule
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [CategoryTheory.EnoughInjectives C] [CategoryTheory.Mono f] (n₀ n₁ : ℤ),
  (∀ i ≤ n₀, QuasiIsoAt f i) →
    autoParam (n₀ + 1 = n₁) CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step._auto_1✝ →
      ∃ F,
        CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.quasiIsoLE✝ n₁ F ∧
          CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIsoLE✝ n₀ F
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.neg_vadd_finset_distrib : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] (a : α) (s : Finset α),
  -(a +ᵥ s) = AddOpposite.op (-a) +ᵥ -s
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.StrongTrans G H) {a : B} {a' : C}
  (f : a' ⟶ G.obj a),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.id a)).hom)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapId a))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapId a) (θ.app a)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor (θ.app a)).hom)
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor (θ.app a)).inv))
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- An iterated biproduct is a biproduct over a sigma type.  -/
CategoryTheory.Limits.biproductBiproductIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_3} →
        (f : ι → Type u_2) →
          (g : (i : ι) → f i → C) →
            [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBiproduct (g i)] →
              [inst_3 : CategoryTheory.Limits.HasBiproduct fun i => ⨁ g i] →
                (⨁ fun i => ⨁ g i) ≅ ⨁ fun p => g p.fst p.snd
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckStep.noConfusionType : Sort v✝ → DyckStep → DyckStep → Sort v✝
-- Init.Data.List.Basic
List.head?_cons : ∀ {α : Type u} {a : α} {l : List α}, (a :: l).head? = some a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapIso_inverse : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ≅ Y),
  (CategoryTheory.Over.mapIso f).inverse = CategoryTheory.Over.map f.inv
-- Mathlib.Data.Set.Card
Set.ncard_union_eq_iff : ∀ {α : Type u_1} {s t : Set α},
  autoParam s.Finite Set.ncard_union_eq_iff._auto_1 →
    autoParam t.Finite Set.ncard_union_eq_iff._auto_3 → ((s ∪ t).ncard = s.ncard + t.ncard ↔ Disjoint s t)
-- Mathlib.RingTheory.Noetherian.Basic
/-- A linearly-independent family of vectors in a module over a non-trivial ring must be finite if
the module is Noetherian.  -/
LinearIndependent.finite_of_isNoetherian : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  [Nontrivial R] {ι : Type u_5} {v : ι → M}, LinearIndependent R v → Finite ι
-- Mathlib.Topology.MetricSpace.Gluing
Metric.le_glueDist_inr_inl : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (Φ : Z → X) (Ψ : Z → Y) (ε : ℝ)
  (x : Y) (y : X), ε ≤ Metric.glueDist Φ Ψ ε (Sum.inr x) (Sum.inl y)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.one_of_succ : ∀ {𝕜 : 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 + 1) f → ContDiff 𝕜 1 f
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Fractional operation is a symmetric fractional polymorphism for given VCSP template.  -/
FractionalOperation.IsSymmetricFractionalPolymorphismFor : {D : Type u_1} →
  {C : Type u_2} →
    [inst : AddCommMonoid C] →
      [inst_1 : PartialOrder C] →
        [inst_2 : IsOrderedAddMonoid C] → {m : ℕ} → FractionalOperation D m → ValuedCSP D C → Prop
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.le_pointwise_smul_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ {S T : Subring R}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Init.Data.String.PosRaw
String.Pos.Raw.offsetBy_zero : ∀ {p : String.Pos.Raw}, p.offsetBy 0 = p
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_inter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {h_mem : k ∈ m₁ ∩ m₂}, (m₁ ∩ m₂)[k] = m₁[k]
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_center : ∀ (R : Type u) [inst : NonAssocSemiring R], ↑(Subsemiring.center R) = (NonUnitalSubsemiring.center R).carrier
-- Mathlib.Computability.NFA
NFA.mem_accepts : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α}, x ∈ M.accepts ↔ ∃ S ∈ M.accept, S ∈ M.evalFrom M.start x
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.containsKey_filter : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {f : α → β → Bool} {l : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) =
      if h : Std.Internal.List.containsKey k l = true then
        f (Std.Internal.List.getKey k l h) (Std.Internal.List.getValue k l h)
      else false
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_eq_top : ∀ {R : Type u_2} [inst : NonAssocRing R] {S : Subring Rᵐᵒᵖ}, S.unop = ⊤ ↔ S = ⊤
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Composition as a linear map.  -/
CompactlySupportedContinuousMap.compLinearMap : {β : Type u_3} →
  {γ : Type u_4} →
    {δ : Type u_5} →
      [inst : TopologicalSpace β] →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : TopologicalSpace δ] →
            [inst_3 : AddCommMonoid δ] →
              [inst_4 : ContinuousAdd δ] →
                {R : Type u_6} →
                  [inst_5 : Semiring R] →
                    [inst_6 : Module R δ] →
                      [inst_7 : ContinuousConstSMul R δ] →
                        CocompactMap β γ → CompactlySupportedContinuousMap γ δ →ₗ[R] CompactlySupportedContinuousMap β δ
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Composing `f : Lp E p μ` with `L : E →L[𝕜] F`, seen as a continuous `𝕜`-linear map on
`Lp E p μ`. See also the similar
* `LinearMap.compLeft` for functions,
* `ContinuousLinearMap.compLeftContinuous` for continuous functions,
* `ContinuousLinearMap.compLeftContinuousBounded` for bounded continuous functions,
* `ContinuousLinearMap.compLeftContinuousCompact` for continuous functions on compact spaces.
 -/
ContinuousLinearMap.compLpL : {α : Type u_1} →
  {E : Type u_4} →
    {F : Type u_5} →
      {m : MeasurableSpace α} →
        (p : ENNReal) →
          (μ : MeasureTheory.Measure α) →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedAddCommGroup F] →
                {𝕜 : Type u_6} →
                  {𝕜' : Type u_7} →
                    [inst_2 : NontriviallyNormedField 𝕜] →
                      [inst_3 : NontriviallyNormedField 𝕜'] →
                        [inst_4 : NormedSpace 𝕜 E] →
                          [inst_5 : NormedSpace 𝕜' F] →
                            {σ : 𝕜 →+* 𝕜'} →
                              [RingHomIsometric σ] →
                                [inst_7 : Fact (1 ≤ p)] →
                                  (E →SL[σ] F) → ↥(MeasureTheory.Lp E p μ) →SL[σ] ↥(MeasureTheory.Lp F p μ)
-- Mathlib.Algebra.Torsor.Defs
Equiv.pointReflection.eq_1 : ∀ {G : Type u_3} {P : Type u_4} [inst : AddGroup G] [inst_1 : AddTorsor G P] (x : P),
  Equiv.pointReflection x = (Equiv.constVSub x).trans (Equiv.vaddConst x)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.rotateR_node : ∀ {α : Type u_1} (sz : ℕ) (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α),
  (Ordnode.node sz l x m).rotateR y r = if m.size < Ordnode.ratio * l.size then l.node3R x m y r else l.node4R x m y r
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.pp.oneline : Lean.Option Bool
-- Mathlib.Algebra.Lie.Basic
/-- A Lie algebra is a module with compatible product, known as the bracket, satisfying the Jacobi
identity. Forgetting the scalar multiplication, every Lie algebra is a Lie ring.  -/
LieAlgebra : (R : Type u) → (L : Type v) → [CommRing R] → [LieRing L] → Type (max u v)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_injective : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), Function.Injective ⇑(Polynomial.monomial n)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
/-- A tagged partition is said to be a Henstock partition if for each `J ∈ π`, the tag of `J`
belongs to `J.Icc`.  -/
BoxIntegral.TaggedPrepartition.IsHenstock : {ι : Type u_1} → {I : BoxIntegral.Box ι} → BoxIntegral.TaggedPrepartition I → Prop
-- Mathlib.LinearAlgebra.Finsupp.LSum
/-- A surjective linear map to finitely supported functions has a splitting.  -/
LinearMap.splittingOfFinsuppSurjective : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {α : Type u_4} → (f : M →ₗ[R] α →₀ R) → Function.Surjective ⇑f → (α →₀ R) →ₗ[R] M
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.setIntegral_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] {f : γ → E} {s : Set γ},
  MeasurableSet s →
    MeasureTheory.IntegrableOn f s ((η.comp κ) a) →
      ∫ (z : γ) in s, f z ∂(η.comp κ) a = ∫ (x : β), ∫ (y : γ) in s, f y ∂η x ∂κ a
-- Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureCofibrant
HomotopicalAlgebra.CofibrantObject.instIsConnectedLeftResolutionWeakEquivalencesLocalizerMorphism : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] (X : C),
  CategoryTheory.IsConnected ((HomotopicalAlgebra.CofibrantObject.localizerMorphism C).LeftResolution X)
-- Mathlib.Order.Shrink
instLinearOrderShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [LinearOrder α] → LinearOrder (Shrink.{u, u_1} α)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsTriangulatedBounded : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), t.bounded.IsTriangulated