mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.Spectrum
StarAlgEquiv.nnnorm_map : ∀ {F : Type u_1} {A : Type u_2} {B : Type u_3} [inst : NonUnitalCStarAlgebra A] [inst_1 : NonUnitalCStarAlgebra B]
  [inst_2 : EquivLike F A B] [NonUnitalAlgEquivClass F ℂ A B] [StarHomClass F A B] (φ : F) (a : A), ‖φ a‖₊ = ‖a‖₊
-- Mathlib.Topology.DiscreteSubset
/-- If `s` is codiscrete within `U`, then `sᶜ ∩ U` has discrete topology.  -/
isDiscrete_of_codiscreteWithin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U s : Set X}, sᶜ ∈ Filter.codiscreteWithin U → IsDiscrete (s ∩ U)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape
CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit : ∀ {J : Type w} [inst : LinearOrder J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasIterationOfShape J C] (j : J),
  Order.IsSuccLimit j → CategoryTheory.Limits.HasColimitsOfShape (↑(Set.Iio j)) C
-- Mathlib.Topology.Algebra.Order.UpperLower
IsUpperSet.interior : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] [HasUpperLowerClosure α] {s : Set α},
  IsUpperSet s → IsUpperSet (interior s)
-- Lean.Util.Trace
_private.Lean.Util.Trace.0.Lean.getResetTraces : {m : Type → Type} → [Monad m] → [Lean.MonadTrace m] → m (Lean.PersistentArray Lean.TraceElem)
-- Mathlib.CategoryTheory.Sites.Descent.IsStack
CategoryTheory.Pseudofunctor.IsStack.toIsPrestack : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C}
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat}
  {J : CategoryTheory.GrothendieckTopology C} [self : F.IsStack J], F.IsPrestack J
-- Lean.Data.KVMap
Lean.DataValue.getBoolEx : Lean.DataValue → Bool
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The additive map forgetting that a bounded continuous
function is bounded. -/
BoundedContinuousFunction.toContinuousMapAddMonoidHom : (α : Type u) →
  (R : Type u_2) →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : AddMonoid R] →
          [inst_3 : BoundedAdd R] → [inst_4 : ContinuousAdd R] → BoundedContinuousFunction α R →+ C(α, R)
-- Mathlib.Data.Finsupp.Notation
/-- Unexpander for the `fun₀ | i => x` notation.  -/
Finsupp.updateUnexpander : Lean.PrettyPrinter.Unexpander
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.type? : LeanSearchClient.SearchResult → Option String
-- Mathlib.Data.PSigma.Order
/-- Dictionary / lexicographic `LinearOrder` for pairs.  -/
PSigma.Lex.linearOrder : {ι : Type u_1} → {α : ι → Type u_2} → [LinearOrder ι] → [(i : ι) → LinearOrder (α i)] → LinearOrder (Σₗ' (i : ι), α i)
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_map : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {β : Type u_2} [inst_2 : Lattice β] [inst_3 : OrderBot β]
  {a : α} {e : α ≃o β} {P : Finpartition a}, (Finpartition.map e P).parts = Finset.map (↑e).toEmbedding P.parts
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instUpwardEnumerable_eq : Int16.instUpwardEnumerable = HasModel.instUpwardEnumerable✝
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `AddSubgroup.top_lowerCentralSeries_one`. -/
AddSubgroup.lowerCentralSeries_one : ∀ {G : Type u_1} [inst : AddGroup G], ⊤.lowerCentralSeries 1 = addCommutator G
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapₗ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapₗ F).app X =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv
-- Aesop.Rule.Name
Aesop.RuleName.mk.injEq : ∀ (name : Lean.Name) (builder : Aesop.BuilderName) (phase : Aesop.PhaseName) (scope : Aesop.ScopeName) (hash : UInt64)
  (name_1 : Lean.Name) (builder_1 : Aesop.BuilderName) (phase_1 : Aesop.PhaseName) (scope_1 : Aesop.ScopeName)
  (hash_1 : UInt64),
  ({ name := name, builder := builder, phase := phase, scope := scope, hash := hash } =
      { name := name_1, builder := builder_1, phase := phase_1, scope := scope_1, hash := hash_1 }) =
    (name = name_1 ∧ builder = builder_1 ∧ phase = phase_1 ∧ scope = scope_1 ∧ hash = hash_1)
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.replacePartialEquiv_eq_self : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y)
  (e' : PartialEquiv X Y) (h : e.toPartialEquiv = e'), e.replacePartialEquiv e' h = e
