mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_unique : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a b : A},
  b * b = a → autoParam (0 ≤ b) CFC.sqrt_unique._auto_1 → CFC.sqrt a = b
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isRadical_bot_iff : ∀ {R : Type u} [inst : CommSemiring R], ⊥.IsRadical ↔ IsReduced R
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabImage.alt : Lean.Doc.ElabImage✝ → String
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.arrows_eq_bot_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {S : CategoryTheory.Sieve X}, S.arrows = ⊥ ↔ S = ⊥
-- Mathlib.SetTheory.Lists
Lists'.nil : {α : Type u} → Lists' α true
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- **Alias** of the reverse direction of `Matroid.IsBasis.finite_iff_isRkFinite`. -/
Matroid.IsBasis.finite_of_isRkFinite : ∀ {α : Type u_1} {M : Matroid α} {X I : Set α}, M.IsBasis I X → M.IsRkFinite X → I.Finite
-- Mathlib.RingTheory.TensorProduct.Quotient
/-- (Implementation): Use `Algebra.TensorProduct.quotIdealMapEquivTensorQuot` instead.  -/
Algebra.TensorProduct.quotIdealMapEquivTensorQuotAux : {A : Type u_1} →
  (B : Type u_2) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] → (I : Ideal A) → (B ⧸ Ideal.map (algebraMap A B) I) ≃ₗ[B] TensorProduct A B (A ⧸ I)
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.card_nsmul_le_sum : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] [AddLeftMono M] (l : List M) (n : M),
  (∀ x ∈ l, n ≤ x) → l.length • n ≤ l.sum
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.d_pOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.d i j) (K.pOpcycles j) = 0
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instExistsMulOfLE : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Mul β] [inst_1 : LE β] [ExistsMulOfLE β],
  ExistsMulOfLE (l.Germ β)
-- Mathlib.Order.CompleteLattice.Basic
/-- Introduction rule to prove that `b` is the infimum of `s`: it suffices to check that `b`
is smaller than all elements of `s`, and that this is not the case of any `w > b`.
See `csInf_eq_of_forall_ge_of_forall_gt_exists_lt` for a version in conditionally complete
lattices.  -/
sInf_eq_of_forall_ge_of_forall_gt_exists_lt : ∀ {α : Type u_1} [inst : CompleteLattice α] {s : Set α} {b : α},
  (∀ a ∈ s, b ≤ a) → (∀ (w : α), b < w → ∃ a ∈ s, a < w) → sInf s = b
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_of_lt_one_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Monoid α] [inst_1 : Zero β] [inst_2 : MulAction α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosStrictMono α β], 0 < b → a < 1 → a • b < b
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.toList_flatMapAfterM : ∀ {α α₂ β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α m β] [inst_5 : Std.Iterator α₂ m γ] [Std.Iterators.Finite α m]
  [Std.Iterators.Finite α₂ m] {f : β → m (Std.IterM m γ)} {it₁ : Std.IterM m β} {it₂ : Option (Std.IterM m γ)},
  (Std.IterM.flatMapAfterM f it₁ it₂).toList =
    match it₂ with
    | none =>
      List.flatten <$>
        (Std.IterM.mapM
            (fun b => do
              let __do_lift ← f b
              __do_lift.toList)
            it₁).toList
    | some it₂ => do
      let __do_lift ← it₂.toList
      let __do_lift_1 ←
        List.flatten <$>
            (Std.IterM.mapM
                (fun b => do
                  let __do_lift ← f b
                  __do_lift.toList)
                it₁).toList
      pure (__do_lift ++ __do_lift_1)
-- Mathlib.Algebra.Category.Grp.EpiMono
AddCommGrpCat.range_eq_top_of_epi : ∀ {A B : AddCommGrpCat} (f : A ⟶ B) [CategoryTheory.Epi f], (AddCommGrpCat.Hom.hom f).range = ⊤
-- Mathlib.CategoryTheory.IsConnected
/-- If any two objects in a nonempty category are related by `Zigzag`, the category is connected.
 -/
