mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Moments.ComplexMGF
/-- For all `z : ℂ` with `z.re ∈ interior (integrableExpSet X μ)`,
`complexMGF X μ` is differentiable at `z` with derivative `μ[X * exp (z * X)]`.  -/
ProbabilityTheory.hasDerivAt_complexMGF : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    HasDerivAt (ProbabilityTheory.complexMGF X μ) (∫ (x : Ω), (fun ω => ↑(X ω) * Complex.exp (z * ↑(X ω))) x ∂μ) z
-- Mathlib.Algebra.Group.Units.Basic
add_ne_zero' : ∀ {α : Type u} [inst : AddCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b ≠ 0 ↔ a ≠ 0 ∨ b ≠ 0
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.toNonneg_of_nonneg : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : SemilatticeSup α] {a : α} (h : 0 ≤ a), Nonneg.toNonneg a = ⟨a, h⟩
-- Std.Data.TreeMap.Basic
Std.TreeMap.instSingletonProd : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Singleton (α × β) (Std.TreeMap α β cmp)
-- Mathlib.Topology.LocallyFinsupp
LocallyFiniteSupport.iff_locallyFinite_support : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : Zero Y] (f : X → Y),
  (LocallyFinite fun s => {↑s}) ↔ LocallyFiniteSupport f
-- Mathlib.ModelTheory.Syntax
/-- Maps a sentence's symbols along a language equivalence.  -/
FirstOrder.Language.LEquiv.onSentence : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L ≃ᴸ L') → L.Sentence ≃ L'.Sentence
-- Lean.LocalContext
Lean.LocalDecl.setIndex : Lean.LocalDecl → ℕ → Lean.LocalDecl
-- Mathlib.Algebra.Order.SuccPred.TypeTags
Order.succ_toMul : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : SuccOrder X] (x : Additive X),
  Order.succ (Additive.toMul x) = Additive.toMul (Order.succ x)
-- Mathlib.Data.ZMod.IntUnitsPower
one_uzpow : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (x : R), 1 ^ x = 1
-- Mathlib.Order.Category.PartOrdEmb
/-- The equivalence between `PartOrdEmb` and itself induced by `OrderDual` both ways.  -/
PartOrdEmb.dualEquiv : PartOrdEmb ≌ PartOrdEmb
-- Mathlib.Data.FunLike.Basic
DFunLike.dite_apply : ∀ {F : Sort u_1} {α : Sort u_2} {β : Sort u_3} [i : FunLike F α β] {P : Prop} [inst : Decidable P] (f : P → F)
  (g : ¬P → F) (x : α), (if h : P then f h else g h) x = if h : P then (f h) x else (g h) x
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.δ_μ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (i j : M)
  (X : C) [inst_3 : F.Monoidal],
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F i j).app X)
      ((CategoryTheory.Functor.LaxMonoidal.μ F i j).app X) =
    CategoryTheory.CategoryStruct.id ((F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj i j)).obj X)
