mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.jp.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {decl : Lean.Compiler.LCNF.FunDecl pu} {k : Lean.Compiler.LCNF.Code pu}
  {decl_1 : Lean.Compiler.LCNF.FunDecl pu} {k_1 : Lean.Compiler.LCNF.Code pu},
  Lean.Compiler.LCNF.Code.jp decl k = Lean.Compiler.LCNF.Code.jp decl_1 k_1 → decl = decl_1 ∧ k = k_1
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_subset_closure_image2 : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  {u : Set τ}, u ∈ f → omegaLimit f ϕ s ⊆ closure (Set.image2 ϕ u s)
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.baseChange_jacobian : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (T : Type u_1) [inst_3 : CommRing T] [inst_4 : Algebra R T] (P : Algebra.PreSubmersivePresentation R S ι σ)
  [inst_5 : Finite σ], (Algebra.PreSubmersivePresentation.baseChange T P).jacobian = 1 ⊗ₜ[R] P.jacobian
-- Mathlib.SetTheory.Cardinal.Aleph
/-- The Beth function is defined so that `beth 0 = ℵ₀`, `beth (succ o) = 2 ^ beth o`, and that for a
limit ordinal `o`, `beth o` is the supremum of `beth a` for `a < o`.

Assuming the generalized continuum hypothesis, which is undecidable in ZFC, we have `ℶ_ o = ℵ_ o`
for all ordinals.

For a version which starts at zero, see `Cardinal.preBeth`.  -/
Cardinal.beth : Ordinal.{u} → Cardinal.{u}
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.lift_one : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : MulOneClass β] (f : α →ₙ* β), (WithOne.lift f) 1 = 1
-- Mathlib.Analysis.Convex.Side
/-- If `x` and `y` lie off `s` and are displaced from points of `s` by multiples of a common
vector whose coefficients have nonnegative product, they are strictly on the same side of `s`.  -/
AffineSubspace.sSameSide_of_vsub_eq_smul : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing 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₁ p₂ : P} {m : V} {c₁ c₂ : R},
  p₁ ∈ s → p₂ ∈ s → x -ᵥ p₁ = c₁ • m → y -ᵥ p₂ = c₂ • m → 0 ≤ c₁ * c₂ → x ∉ s → y ∉ s → s.SSameSide x y
-- Mathlib.Computability.NFA
NFA.evalFrom_nil : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ), M.evalFrom S [] = S
-- Std.Time.DateTime.Timestamp
/-- Converts a `Timestamp` to nanoseconds as `Nanosecond.Offset`.
 -/
Std.Time.Timestamp.toNanosecondsSinceUnixEpoch : Std.Time.Timestamp → Std.Time.Nanosecond.Offset
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- If `1 ≤ n`, then `seminormFromConst_seq c f 1 n = 1`.  -/
seminormFromConst_seq_one : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f c ≠ 0 → IsPowMul ⇑f → ∀ (n : ℕ), 1 ≤ n → seminormFromConst_seq c f 1 n = 1
-- Mathlib.Order.Interval.Finset.Defs
BddAbove.finite_of_bddBelow : ∀ {α : Type u_3} [inst : Preorder α] [LocallyFiniteOrder α] {s : Set α}, BddAbove s → BddBelow s → s.Finite
-- Mathlib.Topology.DenseEmbedding
/-- A dense embedding is injective.  -/
IsDenseEmbedding.injective : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {e : α → β},
  IsDenseEmbedding e → Function.Injective e
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_lineMap_eq : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (p₀ p₁ : P) [inst_5 : TopologicalSpace R]
  [inst_6 : TopologicalSpace V] [inst_7 : ContinuousSMul R V] [inst_8 : ContinuousVAdd V P],
  ⇑(ContinuousAffineMap.lineMap p₀ p₁) = ⇑(AffineMap.lineMap p₀ p₁)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.zsmul_modEq_zero : ∀ {G : Type u_1} [inst : AddCommGroup G] {p : G} (z : ℤ), z • p ≡ 0 [PMOD p]
-- Std.Data.DTreeMap.Internal.Lemmas
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.tacticWf_trivial : Lean.ParserDescr
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher.mk.injEq : ∀ {ρ : Type} {pat : ρ} {s : String.Slice} (currPos currPos_1 : s.Pos),
  ({ currPos := currPos } = { currPos := currPos_1 }) = (currPos = currPos_1)
