mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Rule
Aesop.instInhabitedUnsafeRuleInfo : Inhabited Aesop.UnsafeRuleInfo
-- Mathlib.LinearAlgebra.SModEq.Basic
/-- A predicate saying two elements of a module are equivalent modulo a submodule.  -/
SModEq : {R : Type u_1} →
  [inst : Ring R] → {M : Type u_4} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Submodule R M → M → M → Prop
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.BifibrantObject.homMk_homMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_4 : CategoryTheory.Limits.HasTerminal C] {X Y Z : C} [inst_5 : HomotopicalAlgebra.IsCofibrant X]
  [inst_6 : HomotopicalAlgebra.IsCofibrant Y] [inst_7 : HomotopicalAlgebra.IsCofibrant Z]
  [inst_8 : HomotopicalAlgebra.IsFibrant X] [inst_9 : HomotopicalAlgebra.IsFibrant Y]
  [inst_10 : HomotopicalAlgebra.IsFibrant Z] (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.BifibrantObject.homMk f)
      (HomotopicalAlgebra.BifibrantObject.homMk g) =
    HomotopicalAlgebra.BifibrantObject.homMk (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ],
  (↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.mappingCone.inl φ) ⋯ +
      (CochainComplex.mappingCone.snd φ).comp
        (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.inr φ)) ⋯ =
    CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.id (CochainComplex.mappingCone φ))
