mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_comp : ∀ {X Y Z : SSet} (A : Z.Subcomplex) (f : X ⟶ Y) (g : Y ⟶ Z),
  A.preimage (CategoryTheory.CategoryStruct.comp f g) = (A.preimage g).preimage f
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α],
  t.WF → ∀ {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKey! k = default
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
CategoryTheory.Limits.WalkingMultispan.instFinCategoryOfLOfDecidableEqR : {J : CategoryTheory.Limits.MultispanShape} →
  [Fintype J.L] →
    [Fintype J.R] →
      [DecidableEq J.L] → [DecidableEq J.R] → CategoryTheory.FinCategory (CategoryTheory.Limits.WalkingMultispan J)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (m.insertMany l).getKey? k = m.getKey? k
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.isoShift_hom_naturality_assoc : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] (n : M) {X Y : C} (f : X ⟶ Y) {Z : A}
  (h : (F.shift n).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctor C n).map f))
      (CategoryTheory.CategoryStruct.comp ((F.isoShift n).hom.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((F.isoShift n).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((F.shift n).map f) h)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.mem_uIoo_of_gt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b x : α}, b < x → x < a → x ∈ Set.uIoo a b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.ModObj.lift_leftSMul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] (Z : C) (x : Z ⟶ X) (m : Z ⟶ M),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift m x)
      (CategoryTheory.ModObj.leftSMul M X) =
    CategoryTheory.CartesianMonoidalCategory.lift (m • x) x
-- Mathlib.Topology.Path
/-- Path composition commutes with products  -/
Path.trans_pi_eq_pi_trans : ∀ {ι : Type u_3} {χ : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (χ i)] {as bs cs : (i : ι) → χ i}
  (γ₀ : (i : ι) → Path (as i) (bs i)) (γ₁ : (i : ι) → Path (bs i) (cs i)),
  (Path.pi γ₀).trans (Path.pi γ₁) = Path.pi fun i => (γ₀ i).trans (γ₁ i)
-- Mathlib.Data.Setoid.Basic
/-- The map induced between quotients by a setoid inequality.  -/
Setoid.map_of_le : {α : Type u_1} → {s t : Setoid α} → s ≤ t → Quotient s → Quotient t
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- The canonical cofork `CokernelCofork.ofπ Φ.π Φ.ι_π` exhibits `Φ.π : 𝟭 C ⟶ Φ.quotient` as the
cokernel of `Φ.ι : Φ.r ⟶ 𝟭 C`.  -/
CategoryTheory.Abelian.Preradical.isColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (Φ : CategoryTheory.Abelian.Preradical C) →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ Φ.π ⋯)
-- Mathlib.Topology.List
nhds_list : ∀ {α : Type u_1} [inst : TopologicalSpace α] (as : List α), nhds as = traverse nhds as
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionClientCapabilities.fromJson : Lean.Json → Except String Lean.Lsp.CodeActionClientCapabilities
-- Aesop.Forward.State
Aesop.RuleState.mk : Aesop.ForwardRule →
  Array Aesop.ClusterState → Lean.PHashMap Aesop.Substitution (Lean.PHashSet Aesop.PatSubstSource) → Aesop.RuleState
-- Std.Do.WP.SimpLemmas
Std.Do.WP.throw_MonadExcept : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε : Type u_1} {α : Type u} {e : ε} {Q : Std.Do.PostCond α ps}
  [inst : MonadExceptOf ε m] [inst_1 : Std.Do.WP m ps],
  (Std.Do.wp (throw e)).apply Q = (Std.Do.wp (MonadExceptOf.throw e)).apply Q
-- Mathlib.Order.Filter.Basic
Filter.Eventually.bot_lt_iff_ne_bot : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] [inst_1 : OrderBot β] {l : Filter α} {f : α → β},
  (∀ᶠ (x : α) in l, ⊥ < f x) ↔ ∀ᶠ (x : α) in l, f x ≠ ⊥
