mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_dotProduct : ∀ {α : Type u} {n : ℕ} [inst : AddCommMonoid α] [inst_1 : Mul α] (x : α) (v : Fin n → α) (w : Fin n.succ → α),
  Matrix.vecCons x v ⬝ᵥ w = x * Matrix.vecHead w + v ⬝ᵥ Matrix.vecTail w
-- Mathlib.GroupTheory.PGroup
/-- p-groups with different p are disjoint  -/
IsPGroup.disjoint_of_ne : ∀ {G : Type u_1} [inst : Group G] (p₁ p₂ : ℕ) [hp₁ : Fact (Nat.Prime p₁)] [hp₂ : Fact (Nat.Prime p₂)],
  p₁ ≠ p₂ → ∀ (H₁ H₂ : Subgroup G), IsPGroup p₁ ↥H₁ → IsPGroup p₂ ↥H₂ → Disjoint H₁ H₂
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOp_left : CategoryTheory.Limits.walkingParallelPairOp.map CategoryTheory.Limits.WalkingParallelPairHom.left =
  Quiver.Hom.op CategoryTheory.Limits.WalkingParallelPairHom.left
-- Lean.CoreM
Lean.MonadDeclNameGenerator.mk : {m : Type → Type} → m Lean.DeclNameGenerator → (Lean.DeclNameGenerator → m Unit) → Lean.MonadDeclNameGenerator m
-- Mathlib.RingTheory.Artinian.Ring
IsArtinianRing.jacobson_eq_radical : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R] (I : Ideal R), I.jacobson = I.radical
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.toArray : Lean.Meta.Simp.UsedSimps → Array Lean.Meta.Origin
-- Mathlib.Probability.Moments.Basic
/-- Cumulant-generating function of a real random variable `X`: `fun t => log μ[exp(t*X)]`.  -/
ProbabilityTheory.cgf : {Ω : Type u_1} → {m : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → ℝ → ℝ
-- Mathlib.Order.Bounds.Image
IsLeast.isGreatest_image2_of_isGreatest : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Monotone (f a)) → IsLeast s a → IsGreatest t b → IsGreatest (Set.image2 f s t) (f a b)
-- Std.Sync.CancellationContext
/-- Creates a selector that waits for cancellation.
 -/
Std.CancellationContext.doneSelector : Std.CancellationContext → Std.Async.Selector Unit
-- Init.Data.SInt.Lemmas
Int64.ofIntLE_int32ToInt : ∀ (x : Int32), Int64.ofIntLE x.toInt ⋯ ⋯ = x.toInt64
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map sending `∑ aᵢ·gᵢ : G →₀ A` to `∑ φ(aᵢ)·f(gᵢ) : H →₀ B`.  -/
groupHomology.chainsMap₁ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u_1, u, u} k G} →
          {B : Rep.{u_1, u, u} k H} →
            (f : G →* H) → (A ⟶ Rep.res f B) → (ModuleCat.of k (G →₀ ↑A) ⟶ ModuleCat.of k (H →₀ ↑B))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_nat_mul_two_pi_mul_I : ∀ (n : ℕ), Complex.exp (↑n * (2 * ↑Real.pi * Complex.I)) = 1
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget_createsLimits.eq_1 : CommMonCat.forget_createsLimits = CommMonCat.forget_createsLimitsOfSize
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- If `f` is box-additive on subboxes of `I₀`, then it is box-additive on subboxes of any
`I ≤ I₀`.  -/
BoxIntegral.BoxAdditiveMap.restrict : {ι : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] →
      {I₀ : WithTop (BoxIntegral.Box ι)} →
        BoxIntegral.BoxAdditiveMap ι M I₀ →
          (I : WithTop (BoxIntegral.Box ι)) → I ≤ I₀ → BoxIntegral.BoxAdditiveMap ι M I
