mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
CategoryTheory.Functor.isDenseAt_eq_isPointwiseLeftKanExtensionAt : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  F.isDenseAt =
    (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.Functor.id D)
        F.rightUnitor.inv).isPointwiseLeftKanExtensionAt
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.symmDiff : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  MeasureTheory.NullMeasurableSet s₁ μ →
    MeasureTheory.NullMeasurableSet s₂ μ → MeasureTheory.NullMeasurableSet (symmDiff s₁ s₂) μ
-- Mathlib.Analysis.Real.Pi.Chudnovsky
/-- The infinite sum in Chudnovsky's formula for `π⁻¹`  -/
chudnovskySum : ℝ
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.zip_toOrderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c₀ : OmegaCompletePartialOrder.Chain α)
  (c₁ : OmegaCompletePartialOrder.Chain β), (c₀.zip c₁).toOrderHom = c₀.prod c₁.toOrderHom
-- Init.Data.BitVec.Lemmas
BitVec.sub_eq_iff_eq_add : ∀ {w : ℕ} {x y z : BitVec w}, x - y = z ↔ x = z + y
-- Mathlib.Order.RelIso.Basic
RelIso.cast_apply : ∀ {α β : Type u} {r : α → α → Prop} {s : β → β → Prop} (h₁ : α = β) (h₂ : r ≍ s) (a : α),
  (RelIso.cast h₁ h₂) a = cast h₁ a
-- Mathlib.Data.Set.Lattice
Function.Surjective.iInter_comp : ∀ {α : Type u_1} {ι : Sort u_5} {ι₂ : Sort u_7} {f : ι → ι₂},
  Function.Surjective f → ∀ (g : ι₂ → Set α), ⋂ x, g (f x) = ⋂ y, g y
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instBEqOfLawfulBEq : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [LawfulBEq α] → [(k : α) → BEq (β k)] → BEq (Std.ExtDHashMap α β)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.inclusion_apply : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M} (h : N ≤ N') (m : ↥N),
  (LieSubmodule.inclusion h) m = ⟨↑m, ⋯⟩
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
AnalyticAt.log : ∀ {f : ℝ → ℝ} {x : ℝ}, AnalyticAt ℝ f x → 0 < f x → AnalyticAt ℝ (fun z => Real.log (f z)) x
-- Mathlib.Topology.Algebra.Module.Multilinear.Bounded
/-- The image of a von Neumann bounded set under a continuous multilinear map
is von Neumann bounded.

This version does not assume that the topologies on the domain and on the codomain
agree with the vector space structure in any way
but it assumes that `ι` is nonempty.
 -/
Bornology.IsVonNBounded.image_multilinear' : ∀ {ι : Type u_1} {𝕜 : Type u_2} {F : Type u_3} {E : ι → Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → AddCommGroup (E i)] [inst_2 : (i : ι) → Module 𝕜 (E i)]
  [inst_3 : (i : ι) → TopologicalSpace (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [Nonempty ι] {s : Set ((i : ι) → E i)},
  Bornology.IsVonNBounded 𝕜 s → ∀ (f : ContinuousMultilinearMap 𝕜 E F), Bornology.IsVonNBounded 𝕜 (⇑f '' s)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.IsPushout.inr_fst' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} {b : CategoryTheory.Limits.BinaryBicone X Y}
  (h : b.IsBilimit), CategoryTheory.IsPushout b.inr 0 b.fst 0
-- Mathlib.FieldTheory.IsAlgClosed.Basic
IsAlgClosure.equivOfEquiv_symm_algebraMap : ∀ {R : Type u} {S : Type u_3} (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field L]
  [inst_3 : Field M] [inst_4 : Algebra R M] [inst_5 : Module.IsTorsionFree R M] [inst_6 : IsAlgClosure R M]
  [inst_7 : Algebra S L] [inst_8 : Module.IsTorsionFree S L] [inst_9 : IsAlgClosure S L] [inst_10 : IsDomain R]
  [inst_11 : IsDomain S] (hSR : S ≃+* R) (r : R),
  (IsAlgClosure.equivOfEquiv L M hSR).symm ((algebraMap R M) r) = (algebraMap S L) (hSR.symm r)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Ico_iff_integrableOn_Ioo : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α} [MeasureTheory.NullSingletonClass μ],
  autoParam (‖f a‖ₑ ≠ ⊤) integrableOn_Ico_iff_integrableOn_Ioo._auto_1 →
    (MeasureTheory.IntegrableOn f (Set.Ico a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ)
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of an integrable function is greater than its mean.  -/
MeasureTheory.exists_setAverage_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ℝ},
  μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ → ∃ x ∈ s, ⨍ (a : α) in s, f a ∂μ ≤ f x
-- Lean.Data.JsonRpc
Lean.JsonRpc.Notification.mk.injEq : ∀ {α : Type u} (method : String) (param : α) (method_1 : String) (param_1 : α),
  ({ method := method, param := param } = { method := method_1, param := param_1 }) =
    (method = method_1 ∧ param = param_1)
-- Lean.Meta.Tactic.Grind.Types
/-- `goal.withContext x` executes `x` using the given metavariable `LocalContext` and `LocalInstances`.
The type class resolution cache is flushed when executing `x` if its `LocalInstances` are
different from the current ones.  -/
Lean.Meta.Grind.Goal.withContext : {m : Type → Type u_1} → {α : Type} → [MonadControlT Lean.MetaM m] → [Monad m] → Lean.Meta.Grind.Goal → m α → m α
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteAtFilter.mono : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f g : Filter α},
  f ≤ g → μ ≤ ν → ν.FiniteAtFilter g → μ.FiniteAtFilter f
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- In a vector space, given a nonzero linear form `f`,
a nonzero vector `v` such that `f v ≠ 0`,
there exists a basis `b` with an index `i`
such that `v = b i` and `f = (f v) • b.coord i`.  -/
exists_basis_of_pairing_ne_zero : ∀ {K : Type u_6} {V : Type u_7} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {f : V →ₗ[K] K}
  {v : V}, f v ≠ 0 → ∃ n b i, v = b i ∧ f = f v • b.coord i
-- Init.Grind.AC
Lean.Grind.AC.superpose_ac_idempotent_cert : Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Aesop.BaseM
Aesop.BaseM.instMonadStats : Aesop.MonadStats Aesop.BaseM
-- Mathlib.Topology.WithTopology
WithTopology.instLinearOrder : {X : Type u_1} → (t : TopologicalSpace X) → [LinearOrder X] → LinearOrder (WithTopology X t)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
NonUnitalStarAlgebra.elemental.eq_1 : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] [inst_8 : TopologicalSpace A] [inst_9 : IsSemitopologicalSemiring A]
  [inst_10 : ContinuousConstSMul R A] [inst_11 : ContinuousStar A] (x : A),
  NonUnitalStarAlgebra.elemental R x = (NonUnitalStarAlgebra.adjoin R {x}).topologicalClosure
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.normedAddCommGroup : {E : Type u_2} → [NormedAddCommGroup E] → NormedAddCommGroup Eᵒᵈ
-- Mathlib.Data.Finset.SDiff
Finset.coe_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), ↑(s₁ \ s₂) = ↑s₁ \ ↑s₂
-- Mathlib.RingTheory.RingHom.Locally
/-- **Alias** of `RingHom.locally_stableUnderCompositionWithLocalizationAwaySource`.

