mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- A finite-product-preserving functor between Cartesian monoidal categories is braided.

This is not made an instance because it would create a diamond for the monoidal structure on
the identity and composition of functors.  -/
CategoryTheory.Functor.Braided.ofChosenFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            [inst_4 : CategoryTheory.BraidedCategory C] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (F : CategoryTheory.Functor C D) → [CategoryTheory.Limits.PreservesFiniteProducts F] → F.Braided
-- Mathlib.Algebra.Module.Presentation.Basic
/-- the index type for generators  -/
Module.Relations.G : {A : Type u} → [inst : Ring A] → Module.Relations A → Type w₀
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_union_add_inter₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasureTheory.NullMeasurableSet t μ → μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
-- Mathlib.Topology.Bases
/-- If `β` is a first-countable space, then its induced topology via `f` on `α` is also
first-countable.  -/
TopologicalSpace.firstCountableTopology_induced : ∀ (α : Type u_1) (β : Type u_2) [t : TopologicalSpace β] [FirstCountableTopology β] (f : α → β),
  FirstCountableTopology α
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_mono_fun : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} {hs : s.Nonempty} {f g : β → α},
  (∀ b ∈ s, f b ≤ g b) → s.sup' hs f ≤ s.sup' hs g
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.maxKeyD_erase_le_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α},
      (t.erase k).isEmpty = false →
        ∀ {fallback : α}, (cmp ((t.erase k).maxKeyD fallback) (t.maxKeyD fallback)).isLE = true
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.neg_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  {f : E →SWOT[σ] F} (x : E), (-f) x = -f x
-- Mathlib.RingTheory.MatrixAlgebra
matrixEquivTensor_apply_single : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] (i j : n) (x : A),
  (matrixEquivTensor n R A) (Matrix.single i j x) = x ⊗ₜ[R] Matrix.single i j 1
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.nonempty : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P), Nonempty ι
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instLawfulBEqOfLawfulEqCmp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [inst_2 : BEq β]
  [LawfulBEq β], LawfulBEq (Std.ExtTreeMap α β cmp)
-- Mathlib.Order.Category.Lat
/-- The underlying `LatticeHom`.  -/
Lat.Hom.hom' : {X Y : Lat} → X.Hom Y → LatticeHom ↑X ↑Y
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.mk_mul_mk_inv_eq_one : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units),
  ⟨(Units.coeHom M) x, ⋯⟩ * ⟨(Units.coeHom M) x⁻¹, ⋯⟩ = 1
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_7 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.sub b →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_7 a b
-- Mathlib.CategoryTheory.GlueData
/-- For each `i j : J`, an object `V i j`  -/
CategoryTheory.GlueData.V : {C : Type u₁} → [inst : CategoryTheory.Category.{v, u₁} C] → (self : CategoryTheory.GlueData C) → self.J × self.J → C
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.find?_toArray_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] {k : α},
  t.WF → (Array.find? (fun x => compare x.fst k == Ordering.eq) t.toArray = none ↔ k ∉ t)
-- Mathlib.Analysis.LConvolution
/-- Convolution of a function with the zero function returns the zero function.  -/
MeasureTheory.lconvolution_zero : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : Add G] [inst_1 : Neg G] (f : G → ENNReal)
  (μ : MeasureTheory.Measure G), MeasureTheory.lconvolution f 0 μ = 0
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- The coefficients of a Mahler series can be recovered from the sum by taking forward differences at
`0`.
 -/