-- Mathlib.Algebra.Free
FreeSemigroup.tail_mul : ∀ {α : Type u} (x y : FreeSemigroup α), (x * y).tail = x.tail ++ y.head :: y.tail
-- Mathlib.SetTheory.Cardinal.Continuum
/-- Cardinality of the continuum.  -/
Cardinal.continuum : Cardinal.{u}
-- Mathlib.Order.JordanHolder
JordanHolderLattice.iso_refl : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {x : X × X}, JordanHolderLattice.Iso x x
-- Mathlib.Algebra.Lie.TraceForm
LieIdeal.mem_killingCompl : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  {x : L}, x ∈ LieIdeal.killingCompl R L I ↔ ∀ y ∈ I, ((killingForm R L) y) x = 0
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.mk.sizeOf_spec : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W]
  [inst_2 : SizeOf V] [inst_3 : SizeOf W] (toFun : V → W)
  (map_add' : ∀ (v₁ v₂ : V), toFun (v₁ + v₂) = toFun v₁ + toFun v₂) (bound' : ∃ C, ∀ (v : V), ‖toFun v‖ ≤ C * ‖v‖),
  sizeOf { toFun := toFun, map_add' := map_add', bound' := bound' } = 1 + sizeOf bound'
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.isExtTangentAt_center_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P},
  s₁.IsExtTangentAt s₂ s₁.center ↔ s₁.radius = 0 ∧ s₁.center ∈ s₂
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.indep_iff_forall_indepSet : ∀ {Ω : Type u_1} {m₁ m₂ _mΩ : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.Indep m₁ m₂ μ ↔
    ∀ (s t : Set Ω), MeasurableSet s → MeasurableSet t → ProbabilityTheory.IndepSet s t μ
-- Mathlib.Tactic.DefEqTransformations
/-- Like `Mathlib.Tactic.runDefEqTactic` but for `conv` mode.  -/
Mathlib.Tactic.runDefEqConvTactic : (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.unop.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : Mul α] [inst_1 : Mul β], MulEquiv.unop = MulEquiv.op.symm
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- Flattening nested binary convex combination into a single convex combination.  -/
Convexity.convexCombPair_convexCombPair_left_eq_sConvexComb : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s')
  (ht' : 0 ≤ t') (h' : s' + t' = 1) (m₁ m₂ m₃ : M),
  Convexity.convexCombPair s t hs ht h (Convexity.convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ =
    Convexity.sConvexComb
      (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.duple m₁ m₂ hs' ht' h')
        (Convexity.StdSimplex.single m₃))
-- Mathlib.Data.Fin.VecNotation
/-- `![...]` notation is used to construct a vector `Fin n → α` using `Matrix.vecEmpty` and
`Matrix.vecCons`.

For instance, `![a, b, c] : Fin 3` is syntax for `vecCons a (vecCons b (vecCons c vecEmpty))`.

Note that this should not be used as syntax for `Matrix` as it generates a term with the wrong type.
The `!![a, b; c, d]` syntax (provided by `Matrix.matrixNotation`) should be used instead.
 -/
Matrix.vecNotation : Lean.ParserDescr
-- Mathlib.Geometry.Manifold.DerivationBundle
PointedContMDiffMap.instInhabitedSomeENatTop : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → {x : M} → Inhabited (PointedContMDiffMap 𝕜 I M (↑⊤) x)
-- Mathlib.Topology.Order.OrderClosed
Ioo_mem_nhdsGE_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b c : α},
  b ∈ Set.Ioo c a → Set.Ioo c a ∈ nhdsWithin b (Set.Ici b)
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
IsZGroup.of_injective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'} [hG' : IsZGroup G'],
  Function.Injective ⇑f → IsZGroup G
-- Mathlib.Algebra.Regular.Basic
/-- In an additive semigroup, the sum of add-left-regular elements is add-left.regular.  -/
IsAddLeftRegular.add : ∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R}, IsAddLeftRegular a → IsAddLeftRegular b → IsAddLeftRegular (a + b)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.mem_sup_left : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {S T : NonUnitalStarSubalgebra R A} {x : A}, x ∈ S → x ∈ S ⊔ T
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.vcomp_right : ∀ {B : Type u} [inst : Quiver B] {a b : B} {f g h : CategoryTheory.FreeBicategory.Hom a b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g) (θ₁ θ₂ : CategoryTheory.FreeBicategory.Hom₂ g h),
  CategoryTheory.FreeBicategory.Rel θ₁ θ₂ → CategoryTheory.FreeBicategory.Rel (η.vcomp θ₁) (η.vcomp θ₂)
-- Mathlib.Data.SubtypeNeLift
/-- Given `i₀ : ι` and `x : M i₀`, this is the (dependent) map `(i : ι) → M i`
whose value at `i₀` is `x` and which extends a given map on the complement of `{i₀}`.  -/
Function.subtypeNeLift : {ι : Type u_1} → [DecidableEq ι] → {M : ι → Type u_2} → (i₀ : ι) → ((j : { i // i ≠ i₀ }) → M ↑j) → M i₀ → (i : ι) → M i
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.TextDocumentClientCapabilities.mk.injEq : ∀ (completion? : Option Lean.Lsp.CompletionClientCapabilities)
  (codeAction? : Option Lean.Lsp.CodeActionClientCapabilities)
  (inlayHint? : Option Lean.Lsp.InlayHintClientCapabilities)
  (completion?_1 : Option Lean.Lsp.CompletionClientCapabilities)
  (codeAction?_1 : Option Lean.Lsp.CodeActionClientCapabilities)
  (inlayHint?_1 : Option Lean.Lsp.InlayHintClientCapabilities),
  ({ completion? := completion?, codeAction? := codeAction?, inlayHint? := inlayHint? } =
      { completion? := completion?_1, codeAction? := codeAction?_1, inlayHint? := inlayHint?_1 }) =
    (completion? = completion?_1 ∧ codeAction? = codeAction?_1 ∧ inlayHint? = inlayHint?_1)
-- Aesop.Search.Queue
Aesop.BestFirstQueue.ActiveGoal.mk.inj : ∀ {goal : Aesop.GoalRef} {priority : Aesop.Percent} {lastExpandedInIteration addedInIteration : Aesop.Iteration}
  {goal_1 : Aesop.GoalRef} {priority_1 : Aesop.Percent}
  {lastExpandedInIteration_1 addedInIteration_1 : Aesop.Iteration},
  { goal := goal, priority := priority, lastExpandedInIteration := lastExpandedInIteration,
        addedInIteration := addedInIteration } =
      { goal := goal_1, priority := priority_1, lastExpandedInIteration := lastExpandedInIteration_1,
        addedInIteration := addedInIteration_1 } →
    goal = goal_1 ∧
      priority = priority_1 ∧
        lastExpandedInIteration = lastExpandedInIteration_1 ∧ addedInIteration = addedInIteration_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ \ m₂},
  Std.DTreeMap.Raw.Const.get (m₁ \ m₂) k h_mem = Std.DTreeMap.Raw.Const.get m₁ k ⋯
-- Mathlib.Algebra.Order.ToIntervalMod
/-- **Alias** of the reverse direction of `toIcoDiv_eq_iff`. -/
toIcoDiv_eq_of_sub_zsmul_mem_Ico : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α} {n : ℤ}, b - n • p ∈ Set.Ico a (a + p) → toIcoDiv hp a b = n
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasSum_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (m : β) (f : β → α),
  HasSum ({m}.domRestrict f) (f m)
-- Mathlib.Analysis.Analytic.ConvergenceRadius
/-- For `r` strictly smaller than the radius of `p`, then `‖pₙ‖ rⁿ` tends to zero exponentially:
for some `0 < a < 1` and `C > 0`, `‖p n‖ * r ^ n ≤ C * a ^ n`.  -/
FormalMultilinearSeries.norm_mul_pow_le_mul_pow_of_lt_radius : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) {r : NNReal},
  ↑r < p.radius → ∃ a ∈ Set.Ioo 0 1, ∃ C > 0, ∀ (n : ℕ), ‖p n‖ * ↑r ^ n ≤ C * a ^ n
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
HasProd.of_sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : UniformSpace α] [IsUniformGroup α] {γ : β → Type u_4}
  {f : (b : β) × γ b → α} {g : β → α} {a : α},
  (∀ (b : β), HasProd (fun c => f ⟨b, c⟩) (g b)) → HasProd g a → (CauchySeq fun s => ∏ i ∈ s, f i) → HasProd f a
