mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.associator.congr_simp : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₁.HasTensor X₂]
  [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] [inst_5 : X₂.HasTensor X₃]
  [inst_6 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)]
  [inst_7 : X₁.HasGoodTensor₁₂Tensor X₂ X₃] [inst_8 : X₁.HasGoodTensorTensor₂₃ X₂ X₃],
  CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃ = CategoryTheory.GradedObject.Monoidal.associator X₁ X₂ X₃
-- Mathlib.Order.Filter.Pointwise
Filter.mem_inv : ∀ {α : Type u_2} [inst : Inv α] {f : Filter α} {s : Set α}, s ∈ f⁻¹ ↔ Inv.inv ⁻¹' s ∈ f
-- Mathlib.Topology.Order.IntermediateValue
/-- A preconnected set is either one of the intervals `Icc`, `Ico`, `Ioc`, `Ioo`, `Ici`, `Ioi`,
`Iic`, `Iio`, or `univ`, or `∅`. The converse statement requires `α` to be densely ordered. Though
one can represent `∅` as `(Inf ∅, Inf ∅)`, we include it into the list of possible cases to improve
readability.  -/
setOfPred_isPreconnected_subset_of_ordered : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α],
  {s | IsPreconnected s} ⊆
    Set.range (Function.uncurry Set.Icc) ∪ Set.range (Function.uncurry Set.Ico) ∪ Set.range (Function.uncurry Set.Ioc) ∪
        Set.range (Function.uncurry Set.Ioo) ∪
      (Set.range Set.Ici ∪ Set.range Set.Ioi ∪ Set.range Set.Iic ∪ Set.range Set.Iio ∪ {Set.univ, ∅})
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.coe_mapCocycles₁ : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B)
  (x : ↑(ModuleCat.of k ↥(groupCohomology.cocycles₁ A))),
  ⇑((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₁ f φ)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsMap₁ f φ)) ⇑x
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.ofSequence_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (a : ℕ),
  (CategoryTheory.Functor.ofSequence f).obj a = X a
-- Mathlib.Algebra.Order.Field.Basic
lt_div_iff_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < 0 → (a < b / c ↔ b < a * c)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] (x size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l r).keyAtIdx! x =
    match compare x l.size with
    | Ordering.lt => l.keyAtIdx! x
    | Ordering.eq => k
    | Ordering.gt => r.keyAtIdx! (x - l.size - 1)
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isTop : ℕ → Mathlib.Tactic.Order.AtomicFact
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.Types.end_.condition : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} {i j : J} (f : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.end_.π F i) ((F.obj (Opposite.op i)).map f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.end_.π F j) ((F.map f.op).app j)
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobeniusPolyAux.eq_def : ∀ (p x : ℕ),
  WittVector.frobeniusPolyAux p x =
    have n := x;
    MvPolynomial.X (n + 1) -
      ∑ i,
        have x := ⋯;
        ∑ j ∈ Finset.range (p ^ (n - ↑i)),
          (MvPolynomial.X ↑i ^ p) ^ (p ^ (n - ↑i) - (j + 1)) * WittVector.frobeniusPolyAux p ↑i ^ (j + 1) *
            MvPolynomial.C
              ↑((p ^ (n - ↑i)).choose (j + 1) / p ^ (n - ↑i - multiplicity p (j + 1)) *
                  p ^ (j - multiplicity p (j + 1)))
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.opEquivalence_functor_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (n : ℕ) (X : (CategoryTheory.Functor (Fin (n + 1)) C)ᵒᵖ)
  (X_1 : Fin (n + 1)),
  ((CategoryTheory.ComposableArrows.opEquivalence C n).functor.obj X).obj X_1 =
    Opposite.op ((Opposite.unop X).obj X_1.rev)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- `ContMDiffWithinAt.comp` for a function of two arguments.  -/
