mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.coe_comp : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (g : N →ₙ* P)
  (f : M →ₙ* N), ⇑(g.comp f) = ⇑g ∘ ⇑f
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s t : Set β} {a : α}, a • s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a • b ∈ t
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.associator_actionHom : ∀ {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} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c₁ c₂ c₃ : C) (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
        (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom d)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁
            (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃) d).hom
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c₁
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₂ c₃ d).hom)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso
          (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂) c₃ d).hom
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c₁ c₂
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c₃ d)).hom
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.absolutelyContinuous_sum_left : ∀ {α : Type u_1} {ι : Type u_4} {mα : MeasurableSpace α} {ν : MeasureTheory.Measure α}
  {μs : ι → MeasureTheory.Measure α},
  (∀ (i : ι), (μs i).AbsolutelyContinuous ν) → (MeasureTheory.Measure.sum μs).AbsolutelyContinuous ν
-- Mathlib.Geometry.Euclidean.MongePoint
/-- Given any triangle in an orthocentric system, the fourth point is
its orthocenter.  -/
EuclideanGeometry.OrthocentricSystem.eq_insert_orthocenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : Set P},
  EuclideanGeometry.OrthocentricSystem s →
    ∀ {t : Affine.Triangle ℝ P}, Set.range t.points ⊆ s → s = insert t.orthocenter (Set.range t.points)
