mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- The function `exp (b * x) / x ^ s` tends to `+∞` at `+∞`, for any real `s` and `b > 0`.  -/
tendsto_exp_mul_div_rpow_atTop : ∀ (s b : ℝ), 0 < b → Filter.Tendsto (fun x => Real.exp (b * x) / x ^ s) Filter.atTop Filter.atTop
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackComp_hom_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.ChosenPullbacksAlong.pullbackComp f g).hom
        (CategoryTheory.Over.map (CategoryTheory.CategoryStruct.comp f g)))
      (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).counit =
    (CategoryTheory.ChosenPullbacksAlong.mapPullbackAdj (CategoryTheory.CategoryStruct.comp f g)).counit
-- Mathlib.Order.RelSeries
RelSeries.instCoeFunForallFinHAddNatLengthOfNat : {α : Type u_1} → (r : SetRel α α) → CoeFun (RelSeries r) fun x => Fin (x.length + 1) → α
-- Mathlib.RingTheory.IsAdjoinRoot
/-- Algebra isomorphism with `R[X]/(f)`.  -/
IsAdjoinRoot.adjoinRootAlgEquiv : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : Ring S] → {f : Polynomial R} → [inst_2 : Algebra R S] → IsAdjoinRoot S f → AdjoinRoot f ≃ₐ[R] S
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.of_map : ∀ {B : Type u} [inst : Quiver B] (x x_1 : B) (f : x ⟶ x_1),
  CategoryTheory.FreeBicategory.of.map f = CategoryTheory.FreeBicategory.Hom.of f
-- Init.Data.Stream
Std.instToStreamRange : Std.ToStream Std.Legacy.Range Std.Legacy.Range
-- Mathlib.Data.Set.Countable
Set.countable_univ_pi : ∀ {α : Type u} {π : α → Type u_1} [Finite α] {s : (a : α) → Set (π a)},
  (∀ (a : α), (s a).Countable) → (Set.univ.pi s).Countable
