mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder
CStarAlgebra.convexOn_ringInverse : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  ConvexOn ℝ {a | IsStrictlyPositive a} Ring.inverse
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_eq_getD_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  {fallback : β}, m.getD a fallback = m[a]?.getD fallback
-- Mathlib.Data.Finset.Image
/-- Variant of `Finset.image_subset_image_iff` under an `InjOn` rather than `Injective`
hypothesis.  -/
Finset.image_subset_image_iff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s s₁ s₂ : Finset α},
  Set.InjOn f ↑s → s₁ ⊆ s → s₂ ⊆ s → (Finset.image f s₁ ⊆ Finset.image f s₂ ↔ s₁ ⊆ s₂)
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommProd.congr_simp : ∀ {α : Type u_3} {β : Type u_4} [inst : Monoid β] (s s_1 : Finset α) (e_s : s = s_1) (f f_1 : α → β) (e_f : f = f_1)
  (comm : (↑s).Pairwise (Function.onFun Commute f)), s.noncommProd f comm = s_1.noncommProd f_1 ⋯
-- Mathlib.Data.EReal.Basic
EReal.range_coe_ennreal : Set.range ENNReal.toEReal = Set.Ici 0
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.spec_le_iff : ∀ (R : CommRingCat) (p q : ↥(AlgebraicGeometry.Spec R)), p ≤ q ↔ q.asIdeal ≤ p.asIdeal
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.«builder_option(Transparency:=_)» : Lean.ParserDescr
-- Mathlib.Algebra.Group.End
Equiv.Perm.sumCongrHom_apply : ∀ (α : Type u_7) (β : Type u_8) (a : Equiv.Perm α × Equiv.Perm β), (Equiv.Perm.sumCongrHom α β) a = a.1.sumCongr a.2
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.exists_ne_zero_of_sum_ne_zero : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M}, ∑ x ∈ s, f x ≠ 0 → ∃ a ∈ s, f a ≠ 0
-- Init.Data.Int.Order
Int.sub_pos_of_lt : ∀ {a b : ℤ}, b < a → 0 < a - b
-- Mathlib.RingTheory.Finiteness.Basic
Submodule.fg_map_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_3}
  {P : Type u_4} [inst_3 : Semiring S] [inst_4 : AddCommMonoid P] [inst_5 : Module S P] {σ : R →+* S}
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] P),
  Function.Injective ⇑f → ∀ {N : Submodule R M}, (Submodule.map f N).FG ↔ N.FG
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.Hom.ofRel.sizeOf_spec : ∀ {X Y : CategoryTheory.RelCat} [inst : SizeOf X] [inst_1 : SizeOf Y] (rel : SetRel X Y), sizeOf { rel := rel } = 1
-- Mathlib.Computability.Primrec.List
/-- `List.modify` with a function depending on external data is primitive recursive.  -/
Primrec.list_modify' : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {g : β → α → α},
  Primrec₂ g → Primrec₂ fun l p => l.modify p.1 (g p.2)
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The canonical linear map `M ⧸ (I ^ n • ⊤) →ₗ[R] M ⧸ (I ^ m • ⊤)` for `m ≤ n` used
to define `AdicCompletion`.  -/
AdicCompletion.transitionMap : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {m n : ℕ} → m ≤ n → M ⧸ I ^ n • ⊤ →ₗ[R] M ⧸ I ^ m • ⊤
-- Lean.Level
Lean.Level.imax.inj : ∀ {a a_1 a_2 a_3 : Lean.Level}, a.imax a_1 = a_2.imax a_3 → a = a_2 ∧ a_1 = a_3
-- Lean.Meta.Tactic.Intro
/-- Introduce `n` binders in the goal `mvarId`. The new hypotheses are named using the binder names.
The suffix `P` stands for "preserving`.
 -/
Lean.MVarId.introNP : Lean.MVarId → ℕ → Lean.MetaM (Array Lean.FVarId × Lean.MVarId)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.shearMulRight_symm_coe : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G],
  ⇑(Homeomorph.shearMulRight G).symm = fun z => (z.1, z.1⁻¹ * z.2)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.powerBasisAux'.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R} (hg : g.Monic),
  AdjoinRoot.powerBasisAux' hg =
    Module.Basis.ofEquivFun
      { toFun := fun f i => ((AdjoinRoot.modByMonicHom hg) f).coeff ↑i, map_add' := ⋯, map_smul' := ⋯,
        invFun := fun c => (AdjoinRoot.mk g) (∑ i, (Polynomial.monomial ↑i) (c i)), left_inv := ⋯, right_inv := ⋯ }
-- Init.Prelude
/-- Run `x : m α` with a modified value for the `ref`  -/
Lean.MonadRef.withRef : {m : Type → Type} → [self : Lean.MonadRef m] → {α : Type} → Lean.Syntax → m α → m α
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
inv_riemannZeta_sub_sub_isBigO : (fun s => (riemannZeta s)⁻¹ - (s - 1)) =O[nhdsWithin 1 {1}ᶜ] fun s => (s - 1) ^ 2
-- Lean.Meta.WHNF
/-- Try to reduce matcher/recursor/quot applications. We say they are all "morally" recursor applications.  -/
Lean.Meta.reduceRecMatcher? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.finite_emptyOn : ∀ (α : Type u_2), (Matroid.emptyOn α).Finite
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  (CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₂ = CategoryTheory.CategoryStruct.id S.L₂
-- Mathlib.MeasureTheory.Integral.MeanInequalities
Real.conjExponent.eq_1 : ∀ (p : ℝ), p.conjExponent = p / (p - 1)
-- Mathlib.Algebra.Field.Defs
Semifield.toInv : {K : Type u_2} → [self : Semifield K] → Inv K
-- Mathlib.Algebra.Module.Torsion.Free
Module.IsTorsionFree.trans : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [Module.IsTorsionFree R M] [inst_6 : Module S R]
  [Module.IsTorsionFree S R] [IsScalarTower S R R] [SMulCommClass S R R] [IsScalarTower S R M], Module.IsTorsionFree S M
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, `HasSum` version.  -/
hasSum_coe_mul_geometric_of_norm_lt_one : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] {r : 𝕜}, ‖r‖ < 1 → HasSum (fun n => ↑n * r ^ n) (r / (1 - r) ^ 2)
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Hom.ext : ∀ {a b : SimplexCategory} (f g : a ⟶ b), SimplexCategory.Hom.toOrderHom f = SimplexCategory.Hom.toOrderHom g → f = g
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.ofInv_X' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (s : Y ⟶ X) (hs : W s), (CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).X' = Y
-- Mathlib.RingTheory.AdjoinRoot
/-- **Alias** of `AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk`. -/
AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f)
      ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.mk f) (Ideal.map Polynomial.C I))) ((AdjoinRoot.mk f) p)) =
    (DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p
-- Lean.Server.References
/-- Yields a map from all modules to all of their references.  -/
Lean.Server.References.allRefs : Lean.Server.References → Lean.Server.References.AllRefsMap
-- Mathlib.Data.Finset.Pi
Finset.pi_const_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] {β : Type u_2} (s : Finset α) (i : β), (s.pi fun x => {i}) = {fun x x_1 => i}
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.lift_symm_apply : ∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : CommGroup A] (f : Abelianization G →* A),
  Abelianization.lift.symm f = f.comp Abelianization.of
-- Mathlib.Data.List.AList
AList.instDecidableMem : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → (s : AList β) → Decidable (a ∈ s)
-- Mathlib.Order.SuccPred.Basic
Order.le_and_pred_le_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α},
  b ≤ a ∧ Order.pred a ≤ b ↔ b = a ∨ b = Order.pred a
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_eval_two_mul_zero : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.eval 0 (Polynomial.Chebyshev.T R (2 * n)) = ↑↑n.negOnePow
-- Init.Data.Bool
Bool.not_eq : ∀ {a b : Bool}, (!a) = b ↔ a ≠ b
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.MemLp.condExpL2_ae_eq_condExp' : ∀ {α : Type u_1} {E : Type u_3} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m m₀ : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → E} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : CompleteSpace E] [inst_4 : InnerProductSpace 𝕜 E] (hm : m ≤ m₀),
  MeasureTheory.Integrable f μ →
    ∀ (hf2 : MeasureTheory.MemLp f 2 μ) [MeasureTheory.SigmaFinite (μ.trim hm)],
      ↑↑↑((MeasureTheory.condExpL2 E 𝕜 hm) (MeasureTheory.MemLp.toLp f hf2)) =ᵐ[μ] μ[f | m]
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_le_mul_iff_of_pos_left : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, 0 < c → (c * a ≤ c * b ↔ a ≤ b)
-- Mathlib.Logic.Equiv.Basic
/-- A family of equivalences between fibers gives an equivalence between domains.  -/
Equiv.ofFiberEquiv : {α : Type u_13} →
  {β : Type u_14} →
    {γ : Type u_15} → {f : α → γ} → {g : β → γ} → ((c : γ) → { a // f a = c } ≃ { b // g b = c }) → α ≃ β
-- Init.Data.Array.Lemmas
Array.toList_flatten : ∀ {α : Type u_1} {xss : Array (Array α)}, xss.flatten.toList = (List.map Array.toList xss.toList).flatten
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- The parent pattern is the gadget `Grind.eqBwdPattern`.
In this case, we do not collect the symbols in ground children pattern.
 -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.ParentKind.eqBwdPattern : Lean.Meta.Grind.NormalizePattern.ParentKind✝
-- Mathlib.Topology.Constructions
mem_nhds_subtype : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X) (x : { x // x ∈ s }) (t : Set { x // x ∈ s }),
  t ∈ nhds x ↔ ∃ u ∈ nhds ↑x, Subtype.val ⁻¹' u ⊆ t
-- Mathlib.Topology.Algebra.Support
tsupport_mul_subset_left : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_9} [inst_1 : MulZeroClass α] {f g : X → α},
  (tsupport fun x => f x * g x) ⊆ tsupport f
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.foldUntil.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (x : Option α) →
      ((a : α) → motive (some a)) → ((x : Option α) → (∀ (a : α), x = some a → False) → motive x) → motive x
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.coeff.match_1.eq_1 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (a : ℤ) (y : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly)
  (h_1 :
    (a : ℤ) →
      (y : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add a y p))
  (h_2 : (k : ℤ) → motive (Int.Internal.Linear.Poly.num k)),
  (match Int.Internal.Linear.Poly.add a y p with
    | Int.Internal.Linear.Poly.add a y p => h_1 a y p
    | Int.Internal.Linear.Poly.num k => h_2 k) =
    h_1 a y p
-- Mathlib.Topology.GDelta.Basic
IsMeagre.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X), IsMeagre s = (sᶜ ∈ residual X)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] {c : CategoryTheory.Limits.Cocone F}
  (hc : CategoryTheory.Limits.IsColimit c) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j)
      (hc.coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit F)).inv =
    c.ι.app j
-- Init.Grind.Util
/-- Gadget for representing offsets `t+k` in patterns.  -/
Lean.Grind.offset : ℕ → ℕ → ℕ
-- Init.Data.UInt.BasicAux
/-- Converts a 64-bit unsigned integer to an arbitrary-precision natural number.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.toNat : UInt64 → ℕ
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsWide.eqToHom_mem : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  S.IsWide → ∀ {c d : C} (h : c = d), CategoryTheory.eqToHom h ∈ S.arrows c d
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCircuit.ne_nil : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCircuit → p ≠ SimpleGraph.Walk.nil
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.FormallyUnramified fun {R S} [CommRing R] [CommRing S] =>
  RingHom.FormallyUnramified
-- Mathlib.LinearAlgebra.Complex.Module
imaginaryPart_imaginaryPart : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : A}, imaginaryPart ↑(imaginaryPart x) = 0
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.comp.injEq : ∀ (a a_1 a_2 a_3 : Nat.Partrec.Code), (a.comp a_1 = a_2.comp a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Logic.Function.Conjugate
Function.Semiconj₂.isAssociative_left : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {ga : α → α → α} {gb : β → β → β} [Std.Associative gb],
  Function.Semiconj₂ f ga gb → Function.Injective f → Std.Associative ga
-- Init.Data.ByteArray.Bootstrap
_private.Init.Data.ByteArray.Bootstrap.0.List.toList_data_toByteArray.toList_push : ∀ {xs : Array UInt8} {x : UInt8}, (xs.push x).toList = xs.toList ++ [x]
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.resolutionMap_succ : ∀ {k : Type u} {G H : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ),
  ContinuousCohomology.resolutionMap φ f (i + 1) =
    TopRep.ofHom (ContRepresentation.coind₁ResMap φ (TopRep.Hom.hom (ContinuousCohomology.resolutionMap φ f i)))
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instModuleReal : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Module ℝ (CuspForm Γ k)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- The type of all partial Hahn embeddings.  -/
HahnEmbedding.Partial : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] → HahnEmbedding.Seed K M R → Type (max 0 u_2 u_3)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₂ → (t₁ ∪ t₂).getD k fallback = t₁.getD k fallback
-- Init.Data.Range.Polymorphic.NatLemmas
List.range'_eq_toList_rco : ∀ {m n : ℕ}, List.range' m n = (m...m + n).toList
-- Mathlib.Geometry.Polygon.Basic
/-- The vertices of the polygon, indexed by `Fin n`.  -/
Polygon.vertices : {P : Type u_1} → {n : ℕ} → Polygon P n → Fin n → P
-- Mathlib.Order.Defs.PartialOrder
instIsPreorder_mathlib : ∀ {α : Type u_1} [inst : Preorder α], Std.IsPreorder α
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.instDecidableOfExistsAddUnitsEqVal.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (x : M) [h : Decidable (∃ u, ↑u = x)],
  IsAddUnit.instDecidableOfExistsAddUnitsEqVal x = h
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- An arbitrary choice of weak limit object of a functor.  -/
CategoryTheory.Limits.weakLimit : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {C : Type u_3} →
      [inst_1 : CategoryTheory.Category.{v_3, u_3} C] →
        (F : CategoryTheory.Functor J C) → [CategoryTheory.Limits.HasWeakLimit F] → C
-- Mathlib.Tactic.NormNum.IsCoprime
Mathlib.Meta.NormNum.isInt_isCoprime : ∀ {x y nx ny : ℤ}, Mathlib.Meta.NormNum.IsInt x nx → Mathlib.Meta.NormNum.IsInt y ny → IsCoprime nx ny → IsCoprime x y
-- Mathlib.Algebra.Group.Action.Hom
monoidHomEquivMulActionIsScalarTower.eq_1 : ∀ (M : Type u_4) (N : Type u_5) [inst : Monoid M] [inst_1 : Monoid N],
  monoidHomEquivMulActionIsScalarTower M N =
    { toFun := fun f => ⟨MulAction.compHom N f, ⋯⟩,
      invFun := fun x =>
        match x with
        | ⟨val, property⟩ => MonoidHom.smulOneHom,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The `Equiv` underlying a `MulEquiv`.  -/
MulEquiv.toEquiv : {M : Type u_9} → {N : Type u_10} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → M ≃ N
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_not : ∀ {v i : ℕ} {x : BitVec v}, (~~~x).getLsbD i = (decide (i < v) && !x.getLsbD i)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.toAdjunction.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D),
  e.toAdjunction = { unit := e.unit, counit := e.counit, left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableOn.mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a b : E → 𝔸}, DifferentiableOn 𝕜 a s → DifferentiableOn 𝕜 b s → DifferentiableOn 𝕜 (a * b) s
-- Mathlib.Algebra.CharP.Frobenius
RingHom.map_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] (g : R →+* S) (p : ℕ)
  [inst_2 : ExpChar R p] [inst_3 : ExpChar S p] (x : R), g ((frobenius R p) x) = (frobenius S p) (g x)
-- Mathlib.Algebra.Group.Center
IsMulCentral.mk : ∀ {M : Type u_1} [inst : Mul M] {z : M},
  (∀ (a : M), Commute z a) →
    (∀ (b c : M), z * (b * c) = z * b * c) → (∀ (a b : M), a * b * z = a * (b * z)) → IsMulCentral z
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derivedε_fac_app_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₂.IsLocalization W₂] {G' : CategoryTheory.Functor D₁ D₂}
  {F' : CategoryTheory.Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F')
  [inst_5 :
    (F'.comp G').IsRightDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂]
  (X₂ : C₂) {Z : D₂} (h : L₂.obj X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G'.map (β.app X₂))
      (CategoryTheory.CategoryStruct.comp ((adj.derivedε W₂ α β).app (L₂.obj X₂)) h) =
    CategoryTheory.CategoryStruct.comp (α.app (F.obj X₂))
      (CategoryTheory.CategoryStruct.comp (L₂.map (adj.counit.app X₂)) h)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- `lpMeasSubgroup` and `lpMeas` are isometric.  -/
MeasureTheory.lpMeasSubgroupToLpMeasIso : {α : Type u_1} →
  (F : Type u_2) →
    (𝕜 : Type u_3) →
      (p : ENNReal) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup F] →
            [inst_2 : NormedSpace 𝕜 F] →
              {m m0 : MeasurableSpace α} →
                (μ : MeasureTheory.Measure α) →
                  [inst_3 : Fact (1 ≤ p)] → ↥(MeasureTheory.lpMeasSubgroup F m p μ) ≃ᵢ ↥(MeasureTheory.lpMeas F 𝕜 m p μ)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.fst.sizeOf_spec : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : SizeOf α₁] [inst_1 : SizeOf α₂]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] (a : Std.IterM m β) (a_1 : Std.IterM m β),
  sizeOf (Std.Iterators.Types.Append.fst a a_1) = 1 + sizeOf a + sizeOf a_1
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.collect : Lean.CollectLevelParams.State → Lean.Expr → Lean.CollectLevelParams.State
-- Init.System.IOError
/-- An inappropriate I/O control operation was attempted.

This corresponds to the POSIX error `ENOTTY`.
 -/
IO.Error.illegalOperation : UInt32 → String → IO.Error
-- Mathlib.RingTheory.Multiplicity
emultiplicity_one_left : ∀ {α : Type u_1} [inst : Monoid α] (b : α), emultiplicity 1 b = ⊤
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
/-- The `ℤ`-algebra equivalence between `Subring.closure s` and `Algebra.adjoin ℤ s` given by
the identity map.  -/
Subring.closureEquivAdjoinInt : {R : Type u_1} → [inst : Ring R] → (s : Set R) → ↥(Subring.closure s) ≃ₐ[ℤ] ↥(Algebra.adjoin ℤ s)
-- Mathlib.CategoryTheory.Iso
/-- The `IsIso` typeclass expresses that a morphism is invertible.

Given a morphism `f` with `IsIso f`, one can view `f` as an isomorphism via `asIso f` and get
the inverse using `inv f`.  -/
CategoryTheory.IsIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → Prop
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqPublishDiagnosticsParams.beq : Lean.Lsp.PublishDiagnosticsParams → Lean.Lsp.PublishDiagnosticsParams → Bool
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.instCoeOutSubmodule : {R : Type u} →
  [inst : CommRing R] →
    {M : Type v} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {k : ℕ} → CoeOut (Module.Grassmannian R M k) (Submodule R M)
-- Init.Grind.Lemmas
Lean.Grind.false_of_not_eq_self : ∀ {a : Prop}, (¬a) = a → False
-- Init.Prelude
/-- The first element of a pair.  -/
MProd.fst : {α β : Type u} → MProd α β → α
-- Mathlib.Data.List.DropRight
List.rtakeWhile_nil : ∀ {α : Type u_1} (p : α → Bool), List.rtakeWhile p [] = []
-- Mathlib.Algebra.Torsor.Basic
sdiv_div_sdiv_comm : ∀ {G : Type u_1} {P : Type u_2} [inst : CommGroup G] [inst_1 : Torsor G P] (p₁ p₂ p₃ p₄ : P),
  (p₁ /ₛ p₂) / (p₃ /ₛ p₄) = (p₁ /ₛ p₃) / (p₂ /ₛ p₄)