mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Mathlib.Meta.Positivity.log_pos_of_isNegNat : ∀ {e : ℝ} {n : ℕ}, Mathlib.Meta.NormNum.IsInt e (Int.negOfNat n) → Nat.blt 1 n = true → 0 < Real.log e
-- Mathlib.Topology.Connected.PathConnected
isPathConnected_pathComponentIn : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {F : Set X}, x ∈ F → IsPathConnected (pathComponentIn F x)
-- Mathlib.Algebra.Colimit.Module
AddCommGroup.DirectLimit.hom_ext : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (G i)]
  {f : (i j : ι) → i ≤ j → G i →+ G j} [inst_2 : DecidableEq ι] (P : Type u_4) [inst_3 : AddCommMonoid P]
  {g₁ g₂ : AddCommGroup.DirectLimit G f →+ P},
  (∀ (i : ι), g₁.comp (AddCommGroup.DirectLimit.of G f i) = g₂.comp (AddCommGroup.DirectLimit.of G f i)) → g₁ = g₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.equiv_of_beq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap.Raw α β cmp} [inst : (k : α) → BEq (β k)]
  [inst_1 : Std.LawfulEqCmp cmp] [Std.TransCmp cmp] [∀ (k : α), LawfulBEq (β k)],
  m₁.WF → m₂.WF → m₁.beq m₂ = true → m₁.Equiv m₂
-- Mathlib.Order.CompleteLattice.Basic
Equiv.biInf_comp : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} {ι' : Type u_9} {g : ι' → α} (e : ι ≃ ι') (s : Set ι'),
  ⨅ i ∈ ⇑e.symm '' s, g (e i) = ⨅ i ∈ s, g i
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- Two finite measures are equal if they are equal on the π-system generating the σ-algebra
(and `univ`).  -/
MeasureTheory.ext_of_generate_finite : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (C : Set (Set α)),
  m0 = MeasurableSpace.generateFrom C →
    IsPiSystem C → ∀ [MeasureTheory.IsFiniteMeasure μ], (∀ s ∈ C, μ s = ν s) → μ Set.univ = ν Set.univ → μ = ν
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.iff_isIntegralHom_and_locallyOfFiniteType : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsFinite f ↔ AlgebraicGeometry.IsIntegralHom f ∧ AlgebraicGeometry.LocallyOfFiniteType f
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LeftLinear.instIsIsoμₗ : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.LeftLinear C] (c : C) (d : D),
  CategoryTheory.IsIso (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasUnifEigenvalue.eq_1 : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ : R) (k : ℕ∞), f.HasUnifEigenvalue μ k = ((f.genEigenspace μ) k ≠ ⊥)
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.forM : {α : Type u} →
  {cmp : α → α → Ordering} →
    {m : Type w → Type w₂} → [Monad m] → (α → m PUnit.{w + 1}) → Std.TreeSet.Raw α cmp → m PUnit.{w + 1}
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry?.induct_unfolding : ∀ {α : Type u} {β : Type v} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β) → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf none →
    (∀ (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) (some (k, v))) →
      (∀ (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
          (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)
              (Std.DTreeMap.Internal.Impl.Const.maxEntry? (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
              (Std.DTreeMap.Internal.Impl.Const.maxEntry? (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))) →
        ∀ (a : Std.DTreeMap.Internal.Impl α fun x => β), motive a (Std.DTreeMap.Internal.Impl.Const.maxEntry? a)
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] {c : ComplexShape ι} {F G : CategoryTheory.Functor W₁ W₂}
  [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms] (α : F ⟶ G) {C D : HomologicalComplex W₁ c}
  (f : C ⟶ D) {Z : HomologicalComplex W₂ c} (h : (G.mapHomologicalComplex c).obj D ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapHomologicalComplex c).map f)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app D) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.NatTrans.mapHomologicalComplex α c).app C)
      (CategoryTheory.CategoryStruct.comp ((G.mapHomologicalComplex c).map f) h)
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.instMin : {α : Type u_1} → [inst : TopologicalSpace α] → [inst_1 : LE α] → Min (ClopenUpperSet α)
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
/-- `forget F : ∫ᶜ F ⥤ 𝒮` is a fibered category.  -/
CategoryTheory.Pseudofunctor.CoGrothendieck.instIsFiberedForget : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat},
  (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F).IsFibered
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.mk : {B : Type u} → [inst : CategoryTheory.Bicategory B] → B → CategoryTheory.Bicategory.Adj B
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.extractLsb'_extractAndExtend_eq : ∀ {w i len : ℕ} {x : BitVec w},
  BitVec.extractLsb' (i * len) len (BitVec.extractAndExtend len x) = BitVec.extractAndExtendBit i len x
