mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Group.Basic
norm_units_zsmul : ∀ {E : Type u_8} [inst : SeminormedAddGroup E] (n : ℤˣ) (a : E), ‖n • a‖ = ‖a‖
-- Std.Time.DateTime.PlainDateTime
/-- Converts the number of days relative to 1970-01-01 as a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.ofEpochDay : Std.Time.Day.Offset → Std.Time.PlainTime → Std.Time.PlainDateTime
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.Indep.indep_insert_sdiff_of_mem_closure`. -/
Matroid.Indep.indep_insert_diff_of_mem_closure : ∀ {α : Type u_2} {M : Matroid α} {e f : α} {I : Set α},
  M.Indep I → f ∈ M.closure I → e ∈ M.closure (insert f I \ {e}) → e ∈ insert f I → M.Indep (insert f I \ {e})
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.IsFinitelyPresentable.exists_eq_of_isColimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsFiltered J] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D}
  (hc : CategoryTheory.Limits.IsColimit c) {X : C} [CategoryTheory.IsFinitelyPresentable X] {i j : J} (f : X ⟶ D.obj i)
  (g : X ⟶ D.obj j),
  CategoryTheory.CategoryStruct.comp f (c.ι.app i) = CategoryTheory.CategoryStruct.comp g (c.ι.app j) →
    ∃ k u v, CategoryTheory.CategoryStruct.comp f (D.map u) = CategoryTheory.CategoryStruct.comp g (D.map v)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_add_of_le_of_nonneg : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, b ≤ c → 0 ≤ a → b ≤ c + a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertManyIfNewUnit.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ α] (m m_1 : Std.ExtDHashMap α fun x => Unit),
  m = m_1 →
    ∀ (l l_1 : ρ),
      l = l_1 → Std.ExtDHashMap.Const.insertManyIfNewUnit m l = Std.ExtDHashMap.Const.insertManyIfNewUnit m_1 l_1
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
/-- Given a square `w : TwoSquare T L R B` (consisting of a natural transformation
`T ⋙ R ⟶ L ⋙ B`), this is the obvious map `R.LeftExtension F → L.LeftExtension (T ⋙ F)`
obtained by the precomposition with `B` and the postcomposition with `w`.  -/
CategoryTheory.Functor.LeftExtension.compTwoSquare : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        {D : Type u₅} →
          [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
            [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
              [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D] →
                    {T : CategoryTheory.Functor C₁ C₂} →
                      {L : CategoryTheory.Functor C₁ C₃} →
                        {R : CategoryTheory.Functor C₂ C₄} →
                          {B : CategoryTheory.Functor C₃ C₄} →
                            {F : CategoryTheory.Functor C₂ D} →
                              R.LeftExtension F → CategoryTheory.TwoSquare T L R B → L.LeftExtension (T.comp F)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Subgraph.instCoeFunPreconnectedForallForallReachableElemVertsCoe : {V : Type u} →
  {G : SimpleGraph V} → {H : G.Subgraph} → CoeFun H.Preconnected fun x => ∀ (u v : ↑H.verts), H.coe.Reachable u v
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.instCoeSortType : CoeSort AlgebraicGeometry.RingedSpace (Type u_1)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.coeff_single`. -/
SkewMonoidAlgebra.toFinsupp_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a : G) (b : k),
  (SkewMonoidAlgebra.single a b).coeff = fun₀ | a => b