-- Mathlib.Order.Filter.Extr
/-- If `f` is antitone on `Icc a b` and monotone on `Ici b`, then the minimum of `f` on `Ici a` is
attained at `b`.  -/
isMinOn_Ici_of_anti_mono : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  AntitoneOn f (Set.Icc a b) → MonotoneOn f (Set.Ici b) → IsMinOn f (Set.Ici a) b
-- Mathlib.Algebra.Order.Module.Defs
/-- **Alias** of the reverse direction of `smul_pos_iff_of_neg_left`. -/
smul_pos_of_neg_of_neg : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] [PosSMulReflectLT α β], a < 0 → b < 0 → 0 < a • b
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
abs_le_abs_of_nonpos : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] {a b : α} [AddRightMono α],
  a ≤ 0 → b ≤ a → |a| ≤ |b|
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.endsWith_bool_eq_getLast? : ∀ {p : Char → Bool} {s : String.Slice}, s.endsWith p = Option.any p s.copy.toList.getLast?
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.isBasis_union : ∀ {α : Type u_1} {M : Matroid α} {I X Y : Set α}, M.IsBasis I X → M.IsBasis I Y → M.IsBasis I (X ∪ Y)
-- Mathlib.Order.Filter.Tendsto
Filter.comap_eq_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {φ : α → β} (ψ : β → α),
  ψ ∘ φ = id → Filter.Tendsto φ f g → Filter.Tendsto ψ g f → Filter.comap φ g = f
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findM?.eq_2 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type} (p : α → m Bool) (a : α) (as : List α),
  List.findM? p (a :: as) = do
    let __do_lift ← p a
    match __do_lift with
      | true => pure (some a)
      | false => List.findM? p as
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- A version of `yonedaEquiv` for `uliftYoneda`.  -/
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : J.Subcanonical] →
        {X : C} →
          {F : CategoryTheory.Sheaf J (Type (max v v'))} →
            ((CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) ≃ F.obj.obj (Opposite.op X)
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- `X` is the colimit of its affine opens.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.isColimitCocone : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Limits.IsColimit (AlgebraicGeometry.Scheme.AffineZariskiSite.cocone X)
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.mkContext : optParam Lean.Meta.Simp.Config { } →
  optParam Lean.Meta.SimpTheoremsArray ∅ →
    optParam Lean.Meta.SimpCongrTheorems { } → optParam Lean.Options ∅ → Lean.MetaM Lean.Meta.Simp.Context
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalFirst : Lean.Elab.Tactic.Tactic
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_eq_of_add_eq : ∀ {a b c : Ordinal.{u_4}}, a + b = c → c - a = b
-- Std.Internal.Do.PredTrans
/-- Chain-complete partial order on predicate transformers, for fixed-point reasoning.  -/
Std.Internal.Do.instCCPOPredTrans : {Pred : Type u_1} →
  {EPred : Type u_2} →
    {α : Type u_3} → [Lean.Order.CCPO Pred] → Lean.Order.CCPO (Std.Internal.Do.PredTrans Pred EPred α)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.injective : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  Function.Injective ⇑e
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.locallyLipschitz : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} [FiniteDimensional ℝ E],
  ConvexOn ℝ Set.univ f → LocallyLipschitz f
-- Std.Time.Zoned.ZoneRules
/-- Creates ZoneRules with a fixed GMT offset.
 -/
Std.Time.TimeZone.ZoneRules.fixedOffsetZone : Std.Time.Second.Offset → optParam (Option String) none → optParam (Option String) none → Std.Time.TimeZone.ZoneRules
-- Mathlib.Order.Filter.Tendsto
/-- If two filters are disjoint, then a function cannot tend to both of them along a non-trivial
filter.  -/
Filter.Tendsto.not_tendsto : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {a : Filter α} {b₁ b₂ : Filter β},
  Filter.Tendsto f a b₁ → ∀ [a.NeBot], Disjoint b₁ b₂ → ¬Filter.Tendsto f a b₂
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} (self : P.LeftHomotopy f g) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.i₀ (CategoryTheory.CategoryStruct.comp self.h h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Data.Multiset.Defs
Multiset.quot_mk_to_coe : ∀ {α : Type u_1} (l : List α), ⟦l⟧ = ↑l
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
lineDerivWithin_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f f₁ : E → F} {s : Set E}
  {x v : E}, Set.EqOn f₁ f s → f₁ x = f x → lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v
-- Mathlib.Data.Set.Subset
Set.image_val_union_self_left_eq : ∀ {α : Type u_2} {A : Set α} {D : Set ↑A}, Subtype.val '' D ∪ A = A
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inr_comp_inl_comp_associator_assoc : ∀ (x y z : AugmentedSimplexCategory) {Z : AugmentedSimplexCategory}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj x (CategoryTheory.MonoidalCategoryStruct.tensorObj y z) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (x.inr y)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom h)) =
    CategoryTheory.CategoryStruct.comp (y.inl z)
      (CategoryTheory.CategoryStruct.comp (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)) h)
