mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and
`L/K` is an algebraic extension, then the spectral norm on `L` is multiplicative.  -/
spectralAlgNorm_mul : ∀ {K : Type u} [inst : NontriviallyNormedField K] {L : Type v} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Algebra.IsAlgebraic K L] [hu : IsUltrametricDist K] [CompleteSpace K] (x y : L),
  (spectralAlgNorm K L) (x * y) = (spectralAlgNorm K L) x * (spectralAlgNorm K L) y
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.liftToTerminalUnique_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (hZ : CategoryTheory.Limits.IsTerminal Z)
  (G : CategoryTheory.Functor (CategoryTheory.WithTerminal C) D) (h : CategoryTheory.WithTerminal.incl.comp G ≅ F)
  (hG : G.obj CategoryTheory.WithTerminal.star ≅ Z) (X : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.liftToTerminalUnique F hZ G h hG).hom.app X =
    (match X with
      | CategoryTheory.WithTerminal.of x => h.app x
      | CategoryTheory.WithTerminal.star => hG).hom
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
/-- the predicate of objects that are `≤ n` for `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.le : {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] →
              CategoryTheory.Triangulated.TStructure C → ℤ → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes right covariance.
The lemma assuming left covariance is `Left.add_neg`.  -/
Right.add_neg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightStrictMono α] {a b : α},
  a < 0 → b < 0 → a + b < 0
-- Mathlib.CategoryTheory.Opposites
/-- Given a functor `F : Cᵒᵖ ⥤ Dᵒᵖ` we can take the "unopposite" functor `F : C ⥤ D`.
In informal mathematics no distinction is made between these.
 -/
CategoryTheory.Functor.unop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor Cᵒᵖ Dᵒᵖ → CategoryTheory.Functor C D
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_balance2 : ∀ {α : Type u_1} (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (l.balance2 v r).reverse = r.reverse.balance1 v l.reverse
-- Mathlib.Algebra.Category.FGModuleCat.Basic
/-- The coevaluation map is defined in `LinearAlgebra.coevaluation`.  -/
FGModuleCat.FGModuleCatCoevaluation : (K : Type u) →
  [inst : Field K] →
    (V : FGModuleCat K) →
      CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGModuleCat K) ⟶
        CategoryTheory.MonoidalCategoryStruct.tensorObj V (FGModuleCat.FGModuleCatDual K V)
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic absolute value of an integer is `≤ 1`.  -/
NumberField.HeightOneSpectrum.adicAbv_intCast_le_one : ∀ (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)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (n : ℤ), (NumberField.HeightOneSpectrum.adicAbv K v) ↑n ≤ 1
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.objEquiv_apply_snd : ∀ {p q n : ℕ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n }))
  (i : Fin (n + 1)), ((SSet.prodStdSimplex.objEquiv x) i).2 = x.2 i
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil.eq_def : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {v w : V} (x : G.Walk v w) (x_1 : V) (x_2 : x_1 ∈ x.support),
  x.takeUntil x_1 x_2 =
    match w, x, x_1, x_2 with
    | .(v), SimpleGraph.Walk.nil, u, h => ⋯.mpr SimpleGraph.Walk.nil
    | w, SimpleGraph.Walk.cons r p, u, h =>
      if hx : v = u then hx ▸ SimpleGraph.Walk.nil else SimpleGraph.Walk.cons r (p.takeUntil u ⋯)
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.neg_iff : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp (-f) p ↔ Memℓp f p
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_lt_div_left : ∀ {a b c : ENNReal}, a ≠ 0 → a ≠ ⊤ → c < b → a / b < a / c
-- Mathlib.Algebra.Group.Units.Basic
divp_eq_iff_mul_eq : ∀ {α : Type u} [inst : Monoid α] {x : α} {u : αˣ} {y : α}, x /ₚ u = y ↔ y * ↑u = x
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.mkDerivation_apply : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (Polynomial R) A] [inst_4 : IsScalarTower R (Polynomial R) A] (a : A) (f : Polynomial R),
  ((Polynomial.mkDerivation R) a) f = Polynomial.derivative f • a
-- Mathlib.Logic.IsEmpty.Basic
not_isEmpty_iff : ∀ {α : Sort u_1}, ¬IsEmpty α ↔ Nonempty α
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that
`f(S) ⊆ Nˣ`, for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`, we have
`f x₁ * (f y₁)⁻¹ = f x₂ * (f y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁)`.  -/
Submonoid.LocalizationMap.mul_inv : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
  (h : ∀ (y : ↥S), IsUnit (f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S},
  f x₁ * ↑((IsUnit.liftRight (f.domRestrict S) h) y₁)⁻¹ = f x₂ * ↑((IsUnit.liftRight (f.domRestrict S) h) y₂)⁻¹ ↔
    f (x₁ * ↑y₂) = f (x₂ * ↑y₁)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.get?.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (t t_1 : Std.DTreeMap.Internal.Impl α β),
  t = t_1 → ∀ (k : α), t.get? k = t_1.get? k
-- Init.Meta.Defs
Lean.version.patch : ℕ
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.coe_centralizer : ∀ {M : Type u_1} (S : Set M) [inst : AddMonoid M], ↑(AddSubmonoid.centralizer S) = S.addCentralizer
-- Mathlib.Topology.Category.TopCat.Sphere
/-- The inclusion `∂𝔻 n ⟶ 𝔻 n` of the boundary of the `n`-disk.  -/
TopCat.diskBoundaryInclusion : (n : ℕ) → TopCat.diskBoundary n ⟶ TopCat.disk n
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.of_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : C} (i : P ≅ Q),
  CategoryTheory.Injective P → CategoryTheory.Injective Q
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : SizeOf C] (X : C) [addMon : CategoryTheory.AddMonObj X],
  sizeOf { X := X, addMon := addMon } = 1 + sizeOf X + sizeOf addMon