CategoryTheory.zigzag_isConnected : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [Nonempty J],
  (∀ (j₁ j₂ : J), CategoryTheory.Zigzag j₁ j₂) → CategoryTheory.IsConnected J
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis
Tactic.ComputeAsymptotics.BasisExtension.getBasis.eq_3 : ∀ {basis : Tactic.ComputeAsymptotics.Basis} (f : ℝ → ℝ) (ex_2 : Tactic.ComputeAsymptotics.BasisExtension basis),
  (Tactic.ComputeAsymptotics.BasisExtension.insert f ex_2).getBasis = f :: ex_2.getBasis
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_zero : Chebyshev.psi 0 = 0
-- Mathlib.Data.Multiset.MapFold
Multiset.map_injective : ∀ {α : Type u_1} {β : Type v} {f : α → β}, Function.Injective f → Function.Injective (Multiset.map f)
-- Std.Async.ContextAsync
/-- An asynchronous computation with cooperative cancellation support via a `CancellationContext`. `ContextAsync α`
is equivalent to `ReaderT CancellationContext Async α`, providing a `CancellationContext` value to async
computations.
 -/
Std.Async.ContextAsync : Type → Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_insertMany_list_le : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {l : List ((a : α) × β a)}, (m.insertMany l).size ≤ m.size + l.length
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.CommGrp C} (e : G.X ≅ H.X)
  (one_f :
    autoParam (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one e.hom = CategoryTheory.MonObj.one)
      _auto_100✝)
  (mul_f :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul e.hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
          CategoryTheory.MonObj.mul)
      _auto_102✝),
  (CategoryTheory.CommGrp.mkIso e one_f mul_f).hom.hom.hom.hom = e.hom
-- Mathlib.Data.FunLike.Basic
/-- **Alias** of `DFunLike.coe_injective`.

---

The coercion to functions must be injective.  -/
DFunLike.coe_injective' : ∀ {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (α → Sort u_3)} [self : DFunLike F α β],
  Function.Injective DFunLike.coe
-- Init.Data.UInt.BasicAux
UInt32.ofNatLT.eq_1 : ∀ (n : ℕ) (h : n < UInt32.size), UInt32.ofNatLT n h = { toBitVec := n#'h }
-- Init.Data.SInt.Lemmas
ISize.toInt_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 31 ≤ n → n < 2 ^ 31 → (ISize.ofInt n).toInt = n
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.p : Lean.Meta.Grind.Arith.CommRing.PolyDerivation → Lean.Grind.CommRing.Poly
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.SuggestionText.string.inj : ∀ {a a_1 : String},
  Lean.Meta.Tactic.TryThis.SuggestionText.string a = Lean.Meta.Tactic.TryThis.SuggestionText.string a_1 → a = a_1
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Context.congrTheorems : Lean.Meta.Simp.Context → Lean.Meta.SimpCongrTheorems
-- Mathlib.RepresentationTheory.Basic
Representation.ofModule_asModule_act : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G) (x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule),
  ((Representation.ofModule ρ.asModule) g) x =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm
      (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x))))
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.image_add_left_Ico : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq α] (a b c : α),
  Finset.image (fun x => c + x) (Finset.Ico a b) = Finset.Ico (c + a) (c + b)
-- Mathlib.Tactic.DefEqTransformations
/-- Eta expand every sub-expression in the given expression.

As a side-effect, beta reduces any pre-existing instances of eta expanded terms.  -/
Mathlib.Tactic.etaExpandAll : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Defs
/-- Exponentiation by repeated squaring.  -/
npowBinRec : {M : Type u_2} → [One M] → [Mul M] → ℕ → M → M
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extInv_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt)
  (w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j)
      CategoryTheory.Limits.Cone.extInv._auto_1),
  (CategoryTheory.Limits.Cone.extInv φ w).hom.hom = φ.hom
