mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.pow : ∀ {𝕜 : 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] {s : Set M} {F' : Type u_21} [inst_6 : NormedRing F']
  [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'}, MDiff[s] p → ∀ (n : ℕ), MDiff[s] (p ^ n)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- A more explicit version of `FamilyOfElements.PullbackCompatible` for a `Presieve.ofArrows`.
 -/
CategoryTheory.Presieve.Arrows.PullbackCompatible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {B : C} →
        {I : Type u_1} →
          {X : I → C} →
            (π : (i : I) → X i ⟶ B) →
              [(CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] →
                ((i : I) → P.obj (Opposite.op (X i))) → Prop
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.ofEq_coe : ∀ {M : Type u_2} {N : Type u_3} {φ : M → N} {X : Type u_5} [inst : VAdd M X] {Y : Type u_6} [inst_1 : VAdd N Y]
  {φ' : M → N} (h : φ = φ') (f : X →ₑ[φ] Y), (AddActionHom.ofEq h f).toFun = f.toFun
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.norm : Lean.Meta.Grind.Params → Lean.Meta.Simp.Context
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
/-- The homeomorphism between the character space of the unital C⋆-subalgebra generated by a
single normal element `a : A` and `spectrum ℂ a`.  -/
StarAlgebra.elemental.characterSpaceHomeo : {A : Type u_1} →
  [inst : CStarAlgebra A] →
    (a : A) → [inst_1 : IsStarNormal a] → ↑(WeakDual.characterSpace ℂ ↥(StarAlgebra.elemental ℂ a)) ≃ₜ ↑(spectrum ℂ a)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun.indepFun_add_left : ∀ {Ω : Type u_1} {ι : Type u_2} {β : Type u_3} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {m : MeasurableSpace β} [inst_2 : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.iCondIndepFun m' hm' f μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.CondIndepFun m' hm' (f i + f j) (f k) μ
-- Std.Data.HashSet.Lemmas
Std.HashSet.mem_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a b : α},
  (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Qq.Macro
/-- `a =Q b` says that `a` and `b` are definitionally equal.  -/
Qq.«term_=Q_» : Lean.TrailingParserDescr
-- Mathlib.Order.Category.Preord
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
Preord.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.Data.Set.MemPartition
sUnion_memPartition : ∀ {α : Type u_1} (f : ℕ → Set α) (n : ℕ), ⋃₀ memPartition f n = Set.univ
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sigma.fst_eq_of_dist_lt_one : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → MetricSpace (E i)] (x y : (i : ι) × E i),
  dist x y < 1 → x.fst = y.fst
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finprod_mem_powerset_sdiff_elem`. -/
finprod_mem_powerset_diff_elem : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : Set α → M} {s : Set α} {a : α},
  s.Finite →
    a ∈ s →
      ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 s), f t =
        (∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f t) * ∏ᶠ (t : Set α) (_ : t ∈ 𝒫 (s \ {a})), f (insert a t)
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.isClosed_range : ∀ {α : Type u_4} {β : Type u_5} [inst : PseudoEMetricSpace α] [inst_1 : EMetricSpace β] [CompleteSpace α] {f : α → β}
  {K : NNReal}, AntilipschitzWith K f → UniformContinuous f → IsClosed (Set.range f)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey!ₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (l : Std.DTreeMap.Internal.Impl α β) (k : α) [inst_1 : Inhabited α],
  l.getKey!ₘ k = (l.getKey?ₘ k).get!
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.instIsFiniteTypeMap : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₁} [inst_3 : CategoryTheory.Category.{v₁, u₁} C']
  {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat}
  [inst_4 : CategoryTheory.HasSheafify J' AddCommGrpCat] [inst_5 : J'.WEqualsLocallyBijective AddCommGrpCat]
  {M : SheafOfModules R} (G : M.GeneratingSections) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S))
  [inst_6 :
    CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u', max u u₁, max (max (u + 1) u') v',
        max (max (u + 1) u₁) v₁}
      F]
  (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) [G.IsFiniteType], (G.map F η).IsFiniteType
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_semilinearMap : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  {F : Type u_14} [inst_6 : FunLike F M M₃] [inst_7 : SemilinearMapClass F σ M M₃] (f : F), ⇑↑f = ⇑f
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getEntry_eq_getEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : PartialEquivBEq α]
  [inst_3 : LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α}
  {h : m.contains a = true},
  m.getEntry a h = Std.Internal.List.getEntry a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
/-- If `C, D` has all colimits of shape `J`, and `G` preserves them, then `preservesColimitIso`
is functorial w.r.t. `F`.  -/
CategoryTheory.preservesColimitNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            [inst_2 : CategoryTheory.Category.{w', w} J] →
              [CategoryTheory.Limits.PreservesColimitsOfShape J G] →
                [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J D] →
                  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape J C] →
                    CategoryTheory.Limits.colim.comp G ≅
                      ((CategoryTheory.Functor.whiskeringRight J C D).obj G).comp CategoryTheory.Limits.colim
-- Mathlib.Algebra.Algebra.Equiv
/-- Auxiliary definition to avoid looping in `dsimp` with `AlgEquiv.ofLinearEquiv_symm`.  -/
AlgEquiv.ofLinearEquiv_symm.aux : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] →
            [inst_3 : Algebra R A₁] →
              [inst_4 : Algebra R A₂] →
                (l : A₁ ≃ₗ[R] A₂) → l 1 = 1 → (∀ (x y : A₁), l (x * y) = l x * l y) → A₂ ≃ₐ[R] A₁
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The trivial continuous homomorphism.  -/
ContinuousAddMonoidHom.instZero : (A : Type u_2) →
  (B : Type u_3) →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → Zero (A →ₜ+ B)
-- Mathlib.Data.Set.Functor
instLawfulMonadSetM : LawfulMonad SetM
-- Std.Net.Addr
Std.Net.IPAddr.v4.injEq : ∀ (addr addr_1 : Std.Net.IPv4Addr), (Std.Net.IPAddr.v4 addr = Std.Net.IPAddr.v4 addr_1) = (addr = addr_1)
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkHCongrProof : Lean.Expr → Lean.Expr → Bool → Lean.Meta.Grind.GoalM Lean.Expr
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_eq_zero`. -/
SkewMonoidAlgebra.ofFinsupp_eq_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a : G →₀ k}, { coeff := a } = 0 ↔ a = 0
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendRestrictScalarsAdj.homEquiv_symm_apply : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {X : ModuleCat R}
  {Y : ModuleCat S} (g : X ⟶ (ModuleCat.restrictScalars f).obj Y),
  (ModuleCat.ExtendRestrictScalarsAdj.homEquiv f).symm g =
    ModuleCat.ExtendRestrictScalarsAdj.HomEquiv.fromExtendScalars f g
-- Mathlib.Order.Hom.Basic
OrderHom.prodIso_symm_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  (f : (α →o β) × (α →o γ)), (RelIso.symm OrderHom.prodIso) f = f.1.prod f.2
-- Mathlib.Analysis.Calculus.Deriv.Prod
deriv_pi : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_1} {E' : ι → Type u_2}
  [inst_1 : (i : ι) → NormedAddCommGroup (E' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i},
  (∀ (i : ι), DifferentiableAt 𝕜 (fun x => φ x i) x) → deriv φ x = fun i => deriv (fun x => φ x i) x
-- Mathlib.Data.Nat.ModEq
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`  -/
Nat.ModEq.cancel_right_div_gcd : ∀ {m a b c : ℕ}, 0 < m → a * c ≡ b * c [MOD m] → a ≡ b [MOD m / m.gcd c]
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Mul α] →
      [inst_1 : Add α] →
        [inst_2 : Mul β] →
          [inst_3 : Add β] →
            [inst_4 : LE α] →
              [inst_5 : LE β] →
                (toRingEquiv : α ≃+* β) → (∀ {a b : α}, toRingEquiv.toFun a ≤ toRingEquiv.toFun b ↔ a ≤ b) → α ≃+*o β
-- Mathlib.Data.List.Lattice
List.Nodup.bagInter_right : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α], l₁.Nodup → (l₁.bagInter l₂).Nodup
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.instInhabitedTrySuggestionEntry.default : Lean.Elab.Tactic.Try.TrySuggestionEntry
-- Mathlib.Order.OmegaCompletePartialOrder
Prod.ωSup_fst : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α × β)),
  (OmegaCompletePartialOrder.ωSup c).1 = OmegaCompletePartialOrder.ωSup (c.map OrderHom.fst)
-- Mathlib.Logic.Encodable.Basic
PNat.encodable : Encodable ℕ+
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.neg_neg_iff : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a b : G}, AddCommute (-a) (-b) ↔ AddCommute a b
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
/-- The product of tensor products made of a single vector is the same as a single product of
all the vectors.  -/
TensorPower.list_prod_gradedMonoid_mk_single : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (n : ℕ)
  (x : Fin n → M),
  (List.map (fun a => GradedMonoid.mk 1 ((PiTensorProduct.tprod R) fun x_1 => x a)) (List.finRange n)).prod =
    GradedMonoid.mk n ((PiTensorProduct.tprod R) x)
-- Init.PropLemmas
Decidable.not_and_not_right : ∀ {b a : Prop} [Decidable b], ¬(a ∧ ¬b) ↔ a → b
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- **Alias** of `AbsolutelyContinuousOnInterval.uniformContinuousOn`.

---

If `f` is absolutely continuous on `uIcc a b`, then `f` is uniformly continuous on `uIcc a b`.
 -/
AbsolutelyContinuousOnInterval.uniformlyContinuousOn : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F},
  AbsolutelyContinuousOnInterval f a b → UniformContinuousOn f (Set.uIcc a b)
-- Mathlib.LinearAlgebra.Finsupp.Pi
Finsupp.uniqueLinearEquiv_symm_apply_apply : ∀ (R : Type u_1) {α : Type u_3} (M : Type u_4) [inst : AddCommMonoid M] [inst_1 : Semiring R] [inst_2 : Module R M]
  (a : α) [inst_3 : Subsingleton α] (m : M) (b : α), ((Finsupp.uniqueLinearEquiv R M a).symm m) b = m
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.instVAddSubtypeMem : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        {module_M : Module R M} → (p : Submodule R M) → {α : Type u_1} → [VAdd M α] → VAdd (↥p) α
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.ι_fromGlued : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Scheme.Cover.gluedCover 𝒰).ι x)
      (AlgebraicGeometry.Scheme.Cover.fromGlued 𝒰) =
    𝒰.f x
-- Mathlib.Algebra.Regular.Opposite
isAddLeftRegular_op : ∀ {R : Type u_1} [inst : Add R] {a : R}, IsAddLeftRegular (AddOpposite.op a) ↔ IsAddRightRegular a
-- Mathlib.Data.Real.Pointwise
Real.sSup_smul_of_nonpos : ∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Module α ℝ]
  [IsOrderedModule α ℝ] {a : α}, a ≤ 0 → ∀ (s : Set ℝ), sSup (a • s) = a • sInf s
-- Mathlib.Data.ENNReal.Operations
ENNReal.iInf_add : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal}, iInf f + a = ⨅ i, f i + a
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : A ⟶ Res(f)(B)`,
this is the induced map `Z₁(G, A) ⟶ Z₁(H, B)`.  -/
groupHomology.mapCycles₁ : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k G} →
          {B : Rep.{u, u, u} k H} →
            (f : G →* H) →
              (A ⟶ Rep.res f B) →
                (ModuleCat.of k ↥(groupHomology.cycles₁ A) ⟶ ModuleCat.of k ↥(groupHomology.cycles₁ B))
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_pos_pos_neg_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A : Finset G} {K : ℝ},
  ↑(A ^ 3).card ≤ K * ↑A.card → ↑(A * A * A⁻¹).card ≤ K ^ 2 * ↑A.card
-- Mathlib.FieldTheory.LinearDisjoint
_private.Mathlib.FieldTheory.LinearDisjoint.0.IntermediateField.LinearDisjoint.of_inf_eq_bot_aux : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  [IsGalois F ↥A] [FiniteDimensional F E], A ⊔ B = ⊤ → A ⊓ B = ⊥ → A.LinearDisjoint ↥B
-- Init.Data.Dyadic.Inv
/-- For positive `b`, `divAtPrec a b prec` is the unique dyadic with precision at most `prec`
satisfying both `_ * b ≤ a` and `a < (_ + ofIntWithPrec 1 prec) * b`.
 -/
Dyadic.eq_divAtPrec : ∀ {a b : Dyadic},
  0 < b →
    ∀ {prec : ℤ} {y : Dyadic},
      y.precision ≤ some prec → y * b ≤ a → a < (y + Dyadic.ofIntWithPrec 1 prec) * b → y = a.divAtPrec b prec
-- Mathlib.Analysis.ConstantSpeed
HasConstantSpeedOnWith.Icc_Icc : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {l : NNReal} {x y z : ℝ},
  HasConstantSpeedOnWith f (Set.Icc x y) l →
    HasConstantSpeedOnWith f (Set.Icc y z) l → HasConstantSpeedOnWith f (Set.Icc x z) l
-- Init.Data.Nat.Simproc
Nat.Simproc.add_eq_le : ∀ (a : ℕ) {b c : ℕ}, b ≤ c → (a + b = c) = (a = c - b)
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.coe_flipₗᵢ : ∀ {𝕜 : Type u_1} {E : Type u_4} {Fₗ : Type u_7} {Gₗ : Type u_9} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Fₗ] [inst_2 : SeminormedAddCommGroup Gₗ] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace 𝕜 Gₗ],
  ⇑(ContinuousLinearMap.flipₗᵢ 𝕜 E Fₗ Gₗ) = ContinuousLinearMap.flip
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.eq_mk'_iff_mul_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {x : M} {y : ↥S} {z : N}, z = f.mk' x y ↔ z * f ↑y = f x
-- Std.Data.TreeMap.Raw.Basic
/-- Folds the given function over the mappings in the map in descending order.  -/
Std.TreeMap.Raw.foldr : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → {δ : Type w} → (α → β → δ → δ) → δ → Std.TreeMap.Raw α β cmp → δ
-- Std.Time.Date.Unit.Year
Std.Time.Year.instInhabitedOffset : Inhabited Std.Time.Year.Offset
-- Mathlib.Combinatorics.Graph.Basic
/-- **Alias** of `Graph.edgeSet_eq_setOfPred_exists_isLink`. -/
Graph.edgeSet_eq_setOf_exists_isLink : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.edgeSet = {e | ∃ x y, G.IsLink e x y}
-- Mathlib.Data.Ineq
Mathlib.Ineq.instToString : ToString Mathlib.Ineq
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
  (∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ w j) → v.restrict i ≤ w.restrict i
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
IsLocalRing.maximalIdeal_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : IsLocalRing R] [inst_2 : CommSemiring S]
  [inst_3 : IsLocalRing S] (f : R →+* S) [IsLocalHom f],
  Ideal.comap f (IsLocalRing.maximalIdeal S) = IsLocalRing.maximalIdeal R