ContMDiffWithinAt.comp₂ : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {s : Set M} {n : WithTop ℕ∞} {h : M' × N' → N} {f : M → M'} {g : M → N'} {x : M}
  {t : Set (M' × N')},
  ContMDiffWithinAt (I'.prod J') J n h t (f x, g x) →
    ContMDiffWithinAt I I' n f s x →
      ContMDiffWithinAt I J' n g s x →
        Set.MapsTo (fun x => (f x, g x)) s t → ContMDiffWithinAt I J n (fun x => h (f x, g x)) s x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_of_neg_of_le : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b c : α},
  a < 0 → b ≤ c → a + b < c
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
/-- Predicate asserting that the word `L` is cyclically reduced, i.e., it is reduced
and furthermore the first and the last letter of the word do not cancel. The empty word is by
convention also cyclically reduced.  -/
FreeAddGroup.IsCyclicallyReduced : {α : Type u} → List (α × Bool) → Prop
-- Init.Meta.Defs
Lean.MonadNameGenerator.mk : {m : Type → Type} → m Lean.NameGenerator → (Lean.NameGenerator → m Unit) → Lean.MonadNameGenerator m
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.sSup_iff : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (S : Set (CategoryTheory.MorphismProperty C)) {X Y : C}
  (f : X ⟶ Y), sSup S f ↔ ∃ W ∈ S, W f
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.preservesMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  L.PreservesMonomorphisms
-- Mathlib.ModelTheory.DirectLimit
/-- Every element of the direct limit corresponds to some element in
some component of the directed system.  -/
FirstOrder.Language.DirectLimit.exists_of : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι] (z : FirstOrder.Language.DirectLimit G f),
  ∃ i x, (FirstOrder.Language.DirectLimit.of L ι G f i) x = z
-- Mathlib.Order.Filter.Pointwise
Filter.instDiv.eq_1 : ∀ {α : Type u_2} [inst : Div α],
  Filter.instDiv =
    {
      div := fun f g =>
        let __src := Filter.map₂ (fun x1 x2 => x1 / x2) f g;
        { sets := {s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ / t₂ ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }
-- Init.SizeOf
MProd.mk.sizeOf_spec : ∀ {α β : Type u} [inst : SizeOf α] [inst_1 : SizeOf β] (fst : α) (snd : β),
  sizeOf ⟨fst, snd⟩ = 1 + sizeOf fst + sizeOf snd
-- Mathlib.Analysis.Normed.Lp.lpHolder
Memℓp.holder_top_left_bound : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} {G : ι → Type u_5} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (G i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (G i)] {q : ENNReal}
  {e : (i : ι) → E i} {f : (i : ι) → F i} (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] G i) {K C D : ℝ},
  (∀ (i : ι), ‖B i‖ ≤ K) →
    0 ≤ K →
      0 ≤ C →
        (∀ (i : ι), ‖e i‖ ≤ C) →
          (∀ (s : Finset ι), ∑ i ∈ s, ‖f i‖ ^ q.toReal ≤ D) →
            ∀ (s : Finset ι), ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ q.toReal ≤ (K * C) ^ q.toReal * D
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.instIsDenseSubsiteRegularTopologyInverse : ∀ {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] [inst_2 : CategoryTheory.Preregular C] (e : C ≌ D),
  CategoryTheory.Functor.IsDenseSubsite (CategoryTheory.regularTopology D) (CategoryTheory.regularTopology C) e.inverse
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
Ideal.liesOver_iff_dvd_map : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [IsDedekindDomain A] [inst_3 : Algebra R A]
  {p : Ideal R} {P : Ideal A}, P ≠ ⊤ → ∀ [p.IsMaximal], P.LiesOver p ↔ P ∣ Ideal.map (algebraMap R A) p
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.topEquiv_symm_apply_coe : ∀ {M : Type u_5} [inst : AddZeroClass M] (x : M), ↑(AddSubmonoid.topEquiv.symm x) = x
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.simp : Lean.Expr →
  optParam Lean.Meta.Sym.Simp.Methods { } →
    optParam Lean.Meta.Sym.Simp.Config { } → Lean.Meta.Sym.SymM Lean.Meta.Sym.Simp.Result
