mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_two : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  (CategoryTheory.ComposableArrows.fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 2 = f₃
-- Mathlib.Algebra.GroupWithZero.Associated
associated_of_dvd_dvd : ∀ {M : Type u_1} [inst : MonoidWithZero M] [IsLeftCancelMulZero M] {a b : M}, a ∣ b → b ∣ a → Associated a b
-- Lean.Meta.IndPredBelow
/-- The minor premises (fvars)  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.Context.minors : Lean.Meta.IndPredBelow.Context✝ → Array Lean.Expr
-- Init.System.IO
instMonadAttachBaseIO : MonadAttach BaseIO
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.Hom.mk.injEq : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {x y : CategoryTheory.Limits.CategoricalPullback F G} (fst : x.fst ⟶ y.fst) (snd : x.snd ⟶ y.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map fst) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map snd))
      CategoryTheory.Limits.CategoricalPullback.Hom.w._autoParam)
  (fst_1 : x.fst ⟶ y.fst) (snd_1 : x.snd ⟶ y.snd)
  (w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map fst_1) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (G.map snd_1))
      CategoryTheory.Limits.CategoricalPullback.Hom.w._autoParam),
  ({ fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := w_1 }) = (fst = fst_1 ∧ snd = snd_1)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMul_zero : ∀ (R : Type u_1) {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] (A : Matrix l m α), Matrix.kroneckerMap (TensorProduct.tmul R) A 0 = 0
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_3),
  (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₃ = X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.GroupTheory.Sylow
/-- Sylow subgroups are isomorphic  -/
Sylow.equivSMul : {p : ℕ} → {G : Type u_1} → [inst : Group G] → (P : Sylow p G) → (g : G) → ↥↑P ≃* ↥↑(g • P)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.restr_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ) (s : Set α),
  (e.restr s).trans e' = (e.trans e').restr s
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_lt_mul_inv_iff' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c d : α},
  a * b⁻¹ < c * d⁻¹ ↔ a * d < c * b
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonUnitalNonAssocSemiring` instance along a surjective function.
See note [reducible non-instances].  -/
Function.Surjective.nonUnitalNonAssocSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NonUnitalNonAssocSemiring R] →
                  f 0 = 0 →
                    (∀ (x y : R), f (x + y) = f x + f y) →
                      (∀ (x y : R), f (x * y) = f x * f y) →
                        (∀ (n : ℕ) (x : R), f (n • x) = n • f x) → NonUnitalNonAssocSemiring S
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.le_inv_mul_iff`. -/
Units.le_inv_mul_of_mul_le : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a b : M}, ↑u * a ≤ b → a ≤ ↑u⁻¹ * b
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeAction.toJson : Lean.Lsp.CodeAction → Lean.Json
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The functor `ComposableArrows C (n + 1) ⥤ ComposableArrows C n` which forgets
the first arrow.  -/
CategoryTheory.ComposableArrows.δ₀Functor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} → CategoryTheory.Functor (CategoryTheory.ComposableArrows C (n + 1)) (CategoryTheory.ComposableArrows C n)
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.mem_support_ofSubtype : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {p : α → Prop} [inst_2 : DecidablePred p] (x : α)
  (u : Equiv.Perm (Subtype p)), x ∈ (Equiv.Perm.ofSubtype u).support ↔ ∃ (hx : p x), ⟨x, hx⟩ ∈ u.support
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_codRestrict : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₂₁ : R₂ →+* R}
  [inst_6 : RingHomSurjective τ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c ∈ p),
  (LinearMap.codRestrict p f hf).range = Submodule.comap p.subtype f.range
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.tan_eq_inv_of_two_nsmul_add_two_nsmul_eq_pi : ∀ {θ ψ : Real.Angle}, 2 • θ + 2 • ψ = ↑Real.pi → ψ.tan = θ.tan⁻¹
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.top_coe_div : ∀ {K : Type u} [inst : Field K] (x y : ↥⊤), ↑(x / y) = ↑x / ↑y
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
/-- The collection of all single functors `C ⥤ CochainComplex C ℤ` along with
their compatibilities with shifts. (This definition has purposely no `simps`
attribute, as the generated lemmas would not be very useful.)  -/
CochainComplex.singleFunctors : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasZeroObject C] → CategoryTheory.SingleFunctors C (CochainComplex C ℤ) ℤ
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.toAffineEquiv_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂), e.symm.toAffineEquiv = e.symm
-- Mathlib.Topology.Homeomorph.Quotient
/-- A homeomorphism `e : X ≃ₜ Y` generates a homeomorphism between quotient spaces,
if `rX x₁ x₂ ↔ rY (e x₁) (e x₂)`.  -/
Homeomorph.Quot.congr : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {rX : X → X → Prop} →
          {rY : Y → Y → Prop} → (e : X ≃ₜ Y) → (∀ (x₁ x₂ : X), rX x₁ x₂ ↔ rY (e x₁) (e x₂)) → Quot rX ≃ₜ Quot rY
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.implicitFunction_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (φ : ImplicitFunctionData 𝕜 E F G) {x : F} {y : G},
  φ.implicitFunction x y = ↑φ.toOpenPartialHomeomorph.symm (x, y)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.lift_comp_zero_right_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddMonObj B] (f : A ⟶ B)
  (g : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f
        (CategoryTheory.CategoryStruct.comp g CategoryTheory.AddMonObj.zero))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Data.Multiset.UnionInter
