mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- `F` is monoidal given a unit isomorphism `ε : 𝟙_ D ≅ F.obj (𝟙_ C)` and a tensorator isomorphism
`μ : F - ⊗ F - ≅ F (- ⊗ -)` as a natural isomorphism between bifunctors, satisfying the
relevant compatibilities.
 -/
CategoryTheory.Functor.CoreMonoidal.ofBifunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (ε :
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D ≅
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                (μ :
                    CategoryTheory.MonoidalCategory.curriedTensorPre F ≅
                      CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                  CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap μ.hom =
                      CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap μ.hom →
                    CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ F =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ ε.hom)
                          (CategoryTheory.CategoryStruct.comp
                            (μ.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                            (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ F)) →
                      CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ F =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ ε.hom)
                            (CategoryTheory.CategoryStruct.comp
                              (((CategoryTheory.flipFunctor C C D).map μ.hom).app
                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                              (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ F)) →
                        F.CoreMonoidal
-- Lean.Elab.PatternVar
/-- Pattern variables found so far as an array. It contains the order they were found.  -/
Lean.Elab.Term.CollectPatternVars.State.vars : Lean.Elab.Term.CollectPatternVars.State → Array Lean.Elab.Term.PatternVar
-- Mathlib.Algebra.Order.Field.Basic
inv_antitoneOn_Ioi : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α],
  AntitoneOn (fun x => x⁻¹) (Set.Ioi 0)
-- Mathlib.Geometry.Euclidean.Incenter
/-- The distance between the incenter and its projection in the plane of each face is the
inradius.  -/
Affine.Simplex.dist_incenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  dist s.incenter (s.touchpoint ∅ i) = s.inradius
-- Mathlib.Order.WellQuasiOrder
RelIso.wellQuasiOrdered_iff : ∀ {α : Type u_3} {β : Type u_4} {r : α → α → Prop} {s : β → β → Prop} (f : r ≃r s),
  WellQuasiOrdered r ↔ WellQuasiOrdered s
-- Mathlib.Analysis.Fourier.ZMod
_private.Mathlib.Analysis.Fourier.ZMod.0.ZMod.auxDFT.eq_1 : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E)
  (k : ZMod N), ZMod.auxDFT✝ Φ k = ∑ j, ZMod.stdAddChar (-(j * k)) • Φ j
