mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- **Alias** of `ProbabilityTheory.iIndepFun.charFunDual_map_fun_finsetSum_eq_prod`. -/
ProbabilityTheory.iIndepFun.charFunDual_map_fun_finset_sum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : NormedSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun ω => ∑ i ∈ s, X i ω) P) =
        ∏ i ∈ s, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P)
-- Init.Meta.Defs
Lean.Name.appendBefore : Lean.Name → String → Lean.Name
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv_le_inv : ∀ {G : Type u_2} [inst : Group G] (S T : Submonoid G), S⁻¹ ≤ T⁻¹ ↔ S ≤ T
-- Mathlib.RingTheory.Ideal.Operations
Ideal.instIsTorsionFreeSubtypeMemSubmodule : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} {A : Type u_2} [inst_1 : Semiring S] [inst_2 : SMul R S]
  [inst_3 : AddCommMonoid A] [inst_4 : Module R A] [inst_5 : Module S A] [inst_6 : IsScalarTower R S A]
  [Module.IsTorsionFree R A] {I : Submodule S A}, Module.IsTorsionFree R ↥I
-- Mathlib.Data.Sym.NatCard
Sym2.natCard_subtype_diag : ∀ (α : Type u_1), Nat.card { a // a.IsDiag } = Nat.card α
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.mono_ac : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  {ν : MeasureTheory.Measure α} {φ : ι → Set α},
  MeasureTheory.AECover μ l φ → ν.AbsolutelyContinuous μ → MeasureTheory.AECover ν l φ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.isLocalizationMap : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (self : S.LocalizationMap N), S.IsLocalizationMap self.toFun
-- Mathlib.Order.Hom.Bounded
TopHom.id.eq_1 : ∀ (α : Type u_2) [inst : Top α], TopHom.id α = { toFun := id, map_top' := ⋯ }
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Combinators.Monadic.FlatMap.0.Std.Iterators.Types.Flatten.instFinitenessRelation : {α α₂ β : Type w} →
  {m : Type w → Type w'} →
    [inst : Monad m] →
      [inst_1 : Std.Iterator α m (Std.IterM m β)] →
        [inst_2 : Std.Iterator α₂ m β] →
          [Std.Iterators.Finite α m] →
            [Std.Iterators.Finite α₂ m] → Std.Iterators.FinitenessRelation (Std.Iterators.Types.Flatten α α₂ β m) m
-- Mathlib.LinearAlgebra.Contraction
lTensorHomEquivHomLTensor.eq_1 : ∀ (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] [inst_7 : Module.Projective R M] [inst_8 : Module.Finite R M],
  lTensorHomEquivHomLTensor R M P Q =
    ((TensorProduct.congr (LinearEquiv.refl R P) (dualTensorHomEquiv R M Q).symm).trans
          (TensorProduct.leftComm R P (Module.Dual R M) Q)).trans
      (dualTensorHomEquiv R M (TensorProduct R P Q))
-- Init.Data.SInt.Lemmas
Int16.add_left_inj : ∀ {a b : Int16} (c : Int16), a + c = b + c ↔ a = b
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.self_le_maxKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (cmp k ((t.insert k v).maxKey ⋯)).isLE = true
-- Lean.HeadIndex
Lean.HeadIndex.const.inj : ∀ {constName constName_1 : Lean.Name},
  Lean.HeadIndex.const constName = Lean.HeadIndex.const constName_1 → constName = constName_1
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterMatrix.reindex_relationsSet : ∀ {B : Type u_1} {B' : Type u_2} (M : CoxeterMatrix B) (e : B ≃ B'),
  (CoxeterMatrix.reindex e M).relationsSet = ⇑(FreeGroup.freeGroupCongr e) '' M.relationsSet
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g],
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F) →
    CategoryTheory.Comonad.PreservesLimitOfIsCosplitPair F
-- Mathlib.NumberTheory.Zsqrtd.Basic
/-- The one of the ring  -/
Zsqrtd.instOne : {d : ℤ} → One (ℤ√d)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The unit axiom associated to an algebra.  -/
CategoryTheory.Monad.Algebra.unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (self : T.Algebra),
  CategoryTheory.CategoryStruct.comp (T.η.app self.A) self.a = CategoryTheory.CategoryStruct.id self.A
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.isFintype : (self : FinPartOrd) → Fintype ↑self.toPartOrd
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mk'_d_1_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d₀ : X₁ ⟶ X₀)
  (succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' CategoryTheory.CategoryStruct.comp d f = 0),
  (ChainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d 1 0 = d₀
-- Mathlib.Order.Heyting.Basic
compl_le_himp : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, aᶜ ≤ a ⇨ b
-- Mathlib.Algebra.Group.Action.Option
Option.VAdd : {M : Type u_1} → {α : Type u_3} → [VAdd M α] → VAdd M (Option α)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.measure_apply : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G] [S : MeasurableSpace G]
  [inst_2 : BorelSpace G] {s : Set G}, MeasurableSet s → μ.measure s = μ.outerMeasure s
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.memLp_of_cauchy_tendsto : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {E : Type u_3}
  [inst : NormedAddCommGroup E],
  1 ≤ p →
    ∀ {f : ℕ → α → E},
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        ∀ (f_lim : α → E),
          MeasureTheory.AEStronglyMeasurable f_lim μ →
            Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - f_lim) p μ) Filter.atTop (nhds 0) →
              MeasureTheory.MemLp f_lim p μ
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_erase_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m.erase k).size ≤ m.size
-- Mathlib.FieldTheory.IsSepClosed
/-- A (random) homomorphism from a separable extension L of K into a separably
closed extension M of K.  -/
IsSepClosed.lift : {K : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [inst_3 : Field M] → [inst_4 : Algebra K M] → [IsSepClosed M] → [Algebra.IsSeparable K L] → L →ₐ[K] M
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TermElabM.run : {α : Type} →
  Lean.Elab.TermElabM α →
    optParam Lean.Elab.Term.Context { } → optParam Lean.Elab.Term.State { } → Lean.MetaM (α × Lean.Elab.Term.State)
-- Init.Prelude
Lean.instInhabitedSourceInfo : Inhabited Lean.SourceInfo
-- Lean.Linter.Util
/-- Go upwards through the given `tree` starting from the smallest node that
contains the given `range` and collect all `MacroExpansionInfo`s on the way up.
The result is `some []` if no `MacroExpansionInfo` was found on the way and
`none` if no `InfoTree` node was found that covers the given `range`.

Return the result reversed, s.t. the macro expansion that would be applied to
the original syntax first is the first element of the returned list.  -/
Lean.Linter.collectMacroExpansions? : {m : Type → Type u_1} →
  [Monad m] → Lean.Syntax.Range → Lean.Elab.InfoTree → m (Option (List Lean.Elab.MacroExpansionInfo))
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasurableSet.cylinder : ∀ {ι : Type u_2} {α : ι → Type u_1} [inst : (i : ι) → MeasurableSpace (α i)] (s : Finset ι) {S : Set ((i : ↥s) → α ↑i)},
  MeasurableSet S → MeasurableSet (MeasureTheory.cylinder s S)
-- Mathlib.Data.Set.Card
Set.encard_lt_one : ∀ {α : Type u_1} {s : Set α}, s.encard < 1 ↔ s = ∅
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal
/-- If `F : C ⥤ D` is such that `F.obj X` is terminal for any `X : C`,
then `F` is a terminal object.  -/
CategoryTheory.Functor.isTerminal : {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] →
        {F : CategoryTheory.Functor C D} →
          ((X : C) → CategoryTheory.Limits.IsTerminal (F.obj X)) → CategoryTheory.Limits.IsTerminal F
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.not_beq_one : ∀ (a : BitVec 1), (!a == 1#1) = (a == 0#1)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.coeff_mul_right' : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] {x y : HahnSeries Γ R} {a : Γ} {s : Set Γ} (hs : s.IsPWO),
  y.support ⊆ s → (x * y).coeff a = ∑ ij ∈ Finset.antidiagonal ⋯ hs a, x.coeff ij.1 * y.coeff ij.2
-- Std.Data.ExtDTreeMap.Lemmas
_private.Std.Data.ExtDTreeMap.Lemmas.0.Std.ExtDTreeMap.insertMany_list_mk : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t : Std.DTreeMap α β cmp}
  {l : List ((a : α) × β a)}, (Std.ExtDTreeMap.mk t).insertMany l = Std.ExtDTreeMap.mk (t.insertMany l)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.support_neg : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddGroup (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i}, (-f).support = f.support
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- There is a canonical equivalence between the costructured arrow category with codomain `c` on
the functor `Comma.fst F G : Comma F G ⥤ F` and the comma category over
`Over.forget c ⋙ F : Over c ⥤ T` and `G`.  -/
CategoryTheory.CostructuredArrow.ofCommaFstEquivalence : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor C T) →
              (G : CategoryTheory.Functor D T) →
                (c : C) →
                  CategoryTheory.CostructuredArrow (CategoryTheory.Comma.fst F G) c ≌
                    CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G
