mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.CommutingProbability
commProb_pi : ∀ {α : Type u_2} (i : α → Type u_3) [inst : Fintype α] [inst_1 : (a : α) → Mul (i a)],
  commProb ((a : α) → i a) = ∏ a, commProb (i a)
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
/-- The map `RightHomotopyClass X Y → (L.obj X ⟶ L.obj Y)` when `L` is
a localization functor with respect to `weakEquivalences C`.  -/
HomotopicalAlgebra.rightHomotopyClassToHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {H : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} H] →
          (L : CategoryTheory.Functor C H) →
            [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              {X Y : C} → HomotopicalAlgebra.RightHomotopyClass X Y → (L.obj X ⟶ L.obj Y)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.mono_eta_iff_residuallyFinite : ∀ (G : GrpCat), CategoryTheory.Mono (ProfiniteGrp.ProfiniteCompletion.eta G) ↔ Group.ResiduallyFinite ↑G
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] {l : List α}
  {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {h' : k' ∈ Std.DTreeMap.Const.insertManyIfNewUnit t l},
      k ∉ t →
        List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
          k ∈ l → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKey k' h' = k
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.instPreadditive : {k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] → [inst_1 : Ring k] → [inst_2 : Monoid G] → CategoryTheory.Preadditive (TopRep k G)
-- Init.Data.Vector.Monadic
Vector.anyM_pure : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → Bool} {xs : Vector α n},
  Vector.anyM (fun x => pure (p x)) xs = pure (xs.any p)
-- Mathlib.Order.UpperLower.Relative
isRelUpperSet_self : ∀ {α : Type u_1} {s : Set α} [inst : LE α], IsRelUpperSet s fun x => x ∈ s
-- Mathlib.Topology.ContinuousMap.Ordered
/-- Extend a continuous function `f : C(Set.Icc a b, β)` to a function `f : C(α, β)`.  -/
ContinuousMap.IccExtend : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : LinearOrder α] → [OrderTopology α] → {a b : α} → a ≤ b → C(↑(Set.Icc a b), β) → C(α, β)
-- Init.Internal.Order.Basic
Lean.Order.instCCPOOption : {α : Type u_1} → Lean.Order.CCPO (Option α)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.id_tensorHom_id : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C}, CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Init.Data.List.Nat.Modify
List.getElem?_modifyHead_zero : ∀ {α : Type u_1} {l : List α} {f : α → α}, (List.modifyHead f l)[0]? = Option.map f l[0]?
-- Init.Data.Array.Basic
Array.instAppend : {α : Type u} → Append (Array α)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.neg_neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [MeasurableNeg G] (μ : MeasureTheory.Measure G),
  μ.neg.neg = μ
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.existsUnique : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g}
  (hs : CategoryTheory.Limits.IsLimit s) {W : C} (k : W ⟶ X),
  CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g →
    ∃! l, CategoryTheory.CategoryStruct.comp l s.ι = k
-- Mathlib.Algebra.Homology.EulerCharacteristic
/-- If a complex has finite rank support contained in a finite set,
the `finsum` Euler characteristic equals the finite sum over that set.  -/
HomologicalComplex.eulerChar_eq_sum_finSet_of_finrankSupport_subset : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} {c : ComplexShape ι} [inst_1 : c.EulerCharSigns]
  (C : HomologicalComplex (ModuleCat R) c) (indices : Finset ι),
  GradedObject.finrankSupport C.X ⊆ ↑indices → C.eulerChar = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(C.X i))
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coreflection_inv : ∀ {ι : 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 : ι),
  (P.coreflection i)⁻¹ = P.coreflection i
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.support_coeff : ∀ (b o : Ordinal.{u_1}), (Ordinal.CNF.coeff b o).support = (List.map Prod.fst (Ordinal.CNF b o)).toFinset
-- Lean.Meta.Diagnostics
Lean.Meta.DiagSummary.data : Lean.Meta.DiagSummary → Array Lean.MessageData
-- Init.GetElem
getElem?_pos : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) (h : dom c i), c[i]? = some c[i]
-- Mathlib.CategoryTheory.Sites.Coherent.Comparison
CategoryTheory.instPreregularOfPrecoherentOfHasFiniteCoproducts : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Precoherent C]
  [CategoryTheory.Limits.HasFiniteCoproducts C], CategoryTheory.Preregular C