---

If `P` is stable under composition with localization away maps on the left,
then so is `Locally P`.  -/
RingHom.locally_StableUnderCompositionWithLocalizationAwaySource : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] =>
      RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- `Y` identifies to the cokernel of a zero map `X ⟶ Y`.  -/
CategoryTheory.Limits.CokernelCofork.IsColimit.ofId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          (hf : f = 0) →
            CategoryTheory.Limits.IsColimit
              (CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.CategoryStruct.id Y) ⋯)
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.ι₀_snd : ∀ (X : SSet),
  CategoryTheory.CategoryStruct.comp SSet.ι₀
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X (SSet.stdSimplex.obj { len := 1 })) =
    SSet.const (SSet.stdSimplex.obj₀Equiv.symm 0)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.delabLevel : Lean.Level → ℕ → Lean.MetaM Lean.Syntax.Level
-- Mathlib.Algebra.Order.Sub.Basic
tsub_lt_self : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α} [AddLeftReflectLE α], 0 < a → 0 < b → a - b < a
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {X Y : SheafOfModules R} {x y : X.Hom Y}, x.val = y.val → x = y
-- Mathlib.Analysis.Complex.HasPrimitives
/-- The `(z, w)`-wedge-integral of `f`, is the integral of `f` over two sides of the rectangle
determined by `z` and `w`.  -/
Complex.wedgeIntegral : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → ℂ → ℂ → (ℂ → E) → E
-- Mathlib.Algebra.Ring.Pi
Pi.nonUnitalNonAssocSemiring : {I : Type u} →
  {f : I → Type v} → [(i : I) → NonUnitalNonAssocSemiring (f i)] → NonUnitalNonAssocSemiring ((i : I) → f i)
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.instCore_1 : {R : Type u_1} →
  {S : Type u_2} →
    {ι : Type u_3} →
      {σ : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {P : Algebra.Presentation R S ι σ} → Algebra P.Core S
-- Init.Data.BitVec.Lemmas
BitVec.sub_toNat_mod_cancel : ∀ {w : ℕ} {x : BitVec w}, ¬x = 0#w → (2 ^ w - x.toNat) % 2 ^ w = 2 ^ w - x.toNat
-- Init.Data.Order.Lemmas
Std.instLawfulBEqOfLawfulOrderBEqOfIsPartialOrder : ∀ {α : Type u} [inst : BEq α] [inst_1 : LE α] [Std.LawfulOrderBEq α] [Std.IsPartialOrder α], LawfulBEq α
-- Mathlib.Algebra.Polynomial.Degree.Support
/-- We can reexpress a sum over `p.support` as a sum over `range n`,
for any `n` satisfying `p.natDegree < n`.
 -/
Polynomial.sum_over_range' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid S] (p : Polynomial R) {f : ℕ → R → S},
  (∀ (n : ℕ), f n 0 = 0) → ∀ (n : ℕ), p.natDegree < n → p.sum f = ∑ a ∈ Finset.range n, f a (p.coeff a)
-- Mathlib.Tactic.Explode.Pretty
/-- Given a list of `MessageData`s, make them of equal length.
We need this in order to form columns in our Fitch table.

```lean
padRight ["hi", "hello"] = ["hi   ", "hello"]
```
 -/
Mathlib.Explode.padRight : List Lean.MessageData → Lean.MetaM (List Lean.MessageData)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_rotateRight : ∀ {w : ℕ} {x : BitVec w} {r : ℕ},
  (x.rotateRight r).toFin = x.toFin / Fin.ofNat (2 ^ w) (2 ^ (r % w)) ||| Fin.ofNat (2 ^ w) (x.toNat <<< (w - r % w))
-- Mathlib.Algebra.Group.Defs
AddCommMagma.ext_iff : ∀ {G : Type u} {x y : AddCommMagma G}, x = y ↔ Add.add = Add.add
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.run_bind.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (x : α) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok x s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 x s
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- Any linear form on a topological vector space over a nontrivially normed field is continuous if
and only if its kernel is closed.  -/
LinearMap.continuous_iff_isClosed_ker : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] (l : E →ₗ[𝕜] 𝕜),
  Continuous ⇑l ↔ IsClosed ↑l.ker
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.compProd_posterior_eq_swap_comp : ∀ {Ω : Type u_1} {𝓧 : Type u_2} {mΩ : MeasurableSpace Ω} {m𝓧 : MeasurableSpace 𝓧} {κ : ProbabilityTheory.Kernel Ω 𝓧}
  {μ : MeasureTheory.Measure Ω} [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : ProbabilityTheory.IsFiniteKernel κ]
  [inst_2 : StandardBorelSpace Ω] [inst_3 : Nonempty Ω],
  (μ.bind ⇑κ).compProd (ProbabilityTheory.posterior κ μ) = (μ.compProd κ).bind ⇑(ProbabilityTheory.Kernel.swap Ω 𝓧)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.liftOfRightInverse_eq : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : CommRing M]
  [inst_3 : Algebra R A] [inst_4 : Algebra R M] {F : Type u_4} [inst_5 : FunLike F A M] [inst_6 : AlgHomClass F R A M]
  {f : F} {f_inv₁ f_inv₂ : M → A} (hf₁ : Function.RightInverse f_inv₁ ⇑f) (hf₂ : Function.RightInverse f_inv₂ ⇑f),
  Derivation.liftOfRightInverse hf₁ = Derivation.liftOfRightInverse hf₂
