mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
/-- Let `X : Type u`, `A : Set X`, `U : ι → Set X` and `V : ι → ι → Set X` such
that `MulticoequalizerDiagram A U V` holds, then in the category of types,
`A` is the multicoequalizer of the `U i`s along the `V i j`s. In this version,
we assume `ι` has a linear order, which allows to consider only the `V i j`
for which `i < j`.  -/
CategoryTheory.Limits.Types.isColimitOfMulticoequalizerDiagram' : {X : Type u} →
  {ι : Type w} →
    {A : Set X} →
      {U : ι → Set X} →
        {V : ι → ι → Set X} →
          [inst : LinearOrder ι] →
            (c : CompleteLattice.MulticoequalizerDiagram A U V) →
              CategoryTheory.Limits.IsColimit (c.multicofork.toLinearOrder.map Set.functorToTypes)
-- Mathlib.Algebra.Torsor.Basic
smul_sdiv_smul_cancel_left : ∀ {G : Type u_1} {P : Type u_2} [inst : CommGroup G] [inst_1 : Torsor G P] (v : G) (p₁ p₂ : P),
  v • p₁ /ₛ v • p₂ = p₁ /ₛ p₂
-- Mathlib.Algebra.Module.Submodule.Ker
Submodule.ker_inclusion : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M) (h : p ≤ p'), (Submodule.inclusion h).ker = ⊥
-- Mathlib.Data.List.Sort
/-- `insertionSort l` returns `l` sorted using the insertion sort algorithm.  -/
List.insertionSort : {α : Type u_1} → (r : α → α → Prop) → [DecidableRel r] → List α → List α
-- Mathlib.Topology.Algebra.ConstMulAction
subset_interior_vadd_right : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] {s : Set G} {t : Set α}, s +ᵥ interior t ⊆ interior (s +ᵥ t)
-- Init.Meta.Defs
/-- Finds the first `SourceInfo` from the back of `stx` or `none` if no `SourceInfo` can be found.
 -/
Lean.Syntax.getTailInfo? : Lean.Syntax → Option Lean.SourceInfo
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_congr_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f g : α → MeasureTheory.Measure β}, f =ᵐ[μ] g → μ.bind f = μ.bind g
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_15.eq_3 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3)
  (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star)
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x with
    | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => h_2 unop x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_3 x
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.one_le_blocks : ∀ {n : ℕ} (c : Composition n) {i : ℕ}, i ∈ c.blocks → 1 ≤ i
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Subalgebra.eq_bot_of_rank_le_one : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  {S : Subalgebra F E}, Module.rank F ↥S ≤ 1 → ∀ [Module.Free F ↥S], S = ⊥
-- Lean.DocString.Parser
/-- Parses emphasis: a matched pair of one or more `_`.
 -/
Lean.Doc.Parser.emph : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (t.alter k f).isEmpty = ((t.isEmpty || t.size == 1 && t.contains k) && (f t[k]?).isNone)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.restrictSubtype.eq_1 : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.restrictSubtype X = (M.restrict X).comap Subtype.val
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- The product of two Chebyshev `C` polynomials is the sum of two other Chebyshev `C` polynomials.
 -/
Polynomial.Chebyshev.C_mul_C : ∀ (R : Type u_1) [inst : CommRing R] (m k : ℤ),
  Polynomial.Chebyshev.C R m * Polynomial.Chebyshev.C R k =
    Polynomial.Chebyshev.C R (m + k) + Polynomial.Chebyshev.C R (m - k)
-- Init.Try
/-- `register_try?_tactic tac` registers a tactic `tac` as a suggestion generator for the `try?` tactic.

An optional priority can be specified with `register_try?_tactic (priority := 500) tac`.
Higher priority generators are tried first. The default priority is 1000.
 -/
Lean.Parser.Command.registerTryTactic : Lean.ParserDescr
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.step.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) (l : Λ) (v : σ)
  (T : Turing.Tape Γ), Turing.TM1.step M { l := some l, var := v, Tape := T } = some (Turing.TM1.stepAux (M l) v T)
-- Init.Simproc
/-- Auxiliary command for associating a pattern with a simplification procedure.
 -/