-- Mathlib.Analysis.Normed.Group.Basic
coe_normGroupSeminorm : ∀ (E : Type u_5) [inst : SeminormedGroup E], ⇑(normGroupSeminorm E) = norm
-- Mathlib.RingTheory.Ideal.Span
IsPrincipalIdealRing.mk : ∀ {R : Type u} [inst : Semiring R], (∀ (S : Ideal R), Submodule.IsPrincipal S) → IsPrincipalIdealRing R
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesFunctor_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.opcyclesFunctor C).obj S = S.opcycles
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The left arrow of the walking span.  -/
CategoryTheory.Limits.WalkingSpan.Hom.fst : CategoryTheory.Limits.WalkingSpan.zero ⟶ CategoryTheory.Limits.WalkingSpan.left
-- Init.Data.Order.Lemmas
Std.Antisymm.trichotomous_of_antisymm_not : ∀ {α : Sort u_1} {r : α → α → Prop} [i : Std.Antisymm fun x1 x2 => ¬r x1 x2], Std.Trichotomous r
-- Mathlib.Algebra.BigOperators.Ring.List
List.prod_ne_zero : ∀ {M₀ : Type u_4} [inst : MonoidWithZero M₀] {l : List M₀} [Nontrivial M₀] [NoZeroDivisors M₀], 0 ∉ l → l.prod ≠ 0
-- Mathlib.Topology.Order.Basic
/-- A set in a nontrivial densely linear ordered type is dense in the sense of topology if and only
if for any `a < b` there exists `c ∈ s`, `a < c < b`. Each implication requires less typeclass
assumptions.  -/
dense_iff_exists_between : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] [Nontrivial α]
  {s : Set α}, Dense s ↔ ∀ (a b : α), a < b → ∃ c ∈ s, a < c ∧ c < b
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_inv_naturality_right_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h')
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h').inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) h_1)
-- Mathlib.Topology.Semicontinuity.Defs
LowerSemicontinuousAt.lowerSemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α} (s : Set α),
  LowerSemicontinuousAt f x → LowerSemicontinuousWithinAt f s x
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.op.eq_1 : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G),
  H.op = { carrier := MulOpposite.unop ⁻¹' ↑H, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.Control.ULiftable
ULiftable.congr : {f : outParam (Type u₀ → Type u₁)} →
  {g : Type v₀ → Type v₁} → [self : ULiftable f g] → {α : Type u₀} → {β : Type v₀} → α ≃ β → f α ≃ g β
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.restrictScalar_directSumRight : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_2) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type v₂}
  [inst_3 : DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'] (S₀ : Type u_1) [inst_10 : CommSemiring S₀]
  [inst_11 : Algebra R S₀] [inst_12 : Algebra S₀ S] [inst_13 : Module S₀ M₁'] [inst_14 : IsScalarTower R S₀ M₁']
  [inst_15 : IsScalarTower S₀ S M₁'],
  LinearEquiv.restrictScalars S₀ (TensorProduct.directSumRight R S M₁' M₂) = TensorProduct.directSumRight R S₀ M₁' M₂
-- Mathlib.Tactic.CategoryTheory.BicategoryCoherence
Mathlib.Tactic.BicategoryCoherence.liftHomOf : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → {a b : B} → (f : a ⟶ b) → Mathlib.Tactic.BicategoryCoherence.LiftHom f
-- Mathlib.Algebra.Homology.BifunctorAssociator
/-- Given bifunctors `F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂`, `G : C₁₂ ⥤ C₃ ⥤ C₄`, homological complexes
`K₁ : HomologicalComplex C₁ c₁`, `K₂ : HomologicalComplex C₂ c₂` and
`K₃ : HomologicalComplex C₃ c₃`, and complexes shapes `c₁₂`, `c₄`, this asserts
that for all `i₁₂ : ι₁₂` and `i₃ : ι₃`, the functor `G(-, K₃.X i₃)` commutes with
the coproducts of the `F₁₂(X₁ i₁, X₂ i₂)` such that `π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂`.  -/
HomologicalComplex.HasGoodTrifunctor₁₂Obj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₁₂ : Type u_3} →
      {C₃ : Type u_5} →
        {C₄ : Type u_6} →
          [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
            [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
              [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] →
                [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] →
                    [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                      [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                        [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃] →
                          CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂) →
                            CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄) →
                              {ι₁ : Type u_7} →
                                {ι₂ : Type u_8} →
                                  {ι₃ : Type u_9} →
                                    {ι₁₂ : Type u_10} →
                                      {ι₄ : Type u_12} →
                                        {c₁ : ComplexShape ι₁} →
                                          {c₂ : ComplexShape ι₂} →
                                            {c₃ : ComplexShape ι₃} →
                                              HomologicalComplex C₁ c₁ →
                                                HomologicalComplex C₂ c₂ →
                                                  HomologicalComplex C₃ c₃ →
                                                    (c₁₂ : ComplexShape ι₁₂) →
                                                      (c₄ : ComplexShape ι₄) →
                                                        [TotalComplexShape c₁ c₂ c₁₂] →
                                                          [TotalComplexShape c₁₂ c₃ c₄] → Prop
-- Mathlib.RingTheory.Ideal.Operations
Ideal.le_radical : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I ≤ I.radical
-- Mathlib.RingTheory.Valuation.Basic
Valuation.one_apply_eq_one_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : Nontrivial R]
  [inst_3 : NoZeroDivisors R] [inst_4 : DecidablePred fun x => x = 0] [Nontrivial Γ₀] {x : R}, 1 x = 1 ↔ x ≠ 0
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
exists_maximalIdeal_pow_eq_of_principal : ∀ (R : Type u_1) [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] [IsDomain R],
  Submodule.IsPrincipal (IsLocalRing.maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = IsLocalRing.maximalIdeal R ^ n
-- Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered
/-- Variant of `descColimitType_injective_iff_of_isFiltered` where we
assume both elements `x` and `x'` are in the same type `F.obj j`.  -/
CategoryTheory.Functor.CoconeTypes.descColimitType_injective_iff_of_isFiltered' : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFiltered J]
  {F : CategoryTheory.Functor J (Type w₀)} (c : F.CoconeTypes),
  Function.Injective (F.descColimitType c) ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' →
        ∃ k f, (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f)) x'
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.minKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne
SSet.stdSimplex.objMk₁_bijective : ∀ {n : ℕ}, Function.Bijective SSet.stdSimplex.objMk₁
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_fun_getElem : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] (l : List ι) (f : ι → M), ∏ i, f l[↑i] = (List.map f l).prod
-- Std.Data.Internal.List.Associative
Std.Internal.List.contains_of_contains_insertList_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true →
    Std.Internal.List.containsKey k toInsert = false → Std.Internal.List.containsKey k l = true
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterMapWithPostcondition.match_1.splitter : {β β' : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → Std.Iterators.PostconditionT n (Option β')} →
      (out : β) →
        (motive : Subtype (f out).Property → Sort u_3) →
          (__do_lift : Subtype (f out).Property) →
            ((h' : (f out).Property none) → motive ⟨none, h'⟩) →
              ((out' : β') → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩) → motive __do_lift
-- Init.Data.UInt.Bitwise
UInt16.ofBitVec_shiftRight : ∀ (a : BitVec 16), ∀ b < 16, { toBitVec := a >>> b } = { toBitVec := a } >>> UInt16.ofNat b
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel.name.injEq : ∀ (name name_1 : String),
  (Lean.Lsp.ParameterInformationLabel.name name = Lean.Lsp.ParameterInformationLabel.name name_1) = (name = name_1)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Option.isNone.eq_1 : ∀ {α : Type u_1} (val : α), (some val).isNone = false
-- Init.Data.Fin.Lemmas
Fin.pred_eq_iff_eq_succ : ∀ {n : ℕ} {i : Fin (n + 1)} (hi : i ≠ 0) {j : Fin n}, i.pred hi = j ↔ i = j.succ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} {l : List α} {k : α}
  {h' : k ∈ Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l) k h' = ()
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.RecCallCache.mk''.sizeOf_spec : ∀ (callerName : Lean.Name) (decrTactic? : Option Lean.Elab.DecreasingBy)
  (callerMeasures calleeMeasures : Array Lean.Elab.WF.GuessLex.BasicMeasure)
  (rcc : Lean.Elab.WF.GuessLex.RecCallWithContext)
  (cache : IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel)))),
  sizeOf
      { callerName := callerName, decrTactic? := decrTactic?, callerMeasures := callerMeasures,
        calleeMeasures := calleeMeasures, rcc := rcc, cache := cache } =
    1 + sizeOf callerName + sizeOf decrTactic? + sizeOf callerMeasures + sizeOf calleeMeasures + sizeOf rcc +
      sizeOf cache