-- Mathlib.Topology.GDelta.Basic
IsGδ.biInter : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] {s : Set ι},
  s.Countable →
    ∀ {t : (i : ι) → i ∈ s → Set X}, (∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)) → IsGδ (⋂ i, ⋂ (h : i ∈ s), t i h)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.linearIndependent_completeFamily : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  LinearIndependent ℝ (NumberField.mixedEmbedding.fundamentalCone.completeFamily K)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.mem_range_typein_iff : ∀ {α : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] {o : Ordinal.{u}},
  o ∈ Set.range ⇑(Ordinal.typein r).toRelEmbedding ↔ o < Ordinal.type r
-- Mathlib.Topology.Algebra.GroupWithZero
Homeomorph.coe_mulRight₀ : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : GroupWithZero α] [inst_2 : SeparatelyContinuousMul α] (c : α)
  (hc : c ≠ 0), ⇑(Homeomorph.mulRight₀ c hc) = fun x => x * c
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1_of_measure_eq_top : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)],
  μ s = ⊤ → ∀ (x : G), MeasureTheory.condExpIndL1 hm μ s x = 0
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_succ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (n : ℕ),
  P.extensionProductIter (n + 1) = P.extensionProduct (P.extensionProductIter n)
-- Mathlib.Data.Set.Pairwise.Basic
pairwise_disjoint_on_bool : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α},
  Pairwise (Function.onFun Disjoint fun c => bif c then a else b) ↔ Disjoint a b
