mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.LetToHave
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.Result.mk.injEq : ∀ (expr : Lean.Expr) (type? : Option Lean.Expr) (expr_1 : Lean.Expr) (type?_1 : Option Lean.Expr),
  ({ expr := expr, type? := type? } = { expr := expr_1, type? := type?_1 }) = (expr = expr_1 ∧ type? = type?_1)
-- Init.Data.Ord.UInt
UInt64.instOrd : Ord UInt64
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.instLifting₂LocalizedMonoidalToMonoidalCategoryCompFunctorCurriedTensorObjWhiskeringRightTensorBifunctor : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      CategoryTheory.Localization.Lifting₂
                        (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)
                        (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε) W W
                        ((CategoryTheory.MonoidalCategory.curriedTensor C).comp
                          ((CategoryTheory.Functor.whiskeringRight C C (CategoryTheory.LocalizedMonoidal L W ε)).obj
                            (CategoryTheory.Localization.Monoidal.toMonoidalCategory L W ε)))
                        (CategoryTheory.Localization.Monoidal.tensorBifunctor L W ε)
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Additive monoid homomorphism between the function spaces `I → α` and `I → β`, induced by an
additive monoid homomorphism `f` between `α` and `β`  -/
AddMonoidHom.compLeft : {α : Type u_5} →
  {β : Type u_6} → [inst : AddZeroClass α] → [inst_1 : AddZeroClass β] → (α →+ β) → (I : Type u_7) → (I → α) →+ I → β
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.instMulI : (G : Type u) → (H : Type v) → [Mul G] → [Mul H] → (b : Bool) → Mul (I✝ G H b)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.ι_desc : ∀ {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)
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) (CategoryTheory.Limits.colimit.desc F c) =
    c.ι.app j
-- Std.Time.Zoned.Database.TZdb
/-- Parsed form of the `TZ` environment variable.

The POSIX proleptic format (e.g. `TZ=EST5EDT,M3.2.0,M11.1.0`) is not supported;
only file paths and timezone IDs backed by zoneinfo data are recognized.
 -/
Std.Time.Database.TZdb.TZSpec : Type
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.hasFPowerSeriesOnBall_bilinear : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  HasFPowerSeriesOnBall (fun x => (f x.1) x.2) (f.fpowerSeriesBilinear x) x ⊤
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_union_of_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ → k ∈ t₁ ∪ t₂
-- Mathlib.Order.TypeTags
/-- The canonical map from `α` into `WithTop α`  -/
WithTop.some : {α : Type u_1} → α → WithTop α
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.iso_symm_apply' : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M') (a : M) (b : ↥S),
  b • m = f a → (IsLocalizedModule.iso S f).symm m = LocalizedModule.mk a b
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_mul : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (e e' : P₁ ≃ᵃ[k] P₁), ⇑(e * e') = ⇑e ∘ ⇑e'
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.pow_scaleRoots' : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) (r : R) (n : ℕ),
  p.leadingCoeff ^ n ≠ 0 → (p ^ n).scaleRoots r = p.scaleRoots r ^ n
-- Mathlib.Logic.Denumerable
/-- Denumerability is conserved by equivalences. This is transitivity of equivalence the denumerable
way.  -/
Denumerable.ofEquiv : (α : Type u_3) → {β : Type u_4} → [Denumerable α] → β ≃ α → Denumerable β
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_add_of_lt : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    ∀ {m : ℕ},
      m < n →
        ∀ {x y : A},
          x ∈ I →
            y ∈ I →
              DividedPowers.OfInvertibleFactorial.dpow I m (x + y) =
                ∑ k ∈ Finset.HasAntidiagonal.antidiagonal m,
                  DividedPowers.OfInvertibleFactorial.dpow I k.1 x * DividedPowers.OfInvertibleFactorial.dpow I k.2 y
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.mkEqTransResultStep : Lean.Meta.Simp.Result → Lean.Meta.Simp.Step → Lean.MetaM Lean.Meta.Simp.Step
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Given a pointwise right Kan extension of `F` along `L` at `c`, exhibits
`(RightExtension.whiskerRight L F G).obj E` as a pointwise right Kan extension of `F ⋙ G` along
`L` at `c`.  -/
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtensionAt.postcompose : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  {F : CategoryTheory.Functor A B} →
                    {L : CategoryTheory.Functor A C} →
                      {c : C} →
                        [G.PreservesPointwiseRightKanExtensionAt F L c] →
                          {E : L.RightExtension F} →
                            E.IsPointwiseRightKanExtensionAt c →
                              ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj
                                    E).IsPointwiseRightKanExtensionAt
                                c
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_congr : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} {f g : G →* H} {φ : Rep.res f A ⟶ B} {ψ : Rep.res g A ⟶ B},
  f = g →
    (Rep.Hom.hom φ).toLinearMap = (Rep.Hom.hom ψ).toLinearMap →
      groupCohomology.cochainsMap f φ = groupCohomology.cochainsMap g ψ
