mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.opEquiv.match_3.eq_2 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithTerminal C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3)
  (a : C)
  (x :
    Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of a)) ⟶
      Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star))
  (x_1 : Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op (CategoryTheory.WithTerminal.of a))
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithTerminal.of x) ⟶ Opposite.op (CategoryTheory.WithTerminal.of y)) →
          motive (Opposite.op (CategoryTheory.WithTerminal.of x)) (Opposite.op (CategoryTheory.WithTerminal.of y)) f
            x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op (CategoryTheory.WithTerminal.of a)) ⟶
            Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star)) →
        (x_2 : Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op (CategoryTheory.WithTerminal.of a)) →
          motive (Opposite.op CategoryTheory.WithTerminal.star) (Opposite.op (CategoryTheory.WithTerminal.of a)) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithTerminal.star)) →
      (x_2 : Opposite.op CategoryTheory.WithTerminal.star ⟶ Opposite.op CategoryTheory.WithTerminal.star) →
        motive (Opposite.op CategoryTheory.WithTerminal.star) (Opposite.op CategoryTheory.WithTerminal.star) x x_2),
  (match Opposite.op CategoryTheory.WithTerminal.star, Opposite.op (CategoryTheory.WithTerminal.of a), x, x_1 with
    | Opposite.op (CategoryTheory.WithTerminal.of x), Opposite.op (CategoryTheory.WithTerminal.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op (CategoryTheory.WithTerminal.of a), x, x_2 =>
      h_2 a x x_2
    | Opposite.op CategoryTheory.WithTerminal.star, Opposite.op CategoryTheory.WithTerminal.star, x, x_2 => h_3 x x_2) =
    h_2 a x x_1
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel_apply : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a b : α},
  (MulAction.orbitRel G α) a b ↔ a ∈ MulAction.orbit G b