-- Std.Internal.Do.Order.Basic
/-- Embedding a proposition into the `Prop` lattice (`⌜p⌝`) is the proposition itself. See
`top_prop_eq` for why this is not `@[simp]`.  -/
Lean.Order.ofProp_prop_eq : ∀ (p : Prop), Lean.Order.CompleteLattice.ofProp p = p
-- Mathlib.RingTheory.Flat.Equalizer
AlgHom.coe_tensorEqualizer : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {A : Type u_4}
  {B : Type u_5} [inst_7 : CommRing A] [inst_8 : CommRing B] [inst_9 : Algebra R A] [inst_10 : Algebra R B]
  (f g : A →ₐ[R] B) (x : TensorProduct R T ↥(f.equalizer g)),
  ↑((AlgHom.tensorEqualizer S T f g) x) = (Algebra.TensorProduct.map (AlgHom.id S T) (f.equalizer g).val) x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_inter_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} {fallback : β},
        m₁.contains k = false → Std.DHashMap.Internal.Raw₀.Const.getD (m₁.inter m₂) k fallback = fallback
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.germ_residue_assoc : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (x : ↥X) (hx : x ∈ U) {Z : CommRingCat} (h : X.residueField x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ U x hx) (CategoryTheory.CategoryStruct.comp (X.residue x) h) =
    CategoryTheory.CategoryStruct.comp (X.evaluation U x hx) h
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_eraseManyEntries!_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [inst : BEq α] [Std.LawfulBEqOrd α] [Std.TransOrd α]
  {t₁ : Std.DTreeMap.Internal.Impl α β},
  t₁.WF →
    ∀ {t₂ : Std.DTreeMap.Internal.Impl α β},
      (↑(t₁.eraseManyEntries! t₂)).toListModel.Perm
        (List.filter (fun p => !(List.map Sigma.fst t₂.toListModel).contains p.fst) t₁.toListModel)
-- Mathlib.Order.Filter.SmallSets
Filter.frequently_smallSets_mem : ∀ {α : Type u_1} (l : Filter α), ∃ᶠ (s : Set α) in l.smallSets, s ∈ l
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.wellFoundedLT : WellFoundedLT Ordinal.{u_1}
-- Mathlib.Algebra.Algebra.Equiv
/-- An algebra isomorphism induces a group isomorphism between automorphism groups.

