mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AlgebraTower
/-- **Alias** of `AlgHom.domRestrict`.

---

Restrict the domain of an `AlgHom`.  -/
AlgHom.restrictDomain : {A : Type u_3} →
  (B : Type u_4) →
    {C : Type u_5} →
      {D : Type u_6} →
        [inst : CommSemiring A] →
          [inst_1 : CommSemiring C] →
            [inst_2 : CommSemiring D] →
              [inst_3 : Algebra A C] →
                [inst_4 : Algebra A D] →
                  [inst_5 : CommSemiring B] →
                    [inst_6 : Algebra A B] → [inst_7 : Algebra B C] → [IsScalarTower A B C] → (C →ₐ[A] D) → B →ₐ[A] D
-- Mathlib.MeasureTheory.Group.Prod
/-- A technical lemma relating two different measures. This is basically [Halmos, §60 Th. A]. Note
that if `f` is the characteristic function of a measurable set `t` this states that `μ t = c * μ s`
for a constant `c` that does not depend on `μ`.

Note: There is a gap in the last step of the proof in [Halmos]. In the last line, the equality
`g(-x) + ν(s - x) = f(x)` holds if we can prove that `0 < ν(s - x) < ∞`. The first inequality
follows from §59, Th. D, but the second inequality is not justified. We prove this inequality for
almost all `x` in `MeasureTheory.ae_measure_preimage_add_right_lt_top_of_ne_zero`.  -/
MeasureTheory.measure_lintegral_sub_measure : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant],
  MeasurableSet s →
    ν' s ≠ 0 →
      ν' s ≠ ⊤ →
        ∀ (f : G → ENNReal),
          Measurable f → μ' s * ∫⁻ (y : G), f (-y) / ν' ((fun x => x + -y) ⁻¹' s) ∂ν' = ∫⁻ (x : G), f x ∂μ'
-- Lean.Elab.PreDefinition.Structural.SmartUnfolding
Lean.Elab.Structural.addSmartUnfoldingDefAux : Lean.Elab.PreDefinition → ℕ → Lean.MetaM Lean.Elab.PreDefinition
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationsParams.mk : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx → ProofWidgets.GetExprPresentationsParams
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.alt.sizeOf_spec : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} [inst : SizeOf R] [inst_1 : SizeOf ι] [inst_2 : SizeOf M] (m : ι → M)
  (i j : ι) (hm : m i = m j) (hij : i ≠ j),
  sizeOf (exteriorPower.presentation.Rels.alt m i j hm hij) = 1 + sizeOf i + sizeOf j + sizeOf hm
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.Spec_iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q] {R S : CommRingCat} {φ : R ⟶ S},
  P (AlgebraicGeometry.Spec.map φ) ↔ Q (CommRingCat.Hom.hom φ)
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel.eq_2 : ∀ {α β : Type} (r : α → β) (a : α), Std.Sat.AIG.Decl.relabel r (Std.Sat.AIG.Decl.atom a) = Std.Sat.AIG.Decl.atom (r a)
-- Lean.Server.References
Lean.Server.References.ParentDecl.mk.inj : ∀ {name : String} {range selectionRange : Lean.Lsp.Range} {name_1 : String} {range_1 selectionRange_1 : Lean.Lsp.Range},
  { name := name, range := range, selectionRange := selectionRange } =
      { name := name_1, range := range_1, selectionRange := selectionRange_1 } →
    name = name_1 ∧ range = range_1 ∧ selectionRange = selectionRange_1
