mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AdicCompletion.Exactness
_private.Mathlib.RingTheory.AdicCompletion.Exactness.0.AdicCompletion.mapPreimage.match_5.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive Nat.zero) (h_2 : (n : ℕ) → motive n.succ),
  (match Nat.zero with
    | Nat.zero => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Order.Filter.Map
Filter.pure_injective : ∀ {α : Type u_1}, Function.Injective pure
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.mk_obj : ∀ {V : Type u_1} {W : Type u_2} [inst : CategoryTheory.ReflQuiver V] [inst_1 : CategoryTheory.ReflQuiver W]
  {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X : V}, { obj := obj, map := map }.obj X = obj X
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.coeff_zero_left : ∀ (o : Ordinal.{u_1}), Ordinal.CNF.coeff 0 o = fun₀ | 0 => o
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_mul : ∀ {ι : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (s : Finset ι) (f : ι → R) (a : R),
  (∑ i ∈ s, f i) * a = ∑ i ∈ s, f i * a
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
/-- Given a commutative square `CommSq t l r b` in a strict bicategory `B` and
a pseudofunctor from `B`, this is the isomorphism
`F.map t ≫ F.map r ≅ F.map l ≫ F.map b`.  -/
CategoryTheory.Pseudofunctor.isoMapOfCommSq : {B : Type u₁} →
  {C : Type u₂} →
    [inst : CategoryTheory.Bicategory B] →
      [inst_1 : CategoryTheory.Bicategory.Strict B] →
        [inst_2 : CategoryTheory.Bicategory C] →
          (F : CategoryTheory.Pseudofunctor B C) →
            {X₁ X₂ Y₁ Y₂ : B} →
              {t : X₁ ⟶ Y₁} →
                {l : X₁ ⟶ X₂} →
                  {r : Y₁ ⟶ Y₂} →
                    {b : X₂ ⟶ Y₂} →
                      CategoryTheory.CommSq t l r b →
                        (CategoryTheory.CategoryStruct.comp (F.map t) (F.map r) ≅
                          CategoryTheory.CategoryStruct.comp (F.map l) (F.map b))
-- Mathlib.Order.SupClosed
isSublattice_empty : ∀ {α : Type u_3} [inst : Lattice α], IsSublattice ∅
-- Lean.Server.CodeActions.Basic
Lean.Server.addBuiltinCodeActionProvider : Lean.Name → Lean.Server.CodeActionProvider → IO Unit
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.mkInv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (f : Y ⟶ X) (hf : W f) [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y],
  CategoryTheory.Localization.SmallHom.mkInv f hf =
    (CategoryTheory.Localization.SmallHom.equiv W W.Q).symm (CategoryTheory.Localization.isoOfHom W.Q W f hf).inv
-- Init.Data.Hashable
instHashableUInt16 : Hashable UInt16
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
/-- The ring isomorphism between the infinite adele ring of a number field and the
space `ℝ ^ r₁ × ℂ ^ r₂`, where `(r₁, r₂)` is the signature of the number field.  -/
NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace : (K : Type u_1) → [inst : Field K] → NumberField.InfiniteAdeleRing K ≃+* NumberField.mixedEmbedding.mixedSpace K
-- Mathlib.Logic.IsEmpty.Defs
/-- Eliminate out of a type that `IsEmpty` (using projection notation).  -/
IsEmpty.elim : {α : Sort u} → IsEmpty α → {p : α → Sort v} → (a : α) → p a
-- Init.Prelude
/-- Retrieves the current value of the monad's mutable state.
 -/
EStateM.get : {ε σ : Type u} → EStateM ε σ σ
-- Mathlib.LinearAlgebra.Dimension.Free
Module.Free.exists_linearMap_injective_of_linearIndependent_of_rank_le : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {N : Type v} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] {ι : Type v} {v : ι → N},
  LinearIndependent R v → Module.rank R M ≤ Cardinal.mk ι → ∃ f, Function.Injective ⇑f
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.finite_preimage_singleton : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f]
  [AlgebraicGeometry.QuasiCompact f] (y : ↥Y), (⇑f ⁻¹' {y}).Finite
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : Add α] →
          [inst_3 : Add β] →
            (toAddEquiv : α ≃+ β) → (∀ {a b : α}, toAddEquiv.toFun a ≤ toAddEquiv.toFun b ↔ a ≤ b) → α ≃+o β
