mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_insertEntry_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β},
  Std.Internal.List.getValue k (Std.Internal.List.insertEntry k v l) ⋯ = v
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_half_eq_neg_sqrt : ∀ {x : ℝ}, -(2 * Real.pi) ≤ x → x ≤ 0 → Real.sin (x / 2) = -√((1 - Real.cos x) / 2)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- An embedding of the edges of a bipartite graph into the edges of the complete bipartite graph  -/
SimpleGraph.IsBipartiteWith.edgeSetEmbeddingCompleteBipartiteGraph : {V : Type u_1} →
  {G : SimpleGraph V} →
    {s t : Set V} →
      [DecidableRel fun x1 x2 => x1 ∈ x2] → G.IsBipartiteWith s t → ↑G.edgeSet ↪ ↑(completeBipartiteGraph ↑s ↑t).edgeSet
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.coe_preimageHomeomorphFiber_symm_apply_coe_asIdeal : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R)
  (q : PrimeSpectrum (p.asIdeal.Fiber S)),
  ↑(↑((PrimeSpectrum.preimageHomeomorphFiber R S p).symm q)).asIdeal =
    ⇑Algebra.TensorProduct.includeRight ⁻¹' ↑q.asIdeal
-- Mathlib.RingTheory.Localization.Integer
IsLocalization.isInteger_add : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {a b : S},
  IsLocalization.IsInteger R a → IsLocalization.IsInteger R b → IsLocalization.IsInteger R (a + b)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.coe_sup : ∀ {E : Type u_3} [inst : AddGroup E] (p q : AddGroupSeminorm E), ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
-- Lean.Meta.Basic
/-- Given a user-facing name for a free variable, return the free variable or throw if not declared.  -/
Lean.Meta.getFVarFromUserName : Lean.Name → Lean.MetaM Lean.Expr
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack.eq_1 : ∀ (spec : Float.Model.Format) (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.unpack spec b =
    if Float.Model.UnpackedFloat.unpackExponent b = -1#spec.exponentBits then
      if Float.Model.UnpackedFloat.unpackMantissa b = 0#spec.mantissaBitsWithoutImplicit then
        Float.Model.UnpackedFloat.infinity
          (Float.Model.UnpackedFloat.Sign.ofBitVec (Float.Model.UnpackedFloat.unpackSign b))
      else Float.Model.UnpackedFloat.notANumber
    else
      if Float.Model.UnpackedFloat.unpackExponent b = 0#spec.exponentBits then
        if h : Float.Model.UnpackedFloat.unpackMantissa b = 0#spec.mantissaBitsWithoutImplicit then
          Float.Model.UnpackedFloat.zero
            (Float.Model.UnpackedFloat.Sign.ofBitVec (Float.Model.UnpackedFloat.unpackSign b))
        else
          Float.Model.UnpackedFloat.finite
            (Float.Model.UnpackedFloat.Sign.ofBitVec (Float.Model.UnpackedFloat.unpackSign b))
            (Float.Model.UnpackedFloat.unpackMantissa b).toNat
            (↑(Float.Model.UnpackedFloat.unpackExponent b).toNat -
                (↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit) +
              1)
            ⋯
      else
        Float.Model.UnpackedFloat.finite
          (Float.Model.UnpackedFloat.Sign.ofBitVec (Float.Model.UnpackedFloat.unpackSign b))
          (1#1 ++ Float.Model.UnpackedFloat.unpackMantissa b).toNat
          (↑(Float.Model.UnpackedFloat.unpackExponent b).toNat -
            (↑spec.exponentBias + ↑spec.mantissaBitsWithoutImplicit))
          ⋯
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_monomial_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ →₀ ℕ) (c : R),
  ((MvPolynomial.monomial s) c).totalDegree ≤ s.sum fun x => id
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sum_X_inr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S) (i : F.I₀), (E.sum F).X (Sum.inr i) = F.X i
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceOpcycles_exact._auto_1),
  (X.cokernelSequenceOpcycles f g n₀ n₁ hn₁).Exact