-- Mathlib.AlgebraicTopology.SimplicialObject.Homotopy
CategoryTheory.SimplicialObject.Homotopy.h_castSucc_comp_δ_succ_of_lt_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject C} {f g : X ⟶ Y}
  (self : CategoryTheory.SimplicialObject.Homotopy f g) {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)),
  j.castSucc < i →
    ∀ {Z : C} (h : Y.obj (Opposite.op { len := n + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (self.h j.castSucc) (CategoryTheory.CategoryStruct.comp (Y.δ i.succ) h) =
        CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (self.h j) h)
-- Lean.Environment
_private.Lean.Environment.0.Lean.instNonemptyAsyncContext : Nonempty Lean.AsyncContext✝
-- Mathlib.RingTheory.Algebraic.Denominator
/-- The natural-number denominator of an element `x` of a ring: it is the absolute value of the
denominator of `x` over `ℤ`.  -/
Algebra.natDenominator : {S : Type u_2} → [CommRing S] → S → ℕ
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f` is continuous
at `a`, then the derivative of `u ↦ ∫ x in u..b, f x` at `a` equals `-f a`.  -/
intervalIntegral.deriv_integral_left : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds a) MeasureTheory.volume →
      ContinuousAt f a → deriv (fun u => ∫ (x : ℝ) in u..b, f x) a = -f a
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithLowerSet.instTopologicalSpace : {α : Type u_1} → [Preorder α] → TopologicalSpace (Topology.WithLowerSet α)
-- Mathlib.GroupTheory.GroupAction.DomAct.ActionHom
DomMulAct.smul_mulActionHom_apply : ∀ {M : Type u_1} {α : Type u_2} {N : Type u_3} {β : Type u_4} [inst : SMul M α] [inst_1 : SMul N α]
  [inst_2 : SMulCommClass M N α] [inst_3 : SMul N β] (c : Mᵈᵐᵃ) (f : α →ₑ[id] β) (a : α),
  (c • f) a = f (DomMulAct.mk.symm c • a)
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_eq_group_inv : ∀ {α : Type u} [inst : Group α] (a : α) [inst_1 : Invertible a], ⅟a = a⁻¹
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.instFintypeZero.eq_1 : ∀ {α : Type u_2} [inst : Zero α], Set.instFintypeZero = Set.fintypeSingleton 0
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithLower.isOpen_def : ∀ {α : Type u_1} [inst : Preorder α] (T : Set (Topology.WithLower α)),
  IsOpen T ↔ IsOpen (⇑Topology.WithLower.toLower ⁻¹' T)
-- Mathlib.Data.ENat.Basic
/-- A version of `ENat.map` for `RingHom`s.  -/
RingHom.ENatMap : {S : Type u_2} →
  [inst : CommSemiring S] →
    [inst_1 : PartialOrder S] →
      [inst_2 : CanonicallyOrderedAdd S] →
        [inst_3 : DecidableEq S] → [inst_4 : Nontrivial S] → (f : ℕ →+* S) → Function.Injective ⇑f → ℕ∞ →+* WithTop S
-- Mathlib.Analysis.Normed.Group.Uniform
AddMonoidHomClass.lipschitz_of_bound_nnnorm : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : NNReal),
  (∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊) → LipschitzWith C ⇑f
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv_mul_self : ∀ (a b : ℤ), a / b * b = a - a % b
-- Mathlib.Analysis.SpecialFunctions.Sqrt
Real.deriv_sqrt_aux : ∀ {x : ℝ}, x ≠ 0 → HasStrictDerivAt (fun x => √x) (1 / (2 * √x)) x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ n (fun x => √x) x
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_singleton_group_smul_eq : ∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {G : Type u_9}
  [inst_3 : Group G] [inst_4 : SMul G R] [inst_5 : MulAction G M] [IsScalarTower G R M] (g : G) (x : M),
  R ∙ g • x = R ∙ x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₁.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupCohomology.isoCocycles₁ A =
    CategoryTheory.ShortComplex.cyclesMapIso' (groupCohomology.isoShortComplexH1 A)
      (HomologicalComplex.sc (groupCohomology.inhomogeneousCochains A) 1).leftHomologyData
      (groupCohomology.shortComplexH1 A).moduleCatLeftHomologyData
-- Init.Grind.Ring.Basic
/-- A commutative ring, i.e. a ring with commutative multiplication.
 -/
Lean.Grind.CommRing : Type u → Type u
-- Mathlib.Algebra.Star.Pointwise
Set.Finite.star : ∀ {α : Type u_1} [inst : InvolutiveStar α] {s : Set α}, s.Finite → (star s).Finite
-- Mathlib.Algebra.Group.Semiconj.Basic
AddSemiconjBy.eq_zero_iff : ∀ {G : Type u_1} [inst : AddGroup G] (a : G) {x y : G}, AddSemiconjBy a x y → (x = 0 ↔ y = 0)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A B : Subalgebra R S), A.mulMap B = Algebra.TensorProduct.productMap A.val B.val
-- Mathlib.Topology.Separation.CompletelyRegular
completelyRegularSpace_inf : ∀ {X : Type u_1} {t₁ t₂ : TopologicalSpace X},
  CompletelyRegularSpace X → CompletelyRegularSpace X → CompletelyRegularSpace X
-- Init.Data.Int.Linear
Int.Internal.Linear.diseq_split : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.diseq_split_cert p₁ p₂ p₃ = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≠ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 ∨ Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Batteries.Data.List.Basic
/-- `forDiagM f l` calls `f` on all elements in the upper triangular part of `l × l`.
That is, for each `e ∈ l`, it will run `f e e` and then `f e e'`
for each `e'` that appears after `e` in `l`.
```
forDiagM f [1, 2, 3] = do f 1 1; f 1 2; f 1 3; f 2 2; f 2 3; f 3 3
```
 -/
List.forDiagM : {m : Type u_1 → Type u_2} → {α : Type u_3} → [Monad m] → (α → α → m PUnit.{u_1 + 1}) → List α → m PUnit.{u_1 + 1}
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonUnitalSemiring` instance along a surjective function.  -/
Function.Surjective.nonUnitalSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NonUnitalSemiring R] →
                  f 0 = 0 →
                    (∀ (x y : R), f (x + y) = f x + f y) →
                      (∀ (x y : R), f (x * y) = f x * f y) →
                        (∀ (n : ℕ) (x : R), f (n • x) = n • f x) → NonUnitalSemiring S
-- Mathlib.RingTheory.Extension.Basic
/-- The underlying ring homomorphism of a hom between extensions.  -/
Algebra.Extension.Hom.toRingHom : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u_1} →
              {S' : Type u_2} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] → [inst_7 : Algebra S S'] → P.Hom P' → P.Ring →+* P'.Ring
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkSimpLike : Lean.Linter.MissingDocs.SimpleHandler
-- Mathlib.MeasureTheory.Integral.CompactlySupported
/-- Integration as a positive linear functional on `C_c(X, ℝ≥0)`.  -/
CompactlySupportedContinuousMap.integralLinearMap : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    [inst_1 : MeasurableSpace X] →
      [OpensMeasurableSpace X] →
        (μ : MeasureTheory.Measure X) →
          [MeasureTheory.IsFiniteMeasureOnCompacts μ] → CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_ball_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] [Nontrivial E] (x : E) {r : ℝ},
  0 ≤ r → ∀ (s : ℝ), μ (Metric.ball x (r * s)) = ENNReal.ofReal (r ^ Module.finrank ℝ E) * μ (Metric.ball 0 s)
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- Möbius inversion for functions to a `Ring`.  -/
ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq : ∀ {R : Type u_1} [inst : NonAssocRing R] {f g : ℕ → R},
  (∀ n > 0, ∑ i ∈ n.divisors, f i = g n) ↔
    ∀ n > 0, ∑ x ∈ n.divisorsAntidiagonal, ↑(ArithmeticFunction.moebius x.1) * g x.2 = f n
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
_private.Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup.0.Matrix.SpecialLinearGroup.diag2_coe.match_1.eq_1 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_1 ()
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.agree_iff_agree' : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} (x y : F.M),
  PFunctor.Approx.Agree (x.approx n) (y.approx (n + 1)) ↔ PFunctor.M.Agree' n x y
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.setOfPred_sOppSide_eq_image2`. -/
AffineSubspace.setOf_sOppSide_eq_image2 : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x p : P},
  x ∉ s → p ∈ s → {y | s.SOppSide x y} = Set.image2 (fun t q => t • (x -ᵥ p) +ᵥ q) (Set.Iio 0) ↑s
-- Mathlib.Data.Prod.Lex
Prod.Lex.instDenselyOrderedLexOfNoMaxOrder : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMaxOrder β] [DenselyOrdered β],
  DenselyOrdered (Lex (α × β))
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.bitwise.match_1.eq_3 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.negSucc m, Int.ofNat n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_3 m n
-- Init.Data.Vector.Lemmas
Vector.replicate_append_replicate : ∀ {n : ℕ} {α : Type u_1} {a : α} {m : ℕ}, Vector.replicate n a ++ Vector.replicate m a = Vector.replicate (n + m) a
-- Mathlib.Algebra.Group.Units.Equiv
/-- A version of `Equiv.addRight (-a) b` that is defeq to `b - a`.  -/
Equiv.subRight : {G : Type u_5} → [AddGroup G] → G → G ≃ G
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegrable_fun_neg_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b}, CurveIntegrable (fun x => -ω x) γ ↔ CurveIntegrable ω γ
-- Mathlib.Computability.RecursiveIn
Computable.computableIn : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → β} {O : Set (ℕ →. ℕ)},
  Computable f → ComputableIn O f
