mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.mapRange_smul' : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} {S : Type u_12} [inst : Zero M]
  [inst_1 : SMulZeroClass R M] [inst_2 : Zero N] [inst_3 : SMulZeroClass S N] {f : M → N} {hf : f 0 = 0} (c : R) (d : S)
  (v : α →₀ M), (∀ (x : M), f (c • x) = d • f x) → Finsupp.mapRange f hf (c • v) = d • Finsupp.mapRange f hf v
-- Mathlib.MeasureTheory.Measure.Haar.Unique
/-- **Uniqueness of left-invariant measures**:
Given two left-invariant measures which are finite
on compacts and regular, they coincide up to a multiplicative constant.  -/
MeasureTheory.Measure.isMulLeftInvariant_eq_smul_of_regular : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : μ'.IsMulLeftInvariant] [μ.Regular] [inst_9 : μ'.Regular],
  μ' = μ'.haarScalarFactor μ • μ
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.eventually_hasSum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → ∀ᶠ (y : E) in nhds 0, HasSum (fun n => (p n) fun x => y) (f (x + y))
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
/-- Note that this is not trivial as we don't assume that `f` is integrable.  -/
MeasureTheory.integral_condExp_le_of_ae_nonneg : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ᵐ[μ] f → ∫ (x : α), μ[f | m] x ∂μ ≤ ∫ (x : α), f x ∂μ
-- Mathlib.Analysis.Calculus.MeanValue
isLocallyConstant_of_fderiv_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {𝕜 : Type u_3} {G : Type u_4}
  [inst_2 : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → G},
  Differentiable 𝕜 f → (∀ (x : E), fderiv 𝕜 f x = 0) → IsLocallyConstant f
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorRightUnitor.congr_simp : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e e_1 : F.flip.obj Y ≅ CategoryTheory.Functor.id D),
  e = e_1 →
    ∀ [inst_5 : ∀ (X : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.obj X)]
      (p : J × I → J) (hp : ∀ (j : J), p (j, 0) = j) (X : CategoryTheory.GradedObject J D)
      [inst_6 :
        (((CategoryTheory.GradedObject.mapBifunctor F J I).obj X).obj
              ((CategoryTheory.GradedObject.single₀ I).obj Y)).HasMap
          p],
      CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e p hp X =
        CategoryTheory.GradedObject.mapBifunctorRightUnitor F Y e_1 p hp X
-- Mathlib.GroupTheory.Nilpotent
Subgroup.nilpotencyClass_le_of_upperCentralSeries_eq : ∀ {G : Type u_1} [inst : Group G] {a b : ℕ},
  a < b → Subgroup.upperCentralSeries G a = Subgroup.upperCentralSeries G b → Group.nilpotencyClass G ≤ a
-- Lean.Elab.Exception
Lean.Elab.isAbortExceptionId : Lean.InternalExceptionId → Bool
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- Auxiliary definition for `forgetToPresheafModuleCatObj`.  -/
PresheafOfModules.forgetToPresheafModuleCatObjMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      (X : Cᵒᵖ) →
        (hX : CategoryTheory.Limits.IsInitial X) →
          (M : PresheafOfModules R) →
            {Y Z : Cᵒᵖ} →
              (Y ⟶ Z) →
                (PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y ⟶
                  PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Z)
-- Mathlib.LinearAlgebra.Quotient.Basic
/-- Given modules `M`, `M₂` over a commutative ring, together with submodules `p ⊆ M`, `q ⊆ M₂`,
the natural map $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \} \to Hom(M/p, M₂/q)$ is linear.  -/
Submodule.mapQLinear : {R : Type u_1} →
  {M : Type u_2} →
    {M₂ : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup M₂] →
              [inst_4 : Module R M₂] →
                (p : Submodule R M) → (q : Submodule R M₂) → ↥(p.compatibleMaps q) →ₗ[R] M ⧸ p →ₗ[R] M₂ ⧸ q
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.Std.Do.PredTrans.pushExcept.match_1.eq_1 : ∀ {α ε : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.congr_mapMap : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p] (φ₁ φ₂ : X ⟶ Y),
  φ₁ = φ₂ → CategoryTheory.GradedObject.mapMap φ₁ p = CategoryTheory.GradedObject.mapMap φ₂ p
-- Mathlib.Tactic.Explode
/-- Core `explode` algorithm.

