mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
ContinuousLinearMap.coe_mkOfIsCompactOperator : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : NontriviallyNormedField 𝕜₂]
  {σ₁₂ : 𝕜₁ →+* 𝕜₂} [inst_2 : RingHomIsometric σ₁₂] {M₁ : Type u_3} {M₂ : Type u_4} [inst_3 : TopologicalSpace M₁]
  [inst_4 : AddCommGroup M₁] [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommGroup M₂] [inst_7 : Module 𝕜₁ M₁]
  [inst_8 : Module 𝕜₂ M₂] [inst_9 : IsTopologicalAddGroup M₁] [inst_10 : ContinuousConstSMul 𝕜₁ M₁]
  [inst_11 : IsTopologicalAddGroup M₂] [inst_12 : ContinuousSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂}
  (hf : IsCompactOperator ⇑f), ⇑(ContinuousLinearMap.mkOfIsCompactOperator hf) = ⇑f
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.mem_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {S : AddSubsemigroup N} {f : M →ₙ+ N} {x : M},
  x ∈ AddSubsemigroup.comap f S ↔ f x ∈ S
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.spanCarrier.below : {K : Type u_1} →
  {V : Type u_2} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          {S : Set (Projectivization K V)} →
            {motive : (a : Projectivization K V) → Projectivization.Subspace.spanCarrier S a → Prop} →
              {a : Projectivization K V} → Projectivization.Subspace.spanCarrier S a → Prop
-- Mathlib.Algebra.Group.End
/-- Group conjugation, `MulAut.conj g h = g * h * g⁻¹`, as a monoid homomorphism
mapping multiplication in `G` into multiplication in the automorphism group `MulAut G`.
See also the type `ConjAct G` for any group `G`, which has a `MulAction (ConjAct G) G` instance
where `conj G` acts on `G` by conjugation.  -/
MulAut.conj : {G : Type u_3} → [inst : Group G] → G →* MulAut G
-- Mathlib.Analysis.InnerProductSpace.l2Space
lp.inner_single_left : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {G : ι → Type u_4} [inst_1 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_2 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_3 : DecidableEq ι] (i : ι) (a : G i) (f : ↥(lp G 2)),
  inner 𝕜 (lp.single 2 i a) f = inner 𝕜 a (↑f i)
-- Batteries.Data.List.Lemmas
List.ge_of_mem_idxsOf : ∀ {α : Type u_1} {xs : List α} {x : α} {s : ℕ} [inst : BEq α], ∀ y ∈ List.idxsOf x xs s, s ≤ y
-- Mathlib.Tactic.CongrExclamation
/-- A version of `Lean.MVarId.congrImplies?` that uses `implies_congr'`
instead of `implies_congr`.  -/
Lean.MVarId.congrImplies?' : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.le_of_blt_false : ∀ {a b : ℕ}, a.blt b = false → b ≤ a
-- Mathlib.Topology.Category.Profinite.Product
/-- The morphism part of the functor `indexFunctor : (Finset ι)ᵒᵖ ⥤ Profinite`.  -/
Profinite.IndexFunctor.map : {ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      (C : Set ((i : ι) → X i)) →
        {J K : ι → Prop} →
          (∀ (i : ι), J i → K i) → C(↑(Profinite.IndexFunctor.obj C K), ↑(Profinite.IndexFunctor.obj C J))
-- Mathlib.RingTheory.RamificationInertia.Ramification
Ideal.IsDedekindDomain.ramificationIdx_eq_factors_count : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [inst_3 : IsDedekindDomain S] [q.LiesOver p],
  Ideal.map (algebraMap R S) p ≠ ⊥ →
    q.ramificationIdx R = Multiset.count q (UniqueFactorizationMonoid.factors (Ideal.map (algebraMap R S) p))
-- Mathlib.Algebra.Algebra.Spectrum.Basic
AlgHom.spectrum_apply_subset : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : Ring B] [inst_4 : Algebra R B] [inst_5 : FunLike F A B] [AlgHomClass F R A B] (φ : F)
  (a : A), spectrum R (φ a) ⊆ spectrum R a
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_one_add' : ∀ {x y : ℝ}, 0 ≤ x → 1 + y ≠ 0 → x ^ (1 + y) = x * x ^ y
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pos.revSkip?_prop_eq_revSkip?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  pos.revSkip? p = pos.revSkip? fun x => decide (p x)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.prod_sub_prod_comm : ∀ {α : Type u_2} {β : Type u_3} [inst : Sub α] [inst_1 : Sub β] (s₁ s₂ : Set α) (t₁ t₂ : Set β),
  s₁ ×ˢ t₁ - s₂ ×ˢ t₂ = (s₁ - s₂) ×ˢ (t₁ - t₂)
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOver'_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] (x : 𝒰.I₀),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOver' S 𝒰 f).f x =
    CategoryTheory.Over.Hom.left
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Hom.asOver (𝒰.f x) S)
        (AlgebraicGeometry.Scheme.Hom.asOver f S))
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.Hom.ext_iff : ∀ {A B : CommGrpCat} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂_P : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular] {ι : Type w}
  (D : ι → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ)
  (hι : HasCardinalLT ι κ) {m : J} (u : (i : ι) → (D i).top ⟶ m) (a : J),
  (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.D₂ D hι u).P a = ((∃ a_1, (D a_1).P a) ∨ m = a)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ofPoly : Int.Internal.Linear.Poly → Lean.Expr