Lean.Parser.simprocPattern : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.instMonoidalFunctorTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  (e : C ≌ D) →
                    [e.functor.Monoidal] → (e' : D ≌ E) → [e'.functor.Monoidal] → (e.trans e').functor.Monoidal
-- Lean.Meta.Tactic.Grind.Types
/-- Returns activated `match`-declaration equations.
Recall that in tactics such as `instantiate only [...]`, `match`-declarations are always instantiated.
 -/
Lean.Meta.Grind.Goal.getActiveMatchEqTheorems : Lean.Meta.Grind.Goal → Lean.CoreM (Array Lean.Meta.Grind.EMatchTheorem)
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instSMulNat : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → SMul ℕ (ρ.IntertwiningMap σ)
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinearEquivRight'OfInv_apply : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} {n : Type u_4} [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  [inst_3 : Fintype n] [inst_4 : DecidableEq n] {M : Matrix m n R} {M' : Matrix n m R} (hMM' : M * M' = 1)
  (hM'M : M' * M = 1) (a : n → R) (a_1 : m),
  (Matrix.toLinearEquivRight'OfInv hMM' hM'M) a a_1 = (Matrix.toLinearMapRight' M') a a_1
-- Mathlib.Order.Basic
instDenselyOrderedForall : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → Preorder (π i)] [∀ (i : ι), DenselyOrdered (π i)],
  DenselyOrdered ((i : ι) → π i)
-- Mathlib.Data.Set.SMulAntidiagonal
Set.SMulAntidiagonal.fst_eq_fst_iff_snd_eq_snd : ∀ {G : Type u_1} {P : Type u_2} {s : Set G} {t : Set P} {a : P} [inst : SMul G P] {x y : ↑(s.smulAntidiagonal t a)}
  [IsCancelSMul G P], (↑x).1 = (↑y).1 ↔ (↑x).2 = (↑y).2
-- Mathlib.Data.Seq.Basic
Stream'.Seq.join_cons_cons : ∀ {α : Type u} (a b : α) (s : Stream'.Seq α) (S : Stream'.Seq (Stream'.Seq1 α)),
  (Stream'.Seq.cons (a, Stream'.Seq.cons b s) S).join = Stream'.Seq.cons a (Stream'.Seq.cons (b, s) S).join
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.mk : {M : Type u_10} →
  {N : Type u_11} →
    [inst : Add M] → [inst_1 : Add N] → (toFun : M → N) → (∀ (x y : M), toFun (x + y) = toFun x + toFun y) → M →ₙ+ N
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).get? k' = some (cast ⋯ v)
-- Mathlib.Topology.Algebra.GroupWithZero
/-- Eta-expanded form of `ContinuousWithinAt.inv₀` -/
ContinuousWithinAt.fun_inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {f : α → G₀} {s : Set α} {a : α} [inst_4 : TopologicalSpace α],
  ContinuousWithinAt f s a → f a ≠ 0 → ContinuousWithinAt (fun i => (f i)⁻¹) s a
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalBitVec_qq : {n : ℕ} → Lean.Meta.ReduceEval (BitVec n)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instSemilatticeSup : {R : Type u_2} →
  {N : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : TopologicalSpace N] →
          [inst_3 : Module R N] → [ContinuousAdd N] → [ContinuousConstSMul R N] → SemilatticeSup (ClosedSubmodule R N)
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.throwNotRing : {α : Type} → Lean.Meta.Grind.Arith.Linear.LinearM α
-- Mathlib.Topology.Order.OrderClosed
instClosedIicTopologyOrderDual : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α], ClosedIicTopology αᵒᵈ
-- Init.Data.Vector.Lemmas
Vector.allM_mk : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] {p : α → m Bool} {xs : Array α} (h : xs.size = n),
  Vector.allM p (Vector.mk xs h) = Array.allM p xs