Multiset.mem_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} {a : α}, a ∈ s ∩ t ↔ a ∈ s ∧ a ∈ t
-- Mathlib.Analysis.Calculus.FDeriv.OfCompLeft
HasStrictFDerivAt.of_comp_of_isEmbedding : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : E → F} {f : F → G} {h : E → G} {g' : E →L[𝕜] F}
  {f' : F →L[𝕜] G} {a : E},
  ContinuousAt g a →
    HasStrictFDerivAt f f' (g a) →
      Topology.IsEmbedding ⇑f' → HasStrictFDerivAt h (f' ∘SL g') a → f ∘ g =ᶠ[nhds a] h → HasStrictFDerivAt g g' a
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instEmptyCollection : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → EmptyCollection (Std.TreeMap.Raw α β cmp)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.mk : {α : Type} → Std.Mutex (Std.CloseableChannel.Zero.State✝ α) → Std.CloseableChannel.Zero✝ α
-- Mathlib.Algebra.Category.CommBialgCat
_private.Mathlib.Algebra.Category.CommBialgCat.0.CommBialgCat.mk.injEq : ∀ {R : Type u} [inst : CommRing R] (carrier : Type v) [commRing : CommRing carrier] [bialgebra : Bialgebra R carrier]
  (carrier_1 : Type v) (commRing_1 : CommRing carrier_1) (bialgebra_1 : Bialgebra R carrier_1),
  ({ carrier := carrier, commRing := commRing, bialgebra := bialgebra } =
      { carrier := carrier_1, commRing := commRing_1, bialgebra := bialgebra_1 }) =
    (carrier = carrier_1 ∧ commRing ≍ commRing_1 ∧ bialgebra ≍ bialgebra_1)
-- Mathlib.Order.Interval.Set.Disjoint
IsLUB.biUnion_Iic_eq_Iic : ∀ {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α}, IsLUB s a → a ∈ s → ⋃ x ∈ s, Set.Iic x = Set.Iic a
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.instIsAddCommutative_iSup : ∀ {G : Type u_1} [inst : AddGroup G] {ι : Type u_2} [Nonempty ι] [inst_2 : Preorder ι] [IsDirectedOrder ι]
  {S : ι →o AddSubgroup G} [hS : ∀ (i : ι), IsAddCommutative ↥(S i)], IsAddCommutative ↥(⨆ i, S i)
-- Init.Data.List.Attach
List.reverse_attachWith : ∀ {α : Type u_1} {P : α → Prop} {xs : List α} {H : ∀ a ∈ xs, P a},
  (xs.attachWith P H).reverse = xs.reverse.attachWith P ⋯
-- Mathlib.CategoryTheory.SmallRepresentatives
/-- The family of all categories such that the types of objects and
morphisms are subtypes of a given type `Ω`.  -/
CategoryTheory.SmallCategoryOfSet.categoryFamily : (Ω : Type w) → CategoryTheory.SmallCategoryOfSet Ω → Type w
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- A version of submodularity applied to the complements of two insertions.  -/
Matroid.eRk_compl_insert_union_add_eRk_compl_insert_inter_le : ∀ {α : Type u_1} {e : α} (M : Matroid α) (X Y : Set α),
  M.eRk (M.E \ insert e (X ∪ Y)) + M.eRk (M.E \ insert e (X ∩ Y)) ≤ M.eRk (M.E \ insert e X) + M.eRk (M.E \ insert e Y)
-- Mathlib.Order.Irreducible
/-- **Alias** of the reverse direction of `infPrime_ofDual`. -/
SupPrime.ofDual : ∀ {α : Type u_2} [inst : SemilatticeInf α] {a : αᵒᵈ}, SupPrime a → InfPrime (OrderDual.ofDual a)
-- Mathlib.Topology.Perfect
/-- The **Cantor-Bendixson Theorem**: Any closed subset of a second countable space
can be written as the union of a countable set and a perfect set.  -/
exists_countable_union_perfect_of_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {C : Set α} [SecondCountableTopology α],
  IsClosed C → ∃ V D, V.Countable ∧ Perfect D ∧ C = V ∪ D
-- Mathlib.Data.Fintype.Sets
Set.toFinset_ssubset : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s] {t : Finset α}, s.toFinset ⊂ t ↔ s ⊂ ↑t
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.AffineTargetMorphismProperty.toProperty_apply : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y)
  [i : AlgebraicGeometry.IsAffine Y], P.toProperty f ↔ P f
