mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
QuotientAddGroup.measurable_from_quotient : ∀ {α : Type u_1} [inst : MeasurableSpace α] {G : Type u_6} [inst_1 : AddGroup G] [inst_2 : MeasurableSpace G]
  {S : AddSubgroup G} {f : G ⧸ S → α}, Measurable f ↔ Measurable (f ∘ QuotientAddGroup.mk)
-- Lean.Attributes
/-- Sets the attribute (without running `validate`)  -/
Lean.TagAttribute.setTag : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [Lean.MonadEnv m] → Lean.TagAttribute → Lean.Name → m Unit
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.pentagon : ∀ {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}
  (Y₁ Y₂ Y₃ Y₄ : CategoryTheory.LocalizedMonoidal L W ε), CategoryTheory.MonoidalCategory.Pentagon Y₁ Y₂ Y₃ Y₄
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.of_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C₁ C₂ s t : NNReal}, HolderWith C₁ r f → HolderWith C₂ s f → r ≤ t → t ≤ s → HolderWith (max C₁ C₂) t f
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.trans : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {μ : MeasureTheory.Measure ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε] {a b c : ℝ},
  IntervalIntegrable f μ a b → IntervalIntegrable f μ b c → IntervalIntegrable f μ a c
-- Mathlib.Topology.Algebra.Group.Basic
continuousNeg_of_indiscreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Neg H] [IndiscreteTopology H], ContinuousNeg H
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The indexing type of a representation of `comul a`  -/
Coalgebra.Repr.ι : {R : Type u} →
  {A : Type v} →
    {ι : Type u_1} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] → [inst_3 : Coalgebra R A] → {a : A} → Coalgebra.Repr R a ι → Type u_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.isEmpty_takeWhile_dropWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String}, ((s.dropWhile pat).takeWhile pat).isEmpty = true
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.FinalizeInductiveDecl.indFvars : Lean.Elab.Command.FinalizeInductiveDecl✝ → Array Lean.Expr
-- Mathlib.Data.Finset.Filter
Finset.filter_const : ∀ {α : Type u_1} (p : Prop) [inst : Decidable p] (s : Finset α), {_a ∈ s | p} = if p then s else ∅
-- Batteries.Data.List.Lemmas
List.isSome_isSuffixOf?_eq_isSuffixOf : ∀ {α : Type u_1} [inst : BEq α] (xs ys : List α), (xs.isSuffixOf? ys).isSome = xs.isSuffixOf ys
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_toDual : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ioi (OrderDual.toDual a) = ⇑OrderDual.ofDual ⁻¹' Set.Iio a
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.comp_assoc : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {R₄ : Type u_4} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7}
  {E₄ : Type u_8} [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : Semiring R₄]
  {σ₁₂ : R →+* R₂} {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  [inst_4 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_5 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
  [inst_6 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_7 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [inst_8 : SeminormedAddCommGroup E]
  [inst_9 : SeminormedAddCommGroup E₂] [inst_10 : SeminormedAddCommGroup E₃] [inst_11 : SeminormedAddCommGroup E₄]
  [inst_12 : Module R E] [inst_13 : Module R₂ E₂] [inst_14 : Module R₃ E₃] [inst_15 : Module R₄ E₄]
  (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.IsVerdierRightLocalizing.fac : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {A B : CategoryTheory.ObjectProperty C}
  [self : A.IsVerdierRightLocalizing B] {X Y : C} (f : X ⟶ Y),
  B X → A Y → ∃ Z a b, A Z ∧ B Z ∧ CategoryTheory.CategoryStruct.comp a b = f
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `FunLike.coe_smul`. -/
GroupSeminorm.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_le_norm_div_add_norm_div : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b c : E), ‖a / c‖ ≤ ‖a / b‖ + ‖b / c‖
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- Note the `AddSubmonoid` version of this lemma is called `AddSubmonoid.coe_finsetSum`.  -/
Submodule.coe_sum : ∀ {R : Type u} {M : Type v} {ι : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M}
  (p : Submodule R M) (x : ι → ↥p) (s : Finset ι), ↑(∑ i ∈ s, x i) = ∑ i ∈ s, ↑(x i)
-- Mathlib.Algebra.Field.Subfield.Defs
SubfieldClass.coe_nnqsmul : ∀ {K : Type u} [inst : DivisionRing K] {S : Type u_1} [inst_1 : SetLike S K] [h : SubfieldClass S K] (s : S) (q : ℚ≥0)
  (x : ↥s), ↑(q • x) = q • ↑x
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_truncFinset_pow : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)},
  IsLowerSet ↑s →
    ∀ {k : ℕ},
      1 ≤ k →
        ∀ (p : MvPowerSeries σ R),
          (MvPowerSeries.truncFinset R s) (↑((MvPowerSeries.truncFinset R s) p) ^ k) =
            (MvPowerSeries.truncFinset R s) (p ^ k)
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instT2Space : ∀ {𝕜 : 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],
  T2Space (ContinuousMultilinearMap 𝕜 E F)
-- Mathlib.Topology.Compactness.Compact
IsCompact.exists_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → ∀ {f : Filter X} [f.NeBot], f ≤ Filter.principal s → ∃ x ∈ s, ClusterPt x f
-- Mathlib.Data.List.Cycle
decidable_of_iff'.congr_simp : ∀ {a : Prop} (b b_1 : Prop) (e_b : b = b_1) (h : a ↔ b) {inst : Decidable b} [inst_1 : Decidable b_1],
  decidable_of_iff' b h = decidable_of_iff' b_1 ⋯
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instIsScalarTower : ∀ (k : Type u) [inst : Field k] {R : Type u_1} {S : Type u_2} [inst_1 : CommSemiring R] [inst_2 : CommSemiring S]
  [inst_3 : Algebra R S] [inst_4 : Algebra S k] [inst_5 : Algebra R k] [IsScalarTower R S k],
  IsScalarTower R S (AlgebraicClosure k)
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedSup_of_isAntichain : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : OrderTop α],
  IsAntichain (fun x1 x2 => x1 ≤ x2) ↑s → a ∈ s → s.truncatedSup a = a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_erase_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {fallback : β}, Std.DHashMap.Raw.Const.getD (m.erase k) k fallback = fallback