-- Mathlib.Algebra.Order.Monovary
monovary_neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Monovary (-f) g ↔ Antivary f g
-- Mathlib.Order.BourbakiWitt
CompleteLattice.ωScottContinuous.sSup : ∀ {α : Type u_1} {β : Type u_2} [inst : OmegaCompletePartialOrder α] [inst_1 : CompleteLattice β] {s : Set (α → β)},
  (∀ f ∈ s, OmegaCompletePartialOrder.ωScottContinuous f) → OmegaCompletePartialOrder.ωScottContinuous (sSup s)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis.contract_isBasis_of_disjoint : ∀ {α : Type u_1} {M : Matroid α} {I J X C : Set α},
  M.IsBasis I X → M.IsBasis J C → Disjoint C X → M.Indep (I ∪ J) → (M.contract C).IsBasis I X
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.instSupSet : {α : Type u_1} → [LE α] → [SupSet α] → SupSet (WithTop α)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.prod_toFun : ∀ {R : Type u} [inst : Monoid R] {A : Type v} {B : Type w} {C : Type w₁} [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : NonUnitalNonAssocSemiring C]
  [inst_5 : DistribMulAction R B] [inst_6 : DistribMulAction R C] (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) (i : A),
  (f.prod g) i = Function.prod (⇑f) (⇑g) i
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctor₁₂BifunctorMapObj_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₁₂ : Type u_5}
  [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} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C₁₂] {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃] {j : J} {A : C₄}
  {f g :
    CategoryTheory.GradedObject.mapBifunctorMapObj G ρ₁₂.q
        (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶
      A},
  (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) f =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h) g) →
    f = g
-- Batteries.Recycling.RBTree.WF
/-- The balance properties of the `append` function.  -/
RBTree.RBNode.Balanced.append : ∀ {α : Type u_1} {c₁ : RBTree.RBColor} {n : ℕ} {c₂ : RBTree.RBColor} {l r : RBTree.RBNode α},
  l.Balanced c₁ n →
    r.Balanced c₂ n → RBTree.RBNode.RedRed (c₁ = RBTree.RBColor.black → c₂ ≠ RBTree.RBColor.black) (l.append r) n
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.mk.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (pt : C) (ι : F ⟶ (CategoryTheory.Functor.const J).obj pt) (pt_1 : C)
  (ι_1 : F ⟶ (CategoryTheory.Functor.const J).obj pt_1),
  ({ pt := pt, ι := ι } = { pt := pt_1, ι := ι_1 }) = (pt = pt_1 ∧ ι ≍ ι_1)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.of.eq_1 : ∀ (M : Type u) [inst : CommGroup M], CommGrpCat.of M = { carrier := M, str := inst }
-- Mathlib.Data.Matrix.Basic
Matrix.entryLinearMap_toAddMonoidHom : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type u_11} [inst : Semiring R] [inst_1 : AddCommMonoid α]
  [inst_2 : Module R α] {i : m} {j : n}, ↑(Matrix.entryLinearMap R α i j) = Matrix.entryAddMonoidHom α i j
-- Mathlib.Order.Filter.Germ.Basic
Filter.const_eventuallyEq' : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [l.NeBot] {a b : β}, (∀ᶠ (x : α) in l, a = b) ↔ a = b
-- Init.GetElem
/-- `GetElem?.getElem!` succeeds and fails when `GetElem.getElem?` succeeds and fails.  -/
LawfulGetElem.getElem!_def : ∀ {cont : Type u} {idx : Type v} {elem : outParam (Type w)} {dom : outParam (cont → idx → Prop)}
  {ge : GetElem? cont idx elem dom} [self : LawfulGetElem cont idx elem dom] [inst : Inhabited elem] (c : cont)
  (i : idx),
  c[i]! =
    match c[i]? with
    | some e => e
    | none => default