-- Init.Data.Order.Ord
Std.OrientedOrd.opposite : ∀ {α : Type u} [inst : Ord α] [Std.OrientedOrd α], Std.OrientedOrd α
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.instToJsonCancelParams.toJson : Lean.Lsp.CancelParams → Lean.Json
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.rightDual_leftDual : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  [inst_2 : CategoryTheory.HasLeftDual X], (ᘁX)ᘁ = X
-- Mathlib.Computability.Language
Symbol.nonterminal.inj : ∀ {T : Type u_4} {N : Type u_5} {n n_1 : N}, Symbol.nonterminal n = Symbol.nonterminal n_1 → n = n_1
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.instIsSFiniteKernelCarrierHom : ∀ {X Y : SFinKer} {κ : X.Hom Y}, ProbabilityTheory.IsSFiniteKernel κ.hom
-- Init.Data.UInt.Lemmas
USize.ofNat_mod_size : ∀ {x : ℕ}, USize.ofNat (x % 2 ^ System.Platform.numBits) = USize.ofNat x
-- Mathlib.Control.Bifunctor
Bifunctor.fst_id : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α : Type u₀} {β : Type u₁},
  Bifunctor.fst id = id
-- Mathlib.Algebra.Group.ULift
MulEquiv.ulift.eq_1 : ∀ {α : Type u} [inst : Mul α], MulEquiv.ulift = { toEquiv := Equiv.ulift, map_mul' := ⋯ }
-- Mathlib.Logic.Unique
Unique.mk.sizeOf_spec : ∀ {α : Sort u} [inst : SizeOf α] (toInhabited : Inhabited α) (uniq : ∀ (a : α), a = default),
  sizeOf { toInhabited := toInhabited, uniq := uniq } = 1 + sizeOf toInhabited
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.dickson_one_one_eq_chebyshev_C : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ), Polynomial.dickson 1 1 n = Polynomial.Chebyshev.C R ↑n
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- **Alias** of the forward direction of `ContinuousLinearMapWOT.continuousWithinAt_iff`. -/
ContinuousLinearMapWOT.continuousWithinAt_inner_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α} {a : α},
  ContinuousWithinAt f s a → ∀ (x : E) (y : F), ContinuousWithinAt (fun x_1 => inner 𝕜 y ((f x_1) x)) s a
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.labelledCopyCount_of_isEmpty : ∀ {V : Type u_1} {W : Type u_2} [inst : Fintype V] [inst_1 : Fintype W] [IsEmpty W] (G : SimpleGraph V)
  (H : SimpleGraph W), G.labelledCopyCount H = 1
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
limsup_add_le : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommGroup α] [inst_1 : ConditionallyCompleteLinearOrder α] [DenselyOrdered α]
  [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f u) limsup_add_le._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) limsup_add_le._auto_3 →
      autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) limsup_add_le._auto_5 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) limsup_add_le._auto_7 →
          Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
-- Init.Data.SInt.Lemmas
Int16.toBitVec_ofInt : ∀ (i : ℤ), (Int16.ofInt i).toBitVec = BitVec.ofInt 16 i
-- Lean.Data.PersistentArray
Lean.instInhabitedPersistentArray : {a : Type u_1} → Inhabited (Lean.PersistentArray a)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMapIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  (CategoryTheory.ShortComplex.rightHomologyMapIso e).hom = CategoryTheory.ShortComplex.rightHomologyMap e.hom
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.ext_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] {f g : M ≃* N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
WeierstrassCurve.j.congr_simp : ∀ {R : Type u} [inst : CommRing R] (W W_1 : WeierstrassCurve R) (e_W : W = W_1) [inst_1 : W.IsElliptic], W.j = W_1.j
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The `vectorSpan` of an indexed family is the span of the pairwise subtractions with a given
point on the right.  -/
vectorSpan_range_eq_span_range_vsub_right : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} (p : ι → P) (i0 : ι),
  vectorSpan k (Set.range p) = Submodule.span k (Set.range fun i => p i -ᵥ p i0)
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The inclusion
`X₁ i₁ ⊗ X₂ i₂ ⊗ X₃ i₃ ⊗ X₄ i₄ ⟶ tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j`
when `i₁ + i₂ + i₃ + i₄ = j`.  -/
CategoryTheory.GradedObject.Monoidal.ιTensorObj₄ : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C) →
            [inst_3 : X₃.HasTensor X₄] →
              [inst_4 : X₂.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄)] →
                [inst_5 :
                    X₁.HasTensor
                      (CategoryTheory.GradedObject.Monoidal.tensorObj X₂
                        (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))] →
                  (i₁ i₂ i₃ i₄ j : I) →
                    i₁ + i₂ + i₃ + i₄ = j →
                      (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₁ i₁)
                          (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₂ i₂)
                            (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₃ i₃) (X₄ i₄))) ⟶
                        CategoryTheory.GradedObject.Monoidal.tensorObj X₁
                          (CategoryTheory.GradedObject.Monoidal.tensorObj X₂
                            (CategoryTheory.GradedObject.Monoidal.tensorObj X₃ X₄))
                          j)
