mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.canonicallyOrderedAdd : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedRing α],
  CanonicallyOrderedAdd { x // 0 ≤ x }
-- Mathlib.Data.List.Map2
List.map₂Right'_cons_cons : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (a : α) (as : List α) (b : β) (bs : List β),
  List.map₂Right' f (a :: as) (b :: bs) =
    have r := List.map₂Right' f as bs;
    (f (some a) b :: r.1, r.2)
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.instInhabitedComp : Inhabited Mathlib.Tactic.Linarith.Comp
-- Mathlib.Order.Lattice
exists_and_iff_of_antitone : ∀ {α : Type u} [inst : SemilatticeInf α] {P Q : α → Prop},
  Antitone P → Antitone Q → (((∃ x, P x) ∧ ∃ x, Q x) ↔ ∃ x, P x ∧ Q x)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.commute_of_mem_adjoin_self : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] {a b : A} [IsStarNormal a], b ∈ NonUnitalStarAlgebra.adjoin R {a} → Commute a b
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.measurable_partitionFiltration_memPartitionSet : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)) (n : ℕ),
  Measurable (memPartitionSet t n)
-- Mathlib.Order.DirectedInverseSystem
DirectLimit.exists_eq_mk : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] (z : DirectLimit F f),
  ∃ i x, z = ⟦⟨i, x⟩⟧
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.mem_implicitToOpenPartialHomeomorphOfComplemented_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E}
  (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  (f a, 0) ∈ (HasStrictFDerivAt.implicitToOpenPartialHomeomorphOfComplemented f f' hf hf' hker).target
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.nerveEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.ComposableArrows C 0),
  SSet.OneTruncation₂.nerveEquiv f = f.obj 0
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.prop_tensor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {P₁ P₂ Q : CategoryTheory.ObjectProperty C} [P₁.TensorLE P₂ Q] {X₁ X₂ : C},
  P₁ X₁ → P₂ X₂ → Q (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
-- Mathlib.Topology.Neighborhoods
eventually_eventuallyLE_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} [inst_1 : LE α] {f g : X → α},
  (∀ᶠ (y : X) in nhds x, f ≤ᶠ[nhds y] g) ↔ f ≤ᶠ[nhds x] g
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.comap_comap : ∀ {K : Type u} [inst : Field K] {L : Type u_1} {J : Type u_2} [inst_1 : Field L] [inst_2 : Field J]
  (A : ValuationSubring J) (g : L →+* J) (f : K →+* L), (A.comap g).comap f = A.comap (g.comp f)
-- Std.Data.DHashMap.Raw
/-- Retrieves the mapping for the given key. Ensures that such a mapping exists by requiring a proof
of `a ∈ m`.

Uses the `LawfulBEq` instance to cast the retrieved value to the correct type.
 -/
Std.DHashMap.Raw.get : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → [LawfulBEq α] → (m : Std.DHashMap.Raw α β) → (a : α) → a ∈ m → β a
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.IterM.step_drop.match_3.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (h : it.IsPlausibleStep Std.IterStep.done)
  (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.done, 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_3 h
-- Mathlib.Data.Fintype.Inv
Function.Injective.left_inv_of_invOfMemRange : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β} (hf : Function.Injective f)
  (b : ↑(Set.range f)), f (hf.invOfMemRange b) = ↑b
-- Mathlib.Algebra.Polynomial.Lifts
/-- A polynomial `p` lifts if and only if it is in the image of `mapAlg`.  -/
Polynomial.mem_lifts_iff_mem_alg : ∀ (R : Type u) [inst : CommSemiring R] {S : Type v} [inst_1 : Semiring S] [inst_2 : Algebra R S] (p : Polynomial S),
  p ∈ Polynomial.lifts (algebraMap R S) ↔ p ∈ (Polynomial.mapAlg R S).range
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold.inj : ∀ {fvarId fvarId_1 : Lean.FVarId},
  Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold fvarId =
      Lean.Elab.Tactic.ElabSimpArgResult.addLetToUnfold fvarId_1 →
    fvarId = fvarId_1
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_fun_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 g s x → derivWithin (fun y => f y - g y) s x = derivWithin f s x - derivWithin g s x
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.zero.injEq : ∀ {α : Type} (ch ch_1 : Std.CloseableChannel.Zero✝ α),
  (Std.CloseableChannel.Flavors.zero✝ ch = Std.CloseableChannel.Flavors.zero✝ ch_1) = (ch = ch_1)