-- Mathlib.Data.List.AList
AList.insertRec_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {C : AList β → Sort u_1} (H0 : C ∅)
  (IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)) {c : Sigma β} {l : AList β}
  (h : c.fst ∉ l), AList.insertRec H0 IH (AList.insert c.fst c.snd l) = IH c.fst c.snd l h (AList.insertRec H0 IH l)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffAt.smul_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {f : M → 𝕜} {s : (x : M) → V x} {x₀ : M},
  ContMDiffAt I (modelWithCornersSelf 𝕜 𝕜) n f x₀ →
    ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) x₀ →
      ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (f • s) x⟩) x₀
-- Mathlib.Analysis.Normed.Group.Continuity
controlled_prod_of_mem_closure : ∀ {E : Type u_4} [inst : SeminormedCommGroup E] {a : E} {s : Subgroup E},
  a ∈ closure ↑s →
    ∀ {b : ℕ → ℝ},
      (∀ (n : ℕ), 0 < b n) →
        ∃ v,
          Filter.Tendsto (fun n => ∏ i ∈ Finset.range (n + 1), v i) Filter.atTop (nhds a) ∧
            (∀ (n : ℕ), v n ∈ s) ∧ ‖(v 0)⁻¹ * a‖ < b 0 ∧ ∀ (n : ℕ), 0 < n → ‖v n‖ < b n
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
/-- Given `X : TopCat`, this is the bijection between `ZerothHomotopy X` and the
type of connected components of the simplicial set `toSSet.obj X`.  -/
TopCat.zerothHomotopyEquiv : {X : TopCat} → ZerothHomotopy ↑X ≃ (TopCat.toSSet.obj X).π₀
-- Init.Data.Order.Lemmas
Std.instIrreflOfAsymm : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Asymm r], Std.Irrefl r
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffWithinAt.smul : ∀ {𝕜 : 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} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : SMul G M] {n : WithTop ℕ∞} [ContMDiffSMul I I' n G M] {f : N → G} {g : N → M} {s : Set N} {x : N},
  ContMDiffWithinAt I'' I n f s x → ContMDiffWithinAt I'' I' n g s x → ContMDiffWithinAt I'' I' n (f • g) s x
-- Mathlib.RingTheory.PicardGroup
/-- If `FractionRing R` has trivial Picard group,
every invertible `R`-module is isomorphic to an ideal.  -/
Module.Invertible.exists_linearEquiv_ideal : ∀ (R : Type u_5) (M : Type u_6) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.Invertible R M] [Subsingleton (CommRing.Pic (FractionRing R))], ∃ I, Nonempty (M ≃ₗ[R] ↥I)
-- Mathlib.Topology.UniformSpace.Closeds
/-- A compact set has the same neighborhoods in the Hausdorff uniformity and the Vietoris topology.
 -/