PadicInt.fwdDiff_mahlerSeries : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E},
  Filter.Tendsto a Filter.atTop (nhds 0) → ∀ (n : ℕ), (fwdDiff 1)^[n] (⇑(PadicInt.mahlerSeries a)) 0 = a n
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.zipWithM'_eq_zipWithM.go : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} [inst : Monad m] [LawfulMonad m]
  {f : α → β → m γ} (l : List α) (l' : List β) (acc : Array γ),
  List.zipWithM.loop f l l' acc = do
    let __do_lift ← List.zipWithM' f l l'
    pure (acc.toList ++ __do_lift)
-- Mathlib.Order.Filter.CountableInter
/-- For a countable collection of sets `s ∈ l`, their intersection belongs to `l` as well.  -/
CountableInterFilter.countable_sInter_mem : ∀ {α : Type u_2} {l : Filter α} [self : CountableInterFilter l] (S : Set (Set α)),
  S.Countable → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.mk : {α : Type u} →
  (toLinearPreorderOfLEArgs : Std.Packages.LinearPreorderOfLEArgs α) →
    autoParam
        (let this := toLinearPreorderOfLEArgs.le;
        ∀ (a b : α), a ≤ b → b ≤ a → a = b)
        Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam →
      (min :
          autoParam
            (let this := toLinearPreorderOfLEArgs.le;
            let this := toLinearPreorderOfLEArgs.decidableLE;
            Min α)
            Std.Packages.LinearOrderOfLEArgs.min._autoParam) →
        (max :
            autoParam
              (let this := toLinearPreorderOfLEArgs.le;
              let this := toLinearPreorderOfLEArgs.decidableLE;
              Max α)
              Std.Packages.LinearOrderOfLEArgs.max._autoParam) →
          autoParam
              (let this := toLinearPreorderOfLEArgs.le;
              let this_1 := toLinearPreorderOfLEArgs.decidableLE;
              let this_2 := min;
              ∀ (a b : α), a ⊓ b = if a ≤ b then a else b)
              Std.Packages.LinearOrderOfLEArgs.min_eq._autoParam →
            autoParam
                (let this := toLinearPreorderOfLEArgs.le;
                let this_1 := toLinearPreorderOfLEArgs.decidableLE;
                let this_2 := max;
                ∀ (a b : α), a ⊔ b = if b ≤ a then a else b)
                Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam →
              Std.Packages.LinearOrderOfLEArgs α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_congr : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Constructs an isomorphism of `BinaryCofan`s out of an isomorphism of the tips that commutes with
the injections.  -/
CategoryTheory.Limits.BinaryCofan.ext : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : C} →
      {c c' : CategoryTheory.Limits.BinaryCofan A B} →
        (e : c.pt ≅ c'.pt) →
          CategoryTheory.CategoryStruct.comp c.inl e.hom = c'.inl →
            CategoryTheory.CategoryStruct.comp c.inr e.hom = c'.inr → (c ≅ c')
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subRight_symm_apply : ∀ {G : Type u_5} [inst : AddGroup G] (a b : G), (Equiv.subRight a).symm b = b + a
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.coe_unop : ∀ {M : Type u_2} [inst : Mul M] (x : Subsemigroup Mᵐᵒᵖ), ↑x.unop = MulOpposite.op ⁻¹' ↑x
-- Mathlib.FieldTheory.Normal.Basic
Polynomial.SplittingField.instNormal : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F), Normal F p.SplittingField
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget MonCat)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {k k' : α} {f : Option β → Option β},
  m.WF →
    (m.alter k f).getKey! k' = if (k == k') = true then if (f m[k]?).isSome = true then k else default else m.getKey! k'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_beq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, Option.all (fun x_2 => x_2 == k) (m.getKey? k) = true
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.instInhabitedState : Inhabited Std.Http.Protocol.H1.Writer.State
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.zero_lt_coe : ∀ {α : Type u_1} [inst : LT α] (a : α), 0 < ↑a
-- Mathlib.Analysis.Complex.Hadamard
/-- Rewrite for `InterpStrip` on the open vertical strip.  -/
Complex.HadamardThreeLines.interpStrip_eq_of_mem_verticalStrip : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E),
  ∀ z ∈ Complex.HadamardThreeLines.verticalStrip 0 1,
    Complex.HadamardThreeLines.interpStrip f z =
      ↑(Complex.HadamardThreeLines.sSupNormIm f 0) ^ (1 - z) * ↑(Complex.HadamardThreeLines.sSupNormIm f 1) ^ z