-- Mathlib.Algebra.Module.LocalizedModule.Int
IsLocalizedModule.map_integerMultiple : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] {ι : Type u_4} (s : Finset ι) (g : ι → M') (i : ↥s),
  f (IsLocalizedModule.integerMultiple S f s g i) = IsLocalizedModule.commonDenom S f s g • g ↑i
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.Hom.ext_iff : ∀ {X Y : SFinKer} {x y : X.Hom Y}, x = y ↔ x.hom = y.hom
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Given any distinguished triangle
```
      f       g       h
  X  ───> Y  ───> Z  ───> X⟦1⟧
```
the composition `g ≫ h = 0`.  -/
CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₂₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, CategoryTheory.CategoryStruct.comp T.mor₂ T.mor₃ = 0
-- Mathlib.Algebra.Module.NatInt
instSMulWithZeroInt : {M : Type u_3} → [inst : SubtractionMonoid M] → SMulWithZero ℤ M
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
/-- A cocone in `HomologicalComplex C c` is colimit if the induced cocones obtained
by applying `eval C c i : HomologicalComplex C c ⥤ C` for all `i` are colimit.  -/
HomologicalComplex.isColimitOfEval : {C : Type u_1} →
  {ι : Type u_2} →
    {J : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_3} J] →
          {c : ComplexShape ι} →
            [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (F : CategoryTheory.Functor J (HomologicalComplex C c)) →
                (s : CategoryTheory.Limits.Cocone F) →
                  ((i : ι) → CategoryTheory.Limits.IsColimit ((HomologicalComplex.eval C c i).mapCocone s)) →
                    CategoryTheory.Limits.IsColimit s
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.mk : {α : Type u_7} →
  {β : Type u_8} →
    [inst : MulZeroOneClass α] →
      [inst_1 : MulZeroOneClass β] →
        (toZeroHom : ZeroHom α β) →
          toZeroHom.toFun 1 = 1 →
            (∀ (x y : α), toZeroHom.toFun (x * y) = toZeroHom.toFun x * toZeroHom.toFun y) → α →*₀ β
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatTrans.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (RF RF' : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α α_1 : F ⟶ L.comp RF) (e_α : α = α_1) (α' α'_1 : F' ⟶ L.comp RF'),
  α' = α'_1 →
    ∀ (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) [inst_3 : L.IsLocalization W]
      [inst_4 : RF.IsRightDerivedFunctor α W] (τ τ_1 : F ⟶ F'),
      τ = τ_1 → RF.rightDerivedNatTrans RF' α α' W τ = RF.rightDerivedNatTrans RF' α_1 α'_1 W_1 τ_1
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.top_toSubring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A], ⊤.toSubring = ⊤
-- Aesop.Index.Basic
Aesop.IndexingMode.target.injEq : ∀ (keys keys_1 : Array Lean.Meta.DiscrTree.Key),
  (Aesop.IndexingMode.target keys = Aesop.IndexingMode.target keys_1) = (keys = keys_1)
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- Given `h : ConnectData K L` where `K : ChainComplex C ℕ` and `L : CochainComplex C ℕ`,
this is the cochain complex indexed by `ℤ` obtained by connecting `K` and `L`:
`... ⟶ K.X 2 ⟶ K.X 1 ⟶ K.X 0 ⟶ L.X 0 ⟶ L.X 1 ⟶ L.X 2 ⟶ ...`.  -/
CochainComplex.ConnectData.cochainComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} → {L : CochainComplex C ℕ} → CochainComplex.ConnectData K L → CochainComplex C ℤ
-- Init.PropLemmas
Decidable.iff_iff_not_or_and_or_not : ∀ {a b : Prop} [Decidable a] [Decidable b], (a ↔ b) ↔ (¬a ∨ b) ∧ (a ∨ ¬b)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
/-- The `finrank` of `M →ₗ[R] N` as an `S`-module is `(finrank R M) * (finrank S N)`.  -/
Module.finrank_linearMap : ∀ (R : Type u) (S : Type u') (M : Type v) (N : Type w) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Free R M] [Module.Finite R M] [inst_6 : AddCommGroup N] [inst_7 : Module R N]
  [inst_8 : Module S N] [inst_9 : SMulCommClass R S N] [StrongRankCondition R] [StrongRankCondition S]
  [Module.Free S N], Module.finrank S (M →ₗ[R] N) = Module.finrank R M * Module.finrank S N
-- Lean.Meta.LazyDiscrTree
/-- Append results to array
 -/
Lean.Meta.LazyDiscrTree.MatchResult.appendResultsAux : {α : Type} → {β : Type u_1} → Lean.Meta.LazyDiscrTree.MatchResult α → Array β → (ℕ → α → β) → Array β
-- Mathlib.Lean.MessageData.Trace
/-- Deduplicate an array of `MessageData` by their rendered string representations.  -/
Lean.MessageData.dedupByString : Array Lean.MessageData → BaseIO (Array Lean.MessageData)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_inv_naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens}
  (i : Opposite.op U ⟶ Opposite.op V) {Z : CommRingCat}
  (h : Y.presheaf.obj (Opposite.op ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj V)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f V).inv h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).inv
      (CategoryTheory.CategoryStruct.comp (Y.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).op.map i)) h)