-- Mathlib.Algebra.Star.Module
isSelfAdjoint_algebraMap_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A] [inst_3 : StarMul A]
  [inst_4 : Algebra R A] [StarModule R A] {r : R},
  Function.Injective ⇑(algebraMap R A) → (IsSelfAdjoint ((algebraMap R A) r) ↔ IsSelfAdjoint r)
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
AlgebraicGeometry.Scheme.instIsClosedImmersionIrreducibleComponentι : ∀ (X : AlgebraicGeometry.Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X)
  [inst : AlgebraicGeometry.IsNoetherian X], AlgebraicGeometry.IsClosedImmersion (X.irreducibleComponentι Z hZ)
-- Mathlib.Analysis.Calculus.ContDiff.CPolynomial
ContinuousMultilinearMap.contDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F) {n : WithTop ℕ∞}
  {x : (i : ι) → E i}, ContDiffAt 𝕜 n (⇑f) x
-- Mathlib.Topology.Sheaves.Over
/-- Sheaves on the over category of `U` are equivalent to sheaves on `U` as a topological space.  -/
TopologicalSpace.Opens.sheafEquivOver : {X : Type u} →
  [inst : TopologicalSpace X] →
    (U : TopologicalSpace.Opens X) →
      {A : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
          CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A ≌
            CategoryTheory.Sheaf (Opens.grothendieckTopology ↥U) A
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.zero_def : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], 0 = ⟦0⟧
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `NormedAddCommGroup E` instance from a `NormedSpace.Core` on a type
that already has an existing uniform space structure. This requires a proof that the uniformity
induced by the norm is equal to the preexisting uniformity. See note [reducible non-instances].  -/
NormedAddCommGroup.ofCoreReplaceUniformity : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : Norm E] →
            [U : UniformSpace E] → (core : NormedSpace.Core 𝕜 E) → uniformity E = uniformity E → NormedAddCommGroup E
