mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.CardinalInter
Filter.EventuallyLE.cardinal_iInter : ∀ {ι α : Type u} {c : Cardinal.{u}} {l : Filter α} [CardinalInterFilter l c] {s t : ι → Set α},
  Cardinal.mk ι < c → (∀ (i : ι), s i ≤ᶠ[l] t i) → ⋂ i, s i ≤ᶠ[l] ⋂ i, t i
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.instReprHeap : {α : Type u_1} → [Repr α] → Repr (Batteries.BinomialHeap.Imp.Heap α)
-- Mathlib.CategoryTheory.Functor.TypeValuedFlat
/-- Given a functor `F : C ⥤ Type w`, an object `X : C` and `x : F.obj X`,
this is the subfunctor of the functor `Over.forget X ⋙ F : Over X ⥤ Type w`
which sends an object of `Over X` corresponding to a morphism `f : Y ⟶ X`
to the subset of `F.obj Y` consisting of those elements `y : F.obj Y`
such that `F.map f y = x`.  -/
CategoryTheory.FunctorToTypes.fromOverSubfunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type w)) →
      {X : C} → F.obj X → CategoryTheory.Subfunctor ((CategoryTheory.Over.forget X).comp F)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_map_of_mem : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] (f : L.Hom M N)
  {S : L.Substructure M} {x : M}, x ∈ S → f x ∈ FirstOrder.Language.Substructure.map f S
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The product of measurable functions is measurable.  -/
Measurable.tprod : ∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [SecondCountableTopology E]
  [inst_5 : MeasurableSpace E] [BorelSpace E] [MeasurableMul₂ E] [Countable ι] {L : SummationFilter ι} [L.NeBot]
  [L.filter.IsCountablyGenerated] {f : ι → X → E},
  (∀ (i : ι), Measurable (f i)) → Measurable fun x => ∏'[L] (i : ι), f i x
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.foldM_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {ps : Std.Do.PostShape} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''}
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m] [inst_3 : Monad n] [inst_4 : Monad o]
  [LawfulMonad m] [LawfulMonad n] [LawfulMonad o] [inst_8 : Std.Do.WPMonad o ps] [inst_9 : Std.IteratorLoop α m n]
  [inst_10 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m n] [Std.LawfulIteratorLoop α m o]
  [inst_13 : MonadLiftT m n] [inst_14 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Std.IterM m β}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let __x ← liftM (f b).run
          match __x with
            | some c => g d c
            | x => pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.IterM.filterMapWithPostcondition f it) ⦃Q⦄
-- Mathlib.Probability.Kernel.Basic
/-- In a countable space with measurable singletons, every function `α → MeasureTheory.Measure β`
defines a kernel.  -/
ProbabilityTheory.Kernel.ofFunOfCountable : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {x : MeasurableSpace β} →
        [Countable α] → [MeasurableSingletonClass α] → (α → MeasureTheory.Measure β) → ProbabilityTheory.Kernel α β
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_extract : ∀ {a : ByteArray} {i j k l : ℕ}, (a.extract i j).extract k l = a.extract (i + k) (min (i + l) j)
-- Mathlib.Algebra.GroupWithZero.ULift
ULift.groupWithZero : {α : Type u} → [GroupWithZero α] → GroupWithZero (ULift.{u_1, u} α)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.isClosed : {α : Type} → Std.CloseableChannel.Bounded✝ α → BaseIO Bool
-- Init.System.ST
/-- Atomically modifies a mutable reference cell by replacing its contents with the result of a function
call that simultaneously computes a value to return.
 -/