-- Mathlib.NumberTheory.LSeries.Convolution
LSeries.convolution_congr : ∀ {R : Type u_1} [inst : Semiring R] {f f' g g' : ℕ → R},
  (∀ {n : ℕ}, n ≠ 0 → f n = f' n) →
    (∀ {n : ℕ}, n ≠ 0 → g n = g' n) → LSeries.convolution f g = LSeries.convolution f' g'
-- Mathlib.Topology.Algebra.Group.Extension
/-- A predicate stating that `φ` and `ψ` define a short exact sequence of topological groups.  -/
TopologicalGroup.IsSES : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : Group A] →
        [inst_1 : Group B] →
          [inst_2 : Group C] →
            [TopologicalSpace A] → [TopologicalSpace B] → [TopologicalSpace C] → (A →* B) → (B →* C) → Prop
-- Mathlib.Algebra.Ring.Defs
NonAssocCommSemiring.toNonUnitalNonAssocCommSemiring : {α : Type u} → [self : NonAssocCommSemiring α] → NonUnitalNonAssocCommSemiring α
-- Lean.Server.References
/-- References from ilean files and current ilean information from file workers.  -/
Lean.Server.References : Type
-- Mathlib.Analysis.Normed.Group.Bounded
tendsto_norm_cobounded_atTop : ∀ {E : Type u_2} [inst : SeminormedAddGroup E], Filter.Tendsto norm (Bornology.cobounded E) Filter.atTop
-- Mathlib.Data.Set.Operations
Set.subset_kernImage_iff : ∀ {α : Type u} {β : Type v} {s : Set β} {t : Set α} {f : α → β}, s ⊆ Set.kernImage f t ↔ f ⁻¹' s ⊆ t
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.dirichletInverseFun.eq_def : ∀ {R : Type u_1} [inst : Ring R] (f : ℕ → R) (hf : Invertible (f 1)) (n : ℕ),
  ArithmeticFunction.dirichletInverseFun f hf n =
    if n = 0 then 0
    else
      if n = 1 then ⅟(f 1)
      else
        -⅟(f 1) *
          ∑ d,
            have this := ⋯;
            f (n / ↑d) * ArithmeticFunction.dirichletInverseFun f hf ↑d
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- **Riesz's theorem**: in a T2 topological vector space over a complete non-trivial normed field,
if there exists a totally bounded neighborhood of some point, then the space is finite-dimensional.
 -/
FiniteDimensional.of_exists_totallyBounded_nhds : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {Eᵤ : Type u_6} [inst_2 : AddCommGroup Eᵤ]
  [inst_3 : Module 𝕜 Eᵤ] [inst_4 : UniformSpace Eᵤ] [T2Space Eᵤ] [IsUniformAddGroup Eᵤ] [ContinuousSMul 𝕜 Eᵤ],
  (∃ x, ∃ U ∈ nhds x, TotallyBounded U) → FiniteDimensional 𝕜 Eᵤ
-- Mathlib.Data.Finset.Basic
Multiset.toFinset_filter : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (p : α → Prop) [inst_1 : DecidablePred p],
  (Multiset.filter p s).toFinset = Finset.filter p s.toFinset
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Client.shared : Std.Http.Internal.Mock.Client → Std.Http.Internal.Mock.SharedState✝
-- Mathlib.Data.Set.Card
Set.encard_le_encard_sdiff_add_encard : ∀ {α : Type u_1} (s t : Set α), s.encard ≤ (s \ t).encard + t.encard
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- Proves the left to right direction of a generated iff theorem.
`shape` is the output of a call to `constrToProp`.
 -/
Mathlib.Tactic.MkIff.toCases : Lean.MVarId → List Mathlib.Tactic.MkIff.Shape → Lean.MetaM Unit
-- Std.Sync.RecursiveMutex
_private.Std.Sync.RecursiveMutex.0.Std.RecursiveMutex.mk.inj : ∀ {α : Type} {ref : IO.Ref α} {mutex : Std.BaseRecursiveMutex} {ref_1 : IO.Ref α} {mutex_1 : Std.BaseRecursiveMutex},
  { ref := ref, mutex := mutex } = { ref := ref_1, mutex := mutex_1 } → ref = ref_1 ∧ mutex = mutex_1
-- Mathlib.Combinatorics.Quiver.ReflQuiver
CategoryTheory.ReflPrefunctor.mk_map : ∀ {V : Type u_1} {W : Type u_2} [inst : CategoryTheory.ReflQuiver V] [inst_1 : CategoryTheory.ReflQuiver W]
  {obj : V → W} {map : {X Y : V} → (X ⟶ Y) → (obj X ⟶ obj Y)} {X Y : V} {f : X ⟶ Y},
  { obj := obj, map := map }.map f = map f
-- Mathlib.Order.Filter.AtTopBot.Archimedean
/-- If a function tends to infinity along a filter, then this function multiplied by a positive
constant (on the right) also tends to infinity. The archimedean assumption is convenient to get a
statement that works on `ℕ`, `ℤ` and `ℝ`, although not necessary (a version in ordered fields is
given in `Filter.Tendsto.atTop_mul_const`).  -/
Filter.Tendsto.atTop_mul_const' : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [inst : Semiring R] [inst_1 : LinearOrder R]
  [IsStrictOrderedRing R] [Archimedean R],
  0 < r → Filter.Tendsto f l Filter.atTop → Filter.Tendsto (fun x => f x * r) l Filter.atTop
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackCone.eq_1 : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z),
  TopCat.pullbackCone f g = CategoryTheory.Limits.PullbackCone.mk (TopCat.pullbackFst f g) (TopCat.pullbackSnd f g) ⋯
