mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.id_whiskerRight_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} {M : Bimod X Y} {N : Bimod Y Z},
  Bimod.whiskerRight (CategoryTheory.CategoryStruct.id M) N = CategoryTheory.CategoryStruct.id (M.tensorBimod N)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.fderivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {m n : WithTop ℕ∞},
  ContDiffOn 𝕜 n f s → UniqueDiffOn 𝕜 s → m + 1 ≤ n → ContDiffOn 𝕜 m (fderivWithin 𝕜 f s) s
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Get a prefix of `n₁` that is related to any prefix of the names in `ns`; return the prefixes.

This should be more efficient than iterating over all names in `ns` and calling `find`,
since it doesn't need to worry about overlapping prefixes.
 -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.NamePrefixRel.findAny : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝ → Lean.Name → Array Lean.Name → Option (Lean.Name × Lean.Name)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_lt_one_cert : Lean.Grind.Linarith.Poly → Bool
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.map_eq_iff : ∀ {𝕜 : Type u_1} {V₁' : Type u_4} {V₂ : Type u_5} {P₁' : Type u_9} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V₁'] [inst_2 : NormedSpace 𝕜 V₁'] [inst_3 : MetricSpace P₁']
  [inst_4 : NormedAddTorsor V₁' P₁'] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (f₁ : P₁' →ᵃⁱ[𝕜] P₂) {x y : P₁'}, f₁ x = f₁ y ↔ x = y
-- Init.Data.BitVec.Lemmas
BitVec.toNat_flattenList_append : ∀ {n : ℕ} (l r : List (BitVec n)),
  (BitVec.flattenList (l ++ r)).toNat = (BitVec.flattenList l).toNat <<< (n * r.length) ||| (BitVec.flattenList r).toNat
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.sub_mul_right_right_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime x (y - z * x) ↔ IsRelPrime x y
-- Init.Data.Option.Lemmas
Option.filter_some_eq_none : ∀ {α : Type u_1} {p : α → Bool} {a : α}, Option.filter p (some a) = none ↔ ¬p a = true
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_support_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq β] {f : α → β}
  (s : α →₀ M), Set.InjOn f ↑s.support → (Finsupp.mapDomain f s).support = Finset.image f s.support
-- Init.Prelude
/-- Extracts a wrapped value from a universe-lifted type.  -/
PULift.down : {α : Sort s} → PULift α → α
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- `symm` is `none` if the given relations are symmetric.
`symm` is `true` when you can only rewrite from right to left.  -/
Mathlib.Tactic.ClickSuggestions.GrwPos.symm? : Mathlib.Tactic.ClickSuggestions.GrwPos → Option Bool
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.arg.sizeOf_spec : ∀ (a b : Lean.Expr) (i : ℕ) (eq : Lean.Expr) (source : Lean.Meta.Grind.SplitSource),
  sizeOf (Lean.Meta.Grind.SplitInfo.arg a b i eq source) =
    1 + sizeOf a + sizeOf b + sizeOf i + sizeOf eq + sizeOf source
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `fallback` if no such pair exists.
 -/
Std.TreeMap.getEntryLTD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α × β → α × β
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_of_not_sigmaFinite : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (hm : m ≤ m₀),
  ¬MeasureTheory.SigmaFinite (μ.trim hm) → μ[f | m] = 0
