mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs : Lean.Meta.Grind.Arith.Cutsat.LeCnstr →
  Lean.Meta.Grind.Arith.Cutsat.LeCnstr → ℤ → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.piTensorHomMap_tprod_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i) (x : (i : ι) → s i),
  (PiTensorProduct.piTensorHomMap ((PiTensorProduct.tprod R) f)) ((PiTensorProduct.tprod R) x) =
    ⨂ₜ[R] (i : ι), (f i) (x i)
-- Mathlib.Algebra.Group.Units.Equiv
/-- Extra simp lemma that `dsimp` can use. `simp` will never use this.  -/
Equiv.addLeft_symm_apply : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), ⇑(Equiv.symm (Equiv.addLeft a)) = fun x => -a + x
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_single : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] {f : α → β} {a : α} {b : M},
  (Finsupp.mapDomain f fun₀ | a => b) = fun₀ | f a => b
-- Std.Http.Data.Method
Std.Http.Method.noConfusionType : Sort v✝ → Std.Http.Method → Std.Http.Method → Sort v✝
-- Mathlib.Data.Finset.Basic
Finset.disjoint_union_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, Disjoint s (t ∪ u) ↔ Disjoint s t ∧ Disjoint s u
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.isPlausibleOutput_next : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  {it : Std.Iter α}, it.internalState.next = some a → a < it.internalState.upperBound → it.IsPlausibleOutput a
-- Mathlib.Topology.MetricSpace.Bounded
Metric.disjoint_cobounded_nhds : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), Disjoint (Bornology.cobounded α) (nhds x)
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.id_apply : ∀ {α : Type u_2} [inst : Bornology α] (a : α), (LocallyBoundedMap.id α) a = a
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
instPolynormableSpaceSubtypeMemSubmodule : ∀ {𝕜₂ : Type u_3} {F : Type u_7} [inst : NormedField 𝕜₂] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜₂ F]
  [inst_3 : TopologicalSpace F] [PolynormableSpace 𝕜₂ F] {S : Submodule 𝕜₂ F}, PolynormableSpace 𝕜₂ ↥S
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.zeroth_conv_eq_h : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K], g.convs 0 = g.h
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.hom_ext_iff : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {a b : p.Fiber S} {φ ψ : a ⟶ b},
  φ = ψ ↔ CategoryTheory.Functor.Fiber.fiberInclusion.map φ = CategoryTheory.Functor.Fiber.fiberInclusion.map ψ
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.map_dest : ∀ {n : ℕ} (P : MvPFunctor.{u} (n + 1)) {α β : TypeVec.{u} n} (g : (α ::: P.M α).Arrow (β ::: P.M β)) (x : P.M α),
  (∀ (x : P.M α), TypeVec.lastFun g x = MvFunctor.map (TypeVec.dropFun g) x) →
    MvFunctor.map g (MvPFunctor.M.dest P x) = MvPFunctor.M.dest P (MvFunctor.map (TypeVec.dropFun g) x)
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
EuclideanSpace.volume_ball_fin_three : ∀ (x : EuclideanSpace ℝ (Fin 3)) (r : ℝ),
  MeasureTheory.volume (Metric.ball x r) = ENNReal.ofReal r ^ 3 * ENNReal.ofReal (Real.pi * 4 / 3)
-- Init.Data.Vector.Count
Vector.countP_flatMap : ∀ {α : Type u_2} {β : Type u_1} {n m : ℕ} {p : β → Bool} {xs : Vector α n} {f : α → Vector β m},
  Vector.countP p (xs.flatMap f) = (Vector.map (Vector.countP p ∘ f) xs).sum
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.snd_δ_inr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd S.L₁.g S.v₀₁.τ₃)
      (CategoryTheory.CategoryStruct.comp S.δ (CategoryTheory.Limits.pushout.inr S.L₂.f S.v₂₃.τ₁)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst S.L₁.g S.v₀₁.τ₃)
      (CategoryTheory.CategoryStruct.comp S.v₁₂.τ₂ (CategoryTheory.Limits.pushout.inl S.L₂.f S.v₂₃.τ₁))
