mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
/-- The pullback of a monoid object is a monoid object.  -/
CategoryTheory.Over.monObjMkPullbackSnd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {X R S : C} →
        {f : R ⟶ X} →
          {g : S ⟶ X} →
            [CategoryTheory.MonObj (CategoryTheory.Over.mk f)] →
              CategoryTheory.MonObj (CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd f g))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.instHasCoproductSigmaFstSndOfSigmaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C)
  [inst_1 : ∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun i => ∐ g i],
  CategoryTheory.Limits.HasCoproduct fun p => g p.fst p.snd
-- Mathlib.Algebra.Module.ZLattice.Summable
LinearEquiv.toContinuousLinearEquiv.congr_simp : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F]
  [inst_13 : FiniteDimensional 𝕜 E] (e e_1 : E ≃ₗ[𝕜] F),
  e = e_1 → e.toContinuousLinearEquiv = e_1.toContinuousLinearEquiv
-- Mathlib.Algebra.Group.Action.Defs
/-- Frequently, we find ourselves wanting to express a bilinear map `M →ₗ[R] N →ₗ[R] P` or an
equivalence between maps `(M →ₗ[R] N) ≃ₗ[R] (M' →ₗ[R] N')` where the maps have an associated ring
`R`. Unfortunately, using definitions like these requires that `R` satisfy `CommSemiring R`, and
not just `Semiring R`. Using `M →ₗ[R] N →+ P` and `(M →ₗ[R] N) ≃+ (M' →ₗ[R] N')` avoids this
problem, but throws away structure that is useful for when we _do_ have a commutative (semi)ring.

To avoid making this compromise, we instead state these definitions as `M →ₗ[R] N →ₗ[S] P` or
`(M →ₗ[R] N) ≃ₗ[S] (M' →ₗ[R] N')` and require `SMulCommClass S R` on the appropriate modules. When
the caller has `CommSemiring R`, they can set `S = R` and `smulCommClass_self` will populate the
instance. If the caller only has `Semiring R` they can still set either `R = ℕ` or `S = ℕ`, and
`AddCommMonoid.nat_smulCommClass` or `AddCommMonoid.nat_smulCommClass'` will populate
the typeclass, which is still sufficient to recover a `≃+` or `→+` structure.

An example of where this is used is `LinearMap.prod_equiv`.
 -/
LibraryNote.bundled_maps_over_different_rings : Batteries.Util.LibraryNote
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K]
  (x : ArchimedeanClass.FiniteResidueField K), (⇑ArchimedeanClass.FiniteResidueField.mk ⁻¹' {x}).OrdConnected
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddZeroClass α], Function.Periodic f c → f c = f 0
-- Lean.Meta.IndPredBelow
/-- Recursor names (corresponding to the motives)  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.recNames : Lean.Meta.IndPredBelow.Context✝ → Array Lean.Name
-- Batteries.Tactic.Lemma
/-- `lemma` is not supported, please use `theorem` instead  -/
Batteries.Tactic.Lemma.lemmaCmd : Lean.ParserDescr
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.χ_unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F G : CategoryTheory.Sheaf J (Type (max u v))} (m : F ⟶ G) [inst_1 : CategoryTheory.Mono m]
  (χ' : G ⟶ CategoryTheory.Sheaf.Ω J),
  CategoryTheory.IsPullback m
      ((CategoryTheory.Sheaf.isTerminalTerminal J CategoryTheory.Limits.Types.isTerminalPUnit).from F) χ'
      (CategoryTheory.Sheaf.truth J) →
    χ' = CategoryTheory.Sheaf.χ m
-- Lean.Data.Json.Elab
/-- Json null value syntax.  -/
Lean.Json.jsonNull : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne' : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ W.negY Q * P 2 → IsUnit (W.dblZ P)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.step_filterMapM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} {m : Type w → Type w'} {n : Type w → Type w''}
  {β' : Type w} {f : β → n (Option β')} [inst_1 : Monad n] [inst_2 : MonadAttach n] [LawfulMonad n] [MonadLiftT m n],
  (Std.Iter.filterMapM f it).step =
    match it.step with
    | ⟨Std.IterStep.yield it' out, h⟩ => do
      let __do_lift ← MonadAttach.attach (f out)
      match __do_lift with
        | ⟨none, hf⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.filterMapM f it') ⋯))
        | ⟨some out', hf⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.Iter.filterMapM f it') out' ⋯))
    | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.filterMapM f it') ⋯))
    | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.pullbackCompatible_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (x : CategoryTheory.Presieve.FamilyOfElements P R) [inst_1 : R.HasPairwisePullbacks],
  x.Compatible ↔ x.PullbackCompatible