-- Mathlib.Data.List.Lattice
List.bagInter_erase_of_not_mem : ∀ {α : Type u_1} {l₁ l₂ : List α} {a : α} [inst : DecidableEq α], a ∉ l₁ → l₁.bagInter (l₂.erase a) = l₁.bagInter l₂
-- Mathlib.Topology.Closure
interior_union_isClosed_of_interior_empty : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClosed s → interior t = ∅ → interior (s ∪ t) = interior s
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- The isomorphism `shrinkYoneda.{w} ⋙ Φ.presheafFiber ≅ Φ.fiber`.  -/
CategoryTheory.GrothendieckTopology.Point.shrinkYonedaCompPresheafFiberIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
          CategoryTheory.shrinkYoneda.{w, v, u}.comp Φ.presheafFiber ≅ Φ.fiber
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_setRed : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.setRed.reverse = t.reverse.setRed
-- Init.Data.UInt.Lemmas
UInt32.ofFin_mul : ∀ (a b : Fin UInt32.size), UInt32.ofFin (a * b) = UInt32.ofFin a * UInt32.ofFin b
-- Mathlib.Topology.Order.Compact
IsCompact.sSup_lt_iff_of_continuous : ∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [inst_2 : TopologicalSpace β] [ClosedIciTopology α] {f : β → α} {K : Set β},
  IsCompact K → K.Nonempty → ContinuousOn f K → ∀ (y : α), sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- A prop-valued typeclass stating that a crystallographic, reduced, irreducible root system is not
`𝔤₂`.  -/
RootPairing.IsNotG2 : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → Prop
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size_deleteMin : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {s' s : Batteries.PairingHeapImp.Heap α},
  s.NoSibling → Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s') → s.size = s'.size + 1
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.const' : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (b : β) {K : NNReal},
  LipschitzWith K fun x => b
-- Lean.Environment
/-- Realization results, to be replayed onto other branches.  -/
_private.Lean.Environment.0.Lean.Environment.RealizeConstResult : Type
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_le_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 0 < a → a ≤ 1 → 0 ≤ n → a ^ n ≤ 1
-- Batteries.Lean.Meta.UnusedNames
/-- Match up to suffix.  -/
Lean.Name.MatchUpToIndexSuffix.suffixMatch : ℕ → Lean.Name.MatchUpToIndexSuffix
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseRightKanExtensionCounit_app : ∀ {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) [inst_3 : L.HasPointwiseRightKanExtension F]
  (X : C),
  (L.pointwiseRightKanExtensionCounit F).app X =
    CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj (L.obj X) L).comp F)
      (CategoryTheory.StructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.comap_equiv_eq_map_symm : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : N ≃+ M) (K : AddSubsemigroup M),
  AddSubsemigroup.comap (↑f) K = AddSubsemigroup.map (↑f.symm) K
-- Mathlib.Order.JordanHolder
CompositionSeries.toList_nodup : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X), (RelSeries.toList s).Nodup
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_rio : ∀ {α : Type u_1} {xs : Array α} {hi : ℕ}, (Std.Rio.Sliceable.mkSlice xs *...hi).stop = min hi xs.size
-- Lean.Compiler.IR.CompilerM
Lean.IR.LogEntry.fmt : Lean.IR.LogEntry → Std.Format
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `upperSemicontinuousWithinAt_iff_frequently`. -/
UpperSemicontinuousWithinAt.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α} {s : Set α},
  (∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≥ y) → f x ≥ y) → UpperSemicontinuousWithinAt f s x
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.absolutelyContinuous_map_div_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] (g : G),
  μ.AbsolutelyContinuous (MeasureTheory.Measure.map (fun h => g / h) μ)
