mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Constructions
Units.instTopologicalSpaceUnits.eq_1 : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M],
  Units.instTopologicalSpaceUnits = TopologicalSpace.induced (⇑(Units.embedProduct M)) inferInstance
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- The object in the category of `R`-Hopf algebras associated to an `R`-Hopf algebra.  -/
HopfAlgCat.of : (R : Type u) → [inst : CommRing R] → (X : Type v) → [inst_1 : Ring X] → [HopfAlgebra R X] → HopfAlgCat R
-- Mathlib.Analysis.LocallyConvex.SeparatingDual
SeparatingDual.exists_ne_zero : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V] [SeparatingDual R V] {x : V}, x ≠ 0 → ∃ f, f x ≠ 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_left_cancel : ∀ {α : Type u} [inst : Add α] {x y z : WithBot α} [IsLeftCancelAdd α], x ≠ ⊥ → x + y = x + z → y = z
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- The type of simplices of a simplicial set `X`. This type `X.S` is in bijection
with `X.Elements` (see `SSet.S.equivElements`), but `X.S` is not what the literature
names "category of simplices of `X`", as the category on `X.S` comes from
a preorder (see `S.le_iff_nonempty_hom`).  -/
SSet.S : SSet → Type u
-- Mathlib.Algebra.Jordan.Basic
_private.Mathlib.Algebra.Jordan.Basic.0.aux1 : ∀ {A : Type u_1} [inst : NonUnitalNonAssocCommRing A] {a b c : A},
  ⁅AddMonoid.End.mulLeft a + AddMonoid.End.mulLeft b + AddMonoid.End.mulLeft c,
      AddMonoid.End.mulLeft (a * a) + AddMonoid.End.mulLeft (b * b) + AddMonoid.End.mulLeft (c * c) +
            2 • AddMonoid.End.mulLeft (a * b) +
          2 • AddMonoid.End.mulLeft (c * a) +
        2 • AddMonoid.End.mulLeft (b * c)⁆ =
    ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (a * a)⁆ +
                  ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (b * b)⁆ +
                ⁅AddMonoid.End.mulLeft a, AddMonoid.End.mulLeft (c * c)⁆ +
              ⁅AddMonoid.End.mulLeft a, 2 • AddMonoid.End.mulLeft (a * b)⁆ +
            ⁅AddMonoid.End.mulLeft a, 2 • AddMonoid.End.mulLeft (c * a)⁆ +
          ⁅AddMonoid.End.mulLeft a, 2 • AddMonoid.End.mulLeft (b * c)⁆ +
        (⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (a * a)⁆ +
                  ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (b * b)⁆ +
                ⁅AddMonoid.End.mulLeft b, AddMonoid.End.mulLeft (c * c)⁆ +
              ⁅AddMonoid.End.mulLeft b, 2 • AddMonoid.End.mulLeft (a * b)⁆ +
            ⁅AddMonoid.End.mulLeft b, 2 • AddMonoid.End.mulLeft (c * a)⁆ +
          ⁅AddMonoid.End.mulLeft b, 2 • AddMonoid.End.mulLeft (b * c)⁆) +
      (⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (a * a)⁆ +
                ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (b * b)⁆ +
              ⁅AddMonoid.End.mulLeft c, AddMonoid.End.mulLeft (c * c)⁆ +
            ⁅AddMonoid.End.mulLeft c, 2 • AddMonoid.End.mulLeft (a * b)⁆ +
          ⁅AddMonoid.End.mulLeft c, 2 • AddMonoid.End.mulLeft (c * a)⁆ +
        ⁅AddMonoid.End.mulLeft c, 2 • AddMonoid.End.mulLeft (b * c)⁆)
-- Mathlib.MeasureTheory.Measure.Regular
/-- Let `μ` be a locally finite measure on an R₁ topological space with Borel σ-algebra.
If `μ` is inner regular for finite measure sets with respect to compact sets,
then any null measurable set of finite measure can be approximated in measure by an open set.
See also `Set.exists_isOpen_lt_of_lt` and `MeasurableSet.exists_isOpen_diff_lt`
for the case of an outer regular measure.  -/
MeasureTheory.NullMeasurableSet.exists_isOpen_symmDiff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    μ s ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (symmDiff U s) < ε
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.kernelBiprodFstIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.Limits.kernelBiprodFstIso.hom =
    (CategoryTheory.Limits.biprod.isKernelFstKernelFork X Y).lift
      (CategoryTheory.Limits.limit.cone (CategoryTheory.Limits.parallelPair CategoryTheory.Limits.biprod.fst 0))