-- Mathlib.Order.Types.Defs
/-- **Alias** of `OrderType.type_le_type`. -/
OrderEmbedding.type_le_type : ∀ {α β : Type u} [inst : LinearOrder α] [inst_1 : LinearOrder β] (h : α ↪o β), OrderType.type α ≤ OrderType.type β
-- Mathlib.Tactic.Linter.MinImports
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.instInhabitedImportState : Inhabited Mathlib.Linter.ImportState✝
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.instIsDomainFiniteElement : ∀ (K : Type u_1) [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K],
  IsDomain (ArchimedeanClass.FiniteElement K)
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.pushoutCocone_inl : ∀ (R A B : Type u) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A]
  [inst_4 : Algebra R B],
  (CommRingCat.pushoutCocone R A B).inl = CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.sSup_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M : PresheafOfModules R} (s : Set M.Submodule) (X : Cᵒᵖ), (sSup s).obj X = ⨆ N ∈ s, N.obj X
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.zeroLocus_anti_mono : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] {σ : Type u_3}
  {I J : Ideal (MvPolynomial σ k)}, I ≤ J → MvPolynomial.zeroLocus K J ⊆ MvPolynomial.zeroLocus K I
-- Lean.Meta.DiscrTree.Main
/-- Return true if `e` is one of the following
- A nat literal (numeral)
- `Nat.zero`
- `Nat.succ x` where `isNumeral x`
- `OfNat.ofNat _ x _` where `isNumeral x`  -/
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.isNumeral : Lean.Expr → Bool
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instAddCommMonoid : {𝕜 : Type u_2} → {α : Type u_5} → [inst : AddCommMonoid 𝕜] → [inst_1 : LE α] → AddCommMonoid (IncidenceAlgebra 𝕜 α)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_le_card_mul_left : ∀ {α : Type u_2} [inst : Mul α] [IsLeftCancelMul α] [inst_2 : DecidableEq α] {t s : Finset α},
  s.Nonempty → t.card ≤ (s * t).card
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.any_eq_true_iff_exists_contains_getKey_get : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → β → Bool},
  m.WF → (m.any p = true ↔ ∃ a, ∃ (h : m.contains a = true), p (m.getKey a h) (Std.DHashMap.Raw.Const.get m a h) = true)
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.isLocallyConstant_rankAtStalk_freeLocus : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M], IsLocallyConstant fun x => Module.rankAtStalk M ↑x
-- Mathlib.CategoryTheory.Limits.Sifted
/-- In particular a category is sifted iff and only if it is so when viewed as a small category  -/
CategoryTheory.IsSifted.isSifted_iff_asSmallIsSifted : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.IsSifted C ↔ CategoryTheory.IsSifted (CategoryTheory.AsSmall C)
-- Lean.LocalContext
Lean.LocalDecl.ldecl.inj : ∀ {index : ℕ} {fvarId : Lean.FVarId} {userName : Lean.Name} {type value : Lean.Expr} {nondep : Bool}
  {kind : Lean.LocalDeclKind} {index_1 : ℕ} {fvarId_1 : Lean.FVarId} {userName_1 : Lean.Name}
  {type_1 value_1 : Lean.Expr} {nondep_1 : Bool} {kind_1 : Lean.LocalDeclKind},
  Lean.LocalDecl.ldecl index fvarId userName type value nondep kind =
      Lean.LocalDecl.ldecl index_1 fvarId_1 userName_1 type_1 value_1 nondep_1 kind_1 →
    index = index_1 ∧
      fvarId = fvarId_1 ∧ userName = userName_1 ∧ type = type_1 ∧ value = value_1 ∧ nondep = nondep_1 ∧ kind = kind_1
-- Init.System.IO
/-- Reads bytes from a system entropy source. It is not guaranteed to be cryptographically secure.

If `nBytes` is `0`, returns immediately with an empty buffer.
 -/