-- Lean.Language.Basic
Lean.Language.instInhabitedSnapshotTree : Inhabited Lean.Language.SnapshotTree
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- Compatible equivalences of types and hom-types induce an isomorphism of reflexive quivers.  -/
CategoryTheory.ReflQuiv.isoOfEquiv : {V W : Type u} →
  [inst : CategoryTheory.ReflQuiver V] →
    [inst_1 : CategoryTheory.ReflQuiver W] →
      (e : V ≃ W) →
        (he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)) →
          (∀ (X : V), (he X X) (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (e X)) →
            (CategoryTheory.ReflQuiv.of V ≅ CategoryTheory.ReflQuiv.of W)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.alter.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.continuous_dual_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] (x : E) (y : StrongDual 𝕜₂ F), Continuous fun A => y (A x)
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.extract' : ∀ {l ml mm mr r : List Char} {b e : String.Pos.Raw} {s : Substring.Raw},
  Substring.Raw.ValidFor l (ml ++ mm ++ mr) r s →
    Substring.Raw.ValidFor ml mm mr { str := String.ofList (ml ++ mm ++ mr), startPos := b, stopPos := e } →
      ∃ l' r', Substring.Raw.ValidFor l' mm r' (s.extract b e)
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.smul : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : SMul M X] {m : MeasurableSpace α}
  {f : α → M} {g : α → X} [inst_2 : MeasurableSpace M] [MeasurableSMul₂ M X],
  Measurable f → Measurable g → Measurable (f • g)
-- Init.Coe
/-- `CoeT` is the core typeclass which is invoked by Lean to resolve a type error.
It can also be triggered explicitly with the notation `↑x` or by double type
ascription `((x : α) : β)`.

A `CoeT` chain has the grammar `CoeHead? CoeOut* Coe* CoeTail? | CoeDep`.
 -/
CoeT : (α : Sort u) → α → Sort v → Sort (max 1 v)
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.coe_pure : ∀ {α : Type u} (a : α), ↑(pure a) = pure a
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_mul_left : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {c : ℝ},
      autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_mul_left._auto_1 →
        autoParam (‖f (c * min (a / c) (b / c))‖ₑ ≠ ⊤) IntervalIntegrable.comp_mul_left._auto_3 →
          IntervalIntegrable (fun x => f (c * x)) MeasureTheory.volume (a / c) (b / c)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatch.not_isMatch : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos →
    ∀ (pos' : s.Pos), pos < pos' → ¬String.Slice.Pattern.Model.IsMatch pat pos'
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_uIoc_succ : ∀ {n : ℕ} (i j : Fin n), Fin.succ ⁻¹' Set.uIoc i.succ j.succ = Set.uIoc i j
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintOptions.mk.injEq : ∀ (toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions) (resolveProvider? : Option Bool)
  (toWorkDoneProgressOptions_1 : Lean.Lsp.WorkDoneProgressOptions) (resolveProvider?_1 : Option Bool),
  ({ toWorkDoneProgressOptions := toWorkDoneProgressOptions, resolveProvider? := resolveProvider? } =
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions_1, resolveProvider? := resolveProvider?_1 }) =
    (toWorkDoneProgressOptions = toWorkDoneProgressOptions_1 ∧ resolveProvider? = resolveProvider?_1)
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.sheafFiberCompIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] {B : Type u''}
  [inst_2 : CategoryTheory.Category.{v'', u''} B] [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] (F : CategoryTheory.Functor A B)
  [inst_5 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_6 : CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F]
  [inst_7 : J.HasSheafCompose F] (X : CategoryTheory.Sheaf J A),
  (Φ.sheafFiberCompIso F).inv.app X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (F.obj (Φ.presheafFiber.obj X.obj)))
      ((Φ.presheafFiberCompIso F).inv.app X.obj)
-- Init.Data.Array.Lemmas
Array.map_filter_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {p : α → Bool} {xs : Array α},
  Array.map f (Array.filter p xs) = Array.foldl (fun acc x => bif p x then acc.push (f x) else acc) #[] xs
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.isoMk_inv_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f f' : CategoryTheory.CostructuredArrow S T} (g : f.left ≅ f'.left)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (S.map g.hom) f'.hom = f.hom)
      CategoryTheory.CostructuredArrow.isoMk._auto_1),
  (CategoryTheory.CostructuredArrow.isoMk g w).inv.left = g.inv