- `select` is a condition for which expressions to process
- `includeAllDeps` is whether to include dependencies even if they were filtered out.
  If `True`, then `none` is inserted for omitted dependencies
- `e` is the expression to process
- `depth` is the current abstraction depth
- `entries` is the table so far
- `start` is whether we are at the top-level of the expression, which
  causes lambdas to use `Status.sintro` to prevent a layer of nesting.
 -/
Mathlib.Explode.explodeCore : (Lean.Expr → Lean.MetaM Bool) →
  Bool →
    Lean.Expr →
      ℕ →
        Mathlib.Explode.Entries →
          optParam Bool false → Lean.MetaM (Option Mathlib.Explode.Entry × Mathlib.Explode.Entries)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.instIsEquivalenceLocalizationLift : ∀ {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] (L : CategoryTheory.Functor C D)
  {W : CategoryTheory.MorphismProperty C} [inst_2 : L.IsLocalization W],
  (CategoryTheory.Localization.Construction.lift L ⋯).IsEquivalence
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- If `f` is a collection of continuous linear maps, then the construction
`ContinuousMultilinearMap.compContinuousLinearMap`
sending a continuous multilinear map `g` to `g (f₁ ·, ..., fₙ ·)`
is continuous-linear in `g` and multilinear in `f₁, ..., fₙ`.  -/
ContinuousMultilinearMap.compContinuousLinearMapMultilinear : (𝕜 : Type u) →
  {ι : Type v} →
    (E : ι → Type wE) →
      (E₁ : ι → Type wE₁) →
        (G : Type wG) →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] →
                  [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)] →
                    [inst_5 : SeminormedAddCommGroup G] →
                      [inst_6 : NormedSpace 𝕜 G] →
                        MultilinearMap 𝕜 (fun i => E i →L[𝕜] E₁ i)
                          (ContinuousMultilinearMap 𝕜 E₁ G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.join_mono_left : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P P' Q : l},
  Lean.Order.PartialOrder.rel P P' → Lean.Order.PartialOrder.rel (Lean.Order.join P Q) (Lean.Order.join P' Q)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.surjOn_exp_neg_pi_pi : Set.SurjOn (⇑Circle.exp) (Set.Ioc (-Real.pi) Real.pi) Set.univ
-- Mathlib.Analysis.Normed.Module.Span
ContinuousLinearEquiv.coord_self : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (x : E) (h : x ≠ 0), (ContinuousLinearEquiv.coord 𝕜 x h) ⟨x, ⋯⟩ = 1
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instOrdLeanDiagnosticTag : Ord Lean.Lsp.LeanDiagnosticTag
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.toLocallyCompactSpace : ∀ {K : Type u_1} {inst : Field K} {inst_1 : ValuativeRel K} {inst_2 : TopologicalSpace K}
  [self : IsNonarchimedeanLocalField K], LocallyCompactSpace K
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- An element `b : F.obj A` defines a permutation of the fiber of `X` by projecting onto the
`F.map u b` factor.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.fiberPerm : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          {X A : C} →
            {u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd✝ F X} →
              {a : (F.obj A).obj} →
                (CategoryTheory.ConcreteCategory.hom (F.map u)) a =
                    CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X →
                  [CategoryTheory.PreGaloisCategory.IsConnected A] → (F.obj A).obj → (F.obj X).obj ≃ (F.obj X).obj
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_lineMap_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, x ∈ s → y ∉ s → ∀ {t : R}, 0 < t → s.SSameSide ((AffineMap.lineMap x y) t) y
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.div : ∀ {α : Type u_1} {β : Type u_3} [inst : NormedField β] {t u v w : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l t u → Asymptotics.IsEquivalent l v w → Asymptotics.IsEquivalent l (t / v) (u / w)
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
ProbabilityTheory.hasIndepIncrements_iff_nat : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : T → Ω → E}
  [inst : Preorder T] [inst_1 : MeasurableSpace E] [inst_2 : Sub E],
  ProbabilityTheory.HasIndepIncrements X P ↔
    ∀ (t : ℕ → T), Monotone t → ProbabilityTheory.iIndepFun (fun i ω => X (t (i + 1)) ω - X (t i) ω) P
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.Normal.comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup N},
  H.Normal → ∀ (f : G →* N), (Subgroup.comap f H).Normal