-- Mathlib.RingTheory.PowerBasis
PowerBasis.mem_span_pow : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {x y : S} {d : ℕ},
  d ≠ 0 → (y ∈ Submodule.span R (Set.range fun i => x ^ ↑i) ↔ ∃ f, f.natDegree < d ∧ y = (Polynomial.aeval x) f)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.SavedState.mk.injEq : ∀ (term term_1 : Lean.Elab.Term.SavedState), ({ term := term } = { term := term_1 }) = (term = term_1)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.universallyOpen_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.UniversallyOpen f ↔ (AlgebraicGeometry.topologically @IsOpenMap).universally f
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHomClass.exists_map_eq_of_map_le : ∀ {F : Type u_6} {α : outParam (Type u_7)} {β : outParam (Type u_8)} {inst : TopologicalSpace α} {inst_1 : Preorder α}
  {inst_2 : TopologicalSpace β} {inst_3 : Preorder β} {inst_4 : FunLike F α β} [self : EsakiaHomClass F α β] (f : F)
  ⦃a : α⦄ ⦃b : β⦄, f a ≤ b → ∃ c, a ≤ c ∧ f c = b
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaMon.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.shrinkYonedaMon.{w, v, u} =
    { obj := fun X => MonCat.shrinkFunctor.{w, v, v, u} (CategoryTheory.yonedaMon.obj X),
      map := fun {X Y} f => MonCat.shrinkFunctorMap (CategoryTheory.yonedaMon.map f), map_id := ⋯, map_comp := ⋯ }
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The direction of an affine subspace is the submodule spanned by
the pairwise differences of points.  (Except in the case of an empty
affine subspace, where the direction is the zero submodule, every
vector in the direction is the difference of two points in the affine
subspace.)

This can also be used to reinterpret an affine subspace that contains
zero as a submodule, see `direction_eq_self_iff_zero_mem`.
 -/