-- Mathlib.MeasureTheory.Integral.Lebesgue.DominatedConvergence
MeasureTheory.limsup_lintegral_le : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : ℕ → α → ENNReal} (g : α → ENNReal),
  (∀ (n : ℕ), Measurable (f n)) →
    (∀ (n : ℕ), f n ≤ᵐ[μ] g) →
      ∫⁻ (a : α), g a ∂μ ≠ ⊤ →
        Filter.limsup (fun n => ∫⁻ (a : α), f n a ∂μ) Filter.atTop ≤
          ∫⁻ (a : α), Filter.limsup (fun n => f n a) Filter.atTop ∂μ
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K]
  [inst_6 : IsFractionRing R K], FractionalIdeal.absNorm 1 = 1
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- A prop-valued typeclass characterising the `𝔤₂` root system.  -/
RootPairing.IsG2 : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → Prop
-- Plausible.ArbitraryFueled
/-- Takes a `Nat` and produces a random generator dependent on the `Nat` parameter
(which indicates the amount of fuel to be used before failing).  -/
Plausible.ArbitraryFueled.arbitraryFueled : {α : Type} → [self : Plausible.ArbitraryFueled α] → ℕ → Plausible.Gen α
-- Mathlib.ModelTheory.LanguageMap
/-- The language map removing an empty constant set.  -/
FirstOrder.Language.LEquiv.addEmptyConstants : (L : FirstOrder.Language) → (α : Type w') → [ie : IsEmpty α] → L ≃ᴸ L.withConstants α
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.isWriterClosed : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.Equivalence.induced_functor : ∀ {D : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D),
  (CategoryTheory.Equivalence.induced e).functor = CategoryTheory.inducedFunctor ⇑e
-- Mathlib.LinearAlgebra.Reflection
/-- A formula for $(r_1 r_2)^m z$, where $m$ is an integer and $z \in M$.  -/
Module.reflection_mul_reflection_zpow_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (z : M) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_zpow_apply._auto_1 →
    ((Module.reflection hf * Module.reflection hg) ^ m) z =
      z +
          (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 2) / 2)) *
              (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 1) / 2)) +
                Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 3) / 2)))) •
            ((g x * f z - g z) • y - f z • x) +
        (Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 1) / 2)) *
            (Polynomial.eval t (Polynomial.Chebyshev.S R (m / 2)) +
              Polynomial.eval t (Polynomial.Chebyshev.S R ((m - 2) / 2)))) •
          ((f y * g z - f z) • x - g z • y)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.mono_precomp_mk₀_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (L : C) {M N : C} (g : M ⟶ N) [hg : CategoryTheory.Epi g],
  CategoryTheory.Mono (AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ g).precomp L ⋯))