IsCompact.nhds_hausdorff_eq_nhds_vietoris : ∀ {α : Type u_1} [inst : UniformSpace α] {s : Set α}, IsCompact s → nhds s = nhds s
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fastGrowing_zero : ONote.fastGrowing 0 = Nat.succ
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.diam_image : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (s : Set P),
  Metric.diam (⇑e '' s) = Metric.diam s
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.limitAddGroup : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections] →
        AddGroup (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddGrpCat))).pt
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.comp_deterministic_eq_comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) (hg : Measurable g),
  κ.comp (ProbabilityTheory.Kernel.deterministic g hg) = κ.comap g hg
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.limNthHom_add : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (r s : R),
  PadicInt.limNthHom f_compat (r + s) = PadicInt.limNthHom f_compat r + PadicInt.limNthHom f_compat s
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_Ioo_eq_restrict_Ioc : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ioc a b)
-- Mathlib.Analysis.LocallyConvex.AbsConvex
AbsConvex.univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜], AbsConvex 𝕜 Set.univ
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsStable.and : ∀ {ι : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} [inst : LinearOrder ι]
  {𝓕 : MeasureTheory.Filtration ι mΩ} {p q : (ι → Ω → E) → Prop} [inst_1 : OrderBot ι] [inst_2 : Zero E],
  ProbabilityTheory.IsStable 𝓕 p → ProbabilityTheory.IsStable 𝓕 q → ProbabilityTheory.IsStable 𝓕 fun X => p X ∧ q X
-- Mathlib.Analysis.Normed.Group.Basic
add_mem_closedBall_iff_norm : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ}, a + b ∈ Metric.closedBall a r ↔ ‖b‖ ≤ r
-- Mathlib.Order.Restriction
Preorder.piCongrLeft_comp_frestrictLe : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] {a : α},
  ⇑(Equiv.piCongrLeft (fun i => π ↑i) (Equiv.IicFinsetSet a)) ∘ Preorder.frestrictLe a = Preorder.restrictLe a
