mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} {mon : CategoryTheory.MonObj X}
  {comm : CategoryTheory.IsCommMonObj X} {X_1 : C} {mon_1 : CategoryTheory.MonObj X_1}
  {comm_1 : CategoryTheory.IsCommMonObj X_1},
  { X := X, mon := mon, comm := comm } = { X := X_1, mon := mon_1, comm := comm_1 } → X = X_1 ∧ mon ≍ mon_1
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.getEntry?.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) (x : List ((a : α) × β a)),
  Std.Internal.List.getEntry? a x =
    match x with
    | [] => none
    | ⟨k, v⟩ :: l => bif k == a then some ⟨k, v⟩ else Std.Internal.List.getEntry? a l
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.insert : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ (k : α) (v : β), m₁.Equiv m₂ → (m₁.insert k v).Equiv (m₂.insert k v)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.EMatchDiagSource.ematch.sizeOf_spec : ∀ (origin : Lean.Meta.Grind.Origin) (inst : Lean.Expr),
  sizeOf (Lean.Meta.Grind.EMatchDiagSource.ematch origin inst) = 1 + sizeOf origin + sizeOf inst
-- Lean.Elab.RecAppSyntax
/-- Checks if the `MData` is for a recursive application.
 -/
Lean.MData.isRecApp : Lean.MData → Bool
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonOpenNamespace.toJson : Lean.Lsp.OpenNamespace → Lean.Json
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_some_getD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α], t.WF → ∀ {a : α} {fallback : β a}, a ∈ t → t.get? a = some (t.getD a fallback)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_closure : ∀ {G : Type u_2} [inst : AddGroup G] (s : Set Gᵃᵒᵖ),
  (AddSubgroup.closure s).unop = AddSubgroup.closure (AddOpposite.op ⁻¹' s)
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonPMFReal_ofReal_eq_poissonPMF : ∀ (r : NNReal) (n : ℕ), ENNReal.ofReal (ProbabilityTheory.poissonPMFReal r n) = (ProbabilityTheory.poissonPMF r) n
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.Monics.map_eq_prod : ∀ (k : Type u) [inst : Field k] {f : AlgebraicClosure.Monics k},
  Polynomial.map (algebraMap k (AlgebraicClosure k)) ↑f =
    ∏ i,
      Polynomial.map (Ideal.Quotient.mk (AlgebraicClosure.maxIdeal k))
        (Polynomial.X - Polynomial.C (MvPolynomial.X ⟨f, i⟩))
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_retracts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T.retracts.rlp = T.rlp
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce.cons : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α] (x : α × Bool),
  FreeAddGroup.reduce (x :: L) =
    List.casesOn (FreeAddGroup.reduce L) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
MagmaCat.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Probability.ProductMeasure
/-- Let `μ : (i : Iic b) → Measure (X i)` be a family of measures. Up to an equivalence,
`(⨂ i : Iic a, μ i) ⊗ (⨂ i : Ioc a b, μ i) = ⨂ i : Iic b, μ i`, where `⊗` denotes the
product of measures.  -/
MeasureTheory.Measure.pi_prod_map_IicProdIoc : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {a b : ℕ},
  MeasureTheory.Measure.map (IicProdIoc a b)
      ((MeasureTheory.Measure.pi fun i => μ ↑i).prod (MeasureTheory.Measure.pi fun i => μ ↑i)) =
    MeasureTheory.Measure.pi fun i => μ ↑i
-- Init.Data.Int.Lemmas
/-- If a predicate on the integers is invariant under negation,
then it is sufficient to prove it for the nonnegative integers.
 -/
Int.wlog_sign : ∀ {P : ℤ → Prop}, (∀ (i : ℤ), P i ↔ P (-i)) → (∀ (n : ℕ), P ↑n) → ∀ (i : ℤ), P i
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorCore.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (toStrictPseudofunctorPreCore : CategoryTheory.StrictPseudofunctorPreCore B C) →
          autoParam
              (∀ {a b : B} (f : a ⟶ b),
                toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
                    (CategoryTheory.Bicategory.leftUnitor (toStrictPseudofunctorPreCore.map f)).hom)
              CategoryTheory.StrictPseudofunctorCore.map₂_left_unitor._autoParam →
            autoParam
                (∀ {a b : B} (f : a ⟶ b),
                  toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom =
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
                      (CategoryTheory.Bicategory.rightUnitor (toStrictPseudofunctorPreCore.map f)).hom)
                CategoryTheory.StrictPseudofunctorCore.map₂_right_unitor._autoParam →
              autoParam
                  (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
                    toStrictPseudofunctorPreCore.map₂ (CategoryTheory.Bicategory.associator f g h).hom =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Bicategory.associator (toStrictPseudofunctorPreCore.map f)
                              (toStrictPseudofunctorPreCore.map g) (toStrictPseudofunctorPreCore.map h)).hom
                          (CategoryTheory.eqToHom ⋯)))
                  CategoryTheory.StrictPseudofunctorCore.map₂_associator._autoParam →
                CategoryTheory.StrictPseudofunctorCore B C