-- Mathlib.CategoryTheory.Functor.Category
/-- A natural transformation is an epimorphism if each component is.  -/
CategoryTheory.NatTrans.epi_of_epi_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) [∀ (X : C), CategoryTheory.Epi (α.app X)], CategoryTheory.Epi α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.isoCartesianComon_inv_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Comon C),
  (CategoryTheory.isoCartesianComon A).inv.hom =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.cartesianComon C).obj A.X).X
-- Mathlib.RingTheory.Bialgebra.GroupLike
/-- The group-like elements form a submonoid.  -/
groupLikeSubmonoid : (R : Type u_1) → (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [Bialgebra R A] → Submonoid A
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.eq_neg_of_valMinAbs_eq_neg_valMinAbs : ∀ {n : ℕ} {a b : ZMod n}, a.valMinAbs = -b.valMinAbs → a = -b
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.foldr_induction.go : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} (motive : ℕ → β → Prop) {f : α → β → β},
  (∀ (i : Fin as.size) (b : β), motive (↑i + 1) b → motive (↑i) (f as[i] b)) →
    ∀ {i : ℕ} {b : β} (hi : i ≤ as.size), motive i b → motive 0 (Array.foldrM.fold f as 0 i hi b)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.instAdditiveLocalizationQ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (W : CategoryTheory.MorphismProperty C) [inst_2 : W.HasLeftCalculusOfFractions], W.Q.Additive
-- Mathlib.Data.Quot
/-- Noncomputably extract a representative of `Trunc α` (using the axiom of choice).  -/
Trunc.out : {α : Sort u_1} → Trunc α → α
-- Mathlib.Algebra.Group.Action.Pi
Pi.smulCommClass' : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} {β : ι → Type u_5} [inst : (i : ι) → SMul M (β i)]
  [inst_1 : (i : ι) → SMul (α i) (β i)] [∀ (i : ι), SMulCommClass M (α i) (β i)],
  SMulCommClass M ((i : ι) → α i) ((i : ι) → β i)
-- Mathlib.CategoryTheory.Category.Basic
CategoryTheory.Category.mk : {obj : Type u} →
  [toCategoryStruct : CategoryTheory.CategoryStruct.{v, u} obj] →
    autoParam (∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f = f)
        CategoryTheory.Category.id_comp._autoParam →
      autoParam
          (∀ {X Y : obj} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id Y) = f)
          CategoryTheory.Category.comp_id._autoParam →
        autoParam
            (∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
              CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h =
                CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))
            CategoryTheory.Category.assoc._autoParam →
          CategoryTheory.Category.{v, u} obj
-- Lean.Server.FileWorker.Utils
/-- The `IO.monoMsNow` time when the session expires. See `$/lean/rpc/keepAlive`.  -/
Lean.Server.FileWorker.RpcSession.expireTime : Lean.Server.FileWorker.RpcSession → ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_pi_sub : ∀ (x : ℂ), Complex.cos (↑Real.pi - x) = -Complex.cos x
-- Mathlib.Analysis.Normed.Module.Ball.Action
instSMulElemSphereOfNatRealBall : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] → [NormedSpace 𝕜 E] → {r : ℝ} → SMul ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)
-- Mathlib.Analysis.Calculus.Deriv.Pow
/-- Eta-expanded form of `derivWithin_pow` -/
derivWithin_fun_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    ∀ (n : ℕ), derivWithin (fun i => f i ^ n) s x = ↑n * f x ^ (n - 1) * derivWithin f s x
-- Mathlib.MeasureTheory.Integral.Prod
/-- A binary function is integrable if the function `y ↦ f (x, y)` is integrable for almost every
`x` and the function `x ↦ ∫ ‖f (x, y)‖ dy` is integrable.  -/
MeasureTheory.integrable_prod_iff : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  ⦃f : α × β → E⦄,
  MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
    (MeasureTheory.Integrable f (μ.prod ν) ↔
      (∀ᵐ (x : α) ∂μ, MeasureTheory.Integrable (fun y => f (x, y)) ν) ∧
        MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.instIteratorAccess : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [Std.PRange.LawfulUpwardEnumerable α] → Std.IteratorAccess (Std.Rxi.Iterator α) Id
-- Mathlib.Logic.Function.Basic
Function.leftInverse_invFun : ∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β},
  Function.Injective f → Function.LeftInverse (Function.invFun f) f