This is a more bundled version of `AlgEquiv.equivCongr`.  -/
AlgEquiv.autCongr : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] →
            [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → (A₁ ≃ₐ[R] A₂) → (A₁ ≃ₐ[R] A₁) ≃* A₂ ≃ₐ[R] A₂
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (x y : R), v (x + y) ≤ max (v x) (v y)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedInstance : Inhabited Lean.Meta.SynthInstance.Instance
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.trans : ∀ {α : Type u} {L₁ L₂ L₃ : List (α × Bool)}, FreeGroup.Red L₁ L₂ → FreeGroup.Red L₂ L₃ → FreeGroup.Red L₁ L₃
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.instModuleDomMulActOfSMulCommClass : {R : Type u_1} →
  {R' : Type u_2} →
    {S : Type u_3} →
      {M : Type u_4} →
        {M' : Type u_5} →
          [inst : Semiring R] →
            [inst_1 : Semiring R'] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M'] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module R' M'] →
                      {σ₁₂ : R →+* R'} →
                        [inst_6 : Semiring S] →
                          [inst_7 : Module S M] → [SMulCommClass R S M] → Module Sᵈᵐᵃ (M →ₛₗ[σ₁₂] M')
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_eq_some_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.minKey? = some (t.minKeyD fallback)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.Pos.skipWhile.eq_1 : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_conj : ∀ {α : Type u_1} {m : MeasurableSpace α} {K : Type u_3} [inst : RCLike K] (f : α → K) (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm ((starRingEnd (α → K)) f) p μ = MeasureTheory.lpNorm f p μ
-- Mathlib.Algebra.Ring.Defs
NonUnitalRing.toNonUnitalNonAssocRing : {α : Type u_1} → [self : NonUnitalRing α] → NonUnitalNonAssocRing α
-- Mathlib.RingTheory.LocalRing.ResidueField.Instances
instIsSeparableResidueFieldOfQuotientIdeal : ∀ {A : Type u_2} {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (q : Ideal B) [inst_3 : q.LiesOver p] [inst_4 : p.IsMaximal] [inst_5 : q.IsMaximal]
  [inst_6 : Algebra (Localization.AtPrime p) (Localization.AtPrime q)]
  [inst_7 : Localization.AtPrime.IsLiesOverAlgebra p q] [Algebra.IsSeparable (A ⧸ p) (B ⧸ q)],
  Algebra.IsSeparable p.ResidueField q.ResidueField
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
/-- Auxiliary definition for `totalFlipIso`.  -/
HomologicalComplex₂.totalFlipIsoX : {C : Type u_1} →
  {I₁ : Type u_2} →
    {I₂ : Type u_3} →
      {J : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Preadditive C] →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  (c : ComplexShape J) →
                    [inst_2 : TotalComplexShape c₁ c₂ c] →
                      [inst_3 : TotalComplexShape c₂ c₁ c] →
                        [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] →
                          [inst_5 : K.HasTotal c] →
                            [inst_6 : DecidableEq J] → (j : J) → (K.flip.total c).X j ≅ (K.total c).X j
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.categoryParser.formatter : Lean.Name → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.cancel_iso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (g g' : Z ⟶ Y) (f : X ≅ Y),
  CategoryTheory.CategoryStruct.comp g f.inv = CategoryTheory.CategoryStruct.comp g' f.inv ↔ g = g'
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.instRespectsIsoInnerAnodyneExtensions : SSet.innerAnodyneExtensions.RespectsIso
-- Mathlib.Topology.Constructions
frontier_inter_open_inter : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen t → frontier (s ∩ t) ∩ t = frontier s ∩ t
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- The equivalence of categories `(C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ≌ C₁ × C₂ × C₃ ⥤ E`
given by the curryfication of functors in three variables.  -/
CategoryTheory.Functor.currying₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {E : Type u_9} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
              [inst_3 : CategoryTheory.Category.{v_9, u_9} E] →
                CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)) ≌
                  CategoryTheory.Functor (C₁ × C₂ × C₃) E
-- Lean.Data.Json.Elab
/-- Json number negation syntax for ordinary numbers.  -/
Lean.Json.«json-_» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) =
    h_1 ()
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isSymm_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsSymm ↔ LinearMap.IsSymm B
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_le_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : t.contains k = true), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.opObjEquiv_mem_nonDegenerate_iff : ∀ (X : SSet) {n : ℕ} (x : X.op.obj (Opposite.op { len := n })),
  SSet.opObjEquiv x ∈ X.nonDegenerate n ↔ x ∈ X.op.nonDegenerate n
-- Batteries.Control.ForInStep.Lemmas
ForInStep.run_yield : ∀ {α : Type u_1} {a : α}, (ForInStep.yield a).run = a
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- The right unitor: `f ≫ 𝟙 b ≅ f`  -/
CategoryTheory.Bicategory.termρ_ : Lean.ParserDescr
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformInducing.isComplete_range : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} [CompleteSpace α],
  IsUniformInducing f → IsComplete (Set.range f)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_toCompactsOrderEmbedding : ∀ {α : Type u_1} [inst : TopologicalSpace α],
  ⇑TopologicalSpace.NonemptyCompacts.toCompactsOrderEmbedding = TopologicalSpace.NonemptyCompacts.toCompacts
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf'_apply : ∀ {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [inst : (b : β) → SemilatticeInf (C b)] {s : Finset α}
  (H : s.Nonempty) (f : α → (b : β) → C b) (b : β), s.inf' H f b = s.inf' H fun a => f a b
-- Mathlib.Data.Int.Interval
Int.image_Ico_emod : ∀ (n a : ℤ), 0 ≤ a → Finset.image (fun x => x % a) (Finset.Ico n (n + a)) = Finset.Ico 0 a
-- Mathlib.GroupTheory.Perm.Fin
Fin.sign_cycleIcc_of_le : ∀ {n : ℕ} {i j : Fin n}, i ≤ j → Equiv.Perm.sign (i.cycleIcc j) = (-1) ^ (↑j - ↑i)
-- Init.Data.Int.Order
Int.le_add_of_nonneg_right : ∀ {a b : ℤ}, 0 ≤ b → a ≤ a + b
-- Mathlib.Data.Multiset.MapFold
Multiset.Nodup.pmap : ∀ {α : Type u_1} {β : Type v} {p : α → Prop} {f : (a : α) → p a → β} {s : Multiset α} {H : ∀ a ∈ s, p a},
  (∀ (a : α) (ha : p a) (b : α) (hb : p b), f a ha = f b hb → a = b) → s.Nodup → (Multiset.pmap f s H).Nodup
-- Mathlib.Data.Nat.Init
Nat.mul_def : ∀ {m n : ℕ}, m.mul n = m * n
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Simplex.equilateral_reindex_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {m n : ℕ}
  {s : Affine.Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)), (s.reindex e).Equilateral ↔ s.Equilateral
-- Mathlib.Dynamics.Ergodic.Action.Basic
MeasureTheory.aeconst_of_forall_vadd_ae_eq : ∀ (G : Type u_1) {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : AddGroup G]
  [inst_1 : AddAction G α] [ErgodicVAdd G α μ] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → (∀ (g : G), g +ᵥ s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.Cotangent.surjective_map_ofComp : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Function.Surjective ⇑(Algebra.Extension.Cotangent.map (Q.ofComp P).toExtensionHom)
-- Aesop.Util.Tactic.Ext
Aesop.ExtResult.goals : Aesop.ExtResult → Array (Lean.MVarId × Array Lean.FVarId)
-- Mathlib.Order.ConditionallyCompleteLattice.Group
ciInf_mul_ciInf_le_ciInf_mul : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Mul α] [MulLeftMono α]
  [MulRightMono α] {f g : ι → α},
  BddBelow (Set.range f) → BddBelow (Set.range g) → (⨅ i, f i) * ⨅ i, g i ≤ ⨅ i, f i * g i
-- Mathlib.Analysis.Normed.Lp.WithLp
LinearMap.withLpMap_comp : ∀ (p : ENNReal) {K : Type u_1} {K' : Type u_2} {K'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6}
  [inst : Semiring K] [inst_1 : Semiring K'] [inst_2 : Semiring K''] {σ : K →+* K'} {τ : K' →+* K''} {ρ : K →+* K''}
  [inst_3 : RingHomCompTriple σ τ ρ] [inst_4 : AddCommGroup V] [inst_5 : Module K V] [inst_6 : AddCommGroup V']
  [inst_7 : Module K' V'] [inst_8 : AddCommGroup V''] [inst_9 : Module K'' V''] (f : V' →ₛₗ[τ] V'') (g : V →ₛₗ[σ] V'),
  LinearMap.withLpMap p (f ∘ₛₗ g) = LinearMap.withLpMap p f ∘ₛₗ LinearMap.withLpMap p g
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.instIsClosedUnderColimitsOfShapeDiscretePEmptyOfContainsZeroOfIsClosedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero]
  [P.IsClosedUnderIsomorphisms], P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})