IO.getRandomBytes : USize → IO ByteArray
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T S : E →L[𝕜] E}, T.IsPositive → S.IsPositive → (T + S).IsPositive
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- Version of `completedRiemannZeta₀` that avoids `s ≠ 0`  -/
riemannZeta_eq_mul_completedRiemannZeta₀ : ∀ (s : ℂ),
  riemannZeta s =
    (s * completedRiemannZeta₀ s - 1 - s / (1 - s)) / (2 * ↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2 + 1))
-- Lean.Meta.InferType
/-- Returns `u` iff `type` is `Sort u` or `As → Sort u`.
 -/
Lean.Meta.typeFormerTypeLevel : Lean.Expr → Lean.MetaM (Option Lean.Level)
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.add_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {E'' : Type u_7} [inst_9 : NormedAddCommGroup E''] [inst_10 : NormedSpace 𝕜 E''] {H'' : Type u_8}
  [inst_11 : TopologicalSpace H''] {I'' : ModelWithCorners 𝕜 E'' H''} {N' : Type u_9} [inst_12 : TopologicalSpace N']
  [inst_13 : ChartedSpace H'' N'] {n : WithTop ℕ∞} {G : Type u_10} [inst_14 : Add G] [inst_15 : TopologicalSpace G]
  [inst_16 : ChartedSpace H' G] [inst_17 : ContMDiffAdd I' n G] (f g : ContMDiffMap I'' I' N' G n)
  (h : ContMDiffMap I I'' N N' n), (f + g).comp h = f.comp h + g.comp h
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_of_mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, l.contains k = false → k ∈ t.insertMany l → k ∈ t
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_succ_right_eq_cons_map : ∀ {m n : ℤ}, m ≤ n → (m...n + 1).toList = m :: List.map (fun x => x + 1) (m...n).toList
-- Mathlib.RingTheory.Derivation.Basic
Derivation.ext : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  {D1 D2 : Derivation R A M}, (∀ (a : A), D1 a = D2 a) → D1 = D2
-- Mathlib.Topology.Homeomorph.Lemmas
/-- `ULift X` is homeomorphic to `X`.  -/
Homeomorph.ulift : {X : Type v} → [inst : TopologicalSpace X] → ULift.{u, v} X ≃ₜ X
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.mk'.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {x : CommGroup α} {x_1 : Preorder α} {x_2 : CommGroup β} {x_3 : PartialOrder β}
  (f : α → β) (hf : Monotone f) (map_mul : ∀ (a b : α), f (a * b) = f a * f b),
  OrderMonoidHom.mk' f hf map_mul = { toMonoidHom := MonoidHom.mk' f map_mul, monotone' := hf }
-- Init.Core
/-- Split an if-then-else into cases. The `split` tactic is generally easier to use than this theorem.  -/
iteInduction : {α : Sort u_1} →
  {c : Prop} →
    [inst : Decidable c] →
      {motive : α → Sort u_2} → {t e : α} → (c → motive t) → (¬c → motive e) → motive (if c then t else e)
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.accPt_subtype : ∀ {p o : Ordinal.{u_1}} (S : Set Ordinal.{u_1}) (hpo : p < o),
  AccPt p (Filter.principal S) ↔ AccPt ⟨p, hpo⟩ (Filter.principal (Subtype.val ⁻¹' S))
-- Init.Data.OfScientific
/-- Precomputed values of `10 ^ e` for `0 ≤ e ≤ 10 `. In this range, the values can be represented
exactly.
 -/
Float32.exactlyRepresentablePowersOfTen : Array Float32
-- Std.Time.Notation
/-- Defines a syntax for timezone identifiers. The input string should be a valid timezone name or
abbreviation.

Example:
`timezone("America/Sao_Paulo")`
 -/
Std.Time.«termTimezone(_)» : Lean.ParserDescr
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformly.tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι}, TendstoUniformly F f p → TendstoUniformlyOn F f p s
-- Mathlib.Data.Multiset.FinsetOps
Multiset.coe_ndinsert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), Multiset.ndinsert a ↑l = ↑(insert a l)
-- Mathlib.Topology.Instances.ENat
ENat.continuousAt_sub : ∀ {a b : ℕ∞}, a ≠ ⊤ ∨ b ≠ ⊤ → ContinuousAt (Function.uncurry fun x1 x2 => x1 - x2) (a, b)
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- `minTensorProduct` is monotone.  -/
PointedCone.minTensorProduct_mono : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  {C₁ C₁' : PointedCone R G} {C₂ C₂' : PointedCone R H},
  C₁ ≤ C₁' → C₂ ≤ C₂' → C₁.minTensorProduct C₂ ≤ C₁'.minTensorProduct C₂'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.span_map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  (w : CategoryTheory.Limits.WalkingSpan),
  (CategoryTheory.Limits.span f g).map (CategoryTheory.Limits.WalkingSpan.Hom.id w) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Limits.span f g).obj w)
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.mk_dest : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : MvQPF.Cofix F α),
  MvQPF.Cofix.mk x.dest = x
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.Context.mk.sizeOf_spec : ∀ {m : Type → Type} [inst : (a : Type) → SizeOf (m a)] (initialMask : Array Bool) (test : Array Bool → m Bool)
  (maxCalls : ℕ),
  sizeOf { initialMask := initialMask, test := test, maxCalls := maxCalls } = 1 + sizeOf initialMask + sizeOf maxCalls
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
instNonemptyElemWeakDualComplexCharacterSpaceOfNontrivial : ∀ {A : Type u_1} [inst : NormedCommRing A] [inst_1 : NormedAlgebra ℂ A] [CompleteSpace A] [Nontrivial A],
  Nonempty ↑(WeakDual.characterSpace ℂ A)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.enorm_integral_le_lintegral_enorm : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (f : α → G), ‖∫ (a : α), f a ∂μ‖ₑ ≤ ∫⁻ (a : α), ‖f a‖ₑ ∂μ
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_mul_add_lt_opow : ∀ {b u v w x : Ordinal.{u_1}}, v < b → w < b ^ u → u < x → b ^ u * v + w < b ^ x
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.UnusedSimpArgsInfo.mk.sizeOf_spec : ∀ (mask : Array Bool), sizeOf { mask := mask } = 1 + sizeOf mask
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).H = c.pt
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.unitsEquiv_apply : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (f : (M →L[R] M)ˣ) (x : M), ((ContinuousLinearEquiv.unitsEquiv R M) f) x = ↑f x
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.isScalarTower : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : SMul α β] [inst_2 : SMul α γ]
  [inst_3 : SMul β γ] [IsScalarTower α β γ], IsScalarTower α β (Finset γ)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `X` represents a presheaf of monoids `F`, then `Hom(-, X)` is isomorphic to `F` as