-- Mathlib.Data.Rel
SetRel.trans : ∀ {α : Type u_1} (R : SetRel α α) {a b c : α} [R.IsTrans], (a, b) ∈ R → (b, c) ∈ R → (a, c) ∈ R
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.card_eq : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α}, G.IsNClique n s → s.card = n
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α}, (List.map Prod.fst l).contains k = false → (Std.HashMap.Raw.ofList l).getKey? k = none
-- Mathlib.NumberTheory.Chebyshev
/-- The sum of `ArithmeticFunction.vonMangoldt` over integers `n ≤ x`.  -/
Chebyshev.termψ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.cocone_x : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F],
  (CategoryTheory.Limits.colimit.cocone F).pt = CategoryTheory.Limits.colimit F
-- Mathlib.Order.CompleteLattice.Defs
lt_biSup_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] {a : α} {s : Set β} {f : β → α},
  a < ⨆ i ∈ s, f i ↔ ∃ i ∈ s, a < f i
-- Mathlib.Data.Ordmap.Invariants
Ordnode.merge_nil_left : ∀ {α : Type u_1} (t : Ordnode α), t.merge Ordnode.nil = t
-- Mathlib.RingTheory.Ideal.Prod
/-- `I × J` as an ideal of `R × S`.  -/
Ideal.prod : {R : Type u} → {S : Type v} → [inst : Semiring R] → [inst_1 : Semiring S] → Ideal R → Ideal S → Ideal (R × S)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_con : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {A : Set M} {a : ↑A} {v : α → M},
  FirstOrder.Language.Term.realize v (L.con a).term = ↑a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.size_filterMap_le_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ}, (Std.ExtDHashMap.filterMap f m).size ≤ m.size
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multiequalizer is isomorphic to the equalizer of `∏ᶜ I.left ⇉ ∏ᶜ I.right`.  -/
CategoryTheory.Limits.Multiequalizer.isoEqualizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] →
          [inst_2 : CategoryTheory.Limits.HasProduct I.left] →
            [inst_3 : CategoryTheory.Limits.HasProduct I.right] →
              CategoryTheory.Limits.multiequalizer I ≅ CategoryTheory.Limits.equalizer I.fstPiMap I.sndPiMap
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set
Set.smul_set_inter₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : GroupWithZero α] [inst_1 : MulAction α β] {s t : Set β} {a : α},
  a ≠ 0 → a • (s ∩ t) = a • s ∩ a • t
-- Mathlib.Topology.Algebra.ConstMulAction
set_vadd_closure_subset : ∀ {M : Type u_1} {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α] (s : Set M)
  (t : Set α), s +ᵥ closure t ⊆ closure (s +ᵥ t)