-- Mathlib.Analysis.Real.Sqrt
Real.coe_sqrt : ∀ {x : NNReal}, ↑(NNReal.sqrt x) = √↑x
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid_isBasis_iff : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : IsDomain A] {s t : Set A},
  (AlgebraicIndependent.matroid R A).IsBasis s t ↔
    AlgebraicIndepOn R id s ∧ s ⊆ t ∧ ∀ a ∈ t, IsAlgebraic (↥(Algebra.adjoin R s)) a
-- Mathlib.Order.SuccPred.Limit
Order.IsSuccPrelimit.mid.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] {i j : α} (hi : Order.IsSuccPrelimit i) (hj : j < i),
  hi.mid hj = Classical.indefiniteDescription (Membership.mem (Set.Ioo j i)) ⋯
-- Mathlib.Data.Nat.Totient
/-- For `d ∣ n`, the totient of `n/d` equals the number of values `k < n` such that `gcd n k = d`  -/
Nat.totient_div_of_dvd : ∀ {n d : ℕ}, d ∣ n → (n / d).totient = {k ∈ Finset.range n | n.gcd k = d}.card
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A set is countably compact if and only if every sequence eventually in it has a cluster point
in it.  -/
isCountablyCompact_iff_seq_clusterPt : ∀ {E : Type u_2} [inst : TopologicalSpace E] {A : Set E},
  IsCountablyCompact A ↔ ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in Filter.atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a Filter.atTop x
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientWithinAt_iff_tendsto : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s : Set F},
  HasGradientWithinAt f f' s x ↔
    Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - inner 𝕜 f' (x' - x)‖) (nhdsWithin x s) (nhds 0)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.toLinearMap_mkQL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (S : Submodule R M), ↑S.mkQL = S.mkQ
-- Mathlib.Algebra.Star.Basic
/-- `star` commutes with scalar multiplication  -/
StarModule.star_smul : ∀ {R : Type u} {A : Type v} {inst : Star R} {inst_1 : Star A} {inst_2 : SMul R A} [self : StarModule R A] (r : R)
  (a : A), star (r • a) = star r • star a
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.w_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {Q Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj P Q ⟶ Z_1),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Q)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inl Q) h) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Q)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight inr Q) h)
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_integral_norm : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_3 : NormedSpace ℝ E]
  (T : Set α → E →L[ℝ] F) {C : ℝ},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ‖T s‖ ≤ C * μ.real s) →
    ∀ {f : MeasureTheory.SimpleFunc α E},
      MeasureTheory.Integrable (⇑f) μ →
        ‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤
          C * MeasureTheory.SimpleFunc.integral μ (MeasureTheory.SimpleFunc.map norm f)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.eq_7 : ∀ (motive : ZMod 8 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 4)
  (h_4 : Unit → motive 6) (h_5 : Unit → motive 1) (h_6 : Unit → motive 7) (h_7 : Unit → motive 3)
  (h_8 : Unit → motive 5),
  (match 3 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 4 => h_3 ()
    | 6 => h_4 ()
    | 1 => h_5 ()
    | 7 => h_6 ()
    | 3 => h_7 ()
    | 5 => h_8 ()) =
    h_7 ()
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator : (α : Type u) → (α → Type v) → [Ord α] → Type (max u v)
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.homMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (f f_1 : F.toFunctor ⟶ G.toFunctor) (e_f : f = f_1)
  [inst_4 : CategoryTheory.NatTrans.IsMonoidal f],
  CategoryTheory.LaxMonoidalFunctor.homMk f = CategoryTheory.LaxMonoidalFunctor.homMk f_1