-- Lean.Util.CollectFVars
Lean.CollectFVars.State.add : Lean.CollectFVars.State → Lean.FVarId → Lean.CollectFVars.State
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsBase.spanning_of_superset : ∀ {α : Type u_2} {M : Matroid α} {X B : Set α},
  M.IsBase B → B ⊆ X → autoParam (X ⊆ M.E) Matroid.IsBase.spanning_of_superset._auto_1 → M.Spanning X
-- Batteries.Data.Nat.Bisect
Nat.le_avg_right : ∀ {b a : ℕ}, b ≤ a → b ≤ a.avg b
-- Mathlib.Algebra.Group.InjSurj
/-- A type has an involutive negation if it admits a surjective map that
preserves `-` to a type which has an involutive negation.  -/
Function.Injective.involutiveNeg : {M₂ : Type u_2} →
  {M₁ : Type u_3} →
    [inst : Neg M₁] →
      [inst_1 : InvolutiveNeg M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x : M₁), f (-x) = -f x) → InvolutiveNeg M₁
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.mk.injEq : ∀ {R : Type u} (a₁ a₂ a₃ a₄ a₆ a₁_1 a₂_1 a₃_1 a₄_1 a₆_1 : R),
  ({ a₁ := a₁, a₂ := a₂, a₃ := a₃, a₄ := a₄, a₆ := a₆ } =
      { a₁ := a₁_1, a₂ := a₂_1, a₃ := a₃_1, a₄ := a₄_1, a₆ := a₆_1 }) =
    (a₁ = a₁_1 ∧ a₂ = a₂_1 ∧ a₃ = a₃_1 ∧ a₄ = a₄_1 ∧ a₆ = a₆_1)