-- Mathlib.Geometry.Euclidean.Volume.Measure
MeasureTheory.Measure.euclideanHausdorffMeasure.congr_simp : ∀ {X : Type u_1} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (d d_1 : ℕ),
  d = d_1 → MeasureTheory.Measure.euclideanHausdorffMeasure d = MeasureTheory.Measure.euclideanHausdorffMeasure d_1
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.coe_symm_toEquiv : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), ⇑(↑e).symm = ⇑e.symm
-- Init.Data.Nat.Dvd
Nat.dvd_eq_true_of_mod_eq_zero : ∀ {m n : ℕ}, (n % m == 0) = true → (m ∣ n) = True
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_comp_eq_preimage : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : One M] (g : κ → M) (f : ι → κ),
  Function.mulSupport (g ∘ f) = f ⁻¹' Function.mulSupport g
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Int.addRight_one_isCycle : (Equiv.addRight 1).IsCycle
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- If the `ChartedSpace` structure on a manifold `M` is given by an open embedding `e : M → H`,
then `e` is `C^n`.  -/
contMDiff_isOpenEmbedding : ∀ {𝕜 : 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] {e : M → H} (h : Topology.IsOpenEmbedding e) {n : WithTop ℕ∞} [inst_5 : Nonempty M],
  ContMDiff I I n e
-- Mathlib.Topology.Algebra.Group.Torsor
Continuous.vsub : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : AddGroup V] [inst_1 : TopologicalSpace V]
  [inst_2 : AddTorsor V P] [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P] [inst_5 : TopologicalSpace α]
  {f g : α → P}, Continuous f → Continuous g → Continuous fun x => f x -ᵥ g x
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
Real.strictConcave_binEntropy : StrictConcaveOn ℝ (Set.Icc 0 1) Real.binEntropy
-- Mathlib.Algebra.Homology.Localization
HomotopyCategory.homologyFunctor_inverts_quasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C] (i : ι),
  (HomotopyCategory.quasiIso C c).IsInvertedBy (HomotopyCategory.homologyFunctor C c i)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ [Inhabited α] {k : α} {f : β → β} {hc : k ∈ t.modify k f}, (t.modify k f).getKey k hc = k
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.next_le_iff_lt : ∀ {s : String.Slice} {p q : s.Pos} {h : p ≠ s.endPos}, p.next h ≤ q ↔ p < q
-- Mathlib.AlgebraicGeometry.Properties
/-- If `X` is reduced and has finitely many irreducible components, then the stalks at the generic
points of the irreducible components are fields.  -/
AlgebraicGeometry.isField_stalk_of_closure_mem_irreducibleComponents : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X),
  closure {x} ∈ irreducibleComponents ↥X → ∀ [AlgebraicGeometry.IsReduced X], IsField ↑(X.presheaf.stalk x)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Reinterpret an element of a type of linear maps as a linear map.  -/
LinearMapClass.linearMap : {R : Type u_1} →
  {M₁ : Type u_9} →
    {M₂ : Type u_10} →
      {F : Type u_14} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : Module R M₁] →
                [inst_4 : Module R M₂] → F → [inst_5 : FunLike F M₁ M₂] → [LinearMapClass F R M₁ M₂] → M₁ →ₗ[R] M₂
-- Init.Data.Nat.Lemmas
Nat.decidableExistsLT_eq_decidableExistsLTTR : @Nat.decidableExistsLT = @Nat.decidableExistsLTTR
-- Init.Data.Dyadic.Inv
/-- The equality `divAtPrec a b prec = a * invAtPrec b prec` does *not* hold in general:
`a * invAtPrec b prec` rounds `1/b` first and then multiplies, whereas `divAtPrec a b prec`
rounds `a/b` directly. The next two theorems pin the gap asymmetrically:

  `divAtPrec a b prec - a * 2 ^ (-prec) < a * invAtPrec b prec < divAtPrec a b prec + 2 ^ (-prec)`.

For nonneg `a` and positive `b`, `a * invAtPrec b prec` is less than `2 ^ (-prec)` larger
than `divAtPrec a b prec`.
 -/
Dyadic.mul_invAtPrec_lt_divAtPrec_add : ∀ {a b : Dyadic}, 0 ≤ a → 0 < b → ∀ (prec : ℤ), a * b.invAtPrec prec < a.divAtPrec b prec + Dyadic.ofIntWithPrec 1 prec
-- Init.Core
HasSSubset.mk : {α : Type u} → (α → α → Prop) → HasSSubset α
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- A cocone precomposed with a natural isomorphism is a colimit cocone
if and only if the original cocone is.
 -/