-- Mathlib.Data.Set.Card
/-- A version of the pigeonhole principle for `Set`s rather than `Finset`s.

See also `Finset.exists_ne_map_eq_of_card_lt_of_maps_to` and
`Set.exists_ne_map_eq_of_ncard_lt_of_maps_to`.  -/
Set.exists_ne_map_eq_of_encard_lt_of_maps_to : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  t.encard < s.encard → Set.MapsTo f s t → ∃ a₁ ∈ s, ∃ a₂ ∈ s, a₁ ≠ a₂ ∧ f a₁ = f a₂
-- Init.Data.Range.Polymorphic.PRange
Std.Rcc.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (lower upper : α), (sizeOf lower...=upper) = 1 + sizeOf lower + sizeOf upper
-- Mathlib.Lean.Name
/-- Determines if the pretty-printed version of the given name would parse as an
`ident` with an underlying name (via `getId`) equal to the original name.
The pretty-printer usually escapes unparsable components of a name with `«»`,
but makes exceptions for various names with special meaning, meaning that the result does not
round trip. We therefore re-check those conditions here.

This function is intended to be "safe" in that if it returns `true`,
the name will definitely round trip. (The converse is not guaranteed.) Any deviation from this
behavior is a bug which should be fixed.
 -/
Lean.Name.willRoundTrip : Lean.Name → Bool
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
/-- If the tangent of a complex number is well-defined,
then it is equal to zero iff the number is equal to `k * π` for an integer `k`.

See also `Complex.tan_eq_zero_iff` for a version that takes into account junk values of `θ`.  -/
Complex.tan_eq_zero_iff' : ∀ {θ : ℂ}, Complex.cos θ ≠ 0 → (Complex.tan θ = 0 ↔ ∃ k, ↑k * ↑Real.pi = θ)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.mkIso_inv_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.Grp C} (e : G.X ≅ H.X)
  (one_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
      CategoryTheory.Grp.mkIso._auto_1)
  (mul_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
          CategoryTheory.MonObj.mul)
      CategoryTheory.Grp.mkIso._auto_3),
  (CategoryTheory.Grp.mkIso e one_f mul_f).inv.hom.hom = e.inv
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_mul_right_one' : ∀ {α : Type u_2} [inst : Group α] {b : α}, Finset.preimage 1 (fun x => x * b⁻¹) ⋯ = {b}
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is strictly monotone on a neighborhood of `a`
and the image of this set under `f` is a neighborhood of `f a`, then `f` is continuous at `a`.  -/
StrictMonoOn.continuousAt_of_image_mem_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α}, StrictMonoOn f s → s ∈ nhds a → f '' s ∈ nhds (f a) → ContinuousAt f a
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- A Type `R` is a `CompatibleRing` if it is a structure for the language of rings and this
structure is the same as the structure already given on `R` by the classes `Add`, `Mul` etc.