-- Mathlib.Data.ENNReal.Operations
/-- If `a ≤ b + c` and `a = ∞` whenever `b = ∞` or `c = ∞`, then
`ENNReal.toReal a ≤ ENNReal.toReal b + ENNReal.toReal c`. This lemma is useful to transfer
triangle-like inequalities from `ENNReal`s to `Real`s.  -/
ENNReal.toReal_le_add' : ∀ {a b c : ENNReal}, a ≤ b + c → (b = ⊤ → a = ⊤) → (c = ⊤ → a = ⊤) → a.toReal ≤ b.toReal + c.toReal
-- Mathlib.Topology.Order.IntermediateValue
/-- **Intermediate value theorem**: if `f` is continuous on an order-connected set `s` and `a`,
`b` are two points of this set, then `f` sends `s` to a superset of `[f a, f b]`.  -/
ContinuousOn.surjOn_uIcc : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {s : Set α} [hs : s.OrdConnected] {f : α → δ},
  ContinuousOn f s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.SurjOn f s (Set.uIcc (f a) (f b))
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_id : ∀ {M : Type u_1} [inst : Mul M] (S : Subsemigroup M), Subsemigroup.map (MulHom.id M) S = S
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_injective : ∀ {M : Type u_2} [inst : MulOneClass M], Function.Injective Submonoid.op
-- Lean.Meta.Tactic.Simp.Types
/-- Helper function for `simpAppUsingCongr`  -/
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.mkCongrPrefix : Lean.Name → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.algebra : {R : Type u_2} →
  {A : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : Semiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Algebra R A] → [inst_5 : StarModule R A] → (s : StarSubalgebra R A) → Algebra R ↥s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toList_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  {f : (a : α) → β a → γ a}, (Std.DTreeMap.Raw.map f t).toList = List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) t.toList
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.termℓ_ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.Group
/-- **Alias** of `Multipliable.hasFiniteMulSupport_of_discreteTopology`. -/
Multipliable.finite_mulSupport_of_discreteTopology : ∀ {α : Type u_5} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [DiscreteTopology α] {β : Type u_6} (f : β → α),
  Multipliable f → Function.HasFiniteMulSupport f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblXYZ_Z : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P : Fin 3 → R), W'.dblXYZ P 2 = W'.dblZ P
-- Mathlib.CategoryTheory.Preadditive.EilenbergMoore
CategoryTheory.Monad.algebraPreadditive_homGroup_zero_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (T : CategoryTheory.Monad C) [inst_2 : T.Additive] (F G : T.Algebra), CategoryTheory.Monad.Algebra.Hom.f 0 = 0
-- Mathlib.RingTheory.Coalgebra.TensorProduct
TensorProduct.comul_def : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid B] [inst_4 : Algebra R S] [inst_5 : Module R A]
  [inst_6 : Module S A] [inst_7 : Module R B] [inst_8 : IsScalarTower R S A] [inst_9 : CoalgebraStruct R B]
  [inst_10 : CoalgebraStruct S A],
  CoalgebraStruct.comul =
    ↑(TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R S R S A A B B) ∘ₗ
      TensorProduct.AlgebraTensorModule.map CoalgebraStruct.comul CoalgebraStruct.comul
-- Mathlib.GroupTheory.Finiteness
/-- A finitely generated submonoid has a minimal generating set.  -/
Submonoid.FG.exists_minimal_closure_eq : ∀ {M : Type u_1} [inst : Monoid M] {P : Submonoid M}, P.FG → ∃ S, Minimal (fun S => Submonoid.closure ↑S = P) S
-- Lean.Meta.Tactic.Grind.Types
/-- Pushes `a = Bool.true` with `proof` to `newEqs`.  -/
Lean.Meta.Grind.pushEqBoolTrue : Lean.Expr → Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- The image of a `Edge.CompStruct` by a morphism of `2`-truncated
simplicial sets.  -/
SSet.Truncated.Edge.CompStruct.map : {X Y : SSet.Truncated 2} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    {e₀₁ : SSet.Truncated.Edge x₀ x₁} →
      {e₁₂ : SSet.Truncated.Edge x₁ x₂} →
        {e₀₂ : SSet.Truncated.Edge x₀ x₂} →
          e₀₁.CompStruct e₁₂ e₀₂ → (f : X ⟶ Y) → (e₀₁.map f).CompStruct (e₁₂.map f) (e₀₂.map f)
-- Mathlib.Algebra.Star.MonoidHom
StarMonoidHom.coe_toMonoidHom : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Star A] [inst_2 : Monoid B] [inst_3 : Star B] (f : A →⋆* B),
  ⇑f.toMonoidHom = ⇑f
