mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Hom
RingHom.equivNatAlgHom_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S),
  (RingHom.equivNatAlgHom R S) f = f.toNatAlgHom
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.minView!.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) →
      (l : Std.DTreeMap.Internal.Impl α β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k' : α) →
                (v' : β k') →
                  (l' r' : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')) →
            motive l
-- Mathlib.Control.Functor
_private.Mathlib.Control.Functor.0.Functor.Comp.map.match_1.splitter : {F : Type u_1 → Type u_3} →
  {G : Type u_2 → Type u_1} →
    {α : Type u_2} →
      (motive : Functor.Comp F G α → Sort u_4) → (x : Functor.Comp F G α) → ((x : F (G α)) → motive x) → motive x
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
/-- The topological closure of the non-unital subalgebra generated by a single element.  -/
NonUnitalAlgebra.elemental : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] →
          [IsScalarTower R A A] →
            [SMulCommClass R A A] →
              [inst_5 : TopologicalSpace A] →
                [IsSemitopologicalSemiring A] → [ContinuousConstSMul R A] → A → NonUnitalSubalgebra R A
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.IsMeasurableRatCDF_defaultRatCDF : ∀ (α : Type u_2) [inst : MeasurableSpace α],
  ProbabilityTheory.IsMeasurableRatCDF fun x q => ProbabilityTheory.defaultRatCDF q
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- Polarization restricted to `S`-span of roots.  -/
RootPairing.CoPolarizationIn : {ι : 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] →
                  (P : RootPairing ι R M N) →
                    (S : Type u_5) →
                      [inst_5 : CommRing S] →
                        [inst_6 : Algebra S R] →
                          [FaithfulSMul S R] →
                            [inst_8 : Module S M] →
                              [inst_9 : Module S N] →
                                [IsScalarTower S R N] → [P.IsValuedIn S] → [Fintype ι] → ↥(P.corootSpan S) →ₗ[S] M
-- Mathlib.Data.List.Nodup
List.Nodup.getElem_inj_iff : ∀ {α : Type u} {l : List α}, l.Nodup → ∀ {i : ℕ} {hi : i < l.length} {j : ℕ} {hj : j < l.length}, l[i] = l[j] ↔ i = j
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.inter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Raw α β),
  m₁.inter m₂ =
    if h₁ : 0 < m₁.buckets.size then
      if h₂ : 0 < m₂.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩) else m₁
    else m₂
-- Lean.Meta.Transform
Lean.TransformStep : Type
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.equivalence_rel : ∀ {X Y : AlgebraicGeometry.Scheme}, Equivalence AlgebraicGeometry.Scheme.PartialMap.equiv
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.BimonObj.mul_counit : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (M : C) [self : CategoryTheory.BimonObj M],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.counit =
    CategoryTheory.ComonObj.counit
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.lt_def : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupNorm E}, p < q ↔ ⇑p < ⇑q
-- Mathlib.CategoryTheory.Sites.Spaces
/-- The pretopology associated to a space induces the Grothendieck topology associated to the space.
 -/
Opens.pretopology_toGrothendieck : ∀ (T : Type u) [inst : TopologicalSpace T], (Opens.pretopology T).toGrothendieck = Opens.grothendieckTopology T
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- If the category `C` has pullbacks, this is an alternative condition for a family of elements to be
compatible: For any `f : Y ⟶ X` and `g : Z ⟶ X` in the presieve `R`, the restriction of the
given elements for `f` and `g` to the pullback agree.
This is equivalent to being compatible (provided `C` has pullbacks), shown in
`pullbackCompatible_iff`.

This is the definition for a "matching" family given in [MM92], Chapter III, Section 4,
Equation (5). Viewing the type `FamilyOfElements` as the middle object of the fork in
https://stacks.math.columbia.edu/tag/00VM, this condition expresses that `pr₀* (x) = pr₁* (x)`,
using the notation defined there.

