mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.sInf_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (S : Set (NonUnitalStarSubalgebra R A)),
  (sInf S).toNonUnitalSubalgebra = sInf (NonUnitalStarSubalgebra.toNonUnitalSubalgebra '' S)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).minKey? = some (t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k')
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a commutative subtraction monoid under pointwise operations if `α` is.  -/
Finset.subtractionCommMonoid : {α : Type u_2} → [DecidableEq α] → [SubtractionCommMonoid α] → SubtractionCommMonoid (Finset α)
-- Mathlib.NumberTheory.Dioph
Dioph.ex_dioph : ∀ {α β : Type u} {S : Set (α ⊕ β → ℕ)}, Dioph S → Dioph {v | ∃ x, Sum.elim v x ∈ S}
-- Mathlib.Tactic.ClickSuggestions.SectionState
/-- Whether the section corresponds to local hypotheses, declarations from the current file,
or imported declarations.  -/
Mathlib.Tactic.ClickSuggestions.SectionKind : Type
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.congr_identDistrib : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal} {Ω' : Type u_2}
  {mΩ' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} {Y : Ω' → ℝ},
  ProbabilityTheory.HasSubgaussianMGF X c μ →
    ProbabilityTheory.IdentDistrib X Y μ μ' → ProbabilityTheory.HasSubgaussianMGF Y c μ'
-- Mathlib.Analysis.Normed.Group.Continuity
/-- See `tendsto_norm_zero` for a version with full neighborhoods.  -/
tendsto_norm_nhdsNE_zero : ∀ {E : Type u_4} [inst : NormedAddGroup E], Filter.Tendsto norm (nhdsWithin 0 {0}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
-- Init.Data.SInt.Lemmas
Int32.eq_iff_ofBitVec_eq : ∀ {a b : BitVec 32}, a = b ↔ Int32.ofBitVec a = Int32.ofBitVec b
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_iSup_of_disjoint : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {m : ι → MeasurableSpace Ω},
  (∀ (i : ι), m i ≤ _mΩ) →
    ProbabilityTheory.Kernel.iIndep m κ μ →
      ∀ {S T : Set ι}, Disjoint S T → ProbabilityTheory.Kernel.Indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) κ μ
-- Mathlib.Topology.MetricSpace.HausdorffDimension
Real.dimH_univ_pi_fin : ∀ (n : ℕ), dimH Set.univ = ↑n
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.instIsZLatticeRealMixedSpaceIntegerLattice : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  IsZLattice ℝ (NumberField.mixedEmbedding.euclidean.integerLattice K)
-- Lean.Linter.UnusedVariables
Lean.Linter.UnusedVariables.References.mk.injEq : ∀ (constDecls : Std.HashSet Lean.Syntax.Range)
  (fvarDefs : Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition)
  (fvarUses : Std.HashSet Lean.FVarId) (fvarAliases : Std.HashMap Lean.FVarId Lean.FVarId)
  (assignments : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)) (constDecls_1 : Std.HashSet Lean.Syntax.Range)
  (fvarDefs_1 : Std.HashMap Lean.Syntax.Range Lean.Linter.UnusedVariables.FVarDefinition)
  (fvarUses_1 : Std.HashSet Lean.FVarId) (fvarAliases_1 : Std.HashMap Lean.FVarId Lean.FVarId)
  (assignments_1 : Array (Lean.PersistentHashMap Lean.MVarId Lean.Expr)),
  ({ constDecls := constDecls, fvarDefs := fvarDefs, fvarUses := fvarUses, fvarAliases := fvarAliases,
        assignments := assignments } =
      { constDecls := constDecls_1, fvarDefs := fvarDefs_1, fvarUses := fvarUses_1, fvarAliases := fvarAliases_1,
        assignments := assignments_1 }) =
    (constDecls = constDecls_1 ∧
      fvarDefs = fvarDefs_1 ∧ fvarUses = fvarUses_1 ∧ fvarAliases = fvarAliases_1 ∧ assignments = assignments_1)