-- Mathlib.Analysis.Calculus.Taylor
hasDerivWithinAt_taylor_coeff_within : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {x y : ℝ} {k : ℕ} {s t : Set ℝ},
  UniqueDiffWithinAt ℝ t y →
    s ∈ nhdsWithin y t →
      DifferentiableWithinAt ℝ (iteratedDerivWithin (k + 1) f s) s y →
        HasDerivWithinAt
          (fun z => (((↑k + 1) * ↑k.factorial)⁻¹ * (x - z) ^ (k + 1)) • iteratedDerivWithin (k + 1) f s z)
          ((((↑k + 1) * ↑k.factorial)⁻¹ * (x - y) ^ (k + 1)) • iteratedDerivWithin (k + 2) f s y -
            ((↑k.factorial)⁻¹ * (x - y) ^ k) • iteratedDerivWithin (k + 1) f s y)
          t y
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- If `X` is compactly generated, to prove that `f : X → Y` is continuous it is enough to show
that for every compact Hausdorff space `K` and every continuous map `g : K → X`,
`f ∘ g` is continuous.  -/
continuous_from_uCompactlyGeneratedSpace : ∀ {X : Type w} {Y : Type x} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] [UCompactlyGeneratedSpace X]
  (f : X → Y), (∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)) → Continuous f
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPullback_pushforward_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (R : CategoryTheory.Sieve (F.obj X)),
  CategoryTheory.Sieve.functorPushforward F (CategoryTheory.Sieve.functorPullback F R) ≤ R
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.Kernel.HasSubgaussianMGF.zero_kernel : ∀ {Ω : Type u_1} {Ω' : Type u_2} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω'} {ν : MeasureTheory.Measure Ω'}
  {X : Ω → ℝ} {c : NNReal}, ProbabilityTheory.Kernel.HasSubgaussianMGF X c 0 ν
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_sdiff_singleton_add_one`. -/
Set.ncard_diff_singleton_add_one : ∀ {α : Type u_1} {s : Set α} {a : α},
  a ∈ s → autoParam s.Finite Set.ncard_sdiff_singleton_add_one._auto_1 → (s \ {a}).ncard + 1 = s.ncard
-- Mathlib.CategoryTheory.Preadditive.FunctorCategory
CategoryTheory.NatTrans.app_add : ∀ {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] [inst_2 : CategoryTheory.Preadditive D]
  {F G : CategoryTheory.Functor C D} (X : C) (α β : F ⟶ G), (α + β).app X = α.app X + β.app X
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.CompStruct.d₀ : ∀ {X : SSet.Truncated 2}
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (self : e₀₁.CompStruct e₁₂ e₀₂),
  (CategoryTheory.ConcreteCategory.hom
        (X.map
          (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_2 SSet.Truncated.Edge.CompStruct._proof_2).op))
      self.simplex =
    e₁₂.edge
-- Mathlib.LinearAlgebra.RootSystem.OfBilinear
LinearMap.IsReflective.coroot_apply_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : M →ₗ[R] M →ₗ[R] R) {x : M} (hx : B.IsReflective x), (LinearMap.IsReflective.coroot B hx) x = 2
-- Std.Sat.AIG.Basic
Std.Sat.AIG.BinaryInput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} [inst_2 : SizeOf α] (lhs rhs : aig.Ref),
  sizeOf { lhs := lhs, rhs := rhs } = 1 + sizeOf lhs + sizeOf rhs
-- Mathlib.Analysis.Normed.Group.Constructions
OrderDual.normedAddGroup : {E : Type u_2} → [NormedAddGroup E] → NormedAddGroup Eᵒᵈ
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- Differences whose minuends differ by a common summand can be proven equal if
those summands expand to equal elements of `R`.  -/
AddOreLocalization.eq_of_num_factor_eq : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {r r' r₁ r₂ : R}
  {s t : ↥S}, ↑t + r = ↑t + r' → r₁ + r + r₂ -ₒ s = r₁ + r' + r₂ -ₒ s
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.UniquePartitionOne : Unique (Nat.Partition 1)
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.flip_toLinearMap : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  P.flip.toLinearMap = P.flip
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformContinuous_proj : ∀ {ι : Type u_1} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (i : ι), UniformContinuous fun a => a i
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.mk.inj : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  {tiles tiles_1 : ιₚ → DiscreteTiling.Prototile G X}, { tiles := tiles } = { tiles := tiles_1 } → tiles = tiles_1
-- Mathlib.Algebra.Category.BialgCat.Monoidal
BialgCat.instMonoidalCategoryStruct : (R : Type u) → [inst : CommRing R] → CategoryTheory.MonoidalCategoryStruct (BialgCat R)
-- Mathlib.RingTheory.Flat.Basic
/-- `M` is flat if and only if `𝟙 M ⊗ f` is injective whenever `f` is an injective linear map.
See `Module.Flat.iff_lTensor_preserves_injective_linearMap` to specialize the universe of
`N, N', N''` to `Type (max u v)`.  -/
Module.Flat.iff_lTensor_preserves_injective_linearMap' : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Small.{v', u} R],
  Module.Flat R M ↔
    ∀ ⦃N N' : Type v'⦄ [inst_4 : AddCommGroup N] [inst_5 : AddCommGroup N'] [inst_6 : Module R N] [inst_7 : Module R N']
      (f : N →ₗ[R] N'), Function.Injective ⇑f → Function.Injective ⇑(LinearMap.lTensor M f)
-- Mathlib.Logic.Denumerable
/-- If `α` and `β` are denumerable, then so is their product.  -/
Denumerable.prod : {α : Type u_1} → {β : Type u_2} → [Denumerable α] → [Denumerable β] → Denumerable (α × β)
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso_inv_app_left : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange] (X_1 : P.Over Q Y),
  ((CategoryTheory.MorphismProperty.Over.pullbackCompForgetIso f).inv.app X_1).left =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.pullback X_1.hom f)
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} {φ₁ : K₁ ⟶ L₁}
  {φ₂ : K₂ ⟶ L₂} {a : K₁ ⟶ K₂} {b : L₁ ⟶ L₂}
  (H : Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂)),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.mapOfHomotopy H)
      (CochainComplex.mappingCone.triangle φ₂).mor₃ =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ₁).mor₃
      ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a)