-- Init.Core
/-- Existential introduction. If `a : α` and `h : p a`,
then `⟨a, h⟩` is a proof that `∃ x : α, p x`.  -/
Exists.intro : ∀ {α : Sort u} {p : α → Prop} (w : α), p w → Exists p
-- Init.Data.Fin.Lemmas
Fin.mk_eq_zero : ∀ {n a : ℕ} {ha : a < n} [inst : NeZero n], ⟨a, ha⟩ = 0 ↔ a = 0
-- Mathlib.Algebra.Group.Defs
/-- Any `AddCommMagma G` that satisfies
`IsLeftCancelAdd G` also satisfies `IsCancelAdd G`.  -/
AddCommMagma.IsLeftCancelAdd.toIsCancelAdd : ∀ (G : Type u) [inst : AddCommMagma G] [IsLeftCancelAdd G], IsCancelAdd G
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
/-- `equiv.divRight` as a `MeasurableEquiv`.  -/
MeasurableEquiv.divRight : {G : Type u_1} → [inst : Group G] → [inst_1 : MeasurableSpace G] → [MeasurableMul G] → G → G ≃ᵐ G
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonPlainGoalParams.fromJson : Lean.Json → Except String Lean.Lsp.PlainGoalParams
-- Mathlib.Computability.ContextFreeGrammar
instDecidableEqContextFreeRule : {T : Type u_1} → {N : Type u_2} → [DecidableEq T] → [DecidableEq N] → DecidableEq (ContextFreeRule T N)
-- Mathlib.LinearAlgebra.PerfectPairing.Restrict
LinearMap.finrank_eq_of_isPerfPair : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module L M] [inst_6 : Module L N] [inst_7 : Module K M]
  [inst_8 : Module K N] [IsScalarTower K L M] (p : M →ₗ[L] N →ₗ[L] L) [p.IsPerfPair] (M' : Submodule K M)
  (N' : Submodule K N),
  Submodule.span L ↑M' = ⊤ →
    Submodule.span L ↑N' = ⊤ →
      (∀ x ∈ M', ∀ y ∈ N', (p x) y ∈ (algebraMap K L).range) → Module.finrank K ↥M' = Module.finrank L M
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.instIsScalarTowerPolynomial : ∀ (R : Type u_3) [inst : Semiring R], IsScalarTower (Polynomial R) (Polynomial R) (LaurentPolynomial R)
-- Mathlib.Algebra.Group.Basic
neg_comp_neg : ∀ (G : Type u_3) [inst : InvolutiveNeg G], Neg.neg ∘ Neg.neg = id
-- Mathlib.Data.Multiset.AddSub
Multiset.mem_add : ∀ {α : Type u_1} {a : α} {s t : Multiset α}, a ∈ s + t ↔ a ∈ s ∨ a ∈ t
-- Mathlib.Algebra.Order.Interval.Basic
Interval.sub_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [inst_3 : OrderedSub α]
  [inst_4 : AddLeftMono α] (s : Interval α), s - ⊥ = ⊥
-- Mathlib.Order.Filter.Pointwise
IsUnit.filter : ∀ {α : Type u_2} [inst : Monoid α] {a : α}, IsUnit a → IsUnit (pure a)
-- Batteries.Data.Random.MersenneTwister
Batteries.Random.MersenneTwister.Config.zero_lt_stateSize : ∀ (cfg : Batteries.Random.MersenneTwister.Config), 0 < cfg.stateSize
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.uniformizer_inv_le_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] [inst_2 : ValuativeRel.IsDiscrete R]
  [ValuativeRel.IsNontrivial R] {a : ValuativeRel.ValueGroupWithZero R}, (ValuativeRel.uniformizer R)⁻¹ ≤ a ↔ 1 < a
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- **Alias** of `OpenPartialHomeomorph.image_source_subset`.

---

Variant of `map_source`, stated for images of subsets of `source`.  -/
OpenPartialHomeomorph.map_source'' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), ↑e '' e.source ⊆ e.target
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.mem_closure : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {x : M},
  x ∈ AddSubmonoid.closure s ↔ ∀ (S : AddSubmonoid M), s ⊆ ↑S → x ∈ S
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associatorNatIso_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C × C × C),
  (CategoryTheory.MonoidalCategory.associatorNatIso C).hom.app X =
    (CategoryTheory.MonoidalCategoryStruct.associator X.1 X.2.1 X.2.2).hom
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.equivalenceOfIsInitial_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (hX : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.Under.equivalenceOfIsInitial hX).functor = CategoryTheory.Under.forget X
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- The fiber functor on sheaves is obtained from the fiber functor on presheaves
by localization with respect to the class of morphisms `J.W`.  -/
CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiberIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        (A : Type u') →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasProducts A] →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                  (CategoryTheory.presheafToSheaf J A).comp Φ.sheafFiber ≅ Φ.presheafFiber
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.RepresentablyFlat.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) [CategoryTheory.RepresentablyFlat F] [CategoryTheory.RepresentablyFlat G],
  CategoryTheory.RepresentablyFlat (F.comp G)