-- Mathlib.Algebra.Order.Kleene
/-- Pullback an `IdemCommSemiring` instance along an injective function.  -/
Function.Injective.idemCommSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : IdemCommSemiring α] →
      [inst_1 : LE β] →
        [inst_2 : LT β] →
          [inst_3 : Zero β] →
            [inst_4 : One β] →
              [inst_5 : Add β] →
                [inst_6 : Mul β] →
                  [inst_7 : Pow β ℕ] →
                    [inst_8 : SMul ℕ β] →
                      [inst_9 : NatCast β] →
                        [inst_10 : Max β] →
                          [inst_11 : Bot β] →
                            (f : β → α) →
                              Function.Injective f →
                                (∀ {x y : β}, f x ≤ f y ↔ x ≤ y) →
                                  (∀ {x y : β}, f x < f y ↔ x < y) →
                                    f 0 = 0 →
                                      f 1 = 1 →
                                        (∀ (x y : β), f (x + y) = f x + f y) →
                                          (∀ (x y : β), f (x * y) = f x * f y) →
                                            (∀ (n : ℕ) (x : β), f (n • x) = n • f x) →
                                              (∀ (x : β) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                (∀ (n : ℕ), f ↑n = ↑n) →
                                                  (∀ (a b : β), f (a ⊔ b) = f a ⊔ f b) → f ⊥ = ⊥ → IdemCommSemiring β
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.union_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ ∪ m₃).Equiv (m₂ ∪ m₃)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Result.mk.sizeOf_spec : ∀ (allConsts unfoldCandidates eqnCandidates : Lean.Meta.Try.Collector.OrdSet Lean.Name)
  (funIndCandidates : Lean.Meta.FunInd.SeenCalls) (indCandidates : Array Lean.Meta.Try.Collector.InductionCandidate)
  (libSearchResults : Lean.Meta.Try.Collector.OrdSet (Lean.Name × Lean.Meta.Grind.EMatchTheoremKind)),
  sizeOf
      { allConsts := allConsts, unfoldCandidates := unfoldCandidates, eqnCandidates := eqnCandidates,
        funIndCandidates := funIndCandidates, indCandidates := indCandidates, libSearchResults := libSearchResults } =
    1 + sizeOf allConsts + sizeOf unfoldCandidates + sizeOf eqnCandidates + sizeOf funIndCandidates +
        sizeOf indCandidates +
      sizeOf libSearchResults