-- Mathlib.Algebra.Group.Submonoid.Saturation
/-- `saturation` forms a `GaloisInsertion` with the forgetful functor
`SaturatedSubmonoid.toSubmonoid`.  -/
Submonoid.giSaturation : (M : Type u_1) → [inst : MulOneClass M] → GaloisInsertion Submonoid.saturation fun x => x.toSubmonoid
-- Std.Async.ContextAsync
Std.Async.ContextAsync.instFunctor : Functor Std.Async.ContextAsync
-- Mathlib.Data.Set.Basic
Set.nonempty_def : ∀ {α : Type u} {s : Set α}, s.Nonempty ↔ ∃ x, x ∈ s
-- Mathlib.Data.Multiset.Fold
Multiset.fold_cons_right : ∀ {α : Type u_1} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] (b a : α) (s : Multiset α),
  Multiset.fold op b (a ::ₘ s) = op (Multiset.fold op b s) a
-- Mathlib.Analysis.Normed.Ring.Units
/-- The `Ideal.closure` of a proper ideal in a normed ring with summable
geometric series is proper.  -/
Ideal.closure_ne_top : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (I : Ideal R), I ≠ ⊤ → I.closure ≠ ⊤
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_iInf_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {ι : Type u_5} {f : M →ₙ+ N},
  Function.Injective ⇑f →
    ∀ (S : ι → AddSubsemigroup M), AddSubsemigroup.comap f (⨅ i, AddSubsemigroup.map f (S i)) = iInf S
-- Mathlib.Logic.Equiv.Basic
Equiv.piCurry_apply : ∀ {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (x : (i : α) × β i) → γ x.fst x.snd),
  (Equiv.piCurry γ) f = Sigma.curry f
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_aleph_succ : ∀ (o : Ordinal.{u_1}), (Cardinal.aleph (Order.succ o)).IsRegular
-- Std.Data.TreeSet.Raw.Iterator
Std.TreeSet.Raw.toList.eq_1 : ∀ {α : Type u} {cmp : α → α → Ordering} (t : Std.TreeSet.Raw α cmp),
  t.toList = Std.DTreeMap.Internal.Impl.foldr (fun a x l => a :: l) ∅ t.inner.inner.inner
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] {d d' : Dᵒᵖ} {c c' : Cᵒᵖ} (f : d ⟶ d')
  (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f.unop g.unop =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g)
-- Mathlib.CategoryTheory.SmallObject.TransfiniteIteration
CategoryTheory.SmallObject.SuccStruct.arrowMk_iterationFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Φ : CategoryTheory.SmallObject.SuccStruct C) {J : Type w}
  [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] (i₁ i₂ : J) (h₁₂ : i₁ ≤ i₂) {j : J} (iter : Φ.Iteration j)
  (hj : i₂ ≤ j),
  CategoryTheory.Arrow.mk ((Φ.iterationFunctor J).map (CategoryTheory.homOfLE h₁₂)) =
    CategoryTheory.Arrow.mk (iter.F.map (CategoryTheory.homOfLE h₁₂))
-- Init.Data.UInt.Lemmas
UInt32.toUSize_sub : ∀ (a b : UInt32), (a - b).toUSize = (a.toUSize - b.toUSize) % 4294967296
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuousConstSMul.uniformContinuous_const_smul : ∀ {M : Type v} {X : Type x} {inst : UniformSpace X} {inst_1 : SMul M X} [self : UniformContinuousConstSMul M X] (c : M),
  UniformContinuous fun x => c • x