-- Mathlib.Data.Set.MemPartition
memPartitionSet.eq_1 : ∀ {α : Type u_1} (f : ℕ → Set α), memPartitionSet f 0 = fun x => Set.univ
-- Mathlib.Algebra.Azumaya.Basic
IsAzumaya.AlgHom.mulLeftRight_bij : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] [h : IsAzumaya R A],
  Function.Bijective ⇑(AlgHom.mulLeftRight R A)
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] {φ : S₁ ⟶ S₂}
  {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
  (γ : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁ h₂),
  CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.IsIso γ.φH
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.ext'_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Comonad C} {f g : T₁ ⟶ T₂},
  f = g ↔ f.app = g.app
-- Init.Data.Array.MapIdx
Array.getElem?_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} {i : ℕ},
  (xs.mapFinIdx f)[i]? = xs[i]?.pbind fun b h => some (f i b ⋯)
-- Mathlib.Analysis.Normed.Group.Completeness
/-- A normed additive group is complete if any absolutely convergent series converges in the
space.  -/
NormedAddCommGroup.completeSpace_of_summable_imp_tendsto : ∀ {E : Type u_1} [inst : NormedAddCommGroup E],
  (∀ (u : ℕ → E),
      (Summable fun x => ‖u x‖) → ∃ a, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, u i) Filter.atTop (nhds a)) →
    CompleteSpace E
-- Mathlib.Analysis.Calculus.FDeriv.Mul
hasStrictFDerivAt_finsetProd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {ι : Type u_5} {𝔸' : Type u_7} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} [inst_3 : DecidableEq ι] [Finite ι] {x : ι → 𝔸'},
  HasStrictFDerivAt (fun x => ∏ i ∈ u, x i) (∑ i ∈ u, (∏ j ∈ u.erase i, x j) • ContinuousLinearMap.proj i) x
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.trivial_comon_counit : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Init.Data.List.Erase
List.erase_cons_tail : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {l : List α}, ¬(b == a) = true → (b :: l).erase a = b :: l.erase a
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.tanh_arcosh : ∀ {x : ℝ}, 1 ≤ x → Real.tanh (Real.arcosh x) = √(x ^ 2 - 1) / x
-- Mathlib.Data.Set.Finite.Lattice
Directed.exists_mem_subset_of_finset_subset_biUnion : ∀ {α : Type u_1} {ι : Type u_2} [Nonempty ι] {f : ι → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) f → ∀ {s : Finset α}, ↑s ⊆ ⋃ i, f i → ∃ i, ↑s ⊆ f i
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.instIsSMulApplyℝ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {α : Type u_1} [inst : SMul α ℝ] [inst_1 : SMul α ℂ]
  [inst_2 : IsScalarTower α ℝ ℂ], IsSMulApply α (ModularForm Γ k) UpperHalfPlane ℂ
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.snd_decompLinearEquiv : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) (W : Type u_4) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : IsTopologicalAddGroup W]
  (f : V →ᴬ[R] W), ((ContinuousAffineMap.decompLinearEquiv R S V W) f).2 = f.contLinear