ST.Ref.modifyGet : {σ : Type} → {m : Type → Type} → [MonadLiftT (ST σ) m] → {α β : Type} → ST.Ref σ α → (α → β × α) → m β
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- **Alias** of `thickenedIndicatorAux_mono_infEDist`. -/
thickenedIndicatorAux_mono_infEdist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) {E : Set α} {x y : α},
  Metric.infEDist x E ≤ Metric.infEDist y E → thickenedIndicatorAux δ E y ≤ thickenedIndicatorAux δ E x
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrable_cexp_neg_mul_sq : ∀ {b : ℂ}, 0 < b.re → MeasureTheory.Integrable (fun x => Complex.exp (-b * ↑x ^ 2)) MeasureTheory.volume
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mulPosStrictMono_iff_mulPosReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α], MulPosStrictMono α ↔ MulPosReflectLE α
-- Init.Data.String.OrderInstances
String.Pos.Raw.instLinearOrderPackage : Std.LinearOrderPackage String.Pos.Raw
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.zsmul_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] (r : ℤ)
  (f : BoundedContinuousFunction α β) (v : α), (r • f) v = r • f v
-- Mathlib.Data.Ordmap.Invariants
Ordnode.node4R.eq_1 : ∀ {α : Type u_1} (x : Ordnode α) (x_1 x_2 : α) (x_3 : Ordnode α) (size : ℕ) (ml : Ordnode α) (y : α) (mr : Ordnode α),
  x.node4R x_1 (Ordnode.node size ml y mr) x_2 x_3 = (x.node' x_1 ml).node' y (mr.node' x_2 x_3)
-- Mathlib.Algebra.GroupWithZero.Opposite
MulOpposite.instIsLeftCancelMulZeroOfIsRightCancelMulZero : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [IsRightCancelMulZero α], IsLeftCancelMulZero αᵐᵒᵖ
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy) (n : ℕ) (i : Fin (n + 1)) {Z : C} (h : X.left.obj (Opposite.op { len := n + 1 + 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.s n) (CategoryTheory.CategoryStruct.comp (X.left.σ i.succ) h) =
    CategoryTheory.CategoryStruct.comp (X.left.σ i) (CategoryTheory.CategoryStruct.comp (self.s (n + 1)) h)
-- Std.Data.TreeMap.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeMap.getKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → α → α
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (self.s n) (X.left.δ 0) =
    CategoryTheory.CategoryStruct.id (X.left.obj (Opposite.op { len := n }))
-- Mathlib.Topology.Sion
/-- From lower semicontinuity of `f(·, y)`, deduce that `sublevelLeft` sets are closed  -/
_private.Mathlib.Topology.Sion.0.Sion.isClosed_sublevelLeft : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E],
  (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) → ∀ (b : β) (y : ↑Y), IsClosed (Sion.sublevelLeft✝ X f b ↑y)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_mod_omega0 : ∀ (n : ℕ), ↑n % Ordinal.omega0 = ↑n
-- Mathlib.Data.List.Basic
List.left_le_of_mem_range' : ∀ {a b s x : ℕ}, x ∈ List.range' a b s → a ≤ x
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.lipschitzOnWith_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] {𝔖 : Set (Set α)}
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Finite ↑𝔖] {f : γ → UniformOnFun α β 𝔖} {K : NNReal} {s : Set γ},
  LipschitzOnWith K f s ↔ ∀ c ∈ ⋃₀ 𝔖, LipschitzOnWith K (fun x => (UniformOnFun.toFun 𝔖) (f x) c) s
-- Mathlib.NumberTheory.Padics.Complex
/-- `ℂ_[p]` is the field of `p`-adic complex numbers.  -/
«termℂ_[_]» : Lean.ParserDescr
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformation.label : Lean.Lsp.ParameterInformation → Lean.Lsp.ParameterInformationLabel
-- Mathlib.Tactic.Linarith.Parsing
/-- `1` is represented as the singleton sum of the monomial `Monom.one` with coefficient 1.  -/
Mathlib.Tactic.Linarith.Sum.one : Mathlib.Tactic.Linarith.Sum
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_rel : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {v : α → M} {xs : Fin l → M}
  {k : ℕ} {R : L.Relations k} {ts : Fin k → L.Term (α ⊕ Fin l)},
  (R.boundedFormula ts).Realize v xs ↔
    FirstOrder.Language.Structure.RelMap R fun i => FirstOrder.Language.Term.realize (Sum.elim v xs) (ts i)