-- Mathlib.Algebra.GCDMonoid.Basic
GCDMonoid.mk : {α : Type u_2} →
  [inst : CommMonoidWithZero α] →
    [toIsCancelMulZero : IsCancelMulZero α] →
      (gcd lcm : α → α → α) →
        (∀ (a b : α), gcd a b ∣ a) →
          (∀ (a b : α), gcd a b ∣ b) →
            (∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b) →
              (∀ (a b : α), Associated (gcd a b * lcm a b) (a * b)) →
                (∀ (a : α), lcm 0 a = 0) → (∀ (a : α), lcm a 0 = 0) → GCDMonoid α
-- Mathlib.Algebra.Homology.Factorizations.Basic
CochainComplex.instIsStableUnderRetractsIntDegreewiseEpiWithInjectiveKernel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C],
  CochainComplex.degreewiseEpiWithInjectiveKernel.IsStableUnderRetracts
-- Mathlib.Algebra.Group.Hom.Defs
map_add_eq_zero : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : AddZero M] [inst_1 : AddZero N] [inst_2 : FunLike F M N]
  [AddMonoidHomClass F M N] (f : F) {a b : M}, a + b = 0 → f a + f b = 0
-- Mathlib.Data.Nat.Find
Nat.findGreatest_succ : ∀ {P : ℕ → Prop} [inst : DecidablePred P] (n : ℕ),
  Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else Nat.findGreatest P n
-- Init.Data.UInt.Lemmas
UInt32.zero_add : ∀ (a : UInt32), 0 + a = a
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_le_restrict_union : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] (v w : MeasureTheory.VectorMeasure α M)
  {i j : Set α},
  MeasurableSet i →
    v.restrict i ≤ w.restrict i →
      MeasurableSet j → v.restrict j ≤ w.restrict j → v.restrict (i ∪ j) ≤ w.restrict (i ∪ j)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.ofVectorSpace_apply_self : ∀ (K : Type u_3) (V : Type u_4) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (x : ↑(Module.Basis.ofVectorSpaceIndex K V)), (Module.Basis.ofVectorSpace K V) x = ↑x
-- Init.Core
SDiff.mk : {α : Type u} → (α → α → α) → SDiff α
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Turn an element of a type `F` satisfying `NonUnitalRingHomClass F α β` into an actual
`NonUnitalRingHom`. This is declared as the default coercion from `F` to `α →ₙ+* β`.  -/
NonUnitalRingHomClass.toNonUnitalRingHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : NonUnitalNonAssocSemiring α] →
        [inst_1 : NonUnitalNonAssocSemiring β] → [inst_2 : FunLike F α β] → [NonUnitalRingHomClass F α β] → F → α →ₙ+* β
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
mem_integralClosure_iff_mem_fg : ∀ (R : Type u_1) (A : Type u_2) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {r : A},
  r ∈ integralClosure R A ↔ ∃ M, (Subalgebra.toSubmodule M).FG ∧ r ∈ M
-- Batteries.Control.Monad
/-- **Alias** of `map_inj_right`. -/
LawfulMonad.map_inj_right : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → β},
  (∀ {x y : α}, f x = f y → x = y) → ∀ {x y : m α}, f <$> x = f <$> y ↔ x = y