-- Lean.Meta.Tactic.Grind.ProveEq
_private.Lean.Meta.Tactic.Grind.ProveEq.0.Lean.Meta.Grind.AbstractM.Context.mk : ℕ → Lean.Meta.Grind.AbstractM.Context✝
-- Mathlib.Topology.Constructions.SumProd
/-- If `Sum.elim f g` is an inducing map, then so is `f`.  -/
Topology.IsInducing.sumElim_left : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, Topology.IsInducing (Sum.elim f g) → Topology.IsInducing f
-- Mathlib.Data.Setoid.Partition
/-- membership invariance for `index`  -/
IndexedPartition.mem_index : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (self : IndexedPartition s) (x : α), x ∈ s (self.index x)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardNatTrans_app_val_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S)
  (α : F ⟶ G) (X : SheafOfModules S) (U : Cᵒᵖ) (x : ↑(((SheafOfModules.pushforward φ).obj X).val.obj U)),
  (CategoryTheory.ConcreteCategory.hom (((SheafOfModules.pushforwardNatTrans φ α).app X).val.app U)) x =
    (CategoryTheory.ConcreteCategory.hom (X.val.map (α.app (Opposite.unop U)).op)) x
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.abelian_radical_of_hasTrivialRadical : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.HasTrivialRadical R L], IsLieAbelian ↥(LieAlgebra.radical R L)
-- Mathlib.NumberTheory.SumTwoSquares
/-- If `-1` is a square modulo coprime natural numbers `m` and `n`, then `-1` is also
a square modulo `m*n`.  -/
ZMod.isSquare_neg_one_mul : ∀ {m n : ℕ}, m.Coprime n → IsSquare (-1) → IsSquare (-1) → IsSquare (-1)
-- Mathlib.Order.Filter.Map
Filter.comap_inf : ∀ {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β},
  Filter.comap m (g₁ ⊓ g₂) = Filter.comap m g₁ ⊓ Filter.comap m g₂
-- Mathlib.Geometry.Convex.Cone.DualFinite
/-- The top cone is dually finitely generated.  -/
PointedCone.DualFG.top : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R}, PointedCone.DualFG p ⊤
-- Mathlib.Data.Stream.Init
Stream'.drop_drop : ∀ {α : Type u} (n m : ℕ) (s : Stream' α), Stream'.drop n (Stream'.drop m s) = Stream'.drop (m + n) s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k},
  (t.insertIfNew k v).maxKey! = t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.ofBijective_apply : ∀ {F : Type u_1} {A : Type u_3} {B : Type u_4} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : FunLike F A B]
  [inst_5 : NonUnitalRingHomClass F A B] [inst_6 : NonUnitalStarRingHomClass F A B] {f : F} (hf : Function.Bijective ⇑f)
  (a : A), (StarRingEquiv.ofBijective f hf) a = f a
-- Mathlib.Tactic.Order.ToInt
Mathlib.Tactic.Order.ToInt.toInt_nle_toInt : ∀ {α : Type u_1} [inst : LinearOrder α] {n : ℕ} (val : Fin n → α) (i j : Fin n),
  ¬Mathlib.Tactic.Order.ToInt.toInt val i ≤ Mathlib.Tactic.Order.ToInt.toInt val j ↔ ¬val i ≤ val j
-- Mathlib.Data.WSeq.Defs
/-- Calculate one step of computation  -/
Stream'.WSeq.compute : {α : Type u} → Stream'.WSeq α → Stream'.WSeq α
-- Mathlib.RingTheory.Int.Basic
Int.Prime.dvd_pow : ∀ {n : ℤ} {k p : ℕ}, Nat.Prime p → ↑p ∣ n ^ k → p ∣ n.natAbs
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.encard_sdiff_comm : ∀ {α : Type u_1} {M : Matroid α} {B₁ B₂ : Set α}, M.IsBase B₁ → M.IsBase B₂ → (B₁ \ B₂).encard = (B₂ \ B₁).encard
-- Lean.Data.Options
Lean.instInhabitedOptionDecl.default : Lean.OptionDecl
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.eta_inv_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T),
  f.eta.inv.right = CategoryTheory.CategoryStruct.id f.right