-- Mathlib.CategoryTheory.Category.Cat
/-- The 1-morphism in `Cat` corresponding to a functor.  -/
CategoryTheory.Functor.toCatHom : {C D : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Category.{v, u} D] →
      CategoryTheory.Functor C D → (CategoryTheory.Cat.of C ⟶ CategoryTheory.Cat.of D)
-- Mathlib.Analysis.RCLike.Basic
RCLike.toStarRing : {K : semiOutParam (Type u_1)} → [self : RCLike K] → StarRing K
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt.0.UInt64.fromExpr : Lean.Expr → Lean.Meta.SimpM (Option UInt64)
-- Mathlib.Tactic.GCongr.Core
/-- Run the discharger for main goals.  -/
_private.Mathlib.Tactic.GCongr.Core.0.Mathlib.Tactic.GCongr.dischargeMain : Lean.MVarId → Mathlib.Tactic.GCongr.GCongrM Bool
-- Mathlib.Algebra.Group.Defs
AddCommGroup.toAddCommMonoid : {G : Type u} → [self : AddCommGroup G] → AddCommMonoid G
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.coe_desc : ∀ {X : Type u_5} {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace X] (f : X → α) (g : α → β)
  (h : LocallyConstant X β) (cond : g ∘ f = ⇑h) (inj : Function.Injective g), ⇑(LocallyConstant.desc f h cond inj) = f
-- Mathlib.Order.Category.LinOrd
/-- Constructs an equivalence between linear orders from an order isomorphism between them.  -/
LinOrd.Iso.mk : {α β : LinOrd} → ↑α ≃o ↑β → (α ≅ β)
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialAt.congr : ∀ {𝕜 : 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 g : E → F} {x : E},
  CPolynomialAt 𝕜 f x → f =ᶠ[nhds x] g → CPolynomialAt 𝕜 g x
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  {γ₁ γ₂ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂}, γ₁ = γ₂ → γ₁.φK = γ₂.φK
-- Mathlib.Algebra.Group.AddChar
AddChar.nsmul_apply : ∀ {A : Type u_2} {M : Type u_3} [inst : AddMonoid A] [inst_1 : CommMonoid M] (ψ : AddChar A M) (n : ℕ) (a : A),
  (n • ψ) a = ψ a ^ n
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
dist_birkhoffAverage_birkhoffAverage_le : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] (𝕜 : Type u_3) [inst_1 : RCLike 𝕜]
  [inst_2 : NormedSpace 𝕜 E] (f : α → α) (g : α → E) (n : ℕ) (x y : α),
  dist (birkhoffAverage 𝕜 f g n x) (birkhoffAverage 𝕜 f g n y) ≤
    (∑ k ∈ Finset.range n, dist (g (f^[k] x)) (g (f^[k] y))) / ↑n
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.SeenCalls.mk.injEq : ∀ (calls : Array Lean.Expr) (seen : Std.HashSet (Lean.Name × Array Lean.Expr)) (calls_1 : Array Lean.Expr)
  (seen_1 : Std.HashSet (Lean.Name × Array Lean.Expr)),
  ({ calls := calls, seen := seen } = { calls := calls_1, seen := seen_1 }) = (calls = calls_1 ∧ seen = seen_1)
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
CategoryTheory.ShortComplex.FunctorEquivalence.inverse_obj_f : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)),
  ((CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).obj F).f =
    F.whiskerLeft CategoryTheory.ShortComplex.π₁Toπ₂
