mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
/-- a morphism `S₁.X₂ ⟶ S₂.X₁`  -/
CategoryTheory.ShortComplex.Homotopy.h₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        {φ₁ φ₂ : S₁ ⟶ S₂} → CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ → (S₁.X₂ ⟶ S₂.X₁)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι} [NeZero 2]
  [IsDomain R] [Module.IsTorsionFree R M], P.pairing i j = 0 ↔ P.pairing j i = 0
-- Mathlib.Order.CompleteLattice.SetLike
Sublattice.ext_mem : ∀ {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L}, (∀ (x : X), x ∈ S ↔ x ∈ T) → S = T
-- Std.Http.Internal.Encode
/-- Encodes a type `t` to a `ChunkedBuffer`.
 -/
Std.Http.Internal.Encode.encode : (v : Std.Http.Version) →
  {t : Type} →
    [self : Std.Http.Internal.Encode v t] → Std.Http.Internal.ChunkedBuffer → t → Std.Http.Internal.ChunkedBuffer
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.M.mk_surjective : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  (m : AddMonCat.FilteredColimits.M F), ∃ j x, AddMonCat.FilteredColimits.M.mk F ⟨j, x⟩ = m
-- Mathlib.Analysis.Normed.Module.Span
/-- Given a unit element `x` of a normed space `E` over a field `𝕜`, the natural
linear isometry equivalence from `𝕜` to the span of `x`.  -/
LinearIsometryEquiv.toSpanUnitSingleton : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NormedDivisionRing 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [inst_2 : Module 𝕜 E] → [NormSMulClass 𝕜 E] → (x : E) → ‖x‖ = 1 → 𝕜 ≃ₗᵢ[𝕜] ↥(𝕜 ∙ x)
-- Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts
/-- Show that if the two given fans in `extendFan` are limits, then the constructed fan is also a
limit.
 -/
CategoryTheory.extendFanIsLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      (f : Fin (n + 1) → C) →
        {c₁ : CategoryTheory.Limits.Fan fun i => f i.succ} →
          {c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt} →
            CategoryTheory.Limits.IsLimit c₁ →
              CategoryTheory.Limits.IsLimit c₂ → CategoryTheory.Limits.IsLimit (CategoryTheory.extendFan c₁ c₂)
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_left_pure_ceil_sub_one : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (x : α),
  Filter.Tendsto Int.floor (nhdsWithin x (Set.Iio x)) (pure (⌈x⌉ - 1))
-- Mathlib.Tactic.Linarith.Parsing
/-- `sum.mul s1 s2` distributes the multiplication of two sums.  -/
Mathlib.Tactic.Linarith.Sum.mul : Mathlib.Tactic.Linarith.Sum → Mathlib.Tactic.Linarith.Sum → Mathlib.Tactic.Linarith.Sum
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.π_descTruncGT_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
  [inst_6 : t.IsGE Y n₁] {Z : C} (h_1 : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGTπ n₀).app X)
      (CategoryTheory.CategoryStruct.comp (t.descTruncGT f n₀ n₁ h) h_1) =
    CategoryTheory.CategoryStruct.comp f h_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
IsUnit.mulLECancellable : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] {a : M}, IsUnit a → MulLECancellable a
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg_def : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Neg G] (μ : MeasureTheory.Measure G),
  μ.neg = MeasureTheory.Measure.map Neg.neg μ
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.instIsOverHomSchemeTransPullbackSymmetryOverSpecOfInferInstanceOverClassPullbackSpecIso' : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  AlgebraicGeometry.Scheme.Hom.IsOver
    (CategoryTheory.Limits.pullbackSymmetry
          (AlgebraicGeometry.Spec (CommRingCat.of T) ↘ AlgebraicGeometry.Spec (CommRingCat.of R))
          (AlgebraicGeometry.Spec (CommRingCat.of S) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) ≪≫
        AlgebraicGeometry.pullbackSpecIso' R S T).hom
    (AlgebraicGeometry.Spec (CommRingCat.of S))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    t.isEmpty = false →
      ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare k km).isLE = true