-- Mathlib.Logic.Small.Set
small_diff : ∀ {α : Type u1} (s t : Set α) [Small.{u, u1} ↑s], Small.{u, u1} ↑(s \ t)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.repr_toLin : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype n] [inst_2 : Finite m]
  [inst_3 : DecidableEq n] {M₁ : Type u_5} {M₂ : Type u_6} [inst_4 : AddCommMonoid M₁] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₁] [inst_7 : Module R M₂] (v₁ : Module.Basis n R M₁) (v₂ : Module.Basis m R M₂) (M : Matrix m n R)
  (x : M₁), ⇑(v₂.repr (((Matrix.toLin v₁ v₂) M) x)) = M.mulVec ⇑(v₁.repr x)
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_toBitVec : ∀ (x : Int64), Int64.ofBitVec x.toBitVec = x
-- Mathlib.LinearAlgebra.Quotient.Pi
/-- Lift a family of maps to a quotient of direct sums.  -/
Submodule.quotientPiLift : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {Ms : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommGroup (Ms i)] →
          [inst_2 : (i : ι) → Module R (Ms i)] →
            {Ns : ι → Type u_5} →
              [inst_3 : (i : ι) → AddCommGroup (Ns i)] →
                [inst_4 : (i : ι) → Module R (Ns i)] →
                  (p : (i : ι) → Submodule R (Ms i)) →
                    (f : (i : ι) → Ms i →ₗ[R] Ns i) →
                      (∀ (i : ι), p i ≤ (f i).ker) → ((i : ι) → Ms i) ⧸ Submodule.pi Set.univ p →ₗ[R] (i : ι) → Ns i
-- Mathlib.Algebra.Exact.Basic
LinearMap.exact_of_comp_of_mem_range : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  g ∘ₗ f = 0 → (∀ (x : N), g x = 0 → x ∈ f.range) → Function.Exact ⇑f ⇑g
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlDisplay : ProofWidgets.Component ProofWidgets.HtmlDisplayProps
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instAddGroup : {M : Type u_2} →
  {N : Type u_3} →
    {X : Type u_4} →
      {Y : Type u_5} →
        {σ : M → N} → [inst : SMul M X] → [inst_1 : AddGroup Y] → [inst_2 : DistribSMul N Y] → AddGroup (X →ₑ[σ] Y)
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.coe_comp_sup_hom' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedLatticeHom β γ)
  (g : BoundedLatticeHom α β),
  { toFun := ⇑f ∘ ⇑g, map_sup' := ⋯ } = { toFun := ⇑f, map_sup' := ⋯ }.comp { toFun := ⇑g, map_sup' := ⋯ }
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- `it.PlausibleStep step` is the proposition that `step` is a possible next step from the
`filterMap` iterator `it`. This is mostly internally relevant, except if one needs to manually
prove termination (`Finite` or `Productive` instances, for example) of a `filterMap` iterator.
 -/
Std.Iterators.Types.FilterMap.PlausibleStep : {α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      {lift : ⦃α : Type w⦄ → m α → n α} →
        {f : β → Std.Iterators.PostconditionT n (Option γ)} →
          [Std.Iterator α m β] → Std.IterM n γ → Std.IterStep (Std.IterM n γ) γ → Prop
-- Init.Data.String.PosRaw
String.pos_lt_eq : ∀ (p₁ p₂ : String.Pos.Raw), (p₁ < p₂) = (p₁.byteIdx < p₂.byteIdx)
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  ProbabilityTheory.IsZeroOrMarkovKernel 0
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.neg_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.neg.h₁ = -h.h₁
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
/-- Auxiliary definition for `LeftResolution.karoubi`.  -/
CategoryTheory.Abelian.LeftResolution.karoubi.F : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} →
          CategoryTheory.Abelian.LeftResolution ι →
            [CategoryTheory.Preadditive C] →
              [CategoryTheory.Preadditive A] →
                CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi A) (CategoryTheory.Idempotents.Karoubi C)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.instHSubDuration_1 : HSub Std.Time.Timestamp Std.Time.Timestamp Std.Time.Duration
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.ne_bot_iff_exists_ne_one : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H ≠ ⊥ ↔ ∃ a, a ≠ 1
-- Mathlib.Dynamics.Transitive
AddAction.IsTopologicallyTransitive.mk : ∀ {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst_1 : TopologicalSpace α] [inst_2 : AddAction M α],
  (∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, ((m +ᵥ U) ∩ V).Nonempty) →
    AddAction.IsTopologicallyTransitive M α
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsComplete.eq_1 : ∀ {α : Type u} [uniformSpace : UniformSpace α] (s : Set α),
  IsComplete s = ∀ (f : Filter α), Cauchy f → f ≤ Filter.principal s → ∃ x ∈ s, f ≤ nhds x
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.zero_snd : ∀ {A : Type u_2} {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F], 0.2 = 0
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokensLegend.toJson : Lean.Lsp.SemanticTokensLegend → Lean.Json
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
/-- Vertical inverse of the 2-commutative square of
`CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctor`.
 -/