-- Init.Sym.Lemmas
Lean.Sym.UInt32.lt_eq_false : ∀ (a b : UInt32), decide (a < b) = false → (a < b) = False
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
mdifferentiableOn_continuousLinearMapCoordChange : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {E₁ : B → Type u_6} {E₂ : B → Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_9} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B]
  [inst_18 : FiberBundle F₁ E₁] [inst_19 : VectorBundle 𝕜 F₁ E₁] [inst_20 : FiberBundle F₂ E₂]
  [inst_21 : VectorBundle 𝕜 F₂ E₂] {e₁ e₁' : Bundle.Trivialization F₁ Bundle.TotalSpace.proj}
  {e₂ e₂' : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [ContMDiffVectorBundle 1 F₁ E₁ IB]
  [ContMDiffVectorBundle 1 F₂ E₂ IB] [inst_24 : MemTrivializationAtlas e₁] [inst_25 : MemTrivializationAtlas e₁']
  [inst_26 : MemTrivializationAtlas e₂] [inst_27 : MemTrivializationAtlas e₂'],
  MDiff[e₁.baseSet ∩ e₂.baseSet ∩ (e₁'.baseSet ∩ e₂'.baseSet)]
    (Bundle.Pretrivialization.continuousLinearMapCoordChange (RingHom.id 𝕜) e₁ e₁' e₂ e₂')
-- Init.Data.Array.Attach
Array.attachWith_map : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → β} {P : β → Prop} (H : ∀ b ∈ Array.map f xs, P b),
  (Array.map f xs).attachWith P H =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      (xs.attachWith (P ∘ f) ⋯)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.toUnfoldThms : Lean.Name → Array Lean.Name → Lean.Meta.SimpEntry
-- Aesop.Tree.State
Aesop.Rapp.isIrrelevantNoCache : Aesop.Rapp → BaseIO Bool
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.lift_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C} (a : W ⟶ Y) (b : W ⟶ Z)
  (h : autoParam (CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) _auto_80✝),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.lift a b h)
      (CategoryTheory.ChosenPullbacksAlong.fst f g) =
    a
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.mk'.injEq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α]
  (inner inner_1 : Quotient (Std.DHashMap.isSetoid α β)),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedCategory.whiskerRight_toNatTrans : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {𝒵 : CategoryTheory.BasedCategory 𝒮} {F G : CategoryTheory.BasedFunctor 𝒳 𝒴}
  (α : F ⟶ G) (H : CategoryTheory.BasedFunctor 𝒴 𝒵),
  (CategoryTheory.BasedCategory.whiskerRight α H).toNatTrans =
    CategoryTheory.Functor.whiskerRight α.toNatTrans H.toFunctor
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.ofIso_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {Y : C} (e : X ≅ Y),
  (P.ofIso e).π = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map e.inv) P.π
-- Std.Data.HashMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 -/
Std.HashMap.getD : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → α → β → β
-- Mathlib.Control.LawfulFix
/-- Intuitively, a fixed point operator `fix` is lawful if it satisfies `fix f = f (fix f)` for all
`f`, but this is inconsistent / uninteresting in most cases due to the existence of "exotic"
functions `f`, such as the function that is defined iff its argument is not, familiar from the
halting problem. Instead, this requirement is limited to only functions that are `Continuous` in the
sense of `ω`-complete partial orders, which excludes the example because it is not monotone
(making the input argument less defined can make `f` more defined).  -/
LawfulFix : (α : Type u_3) → [OmegaCompletePartialOrder α] → Type u_3
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.comp_homeomorph : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f → ∀ {E' : Type u_3} [inst_2 : TopologicalSpace E'] (g : E' ≃ₜ E), IsCoveringMap (f ∘ ⇑g)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.interSmaller.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l₁ l₂ : List ((a : α) × β a)),
  Std.Internal.List.interSmaller l₁ l₂ =
    List.foldl (fun sofar kv => Std.Internal.List.interSmallerFn l₁ sofar kv.fst) [] l₂
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_injective : ∀ {R : Type u_2} [inst : NonAssocSemiring R], Function.Injective Subsemiring.op
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.isTerminal : Lean.IR.FnBody → Bool
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.comp_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g⁻¹ h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g)⁻¹ h
-- Init.Prelude
Lean.Syntax.brecOn.go : {motive_1 : Lean.Syntax → Sort u} →
  {motive_2 : Array Lean.Syntax → Sort u} →
    {motive_3 : List Lean.Syntax → Sort u} →
      (t : Lean.Syntax) →
        ((t : Lean.Syntax) → t.below → motive_1 t) →
          ((t : Array Lean.Syntax) → Lean.Syntax.below_1 t → motive_2 t) →
            ((t : List Lean.Syntax) → Lean.Syntax.below_2 t → motive_3 t) → motive_1 t ×' t.below
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
/-- The `MulStruct` for `X.op` that is deduced from a `MulStruct` for the simplicial
set `X`.  -/
SSet.PtSimplex.MulStruct.op : {X : SSet} →
  {n : ℕ} →
    {x : X.obj (Opposite.op { len := 0 })} →
      {f g fg : X.PtSimplex n x} →
        {i : Fin n} →
          f.MulStruct g fg i →
            {j : Fin n} → autoParam (i.rev = j) SSet.PtSimplex.MulStruct.op._auto_1 → g.op.MulStruct f.op fg.op j