-- Mathlib.Order.Partition.Basic
Partition.instSymmRel : ∀ {α : Type u_1} {u : Set α} (P : Partition u), Std.Symm P.Rel
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.Odd.toUnitHom_eval_neg_one : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m), ψ.Odd → (MulChar.toUnitHom ψ) (-1) = -1
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st.eq_1 : ∀ (x : ℝ*), x.st = if h : ∃ r, x.IsSt r then Classical.choose h else 0
-- Mathlib.Util.MemoFix
_private.Mathlib.Util.MemoFix.0.injectIntoBaseIO : {α : Type} → α → BaseIO α
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.IsTriangulatedClosed₃.ext₃' : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} 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} {inst_5 : CategoryTheory.Pretriangulated C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsTriangulatedClosed₃],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, P T.obj₁ → P T.obj₂ → P.isoClosure T.obj₃
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_zsmul_sub_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp a b • p + toIocMod hp a b = b
-- Init.Data.Format.Basic
/-- Whether the given directive indicates that flattening should occur.  -/
Std.Format.FlattenAllowability.shouldFlatten : Std.Format.FlattenAllowability → Bool
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Any limit cone defines a weak limit cone with the same underlying cone over `F` and the same
lifts.
 -/
CategoryTheory.Limits.WeakLimitCone.ofLimitCone : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.LimitCone F → CategoryTheory.Limits.WeakLimitCone F
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upperCrossingTime_lt_succ : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  a < b →
    MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N →
      MeasureTheory.upperCrossingTime a b f N n ω < MeasureTheory.upperCrossingTime a b f N (n + 1) ω
-- Mathlib.Combinatorics.Additive.FreimanHom
/-- An `n`-Freiman homomorphism from a set `A` to a set `B` is a map which preserves products of `n`
elements.  -/
IsMulFreimanIso : {α : Type u_2} → {β : Type u_3} → [CommMonoid α] → [CommMonoid β] → ℕ → Set α → Set β → (α → β) → Prop
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.one_lt_of_one_lt_of_mk_lt : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  1 < a → MulArchimedeanClass.mk a < MulArchimedeanClass.mk (b / a) → 1 < b
-- Mathlib.NumberTheory.Real.Irrational
Irrational.ratCast_div : ∀ {x : ℝ}, Irrational x → ∀ {q : ℚ}, q ≠ 0 → Irrational (↑q / x)
-- Mathlib.RingTheory.Localization.Defs
isLocalization_iff_isLocalizationMap : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S], IsLocalization M S ↔ M.IsLocalizationMap ⇑(algebraMap R S)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
instPartialOrderHomogeneousIdeal : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : SetLike σ A] →
          [inst_2 : AddSubmonoidClass σ A] →
            {𝒜 : ι → σ} →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddMonoid ι] → [inst_5 : GradedRing 𝒜] → PartialOrder (HomogeneousIdeal 𝒜)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC : Lean.Grind.CommRing.Expr → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_iInf : ∀ {K : Type u} [inst : DivisionRing K] {ι : Sort u_1} {S : ι → Subfield K} {x : K}, x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_ne_zero_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0