CategoryTheory.Limits.IsColimit.precomposeHomEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (α : F ≅ G) →
            (c : CategoryTheory.Limits.Cocone G) →
              CategoryTheory.Limits.IsColimit ((CategoryTheory.Limits.Cocone.precompose α.hom).obj c) ≃
                CategoryTheory.Limits.IsColimit c
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.Localization.essSurj_mapArrow_of_hasRightCalculusOfFractions : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions], L.mapArrow.EssSurj
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optTypeForStructInst : Lean.Parser.Parser
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.order_eq_find' : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} [inst_11 : DecidablePred fun n => p n ≠ 0] (hp : p ≠ 0), p.order = Nat.find ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
/-- Reduces the clause with respect to the given assignment  -/
Std.Tactic.BVDecide.LRAT.Internal.Clause.reduce : {α : outParam (Type u)} →
  {β : Type v} →
    [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] →
      β → Array Std.Tactic.BVDecide.LRAT.Internal.Assignment → Std.Tactic.BVDecide.LRAT.Internal.ReduceResult α
-- Lean.Meta.Tactic.LibrarySearch
/-- An exception ID that indicates further speculation on candidate lemmas should stop
and current results should be returned.
 -/
_private.Lean.Meta.Tactic.LibrarySearch.0.Lean.Meta.LibrarySearch.abortSpeculationId : Lean.InternalExceptionId
-- Mathlib.Order.Notation
HImp.mk : {α : Type u_1} → (α → α → α) → HImp α
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
CategoryTheory.Bicategory.whiskerLeft_eqToHom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g = h),
  CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.eqToHom η) = CategoryTheory.eqToHom ⋯
-- Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane
/-- The inversion with center `c` and radius `R` maps a sphere passing through the center to a
hyperplane.  -/
EuclideanGeometry.inversion_mem_perpBisector_inversion_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {c x y : P} {R : ℝ},
  R ≠ 0 →
    x ≠ c →
      y ≠ c →
        (EuclideanGeometry.inversion c R x ∈ AffineSubspace.perpBisector c (EuclideanGeometry.inversion c R y) ↔
          dist x y = dist y c)
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkHInjectiveTheoremValue? : Lean.ConstructorVal → Lean.Meta.MkHInjTypeResult✝ → Lean.MetaM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.category.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C}, CategoryTheory.Limits.Cocone.category = CategoryTheory.Category.mk' ⋯ ⋯ ⋯
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
norm_cfcₙ_one_sub_one_add_inv_lt_one : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] (a : A),
  ‖cfcₙ (fun x => 1 - (1 + x)⁻¹) a‖ < 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k : α} {f : β → β}, cmp (t.modify k f).minKey! t.minKey! = Ordering.eq
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- **Alias** of `MeasureTheory.SignedMeasure.of_sdiff_eq_zero_of_symmDiff_eq_zero_positive`.

---

If the symmetric difference of two positive sets is a null-set, then so are the differences
between the two sets.  -/
MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_positive : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u →
        MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v →
          s (symmDiff u v) = 0 → s (u \ v) = 0 ∧ s (v \ u) = 0
