mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxcIterator.step.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (motive : Std.DTreeMap.Internal.RxcIterator α β → Sort u_3) (k : α)
  (v : β k) (t : Std.DTreeMap.Internal.Impl α β) (it : Std.DTreeMap.Internal.Zipper α β) (upper : α)
  (h_1 : (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper })
  (h_2 :
    (k : α) →
      (v : β k) →
        (t : Std.DTreeMap.Internal.Impl α β) →
          (it : Std.DTreeMap.Internal.Zipper α β) →
            (upper : α) → motive { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }),
  (match { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper } with
    | { iter := Std.DTreeMap.Internal.Zipper.done, upper := upper } => h_1 upper
    | { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper } => h_2 k v t it upper) =
    h_2 k v t it upper
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.mk_surjective : ∀ {V : SSet.Truncated 2}, Function.Surjective SSet.Truncated.HomotopyCategory.mk
-- Init.Data.Float.Float32
/-- Converts a floating-point number to a 64-bit unsigned integer.

If the given `Float32` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `UInt64`. Returns `0` if the `Float32` is negative or `NaN`, and returns
the largest `UInt64` value (i.e. `UInt64.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float32.Model`.
 -/
Float32.toUInt64 : Float32 → UInt64
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.mp : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ Q → R) → (P ⊢ₛ Q) → P ⊢ₛ R
-- Mathlib.Algebra.Group.Finsupp
Finsupp.support_single_add_single_subset : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [inst_1 : DecidableEq ι] {f₁ f₂ : ι} {g₁ g₂ : M},
  ((fun₀ | f₁ => g₁) + fun₀ | f₂ => g₂).support ⊆ {f₁, f₂}
