mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj₂.eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β},
  Function.Semiconj₂ f ga gb → ∀ (x y : α), f (ga x y) = gb (f x) (f y)
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {len : ℕ} → aig.RefVec len → aig.RefVec len → aig.BinaryRefVec len
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.close : {α : Type} → Std.Bounded✝ α → EIO Std.Broadcast.Error Unit
-- Mathlib.Analysis.Meromorphic.Basic
/-- `MeromorphicAt` is invariant under translation.  -/
meromorphicAt_comp_sub_const_iff_meromorphicAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x c : 𝕜} {f : 𝕜 → E}, MeromorphicAt (f ∘ fun x => x - c) x ↔ MeromorphicAt f (x - c)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.continuousLinearEquivAt_symm_apply : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] (b : B)
  (hb : b ∈ e.baseSet), ⇑(Bundle.Trivialization.continuousLinearEquivAt R e b hb).symm = e.symm b
-- Init.Data.UInt.Lemmas
UInt8.ofNat.eq_1 : ∀ (n : ℕ), UInt8.ofNat n = { toBitVec := BitVec.ofNat 8 n }
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- **Alias** of `four_mul_le_sq_add`.

---

Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
(aka AM-GM inequality) for linearly ordered commutative semirings.  -/
four_mul_le_pow_two_add : ∀ {R : Type u} [inst : CommSemiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddLeftReflectLE R] [AddLeftMono R] (a b : R), 4 * a * b ≤ (a + b) ^ 2
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- Consider the differential of the inclusion of the sphere in `E` at the point `v` as a continuous
linear map from `TangentSpace (𝓡 n) v` to `E`.  This map is injective.  -/
injective_mvfderiv_subtypeVal_sphere : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [inst_2 : Fact (Module.finrank ℝ E = n + 1)] (v : ↑(Metric.sphere 0 1)), Function.Injective ⇑(d% Subtype.val v)
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
le_iff_forall_one_lt_le_mul : ∀ {α : Type u} [inst : LinearOrder α] [DenselyOrdered α] [inst_2 : Monoid α] [ExistsMulOfLE α] [MulLeftReflectLT α]
  {a b : α} [MulLeftStrictMono α], a ≤ b ↔ ∀ (ε : α), 1 < ε → a ≤ b * ε
-- Mathlib.Algebra.BigOperators.Associated
Associates.rel_associated_iff_map_eq_map : ∀ {M : Type u_2} [inst : CommMonoid M] {p q : Multiset M},
  Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_eq_one_of_infinite : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α},
  (s ∩ Function.mulSupport f).Infinite → ∏ᶠ (i : α) (_ : i ∈ s), f i = 1
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanModuleHierarchyImportsParams.fromJson : Lean.Json → Except String Lean.Lsp.LeanModuleHierarchyImportsParams
-- Mathlib.Util.PrintSorries
/-- The set of already visited declarations.  -/
Mathlib.PrintSorries.State.visited : Mathlib.PrintSorries.State → Lean.NameSet
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHAddOffset_1 : HAdd Std.Time.PlainTime Std.Time.Millisecond.Offset Std.Time.PlainTime
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.hasInv : {l : Type u_1} →
  {R : Type u_2} →
    [inst : DecidableEq l] → [inst_1 : Fintype l] → [inst_2 : CommRing R] → Inv ↥(Matrix.symplecticGroup l R)
-- Init.Data.List.Nat.Modify
List.drop_modify_of_ge : ∀ {α : Type u_1} (f : α → α) (i j : ℕ) (l : List α),
  i ≥ j → List.drop j (l.modify i f) = (List.drop j l).modify (i - j) f
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_closure : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V]
  [inst_11 : TopologicalSpace P] [IsTopologicalAddTorsor P] (s : Set P),
  asymptoticCone k (closure s) = asymptoticCone k s
