mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.isTotallyComplex : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [NumberField.IsCMField K], NumberField.IsTotallyComplex K
-- Mathlib.Probability.Process.Adapted
/-- The norm of a strongly adapted process is strongly adapted.  -/
MeasureTheory.StronglyAdapted.norm : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_4} {u : (i : ι) → Ω → β i} [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)],
  MeasureTheory.StronglyAdapted f u → MeasureTheory.StronglyAdapted f fun t ω => ‖u t ω‖
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α)
  (target : Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget aig w) (lhs : BitVec w) (rhs : BitVec target.n)
  (assign : α → Bool),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := target.lhs.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < target.n), ⟦assign, { aig := aig, ref := target.rhs.get idx hidx }⟧ = rhs.getLsbD idx) →
      ∀ (idx : ℕ) (hidx : idx < w),
        ⟦assign,
            { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift aig target).aig,
              ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift aig target).vec.get idx hidx }⟧ =
          (lhs >>> (rhs &&& BitVec.twoPow target.n target.pow)).getLsbD idx
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE'.homologyData.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i j k : ι) (hk : c.next j = k) {j' : ι'} (hj' : e.f j = j') (hj : e.BoundaryGE j),
  HomologicalComplex.truncGE'.homologyData K e i j k hk hj' hj =
    CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork ((K.truncGE' e).sc' i j k) ⋯
      (CategoryTheory.Limits.KernelFork.ofι
        (CategoryTheory.CategoryStruct.comp (K.homologyι j') (K.truncGE'XIsoOpcycles e hj' hj).inv) ⋯)
      (HomologicalComplex.truncGE'.isLimitKernelFork K e j k hk hj' hj)
-- Mathlib.Analysis.Normed.Lp.lpHolder
Memℓp.holder_top_right_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)] {p : 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 ≤ D →
        (∀ (s : Finset ι), ∑ i ∈ s, ‖e i‖ ^ p.toReal ≤ C) →
          (∀ (i : ι), ‖f i‖ ≤ D) → ∀ (s : Finset ι), ∑ i ∈ s, ‖((B i) (e i)) (f i)‖ ^ p.toReal ≤ (K * D) ^ p.toReal * C
-- Mathlib.Algebra.Group.End
/-- The group of additive automorphisms.  -/
AddAut : (M : Type u_7) → [Add M] → Type u_7
-- Lean.Parser
Lean.PrettyPrinter.Formatter.numLit.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.mkOfLT : Lean.Meta.Grind.Arith.Cutsat.ToIntM (Option Lean.Expr × Option Lean.Expr)
-- Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
AlgebraicClosure.hasEnoughRootsOfUnity : ∀ (F : Type u_1) [inst : Field F] (n : ℕ) [NeZero ↑n], HasEnoughRootsOfUnity (AlgebraicClosure F) n
-- Mathlib.RingTheory.HopkinsLevitzki
/-- [Stacks Tag 00JB](https://stacks.math.columbia.edu/tag/00JB) (A ring is Artinian if and only if it has finite length as a module over itself.
**Any such ring is both Artinian and Noetherian.**) -/
instIsNoetherianRingOfIsArtinianRing : ∀ (R : Type u_2) [inst : Ring R] [IsArtinianRing R], IsNoetherianRing R
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- The action of the permutation group of `α` on `α` is preprimitive  -/
Equiv.Perm.instIsPreprimitive : ∀ {α : Type u_1}, MulAction.IsPreprimitive (Equiv.Perm α) α
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
List.Nat.antidiagonalTuple.eq_2 : ∀ (n : ℕ), List.Nat.antidiagonalTuple 0 n.succ = []
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.add.injEq : ∀ (a b a_1 b_1 : Lean.Grind.CommRing.Expr), (a.add b = a_1.add b_1) = (a = a_1 ∧ b = b_1)
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.empty_ne_coe : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), ∅ ≠ ↑I
-- Mathlib.CategoryTheory.Action.Basic
Action.hom_ext : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (φ₁ φ₂ : M ⟶ N), φ₁.hom = φ₂.hom → φ₁ = φ₂
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_C : ∀ {R : Type u} {σ : Type u_1} {r : R} [inst : CommSemiring R], (MvPolynomial.C r).vars = ∅
-- Mathlib.LinearAlgebra.Orientation
Orientation.map.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  (ι : Type u_4) (e : M ≃ₗ[R] N), Orientation.map ι e = Module.Ray.map (AlternatingMap.domLCongr R R ι R e)
-- Mathlib.Algebra.GroupWithZero.Basic
eq_zero_of_pow_eq_zero : ∀ {R : Type u_3} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ] [IsReduced R] {n : ℕ}, x ^ n = 0 → x = 0
-- Lean.Data.SMap
Lean.SMap.findD : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → α → β → β
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.BisimO.match_1.eq_1 : ∀ {α : Type u_1} (motive : α ⊕ Computation α → α ⊕ Computation α → Sort u_2) (a a' : α)
  (h_1 : (a a' : α) → motive (Sum.inl a) (Sum.inl a')) (h_2 : (s s' : Computation α) → motive (Sum.inr s) (Sum.inr s'))
  (h_3 : (x x_1 : α ⊕ Computation α) → motive x x_1),
  (match Sum.inl a, Sum.inl a' with
    | Sum.inl a, Sum.inl a' => h_1 a a'
    | Sum.inr s, Sum.inr s' => h_2 s s'
    | x, x_1 => h_3 x x_1) =
    h_1 a a'
-- Mathlib.AlgebraicGeometry.Stalk
/-- **Alias** of `AlgebraicGeometry.Spec.fromSpecStalk_eq'`.

---

A variant of `Spec.fromSpecStalk_eq` that breaks abstraction boundaries.  -/
AlgebraicGeometry.Scheme.Spec_fromSpecStalk' : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)),
  (AlgebraicGeometry.Spec R).fromSpecStalk x =
    AlgebraicGeometry.Spec.map (AlgebraicGeometry.StructureSheaf.toStalk (↑R) x)
-- Mathlib.Data.List.Sigma
/-- `lookup_all a l` is the list of all values in `l` corresponding to the key `a`.  -/
List.lookupAll : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → List (Sigma β) → List (β a)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.ext_iff_natDegree_le : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} {n : ℕ},
  p.natDegree ≤ n → q.natDegree ≤ n → (p = q ↔ ∀ i ≤ n, p.coeff i = q.coeff i)
-- Mathlib.Topology.MetricSpace.Bounded
totallyBounded_Ioo : ∀ {α : Type u} [inst : UniformSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (a b : α), TotallyBounded (Set.Ioo a b)
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.image_isFinite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) [G.IsFinite] {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F'),
  (G.image f).IsFinite
-- Mathlib.Algebra.Free
Magma.AssocQuotient.instInhabited : {α : Type u} → [inst : Mul α] → [Inhabited α] → Inhabited (Magma.AssocQuotient α)
-- Lean.LoadDynlib
/-- Runs a module initializer function.
The symbol should have the signature `(builtin : Bool) → IO Unit`
(e.g., `initialize_Foo(uint8_t builtin)`).

This function is unsafe because there is no guarantee the symbol has the
expected signature. An invalid symbol can thus produce undefined behavior.
Furthermore, if the initializer introduces pointers (e.g., function closures)
from the dynamic library into the global state, future garbage collection of
the library will produce undefined behavior. In such cases, garbage collection
of the dynamic library can be prevented via `Runtime.markPersistent` or
`Runtime.forget`.
 -/
Lean.Dynlib.Symbol.runAsInit : {dynlib : Lean.Dynlib} → dynlib.Symbol → IO Unit
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.naturality_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f : M₁ ⟶ M₂) {X Y : Cᵒᵖ} (g : X ⟶ Y) (x : ↑(M₁.obj X)),
  (CategoryTheory.ConcreteCategory.hom (f.app Y)) ((CategoryTheory.ConcreteCategory.hom (M₁.map g)) x) =
    (CategoryTheory.ConcreteCategory.hom (M₂.map g)) ((CategoryTheory.ConcreteCategory.hom (f.app X)) x)
-- Mathlib.Order.CompleteLattice.Basic
iSup_apply : ∀ {α : Type u_8} {β : α → Type u_9} {ι : Sort u_10} [inst : (i : α) → SupSet (β i)] {f : ι → (a : α) → β a} {a : α},
  (⨆ i, f i) a = ⨆ i, f i a
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_le_expGrowthSup_of_frequently_le : ∀ {u v : ℕ → ENNReal}, (∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ v n) → ExpGrowth.expGrowthInf u ≤ ExpGrowth.expGrowthSup v
-- Init.Data.Array.DecidableEq
_private.Init.Data.Array.DecidableEq.0.Array.isEqvAux.match_1.eq_2 : ∀ {α : Type u_1} (xs : Array α) (motive : (x : ℕ) → x ≤ xs.size → Sort u_2) (i : ℕ) (h : i + 1 ≤ xs.size)
  (h_1 : (x : 0 ≤ xs.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ xs.size) → motive i.succ h),
  (match i.succ, h with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_2 i h
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- Each chart of a charted space is a structomorphism between its source and target.  -/
OpenPartialHomeomorph.toStructomorph : {H : Type u} →
  {M : Type u_2} →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : ChartedSpace H M] →
          {G : StructureGroupoid H} →
            {e : OpenPartialHomeomorph M H} →
              e ∈ atlas H M →
                [HasGroupoid M G] →
                  [ClosedUnderRestriction G] →
                    have s := { carrier := e.source, is_open' := ⋯ };
                    have t := { carrier := e.target, is_open' := ⋯ };
                    Structomorph G ↥s ↥t
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono_fun_enorm' : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε] {f : ℝ → ε} {g : ℝ → ENNReal},
  IntervalIntegrable g μ a b →
    MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)) →
      (fun x => ‖f x‖ₑ) ≤ᵐ[μ.restrict (Set.uIoc a b)] g → IntervalIntegrable f μ a b
-- Init.PropLemmas
right_iff_dite_iff : ∀ {p : Prop} [inst : Decidable p] {x : p → Prop} {y : Prop}, (y ↔ if h : p then x h else y) ↔ ∀ (h : p), y ↔ x h
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.step.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (motive : Std.DTreeMap.Internal.RxcIterator α β → Sort u_3)
  (upper : α) (h_1 : (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper })
  (h_2 :
    (k : α) →
      (v : β k) →
        (t : Std.DTreeMap.Internal.Impl α β) →
          (it : Std.DTreeMap.Internal.Zipper α β) →
            (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }),
  (match { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper } with
    | { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper } => h_1 upper
    | { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper } => h_2 k v t it upper) =
    h_1 upper
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {a : α}, a ∉ t → t[a]! = default
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₀_prev : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r r' : ℤ) (pq pq' : κ),
  (c r).Rel pq pq' →
    ∀ (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_41)
      (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_43),
      self.i₀ r' pq ⋯ = self.i₁ pq'
