mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.Process.Basic
/-- Two stochastic processes $(X_s)_{s \in S}$ and $(Y_t)_{t \in T}$ are independent if
for all $s_1, ..., s_p \in S$ and $t_1, ..., t_q \in T$ the two families
$(X_{s_1}, ..., X_{s_p})$ and $(Y_{t_1}, ..., Y_{t_q})$ are independent.  -/
ProbabilityTheory.IndepFun.process_indepFun_process : ∀ {S : Type u_1} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {T : Type u_4} {𝓧 : S → Type u_5}
  {𝓨 : T → Type u_6} [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : (j : T) → MeasurableSpace (𝓨 j)]
  {X : (i : S) → Ω → 𝓧 i} {Y : (j : T) → Ω → 𝓨 j},
  (∀ (i : S), Measurable (X i)) →
    (∀ (j : T), Measurable (Y j)) →
      (∀ (I : Finset S) (J : Finset T), ProbabilityTheory.IndepFun (fun ω i => X (↑i) ω) (fun ω j => Y (↑j) ω) P) →
        ∀ [MeasureTheory.IsZeroOrProbabilityMeasure P],
          ProbabilityTheory.IndepFun (fun ω i => X i ω) (fun ω j => Y j ω) P
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.hasCoeOpens.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.hasCoeOpens = { coe := OpenSubgroup.toOpens }
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instPartialOrder : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] → [StarOrderedRing A] → {n : Type u_3} → [Fintype n] → PartialOrder (CStarMatrix n n A)
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.isoMk_inv_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src)
  (e₂ : X.tgt ≅ Y.tgt)
  (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel),
  (CategoryTheory.Dial.isoMk e₁ e₂ eq).inv.F = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd e₂.hom
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.det_symm : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : M ≃ₗ[R] M),
  LinearEquiv.det f.symm = LinearEquiv.det f⁻¹
-- Mathlib.Data.Quot
Trunc.lift_mk : ∀ {α : Sort u_1} {β : Sort u_2} (f : α → β) (c : ∀ (a b : α), f a = f b) (a : α), Trunc.lift f c (Trunc.mk a) = f a
-- Mathlib.Data.DFinsupp.Module
DFinsupp.subtypeDomain_smul : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : (i : ι) → SMulZeroClass γ (β i)]
  {p : ι → Prop} [inst_2 : DecidablePred p] (r : γ) (f : Π₀ (i : ι), β i),
  DFinsupp.subtypeDomain p (r • f) = r • DFinsupp.subtypeDomain p f
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.freeVarFinset.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (_n l : ℕ)
  (_R : L.Relations l) (ts : Fin l → L.Term (α ⊕ Fin _n))
  (h_1 : (_n : ℕ) → motive _n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (_n : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_n l : ℕ) →
      (_R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.rel _R ts))
  (h_4 : (_n : ℕ) → (f₁ f₂ : L.BoundedFormula α _n) → motive _n (f₁.imp f₂))
  (h_5 : (_n : ℕ) → (f : L.BoundedFormula α (_n + 1)) → motive _n f.all),
  (match _n, FirstOrder.Language.BoundedFormula.rel _R ts with
    | _n, FirstOrder.Language.BoundedFormula.falsum => h_1 _n
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _n t₁ t₂
    | _n, FirstOrder.Language.BoundedFormula.rel _R ts => h_3 _n l _R ts
    | _n, f₁.imp f₂ => h_4 _n f₁ f₂
    | _n, f.all => h_5 _n f) =
    h_3 _n l _R ts
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The preimage of an affine subspace under an affine map as an affine subspace.  -/
AffineSubspace.comap : {k : Type u_1} →
  {V₁ : Type u_2} →
    {P₁ : Type u_3} →
      {V₂ : Type u_4} →
        {P₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : Module k V₁] →
                [inst_3 : AddTorsor V₁ P₁] →
                  [inst_4 : AddCommGroup V₂] →
                    [inst_5 : Module k V₂] →
                      [inst_6 : AddTorsor V₂ P₂] → (P₁ →ᵃ[k] P₂) → AffineSubspace k P₂ → AffineSubspace k P₁
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverTerms.next : ℕ → Lean.Expr → Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- An isomorphism between `PGL(n, F)` and `PSL(n, F)` in the case of an algebraically closed field
induced from the natural inclusion map where when `n` is empty it gives a junk isomorphism.  -/
Matrix.ProjectiveSpecialLinearGroup.isoPSLOfAlgClosed : {n : Type u_1} →
  [inst : Fintype n] →
    [inst_1 : DecidableEq n] →
      {F : Type u_3} →
        [inst_2 : Field F] → [IsAlgClosed F] → Matrix.ProjGenLinGroup n F ≃* Matrix.ProjectiveSpecialLinearGroup n F