-- Mathlib.AlgebraicGeometry.Over
/-- Given a morphism `X ⟶ Y` with `f.IsOver S`, this is the bundled morphism in `Over S`.  -/
AlgebraicGeometry.Scheme.Hom.asOver : {X Y : AlgebraicGeometry.Scheme} →
  (f : X.Hom Y) →
    (S : AlgebraicGeometry.Scheme) →
      [inst : X.Over S] →
        [inst_1 : Y.Over S] → [f.IsOver S] → CategoryTheory.OverClass.asOver X S ⟶ CategoryTheory.OverClass.asOver Y S
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_uInt64ToBitVec : ∀ (x : UInt64), Int64.ofBitVec x.toBitVec = x.toInt64
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- Predicate ensuring that, at all points of a set, a function can have at most one derivative.  -/
UniqueMDiffOn : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H → {M : Type u_4} → [inst : TopologicalSpace M] → [ChartedSpace H M] → Set M → Prop
-- Init.Data.Array.Lemmas
Array.allM_congr : ∀ {m : Type → Type u_1} {α : Type u_2} {start₁ start₂ stop₁ stop₂ : ℕ} [inst : Monad m] {xs ys : Array α},
  xs = ys →
    ∀ {p q : α → m Bool},
      (∀ (a : α), p a = q a) →
        start₁ = start₂ → stop₁ = stop₂ → Array.allM p xs start₁ stop₁ = Array.allM q ys start₂ stop₂
-- Mathlib.CategoryTheory.Monad.Equalizer
CategoryTheory.Comonad.instIsCoreflexivePairCoalgebraTopMapBottomMap : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Comonad C} (X : T.Coalgebra),
  CategoryTheory.IsCoreflexivePair (CategoryTheory.Comonad.CofreeEqualizer.topMap X)
    (CategoryTheory.Comonad.CofreeEqualizer.bottomMap X)
-- Mathlib.Tactic.FunProp.Mor
/-- Argument of morphism application that stores corresponding coercion if necessary  -/
Mathlib.Meta.FunProp.Mor.Arg : Type
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.preimage_symm_proj_inter : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) (s : Set B),
  ↑e.symm ⁻¹' proj ⁻¹' s ∩ e.baseSet ×ˢ Set.univ = (s ∩ e.baseSet) ×ˢ Set.univ
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.bind_dmap_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (x : Option α) (f : (a : α) → x = some a → β) (g : β → Option γ),
  (Std.Internal.List.Option.dmap✝ x f).bind g = x.pbind fun a h => g (f a h)
-- Mathlib.Order.Interval.Set.Pi
/-- **Alias** of `Set.Icc_sdiff_pi_univ_Ioo_subset`.

---

If `x`, `y`, `x'`, and `y'` are functions `Π i : ι, α i`, then
the set difference between the box `[x, y]` and the product of the open intervals `(x' i, y' i)`
is covered by the union of the following boxes: for each `i : ι`, we take
`[x, update y i (x' i)]` and `[update x i (y' i), y]`.

E.g., if `x' = x` and `y' = y`, then this lemma states that the difference between a closed box
`[x, y]` and the corresponding open box `{z | ∀ i, x i < z i < y i}` is covered by the union
of the faces of `[x, y]`.  -/
Set.Icc_diff_pi_univ_Ioo_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → LinearOrder (α i)]
  (x y x' y' : (i : ι) → α i),
  (Set.Icc x y \ Set.univ.pi fun i => Set.Ioo (x' i) (y' i)) ⊆
    (⋃ i, Set.Icc x (Function.update y i (x' i))) ∪ ⋃ i, Set.Icc (Function.update x i (y' i)) y
-- Lean.Data.JsonRpc
Lean.IO.FS.Stream.writeRequest : {α : Type u_1} → [Lean.ToJson α] → IO.FS.Stream → Lean.JsonRpc.Request α → IO Unit
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- "A special case of `Multipliable.map_iff_of_leftInverse` for convenience"  -/
Multipliable.map_iff_of_equiv : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {L : SummationFilter β} [inst_2 : CommMonoid γ] [inst_3 : TopologicalSpace γ] {G : Type u_4}
  [inst_4 : EquivLike G α γ] [MulEquivClass G α γ] (g : G),
  Continuous ⇑g → Continuous (EquivLike.inv g) → (Multipliable (⇑g ∘ f) L ↔ Multipliable f L)
-- Mathlib.Algebra.Order.Field.Basic
div_pos_iff_of_pos_right : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α],
  0 < b → (0 < a / b ↔ 0 < a)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.homInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → {A B : CategoryTheory.Mon C} → (M : Bimod A B) → Inhabited (M.Hom M)
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.toSupHom : {α : Type u_6} →
  {β : Type u_7} → [inst : Max α] → [inst_1 : Max β] → [inst_2 : Bot α] → [inst_3 : Bot β] → SupBotHom α β → SupHom α β
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.isNextArgAccessible : Lean.Elab.Term.CollectPatternVars.Context → Bool
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.xNextIso.congr_simp : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j), C.xNextIso r = C.xNextIso r
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat.sizeOf_spec : ∀ (e : Lean.Expr) (natStructId : ℕ) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat e natStructId lhs rhs) =
    1 + sizeOf e + sizeOf natStructId + sizeOf lhs + sizeOf rhs
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_inl_inr : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.inl R M M₂).coprod (LinearMap.inr R M M₂) = LinearMap.id
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Preadditive.isWeakLimitForkOfKernelFork_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {f g : X ⟶ Y} {c : CategoryTheory.Limits.KernelFork (f - g)} (i : CategoryTheory.Limits.IsWeakLimit c)
  (s : CategoryTheory.Limits.Fork f g),
  (CategoryTheory.Preadditive.isWeakLimitForkOfKernelFork i).lift s =
    i.lift (CategoryTheory.Preadditive.kernelForkOfFork s)
