mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_filterMapM_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : γ → o (Option δ)}
  {it : Std.IterM m β},
  (Std.IterM.filterMapM g (Std.IterM.filterMapWithPostcondition f it)).toListRev =
    (Std.IterM.filterMapM
        (fun b => do
          let __do_lift ← liftM (f b).run
          match __do_lift with
            | none => pure none
            | some fb => g fb)
        it).toListRev
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.bipartiteBelow.congr_simp : ∀ {α : Type u_2} {β : Type u_3} (r r_1 : α → β → Prop),
  r = r_1 →
    ∀ (s s_1 : Finset α),
      s = s_1 →
        ∀ (b b_1 : β),
          b = b_1 →
            ∀ {inst : (a : α) → Decidable (r a b)} [inst_1 : (a : α) → Decidable (r_1 a b_1)],
              Finset.bipartiteBelow r s b = Finset.bipartiteBelow r_1 s_1 b_1
-- Init.Data.Range.Polymorphic.IntLemmas
/-- Induction principle for proving properties of `Int`-based ranges of the form `a...=b` by
varying the upper bound.

In the `base` case, one proves that for any `a : Int` and `b : Int` with
`b ≤ a`, the statement holds for the subsingleton range `a...=b`.

In the `step` case, one proves that for any `a : Int` and `b : Int`, if the
statement holds for `a...=b`, it also holds for the larger range `a...=(b + 1)`.

The following is an example reproving `length_toList_rcc`.

```
example (a b : Int) : (a...=b).toList.length = (b + 1 - a).toNat := by
  induction a, b using Int.induct_rcc_right
  case base a b hge =>
    by_cases h : b < a
    · simp only [Int.toList_rcc_eq_nil, List.length_nil, *]
      omega
    · have : b = a := by omega
      simp only [Int.toList_rcc_eq_singleton, List.length_singleton,
        Int.sub_eq_iff_eq_add'.mpr rfl, Int.toNat_one, *]
  case step a b hle ih =>
    rw [Int.toList_rcc_succ_right_eq_append (by omega), List.length_append,
      List.length_singleton, ih] <;> omega
``` -/
Int.induct_rcc_right : ∀ (motive : ℤ → ℤ → Prop),
  (∀ (a b : ℤ), b ≤ a → motive a b) → (∀ (a b : ℤ), a ≤ b → motive a b → motive a (b + 1)) → ∀ (a b : ℤ), motive a b
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.Context.mk.sizeOf_spec : ∀ (elimInfo : Lean.Meta.ElimInfo) (targets : Array Lean.Expr),
  sizeOf { elimInfo := elimInfo, targets := targets } = 1 + sizeOf elimInfo + sizeOf targets
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- If `v ≠ w` are two maximal ideals of `R`, then `val_v(w) = 0`.  -/
FractionalIdeal.count_maximal_coprime : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {w : IsDedekindDomain.HeightOneSpectrum R}, w ≠ v → FractionalIdeal.count K v ↑w.asIdeal = 0
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.mk : {X : Type u_5} →
  {Y : Type u_6} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (toEquiv : X ≃ Y) →
          autoParam (Continuous toEquiv.toFun) Homeomorph.continuous_toFun._autoParam →
            autoParam (Continuous toEquiv.invFun) Homeomorph.continuous_invFun._autoParam → X ≃ₜ Y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.le_one_of_one_le_inv : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {a : Aˣ}, 1 ≤ ↑a⁻¹ → ↑a ≤ 1
-- Batteries.Data.Bool
/-- Boolean '<' is well founded  -/
Bool.lt_wfRel : WellFoundedRelation Bool
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_of_prime : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
  IsPrimitiveRoot ζ k → ∀ {p : ℕ}, Nat.Prime p → ¬p ∣ k → IsPrimitiveRoot (ζ ^ p) k
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.coeff_pow_of_natDegree_le : ∀ {R : Type u} {m n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.natDegree ≤ n → (p ^ m).coeff (m * n) = p.coeff n ^ m
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuous_obj_obj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K]
  (X : CategoryTheory.Sheaf K A) (X_1 : Cᵒᵖ),
  ((F.sheafPushforwardContinuous A J K).obj X).obj.obj X_1 = X.obj.obj (Opposite.op (F.obj (Opposite.unop X_1)))