-- Lean.Meta.HaveTelescope
/-- Efficiently collect dependency information for a `have` telescope.
This is part of a scheme to avoid quadratic overhead from the locally nameless discipline
(see `HaveTelescopeInfo` and `simpHaveTelescope`).

The expression `e` must not have loose bvars.
 -/
Lean.Meta.getHaveTelescopeInfo : Lean.Expr → Lean.MetaM Lean.Meta.HaveTelescopeInfo
-- Lean.Meta.Basic
/-- When `ctxApprox` is set to true, we relax condition 4, by creating an
auxiliary metavariable `?n'` with a smaller context than `?m'`.
 -/
Lean.Meta.Config.ctxApprox : Lean.Meta.Config → Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.equiv_iff_toArray_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ t₁.toArray = t₂.toArray)
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instTopOfBot : (α : Type u) → [h : Bot α] → Top αᵒᵈ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getThenInsertIfNew?_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {v : β k}, (t.getThenInsertIfNew? k v).2 = t.insertIfNew k v
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toListRev.match_1.splitter : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        (it : Std.IterM m β) →
          (motive : it.Step → Sort u_3) →
            (x : it.Step) →
              ((it' : Std.IterM m β) →
                  (out : β) →
                    (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
                ((it' : Std.IterM m β) →
                    (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                  ((property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩) → motive x
-- Mathlib.Topology.Compactness.Compact
Set.Subsingleton.isCompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s.Subsingleton → IsCompact s
-- Init.Data.String.Slice
String.Slice.toString_eq : String.Slice.toString = String.Slice.copy
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.intCast_div_mul_eq_zsmul : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] (p q r : 𝕜) (m : ℤ), ↑(↑m / q * r) = m • ↑(r / q)
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.sum_split_boxes : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] (I : BoxIntegral.Box ι) (i : ι) (x : ℝ)
  (f : BoxIntegral.Box ι → M),
  ∑ J ∈ (BoxIntegral.Prepartition.split I i x).boxes, f J =
    Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_empty_type : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [IsEmpty ι], LinearIndependent R v
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Pi.iConvexComb_apply : ∀ {I : Type u_1} {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  {ι : Type u_3} {X : ι → Type u_4} [inst_3 : (i : ι) → Convexity.ConvexSpace R (X i)] (w : Convexity.StdSimplex R I)
  (f : I → (i : ι) → X i) (i : ι), Convexity.iConvexComb w f i = Convexity.iConvexComb w fun j => f j i
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The composition of continuous functions.  -/
OmegaCompletePartialOrder.ContinuousHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : OmegaCompletePartialOrder α] →
        [inst_1 : OmegaCompletePartialOrder β] → [inst_2 : OmegaCompletePartialOrder γ] → (β →𝒄 γ) → (α →𝒄 β) → α →𝒄 γ
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.IsAccessible.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∃ κ, ∃ (x : Fact κ.IsRegular), F.IsCardinalAccessible κ) → CategoryTheory.Functor.IsAccessible.{w, v₁, v₂, u₁, u₂} F
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.mk_le_mk : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelMonoid α] {s : Submonoid α}
  {a₁ b₁ : α} {a₂ b₂ : ↥s}, Localization.mk a₁ a₂ ≤ Localization.mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ ↑a₂ * b₁
-- Mathlib.Data.Ineq
/-- Prints an `Ineq` as the corresponding infix symbol.  -/
Mathlib.Ineq.toString : Mathlib.Ineq → String
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv_counitIso_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.MonoidalOpposite.unmopEquiv C).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.RingTheory.Algebraic.Defs
Transcendental.eq_1 : ∀ (R : Type u) {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A),
  Transcendental R x = ¬IsAlgebraic R x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.π_leftRightHomologyComparison_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasLeftHomology] [inst_3 : S.HasRightHomology],
  CategoryTheory.CategoryStruct.comp S.leftHomologyπ
      (CategoryTheory.CategoryStruct.comp S.leftRightHomologyComparison S.rightHomologyι) =
    CategoryTheory.CategoryStruct.comp S.iCycles S.pOpcycles
-- Mathlib.RingTheory.DedekindDomain.Dvr
/-- In a Dedekind domain, the localization at every nonzero prime ideal is a DVR.  -/
IsLocalization.AtPrime.isDiscreteValuationRing_of_dedekind_domain : ∀ (A : Type u_1) [inst : CommRing A] [IsDomain A] [IsDedekindDomain A] {P : Ideal A},
  P ≠ ⊥ →
    ∀ [pP : P.IsPrime] (Aₘ : Type u_2) [inst_3 : CommRing Aₘ] [inst_4 : IsDomain Aₘ] [inst_5 : Algebra A Aₘ]
      [IsLocalization.AtPrime Aₘ P], IsDiscreteValuationRing Aₘ
-- Mathlib.RingTheory.Localization.Ideal
/-- Explicit characterization of the ideal given by `Ideal.map (algebraMap R S) I`.
In practice, this ideal differs only in that the carrier set is defined explicitly.
This definition is only meant to be used in proving `mem_map_algebraMap_iff`,
and any proof that needs to refer to the explicit carrier set should use that theorem.  -/
_private.Mathlib.RingTheory.Localization.Ideal.0.IsLocalization.map_ideal : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) → [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → Ideal R → Ideal S
-- Mathlib.NumberTheory.NumberField.AdeleRing
NumberField.instIsTopologicalRingAdeleRing : ∀ (R : Type u_1) (K : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K], IsTopologicalRing (NumberField.AdeleRing R K)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instBEqLetDecl.beq : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.LetDecl pu → Lean.Compiler.LCNF.LetDecl pu → Bool
-- Init.Data.Rat.Lemmas
Rat.max_def : ∀ {n m : ℚ}, max n m = if n ≤ m then m else n
-- Mathlib.Analysis.Complex.Trigonometric
Real.cosh_add : ∀ (x y : ℝ), Real.cosh (x + y) = Real.cosh x * Real.cosh y + Real.sinh x * Real.sinh y
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_of_nonpos_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddRightMono α] {a b : α}, b ≤ 0 → b + a ≤ a
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.instIsStableUnderRetractsInnerFibrations : SSet.innerFibrations.IsStableUnderRetracts
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.reindex_cofan₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {ι' : Type w'} (e : ι' ≃ c.ι),
  (c.reindex e).cofan₂ = CategoryTheory.Limits.Cofan.mk c.cofan₂.pt fun i' => c.cofan₂.inj (e i')
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
/-- The infimum of the elements of `s` less than `a` if there are some, otherwise `⊥`.  -/
Finset.truncatedInf : {α : Type u_1} → [inst : SemilatticeInf α] → [DecidableLE α] → [BoundedOrder α] → Finset α → α → α
-- Mathlib.Computability.Encoding
Computability.inhabitedΓ' : Inhabited Computability.Γ'
-- Mathlib.RingTheory.Localization.Away.Basic
/-- If `x ≠ 0`, then the localization of a domain away from `x` is again a domain.  -/
Localization.Away.isDomain : ∀ {R : Type u_1} [inst : CommSemiring R] [IsDomain R] {x : R}, x ≠ 0 → IsDomain (Localization.Away x)
-- Init.Grind.Lemmas
Lean.Grind.not_eq_of_eq_false : ∀ {a : Prop}, a = False → (¬a) = True
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.instCompletelyPositiveMapClass : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂],
  CompletelyPositiveMapClass (CompletelyPositiveMap A₁ A₂) A₁ A₂
