mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.karoubi_alternatingFaceMapComplex_d : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C)) (n : ℕ),
  ((AlgebraicTopology.AlternatingFaceMapComplex.obj
            (CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj P)).d
        (n + 1) n).f =
    CategoryTheory.CategoryStruct.comp (P.p.app (Opposite.op { len := n + 1 }))
      ((AlgebraicTopology.AlternatingFaceMapComplex.obj P.X).d (n + 1) n)
-- Mathlib.Data.Finset.Empty
Finset.nonempty_coe_sort : ∀ {α : Type u_1} {s : Finset α}, Nonempty ↥s ↔ s.Nonempty
-- Mathlib.RingTheory.Ideal.Maximal
/-- If a maximal principal ideal is not generated by an idempotent,
then every generator is irreducible.  -/
Ideal.irreducible_of_isMaximal_of_eq_span_singleton_of_not_isIdempotentElem : ∀ {α : Type u} [inst : CommSemiring α] {a : α},
  (Ideal.span {a}).IsMaximal → (∀ (x : α), Ideal.span {a} = Ideal.span {x} → ¬IsIdempotentElem x) → Irreducible a
-- Mathlib.Data.List.Lookmap
List.lookmap_of_forall_not : ∀ {α : Type u_1} (f : α → Option α) {l : List α}, (∀ a ∈ l, f a = none) → List.lookmap f l = l
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.instCategory : CategoryTheory.Category.{u, u + 1} MonCat
-- Mathlib.Algebra.Free
FreeAddSemigroup.lift_of_add : ∀ {α : Type u} {β : Type v} [inst : AddSemigroup β] (f : α → β) (x : α) (y : FreeAddSemigroup α),
  (FreeAddSemigroup.lift f) (FreeAddSemigroup.of x + y) = f x + (FreeAddSemigroup.lift f) y
-- Mathlib.Algebra.Group.Subsemigroup.Operations
_private.Mathlib.Algebra.Group.Subsemigroup.Operations.0.AddHom.srange_mk_aux_add : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M → N},
  (∀ (x y : M), f (x + y) = f x + f y) → ∀ {x y : N}, x ∈ Set.range f → y ∈ Set.range f → x + y ∈ Set.range f
-- Mathlib.Algebra.Module.Equiv.Basic
Units.mulLeftLinearEquiv_trans_mulLeftLinearEquiv : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a b : Aˣ),
  (Units.mulLeftLinearEquiv R A) a ≪≫ₗ (Units.mulLeftLinearEquiv R A) b = (Units.mulLeftLinearEquiv R A) (b * a)
-- Mathlib.Data.Rel
SetRel.preimage_union : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t₁ t₂ : Set β), R.preimage (t₁ ∪ t₂) = R.preimage t₁ ∪ R.preimage t₂
-- Mathlib.Computability.AkraBazzi.SumTransform
/-- The exponent `p` associated with a particular Akra-Bazzi recurrence.  -/
AkraBazziRecurrence.p : {α : Type u_2} → [Fintype α] → (α → ℝ) → (α → ℝ) → ℝ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- This is a helper construction that can be useful when verifying that a category has all
pullbacks. Given `F : WalkingCospan ⥤ C`, which is really the same as
`cospan (F.map inl) (F.map inr)`, and a pullback cone on `F.map inl` and `F.map inr`, we
get a cone on `F`.

If you're thinking about using this, have a look at `hasPullbacks_of_hasLimit_cospan`,
which you may find to be an easier way of achieving your goal.  -/
CategoryTheory.Limits.Cone.ofPullbackCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} →
      CategoryTheory.Limits.PullbackCone (F.map CategoryTheory.Limits.WalkingCospan.Hom.inl)
          (F.map CategoryTheory.Limits.WalkingCospan.Hom.inr) →
        CategoryTheory.Limits.Cone F
