mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd'_assoc : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
  (h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃),
  CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯ ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂)
          (CategoryTheory.shiftFunctor C a₃) ≪≫
        (CategoryTheory.shiftFunctor C a₁).associator (CategoryTheory.shiftFunctor C a₂)
          (CategoryTheory.shiftFunctor C a₃) =
    CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯ ≪≫
      (CategoryTheory.shiftFunctor C a₁).isoWhiskerLeft (CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃)
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_withDensity_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ENNReal} (μ ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν],
  AEMeasurable f ν →
    (∀ᵐ (x : α) ∂ν, f x ≠ 0) →
      (∀ᵐ (x : α) ∂ν, f x ≠ ⊤) → μ.rnDeriv (ν.withDensity f) =ᵐ[ν] fun x => (f x)⁻¹ * μ.rnDeriv ν x
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.lift_of : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : IsFreeAddGroup G] {H : Type u_2} [inst_2 : AddGroup H]
  (f : IsFreeAddGroup.Generators G → H) (a : IsFreeAddGroup.Generators G),
  (IsFreeAddGroup.lift f) (IsFreeAddGroup.of a) = f a
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt32.size ≤ n → (UInt32.ofNatClamp n).toNat = UInt32.size - 1
-- Mathlib.Data.Part
Part.instZero.eq_1 : ∀ {α : Type u_1} [inst : Zero α], Part.instZero = { zero := pure 0 }
-- Lean.Message
Lean.MessageData.trace : Lean.TraceData → Lean.MessageData → Array Lean.MessageData → Lean.MessageData
-- Mathlib.Algebra.Order.Field.Basic
div_neg_of_neg_of_pos : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → 0 < b → a / b < 0
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mk.sizeOf_spec : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : SizeOf R] [inst_6 : SizeOf ι] [inst_7 : (a : ι) → SizeOf (M₁ a)] [inst_8 : SizeOf M₂]
  (toFun : ((i : ι) → M₁ i) → M₂)
  (map_update_add' :
    ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
      toFun (Function.update m i (x + y)) = toFun (Function.update m i x) + toFun (Function.update m i y))
  (map_update_smul' :
    ∀ [inst_9 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
      toFun (Function.update m i (c • x)) = c • toFun (Function.update m i x)),
  sizeOf { toFun := toFun, map_update_add' := map_update_add', map_update_smul' := map_update_smul' } = 1
-- Init.Control.Basic
/-- Lifts an action from the inner monad `m` to the outer monad `n`. The inner monad has access to a
reverse lifting operator that can run an `n` action, returning a value and state together.
 -/
MonadControlT.liftWith : {m : Type u → Type v} →
  {n : Type u → Type w} → [self : MonadControlT m n] → {α : Type u} → (({β : Type u} → n β → m (stM m n β)) → m α) → n α
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContinuousLinearEquiv.contDiffPointwiseHolderAt : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {k : ℕ} {α : ↑unitInterval} {a : E} (f : E ≃L[ℝ] F), ContDiffPointwiseHolderAt k α (⇑f) a
-- Mathlib.RepresentationTheory.Basic
/-- A representation of `G` on the `k`-module `V` is a homomorphism `G →* (V →ₗ[k] V)`.
 -/
Representation : (k : Type u_1) →
  (G : Type u_2) →
    (V : Type u_3) → [inst : Semiring k] → [Monoid G] → [inst_2 : AddCommMonoid V] → [Module k V] → Type (max u_2 u_3)
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.MorphismProperty.overEquivOfIsInitial_inverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C)
  [inst_1 : P.ContainsIdentities] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.RespectsIso]
  [inst_4 : CategoryTheory.Limits.HasStrictInitialObjects C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  (CategoryTheory.MorphismProperty.overEquivOfIsInitial.{w, v_1, u_1} P Q X h).inverse =
    CategoryTheory.Functor.fromPUnit (CategoryTheory.MorphismProperty.Over.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoc_of_ge : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ≤ a → Set.uIoc a b = Set.Ioc b a
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_Ioo : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [DenselyOrdered α],
  (Finset.Ioo a b).Nonempty ↔ a < b
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
instIsLocalHomZModRingHomOfIsLocalRingOfNontrivial : ∀ {R : Type u_4} [inst : CommRing R] [IsLocalRing R] {n : ℕ} [Nontrivial (ZMod n)] (f : R →+* ZMod n), IsLocalHom f
-- Mathlib.Topology.MetricSpace.Holder
holderWith_zero_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoMetricSpace X] [inst_1 : MetricSpace Y] {r : NNReal} {f : X → Y},
  HolderWith 0 r f ↔ ∀ (x₁ x₂ : X), f x₁ = f x₂
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => Unit} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List α} {k fallback : α},
      k ∈ m → (Std.DHashMap.Raw.Const.insertManyIfNewUnit m l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.Data.NNReal.Defs
NNReal.mk_zero : NNReal.mk 0 ⋯ = 0
-- Lean.Parser.Extension
Lean.Parser.isValidSyntaxNodeKind : Lean.Environment → Lean.SyntaxNodeKind → Bool
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
/-- The type (I) simplices of `h : A.PairingCore`, as a subset of `A.N`.  -/
SSet.Subcomplex.PairingCore.I : {X : SSet} → {A : X.Subcomplex} → A.PairingCore → Set A.N
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.mk : Lean.AttributeImpl →
  Lean.SimplePersistentEnvExtension (Lean.Name × Lean.Name) (Lean.NameMap Lean.Name) →
    Lean.ParserCompiler.CombinatorAttribute
-- Mathlib.Data.Seq.Computation
Computation.of_results_bind : ∀ {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {b : β} {k : ℕ},
  (s.bind f).Results b k → ∃ a m n, s.Results a m ∧ (f a).Results b n ∧ k = n + m
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.inclusion_self : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {S : NonUnitalStarSubalgebra R A},
  NonUnitalAlgHomClass.toNonUnitalAlgHom (NonUnitalStarSubalgebra.inclusion ⋯) = NonUnitalAlgHom.id R ↥S
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castSucc_Ico : ∀ {n : ℕ} (i j : Fin n), Fin.castSucc '' Set.Ico i j = Set.Ico i.castSucc j.castSucc
-- Mathlib.Data.Set.Disjoint
Set.disjoint_iff_inter_eq_empty : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ s ∩ t = ∅
-- Mathlib.Combinatorics.Matroid.Basic
/-- For finite `E`, finitely many matroids have ground set contained in `E`.  -/
Matroid.finite_setOfPred_matroid : ∀ {α : Type u_1} {E : Set α}, E.Finite → {M | M.E ⊆ E}.Finite
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
/-- The constant presheaf functor is left adjoint to evaluation at a terminal object.  -/
CategoryTheory.constantPresheafAdj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (D : Type u_2) →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {T : C} →
          CategoryTheory.Limits.IsTerminal T →
            (CategoryTheory.Functor.const Cᵒᵖ ⊣ (CategoryTheory.evaluation Cᵒᵖ D).obj (Opposite.op T))
-- Mathlib.Algebra.Notation.Defs
VSub.ext_iff : ∀ {G : outParam (Type u_1)} {P : Type u_2} {x y : VSub G P}, x = y ↔ VSub.vsub = VSub.vsub
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- The nonsingular inverse of `A` is a left inverse.  -/
Matrix.nonsing_inv_mul : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  IsUnit A.det → A⁻¹ * A = 1
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.coe_addLeft : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableAdd G] (g : G),
  ⇑(MeasurableEquiv.addLeft g) = fun x => g + x
-- Mathlib.Topology.Sheaves.Presheaf
/-- The natural isomorphism between
the pushforward of a presheaf along the composition of two continuous maps and
the corresponding pushforward of a pushforward.  -/
TopCat.Presheaf.Pushforward.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : TopCat} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          (ℱ : TopCat.Presheaf C X) →
            (TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.comp f g)).obj ℱ ≅
              (TopCat.Presheaf.pushforward C g).obj ((TopCat.Presheaf.pushforward C f).obj ℱ)