-- Mathlib.Combinatorics.Configuration
Configuration.Dual.hasLines : (P : Type u_1) →
  (L : Type u_2) →
    [inst : Membership P L] →
      [Configuration.HasPoints P L] → Configuration.HasLines (Configuration.Dual L) (Configuration.Dual P)
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalizer_le_normalizer_closure : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G),
  AddSubgroup.normalizer s ≤ AddSubgroup.normalizer ↑(AddSubgroup.closure s)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_tendsto_zero_of_firstNonzeroIsNeg : ∀ {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length m = List.length basis → m.FirstNonzeroIsNeg → Filter.Tendsto (m.toFun basis) Filter.atTop (nhds 0)
-- Init.Data.Order.PackageFactories
/-- This class entails `LE α`, `LT α` and `BEq α` instances as well as proofs that these operations
represent the same preorder structure on `α`.
 -/
Std.PreorderPackage : Type u → Type u
-- Mathlib.Algebra.Order.IsBotOne
nonpos_iff_eq_zero : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : Zero α] [IsBotZeroClass α], a ≤ 0 ↔ a = 0
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.mk.injEq : ∀ {M : Type u_3} [inst : MulOneClass M] (toSubsemigroup : Subsemigroup M) (one_mem' : 1 ∈ toSubsemigroup.carrier)
  (toSubsemigroup_1 : Subsemigroup M) (one_mem'_1 : 1 ∈ toSubsemigroup_1.carrier),
  ({ toSubsemigroup := toSubsemigroup, one_mem' := one_mem' } =
      { toSubsemigroup := toSubsemigroup_1, one_mem' := one_mem'_1 }) =
    (toSubsemigroup = toSubsemigroup_1)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.instInhabitedNormalExpr.default : Mathlib.Tactic.Abel.NormalExpr
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_unitIso_hom_app_hom_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.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).unitIso.hom.app X).hom.app X_1 =
    X.obj.map (e.unitIso.inv.app (Opposite.unop X_1)).op
-- Lean.DocString.Markdown
Lean.Doc.MarkdownM.instInhabitedInlineCtx.default : Lean.Doc.MarkdownM.InlineCtx
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.compCreatesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {K : CategoryTheory.Functor J C} →
              {E : Type u₃} →
                [ℰ : CategoryTheory.Category.{v₃, u₃} E] →
                  (F : CategoryTheory.Functor C D) →
                    (G : CategoryTheory.Functor D E) →
                      [CategoryTheory.CreatesColimit K F] →
                        [CategoryTheory.CreatesColimit (K.comp F) G] → CategoryTheory.CreatesColimit K (F.comp G)
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- A bundled version of `S.asLimitCone` and `S.asLimit`.  -/
LightProfinite.lim : (S : LightProfinite) → CategoryTheory.Limits.LimitCone S.diagram
-- Mathlib.RingTheory.Localization.Away.Basic
/-- If `r` and `r'` are associated elements of `R`, an `R`-algebra `S`
is the localization of `R` away from `r` if and only if it is the localization of `R` away from
`r'`.  -/
IsLocalization.Away.iff_of_associated : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {r r' : R},
  Associated r r' → (IsLocalization.Away r S ↔ IsLocalization.Away r' S)
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- From a functor `F : J ⥤ C`, given an initial object of `J`, show the cone
`coneOfDiagramInitial` is a limit.  -/
CategoryTheory.Limits.limitOfDiagramInitial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {X : J} →
          (tX : CategoryTheory.Limits.IsInitial X) →
            (F : CategoryTheory.Functor J C) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfDiagramInitial tX F)
