mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
/-- The bijection between types of morphisms which is part of the adjunction
`sheafificationAdjunction`.  -/
PresheafOfModules.sheafificationHomEquiv : {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) →
            [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α] →
                [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] →
                  [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
                    {P : PresheafOfModules R₀} →
                      {F : SheafOfModules R} →
                        ((PresheafOfModules.sheafification α).obj P ⟶ F) ≃
                          (P ⟶ (PresheafOfModules.restrictScalars α).obj ((SheafOfModules.forget R).obj F))
-- Mathlib.Algebra.Colimit.Ring
/-- The direct limit of a directed system is the ring obtained by gluing the components along the
maps.  -/
Ring.DirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) → [(i : ι) → CommRing (G i)] → ((i j : ι) → i ≤ j → G i → G j) → Type (max (max u_1 u_2) u_2 u_1)
-- Mathlib.Order.BoundedOrder.Lattice
max_eq_bot : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : OrderBot α] {a b : α}, max a b = ⊥ ↔ a = ⊥ ∧ b = ⊥
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
ModuleCat.MonoidalCategory.symmetricCategory : {R : Type u} → [inst : CommRing R] → CategoryTheory.SymmetricCategory (ModuleCat R)
-- Mathlib.Data.Multiset.AddSub
Multiset.erase_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s : Multiset α), s.erase a ⊆ s
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.w_whiskerRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {Q : C},
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Q)
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight inl Q) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Q)
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight inr Q)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_3.eq_1 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₂ m γ] (it₂ : Std.IterM m γ)
  (motive : it₂.Step → Sort u_3) (it₂' : Std.IterM m γ) (out : γ)
  (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out))
  (h_1 :
    (it₂' : Std.IterM m γ) →
      (out : γ) → (h : it₂.IsPlausibleStep (Std.IterStep.yield it₂' out)) → motive ⟨Std.IterStep.yield it₂' out, h⟩)
  (h_2 :
    (it₂' : Std.IterM m γ) → (h : it₂.IsPlausibleStep (Std.IterStep.skip it₂')) → motive ⟨Std.IterStep.skip it₂', h⟩)
  (h_3 : (h : it₂.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₂' out, h⟩ with
    | ⟨Std.IterStep.yield it₂' out, h⟩ => h_1 it₂' out h
    | ⟨Std.IterStep.skip it₂', h⟩ => h_2 it₂' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₂' out h
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₈_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3],
  W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- The canonical isomorphism `shiftFunctor C n ⋙ F ≅ F.shift n`.  -/
CategoryTheory.Functor.isoShift : {C : Type u_1} →
  {A : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} A] →
        (F : CategoryTheory.Functor C A) →
          {M : Type u_4} →
            [inst_2 : AddMonoid M] →
              [inst_3 : CategoryTheory.HasShift C M] →
                [inst_4 : F.ShiftSequence M] → (n : M) → (CategoryTheory.shiftFunctor C n).comp F ≅ F.shift n
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.mul_left' : ∀ {n a b : ℕ} (c : ℕ), a ≡ b [MOD n] → c * a ≡ c * b [MOD c * n]
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getEntry?ₘ : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → α → Option ((a : α) × β a)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.embedding_apply : ∀ {K : Type u_1} [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : K),
  (NumberField.FinitePlace.embedding v) x =
    { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm x) }
-- Mathlib.Data.EReal.Operations
/-- If `-a ≤ b` then `-b ≤ a` on `EReal`.  -/
EReal.neg_le_of_neg_le : ∀ {a b : EReal}, -a ≤ b → -b ≤ a
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- The unit for the adjunction for `Cocone.functoriality K F : Cocone K ⥤ Cocone (K ⋙ F)`.

Auxiliary definition for `functorialityAdjunction`.
 -/
CategoryTheory.Adjunction.functorialityUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (adj : F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  (K : CategoryTheory.Functor J C) →
                    CategoryTheory.Functor.id (CategoryTheory.Limits.Cocone K) ⟶
                      (CategoryTheory.Limits.Cocone.functoriality K F).comp (adj.functorialityRightAdjoint K)
-- Lean.Parser.Attr
Lean.Parser.Attr.externEntry.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.InnerProductSpace.Rayleigh
/-- The supremum of the Rayleigh quotient of a symmetric operator `T` on a nontrivial
finite-dimensional vector space is an eigenvalue for that operator.  -/
LinearMap.IsSymmetric.hasEigenvalue_iSup_of_finiteDimensional : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [FiniteDimensional 𝕜 E] {T : E →ₗ[𝕜] E} [Nontrivial E],
  T.IsSymmetric → Module.End.HasEigenvalue T ↑(⨆ x, RCLike.re (inner 𝕜 (T ↑x) ↑x) / ‖↑x‖ ^ 2)
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- The one-preserving homomorphism including a single value
into a dependent family of values, as functions supported at a point.

This is the `OneHom` version of `Pi.mulSingle`.  -/
OneHom.mulSingle : {I : Type u} →
  (f : I → Type v) → [DecidableEq I] → [inst : (i : I) → One (f i)] → (i : I) → OneHom (f i) ((i : I) → f i)
-- Batteries.Tactic.Lint.Simp
/-- Render the list of simp lemmas.  -/
Batteries.Tactic.Lint.formatLemmas : Lean.Meta.Simp.UsedSimps → String → Option Bool → Lean.MetaM Lean.MessageData
-- Aesop.Search.Expansion
Aesop.runFirstUnsafeRule : {Q : Type} → [inst : Aesop.Queue Q] → Array Aesop.PostponedSafeRule → Aesop.GoalRef → Aesop.SearchM Q Aesop.RuleResult
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Mon.mul.go.match_1.splitter : (motive : Nat.Internal.SOM.Mon → Nat.Internal.SOM.Mon → Sort u_1) →
  (m₁ m₂ : Nat.Internal.SOM.Mon) →
    ((m₁ : Nat.Internal.SOM.Mon) → motive m₁ []) →
      ((m₂ : Nat.Internal.SOM.Mon) → (m₂ = [] → False) → motive [] m₂) →
        ((v₁ : Nat.Internal.Linear.Var) →
            (m₁ : List Nat.Internal.Linear.Var) →
              (v₂ : Nat.Internal.Linear.Var) → (m₂ : List Nat.Internal.Linear.Var) → motive (v₁ :: m₁) (v₂ :: m₂)) →
          motive m₁ m₂
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.incidenceSet.eq_1 : ∀ {V : Type u} (G : SimpleGraph V) (v : V), G.incidenceSet v = {e | e ∈ G.edgeSet ∧ v ∈ e}
-- Mathlib.RingTheory.Ideal.Operations
Ideal.finset_inf_span_singleton : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type u_2} (s : Finset ι) (I : ι → R),
  (↑s).Pairwise (Function.onFun IsCoprime I) → (s.inf fun i => Ideal.span {I i}) = Ideal.span {∏ i ∈ s, I i}
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.restr_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set α), (e.restr s).source = e.source ∩ s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_filter_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  t.WF → ((Std.DTreeMap.Raw.filter f t).isEmpty = true ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = false)
-- Std.Tactic.BVDecide.LRAT.Internal.Actions
Std.Tactic.BVDecide.LRAT.Internal.natLiteralToPosFinLiteral : {n : ℕ} → Std.Sat.Literal ℕ → Option (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
-- Mathlib.CategoryTheory.Sites.Preserves
/-- If `F` preserves a particular product, then it `IsSheafFor` the corresponding presieve of arrows.
 -/
CategoryTheory.Presieve.isSheafFor_of_preservesProduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type w)) {α : Type u_1}
  [Small.{w, u_1} α] {X : α → C} (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c)
  [(CategoryTheory.Presieve.ofArrows X c.inj).HasPairwisePullbacks]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor fun x => Opposite.op (X x)) F],
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows X c.inj)
-- Mathlib.Order.Antisymmetrization
wellFoundedLT_antisymmetrization_iff : ∀ {α : Type u_1} [inst : Preorder α], WellFoundedLT (Antisymmetrization α fun x1 x2 => x1 ≤ x2) ↔ WellFoundedLT α
-- Mathlib.ModelTheory.Skolem
FirstOrder.Language.skolem₁_Functions : ∀ (L : FirstOrder.Language) (n : ℕ), L.skolem₁.Functions n = L.BoundedFormula Empty (n + 1)
-- Mathlib.AlgebraicGeometry.PullbackCarrier
/-- A helper lemma to work with `AlgebraicGeometry.Scheme.Pullback.carrierEquiv`.  -/
AlgebraicGeometry.Scheme.Pullback.carrierEquiv_eq_iff : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S}
  {T₁ T₂ : (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g) × ↥(AlgebraicGeometry.Spec T.tensor)},
  T₁ = T₂ ↔
    ∃ (e : T₁.fst = T₂.fst),
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Pullback.Triplet.tensorCongr e).inv) T₁.snd = T₂.snd
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_maxKey?_of_isSome_maxKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).maxKey?.isSome = true → t.maxKey?.isSome = true
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelBorel.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] {mΩ : MeasurableSpace Ω} [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] (κ : ProbabilityTheory.Kernel α (γ × Ω)) [inst_3 : ProbabilityTheory.IsFiniteKernel κ],
  κ.condKernelBorel =
    ProbabilityTheory.Kernel.borelMarkovFromReal Ω (κ.map (Prod.map id (MeasureTheory.embeddingReal Ω))).condKernelReal
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Fmla.subsumes.prop : ∀ {f f' : Sat.Fmla}, f.subsumes f' → ∀ x ∈ f', x ∈ f
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_add_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.degree < q.degree → (p + q).leadingCoeff = q.leadingCoeff
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.StructuredArrow.hasLimitsOfSize : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {T : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} T]
  {X : T} {G : CategoryTheory.Functor A T} [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, u₁} A]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₃, u₁, u₃} G],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, max u₁ v₃} (CategoryTheory.StructuredArrow X G)
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.fst_comp_inl : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], (OrderAddMonoidHom.fst α β).comp (OrderAddMonoidHom.inl α β) = OrderAddMonoidHom.id α
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valuation.isNontrivial_iff_not_a_field : ∀ {K : Type u_3} {Γ : Type u_4} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ),
  v.IsNontrivial ↔ IsLocalRing.maximalIdeal ↥v.integer ≠ ⊥