It is recommended to use this type class as a hypothesis to any theorem whose statement
requires a type to have be both a `Ring` (or `Field` etc.) and a
`Language.ring.Structure`  -/
FirstOrder.Ring.CompatibleRing : (R : Type u_2) → [Add R] → [Mul R] → [Neg R] → [One R] → [Zero R] → Type u_2
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Construct a morphism between parallel pairs.  -/
CategoryTheory.Limits.parallelPairHom : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X' Y' : C} →
        (f g : X ⟶ Y) →
          (f' g' : X' ⟶ Y') →
            (p : X ⟶ X') →
              (q : Y ⟶ Y') →
                CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p f' →
                  CategoryTheory.CategoryStruct.comp g q = CategoryTheory.CategoryStruct.comp p g' →
                    (CategoryTheory.Limits.parallelPair f g ⟶ CategoryTheory.Limits.parallelPair f' g')
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformly.add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformly f g l → TendstoUniformly f' g' l → TendstoUniformly (f + f') (g + g') l
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNorm_mul : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype l] [inst_1 : Fintype m]
  [inst_2 : Fintype n] [inst_3 : NonUnitalSeminormedRing α] (A : Matrix l m α) (B : Matrix m n α), ‖A * B‖ ≤ ‖A‖ * ‖B‖
-- Std.Sync.RecursiveMutex
_private.Std.Sync.RecursiveMutex.0.Std.RecursiveMutex.ref : {α : Type} → Std.RecursiveMutex α → IO.Ref α
-- Init.Data.List.Control
/-- Folds a monadic function over a list from the right, accumulating a value starting with `init`. The
accumulated value is combined with the each element of the list in reverse order, using `f`.

Example:
```lean example
example [Monad m] (f : α → β → m β) :
  List.foldrM (m := m) f x₀ [a, b, c] = (do
    let x₁ ← f c x₀
    let x₂ ← f b x₁
    let x₃ ← f a x₂
    pure x₃)
  := by rfl
```
 -/
List.foldrM : {m : Type u → Type v} → [Monad m] → {s : Type u} → {α : Type w} → (α → s → m s) → s → List α → m s
-- Mathlib.Data.Set.Basic
Set.union_union_distrib_right : ∀ {α : Type u} (s t u : Set α), s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {f : β → β}, (Std.DHashMap.Const.modify m k f).isEmpty = m.isEmpty
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Yoneda.fullyFaithful_preimage : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C}
  (f : CategoryTheory.yoneda.obj X ⟶ CategoryTheory.yoneda.obj Y),
  CategoryTheory.Yoneda.fullyFaithful.preimage f =
    (CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) (CategoryTheory.CategoryStruct.id X)
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
/-- **Alias** of `SSet.degenerate_eq_univ_of_hasDimensionLT`. -/
SSet.degenerate_eq_top_of_hasDimensionLT : ∀ (X : SSet) (d : ℕ) [X.HasDimensionLT d] (n : ℕ),
  autoParam (d ≤ n) SSet.degenerate_eq_univ_of_hasDimensionLT._auto_1 → X.degenerate n = Set.univ
-- Lean.Parser.Basic
/-- Run `p`, falling back to `q` if `p` failed without consuming any input.

NOTE: In order for the pretty printer to retrace an `orelse`, `p` must be a call to `node` or some other parser
producing a single node kind. Nested `orelse` calls are flattened for this, i.e. `(node k1 p1 <|> node k2 p2) <|> ...`
is fine as well.  -/
Lean.Parser.orelse : Lean.Parser.Parser → Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullbackCoverOfRight.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y : C} (E E_1 : CategoryTheory.PreZeroHypercover Y)
  (e_E : E = E_1) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)],
  E.pullbackCoverOfRight f g = E_1.pullbackCoverOfRight f g
-- Init.Data.SInt.Lemmas
Int64.one_mul : ∀ (a : Int64), 1 * a = a
-- Mathlib.Analysis.Convex.Gauge
mem_frontier_of_gauge_eq_one : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], Convex ℝ s → 0 ∈ s → Absorbent ℝ s → gauge s x = 1 → x ∈ frontier s
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.coeMulHom_apply : ∀ {α : Type u} [inst : Mul α] (a : α), WithOne.coeMulHom a = ↑a
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.fineSubfamilyOn_iff_frequently : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {f : X → Set (Set X)} {s : Set X},
  v.FineSubfamilyOn f s ↔ ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The canonical map from the empty locally ringed space.  -/