-- Mathlib.NumberTheory.EulerProduct.Basic
_private.Mathlib.NumberTheory.EulerProduct.Basic.0.instT0Space : ∀ {R : Type u_1} [inst : NormedCommRing R], T0Space R
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.toMeasure_ofFinset_apply : ∀ {α : Type u_1} {f : α → ENNReal} {s : Finset α} (h : ∑ a ∈ s, f a = 1) (h' : ∀ a ∉ s, f a = 0) (t : Set α)
  [inst : MeasurableSpace α], MeasurableSet t → (PMF.ofFinset f s h h').toMeasure t = ∑' (x : α), t.indicator f x
-- Lean.Parser.Command
Lean.Parser.Command.structCtor : Lean.Parser.Parser
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.InteractiveDiagnostic.toDiagnostic : Lean.Widget.InteractiveDiagnostic → Lean.Lsp.Diagnostic
-- Lean.Elab.ConfigEval.Basic
Lean.Elab.ConfigEval.ConfigItem.isAnonymous : Lean.Elab.ConfigEval.ConfigItem → Bool
-- Mathlib.ModelTheory.PartialEquiv
/-- The type of equivalences between finitely generated substructures.  -/
FirstOrder.Language.FGEquiv : (L : FirstOrder.Language) → (M : Type w) → (N : Type w') → [L.Structure M] → [L.Structure N] → Type (max 0 w w')
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_sub_eq_mk_left : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk a < ArchimedeanClass.mk b → ArchimedeanClass.mk (a - b) = ArchimedeanClass.mk a
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Frequently.expGrowthInf_le : ∀ {u : ℕ → ENNReal} {a : EReal}, (∃ᶠ (n : ℕ) in Filter.atTop, u n ≤ (a * ↑n).exp) → ExpGrowth.expGrowthInf u ≤ a
-- Mathlib.RingTheory.Polynomial.Chebyshev
_private.Mathlib.RingTheory.Polynomial.Chebyshev.0.Polynomial.Chebyshev.T.match_1.splitter : (motive : ℤ → Sort u_1) →
  (x : ℤ) →
    (Unit → motive 0) →
      (Unit → motive 1) → ((n : ℕ) → motive (Int.ofNat n.succ.succ)) → ((n : ℕ) → motive (Int.negSucc n)) → motive x
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits, then `F : C ⥤ D` preserves colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.op],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
CategoryTheory.presheafToSheaf.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] [inst_2 : CategoryTheory.HasWeakSheafify J A],
  CategoryTheory.presheafToSheaf J A = CategoryTheory.presheafToSheaf J A
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.constantCoeff_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (d : σ →₀ ℕ) (r : R),
  MvPolynomial.constantCoeff ((MvPolynomial.monomial d) r) = if d = 0 then r else 0
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_8 : ∀ (cf : Nat.Partrec.Code),
  cf.rfind'.eval =
    Nat.unpaired fun a m =>
      Part.map (fun x => x + m) (Nat.rfind fun n => (fun m => decide (m = 0)) <$> cf.eval (Nat.pair a (n + m)))
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.mapBinaryBicone_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C}
  (b : CategoryTheory.Limits.BinaryBicone X Y), (F.mapBinaryBicone b).fst = F.map b.fst
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.skipWhile_prop_eq_self_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos},
  pos.skipWhile P = pos ↔ ∀ (h : pos ≠ s.endPos), ¬P (pos.get h)
-- Mathlib.GroupTheory.Congruence.Defs
ConGen.Rel.below.mul : ∀ {M : Type u_1} [inst : Mul M] {r : M → M → Prop} {motive : (a a_1 : M) → ConGen.Rel r a a_1 → Prop} {w x y z : M}
  (a : ConGen.Rel r w x) (a_1 : ConGen.Rel r y z),
  ConGen.Rel.below a → motive w x a → ConGen.Rel.below a_1 → motive y z a_1 → ConGen.Rel.below ⋯
-- Init.Data.Vector.Lemmas
Vector.foldr_assoc : ∀ {α : Type u_1} {n : ℕ} {op : α → α → α} [ha : Std.Associative op] {xs : Vector α n} {a₁ a₂ : α},
  Vector.foldr op (op a₁ a₂) xs = op (Vector.foldr op a₁ xs) a₂
