mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- The inverse functor that makes up `TransportEnrichment.forgetEnrichmentEquiv`.  -/
CategoryTheory.TransportEnrichment.forgetEnrichmentEquivInverse : {V : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {W : Type u''} →
        [inst_2 : CategoryTheory.Category.{v'', u''} W] →
          [inst_3 : CategoryTheory.MonoidalCategory W] →
            (F : CategoryTheory.Functor V W) →
              [inst_4 : F.LaxMonoidal] →
                (D : Type u) →
                  [inst_5 : CategoryTheory.EnrichedCategory V D] →
                    (e :
                        (v : V) →
                          (CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v) ≃
                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit W ⟶ F.obj v)) →
                      (∀ (v : V) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶ v),
                          (e v) f =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map f)) →
                        CategoryTheory.Functor
                          (CategoryTheory.ForgetEnrichment W (CategoryTheory.TransportEnrichment F D))
                          (CategoryTheory.TransportEnrichment F (CategoryTheory.ForgetEnrichment V D))
-- Mathlib.CategoryTheory.Limits.Chosen.End
/-- The chosen cowedge is colimiting.  -/
CategoryTheory.Limits.ChosenCoendsOfShape.isCoend : {J : Type u_1} →
  {inst : CategoryTheory.Category.{v_1, u_1} J} →
    {C : Type u_2} →
      {inst_1 : CategoryTheory.Category.{v_2, u_2} C} →
        [self : CategoryTheory.Limits.ChosenCoendsOfShape J C] →
          (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.ChosenCoendsOfShape.cowedge F)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_hom_inv_id_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a)
  (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLTι a).app X))
      ((t.eTruncLTLTIsoLT a b hab).inv.app X) =
    CategoryTheory.CategoryStruct.id ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X))
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_zero : ∀ {α : Type u_1} [inst : Zero α], ofLex 0 = 0
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valuation.norm_add_le : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀)
  [hv : v.RankOne] (x y : L), v.norm (x + y) ≤ max (v.norm x) (v.norm y)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_comm : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), s₁ ∩ s₂ = s₂ ∩ s₁
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.isReal_or_isComplex : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K), w.IsReal ∨ w.IsComplex
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.copy_eq : ∀ {α : Type u_1} [inst : CompleteLattice α] (L : CompleteSublattice α) (s : Set α) (hs : s = ↑L), L.copy s hs = L
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
/-- A version of `charpoly_mul_comm'` for square matrices.  -/
Matrix.charpoly_mul_comm : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (A B : Matrix n n R),
  (A * B).charpoly = (B * A).charpoly
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteAddGrp.toLimitFun_continuous : ∀ (P : ProfiniteAddGrp.{u}), Continuous ⇑P.toLimitFun
-- Init.Data.Vector.Attach
/-- `O(1)`. "Attach" a proof `P x` that holds for all the elements of `xs` to produce a new array
with the same elements but in the type `{x // P x}`.  -/
Vector.attachWith : {α : Type u_1} → {n : ℕ} → (xs : Vector α n) → (P : α → Prop) → (∀ x ∈ xs, P x) → Vector { x // P x } n
-- Init.Data.List.Count
List.replicate_count_eq_of_count_eq_length : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l : List α},
  List.count a l = l.length → List.replicate (List.count a l) a = l
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- Lüroth's theorem. Any intermediate field between `K` and `K⟮X⟯` is
generated by a single element `generator E`. See also `transcendental_generator`
for the statement that the generator is transcendental if `E ≠ ⊥`.  -/
RatFunc.Luroth.eq_adjoin_generator : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)}, E = K⟮RatFunc.Luroth.generator E⟯
-- Init.Data.BitVec.Lemmas
/-- A nonzero bitvector is lower-bounded by its leading zeroes.  -/
BitVec.two_pow_sub_clz_le_toNat_of_ne_zero : ∀ {w : ℕ} {x : BitVec w}, 0 < w → x ≠ 0#w → 2 ^ (w - 1 - x.clz.toNat) ≤ x.toNat
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If `E / F` is purely inseparable, then the separable closure of `F` in `E` is
equal to `F`.  -/
separableClosure.eq_bot_of_isPurelyInseparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E],
  separableClosure F E = ⊥