CategoryTheory.Functor.instCatCommSqTriangleOppositeMapTriangleOpInverseTriangleOpEquivalence : {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.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.CommShift ℤ] →
                CategoryTheory.CatCommSq F.op.mapTriangle
                  (CategoryTheory.Pretriangulated.triangleOpEquivalence C).inverse
                  (CategoryTheory.Pretriangulated.triangleOpEquivalence D).inverse F.mapTriangle.op
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  (Std.TreeMap.unitOfList l cmp)[k]? = if l.contains k = true then some () else none
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffOn.div : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieGroup I n G] {f g : M → G} {s : Set M},
  ContMDiffOn I' I n f s → ContMDiffOn I' I n g s → ContMDiffOn I' I n (fun x => f x / g x) s
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
instInhabitedWeakDual : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : CommSemiring 𝕜] →
      [inst_1 : TopologicalSpace 𝕜] →
        [inst_2 : ContinuousAdd 𝕜] →
          [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
            [inst_4 : AddCommMonoid E] →
              [inst_5 : Module 𝕜 E] → [inst_6 : TopologicalSpace E] → Inhabited (WeakDual 𝕜 E)
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.directLimitDiagram_map : ∀ {R : Type u} [inst : Ring R] {ι : Type v} [inst_1 : Preorder ι] (G : ι → Type v)
  [inst_2 : (i : ι) → AddCommGroup (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  [inst_4 : DirectedSystem G fun i j h => ⇑(f i j h)] {X Y : ι} (hij : X ⟶ Y),
  (ModuleCat.directLimitDiagram G f).map hij = ModuleCat.ofHom (f X Y ⋯)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_le_minKey!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → (cmp t.minKey! (t.erase k).minKey!).isLE = true
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The first triangle identity for the counit and unit of the adjunction.  -/
CategoryTheory.ExponentiableMorphism.ev_coev_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  (X : CategoryTheory.Over J) {Z : CategoryTheory.Over I}
  (h : (CategoryTheory.ChosenPullbacksAlong.pullback f).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ChosenPullbacksAlong.pullback f).map ((CategoryTheory.ExponentiableMorphism.coev f).app X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ExponentiableMorphism.ev f).app ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj X)) h) =
    h
-- Std.Data.DTreeMap.Raw.Iterator
_private.Std.Data.DTreeMap.Raw.Iterator.0.Std.DTreeMap.Raw.iter.eq_1 : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} (m : Std.DTreeMap.Raw α β cmp),
  m.iter = Std.DTreeMap.Internal.Zipper.iterOfTree m.inner
-- Init.GrindInstances.ToInt
Lean.Grind.instDivUInt16UintOfNatNat : Lean.Grind.ToInt.Div UInt16 (Lean.Grind.IntInterval.uint 16)
-- Std.Time.Duration
/-- Adds an `Hour.Offset` to a `Duration`
 -/