-- Std.Time.Format.Modifier
Std.Time.instReprFraction.repr : Std.Time.Fraction → ℕ → Std.Format
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- An open null set w.r.t. an `IsOpenPosMeasure` is empty.  -/
IsOpen.eq_empty_of_measure_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] {m : MeasurableSpace X} {μ : MeasureTheory.Measure X} [μ.IsOpenPosMeasure]
  {U : Set X}, IsOpen U → μ U = 0 → U = ∅
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.op_closure : ∀ {M : Type u_2} [inst : Add M] (s : Set M),
  (AddSubsemigroup.closure s).op = AddSubsemigroup.closure (AddOpposite.unop ⁻¹' s)
-- Mathlib.CategoryTheory.Presentable.Finite
/-- `IsFinitelyPresentable` as an `ObjectProperty` on `C`. This is sometimes called "compact".  -/
CategoryTheory.ObjectProperty.isFinitelyPresentable : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
isIntegral_of_noetherian : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B],
  IsNoetherian R B → ∀ (x : B), IsIntegral R x
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_self : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.relIndex H = 1
-- Mathlib.Data.Finset.Erase
Finset.mem_erase_of_ne_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ≠ b → a ∈ s → a ∈ s.erase b
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits
CategoryTheory.Enriched.HasConicalLimit.of_equiv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {J' : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J'] (V : Type u') [inst_2 : CategoryTheory.Category.{v', u'} V]
  [inst_3 : CategoryTheory.MonoidalCategory V] {C : Type u} [inst_4 : CategoryTheory.Category.{v, u} C]
  [inst_5 : CategoryTheory.EnrichedOrdinaryCategory V C] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Enriched.HasConicalLimit V F] (G : CategoryTheory.Functor J' J) [G.IsEquivalence],
  CategoryTheory.Enriched.HasConicalLimit V (G.comp F)
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_range_add_sum_Ico : ∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → M) {m n : ℕ},
  m ≤ n → ∑ k ∈ Finset.range m, f k + ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range n, f k