-- Mathlib.RingTheory.PrincipalIdealDomain
IsRelPrime.isCoprime : ∀ {R : Type u} [inst : CommRing R] {x y : R} [Submodule.IsPrincipal (Ideal.span {x, y})], IsRelPrime x y → IsCoprime x y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
/-- The `Y`-coordinate of a representative of `P + Q` for two distinct Jacobian point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`.  -/
WeierstrassCurve.Jacobian.addY : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → (Fin 3 → R) → R
-- Mathlib.Analysis.Fourier.Notation
/-- The Fourier transform is continuous.  -/
ContinuousFourier : (E : Type u_5) → (F : outParam (Type u_6)) → [TopologicalSpace E] → [TopologicalSpace F] → [FourierTransform E F] → Prop
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.skeletonLT_mono`. -/
Topology.CWComplex.skeletonLT_mono : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  {n m : ℕ∞}, m ≤ n → ↑(Topology.RelCWComplex.skeletonLT C m) ⊆ ↑(Topology.RelCWComplex.skeletonLT C n)
-- Mathlib.Topology.Instances.Matrix
/-- For square matrices the usual `continuous_mul` can be used.  -/
Continuous.matrix_mul : ∀ {X : Type u_1} {m : Type u_4} {n : Type u_5} {p : Type u_6} {R : Type u_8} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace R] [inst_2 : Fintype n] [inst_3 : Mul R] [inst_4 : AddCommMonoid R] [ContinuousAdd R]
  [ContinuousMul R] {A : X → Matrix m n R} {B : X → Matrix n p R},
  Continuous A → Continuous B → Continuous fun x => A x * B x
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.isoOfComponents_app : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : (i : ι) → C₁.X i ≅ C₂.X i)
  (hf :
    ∀ (i j : ι),
      c.Rel i j →
        CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) =
          CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom)
  (i : ι), HomologicalComplex.Hom.isoApp (HomologicalComplex.Hom.isoOfComponents f hf) i = f i
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- Two algebra morphism from the graded tensor product agree if their compositions with the left
and right inclusions agree.  -/
GradedTensorProduct.algHom_ext : ∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : DecidableEq ι]
  [inst_2 : CommRing R] [inst_3 : Ring A] [inst_4 : Ring B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  [inst_9 : Module ι (Additive ℤˣ)] {C : Type u_5} [inst_10 : Ring C] [inst_11 : Algebra R C]
  ⦃f g : GradedTensorProduct R 𝒜 ℬ →ₐ[R] C⦄,
  f.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) = g.comp (GradedTensorProduct.includeLeft 𝒜 ℬ) →
    f.comp (GradedTensorProduct.includeRight 𝒜 ℬ) = g.comp (GradedTensorProduct.includeRight 𝒜 ℬ) → f = g
-- Init.NotationExtra
Lean.bracketedExplicitBinders : Lean.ParserDescr
-- Std.Data.HashMap.Basic
/-- Returns the number of buckets in the internal representation of the hash map. This function may be
useful for things like monitoring system health, but it should be considered an internal
implementation detail.
 -/
Std.HashMap.Internal.numBuckets : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.HashMap α β → ℕ
-- Mathlib.RingTheory.LocalRing.ResidueField.Fiber
PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (q : PrimeSpectrum (p.Fiber S)),
  ↑((PrimeSpectrum.primesOverOrderIsoFiber R S p).symm q) = Ideal.comap Algebra.TensorProduct.includeRight q.asIdeal
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_op_pow : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] (s : Finset α) (n : ℕ),
  Finset.map MulOpposite.opEquiv.toEmbedding (s ^ n) = Finset.map MulOpposite.opEquiv.toEmbedding s ^ n
-- Mathlib.Data.Rat.Floor
Rat.isNat_intCeil_ofIsNNRat : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (r : α)
  (n d : ℕ), Mathlib.Meta.NormNum.IsNNRat r n d → Mathlib.Meta.NormNum.IsNat ⌈r⌉ (-(-↑n / ↑d)).toNat
