mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableAt_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {x : M × M'}, MDiffAt Prod.fst x
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.instT3Space : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E}, T3Space (ContDiffMapSupportedIn E F n K)
-- Mathlib.RingTheory.Nakayama
Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M]
  [Module.Finite R M] {r : R}, r ∈ (Module.annihilator R M).jacobson → ⊤ ≠ r • ⊤
-- Init.Data.SInt.Lemmas
Int32.ofInt_mul : ∀ (a b : ℤ), Int32.ofInt (a * b) = Int32.ofInt a * Int32.ofInt b
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- The equivalence between `L →ₐ[K] C` and `primitiveRoots n C` given by a primitive root `ζ`.  -/
IsPrimitiveRoot.embeddingsEquivPrimitiveRoots : {n : ℕ} →
  [NeZero n] →
    {K : Type u} →
      {L : Type v} →
        [inst : Field K] →
          [inst_1 : CommRing L] →
            [IsDomain L] →
              [inst_3 : Algebra K L] →
                [IsCyclotomicExtension {n} K L] →
                  {ζ : L} →
                    IsPrimitiveRoot ζ n →
                      (C : Type u_1) →
                        [inst_5 : CommRing C] →
                          [inst_6 : IsDomain C] →
                            [inst_7 : Algebra K C] →
                              Irreducible (Polynomial.cyclotomic n K) → (L →ₐ[K] C) ≃ ↥(primitiveRoots n C)
-- Init.Data.Dyadic.Basic
Dyadic.pow.eq_1 : ∀ (i : ℕ), Dyadic.zero.pow i = if i = 0 then 1 else 0
-- Init.Tactics
/-- Register a theorem as a rewrite rule for `cbv` evaluation of a given definition.

You can instruct `cbv` to rewrite the lemma from right-to-left:
```lean
@[cbv_eval ←] theorem my_thm : rhs = lhs := ...
```
 -/
Lean.Parser.Attr.cbv_eval : Lean.ParserDescr
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.getFunCasesName : Lean.Name → optParam Bool false → Lean.Name
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.hasLimitsEssentiallySmallSite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₃)
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.EssentiallySmall.{w, v₁, u₁} C]
  [CategoryTheory.Limits.HasLimits
      (CategoryTheory.Sheaf ((CategoryTheory.equivSmallModel C).inverse.inducedTopology J) A)],
  CategoryTheory.Limits.HasLimitsOfSize.{max v₃ w, max v₃ w, max u₁ v₃, max (max (max u₃ u₁) v₃) v₁}
    (CategoryTheory.Sheaf J A)
-- Mathlib.GroupTheory.Finiteness
AddGroup.fg_iff' : ∀ {G : Type u_3} [inst : AddGroup G], AddGroup.FG G ↔ ∃ n S, S.card = n ∧ AddSubgroup.closure ↑S = ⊤
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk_zero : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal], ↑0 = 0
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ →₀ ℕ) {c : R},
  c ≠ 0 → ((MvPolynomial.monomial s) c).totalDegree = s.sum fun x e => e
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.asymptoticNhds_eq_smul : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : TopologicalSpace V] [inst_5 : TopologicalSpace k] [OrderTopology k]
  [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] (v : V),
  AffineSpace.asymptoticNhds k V v = Filter.atTop • nhds v
-- Mathlib.RingTheory.Morita.Basic
/-- Let `A` and `B` be `R`-algebras. A Morita equivalence between `A` and `B` is an `R`-linear
equivalence between the categories of `A`-modules and `B`-modules.
 -/
MoritaEquivalence : (R : Type u₀) →
  [inst : CommSemiring R] →
    (A : Type u₁) →
      [inst_1 : Ring A] →
        [Algebra R A] → (B : Type u₂) → [inst_3 : Ring B] → [Algebra R B] → Type (max (u₁ + 1) (u₂ + 1))
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Turn a morphism in `CommMonCat` back into a `MonoidHom`.  -/
CommMonCat.Hom.hom : {X Y : CommMonCat} → X.Hom Y → ↑X →* ↑Y
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.coe_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), ↑f.range = Set.range ⇑f
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.equiv_iff_toListModel_perm : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β},
  m₁.Equiv m₂ ↔ (Std.DHashMap.Internal.toListModel m₁.buckets).Perm (Std.DHashMap.Internal.toListModel m₂.buckets)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.IsBipartiteWith.symm : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V}, G.IsBipartiteWith s t → G.IsBipartiteWith t s