-- Init.Omega.Int
_private.Init.Omega.Int.0.Int.neg.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.const_apply : ∀ (α : Type u) {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] (b : β),
  ⇑(BoundedContinuousFunction.const α b) = fun x => b
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.ppCutsat : Lean.Meta.Grind.M✝ Unit
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∈ Std.HashSet.Raw.ofList l ↔ l.contains k = true
-- Init.Data.List.Basic
/-- Alternates the lists in `xs` with the separator `sep`, appending them. The resulting list is
flattened.

`O(|xs|)`.

`List.intersperse` is a similar function that alternates a separator element with the elements of a
list.

Examples:
* `List.intercalate sep [] = []`
* `List.intercalate sep [a] = a`
* `List.intercalate sep [a, b] = a ++ sep ++ b`
* `List.intercalate sep [a, b, c] = a ++ sep ++ b ++ sep ++ c`
 -/
List.intercalate : {α : Type u} → List α → List (List α) → List α
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instNatCast : {R₁ : Type u_1} →
  [inst : Semiring R₁] →
    {M₁ : Type u_4} →
      [inst_1 : TopologicalSpace M₁] →
        [inst_2 : AddCommMonoid M₁] → [inst_3 : Module R₁ M₁] → [ContinuousAdd M₁] → NatCast (M₁ →L[R₁] M₁)
-- Init.Data.SInt.Basic
/-- Non-strict inequality of 64-bit signed integers, defined as inequality of the corresponding integers.
Usually accessed via the `≤` operator.
 -/
Int64.le : Int64 → Int64 → Prop
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.extendScalars_toSubfield : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F E : IntermediateField K L}
  (h : F ≤ E), (IntermediateField.extendScalars h).toSubfield = E.toSubfield
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
groupAddGroupEquivalence_unitIso : groupAddGroupEquivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id GrpCat)
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
_private.Mathlib.Analysis.SpecialFunctions.BinaryEntropy.0.Real.binEntropy.eq_1 : ∀ (p : ℝ), Real.binEntropy p = p * Real.log p⁻¹ + (1 - p) * Real.log (1 - p)⁻¹
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
/-- **Alias** of the reverse direction of `Set.finite_neg`. -/
Set.Finite.neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, s.Finite → (-s).Finite
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.foldlM_eq_foldlM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} {a : Type u_1} {f : a → α → m a} {init : a}
  [inst : Monad m] [LawfulMonad m] {t : RBTree.RBSet α cmp}, RBTree.RBSet.foldlM f init t = List.foldlM f init t.toList
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.Entry.mk.injEq : ∀ (name : Lean.Name) (info : Lean.Meta.MatcherInfo) (name_1 : Lean.Name) (info_1 : Lean.Meta.MatcherInfo),
  ({ name := name, info := info } = { name := name_1, info := info_1 }) = (name = name_1 ∧ info = info_1)
-- Init.Data.Array.DecidableEq
Array.eq_of_isEqv : ∀ {α : Type u_1} [inst : DecidableEq α] (xs ys : Array α), (xs.isEqv ys fun x y => decide (x = y)) = true → xs = ys
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.zero_rootSpace_eq_top_of_nilpotent : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing.IsNilpotent L], LieAlgebra.rootSpace ⊤ 0 = ⊤
-- Mathlib.Algebra.Order.Ring.WithTop
_private.Mathlib.Algebra.Order.Ring.WithTop.0.WithTop.instMonoidWithZero.match_1.eq_2 : ∀ {α : Type u_1} (motive : WithTop α → ℕ → Sort u_2) (h_1 : (a : α) → (n : ℕ) → motive (some a) n)
  (h_2 : Unit → motive none 0) (h_3 : (_n : ℕ) → motive none _n.succ),
  (match none, 0 with
    | some a, n => h_1 a n
    | none, 0 => h_2 ()
    | none, _n.succ => h_3 _n) =
    h_2 ()