-- Mathlib.CategoryTheory.Bicategory.Strict.Basic
/-- The associators are given by equalities  -/
CategoryTheory.Bicategory.Strict.associator_eqToIso : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b c d : B}
  (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.Bicategory.associator f g h = CategoryTheory.eqToIso ⋯
-- Init.Data.UInt.Lemmas
UInt64.sub_lt : ∀ {a b : UInt64}, 0 < b → b ≤ a → a - b < a
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.quiv : Quiver FreeSimplexQuiver
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- `Functor.map` of a fully faithful monoidal functor as a `MulEquiv`.  -/
CategoryTheory.Functor.FullyFaithful.homMulEquiv : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v, u_1} C] →
      [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{w, u_2} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            {M X : C} →
              [inst_4 : CategoryTheory.MonObj M] →
                (F : CategoryTheory.Functor C D) →
                  [inst_5 : F.Monoidal] → F.FullyFaithful → (X ⟶ M) ≃* (F.obj X ⟶ F.obj M)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instT3Space : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)] [T2Space F],
  T3Space (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.comp_of_mem_nhdsWithin_image_of_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β} {y : β},
  ContinuousWithinAt g t y →
    ContinuousWithinAt f s x → t ∈ nhdsWithin y (f '' s) → f x = y → ContinuousWithinAt (g ∘ f) s x
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin : Type
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.equivMeasure_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] (v : MeasureTheory.VectorMeasure α ENNReal),
  MeasureTheory.VectorMeasure.equivMeasure v = v.ennrealToMeasure
-- Mathlib.Algebra.Category.Semigrp.Basic
MagmaCat.str : (self : MagmaCat) → Mul ↑self
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.submartingale : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E],
  MeasureTheory.Martingale f ℱ μ → MeasureTheory.Submartingale f ℱ μ
-- Mathlib.Analysis.Calculus.Deriv.Comp
derivWithin.scomp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (x : 𝕜) {s : Set 𝕜} {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] [inst_5 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {t' : Set 𝕜'} {h : 𝕜 → 𝕜'}
  {g₁ : 𝕜' → F},
  DifferentiableWithinAt 𝕜' g₁ t' (h x) →
    DifferentiableWithinAt 𝕜 h s x →
      Set.MapsTo h s t' → derivWithin (g₁ ∘ h) s x = derivWithin h s x • derivWithin g₁ t' (h x)
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_one : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, 1 = b - a
-- Mathlib.Algebra.Order.Group.CompleteLattice
add_ciSup : ∀ {ι : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [AddLeftMono G], BddAbove (Set.range f) → ∀ (a : G), a + ⨆ i, f i = ⨆ i, a + f i
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.eq_top_iff : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] {A : Matrix m n R} {l : m → WithTop n} [inst_1 : LT m]
  [inst_2 : LT n] {i : m}, A.IsPivotedBy l → (l i = ⊤ ↔ A i = 0)
-- Mathlib.Order.Fin.Basic
Fin.addNat_le_addNat_iff : ∀ {n : ℕ} (m : ℕ) {i j : Fin n}, i.addNat m ≤ j.addNat m ↔ i ≤ j
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.mono : ∀ {𝕜 : 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 : M → M'} {s t : Set M} {x : M}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → t ⊆ s → ContMDiffWithinAt I I' n f t x
-- Mathlib.NumberTheory.NumberField.ExistsRamified
/-- If `K` is a number field with positive rank, then there exists some maximal ideal of `𝓞 K`
that is ramified over `ℤ`.  -/
NumberField.exists_not_isUnramifiedAt_int : ∀ {K : Type u_1} {𝒪 : Type u_2} [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K], Module.finrank ℚ K ≠ 1 → ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.intCast_negOfNat_Int : ∀ {R : Type u_2} [inst : CommRing R] (n : ℕ), ↑(Int.negOfNat n).rawCast = (Int.negOfNat n).rawCast
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
riemannZeta_eq_inv_sub_add : ∀ {s : ℂ}, s ≠ 1 → riemannZeta s = (s - 1)⁻¹ + riemannZeta₀ s
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.TriangleIndexData.hp₁₂ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₃ : Type u_3} {J : Type u_4} [inst : Zero I₂] {r : I₁ × I₂ × I₃ → J}
  {π : I₁ × I₃ → J} (self : CategoryTheory.GradedObject.TriangleIndexData r π) (i : I₁ × I₂ × I₃),
  π (self.p₁₂ (i.1, i.2.1), i.2.2) = r i
-- Mathlib.RingTheory.Valuation.ValuationRing
/-- Any valuation ring induces a valuation on its fraction field.  -/
ValuationRing.valuation : (A : Type u) →
  [inst : CommRing A] →
    (K : Type v) →
      [inst_1 : Field K] →
        [inst_2 : Algebra A K] →
          [inst_3 : IsDomain A] →
            [inst_4 : ValuationRing A] → [inst_5 : IsFractionRing A K] → Valuation K (ValuationRing.ValueGroup A K)
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- `overrideAllowedImportDirs` relates module prefixes, specifying that modules with the first
prefix are allowed to import modules with the second prefix, even if disallowed in
`forbiddenImportDirs`.

For example, ``(`Mathlib.Algebra.Notation, `Mathlib.Algebra)`` is in `forbiddenImportDirs` and
``(`Mathlib.Algebra.Notation, `Mathlib.Algebra.Notation)`` is in `overrideAllowedImportDirs`
because modules in `Mathlib/Algebra/Notation.lean` cannot import modules in `Mathlib.Algebra` that are
outside `Mathlib/Algebra/Notation.lean`.
 -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.DirectoryDependency.overrideAllowedImportDirs : Mathlib.Linter.DirectoryDependency.NamePrefixRel✝
-- Mathlib.Data.Seq.Computation
Computation.map.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream' (Option α))
  (al : ∀ ⦃n : ℕ⦄ ⦃a : α⦄, s n = some a → s (n + 1) = some a),
  Computation.map f ⟨s, al⟩ = ⟨Stream'.map (fun o => Option.casesOn o none (some ∘ f)) s, ⋯⟩
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Entry.ref : {α : Type u} → {β : Type v} → {σ : Type w} → σ → Lean.PersistentHashMap.Entry α β σ
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.associator_hom : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X Y Z : C),
  (CategoryTheory.MonoidalCategoryStruct.associator
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Y)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X Y)
        ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).map
            (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) X
              (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
              ((CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε).obj X)
              (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) Y
                Z)))))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nonempty_image_mulRight_inv_inter_iff : ∀ {α : Type u_2} [inst : DivisionMonoid α] {s t : Set α} {a : α},
  ((fun x => x * a⁻¹) '' s ∩ t).Nonempty ↔ ((fun x => a * x) '' s⁻¹ ∩ t⁻¹).Nonempty
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_ennreal_smul_measure : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {c : ENNReal},
  c ≠ 0 → ∀ (f : α → ε), MeasureTheory.eLpNormEssSup f (c • μ) = MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel.congr_simp : ∀ {Ω : Type u_3} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω] (μ μ_1 : MeasureTheory.Measure Ω)
  (e_μ : μ = μ_1) [inst_1 : MeasureTheory.IsFiniteMeasure μ] (m : MeasurableSpace Ω),
  ProbabilityTheory.condExpKernel μ m = ProbabilityTheory.condExpKernel μ_1 m