-- Mathlib.RingTheory.Flat.Domain
/-- Tensor product of injective maps over domains are injective under some flatness conditions.
Also see `TensorProduct.map_injective_of_flat_flat`
for different flatness conditions but without the domain assumption.  -/
TensorProduct.map_injective_of_flat_flat_of_isDomain : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : AddCommGroup N] [inst_5 : Module R N] {P : Type u_4} {Q : Type u_5}
  [inst_6 : AddCommGroup P] [inst_7 : Module R P] [inst_8 : AddCommGroup Q] [inst_9 : Module R Q] (f : P →ₗ[R] M)
  (g : Q →ₗ[R] N) [H : Module.Flat R P] [Module.Flat R Q],
  Function.Injective ⇑f → Function.Injective ⇑g → Function.Injective ⇑(TensorProduct.map f g)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.add.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.add = H.add
-- Mathlib.Analysis.LocallyConvex.Basic
Balanced.union : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] {A B : Set E},
  Balanced 𝕜 A → Balanced 𝕜 B → Balanced 𝕜 (A ∪ B)
-- Init.Data.List.Range
List.range_eq_range' : ∀ {n : ℕ}, List.range n = List.range' 0 n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.GetLsbDTarget.idx : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig → ℕ
-- Mathlib.RingTheory.LaurentSeries
/-- Reinterpret the extension of `coe : WithVal ((idealX K).valuation _) → K⸨X⸩` as a ring
homomorphism  -/
LaurentSeries.extensionAsRingHom : (K : Type u_2) →
  [inst : Field K] →
    Continuous
        ⇑((algebraMap (RatFunc K) (LaurentSeries K)).comp (WithVal.equiv (RatFunc.polynomialValuationX K)).toRingHom) →
      [CompleteSpace (LaurentSeries K)] →
        [T0Space (LaurentSeries K)] →
          UniformSpace.Completion (WithVal (RatFunc.polynomialValuationX K)) →+* LaurentSeries K