a presheaf of monoids.  -/
CategoryTheory.yonedaMonObjIsoOfRepresentableBy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X : C) →
        (F : CategoryTheory.Functor Cᵒᵖ MonCat) →
          (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X) → CategoryTheory.yonedaMonObj X ≅ F
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_eq_right_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α),
  normalize b = b → (lcm a b = b ↔ a ∣ b)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryingFlipEquiv_apply_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (a : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (X : C × D),
  (CategoryTheory.Functor.curryingFlipEquiv a).obj X = (a.obj X.2).obj X.1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Instance implicit arguments are considered support and handled using `isDefEq`.  -/
Lean.Meta.Grind.NormalizePattern.PatternArgKind.instImplicit : Lean.Meta.Grind.NormalizePattern.PatternArgKind
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_neg : ∀ {R : Type u_1} [inst : CommRing R] (p : Polynomial R) (n : ℕ), (-p).homogenize n = -p.homogenize n
-- Mathlib.Algebra.Field.Opposite
AddOpposite.instDivisionSemiring : {α : Type u_1} → [DivisionSemiring α] → DivisionSemiring αᵃᵒᵖ
-- Mathlib.Analysis.Normed.Operator.Banach
/-- A continuous linear endomorphism is a unit iff it's a unit viewed simply as a linear map, provided
the space is complete.
 -/
ContinuousLinearMap.isUnit_iff_isUnit_toLinearMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {f : E →L[𝕜] E}, IsUnit f ↔ IsUnit ↑f