-- Init.Data.Nat.Lemmas
/-- For `a > 1`, `a ^ b = a` iff `b = 1`.  -/
Nat.pow_eq_self_iff : ∀ {a b : ℕ}, 1 < a → (a ^ b = a ↔ b = 1)
-- Std.Data.HashMap.Raw
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.
 -/
Std.HashMap.Raw.getD : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → β → β
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetric.one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  LinearMap.IsSymmetric 1
-- Std.Data.DHashMap.Iterator
/-- Returns a finite iterator over the entries of a dependent hash map.
The iterator yields the elements of the map in order and then terminates.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DHashMap.Raw.iter : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → Std.Iter ((a : α) × β a)
-- Init.System.IO
/-- Extracts the `stdin` field from a `Child` object, allowing the handle to be closed while maintaining
a reference to the child process.

File handles are closed when the last reference to them is dropped. Closing the child's standard
input causes an end-of-file marker. Because the `Child` object has a reference to the standard
input, this operation is necessary in order to close the stream while the process is running (e.g.
to extract its exit code after calling `Child.wait`). Many processes do not terminate until their
standard input is exhausted.
 -/
IO.Process.Child.takeStdin : {cfg : IO.Process.StdioConfig} →
  IO.Process.Child cfg →
    IO
      (cfg.stdin.toHandleType ×
        IO.Process.Child { stdin := IO.Process.Stdio.null, stdout := cfg.stdout, stderr := cfg.stderr })
-- Mathlib.Data.Finsupp.Indicator
Finsupp.eq_indicator_self_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] (s : Finset ι) {d : ι →₀ α},
  (d = Finsupp.indicator s fun i x => d i) ↔ d.support ⊆ s
-- Mathlib.Topology.UniformSpace.Defs
/-- See also `comp_open_symm_mem_uniformity_sets`.  -/
comp_symm_mem_uniformity_sets : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α},
  s ∈ uniformity α → ∃ t ∈ uniformity α, SetRel.IsSymm t ∧ SetRel.comp t t ⊆ s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- If `f : X ⟶ Y`, `g g' : Y ⟶ Z` forms a pullback square, then `f` is the equalizer of
`g` and `g'`.  -/
CategoryTheory.IsPullback.isLimitFork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g g' : Y ⟶ Z} →
          (H : CategoryTheory.IsPullback f f g g') → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f ⋯)
-- Init.Data.List.Lemmas
List.getElem!_nil : ∀ {α : Type u_1} [inst : Inhabited α] {n : ℕ}, [][n]! = default
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.instInhabitedOLeanEntry.default : Lean.Parser.ParserExtension.OLeanEntry
-- Init.Data.Range.Polymorphic.PRange
Std.Roi.LawfulRcoIntersection.mk : ∀ {α : Type w} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.Roi.HasRcoIntersection α],
  (∀ {a : α} {r : Std.Roi α} {s : Std.Rco α}, a ∈ Std.Roi.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s) →
    Std.Roi.LawfulRcoIntersection α