For a more explicit version in the case where `R` is of the form `Presieve.ofArrows`, see
`CategoryTheory.Presieve.Arrows.PullbackCompatible`.
 -/
CategoryTheory.Presieve.FamilyOfElements.PullbackCompatible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X : C} →
        {R : CategoryTheory.Presieve X} → CategoryTheory.Presieve.FamilyOfElements P R → [R.HasPairwisePullbacks] → Prop
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_monoidHom_refl : ∀ {R : Type u_4} [inst : NonAssocSemiring R], ↑(RingEquiv.refl R) = MonoidHom.id R
-- Std.Async.Signal
/-- CPU time limit exceeded.
 -/
Std.Async.Signal.sigxcpu : Std.Async.Signal
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.endofunctorMonoidalCategory_tensorObj_map : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C C) {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).map f = G.map (F.map f)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.iso_inv_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π (F.map f))
      (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv =
    F.map (CategoryTheory.Abelian.coimage.π f)
-- Init.Data.BitVec.Bitblast
BitVec.getLsbD_sub : ∀ {w i : ℕ} {i_lt : i < w} {x y : BitVec w},
  (x - y).getLsbD i = (x.getLsbD i ^^ ((~~~y + 1#w).getLsbD i ^^ BitVec.carry i x (~~~y + 1#w) false))
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
_private.Mathlib.Analysis.BoxIntegral.Partition.Additive.0.Option.elim'.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_toList_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {k : α} {v : β k}, t.WF → (⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.contains (t.minD fallback) = true
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] (S : J.MayerVietorisSquare)
  [inst_2 : CategoryTheory.HasWeakSheafify J AddCommGrpCat],
  (S.map
      (CategoryTheory.yoneda.comp
        (((CategoryTheory.Functor.whiskeringRight Cᵒᵖ (Type v) AddCommGrpCat).obj AddCommGrpCat.free).comp
          (CategoryTheory.presheafToSheaf J AddCommGrpCat)))).IsPushout
-- Init.Meta.Defs
Lean.Name.appendIndexAfter : Lean.Name → ℕ → Lean.Name
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Given `e` a `match`-expression condition, returns the left-hand side
of the ground equations, **and** function application that abstracts the left-hand sides.
As an example, assume we have a `match`-expression condition `C₁` of the form
```
Grind.MatchCond (∀ y₁ y₂ y₃, t = .mk₁ y₁ → s = .mk₂ y₂ y₃ → False)
```
then the result returned by this function is
```
(#[t, s], (fun x₁ x₂ => (∀ y₁ y₂ y₃, x₁ = .mk₁ y₁ → x₂ = .mk₂ y₂ y₃ → False)) t s)
```
Note that the returned expression is definitionally equal to `C₁`.
We use this expression to detect whether two different `match`-expression conditions are
congruent.
For example, suppose we also have the `match`-expression `C₂` of the form
```
Grind.MatchCond (∀ y₁ y₂ y₃, a = .mk₁ y₁ → b = .mk₂ y₂ y₃ → False)
```
This function would return
```
(#[a, b], (fun x₁ x₂ => (∀ y₁ y₂ y₃, x₁ = .mk₁ y₁ → x₂ = .mk₂ y₂ y₃ → False)) a b)
```
Note that the lambda abstraction is identical to the first one. Let's call it `l`.
Thus, we can write the two pairs above as
- `(#[t, s], l t s)`
- `(#[a, b], l a b)`
Moreover, `C₁` is definitionally equal to `l t s`, and `C₂` is definitionally equal to `l a b`.
Then, if `grind` infers that `t = a` and `s = b`, it will detect that `l t s` and `l a b` are
equal by congruence, and consequently `C₁` is equal to `C₂`.

Gruesome details for heterogeneous equalities.

When pattern matching on indexing families, the generated conditions often use heterogeneous equalities. Here is an example:
```
(∀ (x : Vec α 0), n = 0 → as ≍ Vec.nil → bs ≍ x → False)
```
In this case, it is not sufficient to abstract the left-hand side. We also have
to abstract its type. The following is produced in this case.
```
(#[n, Vec α n, as, Vec α n, bs],
 (fun (x_0 : Nat) (ty_1 : Type u_1) (x_1 : ty_1) (ty_2 : Type u_1) (x_2 : ty_2) =>
    ∀ (x : Vec α 0), x_0 = 0 → x_1 ≍ Vec.nil → x_2 ≍ x → False)
 n (Vec α n) as (Vec α n) bs)
```
The example makes it clear why this is needed, `as` and `bs` depend on `n`.
Note that we can abstract the type without introducing type errors because
heterogeneous equality is used for `as` and `bs`.
 -/
Lean.Meta.Grind.collectMatchCondLhssAndAbstract : Lean.Expr → Lean.Meta.Grind.GoalM (Array Lean.Expr × Lean.Expr)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
/-- The (pre)image under `inv` of `Ioo 0 a` is `Ioi a⁻¹`.  -/
Set.inv_Ioo_0_left : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosReflectLT G₀]
  {a : G₀}, 0 < a → (Set.Ioo 0 a)⁻¹ = Set.Ioi a⁻¹
-- Mathlib.Logic.Encodable.Basic
Encodable.decode₂_encode : ∀ {α : Type u_1} [inst : Encodable α] (a : α), Encodable.decode₂ α (Encodable.encode a) = some a
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The cofan constructed of the inclusions from the coproduct is colimiting.  -/
CategoryTheory.Limits.coproductIsCoproduct : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f : β → C) →
        [inst_1 : CategoryTheory.Limits.HasCoproduct f] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (∐ f) (CategoryTheory.Limits.Sigma.ι f))
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.X_pow_sub_one_mul_prod_cyclotomic_eq_X_pow_sub_one_of_dvd : ∀ (R : Type u_1) [inst : CommRing R] {d n : ℕ},
  d ∣ n →
    n ≠ 0 → (Polynomial.X ^ d - 1) * ∏ x ∈ n.divisors \ d.divisors, Polynomial.cyclotomic x R = Polynomial.X ^ n - 1
