mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.adjoinRoot_eq_top : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R}, R[AdjoinRoot.root f] = ⊤
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α},
  t.min? = some km → t.get? km = some km
-- Mathlib.Probability.Process.PartitionFiltration
/-- A filtration built from the measurable spaces generated by the partitions `memPartition t n` for
all `n : ℕ`.  -/
ProbabilityTheory.partitionFiltration : {α : Type u_1} →
  [m : MeasurableSpace α] → {t : ℕ → Set α} → (∀ (n : ℕ), MeasurableSet (t n)) → MeasureTheory.Filtration ℕ m
-- Mathlib.Order.PiLex
Pi.instNoMaxOrderLexForallOfWellFoundedLTOfNonempty : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [WellFoundedLT ι] [Nonempty ι]
  [inst_3 : (i : ι) → PartialOrder (β i)] [∀ (i : ι), NoMaxOrder (β i)], NoMaxOrder (Lex ((i : ι) → β i))
-- Mathlib.Topology.JacobsonSpace
jacobsonSpace_iff : ∀ (X : Type u_1) [inst : TopologicalSpace X],
  JacobsonSpace X ↔ ∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsTopologicalAddGroup.rightUniformSpace.eq_1 : ∀ (G : Type u_1) [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G],
  IsTopologicalAddGroup.rightUniformSpace G =
    { toTopologicalSpace := inst_1, uniformity := Filter.comap (fun p => p.2 + -p.1) (nhds 0), symm := ⋯, comp := ⋯,
      nhds_eq_comap_uniformity := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.toSSetObj₀Equiv_symm_apply : ∀ {X : TopCat} (a : ↑X),
  TopCat.toSSetObj₀Equiv.symm a =
    (X.toSSetObjEquiv (Opposite.op { len := 0 })).symm { toFun := fun x => a, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_inv_right`. -/
MonovaryOn.inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn f g s → AntivaryOn f g⁻¹ s
-- Mathlib.RingTheory.Jacobson.Ring
_private.Mathlib.RingTheory.Jacobson.Ring.0.MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing' : ∀ {n : ℕ} {R : Type u_1} [inst : CommRing R] [IsJacobsonRing R] (P : Ideal (MvPolynomial (Fin n) R)),
  P.IsMaximal → (algebraMap R (MvPolynomial (Fin n) R ⧸ P)).IsIntegral
-- Mathlib.Data.ENat.Basic
ENat.lt_add_one_iff' : ∀ {m n : ℕ∞}, m ≠ ⊤ → (m < n + 1 ↔ m ≤ n)
-- Mathlib.Order.Filter.Map
Filter.instLawfulFunctor : LawfulFunctor Filter
-- Mathlib.Algebra.Group.Invertible.Basic
Commute.invOf_right : ∀ {α : Type u} [inst : Monoid α] {a b : α} [inst_1 : Invertible b], Commute a b → Commute a ⅟b
-- Init.Data.Nat.Basic
Nat.pred_lt_self : ∀ {a : ℕ}, 0 < a → a.pred < a
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.instInhabitedHorizontalComp : Inhabited Mathlib.Tactic.BicategoryLike.HorizontalComp
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The 2-morphism from the original 1-morphism to the normalized 1-morphism.  -/
Mathlib.Tactic.BicategoryLike.Normalize.Result.toNormalize : Mathlib.Tactic.BicategoryLike.Normalize.Result → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.mu_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddCommGroup 𝕜] [inst_1 : One 𝕜] [inst_2 : Preorder α]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : DecidableEq α] (a b : α),
  (IncidenceAlgebra.mu 𝕜) a b = if a = b then 1 else -∑ x ∈ Finset.Ico a b, (IncidenceAlgebra.mu 𝕜) a x
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.toTopologicalSpace : {α : Type u} → [self : UniformSpace α] → TopologicalSpace α
-- Mathlib.RingTheory.FiniteType
/-- If a set `S` generates, as algebra, `R[M]`, then the image of the union of the
supports of elements of `S` generates `R[M]`.  -/
MonoidAlgebra.support_gen_of_gen' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Monoid M] {S : Set (MonoidAlgebra R M)},
  Algebra.adjoin R S = ⊤ → Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ⋃ f ∈ S, ↑f.coeff.support) = ⊤
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.disjoint_vadd_set_vadd : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] {B : Set X} {s : Set G} {g : G},
  AddAction.IsBlock G B → ¬g +ᵥ B ⊆ s +ᵥ B → Disjoint (g +ᵥ B) (s +ᵥ B)
-- Mathlib.Analysis.InnerProductSpace.ProdL2
WithLp.prod_inner_apply : ∀ {𝕜 : Type u_1} {E : Type u_4} {F : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  (x y : WithLp 2 (E × F)), inner 𝕜 x y = inner 𝕜 x.ofLp.1 y.ofLp.1 + inner 𝕜 x.ofLp.2 y.ofLp.2
-- Mathlib.Data.Fintype.Basic
PSigma.fintypePropRight : {α : Type u_4} → {β : α → Prop} → [(a : α) → Decidable (β a)] → [Fintype α] → Fintype ((a : α) ×' β a)
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A sequential space is compactly generated.

The proof is taken from <https://ncatlab.org/nlab/files/StricklandCGHWSpaces.pdf>,
Proposition 1.6.  -/
instUCompactlyGeneratedSpaceOfSequentialSpace : ∀ {X : Type w} [tX : TopologicalSpace X] [SequentialSpace X], UCompactlyGeneratedSpace X
-- Mathlib.CategoryTheory.Sites.Coherent.RegularTopology
/-- A sieve is a cover for the regular topology if and only if it contains an `EffectiveEpi`.  -/
CategoryTheory.regularTopology.mem_sieves_iff_hasEffectiveEpi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C] {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ (CategoryTheory.regularTopology C) X ↔ ∃ Y π, CategoryTheory.EffectiveEpi π ∧ S.arrows π
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Covers.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
  (S : CategoryTheory.Sieve X) (f : Y ⟶ X), J.Covers S f = (CategoryTheory.Sieve.pullback f S ∈ J Y)
-- Mathlib.Data.Set.Prod
Set.Nonempty.fst : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Nonempty → s.Nonempty
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.instIsRightAdjointCommMonCatForget₂RingHomCarrierMonoidHomCarrier : (CategoryTheory.forget₂ CommRingCat CommMonCat).IsRightAdjoint
-- Lean.Elab.Tactic.Try
/-- Entry in the try suggestion registry  -/
Lean.Elab.Tactic.Try.TrySuggestionEntry : Type
-- Mathlib.RingTheory.Valuation.Basic
/-- A ring homomorphism `S → R` induces a map `AddValuation R Γ₀ → AddValuation S Γ₀`.  -/
AddValuation.comap : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] →
        {S : Type u_6} → [inst_2 : Ring S] → (S →+* R) → AddValuation R Γ₀ → AddValuation S Γ₀
-- Mathlib.Analysis.Normed.Group.Constructions
norm_le_pi_norm' : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedGroup (G i)] (f : (i : ι) → G i)
  (i : ι), ‖f i‖ ≤ ‖f‖
-- Lean.LocalContext
/-- A declaration for a `LocalContext`. This is used to register which free variables are in scope.

See `LocalDecl.index`, `LocalDecl.fvarId`, `LocalDecl.userName`, `LocalDecl.type` for accessors for
arguments common to both constructors.
 -/
Lean.LocalDecl : Type
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Precomposing `f` with `Prod.fst` is `C^n` at `(x, y)`  -/
ContDiffAt.fst' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → G} {x : E} {y : F},
  ContDiffAt 𝕜 n f x → ContDiffAt 𝕜 n (fun x => f x.1) (x, y)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` of an `AddGroup` inherits an integer scaling.  -/
AddSubgroup.zsmul : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → SMul ℤ ↥H
-- Mathlib.Data.Num.Bitwise
NzsNum.msb.inj : ∀ {a a_1 : Bool}, NzsNum.msb a = NzsNum.msb a_1 → a = a_1
-- Mathlib.Topology.MetricSpace.Isometry
Fin.appendIsometryOfEq_symm_apply : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {n m l : ℕ} (hmln : m + l = n) (a : Fin n → α),
  (Fin.appendIsometryOfEq hmln).symm a =
    (fun i => a (Fin.cast hmln (Fin.castAdd l i)), fun i => a (Fin.cast hmln (Fin.natAdd m i)))
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  {Z : HomologicalComplex C (ComplexShape.up ℤ)}
  (h :
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj
        (CochainComplex.mappingCone.triangle (CochainComplex.mappingConeCompTriangle f g).mor₁).obj₁ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompHomotopyEquiv f g).hom
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.mappingCone.triangle (CochainComplex.mappingConeCompTriangle f g).mor₁).mor₃ h) =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangle f g).mor₃ h
-- Mathlib.Algebra.Star.StarRingHom
/-- Copy of a `NonUnitalStarRingHom` with a new `toFun` equal to the old one. Useful
to fix definitional equalities.  -/
NonUnitalStarRingHom.copy : {A : Type u_1} →
  {B : Type u_2} →
    [inst : NonUnitalNonAssocSemiring A] →
      [inst_1 : Star A] →
        [inst_2 : NonUnitalNonAssocSemiring B] →
          [inst_3 : Star B] → (f : A →⋆ₙ+* B) → (f' : A → B) → f' = ⇑f → A →⋆ₙ+* B
-- Mathlib.LinearAlgebra.FreeModule.PID
/-- A submodule inside a free `R`-submodule of finite rank is also a free `R`-module of finite rank,
if `R` is a principal ideal domain.

See also the stronger version `Submodule.smithNormalFormOfLE`.
 -/
Submodule.basisOfPidOfLE : {R : Type u_2} →
  [inst : CommRing R] →
    {M : Type u_3} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [IsPrincipalIdealRing R] →
            [IsDomain R] →
              {ι : Type u_4} →
                [Finite ι] → {N O : Submodule R M} → N ≤ O → Module.Basis ι R ↥O → (n : ℕ) × Module.Basis (Fin n) R ↥N
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.backward.proofsInPublic : Lean.Option Bool
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.abs_le_eVariationOn : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  BoundedVariationOn f s → ∀ {a b : α}, |variationOnFromTo f s a b| ≤ (eVariationOn f s).toReal
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.response.sizeOf_spec : ∀ (id : Lean.JsonRpc.RequestID) (result : Lean.Json),
  sizeOf (Lean.JsonRpc.Message.response id result) = 1 + sizeOf id + sizeOf result
-- Init.Data.Array.Basic
Array.eraseIdx.congr_simp : ∀ {α : Type u} (xs xs_1 : Array α) (e_xs : xs = xs_1) (i i_1 : ℕ) (e_i : i = i_1) (h : i < xs.size),
  xs.eraseIdx i h = xs_1.eraseIdx i_1 ⋯
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Taking a product over `s : Finset ι` is the same as multiplying the value on a single element
`f a` by the product of `s.erase a`.

See `Multiset.prod_map_erase` for the `Multiset` version.  -/
Finset.mul_prod_erase : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (f : ι → M) {a : ι},
  a ∈ s → f a * ∏ x ∈ s.erase a, f x = ∏ x ∈ s, f x
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.iIndep : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ι → Type u_8} {mβ : (i : ι) → MeasurableSpace (β i)}
  {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α}
  {f : (x : ι) → Ω → β x},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    ProbabilityTheory.Kernel.iIndep (fun x => MeasurableSpace.comap (f x) (mβ x)) κ μ
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.filter_single_pos : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {p : ι → Prop}
  [inst_2 : DecidablePred p] (i : ι) (x : β i), p i → (DFinsupp.filter p fun₀ | i => x) = fun₀ | i => x
