mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.single_le_sum : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] {s : Multiset α} [IsOrderedAddMonoid α],
  (∀ x ∈ s, 0 ≤ x) → ∀ x ∈ s, x ≤ s.sum
-- Init.Data.Array.Lemmas
Array.size_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {xs : Array α} {ys : Array β} {f : α → β → γ},
  (Array.zipWith f xs ys).size = min xs.size ys.size
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback v : β}, Std.DHashMap.Const.getD (m.insert k v) k fallback = v
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_inter!_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.Const.get? (m₁.inter! m₂) k = none
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_dvd : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x y → x ∣ z → y ∣ z → x * y ∣ z
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.LeftAdjointCommShift.iso_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] (a b : A) (h : a + b = 0) [inst_5 : G.CommShift A] (Y : C),
  (CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a).inv.app Y =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor D a).map (F.map ((CategoryTheory.shiftFunctorCompIsoId C a b h).inv.app Y)))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D a).map
          (F.map ((CategoryTheory.shiftFunctor C b).map (adj.unit.app ((CategoryTheory.shiftFunctor C a).obj Y)))))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.shiftFunctor D a).map
            (F.map
              ((CategoryTheory.Functor.commShiftIso G b).inv.app (F.obj ((CategoryTheory.shiftFunctor C a).obj Y)))))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor D a).map
              (adj.counit.app
                ((CategoryTheory.shiftFunctor D b).obj (F.obj ((CategoryTheory.shiftFunctor C a).obj Y)))))
            ((CategoryTheory.shiftFunctorCompIsoId D b a ⋯).hom.app
              (F.obj ((CategoryTheory.shiftFunctor C a).obj Y))))))