-- Mathlib.Data.Subtype
/-- An alternative version of `Subtype.exists`. This one is useful if Lean cannot figure out `q`
when using `Subtype.exists` from right to left.  -/
Subtype.exists' : ∀ {α : Sort u_1} {p : α → Prop} {q : (x : α) → p x → Prop}, (∃ x, ∃ (h : p x), q x h) ↔ ∃ x, q ↑x ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_le_size_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, t.size - 1 ≤ (Std.DTreeMap.Const.alter t k f).size
-- Mathlib.Data.ZMod.Basic
ZMod.natCast_eq_zero_iff : ∀ (a b : ℕ), ↑a = 0 ↔ b ∣ a
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.coeToRingHom : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {σ : Type u_6} →
        {τ : Type u_7} →
          [inst : Semiring A] →
            [inst_1 : Semiring B] →
              [inst_2 : SetLike σ A] → [inst_3 : SetLike τ B] → {𝒜 : ι → σ} → {ℬ : ι → τ} → CoeOut (𝒜 →+*ᵍ ℬ) (A →+* B)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.comp_eq_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A A' A'' : G.Coalgebra}
  (f : A ⟶ A') (g : A' ⟶ A''), CategoryTheory.Comonad.Coalgebra.Hom.comp f g = CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isInt_negOfNat : ∀ (m n : ℕ), Mathlib.Meta.NormNum.IsNat m n → Mathlib.Meta.NormNum.IsInt (Int.negOfNat m) (Int.negOfNat n)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.key : Lean.Lsp.SymbolKind
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F F_1 : CategoryTheory.Functor J C) (e_F : F = F_1) [inst_2 : CategoryTheory.Limits.HasColimit F],
  CategoryTheory.Limits.colimit F = CategoryTheory.Limits.colimit F_1
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Params.mk.injEq : ∀ (config : Lean.Grind.Config) (extensions : Lean.Meta.Grind.ExtensionStateArray)
  (extra : Lean.PArray Lean.Meta.Grind.EMatchTheorem) (extraInj : Lean.PArray Lean.Meta.Grind.InjectiveTheorem)
  (extraFacts : Lean.PArray Lean.Expr) (symPrios : Lean.Meta.Grind.SymbolPriorities) (norm : Lean.Meta.Simp.Context)
  (normProcs : Array Lean.Meta.Simprocs) (anchorRefs? : Option (Array Lean.Meta.Grind.AnchorRef))
  (config_1 : Lean.Grind.Config) (extensions_1 : Lean.Meta.Grind.ExtensionStateArray)
  (extra_1 : Lean.PArray Lean.Meta.Grind.EMatchTheorem) (extraInj_1 : Lean.PArray Lean.Meta.Grind.InjectiveTheorem)
  (extraFacts_1 : Lean.PArray Lean.Expr) (symPrios_1 : Lean.Meta.Grind.SymbolPriorities)
  (norm_1 : Lean.Meta.Simp.Context) (normProcs_1 : Array Lean.Meta.Simprocs)
  (anchorRefs?_1 : Option (Array Lean.Meta.Grind.AnchorRef)),
  ({ config := config, extensions := extensions, extra := extra, extraInj := extraInj, extraFacts := extraFacts,
        symPrios := symPrios, norm := norm, normProcs := normProcs, anchorRefs? := anchorRefs? } =
      { config := config_1, extensions := extensions_1, extra := extra_1, extraInj := extraInj_1,
        extraFacts := extraFacts_1, symPrios := symPrios_1, norm := norm_1, normProcs := normProcs_1,
        anchorRefs? := anchorRefs?_1 }) =
    (config = config_1 ∧
      extensions = extensions_1 ∧
        extra = extra_1 ∧
          extraInj = extraInj_1 ∧
            extraFacts = extraFacts_1 ∧
              symPrios = symPrios_1 ∧ norm = norm_1 ∧ normProcs = normProcs_1 ∧ anchorRefs? = anchorRefs?_1)
-- Init.System.ST
/-- Mutable reference cells that contain values of type `α`. These cells can read from and mutated in
the `ST σ` monad.
 -/