-- Mathlib.Geometry.Euclidean.Sphere.Basic
/-- The distance from the center of a sphere to any point strictly between
two points on the sphere is strictly less than the radius.  -/
EuclideanGeometry.Sphere.dist_center_lt_radius_of_sbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p : P} {s : EuclideanGeometry.Sphere P},
  p₁ ∈ s → p₂ ∈ s → Sbtw ℝ p₁ p p₂ → dist s.center p < s.radius
-- Init.Data.SInt.Lemmas
ISize.ofInt_sub : ∀ (a b : ℤ), ISize.ofInt (a - b) = ISize.ofInt a - ISize.ofInt b
-- Mathlib.Logic.Pairwise
Set.Pairwise.imp : ∀ {α : Type u_1} {r p : α → α → Prop} {s : Set α}, s.Pairwise r → (∀ ⦃a b : α⦄, r a b → p a b) → s.Pairwise p
-- Mathlib.Dynamics.Flow
Flow.toHomeomorph_symm_apply : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddGroup τ]
  (ϕ : Flow τ α) (t : τ) (x : α), (ϕ.toHomeomorph t).symm x = ϕ.toFun (-t) x
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.id_hom : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (x : ℤ),
  (CategoryTheory.CategoryStruct.id X).hom x = CategoryTheory.CategoryStruct.id (X.H x)
-- Mathlib.Algebra.Group.Defs
three_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M), 3 • a = a + (a + a)
-- Mathlib.Algebra.Order.Floor.Defs
Int.ceil_toNat : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] (a : α), ⌈a⌉.toNat = ⌈a⌉₊
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- One can enlarge a Vitali family by adding to the sets `f x` at `x` all sets which are not
contained in a `δ`-neighborhood on `x`. This does not change the local filter at a point, but it
can be convenient to get a nicer global behavior.  -/
VitaliFamily.enlarge : {X : Type u_1} →
  [inst : PseudoMetricSpace X] →
    {m0 : MeasurableSpace X} → {μ : MeasureTheory.Measure X} → VitaliFamily μ → (δ : ℝ) → 0 < δ → VitaliFamily μ
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorHomEquiv_id : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₁]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V F₁ F₁],
  (CategoryTheory.Enriched.FunctorCategory.functorHomEquiv V) (CategoryTheory.CategoryStruct.id F₁) =
    CategoryTheory.Enriched.FunctorCategory.functorEnrichedId V F₁
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.collision.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (ks : Array α) (vs : Array β) (h : ks.size = vs.size),
  sizeOf (Lean.PersistentHashMap.Node.collision ks vs h) = 1 + sizeOf ks + sizeOf vs + sizeOf h
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.singleMapHomologicalComplex_hom_app_self : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] [inst_4 : CategoryTheory.Limits.HasZeroObject W₁]
  [inst_5 : CategoryTheory.Limits.HasZeroObject W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_6 : F.PreservesZeroMorphisms] (c : ComplexShape ι) [inst_7 : DecidableEq ι] (j : ι) (X : W₁),
  ((HomologicalComplex.singleMapHomologicalComplex F c j).hom.app X).f j =
    CategoryTheory.CategoryStruct.comp (F.map (HomologicalComplex.singleObjXSelf c j X).hom)
      (HomologicalComplex.singleObjXSelf c j (F.obj X)).inv
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.yonedaEquiv_symm_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X X' : C} (f : X' ⟶ X) (F : CategoryTheory.Sheaf J (Type v))
  (x : F.obj.obj (Opposite.op X)),
  CategoryTheory.CategoryStruct.comp (J.yoneda.map f) (J.yonedaEquiv.symm x) =
    J.yonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.obj.map f.op)) x)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.mem_span_iff_id : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  {a : V}, LinearIndepOn K id s → (a ∈ Submodule.span K s ↔ LinearIndepOn K id (insert a s) → a ∈ s)