-- Std.Data.DHashMap.Raw
/-- Computes the intersection of the given hash maps. The result will only contain entries from the first map.

This function always merges the smaller map into the larger map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.DHashMap.Raw.inter : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonpositive on `Ioo a b` and
nonnegative on `Ioo b c`. Then `f` attains its minimum on `Ioo a c` at `b`.  -/
isMinOn_Ioo_of_deriv : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Ioo a b) →
      DifferentiableOn ℝ f (Set.Ioo b c) →
        (∀ x ∈ Set.Ioo a b, deriv f x ≤ 0) → (∀ x ∈ Set.Ioo b c, 0 ≤ deriv f x) → IsMinOn f (Set.Ioo a c) b
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.swap_apply_right : CategoryTheory.Limits.WalkingPair.swap CategoryTheory.Limits.WalkingPair.right = CategoryTheory.Limits.WalkingPair.left
-- Mathlib.RingTheory.Algebraic.Integral
/-- Bijection between algebra equivalences and algebra homomorphisms  -/
algEquivEquivAlgHom : (K : Type u_1) →
  (L : Type u_2) →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → [FiniteDimensional K L] → Gal(L/K) ≃* (L →ₐ[K] L)
-- Mathlib.Data.List.MinMax
/-- `minimum l` returns a `WithTop α`, the smallest element of `l` for nonempty lists, and `⊤` for
`[]`  -/
List.minimum : {α : Type u_1} → [inst : Preorder α] → [DecidableLT α] → List α → WithTop α
-- Mathlib.Algebra.Star.Conjneg
conjneg_add : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R] (f g : G → R),
  conjneg (f + g) = conjneg f + conjneg g