-- Init.Data.UInt.Bitwise
UInt16.toUInt32_shiftLeft_of_lt : ∀ (a b : UInt16), b < 16 → (a <<< b).toUInt32 = a.toUInt32 <<< b.toUInt32 % 65536
-- Aesop.Tree.AddRapp
Aesop.AddRapp.parent : Aesop.AddRapp → Aesop.GoalRef
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C) [F.PreservesHomology],
  F.PreservesRightHomologyOf S
-- Mathlib.Logic.Equiv.Fin.Basic
Fin.appendEquiv_symm_apply : ∀ {α : Type u_1} (m n : ℕ) (f : Fin (m + n) → α),
  (Fin.appendEquiv m n).symm f = (fun i => f (Fin.castAdd n i), fun i => f (Fin.natAdd m i))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_nonneg_iff : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddLeftMono M] {x : M} {n : ℕ},
  n ≠ 0 → (0 ≤ n • x ↔ 0 ≤ x)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.equivalence_unitIso : AddMonCat.equivalence.unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id AddMonCat)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.sub_im_self : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : AddGroup R], a - a.im = ↑a.re
-- Mathlib.RingTheory.EuclideanDomain
/-- Create a `GCDMonoid` whose `GCDMonoid.gcd` matches `EuclideanDomain.gcd`.  -/
EuclideanDomain.gcdMonoid : (R : Type u_1) → [inst : EuclideanDomain R] → [DecidableEq R] → GCDMonoid R
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The cocone over the proposed colimit commutative ring.  -/
CommRingCat.Colimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → (F : CategoryTheory.Functor J CommRingCat) → CategoryTheory.Limits.Cocone F
-- Init.Data.SInt.Lemmas
Int8.zero_le_ofNat_of_lt : ∀ {a : ℕ}, a < 2 ^ 7 → 0 ≤ Int8.ofNat a
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod_comp_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)),
  (f.noncommCoprod g comm).comp (MonoidHom.inr M N) = g
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.ball_mem_nhds : ∀ {α : Type ua} [inst : UniformSpace α] (x : α) ⦃V : SetRel α α⦄, V ∈ uniformity α → UniformSpace.ball x V ∈ nhds x
-- Mathlib.Data.ENat.Basic
ENat.eq_top_iff_forall_ge : ∀ {n : ℕ∞}, n = ⊤ ↔ ∀ (m : ℕ), ↑m ≤ n
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.mk'.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C} {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g : X ⟶ Y}
  {base' base'_1 : CategoryTheory.CatEnrichedOrdinary.homEquiv f ⟶ CategoryTheory.CatEnrichedOrdinary.homEquiv g},
  { base' := base' } = { base' := base'_1 } → base' = base'_1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs.mk.inj : ∀ {pre post : Lean.Meta.Simp.SimprocTree} {simprocNames erased : Lean.PHashSet Lean.Name}
  {pre_1 post_1 : Lean.Meta.Simp.SimprocTree} {simprocNames_1 erased_1 : Lean.PHashSet Lean.Name},
  { pre := pre, post := post, simprocNames := simprocNames, erased := erased } =
      { pre := pre_1, post := post_1, simprocNames := simprocNames_1, erased := erased_1 } →
    pre = pre_1 ∧ post = post_1 ∧ simprocNames = simprocNames_1 ∧ erased = erased_1
-- Mathlib.CategoryTheory.Monoidal.Limits.Basic
CategoryTheory.Limits.lim_ε_π : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] [inst_3 : CategoryTheory.MonoidalCategory C] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε CategoryTheory.Limits.lim)
      (CategoryTheory.Limits.limit.π (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor J C))
        j) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (f : α → ENNReal) (s : Set α),
  ⨍⁻ (x : α) in s, f x ∂μ = (∫⁻ (x : α) in s, f x ∂μ) / μ s