Std.Time.Duration.addHours : Std.Time.Duration → Std.Time.Hour.Offset → Std.Time.Duration
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.zero_lt_prod_node_sub_node : ∀ {n i : ℕ},
  i ≤ n →
    0 < (-1) ^ i * ∏ j ∈ (Finset.range (n + 1)).erase i, (Polynomial.Chebyshev.node n i - Polynomial.Chebyshev.node n j)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₅_app_four : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_449✝ ⟶ g.obj' 0 _proof_449✝) (app₁ : f.obj' 1 _proof_450✝ ⟶ g.obj' 1 _proof_450✝)
  (app₂ : f.obj' 2 _proof_451✝ ⟶ g.obj' 2 _proof_451✝) (app₃ : f.obj' 3 _proof_452✝ ⟶ g.obj' 3 _proof_452✝)
  (app₄ : f.obj' 4 _proof_453✝ ⟶ g.obj' 4 _proof_453✝) (app₅ : f.obj' 5 _proof_454✝ ⟶ g.obj' 5 _proof_454✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
      _auto_502✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_451✝))
      _auto_504✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_452✝))
      _auto_506✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_453✝))
      _auto_508✝)
  (w₄ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅ =
        CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_453✝ _proof_454✝))
      _auto_510✝),
  (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app
      ⟨4, CategoryTheory.ComposableArrows.homMk₅._proof_5⟩ =
    app₄
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.coeff_coeff_optionEquivLeft : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (p : MvPowerSeries (Option σ) R) (n : ℕ) (x : σ →₀ ℕ),
  (MvPowerSeries.coeff x) ((PowerSeries.coeff n) ((MvPowerSeries.optionEquivLeft σ R) p)) =
    (MvPowerSeries.coeff (Finsupp.optionElim n x)) p
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.instMulAction.eq_1 : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Group G] [inst_1 : MulAction G β],
  Function.Embedding.instMulAction = Function.Injective.mulAction DFunLike.coe ⋯ ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], CategoryTheory.NatTrans.CommShift (DerivedCategory.quotientCompQhIso C).hom ℤ