-- Init.Data.Ord.Array
Array.instOrd : {α : Type u_1} → [Ord α] → Ord (Array α)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.apply_skipSuffixWhile_prop : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {h : s.skipSuffixWhile P ≠ s.startPos},
  ¬P (((s.skipSuffixWhile P).prev h).get ⋯)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.max_zero : ∀ {α : Type u_2} [inst : Zero α] [inst_1 : LinearOrder α], Finset.max 0 = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (n m : ℤ) (h : m + n = 0) (a : CochainComplex.HomComplex.Cocycle K L m),
  (CochainComplex.HomComplex.Cocycle.equivHomShift' n m h).symm a = (a.leftShift n 0 h).homOf
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_add_right_eq_map : ∀ {m n : ℤ}, (m<...=m + n).toArray = Array.map (fun x => x + m + 1) (0...n).toArray
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.compare_maxKey?_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {f : β → β} {km kmm : α} (hkm : t.maxKey? = some km),
  (Std.DTreeMap.Raw.Const.modify t k f).maxKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.hasBasis_nhds_zero : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7}
  {F : Type u_8} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F],
  (nhds 0).HasBasis (fun SV => Finite ↑SV.1 ∧ SV.2 ∈ nhds 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.post_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : C) (X : CategoryTheory.CostructuredArrow F S),
  (CategoryTheory.CostructuredArrow.post F G S).obj X = CategoryTheory.CostructuredArrow.mk (G.map X.hom)
-- Lean.Parser.Term
Lean.Parser.Term.scoped.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC.go.eq_def : ∀ (p₂ : Lean.Grind.CommRing.Poly) (c : ℕ) (p₁ acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulC.go p₂ c p₁ acc =
    match p₁ with
    | Lean.Grind.CommRing.Poly.num k => acc.combineC (Lean.Grind.CommRing.Poly.mulConstC k p₂ c) c
    | Lean.Grind.CommRing.Poly.add k m p₁ =>
      Lean.Grind.CommRing.Poly.mulC.go p₂ c p₁ (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC k m p₂ c) c)
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `e` is in the equivalence class of `Bool.false`.  -/
Lean.Meta.Grind.isEqBoolFalse : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addZ_of_X_eq : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R},
  P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → WeierstrassCurve.Jacobian.addZ P Q = 0
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.Boundary.snd_inj : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {e₁ : c₁.Embedding c} {e₂ : c₂.Embedding c} {ac : e₁.AreComplementary e₂} {i₁ : ι₁} {i₂ i₂' : ι₂},
  ac.Boundary i₁ i₂ → ac.Boundary i₁ i₂' → i₂ = i₂'
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_iff_infinite_and_neg : ∀ {x : ℝ*}, x.InfiniteNeg ↔ x.Infinite ∧ x < 0
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : CategoryTheory.Comonad C) (X : C),
  (CategoryTheory.Adjunction.adjToComonadIso G).hom.app X = CategoryTheory.CategoryStruct.id (G.obj X)
-- Mathlib.RingTheory.Adjoin.PowerBasis
/-- If `B : PowerBasis S A` is such that `IsIntegral R B.gen`, then
`IsIntegral R (B.basis.repr (B.gen ^ n) i)` for all `i` if
`minpoly S B.gen = (minpoly R B.gen).map (algebraMap R S)`. This is the case if `R` is a GCD domain
and `S` is its fraction ring.  -/
PowerBasis.repr_gen_pow_isIntegral : ∀ {S : Type u_2} [inst : CommRing S] {R : Type u_3} [inst_1 : CommRing R] [inst_2 : Algebra R S] {A : Type u_4}
  [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : PowerBasis S A},
  IsIntegral R B.gen →
    minpoly S B.gen = Polynomial.map (algebraMap R S) (minpoly R B.gen) →
      ∀ (n : ℕ) (i : Fin B.dim), IsIntegral R ((B.basis.repr (B.gen ^ n)) i)