-- Mathlib.Analysis.Fourier.Inversion
/-- **Fourier inversion formula**: If a function `f` on a finite-dimensional real inner product
space is integrable, and its Fourier transform `𝓕 f` is also integrable, then `𝓕⁻ (𝓕 f) = f` at
continuity points of `f`.  -/
MeasureTheory.Integrable.fourierInv_fourier_eq : ∀ {V : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V]
  [inst_2 : MeasurableSpace V] [inst_3 : BorelSpace V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℂ E] {f : V → E} [CompleteSpace E],
  MeasureTheory.Integrable f MeasureTheory.volume →
    MeasureTheory.Integrable (FourierTransform.fourier f) MeasureTheory.volume →
      ∀ {v : V}, ContinuousAt f v → FourierTransformInv.fourierInv (FourierTransform.fourier f) v = f v
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.instDecidableRel_deleteVerts_adj : {V : Type u} → {G : SimpleGraph V} → (u : Set V) → [r : DecidableRel G.Adj] → DecidableRel (⊤.deleteVerts u).coe.Adj
-- Mathlib.Topology.ClusterPt
/-- If `x` is not an isolated point of a topological space, then the closure of `{x}ᶜ` is the whole
space.  -/
closure_compl_singleton : ∀ {X : Type u} [inst : TopologicalSpace X] (x : X) [(nhdsWithin x {x}ᶜ).NeBot], closure {x}ᶜ = Set.univ
-- Lean.Elab.PreDefinition.Structural.SmartUnfolding
/-- Auxiliary method for annotating `match`-alternatives with `markSmartUnfoldingMatch` and `markSmartUnfoldingMatchAlt`.

It uses the following approach:
- Whenever it finds a `match` application `e` s.t. `recArgHasLooseBVarsAt preDef.declName recArgPos e`,
  it marks the `match` with `markSmartUnfoldingMatch`, and each alternative that does not contain a nested marked `match`
  is marked with `markSmartUnfoldingMatchAlt`.

Recall that the condition `recArgHasLooseBVarsAt preDef.declName recArgPos e` is the one used at `mkBRecOn`.
 -/
_private.Lean.Elab.PreDefinition.Structural.SmartUnfolding.0.Lean.Elab.Structural.addSmartUnfoldingDefAux.visit : Lean.Elab.PreDefinition → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_ric : ∀ {n i fallback : ℕ}, (*...=n).toArray.getD i fallback = if i ≤ n then i else fallback
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.comp_id : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B), f.comp (ContinuousAlgHom.id R A) = f
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.eq_of_abs_lt : ∀ {m a b : ℕ}, a ≡ b [MOD m] → |↑b - ↑a| < ↑m → a = b
-- Mathlib.Topology.Continuous
continuous_iff_continuousAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f ↔ ∀ (x : X), ContinuousAt f x
-- Lean.Data.Json.Basic
Lean.Json.getBool? : Lean.Json → Except String Bool
-- Mathlib.Analysis.Calculus.Deriv.Abs
contDiffOn_abs : ∀ {n : ℕ∞} {s : Set ℝ}, (∀ x ∈ s, x ≠ 0) → ContDiffOn ℝ (↑n) (fun x => |x|) s
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.neg_pf : ∀ {α : Type u_1} {a b : α} [inst : Neg α], a = b → -a = -b
-- Batteries.Util.Pickle
/-- Save an object to disk.
If you need to write multiple objects from within a single declaration,
you will need to provide a unique `key` for each.
 -/