-- Init.Data.Option.Lemmas
Option.choice_eq_default : ∀ {α : Type u_1} [Subsingleton α] [inst : Inhabited α], Option.choice α = some default
-- Mathlib.Order.Heyting.Basic
BiheytingAlgebra.toHNot : {α : Type u_4} → [self : BiheytingAlgebra α] → HNot α
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.compContinuousLinearMap : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {u : E →L[𝕜] F} {f : F → G} {s : Set F},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (f ∘ ⇑u) (⇑u ⁻¹' s)
-- Lean.Meta.Tactic.Simp.Types
/-- For `pre` procedures, the resulting expression is passed to `pre` again.

For `post` procedures, the resulting expression is passed to `pre` again IF
`Simp.Config.singlePass := false` and resulting expression is not equal to initial expression.
 -/
Lean.Meta.Simp.Step.visit : Lean.Meta.Simp.Result → Lean.Meta.Simp.Step
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.isEmpty_toList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] [Std.Iterators.Finite α Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β}, it.toList.isEmpty = it.isEmpty
-- Init.Data.Nat.Basic
Nat.le_of_mul_le_mul_left : ∀ {a b c : ℕ}, c * a ≤ c * b → 0 < c → a ≤ b
-- Mathlib.Order.Filter.Prod
Filter.prod_comap_comap_eq : ∀ {α₁ : Type u} {α₂ : Type v} {β₁ : Type w} {β₂ : Type x} {f₁ : Filter α₁} {f₂ : Filter α₂} {m₁ : β₁ → α₁}
  {m₂ : β₂ → α₂}, Filter.comap m₁ f₁ ×ˢ Filter.comap m₂ f₂ = Filter.comap (fun p => (m₁ p.1, m₂ p.2)) (f₁ ×ˢ f₂)
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.dotProduct_mulVec_degMatrix : ∀ {V : Type u_1} {R : Type u_2} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : CommSemiring R] (x : V → R),
  x ⬝ᵥ (SimpleGraph.degMatrix R G).mulVec x = ∑ i, ↑(G.degree i) * x i * x i
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {w len : ℕ} → aig.RefVec (len * w) → 0 < len → Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTreeTarget aig w
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.ipv6.inj : ∀ {ipv6 ipv6_1 : Std.Net.IPv6Addr}, Std.Http.URI.Host.ipv6 ipv6 = Std.Http.URI.Host.ipv6 ipv6_1 → ipv6 = ipv6_1
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.Pair.mk.sizeOf_spec : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} [inst_2 : SizeOf ι]
  [inst_3 : (a : ι) → SizeOf (G a)] [inst_4 : SizeOf H] (toPair : Monoid.CoprodI.Word.Pair G i)
  (normalized : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ toPair.tail.toList → g ∈ d.set i_1),
  sizeOf { toPair := toPair, normalized := normalized } = 1 + sizeOf toPair
-- Mathlib.Algebra.Homology.Localization
ComplexShape.QFactorsThroughHomotopy_of_exists_prev : ∀ {ι : Type u_1} (c : ComplexShape ι),
  (∀ (j : ι), ∃ i, c.Rel i j) →
    ∀ (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C]
      [CategoryTheory.Limits.HasBinaryBiproducts C] [inst_3 : CategoryTheory.CategoryWithHomology C],
      c.QFactorsThroughHomotopy C