-- Init.Data.Sum.Lemmas
Sum.getRight?_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, x.getRight? = none ↔ x.isLeft = true
-- Mathlib.Topology.Order.IsLUB
exists_seq_strictMono_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] [FirstCountableTopology α] (x : α),
  ∃ u, StrictMono u ∧ (∀ (n : ℕ), u n < x) ∧ Filter.Tendsto u Filter.atTop (nhds x)
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
IsScalarTower.subalgebra' : ∀ (R : Type u) (S : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [IsScalarTower R S A] (S₀ : Subalgebra R S),
  IsScalarTower R (↥S₀) A
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.Quotient.trans_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (γ : Path.Homotopic.Quotient x₀ x₁),
  γ.trans γ.symm = Path.Homotopic.Quotient.refl x₀
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.nsmul_f_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (n : ℕ) (f : C ⟶ D) (i : ι), (n • f).f i = n • f.f i
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- A zero object is in particular initial.  -/
CategoryTheory.Limits.HasZeroObject.zeroIsInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → CategoryTheory.Limits.IsInitial 0
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.mk'.injEq : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (toFun : (i : ι) → β i)
  (support' : Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun i = 0 }) (toFun_1 : (i : ι) → β i)
  (support'_1 : Trunc { s // ∀ (i : ι), i ∈ s ∨ toFun_1 i = 0 }),
  ({ toFun := toFun, support' := support' } = { toFun := toFun_1, support' := support'_1 }) =
    (toFun = toFun_1 ∧ support' ≍ support'_1)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.integral_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : NormedAddCommGroup γ] [inst_4 : NormedSpace ℝ γ] [BorelSpace γ],
  ProbabilityTheory.IdentDistrib f g μ ν → ∫ (x : α), f x ∂μ = ∫ (x : β), g x ∂ν
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Version of `hasSum_ite_sub_hasSum` for `AddCommMonoid` rather than `AddCommGroup`.
Rather than showing that the `ite` expression has a specific sum in terms of `HasSum`,
it gives a relationship between the sums of `f` and `ite (n = b) 0 (f n)` given that both exist.  -/
eq_add_of_hasSum_ite : ∀ {β : Type u_2} {L : SummationFilter β} [L.LeAtTop] [L.NeBot] {α : Type u_4} [inst : TopologicalSpace α]
  [inst_1 : AddCommMonoid α] [T2Space α] [ContinuousAdd α] [inst_4 : DecidableEq β] {f : β → α} {a : α},
  HasSum f a L → ∀ (b : β) (a' : α), HasSum (fun n => if n = b then 0 else f n) a' L → a = a' + f b
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns the first non-`none` result of applying `f` to each output of the iterator, in order.
Returns `none` if `f` returns `none` for all outputs.

`O(|it|)`. Short-circuits when `f` returns `some _`.The outputs of `it` are examined in order of
iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `IterM.findSome?`.

Examples:
 * `([7, 6, 5, 8, 1, 2, 6].iterM Id).ensureTermination.findSome? (fun x => if x < 5 then some (10 * x) else none) = pure (some 10)`
 * `([7, 6, 5, 8, 1, 2, 6].iterM Id).ensureTermination.findSome? (fun x => if x < 1 then some (10 * x) else none) = pure none`
 -/
Std.IterM.Total.findSome? : {α β γ : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] →
        [Std.IteratorLoop α m m] → [Std.Iterators.Finite α m] → Std.IterM.Partial m β → (β → Option γ) → m (Option γ)
-- Std.Async.System
/-- Information about a group.
 -/
Std.Async.System.GroupInfo : Type
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.ChosenEndsOfShape.mk : {J : Type u_3} →
  [inst : CategoryTheory.Category.{v_3, u_3} J] →
    {C : Type u_4} →
      [inst_1 : CategoryTheory.Category.{v_4, u_4} C] →
        (wedge : (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) → CategoryTheory.Limits.Wedge F) →
          ((F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) → CategoryTheory.Limits.IsLimit (wedge F)) →
            CategoryTheory.Limits.ChosenEndsOfShape J C
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumAddHom_toZeroHom : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ), ↑(DFinsupp.sumAddHom φ) = DFinsupp.sumZeroHom fun i => ↑(φ i)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorLeftUnmopIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ)
  (X_1 : C),
  X.tensorLeftUnmopIso.hom.app X_1 =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X.unmop X_1)
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
InnerProductSpace.volume_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [Nontrivial E] (x : E) (r : ℝ),
  MeasureTheory.volume (Metric.ball x r) =
    ENNReal.ofReal r ^ Module.finrank ℝ E *
      ENNReal.ofReal (√Real.pi ^ Module.finrank ℝ E / Real.Gamma (↑(Module.finrank ℝ E) / 2 + 1))