-- Mathlib.Probability.StrongLaw
/-- The truncation of `Xᵢ` up to `i` satisfies the strong law of large numbers
(with respect to the original expectation) along the sequence
`c^n`, for any `c > 1`. This follows from the version from the truncated expectation, and the
fact that the truncated and the original expectations have the same asymptotic behavior.  -/
ProbabilityTheory.strong_law_aux4 : ∀ {Ω : Type u_1} [inst : MeasureTheory.MeasureSpace Ω] [MeasureTheory.IsProbabilityMeasure MeasureTheory.volume]
  (X : ℕ → Ω → ℝ),
  MeasureTheory.Integrable (X 0) MeasureTheory.volume →
    Pairwise (Function.onFun (fun f g => ProbabilityTheory.IndepFun f g MeasureTheory.volume) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) MeasureTheory.volume MeasureTheory.volume) →
        (∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω) →
          ∀ {c : ℝ},
            1 < c →
              ∀ᵐ (ω : Ω),
                (fun n =>
                    ∑ i ∈ Finset.range ⌊c ^ n⌋₊, ProbabilityTheory.truncation (X i) (↑i) ω -
                      ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[Filter.atTop]
                  fun n => ↑⌊c ^ n⌋₊
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldRev_cons_key : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Raw α β} {acc : List α},
  Std.DHashMap.Raw.Internal.foldRev (fun acc k x => k :: acc) acc l =
    Std.Internal.List.keys (Std.DHashMap.Internal.toListModel l.buckets) ++ acc
-- Mathlib.Topology.Homeomorph.Defs
/-- See Note [custom simps projection]  -/
Homeomorph.Simps.symm_apply : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → X ≃ₜ Y → Y → X
-- Mathlib.Data.List.Duplicate
/-- Property that an element `x : α` of `l : List α` can be found in the list more than once.  -/
List.Duplicate : {α : Type u_1} → α → List α → Prop
-- Lean.Language.Basic
Lean.Language.instInhabitedSnapshotTask : {a : Type} → [Inhabited a] → Inhabited (Lean.Language.SnapshotTask a)
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.sOppSide_affineSpan_faceOpposite_point_left_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w : Fin (n + 1) → R},
  ∑ j, w j = 1 →
    ∀ {i : Fin (n + 1)},
      (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide (s.points i)
          ((Finset.affineCombination R Finset.univ s.points) w) ↔
        w i < 0
-- Mathlib.Topology.MetricSpace.Similarity
/-- A similarity pairwise scales distance. Forward direction of
`similar_iff_exists_pairwise_dist_eq`.  -/
Similar.exists_pairwise_dist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoMetricSpace P₁]
  [inst_1 : PseudoMetricSpace P₂],
  Similar v₁ v₂ → ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ => dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)
-- Mathlib.Analysis.Asymptotics.SuperpolynomialDecay
Asymptotics.SuperpolynomialDecay.const_mul : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {k f : α → β} [inst : TopologicalSpace β] [inst_1 : CommSemiring β]
  [ContinuousMul β],
  Asymptotics.SuperpolynomialDecay l k f → ∀ (c : β), Asymptotics.SuperpolynomialDecay l k fun n => c * f n
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.flip_injective_iff₁ : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {B : V₁ →ₗ[K] V₂ →ₗ[K] K} [FiniteDimensional K V₁],
  Function.Injective ⇑B.flip ↔ Function.Surjective ⇑B
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the smallest key that is
greater than or equal to the given key.
 -/
Std.DTreeMap.getKeyGE : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.FinStronglyMeasurable.neg : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β}
  [inst : TopologicalSpace β] [inst_1 : SubtractionMonoid β] [ContinuousNeg β],
  MeasureTheory.FinStronglyMeasurable f μ → MeasureTheory.FinStronglyMeasurable (-f) μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonResolvableCompletionList : Lean.ToJson Lean.Lsp.ResolvableCompletionList
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.isZero_cycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n : ℤ),
  CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g)) →
    CategoryTheory.Limits.IsZero (X.cycles f g n)
-- Std.Sync.Channel
/-- Receive a value from the channel, returning a task that will resolve once the transmission could be
completed. Note that the task may resolve to `none` if the channel was closed before it could be
completed.
 -/