-- Std.Http.Data.URI.Encoding
Std.Http.URI.instBEqEncodedQueryString : {r : UInt8 → Bool} → BEq (Std.Http.URI.EncodedQueryString r)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_le_measureReal_union_right : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_le_measureReal_union_right._auto_1 → μ.real t ≤ μ.real (s ∪ t)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getD_erase_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {k : α} {fallback : β}, Std.DHashMap.Internal.Raw₀.Const.getD (m.erase k) k fallback = fallback
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.contains_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.contains k = t₂.contains k
-- Lean.Parser.Types
Lean.Parser.ParserContextCore.mk.injEq : ∀ (toInputContext : Lean.Parser.InputContext) (toParserModuleContext : Lean.Parser.ParserModuleContext)
  (toCacheableParserContext : Lean.Parser.CacheableParserContext) (tokens : Lean.Parser.TokenTable)
  (toInputContext_1 : Lean.Parser.InputContext) (toParserModuleContext_1 : Lean.Parser.ParserModuleContext)
  (toCacheableParserContext_1 : Lean.Parser.CacheableParserContext) (tokens_1 : Lean.Parser.TokenTable),
  ({ toInputContext := toInputContext, toParserModuleContext := toParserModuleContext,
        toCacheableParserContext := toCacheableParserContext, tokens := tokens } =
      { toInputContext := toInputContext_1, toParserModuleContext := toParserModuleContext_1,
        toCacheableParserContext := toCacheableParserContext_1, tokens := tokens_1 }) =
    (toInputContext = toInputContext_1 ∧
      toParserModuleContext = toParserModuleContext_1 ∧
        toCacheableParserContext = toCacheableParserContext_1 ∧ tokens = tokens_1)
-- Init.Data.SInt.Lemmas
Int32.toInt8_mul : ∀ (a b : Int32), (a * b).toInt8 = a.toInt8 * b.toInt8
-- Lean.LibrarySuggestions.SymbolFrequency
/-- Collect the frequencies for constants occurring in declarations defined in the current module,
skipping instance arguments and proofs.
 -/
Lean.LibrarySuggestions.localSymbolFrequencyMap : Lean.MetaM (Lean.NameMap ℕ)
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.mem_sdiff_shiftr_find : ∀ {X : Type u_1} [inst : TopologicalSpace X] (K : CompactExhaustion X) (x : X),
  x ∈ K.shiftr (K.find x + 1) \ K.shiftr (K.find x)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- `SimplexCategoryGenRel.σ i` is the `i`-th degeneracy map `.mk (n + 1) ⟶ .mk n`.  -/
SimplexCategoryGenRel.σ : {n : ℕ} → Fin (n + 1) → (SimplexCategoryGenRel.mk (n + 1) ⟶ SimplexCategoryGenRel.mk n)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instIsIsoHomHomMon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.Grp C} {f : G ⟶ H} [CategoryTheory.IsIso f], CategoryTheory.IsIso f.hom.hom
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.Hom.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → CategoryTheory.WithTerminal C → Sort u_2) (X Y : C)
  (h_1 : (X Y : C) → motive (CategoryTheory.WithTerminal.of X) (CategoryTheory.WithTerminal.of Y))
  (h_2 : (a : C) → motive CategoryTheory.WithTerminal.star (CategoryTheory.WithTerminal.of a))
  (h_3 : (x : CategoryTheory.WithTerminal C) → motive x CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of X, CategoryTheory.WithTerminal.of Y with
    | CategoryTheory.WithTerminal.of X, CategoryTheory.WithTerminal.of Y => h_1 X Y
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of a => h_2 a
    | x, CategoryTheory.WithTerminal.star => h_3 x) =
    h_1 X Y