-- Mathlib.Analysis.Normed.Group.Uniform
LipschitzWith.norm_div_le_of_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {f : E → F} {C : NNReal}
  {a b : E} {r : ℝ}, LipschitzWith C f → ‖a / b‖ ≤ r → ‖f a / f b‖ ≤ ↑C * r
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGE.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, (compare a k).isGE = true) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isGE = true) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β ky) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isGE = true) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.leaf, x, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_1 x he
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The cosine of the oriented angle between two nonzero vectors is the inner product divided by
the product of the norms.  -/
Orientation.cos_oangle_eq_inner_div_norm_mul_norm : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, x ≠ 0 → y ≠ 0 → (o.oangle x y).cos = inner ℝ x y / (‖x‖ * ‖y‖)
-- Mathlib.Computability.Language
Language.append_mem_mul : ∀ {α : Type u_1} {l m : Language α} {a b : List α}, a ∈ l → b ∈ m → a ++ b ∈ l * m
-- Init.Data.SInt.Bitwise
Int64.shiftLeft_and : ∀ {a b c : Int64}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.pentagon_aux₃ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₃ : CategoryTheory.LocalizedMonoidal L W ε} (i : X₃ ≅ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) i.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ Y₃).hom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ i.inv))) =
    (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.detp_eq_of_col_eq_zero : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (s : ℤˣ)
  {A : Matrix n n R} {p : n}, A.col p = 0 → Matrix.detp s A = 0
-- Mathlib.CategoryTheory.Comma.Basic
/-- The canonical equivalence between `Comma L R` and `(Comma R.op L.op)ᵒᵖ`.  -/
CategoryTheory.Comma.opEquiv : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) → CategoryTheory.Comma L R ≌ (CategoryTheory.Comma R.op L.op)ᵒᵖ
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.LaxTrans.id_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {x x_1 : B} (f : x ⟶ x_1),
  (CategoryTheory.CategoryStruct.id F).naturality f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).hom
      (CategoryTheory.Bicategory.rightUnitor (F.map f)).inv
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadMap_refl : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u} {f : {β : Type u} → m β → m β} {x : m α}
  {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps], ⦃(Std.Do.wp (f x)).apply Q⦄ monadMap f x ⦃Q⦄
-- Mathlib.Algebra.Order.Monoid.Lex
OrderAddMonoidHom.fst_comp_inr : ∀ (α : Type u_1) (β : Type u_2) [inst : AddMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddMonoid β]
  [inst_3 : Preorder β], (OrderAddMonoidHom.fst α β).comp (OrderAddMonoidHom.inr α β) = 0
-- Std.Data.HashMap.Raw
/-- Checks whether a key is present in a map, and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.HashMap.Raw.containsThenInsert : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → β → Bool × Std.HashMap.Raw α β
-- Init.Grind.AC
Lean.Grind.AC.Seq.concat.induct_unfolding : ∀ (s₂ : Lean.Grind.AC.Seq) (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Prop),
  (∀ (x : Lean.Grind.AC.Var), motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.cons x s₂)) →
    (∀ (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq),
        motive s (s.concat s₂) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.cons x (s.concat s₂))) →
      ∀ (s₁ : Lean.Grind.AC.Seq), motive s₁ (s₁.concat s₂)
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
IsSelfAdjoint.nnnorm_sum_eq_sup : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {ι : Type u_2} {f : ι → A} (s : Finset ι),
  (∀ i ∈ s, IsSelfAdjoint (f i)) →
    Pairwise (Function.onFun (fun x1 x2 => x1 * x2 = 0) f) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x => ‖f x‖₊
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
_private.Mathlib.RingTheory.PowerSeries.WeierstrassPreparation.0.PowerSeries.coeff_trunc_order_mem : ∀ {A : Type u_1} [inst : CommRing A] (g : PowerSeries A) (I : Ideal A) (i : ℕ),
  ((PowerSeries.trunc ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat) g).coeff i ∈ I