-- Mathlib.Topology.Order.IntermediateValue
eq_Icc_csInf_csSup_of_connected_bdd_closed : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α] {s : Set α},
  IsConnected s → BddBelow s → BddAbove s → IsClosed s → s = Set.Icc (sInf s) (sSup s)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_iff_of_isLimit_fan : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  {f : β → C} {c : CategoryTheory.Limits.Fan f} (hc : CategoryTheory.Limits.IsLimit c),
  CategoryTheory.IsCoseparator c.pt ↔ (CategoryTheory.ObjectProperty.ofObj f).IsCoseparating
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.instInhabited.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R],
  MonoidAlgebra.instInhabited = { default := MonoidAlgebra.coeffEquiv.symm.1 default }
-- Mathlib.AlgebraicGeometry.Geometrically.Irreducible
/-- If `X` is geometrically irreducible over a point, then it is irreducible.  -/
AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton : ∀ {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) [AlgebraicGeometry.GeometricallyIrreducible f] [Subsingleton ↥S]
  [Nonempty ↥S], IrreducibleSpace ↥X
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The square `precomposeObjTransformObjSquare` is itself natural.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_naturality₂ : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  {U V : CategoryTheory.Functor X Y} (α : U ⟶ V),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map α)
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ))
      (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj V)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj V)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)
          ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)).hom
      (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ).whiskerLeft
        ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).map α))
-- Init.Data.Vector.Lex
Vector.le_toArray : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] {xs ys : Vector α n}, xs.toArray ≤ ys.toArray ↔ xs ≤ ys
-- Std.Tactic.Do.Syntax
/-- `mspec` is an `apply`-like tactic that applies a Hoare triple specification to the target of the
stateful goal.

Given a stateful goal `H ⊢ₛ wp⟦prog⟧ Q'`, `mspec foo_spec` will instantiate
`foo_spec : ... → ⦃P⦄ foo ⦃Q⦄`, match `foo` against `prog` and produce subgoals for
the verification conditions `?pre : H ⊢ₛ P` and `?post : Q ⊢ₚ Q'`.

* If `prog = x >>= f`, then `mspec Specs.bind` is tried first so that `foo` is matched against `x`
  instead. Tactic `mspec_no_bind` does not attempt to do this decomposition.
* If `?pre` or `?post` follow by `.rfl`, then they are discharged automatically.
* `?post` is automatically simplified into constituent `⊢ₛ` entailments on
  success and failure continuations.
* `?pre` and `?post.*` goals introduce their stateful hypothesis under an inaccessible name.
  You can give it a name with the `mrename_i` tactic.
* Any uninstantiated MVar arising from instantiation of `foo_spec` becomes a new subgoal.
* If the target of the stateful goal looks like `fun s => _` then `mspec` will first `mintro ∀s`.
* If `P` has schematic variables that can be instantiated by doing `mintro ∀s`, for example
  `foo_spec : ∀(n:Nat), ⦃fun s => ⌜n = s⌝⦄ foo ⦃Q⦄`, then `mspec` will do `mintro ∀s` first to
  instantiate `n = s`.
* Right before applying the spec, the `mframe` tactic is used, which has the following effect:
  Any hypothesis `Hᵢ` in the goal `h₁:H₁, h₂:H₂, ..., hₙ:Hₙ ⊢ₛ T` that is
  pure (i.e., equivalent to some `⌜φᵢ⌝`) will be moved into the pure context as `hᵢ:φᵢ`.

Additionally, `mspec` can be used without arguments or with a term argument:

* `mspec` without argument will try and look up a spec for `x` registered with `@[spec]`.
* `mspec (foo_spec blah ?bleh)` will elaborate its argument as a term with expected type
  `⦃?P⦄ x ⦃?Q⦄` and introduce `?bleh` as a subgoal.
  This is useful to pass an invariant to e.g., `Specs.forIn_list` and leave the inductive step
  as a hole.
 -/
Lean.Parser.Tactic.mspec : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.mono_measure : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε}, MeasureTheory.Integrable f ν → μ ≤ ν → MeasureTheory.Integrable f μ
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), e.symm.symm = e