-- Init.Data.Iterators.Lemmas.Consumers.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Collect.0.Std.Iter.atIdxSlow?.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β) (motive : it.Step → Sort u_2)
  (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) →
        (property : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, property⟩)
  (h_2 :
    (it' : Std.Iter β) →
      (property : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, property⟩ => h_1 it' out property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Std.Sync.SharedMutex
_private.Std.Sync.SharedMutex.0.Std.SharedMutexImpl : NonemptyType
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insertMany_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  t.insertMany [k] = t.insert k
-- Mathlib.Data.Sym.Basic
/-- Inserts an element into the term of `Sym α n`, increasing the length by one.
 -/
Sym.cons : {α : Type u_1} → {n : ℕ} → α → Sym α n → Sym α n.succ
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.map_injective_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Faithful] {X Y : C} (f g : X ⟶ Y), F.map f = F.map g ↔ f = g
-- Mathlib.Algebra.Field.Basic
/-- Pullback a `Field` along an injective function.  -/
Function.Injective.semifield : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Zero K] →
      [inst_1 : Add K] →
        [inst_2 : One K] →
          [inst_3 : Mul K] →
            [inst_4 : Inv K] →
              [inst_5 : Div K] →
                [inst_6 : SMul ℕ K] →
                  [inst_7 : SMul ℚ≥0 K] →
                    [inst_8 : Pow K ℕ] →
                      [inst_9 : Pow K ℤ] →
                        [inst_10 : NatCast K] →
                          [inst_11 : NNRatCast K] →
                            (f : K → L) →
                              Function.Injective f →
                                [inst_12 : Semifield L] →
                                  f 0 = 0 →
                                    f 1 = 1 →
                                      (∀ (x y : K), f (x + y) = f x + f y) →
                                        (∀ (x y : K), f (x * y) = f x * f y) →
                                          (∀ (x : K), f x⁻¹ = (f x)⁻¹) →
                                            (∀ (x y : K), f (x / y) = f x / f y) →
                                              (∀ (n : ℕ) (x : K), f (n • x) = n • f x) →
                                                (∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x) →
                                                  (∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                    (∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n) →
                                                      (∀ (n : ℕ), f ↑n = ↑n) → (∀ (q : ℚ≥0), f ↑q = ↑q) → Semifield K
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.instOrdDeclMod.ord : Lean.Meta.LibrarySearch.DeclMod → Lean.Meta.LibrarySearch.DeclMod → Ordering
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.getKey?_empty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α}, Std.DTreeMap.Internal.Cell.empty.getKey? = none
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.algebraAdjoinAdjoin.instIsAlgebraicSubtypeMemSubalgebraAdjoinAdjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E),
  Algebra.IsAlgebraic ↥(Algebra.adjoin F S) ↥(IntermediateField.adjoin F S)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) k).isLE = true
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCommGroup : {α : Type u_1} → [CommGroup α] → CommGroup αᵒᵈ
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.algebraMap_right_injective : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : CommSemiring R]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (v : AbsoluteValue T S),
  Function.Injective ⇑(algebraMap R T) → Function.Injective ⇑(algebraMap R (WithAbs v))
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- A functor is said to preserve cofiltered limits, if it preserves all limits of shape `J`, where
`J` is a cofiltered category which is small relative to the universe in which morphisms of the
source live.
 -/
CategoryTheory.Limits.PreservesCofilteredLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.AlgebraicGeometry.Sites.SheafQuasiCompact
/-- A presheaf is a sheaf for the `P`-qc topology if and only if it is a sheaf
for the Zariski topology and satisfies the sheaf property for all single object coverings
`{ f : Spec S ⟶ Spec R }` where `f` satisfies `P`.  -/
AlgebraicGeometry.isSheaf_propQCTopology_iff : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] {A : Type u_1}
  [inst : CategoryTheory.Category.{v_1, u_1} A] [P.IsMultiplicative]
  (F : CategoryTheory.Functor AlgebraicGeometry.Schemeᵒᵖ A) [AlgebraicGeometry.IsZariskiLocalAtSource P],
  CategoryTheory.Presheaf.IsSheaf (AlgebraicGeometry.Scheme.propQCTopology P) F ↔
    CategoryTheory.Presheaf.IsSheaf AlgebraicGeometry.Scheme.zariskiTopology F ∧
      ∀ {R S : CommRingCat} (f : R ⟶ S),
        P (AlgebraicGeometry.Spec.map f) →
          AlgebraicGeometry.Surjective (AlgebraicGeometry.Spec.map f) →
            ∀ (M : A),
              CategoryTheory.Presieve.IsSheafFor (F.comp (CategoryTheory.coyoneda.obj (Opposite.op M)))
                (CategoryTheory.Presieve.singleton (AlgebraicGeometry.Spec.map f))