-- Lean.Elab.Exception
Lean.Elab.postponeExceptionId : Lean.InternalExceptionId
-- Mathlib.Algebra.Group.Prod
MonoidHom.snd_comp_inl : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  (MonoidHom.snd M N).comp (MonoidHom.inl M N) = 1
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.monoidalUnopUnop_δ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : Cᵒᵖᵒᵖ),
  CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.unopUnop C) X Y =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.unopUnop C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core.inj : ∀ {e e_1 : Lean.Expr},
  Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core e = Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core e_1 → e = e_1
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFreeOn.of_succ : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α} {a : α} {n : ℕ},
  G.CliqueFreeOn s (n + 1) → a ∈ s → G.CliqueFreeOn (s ∩ G.neighborSet a) n
-- Mathlib.Order.Category.Semilat
SemilatInfCat.hasForgetToPartOrd : CategoryTheory.HasForget₂ SemilatInfCat PartOrd
-- Mathlib.Analysis.RCLike.Basic
RCLike.smul_im : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ) (z : K), RCLike.im (r • z) = r * RCLike.im z
-- Lean.Compiler.ExternAttr
Lean.getExternEntryForAux : Lean.Name → List Lean.ExternEntry → Option Lean.ExternEntry
-- Init.Control.Lawful.Instances
ExceptT.map.eq_1 : ∀ {ε : Type u} {m : Type u → Type v} [inst : Monad m] {α β : Type u} (f : α → β) (x : ExceptT ε m α),
  ExceptT.map f x =
    ExceptT.mk do
      let a ← x
      match a with
        | Except.ok a => pure (Except.ok (f a))
        | Except.error e => pure (Except.error e)
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_def_module : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E] (f : k → E) (a b : k),
  slope f a b = (b - a)⁻¹ • (f b - f a)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.instNeg : {R : Type u} → [inst : Ring R] → Neg (Polynomial R)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.trans.inj : ∀ {R : Type u} {inst : Rack R} {a b c : Rack.PreEnvelGroup R} {hab : Rack.PreEnvelGroupRel' R a b}
  {hbc : Rack.PreEnvelGroupRel' R b c} {b_1 : Rack.PreEnvelGroup R} {hab_1 : Rack.PreEnvelGroupRel' R a b_1}
  {hbc_1 : Rack.PreEnvelGroupRel' R b_1 c}, hab.trans hbc = hab_1.trans hbc_1 → b = b_1 ∧ hab ≍ hab_1 ∧ hbc ≍ hbc_1
-- Mathlib.Topology.Algebra.Algebra
/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.

See note [reducible non-instances].  -/
Subalgebra.commSemiringTopologicalClosure : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u} →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : Semiring A] →
          [inst_3 : Algebra R A] →
            [inst_4 : IsSemitopologicalSemiring A] →
              [T2Space A] → (s : Subalgebra R A) → (∀ (x y : ↥s), x * y = y * x) → CommSemiring ↥s.topologicalClosure