-- Init.Data.Bool
Bool.eq_false_of_le_false : ∀ {x : Bool}, x ≤ false → x = false
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.lcm_ndinsert : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α] (a : α)
  (s : Multiset α), (Multiset.ndinsert a s).lcm = lcm a s.lcm
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Finsupp.curryLinearEquiv.eq_1 : ∀ {α : Type u_9} {β : Type u_10} (R : Type u_11) {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M],
  Finsupp.curryLinearEquiv R =
    { toFun := Finsupp.curryAddEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := Finsupp.curryAddEquiv.invFun,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.inclusion.congr_simp : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K'), LieSubalgebra.inclusion h = LieSubalgebra.inclusion h
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.size : Lean.Meta.SynthInstance.ConsumerNode → ℕ
-- Mathlib.Tactic.CancelDenoms.Core
_private.Mathlib.Tactic.CancelDenoms.Core.0.Mathlib.Tactic.CancelDenoms.synthesizeUsingNormNum : (type : Q(Prop)) → Lean.MetaM Q(«$type»)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The type of arrows for the diagram indexing a pullback.  -/
CategoryTheory.Limits.WalkingCospan.Hom : CategoryTheory.Limits.WalkingCospan → CategoryTheory.Limits.WalkingCospan → Type
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso_hom_naturality_assoc : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (S₁.map F).HasHomology] [inst_8 : (S₂.map F).HasHomology]
  [inst_9 : F.PreservesLeftHomologyOf S₁] [inst_10 : F.PreservesLeftHomologyOf S₂] {Z : D} (h : F.obj S₂.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapHomologyIso F).hom h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso F).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) h)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey? k = none
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.mem_invSubmonoid_iff_exists_mk' : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (x : S), x ∈ IsLocalization.invSubmonoid M S ↔ ∃ m, IsLocalization.mk' S 1 m = x
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
Mathlib.Tactic.BicategoryLike.Normalize.Result.mk : Mathlib.Tactic.BicategoryLike.NormalizedHom →
  Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Normalize.Result
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.oset.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i : ℕ) (y : Lean.Compiler.LCNF.Arg pu)
  (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_7),
  sizeOf (Lean.Compiler.LCNF.Code.oset fvarId i y k h) = 1 + sizeOf fvarId + sizeOf i + sizeOf y + sizeOf k + sizeOf h
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.constantCoeff_C : ∀ {R : Type u} (σ : Type u_1) [inst : CommSemiring R] (r : R), MvPolynomial.constantCoeff (MvPolynomial.C r) = r
-- Mathlib.Data.Fintype.Card
/-- **Alias** of the forward direction of `Finite.injective_iff_surjective_of_equiv`. -/
Function.Injective.surjective_of_finite : ∀ {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (e : α ≃ β), Function.Injective f → Function.Surjective f
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.toContinuousLinearMap_injective : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂], Function.Injective LinearIsometry.toContinuousLinearMap
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_plift : ∀ (α : Type u_3), ENat.card (PLift α) = ENat.card α