-- Std.Http.Data.Status
Std.Http.instReprCustomStatus.repr : Std.Http.CustomStatus → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Matrix.ToLin
Algebra.smulTower_leftMulMatrix_algebraMap_ne : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [inst_6 : IsScalarTower R S T] {m : Type u_4}
  {n : Type u_5} [inst_7 : Fintype m] [inst_8 : Fintype n] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n]
  (b : Module.Basis m R S) (c : Module.Basis n S T) (x : S) (i j : m) {k k' : n},
  k ≠ k' → (Algebra.leftMulMatrix (b.smulTower c)) ((algebraMap S T) x) (i, k) (j, k') = 0
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.setAllDiagRanges : Lean.Language.SnapshotTree → Lean.Position → Lean.Position → BaseIO Lean.Language.SnapshotTree
-- Mathlib.Algebra.Order.Hom.Ring
/-- Reinterpret an ordered ring homomorphism as a ring homomorphism.  -/
OrderRingHom.toRingHom : {α : Type u_6} →
  {β : Type u_7} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] → [inst_2 : NonAssocSemiring β] → [inst_3 : Preorder β] → α →+*o β → α →+* β
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.pre_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C CategoryTheory.Cat) {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  (G : CategoryTheory.Functor D C) (H : CategoryTheory.Functor E D),
  CategoryTheory.Grothendieck.pre F (H.comp G) =
    (CategoryTheory.Grothendieck.pre (G.comp F) H).comp (CategoryTheory.Grothendieck.pre F G)
-- Mathlib.RingTheory.Morita.Matrix
/-- The functor from the category of modules over `Mₙ(R)` to the category of modules over `R`
induced by sending `M` to the image of `Eᵢᵢ • ·` where `Eᵢᵢ` is the elementary matrix.  -/
MatrixModCat.toModuleCat : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] → ι → CategoryTheory.Functor (ModuleCat (Matrix ι ι R)) (ModuleCat R)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.bind_eq_bind_subtypeCasesOn'_optionPelim' : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] {P : Option α → Prop} (x : m (Subtype P))
  (f : Subtype P → m β),
  x >>= f = do
    let a ← x
    Std.Internal.subtypeCasesOn'✝ a fun a ha =>
        Std.Internal.optionPelim'✝ a (fun h => f ⟨none, ⋯⟩) fun a_1 h => f ⟨some a_1, ⋯⟩
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.hom_ext_iff : ∀ {X Y : FinPartOrd} {f g : X ⟶ Y}, f = g ↔ PartOrd.Hom.hom f.hom = PartOrd.Hom.hom g.hom
-- Std.Http.Data.Method
/-- Converts a `String` into a `Method`, panicking if unrecognized.
 -/