-- Mathlib.Order.Interval.Finset.Defs
Finset.map_subtype_embedding_Ici : ∀ {α : Type u_1} [inst : Preorder α] (p : α → Prop) [inst_1 : DecidablePred p] [inst_2 : LocallyFiniteOrderTop α]
  (a : Subtype p),
  (∀ ⦃a x : α⦄, a ≤ x → p a → p x) → Finset.map (Function.Embedding.subtype p) (Finset.Ici a) = Finset.Ici ↑a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_mem_inv_mul_iff : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, 1 ∈ t⁻¹ * s ↔ ¬Disjoint s t
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- `I.map g` is the pushforward of the fractional ideal `I` along the algebra morphism `g`  -/
FractionalIdeal.map : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            {P' : Type u_3} →
              [inst_3 : CommRing P'] →
                [inst_4 : Algebra R P'] → (P →ₐ[R] P') → FractionalIdeal S P → FractionalIdeal S P'
-- Mathlib.RingTheory.Localization.Integral
/-- If the field `L` is a finite extension of the fraction field of the integral domain `A`,
the integral closure `C` of `A` in `L` has fraction field `L`.  -/
IsIntegralClosure.isFractionRing_of_finite_extension : ∀ (A : Type u_3) (K : Type u_4) [inst : CommRing A] (L : Type u_5) [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra A K] [inst_4 : Algebra A L] [IsFractionRing A K] (C : Type u_6) [inst_6 : CommRing C] [IsDomain C]
  [inst_8 : Algebra C L] [IsIntegralClosure C A L] [inst_10 : Algebra A C] [IsScalarTower A C L] [IsDomain A]
  [inst_13 : Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L], IsFractionRing C L
-- Mathlib.Data.Analysis.Topology
Ctop.top : {α : Type u_1} → {σ : Type u_2} → Ctop α σ → α → σ
-- Mathlib.Tactic.DefEqTransformations
/-- `refold_let x y z at loc` looks for the bodies of local definitions `x`, `y`, and `z` at the given
location and replaces them with `x`, `y`, or `z`. This is the inverse of "zeta reduction."
This also exists as a `conv`-mode tactic.
 -/
Mathlib.Tactic.convRefold_let___ : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- The linear map `fun x => c x • f`.  Associates to a scalar-valued linear map and an element of
`M₂` the `M₂`-valued linear map obtained by multiplying the two (a.k.a. tensoring by `M₂`).
See also `ContinuousLinearMap.smulRightₗ` and `ContinuousLinearMap.smulRightL`.  -/
ContinuousLinearMap.smulRight : {M₁ : Type u_4} →
  [inst : TopologicalSpace M₁] →
    [inst_1 : AddCommMonoid M₁] →
      {M₂ : Type u_6} →
        [inst_2 : TopologicalSpace M₂] →
          [inst_3 : AddCommMonoid M₂] →
            {R : Type u_9} →
              {S : Type u_10} →
                [inst_4 : Semiring R] →
                  [inst_5 : Semiring S] →
                    [inst_6 : Module R M₁] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module R S] →
                          [inst_9 : Module S M₂] →
                            [IsScalarTower R S M₂] →
                              [inst_11 : TopologicalSpace S] → [ContinuousSMul S M₂] → (M₁ →L[R] S) → M₂ → M₁ →L[R] M₂
-- Mathlib.Topology.ContinuousMap.Algebra
/-- The `Submonoid` of continuous maps `α → β`.  -/
continuousSubmonoid : (α : Type u_1) →
  (β : Type u_2) →
    [TopologicalSpace α] →
      [inst : TopologicalSpace β] → [inst_1 : MulOneClass β] → [ContinuousMul β] → Submonoid (α → β)
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
RingHom.IsIntegralElem.map_iff : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_4} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Ring T] {f : R →+* S}
  {g : S →+* T}, Function.Injective ⇑g → ∀ {x : S}, (g.comp f).IsIntegralElem (g x) ↔ f.IsIntegralElem x