-- Mathlib.Algebra.Group.TransferInstance
Equiv.addMonoid.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : AddMonoid β], e.addMonoid = Function.Injective.addMonoid ⇑e ⋯ ⋯ ⋯ ⋯
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.trans : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {l : Filter α} {f g h : α → β}, f ≤ᶠ[l] g → g ≤ᶠ[l] h → f ≤ᶠ[l] h
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.terminal_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Factorisation.terminal.ι = f
-- Mathlib.Algebra.BigOperators.Finprod
finprod_congr : ∀ {M : Type u_2} {α : Sort u_4} [inst : CommMonoid M] {f g : α → M}, (∀ (x : α), f x = g x) → finprod f = finprod g
-- Std.Sat.AIG.Basic
/-- A reference to a node within an AIG.
 -/
Std.Sat.AIG.Ref : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Type
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- A function `f` is called *interval integrable* with respect to a measure `μ` on an unordered
interval `a..b` if it is integrable on both intervals `(a, b]` and `(b, a]`. One of these
intervals is always empty, so this property is equivalent to `f` being integrable on
`(min a b, max a b]`.  -/
IntervalIntegrable : {ε : Type u_3} → [inst : TopologicalSpace ε] → [ENormedAddMonoid ε] → (ℝ → ε) → MeasureTheory.Measure ℝ → ℝ → ℝ → Prop
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangentAt.inner_right_eq_zero_of_mem : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p : P} {as : AffineSubspace ℝ P},
  s.IsTangentAt p as → ∀ {x : P}, x ∈ as → inner ℝ (p -ᵥ s.center) (x -ᵥ p) = 0
-- Mathlib.Algebra.Category.Grp.Zero
AddGrpCat.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddGrpCat
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- Unexpander for the notation `|a|ₘ` for `mabs a`.
Tries to add discretionary parentheses in unparsable cases.  -/
mabs.unexpander : Lean.PrettyPrinter.Unexpander
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.defEvalConfigItem.mkCmd : Option (Lean.TSyntax `Lean.Parser.Command.docComment) →
  Option (Lean.TSyntax `Lean.Parser.Command.visibility) →
    Lean.Syntax →
      Lean.Ident →
        Lean.Ident →
          Lean.TSyntaxArray `Lean.Parser.Term.bracketedBinder →
            Lean.Elab.ConfigEval.EvalConfigItemView → Lean.Name → Lean.Elab.TermElabM Lean.Command
-- Mathlib.Data.Multiset.MapFold
/-- **Alias** of the reverse direction of `Multiset.nodup_attach`. -/
Multiset.Nodup.attach : ∀ {α : Type u_1} {s : Multiset α}, s.Nodup → s.attach.Nodup
-- Init.Core
Task.pure.injEq : ∀ {α : Type u} (get get_1 : α), ({ get := get } = { get := get_1 }) = (get = get_1)