-- Mathlib.Topology.Order.Monotone
/-- A monotone map has a limit to the left of any point `x`, equal to `sSup (f '' (Iio x))`.  -/
Monotone.tendsto_nhdsLT : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Iio x)))
-- Mathlib.Data.Part
Part.instOne : {α : Type u_1} → [One α] → One (Part α)
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instModuleOfSMulCommClass : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {X : Type u_4} →
        {Y : Type u_5} →
          {σ : M → N} →
            [inst : AddCommMonoid Y] →
              [inst_1 : Semiring R] →
                [inst_2 : SMul M X] →
                  [inst_3 : DistribSMul N Y] → [inst_4 : Module R Y] → [SMulCommClass N R Y] → Module R (X →ₑ[σ] Y)
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.mono_iff_ker_eq_bot : ∀ {A B : GrpCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ (GrpCat.Hom.hom f).ker = ⊥
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.addConj_apply`. -/
AddAut.conj_apply : ∀ {G : Type u_3} [inst : AddGroup G] (g h : G), (AddAut.addConj g) h = g + h + -g
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.mk.inj : ∀ {𝕜 : 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} {toPartialEquiv : PartialEquiv H E}
  {source_eq : toPartialEquiv.source = Set.univ}
  {convex_range' :
    if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv) else Set.range ↑toPartialEquiv = Set.univ}
  {nonempty_interior' : (interior (Set.range ↑toPartialEquiv)).Nonempty}
  {continuous_toFun : autoParam (Continuous ↑toPartialEquiv) ModelWithCorners.continuous_toFun._autoParam}
  {continuous_invFun : autoParam (Continuous toPartialEquiv.invFun) ModelWithCorners.continuous_invFun._autoParam}
  {toPartialEquiv_1 : PartialEquiv H E} {source_eq_1 : toPartialEquiv_1.source = Set.univ}
  {convex_range'_1 :
    if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv_1)
    else Set.range ↑toPartialEquiv_1 = Set.univ}
  {nonempty_interior'_1 : (interior (Set.range ↑toPartialEquiv_1)).Nonempty}
  {continuous_toFun_1 : autoParam (Continuous ↑toPartialEquiv_1) ModelWithCorners.continuous_toFun._autoParam}
  {continuous_invFun_1 : autoParam (Continuous toPartialEquiv_1.invFun) ModelWithCorners.continuous_invFun._autoParam},
  { toPartialEquiv := toPartialEquiv, source_eq := source_eq, convex_range' := convex_range',
        nonempty_interior' := nonempty_interior', continuous_toFun := continuous_toFun,
        continuous_invFun := continuous_invFun } =
      { toPartialEquiv := toPartialEquiv_1, source_eq := source_eq_1, convex_range' := convex_range'_1,
        nonempty_interior' := nonempty_interior'_1, continuous_toFun := continuous_toFun_1,
        continuous_invFun := continuous_invFun_1 } →
    toPartialEquiv = toPartialEquiv_1
-- Mathlib.Algebra.Order.Group.Abs
mabs_mul_three : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a b c : G),
  |a * b * c|ₘ ≤ |a|ₘ * |b|ₘ * |c|ₘ
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.commonRetraction.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f f_1 : A ⟶ B) (e_f : f = f_1) (g g_1 : A ⟶ B)
  (e_g : g = g_1) [inst_1 : CategoryTheory.IsCoreflexivePair f g],
  CategoryTheory.commonRetraction f g = CategoryTheory.commonRetraction f_1 g_1
-- Mathlib.Analysis.Normed.Affine.AsymptoticCone
asymptoticCone_subset_singleton_of_bounded : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : Set P}, Bornology.IsBounded s → asymptoticCone ℝ s ⊆ {0}
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
MvPolynomial.sumSMulXSMulY.eq_1 : ∀ {n : Type u_1} {R : Type u_2} [inst : CommRing R],
  MvPolynomial.sumSMulXSMulY =
    Finsupp.linearCombination R fun i => MvPolynomial.X (Sum.inl i) * MvPolynomial.X (Sum.inr i)
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.nontrivial : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀)
  [hv : v.RankOne], ∃ r, v r ≠ 0 ∧ v r ≠ 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcReleaseParams : Lean.FromJson Lean.Lsp.RpcReleaseParams
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.AnchorRef.mk.injEq : ∀ (numDigits : ℕ) (anchorPrefix : UInt64) (numDigits_1 : ℕ) (anchorPrefix_1 : UInt64),
  ({ numDigits := numDigits, anchorPrefix := anchorPrefix } =
      { numDigits := numDigits_1, anchorPrefix := anchorPrefix_1 }) =
    (numDigits = numDigits_1 ∧ anchorPrefix = anchorPrefix_1)
-- Mathlib.Logic.Basic
/-- An identity function with its main argument implicit. This will be printed as `hidden` even
if it is applied to a large term, so it can be used for elision,
as done in the `elide` and `unelide` tactics.  -/
hidden : {α : Sort u_1} → {a : α} → α
-- Mathlib.AlgebraicGeometry.AffineScheme
/-- The prime ideal of `𝒪ₓ(U)` corresponding to a point `x : U`.  -/
AlgebraicGeometry.IsAffineOpen.primeIdealOf : {X : AlgebraicGeometry.Scheme} →
  {U : X.Opens} → AlgebraicGeometry.IsAffineOpen U → ↥U → PrimeSpectrum ↑(X.presheaf.obj (Opposite.op U))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote.match_1.congr_eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (x : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (p : Lean.Grind.CommRing.Power) → (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m))
  (p : Lean.Grind.CommRing.Power) (m : Lean.Grind.CommRing.Mon),
  x = Lean.Grind.CommRing.Mon.mult p m →
    (match x with
      | Lean.Grind.CommRing.Mon.unit => h_1 ()
      | Lean.Grind.CommRing.Mon.mult p m => h_2 p m) ≍
      h_2 p m
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] [Inhabited α] {k : α} {f : Option β → Option β},
  m.WF → ∀ {hc : k ∈ m.alter k f}, (m.alter k f).getKey k hc = k
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.name : {α σ : Type} → Lean.SimplePersistentEnvExtensionDescr α σ → Lean.Name
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.XOpIso_hom_d_op : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) (i j : Option ι),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.XOpIso K i).hom (HomologicalComplex.extend.d K j i).op =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.extend.d K.op i j) (HomologicalComplex.extend.XOpIso K j).hom
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_prod : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] (f₁ : M₁ →L[R] M₂) (f₂ : M₁ →L[R] M₃), ↑(f₁.prod f₂) = (↑f₁).prod ↑f₂
-- Mathlib.CategoryTheory.Localization.Predicate
/-- If `L₁ : C ⥤ D₁` and `L₂ : C ⥤ D₂` are two localization functors for the
same `MorphismProperty C`, this is an equivalence of categories `D₁ ≌ D₂`.  -/
CategoryTheory.Localization.uniq : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D₁ : Type u_4} →
      {D₂ : Type u_5} →
        [inst_1 : CategoryTheory.Category.{v_4, u_4} D₁] →
          [inst_2 : CategoryTheory.Category.{v_5, u_5} D₂] →
            (L₁ : CategoryTheory.Functor C D₁) →
              (L₂ : CategoryTheory.Functor C D₂) →
                (W' : CategoryTheory.MorphismProperty C) → [L₁.IsLocalization W'] → [L₂.IsLocalization W'] → D₁ ≌ D₂
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- If a simple graph `G` has a bipartition, then it is bipartite.  -/
SimpleGraph.IsBipartiteWith.isBipartite : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → G.IsBipartite
-- Mathlib.Data.Seq.Defs
/-- Embed a list as a sequence  -/
Stream'.Seq.ofList : {α : Type u} → List α → Stream'.Seq α
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- Given a nonzero `x : L`, and assuming that `(spectralAlgNorm h_alg hna) 1 ≤ 1`, this is
the real-valued function sending `y ∈ L` to the limit of  `(f (y * x^n))/((f x)^n)`,
regarded as an algebra norm.  -/
algNormFromConst : {K : Type u} →
  [inst : NontriviallyNormedField K] →
    {L : Type v} →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [inst_3 : Algebra.IsAlgebraic K L] →
            [hu : IsUltrametricDist K] → (spectralAlgNorm K L).toRingSeminorm 1 ≤ 1 → {x : L} → x ≠ 0 → AlgebraNorm K L
-- Mathlib.Analysis.Analytic.CPolynomialDef
/-- If `f` has a formal power series on a ball bounded by `0`, then `f` is equal to `0` on
the ball.  -/
HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {pf : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFiniteFPowerSeriesOnBall f pf x 0 r → ∀ y ∈ Metric.eball x r, f y = 0
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.top_toNonUnitalSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ⊤.toNonUnitalSubsemiring = ⊤
-- Mathlib.Data.List.Chain
List.IsChain.take : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α}, List.IsChain R l → ∀ (n : ℕ), List.IsChain R (List.take n l)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.instInhabited : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → Inhabited (MultilinearMap R M₁ M₂)
-- Mathlib.Algebra.Quaternion
Quaternion.coe_add : ∀ {R : Type u_3} [inst : CommRing R] (x y : R), ↑(x + y) = ↑x + ↑y
-- Mathlib.Algebra.Order.Module.Defs
/-- Scalar multiplication on the left by a positive element preserves strict monotonicity.  -/
StrictMono.const_smul : ∀ {α : Type u_1} {β : Type u_2} {a : α} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulStrictMono α β] {γ : Type u_3} [inst_5 : Preorder γ] {f : γ → β},
  StrictMono f → 0 < a → StrictMono fun x => a • f x
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Alt.mk.injEq : ∀ (ref : Lean.Syntax) (idx : ℕ) (rhs : Lean.Expr) (fvarDecls : List Lean.LocalDecl)
  (patterns : List Lean.Meta.Match.Pattern) (cnstrs : List (Lean.Expr × Lean.Expr)) (notAltIdxs : Array ℕ)
  (ref_1 : Lean.Syntax) (idx_1 : ℕ) (rhs_1 : Lean.Expr) (fvarDecls_1 : List Lean.LocalDecl)
  (patterns_1 : List Lean.Meta.Match.Pattern) (cnstrs_1 : List (Lean.Expr × Lean.Expr)) (notAltIdxs_1 : Array ℕ),
  ({ ref := ref, idx := idx, rhs := rhs, fvarDecls := fvarDecls, patterns := patterns, cnstrs := cnstrs,
        notAltIdxs := notAltIdxs } =
      { ref := ref_1, idx := idx_1, rhs := rhs_1, fvarDecls := fvarDecls_1, patterns := patterns_1, cnstrs := cnstrs_1,
        notAltIdxs := notAltIdxs_1 }) =
    (ref = ref_1 ∧
      idx = idx_1 ∧
        rhs = rhs_1 ∧ fvarDecls = fvarDecls_1 ∧ patterns = patterns_1 ∧ cnstrs = cnstrs_1 ∧ notAltIdxs = notAltIdxs_1)
-- Mathlib.NumberTheory.Rayleigh
/-- **Rayleigh's theorem** on Beatty sequences. Let `r` be an irrational number greater than 1, and
`1/r + 1/s = 1`. Then `B⁺_r` and `B⁺_s` partition the positive integers.  -/
Irrational.beattySeq_symmDiff_beattySeq_pos : ∀ {r s : ℝ},
  r.HolderConjugate s →
    Irrational r → symmDiff {x | ∃ k > 0, beattySeq r k = x} {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}
-- Lean.Server.Rpc.RequestHandling
_private.Lean.Server.Rpc.RequestHandling.0.Lean.Server.builtinRpcProcedures : IO.Ref (Lean.PHashMap Lean.Name Lean.Server.RpcProcedure)
-- Mathlib.Topology.Metrizable.Basic
/-- Every pseudo-metrizable space is first countable.  -/
TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology : ∀ {X : Type u_2} [inst : TopologicalSpace X] [h : TopologicalSpace.PseudoMetrizableSpace X], FirstCountableTopology X
-- Mathlib.CategoryTheory.Shift.Pullback
/-- If `F : C ⥤ D` commutes with the shifts on `C` and `D`, then `PullbackShift.functor F φ`
commutes with their pullbacks by an additive map `φ`.
 -/
CategoryTheory.Functor.commShiftPullback : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {A : Type u_2} →
      {B : Type u_3} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (φ : A →+ B) →
                {D : Type u_4} →
                  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] →
                    [inst_5 : CategoryTheory.HasShift D B] →
                      (F : CategoryTheory.Functor C D) →
                        [F.CommShift B] → (CategoryTheory.PullbackShift.functor φ F).CommShift A
-- Std.Http.Internal.Char
/-- obs-text = %x80-FF (and higher Unicode scalar values in this library's `Char` model).
 -/
Std.Http.Internal.Char.obsText : Char → Bool
-- Mathlib.NumberTheory.FLT.Four
/-- We say a solution to `a ^ 4 + b ^ 4 = c ^ 2` is minimal if there is no other solution with
a smaller `c` (in absolute value).  -/
Fermat42.Minimal : ℤ → ℤ → ℤ → Prop
-- Mathlib.RingTheory.Smooth.StandardSmoothOfFree
/-- If `H¹(S/R) = 0` and `Ω[S⁄R]` is free on `{d sᵢ}ᵢ` for some `sᵢ : S`, then `S`
is `R`-standard smooth.  -/
Algebra.IsStandardSmooth.of_basis_kaehlerDifferential : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] [Subsingleton (Algebra.H1Cotangent R S)] {I : Type u_3}
  (b : Module.Basis I S Ω[S⁄R]), Set.range ⇑b ⊆ Set.range ⇑(KaehlerDifferential.D R S) → Algebra.IsStandardSmooth R S
-- Mathlib.Data.Sigma.Basic
/-- Nondependent eliminator for `PSigma`.  -/
PSigma.elim : {α : Sort u_1} → {β : α → Sort u_2} → {γ : Sort u_3} → ((a : α) → β a → γ) → PSigma β → γ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldl_eq_foldl_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w}
  {f : δ → (a : α) → β a → δ} {init : δ},
  Std.DTreeMap.foldl f init t = Array.foldl (fun a b => f a b.fst b.snd) init t.toArray
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.measurable_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → ∀ (a : α) (q : ℚ), Measurable fun t => f (a, t) q
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.HasSheafify.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] (isRightAdjoint : CategoryTheory.HasWeakSheafify J A),
  CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.sheafToPresheaf J A).leftAdjoint →
    CategoryTheory.HasSheafify J A
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_eq_self_sub_mul_bdiv : ∀ (x : ℤ) (m : ℕ), x.bmod m = x - ↑m * x.bdiv m
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- The left unitor as a term of `normalExpr`.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.leftUnitorM : {m : Type → Type} →
  [Monad m] →
    [Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
      [Mathlib.Tactic.BicategoryLike.MonadNormalExpr m] →
        Mathlib.Tactic.BicategoryLike.Mor₁ → m Mathlib.Tactic.BicategoryLike.NormalExpr
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
mul_mem_lowerBounds_mul : ∀ {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M} {a b : M},
  a ∈ lowerBounds s → b ∈ lowerBounds t → a * b ∈ lowerBounds (s * t)
-- Mathlib.Algebra.RingQuot
RingQuot.instNatCast.eq_1 : ∀ {R : Type uR} [inst : Semiring R] (r : R → R → Prop), RingQuot.instNatCast r = { natCast := RingQuot.natCast r }
-- Mathlib.Algebra.Category.Semigrp.Basic
CategoryTheory.Iso.addMagmaCatIsoToAddEquiv.eq_1 : ∀ {X Y : AddMagmaCat} (i : X ≅ Y),
  i.addMagmaCatIsoToAddEquiv = (AddMagmaCat.Hom.hom i.hom).toAddEquiv (AddMagmaCat.Hom.hom i.inv) ⋯ ⋯