-- Mathlib.Algebra.Polynomial.GroupRingAction
Polynomial.smul_eq_map : ∀ {M : Type u_1} [inst : Monoid M] (R : Type u_2) [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M),
  HSMul.hSMul m = Polynomial.map (MulSemiringAction.toRingHom M R m)
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- Given a functor `F : J ⥤ TopCat` and a cone `c : Cone (F ⋙ forget)`
of the underlying functor to types, the limit of `F` is `c.pt` equipped
with the infimum of the induced topologies by the maps `c.π.app j`.  -/
TopCat.isLimitConeOfForget : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J TopCat} →
      (c : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.forget TopCat))) →
        CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (TopCat.coneOfConeForget c)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.fintypeSubtypePathLengthLT : {V : Type u} →
  (G : SimpleGraph V) →
    [DecidableEq V] → [G.LocallyFinite] → (u v : V) → (n : ℕ) → Fintype { p // p.IsPath ∧ p.length < n }
-- Init.Data.SInt.Lemmas
ISize.toUSize_ofNat' : ∀ {n : ℕ}, (ISize.ofNat n).toUSize = USize.ofNat n
-- Init.MetaTypes
/-- When `true` (default: `false`), simplifies simple arithmetic expressions.  -/
Lean.Meta.Simp.Config.arith : Lean.Meta.Simp.Config → Bool
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {P Q : CategoryTheory.ObjectProperty C}, P ≤ Q → P.trW ≤ Q.trW
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.isClosed_ker : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [T1Space M₂] (f : M₁ →SL[σ₁₂] M₂),
  IsClosed ↑(↑f).ker
-- Mathlib.ModelTheory.Definability
Set.DefinableFun.eq_1 : ∀ {M : Type u_1} (L : FirstOrder.Language) [inst : L.Structure M] {α : Type u_2} (A : Set M) (f : (α → M) → M),
  Set.DefinableFun L A f = A.Definable L (Function.tupleGraph f)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_of_not_haveLebesgueDecomposition : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  ¬μ.HaveLebesgueDecomposition ν → μ.singularPart ν = 0
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.nonneg : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (abv : AbsoluteValue R S) (x : R), 0 ≤ abv x
-- Mathlib.Topology.Order.MonotoneConvergence
Monotone.ge_of_tendsto : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsDirectedOrder β] {f : β → α} {a : α},
  Monotone f → Filter.Tendsto f Filter.atTop (nhds a) → ∀ (b : β), f b ≤ a
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_def : ∀ {α : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : α → G),
  MeasureTheory.integral μ f =
    if x_1 : CompleteSpace G then
      if hf : MeasureTheory.Integrable f μ then MeasureTheory.L1.integral (MeasureTheory.Integrable.toL1 f hf) else 0
    else 0
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.fract.eq_1 : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m : E), ZSpan.fract b m = m - ↑(ZSpan.floor b m)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLTGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ),
  t.IsGE ((t.truncLTGE a b).obj X) a
-- Mathlib.NumberTheory.SumTwoSquares
/-- If the natural number `n` is a sum of two squares of coprime natural numbers, then
`-1` is a square modulo `n`.  -/
ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime : ∀ {n x y : ℕ}, n = x ^ 2 + y ^ 2 → x.Coprime y → IsSquare (-1)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s t : Set α} {g : M} (hg : g +ᵥ t = s),
  SubAddAction.fixingAddSubgroupEquivFixingAddSubgroup hg =
    (AddEquiv.addSubgroupMap (AddAut.addConj g) (fixingAddSubgroup M t)).trans (AddEquiv.addSubgroupCongr ⋯)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.set_StateT : ∀ {m : Type u → Type v} {psm : Std.Do.PostShape} {σ : Type u} {s : σ}
  {Q : Std.Do.PostCond PUnit.{u + 1} (Std.Do.PostShape.arg σ psm)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m psm],
  ⦃fun x => Q.1 PUnit.unit s⦄ set s ⦃Q⦄