AffineSubspace.direction : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → AffineSubspace k P → Submodule k V
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- If a function is interval integrable with respect to a given measure `μ` on `a..b` then
it is integrable on `uIoc a b` with respect to `μ`.  -/
IntervalIntegrable.def' : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b → MeasureTheory.IntegrableOn f (Set.uIoc a b) μ
-- Mathlib.Analysis.Normed.Group.Basic
/-- A translated ball is a ball.  -/
setOf_sub_mem_ball_eq_ball : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a : E} {r : ℝ}, {x | x - a ∈ Metric.ball 0 r} = Metric.ball a r
-- Mathlib.Order.Lattice
inf_le_inf_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α} (c : α), b ≤ a → c ⊓ b ≤ c ⊓ a
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [IsEmpty n], CategoryTheory.IsIso (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Mathlib.GroupTheory.Sylow
Sylow.coe_subgroup_smul : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {g : G} {P : Sylow p G}, ↑(g • P) = MulAut.conj g • ↑P
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.foldrM_eq_foldrM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.ExtTreeMap.foldrM (fun a x d => f a d) init t = List.foldrM f init t.keys
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropy_eq_iSup_basis : ∀ {X : Type u_1} [inst : UniformSpace X] {ι : Sort u_2} {p : ι → Prop} {s : ι → SetRel X X},
  (uniformity X).HasBasis p s →
    ∀ (T : X → X) (F : Set X), Dynamics.coverEntropy T F = ⨆ i, ⨆ (_ : p i), Dynamics.coverEntropyEntourage T F (s i)
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
CategoryTheory.Precoverage.Saturate.brecOn : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {J : CategoryTheory.Precoverage C}
  {motive : (X : C) → (a : CategoryTheory.Sieve X) → J.Saturate X a → Prop} {X : C} {a : CategoryTheory.Sieve X}
  (t : J.Saturate X a),
  (∀ (X : C) (a : CategoryTheory.Sieve X) (t : J.Saturate X a),
      CategoryTheory.Precoverage.Saturate.below t → motive X a t) →
    motive X a t
-- Init.Data.Vector.Lemmas
Vector.getElem_swap_of_ne : ∀ {α : Type u_1} {n k : ℕ} {xs : Vector α n} {i j : ℕ} {hi : i < n} {hj : j < n} {hk : k < n},
  k ≠ i → k ≠ j → (xs.swap i j hi hj)[k] = xs[k]
-- Mathlib.Algebra.GroupWithZero.Submonoid.Pointwise
AddSubmonoid.mem_pointwise_smul_iff_inv_smul_mem : ∀ {G : Type u_2} {A : Type u_4} [inst : AddMonoid A] [inst_1 : Group G] [inst_2 : DistribMulAction G A] {a : G}
  {S : AddSubmonoid A} {x : A}, x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.ne_top : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsPrime → I ≠ ⊤
-- Mathlib.Data.Multiset.Count
Multiset.countP_pos_of_mem : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s : Multiset α} {a : α}, a ∈ s → p a → 0 < Multiset.countP p s
-- Init.Core
/-- A symmetric relation satisfies `r a b → r b a`.  -/
Std.Symm.symm : ∀ {α : Sort u} {r : α → α → Prop} [self : Std.Symm r] (a b : α), r a b → r b a
-- Mathlib.Analysis.Normed.Module.RCLike.Real
frontier_closedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ},
  r ≠ 0 → frontier (Metric.closedBall x r) = Metric.sphere x r
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
Filter.EventuallyEq.mfderivWithin_eq_of_mem : ∀ {𝕜 : 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 f₁ : M → M'} {x : M} {s : Set M},
  f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → mfderiv[s] f₁ x = mfderiv[s] f x
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The inf of two orthogonal subspaces equals the subspace orthogonal
to the sup.  -/
ClosedSubmodule.inf_orthogonal : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K₁ K₂ : ClosedSubmodule 𝕜 E), K₁ᗮ ⊓ K₂ᗮ = (K₁ ⊔ K₂)ᗮ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.mem_add : ∀ {α : Type u_2} [inst : Add α] {s t : Set α} {a : α}, a ∈ s + t ↔ ∃ x ∈ s, ∃ y ∈ t, x + y = a
-- Lean.Data.Json.FromToJson.Basic
Lean.NameMap.toJson : {α : Type} → [Lean.ToJson α] → Lean.NameMap α → Lean.Json
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_algHom : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (x : A),
  Polynomial.aeval (f x) = f.comp (Polynomial.aeval x)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.Λ'.Supports.match_1.eq_7 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q₁ q₂ : Turing.PartrecToTM2.Λ')
  (h_1 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k₁ k₂ : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (k : Turing.PartrecToTM2.K') →
      (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
        (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 : (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (p : Turing.PartrecToTM2.Γ' → Bool) →
      (k : Turing.PartrecToTM2.K') → (q : Turing.PartrecToTM2.Λ') → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (q : Turing.PartrecToTM2.Λ') → motive q.copy) (h_6 : (q : Turing.PartrecToTM2.Λ') → motive q.succ)
  (h_7 : (q₁ q₂ : Turing.PartrecToTM2.Λ') → motive (q₁.pred q₂))
  (h_8 : (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match q₁.pred q₂ with
    | Turing.PartrecToTM2.Λ'.move p k₁ k₂ q => h_1 p k₁ k₂ q
    | Turing.PartrecToTM2.Λ'.push k s q => h_2 k s q
    | Turing.PartrecToTM2.Λ'.read q => h_3 q
    | Turing.PartrecToTM2.Λ'.clear p k q => h_4 p k q
    | q.copy => h_5 q
    | q.succ => h_6 q
    | q₁.pred q₂ => h_7 q₁ q₂
    | Turing.PartrecToTM2.Λ'.ret k => h_8 k) =
    h_7 q₁ q₂
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instInhabited : Inhabited AddCommGrpCat
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Set.Finite.measurableSet_biUnion : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {f : β → Set α} {s : Set β},
  s.Finite → (∀ b ∈ s, MeasurableSet (f b)) → MeasurableSet (⋃ b ∈ s, f b)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.unop_injective : ∀ {G : Type u_2} [inst : Group G], Function.Injective Subgroup.unop
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- If an invariant measure is inner regular, then it gives less mass to sets with compact closure
than any other invariant measure, up to the scalar `addHaarScalarFactor μ' μ`.

Auxiliary lemma in the proof of the more general
`measure_isAddInvariant_eq_smul_of_isCompact_closure`, which gives equality for any
set with compact closure.  -/
MeasureTheory.Measure.smul_measure_isAddInvariant_le_of_isCompact_closure : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsAddHaarMeasure] [inst_7 : MeasureTheory.IsFiniteMeasureOnCompacts μ'] [inst_8 : μ'.IsAddLeftInvariant]
  [μ.InnerRegularCompactLTTop] {s : Set G},
  MeasurableSet s → IsCompact (closure s) → μ'.addHaarScalarFactor μ • μ s ≤ μ' s
-- Std.Data.HashMap.Lemmas
Std.HashMap.forIn_eq_forIn_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  (forIn m init fun a d => f a.1 d) = forIn m.keys init f
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuousOn : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R)
  {s : Set R}, ContinuousOn (fun x => Polynomial.eval x p) s
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- If `a` is in the family compression and can be compressed, then its compression is in the
original family.  -/
UV.sup_sdiff_mem_of_mem_compression : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α], a ∈ UV.compression u v s → v ≤ a → Disjoint u a → (a ⊔ u) \ v ∈ s
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.squareCylinders_eq_iUnion_image : ∀ {ι : Type u_2} {α : ι → Type u_1} (C : (i : ι) → Set (Set (α i))),
  MeasureTheory.squareCylinders C = ⋃ s, (fun t => (↑s).pi t) '' Set.univ.pi C
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vadd_subset_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β},
  s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.mem.eq_1 : ∀ {α : Type u_1} (a : FreeMonoid α) (m : α), a.mem m = (m ∈ FreeMonoid.toList a)
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.depthLB.eq_2 : ∀ (x : ℕ), RBTree.RBNode.depthLB RBTree.RBColor.black x = x
-- Std.Internal.UV.Timer
/-- `Timer`s are used to generate `IO.Promise`s that resolve after some time.

A `Timer` can be in one of 3 states:
- Right after construction it's initial.
- While it is ticking it's running.
- If it has stopped for some reason it's finished.

This together with whether it was set up as `repeating` with `Timer.new` determines the behavior
of all functions on `Timer`s.
 -/
Std.Internal.UV.Timer : Type
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.comm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.Equiv t₂ ↔ t₂.Equiv t₁
-- Init.Data.Int.Order
Int.max_add_right : ∀ (a b c : ℤ), max (a + c) (b + c) = max a b + c
-- Mathlib.Algebra.Group.Center
Set.decidableMemCentralizer.eq_1 : ∀ {M : Type u_1} {S : Set M} [inst : Mul M] [inst_1 : (a : M) → Decidable (∀ b ∈ S, b * a = a * b)] (x : M),
  Set.decidableMemCentralizer x = decidable_of_iff' (∀ m ∈ S, m * x = x * m) ⋯
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.preLeft_obj_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma (F.comp L) R),
  ((CategoryTheory.Comma.preLeft F L R).obj X).left = F.obj X.left
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln_complete : ∀ {c : Nat.Partrec.Code} {n x : ℕ}, x ∈ c.eval n ↔ ∃ k, x ∈ Nat.Partrec.Code.evaln k c n
-- Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Matrix.toLinearEquiv'_apply : ∀ {n : Type u_1} [inst : Fintype n] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : DecidableEq n] (P : Matrix n n R)
  (h : Invertible P), ↑(P.toLinearEquiv' h) = Matrix.toLin' P
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- After conversion to normal form on `U`, the function has normal form.
 -/
meromorphicNFOn_toMeromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (U : Set 𝕜), MeromorphicNFOn (toMeromorphicNFOn f U) U
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.condition : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g],
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) f =
    CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) g
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.rightInvSeq.match_1.eq_1 : ∀ {B : Type u_1} (motive : List B → Sort u_2) (h_1 : Unit → motive []) (h_2 : (i : B) → (ω : List B) → motive (i :: ω)),
  (match [] with
    | [] => h_1 ()
    | i :: ω => h_2 i ω) =
    h_1 ()
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The main program. See the section documentation for details.  -/
Turing.PartrecToTM2.tr : Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Stmt'
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.instIsAddCommutative_iSup : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Type u_4} [Nonempty ι] [inst_2 : Preorder ι] [IsDirectedOrder ι]
  {S : ι →o AddSubmonoid M} [hS : ∀ (i : ι), IsAddCommutative ↥(S i)], IsAddCommutative ↥(⨆ i, S i)
-- Mathlib.RingTheory.Flat.Basic
Module.Flat.iff_lTensor_injectiveₛ : ∀ {R : Type u} {M : Type v} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.Flat R M ↔
    ∀ ⦃P : Type u⦄ [inst_3 : AddCommMonoid P] [inst_4 : Module R P] (N : Submodule R P),
      Function.Injective ⇑(LinearMap.lTensor M N.subtype)
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.float32.sizeOf_spec : sizeOf Lean.IR.IRType.float32 = 1
-- Std.Do.WP.Sound
/-- From a `wp`-provable postcondition and a `MonadAttach.CanReturn` witness, conclude `P`
at that value. Convenient when the monad has a `LawfulMonadAttach` instance, since
`CanReturn` is typically definitional.
 -/
Std.Do.WPSound.of_wp_canReturn : ∀ {m : Type u → Type u_1} {ps : Std.Do.PostShape} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m ps]
  [Std.Do.WPSound m ps] [inst_4 : MonadAttach m] [LawfulMonadAttach m] {α : Type u} {x : m α} {a : α} {P : α → Prop},
  MonadAttach.CanReturn x a → (⊢ₛ (Std.Do.wp x).apply (Std.Do.PostCond.mayThrow fun a => ⌜P a⌝)) → P a
-- Plausible.Gen
Plausible.Gen.genericFailure : Plausible.GenError
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
/-- A set `s` in a lattice ordered group is *solid* if for all `x ∈ s` and all `y ∈ α` such that
`|y| ≤ |x|`, then `y ∈ s`.  -/
LatticeOrderedAddCommGroup.IsSolid : {α : Type u_1} → [Lattice α] → [AddCommGroup α] → Set α → Prop
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.stableUnderComposition : RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Mathlib.MeasureTheory.Measure.Map
/-- Even if `s` is not measurable, `map f μ s = 0` implies that `μ (f ⁻¹' s) = 0`.  -/
MeasureTheory.Measure.preimage_null_of_map_null : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, AEMeasurable f μ → ∀ {s : Set β}, (MeasureTheory.Measure.map f μ) s = 0 → μ (f ⁻¹' s) = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.self_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {k : α} {v : β} {kmi : α}, (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.Data.Set.Lattice
Set.iUnion_iUnion_eq_left : ∀ {α : Type u_1} {β : Type u_2} {b : β} {s : (x : β) → x = b → Set α}, ⋃ x, ⋃ (h : x = b), s x h = s b ⋯