-- Init.Data.BitVec.Lemmas
BitVec.getElem_sshiftRight' : ∀ {w : ℕ} {x y : BitVec w} {i : ℕ} (h : i < w),
  (x.sshiftRight' y)[i] = if h : y.toNat + i < w then x[y.toNat + i] else x.msb
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_map_equiv : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {f : R ≃+* S} {K : Subring R} {x : S},
  x ∈ Subring.map (↑f) K ↔ f.symm x ∈ K
-- Mathlib.CategoryTheory.Adjunction.Opposites
CategoryTheory.Functor.IsLeftAdjoint.leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C Dᵒᵖ} [F.IsLeftAdjoint], F.leftOp.IsRightAdjoint
-- Mathlib.Probability.Moments.Basic
/-- Moment of a real random variable, `μ[X ^ p]`.  -/
ProbabilityTheory.moment : {Ω : Type u_1} → {m : MeasurableSpace Ω} → (Ω → ℝ) → ℕ → MeasureTheory.Measure Ω → ℝ
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instNonUnitalNonAssocSemiringOfIsTopologicalSemiring : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : NonUnitalNonAssocSemiring β] →
          [IsTopologicalSemiring β] → NonUnitalNonAssocSemiring (CompactlySupportedContinuousMap α β)
-- Std.Time.DateTime.Timestamp
/-- Creates a `Timestamp` from a `Millisecond.Offset`.
 -/
Std.Time.Timestamp.ofMillisecondsSinceUnixEpoch : Std.Time.Millisecond.Offset → Std.Time.Timestamp
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.ncard_right : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G},
  AddSubgroup.IsComplement (↑H) T → T.ncard = H.index
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_id_eq : ∀ (X : TopCat),
  TopologicalSpace.Opens.map (CategoryTheory.CategoryStruct.id X) =
    CategoryTheory.Functor.id (TopologicalSpace.Opens ↑X)
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α}
  {k fallback : α}, k ∈ m → (m.insertMany l).getD k fallback = m.getD k fallback
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_two_mul' : ∀ (x : ℝ), Real.cos (2 * x) = Real.cos x ^ 2 - Real.sin x ^ 2
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.commute_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R) (s : σ), Commute φ (MvPowerSeries.X s)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} {α β : F ⟶ G} (h : α = β)
  (X : CategoryTheory.Endofunctor.Coalgebra F),
  ((CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq h).inv.app X).f = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.lift_ι_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (hs : CategoryTheory.Limits.IsLimit s) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (hs.lift t) (CategoryTheory.CategoryStruct.comp s.ι h) =
    CategoryTheory.CategoryStruct.comp t.ι h
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.ofCoeff_finsuppSum : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] (f : ι →₀ N) (g : ι → N → ℕ →₀ M),
  { coeff := f.sum g } = f.sum fun i n => { coeff := g i n }
-- Mathlib.Topology.Order.Category.FrameAdjunction
/-- The counit is a frame homomorphism.  -/
Locale.counitAppCont : (L : Locale) → FrameHom (↑(Opposite.unop L)) (TopologicalSpace.Opens (Locale.PT ↑(Opposite.unop L)))
-- Mathlib.Analysis.Quaternion
Quaternion.instNormedAddCommGroupReal : NormedAddCommGroup (Quaternion ℝ)
-- Lean.Data.Lsp.Utf16
Lean.FileMap.utf8PosToLspPos : Lean.FileMap → String.Pos.Raw → Lean.Lsp.Position
-- Lean.Elab.InfoTree.Types
/-- This structure is the state that is being used to build an InfoTree object.
During elaboration, some parts of the info tree may be `holes` which need to be filled later.
The `assignments` field is used to assign these holes.
The `trees` field is a list of pending child trees for the infotree node currently being built.

You should not need to use `InfoState` directly, instead infotrees should be built with the help of the methods here
such as `pushInfoLeaf` to create leaf nodes and `withInfoContext` to create a nested child node.