-- Mathlib.Control.Random
/-- `BoundedRandom m α` gives us machinery to generate values of type `α` between certain bounds in
the monad `m`.  -/
BoundedRandom : (Type u → Type u_1) → (α : Type u) → [Preorder α] → Type (max (max 1 u) u_1)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.ofRestrict_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {U : TopCat} (X : AlgebraicGeometry.PresheafedSpace C)
  (f : U ⟶ ↑X) (hf : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)),
  CategoryTheory.Mono (X.ofRestrict hf)
-- Lean.Data.PrefixTree
Lean.instInhabitedPrefixTreeNode : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → Inhabited (Lean.PrefixTreeNode α β cmp)
-- Aesop.RuleSet
Aesop.BaseRuleSet.contains : Aesop.BaseRuleSet → Aesop.RuleName → Bool
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.pushout_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f] (x : CategoryTheory.Under X) {x' : CategoryTheory.Under X}
  {u : x ⟶ x'},
  (CategoryTheory.Under.pushout f).map u =
    CategoryTheory.Under.homMk
      (CategoryTheory.Limits.pushout.desc
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Under.Hom.right u)
          (CategoryTheory.Limits.pushout.inl x'.hom f))
        (CategoryTheory.Limits.pushout.inr x'.hom f) ⋯)
      ⋯
-- Std.Async.Process
/-- Number of block input operations (disk reads)
 -/
Std.IO.Process.ResourceUsageStats.blockInputOps : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerLeft_whiskerLeft_assoc : ∀ (A : Type u_1) {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor B C) {G H : CategoryTheory.Functor C D}
  (η : G ⟶ H) {Z : CategoryTheory.Functor (CategoryTheory.Join A B) (CategoryTheory.Join A D)}
  (h : CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) (F.comp H) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) (F.whiskerLeft η)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A F G).hom
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).whiskerLeft
          (CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) η))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A F H).inv h))
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.sign_mul_self_eq_abs : ∀ (a : ℤ), a.sign * a = |a|
-- Std.Sat.AIG.RelabelNat
/-- The basic initial state.
 -/