-- Std.Data.TreeSet.Basic
Std.TreeSet.instSDiff : {α : Type u} → {cmp : α → α → Ordering} → SDiff (Std.TreeSet α cmp)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_formPerm_nontrivial : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (l : List α) (hl : 2 ≤ l.length),
  l.Nodup → l.formPerm.toList (l.get ⟨0, ⋯⟩) = l
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCommGroup : {α : Type u_1} → [CommGroup α] → CommGroup (Lex α)
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.rev_map : ∀ {n m : SimplexCategory} (f : n ⟶ m),
  SimplexCategory.rev.map f =
    SimplexCategory.Hom.mk { toFun := fun i => Fin.rev ((CategoryTheory.ConcreteCategory.hom f) i.rev), monotone' := ⋯ }
-- Mathlib.Algebra.Order.GroupWithZero.Basic
le_mul_iff_one_le_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Zero α] {a b : α} [inst_2 : Preorder α] [MulPosMono α]
  [MulPosReflectLE α], 0 < a → (a ≤ b * a ↔ 1 ≤ b)
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C],
  (CategoryTheory.Idempotents.KaroubiKaroubi.equivalence C).functor =
    CategoryTheory.Idempotents.toKaroubi (CategoryTheory.Idempotents.Karoubi C)
-- Mathlib.Data.Finset.Basic
Finset.choose_property : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (l : Finset α) (hp : ∃! a, a ∈ l ∧ p a),
  p (Finset.choose p l hp)
-- Lean.DocString.Extension
Lean.ModuleDoc.mk.injEq : ∀ (doc : String) (declarationRange : Lean.DeclarationRange) (doc_1 : String)
  (declarationRange_1 : Lean.DeclarationRange),
  ({ doc := doc, declarationRange := declarationRange } = { doc := doc_1, declarationRange := declarationRange_1 }) =
    (doc = doc_1 ∧ declarationRange = declarationRange_1)
-- Mathlib.Data.NNReal.Defs
Real.nnabs_coe : ∀ (x : NNReal), Real.nnabs ↑x = x
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_neg : ∀ (a : UInt64), (-a).toUInt16 = -a.toUInt16
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_subset_iff : ∀ {α : Type u_2} [inst : Div α] {s t u : Set α}, s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u
-- Lean.Server.FileWorker.Utils
/-- Diagnostics that persist across document versions (e.g. stale dependency warnings).
Shared across all versions via an `IO.Ref`.
 -/