-- Mathlib.Order.Interval.Finset.Basic
Finset.nonempty_Ico : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], (Finset.Ico a b).Nonempty ↔ a < b
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.rightQuotientEquiv.eq_1 : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {T : Set G} (hT : Subgroup.IsComplement (↑H) T),
  hT.rightQuotientEquiv = (Equiv.ofBijective (T.domRestrict Quotient.mk'') ⋯).symm
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.instBEqPoly.beq.match_1.eq_3 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (x x_1 : Int.Internal.Linear.Poly)
  (h_1 : (a b : ℤ) → motive (Int.Internal.Linear.Poly.num a) (Int.Internal.Linear.Poly.num b))
  (h_2 :
    (a : ℤ) →
      (a_1 : Int.Internal.Linear.Var) →
        (a_2 : Int.Internal.Linear.Poly) →
          (b : ℤ) →
            (b_1 : Int.Internal.Linear.Var) →
              (b_2 : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a a_1 a_2) (Int.Internal.Linear.Poly.add b b_1 b_2))
  (h_3 : (x x_2 : Int.Internal.Linear.Poly) → motive x x_2),
  (∀ (a b : ℤ), x = Int.Internal.Linear.Poly.num a → x_1 = Int.Internal.Linear.Poly.num b → False) →
    (∀ (a : ℤ) (a_1 : Int.Internal.Linear.Var) (a_2 : Int.Internal.Linear.Poly) (b : ℤ) (b_1 : Int.Internal.Linear.Var)
        (b_2 : Int.Internal.Linear.Poly),
        x = Int.Internal.Linear.Poly.add a a_1 a_2 → x_1 = Int.Internal.Linear.Poly.add b b_1 b_2 → False) →
      (match x, x_1 with
        | Int.Internal.Linear.Poly.num a, Int.Internal.Linear.Poly.num b => h_1 a b
        | Int.Internal.Linear.Poly.add a a_1 a_2, Int.Internal.Linear.Poly.add b b_1 b_2 => h_2 a a_1 a_2 b b_1 b_2
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Lean.Elab.Command
/-- If set (when `showPartialSyntaxErrors` is not set and parsing failed), suppresses most elaboration
errors; see also `logMessage` below.
 -/
Lean.Elab.Command.Context.suppressElabErrors : Lean.Elab.Command.Context → Bool
-- Mathlib.Data.Finset.Lattice.Prod
Finset.inf_product_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β)
  (t : Finset γ) (f : β × γ → α), (s ×ˢ t).inf f = s.inf fun i => t.inf fun i' => f (i, i')
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.lt_orderTop_single : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {r : R} {g g' : Γ},
  g < g' → ↑g < ((HahnSeries.single g') r).orderTop
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.num : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          {𝒜 : ι → σ} → {x : Submonoid A} → (self : HomogeneousLocalization.NumDenSameDeg 𝒜 x) → ↥(𝒜 self.deg)
-- Mathlib.Algebra.Group.Basic
/-- If a binary function from a type equipped with a total relation `r` to a monoid is
anti-symmetric (i.e. satisfies `f a b * f b a = 1`), in order to show it is multiplicative
(i.e. satisfies `f a c = f a b * f b c`), we may assume `r a b` and `r b c` are satisfied.
We allow restricting to a subset specified by a predicate `p`.  -/
multiplicative_of_total : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid β] (r : α → α → Prop) [Std.Total r] (f : α → α → β) (p : α → Prop),
  (∀ {a b : α}, p a → p b → f a b * f b a = 1) →
    (∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c) →
      ∀ {a b c : α}, p a → p b → p c → f a c = f a b * f b c
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.hasSmallLocalizedHom_iff_target : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) (X : C) {Y Y' : C}
  (f : Y ⟶ Y'),
  W f →
    (CategoryTheory.Localization.HasSmallLocalizedHom W X Y ↔ CategoryTheory.Localization.HasSmallLocalizedHom W X Y')
-- Mathlib.Order.InitialSeg
PrincipalSeg.lt_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} {b : β} [inst_1 : PartialOrder α] (f : α <i β),
  b < f.toRelEmbedding a ↔ ∃ a' < a, f.toRelEmbedding a' = b
-- Lean.Parser.Syntax
Lean.Parser.Command.mixfixKind.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Set.Prod
Set.prod_eq_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β},
  s ×ˢ t = s₁ ×ˢ t₁ ↔ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅)
-- Mathlib.Algebra.Group.Action.Defs
smul_iterate : ∀ {M : Type u_1} {α : Type u_5} [inst : Monoid M] [inst_1 : MulAction M α] (a : M) (n : ℕ),
  (fun x => a • x)^[n] = fun x => a ^ n • x
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instLawfulBEqOfLawfulEqCmp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  LawfulBEq (Std.ExtTreeSet α cmp)
-- Mathlib.Data.NNRat.Defs
NNRat.den_natCast : ∀ (n : ℕ), (↑n).den = 1
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
SimpleGraph.EdgeLabeling.labelGraph.eq_1 : ∀ {V : Type u_1} {G : SimpleGraph V} {K : Type u_3} (C : G.EdgeLabeling K) (k : K),
  C.labelGraph k = SimpleGraph.fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), C ⟨e, h⟩ = k}