AlgebraicGeometry.LocallyRingedSpace.emptyTo : (X : AlgebraicGeometry.LocallyRingedSpace) → ∅ ⟶ X
-- Mathlib.Data.Fin.Tuple.Basic
Fin.consEquiv_symm_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_1) (f : (i : Fin (n + 1)) → α i), (Fin.consEquiv α).symm f = (f 0, Fin.tail f)
-- Mathlib.Algebra.DualNumber
DualNumber.eps_pow_two : ∀ {R : Type u_1} [inst : Semiring R], DualNumber.eps ^ 2 = 0
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.nil_reverse : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, p.reverse.Nil ↔ p.Nil
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.restrictPreimage : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → ∀ (t : Set X), IsCoveringMap (t.restrictPreimage f)
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.mem_iSup : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {I : Sort u_2} {f : I → ↥L} {x : X}, x ∈ ⨆ i, f i ↔ ∃ i, x ∈ f i
-- Mathlib.Data.Finset.Sort
Finset.sort_mk : ∀ {α : Type u_1} {m : Multiset α} (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r]
  [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] (h : m.Nodup), { val := m, nodup := h }.sort r = m.sort r
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.pow_right_iff : ∀ {α : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {x y : α} {m : ℕ},
  0 < m → (IsRelPrime x (y ^ m) ↔ IsRelPrime x y)
-- Init.Prelude
/-- Parses a literal symbol. The `&` prefix prevents it from being included in the set of reserved tokens ("keywords").
This means that the symbol can still be recognized as an identifier by other parsers.

Some syntax categories, such as `tactic`, automatically apply `&` to the first symbol.

Whitespace before or after the atom is used as a pretty printing hint.
For example, `" + "` parses `+` and pretty prints it with whitespace on both sides.
The whitespace has no effect on parsing behavior.

(Not exposed by parser description syntax:
If the `includeIdent` argument is true, lets `ident` be reinterpreted as `atom` if it matches.)
 -/
Lean.ParserDescr.nonReservedSymbol : String → Bool → Lean.ParserDescr
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.SubmersivePresentation.HasCoeffs.mk : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] {P : Algebra.SubmersivePresentation R S ι σ} {R₀ : Type u_5}
  [inst_4 : CommRing R₀] [inst_5 : Algebra R₀ R] [inst_6 : Algebra R₀ S] [inst_7 : IsScalarTower R₀ R S],
  P.coeffs ⊆ ↑(algebraMap R₀ R).range → P.HasCoeffs R₀
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_neg : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i : ι}, i < i0 → toZ i0 i < 0
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.im_pellZd : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), (Pell.pellZd a1 n).im = ↑(Pell.yn a1 n)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Pi-types are measurably equivalent to iterated products.  -/
MeasurableEquiv.piMeasurableEquivTProd : {δ' : Type u_5} →
  {π : δ' → Type u_6} →
    [inst : (x : δ') → MeasurableSpace (π x)] →
      [DecidableEq δ'] → {l : List δ'} → l.Nodup → (∀ (i : δ'), i ∈ l) → ((i : δ') → π i) ≃ᵐ List.TProd π l
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.isBigO_logb_log : ∀ {b : ℝ}, Real.logb b =O[⊤] Real.log
-- Mathlib.Data.Finset.Union
Finset.singleton_biUnion : ∀ {α : Type u_1} {β : Type u_2} {t : α → Finset β} [inst : DecidableEq β] {a : α}, {a}.biUnion t = t a
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.unitIso_inv_app_τ₂_app : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (X : CategoryTheory.ShortComplex (CategoryTheory.Functor J C)) (X_1 : J),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.unitIso J C).inv.app X).τ₂.app X_1 =
    CategoryTheory.CategoryStruct.id (X.X₂.obj X_1)
-- Init.Data.AC
Lean.Data.AC.mergeIdem.loop.eq_2 : ∀ (a : ℕ), Lean.Data.AC.mergeIdem.loop a [] = [a]
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd.eq_1 : ∀ {A : Type u_1} [inst : AddMonoid A] [inst_1 : Finset.HasAntidiagonal A],
  Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd =
    { toFun := fun x => ↑x.snd, invFun := fun x => ⟨x.1 + x.2, ⟨x, ⋯⟩⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddAction' : {α : Type u_1} →
  {β : Type u_2} →
    {l : Filter α} → {M : Type u_5} → [inst : AddMonoid M] → [AddAction M β] → AddAction (l.Germ M) (l.Germ β)
-- Mathlib.Algebra.Ring.GeomSum
geom_sum₂_succ_eq : ∀ {R : Type u_1} [inst : CommRing R] (x y : R) {n : ℕ},
  ∑ i ∈ Finset.range (n + 1), x ^ i * y ^ (n - i) = x ^ n + y * ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.associativity_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (X Y Z : C) {Z_1 : D}
  (h :
    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) h))
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.exists_pos_eq : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (self : RootPairing.RootPositiveForm S P) (i : ι), ∃ s > 0, (algebraMap S R) s = (self.form (P.root i)) (P.root i)
-- Mathlib.Data.Nat.Dist
Nat.dist_add_add_left : ∀ (k n m : ℕ), (k + n).dist (k + m) = n.dist m
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.ne_zero_of_mk'_ne_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {x : R} {y : ↥M}, IsLocalization.mk' S x y ≠ 0 → x ≠ 0
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- Product rule for Lie brackets: given two vector fields `V` and `W` on `M` and a function
`f : M → 𝕜`, we have `[f • V, W] = -(df W) • V + f • [V, W]`.
 -/
VectorField.mlieBracket_smul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E] {f : M → 𝕜},
  MDiffAt f x →
    (MDiffAt fun x => ⟨x, V x⟩) x →
      VectorField.mlieBracket I (f • V) W x = -(d% f x) (W x) • V x + f x • VectorField.mlieBracket I V W x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Do not use this. Use `le_of_add_le_add_left` instead.  -/