-- Mathlib.RingTheory.Coalgebra.TensorProduct
/-- `rTensor M f : N ⊗ M →ₗc P ⊗ M` is the natural coalgebra morphism induced by `f : N →ₗc P`.  -/
CoalgHom.rTensor : {R : Type u_5} →
  (M : Type u_6) →
    {N : Type u_7} →
      {P : Type u_8} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      [inst_7 : Coalgebra R M] →
                        [inst_8 : Coalgebra R N] →
                          [inst_9 : Coalgebra R P] → (N →ₗc[R] P) → TensorProduct R N M →ₗc[R] TensorProduct R P M
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.trans : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ m₃ : Std.DHashMap.Raw α β}, m₁.Equiv m₂ → m₂.Equiv m₃ → m₁.Equiv m₃
-- Mathlib.Algebra.Regular.Prod
Prod.isAddRegular_mk : ∀ {R : Type u_2} {S : Type u_3} [inst : Add R] [inst_1 : Add S] {a : R} {b : S},
  IsAddRegular (a, b) ↔ IsAddRegular a ∧ IsAddRegular b
-- Mathlib.Data.Vector.Basic
List.Vector.get_cons_zero : ∀ {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n), (a ::ᵥ v).get 0 = a
-- Init.Data.List.Zip
List.zipWith_comm_of_comm : ∀ {α : Type u_1} {β : Type u_2} {f : α → α → β},
  (∀ (x y : α), f x y = f y x) → ∀ {l l' : List α}, List.zipWith f l l' = List.zipWith f l' l
-- Mathlib.Algebra.Order.Group.PosPart
/-- **Alias** of the reverse direction of `posPart_eq_zero`. -/
posPart_of_nonpos : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : SubNegMonoid α] {a : α}, a ≤ 0 → a⁺ = 0
-- Mathlib.Algebra.Order.Sub.Defs
eq_tsub_of_add_eq : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a + c = b → a = b - c
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_string : ∀ {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {s : String} {init : β} {f : Char → β → m (ForInStep β)}
  (inv : Std.Do.StringInvariant s β ps),
  (∀ (pos : s.Pos) (b : β) (h : pos ≠ s.endPos),
      ⦃inv.1 (pos, b)⦄
        f (pos.get h) b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 (pos.next h, b')
          | ForInStep.done b' => inv.1 (s.endPos, b'),
          inv.2)⦄) →
    ⦃inv.1 (s.startPos, init)⦄ forIn s init f ⦃(fun b => inv.1 (s.endPos, b), inv.2)⦄
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.diam_def : ∀ {α : Type u_1} {G : SimpleGraph α}, G.diam = (⨆ p, G.edist p.1 p.2).toNat
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isAlt_neg : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B : LinearMap.BilinForm R₁ M₁}, (-B).IsAlt ↔ B.IsAlt
-- Init.Data.List.ToArray
/-- Variant of `foldr_toArray` with a side condition for the `start` argument.  -/
List.foldr_toArray' : ∀ {α : Type u_1} {β : Type u_2} {start : ℕ} (f : α → β → β) (init : β) (l : List α),
  start = l.toArray.size → Array.foldr f init l.toArray start = List.foldr f init l