-- Mathlib.Algebra.Algebra.Defs
Algebra.algebraMap_self : ∀ {R : Type u} [inst : CommSemiring R], algebraMap R R = RingHom.id R
-- Mathlib.RingTheory.Invariant.Basic
/-- For any domain `k` containing `B ⧸ Q`,
any endomorphism of `k` can be restricted to an endomorphism of `B ⧸ Q`.
 -/
Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under : ∀ {A : Type u_1} {B : Type u_2} {k : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  (G : Type u_4) [Finite G] [inst_4 : Group G] [inst_5 : MulSemiringAction G B] [Algebra.IsInvariant A B G]
  (P : Ideal A) (Q : Ideal B) [inst_7 : Q.LiesOver P] [inst_8 : CommRing k] [inst_9 : Algebra (A ⧸ P) k]
  [inst_10 : Algebra (B ⧸ Q) k] [IsScalarTower (A ⧸ P) (B ⧸ Q) k] [IsDomain k] [FaithfulSMul (B ⧸ Q) k]
  (σ : k ≃ₐ[A ⧸ P] k), ∃ τ, ∀ (x : B ⧸ Q), (algebraMap (B ⧸ Q) k) (τ x) = σ ((algebraMap (B ⧸ Q) k) x)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.sumArrowEquivProdArrow_symm_apply : ∀ {α : Type u_2} {β : Type u_3} {R : Type u_4} [inst : NonAssocSemiring R] (x : (α → R) × (β → R)),
  (RingEquiv.sumArrowEquivProdArrow α β R).symm x = (Equiv.sumArrowEquivProdArrow α β R).symm x
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] {f : BoundedLatticeHom α β},
  Monotone (BooleanSubalgebra.map f)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_iSup_ideal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {γ : Sort u_3} (I : γ → Ideal A),
  ProjectiveSpectrum.zeroLocus 𝒜 ↑(⨆ i, I i) = ⋂ i, ProjectiveSpectrum.zeroLocus 𝒜 ↑(I i)
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instAssociativeHAdd : ∀ (α : Type u) [inst : Lean.Grind.CommSemiring α], Std.Associative fun x1 x2 => x1 + x2
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.popScope : {α β σ : Type} → Lean.ScopedEnvExtension α β σ → Lean.Environment → Lean.Environment
-- Mathlib.Topology.Category.TopCat.Limits.Konig
_private.Mathlib.Topology.Category.TopCat.Limits.Konig.0.TopCat.FiniteDiagram : (J : Type u) → [CategoryTheory.SmallCategory J] → Type u
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- A space is locally path-connected iff all path components of open subsets are open.  -/
locallyPathConnectedSpace_iff_isOpen_pathComponentIn : ∀ {X : Type u_4} [inst : TopologicalSpace X],
  LocallyPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → IsOpen (pathComponentIn u x)
-- Mathlib.Tactic.Linter.FindDeprecations
/-- `since` is the date when the declaration was deprecated.  -/
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.since : Mathlib.Tactic.DeprecationInfo✝ → String
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.any.eq_2 : ∀ (n : ℕ) (f : (i : ℕ) → i < n.succ → Bool), n.succ.any f = ((n.any fun i h => f i ⋯) || f n ⋯)
-- Mathlib.Topology.Separation.Hausdorff
isPreirreducible_iff_subsingleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {S : Set X}, IsPreirreducible S ↔ S.Subsingleton
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
ContMDiff.smoothSheafCommRingHom_hom_app_hom_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  {I : ModelWithCorners 𝕜 E H} {M : Type u} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] {R : Type u}
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] {EP : Type u_7} [inst_11 : NormedAddCommGroup EP]
  [inst_12 : NormedSpace 𝕜 EP] {HP : Type u_8} [inst_13 : TopologicalSpace HP] (IP : ModelWithCorners 𝕜 EP HP)
  (P : Type u) [inst_14 : TopologicalSpace P] [inst_15 : ChartedSpace HP P] [inst_16 : CommRing R]
  [inst_17 : ContMDiffRing I (↑⊤) R] (f : M → P) (hf : ContMDiff IM IP (↑⊤) f)
  (U : (TopologicalSpace.Opens ↑(TopCat.of P))ᵒᵖ) (a : (smoothSheaf IP I P R).obj.obj U),
  (CommRingCat.Hom.hom ((ContMDiff.smoothSheafCommRingHom IP P f hf).hom.app U)) a =
    (CategoryTheory.ConcreteCategory.hom ((ContMDiff.smoothSheafHom IP P f hf).hom.app U)) a
-- Mathlib.RepresentationTheory.Equiv
Representation.finsuppTensorLeft_apply_tmul : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {W : Type w'} [inst_2 : AddCommMonoid W]
  {k : Type u} [inst_3 : CommSemiring k] [inst_4 : Module k V] [inst_5 : Module k W] (σ : Representation k G V)
  (ρ : Representation k G W) {α : Type w'} [inst_6 : DecidableEq α] (f : α →₀ V) (w : W),
  (σ.finsuppTensorLeft ρ α) (f ⊗ₜ[k] w) = f.sum fun i v => fun₀ | i => v ⊗ₜ[k] w
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top : ∀ {X : AlgebraicGeometry.Scheme}, AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal ⊤ = X.nilradical
-- Mathlib.Data.List.TakeWhile
_private.Mathlib.Data.List.TakeWhile.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()