ST.Ref : Type → Type → Type
-- Mathlib.Data.Nat.Digits.Defs
Nat.sum_le_ofDigits : ∀ {p : ℕ} (L : List ℕ), 1 ≤ p → L.sum ≤ Nat.ofDigits p L
-- Std.Data.DTreeMap.Internal.WF.Lemmas
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.SameKeys.inner : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1} (sz : ℕ) (k : α) (v : β k) (v' : β' k)
  (r : Std.DTreeMap.Internal.Impl α β) (r' : Std.DTreeMap.Internal.Impl α β') (l : Std.DTreeMap.Internal.Impl α β)
  (l' : Std.DTreeMap.Internal.Impl α β'),
  r.SameKeys r' →
    l.SameKeys l' →
      (Std.DTreeMap.Internal.Impl.inner sz k v l r).SameKeys (Std.DTreeMap.Internal.Impl.inner sz k v' l' r')
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_left_K : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).left.K = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f)
-- Mathlib.Data.Ordmap.Invariants
/-- `Raised n m` means `m` is either equal or one up from `n`.  -/
Ordnode.Raised : ℕ → ℕ → Prop
-- Init.Data.List.Lemmas
List.filterMap_eq_nil_iff : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {l : List α}, List.filterMap f l = [] ↔ ∀ a ∈ l, f a = none
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.algebraMap_eq : ∀ {α : Type u_1} {R : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Semiring α]
  [inst_3 : Algebra R A] [inst_4 : Algebra A α] (S : Subalgebra R A), algebraMap (↥S) α = (algebraMap A α).comp ↑S.val
-- Mathlib.Algebra.WithConv
WithConv.toConv_add : ∀ {A : Type u_2} [inst : AddMonoid A] (x y : A), WithConv.toConv (x + y) = WithConv.toConv x + WithConv.toConv y
-- Mathlib.Topology.Category.TopCat.Sphere
TopCat.diskBoundaryInclusion.eq_1 : ∀ (n : ℕ),
  TopCat.diskBoundaryInclusion n =
    TopCat.ofHom
      {
        toFun := fun x =>
          match x with
          | { down := ⟨p, hp⟩ } => { down := ⟨p, ⋯⟩ },
        continuous_toFun := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_filter_key : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → Bool} {k fallback : α},
  (Std.ExtDHashMap.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.mk : {T : Type u_1} → {N : Type u_2} → N → List (Symbol T N) → ContextFreeRule T N
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.aestronglyMeasurable_zero_measure : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} (f : α → β),
  MeasureTheory.AEStronglyMeasurable f 0
-- Std.Data.HashSet.Raw
/-- Inserts the given element into the set. If the hash set already contains an element that is
equal (with regard to `==`) to the given element, then the hash set is returned unchanged.

Note: this non-replacement behavior is true for `HashSet` and `HashSet.Raw`.
The `insert` function on `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw` behaves
differently: it will overwrite an existing mapping.
 -/
Std.HashSet.Raw.insert : {α : Type u} → [BEq α] → [Hashable α] → Std.HashSet.Raw α → α → Std.HashSet.Raw α
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.refl_apply : ∀ (α : Type u_2) [inst : Mul α] [inst_1 : Add α] [inst_2 : LE α] (x : α), (OrderRingIso.refl α) x = x
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence_counitIso : ∀ {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₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂),
  (CategoryTheory.LocalizerMorphism.LeftResolution.opEquivalence Φ X₂).counitIso =
    CategoryTheory.Iso.refl
      ((CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor Φ (Opposite.op X₂)).rightOp.comp
        (CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂))
-- Mathlib.CategoryTheory.Adjunction.Triple
/-- Adjunction `G ⊣ H` of the adjoint triple `F ⊣ G ⊣ H`.  -/
CategoryTheory.Adjunction.Triple.adj₂ : {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] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            {H : CategoryTheory.Functor C D} → CategoryTheory.Adjunction.Triple F G H → (G ⊣ H)
-- Mathlib.Data.List.Basic
List.length_eraseIdx_add_one : ∀ {ι : Type u_1} {l : List ι} {i : ℕ}, i < l.length → (l.eraseIdx i).length + 1 = l.length
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM.Context.mk.injEq : ∀ (toIntId toIntId_1 : ℕ), ({ toIntId := toIntId } = { toIntId := toIntId_1 }) = (toIntId = toIntId_1)
-- Init.Omega.Constraint
_private.Init.Omega.Constraint.0.Lean.Omega.instToStringInt : ToString ℤ
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_target : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), (e.restr s).target = e.target ∩ ↑e.symm ⁻¹' interior s
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_dual : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {M : Matroid α} {hf : Set.InjOn f M.E}, (M.map f hf)✶ = M✶.map f hf
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.mk.sizeOf_spec : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  {S : AddGroupExtension N E G} [inst_3 : SizeOf N] [inst_4 : SizeOf E] [inst_5 : SizeOf G] (toAddMonoidHom : G →+ E)
  (rightInverse_rightHom : Function.RightInverse (↑toAddMonoidHom).toFun ⇑S.rightHom),
  sizeOf { toAddMonoidHom := toAddMonoidHom, rightInverse_rightHom := rightInverse_rightHom } =
    1 + sizeOf toAddMonoidHom