-- Mathlib.Data.Sym.Basic
Sym.instEmptyCollectionOfNatNat : {α : Type u_1} → EmptyCollection (Sym α 0)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.coeff_truncate : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m) (i : Fin n)
  (x : TruncatedWittVector p m R),
  TruncatedWittVector.coeff i ((TruncatedWittVector.truncate hm) x) = TruncatedWittVector.coeff (Fin.castLE hm i) x
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- If a sequence `g` converges to some `b`, then the sequence of constant functions
`fun n ↦ fun a ↦ g n` converges to the constant function `fun a ↦ b` on any set `s`.  -/
Filter.Tendsto.tendstoUniformlyOn_const : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {p : Filter ι} {g : ι → β} {b : β},
  Filter.Tendsto g p (nhds b) → ∀ (s : Set α), TendstoUniformlyOn (fun n x => g n) (fun x => b) p s
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- A pullback cone to `X` is a limit if its corresponding binary fan in `Over X` is a limit.  -/
CategoryTheory.Limits.IsLimit.pullbackConeEquivBinaryFanInverse : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : Y ⟶ X} →
        {g : Z ⟶ X} →
          {c : CategoryTheory.Limits.BinaryFan (CategoryTheory.Over.mk f) (CategoryTheory.Over.mk g)} →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.pullbackConeEquivBinaryFan.inverse.obj c)
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.isInitial_one : Ordinal.IsInitial 1
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.trans_refl : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), e.trans (ContinuousAffineEquiv.refl k P₂) = e
-- Mathlib.Combinatorics.Quiver.Path.Weight
_private.Mathlib.Combinatorics.Quiver.Path.Weight.0.Quiver.Path.weight.match_1.eq_1 : ∀ {V : Type u_2} [inst : Quiver V] (motive : (x x_1 : V) → Quiver.Path x x_1 → Sort u_3) (a : V)
  (h_1 : (a : V) → motive a a Quiver.Path.nil)
  (h_2 : (a x b : V) → (p : Quiver.Path a b) → (e : b ⟶ x) → motive a x (p.cons e)),
  (match a, a, Quiver.Path.nil with
    | a, .(a), Quiver.Path.nil => h_1 a
    | a, x, p.cons e => h_2 a x b p e) =
    h_1 a
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.uniformContinuous_compareEquiv_symm : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) (pkg' : AbstractCompletion.{vα', uα} α),
  UniformContinuous ⇑(pkg.compareEquiv pkg').symm
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.instFunLike : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : Star A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] → [inst_6 : Star B] → FunLike (A →⋆ₙₐ[R] B) A B
-- Init.Data.List.Lemmas
List.foldl_flatMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → List β} {g : γ → β → γ} {l : List α} {init : γ},
  List.foldl g init (List.flatMap f l) = List.foldl (fun acc x => List.foldl g acc (f x)) init l
-- Lean.Meta.AbstractNestedProofs
Lean.Meta.AbstractNestedProofs.Context.mk.sizeOf_spec : ∀ (cache : Bool), sizeOf { cache := cache } = 1 + sizeOf cache
-- Mathlib.CategoryTheory.Sites.Equivalence
/-- Transport a presheaf to the equivalent category and sheafify there.  -/
CategoryTheory.Equivalence.transportAndSheafify : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          (K : CategoryTheory.GrothendieckTopology D) →
            (e : C ≌ D) →
              (A : Type u₃) →
                [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
                  [CategoryTheory.Functor.IsDenseSubsite K J e.inverse] →
                    [CategoryTheory.HasSheafify K A] →
                      CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ A) (CategoryTheory.Sheaf J A)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.metaConfig : Lean.Meta.Simp.Context → Lean.Meta.ConfigWithKey
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral value of a monic polynomial `P` is less than or equal to one if and only
if all of its coefficients have norm less than or equal to 1.  -/
spectralValue_le_one_iff : ∀ {R : Type u_1} [inst : NormedDivisionRing R] {P : Polynomial R},
  P.Monic → (spectralValue P ≤ 1 ↔ ∀ (n : ℕ), ‖P.coeff n‖ ≤ 1)
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.trivialization_symm_apply : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] [inst_2 : Zero F] (b : B)
  (f : F), (Bundle.Trivial.trivialization B F).symm b f = f
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
CategoryTheory.CommSq.instHasLiftRightAdjoin : ∀ {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] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
  {A B : C} {X Y : D} {i : A ⟶ B} {p : X ⟶ Y} {u : G.obj A ⟶ X} {v : G.obj B ⟶ Y}
  (sq : CategoryTheory.CommSq u (G.map i) p v) (adj : G ⊣ F) [sq.HasLift], ⋯.HasLift