-- Mathlib.Algebra.Category.Ring.Topology
/-- The topology on `Hom(A, R)` for a topological ring `R`, given by the coarsest topology that
makes `f ↦ f x` continuous for all `x : A` (see `continuous_apply`).
Alternatively, given a presentation `A = ℤ[xᵢ]/I`,
this is the subspace topology `Hom(A, R) ↪ Hom(ℤ[xᵢ], R) = Rᶥ` (see `mvPolynomialHomeomorph`).

This is a scoped instance in `CommRingCat.HomTopology`.
 -/
CommRingCat.HomTopology.instTopologicalSpaceHom : {R A : CommRingCat} → [TopologicalSpace ↑R] → TopologicalSpace (A ⟶ R)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.carg : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℂ}, Measurable f → Measurable fun x => (f x).arg
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.ringInverse_equiv : ∀ {R : Type u_1} {M : Type u_2} [inst : TopologicalSpace M] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (e : M ≃L[R] M), Ring.inverse ↑e = (↑e).inverse
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SL2.commutator_eq_top : ∀ {F : Type u_1} [inst : Field F] {a : F}, a ≠ 0 → a ^ 2 ≠ 1 → commutator (Matrix.SpecialLinearGroup (Fin 2) F) = ⊤
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.le_one_mul_atBot : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f g : α → M},
  (∀ (x : α), f x ≤ 1) → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.finset.inj : ∀ {s s_1 : Lean.Term}, BigOperators.FinsetResult.finset✝ s = BigOperators.FinsetResult.finset✝ s_1 → s = s_1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKey_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {hk : k ∈ t₁} (h : t₁.Equiv t₂), t₁.getKey k hk = t₂.getKey k ⋯
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.sqTo_right : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : C₁.Hom C₂) (j : ι), CategoryTheory.Arrow.Hom.right (f.sqTo j) = f.f j
-- Mathlib.Geometry.Diffeology.Basic
/-- Version of `generateFrom_le_iff_subset_toPlots` that is stated in terms of `IsPlot` instead
of `toPlots`.  -/
DiffeologicalSpace.generateFrom_le_iff : ∀ {X : Type u_1} {g : Set ((n : ℕ) × (EuclideanSpace ℝ (Fin n) → X))} {d : DiffeologicalSpace X},
  DiffeologicalSpace.generateFrom g ≤ d ↔ ∀ (n : ℕ) (p : EuclideanSpace ℝ (Fin n) → X), ⟨n, p⟩ ∈ g → Diffeology.IsPlot p
-- Lean.Elab.Quotation.Util
Lean.Elab.Term.Quotation.hygiene : Lean.Option Bool
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- The associator isomorphism for graded objects.  -/
CategoryTheory.GradedObject.Monoidal.associator : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) →
            [inst_3 : X₁.HasTensor X₂] →
              [inst_4 : (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂).HasTensor X₃] →
                [inst_5 : X₂.HasTensor X₃] →
                  [inst_6 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] →
                    [X₁.HasGoodTensor₁₂Tensor X₂ X₃] →
                      [X₁.HasGoodTensorTensor₂₃ X₂ X₃] →
                        CategoryTheory.GradedObject.Monoidal.tensorObj
                            (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂) X₃ ≅
                          CategoryTheory.GradedObject.Monoidal.tensorObj X₁
                            (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.sub_left_cancel' : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} (c : G), c - a ≡ c - b [PMOD p] → a ≡ b [PMOD p]
-- Mathlib.Topology.Algebra.InfiniteSum.Real
summable_partition : ∀ {α : Type u_3} {β : Type u_4} {f : β → ℝ},
  0 ≤ f →
    ∀ {s : α → Set β},
      (∀ (i : β), ∃! j, i ∈ s j) →
        (Summable f ↔ (∀ (j : α), Summable fun i => f ↑i) ∧ Summable fun j => ∑' (i : ↑(s j)), f ↑i)
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F],
  UniqueDiffWithinAt 𝕜 s x →
    DifferentiableWithinAt 𝕜 f s x → ∀ (c : R), fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x