-- Mathlib.Topology.Compactness.Lindelof
/-- A set `s` is Hereditarily Lindelöf if every subset is a Lindelof set. We require this only
for open sets in the definition, and then conclude that this holds for all sets by ADD.  -/
IsHereditarilyLindelof : {X : Type u} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.Algebra.QuadraticAlgebra.Basic
QuadraticAlgebra.im_div : ∀ {K : Type u_1} [inst : Field K] {a b : K} (w z : QuadraticAlgebra K a b),
  (w / z).im =
    -(w.re * ((QuadraticAlgebra.norm z)⁻¹ * z.im)) + w.im * ((QuadraticAlgebra.norm z)⁻¹ * (z.re + b * z.im)) +
      -(b * w.im * ((QuadraticAlgebra.norm z)⁻¹ * z.im))
-- Mathlib.GroupTheory.Index
Subgroup.sq_mem_of_index_two : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 → ∀ (a : G), a ^ 2 ∈ H
-- Lean.Meta.Sym.Arith.Types
/-- `Semiring` instance for `type`  -/
Lean.Meta.Sym.Arith.Ring.semiringInst : Lean.Meta.Sym.Arith.Ring → Lean.Expr
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.relabel_unsat_iff_of_Nonempty : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {idx : ℕ} {invert : Bool} [Nonempty α] {aig : Std.Sat.AIG α} {r : α → β}
  {hidx1 : idx < (Std.Sat.AIG.relabel r aig).decls.size} {hidx2 : idx < aig.decls.size},
  (∀ (x y : α), x ∈ aig → y ∈ aig → r x = r y → x = y) →
    ((Std.Sat.AIG.relabel r aig).UnsatAt idx invert hidx1 ↔ aig.UnsatAt idx invert hidx2)
-- Mathlib.Data.Set.Image
Set.preimage_id' : ∀ {α : Type u_1} {s : Set α}, (fun x => x) ⁻¹' s = s
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finrank_top : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E], Module.finrank (↥⊤) E = 1
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.mk.inj : ∀ {G : Type w} {inst : TopologicalSpace G} {toFun : TopologicalSpace.Compacts G → NNReal}
  {mono' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun K₁ ≤ toFun K₂}
  {sup_disjoint' :
    ∀ (K₁ K₂ : TopologicalSpace.Compacts G),
      Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂}
  {sup_le' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂}
  {toFun_1 : TopologicalSpace.Compacts G → NNReal}
  {mono'_1 : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun_1 K₁ ≤ toFun_1 K₂}
  {sup_disjoint'_1 :
    ∀ (K₁ K₂ : TopologicalSpace.Compacts G),
      Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun_1 (K₁ ⊔ K₂) = toFun_1 K₁ + toFun_1 K₂}
  {sup_le'_1 : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun_1 (K₁ ⊔ K₂) ≤ toFun_1 K₁ + toFun_1 K₂},
  { toFun := toFun, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' } =
      { toFun := toFun_1, mono' := mono'_1, sup_disjoint' := sup_disjoint'_1, sup_le' := sup_le'_1 } →
    toFun = toFun_1
-- Lean.Meta.Diagnostics
Lean.Meta.DiagSummary.mk.injEq : ∀ (data : Array Lean.MessageData) (max : ℕ) (data_1 : Array Lean.MessageData) (max_1 : ℕ),
  ({ data := data, max := max } = { data := data_1, max := max_1 }) = (data = data_1 ∧ max = max_1)
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_natAddEmb_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.natAddEmb m) (Finset.Ioc i j) = Finset.Ioc (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.Order.Filter.AtTopBot.ModEq
Nat.frequently_even : ∃ᶠ (m : ℕ) in Filter.atTop, Even m
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.uniqueUpToIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C),
  (𝒞₁.uniqueUpToIso 𝒞₂).hom = 𝒞₁.hom 𝒞₂
-- Mathlib.Algebra.Order.Group.Synonym
toLex_one : ∀ {α : Type u_1} [inst : One α], toLex 1 = 1
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_isCircuit_iff : ∀ {α : Type u_1} {M : Matroid α} {D C : Set α}, (M.delete D).IsCircuit C ↔ M.IsCircuit C ∧ Disjoint C D
-- Mathlib.Data.Set.Function
Set.LeftInvOn.extendDomain : ∀ {α : Type u_1} {β : Type u_2} {p : β → Prop} [inst : DecidablePred p] {f : α ≃ Subtype p} {g₁ g₂ : Equiv.Perm α}
  {s : Set α},
  Set.LeftInvOn (⇑g₁) (⇑g₂) s → Set.LeftInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' s)
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- If `F ⋙ G` is full and `G` is faithful, then `F` is full.  -/
CategoryTheory.Functor.Full.of_comp_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [(F.comp G).Full] [G.Faithful], F.Full
-- Mathlib.Topology.Separation.Hausdorff
Set.pairwiseDisjoint_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] (s : Set X), s.PairwiseDisjoint nhds
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_bracket : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  (x y : ↥L'), ↑⁅x, y⁆ = ⁅↑x, ↑y⁆
-- Mathlib.Topology.Compactness.LocallyCompact
instLocallyCompactPairOfLocallyCompactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyCompactSpace X],
  LocallyCompactPair X Y
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `smul_apply`. -/
MeasureTheory.VectorMeasure.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Data.Nat.Factorization.Basic
Nat.prod_primeFactors_dvd : ∀ (n : ℕ), ∏ p ∈ n.primeFactors, p ∣ n
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instSMul'.eq_1 : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α], OrderDual.instSMul' = inst
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.instBot : {α : Type u_1} → [inst : LE α] → Bot (LowerSet α)
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.coe_mul_eq_bind : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : α},
  a ≠ 0 → ∀ (b : WithBot α), ↑a * b = Option.bind b fun b => some (a * b)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_eq_two_iff : ∀ {α : Type u}, Cardinal.mk α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = Set.univ
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.prod.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (w : Monoid.CoprodI.Word M),
  w.prod = (List.map (fun l => Monoid.CoprodI.of l.snd) w.toList).prod
-- Mathlib.Topology.Algebra.Algebra
Algebra.elemental.instCompleteSpaceSubtypeMemSubalgebra : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u_2} [inst_1 : UniformSpace A] [CompleteSpace A]
  [inst_3 : Semiring A] [inst_4 : IsSemitopologicalSemiring A] [inst_5 : Algebra R A] (x : A),
  CompleteSpace ↥(Algebra.elemental R x)
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.mul_left : ∀ {M : Type u_1} [inst : Monoid M] (a : M) {b c : M}, Associated b c → Associated (a * b) (a * c)
-- Mathlib.Data.Int.Init
Int.sign_add_eq_of_sign_eq : ∀ {m n : ℤ}, m.sign = n.sign → (m + n).sign = n.sign
-- Mathlib.Algebra.IsPrimePow
not_isPrimePow_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R], ¬IsPrimePow 1
-- Std.Http.Data.URI.Basic
Std.Http.URI.UserInfo.mk.sizeOf_spec : ∀ (username : Std.Http.URI.EncodedUserInfo) (password : Option Std.Http.URI.EncodedUserInfo),
  sizeOf { username := username, password := password } = 1 + sizeOf username + sizeOf password
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly : ∀ {n : Type u} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤))),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.homOfVector f v)
      (AlgebraicGeometry.AffineSpace.toSpecMvPoly n S) =
    (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n).symm v
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.Hom.ext : ∀ {M N : SemiNormedGrp₁} {x y : M.Hom N}, x.hom' = y.hom' → x = y
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_counitIso_hom_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology D) A) (X_1 : Dᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).counitIso.hom.app X).hom.app X_1 =
    X.obj.map (e.counitIso.inv.app (Opposite.unop X_1)).op
-- Lean.Parser.Attr
Lean.Parser.Attr.specialize : Lean.Parser.Parser
-- Mathlib.Order.LiminfLimsup
Filter.cofinite.bliminf_set_eq : ∀ {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α},
  Filter.bliminf s Filter.cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableAt.snd : ∀ {𝕜 : 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'] {F : Type u_11}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_12} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_13} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {f : N → M × M'} {x : N}, MDiffAt f x → (MDiffAt fun x => (f x).2) x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : Inhabited β] {a : α} {c : ℕ},
  Std.DHashMap.Const.get! (Std.DHashMap.emptyWithCapacity c) a = default
-- Lean.Message
Lean.MessageSeverity.toString : Lean.MessageSeverity → String
-- Mathlib.Algebra.Order.Quantale
Quantale.rightMulResiduation_le_iff_mul_le : ∀ {α : Type u_1} {x y z : α} [inst : Semigroup α] [inst_1 : CompleteLattice α] [IsQuantale α],
  x ≤ Quantale.rightMulResiduation y z ↔ y * x ≤ z
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.compare_def : ∀ {x : ℚ} {a b : Std.Time.Internal.UnitVal x}, compare a b = compare a.val b.val
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonWorkDoneProgressParams : Lean.FromJson Lean.Lsp.WorkDoneProgressParams
-- Mathlib.Order.Interval.Set.Image
StrictMonoOn.image_Ioo_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  StrictMonoOn f (Set.Icc a b) → f '' Set.Ioo a b ⊆ Set.Ioo (f a) (f b)
-- Mathlib.Data.FinEnum
/-- `FinEnum.card` is the cardinality of the `FinEnum`  -/
FinEnum.card : (α : Sort u_1) → [self : FinEnum α] → ℕ
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.mk_eq_bot_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p : Submodule R M} (hp : p ∈ f.invtSubmodule), ⟨p, hp⟩ = ⊥ ↔ p = ⊥