-- Mathlib.Data.Set.Restrict
Set.range_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) (f : α → β), Set.range (t.restrictPreimage f) = Subtype.val ⁻¹' Set.range f
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote'.go : {α : Type u_1} → [Lean.Grind.IntModule α] → Lean.Grind.Linarith.Context α → α → Lean.Grind.Linarith.Poly → α
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_iSup_sum' : ∀ {α : Type u_1} {f : α → ENNReal} {ι : Type u_4} (s : ι → Finset α),
  (∀ (t : Finset α), ∃ i, t ⊆ s i) → ∑' (a : α), f a = ⨆ i, ∑ a ∈ s i, f a
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rci.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rci α}, r.iter.toArray = r.toArray
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.join.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.WSeq α) → Sort u_2) (s : Stream'.WSeq α) (h_1 : Unit → motive none)
  (h_2 : (s : Stream'.WSeq α) → motive (some s)),
  (match some s with
    | none => h_1 ()
    | some s => h_2 s) =
    h_2 s
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
/-- If a product of integers is `-1`, then at least one factor must be `-1`.  -/
List.neg_one_mem_of_prod_eq_neg_one : ∀ {l : List ℤ}, l.prod = -1 → -1 ∈ l
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.symm_image_eq_source_inter_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set Y}, s ⊆ e.target → ↑e.symm '' s = e.source ∩ ↑e ⁻¹' s
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.notMem_of_notMem_closure : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {P : R}, P ∉ NonUnitalSubring.closure s → P ∉ s
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.assoc_tmul : ∀ (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid P] [inst_13 : Module A P] [inst_14 : AddCommMonoid Q] [inst_15 : Module R Q]
  [inst_16 : Module R P] [inst_17 : IsScalarTower R A P] [inst_18 : Algebra A B] [inst_19 : IsScalarTower A B M] (m : M)
  (p : P) (q : Q), (TensorProduct.AlgebraTensorModule.assoc R A B M P Q) (m ⊗ₜ[A] p ⊗ₜ[R] q) = m ⊗ₜ[A] (p ⊗ₜ[R] q)
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The inverse functor used to define the equivalence `ofCommaFstEquivalence`.  -/
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor C T) →
              (G : CategoryTheory.Functor D T) →
                (c : C) →
                  CategoryTheory.Functor (CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G)
                    (CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c)
-- Mathlib.Order.Ideal
Order.Ideal.instSetLike : {P : Type u_1} → [inst : LE P] → SetLike (Order.Ideal P) P
-- Lean.Server.FileWorker.Utils
/-- Collects diagnostics for a `textDocument/publishDiagnostics` notification, updates
the incremental tracking fields and writes the notification to the client.

When `incrementalDiagnosticSupport` is `true` and the state allows it, sends only
the newly added diagnostics with `isIncremental? := some true`. Otherwise, sends
all sticky and non-sticky diagnostics non-incrementally.

The state update and the write are performed atomically under the diagnostics mutex
to prevent reordering between concurrent publishers (the reporter task and the main thread).
 -/
Lean.Server.FileWorker.EditableDocumentCore.publishDiagnostics : Lean.Server.FileWorker.EditableDocumentCore →
  Bool → (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams → BaseIO Unit) → BaseIO Unit
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Conclude that `HD`, being Lipschitz, is continuous  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.HD_continuous : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] [Nonempty X] [Nonempty Y],
  Continuous GromovHausdorff.HD
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.comul_tensorObj : ∀ {R : Type u} [inst : CommRing R] {M N : Type u} [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Coalgebra R M] [inst_6 : Coalgebra R N],
  CoalgebraStruct.comul = CoalgebraStruct.comul