-- Mathlib.Topology.Clopen
ContinuousOn.preimage_isClopen_of_isClopen : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X}
  {t : Set Y}, ContinuousOn f s → IsClopen s → IsClopen t → IsClopen (s ∩ f ⁻¹' t)
-- Mathlib.Topology.Order
setOfPred_isOpen_iSup : ∀ {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α}, {s | IsOpen s} = ⋂ i, {s | IsOpen s}
-- Mathlib.Algebra.Free
/-- The canonical multiplicative morphism from `FreeMagma α` to `FreeSemigroup α`.  -/
FreeMagma.toFreeSemigroup : {α : Type u} → FreeMagma α →ₙ* FreeSemigroup α
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
EisensteinSeries.isBigO_linear_add_const_vec : ∀ (z : UpperHalfPlane) (a b : ℤ), (fun m => ((↑(m 0) + ↑a) * ↑z + ↑(m 1) + ↑b)⁻¹) =O[Filter.cofinite] fun m => ‖m‖⁻¹
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instAddGroup : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddGroup β] → [IsTopologicalAddGroup β] → AddGroup (CompactlySupportedContinuousMap α β)
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitInclusiveIterator.toOption.match_1.eq_1 : ∀ {ρ : Type} {σ : String.Slice → Type} {pat : ρ} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  {s : String.Slice} (motive : String.Slice.SplitInclusiveIterator pat s → Sort u_1) (currPos : s.Pos)
  (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s))
  (h_1 :
    (currPos : s.Pos) →
      (s_2 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive (String.Slice.SplitInclusiveIterator.operating currPos s_2))
  (h_2 : Unit → motive String.Slice.SplitInclusiveIterator.atEnd),
  (match String.Slice.SplitInclusiveIterator.operating currPos s_1 with
    | String.Slice.SplitInclusiveIterator.operating currPos s => h_1 currPos s
    | String.Slice.SplitInclusiveIterator.atEnd => h_2 ()) =
    h_1 currPos s_1
-- Batteries.Data.String.Legacy
String.Pos.Raw.set.eq_1 : ∀ (x : String) (x_1 : String.Pos.Raw) (x_2 : Char),
  String.Pos.Raw.set x x_1 x_2 = String.ofList (String.Pos.Raw.utf8SetAux x_2 x.toList 0 x_1)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The braiding isomorphism is symmetric.  -/
CategoryTheory.Limits.coprod.symmetry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (P Q : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.braiding P Q).hom
      (CategoryTheory.Limits.coprod.braiding Q P).hom =
    CategoryTheory.CategoryStruct.id (P ⨿ Q)
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.identity_N₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂ ◫ AlgebraicTopology.DoldKan.N₂Γ₂.inv)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicTopology.DoldKan.N₂.associator AlgebraicTopology.DoldKan.Γ₂ AlgebraicTopology.DoldKan.N₂).inv
        (AlgebraicTopology.DoldKan.Γ₂N₂.natTrans ◫ CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂)) =
    CategoryTheory.CategoryStruct.id AlgebraicTopology.DoldKan.N₂