-- Mathlib.Topology.UniformSpace.UniformEmbedding
IsUniformEmbedding.discreteUniformity : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] [DiscreteUniformity β] {f : α → β},
  IsUniformEmbedding f → DiscreteUniformity α
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, `negSelf` is `-x` in the Localization (as a quotient type) of `M` at the
Submonoid generated by `x`.  -/
AddLocalization.Away.negSelf : {M : Type u_1} → [inst : AddCommMonoid M] → (x : M) → AddLocalization.Away x
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.instDecidableEqHomObjSimplexCategoryStdSimplexOfOppositeOp : (X : SSet) → (n : SimplexCategory) → [DecidableEq (X.obj (Opposite.op n))] → DecidableEq (SSet.stdSimplex.obj n ⟶ X)
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_ofList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  (Std.HashSet.ofList l).contains k = l.contains k
-- Mathlib.Data.ENat.Basic
instIsOrderedRingENat : IsOrderedRing ℕ∞
-- Mathlib.Algebra.Algebra.Defs
/-- `mul_left_comm` for `Algebra`s when one element is from the base ring.  -/
Algebra.left_comm : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A) (r : R)
  (y : A), x * ((algebraMap R A) r * y) = (algebraMap R A) r * (x * y)
-- Mathlib.Topology.Algebra.Monoid
MulHom.isClosed_range_coe : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : Mul M₁] [inst_3 : Mul M₂]
  [ContinuousMul M₂], IsClosed (Set.range DFunLike.coe)
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- On a metric space `X` with a measure `μ`, consider for each `x : X` a family of measurable sets
with nonempty interiors, called `setsAt x`. This family is a Vitali family if it satisfies the
following property: consider a (possibly non-measurable) set `s`, and for any `x` in `s` a
subfamily `f x` of `setsAt x` containing sets of arbitrarily small diameter. Then one can extract
a disjoint subfamily covering almost all `s`.