-- Mathlib.NumberTheory.Dioph
Dioph.dioph_comp2 : ∀ {α : Type} {f g : (α → ℕ) → ℕ},
  Dioph.DiophFn f →
    Dioph.DiophFn g →
      ∀ {S : ℕ → ℕ → Prop}, Dioph {v | S (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))} → Dioph {v | S (f v) (g v)}
-- Mathlib.Data.Complex.Basic
Complex.canLift : CanLift ℂ ℝ Complex.ofReal fun z => z.im = 0
-- Mathlib.Algebra.Lie.Abelian
LieIdeal.isLieAbelian_of_trivial : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  [h : LieModule.IsTrivial L ↥I], IsLieAbelian ↥I
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.valuation_pos_iff_ne_zero : ∀ {F : Type u} {Γ₀ : Type v} [inst : Field F] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation F Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O F],
  v.Integers O → ∀ {x : O}, 0 < v ((algebraMap O F) x) ↔ x ≠ 0
-- Mathlib.Topology.Filter
Filter.nhds_mono : ∀ {α : Type u_2} {l₁ l₂ : Filter α}, nhds l₁ ≤ nhds l₂ ↔ l₁ ≤ l₂
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
        (CategoryTheory.CategoryStruct.id Y))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom
        h)
-- Mathlib.Algebra.Algebra.Opposite
/-- Swap the `ᵐᵒᵖ` on an algebra hom to the opposite side.  -/
AlgHom.opComm : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] Bᵐᵒᵖ) ≃ (Aᵐᵒᵖ →ₐ[R] B)
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.addHandler : Lean.Environment → Lean.Name → Lean.Name → Lean.Linter.MissingDocs.Handler → Lean.Environment
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.instField : {α : Type u} → {β : Type v} → {φ : Ultrafilter α} → [Field β] → Field ((↑φ).Germ β)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.let.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (decl : Lean.Compiler.LCNF.LetDecl pu),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.let decl) = 1 + sizeOf decl
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivativeFun_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (f g : PowerSeries R),
  (f * g).derivativeFun = f • g.derivativeFun + g • f.derivativeFun
-- Init.Data.UInt.Basic
/-- Adds two 64-bit unsigned integers, wrapping around on overflow. Usually accessed via the `+`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.add : UInt64 → UInt64 → UInt64
-- Lean.DocString.Types
Lean.Doc.Part.mk.inj : ∀ {i : Type u} {b : Type v} {p : Type w} {title : Array (Lean.Doc.Inline i)} {titleString : String}
  {metadata : Option p} {content : Array (Lean.Doc.Block i b)} {subParts : Array (Lean.Doc.Part i b p)}
  {title_1 : Array (Lean.Doc.Inline i)} {titleString_1 : String} {metadata_1 : Option p}
  {content_1 : Array (Lean.Doc.Block i b)} {subParts_1 : Array (Lean.Doc.Part i b p)},
  { title := title, titleString := titleString, metadata := metadata, content := content, subParts := subParts } =
      { title := title_1, titleString := titleString_1, metadata := metadata_1, content := content_1,
        subParts := subParts_1 } →
    title = title_1 ∧ titleString = titleString_1 ∧ metadata = metadata_1 ∧ content = content_1 ∧ subParts = subParts_1
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_mkPiAlgebra_of_empty : ∀ {𝕜 : Type u} {ι : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {A : Type u_1}
  [inst_2 : NormedCommRing A] [inst_3 : NormedAlgebra 𝕜 A] [IsEmpty ι],
  ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖1‖