-- Mathlib.Data.Nat.PSub
Nat.psub'_eq_psub : ∀ (m n : ℕ), m.psub' n = m.psub n
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
SSet.functorN_obj : ∀ (X : SSet) (X_1 : X.N), X.functorN.obj X_1 = X_1.subcomplex.toSSet
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- If `S` is an `R`-algebra, then `S[M]` is a `R[M]` algebra.

Warning: This produces a diamond for `Algebra R[M] S[M][M]` and another one for `Algebra R[M] R[M]`.
That's why it is not a global instance.  -/
MonoidAlgebra.algebraMonoidAlgebra : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_7} →
      [inst : CommMonoid M] →
        [inst_1 : CommSemiring R] →
          [inst_2 : CommSemiring S] → [Algebra R S] → Algebra (MonoidAlgebra R M) (MonoidAlgebra S M)
-- Lean.Expr
Lean.Expr.bindingDomain! : Lean.Expr → Lean.Expr
-- Mathlib.Topology.Algebra.Monoid
Continuous.units_map : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : TopologicalSpace M]
  [inst_3 : TopologicalSpace N] (f : M →* N), Continuous ⇑f → Continuous ⇑(Units.map f)
-- Mathlib.RepresentationTheory.Coinduced
Rep.instPreservesEpimorphismsSubtypeMemSubgroupCoindFunctorSubtype : ∀ {k : Type u} [inst : CommRing k] {G : Type v'} [inst_1 : Group G] (S : Subgroup G),
  (Rep.coindFunctor k S.subtype).PreservesEpimorphisms
-- Init.Data.Nat.Div.Basic
Nat.mul_mod_mul_left : ∀ (z x y : ℕ), z * x % (z * y) = z * (x % y)
-- Mathlib.Data.EReal.Basic
EReal.coe_nonneg : ∀ {x : ℝ}, 0 ≤ ↑x ↔ 0 ≤ x
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.finSuccEquiv.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] (n : ℕ),
  MvPolynomial.finSuccEquiv R n =
    (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivLeft R (Fin n))