-- Mathlib.GroupTheory.Submonoid.Center
AddOpposite.unop_mem_center_iff : ∀ {M : Type u_2} [inst : Add M] {x : Mᵃᵒᵖ}, AddOpposite.unop x ∈ Set.addCenter M ↔ x ∈ Set.addCenter Mᵃᵒᵖ
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.center_eq_top : ∀ {G : Type u_1} [inst : Group G] [hG : IsMulCommutative G], Subgroup.center G = ⊤
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.ordConnectedComponent_univ : ∀ {α : Type u_1} [inst : LinearOrder α] {x : α}, Set.univ.ordConnectedComponent x = Set.univ
-- Mathlib.Data.Set.Basic
/-- **Alias** of the reverse direction of `Set.empty_ssubset`. -/
Set.Nonempty.empty_ssubset : ∀ {α : Type u} {s : Set α}, s.Nonempty → ∅ ⊂ s
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.isLeftInversion_simple_iff_isLeftDescent : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W) (i : B),
  cs.IsLeftInversion w (cs.simple i) ↔ cs.IsLeftDescent w i
-- Init.Data.Option.Lemmas
Option.any_bind : ∀ {β : Type u_1} {α : Type u_2} {p : β → Bool} {f : α → Option β} {o : Option α},
  Option.any p (o.bind f) = Option.any (Option.any p ∘ f) o
-- Mathlib.Order.Fin.Basic
/-- `Fin.predAbove p` as an `OrderHom`.  -/
Fin.predAboveOrderHom : {n : ℕ} → Fin n → Fin (n + 1) →o Fin n
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- For an invertible matrix `U`, `star U * x * U` is positive definite iff `x` is.
This works on any ⋆-ring with a partial order.

See `IsUnit.isStrictlyPositive_star_left_conjugate_iff'` for a similar statement for star-ordered
rings. For matrices, positive definiteness is equivalent to strict positivity when the underlying
field is `ℝ` or `ℂ` (see `Matrix.isStrictlyPositive_iff_posDef`).  -/
Matrix.IsUnit.posDef_star_left_conjugate_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  [inst_4 : DecidableEq n] {x U : Matrix n n R}, IsUnit U → ((star U * x * U).PosDef ↔ x.PosDef)
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
CategoryTheory.sheafToPresheaf_ε : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A],
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.sheafToPresheaf J A) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Functor Cᵒᵖ A))
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.minEntry?_cons.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (w : (a : α) × β a)
  (h_1 : Unit → motive none) (h_2 : (w : (a : α) × β a) → motive (some w)),
  (match some w with
    | none => h_1 ()
    | some w => h_2 w) =
    h_2 w
-- Mathlib.Algebra.CubicDiscriminant
Cubic.eq_prod_three_roots : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
  P.a ≠ 0 →
    (Cubic.map φ P).roots = {x, y, z} →
      (Cubic.map φ P).toPoly =
        Polynomial.C (φ P.a) * (Polynomial.X - Polynomial.C x) * (Polynomial.X - Polynomial.C y) *
          (Polynomial.X - Polynomial.C z)
-- Mathlib.Data.Vector.Zip
/-- Apply the function `f : α → β → γ` to each corresponding pair of elements from two vectors.  -/
List.Vector.zipWith : {α : Type u_1} →
  {β : Type u_2} → {γ : Type u_3} → {n : ℕ} → (α → β → γ) → List.Vector α n → List.Vector β n → List.Vector γ n