-- Mathlib.Algebra.Group.Subgroup.Even
AddSubmonoid.even_toSubsemigroup : ∀ {M : Type u_1} [inst : AddCommMonoid M], (AddSubmonoid.even M).toAddSubsemigroup = AddSubsemigroup.even M
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.leftCancelMonoid : {α : Type u} → [AddLeftCancelMonoid α] → LeftCancelMonoid (Multiplicative α)
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Product of a list of elements in a submonoid is in the submonoid.  -/
Submonoid.list_prod_mem : ∀ {M : Type u_1} [inst : Monoid M] (s : Submonoid M) {l : List M}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- The `LSeries` of `f` is zero for large real arguments if and only if either `f n = 0`
for all `n ≠ 0` or the L-series converges nowhere.  -/
LSeries_eventually_eq_zero_iff' : ∀ {f : ℕ → ℂ},
  (fun x => LSeries f ↑x) =ᶠ[Filter.atTop] 0 ↔ (∀ (n : ℕ), n ≠ 0 → f n = 0) ∨ LSeries.abscissaOfAbsConv f = ⊤
-- Init.Data.Dyadic.Basic
Dyadic.pow.eq_2 : ∀ (i : ℕ) (n k : ℤ) (hn : n % 2 = 1), (Dyadic.ofOdd n k hn).pow i = Dyadic.ofOdd (n ^ i) (k * ↑i) ⋯
-- Mathlib.Topology.Baire.BaireMeasurable
/-- Notation for `=ᶠ[residual _]`. That is, eventual equality with respect to
the filter of residual sets.
In lemma names, this is called `residualEq`.  -/
Topology.«term_=ᵇ_» : Lean.TrailingParserDescr
-- Init.Data.String.Lemmas.Pattern.Basic
_private.Init.Data.String.Lemmas.Pattern.Basic.0.Std.Iter.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
Finset.Nat.antidiagonalTuple_zero_zero : Finset.Nat.antidiagonalTuple 0 0 = {![]}
-- Std.Time.Format.Modifier
Std.Time.Fraction.nano.sizeOf_spec : sizeOf Std.Time.Fraction.nano = 1
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
CategoryTheory.Limits.weakEqualizer.fork_π_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g],
  (CategoryTheory.Limits.weakEqualizer.fork f g).π.app CategoryTheory.Limits.WalkingParallelPair.zero =
    CategoryTheory.Limits.weakEqualizer.ι f g