-- Mathlib.Computability.Language
Language.reverse_iSup : ∀ {α : Type u_1} {ι : Sort u_4} (l : ι → Language α), (⨆ i, l i).reverse = ⨆ i, (l i).reverse
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.tendsto_zero : ∀ {α : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {l : Filter α} {f : α → Γ₀},
  Filter.Tendsto f l (nhds 0) ↔ ∀ (γ₀ : Γ₀), γ₀ ≠ 0 → ∀ᶠ (x : α) in l, f x < γ₀
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineIndependent.injOn_affineCombination_fintypeAffineCoords : ∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
  AffineIndependent k p → Set.InjOn ⇑(Finset.affineCombination k Finset.univ p) ↑(fintypeAffineCoords ι k)
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- A version of `Equiv.optionCongr` for `WithZero`.  -/
MulEquiv.withZero : {α : Type u_1} → {β : Type u_2} → [inst : Group α] → [inst_1 : Group β] → α ≃* β ≃ (WithZero α ≃* WithZero β)
-- Mathlib.Order.Lattice
Ne.inf_lt_or_inf_lt : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ≠ b → a ⊓ b < a ∨ a ⊓ b < b
-- Mathlib.Data.Seq.Computation
Computation.mem_bind : ∀ {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β}, a ∈ s → b ∈ f a → b ∈ s.bind f
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.mem_grade_iff : ∀ {M : Type u_1} (R : Type u_3) [inst : CommSemiring R] (m : M) (a : AddMonoidAlgebra R M),
  a ∈ AddMonoidAlgebra.grade R m ↔ a.coeff.support ⊆ {m}
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.comp_nsmul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ M) (n : ℕ) (h : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp h (n • f) = n • CategoryTheory.CategoryStruct.comp h f
-- Mathlib.RepresentationTheory.Tannaka
/-- The right regular representation `rightRegular` on `G → k` as a `FDRep k G`.  -/
TannakaDuality.FiniteGroup.rightFDRep : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → [Finite G] → FDRep k G
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableAt_iff_comp_sub_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {a b : 𝕜},
  DifferentiableAt 𝕜 f a ↔ DifferentiableAt 𝕜 (fun x => f (x - b)) (a + b)
-- Mathlib.MeasureTheory.Measure.Regular
/-- We say that a measure `μ` is *inner regular* with respect to predicates `p q : Set α → Prop`,
if for every `U` such that `q U` and `r < μ U`, there exists a subset `K ⊆ U` satisfying `p K`
of measure greater than `r`.

This definition is used to prove some facts about regular and weakly regular measures without
repeating the proofs.  -/
MeasureTheory.Measure.InnerRegularWRT : {α : Type u_1} → {x : MeasurableSpace α} → MeasureTheory.Measure α → (Set α → Prop) → (Set α → Prop) → Prop
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} {φ φ' : D₁ ⟶ D₂},
  (∀ (i : ι), φ.hom i = φ'.hom i) → φ = φ'
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.sec_spec' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (z : N), f (f.sec z).1 = f ↑(f.sec z).2 * z
-- Mathlib.RingTheory.ZariskisMainTheorem
Algebra.ZariskisMainProperty.of_isIntegral : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S)
  [p.IsPrime] [Algebra.IsIntegral R S], Algebra.ZariskisMainProperty R p
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biInter_coe : ∀ {α : Type u_2} {β : Type u_3} (s : Finset α) (t : α → Set β), ⋂ x ∈ ↑s, t x = ⋂ x ∈ s, t x
-- Mathlib.FieldTheory.AbsoluteGaloisGroup
_private.Mathlib.FieldTheory.AbsoluteGaloisGroup.0.Field.termG_K_ab : Lean.ParserDescr
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.IsDecompOn.comp' : ∀ {X : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : MulAction G X] {g f : X → X} {B A : Set X} {T S : Finset G},
  Equidecomp.IsDecompOn g B T → Equidecomp.IsDecompOn f A S → Equidecomp.IsDecompOn (g ∘ f) (A ∩ f ⁻¹' B) (T * S)
-- Init.Data.Iterators.Consumers.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.Iter.Partial.size : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → Std.Iter.Partial β → ℕ
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyKey.mk : ℕ → ℕ → ℕ → String → Array Lean.Meta.AbstractMVarsResult → Mathlib.Tactic.ClickSuggestions.ApplyKey
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `upperHemicontinuousOn_iff_frequently`. -/
UpperHemicontinuousOn.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  UpperHemicontinuousOn f s →
    ∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : Cᵒᵖ ⥤ D` creates limits, then `F.rightOp : C ⥤ Dᵒᵖ` creates colimits.  -/
CategoryTheory.Limits.createsColimitsRightOp : {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.CreatesLimits F] → CategoryTheory.CreatesColimits F.rightOp
-- Mathlib.Data.List.Infix
List.subset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (l : List α), l ⊆ List.insert a l
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isSome_get?_eq_contains : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α},
  (m.get? a).isSome = m.contains a
-- Mathlib.Algebra.Quandle
/-- The induced group homomorphism from the enveloping group into bijections of the rack,
using `Rack.toConj`. Satisfies the property `envelAction_prop`.

This gives the rack `R` the structure of an augmented rack over `EnvelGroup R`.
 -/
Rack.envelAction : {R : Type u_1} → [inst : Rack R] → Rack.EnvelGroup R →* R ≃ R
-- Mathlib.Data.EReal.Basic
EReal.preimage_coe_Ico_top : ∀ (x : ℝ), Real.toEReal ⁻¹' Set.Ico ↑x ⊤ = Set.Ici x
-- Mathlib.Analysis.Calculus.FDeriv.Linear
ContinuousLinearMap.hasStrictFDerivAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E →L[𝕜] F) {x : E}, HasStrictFDerivAt (⇑f) f x
-- Mathlib.Order.UpperLower.Prod
LowerSet.prod_le_prod_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s₁ s₂ : LowerSet α} {t₁ t₂ : LowerSet β},
  s₁ ×ˢ t₁ ≤ s₂ ×ˢ t₂ ↔ s₁ ≤ s₂ ∧ t₁ ≤ t₂ ∨ s₁ = ⊥ ∨ t₁ = ⊥
-- Mathlib.RingTheory.Extension.Generators
/-- The `Generators` containing the whole algebra, which induces the canonical map  `R[S] → S`.  -/
Algebra.Generators.self : (R : Type u) →
  (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Generators R S S
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.constantsOnFunc.eq_2 : ∀ (α : Type u') (n : ℕ), FirstOrder.Language.constantsOnFunc α n.succ = PEmpty.{u' + 1}
-- Mathlib.Order.KrullDimension
Order.one_le_krullDim_iff : ∀ {α : Type u_1} [inst : Preorder α], 1 ≤ Order.krullDim α ↔ ∃ x y, x < y
-- Mathlib.MeasureTheory.Covering.Besicovitch
/-- The **measurable Besicovitch covering theorem**. Assume that, for any `x` in a set `s`,
one is given a set of admissible closed balls centered at `x`, with arbitrarily small radii.
Then there exists a disjoint covering of almost all `s` by admissible closed balls centered at some
points of `s`.
This version requires that the underlying measure is finite, and that the space has the Besicovitch
covering property (which is satisfied for instance by finite-dimensional normed real vector spaces).
It expresses the conclusion in a slightly awkward form (with a subset of `α × ℝ`) coming from the
proof technique.
For a version assuming that the measure is s-finite,
see `exists_disjoint_closedBall_covering_ae_aux`.
For a version giving the conclusion in a nicer form, see `exists_disjoint_closedBall_covering_ae`.
 -/
Besicovitch.exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux : ∀ {α : Type u_1} [inst : MetricSpace α] [SecondCountableTopology α] [inst_2 : MeasurableSpace α]
  [OpensMeasurableSpace α] [HasBesicovitchCovering α] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ]
  (f : α → Set ℝ) (s : Set α),
  (∀ x ∈ s, ∀ δ > 0, (f x ∩ Set.Ioo 0 δ).Nonempty) →
    ∃ t,
      t.Countable ∧
        (∀ p ∈ t, p.1 ∈ s) ∧
          (∀ p ∈ t, p.2 ∈ f p.1) ∧
            μ (s \ ⋃ p ∈ t, Metric.closedBall p.1 p.2) = 0 ∧ t.PairwiseDisjoint fun p => Metric.closedBall p.1 p.2
-- Init.Data.UInt.Basic
/-- Bitwise complement, also known as bitwise negation, for 16-bit unsigned integers. Usually accessed
via the `~~~` prefix operator.

Each bit of the resulting integer is the opposite of the corresponding bit of the input integer.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.complement : UInt16 → UInt16
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.ofHom₂_hom_apply_hom : ∀ {R : Type u_1} [inst : CommSemiring R] {M N P : SemimoduleCat R} (f : ↑M →ₗ[R] ↑N →ₗ[R] ↑P) (x : ↑M),
  SemimoduleCat.Hom.hom ((SemimoduleCat.Hom.hom (SemimoduleCat.ofHom₂ f)) x) = f x
-- Std.Data.Internal.List.Associative
Std.Internal.List.distinctKeys_of_sublist : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)},
  l'.Sublist l → Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys l'
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.cosKernel.eq_1 : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.cosKernel a x = ⋯.lift a
-- Aesop.RuleSet
Aesop.BaseRuleSet.add : Aesop.BaseRuleSet → Aesop.BaseRuleSetMember → Aesop.BaseRuleSet
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso_inv_comp_descOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) {A : C} (k : S.X₂ ⟶ A)
  (hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [inst_2 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp h.opcyclesIso.inv (S.descOpcycles k hk) = h.descQ k hk
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The fundamental property of the adjoint.  -/
ContinuousLinearMap.adjoint_inner_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F) (x : E) (y : F),
  inner 𝕜 x ((ContinuousLinearMap.adjoint A) y) = inner 𝕜 (A x) y
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.builder.injEq : ∀ (b b_1 : Aesop.Frontend.DBuilderName),
  (Aesop.Frontend.Feature.builder b = Aesop.Frontend.Feature.builder b_1) = (b = b_1)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flip_f₃₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C), sq.flip.f₃₄ = sq.f₂₄
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- The product of `X` with an initial object in a category with strict initial objects is itself
initial.
This is the generalisation of the fact that `X × Empty ≃ Empty` for types (or `n * 0 = 0`).
 -/
CategoryTheory.Limits.mulInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasStrictInitialObjects C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        (X : C) → [inst_3 : CategoryTheory.Limits.HasBinaryProduct X (⊥_ C)] → X ⨯ ⊥_ C ≅ ⊥_ C
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The difference constant `σ[A, B]` of two finsets `A` and `B` in a group is `|A - B| / |A|`.  -/
Combinatorics.Additive.«termδ[_,_]» : Lean.ParserDescr
-- Mathlib.Data.Set.Image
Sum.range_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ⊕ β → γ),
  Set.range f = Set.range (f ∘ Sum.inl) ∪ Set.range (f ∘ Sum.inr)
-- Mathlib.Data.List.Destutter
List.destutter_eq_self_iff : ∀ {α : Type u_1} (R : α → α → Prop) [inst : DecidableRel R] (l : List α), List.destutter R l = l ↔ List.IsChain R l
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_EStateM : ∀ {α ε σ : Type u_1} {x : EStateM ε σ α} {h : ε → EStateM ε σ α}
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))),
  ⦃fun s =>
    (Std.Do.wp x).apply
      (Q.1, fun e s' => (Std.Do.wp (h e)).apply Q (EStateM.Backtrackable.restore s' (EStateM.Backtrackable.save s)),
        Q.2.2)
      s⦄
    MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- We say that a set `H : Set (X → α)` of functions is equicontinuous if the family
`(↑) : ↥H → (X → α)` is equicontinuous.  -/
Set.Equicontinuous : {X : Type u_3} → {α : Type u_6} → [tX : TopologicalSpace X] → [uα : UniformSpace α] → Set (X → α) → Prop
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a fallback : α} {h : a ∈ t},
  t.get a h = t.getD a fallback
-- Std.Data.HashSet.RawLemmas
_private.Std.Data.HashSet.RawLemmas.0.Std.HashSet.Raw.ext : ∀ {α : Type u} {m m' : Std.HashSet.Raw α}, m.inner = m'.inner → m = m'
-- Mathlib.Algebra.BigOperators.Finprod
Multiset.support_fun_nsmul_count_subset : ∀ {α : Type u_1} {M : Type u_2} [inst : DecidableEq α] [inst_1 : AddCommMonoid M] (s : Multiset α) (f : α → M),
  (Function.support fun a => Multiset.count a s • f a) ⊆ ↑s.toFinset
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_div_div₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Div β]
  [MeasurableDiv₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k l : ι), i ≠ k → i ≠ l → j ≠ k → j ≠ l → ProbabilityTheory.Kernel.IndepFun (f i / f j) (f k / f l) κ μ
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.id_apply : ∀ (X : Type u_1) (a : X), (TypeCat.Fun.id X) a = a
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.w_def : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (D : ℝ),
  ExistsContDiffBumpBase.w D = fun x =>
    ((∫ (x : E), ExistsContDiffBumpBase.u x ∂MeasureTheory.Measure.addHaar) * |D| ^ Module.finrank ℝ E)⁻¹ •
      ExistsContDiffBumpBase.u (D⁻¹ • x)
-- Mathlib.Order.Heyting.Basic
hnot_hnot_sup_distrib : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a b : α), ￢￢(a ⊔ b) = ￢￢a ⊔ ￢￢b
-- Init.Data.BitVec.Basic
/-- Count the number of trailing zeros.  -/
BitVec.ctz : {w : ℕ} → BitVec w → BitVec w