-- Mathlib.Topology.Homotopy.Path
/-- Two constant continuous maps with nonempty domain are homotopic if and only if their values are
joined by a path in the codomain.  -/
ContinuousMap.homotopic_const_iff : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X} [Nonempty Y],
  (ContinuousMap.const Y x₀).Homotopic (ContinuousMap.const Y x₁) ↔ Joined x₀ x₁
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Init.Data.String.Basic
List.asString_append : ∀ {l₁ l₂ : List Char}, String.ofList (l₁ ++ l₂) = String.ofList l₁ ++ String.ofList l₂
-- Mathlib.Topology.Constructions
IsClosedMap.domRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsClosedMap f → ∀ {s : Set X}, IsClosed s → IsClosedMap (s.domRestrict f)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
/-- If `f` is a transfinite composition of shape `J` of morphisms in `W`,
then it is also a transfinite composition of shape `J'` of morphisms in `W` if `J' ≃o J`.  -/
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofOrderIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {J : Type w} →
        [inst_1 : LinearOrder J] →
          [inst_2 : SuccOrder J] →
            [inst_3 : OrderBot J] →
              [inst_4 : WellFoundedLT J] →
                {X Y : C} →
                  {f : X ⟶ Y} →
                    W.TransfiniteCompositionOfShape J f →
                      {J' : Type w'} →
                        [inst_5 : LinearOrder J'] →
                          [inst_6 : OrderBot J'] →
                            [inst_7 : SuccOrder J'] →
                              [inst_8 : WellFoundedLT J'] → J' ≃o J → W.TransfiniteCompositionOfShape J' f
-- Mathlib.Order.Hom.Bounded
TopHom.id_comp : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : Top β] (f : TopHom α β), (TopHom.id β).comp f = f
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered monoids M, N, the natural inclusion ordered homomorphism from M to M × N.  -/
OrderMonoidHom.inl : (α : Type u_1) →
  (β : Type u_2) →
    [inst : Monoid α] → [inst_1 : PartialOrder α] → [inst_2 : Monoid β] → [inst_3 : Preorder β] → α →*o α × β
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.G2Term_summable : ∀ (z : UpperHalfPlane), Summable (EisensteinSeries.G2Term✝ z)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- `mk' f m s` is the fraction `m/s` with respect to the localization map `f`.  -/
IsLocalizedModule.mk' : {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') → [IsLocalizedModule S f] → M → ↥S → M'
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.rOut_pos : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c), 0 < f.rOut
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `extractLsb` on `BitVec`s.  -/
BitVec.reduceExtractLsb : Lean.Meta.Simp.DSimproc
-- Mathlib.Tactic.Attr.Register
/-- simp set for the manipulation of typevec and arrow expressions  -/
Parser.Attr.typevec : Lean.ParserDescr
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_eq_getElem! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α} {h : a ∈ t}, t[a] = t[a]!
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.ext : ∀ {X Y : AddCommGrpCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.CategoryTheory.Sites.Abelian
CategoryTheory.instAdditiveSheafConstantSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{w', w} D]
  [inst_2 : CategoryTheory.Abelian D] {J : CategoryTheory.GrothendieckTopology C}
  [inst_3 : CategoryTheory.HasSheafify J D], (CategoryTheory.constantSheaf J D).Additive
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKeyD fallback =
        t.minKey?.elim k fun k' => if compare k k' = Ordering.lt then k else k'
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.monic_of_subsingleton : ∀ {R : Type u} [inst : Semiring R] [Subsingleton R] (p : Polynomial R), p.Monic
-- Std.Async.Process
/-- Gets the scheduling priority of a process.
 -/
Std.IO.Process.getPriority : Std.IO.Process.PId → IO Int64
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- **Alias** of the forward direction of `hasFDerivAt_iff_hasDerivAt`.

---

Expressing `HasFDerivAt f f' x` in terms of `HasDerivAt`  -/
HasFDerivAt.hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : 𝕜 →L[𝕜] F},
  HasFDerivAt f f' x → HasDerivAt f (f' 1) x
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.smul_top : ∀ {R : Type u_5} [inst : CommRing R] (a : R) (I : Ideal R), a • ⊤ = R ∙ Submodule.Quotient.mk a
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.Measure.countable_meas_level_set_pos : ∀ {α : Type u_4} {β : Type u_5} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ]
  [inst : MeasurableSpace β] [MeasurableSingletonClass β] {g : α → β},
  Measurable g → {t | 0 < μ {a | g a = t}}.Countable
-- ProofWidgets.Component.RefreshComponent
_private.ProofWidgets.Component.RefreshComponent.0.ProofWidgets.RefreshToken.updateLazy.unsafe_impl_2 : IO.Ref ProofWidgets.RefreshComponent.RefreshState → BaseIO ProofWidgets.RefreshComponent.RefreshState
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.IsUniform.mk : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A},
  (∀ {I : Ideal A}, I ∈ F → ∀ (a : A), Submodule.colon I {a} ∈ F) → F.IsUniform
-- Mathlib.Data.Multiset.ZeroCons
Multiset.le_cons_self : ∀ {α : Type u_1} (s : Multiset α) (a : α), s ≤ a ::ₘ s
-- Lean.Meta.Tactic.Grind.Arith.CommRing.PP
_private.Lean.Meta.Tactic.Grind.Arith.CommRing.PP.0.Lean.Meta.Grind.Arith.CommRing.M : Type → Type
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_div2 : Primrec Nat.div2
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.union.eq_1 : ∀ (self : Batteries.UnionFind) (x y : Fin self.size),
  self.union x y =
    match self.find x with
    | ⟨self₁, ⟨rx, ex⟩⟩ =>
      have hy := ⋯;
      match eq : self₁.find ⟨↑y, hy⟩ with
      | ⟨self₂, ⟨ry, ey⟩⟩ => self₂.link ⟨↑rx, ⋯⟩ ry ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the second (middle) object of a `ShortComplex`  -/