-- Init.Data.List.Zip
List.zip_of_prod : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {l' : List β} {xs : List (α × β)},
  List.map Prod.fst xs = l → List.map Prod.snd xs = l' → xs = l.zip l'
-- Mathlib.Combinatorics.Graph.Delete
/-- Restrict `G : Graph α β` to the edges in a set `E₀` without removing vertices  -/
Graph.restrict : {α : Type u_1} → {β : Type u_2} → Graph α β → Set β → Graph α β
-- Mathlib.Data.Multiset.Functor
Multiset.bind_def : ∀ {α β : Type u_1}, (fun x1 x2 => x1 >>= x2) = Multiset.bind
-- Lean.Parser.Term
Lean.Parser.Term.noImplicitLambda.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f} [inst_1 : SizeOf C]
  [inst_2 : SizeOf ι] (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂))) =
          CategoryTheory.CategoryStruct.comp (hom i₁) (D₂.hom i₁ i₂))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1
-- Mathlib.Topology.Instances.ENNReal.ENatENNReal
ENat.continuous_toENNReal : Continuous ENat.toENNReal
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] {s : Finset ι}
  {x : (i : ↑↑s) → β ↑i} {i : ι}, (DFinsupp.mk s x) i = if H : i ∈ s then x ⟨i, H⟩ else 0