-- Mathlib.Tactic.DepRewrite
/-- `rewrite!` is like `rewrite`,
but can also insert casts to adjust types that depend on the LHS of a rewrite.
It is available as an ordinary tactic and a `conv` tactic.

The sort of casts that are inserted is controlled by the `castMode` configuration option.
By default, only proof terms are casted;
by proof irrelevance, this adds no observable complexity.

With `rewrite! +letAbs (castMode := .all)`, casts are inserted whenever necessary.
This means that the 'motive is not type correct' error never occurs,
at the expense of creating potentially complicated terms.
 -/
Mathlib.Tactic.DepRewrite.evalDepRewriteSeq : Lean.Elab.Tactic.Tactic
-- Mathlib.RingTheory.Ideal.Maps
Submodule.restrictScalars_map_smul_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} {M : Type u_4} [inst_1 : CommSemiring S] [inst_2 : Algebra S R]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower S R M] (I : Ideal S)
  (N : Submodule R M),
  Submodule.restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • Submodule.restrictScalars S N
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.skipWhile_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos}, pos.skipWhile pat = ((pos.cast hst).skipWhile pat).cast ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableAt_intCast : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IntCast F] (z : ℤ) (x : E), DifferentiableAt 𝕜 (↑z) x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.pairing_apply_apply : ∀ {𝕜 : Type u_2} {D : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F]
  [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedAddCommGroup D]
  [inst_7 : NormedSpace ℝ D] [inst_8 : NormedAddCommGroup G] [inst_9 : NormedSpace ℝ G] [inst_10 : NormedSpace 𝕜 F]
  [inst_11 : NormedSpace 𝕜 E] [inst_12 : NormedSpace 𝕜 G] (B : E →L[𝕜] F →L[𝕜] G) (f : SchwartzMap D E)
  (g : SchwartzMap D F) (x : D), (((SchwartzMap.pairing B) f) g) x = (B (f x)) (g x)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.eq_swap_of_apply_apply_eq_self : ∀ {α : Type u_4} [inst : DecidableEq α] {f : Equiv.Perm α},
  f.IsCycle → ∀ {x : α}, f x ≠ x → f (f x) = x → f = Equiv.swap x (f x)