-- Mathlib.Tactic.IntervalCases
Int.add_one_le_of_not_le : ∀ {a b : ℤ}, ¬b ≤ a → a + 1 ≤ b
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply_coe : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (a : PrimeSpectrum (p.Fiber S)),
  ↑↑((RelIso.symm (PrimeSpectrum.primesOverOrderIsoFiber R S p)) a) = ⇑Algebra.TensorProduct.includeRight ⁻¹' ↑a.asIdeal
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_eq_isSome_getElem? : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = m[a]?.isSome
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- the second object of a triangle  -/
CategoryTheory.Pretriangulated.Triangle.obj₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] → CategoryTheory.Pretriangulated.Triangle C → C
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.div_const : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f : α → G}
  [MeasurableDiv G], Measurable f → ∀ (c : G), Measurable fun x => f x / c
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
PiLp.hasFDerivAt_toLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [Finite ι] (p : ENNReal)
  [Fact (1 ≤ p)] (f : (i : ι) → E i), HasFDerivAt (WithLp.toLp p) (↑(PiLp.continuousLinearEquiv p 𝕜 E).symm) f
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionTriggerKind.invoked.sizeOf_spec : sizeOf Lean.Lsp.CodeActionTriggerKind.invoked = 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Adds `y` as an occurrence of `x`.
That is, `x` occurs in `lowers[y]`, `uppers[y]`, or `dvdCnstrs[y]`.
 -/
Lean.Meta.Grind.Arith.Cutsat.addOcc : Int.Internal.Linear.Var → Int.Internal.Linear.Var → Lean.Meta.Grind.GoalM Unit
-- Lean.DocString.Extension
Lean.VersoModuleDocs.mk.inj : ∀ {snippets snippets_1 : Lean.PersistentArray Lean.VersoModuleDocs.Snippet},
  { snippets := snippets } = { snippets := snippets_1 } → snippets = snippets_1
-- Mathlib.Order.Lattice
sup_eq_and_inf_eq_iff : ∀ {α : Type u} [inst : Lattice α] {a b c : α}, a ⊔ b = c ∧ a ⊓ b = c ↔ a = c ∧ b = c
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.basisUnitLattice.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.basisUnitLattice K =
    (NumberField.Units.basisModTorsion K).map (NumberField.Units.logEmbeddingEquiv K)
-- Mathlib.Data.Set.Inclusion
/-- `inclusion` is the "identity" function between two subsets `s` and `t`, where `s ⊆ t`  -/
Set.inclusion : {α : Type u_1} → {s t : Set α} → s ⊆ t → ↑s → ↑t
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.coe_id : ∀ (A : Type u_2) [inst : Monoid A] [inst_1 : TopologicalSpace A], ⇑(ContinuousMonoidHom.id A) = id
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.trichotomy : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] (f : CauSeq α abs),
  f.Pos ∨ f.LimZero ∨ (-f).Pos
-- Init.PropLemmas
and_self_iff : ∀ {a : Prop}, a ∧ a ↔ a
-- Mathlib.Data.Nat.Factorization.Basic
/-- A product over `n.factorization` can be written as a product over `n.primeFactors`;  -/
Nat.prod_factorization_eq_prod_primeFactors : ∀ {n : ℕ} {β : Type u_1} [inst : CommMonoid β] (f : ℕ → ℕ → β),
  n.factorization.prod f = ∏ p ∈ n.primeFactors, f p (n.factorization p)