To see how `trees` is used, look at the function body of `withInfoContext'`.
 -/
Lean.Elab.InfoState : Type
-- Init.Data.Slice.Operations
/-- Allocates a new list that contains the elements of the slice in reverse order.  -/
Std.Slice.toListRev : {γ : Type u_1} → {α β : Type u_2} → [Std.ToIterator (Std.Slice γ) Id α β] → [Std.Iterator α Id β] → Std.Slice γ → List β
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.rightRel_pi : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : (i : ι) → Group (β i)] (s' : (i : ι) → Subgroup (β i)),
  QuotientGroup.rightRel (Subgroup.pi Set.univ s') = piSetoid
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.monomial : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R), ((Polynomial.monomial n) a).Splits
-- Mathlib.Computability.TuringMachine.Computable
Turing.FinTM2.inhabitedStmt : (tm : Turing.FinTM2) → Inhabited tm.Stmt
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.SkeletalFunctor.instFaithfulNonemptyFinLinOrdSkeletalFunctor : SimplexCategory.skeletalFunctor.Faithful
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- The composition of `C^n` maps, as a `C^n` map.  -/
ContMDiffMap.comp : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_5} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_6} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {E'' : Type u_8} →
                                          [inst_11 : NormedAddCommGroup E''] →
                                            [inst_12 : NormedSpace 𝕜 E''] →
                                              {H'' : Type u_9} →
                                                [inst_13 : TopologicalSpace H''] →
                                                  {I'' : ModelWithCorners 𝕜 E'' H''} →
                                                    {M'' : Type u_10} →
                                                      [inst_14 : TopologicalSpace M''] →
                                                        [inst_15 : ChartedSpace H'' M''] →
                                                          {n : WithTop ℕ∞} →
                                                            ContMDiffMap I' I'' M' M'' n →
                                                              ContMDiffMap I I' M M' n → ContMDiffMap I I'' M M'' n
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- DayConvolutionUnit structure on the candidate.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorUnitConvolutionUnit : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {V : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  CategoryTheory.MonoidalCategory.DayConvolutionUnit
                    ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).obj
                      (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorUnit
                        C V D))
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.LebesgueDecomposition.sup_mem_measurableLE : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {f g : α → ENNReal},
  f ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν →
    g ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν →
      (fun a => max (f a) (g a)) ∈ MeasureTheory.Measure.LebesgueDecomposition.measurableLE μ ν
-- Mathlib.Analysis.CStarAlgebra.Classes
MulOpposite.instCStarAlgebra : {A : Type u_1} → [CStarAlgebra A] → CStarAlgebra Aᵐᵒᵖ
-- Mathlib.LinearAlgebra.Matrix.Action
Matrix.smul_eq_mulVec : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R] (A : Matrix n n R)
  (v : n → R), A • v = A.mulVec v
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.mulRight.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  MeasurableEquiv.mulRight g = { toEquiv := Equiv.mulRight g, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.Topology.Algebra.GroupWithZero
ContinuousOn.div : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} [inst_4 : TopologicalSpace α] {s : Set α},
  ContinuousOn f s → ContinuousOn g s → (∀ x ∈ s, g x ≠ 0) → ContinuousOn (f / g) s
-- Init.Prelude
Or.resolve_left : ∀ {a b : Prop}, a ∨ b → ¬a → b
-- Mathlib.RingTheory.PowerSeries.Binomial
PowerSeries.rescale_neg_one_invOneSubPow : ∀ {A : Type u_2} [inst : CommRing A] (d : ℕ),
  (PowerSeries.rescale (-1)) ↑(PowerSeries.invOneSubPow A d) = PowerSeries.binomialSeries A (-↑d)
-- Init.Grind.Ring.OfScientific
/-- `OfScientific.ofScientific` is properly defined with respect to the field structure.
 -/