-- Init.Grind.Ring.Field
Lean.Grind.Field.inv_mul : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a b : α), (a * b)⁻¹ = a⁻¹ * b⁻¹
-- Mathlib.Analysis.Calculus.ContDiff.RestrictScalars
/-- Derivation rule for compositions of scalar restriction with continuous multilinear maps.  -/
fderivWithin_restrictScalars_comp : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {x : E} {n : ℕ} {s : Set E}
  {φ : E → E [×n]→L[𝕜'] F},
  DifferentiableWithinAt 𝕜' φ s x →
    UniqueDiffWithinAt 𝕜 s x →
      ⇑(fderivWithin 𝕜 (ContinuousMultilinearMap.restrictScalars 𝕜 ∘ φ) s x) =
        ContinuousMultilinearMap.restrictScalars 𝕜 ∘ ⇑(ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' φ s x))
-- Lean.Parser.Term
Lean.Parser.Term.noindex : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.leftAdjointMate_comp_evaluation_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y] (f : X ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (ᘁf))
      (CategoryTheory.CategoryStruct.comp (ε_ (ᘁX) X) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f ᘁY)
      (CategoryTheory.CategoryStruct.comp (ε_ (ᘁY) Y) h)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.monMonoidal.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Mon.monMonoidal =
    { toMonoidalCategoryStruct := CategoryTheory.Mon.monMonoidalStruct, tensorHom_def := ⋯, id_tensorHom_id := ⋯,
      tensorHom_comp_tensorHom := ⋯, whiskerLeft_id := ⋯, id_whiskerRight := ⋯, associator_naturality := ⋯,
      leftUnitor_naturality := ⋯, rightUnitor_naturality := ⋯, pentagon := ⋯, triangle := ⋯ }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.ring : {R : Type u_1} →
  [inst : Ring R] →
    {M : Type u_4} →
      [inst_1 : TopologicalSpace M] →
        [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [IsTopologicalAddGroup M] → Ring (M →L[R] M)
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.hom_sub : ∀ {M N : AddCommGrpCat} (f g : M ⟶ N), AddCommGrpCat.Hom.hom (f - g) = AddCommGrpCat.Hom.hom f - AddCommGrpCat.Hom.hom g
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sInf_zero : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : Zero M], sInf 0 = 0
-- Init.Data.List.Count
List.count_singleton_self : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α}, List.count a [a] = 1
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.instIteratorLoopIdSearchStep : {ρ : Type} →
  (pat : ρ) →
    {s : String.Slice} →
      [inst : String.Slice.Pattern.BackwardPattern pat] →
        Std.IteratorLoop (String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher pat s) Id Id
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Generalized pattern information. See `Grind.genPattern` gadget.  -/
Lean.Meta.Grind.GenPatternInfo : Type
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
HomologicalComplex.g_shortComplexTruncLEX₃ToTruncGE : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C] [inst_1 : CategoryTheory.Abelian C]
  (K : HomologicalComplex C c) {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} [inst_2 : e₁.IsTruncLE]
  [inst_3 : e₂.IsTruncGE] (ac : e₁.AreComplementary e₂),
  CategoryTheory.CategoryStruct.comp (K.shortComplexTruncLE e₁).g (K.shortComplexTruncLEX₃ToTruncGE ac) = K.πTruncGE e₂