-- Mathlib.CategoryTheory.Limits.Types.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ Type*`, this is the projection `end_ F ⟶ (F.obj (op j)).obj j`
for any `j : J`, which sends `x` to `x.1 j`.  -/
CategoryTheory.Limits.Types.end_.π : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))) →
      (j : J) → CategoryTheory.Limits.Types.end_ F ⟶ (F.obj (Opposite.op j)).obj j
-- Mathlib.Control.ULift
PLift.rec.constant : ∀ {α : Sort u} {β : Type v} (b : β), (PLift.rec fun x => b) = fun x => b
-- Mathlib.RingTheory.KrullDimension.NonZeroDivisors
ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial : ∀ {R : Type u_1} [inst : CommRing R] (σ : Type u_3) [Finite σ],
  ringKrullDim R + ↑(Nat.card σ) ≤ ringKrullDim (MvPolynomial σ R)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.preimage_mk_one : ∀ {α : Type u_1} [inst : Group α] (N : Subgroup α), QuotientGroup.mk ⁻¹' {↑1} = ↑N
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber.eq_1 : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal) (A : Set X),
  Metric.externalCoveringNumber ε A = ⨅ C, ⨅ (_ : Metric.IsCover ε A C), C.encard
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.leftZigzag.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ⟶ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ⟶ CategoryTheory.CategoryStruct.id b),
  CategoryTheory.Bicategory.leftZigzag η ε =
    CategoryTheory.bicategoricalComp (CategoryTheory.Bicategory.whiskerRight η f)
      (CategoryTheory.Bicategory.whiskerLeft f ε)
-- Mathlib.Topology.Algebra.Ring.Basic
instIsSemitopologicalRingAddOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [IsSemitopologicalRing R],
  IsSemitopologicalRing Rᵃᵒᵖ
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps.mk : Std.HashMap ℕ (Std.TreeSet ℕ compare) → Lean.Meta.Match.Overlaps
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.instIterator : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α m β] → {P : β → Prop} → Std.Iterator (Std.Iterators.Types.Attach α m P) m { out // P out }
-- Mathlib.Data.Set.Sigma
Set.sigma_subset_iff : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {u : Set ((i : ι) × α i)},
  s.sigma t ⊆ u ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃a : α i⦄, a ∈ t i → ⟨i, a⟩ ∈ u
-- Mathlib.Algebra.Homology.SpectralObject.Page
_private.Mathlib.Algebra.Homology.SpectralObject.Page.0.CategoryTheory.ComposableArrows.Precomp.obj.match_1.splitter : {n : ℕ} →
  (motive : Fin (n + 1 + 1) → Sort u_1) →
    (x : Fin (n + 1 + 1)) →
      ((isLt : 0 < n + 1 + 1) → motive ⟨0, isLt⟩) →
        ((i : ℕ) → (hi : i + 1 < n + 1 + 1) → motive ⟨i.succ, hi⟩) → motive x
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentation.linearEquiv_symm_var : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] {solution : relations.Solution M} (h : solution.IsPresentation) (g : relations.G),
  h.linearEquiv.symm (solution.var g) = relations.toQuotient fun₀ | g => 1
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.coe_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X : LeftInvariantDerivation I G), ⇑(-X) = -⇑X
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntry?.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3) (size : ℕ) (k : α) (v : β k)
  (l : Std.DTreeMap.Internal.Impl α β) (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.inner size k v l 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_2 size k v l
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.monic_monomial_one : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {d : σ →₀ ℕ},
  m.Monic ((MvPolynomial.monomial d) 1)
-- Mathlib.Analysis.Analytic.Basic
/-- If a function admits a power series expansion within a set at `x`, then it is the locally
uniform limit of the partial sums of this power series on the disk of convergence, i.e., `f (x + y)`
is the locally uniform limit of `p.partialSum n y` there.  -/
HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn : ∀ {𝕜 : 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] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    TendstoLocallyUniformlyOn (fun n y => p.partialSum n y) (fun y => f (x + y)) Filter.atTop
      ((fun x_1 => x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r)
-- Mathlib.Algebra.Order.Field.Power
/-- **Alias** of the reverse direction of `Odd.zpow_nonpos_iff`. -/
Odd.zpow_nonpos : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a : α} {n : ℤ},
  Odd n → a ≤ 0 → a ^ n ≤ 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.length_toList : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α] [Std.Rxi.LawfulHasSize α],
  r.toList.length = r.size
-- Init.Data.Fin.Lemmas
Fin.val_mul : ∀ {n : ℕ} (a b : Fin n), ↑(a * b) = ↑a * ↑b % n
-- Mathlib.Order.Filter.Interval
Filter.Tendsto.Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {l₁ l₂ : Filter α} [Filter.TendstoIxxClass Set.Ioo l₁ l₂]
  {lb : Filter β} {u₁ u₂ : β → α},
  Filter.Tendsto u₁ lb l₁ → Filter.Tendsto u₂ lb l₁ → Filter.Tendsto (fun x => Set.Ioo (u₁ x) (u₂ x)) lb l₂.smallSets
-- Mathlib.Data.List.Nodup
List.get_idxOf : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α}, l.Nodup → ∀ (i : Fin l.length), List.idxOf (l.get i) l = ↑i
-- Mathlib.Order.Grade
/-- Lifts a graded order along a strictly monotone function.  -/
GradeMinOrder.liftLeft : {𝕆 : Type u_1} →
  {ℙ : Type u_2} →
    {α : Type u_3} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder ℙ] →
          [inst_2 : Preorder α] →
            [GradeMinOrder 𝕆 α] →
              (f : 𝕆 → ℙ) →
                StrictMono f → (∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) → (∀ (a : 𝕆), IsMin a → IsMin (f a)) → GradeMinOrder ℙ α
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_nonneg_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → 0 ≤ a.fmod b
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSemiringOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : Semiring Mᵐᵒᵖ], DomMulAct.instSemiringOfMulOpposite = inst
-- Mathlib.CategoryTheory.Linear.Basic
CategoryTheory.Linear.instEpiHSMulHomOfInvertible : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type w)
  [inst_2 : Semiring R] [inst_3 : CategoryTheory.Linear R C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] (r : R)
  [Invertible r], CategoryTheory.Epi (r • f)
-- Mathlib.Order.Ideal
Order.Ideal.IsMaximal.mk : ∀ {P : Type u_1} [inst : LE P] {I : Order.Ideal P} [toIsProper : I.IsProper],
  (∀ ⦃J : Order.Ideal P⦄, I < J → ↑J = Set.univ) → I.IsMaximal
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffWithinAt_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {s : Set E} {x : E}, ContDiffWithinAt 𝕜 n id s x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_alter_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.getKey? k = if (f (t.get? k)).isSome = true then some k else none
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.comp_hom₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y Z : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : C} (h : Z.obj₁ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom₁ h =
    CategoryTheory.CategoryStruct.comp f.hom₁ (CategoryTheory.CategoryStruct.comp g.hom₁ h)
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.equivalence_functor_map : ∀ {X Y : AddMonCat} (f : X ⟶ Y),
  AddMonCat.equivalence.functor.map f = MonCat.ofHom (AddMonoidHom.toMultiplicative (AddMonCat.Hom.hom f))
-- Aesop.RuleTac.Basic
Aesop.instInhabitedSubgoal : Inhabited Aesop.Subgoal
-- Mathlib.Algebra.DirectSum.Module
DirectSum.range_coeLinearMap : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M}, (DirectSum.coeLinearMap A).range = ⨆ i, A i
-- Lean.Environment
Lean.PersistentEnvExtensionState.mk : {α σ : Type} → Array (Array α) → σ → Lean.PersistentEnvExtensionState α σ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
eq_zero_of_add_nonneg_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : PartialOrder α] [AddRightMono α] {a b : α},
  a ≤ 0 → b ≤ 0 → 0 ≤ a + b → b = 0
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.comp_natTransLift_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G H : CategoryTheory.Functor (CategoryTheory.Quotient r) D}
  (τ : (CategoryTheory.Quotient.functor r).comp F ⟶ (CategoryTheory.Quotient.functor r).comp G)
  (τ' : (CategoryTheory.Quotient.functor r).comp G ⟶ (CategoryTheory.Quotient.functor r).comp H)
  {Z : CategoryTheory.Functor (CategoryTheory.Quotient r) D} (h : H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Quotient.natTransLift r τ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Quotient.natTransLift r τ') h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Quotient.natTransLift r (CategoryTheory.CategoryStruct.comp τ τ')) h
-- Std.Http.Protocol.H1.Error
/-- Connection closed.
 -/
Std.Http.Protocol.H1.Error.connectionClosed : Std.Http.Protocol.H1.Error
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- The morphism `⦋1⦌ ⟶ ⦋n⦌` that picks out a specified `h : i ≤ j` in `Fin (n+1)`.  -/
SimplexCategory.mkOfLe : {n : ℕ} → (i j : Fin (n + 1)) → i ≤ j → ({ len := 1 } ⟶ { len := n })
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `lowerSemiContinuous_inv_iff`. -/
UpperSemicontinuous.inv : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} [inst_1 : PartialOrder β] [inst_2 : CommGroup β]
  [IsOrderedMonoid β], UpperSemicontinuous f → LowerSemicontinuous f⁻¹
-- Mathlib.GroupTheory.Transfer
/-- The transfer transversal as a set. Contains elements of the form `g ^ k • g₀` for fixed choices
of representatives `g₀` of fixed choices of representatives `q₀` of `⟨g⟩`-orbits in `G ⧸ H`.  -/
Subgroup.transferSet : {G : Type u_1} → [inst : Group G] → Subgroup G → G → Set G
-- Init.Omega.IntList
Lean.Omega.IntList.neg_nil : -[] = []
-- Mathlib.Order.Filter.Basic
Filter.eventuallyEq_of_mem : ∀ {α : Type u} {β : Type v} {l : Filter α} {f g : α → β} {s : Set α}, s ∈ l → Set.EqOn f g s → f =ᶠ[l] g
-- Init.Data.UInt.Lemmas
USize.toNat_ofNat_of_lt : ∀ {n : ℕ}, n < USize.size → USize.toNat (OfNat.ofNat n) = n
-- Lean.Meta.Tactic.Simp.Types
/-- Executes `x` using a `MetaM` configuration for indexing terms.
It is inferred from `Simp.Config`.
For example, if the user has set `simp (config := { zeta := false })`,
`isDefEq` and `whnf` in `MetaM` should not perform `zeta` reduction.
 -/
Lean.Meta.Simp.withSimpIndexConfig : {α : Type} → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pos.skipWhile.match_1.eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (h_1 : (nextCurr : s.Pos) → motive (some nextCurr))
  (h_2 : Unit → motive none),
  (match none with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_2 ()
-- Batteries.Data.Stream
Std.Stream.drop.eq_def : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (x : ℕ),
  Std.Stream.drop s x =
    match x with
    | 0 => s
    | n.succ =>
      match Std.Stream.next? s with
      | none => s
      | some (fst, s) => Std.Stream.drop s n
-- Mathlib.Topology.Category.Compactum
/-- The type `Compactum` of Compacta, defined as algebras for the ultrafilter monad.  -/
Compactum : Type (u_1 + 1)