-- Std.Http.Server.Config
Std.Http.Config.mk : ℕ →
  ℕ →
    ℕ →
      ℕ →
        Std.Time.Millisecond.Offset →
          { x // x > 0 } →
            Std.Time.Millisecond.Offset →
              Bool →
                ℕ →
                  ℕ →
                    Bool →
                      Option Std.Http.Header.Value →
                        ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → Std.Http.Config
-- Mathlib.Data.Sum.Basic
Function.Injective.sumMap : ∀ {α : Type u} {α' : Type w} {β : Type v} {β' : Type x} {f : α → β} {g : α' → β'},
  Function.Injective f → Function.Injective g → Function.Injective (Sum.map f g)
-- Mathlib.Algebra.Polynomial.OfFn
Polynomial.ofFn.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] (n : ℕ),
  Polynomial.ofFn n =
    { toFun := fun v => { toFinsupp := AddMonoidAlgebra.ofCoeff (List.ofFn v).toFinsupp }, map_add' := ⋯,
      map_smul' := ⋯ }
-- Init.Data.Range.Polymorphic.Basic
/-- If the smallest value in the range satisfies the upper bound and has no successor, the size is
  one.
   -/
Std.Rxc.LawfulHasSize.size_eq_one_of_succ?_eq_none : ∀ {α : Type u} {inst : LE α} {inst_1 : Std.PRange.UpwardEnumerable α} {inst_2 : Std.Rxc.HasSize α}
  [self : Std.Rxc.LawfulHasSize α] (lo hi : α), lo ≤ hi → Std.PRange.succ? lo = none → Std.Rxc.HasSize.size lo hi = 1
-- Batteries.Control.AlternativeMonad
/-- `failure` is a left identity for `orElse`.  -/
LawfulAlternative.failure_orElse : ∀ {m : Type u_1 → Type u_2} {inst : Alternative m} [self : LawfulAlternative m] {α : Type u_1} (y : m α),
  (failure <|> y) = y
-- Mathlib.NumberTheory.Real.Irrational
Irrational.div_intCast : ∀ {x : ℝ}, Irrational x → ∀ {m : ℤ}, m ≠ 0 → Irrational (x / ↑m)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {n : ℤ}
  {X Y : Cᵒᵖ} (f : Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y),
  CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv f =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X)
      ((CategoryTheory.shiftFunctor Cᵒᵖ n).map f)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (h : k ∈ m), (m.getKey k h == k) = true
-- Mathlib.Analysis.Distribution.Sobolev
/-- A tempered distribution `f` is a Sobolev function of order `s` if there exists an `Lp` function
`f'` such that `𝓕⁻ (1 + ‖x‖ ^ 2) ^ (s / 2) 𝓕 f = f'`.  -/
TemperedDistribution.MemSobolev : {E : Type u_1} →
  {F : Type u_2} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : InnerProductSpace ℝ E] →
          [FiniteDimensional ℝ E] →
            [inst_4 : MeasurableSpace E] →
              [BorelSpace E] →
                [inst_6 : NormedSpace ℂ F] →
                  [CompleteSpace F] → ℝ → (p : ENNReal) → [hp : Fact (1 ≤ p)] → TemperedDistribution E F → Prop
-- Mathlib.Data.Finsupp.Option
Finsupp.optionEquiv_symm_apply : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (P : M × (α →₀ M)),
  Finsupp.optionEquiv.symm P = (Finsupp.embDomain Function.Embedding.some P.2).update none P.1
-- Lean.Parser.Term.Doc
/-- Renders the recommended spellings for the given declaration into a string for appending to
the docstring.  -/
Lean.Parser.Term.Doc.getRecommendedSpellingString : Lean.Environment → Lean.Name → String
-- Mathlib.Logic.Equiv.Fin.Basic
finAddFlip_apply_mk_left : ∀ {m n k : ℕ} (h : k < m) (hk : optParam (k < m + n) ⋯) (hnk : optParam (n + k < n + m) ⋯),
  finAddFlip ⟨k, hk⟩ = ⟨n + k, hnk⟩
-- Mathlib.RingTheory.Unramified.Basic
Shrink.ringEquiv.eq_1 : ∀ (α : Type u_1) [inst : Small.{v, u_1} α] [inst_1 : Add α] [inst_2 : Mul α],
  Shrink.ringEquiv α = (equivShrink α).symm.ringEquiv
