mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
PresheafOfModules.pushforward₀Obj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (R : CategoryTheory.Functor Dᵒᵖ RingCat) (M : PresheafOfModules R) {X Y : Cᵒᵖ}
  (f : X ⟶ Y), (PresheafOfModules.pushforward₀Obj F R M).map f = M.map (F.op.map f)
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.map_equiv : ∀ {Ω : Type u_1} {E : Type u_2} {F : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E]
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace ℝ F] [inst_6 : MeasurableSpace F] [BorelSpace F],
  ProbabilityTheory.HasGaussianLaw X P → ∀ (L : E ≃L[ℝ] F), ProbabilityTheory.HasGaussianLaw (⇑L ∘ X) P
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get?ₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α fun x => β) (k : α),
  Std.DTreeMap.Internal.Impl.Const.get?ₘ l k =
    Std.DTreeMap.Internal.Impl.applyCell k l fun c x => Std.DTreeMap.Internal.Cell.Const.get? c
-- Mathlib.RingTheory.Flat.Equalizer
/-- The canonical map `M ⊗[R] eq(f, g) →ₗ[R] eq(𝟙 ⊗ f, 𝟙 ⊗ g)`.  -/
LinearMap.tensorEqLocus : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    {N : Type u_4} →
                      {P : Type u_5} →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : AddCommGroup P] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module R P] →
                                (f g : N →ₗ[R] P) →
                                  TensorProduct R M ↥(f.eqLocus g) →ₗ[S]
                                    ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus
                                        ((TensorProduct.AlgebraTensorModule.lTensor S M) g))
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodePi.match_5.eq_2 : ∀ (motive : (n : ℕ) → (f : Fin n → ℕ) → ((i : Fin n) → Fin (f i)) → Sort u_1) (n : ℕ) (f : Fin (n + 1) → ℕ)
  (x : (i : Fin (n + 1)) → Fin (f i)) (h_1 : (x : Fin 0 → ℕ) → (x_1 : (i : Fin 0) → Fin (x i)) → motive 0 x x_1)
  (h_2 : (n : ℕ) → (f : Fin (n + 1) → ℕ) → (x : (i : Fin (n + 1)) → Fin (f i)) → motive n.succ f x),
  (match n.succ, f, x with
    | 0, x, x_1 => h_1 x x_1
    | n.succ, f, x => h_2 n f x) =
    h_2 n f x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_erase_eq_of_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α},
  (∀ {km : α}, t.minKey? = some km → ¬compare k km = Ordering.eq) →
    (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey? = t.minKey?
-- Mathlib.Topology.UrysohnsLemma
/-- A continuous function `f : X → ℝ` such that

* `0 ≤ f x ≤ 1` for all `x`;
* `f` equals zero on `c.C` and equals one outside of `c.U`;
 -/
Urysohns.CU.lim : {X : Type u_1} → [inst : TopologicalSpace X] → {P : Set X → Set X → Prop} → Urysohns.CU P → X → ℝ
-- Mathlib.Data.ENNReal.Basic
ENNReal.instNoZeroDivisors : NoZeroDivisors ENNReal
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
jacobiTheta_two_add : ∀ (τ : ℂ), jacobiTheta (2 + τ) = jacobiTheta τ
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A bounded variation function has a limit at `+∞`.  -/
BoundedVariationOn.exists_tendsto_atTop : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [CompleteSpace E]
  [hE : Nonempty E] {f : α → E} {s : Set α},
  BoundedVariationOn f s → ∃ l, Filter.Tendsto f (Filter.principal s ⊓ Filter.atTop) (nhds l)
-- Lean.Parser.Do
Lean.Parser.Term.doAssert.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Nat.Lemmas
Nat.sub_lt_succ : ∀ (a b : ℕ), a - b < a.succ
-- Mathlib.Tactic.FailIfNoProgress
_private.Mathlib.Tactic.FailIfNoProgress.0.Mathlib.Tactic.lctxIsDefEq.match_1.splitter : (motive : List (Option Lean.LocalDecl) → List (Option Lean.LocalDecl) → Sort u_1) →
  (x x_1 : List (Option Lean.LocalDecl)) →
    ((l₁ l₂ : List (Option Lean.LocalDecl)) → motive (none :: l₁) l₂) →
      ((l₁ l₂ : List (Option Lean.LocalDecl)) →
          (∀ (l₁_1 : List (Option Lean.LocalDecl)), l₁ = none :: l₁_1 → False) → motive l₁ (none :: l₂)) →
        ((d₁ : Lean.LocalDecl) →
            (l₁ : List (Option Lean.LocalDecl)) →
              (d₂ : Lean.LocalDecl) → (l₂ : List (Option Lean.LocalDecl)) → motive (some d₁ :: l₁) (some d₂ :: l₂)) →
          (Unit → motive [] []) →
            ((x x_2 : List (Option Lean.LocalDecl)) →
                (∀ (l₁ : List (Option Lean.LocalDecl)), x = none :: l₁ → False) →
                  (∀ (l₂ : List (Option Lean.LocalDecl)), x_2 = none :: l₂ → False) →
                    (∀ (d₁ : Lean.LocalDecl) (l₁ : List (Option Lean.LocalDecl)) (d₂ : Lean.LocalDecl)
                        (l₂ : List (Option Lean.LocalDecl)), x = some d₁ :: l₁ → x_2 = some d₂ :: l₂ → False) →
                      (x = [] → x_2 = [] → False) → motive x x_2) →
              motive x x_1
-- Mathlib.FieldTheory.Relrank
Subfield.relrank_comap_comap_eq_relrank_of_le : ∀ {E : Type v} [inst : Field E] (A B : Subfield E) {L : Type v} [inst_1 : Field L] (f : L →+* E),
  B ≤ f.fieldRange → (Subfield.comap f A).relrank (Subfield.comap f B) = A.relrank B
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.secondMap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {U : C} (R : CategoryTheory.Presieve U) (P : CategoryTheory.Functor Cᵒᵖ A)
  [inst_2 : CategoryTheory.Limits.HasProducts A] [inst_3 : CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Presheaf.secondMap R P =
    CategoryTheory.Limits.Pi.lift fun x =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst)) x.2)
        (P.map (CategoryTheory.Limits.pullback.snd ↑x.1.snd ↑x.2.snd).op)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace_apply : ∀ (K : Type u_1) [inst : Field K] (x : NumberField.mixedEmbedding.realMixedSpace K),
  (NumberField.mixedEmbedding.homeoRealMixedSpacePolarSpace K) x =
    (fun w => if hw : w.IsReal then x.1 ⟨w, hw⟩ else (x.2 ⟨w, ⋯⟩).1, fun w => (x.2 w).2)
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.posGT_offset : ∀ {s : String.Slice} {p : s.Pos} {h : p.offset < s.rawEndPos}, s.posGT p.offset h = p.next ⋯
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesColimitsOfSize.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          autoParam
              ({J : Type w} → [inst_2 : CategoryTheory.Category.{w', w} J] → CategoryTheory.CreatesColimitsOfShape J F)
              CategoryTheory.CreatesColimitsOfSize.CreatesColimitsOfShape._autoParam →
            CategoryTheory.CreatesColimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Mathlib.RingTheory.FractionalIdeal.Basic
/-- `(1 : FractionalIdeal S P)` is defined as the R-submodule `f(R) ≤ P`.

However, this is not definitionally equal to `1 : Submodule R P`,
which is proved in the actual `simp` lemma `coe_one`.  -/
FractionalIdeal.coe_one_eq_coeSubmodule_top : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  ↑1 = IsLocalization.coeSubmodule P ⊤
-- Init.Data.BitVec.Bitblast
BitVec.getMsbD_sdiv : ∀ {w i : ℕ} {x y : BitVec w},
  (x.sdiv y).getMsbD i =
    match x.msb, y.msb with
    | false, false => (x / y).getMsbD i
    | false, true => (-(x / -y)).getMsbD i
    | true, false => (-(-x / y)).getMsbD i
    | true, true => (-x / -y).getMsbD i
-- Lean.Compiler.IR.Basic
Lean.IR.Alt.brecOn.go : {motive_1 : Lean.IR.Alt → Sort u} →
  {motive_2 : Lean.IR.FnBody → Sort u} →
    {motive_3 : Array Lean.IR.Alt → Sort u} →
      {motive_4 : List Lean.IR.Alt → Sort u} →
        (t : Lean.IR.Alt) →
          ((t : Lean.IR.Alt) → t.below → motive_1 t) →
            ((t : Lean.IR.FnBody) → t.below → motive_2 t) →
              ((t : Array Lean.IR.Alt) → Lean.IR.Alt.below_1 t → motive_3 t) →
                ((t : List Lean.IR.Alt) → Lean.IR.Alt.below_2 t → motive_4 t) → motive_1 t ×' t.below
-- Mathlib.Order.Interval.Set.Nat
Set.ncard_Ico_nat : ∀ (a b : ℕ), (Set.Ico a b).ncard = b - a
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
/-- Class of Id maps  -/
MonoidHom.CompTriple.IsId : {M : Type u_1} → [inst : Monoid M] → (M →* M) → Prop
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_apply_le' : ∀ {α : Type u_2} {M : Type u_3} [inst : LE M] [inst_1 : Zero M] {s : Set α} {f : α → M} {a : α} {y : M},
  (a ∈ s → f a ≤ y) → (a ∉ s → 0 ≤ y) → s.indicator f a ≤ y
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalLevelMVarId : Lean.Meta.ReduceEval Lean.LevelMVarId
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of `Order.not_isSuccLimit_of_isSuccArchimedean`. -/
Order.not_isSuccLimit : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α], ¬Order.IsSuccLimit a
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- A variant of the Yoneda lemma for sheaves with a raise in the universe level.  -/
CategoryTheory.GrothendieckTopology.uliftYonedaOpCompCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] →
        (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).op.comp CategoryTheory.coyoneda ≅
          (CategoryTheory.evaluation Cᵒᵖ (Type (max v v'))).comp
            (((CategoryTheory.Functor.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max v v'))
                      (Type (max (max v v') u))).obj
                  CategoryTheory.uliftFunctor.{u, max v v'}).comp
              ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Sheaf J (Type (max v v')))
                    (CategoryTheory.Functor Cᵒᵖ (Type (max v v'))) (Type (max (max v v') u))).obj
                (CategoryTheory.sheafToPresheaf J (Type (max v v')))))
-- Mathlib.Data.Pi.Interval
Pi.card_Ioc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
  (Finset.Ioc a b).card = ∏ i, (Finset.Icc (a i) (b i)).card - 1
-- Mathlib.CategoryTheory.Types.Monomorphisms
CategoryTheory.Types.instIsStableUnderCoproductsOfShapeMonomorphismsType : ∀ (T : Type u'), (CategoryTheory.MorphismProperty.monomorphisms (Type u)).IsStableUnderCoproductsOfShape T
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.cofilteredClosure.below.eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  {f : α → C} {motive : (a : C) → CategoryTheory.IsCofiltered.cofilteredClosure f a → Prop} {j j' : C}
  (a : CategoryTheory.IsCofiltered.cofilteredClosure f j) (a_1 : CategoryTheory.IsCofiltered.cofilteredClosure f j')
  (f_1 f' : j ⟶ j'),
  CategoryTheory.IsCofiltered.cofilteredClosure.below a →
    motive j a →
      CategoryTheory.IsCofiltered.cofilteredClosure.below a_1 →
        motive j' a_1 → CategoryTheory.IsCofiltered.cofilteredClosure.below ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderOut : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      (aig : Std.Sat.AIG α) → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig → Std.Sat.AIG.Entrypoint α
-- Mathlib.GroupTheory.FreeGroup.Basic
/-- Two homomorphisms out of a free additive group are equal if they are
equal on generators. See note [partially-applied ext lemmas].  -/
FreeAddGroup.ext_hom : ∀ {α : Type u} {M : Type u_1} [inst : AddMonoid M] (f g : FreeAddGroup α →+ M),
  (∀ (a : α), f (FreeAddGroup.of a) = g (FreeAddGroup.of a)) → f = g
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.closure_preimage : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] (f : E →SL[σ] F) {σ' : 𝕜' →+* 𝕜} [RingHomInvPair σ σ']
  [RingHomIsometric σ] [RingHomIsometric σ'] [CompleteSpace F] [CompleteSpace E],
  Function.Surjective ⇑f → ∀ (s : Set F), closure (⇑f ⁻¹' s) = ⇑f ⁻¹' closure s
-- Init.Data.Ord.Vector
Vector.compareLex_eq_compareLex_toArray : ∀ {α : Type u_1} {n : ℕ} {cmp : α → α → Ordering} {a b : Vector α n},
  Vector.compareLex cmp a b = Array.compareLex cmp a.toArray b.toArray
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.mk₀_comp_mk₀_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z T : C} (f : X ⟶ Y) (g : Y ⟶ Z) {a : M} (ha : a = 0) {d : M}
  (h : CategoryTheory.ShiftedHom Z T d),
  (CategoryTheory.ShiftedHom.mk₀ a ha f).comp ((CategoryTheory.ShiftedHom.mk₀ a ha g).comp h ⋯) ⋯ =
    (CategoryTheory.ShiftedHom.mk₀ a ha (CategoryTheory.CategoryStruct.comp f g)).comp h ⋯
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) {Z : ModuleCat k}
  (h : ModuleCat.of k (G × G × G → ↑B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((groupCohomology.cochainsMap f φ).f 3)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₃ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₃ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsMap₃ f φ) h)
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.of_subsingleton_codomain : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] [Subsingleton ε] {f : α → ε}, MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.strictAntiOn : ∀ {α : Type u} {β : Type v} {s : Set α} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β),
  s.Subsingleton → StrictAntiOn f s
-- Mathlib.Topology.Category.TopCat.Monoidal
/-- The symmetrization map `TopCat.I ⟶ TopCat.I`.  -/
TopCat.I.symm : TopCat.I ⟶ TopCat.I
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- The topology on a linearly ordered group with zero element adjoined is T₅.  -/
WithZeroTopology.t5Space : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀], T5Space Γ₀
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_diff_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.isEmpty = true ↔ ∀ (a : α), a ∉ t
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The boundary of a cell is contained in the union of the base with a finite union of closed
cells of a lower dimension. Use `RelCWComplex.cellFrontier_subset_base_union_finite_closedCell`
instead.  -/
Topology.RelCWComplex.mapsTo : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n),
  ∃ I,
    Set.MapsTo (↑(Topology.RelCWComplex.map n i)) (Metric.sphere 0 1)
      (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(Topology.RelCWComplex.map m j) '' Metric.closedBall 0 1)
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.ofExact_relation : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst_1 : AddCommGroup M₁]
  [inst_2 : Module A M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] [inst_5 : AddCommGroup M₃]
  [inst_6 : Module A M₃] {f : M₁ →ₗ[A] M₂} {g : M₂ →ₗ[A] M₃} (pres₂ : Module.Presentation A M₂) {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g)
  (hg₁ : Submodule.span A (Set.range g₁) = ⊤) (x : pres₂.R ⊕ ι),
  (pres₂.ofExact data hfg hg hg₁).relation x =
    match x with
    | Sum.inl r => pres₂.relation r
    | Sum.inr i => data.lift i
-- Mathlib.Algebra.Order.Group.PosPart
negPart_eq_neg : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddGroup α] {a : α} [AddLeftMono α], a⁻ = -a ↔ a ≤ 0
-- Lean.Message
Lean.instToMessageDataString : Lean.ToMessageData String
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousLinearMap.hasFiniteFPowerSeriesOnBall_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F),
  HasFiniteFPowerSeriesOnBall (fun p => (f p.1) p.2) f.toFormalMultilinearSeriesOfMultilinear 0
    (Fintype.card (Option ι) + 1) ⊤
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- Given submodules `M ⊆ R` and `N ⊆ S = M⁻¹R`, with `f : R →+* S` the localization map, if
`N` contains all the units of `S`, then `N ⁻¹ S = T = (f⁻¹ N) ⁻¹ R`. I.e., the localization of a
localization is a localization.
 -/
IsLocalization.localization_localization_isLocalization_of_has_all_units : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (N : Submonoid S) (T : Type u_3) [inst_3 : CommSemiring T] [inst_4 : Algebra R T]
  [inst_5 : Algebra S T] [IsScalarTower R S T] [IsLocalization M S] [IsLocalization N T],
  (∀ (x : S), IsUnit x → x ∈ N) → IsLocalization (Submonoid.comap (algebraMap R S) N) T
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.findEntry?_insert_of_ne : ∀ {α : Type u_1} {cmp : α → α → Ordering} {β : Type u_2} {k' k : α} {v : β} [Std.TransCmp cmp]
  (t : RBTree.RBMap α β cmp), cmp k' k ≠ Ordering.eq → (t.insert k v).findEntry? k' = t.findEntry? k'
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instDefinable : (n : ℕ) → (i : Fin n) → ZFSet.Definable n fun s => s i
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.squarefree_of_mem_divisors_prodPrimes : ∀ {s : BoundingSieve} {d : ℕ}, d ∈ s.prodPrimes.divisors → Squarefree d
-- Mathlib.Data.Seq.Basic
Stream'.Seq.drop_nil : ∀ {α : Type u} {n : ℕ}, Stream'.Seq.nil.drop n = Stream'.Seq.nil
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- The morphism `(m, x) ↦ (m • x, x)`.  -/
CategoryTheory.ModObj.leftSMul : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (M : C) →
        [inst_2 : CategoryTheory.MonObj M] →
          (X : C) →
            [CategoryTheory.ModObj M X] →
              CategoryTheory.MonoidalCategoryStruct.tensorObj M X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj X X
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (n₀ n₁ n₂ : ℤ)
  (h : CategoryTheory.Limits.IsZero ((X'.H n₂).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hi₀₁))))
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀'_hom_inv_id._auto_3),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
      (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv =
    CategoryTheory.CategoryStruct.id
      (X'.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃) (CategoryTheory.homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Analysis.Convex.Birkhoff
Matrix.l2_opNorm_le_one_of_mem_doublyStochastic : ∀ {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] {M : Matrix n n ℝ}, M ∈ doublyStochastic ℝ n → ‖M‖ ≤ 1
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.integral_iUnion_ae : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} {ι : Type u_5} [Countable ι] {s : ι → Set X},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) s) →
      MeasureTheory.IntegrableOn f (⋃ i, s i) μ → ∫ (x : X) in ⋃ n, s n, f x ∂μ = ∑' (n : ι), ∫ (x : X) in s n, f x ∂μ
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
Real.posLog_le_posLog : ∀ {x y : ℝ}, 0 ≤ x → x ≤ y → x.posLog ≤ y.posLog
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.continuous_coe : Continuous Complex.UnitDisc.coe
-- Init.Data.String.Basic
String.rawEndPos_toSlice : ∀ {s : String}, s.toSlice.rawEndPos = s.rawEndPos
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.whisker_left : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) (g h : CategoryTheory.FreeBicategory.Hom b c)
  (η η' : CategoryTheory.FreeBicategory.Hom₂ g h) (a_1 : CategoryTheory.FreeBicategory.Rel η η'),
  CategoryTheory.FreeBicategory.Rel.below a_1 → motive η η' a_1 → CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.Algebra.Order.Ring.Abs
exists_abs_lt : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] [Nontrivial α] (a : α), ∃ b > 0, |a| < b
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.succ_ne : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α],
  Order.IsSuccPrelimit a → ∀ (b : α), Order.succ b ≠ a
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.HeightOneSpectrum.mk : {R : Type u_1} →
  [inst : CommRing R] → (asIdeal : Ideal R) → asIdeal.IsPrime → asIdeal ≠ ⊥ → IsDedekindDomain.HeightOneSpectrum R
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorCompIsoId.eq_1 : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (i j : A) (h : i + j = 0),
  CategoryTheory.shiftFunctorCompIsoId C i j h =
    (CategoryTheory.shiftFunctorAdd' C i j 0 h).symm ≪≫ CategoryTheory.shiftFunctorZero C A
-- Std.Do.WP.Monad
Std.Do.Option.instWPMonad : Std.Do.WPMonad Option (Std.Do.PostShape.except PUnit.{u_1 + 1} Std.Do.PostShape.pure)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- The seminorms on the space `𝓓^{n}_{K}(E, F)` given by the sup norm of the iterated derivatives.
In the scope `Distributions.Seminorm`, we denote them by `N[𝕜; F]_{K, n, i}`
(or `N[𝕜]_{K, n, i}`), or simply by `N[𝕜; F]_{K, i}` (or `N[𝕜; F]_{K, i}`) when `n = ∞`.  -/
Distributions.«termN[_;_]_{_,_,_}» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.one_sub_inv_le_log_of_pos : ∀ {x : ℝ}, 0 < x → 1 - x⁻¹ ≤ Real.log x
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonPlainGoalParams.toJson : Lean.Lsp.PlainGoalParams → Lean.Json