-- Init.Data.String.Termination
String.Pos.prev_prev_lt : ∀ {s : String} {p : s.Pos} {h : p ≠ s.startPos} {h' : p.prev h ≠ s.startPos}, (p.prev h).prev h' < p
-- Mathlib.Analysis.SpecificLimits.Normed
/-- **Dirichlet's test** for antitone sequences.  -/
Antitone.cauchySeq_series_mul_of_tendsto_zero_of_bounded : ∀ {E : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E},
  Antitone f →
    Filter.Tendsto f Filter.atTop (nhds 0) →
      (∀ (n : ℕ), ‖∑ i ∈ Finset.range n, z i‖ ≤ b) → CauchySeq fun n => ∑ i ∈ Finset.range n, f i • z i
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The left unitor isomorphism for graded objects.  -/
CategoryTheory.GradedObject.Monoidal.leftUnitor : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : DecidableEq I] →
            [inst_4 : CategoryTheory.Limits.HasInitial C] →
              [inst_5 :
                  ∀ (X₂ : C),
                    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                      ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                (X : CategoryTheory.GradedObject I C) →
                  CategoryTheory.GradedObject.Monoidal.tensorObj CategoryTheory.GradedObject.Monoidal.tensorUnit X ≅ X
-- Std.Data.TreeSet.Raw.Basic
Std.TreeSet.Raw.empty_eq_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeSet.Raw.empty = ∅
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.mk : {n : ℕ} →
  (length : ℕ) →
    (partSize : Fin length → ℕ) →
      (partSize_pos : ∀ (m : Fin length), 0 < partSize m) →
        (emb : (m : Fin length) → Fin (partSize m) → Fin n) →
          (∀ (m : Fin length), StrictMono (emb m)) →
            (StrictMono fun m => emb m ⟨partSize m - 1, ⋯⟩) →
              (Set.univ.PairwiseDisjoint fun m => Set.range (emb m)) →
                (∀ (x : Fin n), ∃ m, x ∈ Set.range (emb m)) → OrderedFinpartition n
-- Mathlib.Analysis.SumIntegralComparisons
/-- **Integral test**: A function which is nonnegative, integrable and antitone
for sufficiently large `n` is summable.  -/
AntitoneOn.summable_of_integrableOn_Ioi : ∀ {f : ℝ → ℝ} {N : ℕ},
  AntitoneOn f (Set.Ici ↑N) →
    MeasureTheory.IntegrableOn f (Set.Ioi ↑N) MeasureTheory.volume →
      (∀ t ∈ Set.Ioi ↑N, 0 ≤ f t) → Summable fun n => f ↑n
-- Batteries.Data.DList.Basic
/-- `O(1)` (`apply` is `O(1)`). Return an empty `DList α`.  -/
Batteries.DList.empty : {α : Type u} → Batteries.DList α
-- Init.Data.BEq
BEq.symm_false : ∀ {α : Type u_1} [inst : BEq α] [PartialEquivBEq α] {a b : α}, (a == b) = false → (b == a) = false
-- Mathlib.Order.SymmDiff
symmDiff_sdiff_eq_sup : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff a (b \ a) = a ⊔ b
-- Init.Grind.Ordered.Order
Lean.Grind.Preorder.lt_irrefl : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] (a : α), ¬a < a
-- Init.Data.Nat.Basic
Nat.lt_add_one_iff_lt_or_eq : ∀ {m n : ℕ}, m < n + 1 ↔ m < n ∨ m = n
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.countablySeparated_of_separatesPoints : ∀ {α : Type u_1} [inst : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α]
  [MeasurableSpace.SeparatesPoints α], MeasurableSpace.CountablySeparated α
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The `1`-hypercover associated to a `OneHypercoverDenseData` structure.  -/
CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercover : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              [CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                {X : C} → F.OneHypercoverDenseData J₀ J X → J.OneHypercover X
-- Mathlib.Data.Finset.Interval
Finset.Iic_eq_powerset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Finset.Iic s = s.powerset
-- Mathlib.CategoryTheory.Conj
CategoryTheory.Iso.conjAut_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (α : X ≅ Y) (f g : CategoryTheory.Aut X),
  α.conjAut (f ≪≫ g) = α.conjAut f ≪≫ α.conjAut g
-- Mathlib.Tactic.FunProp.Types
/-- `fun_prop` configuration  -/
Mathlib.Meta.FunProp.Config : Type
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.id_prod_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsSFiniteKernel κ] (a : α) {s : Set (α × β)},
  MeasurableSet s → ((ProbabilityTheory.Kernel.id.prod κ) a) s = (κ a) (Prod.mk a ⁻¹' s)
-- Mathlib.Data.Ordering.Lemmas
Ordering.ite_eq_eq_distrib : ∀ (c : Prop) [inst : Decidable c] (a b : Ordering),
  ((if c then a else b) = Ordering.eq) = if c then a = Ordering.eq else b = Ordering.eq
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.comp.congr_simp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
  (f f_1 : M₂ →ₛₗ[σ₂₃] M₃), f = f_1 → ∀ (g g_1 : M₁ →ₛₗ[σ₁₂] M₂), g = g_1 → f ∘ₛₗ g = f_1 ∘ₛₗ g_1
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.getMatchCore : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → Lean.MetaM (Lean.Meta.DiscrTree.Key × Array α)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
/-- seminorm for `ℒ∞`, equal to the essential supremum of `‖f‖`.  -/
MeasureTheory.eLpNormEssSup : {α : Type u_1} → {ε : Type u_2} → {m0 : MeasurableSpace α} → [ENorm ε] → (α → ε) → MeasureTheory.Measure α → ENNReal
-- Init.Core
Prod.mk.injEq : ∀ {α : Type u} {β : Type v} (fst : α) (snd : β) (fst_1 : α) (snd_1 : β),
  ((fst, snd) = (fst_1, snd_1)) = (fst = fst_1 ∧ snd = snd_1)
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toUInt8 = OfNat.ofNat n
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.PreZeroHypercover.sieve₀.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S),
  E.sieve₀ = CategoryTheory.Sieve.ofArrows E.X E.f
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.IsClosedImmersion.eq_proper_inf_monomorphisms : @AlgebraicGeometry.IsClosedImmersion =
  @AlgebraicGeometry.IsProper ⊓ CategoryTheory.MorphismProperty.monomorphisms AlgebraicGeometry.Scheme
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_sdiff_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Coframe α] {a : α} {f : ι → α}, (⨆ x, f x) \ a = ⨆ x, f x \ a
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.isEmpty_filter_key_eq_false : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {f : α → Bool} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst) l).isEmpty = false ↔
      ∃ k, ∃ (h : Std.Internal.List.containsKey k l = true), f (Std.Internal.List.getKey k l h) = true)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.one_le_mul`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.one_le_mul`.  -/