-- Mathlib.Order.Filter.Prod
Filter.map_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (m : α × β → γ) (f : Filter α) (g : Filter β),
  Filter.map m (f ×ˢ g) = (Filter.map (fun a b => m (a, b)) f).seq g
-- Mathlib.Data.NNReal.Defs
/-- **Alias** of `Real.toNNReal_natCast`. -/
Real.toNNReal_coe_nat : ∀ (n : ℕ), (↑n).toNNReal = ↑n
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_def_of_neg : ∀ {x : ℝ}, x < 0 → ∀ (y : ℝ), x ^ y = Real.exp (Real.log x * y) * Real.cos (y * Real.pi)
-- Mathlib.LinearAlgebra.Quotient.Pi
/-- Lift a family of maps to the direct sum of quotients.  -/
Submodule.piQuotientLift : {ι : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      {Ms : ι → Type u_3} →
        [inst_1 : (i : ι) → AddCommGroup (Ms i)] →
          [inst_2 : (i : ι) → Module R (Ms i)] →
            {N : Type u_4} →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  [Fintype ι] →
                    [DecidableEq ι] →
                      (p : (i : ι) → Submodule R (Ms i)) →
                        (q : Submodule R N) →
                          (f : (i : ι) → Ms i →ₗ[R] N) →
                            (∀ (i : ι), p i ≤ Submodule.comap (f i) q) → ((i : ι) → Ms i ⧸ p i) →ₗ[R] N ⧸ q
-- Init.Sym.Lemmas
Lean.Sym.cond_cond_eq_true : ∀ {α : Sort u} (c : Bool) (a b : α), c = true → (bif c then a else b) = a
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.coe_zsmul : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddGroup Y]
  (D : Function.locallyFinsuppWithin U Y) (n : ℤ), ⇑(n • D) = n • ⇑D
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.coeFn_comp_toFiniteMeasure_eq_coeFn : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (ν : MeasureTheory.ProbabilityMeasure Ω), ⇑ν.toFiniteMeasure = ⇑ν
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.msgToInteractive.fmtToTT : Array Lean.Widget.EmbedFmt✝ → Std.Format → ℕ → IO Lean.Widget.InteractiveMessage
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- A `DayConvolution` structure on functors `F G : C ⥤ V` is the data of
a functor `F ⊛ G : C ⥤ V`, along with a unit `F ⊠ G ⟶ tensor C ⋙ F ⊛ G`
that exhibits this functor as a pointwise left Kan extension of `F ⊠ G` along
`tensor C`. This is a `class` used to prove various properties of such extensions,
but registering global instances of this class is probably a bad idea.  -/
CategoryTheory.MonoidalCategory.DayConvolution : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {V : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [CategoryTheory.MonoidalCategory C] →
          [CategoryTheory.MonoidalCategory V] →
            CategoryTheory.Functor C V → CategoryTheory.Functor C V → Type (max (max (max u₁ u₂) v₁) v₂)