-- Mathlib.Data.PFun
PFun.asSubtype.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : ↑f.Dom), f.asSubtype s = f.fn ↑s ⋯
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.isFOLike : Lean.Expr → Lean.MetaM Bool
-- Aesop.Forward.Match.Types
/-- Compare two queue entries by rule priority, rule name and the expressions
contained in the match. Higher-priority rules are considered less (since the
queues are min-queues). The ordering on expressions is arbitrary.  -/
Aesop.ForwardRuleMatch.le : Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatch → Bool
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Functor.mapExtAddHom.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ), F.mapExtAddHom X Y n = F.mapExtAddHom X Y n
-- Mathlib.RingTheory.Extension.Basic
/-- A hom of extensions `P → P'` can be constructed from an algebra map
`P.Ring →ₐ[R] P'.Ring`.  -/
Algebra.Extension.Hom.ofAlgHom : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            {R' : Type u_1} →
              {S' : Type u_2} →
                [inst_3 : CommRing R'] →
                  [inst_4 : CommRing S'] →
                    [inst_5 : Algebra R' S'] →
                      {P' : Algebra.Extension R' S'} →
                        [inst_6 : Algebra R R'] →
                          [inst_7 : Algebra S S'] →
                            [inst_8 : Algebra R S'] →
                              [inst_9 : IsScalarTower R R' S'] →
                                [inst_10 : IsScalarTower R S S'] →
                                  (f : P.Ring →ₐ[R] P'.Ring) →
                                    (IsScalarTower.toAlgHom R P'.Ring S').comp f =
                                        (IsScalarTower.toAlgHom R S S').comp (IsScalarTower.toAlgHom R P.Ring S) →
                                      P.Hom P'
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.mono' : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : Zero β] [inst_2 : Zero γ]
  {f : α → β} {f' : α → γ}, HasCompactSupport f → Function.support f' ⊆ tsupport f → HasCompactSupport f'
-- Init.Data.Array.Find
Array.findIdx?_eq_none_iff_findIdx_eq : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.findIdx? p xs = none ↔ Array.findIdx p xs = xs.size
-- Init.Data.Hashable
instHashableChar : Hashable Char
-- Mathlib.Analysis.Complex.Basic
/-- The *slit plane* is the complex plane with the closed negative real axis removed.  -/
Complex.slitPlane : Set ℂ
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instMonad : Monad Std.Async.ContextAsync
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Monotone CategoryTheory.MorphismProperty.multiplicativeClosure
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.instHasFrameCurryULiftPropUpAndOfAnd : ∀ {φ : Prop} (σs : List (Type u_1)) (P P' : Std.Do.SVal.StateTuple σs → Prop) (Q : Std.Do.SPred σs)
  [Std.Do.SPred.Tactic.HasFrame
      spred((Std.Do.SVal.curry fun t => { down := P t }) ∧ Std.Do.SVal.curry fun t => { down := P' t }) Q φ],
  Std.Do.SPred.Tactic.HasFrame (Std.Do.SVal.curry fun t => { down := P t ∧ P' t }) Q φ
-- Mathlib.Topology.ContinuousMap.Defs
/-- Deprecated. Use `DFunLike.congr_fun` instead.  -/
ContinuousMap.congr_fun : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)},
  f = g → ∀ (x : X), f x = g x
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOn.congr_inseparable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α}
  {p : Filter ι} {F' : ι → α → β},
  TendstoUniformlyOn F f p s → (∀ᶠ (n : ι) in p, ∀ x ∈ s, Inseparable (F n x) (F' n x)) → TendstoUniformlyOn F' f p s
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_div_cancel_left : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a : α}, IsUnit a → ∀ (b : α), a * b / a = b
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_constToList_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β},
  (Std.DHashMap.Const.toList m₁).Perm (Std.DHashMap.Const.toList m₂) → m₁.Equiv m₂
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.prod_same_index : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {la : Filter α} {sa : ι → Set α} {lb : Filter β} {p : ι → Prop}
  {sb : ι → Set β},
  la.HasBasis p sa →
    lb.HasBasis p sb →
      (∀ {i j : ι}, p i → p j → ∃ k, p k ∧ sa k ⊆ sa i ∧ sb k ⊆ sb j) → (la ×ˢ lb).HasBasis p fun i => sa i ×ˢ sb i
-- Mathlib.Topology.Algebra.MulAction
SMulMemClass.continuousSMul : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X] {S : Type u_5} [inst_4 : SetLike S X] [inst_5 : SMulMemClass S M X] (s : S), ContinuousSMul M ↥s
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.anyTR.loop.congr_simp : ∀ (n : ℕ) (f f_1 : (i : ℕ) → i < n → Bool),
  f = f_1 → ∀ (i i_1 : ℕ) (e_i : i = i_1) (a : i ≤ n), Nat.anyTR.loop✝ n f i a = Nat.anyTR.loop✝ n f_1 i_1 ⋯
-- Mathlib.Topology.Sheaves.LocalPredicate
/-- For a binary operation (e.g. `x ↦ y ↦ x + y`) defined at each stalk, if a prelocal predicate is
closed under the operation on each open set, then the sheafified predicate is also closed under the
operation. See `sheafify_inductionOn₂` for the version with refinement.  -/
TopCat.PrelocalPredicate.sheafify_inductionOn₂' : ∀ {X : TopCat} {T₁ : ↑X → Type u_2} {T₂ : ↑X → Type u_3} {T₃ : ↑X → Type u_4} (P₁ : TopCat.PrelocalPredicate T₁)
  (P₂ : TopCat.PrelocalPredicate T₂) (P₃ : TopCat.PrelocalPredicate T₃) (op : {x : ↑X} → T₁ x → T₂ x → T₃ x),
  (∀ {U V : TopologicalSpace.Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥V) → T₂ ↑x},
      P₁.pred a → P₂.pred b → P₃.pred fun x => op (a ⟨↑x, ⋯⟩) (b ⟨↑x, ⋯⟩)) →
    ∀ {U : TopologicalSpace.Opens ↑X} {a : (x : ↥U) → T₁ ↑x} {b : (x : ↥U) → T₂ ↑x},
      P₁.sheafify.pred a → P₂.sheafify.pred b → P₃.sheafify.pred fun x => op (a x) (b x)
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.eq_nil_of_isRegular_on_artinian : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  {rs : List R}, RingTheory.Sequence.IsRegular M rs → rs = []
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.processConst : Lean.Name → List Lean.Level → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Algebra.Group.Pi.Basic
Pi.commSemigroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → CommSemigroup (f i)],
  Pi.commSemigroup = { toSemigroup := Pi.semigroup, mul_comm := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.unop_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂), ψ.unop.left = ψ.right.unop
-- Init.Data.UInt.Bitwise
UInt64.ofFin_or : ∀ (a b : Fin UInt64.size), UInt64.ofFin (a ||| b) = UInt64.ofFin a ||| UInt64.ofFin b
-- Mathlib.RingTheory.AdicCompletion.Completeness
AdicCompletion.ofPowSMul_val_apply_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b : ℕ}, a ≤ b → ∀ {x : AdicCompletion I ↥(I ^ b • ⊤)}, ↑((AdicCompletion.ofPowSMul I M b) x) a = 0
-- Mathlib.Order.WellFounded
Function.argmin_le : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [inst : LinearOrder β] [inst_1 : WellFoundedLT β] (a : α)
  [inst_2 : Nonempty α], f (Function.argmin f) ≤ f a
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.strictMap_iff : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) (F : CategoryTheory.Functor C D) (Y : D),
  P.strictMap F Y ↔ ∃ X, P X ∧ F.obj X = Y
-- Mathlib.Order.RelClasses
instWellFoundedGTOrderDualOfWellFoundedLT : ∀ (α : Type u_1) [inst : LT α] [h : WellFoundedLT α], WellFoundedGT αᵒᵈ
-- Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
instEssentiallySmallFGModuleCat : ∀ (R : Type u) [inst : Ring R], CategoryTheory.EssentiallySmall.{u, v, max (v + 1) u} (FGModuleCat R)
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Bornology α] [inst_1 : Bornology β] {f g : LocallyBoundedMap α β},
  f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Topology.Separation.DisjointCover
/-- For any continuous function `f : X → V`, with `X` profinite, and `S` a neighbourhood of the
diagonal in `V × V`, there exists a finite cover of `X` by pairwise-disjoint nonempty clopens, on
each of which `f` varies within `S`.
 -/
ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal : ∀ {X : Type u_1} {V : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace V] [TotallyDisconnectedSpace X]
  [T2Space X] [CompactSpace X] {S : Set (V × V)} (f : C(X, V)),
  S ∈ nhdsSet (Set.diagonal V) →
    ∃ n D,
      (∀ (i : Fin n), D i ≠ ⊥) ∧
        (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (f y, f z) ∈ S) ∧
          Set.univ ⊆ ⋃ i, ↑(D i) ∧ Pairwise (Function.onFun Disjoint D)
-- Mathlib.ModelTheory.Syntax
/-- The biimplication between formulas, as a formula.  -/
FirstOrder.Language.Formula.iff : {L : FirstOrder.Language} → {α : Type u'} → L.Formula α → L.Formula α → L.Formula α
-- Init.Data.Vector.Lemmas
Vector.append_inj : ∀ {α : Type u_1} {n m : ℕ} {xs₁ xs₂ : Vector α n} {ys₁ ys₂ : Vector α m},
  xs₁ ++ ys₁ = xs₂ ++ ys₂ → xs₁ = xs₂ ∧ ys₁ = ys₂
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff.eq_1 : ∀ {R : Type u} [inst : Semiring R] (p : AddMonoidAlgebra R ℕ), { toFinsupp := p }.coeff = ⇑p.coeff
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction
CategoryTheory.Adjunction.hasLeftCalculusOfFractions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) (W : CategoryTheory.MorphismProperty C₁) [W.IsMultiplicative],
  W.IsInvertedBy G → W.functorCategory C₁ adj.unit → W.HasLeftCalculusOfFractions
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instIsModularLattice : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M], IsModularLattice (LieSubmodule R L M)
-- Lean.Environment
/-- Map from declaration name to const for fast direct access.  -/
_private.Lean.Environment.0.Lean.AsyncConsts.map : Lean.AsyncConsts✝ → Lean.NameMap Lean.AsyncConst✝
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instCoeTypeForall : {α : Type u} → Coe (Type v) (α → Type v)
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_eq_top : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : UpperSet α} {t : UpperSet β},
  s ×ˢ t = ⊤ ↔ s = ⊤ ∨ t = ⊤
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.indicator_eq_sum_attach_single : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] {s : Finset α} (f : (a : α) → a ∈ s → M),
  Finsupp.indicator s f = ∑ x ∈ s.attach, fun₀ | ↑x => f ↑x ⋯
-- Mathlib.Data.TypeVec
TypeVec.lastFun_of_subtype : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} (p : α.Arrow (TypeVec.repeat (n + 1) Prop)),
  TypeVec.lastFun (TypeVec.ofSubtype p) = id
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RiiSliceData : Type u → Type v → Type (max u v)
-- Mathlib.Algebra.Category.CommBialgCat
/-- The category of commutative `R`-bialgebras and their morphisms.  -/
CommBialgCat : (R : Type u) → [CommRing R] → Type (max u (v + 1))