-- Init.Data.Nat.Lemmas
Nat.pos_of_lt_add_right : ∀ {n k : ℕ}, n < n + k → 0 < k
-- Mathlib.RingTheory.Extension.Basic
/-- The action of `S` on `P.Cotangent` for an extension `P → S`.  -/
Algebra.Extension.Cotangent.val_smul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (r : S) (x : P.Cotangent), (r • x).val = P.σ r • x.val
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Iic.injEq : ∀ (n n_1 : Lean.Term), (BigOperators.FinsetResult.Iic✝ n = BigOperators.FinsetResult.Iic✝ n_1) = (n = n_1)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J),
  CategoryTheory.CategoryStruct.comp (D.t i j) (D.t j i) = CategoryTheory.CategoryStruct.id (D.V (i, j))
-- Mathlib.Topology.CantorBendixson
CantorBendixson.iteratedDerivedSet.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X),
  CantorBendixson.iteratedDerivedSet s = OrdinalApprox.gfpApprox relDerivedSet s
-- Mathlib.Control.Functor
Functor.map_id : ∀ {F : Type u → Type v} {α : Type u} [inst : Functor F] [LawfulFunctor F], (fun x => id <$> x) = id
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the pure predicate `p` returns `true` for
all element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are
examined in order of iteration.
 -/