one_le_mul : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, 1 ≤ a → 1 ≤ b → 1 ≤ a * b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_union_of_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₁ → k ∈ t₁ ∪ t₂
-- Mathlib.Analysis.SpecialFunctions.Exp
Real.map_exp_nhds : ∀ (x : ℝ), Filter.map Real.exp (nhds x) = nhds (Real.exp x)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.opMap_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.opMap φ).τ₂ = φ.τ₂.op
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- `PowIdentity` instance, the synthesized `CommSemiring` instance, and exponent `p` if available.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.powIdentityInst? : Lean.Meta.Grind.Arith.CommRing.CommRing → Option (Lean.Expr × Lean.Expr × ℕ)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.isInducing_postcomp : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup F] [inst_14 : IsTopologicalAddGroup G] (f : F →SL[τ] G),
  Topology.IsInducing ⇑f → Topology.IsInducing f.comp
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.injective_pi_lapply : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)], Function.Injective ⇑(LinearMap.pi DFinsupp.lapply)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
/-- Pull back a continuous compactly supported function `f` on `β` along a closed embedding
`φ : α →* β` to the continuous compactly supported function `a ↦ f (b * φ a)` on `A`.  -/
CompactlySupportedContinuousMap.pullback_monoidHom : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : TopologicalSpace α] →
        [R1Space α] →
          [inst_2 : Group α] →
            [inst_3 : TopologicalSpace β] →
              [R1Space β] →
                [inst_5 : Group β] →
                  [ContinuousMul β] →
                    [inst_7 : NormedAddCommGroup γ] →
                      {φ : α →* β} →
                        Topology.IsClosedEmbedding ⇑φ →
                          CompactlySupportedContinuousMap β γ → β → CompactlySupportedContinuousMap α γ
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
_private.Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ.0.WeierstrassCurve.exists_variableChange_of_char_three_of_j_ne_zero : ∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [inst_2 : E.IsElliptic]
  [inst_3 : E'.IsElliptic] [CharP F 3] [E.IsCharThreeJNeZeroNF] [E'.IsCharThreeJNeZeroNF], E.j = E'.j → ∃ C, C • E = E'
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.InfiniteAdeleRing.norm_eq_zero_of_not_isUnit : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.InfiniteAdeleRing K}, ¬IsUnit x → ‖x‖ = 0
-- Mathlib.Algebra.Lie.Subalgebra
/-- Lie subalgebras that are equal as sets are equivalent as Lie algebras.  -/
LieEquiv.ofEq : {R : Type u} →
  {L₁ : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L₁] →
        [inst_2 : LieAlgebra R L₁] → (L₁' L₁'' : LieSubalgebra R L₁) → ↑L₁' = ↑L₁'' → ↥L₁' ≃ₗ⁅R⁆ ↥L₁''
-- Mathlib.Tactic.Translate.Core
/-- `applyReplacementFun e` replaces the expression `e` with its translation.
It translates each identifier (inductive type, defined function etc) in an expression, unless
* The identifier occurs in an application with `relevantArg` argument `arg`; and
* `shouldTranslate arg` is false.

It will also reorder arguments of certain functions, using the stored `reorder`.
 -/
Mathlib.Tactic.Translate.applyReplacementFun : Mathlib.Tactic.Translate.TranslateData → Lean.Expr → Mathlib.Tactic.Translate.ReplacementM Lean.Expr
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- Given an open set in a finite-dimensional real manifold, there exists a nonnegative smooth
function with support equal to `s`.  -/
IsOpen.exists_contMDiff_support_eq : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [FiniteDimensional ℝ E] [IsManifold I (↑⊤) M] [SigmaCompactSpace M] [T2Space M] {n : ℕ∞} {s : Set M},
  IsOpen s → ∃ f, Function.support f = s ∧ ContMDiff I (modelWithCornersSelf ℝ ℝ) (↑n) f ∧ ∀ (x : M), 0 ≤ f x
-- Init.Data.Int.Order
Int.lt_add_one_iff : ∀ {a b : ℤ}, a < b + 1 ↔ a ≤ b
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.equiv_iff_toList_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ ↔ t₁.toList.Perm t₂.toList
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_counitIso_hom_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma S' (CategoryTheory.Functor.fromPUnit T)),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).counitIso.hom.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.coconeUnopOfCone c = { pt := Opposite.unop c.pt, ι := CategoryTheory.NatTrans.unop c.π }
-- Mathlib.NumberTheory.ModularForms.QExpansion
_private.Mathlib.NumberTheory.ModularForms.QExpansion.0.term𝕢 : Lean.ParserDescr
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
/-- A finite-dimensional inner product space has a canonical measure, the Lebesgue measure giving
volume `1` to the parallelepiped spanned by any orthonormal basis. We define the measure using
some arbitrary choice of orthonormal basis. The fact that it works with any orthonormal basis
is proved in `orthonormalBasis.volume_parallelepiped`.

This instance creates:

- a potential non-defeq diamond with the natural instance for `MeasureSpace (ULift E)`,
  which does not exist in Mathlib at the moment;

- a diamond with the existing instance `MeasureTheory.Measure.instMeasureSpacePUnit`.

However, we've decided not to refactor until one of these diamonds starts creating issues, see
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Hausdorff.20measure.20normalisation
 -/
measureSpaceOfInnerProductSpace : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      [FiniteDimensional ℝ E] → [inst_3 : MeasurableSpace E] → [BorelSpace E] → MeasureTheory.MeasureSpace E
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.toPresheaf_preservesColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (R : CategoryTheory.Functor Cᵒᵖ RingCat)
  [CategoryTheory.Limits.HasColimitsOfSize.{v₂, u₂, v, v + 1} AddCommGrpCat],
  CategoryTheory.Limits.PreservesColimitsOfSize.{v₂, u₂, max u₁ v, max u₁ v, max (max (max u u₁) (v + 1)) v₁,
      max (max u₁ (v + 1)) v₁}
    (PresheafOfModules.toPresheaf R)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpKind.dsimp.sizeOf_spec : sizeOf Lean.Elab.Tactic.SimpKind.dsimp = 1
-- Mathlib.Data.Set.Image
Set.imageFactorization_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Subtype.val ∘ Set.imageFactorization f s = f ∘ Subtype.val
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The range of a multilinear map, closed under scalar multiplication.  -/
MultilinearMap.range : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Ring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] → [Nonempty ι] → MultilinearMap R M₁ M₂ → SubMulAction R M₂
-- Lean.Elab.Term.TermElabM
/-- Info node capturing `def/let rec` bodies, used by the unused variables linter.  -/
Lean.Elab.Term.BodyInfo : Type
-- Mathlib.Order.Sublocale
/-- A sublocale is closed under all meets.