-- Mathlib.Analysis.Convex.Cone.TensorProduct
/-- If a pointed cone `C` is contained in the conic hull of a basis `b`, then the coordinate
functionals of `b` lie in the dual cone of `C`.  -/
PointedCone.basis_coord_mem_dual : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} (b : Module.Basis ι R M) (C : PointedCone R M),
  ↑C ⊆ ↑(PointedCone.hull R (Set.range ⇑b)) → ∀ (i : ι), b.coord i ∈ PointedCone.dual (Module.Dual.eval R M) ↑C
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalOpposite.mopFunctor_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.mopFunctor C) X Y = (β_ { unmop := X } { unmop := Y }).hom
-- Mathlib.Probability.ProbabilityMassFunction.Basic
/-- Since every set is Carathéodory-measurable under `PMF.toOuterMeasure`,
we can further extend this `OuterMeasure` to a `Measure` on `α`.  -/
PMF.toMeasure : {α : Type u_1} → [inst : MeasurableSpace α] → PMF α → MeasureTheory.Measure α
-- Mathlib.Data.Finsupp.SMul
/-- A version of `Finsupp.sum_smul_index'` for bundled additive maps.  -/
Finsupp.sum_smul_index_addMonoidHom : ∀ {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N]
  [inst_2 : SMulZeroClass R M] {g : α →₀ M} {b : R} {h : α → M →+ N},
  ((b • g).sum fun a => ⇑(h a)) = g.sum fun i c => (h i) (b • c)
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
IsDiscreteValuationRing.idealOrderIsoENat.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R],
  IsDiscreteValuationRing.idealOrderIsoENat R = IsDiscreteValuationRing.idealOrderIsoENat R
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_apply_ne_one : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M} {a : α},
  s.mulIndicator f a ≠ 1 ↔ a ∈ s ∩ Function.mulSupport f
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.nhdsOrderEmbedding_apply : ∀ {R : Type u} [inst : CommSemiring R] (x : PrimeSpectrum R), PrimeSpectrum.nhdsOrderEmbedding x = nhds x
-- Init.Data.UInt.Lemmas
UInt32.ofNatClamp.eq_1 : ∀ (n : ℕ),
  UInt32.ofNatClamp n =
    if h : n < UInt32.size then UInt32.ofNatLT n h else UInt32.ofNatLT (UInt32.size - 1) UInt32.ofNatClamp._proof_1
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive monoid, if it admits an
injective map that preserves `0` and `+` to an additive monoid. See note
[reducible non-instances].  -/
Function.Injective.addMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : AddMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 0 = 0 →
                  (∀ (x y : M₁), f (x + y) = f x + f y) → (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddMonoid M₁
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
/-- Given a splitting `s` of a simplicial object `X` in a preadditive category,
this is the split epimorphism from the alternating face map complex of `X` to the chain
complex `s.nondegComplex`.  -/
CategoryTheory.SimplicialObject.Splitting.toNondegComplex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (s : X.Splitting) →
        [inst_1 : CategoryTheory.Preadditive C] → AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ s.nondegComplex
-- Batteries.Data.String.Lemmas
String.endPos_asString : ∀ (cs : List Char), (String.ofList cs).rawEndPos = { byteIdx := String.utf8Len cs }
-- Init.Grind.Util
/-- A helper gadget for annotating nested decidable instances in goals.  -/
Lean.Grind.nestedDecidable : {p : Prop} → Decidable p → Decidable p
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_nsmul : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {M₁ M₂ : TopModuleCat R} (n : ℕ) (φ : M₁ ⟶ M₂),
  TopModuleCat.Hom.hom (n • φ) = n • TopModuleCat.Hom.hom φ
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.MonoOver.bot_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.InitialMonoClass C] {X : C}, ⊥.arrow = CategoryTheory.Limits.initial.to X
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.lmul'_comp_includeLeft : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  (Algebra.TensorProduct.lmul' R).comp Algebra.TensorProduct.includeLeft = AlgHom.id R S
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_iSup_prop : ∀ {G : Type u_1} [inst : AddGroup G] {p : Prop} {K : p → AddSubgroup G} {x : G},
  x ∈ ⨆ (h : p), K h ↔ x = 0 ∨ ∃ (h : p), x ∈ K h
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_mul : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M N : Matrix n n R),
  (M * N).det = M.det * N.det
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableWithinAt_finCons : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {n : ℕ} {F' : Fin n.succ → Type u_6}
  [inst_3 : (i : Fin n.succ) → NormedAddCommGroup (F' i)] [inst_4 : (i : Fin n.succ) → NormedSpace 𝕜 (F' i)]
  {φ : E → F' 0} {φs : E → (i : Fin n) → F' i.succ},
  DifferentiableWithinAt 𝕜 (fun x => Fin.cons (φ x) (φs x)) s x ↔
    DifferentiableWithinAt 𝕜 φ s x ∧ DifferentiableWithinAt 𝕜 φs s x
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.map_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)} (α : F₁ ⟶ F₂),
  (CategoryTheory.CategoryOfElements.map α).comp (CategoryTheory.CategoryOfElements.π F₂) =
    CategoryTheory.CategoryOfElements.π F₁
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Submonoid.subsemiringClosure_coe : ∀ {R : Type u} [inst : NonAssocSemiring R] (M : Submonoid R), ↑M.subsemiringClosure = ↑(AddSubmonoid.closure ↑M)
-- Mathlib.Data.LawfulXor.Equiv
Equiv.xor_trans_xor : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [inst_2 : LawfulXor α] {a b : α},
  Equiv.trans (Equiv.xor b) (Equiv.xor a) = Equiv.xor (a ^^^ b)
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.coe_zero`. -/
AddAut.coe_one : ∀ (M : Type u_2) [inst : Add M], ⇑0 = id
-- Lean.Parser.Term
Lean.Parser.Command.versoCommentBody : Lean.Parser.Parser
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instUpwardEnumerable : {n : ℕ} → Std.PRange.UpwardEnumerable (BitVec n)
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.extend₂.eq_1 : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [inst_2 : UniformSpace γ] (f : α → β → γ),
  pkg.extend₂ pkg' f = Function.curry ((pkg.prod pkg').extend (Function.uncurry f))
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_one : Nat.fib 1 = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.compIso.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) {Z : C} (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasEqualizers C] [inst_2 : CategoryTheory.Limits.HasImage f]
  [inst_3 : CategoryTheory.IsIso g], CategoryTheory.Limits.image.compIso f g = CategoryTheory.Limits.image.compIso f g
-- Init.Data.UInt.Lemmas
UInt8.toUSize_ofNatLT : ∀ {n : ℕ} (h : n < UInt8.size), (UInt8.ofNatLT n h).toUSize = USize.ofNatLT n ⋯
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.instInfSet.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M],
  AddSubmonoid.instInfSet = { sInf := fun s => { carrier := ⋂ t ∈ s, ↑t, add_mem' := ⋯, zero_mem' := ⋯ } }
-- Mathlib.Algebra.Polynomial.Div
Polynomial.eval_divByMonic_eq_trailingCoeff_comp : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  Polynomial.eval t (p /ₘ (Polynomial.X - Polynomial.C t) ^ Polynomial.rootMultiplicity t p) =
    (p.comp (Polynomial.X + Polynomial.C t)).trailingCoeff
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
IntermediateField.splits_of_splits : ∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {p : Polynomial K}
  {F : IntermediateField K L},
  (Polynomial.map (algebraMap K L) p).Splits → (∀ x ∈ p.rootSet L, x ∈ F) → (Polynomial.map (algebraMap K ↥F) p).Splits
-- Mathlib.CategoryTheory.Grothendieck
/-- Applying a functor `G : D ⥤ C` to the base of the Grothendieck construction induces a functor
`Grothendieck (G ⋙ F) ⥤ Grothendieck F`.  -/
CategoryTheory.Grothendieck.pre : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} D] →
        (F : CategoryTheory.Functor C CategoryTheory.Cat) →
          (G : CategoryTheory.Functor D C) →
            CategoryTheory.Functor (CategoryTheory.Grothendieck (G.comp F)) (CategoryTheory.Grothendieck F)
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.fvar : Lean.FVarId → ℕ → Lean.Meta.DiscrTree.Key
-- Mathlib.RingTheory.Localization.FractionRing
/-- If `A` is a commutative ring with fraction field `K`, `L` is a field, `g : A →+* L` lifts to
`f : K →+* L`, then the image of `f` is the subfield generated by the image of `g`.  -/
IsFractionRing.ringHom_fieldRange_eq_of_comp_eq : ∀ {A : Type u_4} [inst : CommRing A] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  {L : Type u_8} [inst_4 : Field L] {g : A →+* L} {f : K →+* L},
  f.comp (algebraMap A K) = g → f.fieldRange = Subfield.closure ↑g.range
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_iff_isSome_utf8DecodeChar?_copy : ∀ {s : String.Slice} {p : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice s p ↔ p = s.rawEndPos ∨ (s.copy.toByteArray.utf8DecodeChar? p.byteIdx).isSome = true
-- Mathlib.Analysis.MeanInequalities
/-- **Minkowski inequality**: the `L_p` seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
exist. A version for `NNReal`-valued functions. For an alternative version, convenient if the
infinite sums are already expressed as `p`-th powers, see `Lp_add_le_hasSum_of_nonneg`.  -/
NNReal.Lp_add_le_tsum : ∀ {ι : Type u} {f g : ι → NNReal} {p : ℝ},
  1 ≤ p →
    (Summable fun i => f i ^ p) →
      (Summable fun i => g i ^ p) →
        (Summable fun i => (f i + g i) ^ p) ∧
          (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.range_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {ι : Sort u_5} (a : α) (f : ι → β),
  (Set.range fun i => a • f i) = a • Set.range f
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The second inclusion of a binary cofan.  -/
CategoryTheory.Limits.BinaryCofan.inr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (s : CategoryTheory.Limits.BinaryCofan X Y) →
        (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right } ⟶
          ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj
            { as := CategoryTheory.Limits.WalkingPair.right }
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.Monad C) [inst_1 : SizeOf C] (of : C),
  sizeOf { of := of } = 1 + sizeOf of
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
AlternatingMap.mkContinuousLinear_norm_le : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (f : F →ₗ[𝕜] E [⋀^ι]→ₗ[𝕜] G) {C : ℝ},
  0 ≤ C → ∀ (H : ∀ (x : F) (m : ι → E), ‖(f x) m‖ ≤ C * ‖x‖ * ∏ i, ‖m i‖), ‖AlternatingMap.mkContinuousLinear f C H‖ ≤ C
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂)
  (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁),
  (CategoryTheory.Pretriangulated.completeDistinguishedTriangleMorphism T₁ T₂ hT₁ hT₂ a b comm).hom₁ = a
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_erase0 : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)}
  (s : Lean.Grind.AC.Seq), Lean.Grind.AC.Seq.denote ctx s.erase0 = Lean.Grind.AC.Seq.denote ctx s
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subLeft_eq_neg_trans_addLeft : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), Equiv.subLeft a = Equiv.trans (Equiv.neg G) (Equiv.addLeft a)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
/-- If `K` is an `n`-th cyclotomic extension of `ℚ`, then there are `φ n / n` complex places
of `K`. Note that this uses `1 / 2 = 0` in the cases `n = 1, 2`.  -/
IsCyclotomicExtension.Rat.nrComplexPlaces_eq_totient_div_two : ∀ (n : ℕ) [NeZero n] (K : Type u) [inst : Field K] [inst_1 : CharZero K] [h : IsCyclotomicExtension {n} ℚ K],
  NumberField.InfinitePlace.nrComplexPlaces K = n.totient / 2
-- Std.Async.TCP
/-- Binds the server socket to the specified address. Address reuse is enabled to allow rebinding the
same address.
 -/
Std.Async.TCP.Socket.Client.bind : Std.Async.TCP.Socket.Client → Std.Net.SocketAddress → IO Unit
-- Mathlib.Data.Set.NAry
Set.image2_singleton_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {t : Set β} {a : α}, Set.image2 f {a} t = f a '' t
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.inv_algebraMap : ∀ {R : Type u_3} {A : Type u_4} [inst : Semifield R] [inst_1 : Semifield A] [inst_2 : Algebra R A] {r s : R},
  r⁻¹ = s → ((algebraMap R A) r)⁻¹ = (algebraMap R A) s
-- Init.Data.Float.Model.Float32
/-- Compute the square root of a `Float32.Model`.
 -/
Float32.Model.sqrt : Float32.Model → Float32.Model
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp}
  {k k' : α} {f : β → β} {hc : k' ∈ Std.DTreeMap.Const.modify t k f},
  Std.DTreeMap.Const.get (Std.DTreeMap.Const.modify t k f) k' hc =
    if heq : cmp k k' = Ordering.eq then f (Std.DTreeMap.Const.get t k ⋯) else Std.DTreeMap.Const.get t k' ⋯
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.instSMulCommClass_circle_left : SMulCommClass Circle Complex.UnitDisc Complex.UnitDisc
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.instCompl : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} → [inst_1 : Ring M] → [inst_2 : Module M X] → Compl { f // IsLprojection X f }
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Precoverage.toCoverage_le_toCoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.HasPullbacks] [inst_2 : J.IsStableUnderBaseChange] (K : CategoryTheory.GrothendieckTopology C),
  (J.toCoverage ≤ K.toCoverage) = ∀ ⦃X : C⦄, ∀ S ∈ J.coverings X, CategoryTheory.Sieve.generate S ∈ K X
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The zero morphism of an additive monoid object.  -/
CategoryTheory.AddMonObj.termζ : Lean.ParserDescr
-- Mathlib.RingTheory.Kaehler.Basic
/-- For an `R`-derivation `S → M`, this is the map `S ⊗[R] S →ₗ[S] M` sending `s ⊗ₜ t ↦ s • D t`.  -/
Derivation.tensorProductTo : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {M : Type u_1} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] → [IsScalarTower R S M] → Derivation R S M → TensorProduct R S S →ₗ[S] M
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity holds if and only if all non-negative distances are proportional.  -/
similar_iff_exists_nndist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
-- Lean.Widget.InteractiveCode
Lean.Widget.SubexprInfo.withDiffTag : Lean.Widget.DiffTag → Lean.Widget.SubexprInfo → Lean.Widget.SubexprInfo
-- Mathlib.Analysis.InnerProductSpace.Basic
coe_innerₛₗ_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v : E), ⇑((innerₛₗ 𝕜) v) = fun w => inner 𝕜 v w