Std.CloseableChannel.recv : {α : Type} → Std.CloseableChannel α → BaseIO (Task (Option α))
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.symbolNoAntiquot.formatter : String → Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `locallyPathConnectedSpace_iff_isOpen_pathComponentIn`.

---

A space is locally path-connected iff all path components of open subsets are open.  -/
locPathConnectedSpace_iff_isOpen_pathComponentIn : ∀ {X : Type u_4} [inst : TopologicalSpace X],
  LocallyPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn u x)
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.mk.inj : ∀ {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} {functor : CategoryTheory.Functor C D}
  {inverse : CategoryTheory.Functor D C} {unit_eq : CategoryTheory.Functor.id C = functor.comp inverse}
  {counit_eq : inverse.comp functor = CategoryTheory.Functor.id D} {functor_1 : CategoryTheory.Functor C D}
  {inverse_1 : CategoryTheory.Functor D C} {unit_eq_1 : CategoryTheory.Functor.id C = functor_1.comp inverse_1}
  {counit_eq_1 : inverse_1.comp functor_1 = CategoryTheory.Functor.id D},
  { functor := functor, inverse := inverse, unit_eq := unit_eq, counit_eq := counit_eq } =
      { functor := functor_1, inverse := inverse_1, unit_eq := unit_eq_1, counit_eq := counit_eq_1 } →
    functor = functor_1 ∧ inverse = inverse_1
-- Mathlib.Order.SuccPred.Basic
Order.succ_ne_succ_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α} [NoMaxOrder α],
  Order.succ a ≠ Order.succ b ↔ a ≠ b
-- Lean.Meta.HaveTelescope
/-- `modified := false` iff `expr` is structurally equal to the input expression.
When false, `proof` is `Eq.refl`.
 -/
_private.Lean.Meta.HaveTelescope.0.Lean.Meta.SimpHaveResult.modified : Lean.Meta.SimpHaveResult✝ → Bool
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
/-- A convenience constructor for `HasAffineProperty P (affineAnd Q)`. The `IsAffineHom` is bundled,
since this goes well with defining morphism properties via `extends IsAffineHom`.  -/
AlgebraicGeometry.HasAffineProperty.affineAnd_iff : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => Q) →
        (AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) ↔
          ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
            P f ↔
              AlgebraicGeometry.IsAffineHom f ∧
                ∀ (U : Y.Opens),
                  AlgebraicGeometry.IsAffineOpen U → Q (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)))
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_mono : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s t : Set M},
  s ⊆ t → Submodule.span R s ≤ Submodule.span R t
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.instAddActionQuotient.eq_1 : ∀ {S : Type u_2} (M : Type u_3) [inst : AddMonoid S] [inst_1 : AddAction S M] (c : VAddCon S M),
  VAddCon.instAddActionQuotient M c = { toVAdd := VAddCon.instVAddQuotient M c, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.subtype_eq_val : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] (p : SubAddAction R M), ⇑p.subtype = Subtype.val
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Limits.cospanIsoMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C}
  (z z_1 : F.obj CategoryTheory.Limits.WalkingCospan.one ≅ G.obj CategoryTheory.Limits.WalkingCospan.one)
  (e_z : z = z_1)
  (l l_1 : F.obj CategoryTheory.Limits.WalkingCospan.left ≅ G.obj CategoryTheory.Limits.WalkingCospan.left)
  (e_l : l = l_1)
  (r r_1 : F.obj CategoryTheory.Limits.WalkingCospan.right ≅ G.obj CategoryTheory.Limits.WalkingCospan.right)
  (e_r : r = r_1)
  (hl :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl) z.hom =
      CategoryTheory.CategoryStruct.comp l.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inl))
  (hr :
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) z.hom =
      CategoryTheory.CategoryStruct.comp r.hom (G.map CategoryTheory.Limits.WalkingCospan.Hom.inr)),
  CategoryTheory.Limits.cospanIsoMk z l r hl hr = CategoryTheory.Limits.cospanIsoMk z_1 l_1 r_1 ⋯ ⋯