Lean.Grind.LawfulOfScientific.ofScientific_def : ∀ {α : Type u} {inst : Lean.Grind.Field α} {inst_1 : OfScientific α} [self : Lean.Grind.LawfulOfScientific α] {m : ℕ}
  {s : Bool} {e : ℕ}, OfScientific.ofScientific m s e = if s = true then ↑m / 10 ^ e else ↑m * 10 ^ e
-- Mathlib.Analysis.Fourier.Notation
/-- The notation typeclass for the Fourier transform.

While the Fourier transform is a linear operator, the notation is for the function `E → F` without
any additional properties. This makes it possible to use the notation for functions where
integrability is an issue.
Moreover, including a scalar multiplication causes problems for inferring the notation type class.
 -/
FourierTransform : Type u → outParam (Type v) → Type (max u v)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Given a vector measure `v` on `M` and a continuous `AddMonoidHom` `f : M → N`, `f ∘ v` is a
vector measure on `N`.  -/
MeasureTheory.VectorMeasure.mapRange : {α : Type u_1} →
  {mα : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          {N : Type u_4} →
            [inst_2 : AddCommMonoid N] →
              [inst_3 : TopologicalSpace N] →
                MeasureTheory.VectorMeasure α M → (f : M →+ N) → Continuous ⇑f → MeasureTheory.VectorMeasure α N
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {v : β k}, k ∈ t.insertIfNew k v
-- Init.Data.Vector.Monadic
Vector.forIn_pure_yield_eq_foldl : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  (f : α → β → β) (init : β),
  (forIn xs init fun a b => pure (ForInStep.yield (f a b))) = pure (Vector.foldl (fun b a => f a b) init xs)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- A strong natural transformation between lax functors `F` and `G` is a natural transformation
that is "natural up to 2-isomorphisms".

More precisely, it consists of the following:
* a 1-morphism `η.app a : F.obj a ⟶ G.obj a` for each object `a : B`.
* a 2-isomorphism `η.naturality f : app a ≫ G.map f ≅ F.map f ≫ app b` for each 1-morphism
  `f : a ⟶ b`.
* These 2-isomorphisms satisfy the naturality condition, and preserve the identities and the
  compositions modulo some adjustments of domains and codomains of 2-morphisms.
 -/
CategoryTheory.Lax.StrongTrans : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.LaxFunctor B C → CategoryTheory.LaxFunctor B C → Type (max (max (max u₁ v₁) v₂) w₂)
-- Init.Data.Rat.Lemmas
Rat.mul_comm : ∀ (a b : ℚ), a * b = b * a
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.condition : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} (j₁ j₂ : J)
  (t : CategoryTheory.Limits.Trident f),
  CategoryTheory.CategoryStruct.comp t.ι (f j₁) = CategoryTheory.CategoryStruct.comp t.ι (f j₂)
-- Mathlib.Order.Disjoint
ComplementedLattice.mk : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : BoundedOrder α], (∀ (a : α), ∃ b, IsCompl a b) → ComplementedLattice α
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
/-- The functor from `OpenNormalSubgroup P` to `FiniteGrp` sending `U` to `P ⧸ U`,
where `P : ProfiniteGrp`.  -/
ProfiniteGrp.toFiniteQuotientFunctor : (P : ProfiniteGrp.{u_1}) → CategoryTheory.Functor (OpenNormalSubgroup ↑P.toProfinite.toTop) FiniteGrp.{u_1}
-- Mathlib.Order.CompactlyGenerated.Basic
isAtomic_of_complementedLattice : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [ComplementedLattice α],
  IsAtomic α
-- Mathlib.RingTheory.ClassGroup.Basic
/-- The class number is `1` iff the ring of integers is a principal ideal domain.  -/
card_classGroup_eq_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDedekindDomain R] [inst_3 : Fintype (ClassGroup R)],
  Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.prod : ∀ {A : Type u_3} [inst : CommRing A] {I : Ideal A} {ι : Type u_6} {s : Finset ι} {x y : ι → A},
  (∀ i ∈ s, x i ≡ y i [SMOD I]) → ∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I]