Do NOT use directly. Use `Sublocale.sInf_mem` instead.  -/
Sublocale.sInf_mem' : ∀ {X : Type u_2} [inst : Order.Frame X] (self : Sublocale X), ∀ s ⊆ self.carrier, sInf s ∈ self.carrier
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
MeasureTheory.Measure.MeasureDense.completion : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  μ.MeasureDense 𝒜 → μ.completion.MeasureDense 𝒜
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.one_lt_rOut_div_rIn : ∀ {E : Type u_1} {c : E} (f : ContDiffBump c), 1 < f.rOut / f.rIn
-- Batteries.Data.AssocList
Batteries.AssocList.eraseP.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (a : α) (b : β) (es : Batteries.AssocList α β),
  Batteries.AssocList.eraseP p (Batteries.AssocList.cons a b es) =
    bif p a b then es else Batteries.AssocList.cons a b (Batteries.AssocList.eraseP p es)
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a bi-Heyting algebra
with possibly different definitional equalities.  -/
BiheytingAlgebra.copy : {α : Type u} →
  (c : BiheytingAlgebra α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (bot : α) →
              bot = ⊥ →
                (sup : α → α → α) →
                  sup = max →
                    (inf : α → α → α) →
                      inf = min →
                        (sdiff : α → α → α) →
                          sdiff = SDiff.sdiff →
                            (hnot : α → α) →
                              hnot = HNot.hnot →
                                (himp : α → α → α) →
                                  himp = HImp.himp → (compl : α → α) → compl = Compl.compl → BiheytingAlgebra α
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LocalPresentationAt.mem_codChart_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (self : Manifold.LocalPresentationAt I J n f x P), f x ∈ self.codChart.source
-- Mathlib.Data.Set.Function
Set.MapsTo.mono : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.MapsTo f s₁ t₁ → s₂ ⊆ s₁ → t₁ ⊆ t₂ → Set.MapsTo f s₂ t₂
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.nonempty_sets : ∀ {α : Type u_1} (B : FilterBasis α), Nonempty ↑B.sets
-- Mathlib.Topology.Order.LocalExtr
IsLocalMinOn.comp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {s : Set α} {a : α}, IsLocalMinOn f s a → ∀ {g : β → γ}, Monotone g → IsLocalMinOn (g ∘ f) s a
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
_private.Mathlib.Data.QPF.Multivariate.Constructions.Sigma.0.MvQPF.Sigma.abs.match_1.eq_1 : ∀ {n : ℕ} {A : Type u_1} (F : A → TypeVec.{u_1} n → Type u_1) [inst : (α : A) → MvQPF (F α)] ⦃α : TypeVec.{u_1} n⦄
  (motive : ↑(MvQPF.Sigma.P F) α → Sort u_2) (a : (MvQPF.Sigma.P F).A) (f : ((MvQPF.Sigma.P F).B a).Arrow α)
  (h_1 : (a : (MvQPF.Sigma.P F).A) → (f : ((MvQPF.Sigma.P F).B a).Arrow α) → motive ⟨a, f⟩),
  (match ⟨a, f⟩ with
    | ⟨a, f⟩ => h_1 a f) =
    h_1 a f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.zero_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C) [inst_3 : CategoryTheory.AddMonObj X]
  [inst_4 : CategoryTheory.AddMonObj Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero (β_ X Y).hom = CategoryTheory.AddMonObj.zero
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.hasBinaryBiproduct_of_iso : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q P' Q' : C} [CategoryTheory.Limits.HasBinaryBiproduct P Q] (eP : P ≅ P') (eQ : Q ≅ Q'),
  CategoryTheory.Limits.HasBinaryBiproduct P' Q'