-- Lean.Meta.Basic
Lean.Meta.ExprConfigCacheKey.configKey : Lean.Meta.ExprConfigCacheKey → UInt64
-- Mathlib.RingTheory.Coalgebra.Hom
Coalgebra.Repr.induced_right : ∀ {R : Type u} {A : Type v} {B : Type w} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A]
  [inst_6 : Coalgebra R B] {a : A} (repr : Coalgebra.Repr R a ι) {F : Type u_2} [inst_7 : FunLike F A B]
  [inst_8 : CoalgHomClass F R A B] (φ : F) (a_1 : ι), (repr.induced φ).right a_1 = (⇑φ ∘ repr.right) a_1
-- Mathlib.CategoryTheory.Skeletal
/-- The `skeleton` of `C` given by choice is a skeleton of `C`.  -/
CategoryTheory.skeleton_isSkeleton : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.IsSkeletonOf C (CategoryTheory.Skeleton C) (CategoryTheory.fromSkeleton C)
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.instNonemptyOfIsClosedUnderLimitsOfShapeDiscretePEmptyOfHasTerminal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [CategoryTheory.Limits.HasTerminal C], P.Nonempty
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_congr : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s : Set M},
  (∀ y ∈ s, f₁ y = f y) → f₁ x = f x → (MDiffAt[s] f₁ x ↔ MDiffAt[s] f x)
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.iSupLift_comp_inclusion : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {ι : Type u_4} [inst_5 : Nonempty ι] (K : ι → Subalgebra R A)
  {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)} {T : Subalgebra R A} {hT : T ≤ iSup K}
  {i : ι} (h : K i ≤ T), (Subalgebra.iSupLift K dir f hf T hT).comp (Subalgebra.inclusion h) = f i