AddLeftReflectLE.le_of_add_le_add_left : ∀ {M : Type u_1} {inst : Add M} {inst_1 : LE M} [self : AddLeftReflectLE M] {a b₁ b₂ : M}, a + b₁ ≤ a + b₂ → b₁ ≤ b₂
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mem_mk' : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {sm : Subsemigroup R} (hm : ↑sm = s) {sa : AddSubgroup R}
  (ha : ↑sa = s) {x : R}, x ∈ NonUnitalSubring.mk' s sm sa hm ha ↔ x ∈ s
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary_eq_iSup : ∀ (n : ℕ), SSet.boundary n = ⨆ i, SSet.stdSimplex.face {i}ᶜ
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addZeroClass.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddZeroClass (f i)],
  Pi.addZeroClass = { toZero := Pi.instZero, toAdd := Pi.instAdd, zero_add := ⋯, add_zero := ⋯ }
-- Mathlib.Data.Seq.Basic
Stream'.Seq.fold_head : ∀ {α : Type u} {β : Type v} (init : β) (f : β → α → β) (s : Stream'.Seq α), (s.fold init f).head = some init
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
AlgebraicGeometry.Scheme.Hom.isIrreducible_preimage : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIrreducible f],
  IsOpenMap ⇑f → ∀ {s : Set ↥S}, IsIrreducible s → IsIrreducible (⇑f ⁻¹' s)
-- Lean.Level
Lean.instBEqLevelMVarId.beq : Lean.LevelMVarId → Lean.LevelMVarId → Bool
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_pow_two_le_of_one_lt : ∀ {M : Type u_2} [inst : LinearOrder M] [DenselyOrdered M] {x : M} [inst_2 : CommMonoid M] [ExistsMulOfLE M]
  [IsOrderedCancelMonoid M], 1 < x → ∃ y, 1 < y ∧ y ^ 2 ≤ x
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_lt_toNat : ∀ {c d : Cardinal.{u}}, c < d → d < Cardinal.aleph0 → Cardinal.toNat c < Cardinal.toNat d
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernsteinApproximation.congr_simp : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : Module ℝ E] [inst_4 : ContinuousSMul ℝ E] (n n_1 : ℕ),
  n = n_1 → ∀ (f f_1 : C(↑unitInterval, E)), f = f_1 → bernsteinApproximation n f = bernsteinApproximation n_1 f_1