-- Mathlib.Topology.MetricSpace.Basic
/-- If a `PseudoMetricSpace` is a T₀ space, then it is a `MetricSpace`.  -/
MetricSpace.ofT0PseudoMetricSpace : (α : Type u_2) → [inst : PseudoMetricSpace α] → [T0Space α] → MetricSpace α
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_neg : ∀ (R : Type u_3) {A : Type u_4} [inst : AddGroup R] [inst_1 : Neg A] (m : A), ↑(-m) = -↑m
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToIso_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (p : X = X),
  CategoryTheory.eqToIso p = CategoryTheory.Iso.refl X
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a)
  (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X))
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app X) h) =
    h
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.colimitsOfShape_isEmpty_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [IsEmpty J] (X : C),
  P.colimitsOfShape J X ↔ Nonempty (CategoryTheory.Limits.IsInitial X)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instHashableEMatchDiagNode : Hashable Lean.Meta.Grind.EMatchDiagNode
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- For an adjoint triple `F ⊣ G ⊣ H` where `F` and `H` are fully faithful, the natural
transformation `F ⟶ H` is monic at `X` iff the counit of the adjunction `F ⊣ G` is monic
at `H.obj X`.  -/
CategoryTheory.Adjunction.Triple.mono_leftToRight_app_iff_mono_adj₁_counit_app : ∀ {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} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : F.Full] [inst_3 : F.Faithful]
  [H.Full] [H.Faithful] {X : C},
  CategoryTheory.Mono (t.leftToRight.app X) ↔ CategoryTheory.Mono (t.adj₁.counit.app (H.obj X))
-- Mathlib.Order.Cover
WCovBy.of_le_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ⩿ c → a ≤ b → b ≤ c → b ⩿ c
-- Mathlib.Order.Filter.Curry
Filter.eventually_curry_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {m : Filter β} {s : Set α} {t : Set β} [l.NeBot] [m.NeBot],
  (∀ᶠ (x : α × β) in l.curry m, x ∈ s ×ˢ t) ↔ s ∈ l ∧ t ∈ m
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.toMul_eq_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α] {a : Additive α}, Additive.toMul a = ⊤ ↔ a = ⊤
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.trans_left : ∀ {α : Type u_1} [inst : Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α},
  t₁.Bounded o₁ ↑x → t₂.Bounded (↑x) o₂ → t₂.Bounded o₁ o₂
-- Mathlib.RingTheory.Unramified.LocalStructure
_private.Mathlib.RingTheory.Unramified.LocalStructure.0.Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Finite R S],
  (∃ x, R[x] = ⊤) →
    ∀ (Q : Ideal S) [inst_4 : Q.IsPrime] [Algebra.IsUnramifiedAt R Q], ∃ f ∉ Q, HasStandardEtaleSurjectionOn R f
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_Ioo : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : α) [inst_2 : Fintype ↑(Set.Ioo a b)],
  Fintype.card ↑(Set.Ioo a b) = (Finset.Ioo a b).card
-- Mathlib.Data.Quot
Quotient.instUniqueQuotient : {α : Sort u_1} → (s : Setoid α) → [Unique α] → Unique (Quotient s)
-- Mathlib.CategoryTheory.MorphismProperty.LocalClosure
CategoryTheory.MorphismProperty.sourceLocalClosure.le_of_isLocalAtSource : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P Q : CategoryTheory.MorphismProperty C},
  P ≤ Q → ∀ [Q.IsLocalAtSource K], CategoryTheory.MorphismProperty.sourceLocalClosure K P ≤ Q
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- The function `m ↦ m / 1` as an `R`-linear map.
 -/
LocalizedModule.mkLinearMap : {R : Type u} →
  [inst : CommSemiring R] →
    (S : Submonoid R) → (M : Type v) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M →ₗ[R] LocalizedModule S M
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.dvd_iff_content_dvd_content_and_primPart_dvd_primPart : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {p q : Polynomial R},
  q ≠ 0 → (p ∣ q ↔ p.content ∣ q.content ∧ p.primPart ∣ q.primPart)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.lift_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Order.Bounds.Basic
upperBounds_empty : ∀ {α : Type u_1} [inst : Preorder α], upperBounds ∅ = Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.toSubtype_fromSubtype_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] [inst_4 : DecidablePred p] {Z : C}
  (h : ⨁ f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.map fun j => if p j then CategoryTheory.CategoryStruct.id (f j) else 0) h
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
ArithmeticFunction.ofPowerSeries_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {q : ℕ},
  1 < q →
    ∀ (f : PowerSeries R) (n : ℕ),
      ((ArithmeticFunction.ofPowerSeries q) f) n =
        Function.extend (fun x => q ^ x) (fun x => (PowerSeries.coeff x) f) 0 n