-- Mathlib.Data.NNReal.Defs
Real.toNNReal_add_toNNReal : ∀ {r p : ℝ}, 0 ≤ r → 0 ≤ p → r.toNNReal + p.toNNReal = (r + p).toNNReal
-- Mathlib.Algebra.Ring.BooleanRing
BooleanRing.le_sup_inf : ∀ {α : Type u_1} [inst : BooleanRing α] (a b c : α), (a ⊔ b) ⊓ (a ⊔ c) ⊔ (a ⊔ b ⊓ c) = a ⊔ b ⊓ c
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.monomial_eq' : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (e : σ →₀ ℕ) (r : R),
  (MvPowerSeries.monomial e) r = MvPowerSeries.C r * e.prod fun s e => MvPowerSeries.X s ^ e
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.Scheme.Hom.asOver.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X.Hom Y) (e_f : f = f_1) (S : AlgebraicGeometry.Scheme) [inst : X.Over S]
  [inst_1 : Y.Over S] [inst_2 : f.IsOver S], f.asOver S = f_1.asOver S
-- Init.Data.Array.Extract
Array.extract_eq_self_of_le : ∀ {α : Type u_1} {j : ℕ} {as : Array α}, as.size ≤ j → as.extract 0 j = as
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.mulAntidiagonal.fst_le : ∀ {A : Type u_1} [inst : CommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedMul A]
  [inst_3 : Finset.HasMulAntidiagonal A] {n : A} {kl : A × A},
  kl ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n → kl.1 ≤ n
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat.sizeOf_spec : ∀ (a b : Lean.Expr) (natStructId : ℕ) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.coreOfNat a b natStructId lhs rhs) =
    1 + sizeOf a + sizeOf b + sizeOf natStructId + sizeOf lhs + sizeOf rhs
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F : J ⥤ Cᵒᵖ` into a limit for `F.leftOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.isLimitConeLeftOpOfCocone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit c →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneLeftOpOfCocone c)
-- Init.MetaTypes
/-- All occurrences should be rewritten.  -/
Lean.Meta.Occurrences.all : Lean.Meta.Occurrences
-- Mathlib.Analysis.Calculus.Deriv.Add
/-- Eta-expanded form of `deriv.neg` -/
deriv.fun_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, deriv (fun i => -f i) x = -deriv f x
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- The only Dyck word that is an additive unit is the empty word.  -/
DyckWord.instUniqueAddUnits : Unique (AddUnits DyckWord)
-- Mathlib.Data.Finset.Piecewise
Finset.piecewise.congr_simp : ∀ {ι : Type u_1} {π : ι → Sort u_2} (s s_1 : Finset ι),
  s = s_1 →
    ∀ (f f_1 : (i : ι) → π i),
      f = f_1 →
        ∀ (g g_1 : (i : ι) → π i),
          g = g_1 →
            ∀ {inst : (j : ι) → Decidable (j ∈ s)} [inst_1 : (j : ι) → Decidable (j ∈ s_1)] (i : ι),
              s.piecewise f g i = s_1.piecewise f_1 g_1 i
-- Mathlib.Probability.BrownianMotion.Basic
ProbabilityTheory.IsBrownianReal.tendsto_nhds_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ},
  ProbabilityTheory.IsBrownianReal B P → ∀ᵐ (ω : Ω) ∂P, Filter.Tendsto (fun x => B x ω) (nhds 0) (nhds 0)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.normalize_eq_self_iff_monic : ∀ {R : Type u} [inst : Field R] [inst_1 : DecidableEq R] {p : Polynomial R}, p ≠ 0 → (normalize p = p ↔ p.Monic)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainRingEquiv_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (e : M ≃* N)
  (r : R) (m : M), (MonoidAlgebra.mapDomainRingEquiv R e) (MonoidAlgebra.single m r) = MonoidAlgebra.single (e m) r