-- Init.Core
DoResultBC.continue.sizeOf_spec : ∀ {σ : Type u} [inst : SizeOf σ] (a : σ), sizeOf (DoResultBC.continue a) = 1 + sizeOf a
-- Mathlib.Data.Tree.Get
/-- Retrieves an element uniquely determined by a `PosNum` from the tree,
taking the following path to get to the element:
- `bit0` - go to left child
- `bit1` - go to right child
- `PosNum.one` - retrieve from here  -/
BinaryTree.get : {α : Type u_1} → PosNum → BinaryTree α → Option α
-- Mathlib.Tactic.ENatToNat
/-- Finds the first `ENat` in the context and applies the `cases` tactic to it.
Then simplifies expressions involving `⊤` using the `enat_to_nat_top` simp set.  -/
Mathlib.Tactic.ENatToNat.tacticCases_first_enat : Lean.ParserDescr
-- Mathlib.CategoryTheory.ConnectedComponents
/-- This type indexes the connected components of the category `J`.  -/
CategoryTheory.ConnectedComponents : (J : Type u₁) → [CategoryTheory.Category.{v₁, u₁} J] → Type u₁
-- Init.Data.List.Basic
/-- Non-strict ordering of lists with respect to a strict ordering of their elements.

`as ≤ bs` if `¬ bs < as`.

This relation can be treated as a lexicographic order if the underlying `LT α` instance is
well-behaved. In particular, it should be irreflexive, asymmetric, and antisymmetric. These
requirements are precisely formulated in `List.cons_le_cons_iff`. If these hold, then `as ≤ bs` if
and only if:
 * `as` is empty, or
 * both `as` and `bs` are non-empty, and the head of `as` is less than the head of `bs`, or
 * both `as` and `bs` are non-empty, their heads are equal, and the tail of `as` is less than or
   equal to the tail of `bs`.
 -/
List.le : {α : Type u} → [LT α] → List α → List α → Prop
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.toSubmodule : {A : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing A] → [inst_1 : LieRing L] → [inst_2 : Module A L] → LieRinehartSubalgebra A L → Submodule A L
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_comp : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.Initial] [G.Initial], (F.comp G).Initial
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.eq_of_forall_toMeasure_apply_eq_iff : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ ν : MeasureTheory.ProbabilityMeasure Ω},
  μ = ν ↔ ∀ (s : Set Ω), MeasurableSet s → ↑μ s = ↑ν s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.keysArray.isEmpty = t.isEmpty
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_Ioi_of_forall_Ioc : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {mβ : MeasurableSpace β}
  [inst : LinearOrder α] [Filter.atTop.IsCountablyGenerated] {x : α} {g : α → β},
  (∀ t > x, AEMeasurable g (μ.restrict (Set.Ioc x t))) → AEMeasurable g (μ.restrict (Set.Ioi x))
-- Init.Data.Slice.List.Iterator
ListSlice.instToIterator : {α : Type u} →
  Std.ToIterator (Std.Slice (Std.Slice.Internal.ListSliceData α)) Id
    (Std.Iterators.Types.Take (Std.Iterators.Types.ListIterator α) Id) α
-- Mathlib.CategoryTheory.Monoidal.Braided.Opposite
CategoryTheory.BraidedCategory.op_tensorμ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y W Z : C),
  (CategoryTheory.MonoidalCategory.tensorμ X W Y Z).op =
    CategoryTheory.MonoidalCategory.tensorμ (Opposite.op X) (Opposite.op Y) (Opposite.op W) (Opposite.op Z)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k k' : α} [inst_1 : Inhabited β] {f : Option β → Option β},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.Const.alter t k f) k' =
    if cmp k k' = Ordering.eq then (f (Std.ExtDTreeMap.Const.get? t k)).get! else Std.ExtDTreeMap.Const.get! t k'