-- Mathlib.GroupTheory.DivisibleHull
_private.Mathlib.GroupTheory.DivisibleHull.0.DivisibleHull.archimedeanClassOrderHomInv.eq_1 : ∀ (M : Type u_2) [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  DivisibleHull.archimedeanClassOrderHomInv✝ M =
    ArchimedeanClass.liftOrderHom (fun x => x.liftOn (fun m s => ArchimedeanClass.mk m) ⋯) ⋯
-- Mathlib.Algebra.Group.Defs
AddCancelCommMonoid.mk : {M : Type u} → [toAddCommMonoid : AddCommMonoid M] → [toIsLeftCancelAdd : IsLeftCancelAdd M] → AddCancelCommMonoid M
-- Mathlib.Control.Monad.Writer
WriterT.instMonadControlOfMonadLiftT : {M : Type u → Type v} → {ω : Type u} → [MonadLiftT M (WriterT ω M)] → MonadControl M (WriterT ω M)
-- Init.Data.UInt.Lemmas
UInt32.toNat_toUInt64 : ∀ (x : UInt32), x.toUInt64.toNat = x.toNat
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.isOpen_right_of_isOpen_union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → IsOpen (s ∪ t) → IsOpen t
-- Mathlib.Analysis.Analytic.Composition
/-- Composing the partial sums of two multilinear series coincides with the sum over all
compositions in `compPartialSumTarget 0 N N`. This is precisely the motivation for the
definition of `compPartialSumTarget`.  -/
FormalMultilinearSeries.comp_partialSum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F) (M N : ℕ) (z : E),
  q.partialSum M (∑ i ∈ Finset.Ico 1 N, (p i) fun _j => z) =
    ∑ i ∈ FormalMultilinearSeries.compPartialSumTarget 0 M N, (q.compAlongComposition p i.snd) fun _j => z
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabTrailingParserMacro : Lean.Elab.Term.TermElab
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.mapM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → [Monad m] → (α → m β) → Lean.Widget.TaggedText α → m (Lean.Widget.TaggedText β)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- Given a group homomorphism `f : G →* H` and a representation morphism `φ : Res(f)(A) ⟶ B`,
this is the induced map `Hⁿ(H, A) ⟶ Hⁿ(G, B)` sending `x : Hⁿ → A` to
`(g : Gⁿ) ↦ φ (x (f ∘ g))`.  -/
groupCohomology.map : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k H} →
          {B : Rep.{u, u, u} k G} →
            (f : G →* H) → (Rep.res f A ⟶ B) → (n : ℕ) → groupCohomology A n ⟶ groupCohomology B n
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_top : ⊤.toReal = 0
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.removeLoops.eq_1 : ∀ {α : Type u_1} (M : Matroid α), M.removeLoops = M.restrict {e | M.IsNonloop e}
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'_even : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℕ),
  preNormEDS' b c d (2 * (m + 3)) =
    preNormEDS' b c d (m + 2) ^ 2 * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 5) -
      preNormEDS' b c d (m + 1) * preNormEDS' b c d (m + 3) * preNormEDS' b c d (m + 4) ^ 2
-- Init.Data.Int.Order
Int.lt_of_add_one_le : ∀ {a b : ℤ}, a + 1 ≤ b → a < b
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0.map_init : ∀ {Γ : Type u_1} [inst : Inhabited Γ] {Γ' : Type u_2} [inst_1 : Inhabited Γ'] {Λ : Type u_3} [inst_2 : Inhabited Λ]
  {Λ' : Type u_4} [inst_3 : Inhabited Λ'] (f₁ : Turing.PointedMap Γ Γ') (g₁ : Turing.PointedMap Λ Λ') (l : List Γ),
  Turing.TM0.Cfg.map f₁ g₁.f (Turing.TM0.init l) = Turing.TM0.init (List.map f₁.f l)
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.mem_rangeIcc_apply_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → LocallyFiniteOrder (α i)] {f g : Π₀ (i : ι), α i} {i : ι} {a : α i},
  a ∈ (f.rangeIcc g) i ↔ f i ≤ a ∧ a ≤ g i
-- Init.Data.Nat.Bitwise.Lemmas
Nat.left_le_or : ∀ {n m : ℕ}, n ≤ n ||| m
-- Lean.DocString.Markdown
Lean.Doc.instToMarkdownVersoDocString : Lean.Doc.ToMarkdown Lean.VersoDocString
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_filter_lt_of_lt_right : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b c : α}
  [inst_2 : DecidablePred fun x => x < c], b < c → {x ∈ Finset.Ioc a b | x < c} = Finset.Ioc a b