-- Mathlib.Order.FixedPoints
OrderHom.le_lfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, (∀ (b : α), f b ≤ b → a ≤ b) → a ≤ OrderHom.lfp f
-- Mathlib.Algebra.Group.Action.Defs
Commute.smul_left_iff : ∀ {G : Type u_3} {H : Type u_4} [inst : Group G] {g : G} [inst_1 : Mul H] [inst_2 : MulAction G H] [SMulCommClass G H H]
  [IsScalarTower G H H] {a b : H}, Commute (g • a) b ↔ Commute a b
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
MvQPF.Sigma.inst : {n : ℕ} → {A : Type u} → (F : A → TypeVec.{u} n → Type u) → [(α : A) → MvQPF (F α)] → MvQPF (MvQPF.Sigma F)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).op =
    (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.op X) (Opposite.op Y) (Opposite.op Z)).symm
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.abs : ∀ {f : ℝ → ℝ}, AkraBazziRecurrence.GrowsPolynomially f → AkraBazziRecurrence.GrowsPolynomially fun x => |f x|
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- The functor `π₀Functor : SSet.{u} ⥤ Type u` is the coequalizer
of the two face maps `δ (0 : Fin 2)` and `δ 1`, considered
as natural transformations.  -/
SSet.isColimitCoforkπ₀Functor : CategoryTheory.Limits.IsColimit SSet.coforkπ₀Functor
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_triangle_right`.  -/
hammingDist_triangle_right : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] (x y z : (i : ι) → β i),
  hammingDist x y ≤ hammingDist x z + hammingDist y z
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- Variant of `map_source`, stated in terms of subsets.  -/
PartialHomeomorph.image_source_subset : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  ↑e '' e.source ⊆ e.target
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
CategoryTheory.Limits.inl_comp_pushoutObjIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Limits.HasPushouts C] (f : F ⟶ G) (g : F ⟶ H) (d : D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (f.app d) (g.app d))
      (CategoryTheory.Limits.pushoutObjIso f g d).inv =
    (CategoryTheory.Limits.pushout.inl f g).app d
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.evaluation₁_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  CategoryTheory.Square.evaluation₁.obj sq = sq.X₁
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.ofList_nil : ∀ {α : Type u_1}, FreeMonoid.ofList [] = 1
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.s.eq_2 : ∀ (i : ℕ), LucasLehmer.s i.succ = LucasLehmer.s i ^ 2 - 2
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Geometry.Manifold.ChartedSpace
achart_def : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (x : M), achart H x = ⟨chartAt H x, ⋯⟩
-- Mathlib.Analysis.Convolution
/-- Compute `(f ⋆ g) x₀` if the support of the `f` is within `Metric.ball 0 R`, and `g` is constant
on `Metric.ball x₀ R`.

We can simplify the RHS further if we assume `f` is integrable, but also if `L = (•)` or more
generally if `L` has an `AntilipschitzWith`-condition.  -/
MeasureTheory.convolution_eq_right' : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : NormedSpace ℝ F]
  [inst_9 : SeminormedAddCommGroup G] {x₀ : G} {R : ℝ},
  Function.support f ⊆ Metric.ball 0 R →
    (∀ x ∈ Metric.ball x₀ R, g x = g x₀) → MeasureTheory.convolution f g L μ x₀ = ∫ (t : G), (L (f t)) (g x₀) ∂μ
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.refl_target : ∀ (X : AlgebraicGeometry.Scheme), (AlgebraicGeometry.Scheme.PartialIso.refl X).target = ⊤
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.trans_le : ∀ {α : Type u_1} {E : Type u_3} {G : Type u_5} {F' : Type u_7} [inst : Norm E] [inst_1 : Norm G]
  [inst_2 : SeminormedAddCommGroup F'] {f : α → E} {k : α → G} {g' : α → F'} {l : Filter α},
  f =O[l] g' → (∀ (x : α), ‖g' x‖ ≤ ‖k x‖) → f =O[l] k
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.mk.injEq : ∀ (definition? : Option Lean.Lsp.RefInfo.Location) (usages : Array Lean.Lsp.RefInfo.Location)
  (definition?_1 : Option Lean.Lsp.RefInfo.Location) (usages_1 : Array Lean.Lsp.RefInfo.Location),
  ({ definition? := definition?, usages := usages } = { definition? := definition?_1, usages := usages_1 }) =
    (definition? = definition?_1 ∧ usages = usages_1)
-- Std.Http.Data.Request
/-- Sets the HTTP method for the request being built.
 -/
Std.Http.Request.Builder.method : Std.Http.Request.Builder → Std.Http.Method → Std.Http.Request.Builder
-- Mathlib.Geometry.Manifold.DerivationBundle
hfdifferential_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : ContMDiffMap I I' M M' ↑⊤} {x : M}
  {y : M'} (h : f x = y) (v : PointDerivation I x) (g : ContMDiffMap I' (modelWithCornersSelf 𝕜 𝕜) M' 𝕜 ↑⊤),
  ((hfdifferential h) v) g = ((fdifferential f x) v) g
-- Init.Data.UInt.Lemmas
UInt8.toFin.eq_1 : ∀ (x : UInt8), x.toFin = x.toBitVec.toFin
-- Batteries.Data.Array.Pairwise
Array.pairwise_iff_getElem : ∀ {α : Type u_1} {R : α → α → Prop} {as : Array α},
  Array.Pairwise R as ↔ ∀ (i j : ℕ) (x : i < as.size) (x_1 : j < as.size), i < j → R as[i] as[j]
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rightCancelEquiv_comp_rTensor_comp_symm : ∀ {R : Type u} {M : Type v} {N : Type u_1} {P : Type u_2} {Q : Type u_3} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  (e : TensorProduct R M N ≃ₗ[R] R) (f : P →ₗ[R] Q),
  ↑(Module.Invertible.rightCancelEquiv Q e) ∘ₗ
      LinearMap.rTensor N (LinearMap.rTensor M f) ∘ₗ ↑(Module.Invertible.rightCancelEquiv P e).symm =
    f
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_diff_le_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ \ m₂).size ≤ m₁.size
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_sInf : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Set (Subsemiring Rᵐᵒᵖ)), (sInf S).unop = sInf (Subsemiring.op ⁻¹' S)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_maxD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.contains (t.maxD fallback) = true
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.Sign.neg : Tactic.ComputeAsymptotics.UnitMonomial.Sign
-- Mathlib.Order.SuccPred.Limit
Order.isLUB_Iio_iff_isSuccPrelimit : ∀ {α : Type u_1} {a : α} [inst : LinearOrder α], IsLUB (Set.Iio a) a ↔ Order.IsSuccPrelimit a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- `pushout f g` computes the pushout of a pair of morphisms with the same source.  -/
CategoryTheory.Limits.pushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → (f : X ⟶ Y) → (g : X ⟶ Z) → [CategoryTheory.Limits.HasPushout f g] → C
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Small
CategoryTheory.CostructuredArrow.instSmallOfLocallySmall : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor C D} {T : D} [Small.{w, u₁} C] [CategoryTheory.LocallySmall.{w, v₂, u₂} D],
  Small.{w, max u₁ v₂} (CategoryTheory.CostructuredArrow S T)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_mul : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : CommSemiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  (I J : HomogeneousIdeal 𝒜), (I * J).toIdeal = I.toIdeal * J.toIdeal
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.subgraphOfAdj_connected : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (hvw : G.Adj v w), (G.subgraphOfAdj hvw).Connected
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.tail : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions can be pushed forward along bijective 2-Freiman homs.  -/
IsAddFreimanHom.addRothNumber_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β]
  [inst_3 : DecidableEq β] {A : Finset α} {B : Finset β} {f : α → β},
  IsAddFreimanHom 2 (↑A) (↑B) f → Set.BijOn f ↑A ↑B → addRothNumber B ≤ addRothNumber A
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.instMonadPrettyFormatStateMState : Std.Format.MonadPrettyFormat (StateM Std.Format.State✝)
-- Mathlib.Tactic.CategoryTheory.Elementwise
/-- Given an equality, extract a `Category` instance from it or raise an error.
Returns the name of the category and its instance.  -/
_private.Mathlib.Tactic.CategoryTheory.Elementwise.0.Mathlib.Tactic.Elementwise.elementwiseExpr.extractCatInstance : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.finite_spans_dense : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : DecidableEq E] (b : HilbertBasis ι 𝕜 E),
  (⨆ J, Submodule.span 𝕜 ↑(Finset.image (⇑b) J)).topologicalClosure = ⊤
-- Mathlib.Algebra.MvPolynomial.CommRing
MvPolynomial.C_neg : ∀ {R : Type u} (σ : Type u_1) (a : R) [inst : CommRing R], MvPolynomial.C (-a) = -MvPolynomial.C a
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
SSet.Truncated.HomotopyCategory.descOfTruncation_map_homMk : ∀ {X : SSet.Truncated 2} {C : Type u} [inst : CategoryTheory.SmallCategory C]
  (φ : X ⟶ (SSet.truncation 2).obj (CategoryTheory.nerve C))
  {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })} (e : SSet.Truncated.Edge x₀ x₁),
  (SSet.Truncated.HomotopyCategory.descOfTruncation φ).map (SSet.Truncated.HomotopyCategory.homMk e) =
    CategoryTheory.nerve.homEquiv (e.map φ)