Std.Sat.AIG.RelabelNat.State.empty : {α : Type} →
  [inst : DecidableEq α] →
    [inst_1 : Hashable α] → {decls : Array (Std.Sat.AIG.Decl α)} → Std.Sat.AIG.RelabelNat.State α decls 0
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.le_limsup_mul : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal},
  (∃ᶠ (x : α) in f, 0 ≤ u x) → 0 ≤ᶠ[f] v → Filter.limsup u f * Filter.liminf v f ≤ Filter.limsup (u * v) f
-- Mathlib.Analysis.Asymptotics.Defs
/-- Eta-expanded form of `Asymptotics.IsBigO.sum` -/
Asymptotics.IsBigO.fun_sum : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {ι : Type u_18} {A : ι → α → E'} {s : Finset ι},
  (∀ i ∈ s, A i =O[l] g) → (fun a => ∑ c ∈ s, A c a) =O[l] g
-- Mathlib.CategoryTheory.Limits.Lattice
CategoryTheory.Limits.CompleteLattice.limitCone_cone_π_app : ∀ {α : Type u} [inst : CompleteLattice α] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J α) (x : J),
  (CategoryTheory.Limits.CompleteLattice.limitCone F).cone.π.app x = CategoryTheory.homOfLE ⋯
-- Lean.SubExpr
Lean.SubExpr.GoalLocation.hyp.inj : ∀ {a a_1 : Lean.FVarId}, Lean.SubExpr.GoalLocation.hyp a = Lean.SubExpr.GoalLocation.hyp a_1 → a = a_1
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.comp_τl_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {a_1 b_1 c : a ⟶ b}
  (x : CategoryTheory.Bicategory.Adj.Hom₂ a_1 b_1) (y : CategoryTheory.Bicategory.Adj.Hom₂ b_1 c) {Z : a.obj ⟶ b.obj}
  (h : c.l ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp x y).τl h =
    CategoryTheory.CategoryStruct.comp x.τl (CategoryTheory.CategoryStruct.comp y.τl h)
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.MaxProducts.congr_simp : ∀ {I : Type u} (C C_1 : Set (I → Bool)),
  C = C_1 →
    ∀ [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o o_1 : Ordinal.{u}} (e_o : o = o_1)
      (ho : o < Ordinal.type fun x1 x2 => x1 < x2) (a a_1 : Profinite.NobelingProof.Products I),
      a = a_1 →
        Profinite.NobelingProof.GoodProducts.MaxProducts C ho a =
          Profinite.NobelingProof.GoodProducts.MaxProducts C_1 ⋯ a_1
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_eq_zero : ∀ {α : Type u_1} [inst : Zero α] {a : Lex α}, ofLex a = 0 ↔ a = 0
-- Mathlib.Data.Multiset.Fintype
Multiset.forall_coe : ∀ {α : Type u_1} [inst : DecidableEq α] {m : Multiset α} (p : m.ToType → Prop),
  (∀ (x : m.ToType), p x) ↔ ∀ (x : α) (i : Fin (Multiset.count x m)), p ⟨x, i⟩