-- Mathlib.Combinatorics.Graph.Basic
Graph.edgeSet_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.edgeSet = ∅ ↔ G = Graph.noEdge G.vertexSet β
-- Mathlib.LinearAlgebra.Finsupp.LSum
LinearMap.CompatibleSMul.finsupp_dom : ∀ (R : Type u_9) (S : Type u_10) (M : Type u_11) (N : Type u_12) (ι : Type u_13) [inst : Semiring S]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : Module S M] [inst_4 : Module S N]
  [inst_5 : SMulZeroClass R M] [inst_6 : DistribSMul R N] [LinearMap.CompatibleSMul M N R S],
  LinearMap.CompatibleSMul (ι →₀ M) N R S
-- Mathlib.Topology.Order.NhdsSet
Ico_mem_nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c d : α},
  a < b → c < d → Set.Ico a d ∈ nhdsSet (Set.Icc b c)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.leftHomologyData'_H_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n m p : ℤ) (hm : n + 1 = m) (hp : m + 1 = p),
  ↑(CochainComplex.HomComplex.leftHomologyData' K L n m p hm hp).H = CochainComplex.HomComplex.CohomologyClass K L m
-- Batteries.Data.List.Perm
List.Subperm.erase : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α] (a : α),
  l₁.Subperm l₂ → (l₁.erase a).Subperm (l₂.erase a)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_lt_top_of_isCompact : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α] {s : Set α},
  μ s ≠ ⊤ → IsCompact s → ∀ {f : α → NNReal}, Continuous f → ∫⁻ (x : α) in s, ↑(f x) ∂μ < ⊤
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_one : ∀ {α : Type u_1} [inst : One α], OrderDual.ofDual 1 = 1
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.modify : {α : Type u} →
  [BEq α] →
    {β : Type v} →
      [Hashable α] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → (β → β) → Std.DHashMap.Internal.Raw₀ α fun x => β