pickle : {α : Type} → System.FilePath → α → autoParam Lean.Name pickle._auto_1 → IO Unit
-- Mathlib.Algebra.Ring.GeomSum
Commute.mul_neg_geom_sum₂ : ∀ {R : Type u_1} [inst : Ring R] {x y : R},
  Commute x y → ∀ (n : ℕ), (y - x) * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i) = y ^ n - x ^ n
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.instReprLoogleResult.repr : LeanSearchClient.LoogleResult → ℕ → Std.Format
-- Mathlib.Order.BoundedOrder.Basic
top_le_iff : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, ⊤ ≤ a ↔ a = ⊤
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- A locally compact right-uniform group is complete.  -/
IsRightUniformGroup.completeSpace_of_weaklyLocallyCompactSpace : ∀ {G : Type u_3} [inst : Group G] [inst_1 : UniformSpace G] [IsRightUniformGroup G] [WeaklyLocallyCompactSpace G],
  CompleteSpace G
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- Maps of `n + 1`-truncated simplicial sets induce maps of paths.  -/
SSet.Truncated.Path.map : {n : ℕ} → {X Y : SSet.Truncated (n + 1)} → {m : ℕ} → X.Path m → (X ⟶ Y) → Y.Path m
-- Std.Time.Format.Modifier
Std.Time.Modifier.e.sizeOf_spec : ∀ (presentation : Std.Time.Number ⊕ Std.Time.Text), sizeOf (Std.Time.Modifier.e presentation) = 1 + sizeOf presentation
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.map : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r → ∀ {f : ℝ → ℝ}, ContinuousAt f r → Hyperreal.IsSt (Filter.Germ.map f x) (f r)
-- Std.Do.PostCond
Std.Do.ExceptConds.entails.trans : ∀ {ps : Std.Do.PostShape} {x y z : Std.Do.ExceptConds ps}, x.entails y → y.entails z → x.entails z
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.comap_isLoop_iff : ∀ {α : Type u_1} {β : Type u_2} {e : α} {M : Matroid β} {f : α → β}, (M.comap f).IsLoop e ↔ M.IsLoop (f e)
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_fun : ∀ {α : Sort u_1} {β : Sort u_2}, IsEmpty (α → β) ↔ Nonempty α ∧ IsEmpty β
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.comp_apply : ∀ {X Y T : AddCommGrpCat} (f : X ⟶ Y) (g : Y ⟶ T) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.neg'_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f : L.obj X ⟶ L.obj Y) (φ : W.LeftFraction X Y),
  f = φ.map L ⋯ → CategoryTheory.Localization.Preadditive.neg' W f = φ.neg.map L ⋯
-- Mathlib.Algebra.Order.Archimedean.Basic
WithBot.instArchimedean : ∀ (M : Type u_5) [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [Archimedean M], Archimedean (WithBot M)
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.iterate_succ' : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f' : Module.End R M} (n : ℕ), f' ^ (n + 1) = f' ∘ₗ f' ^ n
-- Mathlib.Data.ENNReal.Basic
Set.OrdConnected.image_ennreal_ofReal : ∀ {s : Set ℝ}, s.OrdConnected → (ENNReal.ofReal '' s).OrdConnected
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.exists_isBase_subset_union_isBase : ∀ {α : Type u_1} {M : Matroid α} {B I : Set α}, M.Indep I → M.IsBase B → ∃ B', M.IsBase B' ∧ I ⊆ B' ∧ B' ⊆ I ∪ B
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.addMonObj.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 D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.AddMonObj (F.obj X)],
  hF.addMonObj X =
    {
      zero :=
        hF.preimage
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.AddMonObj.zero),
      add :=
        hF.preimage
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X)
            CategoryTheory.AddMonObj.add),
      zero_add := ⋯, add_zero := ⋯, add_assoc := ⋯ }
-- Std.Async.Basic
_private.Std.Async.Basic.0.Std.Async.BaseAsync.bind.bindAsyncTask : {α β : Type} → Task.Priority → Bool → Std.Async.MaybeTask α → (α → Std.Async.BaseAsync β) → Std.Async.BaseAsync β
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.deriv_LFunction_eq_deriv_LSeries : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re → deriv (DirichletCharacter.LFunction χ) s = deriv (LSeries fun x => χ ↑x) s
-- Init.Data.Nat.Basic
Nat.pred_inj : ∀ {a b : ℕ}, 0 < a → 0 < b → a.pred = b.pred → a = b
-- Mathlib.Data.Set.Insert
Set.eq_of_nonempty_of_subsingleton : ∀ {α : Type u_3} [Subsingleton α] (s t : Set α) [Nonempty ↑s] [Nonempty ↑t], s = t
-- Mathlib.CategoryTheory.Filtered.Final
/-- Implementation; use `Functor.Final.exists_coeq instead`.  -/
CategoryTheory.Functor.Final.exists_coeq_of_locally_small : ∀ {C : Type v₁} [inst : CategoryTheory.Category.{v₁, v₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty C] [F.Final] {d : D} {c : C} (s s' : d ⟶ F.obj c),
  ∃ c' t, CategoryTheory.CategoryStruct.comp s (F.map t) = CategoryTheory.CategoryStruct.comp s' (F.map t)
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieIdeal.normalizer_eq_top : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  (LieIdeal.toLieSubalgebra R L I).normalizer = ⊤