Std.Http.Method.ofString! : String → Std.Http.Method
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the number of elements contained in the given left-closed right-open range.
 -/
Std.Rco.size : {α : Type u} → [Std.Rxo.HasSize α] → Std.Rco α → ℕ
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Simp.DischargeWrapper.with : {α : Type} →
  Lean.Elab.Tactic.Simp.DischargeWrapper →
    (Option Lean.Meta.Simp.Discharge → Lean.Elab.Tactic.TacticM α) → Lean.Elab.Tactic.TacticM α
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with addition.  -/
ContDiffWithinAt.laplacianWithin_add : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E} {s : Set E},
  ContDiffWithinAt ℝ 2 f₁ s x →
    ContDiffWithinAt ℝ 2 f₂ s x →
      UniqueDiffOn ℝ s →
        x ∈ s →
          InnerProductSpace.laplacianWithin (f₁ + f₂) s x =
            InnerProductSpace.laplacianWithin f₁ s x + InnerProductSpace.laplacianWithin f₂ s x
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A non-unital subalgebra of a non-unital seminormed ring is also a non-unital seminormed ring,
with the restriction of the norm.  -/
NonUnitalSubalgebraClass.nonUnitalSeminormedRing : {S : Type u_5} →
  {𝕜 : Type u_6} →
    {E : Type u_7} →
      [inst : CommRing 𝕜] →
        [inst_1 : NonUnitalSeminormedRing E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : SetLike S E] →
              [NonUnitalSubringClass S E] → [SMulMemClass S 𝕜 E] → (s : S) → NonUnitalSeminormedRing ↥s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α}, (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Congruence.toIsStableUnderPostcomp : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {r : HomRel C} [self : CategoryTheory.Congruence r],
  CategoryTheory.HomRel.IsStableUnderPostcomp r
-- Mathlib.Data.Nat.Set
Nat.zero_union_range_succ : {0} ∪ Set.range Nat.succ = Set.univ
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LEquiv.mk.inj : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {toLHom : L →ᴸ L'} {invLHom : L' →ᴸ L}
  {left_inv : invLHom.comp toLHom = FirstOrder.Language.LHom.id L}
  {right_inv : toLHom.comp invLHom = FirstOrder.Language.LHom.id L'} {toLHom_1 : L →ᴸ L'} {invLHom_1 : L' →ᴸ L}
  {left_inv_1 : invLHom_1.comp toLHom_1 = FirstOrder.Language.LHom.id L}
  {right_inv_1 : toLHom_1.comp invLHom_1 = FirstOrder.Language.LHom.id L'},
  { toLHom := toLHom, invLHom := invLHom, left_inv := left_inv, right_inv := right_inv } =
      { toLHom := toLHom_1, invLHom := invLHom_1, left_inv := left_inv_1, right_inv := right_inv_1 } →
    toLHom = toLHom_1 ∧ invLHom = invLHom_1
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressReport.mk.injEq : ∀ (kind : String) (message? : Option String) (cancellable : Bool) (percentage? : Option ℕ) (kind_1 : String)
  (message?_1 : Option String) (cancellable_1 : Bool) (percentage?_1 : Option ℕ),
  ({ kind := kind, message? := message?, cancellable := cancellable, percentage? := percentage? } =
      { kind := kind_1, message? := message?_1, cancellable := cancellable_1, percentage? := percentage?_1 }) =
    (kind = kind_1 ∧ message? = message?_1 ∧ cancellable = cancellable_1 ∧ percentage? = percentage?_1)
-- Mathlib.Topology.Hom.ContinuousEvalConst
ContinuousOn.eval_const : ∀ {F : Type u_1} {α : Type u_2} {X : Type u_3} {Z : Type u_4} [inst : FunLike F α X] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace X] [ContinuousEvalConst F α X] [inst_4 : TopologicalSpace Z] {f : Z → F} {s : Set Z},
  ContinuousOn f s → ∀ (x : α), ContinuousOn (fun x_1 => (f x_1) x) s
-- Batteries.Control.AlternativeMonad
failure_seqRight : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Alternative m] [LawfulAlternative m] (x : m α),
  failure *> x = failure
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.associator_inv_comp_tensorHom_tensorHom_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂)
  (fg : CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂ ⟶ W) {Z : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj W Z₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) fg) h)
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom fg (CategoryTheory.CategoryStruct.id Z₂)) h_1))
-- Mathlib.Order.DirectedInverseSystem
_private.Mathlib.Order.DirectedInverseSystem.0.InverseSystem.globalEquivAux : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      [inst : LinearOrder ι] →
        {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
          [WellFoundedLT ι] →
            [inst_2 : SuccOrder ι] →
              [InverseSystem f] →
                (equivSucc : (i : ι) → ¬IsMax i → { e // ∀ (x : F (Order.succ i)), (e x).1 = f ⋯ x }) →
                  ((i : ι) → Order.IsSuccPrelimit i → { e // ∀ (x : F i) (l : ↑(Set.Iio i)), ↑(e x) l = f ⋯ x }) →
                    (i : ι) → InverseSystem.PEquivOn f (fun i hi => ↑(equivSucc i hi)) (Set.Iic i)
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.forgetToCat_full : CategoryTheory.Grpd.forgetToCat.Full
-- Init.Data.Option.Lemmas
Option.or_eq_bif : ∀ {α : Type u_1} {o o' : Option α}, o.or o' = bif o.isSome then o else o'
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
/-- Assume that `u : E →L[𝕜] F` restricts to an isomorphism between closed finite codimension
subspaces `E₁` and `F₁`. Then `u` is Fredholm.

In fact it is enough to assume that the restriction `E₁ →L[𝕜] F₁` is Fredholm, see
`IsFredholm.of_restrict` (not in Mathlib yet).  -/
ContinuousLinearMap.IsFredholm.of_isInvertible_restrict : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] {u : E →L[𝕜] F} {E₁ : Submodule 𝕜 E},
  IsClosed ↑E₁ →
    ∀ [E₁_coFG : E₁.CoFG] {F₁ : Submodule 𝕜 F},
      IsClosed ↑F₁ →
        ∀ [F₁_coFG : F₁.CoFG] (h_mapsto : Set.MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h_mapsto).IsInvertible → u.IsFredholm
-- Init.Prelude
/-- `` `str `` is the node kind of string literals like `"foo"`.  -/
Lean.strLitKind : Lean.SyntaxNodeKind
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_eq_some_getKey : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α} (h : a ∈ m), m.getKey? a = some (m.getKey a h)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariant_lt_of_covariant_le_of_contravariant_eq : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [ContravariantClass M N μ fun x1 x2 => x1 = x2] [inst : PartialOrder N]
  [CovariantClass M N μ fun x1 x2 => x1 ≤ x2], CovariantClass M N μ fun x1 x2 => x1 < x2
-- Mathlib.NumberTheory.LucasLehmer
mersenne_mod_four : ∀ {n : ℕ}, 2 ≤ n → mersenne n % 4 = 3
-- Mathlib.Algebra.Colimit.Ring
/-- A component that corresponds to zero in the direct limit is already zero in some
bigger module in the directed system.  -/
Ring.DirectLimit.of.zero_exact : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f' : (i j : ι) → i ≤ j → G i →+* G j} [DirectedSystem G fun i j h => ⇑(f' i j h)] [IsDirectedOrder ι] {i : ι}
  {x : G i}, (Ring.DirectLimit.of G (fun x1 x2 x3 => ⇑(f' x1 x2 x3)) i) x = 0 → ∃ j, ∃ (hij : i ≤ j), (f' i j hij) x = 0