-- Mathlib.Algebra.Group.Action.Pi
Function.extend_smul : ∀ {ι : Type u_1} {M : Type u_7} {α : Type u_8} {β : Type u_9} [inst : SMul M β] (r : M) (f : ι → α) (g : ι → β)
  (e : α → β), Function.extend f (r • g) (r • e) = r • Function.extend f g e
-- Mathlib.Tactic.Hint
/-- The `hint` tactic tries every tactic registered using `register_hint <prio> tac`,
and reports any that succeed.
 -/
Mathlib.Tactic.Hint.hintStx : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monad.Limits
/-- The forgetful functor from the Eilenberg-Moore category creates colimits.  -/
CategoryTheory.Comonad.forgetCreatesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} → CategoryTheory.CreatesColimitsOfSize.{u_1, u_2, v₁, v₁, max u₁ v₁, u₁} T.forget
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.mem_toAddSubmonoid : ∀ {M : Type u_1} [inst : AddZeroClass M] {s : SaturatedAddSubmonoid M} {x : M}, x ∈ s.toAddSubmonoid ↔ x ∈ s
-- Lean.Parser.Extra
Lean.Parser.withoutPosition.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Init.Prelude
Applicative.toFunctor : {f : Type u → Type v} → [self : Applicative f] → Functor f
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.piMap : ∀ {ι : Type u_5} [inst : Fintype ι] {α : ι → Type u_3} {β : ι → Type u_4} [inst_1 : (i : ι) → PseudoEMetricSpace (α i)]
  [inst_2 : (i : ι) → PseudoEMetricSpace (β i)] (f : (i : ι) → α i → β i),
  (∀ (i : ι), Isometry (f i)) → Isometry (Pi.map f)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