-- Init.Data.SInt.Basic
/-- Decides whether one 32-bit signed integer is strictly less than another. Usually accessed via the
`DecidableLT Int32` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if ((-7) : Int32) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : Int32) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : Int32) < 7) by decide`
 -/
Int32.decLt : (a b : Int32) → Decidable (a < b)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The compatibility of a morphism with the augmentation, on 0-simplices  -/
CategoryTheory.SimplicialObject.Augmented.w₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.SimplicialObject.Augmented C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (f.left.app (Opposite.op { len := 0 })) (Y.hom.app (Opposite.op { len := 0 })) =
    CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 })) f.right
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressParams.mk.sizeOf_spec : ∀ (workDoneToken? : Option Lean.Lsp.ProgressToken),
  sizeOf { workDoneToken? := workDoneToken? } = 1 + sizeOf workDoneToken?
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.take.match_1.splitter : {α : Type u_1} →
  (motive : ℕ → List α → Sort u_2) →
    (x : ℕ) →
      (x_1 : List α) →
        ((x : List α) → motive 0 x) →
          ((n : ℕ) → motive n.succ []) → ((n : ℕ) → (a : α) → (as : List α) → motive n.succ (a :: as)) → motive x x_1
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.coe_liftQL : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Ring R] [inst_1 : Ring R₂] {σ : R →+* R₂} {M : Type u_3} {M₂ : Type u_4}
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] [inst_7 : Module R₂ M₂] (S : Submodule R M) (f : M →SL[σ] M₂) (h : S ≤ (↑f).ker),
  ⇑(S.liftQL f h) = ⇑(S.liftQ (↑f) h)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.coprodSpec_inl_assoc : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of (R × S)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.coprodSpec R S) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (RingHom.fst R S))) h
-- Lean.Data.Format
Lean.Std.Format.format.unicode : Lean.Option Bool
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.mapPiEvalRingHom_bijective : ∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → CommSemiring (R i)] {i : ι} (I : Ideal (R i))
  [inst_1 : I.IsPrime], Function.Bijective ⇑(Localization.AtPrime.mapPiEvalRingHom I)
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.below.succ : ∀ {α : Type u_1} {r : α → α → Prop} {motive : (a : Set α) → ChainClosure r a → Prop} {s : Set α} (a : ChainClosure r s),
  ChainClosure.below a → motive s a → ChainClosure.below ⋯
-- Std.Async.System
/-- Gets the temporary directory.
 -/
Std.Async.System.getTmpDir : IO System.FilePath
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.forget₂_ringCat_obj : ∀ (R : Type u) [inst : CommRing R] (X : AlgCat R), (CategoryTheory.forget₂ (AlgCat R) RingCat).obj X = RingCat.of ↑X
-- Mathlib.Analysis.Calculus.FDeriv.Const
HasFDerivAt.of_notMem_tsupport : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, x ∉ tsupport f → HasFDerivAt f 0 x
-- Mathlib.Data.List.PeriodicityLemma
/-- Induction step for the `periodicity_lemma`  -/
List.HasPeriod.drop_of_hasPeriod_add : ∀ {α : Type u_1} {q k : ℕ} {w : List α}, w.HasPeriod q → w.HasPeriod (k + q) → (List.drop q w).HasPeriod k
-- Mathlib.Algebra.Ring.CentroidHom
_private.Mathlib.Algebra.Ring.CentroidHom.0.CentroidHom.termR : Lean.ParserDescr
-- Init.Data.Vector.Zip
_private.Init.Data.Vector.Zip.0.Array.getElem?_zipWith.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((a : α) → (b : β) → motive (some a) (some b)) →
            ((x : Option α) →
                (x_2 : Option β) → (∀ (a : α) (b : β), x = some a → x_2 = some b → False) → motive x x_2) →
              motive x x_1
-- Mathlib.Topology.Maps.Basic
/-- A map is open if and only if the `Set.kernImage` of every *closed* set is closed.

One way to understand this result is that `f : X → Y` is open if and only if its fibers vary in a
**lower hemicontinuous** way: for any open subset `U ⊆ X`, the set of all `y ∈ Y` such that
`(f ⁻¹' {y} ∩ U).Nonempty` is open in `Y`. See `isOpenMap_iff_lowerHemicontinuous`.  -/
isOpenMap_iff_kernImage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f ↔ ∀ {u : Set X}, IsClosed u → IsClosed (Set.kernImage f u)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (α : X ≅ Y), α.symm.unop = α.unop.symm
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_lt_beth_natCast : ∀ {c : Cardinal.{u}} {n : ℕ}, Cardinal.lift.{v, u} c < Cardinal.beth ↑n ↔ c < Cardinal.beth ↑n
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the forward direction of `upperHemicontinuousAt_iff_frequently`. -/
UpperHemicontinuousAt.frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {x : α},
  UpperHemicontinuousAt f x →
    ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhds x, (f x' ∩ t).Nonempty) → (f x ∩ t).Nonempty
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
IsOpen.liftSourceTargetPropertyAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {g : M → N}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  IsOpen {x | Manifold.LiftSourceTargetPropertyAt I J n g x P}
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F], fderiv 𝕜 0 = 0
-- Mathlib.Order.Interval.Set.Image
Set.preimage_subtype_val_Iic : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a : { x // p x }), Subtype.val ⁻¹' Set.Iic ↑a = Set.Iic a
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ordCompare_maxKeyD_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.ExtTreeMap α β compare} {k : α}
  {f : β → β} {fallback : α}, compare ((t.modify k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.Order.CompleteLattice.Basic
inf_biInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α},
  (∃ i, p i) → a ⊓ ⨅ i, ⨅ (h : p i), f i h = ⨅ i, ⨅ (h : p i), a ⊓ f i h
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- The homotopy category of a 2-truncated quasicategory `A` has as objects the vertices of `A`
 -/
SSet.Truncated.HomotopyCategory₂ : SSet.Truncated 2 → Type u_1
-- Init.Data.Fin.Basic
Fin.instOfNat : {n : ℕ} → [NeZero n] → {i : ℕ} → OfNat (Fin n) i
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.GaloisCategory.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [toPreGaloisCategory : CategoryTheory.PreGaloisCategory C],
  (∃ F, Nonempty (CategoryTheory.PreGaloisCategory.FiberFunctor F)) → CategoryTheory.GaloisCategory C
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.Y_ne_negY_of_Y_ne : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → W'.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ Q 1 * P 2 → P 1 ≠ W'.negY P
-- Init.Data.List.Lemmas
/-- If one has `l[i]` in an expression and `h : l = l'`,
`rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the
implicit `i < l.length` to `i < l'.length` directly. The theorem `getElem_of_eq` can be used to make
such a rewrite, with `rw [getElem_of_eq h]`.
 -/
List.getElem_of_eq : ∀ {α : Type u_1} {l l' : List α} (h : l = l') {i : ℕ} (w : i < l.length), l[i] = l'[i]
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.nndist_integral_add_vectorMeasure_le_lintegral : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ ν : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  μ.Integrable f →
    ν.Integrable f →
      ↑(nndist ∫ᵛ (x : X), f x ∂[B; μ] ∫ᵛ (x : X), f x ∂[B; μ + ν]) ≤ ‖B‖ₑ * ∫⁻ (x : X), ‖f x‖ₑ ∂ν.variation
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_counitIso_hom_app_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core D), (E.core.counitIso.hom.app X).iso.inv = E.counitIso.inv.app X.of
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.hasEqualizers_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C],
  CategoryTheory.Limits.HasEqualizers Cᵒᵖ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.map_fst_toList_eq_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, List.map Prod.fst t.toList = t.keys
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.ExtensionState.funCC : Lean.Meta.Grind.ExtensionState → Lean.NameSet
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.instOmegaCompletePartialOrder : {α : Type u_1} → [ChainCompletePartialOrder α] → OmegaCompletePartialOrder α
-- Mathlib.Topology.UniformSpace.CompareReals
CompareReals.Bourbaki.uniformSpace : UniformSpace CompareReals.Bourbakiℝ
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isMatch_cast_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s t : String.Slice} (h : s.copy = t.copy)
  {pos : s.Pos}, String.Slice.Pattern.Model.IsMatch pat (pos.cast h) ↔ String.Slice.Pattern.Model.IsMatch pat pos
-- Mathlib.NumberTheory.ModularForms.DedekindEta
/-- Notation for the Dedekind eta function.  -/
ModularForm.termη : Lean.ParserDescr