-- Mathlib.CategoryTheory.MorphismProperty.Retract
CategoryTheory.MorphismProperty.instRespectsIsoOfIsStableUnderRetracts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderRetracts], P.RespectsIso
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasFDerivWithinAt.smul` -/
HasFDerivWithinAt.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜']
  [inst_7 : Module 𝕜' F] [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasFDerivWithinAt c c' s x →
    HasFDerivWithinAt f f' s x → HasFDerivWithinAt (fun i => c i • f i) (c x • f' + c'.smulRight (f x)) s x
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split.eq_1 : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ),
  Int.Internal.Linear.cooper_dvd_right_split ctx p₁ p₂ p₃ d k =
    (Int.Internal.Linear.Poly.denote' ctx
          (((p₁.tail.mul p₂.leadCoeff).combine (p₂.tail.mul (-p₁.leadCoeff))).addConst (-p₁.leadCoeff * ↑k)) ≤
        0 ∧
      p₂.leadCoeff ∣ Int.Internal.Linear.Poly.denote' ctx (p₂.tail.addConst ↑k) ∧
        p₂.leadCoeff * d ∣
          Int.Internal.Linear.Poly.denote' ctx
            (((p₂.tail.mul (-p₃.leadCoeff)).combine (p₃.tail.mul p₂.leadCoeff)).addConst (-p₃.leadCoeff * ↑k)))
-- Lean.Meta.Eqns
Lean.Meta.EqnsExtState.mk.sizeOf_spec : ∀ (mapInv : Lean.PHashMap Lean.Name Lean.Name), sizeOf { mapInv := mapInv } = 1 + sizeOf mapInv
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.injective : ∀ {α : Type u} [inst : DecidableEq α] (f : Plausible.InjectiveFunction α), Function.Injective f.apply
-- Mathlib.Order.Filter.Pointwise
Filter.tendsto_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] {a : Filter β} {f : β → α},
  Filter.Tendsto f a 0 ↔ ∀ᶠ (x : β) in a, f x = 0
-- Init.PropLemmas
and_congr_right' : ∀ {b c a : Prop}, (b ↔ c) → (a ∧ b ↔ a ∧ c)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_le_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : k ∈ t), (cmp (t.minKey ⋯) k).isLE = true
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKey?_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {f : β → β}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.minKey? (Std.Internal.List.Const.modifyKey k f l) =
      Option.map (fun km => if (km == k) = true then k else km) (Std.Internal.List.minKey? l)
-- Mathlib.LinearAlgebra.Span.Basic
/-- Taking the span by a large ring of the span by the small ring is the same as taking the span
by just the large ring.  -/
Submodule.span_span_of_tower : ∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set M) [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [IsScalarTower R S M],
  Submodule.span S ↑(Submodule.span R s) = Submodule.span S s
-- Mathlib.Probability.Independence.InfinitePi
/-- Given random variables `X i j : Ω i j → 𝓧 i j`, they are independent when viewed as random
variables defined on the product space `Π i, Π j, Ω i j`.  -/
ProbabilityTheory.iIndepFun_uncurry_infinitePi : ∀ {ι : Type u_1} {κ : ι → Type u_4} {𝓧 : (i : ι) → κ i → Type u_5} {m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)}
  {Ω : (i : ι) → κ i → Type u_6} {mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)}
  {X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j} (μ : (i : ι) → (j : κ i) → MeasureTheory.Measure (Ω i j))
  [∀ (i : ι) (j : κ i), MeasureTheory.IsProbabilityMeasure (μ i j)],
  (∀ (i : ι) (j : κ i), Measurable (X i j)) →
    ProbabilityTheory.iIndepFun (fun p ω => X p.fst p.snd (ω p.fst p.snd))
      (MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.infinitePi (μ i))
-- Mathlib.Algebra.Regular.Basic
Commute.isRegular_iff : ∀ {R : Type u_1} [inst : Mul R] {a : R}, (∀ (b : R), Commute a b) → (IsRegular a ↔ IsLeftRegular a)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.pre_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) {Y X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)}
  (f : Y ⟶ X), ((CategoryTheory.StructuredArrow.pre S F G).map f).left = CategoryTheory.CategoryStruct.id Y.left
-- Mathlib.Topology.Connected.Basic
/-- The preimage of a connected component of `F` is the union of the connected components of
`f ⁻¹' F` at the points of that preimage.  -/
ContinuousOn.preimage_connectedComponentIn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {F : Set β},
  ContinuousOn f (f ⁻¹' F) →
    ∀ (y : β), f ⁻¹' connectedComponentIn F y = ⋃ x ∈ f ⁻¹' connectedComponentIn F y, connectedComponentIn (f ⁻¹' F) x
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.composePath_nil : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C},
  CategoryTheory.composePath Quiver.Path.nil = CategoryTheory.CategoryStruct.id X
-- ProofWidgets.Component.RefreshComponent
/-- Initial state of the component.  -/
ProofWidgets.RefreshComponent.Props.state : ProofWidgets.RefreshComponent.Props → Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef