mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.del.match_1.eq_4 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → RBTree.RBColor → Sort u_2) (c : RBTree.RBColor)
  (parent : RBTree.RBNode.Path α) (y : α) (b a : RBTree.RBNode α)
  (h_1 : (t : RBTree.RBNode α) → (x : RBTree.RBColor) → motive RBTree.RBNode.Path.root t x)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.red)
  (h_3 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.red)
  (h_4 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) →
        (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a RBTree.RBColor.black)
  (h_5 :
    (c : RBTree.RBColor) →
      (a : RBTree.RBNode α) →
        (y : α) →
          (parent : RBTree.RBNode.Path α) →
            (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b RBTree.RBColor.black),
  (match RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.black with
    | RBTree.RBNode.Path.root, t, x => h_1 t x
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.red => h_2 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.red => h_3 c a y parent b
    | RBTree.RBNode.Path.left c parent y b, a, RBTree.RBColor.black => h_4 c parent y b a
    | RBTree.RBNode.Path.right c a y parent, b, RBTree.RBColor.black => h_5 c a y parent b) =
    h_4 c parent y b a
-- Mathlib.Topology.Order.LiminfLimsup
BoundedLENhdsClass.of_closedIciTopology : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIciTopology α], BoundedLENhdsClass α
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.forget_preservesEpimorphisms : ∀ {R : Type u} [inst : Ring R], (CategoryTheory.forget (ModuleCat R)).PreservesEpimorphisms
-- Init.Data.UInt.Lemmas
USize.ofBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < 2 ^ System.Platform.numBits), { toBitVec := n#'hn } = USize.ofNatLT n hn
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapGrp_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal], e.mapGrp.functor = e.functor.mapGrp
-- Mathlib.Data.Finset.Range
Finset.range_zero : Finset.range 0 = ∅
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.eq_one_div_of_mul_eq_one_right : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] (I J : FractionalIdeal (nonZeroDivisors R₁) K),
  I * J = 1 → J = 1 / I
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- The canonical map on sheafifications induced by a morphism.  -/
CategoryTheory.GrothendieckTopology.sheafifyMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
              {P Q : CategoryTheory.Functor Cᵒᵖ D} → (P ⟶ Q) → (J.sheafify P ⟶ J.sheafify Q)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
_private.Mathlib.Analysis.InnerProductSpace.Orthogonal.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)),
  (F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp
        ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
        ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv.toNatTrans.app X)))
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
pos_of_mul_neg_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
  [AddRightReflectLE R] {a b : R}, a * b < 0 → b ≤ 0 → 0 < a
-- Mathlib.Order.Filter.Pi
/-- The indexed product of finitely many pure filters `pure (f i)` is the pure filter `pure f`.

If the index type is infinite, then `mem_pi_pure` and `hasBasis_pi_pure` below may be useful.  -/
Filter.pi_pure : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] (f : (i : ι) → α i), (Filter.pi fun x => pure (f x)) = pure f
-- Mathlib.Data.List.AList
AList.perm_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s₁ s₂ : AList β},
  s₁.entries.Perm s₂.entries → (AList.erase a s₁).entries.Perm (AList.erase a s₂).entries
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorObj_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X A : C}
  {Y Z : CategoryTheory.Over X} {f₁ f₂ : A ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z).left},
  f₁ = f₂ ↔
    CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.ChosenPullbacksAlong.fst Y.hom Z.hom) =
        CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.ChosenPullbacksAlong.fst Y.hom Z.hom) ∧
      CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.ChosenPullbacksAlong.snd Y.hom Z.hom) =
        CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.ChosenPullbacksAlong.snd Y.hom Z.hom)
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.lcomapDomain_apply : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {β : Type u_9} (f : α → β) (hf : Function.Injective f) (l : β →₀ M),
  (Finsupp.lcomapDomain f hf) l = Finsupp.comapDomain f l ⋯
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.ofRestrictScalars.eq_1 : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra R A]
  [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (U : Subalgebra S A) (f : ↥U →ₐ[S] B), Subalgebra.ofRestrictScalars R U f = AlgHom.restrictScalars R f
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.state : {α : Type} → Std.Bounded.Receiver✝ α → Std.Mutex (Std.Bounded.State✝ α)
-- Lean.Meta.Match.Match
Lean.Meta.Match.backward.match.sparseCases : Lean.Option Bool
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.ext_iff : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] {m m' : MeasureTheory.AddContent G C},
  m = m' ↔ ∀ (s : Set α), m s = m' s
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.instHasEnrichedHomUnderCompMapForget : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂] {j j' : J} (f : j ⟶ j'),
  CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom V
    ((CategoryTheory.Under.map f).comp ((CategoryTheory.Under.forget j).comp F₁))
    ((CategoryTheory.Under.map f).comp ((CategoryTheory.Under.forget j).comp F₂))
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank_toNat_eq_finrank : ∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] (A : Matrix m n R),
  Cardinal.toNat A.cRank = Module.finrank R ↥(Submodule.span R (Set.range A.col))
-- Mathlib.Algebra.Category.BialgCat.Basic
CategoryTheory.Iso.toBialgEquiv_trans : ∀ {R : Type u} [inst : CommRing R] {X Y Z : BialgCat R} (e : X ≅ Y) (f : Y ≅ Z),
  (e ≪≫ f).toBialgEquiv = e.toBialgEquiv.trans f.toBialgEquiv
-- Init.Data.List.Zip
List.zipWithAll_map_left : ∀ {α : Type u_1} {β : Type u_2} {α' : Type u_1} {γ : Type u_3} {l₁ : List α} {l₂ : List β} {f : α → α'}
  {g : Option α' → Option β → γ},
  List.zipWithAll g (List.map f l₁) l₂ = List.zipWithAll (fun a b => g (f <$> a) b) l₁ l₂
-- Mathlib.Algebra.Group.UniqueProds.Basic
instTwoUniqueSumsDFinsupp : ∀ {ι : Type u_2} (G : ι → Type u_1) [inst : (i : ι) → AddZeroClass (G i)] [∀ (i : ι), TwoUniqueSums (G i)],
  TwoUniqueSums (Π₀ (i : ι), G i)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- `Isδ₀ i` is a simple condition used to check whether a monomorphism `i` in
`SimplexCategory` identifies to the coface map `δ 0`.  -/
AlgebraicTopology.DoldKan.Isδ₀ : {Δ Δ' : SimplexCategory} → (i : Δ' ⟶ Δ) → [CategoryTheory.Mono i] → Prop
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The minimal distance is monotone with respect to inclusion.  -/
Metric.infDist_le_infDist_of_subset : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α} {x : α},
  s ⊆ t → s.Nonempty → Metric.infDist x t ≤ Metric.infDist x s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_eq_fallback : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {fallback : β}, a ∉ m → m.getD a fallback = fallback
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- The action of the tensor product on maps of `AugmentedSimplexCategory`.  -/
AugmentedSimplexCategory.tensorHom : {x₁ y₁ x₂ y₂ : AugmentedSimplexCategory} → (x₁ ⟶ y₁) → (x₂ ⟶ y₂) → (x₁.tensorObj x₂ ⟶ y₁.tensorObj y₂)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_eq_iff : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a b : α} {n : ℤ}, toIocDiv hp a b = n ↔ b - n • p ∈ Set.Ioc a (a + p)
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_toUInt8 : ∀ (n : UInt64), n.toUInt8.toUInt32 = n.toUInt32 % 256
-- Mathlib.Analysis.Complex.Poisson
_private.Mathlib.Analysis.Complex.Poisson.0.circleAverage_re_smul_on_ball_zero_aux : ∀ {R φ θ r : ℝ},
  ↑R * Complex.exp (↑θ * Complex.I) / (↑R * Complex.exp (↑θ * Complex.I) - ↑r * Complex.exp (↑φ * Complex.I)) -
      ↑r * Complex.exp (↑θ * Complex.I) / (↑r * Complex.exp (↑θ * Complex.I) - ↑R * Complex.exp (↑φ * Complex.I)) =
    ↑((↑R * Complex.exp (↑θ * Complex.I) + ↑r * Complex.exp (↑φ * Complex.I)) /
          (↑R * Complex.exp (↑θ * Complex.I) - ↑r * Complex.exp (↑φ * Complex.I))).re
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.instToFormatKey : Std.ToFormat Lean.Meta.DiscrTree.Key
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State.mvarId : Lean.Meta.Match.SimpH.State✝ → Lean.MVarId
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangle_mor₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Pretriangulated.contractibleTriangle X).mor₃ = 0
-- Mathlib.Order.Monotone.Monovary
Monovary.comp_monotone_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] {f : ι → α} {f' : α → γ} {g : ι → β}, Monovary f g → Monotone f' → Monovary (f' ∘ f) g
-- Mathlib.Algebra.Group.AddChar
AddChar.sum_eq_zero_iff_ne_zero : ∀ {A : Type u_1} {R : Type u_2} [inst : AddGroup A] [inst_1 : Fintype A] [inst_2 : CommSemiring R] [IsDomain R]
  {ψ : AddChar A R} [CharZero R], ∑ x, ψ x = 0 ↔ ψ ≠ 0
-- Lean.Parser.Syntax
Lean.Parser.Command.infix.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
ProfiniteGrp.ProfiniteCompletion.completion.eq_1 : ∀ (G : GrpCat),
  ProfiniteGrp.ProfiniteCompletion.completion G = ProfiniteGrp.limit (ProfiniteGrp.ProfiniteCompletion.diagram G)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.size_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.size = m₂.size
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic
monTypeInhabited : Inhabited (CategoryTheory.Mon (Type u))
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The functor `F.obj (.mk (op S)) ⥤ F.DescentData f`.  -/
CategoryTheory.Pseudofunctor.toDescentData : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            (f : (i : ι) → X i ⟶ S) → CategoryTheory.Functor (↑(F.obj { as := Opposite.op S })) (F.DescentData f)
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isColimitOfConeOfCoconeUnop_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cocone F.unop}
  (hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeUnop c))
  (s : CategoryTheory.Limits.Cocone F.unop),
  (CategoryTheory.Limits.isColimitOfConeOfCoconeUnop F hc).desc s =
    (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
-- Mathlib.Topology.Path
Path.extend_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (γ : Path x y), γ.extend 1 = y
-- Aesop.Search.Queue
Aesop.FIFOQueue.popGoal : Aesop.FIFOQueue → Option Aesop.GoalRef × Aesop.FIFOQueue
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.IsZeroAtImInfty.isBoundedAtImInfty : ∀ {α : Type u_1} [inst : SeminormedAddGroup α] {f : UpperHalfPlane → α},
  UpperHalfPlane.IsZeroAtImInfty f → UpperHalfPlane.IsBoundedAtImInfty f
-- Mathlib.Dynamics.Ergodic.Conservative
/-- Poincaré recurrence theorem: given a conservative map `f` and a measurable set `s`, the set
of points `x ∈ s` such that `x` does not return to `s` after `≥ n` iterations has measure zero.  -/
MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → α} {s : Set α} {μ : MeasureTheory.Measure α},
  MeasureTheory.Conservative f μ →
    MeasureTheory.NullMeasurableSet s μ → ∀ (n : ℕ), μ {x | x ∈ s ∧ ∀ m ≥ n, f^[m] x ∉ s} = 0
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_monadLift_OptionT_apply : ∀ {Pred : Type u} {EPred : Type u_1} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPost.Cons✝ Pred EPred} (x : m α),
  Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x post epost.tail)
    (Std.Internal.Do.wp (MonadLift.monadLift x) post epost)
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.snd_unop_hom : ∀ {R : Type u} [inst : CommRing R] (A B : (CommAlgCat R)ᵒᵖ),
  CommAlgCat.Hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd A B).unop = Algebra.TensorProduct.includeRight
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- The object function for the left adjoint to the comparison functor.  -/
CategoryTheory.Monad.MonadicityInternal.comparisonLeftAdjointObj : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (adj : F ⊣ G) →
              (A : adj.toMonad.Algebra) →
                [CategoryTheory.Limits.HasCoequalizer (F.map A.a) (adj.counit.app (F.obj A.A))] → D
-- Mathlib.NumberTheory.Padics.PadicNumbers
_private.Mathlib.NumberTheory.Padics.PadicNumbers.0.Padic.lim : {p : ℕ} → [inst : Fact (Nat.Prime p)] → CauSeq ℚ_[p] ⇑padicNormE → ℚ_[p]
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ ∩ t₂).getKeyD k fallback = fallback
-- Init.Data.Vector.Lemmas
Vector.findSomeRev?_eq_findSome?_reverse : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → Option β} {xs : Vector α n},
  Vector.findSomeRev? f xs = Vector.findSome? f xs.reverse
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Hard part of FTC-2 for integrable derivatives, real-valued functions: one has
`g b - g a ≤ ∫ y in a..b, g' y` when `g'` is integrable.
Auxiliary lemma in the proof of `integral_eq_sub_of_hasDeriv_right_of_le`.
We give the slightly more general version that `g b - g a ≤ ∫ y in a..b, φ y` when `g' ≤ φ` and
`φ` is integrable (even if `g'` is not known to be integrable).
Version assuming that `g` is differentiable on `[a, b)`.  -/
intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico : ∀ {g' g φ : ℝ → ℝ} {a b : ℝ},
  a ≤ b →
    ContinuousOn g (Set.Icc a b) →
      (∀ x ∈ Set.Ico a b, HasDerivWithinAt g (g' x) (Set.Ioi x) x) →
        MeasureTheory.IntegrableOn φ (Set.Icc a b) MeasureTheory.volume →
          (∀ x ∈ Set.Ico a b, g' x ≤ φ x) → g b - g a ≤ ∫ (y : ℝ) in a..b, φ y
-- Lean.Meta.Basic
Lean.Meta.Config.mk.sizeOf_spec : ∀
  (foApprox ctxApprox quasiPatternApprox constApprox isDefEqStuckEx unificationHints proofIrrelevance
    assignSyntheticOpaque offsetCnstrs : Bool)
  (transparency : Lean.Meta.TransparencyMode) (etaStruct : Lean.Meta.EtaStructMode) (univApprox iota beta : Bool)
  (proj : Lean.Meta.ProjReductionKind) (zeta zetaDelta zetaUnused zetaHave : Bool),
  sizeOf
      { foApprox := foApprox, ctxApprox := ctxApprox, quasiPatternApprox := quasiPatternApprox,
        constApprox := constApprox, isDefEqStuckEx := isDefEqStuckEx, unificationHints := unificationHints,
        proofIrrelevance := proofIrrelevance, assignSyntheticOpaque := assignSyntheticOpaque,
        offsetCnstrs := offsetCnstrs, transparency := transparency, etaStruct := etaStruct, univApprox := univApprox,
        iota := iota, beta := beta, proj := proj, zeta := zeta, zetaDelta := zetaDelta, zetaUnused := zetaUnused,
        zetaHave := zetaHave } =
    1 + sizeOf foApprox + sizeOf ctxApprox + sizeOf quasiPatternApprox + sizeOf constApprox + sizeOf isDefEqStuckEx +
                                sizeOf unificationHints +
                              sizeOf proofIrrelevance +
                            sizeOf assignSyntheticOpaque +
                          sizeOf offsetCnstrs +
                        sizeOf transparency +
                      sizeOf etaStruct +
                    sizeOf univApprox +
                  sizeOf iota +
                sizeOf beta +
              sizeOf proj +
            sizeOf zeta +
          sizeOf zetaDelta +
        sizeOf zetaUnused +
      sizeOf zetaHave
-- Mathlib.GroupTheory.Coset.Basic
leftCoset_assoc : ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α), a • b • s = (a * b) • s
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.comp_hom : ∀ {X Y Z : SFinKer} (κ : X.Hom Y) (η : Y.Hom Z), (CategoryTheory.CategoryStruct.comp κ η).hom = η.hom.comp κ.hom
-- Mathlib.CategoryTheory.PUnit
/-- Any two functors to `Discrete PUnit` are isomorphic.  -/
CategoryTheory.Functor.punitExt : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F G : CategoryTheory.Functor C (CategoryTheory.Discrete PUnit.{w + 1})) → F ≅ G
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.ShiftSequence.shiftIso_add : ∀ {C : Type u_1} {A : Type u_3} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_3, u_3} A} {F : CategoryTheory.Functor C A} {M : Type u_4} {inst_2 : AddMonoid M}
  {inst_3 : CategoryTheory.HasShift C M} [self : F.ShiftSequence M] (n m a a' a'' : M) (ha' : n + a = a')
  (ha'' : m + a' = a''),
  CategoryTheory.Functor.ShiftSequence.shiftIso (m + n) a a'' ⋯ =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorAdd C m n)
        (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫
      (CategoryTheory.shiftFunctor C m).associator (CategoryTheory.shiftFunctor C n)
          (CategoryTheory.Functor.ShiftSequence.sequence F a) ≪≫
        (CategoryTheory.shiftFunctor C m).isoWhiskerLeft (CategoryTheory.Functor.ShiftSequence.shiftIso n a a' ha') ≪≫
          CategoryTheory.Functor.ShiftSequence.shiftIso m a' a'' ha''
-- Mathlib.Data.Matrix.Basis
Matrix.single_apply_of_row_ne : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α]
  {i i' : m}, i ≠ i' → ∀ (j j' : n) (a : α), Matrix.single i j a i' j' = 0
-- Mathlib.Topology.Sets.Closeds
/-- the carrier set, i.e. the points in this set  -/
TopologicalSpace.Closeds.carrier : {α : Type u_4} → [inst : TopologicalSpace α] → TopologicalSpace.Closeds α → Set α
-- Init.Data.Nat.Basic
Nat.eq_add_of_sub_eq : ∀ {a b c : ℕ}, b ≤ a → a - b = c → a = c + b
-- Mathlib.Algebra.Field.Defs
DivisionRing.toDiv : {K : Type u_2} → [self : DivisionRing K] → Div K
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An iso `α ≃+ β` can equivalently be viewed as an iso `αᵃᵒᵖ ≃+ βᵃᵒᵖ`.  -/
AddEquiv.op : {α : Type u_3} → {β : Type u_4} → [inst : Add α] → [inst_1 : Add β] → α ≃+ β ≃ (αᵃᵒᵖ ≃+ βᵃᵒᵖ)
-- Mathlib.Algebra.MonoidAlgebra.Opposite
AddMonoidAlgebra.opRingEquiv_single : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Add M] (r : R) (x : M),
  AddMonoidAlgebra.opRingEquiv (MulOpposite.op (AddMonoidAlgebra.single x r)) =
    AddMonoidAlgebra.single (AddOpposite.op x) (MulOpposite.op r)
-- Mathlib.MeasureTheory.Integral.BoundedContinuousFunction
BoundedContinuousFunction.norm_integral_le_mul_norm : ∀ {X : Type u_1} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] (μ : MeasureTheory.Measure X) {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [OpensMeasurableSpace X] [SecondCountableTopology E] [inst_5 : MeasurableSpace E]
  [BorelSpace E] [inst_7 : NormedSpace ℝ E] [MeasureTheory.IsFiniteMeasure μ] (f : BoundedContinuousFunction X E),
  ‖∫ (x : X), f x ∂μ‖ ≤ μ.real Set.univ * ‖f‖
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
TopRep.d_comp_d : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (n : ℕ),
  CategoryTheory.CategoryStruct.comp (X.d n) (X.d (n + 1)) = 0
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.ofHom_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y) [inst_1 : W.ContainsIdentities], (CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).f = f
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The maximal reduction of a word. It is computable iff `α` has decidable equality.  -/
FreeAddGroup.reduce : {α : Type u_1} → [DecidableEq α] → List (α × Bool) → List (α × Bool)