-- Mathlib.Data.Sigma.Basic
Sigma.map_mk : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} (f₁ : α₁ → α₂)
  (f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)) (x : α₁) (y : β₁ x), Sigma.map f₁ f₂ ⟨x, y⟩ = ⟨f₁ x, f₂ x y⟩
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.setIntegral_traj_partialTraj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] {a b : ℕ},
  a ≤ b →
    ∀ {x₀ : (i : ↥(Finset.Iic a)) → X ↑i} {f : ((n : ℕ) → X n) → E},
      MeasureTheory.Integrable f ((ProbabilityTheory.Kernel.traj κ a) x₀) →
        ∀ {A : Set ((i : ↥(Finset.Iic b)) → X ↑i)},
          MeasurableSet A →
            ∫ (x : (i : ↥(Finset.Iic b)) → X ↑i) in A,
                ∫ (y : (n : ℕ) → X n),
                  f y ∂(ProbabilityTheory.Kernel.traj κ b) x ∂(ProbabilityTheory.Kernel.partialTraj κ a b) x₀ =
              ∫ (y : (n : ℕ) → X n) in Preorder.frestrictLe b ⁻¹' A, f y ∂(ProbabilityTheory.Kernel.traj κ a) x₀
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toPseudofunctor_map : ∀ {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] (F : CategoryTheory.Functor C D)
  {X Y : CategoryTheory.LocallyDiscrete C} (x : X ⟶ Y),
  F.toPseudofunctor.map x =
    match x with
    | { as := f } => (F.map f).toLoc
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
/-- Auxiliary definition for `commGrpEquivalence`.  -/
CategoryTheory.Preadditive.commGrpEquivalenceAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] →
        [inst_3 : CategoryTheory.BraidedCategory C] →
          (CategoryTheory.CommGrp.forget C).comp (CategoryTheory.Preadditive.toCommGrp C) ≅
            CategoryTheory.Functor.id (CategoryTheory.CommGrp C)
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
/-- Version of the set of candidates in bounded_continuous_functions, to apply Arzela-Ascoli.  -/
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.candidatesB : (X : Type u) → (Y : Type v) → [inst : MetricSpace X] → [inst_1 : MetricSpace Y] → Set (GromovHausdorff.Cb✝ X Y)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {fallback v : β},
  (m.insertIfNew k v).getD a fallback = if (k == a) = true ∧ k ∉ m then v else m.getD a fallback