-- Init.Data.SInt.Lemmas
ISize.toNat_toBitVec : ∀ (x : ISize), x.toBitVec.toNat = x.toUSize.toNat
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_mul_left' : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : s.IsPWO),
  x.support ⊆ s → (x * y).coeff a = ∑ ij ∈ Finset.antidiagonal hs ⋯ a, x.coeff ij.1 * y.coeff ij.2
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_eq_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set β} {a : α},
  a • s = Set.univ ↔ s = Set.univ
-- Mathlib.Order.Basic
lt_of_forall_ge_imp_ne : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ (c : α), a ≤ c → c ≠ b) → b < a
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Hour` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.hour : Std.Time.PlainDateTime → Std.Time.Hour.Ordinal
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.instBEqPostponeBehavior.beq : Lean.Elab.Term.PostponeBehavior → Lean.Elab.Term.PostponeBehavior → Bool
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.instIsFiniteKernelProdParallelComp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ} [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η],
  ProbabilityTheory.IsFiniteKernel (κ.parallelComp η)
-- Batteries.Data.String.Lemmas
String.utf8Len_reverseAux : ∀ (cs₁ cs₂ : List Char), String.utf8Len (cs₁.reverseAux cs₂) = String.utf8Len cs₁ + String.utf8Len cs₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_some_get : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α} (h' : a ∈ t),
  t.get? a = some (t.get a h')
-- Mathlib.Algebra.Homology.Bifunctor
/-- The first differential on a summand of `mapBifunctor K₁ K₂ F c`  -/
HomologicalComplex.mapBifunctor.d₁ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : 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} D] →
            {I₁ : Type u_4} →
              {I₂ : Type u_5} →
                {J : Type u_6} →
                  {c₁ : ComplexShape I₁} →
                    {c₂ : ComplexShape I₂} →
                      [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
                        [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                          [inst_5 : CategoryTheory.Preadditive D] →
                            (K₁ : HomologicalComplex C₁ c₁) →
                              (K₂ : HomologicalComplex C₂ c₂) →
                                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                  [inst_6 : F.PreservesZeroMorphisms] →
                                    [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                                      (c : ComplexShape J) →
                                        [inst_8 : TotalComplexShape c₁ c₂ c] →
                                          [inst_9 : K₁.HasMapBifunctor K₂ F c] →
                                            [inst_10 : DecidableEq J] →
                                              (i₁ : I₁) →
                                                (i₂ : I₂) →
                                                  (j : J) →
                                                    (F.obj (K₁.X i₁)).obj (K₂.X i₂) ⟶ (K₁.mapBifunctor K₂ F c).X j
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- Decomposition of a `k`-algebra homomorphism from `SkewMonoidAlgebra k G` by
its values on `F (single a 1)`.  -/
SkewMonoidAlgebra.lift_unique : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u_4} [inst_2 : Semiring A]
  [inst_3 : Algebra k A] [inst_4 : MulSemiringAction G k] [inst_5 : SMulCommClass G k k]
  (F : SkewMonoidAlgebra k G →ₐ[k] A) (f : SkewMonoidAlgebra k G),
  F f = f.sum fun a b => b • F (SkewMonoidAlgebra.single a 1)
-- Std.Async.Signal
_private.Std.Async.Signal.0.Std.Async.Signal.Waiter.ofNative : Std.Internal.UV.Signal → Std.Async.Signal.Waiter
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.coeffLinearEquiv_symm_apply : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (a : M →₀ S), (AddMonoidAlgebra.coeffLinearEquiv R).symm a = AddMonoidAlgebra.ofCoeff a
-- Mathlib.Order.Hom.Basic
/-- An order embedding is also an order embedding between dual orders.  -/
OrderEmbedding.dual : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α ↪o β → αᵒᵈ ↪o βᵒᵈ
-- Init.Data.Nat.MinMax
Nat.zero_max : ∀ (a : ℕ), max 0 a = a
-- Mathlib.Analysis.Convolution
/-- The convolution of two functions `f` and `g` with respect to a continuous bilinear map `L` and
measure `μ`. It is defined to be `(f ⋆[L, μ] g) x = ∫ t, L (f t) (g (x - t)) ∂μ`.  -/
MeasureTheory.convolution : {𝕜 : Type u𝕜} →
  {G : Type uG} →
    {E : Type uE} →
      {E' : Type uE'} →
        {F : Type uF} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedAddCommGroup E'] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NontriviallyNormedField 𝕜] →
                  [inst_4 : NormedSpace 𝕜 E] →
                    [inst_5 : NormedSpace 𝕜 E'] →
                      [inst_6 : NormedSpace 𝕜 F] →
                        [inst_7 : MeasurableSpace G] →
                          [NormedSpace ℝ F] →
                            [Sub G] →
                              (G → E) →
                                (G → E') →
                                  (E →L[𝕜] E' →L[𝕜] F) →
                                    autoParam (MeasureTheory.Measure G) MeasureTheory.convolution._auto_1 → G → F
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₂.eq_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))),
  Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ 0 =
    ⟨0,
      ⟨CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.xPrevIso Q Homotopy.mkInductiveAux₂._proof_1).inv,
        ⋯⟩⟩