-- Mathlib.Algebra.Module.Submodule.Map
/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective.  -/
Submodule.gciMapComap : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [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 : RingHomSurjective σ₁₂] →
                        {f : M →ₛₗ[σ₁₂] M₂} →
                          Function.Injective ⇑f → GaloisCoinsertion (Submodule.map f) (Submodule.comap f)
-- Mathlib.CategoryTheory.Monoidal.Center
/-- The forgetful monoidal functor from the Drinfeld center to the original category.  -/
CategoryTheory.Center.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Functor (CategoryTheory.Center C) C
-- Mathlib.Logic.Encodable.Basic
/-- `ULower α : Type` is an equivalent type in the lowest universe, given `Encodable α`.  -/
ULower : (α : Type u_1) → [Encodable α] → Type
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.CountablyGenerated.comap : ∀ {α : Type u_1} {β : Type u_2} [m : MeasurableSpace β] [h : MeasurableSpace.CountablyGenerated β] (f : α → β),
  MeasurableSpace.CountablyGenerated α
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Functional equation for the even Hurwitz zeta function with poles removed.  -/
HurwitzZeta.completedHurwitzZetaEven₀_one_sub : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedHurwitzZetaEven₀ a (1 - s) = HurwitzZeta.completedCosZeta₀ a s
-- Mathlib.RingTheory.PowerSeries.Basic
/-- The `n`th coefficient of a formal power series.  -/
PowerSeries.coeff : {R : Type u_1} → [inst : Semiring R] → ℕ → PowerSeries R →ₗ[R] R
-- Init.Data.Range.Polymorphic.RangeIterator
/-- An efficient `IteratorLoop` instance:
As long as the compiler cannot optimize away the `Option` in the internal state, we use a special
loop implementation.
 -/
Std.Rxc.Iterator.instIteratorLoop : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LE α] →
      [inst_2 : DecidableLE α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLE α] →
            {n : Type u → Type w} → [Monad n] → Std.IteratorLoop (Std.Rxc.Iterator α) Id n
-- Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm
_private.Mathlib.Analysis.Normed.Unbundled.SmoothingSeminorm.0.mu.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (μ : RingSeminorm R) {x y : R}
  (hn : ∀ (n : ℕ), ∃ m < n + 1, μ ((x + y) ^ n) ^ (1 / ↑n) ≤ (μ (x ^ m) * μ (y ^ (n - m))) ^ (1 / ↑n)) (n : ℕ),
  mu✝ μ hn n = Classical.choose ⋯
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioc_sub_one_sub_one_eq_Ico_of_not_isMin : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] {a : α},
  ¬IsMin a → ∀ (b : α), Set.Ioc (a - 1) (b - 1) = Set.Ico a b
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.sub_of_indepFun : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X Y : Ω → ℝ} {cX cY : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X cX μ →
    ProbabilityTheory.HasSubgaussianMGF Y cY μ →
      ProbabilityTheory.IndepFun X Y μ → ProbabilityTheory.HasSubgaussianMGF (fun ω => X ω - Y ω) (cX + cY) μ
-- Mathlib.Data.Set.Monotone
Monotone.codRestrict : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {s : Set β} (hs : ∀ (x : α), f x ∈ s), Monotone (Set.codRestrict f s hs)
-- Mathlib.Analysis.InnerProductSpace.Calculus
ContDiffAt.norm_sq : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
  [inst : NormedSpace ℝ E] {G : Type u_4} [inst_2 : NormedAddCommGroup G] [inst_3 : NormedSpace ℝ G] {f : G → E} {x : G}
  {n : WithTop ℕ∞}, ContDiffAt ℝ n f x → ContDiffAt ℝ n (fun x => ‖f x‖ ^ 2) x
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.brecOn : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} {inst : BEq α} {inst_1 : Hashable α} {a : Std.DHashMap.Raw α β} (t : a.WF),
  (∀ {β : α → Type v} [inst : BEq α] [inst_2 : Hashable α] (a : Std.DHashMap.Raw α β) (t : a.WF),
      Std.DHashMap.Raw.WF.below t → motive a t) →
    motive a t