-- Mathlib.Topology.Algebra.Algebra
/-- If `A` is an `R`-algebra, then a continuous `A`-algebra morphism can be interpreted as a
continuous `R`-algebra morphism.  -/
ContinuousAlgHom.restrictScalars : (R : Type u_1) →
  [inst : CommSemiring R] →
    {S : Type u_3} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {B : Type u_4} →
            [inst_3 : Ring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R B] →
                  [inst_6 : Algebra S B] →
                    [IsScalarTower R S B] →
                      {C : Type u_5} →
                        [inst_8 : Ring C] →
                          [inst_9 : TopologicalSpace C] →
                            [inst_10 : Algebra R C] →
                              [inst_11 : Algebra S C] → [IsScalarTower R S C] → (B →A[S] C) → B →A[R] C
-- Mathlib.Data.Fintype.Card
/-- **Alias** of the reverse direction of `Finite.injective_iff_surjective_of_equiv`. -/
Function.Surjective.injective_of_finite : ∀ {α : Type u_1} {β : Type u_2} [Finite α] {f : α → β} (e : α ≃ β), Function.Surjective f → Function.Injective f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.event.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.event = 1
-- Mathlib.Tactic.GRewrite.Elab
/-- Apply the `grewrite` tactic to the current goal.  -/
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.grewriteTarget : Lean.Syntax → Bool → Mathlib.Tactic.GRewrite.Config → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_one : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (v : m → α),
  Matrix.vecMul v 1 = v
-- Mathlib.RingTheory.Ideal.Maps
Module.annihilator_pi : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_4} {M : ι → Type u_5} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)], Module.annihilator R ((i : ι) → M i) = ⨅ i, Module.annihilator R (M i)
-- Init.Data.Int.DivMod.Bootstrap
Int.bmod_emod : ∀ {x : ℤ} {m : ℕ}, x.bmod m % ↑m = x % ↑m
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φH : ∀ {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 : CategoryTheory.ShortComplex C}
  {F G : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms] [inst_5 : G.PreservesZeroMorphisms]
  [inst_6 : F.PreservesLeftHomologyOf S] [inst_7 : G.PreservesLeftHomologyOf S] (h : S.LeftHomologyData) (τ : F ⟶ G),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp h τ).φH = τ.app h.H
-- Mathlib.Analysis.Normed.Operator.Mul
/-- **Alias** of `ContinuousLinearMap.toSpanSingletonLIE`.

---