-- Init.Tactics
/-- A simp args list is a list of `simpArg`. This is the main argument to `simp`.  -/
Lean.Parser.Tactic.simpArgs : Lean.ParserDescr
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : ℝ≥0 → ℝ≥0` is continuous on `s` and `a : X → A` is continuous and `a x` is nonnegative
for all `x` and `s` is a common neighborhood of the spectra of `a x` for all `x`, then
`fun x ↦ cfc f (a x)` is continuous.

This is weaker than `Continuous.cfc_nnreal` since it requires `f` to be continuous on a
*neighborhood* of the spectra, but in practice it is often easier to apply because `s` is not
required to be compact, nor does it require an indexed family of compact sets. This is proven using
`Continuous.cfc_nnreal` and `upperHemicontinuous_spectrum_nnreal` to produce the necessary family
of compact sets.  -/
Continuous.cfc_nnreal_of_mem_nhdsSet : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [CompleteSpace A] [inst_11 : TopologicalSpace X] {s : Set NNReal} (f : NNReal → NNReal) {a : X → A},
  s ∈ nhdsSet (⋃ x, spectrum NNReal (a x)) →
    Continuous a →
      autoParam (∀ (x : X), 0 ≤ a x) Continuous.cfc_nnreal_of_mem_nhdsSet._auto_1 →
        autoParam (ContinuousOn f s) Continuous.cfc_nnreal_of_mem_nhdsSet._auto_3 → Continuous fun x => cfc f (a x)
-- Mathlib.Logic.Equiv.Fin.Basic
finSumNatEquiv_symm_apply_add_left : ∀ {n : ℕ} (i : ℕ), (finSumNatEquiv n).symm (i + n) = Sum.inr i
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATCheckerSound.0.Std.Tactic.BVDecide.LRAT.Internal.go_sound : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (proof : Array Std.Tactic.BVDecide.LRAT.IntAction)
  (idx : ℕ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
      Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go f proof idx =
          Std.Tactic.BVDecide.LRAT.Internal.Result.success →
        Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.instFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.WeaklyEtale g],
  AlgebraicGeometry.WeaklyEtale (CategoryTheory.Limits.pullback.fst f g)
-- Lean.Server.References
/-- Range of the parent declaration.  -/
Lean.Server.References.ParentDecl.range : Lean.Server.References.ParentDecl → Lean.Lsp.Range
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.mem_fundamentalInterior : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {s : Set α} {x : α},
  x ∈ MeasureTheory.fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ.sizeOf_spec : ∀ {n : Q(ℕ)} (n' : Q(ℕ)) (pf : «$n» =Q «$n'».succ),
  sizeOf (Mathlib.Meta.Nat.UnifyZeroOrSuccResult.succ n' pf) = 1 + sizeOf n' + sizeOf pf
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isBot.injEq : ∀ (idx idx_1 : ℕ),
  (Mathlib.Tactic.Order.AtomicFact.isBot idx = Mathlib.Tactic.Order.AtomicFact.isBot idx_1) = (idx = idx_1)
-- Lean.DocString.Types
Lean.Doc.instOrdMathMode : Ord Lean.Doc.MathMode
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_mod_4294967296 : ∀ (n : UInt32), n.toUInt64 % 4294967296 = n.toUInt64
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSubtractionMonoid.eq_1 : ∀ {α : Type u_1} {l : Filter α} {G : Type u_6} [inst : SubtractionMonoid G],
  Filter.Germ.instSubtractionMonoid =
    { toSubNegMonoid := Filter.Germ.subNegMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearMap.isBigOWith_id : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F)
  (l : Filter E), Asymptotics.IsBigOWith ‖f‖ l ⇑f fun x => x
-- Lean.Data.KVMap
Lean.instInhabitedKVMap.default : Lean.KVMap
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.HasMapBifunctor.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  (K₁ K₁_1 : CochainComplex C₁ ℤ),
  K₁ = K₁_1 →
    ∀ (K₂ K₂_1 : CochainComplex C₂ ℤ),
      K₂ = K₂_1 →
        ∀ [inst_5 : CategoryTheory.Preadditive D] (F F_1 : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
          (e_F : F = F_1) [inst_6 : F.PreservesZeroMorphisms] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms],
          K₁.HasMapBifunctor K₂ F = K₁_1.HasMapBifunctor K₂_1 F_1
-- Mathlib.Data.Finite.Defs
instFiniteULift : ∀ {α : Type v} [Finite α], Finite (ULift.{u, v} α)
-- Mathlib.Logic.Equiv.Set
Equiv.subset_symm_image : ∀ {α : Type u_3} {β : Type u_4} (e : α ≃ β) (s : Set α) (t : Set β), s ⊆ ⇑e.symm '' t ↔ ⇑e '' s ⊆ t
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.hasLeftExtension_iff_postcomp₁ : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  {G : CategoryTheory.Functor D D'} [G.IsEquivalence] (e : L.comp G ≅ L') (F : CategoryTheory.Functor C H),
  L'.HasLeftKanExtension F ↔ L.HasLeftKanExtension F
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmod_congr_of_sub_mem_max_ideal : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (m n : ℕ),
  x - ↑m ∈ IsLocalRing.maximalIdeal ℤ_[p] → x - ↑n ∈ IsLocalRing.maximalIdeal ℤ_[p] → ↑m = ↑n
-- Mathlib.Logic.Equiv.Prod
/-- `PProd α β` is equivalent to `PLift α × PLift β`  -/
Equiv.pprodEquivProdPLift : {α : Sort u_1} → {β : Sort u_4} → α ×' β ≃ PLift α × PLift β
-- Mathlib.Analysis.Normed.Field.Basic
NormedDivisionRing.toDivisionRing : {α : Type u_5} → [self : NormedDivisionRing α] → DivisionRing α
-- Batteries.Classes.Order
/-- `cmp x y ≠ .gt` holds iff `x ≤ y` is true.  -/
Std.LawfulLECmp.isLE_iff_le : ∀ {α : Type u_1} {inst : LE α} {cmp : α → α → Ordering} [self : Std.LawfulLECmp cmp] {x y : α},
  (cmp x y).isLE = true ↔ x ≤ y
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.enorm_toLp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E} (hf : MeasureTheory.MemLp f p μ),
  ‖MeasureTheory.MemLp.toLp f hf‖ₑ = MeasureTheory.eLpNorm f p μ
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
lipschitzWith_thickenedIndicator : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ : ℝ} (δ_pos : 0 < δ) (E : Set α),
  LipschitzWith δ.toNNReal⁻¹ ⇑(thickenedIndicator δ_pos E)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.apply₂ : ∀ {α : Type u_2} {γ : Type u_4} {β : α → Type u_6} [inst : (x : α) → OmegaCompletePartialOrder (β x)]
  [inst_1 : OmegaCompletePartialOrder γ] {f : γ → (x : α) → β x},
  OmegaCompletePartialOrder.ωScottContinuous f → ∀ (a : α), OmegaCompletePartialOrder.ωScottContinuous fun x => f x a
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.diam_image : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (s : Set E), Metric.diam (⇑e '' s) = Metric.diam s
-- Mathlib.Algebra.Group.Defs
mul_inv_cancel : ∀ {G : Type u_1} [inst : Group G] (a : G), a * a⁻¹ = 1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.toArray_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β},
  (Std.DHashMap.Const.toList m).toArray = Std.DHashMap.Const.toArray m
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  {x : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v},
  x ∉ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v ↔ 1 < Valued.v x
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesWithinAt.unshift : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → E →L[𝕜] F}
  {pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {s : Set E} {x : E} {z : F},
  HasFPowerSeriesWithinAt f pf s x → HasFPowerSeriesWithinAt (fun y => z + (f y) (y - x)) (pf.unshift z) s x
-- Lean.Server.Requests
Lean.Server.RequestM.run : {α : Type} → Lean.Server.RequestM α → Lean.Server.RequestContext → EIO Lean.Server.RequestError α
-- Mathlib.Logic.Small.Defs
Shrink.congr_simp : ∀ (α α_1 : Type v) (e_α : α = α_1) [inst : Small.{w, v} α], Shrink.{w, v} α = Shrink.{w, v} α_1
-- Mathlib.Data.List.Shortlex
_private.Mathlib.Data.List.Shortlex.0.Acc.shortlex : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} {b : List α},
  Acc r a →
    Acc (List.Shortlex r) b →
      (∀ (s : List α), s.length < (a :: b).length → Acc (List.Shortlex r) s) → Acc (List.Shortlex r) (a :: b)
-- Mathlib.Data.Finmap
Finmap.mem_def : ∀ {α : Type u} {β : α → Type v} {a : α} {s : Finmap β}, a ∈ s ↔ a ∈ s.entries.keys
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsStableUnderComposition.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderComposition] [Q.IsStableUnderComposition], (P ⊓ Q).IsStableUnderComposition
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- The kernel of `zpowersHom G g` is equal to the subgroup generated by `orderOf g`.  -/
zpowersHom_ker_eq : ∀ {G : Type u_2} [inst : Group G] (g : G), ((zpowersHom G) g).ker = Subgroup.zpowers (Multiplicative.ofAdd ↑(orderOf g))
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₄_of_isCharTwoJEqZeroNF_of_char_two : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF] [CharP R 2], W.b₄ = 0
-- Mathlib.Data.Seq.Basic
Stream'.Seq.take_drop : ∀ {α : Type u} {s : Stream'.Seq α} {n m : ℕ}, List.drop m (Stream'.Seq.take n s) = Stream'.Seq.take (n - m) (s.drop m)