-- Mathlib.Order.Interval.Set.Pi
Set.piecewise_mem_Icc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] {s : Set ι} [inst_1 : (j : ι) → Decidable (j ∈ s)]
  {f₁ f₂ g₁ g₂ : (i : ι) → α i},
  (∀ i ∈ s, f₁ i ∈ Set.Icc (g₁ i) (g₂ i)) → (∀ i ∉ s, f₂ i ∈ Set.Icc (g₁ i) (g₂ i)) → s.piecewise f₁ f₂ ∈ Set.Icc g₁ g₂
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Ioc a b` and antitone on `Ici b`, then the maximum of `f` on `Ioi a` is
attained at `b`.  -/
isMaxOn_Ioi_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  MonotoneOn f (Set.Ioc a b) → AntitoneOn f (Set.Ici b) → IsMaxOn f (Set.Ioi a) b
-- Mathlib.FieldTheory.SeparableClosure
le_restrictScalars_separableClosure : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : IntermediateField F E),
  L ≤ IntermediateField.restrictScalars F (separableClosure (↥L) E)
-- Mathlib.Logic.Equiv.Defs
Equiv.plift_symm_apply : ∀ {α : Sort u}, ⇑Equiv.plift.symm = PLift.up
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_int8ToBitVec : ∀ (x : Int8), ISize.ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize
-- Std.Time.DateTime.WallTime
Std.Time.instDecidableLtWallTime : {x y : Std.Time.WallTime} → Decidable (x < y)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.eventually : ∀ {ι : Type u_1} (R : ι → Type u_2) (A : (i : ι) → Set (R i)) {𝓕 : Filter ι}
  (x : RestrictedProduct (fun i => R i) (fun i => A i) 𝓕), ∀ᶠ (i : ι) in 𝓕, x i ∈ A i
-- Mathlib.Geometry.Manifold.Immersion
/-- If `f` is an immersion at `x`, its domain chart's target `(h.domChart.extend I).target`
is mapped to its codomain chart's target `(h.domChart.extend J).target`:
see `map_target_subset_target` for a version stated using images.  -/
Manifold.IsImmersionAtOfComplement.target_subset_preimage_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAtOfComplement F I J n f x),
  (h.domChart.extend I).target ⊆ (⇑h.equiv ∘ fun x => (x, 0)) ⁻¹' (h.codChart.extend J).target
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.comp_assoc : ∀ {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : Group E] [inst_1 : Group F] [inst_2 : Group G]
  (p : GroupSeminorm E) (g : F →* E) (f : G →* F), p.comp (g.comp f) = (p.comp g).comp f
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- The `rightInv` direction of the equivalence  -/
YoungDiagram.rowLens_ofRowLens_eq_self : ∀ {w : List ℕ} {hw : w.SortedGE}, (∀ x ∈ w, 0 < x) → (YoungDiagram.ofRowLens w hw).rowLens = w
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpParams.mk : Lean.Lsp.TextDocumentPositionParams →
  Lean.Lsp.WorkDoneProgressParams → Option Lean.Lsp.SignatureHelpContext → Lean.Lsp.SignatureHelpParams
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_congr_ae : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  X =ᵐ[μ] Y → ProbabilityTheory.condVar m X μ =ᵐ[μ] ProbabilityTheory.condVar m Y μ
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.injective : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N), Function.Injective ⇑e
-- Mathlib.InformationTheory.Hamming
Hamming.instNormedAddCommGroupOfAddCommGroup : {ι : Type u_2} →
  {β : ι → Type u_3} →
    [Fintype ι] → [(i : ι) → DecidableEq (β i)] → [(i : ι) → AddCommGroup (β i)] → NormedAddCommGroup (Hamming β)
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.Cache.IsExtensionBy.mk : ∀ {aig : Std.Sat.AIG ℕ} {cnf1 cnf2 : Std.Sat.CNF ℕ} {cache1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf1}
  {cache2 : Std.Sat.AIG.toCNF.Cache✝ aig cnf2} {new : ℕ} {hnew : new < aig.decls.size},
  (∀ (idx : ℕ) (hidx : idx < aig.decls.size),
      (Std.Sat.AIG.toCNF.Cache.marks✝ cache1)[idx] = true → (Std.Sat.AIG.toCNF.Cache.marks✝ cache2)[idx] = true) →
    (Std.Sat.AIG.toCNF.Cache.marks✝ cache2)[new] = true → Std.Sat.AIG.toCNF.Cache.IsExtensionBy✝ cache1 cache2 new hnew
-- Mathlib.Data.Set.Basic
Set.mem_inter : ∀ {α : Type u} {x : α} {a b : Set α}, x ∈ a → x ∈ b → x ∈ a ∩ b
-- Init.Data.List.Attach
_private.Init.Data.List.Attach.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.Data.Finset.Density
Finset.dens_map_equiv : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] {s : Finset α} [inst_1 : Fintype β] (e : α ≃ β),
  (Finset.map e.toEmbedding s).dens = s.dens
-- Mathlib.Order.Filter.Pi
Filter.Eventually.eval_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {p : (i : ι) → α i → Prop} {i : ι},
  (∀ᶠ (x : α i) in f i, p i x) → ∀ᶠ (x : (i : ι) → α i) in Filter.pi f, p i (x i)
-- Mathlib.Topology.Separation.GDelta
T6Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X] [toT0Space : T0Space X] [toPerfectlyNormalSpace : PerfectlyNormalSpace X],
  T6Space X
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.equiv_symm_apply : ∀ {R : Type u_1} (self : PreQuasiregular R), PreQuasiregular.equiv.symm self = self.val
-- Mathlib.Analysis.Normed.Group.Continuity
/-- Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real
function `a` which tends to `0`, then `f` tends to `1` (neutral element of `SeminormedGroup`).
In this pair of lemmas (`squeeze_one_norm'` and `squeeze_one_norm`), following a convention of
similar lemmas in `Topology.MetricSpace.Basic` and `Topology.Algebra.Order`, the `'` version is
phrased using "eventually" and the non-`'` version is phrased absolutely.  -/
squeeze_one_norm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] {f : α → E} {a : α → ℝ} {t₀ : Filter α},
  (∀ᶠ (n : α) in t₀, ‖f n‖ ≤ a n) → Filter.Tendsto a t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 1)
-- Mathlib.Topology.Separation.Regular
lift'_nhds_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] (x : X), (nhds x).lift' closure = nhds x
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.restrictScalars_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  (S : Set E),
  IntermediateField.restrictScalars F (IntermediateField.adjoin (↥K) S) = IntermediateField.adjoin F (↑K ∪ S)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.coe_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N ≃ₗ[R] P), ↑(LinearEquiv.rTensor M f) = LinearMap.rTensor M ↑f
-- Mathlib.LinearAlgebra.Eigenspace.Triangularizable
Module.End.exists_hasEigenvalue_of_genEigenspace_eq_top : ∀ {R : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  {f : Module.End R M} (k : ℕ∞), ⨆ μ, (f.genEigenspace μ) k = ⊤ → ∃ μ, f.HasEigenvalue μ