mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Basic
VectorPrebundle.pretrivializationAtlas : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      {E : B → Type u_4} →
        [inst : NontriviallyNormedField R] →
          [inst_1 : (x : B) → AddCommMonoid (E x)] →
            [inst_2 : (x : B) → Module R (E x)] →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace R F] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : (x : B) → TopologicalSpace (E x)] →
                      VectorPrebundle R F E → Set (Bundle.Pretrivialization F Bundle.TotalSpace.proj)
-- Mathlib.Topology.Order.Hom.Basic
ContinuousOrderHomClass.instCoeTCContinuousOrderHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : TopologicalSpace α] →
            [inst_3 : TopologicalSpace β] →
              [inst_4 : FunLike F α β] → [ContinuousOrderHomClass F α β] → CoeTC F (α →Co β)
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F : C ⥤ D` is initial, we denote by `homToLift` an arbitrary choice of morphism
`F.obj (lift F d) ⟶ d`.
 -/
CategoryTheory.Functor.Initial.homToLift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Initial] → (d : D) → F.obj (CategoryTheory.Functor.Initial.lift F d) ⟶ d
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryGE_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h' : ∃ a ∈ t₁, (cmp a k).isGE = true} (h : t₁.Equiv t₂), t₁.getEntryGE k h' = t₂.getEntryGE k ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHom_isClosedEmbedding : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFC : NonUnitalClosedEmbeddingContinuousFunctionalCalculus R A p] {a : A}
  (ha : p a), Topology.IsClosedEmbedding ⇑(cfcₙHom ha)
-- Mathlib.Order.Hom.Basic
OrderHom.dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (g : β →o γ) (f : α →o β), OrderHom.dual (g.comp f) = (OrderHom.dual g).comp (OrderHom.dual f)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_le_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k km : α} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ (hc : Std.Internal.List.containsKey k l = true),
      (Std.Internal.List.minKey? l).get ⋯ = km → (compare km k).isLE = true
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprExpr_mathlib : Lean.ToExpr Lean.Expr
-- Lean.Server.CodeActions.Basic
Lean.Server.CodeActionResolveData.mk.injEq : ∀ (params : Lean.Lsp.CodeActionParams) (providerName : Lean.Name) (providerResultIndex : ℕ)
  (params_1 : Lean.Lsp.CodeActionParams) (providerName_1 : Lean.Name) (providerResultIndex_1 : ℕ),
  ({ params := params, providerName := providerName, providerResultIndex := providerResultIndex } =
      { params := params_1, providerName := providerName_1, providerResultIndex := providerResultIndex_1 }) =
    (params = params_1 ∧ providerName = providerName_1 ∧ providerResultIndex = providerResultIndex_1)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.homMk_surjective : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {S : T} {X Y : CategoryTheory.Under S} (f : X ⟶ Y),
  ∃ g, ∃ (hg : CategoryTheory.CategoryStruct.comp X.hom g = Y.hom), CategoryTheory.Under.homMk g ⋯ = f
-- Mathlib.Order.SymmDiff
symmDiff_right_inj : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] {a b c : α}, symmDiff a b = symmDiff a c ↔ b = c
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- This data is a recipe in order to produce a spectral sequence starting on
page `r₀` (where the `r`th page is of shape `c r`) from a spectral object
indexed by `ι`. The object on page `r` at the position `pq : κ` shall be
`E^(deg pq)(i₀ ≤ i₁ ≤ i₂ ≤ i₃)`, where `i₀ ≤ i₁ ≤ i₂ ≤ i₃` are elements in the
index type `ι` of the spectral object and `deg pq : ℤ` is a cohomological degree.
The indices `i₀` and `i₃` depend on `r` and `pq`, but `i₁`, `i₂` only depend on `pq`.
Various conditions are added in order to construct the differentials on the pages
and show that the homology of a page identifies to the next page; in certain
cases, additional conditions may be required on the spectral object.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore : (ι : Type u_2) → {κ : Type u_3} → [Preorder ι] → (ℤ → ComplexShape κ) → ℤ → Type (max u_2 u_3)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.forgetReflectIsos : (CategoryTheory.forget RingCat).ReflectsIsomorphisms
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- If `F : J₁ ⥤ J₂` is final and `J₁` is `κ`-filtered, then
`J₂` is also `κ`-filtered. See also `IsFiltered.of_final`
(in `CategoryTheory.Limits.Final`) for the particular case of
filtered categories (`κ = ℵ₀`).  -/
CategoryTheory.IsCardinalFiltered.of_final : ∀ {J₁ : Type u} [inst : CategoryTheory.Category.{v, u} J₁] {J₂ : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J₂]
  (F : CategoryTheory.Functor J₁ J₂) [F.Final] (κ : Cardinal.{w}) [inst_3 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalFiltered J₁ κ], CategoryTheory.IsCardinalFiltered J₂ κ
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.rightKanExtensionCompIsoOfPreserves_hom_fac : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesRightKanExtension F L] [inst_5 : L.HasRightKanExtension F],
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (G.rightKanExtensionCompIsoOfPreserves F L).hom)
      (L.rightKanExtensionCounit (F.comp G)) =
    CategoryTheory.CategoryStruct.comp (L.associator (L.rightKanExtension F) G).inv
      (CategoryTheory.Functor.whiskerRight (L.rightKanExtensionCounit F) G)
-- Qq.Match
Qq.Impl.hasQMatch : Lean.Syntax → Bool
-- Mathlib.MeasureTheory.Integral.CircleTransform
Complex.circleTransformDeriv.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (R : ℝ) (z w : ℂ) (f : ℂ → E) (θ : ℝ),
  Complex.circleTransformDeriv R z w f θ =
    (2 * ↑Real.pi * Complex.I)⁻¹ • deriv (circleMap z R) θ • ((circleMap z R θ - w) ^ 2)⁻¹ • f (circleMap z R θ)
-- Mathlib.Order.Interval.Finset.Fin
Fin.Ioo_sub_one_eq_Ico : ∀ {n : ℕ} {a b : Fin n}, 0 < a → Finset.Ioo (a - 1) b = Finset.Ico a b
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion at `x`, then it is the uniform limit of the
partial sums of this power series on strict subdisks of the disk of convergence, i.e., `f (x + y)`
is the uniform limit of `p.partialSum n y` there.  -/
HasFPowerSeriesOnBall.tendstoUniformlyOn : ∀ {𝕜 : 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}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {r' : NNReal},
  HasFPowerSeriesOnBall f p x r →
    ↑r' < r → TendstoUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop (Metric.ball 0 ↑r')
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.functorExtension₂_obj_obj_p : ∀ (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] (X : CategoryTheory.Functor C D)
  (P : CategoryTheory.Idempotents.Karoubi C),
  (((CategoryTheory.Idempotents.functorExtension₂ C D).obj X).obj P).p = X.map P.p
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The integral closure of `ℤ` inside `CyclotomicField n ℚ` is `CyclotomicRing n ℤ ℚ`.  -/
IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure : ∀ (n : ℕ) [hn : NeZero n], IsIntegralClosure (CyclotomicRing n ℤ ℚ) ℤ (CyclotomicField n ℚ)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The action by a subfield is the action by the underlying field.  -/
Subfield.instMulActionSubtypeMem : {K : Type u} → [inst : DivisionRing K] → {X : Type u_1} → [MulAction K X] → (F : Subfield K) → MulAction (↥F) X
-- Mathlib.RingTheory.LaurentSeries
/-- The `X`-adic completion as an abstract completion of `K⟮X⟯`  -/
LaurentSeries.ratfuncAdicComplPkg : {K : Type u_2} → [inst : Field K] → AbstractCompletion.{u_2, u_2} (WithVal (RatFunc.polynomialValuationX K))
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wfImp_insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} [inst_4 : ForIn Id ρ α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {l : ρ},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    Std.DHashMap.Internal.Raw.WFImp ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_diff_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → m₁.isEmpty = true → (m₁.diff m₂ ⋯).isEmpty = true
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.modify_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k : α} {f : β → β}, Std.ExtDTreeMap.Const.modify t k f = ∅ ↔ t = ∅
-- Mathlib.Data.Analysis.Filter
CFilter.mem_toFilter_sets : ∀ {α : Type u_1} {σ : Type u_3} (F : CFilter (Set α) σ) {a : Set α}, a ∈ F.toFilter ↔ ∃ b, F.f b ⊆ a
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelComparison_map_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)] {Z : C} {h : Y ⟶ Z}
  (w : CategoryTheory.CategoryStruct.comp f h = 0) {Z_1 : D} (h_1 : G.obj Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G)
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.cokernel.desc f h w)) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.desc (G.map f) (G.map h) ⋯) h_1
-- Mathlib.Logic.Equiv.Option
/-- **Alias** of `Equiv.removeNoneAux_some`. -/
Equiv.removeNone_aux_some : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α},
  (∃ x', e (some x) = some x') → some (e.removeNoneAux x) = e (some x)
-- Init.Data.Slice.List.Lemmas
List.size_mkSlice_roc : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.size (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = min (hi + 1) xs.length - (lo + 1)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- Given a functor `F : C ⥤ D`, if `F.map p₁` and `F.map p₂` form a jointly monic pair of
morphisms, then `F` preserves symmetric relations.  -/
CategoryTheory.SymmetricRelation.map : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {R X : C} →
          {p₁ p₂ : R ⟶ X} →
            CategoryTheory.SymmetricRelation p₁ p₂ →
              (F : CategoryTheory.Functor C D) →
                [CategoryTheory.JointlyMono₂ (F.map p₁) (F.map p₂)] →
                  CategoryTheory.SymmetricRelation (F.map p₁) (F.map p₂)
-- Mathlib.Data.List.AList
AList.insert_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b b' : β a} (s : AList β),
  AList.insert a b' (AList.insert a b s) = AList.insert a b' s
-- Mathlib.CategoryTheory.FiberedCategory.HasFibers
/-- HasFibers is an extrinsic notion of fibers on a functor `p : 𝒳 ⥤ 𝒮`. It is given by a
collection of categories `Fib S` for every `S : 𝒮` (the fiber categories), each equipped with a
functors `ι : Fib S ⥤ 𝒳` which map constantly to `S` on the base such that the induced functor
`Fib S ⥤ Fiber p S` is an equivalence.  -/
HasFibers : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        CategoryTheory.Functor 𝒳 𝒮 → Type (max (max (max (max u₁ u₂) (u₃ + 1)) v₂) (v₃ + 1))
-- Lean.Elab.Task
/-- Given a monadic value in `TermElabM`, creates a task that runs it in the current state,
returning
* a cancellation hook and
* a monadic value with the cached result (and subsequent state as it was after running).
 -/
Lean.Elab.Term.TermElabM.asTask : {α : Type} → Lean.Elab.TermElabM α → Lean.Elab.TermElabM (BaseIO Unit × Task (Lean.Elab.TermElabM α))
-- Mathlib.Algebra.Homology.Augment
CochainComplex.truncateAugment_hom_f : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) {X : V} (f : X ⟶ C.X 0) (w : CategoryTheory.CategoryStruct.comp f (C.d 0 1) = 0) (i : ℕ),
  (C.truncateAugment f w).hom.f i = CategoryTheory.CategoryStruct.id (C.X i)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract_zSpan_add : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E) {v : E},
  v ∈ Submodule.span ℤ (Set.range ⇑b) → ZSpan.fract b (v + m) = ZSpan.fract b m
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y_support : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] {D : ℝ},
  0 < D → D < 1 → Function.support (ExistsContDiffBumpBase.y D) = Metric.ball 0 (1 + D)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.whisker_left_id : ∀ {B : Type u} [inst : Quiver B] {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c),
  CategoryTheory.FreeBicategory.Rel
    (CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.id g))
    (CategoryTheory.FreeBicategory.Hom₂.id (f.comp g))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toArray_rco_eq_add : ∀ {m n fallback : ℤ} {i : ℕ}, i < (n - m).toNat → (m...n).toArray.getD i fallback = m + ↑i
-- Lean.Widget.InteractiveCode
/-- The `Elab.Info` node with the semantics of this part of the output.  -/
Lean.Widget.SubexprInfo.info : Lean.Widget.SubexprInfo → Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.dite_tensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {P : Prop}
  [inst_2 : Decidable P] {W X Y Z : C} (f : W ⟶ X) (g : P → (Y ⟶ Z)) (g' : ¬P → (Y ⟶ Z)),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (if h : P then g h else g' h) f =
    if h : P then CategoryTheory.MonoidalCategoryStruct.tensorHom (g h) f
    else CategoryTheory.MonoidalCategoryStruct.tensorHom (g' h) f
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_Iic : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a : α}, IsPreconnected (Set.Iic a)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableOn.smul_const_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {a : 𝕜}
  {s : (x : B) → E x} {u : Set B}, MDiff[u] (T% s) → MDiff[u] fun x => ⟨x, (a • s) x⟩
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- `Unitization 𝕜 A` is complete whenever `𝕜` and `A` are also.  -/
Unitization.instCompleteSpace : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [CompleteSpace 𝕜]
  [CompleteSpace A], CompleteSpace (Unitization 𝕜 A)
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.Context.funId : Lean.Elab.Term.CollectPatternVars.Context → Lean.Ident
-- Mathlib.LinearAlgebra.FreeModule.Basic
Module.Free.mk : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Nonempty ((I : Type v) × Module.Basis I R M) → Module.Free R M
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.le_of_opENorm_le_of_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) {x : E} {a b : ENNReal}, ‖f‖ₑ ≤ a → ‖x‖ₑ ≤ b → ‖f x‖ₑ ≤ a * b
-- Mathlib.RingTheory.Teichmuller
MonoidHom.toMulEquiv.congr_simp : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f f_1 : M →* N) (e_f : f = f_1)
  (g g_1 : N →* M) (e_g : g = g_1) (h₁ : g.comp f = MonoidHom.id M) (h₂ : f.comp g = MonoidHom.id N),
  f.toMulEquiv g h₁ h₂ = f_1.toMulEquiv g_1 ⋯ ⋯
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.instIsIsoModuleCatLocalizationtoStalkₗ : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x : PrimeSpectrum R),
  CategoryTheory.IsIso (AlgebraicGeometry.StructureSheaf.localizationtoStalkₗ✝ R M x)
-- Mathlib.Order.Filter.Pointwise
Filter.pure_sub_pure : ∀ {α : Type u_2} [inst : Sub α] {a b : α}, pure a - pure b = pure (a - b)
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.symm_eq_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {α β : X ≅ Y}, α.symm = β.symm ↔ α = β
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.reflectsFiniteColimitsOfReflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.HasFiniteColimits C]
  [CategoryTheory.Limits.PreservesFiniteColimits F], CategoryTheory.Limits.ReflectsFiniteColimits F
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.unbounded.inj : ∀ {α : Type} {ch ch_1 : Std.CloseableChannel.Unbounded✝ α},
  Std.CloseableChannel.Flavors.unbounded✝ ch = Std.CloseableChannel.Flavors.unbounded✝ ch_1 → ch = ch_1
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_one : ∀ {l : Type u_1} {m : Type u_2} {α : Type u_12} [inst : DecidableEq l] [inst_1 : DecidableEq m] [inst_2 : Zero α]
  [inst_3 : One α], Matrix.fromBlocks 1 0 0 1 = 1
-- Lean.Environment
Lean.Kernel.isDiagnosticsEnabled : Lean.Environment → Bool
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.counitForward_naturality₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)}
  (s t : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ) (f : t ⟶ s) (x : F.obj t),
  CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop s) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.OverPresheafAux.counitForward F (Opposite.unop t) x).map₂ f.unop.left ⋯
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoidClass.coe_nsmul : ∀ {M : Type u_5} [inst : AddMonoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : AddSubmonoidClass A M] {S : A}
  (x : ↥S) (n : ℕ), ↑(n • x) = n • ↑x
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equivFun.congr_simp : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (b b_1 : Module.Basis ι R M), b = b_1 → b.equivFun = b_1.equivFun
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.mapsTo_smul_closure : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [ContinuousConstSMul R M] (s : Submodule R M) (c : R),
  Set.MapsTo (fun x => c • x) (closure ↑s) (closure ↑s)
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- The associator for tensor product of R-modules, as a linear equivalence.  -/
TensorProduct.assoc : (R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_5) →
      (N : Type u_6) →
        (P : Type u_7) →
          [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] →
                      TensorProduct R (TensorProduct R M N) P ≃ₗ[R] TensorProduct R M (TensorProduct R N P)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- If the measure of the symmetric difference of two sets is finite,
then one has finite measure if and only if the other one does.  -/
MeasureTheory.measure_ne_top_iff_of_symmDiff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  μ (symmDiff s t) ≠ ⊤ → (μ s ≠ ⊤ ↔ μ t ≠ ⊤)
-- Mathlib.Combinatorics.SimpleGraph.Basic
instDecidableRelAdjFromRelOfDecidableEq : {V : Type u} → [DecidableEq V] → (r : V → V → Prop) → [DecidableRel r] → DecidableRel (SimpleGraph.fromRel r).Adj
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.mapPower_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Limits.FormalCoproduct C) {α β γ : Type t}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] [inst_2 : CategoryTheory.Limits.HasProductsOfShape β C]
  [inst_3 : CategoryTheory.Limits.HasProductsOfShape γ C] (f : α → β) (g : β → γ)
  {Z : CategoryTheory.Limits.FormalCoproduct C} (h : U.power α ⟶ Z),
  CategoryTheory.CategoryStruct.comp (U.mapPower (g ∘ f)) h =
    CategoryTheory.CategoryStruct.comp (U.mapPower g) (CategoryTheory.CategoryStruct.comp (U.mapPower f) h)
-- Init.Data.Repr
instReprUInt8 : Repr UInt8
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.coe_pullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C} {Z : C}
  (f : Y ⟶ X) (g : Z ⟶ Y) (S : J.Cover X),
  (↑(S.pullback f)).arrows g ↔ (↑S).arrows (CategoryTheory.CategoryStruct.comp g f)
-- Batteries.Data.String.Lemmas
String.toList_drop : ∀ (s : String) (n : ℕ), (String.Legacy.drop s n).toList = List.drop n s.toList
-- Mathlib.Control.Monad.Writer
MonadWriter : outParam (Type u) → (Type u → Type v) → Type (max (u + 1) v)
-- Init.Data.Array.Lemmas
Array.uset_eq_set : ∀ {α : Type u_1} {xs : Array α} {v : α} {i : USize} (h : i.toNat < xs.size), xs.uset i v h = xs.set i.toNat v h
-- Mathlib.Data.Finsupp.Basic
Finsupp.curryAddEquiv_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddZeroClass M] (f : α →₀ β →₀ M),
  Finsupp.curryAddEquiv.symm f = f.uncurry