-- Mathlib.Algebra.Group.Prod
MulHom.prod_apply : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P) (x : M), (f.prod g) x = (f x, g x)
-- Init.Control.Lawful.Instances
ExceptT.run_orElse : ∀ {m : Type u_1 → Type u_2} {ε α : Type u_1} [inst : Monad m] [LawfulMonad m] (x : ExceptT ε m α)
  (h : Unit → ExceptT ε m α),
  (OrElse.orElse x h).run = do
    let r ← x.run
    match r with
      | Except.ok a => pure (Except.ok a)
      | Except.error a => (h ()).run
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_sub_toENNReal : ∀ (r : ENNReal) (n : ℕ∞), ⌈r - ↑n⌉ₑ = ⌈r⌉ₑ - n
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.inst.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N],
  AddMonoid.Coprod.inst =
    { toAdd := AddMonoid.Coprod.instAddZeroClass.toAdd, add_assoc := ⋯,
      toZero := AddMonoid.Coprod.instAddZeroClass.toZero, zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto,
      nsmul_zero := ⋯, nsmul_succ := ⋯ }
-- Mathlib.Order.UpperLower.CompleteLattice
/-- See Note [custom simps projection].  -/
UpperSet.Simps.coe : {α : Type u_1} → [inst : LE α] → UpperSet α → Set α
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_below_le`. -/
Ideal.ramificationIdx'_below_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.IsPrime] [r.LiesOver q] [Module.Finite R T] [Module.Flat S T], q.ramificationIdx R ≤ r.ramificationIdx R
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.Code.instantiateValueLevelParams.instLetValue : List Lean.Name →
  List Lean.Level →
    Lean.Compiler.LCNF.LetValue Lean.Compiler.LCNF.Purity.pure →
      Lean.Compiler.LCNF.LetValue Lean.Compiler.LCNF.Purity.pure
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Construct an isomorphism of additive monoid objects by giving a additive monoid
isomorphism between the underlying objects.  -/
CategoryTheory.AddMon.mkIso' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : C} →
        [inst_2 : CategoryTheory.AddMonObj M] →
          [inst_3 : CategoryTheory.AddMonObj N] →
            (e : M ≅ N) →
              [CategoryTheory.IsAddMonHom e.hom] → { X := M, addMon := inst_2 } ≅ { X := N, addMon := inst_3 }
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.toFunctor_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : CategoryTheory.Bicategory.Strict B] [inst_3 : CategoryTheory.Bicategory.Strict C]
  (F : CategoryTheory.StrictPseudofunctor B C) (a : B), F.toFunctor.obj a = F.obj a
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_preimage_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (s : Set β),
  ⇑e.symm ⁻¹' ⇑e ⁻¹' s = s
-- Init.Data.Order.PackageFactories
Std.PartialOrderPackage.toIsPartialOrder : ∀ {α : Type u} [self : Std.PartialOrderPackage α], Std.IsPartialOrder α
-- Mathlib.Topology.UnitInterval
unitInterval.subtype_Ici_eq_Icc : ∀ (x : ↑unitInterval), Subtype.val ⁻¹' Set.Ici ↑x = Set.Icc x 1
-- Mathlib.CategoryTheory.Adjunction.Evaluation
CategoryTheory.evaluationRightAdjoint.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasProductsOfShape (a ⟶ b) D] (c c_1 : C),
  c = c_1 → CategoryTheory.evaluationRightAdjoint D c = CategoryTheory.evaluationRightAdjoint D c_1
-- Init.Data.List.Lemmas
List.foldrM_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {a : α} {l : List α}
  {f : α → β → m β} {b : β}, List.foldrM f b (a :: l) = List.foldrM f b l >>= f a
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.ComplexConfig.mk.inj : ∀ {out ctx : Type} {trigger : Option ctx → Lean.Syntax → Mathlib.TacticAnalysis.TriggerCondition ctx}
  {test : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → ctx → Lean.MVarId → Lean.Elab.Command.CommandElabM out}
  {tell : Lean.Syntax → List Lean.MVarId → ℕ → out → ℕ → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)}
  {out_1 ctx_1 : Type} {trigger_1 : Option ctx_1 → Lean.Syntax → Mathlib.TacticAnalysis.TriggerCondition ctx_1}
  {test_1 : Lean.Elab.ContextInfo → Lean.Elab.TacticInfo → ctx_1 → Lean.MVarId → Lean.Elab.Command.CommandElabM out_1}
  {tell_1 : Lean.Syntax → List Lean.MVarId → ℕ → out_1 → ℕ → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)},
  { out := out, ctx := ctx, trigger := trigger, test := test, tell := tell } =
      { out := out_1, ctx := ctx_1, trigger := trigger_1, test := test_1, tell := tell_1 } →
    out = out_1 ∧ ctx = ctx_1 ∧ trigger ≍ trigger_1 ∧ test ≍ test_1 ∧ tell ≍ tell_1
-- Mathlib.Order.GaloisConnection.Defs
GaloisInsertion.mk.inj : ∀ {α : Type u_2} {β : Type u_3} {inst : Preorder α} {inst_1 : Preorder β} {l : α → β} {u : β → α}
  {choice : (x : α) → u (l x) ≤ x → β} {gc : GaloisConnection l u} {le_l_u : ∀ (x : β), x ≤ l (u x)}
  {choice_eq : ∀ (a : α) (h : u (l a) ≤ a), choice a h = l a} {choice_1 : (x : α) → u (l x) ≤ x → β}
  {gc_1 : GaloisConnection l u} {le_l_u_1 : ∀ (x : β), x ≤ l (u x)}
  {choice_eq_1 : ∀ (a : α) (h : u (l a) ≤ a), choice_1 a h = l a},
  { choice := choice, gc := gc, le_l_u := le_l_u, choice_eq := choice_eq } =
      { choice := choice_1, gc := gc_1, le_l_u := le_l_u_1, choice_eq := choice_eq_1 } →
    choice = choice_1
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_div : ∀ (x y : ℝ), ↑(x / y) = ↑x / ↑y
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff : ∀ {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω]
  [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F]
  {ρ : MeasureTheory.Measure (α × Ω)} [inst_4 : MeasureTheory.IsFiniteMeasure ρ] {f : α × Ω → F},
  MeasureTheory.AEStronglyMeasurable f ρ →
    ((∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun ω => f (a, ω)) (ρ.condKernel a)) ∧
        MeasureTheory.Integrable (fun a => ∫ (ω : Ω), ‖f (a, ω)‖ ∂ρ.condKernel a) ρ.fst ↔
      MeasureTheory.Integrable f ρ)
-- Init.Data.SInt.Lemmas
ISize.add_comm : ∀ (a b : ISize), a + b = b + a
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.norm_sub_eq : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u v : ↥(unitary A)), ‖↑u - ↑v‖ = ‖↑(u * star v) - 1‖
-- Mathlib.Data.Part
Part.some_injective : ∀ {α : Type u_1}, Function.Injective Part.some
-- Mathlib.Topology.Separation.Profinite
/-- A locally compact Hausdorff space is totally disconnected
if and only if it is totally separated.  -/
loc_compact_t2_tot_disc_iff_tot_sep : ∀ {H : Type u_3} [inst : TopologicalSpace H] [LocallyCompactSpace H] [T2Space H],
  TotallyDisconnectedSpace H ↔ TotallySeparatedSpace H
-- Std.Data.ExtHashMap.Basic
/-- Computes the difference of the given hash maps.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.ExtHashMap.diff : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → Std.ExtHashMap α β → Std.ExtHashMap α β
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
MonotoneOn.map_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α} [WellFoundedLT α] {β : Type u_5}
  [inst_2 : ConditionallyCompleteLattice β] {f : α → β}, MonotoneOn f s → s.Nonempty → f (sInf s) = sInf (f '' s)