-- Mathlib.Data.Real.ConjExponents
/-- Real numbers `p q : ℝ` are **Hölder conjugate** if they are positive and satisfy the
equality `p⁻¹ + q⁻¹ = 1`. This is an abbreviation for `Real.HolderTriple p q 1`. This condition
shows up in many theorems in analysis, notably related to `L^p` norms.

It is equivalent that `1 < p` and `p⁻¹ + q⁻¹ = 1`. See `Real.holderConjugate_iff`.  -/
Real.HolderConjugate : ℝ → ℝ → Prop
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.add_eq_of_eq_eq : ∀ {A : Type u_2} [sA : CommSemiring A] {a₁ a₂ b₁ b₂ : A}, a₁ = b₁ → a₂ = b₂ → a₁ + a₂ = b₁ + b₂
-- Init.Data.Ord.Basic
Ordering.ofNat : ℕ → Ordering
-- Init.Data.Int.Lemmas
Int.neg_ofNat_eq_negSucc_iff : ∀ {a b : ℕ}, -↑a = Int.negSucc b ↔ a = b + 1
-- Mathlib.Order.RelIso.Basic
RelEmbedding.instEmbeddingLike : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop}, EmbeddingLike (r ↪r s) α β
-- Mathlib.Algebra.Order.Sub.Basic
/-- The `Sub` structure using choice satisfies `OrderedSub`.  -/
CanonicallyOrderedAdd.toOrderedSub : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : CanonicallyOrderedAdd α]
  [AddRightReflectLE α], OrderedSub α
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_neg : ∀ {x : ℝ*}, (-x).InfinitePos ↔ x.InfiniteNeg
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.p.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A A], P.p = CategoryTheory.Limits.prod.lift P.p₀ P.p₁