-- Mathlib.Analysis.RCLike.TangentCone
tangentConeAt_real_subset_isRCLikeNormedField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedSpace ℝ E] {s : Set E} {x : E},
  tangentConeAt ℝ s x ⊆ tangentConeAt 𝕜 s x
-- Mathlib.GroupTheory.Congruence.Basic
/-- Given a monoid homomorphism `f`, the induced homomorphism on the quotient by `f`'s kernel has
the same image as `f`.  -/
Con.kerLift_range_eq : ∀ {M : Type u_1} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass P] {f : M →* P},
  MonoidHom.mrange (Con.kerLift f) = MonoidHom.mrange f
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.mk : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Sym.SharedExprs
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasFDerivAt_iff_hasGradientAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {frechet : StrongDual 𝕜 F},
  HasFDerivAt f frechet x ↔ HasGradientAt f ((InnerProductSpace.toDual 𝕜 F).symm frechet) x
-- Mathlib.Data.Real.Pointwise
Real.smul_iInf_of_nonneg : ∀ {ι : Sort u_1} {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : MulActionWithZero α ℝ] [IsOrderedModule α ℝ] {a : α}, 0 ≤ a → ∀ (f : ι → ℝ), a • ⨅ i, f i = ⨅ i, a • f i
-- Std.Time.DateTime.PlainDateTime
/-- Returns the aligned week of the month for a `PlainDateTime`. Weeks are fixed 7-day slots
starting from day 1: days 1–7 are week 1, days 8–14 are week 2, etc.
 -/
Std.Time.PlainDateTime.alignedWeekOfMonth : Std.Time.PlainDateTime → Std.Time.Week.Aligned.Ordinal
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The subterm closure of a statement.  -/
Turing.TM1.stmts₁ : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → Turing.TM1.Stmt Γ Λ σ → Finset (Turing.TM1.Stmt Γ Λ σ)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Extension.extension : Lean.SimplePersistentEnvExtension Lean.Meta.Match.Extension.Entry Lean.Meta.Match.Extension.State
-- Lean.Meta.Sym.Util
/-- Debug helper: throws if any subexpression of the goal's target type is not in the table of maximally shared.  -/
Lean.MVarId.checkMaxShared : Lean.MVarId → optParam String "" → Lean.Meta.Sym.SymM Unit
-- Mathlib.Analysis.Normed.Group.Continuity
/-- See `tendsto_norm_one` for a version with full neighborhoods.  -/
tendsto_norm_nhdsNE_one : ∀ {E : Type u_4} [inst : NormedGroup E], Filter.Tendsto norm (nhdsWithin 1 {1}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- The constant functor `C ⥤ (D ⥤ C)` preserves limits.  -/
CategoryTheory.Limits.preservesLimits_const : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, v, max u' v, u, max (max (max u u') v) v'}
    (CategoryTheory.Functor.const D)
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.data_takeWhile : ∀ (p : Char → Bool) {s : Substring.Raw}, s.Valid → (s.takeWhile p).toString.toList = List.takeWhile p s.toString.toList
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_le_comap_of_le_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {K L : AddSubgroup N},
  K ≤ f.range → (AddSubgroup.comap f K ≤ AddSubgroup.comap f L ↔ K ≤ L)