-- Mathlib.Tactic.ProxyType
/-- Construct the `Sum` expression, using `decorateSum` to adjust each `Sum`.  -/
_private.Mathlib.Tactic.ProxyType.0.Mathlib.ProxyType.defaultMkProxyType.mkCType : (Lean.Expr → Lean.Elab.TermElabM Lean.Expr) → List Lean.Expr → Lean.Elab.TermElabM (Lean.Expr × Lean.TSyntax `tactic)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.Collector.State.done : Lean.Meta.Grind.Collector.State✝ → Bool
-- Mathlib.Analysis.Normed.Module.TransferInstance
/-- Transfer a `SeminormedAddCommGroup` across an `Equiv`  -/
Equiv.seminormedAddCommGroup : {α : Type u_1} → {β : Type u_2} → [SeminormedAddCommGroup β] → α ≃ β → SeminormedAddCommGroup α
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ici_pow_eq : ∀ {α : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [CanonicallyOrderedMul α] [MulRightMono α] {a : α} (n : ℕ),
  n ≠ 0 → Set.Ici a ^ n = Set.Ici (a ^ n)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Adjunction.projective_of_map_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Full] [F.Faithful] (P : C),
  CategoryTheory.Projective (F.obj P) → CategoryTheory.Projective P
-- Mathlib.Algebra.Ring.Subring.Basic
/-- A subring is isomorphic to its image under an injective function  -/
Subring.equivMapOfInjective : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocRing R] →
      [inst_1 : NonAssocRing S] → (s : Subring R) → (f : R →+* S) → Function.Injective ⇑f → ↥s ≃+* ↥(Subring.map f s)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.isRightAdjoint_post : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasPushouts D] {Y : D} {G : CategoryTheory.Functor D C} [G.IsRightAdjoint],
  (CategoryTheory.Under.post G).IsRightAdjoint
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.unop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ}, S.ShortExact → S.unop.ShortExact
-- Mathlib.Data.Multiset.Basic
Multiset.length_toList : ∀ {α : Type u_1} (s : Multiset α), s.toList.length = s.card
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- The inverse of an element of the dihedral group.
 -/
_private.Mathlib.GroupTheory.SpecificGroups.Dihedral.0.DihedralGroup.inv : {n : ℕ} → DihedralGroup n → DihedralGroup n
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Weights for expressing the subtraction of two points as a `weightedVSub`.  -/
Finset.weightedVSubVSubWeights : (k : Type u_1) → [Ring k] → {ι : Type u_4} → [DecidableEq ι] → ι → ι → ι → k
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.UnivEigenvalues.instDecidableEq : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → [DecidableEq R] → (f : Module.End R M) → (k : ℕ∞) → DecidableEq (f.UnifEigenvalues k)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instCommMonoid.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : CommMonoid M] [inst_2 : ContinuousMul M],
  SeparationQuotient.instCommMonoid = { toMonoid := SeparationQuotient.instMonoid, mul_comm := ⋯ }
-- Std.Http.Data.Body.Length
/-- Indicates that the HTTP message body has a **fixed, known length**, as specified by the
`Content-Length` header.
 -/
Std.Http.Body.Length.fixed : ℕ → Std.Http.Body.Length
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.all_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {p : α → β → Bool}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.all p = t₂.all p
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_rci : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toArray (Std.Rci.Sliceable.mkSlice xs lo...*) = (Std.Slice.toArray xs).extract lo
-- Mathlib.MeasureTheory.Measure.Restrict
/-- Restriction of a measure to a subset is monotone both in set and in measure.  -/
MeasureTheory.Measure.restrict_mono : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄,
  s ⊆ s' → ∀ ⦃μ ν : MeasureTheory.Measure α⦄, μ ≤ ν → μ.restrict s ≤ ν.restrict s'
-- Init.Data.SInt.Bitwise
Int16.not_eq_neg_add : ∀ (a : Int16), ~~~a = -a - 1
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.CWComplex.mem_skeleton_iff`. -/
Topology.CWComplex.exists_mem_openCell_of_mem_skeleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C : Set X} [inst : T2Space X] [inst_1 : Topology.CWComplex C] {n : ℕ∞}
  {x : X}, x ∈ Topology.RelCWComplex.skeleton C n ↔ ∃ m, ∃ (_ : ↑m ≤ n), ∃ j, x ∈ Topology.RelCWComplex.openCell m j
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.LpToLpRestrictCLM_coeFn : ∀ {X : Type u_1} {F : Type u_4} {mX : MeasurableSpace X} (𝕜 : Type u_5) [inst : NormedRing 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : Module 𝕜 F] [inst_3 : IsBoundedSMul 𝕜 F] {p : ENNReal}
  {μ : MeasureTheory.Measure X} [inst_4 : Fact (1 ≤ p)] (s : Set X) (f : ↥(MeasureTheory.Lp F p μ)),
  ↑↑((MeasureTheory.LpToLpRestrictCLM X F 𝕜 μ p s) f) =ᵐ[μ.restrict s] ↑↑f
-- Mathlib.Data.Finset.Sups
/-- `s ⊼ t` is the finset of elements of the form `a ⊓ b` where `a ∈ s`, `b ∈ t`.  -/
Finset.hasInfs : {α : Type u_2} → [DecidableEq α] → [SemilatticeInf α] → HasInfs (Finset α)
-- Init.Data.UInt.Basic
instAddUInt16 : Add UInt16
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.unop_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F.op),
  c.unop.π = CategoryTheory.NatTrans.removeOp c.ι
-- Mathlib.Topology.WithTopology
WithTopology.instFinite : ∀ {X : Type u_1} (t : TopologicalSpace X) [Finite X], Finite (WithTopology X t)
-- Init.Data.List.Sublist
List.infix_append_iff : ∀ {α : Type u} {l xs ys : List α},
  l <:+: xs ++ ys ↔ l <:+: xs ∨ l <:+: ys ∨ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁ <:+ xs ∧ l₂ <+: ys