-- Init.Data.Int.Linear
Int.Internal.Linear.Context : Type
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerve.instReflectiveTruncatedOfNatNatCatNerveFunctor₂ : CategoryTheory.Reflective CategoryTheory.Nerve.nerveFunctor₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.get!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.Equiv t₂ → t₁.get! k = t₂.get! k
-- Mathlib.Order.Bounded
Set.bounded_lt_inter_lt : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] [NoMaxOrder α] (a : α),
  Set.Bounded (fun x1 x2 => x1 < x2) (s ∩ {b | a < b}) ↔ Set.Bounded (fun x1 x2 => x1 < x2) s
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isPathConnected_eball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ENNReal},
  0 < r → IsPathConnected (Metric.eball x r)
-- Aesop.Tracing
Aesop.nodeProvedEmoji : String
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.end_apply_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R M) (ij : ι × ι) (k : ι),
  (b.end ij) (b k) = if ij.2 = k then b ij.1 else 0
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection is its own inverse.  -/
Submodule.reflection_inv : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K : Submodule 𝕜 E} [inst_3 : K.HasOrthogonalProjection], K.reflection⁻¹ = K.reflection
-- Init.Data.Int.DivMod.Lemmas
Int.ofNat_mod_ofNat : ∀ (m n : ℕ), ↑m % ↑n = ↑(m % n)
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.maximalIdeal.isMaximal : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : IsLocalRing R], (IsLocalRing.maximalIdeal R).IsMaximal
-- Mathlib.GroupTheory.Submonoid.Center
addUnitsCenterToCenterAddUnits_injective : ∀ (M : Type u_1) [inst : AddMonoid M], Function.Injective ⇑(addUnitsCenterToCenterAddUnits M)
-- Init.SimpLemmas
instIdempotentOpOr : Std.IdempotentOp Or
-- Mathlib.Algebra.Star.CentroidHom
/-- The canonical \*-homomorphism embedding the center of `CentroidHom α` into `CentroidHom α`.  -/
CentroidHom.centerStarEmbedding : {α : Type u_1} →
  [inst : NonUnitalNonAssocSemiring α] →
    [inst_1 : StarRing α] → ↥(Subsemiring.center (CentroidHom α)) →⋆ₙ+* CentroidHom α
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.analyticAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, ContDiffAt 𝕜 ⊤ f x → AnalyticAt 𝕜 f x
-- Mathlib.Data.Complex.Basic
Complex.I_pow_four : Complex.I ^ 4 = 1
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.coeFn_abs : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : Lattice E] [inst_2 : HasSolidNorm E] [inst_3 : IsOrderedAddMonoid E]
  (f : ↥(MeasureTheory.Lp E p μ)), ↑↑|f| =ᵐ[μ] fun x => |↑↑f x|
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.homEquiv_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM) {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf}
  (hcM' : CategoryTheory.Limits.IsColimit cM') {N : ModuleCat ↑cR.pt}
  (φ' : ModuleCat.of (↑cR.pt) (PresheafOfModules.ModuleColimit hcR hcM') ⟶ N) (f : M ⟶ M'),
  (PresheafOfModules.ModuleColimit.homEquiv hcR hcM)
      (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (PresheafOfModules.ModuleColimit.map hcR hcM hcM' f)) φ') =
    CategoryTheory.CategoryStruct.comp f ((PresheafOfModules.ModuleColimit.homEquiv hcR hcM') φ')
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instHasColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {K : Type z} [inst_2 : CategoryTheory.Category.{z', z} K]
  [CategoryTheory.HasWeakSheafify J D] [CategoryTheory.Limits.HasColimitsOfShape K D],
  CategoryTheory.Limits.HasColimitsOfShape K (CategoryTheory.Sheaf J D)
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.adjoin_rootSet : ∀ {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (f : Polynomial K)
  [Polynomial.IsSplittingField K L f], Algebra.adjoin K (f.rootSet L) = ⊤
-- Init.Data.Int.Linear
Int.Internal.Linear.OrOver_cases_type.eq_def : ∀ (n : ℕ) (p : ℕ → Prop),
  Int.Internal.Linear.OrOver_cases_type n p =
    match n with
    | 0 => p 0
    | n.succ => ¬p (n + 1) → Int.Internal.Linear.OrOver_cases_type n p
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_sumPiEquivProdPi : ∀ {ι : Type u_1} {ι' : Type u_2} [inst : Fintype ι] [inst_1 : Fintype ι'] {X : ι ⊕ ι' → Type u_4}
  {_m : (i : ι ⊕ ι') → MeasurableSpace (X i)} (μ : (i : ι ⊕ ι') → MeasureTheory.Measure (X i))
  [∀ (i : ι ⊕ ι'), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.sumPiEquivProdPi X)) (MeasureTheory.Measure.pi μ)
    ((MeasureTheory.Measure.pi fun i => μ (Sum.inl i)).prod (MeasureTheory.Measure.pi fun i => μ (Sum.inr i)))
-- Std.Time.Date.PlainDate
Std.Time.PlainDate.mk.injEq : ∀ (year : Std.Time.Year.Offset) (month : Std.Time.Month.Ordinal) (day : Std.Time.Day.Ordinal)
  (valid : year.Valid month day) (year_1 : Std.Time.Year.Offset) (month_1 : Std.Time.Month.Ordinal)
  (day_1 : Std.Time.Day.Ordinal) (valid_1 : year_1.Valid month_1 day_1),
  ({ year := year, month := month, day := day, valid := valid } =
      { year := year_1, month := month_1, day := day_1, valid := valid_1 }) =
    (year = year_1 ∧ month = month_1 ∧ day = day_1)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.exp_le_exp : ∀ {G : Type u_3} [inst : Preorder G] {a b : G}, WithZero.exp a ≤ WithZero.exp b ↔ a ≤ b
-- Mathlib.Analysis.Fourier.Notation
/-- A `FourierAdd` is a function space on which the Fourier transform is additive.  -/
FourierAdd : (E : Type u_5) → (F : outParam (Type u_6)) → [Add E] → [Add F] → [FourierTransform E F] → Prop
-- Batteries.Data.Stream
Std.Stream.take.eq_1 : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ), Std.Stream.take s 0 = ([], s)
-- Mathlib.CategoryTheory.Comma.Arrow
/-- The right object of an arrow.  -/
CategoryTheory.Arrow.right : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → CategoryTheory.Arrow T → T
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.toBasis_map : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {G : Type u_7} [inst_4 : NormedAddCommGroup G]
  [inst_5 : InnerProductSpace 𝕜 G] (b : OrthonormalBasis ι 𝕜 E) (L : E ≃ₗᵢ[𝕜] G),
  (b.map L).toBasis = b.toBasis.map L.toLinearEquiv
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.isIso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f] [CategoryTheory.Epi f.base],
  CategoryTheory.IsIso f
-- Mathlib.Algebra.AddConstMap.Basic
/-- Pointwise scalar multiplication of `f : G →+c[a, b] H` as a map `G →+c[a, c • b] H`.  -/
AddConstMap.smul : {G : Type u_1} →
  {H : Type u_2} →
    {K : Type u_3} →
      [inst : Add G] →
        [inst_1 : AddZeroClass H] →
          {a : G} → {b : H} → [inst_2 : DistribSMul K H] → (c : K) → AddConstMap G H a b → AddConstMap G H a (c • b)
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.smul_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) (a : M), f • a = f a
-- Mathlib.Topology.Connected.PathConnected
/-- If `x` and `y` are joined in the set `F`, then they are joined in the subtype `F`.  -/
JoinedIn.joined_subtype : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X} (h : JoinedIn F x y), Joined ⟨x, ⋯⟩ ⟨y, ⋯⟩
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.ext_iff : ∀ {V : Type u_1} {M : Type u_2} {inst : SMul M V} {S : Type u_3} {_ι : S → M} {x y : Quiver.SchreierGraph V _ι},
  x = y ↔ x.toVertex = y.toVertex
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_3} {init : α} {x : β} {xs : List β} [inst : Monad m]
  [LawfulMonad m] {f : α → β → m α},
  List.scanAuxM✝ f init (x :: xs) = do
    let __do_lift ← f init x
    let __do_lift ← List.scanAuxM✝ f __do_lift xs
    pure (__do_lift ++ [init])
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.embedding_mem_mixedEmbeddingsOver : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  {v : NumberField.InfinitePlace K},
  ∀ w ∈ NumberField.InfinitePlace.ramifiedPlacesOver L v,
    w.embedding ∈ NumberField.ComplexEmbedding.mixedEmbeddingsOver L v.embedding
-- Aesop.EMap
Aesop.EMap.alter : {α β : Type} → Lean.Expr → (α → Option α × β) → Aesop.EMap α → Lean.MetaM (Aesop.EMap α × Option β)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {he : t.isEmpty = false}, t.getKey! (t.minKey he) = t.minKey he
-- Mathlib.Algebra.Category.MonCat.Shrink
MonCat.shrinkFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C MonCat)
  [inst_1 : ∀ (X : C), Small.{w, w'} ↑(F.obj X)] {X Y : C} (f : X ⟶ Y),
  (MonCat.shrinkFunctor.{w, w', v, u} F).map f =
    MonCat.ofHom ((Shrink.mulEquiv.symm.toMonoidHom.comp (MonCat.Hom.hom (F.map f))).comp Shrink.mulEquiv.toMonoidHom)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- The map from an object to the terminal object.  -/
CategoryTheory.Limits.terminal.from : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → [inst_1 : CategoryTheory.Limits.HasTerminal C] → (P : C) → P ⟶ ⊤_ C
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonSnippetString : Lean.ToJson Lean.Lsp.SnippetString
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_of_lt_of_le : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero α] [inst_4 : Zero β] [PosSMulMono α β] [SMulPosStrictMono α β],
  a₁ < a₂ → b₁ ≤ b₂ → 0 ≤ a₁ → 0 < b₂ → a₁ • b₁ < a₂ • b₂
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.vcgenDischargeTactic : Lean.ParserDescr
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_setWidth_add : ∀ {w k i : ℕ} {x : BitVec w}, k ≤ i → (BitVec.setWidth (w + k) x).getMsbD i = x.getMsbD (i - k)
-- Mathlib.GroupTheory.Submonoid.Inverses
/-- The function from `S.leftInv` to `S` sending an element to its right inverse in `S`.
This is a `MonoidHom` when `M` is commutative.  -/
Submonoid.fromLeftInv : {M : Type u_1} → [inst : Monoid M] → (S : Submonoid M) → ↥S.leftInv → ↥S
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.endofunctorMonoidalCategory.evaluationRightAction_actionAssocIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (d : C) (c c' : CategoryTheory.Functor C C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c c' =
    ((CategoryTheory.Functor.Monoidal.μIso (CategoryTheory.Functor.id (CategoryTheory.Functor C C)) c c').app d).symm
-- Mathlib.Data.Holor
Holor.cprankMax_add : ∀ {α : Type} {ds : List ℕ} [inst : Mul α] [inst_1 : AddMonoid α] {m n : ℕ} {x y : Holor α ds},
  Holor.CPRankMax m x → Holor.CPRankMax n y → Holor.CPRankMax (m + n) (x + y)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
Std.Iter.Intermediate.zip_surj : ∀ {α₁ α₂ β₁ β₂ : Type w} [inst : Std.Iterator α₁ Id β₁] (it : Std.Iter (β₁ × β₂)),
  ∃ it₁ memo it₂, it = Std.Iter.Intermediate.zip it₁ memo it₂
-- Std.Async.Select
/-- Try to atomically finish the `Waiter`. If the race for finishing it is won, `win` is executed
with the internal `IO.Promise` of the `Waiter`. This promise must under all circumstances be
resolved by `win`. If the race is lost some cleanup work can be done in `lose`.
 -/
Std.Async.Waiter.race : {m : Type → Type} →
  {α β : Type} →
    [Monad m] →
      [MonadLiftT (ST IO.RealWorld) m] → Std.Async.Waiter α → m β → (IO.Promise (Except IO.Error α) → m β) → m β
-- Mathlib.GroupTheory.Torsion
/-- Torsion submonoids of a torsion submonoid are isomorphic to the submonoid.  -/
CommMonoid.Torsion.ofTorsion : (G : Type u_1) → [inst : CommMonoid G] → ↥(CommMonoid.torsion ↥(CommMonoid.torsion G)) ≃* ↥(CommMonoid.torsion G)
-- Mathlib.Data.Bool.Basic
/-- convert a `ℕ` to a `Bool`, `0 -> false`, everything else -> `true`  -/
Bool.ofNat : ℕ → Bool
-- Mathlib.Topology.Convenient.HomSpace
Topology.ContinuousMapGeneratedBy.curryEquiv_apply_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] {T : Type v''} [inst_3 : TopologicalSpace T]
  [inst_4 : ∀ (i : ι), LocallyCompactSpace (X i)] [inst_5 : ∀ (i j : ι), Topology.IsGeneratedBy X (X i × X j)]
  (g : Topology.ContinuousMapGeneratedBy X (Y × Z) T) (y : Y) (z : Z),
  ((Topology.ContinuousMapGeneratedBy.curryEquiv g) z) y = g (y, z)
-- Mathlib.Data.Rel
SetRel.isSymm_empty : ∀ {α : Type u_1}, ∅.IsSymm
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
CategoryTheory.GradedObject.mapBifunctorMap_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {I : Type u_4} {J : Type u_5} {K : Type u_6}
  (p : I × J → K)
  [inst_3 :
    ∀ (X : CategoryTheory.GradedObject I C₁) (Y : CategoryTheory.GradedObject J C₂),
      (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p]
  (X : CategoryTheory.GradedObject I C₁) {X_1 Y : CategoryTheory.GradedObject J C₂} (ψ : X_1 ⟶ Y) (i : K),
  ((CategoryTheory.GradedObject.mapBifunctorMap F p).obj X).map ψ i =
    CategoryTheory.GradedObject.mapBifunctorMapMap F p (CategoryTheory.CategoryStruct.id X) ψ i
-- Init.Data.Int.Gcd
Int.gcd_mul_left_add_left : ∀ (m n k : ℤ), (m * k + n).gcd m = n.gcd m
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.linearization_obj_V : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G] (X : Action (Type w) G),
  ↑((Rep.linearization k G).obj X) = MonoidAlgebra k X.V
-- Mathlib.Analysis.Analytic.Within
/-- If `f` is `AnalyticOn` near each point in a set, it is `AnalyticOn` the set  -/
analyticOn_of_locally_analyticOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E},
  (∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)) → AnalyticOn 𝕜 f s
-- Aesop.Search.Expansion
_private.Aesop.Search.Expansion.0.Aesop.withRuleTraceNode.fmt : {Q : Type} →
  [inst : Aesop.Queue Q] →
    {α : Type} → Aesop.RuleName → (α → String) → String → Except Lean.Exception α → Aesop.SearchM Q Lean.MessageData
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalSleep : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Group.Submonoid.Units
ofUnits_units_gci.eq_1 : ∀ {M : Type u_1} [inst : Monoid M], ofUnits_units_gci = GaloisCoinsertion.monotoneIntro ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.Normed.Group.Continuity
Inseparable.norm_eq_norm : ∀ {E : Type u_4} [inst : SeminormedAddGroup E] {u v : E}, Inseparable u v → ‖u‖ = ‖v‖
-- Init.Data.Int.Order
Int.sub_lt_sub_left_iff : ∀ {a b c : ℤ}, c - a < c - b ↔ b < a
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_pow_of_log_lt : ∀ {x y : ℝ} {n : ℕ}, 0 < y → Real.log x < ↑n * Real.log y → x < y ^ n
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.Lifting.compRight_iso : ∀ {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) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E] {E' : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_4, u_4} E'] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_4 : CategoryTheory.Localization.Lifting L W F F'] (G : CategoryTheory.Functor E E'),
  CategoryTheory.Localization.Lifting.iso L W (F.comp G) (F'.comp G) =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Localization.Lifting.iso L W F F') G
-- Mathlib.Topology.UniformSpace.Defs
mem_nhds_right : ∀ {α : Type ua} [inst : UniformSpace α] (y : α) {s : SetRel α α}, s ∈ uniformity α → {x | (x, y) ∈ s} ∈ nhds y
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.le_comap_of_map_le : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F},
  AddSubmonoid.map f S ≤ T → S ≤ AddSubmonoid.comap f T
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.foldrM_eq_foldrM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.ExtTreeMap.foldrM f init t = List.foldrM (fun a b => f a.1 a.2 b) init t.toList
-- Mathlib.Order.BooleanAlgebra.Basic
compl_inj_iff : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], xᶜ = yᶜ ↔ x = y