Lean.Server.FileWorker.DiagnosticsState.stickyDiagsRef : Lean.Server.FileWorker.DiagnosticsState → IO.Ref (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic)
-- Mathlib.Analysis.Complex.Basic
Complex.instDenselyNormedField : DenselyNormedField ℂ
-- Mathlib.Order.Filter.IsBounded
Filter.isCoboundedUnder_le_of_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α},
  (∀ (i : ι), x ≤ f i) → Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) l f
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.isBase_restrict_iff : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  autoParam (X ⊆ M.E) Matroid.isBase_restrict_iff._auto_1 → ((M.restrict X).IsBase I ↔ M.IsBasis I X)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
/-- The module structure on the sections of the sheafification of the underlying
presheaf of abelian groups of a presheaf of modules.  -/
PresheafOfModules.Sheafify.module : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          (X : Cᵒᵖ) → Module ↑(R.obj.obj X) ↑(A.obj.obj X)
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat.comp_apply : ∀ (R : Type u) [inst : Semiring R] {M N K : CategoryTheory.Mat R} (f : M ⟶ N) (g : N ⟶ K) (i : M.obj) (k : K.obj),
  CategoryTheory.CategoryStruct.comp f g i k = ∑ j, f i j * g j k
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.Raw.toList.eq_1 : ∀ {α : Type u} (m : Std.HashSet.Raw α), m.toList = m.inner.keys
-- Mathlib.RingTheory.Multiplicity
emultiplicity_pow_self : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {p : α},
  p ≠ 0 → ¬IsUnit p → ∀ (n : ℕ), emultiplicity p (p ^ n) = ↑n
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_congr : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν], μ = ν → μ.toSignedMeasure = ν.toSignedMeasure
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.cellFrontier_eq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (n : ℕ) (i : ↑(E.I n)),
  Topology.RelCWComplex.cellFrontier n i = Topology.RelCWComplex.cellFrontier n ↑i
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.instReprOfTransCmp : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Repr α] → Repr (Std.ExtTreeSet α cmp)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
/-- `(x, y) ↦ x ^ y` is strictly differentiable at `p : ℝ × ℝ` such that `p.fst < 0`.  -/
Real.hasStrictFDerivAt_rpow_of_neg : ∀ (p : ℝ × ℝ),
  p.1 < 0 →
    HasStrictFDerivAt (fun x => x.1 ^ x.2)
      ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        (p.1 ^ p.2 * Real.log p.1 - Real.exp (Real.log p.1 * p.2) * Real.sin (p.2 * Real.pi) * Real.pi) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      p
-- Mathlib.RingTheory.RingInvo
/-- Every ring involution must be its own inverse  -/
RingInvoClass.involution : ∀ {F : Type u_3} {R : Type u_4} {inst : Semiring R} {inst_1 : EquivLike F R Rᵐᵒᵖ} [self : RingInvoClass F R] (f : F)
  (x : R), MulOpposite.unop (f (MulOpposite.unop (f x))) = x
-- Init.Data.Array.Range
Array.mem_range' : ∀ {s step m n : ℕ}, m ∈ Array.range' s n step ↔ ∃ i < n, m = s + step * i
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
instFactMemSetQuasispectrumOfNat : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] [Nontrivial R]
  (a : A), Fact (0 ∈ quasispectrum R a)
-- Mathlib.Topology.Algebra.Monoid
Submonoid.topologicalClosure_mono : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : SeparatelyContinuousMul M]
  {s t : Submonoid M}, s ≤ t → s.topologicalClosure ≤ t.topologicalClosure
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instCommGroup.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α], Lex.instCommGroup = { toGroup := Lex.instGroup, mul_comm := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.homIso_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {t : CategoryTheory.Limits.Fork f g}
  (ht : CategoryTheory.Limits.IsLimit t) (Z : C)
  (h : { h // CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g }),
  (CategoryTheory.Limits.Fork.IsLimit.homIso ht Z).symm h = ↑(CategoryTheory.Limits.Fork.IsLimit.lift' ht ↑h ⋯)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k fallback : α},
  (Std.DHashMap.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => (f x_2 (Std.DHashMap.Const.get m x_2 ⋯)).isSome).getD fallback
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The boundary of `u : Opens M` is the preimage of the boundary of `M` under the inclusion.  -/
ModelWithCorners.boundary_open : ∀ {𝕜 : 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] {u : TopologicalSpace.Opens M},
  ModelWithCorners.boundary ↥u = Subtype.val ⁻¹' ModelWithCorners.boundary M