-- Std.Data.Iterators.Producers.Monadic.Array
/-- Returns a finite monadic iterator for the given array.
The iterator yields the elements of the array in order and then terminates. There are no side
effects.

The pure version of this iterator is `Array.iter`.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Array.iterM : {α : Type w} → Array α → (m : Type w → Type w') → [Pure m] → Std.IterM m α
-- Mathlib.Analysis.Normed.Module.RCLike.Real
range_norm : ∀ (E : Type u_1) [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] [NontrivialTopology E], Set.range norm = Set.Ici 0
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_sdiff_eq_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {K : Set α} (X : Set α), K ⊆ M.coloops → M.closure (X \ K) = M.closure X \ K
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.comap_monotone : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G'),
  Monotone (SimpleGraph.Subgraph.comap f)
-- Std.Time.DateTime
/-- Getter for the `PlainTime` inside of a `DateTime`
 -/
Std.Time.DateTime.time : Std.Time.DateTime → Std.Time.PlainTime
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkNotCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (gate : aig.Ref),
  aig.mkNotCached gate = { aig := aig, ref := gate.not }
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.PropertyIsLocal.ofLocalizationSpan : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.PropertyIsLocal P → RingHom.OfLocalizationSpan P
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryLT! : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtDTreeMap α (fun x => β) cmp → α → α × β
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_modify_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {k : α} {f : β k → β k} (h : m.WF) {hc : k ∈ m.modify k f}, (m.modify k f).get k hc = f (m.get k ⋯)
-- Lean.Elab.SyntheticMVars
/-- Remove `mvarId` from the `syntheticMVars` table. We use this method after
the metavariable has been synthesized.
 -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.markAsResolved : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.coeff_mirror : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (n : ℕ),
  p.mirror.coeff n = p.coeff ((Polynomial.revAt (p.natDegree + p.natTrailingDegree)) n)
-- Mathlib.Order.Concept
Concept.isUpperSet_intent_lt : ∀ {α : Type u_6} [inst : PartialOrder α] (c : Concept α α fun x1 x2 => x1 < x2), IsUpperSet c.intent
-- Lean.Elab.DefView
Lean.Elab.DefKind.theorem.sizeOf_spec : sizeOf Lean.Elab.DefKind.theorem = 1
-- Batteries.Data.Fin.Coding
Fin.encodeChar.eq_1 : ∀ (c : Char),
  Fin.encodeChar c =
    if x : c.toNat < Char.minSurrogate then ⟨c.toNat, ⋯⟩ else ⟨c.toNat - (Char.maxSurrogate + 1 - Char.minSurrogate), ⋯⟩
-- Init.Data.BitVec.Lemmas
/-- `x - z ≤ y - z` if and only if `x ≤ y`
when `x - z` and `y - z` do not overflow.
 -/
BitVec.sub_le_sub_iff_le : ∀ {w : ℕ} {x y z : BitVec w}, z ≤ x → z ≤ y → (x - z ≤ y - z ↔ x ≤ y)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_pi_mulSingle' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (a : ι) (x : M) (s : Finset ι),
  ∏ a' ∈ s, Pi.mulSingle a x a' = if a ∈ s then x else 1
-- Mathlib.RingTheory.Localization.BaseChange
IsLocalization.Away.tensor : ∀ {R : Type u_7} {S : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (r : R)
  (A : Type u_9) [inst_3 : CommSemiring A] [inst_4 : Algebra R A] [IsLocalization.Away r A],
  IsLocalization.Away ((algebraMap R S) r) (TensorProduct R S A)
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceBilin_eq_covarianceBilinDual : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] {μ : MeasureTheory.Measure E} (x y : E),
  ((ProbabilityTheory.covarianceBilin μ) x) y =
    ((ProbabilityTheory.covarianceBilinDual μ) ((InnerProductSpace.toDualMap ℝ E) x))
      ((InnerProductSpace.toDualMap ℝ E) y)
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd.eq_1 : ∀ (X Y : TopCat),
  X.prodIsoProd Y =
    (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Limits.pair X Y)).conePointUniqueUpToIso
      (X.prodBinaryFanIsLimit Y)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.coeff_toMultiplicativeAlgEquiv_apply : ∀ (R : Type u_1) (A : Type u_4) (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddMonoid M] (x : AddMonoidAlgebra A M),
  ((AddMonoidAlgebra.toMultiplicativeAlgEquiv R A M) x).coeff = Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff
-- Mathlib.Algebra.Group.Prod
/-- Coproduct of two `MulHom`s with the same codomain:
`f.coprod g (p : M × N) = f p.1 * g p.2`.
(Commutative codomain; for the general case, see `MulHom.noncommCoprod`)  -/
MulHom.coprod : {M : Type u_3} →
  {N : Type u_4} →
    {P : Type u_5} →
      [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : CommSemigroup P] → (M →ₙ* P) → (N →ₙ* P) → M × N →ₙ* P
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.domCongr_symm : ∀ (k : Type u_1) {G : Type u_2} {H : Type u_3} (A : Type u_4) [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : Semiring A] [inst_3 : CommSemiring k] [inst_4 : Algebra k A] [inst_5 : MulSemiringAction G A]
  [inst_6 : MulSemiringAction H A] [inst_7 : SMulCommClass G k A] [inst_8 : SMulCommClass H k A] {e : G ≃* H}
  (he : ∀ (a : G) (x : A), a • x = e a • x),
  (SkewMonoidAlgebra.domCongrAlg k A he).symm = SkewMonoidAlgebra.domCongrAlg k A ⋯
-- Mathlib.Data.Set.Finite.Basic
Set.infinite_union : ∀ {α : Type u} {s t : Set α}, (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite
-- Mathlib.Algebra.Category.Ring.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
SemiRingCat.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.comp_of_mem_nhdsWithin_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {s : Set α} {x : α} {g : β → γ} {t : Set β},
  ContinuousWithinAt g t (f x) →
    ContinuousWithinAt f s x → t ∈ nhdsWithin (f x) (f '' s) → ContinuousWithinAt (g ∘ f) s x