Vitali families are provided by covering theorems such as the Besicovitch covering theorem or the
Vitali covering theorem. They make it possible to formulate general versions of theorems on
differentiations of measure that apply in both contexts.
 -/
VitaliFamily : {X : Type u_1} → [PseudoMetricSpace X] → {m : MeasurableSpace X} → MeasureTheory.Measure X → Type u_1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_eq_get!_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {a : α}, t.get! a = (t.get? a).get!
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- Pullbacks distribute over universal coproducts on the left: This is the isomorphism
`∐ (B ×[S] Xᵢ) ≅ B ×[S] (∐ Xᵢ)`.  -/
CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) (s : (i : ι) → CategoryTheory.Limits.PullbackCone v (f i))
      (hs : (i : ι) → CategoryTheory.Limits.IsLimit (s i)) (t : CategoryTheory.Limits.PullbackCone v u)
      (ht : CategoryTheory.Limits.IsLimit t) (d : CategoryTheory.Limits.Cofan fun i => (s i).pt) (e : d.pt ≅ t.pt),
      autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
          CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left._auto_1 →
        autoParam
            (∀ (i : ι),
              CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom t.fst) = (s i).fst)
            CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left._auto_3 →
          autoParam
              (∀ (i : ι),
                CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom t.snd) =
                  CategoryTheory.CategoryStruct.comp (s i).snd (a.inj i))
              CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left._auto_5 →
            Nonempty (CategoryTheory.Limits.IsColimit d)