-- Mathlib.Data.String.Lemmas
String.leftpad.eq_1 : ∀ (n : ℕ) (c : Char) (s : String), String.leftpad n c s = String.ofList (List.leftpad n c s.toList)
-- Mathlib.CategoryTheory.Countable
CategoryTheory.CountableCategory.instCountableHomHomAsType : ∀ (α : Type u) [inst : CategoryTheory.Category.{v, u} α] [inst_1 : CategoryTheory.CountableCategory α]
  {i j : CategoryTheory.CountableCategory.HomAsType α}, Countable (i ⟶ j)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.HasPushoutsAgainst P'` states that for any morphism `f` satisfying `P'`,
`P` has pushouts along `f`.  -/
CategoryTheory.MorphismProperty.HasPushoutsAgainst : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Std.Http.Data.Headers.Basic
/-- The ordered list of transfer codings.
 -/
Std.Http.Header.TransferEncoding.codings : Std.Http.Header.TransferEncoding → Array String
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.hom_ext : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {F₁ F₂ : FreeLieAlgebra R X →ₗ⁅R⁆ L}, (∀ (x : X), F₁ (FreeLieAlgebra.of R x) = F₂ (FreeLieAlgebra.of R x)) → F₁ = F₂
-- Mathlib.Tactic.GRewrite.Core
/-- Apply the `gcongr` lemma to the goal. The main subgoals are visited for rewriting in,
and otherwise closed `by rfl`. If at least one rewrite has happened, we commit to this lemma,
and we try to discharge the side goals.

Returns whether we have done a rewrite in this subgoal, in which case it has been closed.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.processGCongrLemma : Lean.MVarId →
  Mathlib.Tactic.GCongr.GCongrLemma → Bool → Mathlib.Tactic.GRewrite.Config → Mathlib.Tactic.GRewrite.GRewriteM✝ Bool
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Module.rank_linearMap_self : ∀ (R : Type u) (S : Type u') (M : Type v) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Free R M] [Module.Finite R M] [StrongRankCondition R] [StrongRankCondition S]
  [inst_8 : Module R S] [inst_9 : SMulCommClass R S S],
  Module.rank S (M →ₗ[R] S) = Cardinal.lift.{u', v} (Module.rank R M)
-- Init.System.IO
IO.instInhabitedTaskState : Inhabited IO.TaskState
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_union_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ ↔ k ∈ t₁ ∨ k ∈ t₂
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.disjoint_coe : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α}, Codisjoint ↑s ↑t ↔ Codisjoint s t
-- Mathlib.Data.Part
Part.neg_some : ∀ {α : Type u_1} [inst : Neg α] (a : α), -Part.some a = Part.some (-a)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.dist_0_eq_abs : ∀ (x : ℝ), dist x 0 = |x|
-- Mathlib.Probability.Independence.Integration
/-- If `X` and `Y` are independent random variables such that `f(X)` and `g(Y)` are integrable
and `B` is a continuous bilinear map, then
`∫ ω, B (f (X ω)) (g (Y ω)) ∂μ = B (∫ ω, f (X ω) ∂μ) (∫ ω, g (Y ω) ∂μ).`  -/
ProbabilityTheory.IndepFun.integral_bilin_comp_comp : ∀ {Ω : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝓧 : Type u_3}
  {𝓨 : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst_1 : MeasurableSpace 𝓧] [inst_2 : MeasurableSpace 𝓨]
  [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 E] [CompleteSpace E]
  [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℝ F] [inst_9 : NormedSpace 𝕜 F] [CompleteSpace F]
  [inst_11 : NormedAddCommGroup G] [inst_12 : NormedSpace ℝ G] [inst_13 : NormedSpace 𝕜 G] [CompleteSpace G] {X : Ω → 𝓧}
  {Y : Ω → 𝓨} {f : 𝓧 → E} {g : 𝓨 → F},
  ProbabilityTheory.IndepFun X Y μ →
    AEMeasurable X μ →
      AEMeasurable Y μ →
        MeasureTheory.Integrable f (MeasureTheory.Measure.map X μ) →
          MeasureTheory.Integrable g (MeasureTheory.Measure.map Y μ) →
            ∀ (B : E →L[𝕜] F →L[𝕜] G),
              ∫ (ω : Ω), (B (f (X ω))) (g (Y ω)) ∂μ = (B (∫ (ω : Ω), f (X ω) ∂μ)) (∫ (ω : Ω), g (Y ω) ∂μ)
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.sub_f_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D) (i : ι), (f - g).f i = f.f i - g.f i
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If `C` has all colimits of diagrams `pair X Y`, then it has all binary coproducts  -/
CategoryTheory.Limits.hasBinaryCoproducts_of_hasColimit_pair : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [∀ {X Y : C}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.pair X Y)],
  CategoryTheory.Limits.HasBinaryCoproducts C
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, k ∉ t₂ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.tmul_eq_smul_one_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_22}
  [inst_3 : Semiring S] [inst_4 : Module R S] [inst_5 : SMulCommClass R S S] (s : S) (m : M), s ⊗ₜ[R] m = s • 1 ⊗ₜ[R] m
-- Mathlib.Data.Complex.BigOperators
Complex.ofReal_sum : ∀ {α : Type u_1} (s : Finset α) (f : α → ℝ), ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.Algebra.Polynomial.CoeffMem
_private.Mathlib.Algebra.Polynomial.CoeffMem.0.Polynomial.«termDeg(_)» : Lean.ParserDescr
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.iInter_of_antitone : ∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Type u_5} [inst_1 : Preorder ι] [IsDirectedOrder ι]
  [Filter.atTop.IsCountablyGenerated] {s : ι → Set α},
  Antitone s → (∀ (i : ι), MeasurableSet (s i)) → MeasurableSet (⋂ i, s i)
-- Mathlib.NumberTheory.LSeries.Convergence
/-- The abscissa `x : EReal` of absolute convergence of the L-series associated to `f`:
the series converges absolutely at `s` when `re s > x` and does not converge absolutely
when `re s < x`.  -/
LSeries.abscissaOfAbsConv : (ℕ → ℂ) → EReal
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingletonLE_symm_apply : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] [inst_6 : TopologicalSpace M]
  [inst_7 : ContinuousAdd M] [inst_8 : ContinuousConstSMul S M] [inst_9 : TopologicalSpace R]
  [inst_10 : ContinuousSMul R M], ⇑(ContinuousLinearMap.toSpanSingletonLE R S M).symm = fun f => f 1
-- Lean.Message
Lean.MessageLog.mk.inj : ∀ {reported unreported : Lean.PersistentArray Lean.Message} {loggedKinds : Lean.NameSet}
  {reported_1 unreported_1 : Lean.PersistentArray Lean.Message} {loggedKinds_1 : Lean.NameSet},
  { reported := reported, unreported := unreported, loggedKinds := loggedKinds } =
      { reported := reported_1, unreported := unreported_1, loggedKinds := loggedKinds_1 } →
    reported = reported_1 ∧ unreported = unreported_1 ∧ loggedKinds = loggedKinds_1
-- Mathlib.Order.Filter.Basic
Filter.eq_biInf_of_mem_iff_exists_mem : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} {p : ι → Prop} {l : Filter α},
  (∀ {s : Set α}, s ∈ l ↔ ∃ i, p i ∧ s ∈ f i) → l = ⨅ i, ⨅ (_ : p i), f i
-- Mathlib.Data.Finset.Empty
Finset.coe_eq_empty : ∀ {α : Type u_1} {s : Finset α}, ↑s = ∅ ↔ s = ∅
-- Mathlib.Data.Set.Card
Set.encard_eq_zero : ∀ {α : Type u_1} {s : Set α}, s.encard = 0 ↔ s = ∅
-- Mathlib.Analysis.Calculus.VectorField
/-- We have `[0, W] = 0` for all vector fields `W`: this depends on the junk value 0
if `W` is not differentiable.  -/
VectorField.lieBracket_zero_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {W : E → E}, VectorField.lieBracket 𝕜 0 W = 0
-- Init.Prelude
HDiv.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HDiv α β γ
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instModule : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module R (AdicCompletion.AdicCauchySequence I M)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.trW_of_op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated] {X Y : C} {f : X ⟶ Y}, P.op.trW f.op → P.trW f
-- Mathlib.Algebra.Group.Action.Defs
IsLeftCancelVAdd.left_cancel' : ∀ {G : Type u_9} {P : Type u_10} {inst : VAdd G P} [self : IsLeftCancelVAdd G P] (a : G) (b c : P),
  a +ᵥ b = a +ᵥ c → b = c
-- Std.Http.Data.Headers.Name
Std.Http.Header.instReprName.repr : Std.Http.Header.Name → ℕ → Std.Format
-- Init.Core
Bool.of_not_eq_true : ∀ {b : Bool}, ¬b = true → b = false
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- Adding `@[reassoc]` to a lemma named `F` of shape `∀ .., f = g`, where `f g : X ⟶ Y` are
morphisms in some category, will create a new lemma named `F_assoc` of shape
`∀ .. {Z : C} (h : Y ⟶ Z), f ≫ h = g ≫ h`
but with the conclusions simplified using the axioms for a category
(`Category.comp_id`, `Category.id_comp`, and `Category.assoc`).
So, for example, if the conclusion of `F` is `a ≫ b = g` then
the conclusion of `F_assoc` will be `a ≫ (b ≫ h) = g ≫ h` (note that `≫` reassociates
to the right so the brackets will not appear in the statement).

This attribute is useful for generating lemmas which the simplifier can use even on expressions
that are already right associated.

Note that if you want both the lemma and the reassociated lemma to be
`simp` lemmas, you should tag the lemma `@[reassoc (attr := simp)]`.
The variant `@[simp, reassoc]` on a lemma `F` will tag `F` with `@[simp]`,
but not `F_assoc` (this is sometimes useful). This can be combined with `to_dual` in the form
`@[to_dual (attr := reassoc (attr := simp))]`, which tags all 4 lemmas with `simp`, or
`@[to_dual (attr := simp, reassoc)]`, which only tags `F` and its dual with `simp`.

If `F` is tagged with `to_dual`, then `F_assoc` will automatically get a `@[to_dual none]` tag.
This also applies when using `@[to_dual (attr := reassoc)]`.
In the rare case that only `F_assoc` should be tagged with `to_dual`, use `@[reassoc +to_dual]`.

This attribute also works for lemmas of shape `∀ .., f = g` where `f g : X ≅ Y` are
isomorphisms, provided that `Tactic.CategoryTheory.IsoReassoc` has been imported.
 -/
Mathlib.Tactic.Reassoc.reassoc : Lean.ParserDescr
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {a : α}, t.isEmpty = true → t[a]! = default
-- Mathlib.Analysis.Asymptotics.ExpGrowth
/-- Upper exponential growth of a sequence of extended nonnegative real numbers.  -/
ExpGrowth.expGrowthSup : (ℕ → ENNReal) → EReal
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.fourierTransformInv_apply : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : ↥(MeasureTheory.Lp E 1 MeasureTheory.volume)) (x : V),
  (Real.Lp.fourierTransformInv f) x = FourierTransformInv.fourierInv (↑↑f) x
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEmbedding.natCast : ∀ {α : Type u_6} [inst : MeasurableSpace α] [MeasurableSingletonClass α] [inst_2 : AddMonoidWithOne α] [CharZero α],
  MeasurableEmbedding Nat.cast
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiable.clm_precomp : ∀ {𝕜 : 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] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {f : M → F₁ →L[𝕜] F₂},
  MDiff f → MDiff fun y => ContinuousLinearMap.precomp F₃ (f y)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.reindex_reindex : ∀ {ι : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] (e : ι ≃ ι₂) (e' : ι₂ ≃ ι₃)
  (x : PiTensorProduct R fun i => s i),
  (PiTensorProduct.reindex R (fun i => s (e.symm i)) e') ((PiTensorProduct.reindex R s e) x) =
    (PiTensorProduct.reindex R s (e.trans e')) x
-- Mathlib.Logic.Embedding.Basic
Equiv.embeddingCongr_apply : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (h : α ≃ β) (h' : γ ≃ δ) (f : α ↪ γ),
  (h.embeddingCongr h') f = Function.Embedding.congr h h' f
-- Init.Data.Slice.List.Lemmas
ListSlice.toArray_mkSlice_rio : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  Std.Slice.toArray (Std.Rio.Sliceable.mkSlice xs *...hi) = (Std.Slice.toArray xs).extract 0 hi
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a congruence relation `c` on an algebra and a homomorphism `f`
constant on the equivalence classes of `c`, `f` has the same image
as the homomorphism that `f` induces on the quotient.  -/
RingCon.liftₐ_range : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] {c : RingCon M} {f : M →ₐ[R] P} (H : c ≤ RingCon.ker f.toRingHom),
  (c.liftₐ f H).range = f.range
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instAddCommMonoidWithOne : {R : Type u_1} → [AddCommMonoidWithOne R] → AddCommMonoidWithOne Rᵃᵒᵖ
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The set `List.fixedLengthDigits b (l + 1)` is the disjoint union of the sets
`List.consFixedLengthDigits b l d` where `d` ranges through the natural integers `< d`.
 -/
List.fixedLengthDigits_succ_eq_disjiUnion : ∀ {b : ℕ} (hb : 1 < b) (l : ℕ),
  List.fixedLengthDigits hb (l + 1) = (Finset.range b).disjiUnion (List.consFixedLengthDigits hb l) ⋯
-- Lean.Expr
/-- Return `true` if the given expression is a `.sort ..`  -/
Lean.Expr.isSort : Lean.Expr → Bool
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- Consider a point `x` at which a set `s` has density zero, with respect to closed balls. Then it
also has density zero with respect to any measurable set `t`: the proportion of points in `s`
belonging to a rescaled copy `{x} + r • t` of `t` tends to zero as `r` tends to zero.  -/
MeasureTheory.Measure.tendsto_addHaar_inter_smul_zero_of_density_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (s : Set E) (x : E),
  Filter.Tendsto (fun r => μ (s ∩ Metric.closedBall x r) / μ (Metric.closedBall x r)) (nhdsWithin 0 (Set.Ioi 0))
      (nhds 0) →
    ∀ (t : Set E),
      MeasurableSet t →
        μ t ≠ ⊤ → Filter.Tendsto (fun r => μ (s ∩ ({x} + r • t)) / μ ({x} + r • t)) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
one_lt_mabs_of_lt_one : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a : α}, a < 1 → 1 < |a|ₘ
-- Std.Do.SPred.SPred
/-- A pure proposition `P : Prop` embedded into `SPred`.
Prefer to use notation `⌜P⌝`.
 -/
Std.Do.SPred.pure : {σs : List (Type u)} → Prop → Std.Do.SPred σs
-- Mathlib.Data.Sign.Defs
SignType.zero : SignType
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_subset_one_on_sdiff : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f g : ι → M} [inst_1 : DecidableEq ι],
  s₁ ⊆ s₂ → (∀ x ∈ s₂ \ s₁, g x = 1) → (∀ x ∈ s₁, f x = g x) → ∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.RevSplitIterator.toOption.match_1.eq_2 : ∀ {ρ : Type} {ρ_1 : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToBackwardSearcher ρ_1 σ]
  {s : String.Slice} (motive : String.Slice.RevSplitIterator ρ_1 s → Sort u_1)
  (h_1 :
    (currPos : s.Pos) →
      (s_1 : Std.Iter (String.Slice.Pattern.SearchStep s)) →
        motive (String.Slice.RevSplitIterator.operating currPos s_1))
  (h_2 : Unit → motive String.Slice.RevSplitIterator.atEnd),
  (match String.Slice.RevSplitIterator.atEnd with
    | String.Slice.RevSplitIterator.operating currPos s => h_1 currPos s
    | String.Slice.RevSplitIterator.atEnd => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.Ideal.Operations
/-- The reverse inclusion does not hold for e.g. `I := fun n : ℕ ↦ Ideal.span {(2 ^ n : ℤ)}`.  -/
Ideal.radical_iInf_le : ∀ {R : Type u} [inst : CommSemiring R] {ι : Sort u_2} (I : ι → Ideal R), (⨅ i, I i).radical ≤ ⨅ i, (I i).radical
-- Mathlib.Data.Set.Insert
Set.eq_of_mem_singleton : ∀ {α : Type u_1} {x y : α}, x ∈ {y} → x = y
-- Mathlib.Topology.Algebra.Module.Equiv
/-- By definition, if `f` is invertible then `inverse f = f.symm`.  -/
ContinuousLinearMap.inverse_equiv : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (e : M ≃L[R] M₂), (↑e).inverse = ↑e.symm
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.mem_range_self : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S) (x : R),
  f x ∈ f.range
-- Lean.Message
/-- Converts the unreported messages to an array, oldest message first.  -/
Lean.MessageLog.toArray : Lean.MessageLog → Array Lean.Message
-- Mathlib.GroupTheory.OrderOfElement
Subgroup.orderOf_mk : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (a : G) (ha : a ∈ H), orderOf ⟨a, ha⟩ = orderOf a
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.mergeSort.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → (α → α → Bool) → Sort u_2) (x : α → α → Bool)
  (h_1 : (x : α → α → Bool) → motive [] x) (h_2 : (a : α) → (x : α → α → Bool) → motive [a] x)
  (h_3 : (a b : α) → (xs : List α) → (le : α → α → Bool) → motive (a :: b :: xs) le),
  (match [], x with
    | [], x => h_1 x
    | [a], x => h_2 a x
    | a :: b :: xs, le => h_3 a b xs le) =
    h_1 x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.inf_adj : ∀ {V : Type u} (x y : SimpleGraph V) (v w : V), (x ⊓ y).Adj v w ↔ x.Adj v w ∧ y.Adj v w
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_one : ∀ (x : ℂ), x ^ 1 = x
-- Mathlib.Topology.Order.Lattice
ContinuousOn.finset_inf_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [inst_3 : OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L} {t : Set X},
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (fun a => s.inf fun x => f x a) t
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.isLocalization_rightAdjoint' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  [F.Full] [F.Faithful] (adj : F ⊣ G),
  G.IsLocalization ((CategoryTheory.MorphismProperty.isomorphisms C₂).inverseImage G)
-- Mathlib.Algebra.Algebra.Hom
/-- See Note [custom simps projection]  -/
AlgHom.Simps.apply : {R : Type u} →
  {α : Type v} →
    {β : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring α] →
          [inst_2 : Semiring β] → [inst_3 : Algebra R α] → [inst_4 : Algebra R β] → (α →ₐ[R] β) → α → β
-- Mathlib.Data.Set.Finite.Lattice
/-- An increasing intersection distributes over finite union.  -/
Set.iInter_iUnion_of_monotone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [IsCodirectedOrder ι'] [Nonempty ι']
  {s : ι → ι' → Set α}, (∀ (i : ι), Monotone (s i)) → ⋂ j, ⋃ i, s i j = ⋃ i, ⋂ j, s i j
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS'.eq_def : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ) (x : ℕ),
  complEDS' b c d k x =
    match x with
    | 0 => 0
    | 1 => 1
    | n.succ.succ =>
      let m := n / 2 + 1;
      if hn : Even n then complEDS' b c d k m * complEDS₂ b c d (↑m * k)
      else
        have this := ⋯;
        complEDS' b c d k m ^ 2 * normEDS b c d ((↑m + 1) * k + 1) * normEDS b c d ((↑m + 1) * k - 1) -
          complEDS' b c d k (m + 1) ^ 2 * normEDS b c d (↑m * k + 1) * normEDS b c d (↑m * k - 1)
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.instFaithfulUliftFunctor : ∀ (R : Type u) [inst : CommRing R], (CommAlgCat.uliftFunctor R).Faithful
-- Mathlib.Analysis.Convex.StrictConvexSpace
norm_midpoint_lt_iff : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  ‖x‖ = ‖y‖ → (‖(1 / 2) • (x + y)‖ < ‖x‖ ↔ x ≠ y)
-- Init.Data.Option.Attach
Option.unattach_none : ∀ {α : Type u_1} {p : α → Prop}, none.unattach = none