If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly isometrically
equivalent to `M`.  -/
ContinuousLinearMap.ring_lmap_equiv_self : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → E ≃ₗᵢ[𝕜] 𝕜 →L[𝕜] E
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.image_subset : ∀ {α : Type u_1} {s u : Set α} {P : Partition u} {f : α → α}, P.IsRepFun f → u ⊆ s → f '' s ⊆ s
-- Lean.Parser.Command
Lean.Parser.Command.export.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.List.Basic
List.append_eq_appendTR : @List.append = @List.appendTR
-- Mathlib.Topology.CompactOpen
ContinuousMap.inseparable_coe : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : C(X, Y)},
  Inseparable ⇑f ⇑g ↔ Inseparable f g
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.setOfIdeal_ofSet_of_isOpen : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : RCLike 𝕜] [inst_1 : TopologicalSpace X] [CompactSpace X] [T2Space X]
  {s : Set X}, IsOpen s → ContinuousMap.setOfIdeal (ContinuousMap.idealOfSet 𝕜 s) = s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.compare_maxKey!_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {f : β → β}, cmp (t.modify k f).maxKey! t.maxKey! = Ordering.eq
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.Hom.match_1.eq_3 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : CategoryTheory.Join C D → CategoryTheory.Join C D → Sort u_5) (a : C) (a_1 : D)
  (h_1 : (x y : C) → motive (CategoryTheory.Join.left x) (CategoryTheory.Join.left y))
  (h_2 : (x y : D) → motive (CategoryTheory.Join.right x) (CategoryTheory.Join.right y))
  (h_3 : (a : C) → (a_2 : D) → motive (CategoryTheory.Join.left a) (CategoryTheory.Join.right a_2))
  (h_4 : (a : D) → (a_2 : C) → motive (CategoryTheory.Join.right a) (CategoryTheory.Join.left a_2)),
  (match CategoryTheory.Join.left a, CategoryTheory.Join.right a_1 with
    | CategoryTheory.Join.left x, CategoryTheory.Join.left y => h_1 x y
    | CategoryTheory.Join.right x, CategoryTheory.Join.right y => h_2 x y
    | CategoryTheory.Join.left a, CategoryTheory.Join.right a_2 => h_3 a a_2
    | CategoryTheory.Join.right a, CategoryTheory.Join.left a_2 => h_4 a a_2) =
    h_3 a a_1
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_apply' : ∀ {ι : Type u_1} {u : Set ι} {p : ↑unitInterval} (S : Set (Set ι)),
  (ProbabilityTheory.setBernoulli u p) S =
    (MeasureTheory.Measure.infinitePi fun i =>
        unitInterval.toNNReal p • MeasureTheory.Measure.dirac (i ∈ u) +
          unitInterval.toNNReal (unitInterval.symm p) • MeasureTheory.Measure.dirac False)
      ((fun p => {i | p i}) ⁻¹' S)
-- Init.Data.Format.Instances
instToFormatOfToString : {α : Type u_1} → [ToString α] → Std.ToFormat α
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.mono_hasImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f],
  CategoryTheory.Limits.HasImage f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_insert_le_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {k : α} {v : β} {fallback : α}, (cmp ((t.insert k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.le_enum_succ : ∀ {o : Ordinal.{u_1}} (a : (Order.succ o).ToType), a ≤ (Ordinal.enum fun x1 x2 => x1 < x2) ⟨o, ⋯⟩
-- Mathlib.Algebra.Group.Defs
AddRightCancelMonoid.toAddMonoid : {M : Type u} → [self : AddRightCancelMonoid M] → AddMonoid M
-- Mathlib.RingTheory.Localization.Module
LinearMap.extendScalarsOfIsLocalizationEquiv_symm_apply : ∀ {R : Type u_3} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] {M : Type u_5} {N : Type u_6} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Module A M] [inst_7 : IsScalarTower R A M] [inst_8 : AddCommMonoid N]
  [inst_9 : Module R N] [inst_10 : Module A N] [inst_11 : IsScalarTower R A N] (fₗ : M →ₗ[A] N),
  (LinearMap.extendScalarsOfIsLocalizationEquiv S A).symm fₗ = ↑R fₗ
-- Lean.Declaration
Lean.Declaration.opaqueDecl.sizeOf_spec : ∀ (val : Lean.OpaqueVal), sizeOf (Lean.Declaration.opaqueDecl val) = 1 + sizeOf val
-- Mathlib.Geometry.Diffeology.Basic
/-- The diffeology defined by `g`. Same as `generateFrom g`, except that its set of plots is
definitionally equal to `g`.  -/
DiffeologicalSpace.mkOfClosure : {X : Type u_1} →
  (g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))) →
    (DiffeologicalSpace.generateFrom g).toPlots = g → DiffeologicalSpace X
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.instBEqCheckResult.beq : Lean.Meta.Grind.CheckResult → Lean.Meta.Grind.CheckResult → Bool
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.instMonadNormalizeNaturalityMonoidalM : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lcs_succ : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ) (N : LieSubmodule R L M),
  LieSubmodule.lcs (k + 1) N = ⁅⊤, LieSubmodule.lcs k N⁆
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.nondegenerate_toBilin'_of_det_ne_zero' : ∀ {A : Type u_5} [inst : CommRing A] [IsDomain A] {ι : Type u_6} [inst_2 : DecidableEq ι] [inst_3 : Fintype ι]
  (M : Matrix ι ι A), M.det ≠ 0 → (Matrix.toBilin' M).Nondegenerate
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.IsFiltered.initial_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofiltered D], (CategoryTheory.Prod.fst C D).Initial