CategoryTheory.ShortComplex.X₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → C
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.sclosure_preimage_le : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (s : Set S),
  Subsemiring.closure (⇑f ⁻¹' s) ≤ Subsemiring.comap f (Subsemiring.closure s)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_smul : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {S : Type u_6} [inst_10 : Monoid S]
  [inst_11 : DistribMulAction S W] [inst_12 : SMulCommClass R S W] [inst_13 : ContinuousConstSMul S W]
  [inst_14 : LinearMap.CompatibleSMul W W S R] (s : S) (f : ContIntertwiningMap π₁ π₂),
  (s • f).toContinuousLinearMap = s • f.toContinuousLinearMap
-- Init.Control.Except
_private.Init.Control.Except.0.Except.map.match_1.eq_1 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (err : ε) (h_1 : (err : ε) → motive (Except.error err))
  (h_2 : (v : α) → motive (Except.ok v)),
  (match Except.error err with
    | Except.error err => h_1 err
    | Except.ok v => h_2 v) =
    h_1 err
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_natural_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X X' Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : X ⟶ X') (g : CategoryTheory.MonoidalCategoryStruct.tensorObj A X' ⟶ Y),
  CategoryTheory.MonoidalClosed.curry
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) g) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalClosed.curry g)
-- Mathlib.RingTheory.Morita.Matrix
MatrixModCat.isScalarTower_toModuleCat : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  (M : ModuleCat (Matrix ι ι R)), IsScalarTower R (Matrix ι ι R) ↑M
-- Mathlib.Order.Interval.Set.Disjoint
Set.Iic_disjoint_Ici : ∀ {α : Type v} [inst : Preorder α] {a b : α}, Disjoint (Set.Iic a) (Set.Ici b) ↔ ¬b ≤ a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → Std.ExtDHashMap.Const.get? (m₁ ∩ m₂) k = none
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.locallyOfFiniteType_of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.CategoryStruct.comp f g)],
  AlgebraicGeometry.LocallyOfFiniteType f
-- Init.Data.UInt.Basic
instShiftRightUInt16 : ShiftRight UInt16
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.compConstIso_inv_app_app : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor C D) (X : C) (X_1 : J),
  ((CategoryTheory.Functor.compConstIso J F).inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.whiskerRight.inj : ∀ {C : Type u} {X₁ X₂ : CategoryTheory.FreeMonoidalCategory C} {f : X₁.Hom X₂}
  {Y : CategoryTheory.FreeMonoidalCategory C} {f_1 : X₁.Hom X₂}, f.whiskerRight Y = f_1.whiskerRight Y → f = f_1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      match h : compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryGED k l (ky, y)
      | Ordering.eq => (ky, y)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryGE k r ⋯ ⋯
-- Mathlib.Order.DirectedInverseSystem
/-- The inverse limit of an inverse system of types.  -/
InverseSystem.limit : {ι : Type u_1} →
  [inst : Preorder ι] → {F : ι → Type u_4} → (⦃i j : ι⦄ → i ≤ j → F j → F i) → (i : ι) → Set ((l : ↑(Set.Iio i)) → F ↑l)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Print `ω^s*n`, omitting `s` if `e = 0` or `e = 1`, and omitting `n` if `n = 1`  -/
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.toStringAux : ONote → ℕ → String → String
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.IsUpper.isTopologicalBasis_insert_univ_subbasis : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [Topology.IsUpper α],
  TopologicalSpace.IsTopologicalBasis (insert Set.univ {s | ∃ a, (Set.Iic a)ᶜ = s})
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.toGlueData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    AlgebraicGeometry.SheafedSpace.GlueData C → CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.zero_def : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Zero (M i)], 0 = fun x => 0
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_mapHomologicalComplexObjXIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] (i j : ι) (hij : c.Rel j i),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.homotopyCofiber.inlX ((H.mapHomologicalComplex c).map φ) i j hij)
      (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso φ H j).inv =
    H.map (HomologicalComplex.homotopyCofiber.inlX φ i j hij)
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_empty : ∀ (R : Type u_2) (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearIndependent R fun (x : ↑∅) => ↑x
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
/-- The length of a path in a manifold is invariant under an antitone reparametrization.  -/
Manifold.pathELength_comp_of_antitoneOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ : ℝ → M} [∀ (x : M), ENormSMulClass ℝ (TangentSpace I x)]
  {f : ℝ → ℝ},
  a ≤ b →
    AntitoneOn f (Set.Icc a b) →
      DifferentiableOn ℝ f (Set.Icc a b) →
        MDiff[Set.Icc (f b) (f a)] γ → Manifold.pathELength I (γ ∘ f) a b = Manifold.pathELength I γ (f b) (f a)