-- Lean.MetavarContext
Lean.instantiateLevelMVarsImp : Lean.MetavarContext → Lean.Level → Lean.MetavarContext × Lean.Level
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
SimpleGraph.Walk.penultimate_nil : ∀ {V : Type u} {G : SimpleGraph V} {v : V}, SimpleGraph.Walk.nil.penultimate = v
-- Mathlib.Topology.Category.Profinite.Basic
FintypeCat.discreteTopology : ∀ (A : FintypeCat), DiscreteTopology A.obj
-- Mathlib.Topology.Algebra.ConstMulAction
ContinuousWithinAt.fun_const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {b : β} {s : Set β},
  ContinuousWithinAt g s b → ∀ (c : M), ContinuousWithinAt (fun i => c +ᵥ g i) s b
-- Init.Data.Fin.Lemmas
Fin.rev_inj : ∀ {n : ℕ} {i j : Fin n}, i.rev = j.rev ↔ i = j
-- Mathlib.Analysis.Fourier.Convolution
/-- The Fourier transform of the convolution is given by the multiplication of the Fourier transform
of the individual functions.

Version for scalar multiplication.  -/
Real.fourier_smul_convolution_eq : ∀ {E : Type u_3} {F₁ : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F₁]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [CompleteSpace F₁] [inst_7 : NormedSpace ℂ F₁] {f₁ : E → ℂ} {f₂ : E → F₁},
  MeasureTheory.Integrable f₁ MeasureTheory.volume →
    MeasureTheory.Integrable f₂ MeasureTheory.volume →
      ∀ (ξ : E),
        FourierTransform.fourier (MeasureTheory.convolution f₁ f₂ (ContinuousLinearMap.lsmul ℂ ℂ) MeasureTheory.volume)
            ξ =
          FourierTransform.fourier f₁ ξ • FourierTransform.fourier f₂ ξ
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.Presieve.FamilyOfElements.pullback.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X Y : C}
  {S : CategoryTheory.Sieve X} (f : Y ⟶ X) (x : CategoryTheory.Presieve.FamilyOfElements P S.arrows) (x_1 : C)
  (g : x_1 ⟶ Y) (hg : (CategoryTheory.Sieve.pullback f S).arrows g),
  CategoryTheory.Presieve.FamilyOfElements.pullback f x g hg = x (CategoryTheory.CategoryStruct.comp g f) hg
-- Lean.Server.InfoUtils
Lean.Elab.instOrdHoverableInfoPrio : Ord Lean.Elab.HoverableInfoPrio
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.algebraMap_surjective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), Function.Surjective ⇑(algebraMap P.Ring S)
-- Batteries.Data.Fin.Lemmas
Fin.isNone_find?_iff : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.find? p).isNone = true ↔ ∀ (i : Fin n), p i = false