-- Mathlib.RingTheory.WittVector.Basic
WittVector.mapFun.injective : ∀ {p : ℕ} {α : Type u_3} {β : Type u_4} (f : α → β), Function.Injective f → Function.Injective (WittVector.mapFun f)
-- Mathlib.Algebra.Group.Int.Defs
zsmul_int_one : ∀ (n : ℤ), n • 1 = n
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (x : CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n),
  R.extEquivCohomologyClass.symm (-x) = -R.extEquivCohomologyClass.symm x
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContinuousLinearEquiv_mk' : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {e : V ≃L[R] W}
  (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e), (ContRepresentation.Equiv.mk e he).toContinuousLinearEquiv = e
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
Localization.awayLift.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (f f_1 : R →+* P) (e_f : f = f_1)
  (r : R) (hr : IsUnit (f r)), Localization.awayLift f r hr = Localization.awayLift f_1 r ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α], Finset.inv = { inv := Finset.image Inv.inv }
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom : @AlgebraicGeometry.IsFinite = @AlgebraicGeometry.IsProper ⊓ @AlgebraicGeometry.IsAffineHom
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRat_base_case : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n)
  (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  have insertRat_res := f.insertRatUnits units;
  f.ClearInsertInductionMotive ⋯ insertRat_res.1.ratUnits 0 insertRat_res.1.assignments
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_basisFun : ∀ {R₁ : Type u_1} [inst : CommSemiring R₁] {n : Type u_5} [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  LinearMap.BilinForm.toMatrix (Pi.basisFun R₁ n) = LinearMap.BilinForm.toMatrix'
-- Init.Data.Vector.Lex
Vector.lex_eq_true_iff_lt : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] [LawfulBEq α] [inst_2 : LT α] [inst_3 : DecidableLT α] {xs ys : Vector α n},
  (xs.lex ys fun x1 x2 => decide (x1 < x2)) = true ↔ xs < ys
-- Mathlib.Data.Seq.Basic
/-- The statement of `lt_length_iff'` does not assume that the sequence terminates. For a
simpler statement of the theorem where the sequence is known to terminate see `lt_length_iff`.  -/
Stream'.Seq.lt_length_iff' : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ}, (∀ (h : s.Terminates), n < s.length h) ↔ ∃ a, a ∈ s.get? n
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instBEqOrigin.beq : Mathlib.Meta.FunProp.Origin → Mathlib.Meta.FunProp.Origin → Bool
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.coprime_iff_inf_one : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a b : α},
  a ≠ 0 → b ≠ 0 → (Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoCechNerve_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (X : SimplexCategoryᵒᵖ), (U.cechIsoCechNerve hT).inv.app X = (U.cechIsoCechNerveApp hT X).inv
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- The trivial case if `X` is initial.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (X : C) (h : CategoryTheory.Limits.IsInitial X),
  ∃ ι f g x, (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.ind : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Prop},
  (∀ (y : M × ↥S), p (Localization.mk y.1 y.2)) → ∀ (x : Localization S), p x
-- Mathlib.Data.Matrix.Basic
Matrix.scalar.eq_1 : ∀ {α : Type u_11} [inst : Semiring α] (n : Type u) [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.scalar n = (Matrix.diagonalRingHom n α).comp (Pi.constRingHom n α)