-- Mathlib.Analysis.SumIntegralComparisons
AntitoneOn.tsum_comp_add_le_integral : ∀ {f : ℝ → ℝ} (N : ℕ),
  AntitoneOn f (Set.Ici ↑N) →
    MeasureTheory.IntegrableOn f (Set.Ioi ↑N) MeasureTheory.volume →
      (∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) → ∑' (n : ℕ), f ↑(n + N + 1) ≤ ∫ (x : ℝ) in Set.Ioi ↑N, f x
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- If `G` preserves limits, we have an isomorphism from the image of a product to the product of the
images.
 -/
CategoryTheory.Limits.PreservesProduct.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              [inst_2 : CategoryTheory.Limits.HasProduct f] →
                [inst_3 : CategoryTheory.Limits.HasProduct fun j => G.obj (f j)] →
                  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G] →
                    G.obj (∏ᶜ f) ≅ ∏ᶜ fun j => G.obj (f j)
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Iic b` and antitone on `Icc b a`, then the maximum of `f` on `Iic a`
is attained at `b`.  -/
isMaxOn_Iic_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  MonotoneOn f (Set.Iic b) → AntitoneOn f (Set.Icc b a) → IsMaxOn f (Set.Iic a) b
-- Mathlib.Algebra.Group.Pi.Lemmas
Sigma.curry_one : ∀ {α : Type u_5} {β : α → Type u_6} {γ : (a : α) → β a → Type u_7} [inst : (a : α) → (b : β a) → One (γ a b)],
  Sigma.curry 1 = 1
-- Init.Data.SInt.Lemmas
Int32.le_antisymm : ∀ {a b : Int32}, a ≤ b → b ≤ a → a = b
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.iIndepFun.charFunDual_map_fun_finsetSum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : NormedSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω => ∑ i ∈ s, X i ω) P) =
        ∏ i ∈ s, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P)
-- Mathlib.Data.Nat.MaxPowDiv
padicValNat_zero_left : ∀ (n : ℕ), padicValNat 0 n = 0
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M` and a map of
`AddCommMonoid`s `g : M →+ P` such that `g(S) ⊆ AddUnits P`, `f x = f y → g x = g y`
for all `x y : M`.  -/
AddSubmonoid.LocalizationMap.eq_of_eq : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P},
  (∀ (y : ↥S), IsAddUnit (g ↑y)) → ∀ {x y : M}, f x = f y → g x = g y
-- Mathlib.RingTheory.Finiteness.Basic
/-- The top submodule of another submodule `N` is FG iff `N` is `FG`.

See also `Module.Finite.fg_top`.  -/
Submodule.fg_top : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N : Submodule R M), ⊤.FG ↔ N.FG
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ιOfLE_ε : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsMonoidal] {P' : CategoryTheory.ObjectProperty C}
  [inst_3 : P'.IsMonoidal] (h : P ≤ P'),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.ObjectProperty.ιOfLE h) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit P'.FullSubcategory)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_epi : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [CategoryTheory.Limits.HasZeroObject C],
  S.g = 0 → (S.Exact ↔ CategoryTheory.Epi S.f)
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.instCoeFunForallPrototile : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] → CoeFun (DiscreteTiling.Protoset G X ιₚ) fun x => ιₚ → DiscreteTiling.Prototile G X
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_zero : ∀ (x : ℕ), x &&& 0 = 0
-- Mathlib.RingTheory.MvPolynomial.FreeCommRing
FirstOrder.Ring.mvPolynomialSupportLEEquiv.eq_1 : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_3} [inst : DecidableEq κ] [inst_1 : CommRing R] [inst_2 : DecidableEq R]
  (monoms : ι → Finset (κ →₀ ℕ)),
  FirstOrder.Ring.mvPolynomialSupportLEEquiv monoms =
    { toFun := fun p i => MvPolynomial.coeff (↑i.snd) (↑p i.fst),
      invFun := fun p =>
        ⟨fun i =>
          AddMonoidAlgebra.ofCoeff
            { support := {m ∈ monoms i | ∃ (hm : m ∈ monoms i), p ⟨i, ⟨m, hm⟩⟩ ≠ 0},
              toFun := fun m => if hm : m ∈ monoms i then p ⟨i, ⟨m, hm⟩⟩ else 0, mem_support_toFun := ⋯ },
          ⋯⟩,
      left_inv := ⋯, right_inv := ⋯ }