-- Mathlib.Data.Finsupp.Basic
/-- The `Finsupp` version of `Pi.unique`.  -/
Finsupp.uniqueOfRight : {α : Type u_1} → {R : Type u_10} → [inst : Zero R] → [Subsingleton R] → Unique (α →₀ R)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.mk_lt_mk : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M} (ha : a ≠ 1) {b : M}
  (hb : b ≠ 1),
  FiniteMulArchimedeanClass.mk a ha < FiniteMulArchimedeanClass.mk b hb ↔
    MulArchimedeanClass.mk a < MulArchimedeanClass.mk b
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instSMulCommClass : ∀ (R : Type u_1) (R' : Type u_2) (A : Type u_3) (E : Type u_4) [inst : SMul R E] [inst_1 : SMul R' E]
  [SMulCommClass R R' E], SMulCommClass R R' (WithCStarModule A E)
-- Mathlib.Order.Interval.Set.Image
StrictMono.image_Ioc_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictMono f → f '' Set.Ioc a b ⊆ Set.Ioc (f a) (f b)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
/-- **Alias** of `measurable_infEDist`. -/
measurable_infEdist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α},
  Measurable fun x => Metric.infEDist x s
-- Batteries.Data.ByteArray
_private.Batteries.Data.ByteArray.0.ByteArray.get.match_1.eq_1 : ∀ (motive : (x : ByteArray) → (x_1 : ℕ) → x_1 < x.size → Sort u_1) (bs : Array UInt8) (i : ℕ)
  (x : i < { data := bs }.size)
  (h_1 : (bs : Array UInt8) → (i : ℕ) → (x : i < { data := bs }.size) → motive { data := bs } i x),
  (match { data := bs }, i, x with
    | { data := bs }, i, x => h_1 bs i x) =
    h_1 bs i x
-- Init.GrindInstances.Ring.UInt
UInt64.intCast_neg : ∀ (x : ℤ), ↑(-x) = -↑x
-- Init.Data.Nat.Bitwise.Lemmas
Nat.xor_comm : ∀ (x y : ℕ), x ^^^ y = y ^^^ x
-- Mathlib.Topology.DiscreteSubset
IsDiscrete.univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [DiscreteTopology X], IsDiscrete Set.univ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.subsingleton_of_subsingleton : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] {S : AddSubmonoid M} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) [Subsingleton M], Subsingleton N
-- Mathlib.Data.Finsupp.Order
Finsupp.single_nonneg : ∀ {ι : Type u_1} {α : Type u_3} [inst : Zero α] [inst_1 : Preorder α] {i : ι} {a : α}, (0 ≤ fun₀ | i => a) ↔ 0 ≤ a
-- Mathlib.Topology.Algebra.GroupWithZero
/-- The function `f x / g x` is discontinuous when `g x = 0`. However, under appropriate
conditions, `h x (f x / g x)` is still continuous.  The condition is that if `g a = 0` then `h x y`
must tend to `h a 0` when `x` tends to `a`, with no information about `y`. This is represented by
the `⊤` filter.  Note: `tendsto_prod_top_iff` characterizes this convergence in uniform spaces.  See
also `Filter.prod_top` and `Filter.mem_prod_top`.  -/
ContinuousAt.comp_div_cases : ∀ {α : Type u_1} {β : Type u_2} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀]
  [ContinuousInv₀ G₀] [ContinuousMul G₀] [inst_4 : TopologicalSpace α] [inst_5 : TopologicalSpace β] {a : α}
  {f g : α → G₀} (h : α → G₀ → β),
  ContinuousAt f a →
    ContinuousAt g a →
      (g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)) →
        (g a = 0 → Filter.Tendsto (↿h) (nhds a ×ˢ ⊤) (nhds (h a 0))) → ContinuousAt (fun x => h x (f x / g x)) a
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.comp : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            (F : CategoryTheory.Functor C D) →
              (G : CategoryTheory.Functor D E) →
                {A : Type u_4} →
                  [inst_3 : AddMonoid A] →
                    [inst_4 : CategoryTheory.HasShift C A] →
                      [inst_5 : CategoryTheory.HasShift D A] →
                        [inst_6 : CategoryTheory.HasShift E A] →
                          [F.CommShift A] → [G.CommShift A] → (F.comp G).CommShift A