_private.Mathlib.Analysis.InnerProductSpace.Adjoint.0.ContinuousLinearMap.adjointAux_norm : ∀ {𝕜 : 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] [CompleteSpace F] (A : E →L[𝕜] F), ‖ContinuousLinearMap.adjointAux✝ A‖ = ‖A‖
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `getD` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.Const.getDₘ : {α : Type u} → {β : Type v} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => β) → α → β → β
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.join_eq_bind : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure (MeasureTheory.Measure α)), μ.join = μ.bind id
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- Each ball in an extended metric space gives us a metric space, as the edist
is everywhere finite.  -/
metricSpaceEMetricBall : {β : Type u_2} → [inst : EMetricSpace β] → (a : β) → (r : ENNReal) → MetricSpace ↑(Metric.eball a r)
-- Aesop.Util.OrderedHashSet
Aesop.instInhabitedOrderedHashSet : {a : Type u_1} → {a_1 : BEq a} → {a_2 : Hashable a} → Inhabited (Aesop.OrderedHashSet a)
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_ofNat : ∀ (n : ℕ), { toBitVec := BitVec.ofNat 8 n } = OfNat.ofNat n
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.mapTriangulatedFunctor_δ' : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {D : Type u_3} [inst_7 : CategoryTheory.Category.{v_3, u_3} D] [inst_8 : CategoryTheory.Limits.HasZeroObject D]
  [inst_9 : CategoryTheory.HasShift D ℤ] [inst_10 : CategoryTheory.Preadditive D]
  [inst_11 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_12 : CategoryTheory.Pretriangulated D]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) (F : CategoryTheory.Functor C D) [inst_13 : F.CommShift ℤ]
  [inst_14 : F.IsTriangulated],
  (X.mapTriangulatedFunctor F).δ' =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight X.δ' F)
      (((CategoryTheory.ComposableArrows.functorArrows ι 0 1 2 CategoryTheory.Triangulated.SpectralObject._proof_6
                CategoryTheory.Triangulated.SpectralObject._proof_2).comp
            X.ω₁).whiskerLeft
        (CategoryTheory.Functor.commShiftIso F 1).hom)
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
/-- The Cesaro average of a converging sequence converges to the same limit.  -/
Filter.Tendsto.cesaro : ∀ {u : ℕ → ℝ} {l : ℝ},
  Filter.Tendsto u Filter.atTop (nhds l) →
    Filter.Tendsto (fun n => (↑n)⁻¹ * ∑ i ∈ Finset.range n, u i) Filter.atTop (nhds l)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- A measurable set `t ⊇ s` such that `μ t = μ s`. It even satisfies `μ (t ∩ u) = μ (s ∩ u)` for
any measurable set `u` if `μ s ≠ ∞`, see `measure_toMeasurable_inter`.
This property holds without the assumption `μ s ≠ ∞` when the space is s-finite (for example
σ-finite); see `measure_toMeasurable_inter_of_sFinite`.
If `s` is a null measurable set, then
we also have `t =ᵐ[μ] s`, see `NullMeasurableSet.toMeasurable_ae_eq`.
This notion is sometimes called a "measurable hull" in the literature.  -/
MeasureTheory.toMeasurable : {α : Type u_6} → [inst : MeasurableSpace α] → MeasureTheory.Measure α → Set α → Set α
-- Mathlib.Algebra.Lie.Classical
/-- The definite orthogonal Lie subalgebra: skew-adjoint matrices with respect to the symmetric
bilinear form defined by the identity matrix.  -/
LieAlgebra.Orthogonal.so : (n : Type u_1) →
  (R : Type u₂) → [inst : CommRing R] → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → LieSubalgebra R (Matrix n n R)
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.mul.congr_simp : ∀ {ι : Type u_1} {R : Type u_3} {A : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (A i)] [inst_2 : (i : ι) → Module R (A i)]
  [inst_3 : ∀ (i : ι), SMulCommClass R (A i) (A i)] [inst_4 : ∀ (i : ι), IsScalarTower R (A i) (A i)],
  PiTensorProduct.mul = PiTensorProduct.mul
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_diff_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Mathlib.MeasureTheory.Measure.DiracProba
MeasureTheory.not_tendsto_diracProba_of_not_tendsto : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : OpensMeasurableSpace X]
  [CompletelyRegularSpace X] {x : X} (L : Filter X),
  ¬Filter.Tendsto id L (nhds x) → ¬Filter.Tendsto MeasureTheory.diracProba L (nhds (MeasureTheory.diracProba x))
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_rcc_succ_right_eq_cons_map : ∀ {m n : ℕ}, m ≤ n + 1 → (m...=n + 1).toList = m :: List.map (fun x => x + 1) (m...=n).toList
-- Std.Http.Data.URI.Encoding
/-- Creates an encoded path segment from raw bytes, panicking on invalid encoding.
 -/
Std.Http.URI.EncodedSegment.ofByteArray! : ByteArray → Std.Http.URI.EncodedSegment
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsMarkovKernel.map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : β → γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsMarkovKernel κ],
  Measurable f → ProbabilityTheory.IsMarkovKernel (κ.map f)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderIdent : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C),
  (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).obj F =
    F.mapMon.obj (CategoryTheory.Mon.trivial (CategoryTheory.Discrete PUnit.{w + 1}))