-- Init.Data.Iterators.Basic
Std.Iterators.Finite.mk : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β],
  WellFounded Std.IterM.IsPlausibleSuccessorOf → Std.Iterators.Finite α m
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.instFreeCotangentToExtensionUnitLocalizationAway : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S], Module.Free S (Algebra.Generators.localizationAway S r).toExtension.Cotangent
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_top : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] (x : M), x ∈ ⊤
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.extendCoordChange_source_mem_nhdsWithin : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} {x : E},
  x ∈ (ModelWithCorners.extendCoordChange e e').source →
    (ModelWithCorners.extendCoordChange e e').source ∈ nhdsWithin x (Set.range ↑I)
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.ext : ∀ {X : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} {x y : hom.InvStruct},
  x.inv = y.inv → x.homInvId ≍ y.homInvId → x.invHomId ≍ y.invHomId → x = y
-- Mathlib.CategoryTheory.Join.Basic
/-- `mapPair` respects identities  -/
CategoryTheory.Join.mapPairId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Join.mapPair (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id D) ≅
          CategoryTheory.Functor.id (CategoryTheory.Join C D)
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.refl.eq_1 : ∀ (M : Type u_9) [inst : Mul M], MulEquiv.refl M = { toEquiv := Equiv.refl M, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- The map of a cofan is a colimit iff the cofan consisting of the mapped morphisms is a colimit.
This essentially lets us commute `Cofan.mk` with `Functor.mapCocone`.
 -/
CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              {P : C} →
                (g : (j : J) → f j ⟶ P) →
                  CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.Cofan.mk P g)) ≃
                    CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Mathlib.Logic.Function.Basic
Function.instIsLinearOrderSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [IsLinearOrder α r], IsLinearOrder α (Function.swap r)
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- The **Wedderburn–Artin Theorem**: a semisimple ring is isomorphic to a
product of matrix rings over division rings.  -/
IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing : ∀ (R : Type u) [inst : Ring R] [IsSemisimpleRing R],
  ∃ n D d x, (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)))
-- Mathlib.SetTheory.Ordinal.Rank
/-- if `r a b` then the rank of `a` is less than the rank of `b`.  -/
Acc.rank_lt_of_rel : ∀ {α : Type u} {a b : α} {r : α → α → Prop} (hb : Acc r b) (h : r a b), ⋯.rank < hb.rank
-- Mathlib.Algebra.Squarefree.Basic
IsUnit.squarefree : ∀ {R : Type u_1} [inst : CommMonoid R] {x : R}, IsUnit x → Squarefree x
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.notMem_bot : ∀ {α : Type u_1} [inst : LE α] {a : α}, a ∉ ⊥
-- Mathlib.Algebra.GroupWithZero.Action.TransferInstance
/-- Transfer `DistribSMul` across an `Equiv`  -/
Equiv.distribSMul : (M : Type u_1) →
  {A : Type u_3} → {B : Type u_4} → (e : A ≃ B) → [inst : AddZeroClass B] → [DistribSMul M B] → DistribSMul M A
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst_iCycles_even_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) [inst_3 : CategoryTheory.CategoryWithHomology C] {j : ℕ},
  c.Rel (c.prev j) j →
    c.Rel j (c.next j) →
      Even j →
        ∀ {Z : C} (h : A ⟶ Z),
          CategoryTheory.CategoryStruct.comp ((HomologicalComplex.alternatingConst A hOdd hEven hc).iCycles j)
              (CategoryTheory.CategoryStruct.comp φ h) =
            CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.ext_iff : ∀ {E : Type u_3} [inst : Group E] {p q : GroupSeminorm E}, p = q ↔ ∀ (x : E), p x = q x
-- Mathlib.Order.Ideal
Order.Ideal.mem_inf : ∀ {P : Type u_1} [inst : SemilatticeSup P] [inst_1 : IsCodirectedOrder P] {x : P} {I J : Order.Ideal P},
  x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.symm_iso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y), f.symm.iso = f.iso.symm
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- The trailing coefficient of the power of a function is the power of the trailing coefficient.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_fun_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {n : ℕ} {f : 𝕜 → 𝕜},
  MeromorphicAt f x → meromorphicTrailingCoeffAt (fun z => f z ^ n) x = meromorphicTrailingCoeffAt f x ^ n