Std.Iter.all : {α β : Type w} → [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id Id] → (β → Bool) → Std.Iter β → Bool
-- Init.Data.Array.MinMax
Array.min?_eq_some_min : ∀ {α : Type u_1} [inst : Min α] {xs : Array α} (h : xs ≠ #[]), xs.min? = some (xs.min h)
-- Mathlib.Data.Int.Init
Int.div_lt_iff_of_dvd_of_pos : ∀ {a b c : ℤ}, 0 < b → b ∣ a → (a / b < c ↔ a < b * c)
-- Mathlib.Algebra.Star.Module
skewAdjointPart_comp_subtype_selfAdjoint : ∀ (R : Type u_1) {A : Type u_2} [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2], skewAdjointPart R ∘ₗ (selfAdjoint.submodule R A).subtype = 0
-- Mathlib.Data.PNat.Find
PNat.find_mono : ∀ {p q : ℕ+ → Prop} [inst : DecidablePred p] [inst_1 : DecidablePred q],
  (∀ (n : ℕ+), q n → p n) → ∀ {hp : ∃ n, p n} {hq : ∃ n, q n}, PNat.find hp ≤ PNat.find hq
-- Std.Sat.CNF.Dimacs
_private.Std.Sat.CNF.Dimacs.0.Std.Sat.CNF.DimacsState.numClauses : Std.Sat.CNF.DimacsState✝ → ℕ
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousWithinAt_inv_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], LowerSemicontinuousWithinAt f⁻¹ s a ↔ UpperSemicontinuousWithinAt f s a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae : ∀ {α : Type u_1} {β : Type u_5} {f : α → β} [inst : NormedAddCommGroup β] [inst_1 : NormedSpace ℝ β]
  {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hf : MeasureTheory.StronglyMeasurable f) {c : ℝ},
  (∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c) →
    ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => (hf.approxBounded c n) x) Filter.atTop (nhds (f x))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.map_id_fun : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], Std.ExtDHashMap.map (fun x v => v) m = m
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
CategoryTheory.Functor.totalRightDerived.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (F F_1 : CategoryTheory.Functor C H) (e_F : F = F_1) (L L_1 : CategoryTheory.Functor C D) (e_L : L = L_1)
  (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) [inst_3 : L.IsLocalization W]
  [inst_4 : F.HasRightDerivedFunctor W], F.totalRightDerived L W = F_1.totalRightDerived L_1 W_1
-- Mathlib.NumberTheory.Divisors
Nat.sortedGT_map_snd_divisorsAntidiagonalList : ∀ {n : ℕ}, (List.map Prod.snd n.divisorsAntidiagonalList).SortedGT
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_single_source : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K),
  (NumberField.mixedEmbedding.fundamentalCone.expMap_single w).source = Set.univ
-- Mathlib.Order.Monotone.MonovaryOrder
antivary_iff_exists_monotone_antitone : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Antivary f g ↔ ∃ x, Monotone f ∧ Antitone g
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.iSupIndep_toSubmodule : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {ι : Type u_1} {N : ι → LieSubmodule R L M},
  (iSupIndep fun i => ↑(N i)) ↔ iSupIndep N
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The composition of the three right maps in the oplax associativity hexagon.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPre F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPostPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPrePre' F)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.smul_mk : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  {𝕜 : Type u_5} [inst_2 : SMul 𝕜 γ] [inst_3 : ContinuousConstSMul 𝕜 γ] (c : 𝕜) (f : α → γ)
  (hf : MeasureTheory.AEStronglyMeasurable f μ), c • MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (c • f) ⋯