-- Mathlib.Topology.Inseparable
Specializes.map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} {f : X → Y},
  x ⤳ y → Continuous f → f x ⤳ f y
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM_sum : ∀ {ι : Type u_1} {E : Type u_3} (F : Type u_4) [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] {g : ι → E → ℂ} {s : Finset ι},
  (∀ i ∈ s, Function.HasTemperateGrowth (g i)) →
    (TemperedDistribution.fourierMultiplierCLM F fun x => ∑ i ∈ s, g i x) =
      ∑ i ∈ s, TemperedDistribution.fourierMultiplierCLM F (g i)
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.map_smul : ∀ {Γ : Type u_1} {R : Type u_3} {U : Type u_5} {V : Type u_6} [inst : PartialOrder Γ] [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : AddCommMonoid U] [inst_5 : Module R U] (f : U →ₗ[R] V)
  {r : R} {x : HahnSeries Γ U}, (r • x).map f = r • x.map f
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.id_tensorHom_id : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X Y : CategoryTheory.GradedObject I C) [inst_3 : X.HasTensor Y],
  CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X)
      (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.GradedObject.Monoidal.tensorObj X Y)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.C_pow : ∀ {R : Type u_1} {n : ℕ} [inst : Semiring R] {a : R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  SkewPolynomial.C (a ^ n) = SkewPolynomial.C a ^ n
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_map_equiv : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} {Y : Type u_5} [inst_2 : MeasurableSpace Y] (e : X ≃ᵐ Y) (f : Y → E) (s : Set Y),
  ∫ (y : Y) in s, f y ∂MeasureTheory.Measure.map (⇑e) μ = ∫ (x : X) in ⇑e ⁻¹' s, f (e x) ∂μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_insertMany!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α} {v : β},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
          (k, v) ∈ l →
            Std.DTreeMap.Internal.Impl.Const.get! (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k' = v
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {fallback v : β}, (t.insert k v).getD k fallback = v
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.restrict_withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ (f : α → ENNReal), (μ.withDensity f).restrict s = (μ.restrict s).withDensity f
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.negPart : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : AddGroup β] [inst_2 : Lattice β] [ContinuousSup β] [ContinuousNeg β],
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x)⁻) μ
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_comm : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v = G.edist v u
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- A set `s` is *everywhere positive* (also called *self-supporting*) with respect to a
measure `μ` if it has positive measure around each of its points, i.e., if all neighborhoods `n`
of points of `s` satisfy `μ (s ∩ n) > 0`.  -/
MeasureTheory.Measure.IsEverywherePos : {α : Type u_1} → [TopologicalSpace α] → [inst : MeasurableSpace α] → MeasureTheory.Measure α → Set α → Prop
-- Mathlib.Lean.PrettyPrinter.Delaborator
/-- Assuming the current expression in a lambda or pi,
descend into the body using an unused name generated from the binder's name.
Provides `d` with both `Syntax` for the bound name as an identifier
as well as the fresh fvar for the bound variable.
See also `Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName`.  -/
Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName' : {α : Type} →
  (Lean.Syntax → Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM α) → Lean.PrettyPrinter.Delaborator.DelabM α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toArray_insert_perm : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : BEq α]
  [Std.TransOrd α] [Std.LawfulBEqOrd α] (h : t.WF) {k : α} {v : β},
  (Std.DTreeMap.Internal.Impl.Const.toArray (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl).Perm
    ((Array.filter (fun x => decide ¬(k == x.1) = true) (Std.DTreeMap.Internal.Impl.Const.toArray t)).push (k, v))
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.oreSubtra.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (r : R) (s : ↥S),
  AddOreLocalization.oreSubtra r s = AddOreLocalization.AddOreSet.oreSubtra r s
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsPartition.infPrepartition : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ : BoxIntegral.TaggedPrepartition I},
  π₁.IsPartition → ∀ {π₂ : BoxIntegral.Prepartition I}, π₂.IsPartition → (π₁.infPrepartition π₂).IsPartition
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.liftStar_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y),
  (CategoryTheory.WithInitial.liftStar F M hM).hom = CategoryTheory.CategoryStruct.id Z
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.insert_Nonneg : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  k ≥ 0 → p.NonnegCoeffs → (Lean.Grind.CommRing.Poly.insert k m p).NonnegCoeffs