-- Mathlib.Topology.Algebra.UniformConvergence
instMulActionUniformOnFun : {α : Type u_1} →
  {β : Type u_2} →
    {𝔖 : Set (Set α)} → {M : Type u_5} → [inst : Monoid M] → [MulAction M β] → MulAction M (UniformOnFun α β 𝔖)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  l.contains k = false → (Std.TreeSet.Raw.ofList l cmp).get? k = none
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of the forward direction of `continuousAt_neg_iff`. -/
ContinuousAt.of_neg : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G]
  [inst_3 : TopologicalSpace α] {f : α → G} {x : α}, ContinuousAt (-f) x → ContinuousAt f x
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftAssocTensor_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C × C × C}
  (f : X ⟶ Y),
  (CategoryTheory.MonoidalCategory.leftAssocTensor C).map f =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f.1 f.2.1) f.2.2
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceBEq : Lean.Meta.Simp.DSimproc
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Converts an entry (i.e., `List Key`) to the discrimination tree into
`MessageData` that is more user-friendly.

This is a copy of `Lean.Meta.DiscrTree.keysAsPattern`
 -/
Lean.Meta.RefinedDiscrTree.keysAsPattern : Array Lean.Meta.RefinedDiscrTree.Key → Lean.CoreM Lean.MessageData
-- Mathlib.LinearAlgebra.Contraction
rTensorHomEquivHomRTensor_toLinearMap : ∀ (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] [inst_7 : Module.Projective R M] [inst_8 : Module.Finite R M],
  ↑(rTensorHomEquivHomRTensor R M P Q) = TensorProduct.rTensorHomToHomRTensor (RingHom.id R) M P Q
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instIsAddMonHomμ : ∀ {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 : CategoryTheory.BraidedCategory C]
  [inst_5 : CategoryTheory.BraidedCategory D] [inst_6 : F.LaxBraided] (M N : C) [inst_7 : CategoryTheory.AddMonObj M]
  [inst_8 : CategoryTheory.AddMonObj N], CategoryTheory.IsAddMonHom (CategoryTheory.Functor.LaxMonoidal.μ F M N)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.contains a = false → m.get! a = default
-- Init.Data.UInt.Lemmas
UInt64.ofNat_le_iff_le : ∀ {a b : ℕ}, a < UInt64.size → b < UInt64.size → (UInt64.ofNat a ≤ UInt64.ofNat b ↔ a ≤ b)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flippingEquiv_symm_apply_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (k : C) (j : D),
  ((CategoryTheory.Functor.flippingEquiv.symm F).obj k).obj j = (F.obj j).obj k
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.BinaryCoproductDisjoint.of_binaryCofan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {c : CategoryTheory.Limits.BinaryCofan X Y}
  (hc : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Mono c.inl] [CategoryTheory.Mono c.inr]
  {s : CategoryTheory.Limits.PullbackCone c.inl c.inr} (hs : CategoryTheory.Limits.IsLimit s)
  (H : CategoryTheory.Limits.IsInitial s.pt), CategoryTheory.Limits.BinaryCoproductDisjoint X Y
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
/-- `Rel` as a ring congruence, used to build the quotient.  -/
TensorAlgebra.ringCon : (R : Type u_1) →
  [inst : CommSemiring R] → (M : Type u_2) → [inst_1 : AddCommMonoid M] → [Module R M] → RingCon (FreeAlgebra R M)
-- Mathlib.Order.Filter.Pointwise
Filter.mul_eq_bot_iff : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α}, f * g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The canonical map `Φ.op.LeftResolution X₂ → Φ.RightResolution X₂`.  -/
CategoryTheory.LocalizerMorphism.LeftResolution.unop : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂ᵒᵖ} → Φ.op.LeftResolution X₂ → Φ.RightResolution (Opposite.unop X₂)
-- Init.Data.List.Lemmas
List.insert_append_of_not_mem_left : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α},
  a ∉ l₂ → List.insert a (l₁ ++ l₂) = List.insert a l₁ ++ l₂
-- Mathlib.Topology.Order
induced_sInf : ∀ {α : Type u_1} {β : Type u_2} {g : β → α} {s : Set (TopologicalSpace α)},
  TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- The formal derivative of a formal power series  -/
PowerSeries.derivative : (R : Type u_1) → [inst : CommSemiring R] → Derivation R (PowerSeries R) (PowerSeries R)