-- Init.Data.UInt.Bitwise
UInt64.shiftRight_zero : ∀ {a : UInt64}, a >>> 0 = a
-- Mathlib.GroupTheory.OrderOfElement
/-- 0 is of finite order in any additive monoid.  -/
IsOfFinAddOrder.zero : ∀ {G : Type u_1} [inst : AddMonoid G], IsOfFinAddOrder 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (a b : ℤ) →
                  a ≤ b →
                    (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t a ⟶
                      CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t b)
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- A Gaussian measure over `ℝ` is some `gaussianReal`.  -/
ProbabilityTheory.IsGaussian.eq_gaussianReal : ∀ (μ : MeasureTheory.Measure ℝ),
  ProbabilityTheory.IsGaussian μ →
    μ = ProbabilityTheory.gaussianReal (∫ (x : ℝ), id x ∂μ) (ProbabilityTheory.variance id μ).toNNReal
-- Mathlib.Topology.GDelta.Basic
/-- **Alias** of the forward direction of `isGδ_iff_eq_iInter_nat`. -/
IsGδ.eq_iInter_nat : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsGδ s → ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n
-- Mathlib.Tactic.GRewrite.Elab
/-- `nth_grw n₁ ... nₖ [e₁, ..., eₙ]` is a variant of `grw` that for each expression `eᵢ : R aᵢ bᵢ` only
replaces the `n₁, ..., nₖ`th occurrence of `aᵢ` with `bᵢ`. Use `nth_grw n₁ ... nₖ [← eᵢ]` to rewrite
in the other direction, replacing occurrences of `bᵢ` with `aᵢ`.

If an expression `e` is a defined constant, then the equational theorems associated with `e` are
used. This provides a convenient way to unfold `e`. If `e` has parameters, the tactic will try to
fill these in by unification with the matching part of the target. Parameters are only filled in
once per rule, restricting which later rewrites can be found. Parameters that are not filled in
after unification will create side goals.

To be able to use `nth_grw`, the relevant lemmas need to be tagged with `@[gcongr]`.
To rewrite inside a transitive relation, you can also give it an `IsTrans` instance.
Rewriting with a strict inequality `a < b` may change the strictness of the goal,
replacing a goal `_ < _` by `_ ≤ _`. If this is not possible, then `a < b` is treated as `a ≤ b`.

* `nth_grw n₁ ... nₖ [← e]` applies the rewrite rule `e : R a b` in the reverse direction, replacing
  the `n₁, ..., nₖ`th occurrences of `b` with `a`.
* `nth_grw (config := cfg) n₁ ... nₖ [e₁, ..., eₙ]` uses `cfg` as configuration. See
  `GRewrite.Config` for details.
  * To let `nth_grw` unfold more aggressively, as in `erw`, use
    `nth_grw (transparency := default) n₁ ... nₖ [e₁, ..., eₙ]`.
  * `nth_grw +implicationHyp n₁ ... nₖ [e₁, ..., eₙ]` interprets `· → ·` as a relation.
* `nth_grw n₁ ... nₖ [e₁, ..., eₙ] at l` rewrites at the location(s) `l`.
 -/
Mathlib.Tactic.GRewrite.tacticNth_grw_____ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.HalfBraiding.naturality_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (self : CategoryTheory.HalfBraiding X) {U U' : C} (f : U ⟶ U') {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj U' X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)
      (CategoryTheory.CategoryStruct.comp (self.β U').hom h) =
    CategoryTheory.CategoryStruct.comp (self.β U).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X) h)