-- Mathlib.Topology.Germ
/-- The map `Germ (𝓝 x) E → E` as a monotone ring homomorphism  -/
Filter.Germ.valueOrderRingHom : {X : Type u_4} →
  {E : Type u_5} →
    [inst : Semiring E] → [inst_1 : PartialOrder E] → [inst_2 : TopologicalSpace X] → {x : X} → (nhds x).Germ E →+*o E
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.epi_π_app : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (self : CategoryTheory.Abelian.LeftResolution ι) (X : A), CategoryTheory.Epi (self.π.app X)
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.quasiCompactCover_shrink_iff : ∀ {S : AlgebraicGeometry.Scheme} (E : CategoryTheory.PreZeroHypercover S),
  AlgebraicGeometry.QuasiCompactCover E.shrink ↔ AlgebraicGeometry.QuasiCompactCover E
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Real.sigmoid_monotone : Monotone Real.sigmoid
-- Mathlib.Order.Hom.Basic
/-- See Note [custom simps projection]. We give this manually so that we use `toFun` as the
projection directly instead.  -/
OrderHom.Simps.coe : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → α → β
-- Mathlib.Topology.IsLocalHomeomorph
isLocalHomeomorphOn_iff_isOpenEmbedding_restrict : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) {f : X → Y},
  IsLocalHomeomorphOn f s ↔ ∀ x ∈ s, ∃ U ∈ nhds x, Topology.IsOpenEmbedding (U.domRestrict f)
-- Mathlib.Algebra.Ring.IsFormallyReal
AddSubsemigroup.closure_mul_self : ∀ {R : Type u_1} [inst : AddMonoid R] [inst_1 : Mul R],
  AddSubsemigroup.closure {x | ∃ x_1, x_1 ≠ 0 ∧ x_1 * x_1 = x} = AddSubsemigroup.sumNonzeroSq R
-- Mathlib.Combinatorics.Hypergraph.Basic
Hypergraph.IsTrivial.isNonempty : ∀ {α : Type u_1} {H : Hypergraph α}, H.IsTrivial → H.IsNonempty
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- A pointwise right Kan extension is universal, i.e. it is a right Kan extension.  -/
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.isUniversal : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                {E : L.RightExtension F} →
                  E.IsPointwiseRightKanExtension → CategoryTheory.CostructuredArrow.IsUniversal E
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_le_size_insertMany_list : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {l : List ((a : α) × β a)}, (↑m).size ≤ (↑↑(m.insertMany l)).size
-- Init.Grind.Lemmas
Lean.Grind.Bool.or_eq_of_eq_false_right : ∀ {a b : Bool}, b = false → (a || b) = a
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_le : ∀ {α : Type u_2} {M : Type u_3} [inst : AddMonoid M] [inst_1 : PartialOrder M] [CanonicallyOrderedAdd M] {s : Set α}
  {f g : α → M}, (∀ a ∈ s, f a ≤ g a) → s.indicator f ≤ g
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- Associating to a continuous multilinear map in `0` variables the unique value it takes.  -/
ContinuousMultilinearMap.curry0 : {𝕜 : Type u} →
  {G : Type wG} →
    {G' : Type wG'} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] →
            [inst_3 : NormedAddCommGroup G'] → [inst_4 : NormedSpace 𝕜 G'] → (G [×0]→L[𝕜] G') → G'
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.coreToInt : Lean.Expr →
  Lean.Expr →
    Lean.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_pow : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] [Nontrivial R] (p : Polynomial R) (n : ℕ),
  (p ^ n).degree = n • p.degree
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_equiv_eq_comap_symm : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] [inst_7 : RingHomInvPair τ₂₁ τ₁₂] (e : M ≃ₛₗ[τ₁₂] M₂)
  (K : Submodule R M), Submodule.map (↑e) K = Submodule.comap (↑e.symm) K
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- Restriction of an element in the closure along a morphism.  -/
CategoryTheory.Precoverage.SubsheafClosure.restrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))} {Z W : C} (h : Z ⟶ W)
  {a : F.obj (Opposite.op W)},
  K.SubsheafClosure 𝒮 W a → K.SubsheafClosure 𝒮 Z ((CategoryTheory.ConcreteCategory.hom (F.map h.op)) a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.foldM_eq_foldlM_toList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  Std.HashMap.foldM f init m = List.foldlM (fun a b => f a b.1 b.2) init m.toList
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the smallest key that is
greater than or equal to the given key.
 -/
Std.DTreeMap.Const.getEntryGE : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α (fun x => β) cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isGE = true) → α × β
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.Preconnected.coeSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (G'' : G'.coe.Subgraph),
  G''.Preconnected → (SimpleGraph.Subgraph.coeSubgraph G'').Preconnected
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.const.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()