-- Mathlib.Data.Finset.Density
Finset.dens_filter_add_dens_filter_not_eq_dens : ∀ {α : Type u_4} [inst : Fintype α] {s : Finset α} (p : α → Prop) [inst_1 : DecidablePred p]
  [inst_2 : (x : α) → Decidable ¬p x], {a ∈ s | p a}.dens + {a ∈ s | ¬p a}.dens = s.dens
-- Init.Data.Array.Lemmas
List.firstM_toArray : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Alternative m] {as : List α} {f : α → m β},
  Array.firstM f as.toArray = List.firstM f as
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Mathlib.Algebra.Category.Ring.Basic
CategoryTheory.Iso.commSemiRingCatIsoToRingEquiv_toRingHom : ∀ {R S : CommSemiRingCat} (e : R ≅ S), ↑e.commSemiRingCatIsoToRingEquiv = CommSemiRingCat.Hom.hom e.hom
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.minView!.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k' : α) →
                (v' : β k') →
                  (l' r' : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')) →
            motive l
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.ringEquivOpMop_symm_apply_coe : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R) (a : (↥S.op)ᵐᵒᵖ),
  ↑(S.ringEquivOpMop.symm a) = MulOpposite.unop ↑(MulOpposite.unop a)
-- Mathlib.Data.Int.Fib.Basic
Int.gcd_fib : ∀ (m n : ℤ), (Int.fib m).gcd (Int.fib n) = Nat.fib (m.gcd n)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.find?_toArray_eq_none_iff_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  Array.find? (fun x => cmp x.1 k == Ordering.eq) t.toArray = none ↔ k ∉ t
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.orderIsoRingCon_symm_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (ringCon : RingCon R),
  (RelIso.symm TwoSidedIdeal.orderIsoRingCon) ringCon = { ringCon := ringCon }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
HomogeneousLocalization.mapId.congr_simp : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {P Q : Submonoid A} (h : P ≤ Q),
  HomogeneousLocalization.mapId 𝒜 h = HomogeneousLocalization.mapId 𝒜 h
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `UniformCauchySeqOn.div` -/
UniformCauchySeqOn.fun_div : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {s : Set β},
  UniformCauchySeqOn f l s → UniformCauchySeqOn f' l s → UniformCauchySeqOn (fun i i_1 => f i i_1 / f' i i_1) l s
-- Lean.Elab.Tactic.Induction
Lean.Elab.Tactic.ElimApp.Result.mk.inj : ∀ {elimApp : Lean.Expr} {elimArgs : Array Lean.Expr} {motive : Lean.MVarId} {alts : Array Lean.Elab.Tactic.ElimApp.Alt}
  {others : Array Lean.MVarId} {complexArgs : Array Lean.Expr} {elimApp_1 : Lean.Expr} {elimArgs_1 : Array Lean.Expr}
  {motive_1 : Lean.MVarId} {alts_1 : Array Lean.Elab.Tactic.ElimApp.Alt} {others_1 : Array Lean.MVarId}
  {complexArgs_1 : Array Lean.Expr},
  { elimApp := elimApp, elimArgs := elimArgs, motive := motive, alts := alts, others := others,
        complexArgs := complexArgs } =
      { elimApp := elimApp_1, elimArgs := elimArgs_1, motive := motive_1, alts := alts_1, others := others_1,
        complexArgs := complexArgs_1 } →
    elimApp = elimApp_1 ∧
      elimArgs = elimArgs_1 ∧ motive = motive_1 ∧ alts = alts_1 ∧ others = others_1 ∧ complexArgs = complexArgs_1
-- Mathlib.Probability.Decision.Risk.Defs
ProbabilityTheory.avgRisk.eq_1 : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧) (κ : ProbabilityTheory.Kernel 𝓧 𝓨)
  (π : MeasureTheory.Measure Θ), ProbabilityTheory.avgRisk ℓ P κ π = ∫⁻ (θ : Θ), ∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ ∂π