-- Mathlib.Algebra.Group.Conj
ConjClasses.mk_eq_mk_iff_isConj : ∀ {α : Type u} [inst : Monoid α] {a b : α}, ConjClasses.mk a = ConjClasses.mk b ↔ IsConj a b
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) {x y : E}, x ≠ 0 → y ≠ 0 → (o.kahler x) y ≠ 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_inter_le_size_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α], (↑m₁).WF → (↑m₂).WF → (↑(m₁.inter m₂)).size ≤ (↑m₂).size
-- Mathlib.Algebra.Module.Equiv.Opposite
MulOpposite.coe_opLinearEquiv_toLinearMap : ∀ (R : Type u) {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⇑↑(MulOpposite.opLinearEquiv R) = MulOpposite.op
-- Mathlib.RingTheory.Smooth.Field
/-- Purely transcendental extensions are formally smooth.  -/
Algebra.FormallySmooth.of_algebraicIndependent : ∀ {K : Type u_1} {L : Type u_2} {ι : Type u_3} [inst : Field L] [inst_1 : Field K] [inst_2 : Algebra K L] {v : ι → L},
  AlgebraicIndependent K v → IntermediateField.adjoin K (Set.range v) = ⊤ → Algebra.FormallySmooth K L
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkHInjType?.mkArgs2.eq_def : ∀ (ctorVal : Lean.ConstructorVal) (args1 : Array Lean.Expr)
  (k : Array Lean.Expr → Lean.MetaM (Option Lean.Meta.MkHInjTypeResult✝)) (i : ℕ) (type : Lean.Expr)
  (args2 : Array Lean.Expr),
  Lean.Meta.mkHInjType?.mkArgs2✝ ctorVal args1 k i type args2 =
    if h : i < args1.size then do
      let __x ← Lean.Meta.whnf type
      match __x with
        | Lean.Expr.forallE n d b binderInfo =>
          have arg1 := args1[i];
          Lean.Meta.withLocalDecl n Lean.BinderInfo.implicit d fun arg2 =>
            Lean.Meta.mkHInjType?.mkArgs2✝ ctorVal args1 k (i + 1) (b.instantiate1 arg2) (args2.push arg2)
        | x =>
          Lean.throwError
            (Lean.toMessageData "unexpected constructor type for `" ++ Lean.toMessageData ctorVal.name ++
              Lean.toMessageData "`")
    else k args2
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.mk.inj : ∀ {R : Type u_1} {inst : CommRing R} {f : Polynomial R} {monic_f : f.Monic} {g : Polynomial R}
  {cond : ∃ p₁ p₂ n, Polynomial.derivative f * p₁ + f * p₂ = g ^ n} {f_1 : Polynomial R} {monic_f_1 : f_1.Monic}
  {g_1 : Polynomial R} {cond_1 : ∃ p₁ p₂ n, Polynomial.derivative f_1 * p₁ + f_1 * p₂ = g_1 ^ n},
  { f := f, monic_f := monic_f, g := g, cond := cond } = { f := f_1, monic_f := monic_f_1, g := g_1, cond := cond_1 } →
    f = f_1 ∧ g = g_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.mk.sizeOf_spec : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] [inst_7 : SizeOf k] [inst_8 : SizeOf V1] [inst_9 : SizeOf P1]
  [inst_10 : SizeOf V2] [inst_11 : SizeOf P2] (toFun : P1 → P2) (linear : V1 →ₗ[k] V2)
  (map_vadd' : ∀ (p : P1) (v : V1), toFun (v +ᵥ p) = linear v +ᵥ toFun p),
  sizeOf { toFun := toFun, linear := linear, map_vadd' := map_vadd' } = 1 + sizeOf linear
-- Lean.Server.References
/-- Replaces the direct imports of a worker for the module `name` in `self` with
a new set of direct imports.
 -/
Lean.Server.References.updateWorkerSetupInfo : Lean.Server.References →
  Lean.Name → Lean.Lsp.DocumentUri → ℕ → Array Lean.Lsp.ImportInfo → Bool → IO Lean.Server.References