-- Lean.Parser.Tactic
Lean.Parser.Tactic.introMatch.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.leftRel_pi : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Group (β i)] (s' : (i : ι) → Subgroup (β i)),
  QuotientGroup.leftRel (Subgroup.pi Set.univ s') = piSetoid
-- Mathlib.Data.Int.ModEq
Int.ModEq.of_dvd : ∀ {m n a b : ℤ}, m ∣ n → a ≡ b [ZMOD n] → a ≡ b [ZMOD m]
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- A strong natural transformation between oplax functors `F` and `G` is a natural transformation
that is "natural up to 2-isomorphisms".

More precisely, it consists of the following:
* a 1-morphism `η.app a : F.obj a ⟶ G.obj a` for each object `a : B`.
* a 2-isomorphism `η.naturality f : F.map f ≫ app b ≅ app a ≫ G.map f` for each 1-morphism
  `f : a ⟶ b`.
* These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the
  compositions modulo some adjustments of domains and codomains of 2-morphisms.
 -/
CategoryTheory.Oplax.StrongTrans : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.OplaxFunctor B C → CategoryTheory.OplaxFunctor B C → Type (max (max (max u₁ v₁) v₂) w₂)
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.addGroupMultiples.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] {x : M} {n : ℕ} (hpos : 0 < n) (hx : n • x = 0),
  AddSubmonoid.addGroupMultiples hpos hx =
    { toAddMonoid := (AddSubmonoid.multiples x).toAddMonoid, neg := fun x_1 => (n - 1) • x_1, sub := SubNegMonoid.sub',
      zsmul := fun z x_1 => z.natMod ↑n • x_1, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯,
      neg_add_cancel := ⋯ }
-- Mathlib.Data.Seq.Defs
/-- Embed a `MLList α` as a sequence. Note that even though this
is non-meta, it will produce infinite sequences if used with
cyclic `MLList`s created by meta constructions.  -/
Stream'.Seq.ofMLList : {α : Type u} → MLList Id α → Stream'.Seq α
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The map `F.obj' i ⟶ F.obj' j` when `F : ComposableArrows C n`, and `i` and `j`
are natural numbers such that `i ≤ j ≤ n`.  -/
CategoryTheory.ComposableArrows.map' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} →
      (F : CategoryTheory.ComposableArrows C n) →
        (i j : ℕ) →
          (hij : autoParam (i ≤ j) CategoryTheory.ComposableArrows.map'._auto_1) →
            (hjn : autoParam (j ≤ n) CategoryTheory.ComposableArrows.map'._auto_3) → F.obj ⟨i, ⋯⟩ ⟶ F.obj ⟨j, ⋯⟩
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.mk.injEq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (set set_1 : Lean.PersistentHashMap α Unit),
  ({ set := set } = { set := set_1 }) = (set = set_1)
-- Mathlib.Analysis.Normed.Operator.ContinuousAlgEquiv
LinearIsometryEquiv.congr_simp : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Semiring R] [inst_1 : Semiring R₂] (σ₁₂ σ₁₂_1 : R →+* R₂) (e_σ₁₂ : σ₁₂ = σ₁₂_1)
  {σ₂₁ σ₂₁_1 : R₂ →+* R} (e_σ₂₁ : σ₂₁ = σ₂₁_1) [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  (E : Type u_11) (E₂ : Type u_12) [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂]
  [inst_6 : Module R E] [inst_7 : Module R₂ E₂], (E ≃ₛₗᵢ[σ₁₂] E₂) = (E ≃ₛₗᵢ[σ₁₂_1] E₂)
-- Mathlib.Algebra.Group.Basic
div_left_inj : ∀ {G : Type u_3} [inst : Group G] {a b c : G}, b / a = c / a ↔ b = c
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Eta rule for costructured arrows.  -/
CategoryTheory.CostructuredArrow.eta : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T : D} →
          {S : CategoryTheory.Functor C D} →
            (f : CategoryTheory.CostructuredArrow S T) → f ≅ CategoryTheory.CostructuredArrow.mk f.hom
-- Lean.Meta.CoeAttr
Lean.Meta.instInhabitedCoeFnType : Inhabited Lean.Meta.CoeFnType
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The product of `x y : R[M]` is the finitely supported function whose value at `m`
is the sum of `x m₁ * y m₂` over all pairs `m₁, m₂` such that `m₁ * m₂ = m`.  -/
MonoidAlgebra.instMul : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [Mul M] → Mul (MonoidAlgebra R M)
-- Mathlib.Data.List.Chain
/-- The lexicographic order on the `r`-decreasing chains  -/
List.lex_chains : {α : Type u_1} → (r : α → α → Prop) → List.chains r → List.chains r → Prop
-- Mathlib.Order.RelIso.Basic
/-- `Sum.map` as a relation embedding between `Sum.Lex` relations.  -/
RelEmbedding.sumLexMap : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        {r : α → α → Prop} →
          {s : β → β → Prop} → {t : γ → γ → Prop} → {u : δ → δ → Prop} → r ↪r s → t ↪r u → Sum.Lex r t ↪r Sum.Lex s u
-- Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
/-- A form of Chinese remainder theorem for modules, part I: if ideals `Iᵢ` of `R` are pairwise
coprime, then for any `R`-module `M`, the natural map `M → Πᵢ (R ⧸ Iᵢ) ⊗[R] M` is surjective.  -/
Ideal.pi_tensorProductMk_quotient_surjective : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} (M : Type u_3) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (I : ι → Ideal R),
  Pairwise (Function.onFun IsCoprime I) →
    ∀ [Finite ι], Function.Surjective ⇑(LinearMap.pi fun i => (TensorProduct.mk R (R ⧸ I i) M) 1)
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving.mk : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  (∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} [inst : CategoryTheory.Limits.HasPullback f g],
      P g → ∀ (x : ↥X) (y : ↥Y), f x = g y → ∃ a, (CategoryTheory.Limits.pullback.fst f g) a = x) →
    AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_sdiff_cancel : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s ∪ t \ s = t
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_left : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'),
  T = T' → ∀ (f : α → E), MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T' hT' f
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLT_map_ofDual`. -/
List.SortedLT.map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.ofDual) l).SortedLT → l.SortedGT
-- Mathlib.RingTheory.WittVector.StructurePolynomial
constantCoeff_wittStructureRat_zero : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℚ),
  MvPolynomial.constantCoeff (wittStructureRat p Φ 0) = MvPolynomial.constantCoeff Φ