-- Mathlib.Analysis.Fourier.Notation
/-- `𝓕 f` is the Fourier transform of `f`. The meaning of this notation is type-dependent.  -/
FourierTransform.fourier : {E : Type u} → {F : outParam (Type v)} → [self : FourierTransform E F] → E → F
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.PInfty_toNondegComplex_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C] {Z : ChainComplex C ℕ} (h : s.nondegComplex ⟶ Z),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty
      (CategoryTheory.CategoryStruct.comp s.toNondegComplex h) =
    CategoryTheory.CategoryStruct.comp s.toNondegComplex h
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.coeff_mul_prod_one_sub_of_lt_order : ∀ {σ : Type u_1} {R : Type u_4} {ι : Type u_5} [inst : CommRing R] (d : σ →₀ ℕ) (s : Finset ι) (f : MvPowerSeries σ R)
  (g : ι → MvPowerSeries σ R),
  (∀ i ∈ s, ↑(Finsupp.degree d) < (g i).order) →
    (MvPowerSeries.coeff d) (f * ∏ i ∈ s, (1 - g i)) = (MvPowerSeries.coeff d) f
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
/-- A C⋆-algebra is spanned by its nonnegative elements.  -/
CStarAlgebra.span_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℂ A] [inst_2 : SMulCommClass ℂ A A]
  [inst_3 : IsScalarTower ℂ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A] [StarModule ℂ A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_8 : PartialOrder A] [StarOrderedRing A],
  Submodule.span ℂ {a | 0 ≤ a} = ⊤
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.evalStarAlgHom_apply : ∀ {X : Type u_1} (S : Type u_2) (R : Type u_3) [inst : TopologicalSpace X] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring R] [inst_3 : Algebra S R] [inst_4 : TopologicalSpace R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : StarRing R] [inst_7 : ContinuousStar R] (x : X) (f : C(X, R)), (ContinuousMap.evalStarAlgHom S R x) f = f x
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxEntry?.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) =
    h_1 ()
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearMap.transvection.congr : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] (f : Module.Dual R V) (v : V) (e : V ≃ₗ[R] W),
  ↑e ∘ₗ LinearMap.transvection f v ∘ₗ ↑e.symm = (f ∘ₗ ↑e.symm).transvection (e v)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.closure_openCell_eq_closedCell`. -/
Topology.CWComplex.closure_openCell_eq_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {n : ℕ}
  {j : Topology.RelCWComplex.cell C n},
  closure (Topology.RelCWComplex.openCell n j) = Topology.RelCWComplex.closedCell n j
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.algebra : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : Semiring R] →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : CommSemiring S] →
                [inst_5 : Module S M] →
                  [SMulCommClass R S M] →
                    [inst_7 : SMul S R] →
                      [IsScalarTower S R M] →
                        [ContinuousConstSMul S M] → [inst_10 : IsTopologicalAddGroup M] → Algebra S (M →L[R] M)
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.isLimitOfPreserves₂.congr_simp : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [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] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] {c₁ : CategoryTheory.Limits.Cone K₁}
  (hc₁ hc₁_1 : CategoryTheory.Limits.IsLimit c₁),
  hc₁ = hc₁_1 →
    ∀ {c₂ : CategoryTheory.Limits.Cone K₂} (hc₂ hc₂_1 : CategoryTheory.Limits.IsLimit c₂),
      hc₂ = hc₂_1 →
        CategoryTheory.Limits.isLimitOfPreserves₂ G hc₁ hc₂ = CategoryTheory.Limits.isLimitOfPreserves₂ G hc₁_1 hc₂_1
-- Mathlib.Logic.Basic
not_imp_not : ∀ {a b : Prop}, ¬a → ¬b ↔ b → a
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_sUnion : ∀ {x y : PSet.{u}}, y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_mul_self : ∀ (x : NNReal), NNReal.sqrt (x * x) = x
-- Lean.Syntax
Lean.IsNode.mk : ∀ (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax),
  Lean.IsNode (Lean.Syntax.node info kind args)
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a lattice inherits a difference.  -/
BooleanSubalgebra.instSDiffCoe : {α : Type u_2} → [inst : BooleanAlgebra α] → {L : BooleanSubalgebra α} → SDiff ↥L
-- Mathlib.RingTheory.Congruence.Defs
/-- The induced multiplicative congruence from a `RingCon`.  -/
RingCon.toCon : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → RingCon R → Con R
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.sin_eq_sin_iff : ∀ {x y : ℝ}, Real.sin x = Real.sin y ↔ ∃ k, y = 2 * ↑k * Real.pi + x ∨ y = (2 * ↑k + 1) * Real.pi - x
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.eq_id : ∀ {A : Type u} {x : CategoryTheory.Codiscrete A} (f : x ⟶ x), f = CategoryTheory.CategoryStruct.id x
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
/-- The edge of the `2`-truncation of a simplicial set `X` that is induced
by an edge of `X`.  -/
SSet.Edge.toTruncated : {X : SSet} → {x₀ x₁ : X.obj (Opposite.op { len := 0 })} → SSet.Edge x₀ x₁ → SSet.Truncated.Edge x₀ x₁
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.inter_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ t₄ : Std.DTreeMap.Raw α β cmp},
  t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ ∩ t₂).Equiv (t₃ ∩ t₄)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.typeClass.sizeOf_spec : ∀ (extraErrorMsg? : Option Lean.MessageData),
  sizeOf (Lean.Elab.Term.SyntheticMVarKind.typeClass extraErrorMsg?) = 1 + sizeOf extraErrorMsg?
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddZeroClass : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : AddZeroClass M] → [ContinuousAdd M] → AddZeroClass (SeparationQuotient M)
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- The power series for `f.changeOrigin k`.

Given a formal multilinear series `p` and a point `x` in its ball of convergence,
`p.changeOrigin x` is a formal multilinear series such that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Its `k`-th term is the sum of
the series `p.changeOriginSeries k`.  -/
FormalMultilinearSeries.changeOriginSeries : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                FormalMultilinearSeries 𝕜 E F → (k : ℕ) → FormalMultilinearSeries 𝕜 E (E [×k]→L[𝕜] F)
-- Init.Data.Nat.Lemmas
Nat.add_right_cancel_iff : ∀ {m k n : ℕ}, m + n = k + n ↔ m = k
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- **Banach-Alaoglu** theorem. The set of functions `f : E → F` that represent continuous linear
maps `f : E →SL[σ₁₂] F` at distance `≤ r` from `f₀ : E →SL[σ₁₂] F` is compact in the topology of
pointwise convergence. Other versions of this theorem can be found in
`Analysis.Normed.Module.WeakDual`.  -/
ContinuousLinearMap.isCompact_image_coe_closedBall : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  [ProperSpace F] (f₀ : E →SL[σ₁₂] F) (r : ℝ), IsCompact (DFunLike.coe '' Metric.closedBall f₀ r)
-- Init.Data.UInt.Basic
instMulUInt8 : Mul UInt8
-- Mathlib.Algebra.Group.Action.Hom
/-- An additive action of `M` on `α` and an additive monoid homomorphism `N → M` induce
an additive action of `N` on `α`.

See note [reducible non-instances].  -/
AddAction.compHom : {M : Type u_1} →
  {N : Type u_2} →
    (α : Type u_3) → [inst : AddMonoid M] → [AddAction M α] → [inst_2 : AddMonoid N] → (N →+ M) → AddAction N α
-- Init.Data.List.Monadic
List.zipWithM'_cons_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {a : α} {as : List α} {b : β} {bs : List β}
  [inst : Monad m] {f : α → β → m γ},
  List.zipWithM' f (a :: as) (b :: bs) = do
    let __do_lift ← f a b
    let __do_lift_1 ← List.zipWithM' f as bs
    pure (__do_lift :: __do_lift_1)
-- Mathlib.Analysis.RCLike.Basic
RCLike.intCast_re : ∀ {K : Type u_1} [inst : RCLike K] (n : ℤ), RCLike.re ↑n = ↑n
-- Lean.Meta.CongrTheorems
/-- Computes `CongrArgKind`s for a simp congruence theorem.  -/
Lean.Meta.getCongrSimpKinds : Lean.Expr → Lean.Meta.FunInfo → Lean.MetaM (Array Lean.Meta.CongrArgKind)
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstDvdNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.Sheaves.Flasque
Quiver.Hom.hcongr_4 : ∀ (V V' : Type u),
  V = V' →
    ∀ (self : Quiver V) (self' : Quiver V'),
      self ≍ self' → ∀ (a : V) (a' : V'), a ≍ a' → ∀ (a_1 : V) (a'_1 : V'), a_1 ≍ a'_1 → (a ⟶ a_1) ≍ (a' ⟶ a'_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_get_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k} {w : k ∈ m}, m.get k w = v → k ∈ m
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasDetector.wellPowered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C]
  [CategoryTheory.HasDetector C], CategoryTheory.WellPowered.{v₁, v₁, u₁} C
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.continuous_eval : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] (x : X), Continuous fun f => f x
-- Lean.Meta.Tactic.Repeat
_private.Lean.Meta.Tactic.Repeat.0.Lean.Meta.repeat'Core.go.match_5.eq_1 : ∀ (motive : ℕ → Bool → List Lean.MVarId → List (List Lean.MVarId) → Array Lean.MVarId → Sort u_1) (x : ℕ) (p : Bool)
  (acc : Array Lean.MVarId) (h_1 : (x : ℕ) → (p : Bool) → (acc : Array Lean.MVarId) → motive x p [] [] acc)
  (h_2 :
    (n : ℕ) →
      (p : Bool) →
        (goals : List Lean.MVarId) →
          (stk : List (List Lean.MVarId)) → (acc : Array Lean.MVarId) → motive n p [] (goals :: stk) acc)
  (h_3 :
    (n : ℕ) →
      (p : Bool) →
        (g : Lean.MVarId) →
          (goals : List Lean.MVarId) →
            (stk : List (List Lean.MVarId)) → (acc : Array Lean.MVarId) → motive n p (g :: goals) stk acc),
  (match x, p, [], [], acc with
    | x, p, [], [], acc => h_1 x p acc
    | n, p, [], goals :: stk, acc => h_2 n p goals stk acc
    | n, p, g :: goals, stk, acc => h_3 n p g goals stk acc) =
    h_1 x p acc
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.of_symm_eq : ∀ {M : Type u_1}, ArchimedeanOrder.of.symm = ArchimedeanOrder.val
-- Mathlib.Analysis.Meromorphic.Order
/-- The set where a meromorphic function has zero or infinite
order is codiscrete within its domain of meromorphicity.  -/
MeromorphicOn.codiscrete_setOfPred_meromorphicOrderAt_eq_zero_or_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤} ∈ Filter.codiscrete ↑U
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.Const.getD.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α fun x => β) (a : α)
  (fallback : β),
  Std.DHashMap.Raw.Const.getD m a fallback =
    if h : 0 < m.buckets.size then Std.DHashMap.Internal.Raw₀.Const.getD ⟨m, h⟩ a fallback else fallback
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.singleton_eq_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {p : α × β}, {p} = ∅.insert p.1 p.2
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_union_of_notMem_inter : ∀ {α : Type u_1} {M : Type u_4} [inst : MulOneClass M] {s t : Set α} {a : α},
  a ∉ s ∩ t → ∀ (f : α → M), (s ∪ t).mulIndicator f a = s.mulIndicator f a * t.mulIndicator f a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSlice.instToIterator : {α : Type u_1} →
  {β : Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RcoSliceData α β)) Id
        (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxoIterator α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
          pure (b.fst, b.snd))
        (α × β)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.toVal_mul : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x y : R), WithVal.toVal v (x * y) = WithVal.toVal v x * WithVal.toVal v y
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- the morphism from the first row to the second row  -/
CategoryTheory.ShortComplex.SnakeInput.v₁₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (self : CategoryTheory.ShortComplex.SnakeInput C) → self.L₁ ⟶ self.L₂
-- Init.Data.Option.Basic
/-- Recover from failing `Option` computations with a handler function.

This function is usually accessed through the `MonadExceptOf Unit Option` instance.

Examples:
* `Option.tryCatch none (fun () => some "handled") = some "handled"`
* `Option.tryCatch (some "succeeded") (fun () => some "handled") = some "succeeded"`
 -/
Option.tryCatch : {α : Type u_1} → Option α → (Unit → Option α) → Option α
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- If the first and third components of a morphism of distinguished triangles are
isomorphisms, the second component is as well. This can be thought of as a
pretriangulated category theoretical version of the five lemma.  -/
CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (φ : T ⟶ T'),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
      CategoryTheory.IsIso φ.hom₁ → CategoryTheory.IsIso φ.hom₃ → CategoryTheory.IsIso φ.hom₂
-- Mathlib.Analysis.CStarAlgebra.Spectrum
/-- **Spectral permanence.** The spectrum of an element is invariant of the (closed)
`StarSubalgebra` in which it is contained.  -/
StarSubalgebra.spectrum_eq : ∀ {A : Type u_1} [inst : CStarAlgebra A] (S : StarSubalgebra ℂ A) [hS : IsClosed ↑S] {a : ↥S},
  spectrum ℂ a = spectrum ℂ ↑a
-- Mathlib.Topology.Algebra.Algebra
/-- `ContinuousAlgHom.prod` as an `Equiv`.  -/
ContinuousAlgHom.prodEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_3} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] →
                  [inst_6 : Algebra R B] →
                    {C : Type u_4} →
                      [inst_7 : Semiring C] →
                        [inst_8 : Algebra R C] →
                          [inst_9 : TopologicalSpace C] → (A →A[R] B) × (A →A[R] C) ≃ (A →A[R] B × C)
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.EvalTacticFailure.state : Lean.Elab.Tactic.Grind.EvalTacticFailure → Lean.Elab.Tactic.Grind.SavedState
-- Mathlib.Computability.Ackermann
ack.eq_2 : ∀ (m : ℕ), ack m.succ 0 = ack m 1
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- The centralizer of a set as a non-unital subalgebra.  -/
NonUnitalSubalgebra.centralizer : (R : Type u_1) →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Set A → NonUnitalSubalgebra R A
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instBot.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M],
  AddSubmonoid.instBot = { bot := { carrier := {0}, add_mem' := ⋯, zero_mem' := ⋯ } }
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.instPow : Pow ℂ ℂ
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.instMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.IsPreimmersion f],
  AlgebraicGeometry.IsPreimmersion (f ∣_ V)
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNatLT : ∀ {n : ℕ} {h : n < UInt8.size}, (UInt8.ofNatLT n h).toNat = n
-- Mathlib.LinearAlgebra.BilinearMap
/-- Restrict the scalars, domains, and range of a bilinear map.  -/
LinearMap.restrictScalarsRange₂ : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        {P : Type u_5} →
          {M' : Type u_6} →
            {N' : Type u_7} →
              {P' : Type u_8} →
                [inst : CommSemiring R] →
                  [inst_1 : CommSemiring S] →
                    [inst_2 : SMul S R] →
                      [inst_3 : AddCommMonoid M] →
                        [inst_4 : Module R M] →
                          [inst_5 : AddCommMonoid N] →
                            [inst_6 : Module R N] →
                              [inst_7 : AddCommMonoid P] →
                                [inst_8 : Module R P] →
                                  [inst_9 : Module S M] →
                                    [inst_10 : Module S N] →
                                      [inst_11 : Module S P] →
                                        [IsScalarTower S R M] →
                                          [IsScalarTower S R N] →
                                            [IsScalarTower S R P] →
                                              [inst_15 : AddCommMonoid M'] →
                                                [inst_16 : Module S M'] →
                                                  [inst_17 : AddCommMonoid N'] →
                                                    [inst_18 : Module S N'] →
                                                      [inst_19 : AddCommMonoid P'] →
                                                        [inst_20 : Module S P'] →
                                                          [SMulCommClass R S P] →
                                                            (i : M' →ₗ[S] M) →
                                                              (j : N' →ₗ[S] N) →
                                                                (k : P' →ₗ[S] P) →
                                                                  Function.Injective ⇑k →
                                                                    (B : M →ₗ[R] N →ₗ[R] P) →
                                                                      (∀ (m : M') (n : N'), (B (i m)) (j n) ∈ k.range) →
                                                                        M' →ₗ[S] N' →ₗ[S] P'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getD_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k}, (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.toFun_eq : ∀ {R : Type u_1} [inst : Zero R] (f : ArithmeticFunction R), f.toFun = ⇑f
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- When `[HasImages C] [HasBinaryCoproducts C]`, `MonoOver A` has a `sup` construction,
which is functorial in both arguments,
and which on `Subobject A` will induce a `SemilatticeSup`.  -/
CategoryTheory.MonoOver.sup : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasImages C] →
      [CategoryTheory.Limits.HasBinaryCoproducts C] →
        {A : C} →
          CategoryTheory.Functor (CategoryTheory.MonoOver A)
            (CategoryTheory.Functor (CategoryTheory.MonoOver A) (CategoryTheory.MonoOver A))