-- Init.Data.String.Termination
String.Pos.Down.mk.inj : ∀ {s : String} {inner inner_1 : s.Pos}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorHomMk_app_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J]
  (A B : CategoryTheory.Functor J (CategoryTheory.Pretriangulated.Triangle C))
  (hom₁ : A.comp CategoryTheory.Pretriangulated.Triangle.π₁ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₁)
  (hom₂ : A.comp CategoryTheory.Pretriangulated.Triangle.π₂ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₂)
  (hom₃ : A.comp CategoryTheory.Pretriangulated.Triangle.π₃ ⟶ B.comp CategoryTheory.Pretriangulated.Triangle.π₃)
  (comm₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂) hom₂ =
        CategoryTheory.CategoryStruct.comp hom₁ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₁Toπ₂))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_1)
  (comm₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃) hom₃ =
        CategoryTheory.CategoryStruct.comp hom₂ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_3)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (A.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁)
          (CategoryTheory.Functor.whiskerRight hom₁ (CategoryTheory.shiftFunctor C 1)) =
        CategoryTheory.CategoryStruct.comp hom₃ (B.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₃Toπ₁))
      CategoryTheory.Pretriangulated.Triangle.functorHomMk._auto_5)
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorHomMk A B hom₁ hom₂ hom₃ comm₁ comm₂ comm₃).app j).hom₂ = hom₂.app j
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_npowRec : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : SeminormedRing R]
  (f : BoundedContinuousFunction α R) (n : ℕ), ⇑(npowRec n f) = ⇑f ^ n
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateFieldMin_1 : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L₁ L₂ : IntermediateField k K) [FiniteDimensional k ↥L₂], FiniteDimensional k ↥(L₁ ⊓ L₂)
-- Batteries.Recycling.MonadSatisfying.Vector
Vector.mapM_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : MonadSatisfying m] (a : Array α) (h : a.size = n) (f : α → m β),
  Vector.mapM f (Vector.mk a h) =
    (fun x =>
        match x with
        | ⟨a_1, h'⟩ => Vector.mk a_1 ⋯) <$>
      satisfying ⋯
-- Mathlib.RingTheory.Ideal.Height
/-- `dim R ≤ n` if and only if the height of all prime ideals is less than `n`.  -/
ringKrullDim_le_iff_height_le : ∀ {R : Type u_2} [inst : CommRing R] (n : WithBot ℕ∞), ringKrullDim R ≤ n ↔ ∀ ⦃p : Ideal R⦄, p.IsPrime → ↑p.height ≤ n
-- Mathlib.Algebra.Lie.DirectSum
DirectSum.instLieModule : ∀ {R : Type u} {ι : Type v} [inst : CommRing R] {L : Type w₁} {M : ι → Type w} [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : (i : ι) → AddCommGroup (M i)] [inst_4 : (i : ι) → Module R (M i)]
  [inst_5 : (i : ι) → LieRingModule L (M i)] [∀ (i : ι), LieModule R L (M i)], LieModule R L (DirectSum ι fun i => M i)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Icc_add_one_left_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] [NoMaxOrder α] (a b : α),
  Set.Icc (a + 1) b = Set.Ioc a b
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A)
  (x : R),
  (DoubleQuot.quotQuotEquivQuotSup I J) ((algebraMap R ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mk I) J)) x) =
    (algebraMap R (A ⧸ I ⊔ J)) x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.iteratedDeriv_odd_sinh : ∀ (n : ℕ), iteratedDeriv (2 * n + 1) Complex.sinh = Complex.cosh
-- Mathlib.Data.Part
Part.append_def : ∀ {α : Type u_1} [inst : Append α] (a b : Part α),
  a ++ b = do
    let y ← a
    Part.map (fun x => y ++ x) b
-- Lean.Message
Lean.MessageData.format : Lean.MessageData → optParam (Option Lean.MessageDataContext) none → BaseIO Std.Format
-- Mathlib.GroupTheory.SpecificGroups.Dihedral
/-- If n is odd, then the Dihedral group of order $2n$ has $n(n+3)$ pairs of commuting elements.  -/
DihedralGroup.card_commute_odd : ∀ {n : ℕ}, Odd n → Nat.card { p // Commute p.1 p.2 } = n * (n + 3)
-- Init.Core
/-- Superset relation: `a ⊇ b`  

Conventions for notations in identifiers:

 * The recommended spelling of `⊇` in identifiers is `superset` (prefer `⊆` over `⊇`). -/
Superset : {α : Type u_1} → [HasSubset α] → α → α → Prop