mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Induction
_private.Mathlib.Data.List.Induction.0.List.reverseRec.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match a :: l with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_2 a l
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.contains_eq_containsₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.contains k l = l.containsₘ k
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_subset_inter_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ⊆ t → s ∩ u ⊆ t ∩ u
-- Mathlib.CategoryTheory.Category.Preorder
/-- A functor between preorder categories is monotone.  -/
CategoryTheory.Functor.monotone : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (f : CategoryTheory.Functor X Y), Monotone f.obj
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.singleton.injEq : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (x : M i) (a : x ≠ 1) (x_1 : M i)
  (a_1 : x_1 ≠ 1), (Monoid.CoprodI.NeWord.singleton x a = Monoid.CoprodI.NeWord.singleton x_1 a_1) = (x = x_1)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two finite measures on a Borel space are equal if they agree on all left-infinite right-closed
intervals.  -/
MeasureTheory.Measure.ext_of_Iic : ∀ {α : Type u_5} [inst : TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ], (∀ (a : α), μ (Set.Iic a) = ν (Set.Iic a)) → μ = ν
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The inner product of two unit vectors is equal to the cosine of the angle between them.  -/
InnerProductGeometry.inner_eq_cos_angle_of_norm_eq_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  ‖x‖ = 1 → ‖y‖ = 1 → inner ℝ x y = Real.cos (InnerProductGeometry.angle x y)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_congr_Ioo_of_le : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ],
  a ≤ b → Set.EqOn f g (Set.Ioo a b) → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
-- Mathlib.Data.Sigma.Lex
Sigma.Lex.left : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} {i j : ι} (a : α i) (b : α j),
  r i j → Sigma.Lex r s ⟨i, a⟩ ⟨j, b⟩
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.ae_restrict_iUnion_eq : ∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [Countable ι] (s : ι → Set α),
  MeasureTheory.ae (μ.restrict (⋃ i, s i)) = ⨆ i, MeasureTheory.ae (μ.restrict (s i))
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instIsScalarTower_valuationSubring' : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁)
  [inst_5 : vK.HasExtension vL], IsScalarTower (↥vK.valuationSubring) (↥vL.valuationSubring) L
-- Mathlib.Order.Filter.IsBounded
Filter.IsCoboundedUnder.frequently_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : LinearOrder α] {f : Filter ι} [f.NeBot] {u : ι → α},
  Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) f u → ∃ a, ∃ᶠ (x : ι) in f, u x ≤ a
-- Init.Data.Float.Model.Float
/-- Converts a `Float.Model` to an `Int8`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.toInt8 : Float.Model → Int8
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- If `Module.Free R M` then `ChooseBasisIndex R M` is the `ι` which indexes the basis
`ι → M`. Note that this is defined such that this type is finite if `R` is trivial.  -/
Module.Free.ChooseBasisIndex : (R : Type u) →
  (M : Type v) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Module.Free R M] → Type v
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.completedCosZeta₀_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedCosZeta₀ (-a) s = HurwitzZeta.completedCosZeta₀ a s
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue.eq_1 : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] (u : ι → Ω → β) (τ : Ω → WithTop ι) (ω : Ω),
  MeasureTheory.stoppedValue u τ ω = u (τ ω).untopA ω
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.of_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ j₃ : J} (f₁₂ : j₁ ⟶ j₂) (f₂₃ : j₂ ⟶ j₃),
  CategoryTheory.Zigzag j₁ j₃
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Functor.toProfunctor_map_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) (X_1 : Dᵒᵖ),
  (F.toProfunctor.map f).app X_1 = TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp g (F.map f)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.toUnit_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  {R : CategoryTheory.Over X},
  CategoryTheory.Over.Hom.left (CategoryTheory.SemiCartesianMonoidalCategory.toUnit R) = R.hom
-- Mathlib.Data.Nat.Log
Nat.log.fun_cases_unfolding : ∀ (b n : ℕ) (motive : ℕ → Prop), (b ≤ 1 → motive 0) → (¬b ≤ 1 → motive (Nat.log.go n b n).2) → motive (Nat.log b n)
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.trace.injEq : ∀ (cls : Lean.Name) (msg : Std.Format) (collapsed : Bool)
  (children : Lean.Widget.StrictOrLazy (Array Std.Format) (Array Lean.MessageData)) (cls_1 : Lean.Name)
  (msg_1 : Std.Format) (collapsed_1 : Bool)
  (children_1 : Lean.Widget.StrictOrLazy (Array Std.Format) (Array Lean.MessageData)),
  (Lean.Widget.EmbedFmt.trace✝ cls msg collapsed children =
      Lean.Widget.EmbedFmt.trace✝ cls_1 msg_1 collapsed_1 children_1) =
    (cls = cls_1 ∧ msg = msg_1 ∧ collapsed = collapsed_1 ∧ children = children_1)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toArray_roc_eq_add : ∀ {m n i fallback : ℕ}, i < n - m → (m<...=n).toArray.getD i fallback = m + 1 + i
-- Plausible.Sampleable
/-- Default instance whose purpose is to simply generate values
of a type directly using the `Arbitrary` instance  -/
Plausible.SampleableExt.selfContained : {α : Type u_1} → [Repr α] → [Plausible.Shrinkable α] → [Plausible.Arbitrary α] → Plausible.SampleableExt α
-- Mathlib.SetTheory.Ordinal.Notation
NONote.instRepr : Repr NONote
-- Batteries.Lean.Meta.Basic
/-- A variant of `mkFreshId` which generates names with a particular prefix. The
generated names are unique and have the form `<prefix>.<N>` where `N` is a
natural number. They are not suitable as user-facing names.
 -/
Lean.Meta.mkFreshIdWithPrefix : {m : Type → Type} → [Monad m] → [Lean.MonadNameGenerator m] → Lean.Name → m Lean.Name
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioo_atBot_atBot : ∀ {α : Type u_1} [inst : Preorder α], Filter.TendstoIxxClass Set.Ioo Filter.atBot Filter.atBot
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.get?.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) →
    (x = Ordering.lt → motive Ordering.lt) →
      (x = Ordering.gt → motive Ordering.gt) → (x = Ordering.eq → motive Ordering.eq) → motive x
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- If `f, g` are analytic on a neighbourhood of the preconnected open set `U`, and `f * g = 0`
on `U`, then either `f = 0` on `U` or `g = 0` on `U`.  -/
AnalyticOnNhd.eq_zero_or_eq_zero_of_mul_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {A : Type u_3} [inst_1 : NormedRing A] [IsDomain A]
  [inst_3 : NormedAlgebra 𝕜 A] {f g : 𝕜 → A},
  AnalyticOnNhd 𝕜 f U →
    AnalyticOnNhd 𝕜 g U → (∀ z ∈ U, f z * g z = 0) → IsPreconnected U → (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0
-- Mathlib.Algebra.Lie.LieTheorem
LieModule.weightSpaceOfIsLieTower.eq_1 : ∀ (R : Type u_1) {L : Type u_2} {A : Type u_3} (V : Type u_4) [inst : CommRing R] [inst_1 : IsPrincipalIdealRing R]
  [inst_2 : IsDomain R] [inst_3 : CharZero R] [inst_4 : LieRing L] [inst_5 : LieAlgebra R L] [inst_6 : LieRing A]
  [inst_7 : LieAlgebra R A] [inst_8 : Bracket L A] [inst_9 : Bracket A L] [inst_10 : AddCommGroup V]
  [inst_11 : Module R V] [inst_12 : Module.Free R V] [inst_13 : Module.Finite R V] [inst_14 : LieRingModule L V]
  [inst_15 : LieModule R L V] [inst_16 : LieRingModule A V] [inst_17 : LieModule R A V] [inst_18 : IsLieTower L A V]
  [inst_19 : IsLieTower A L V] (χ : A → R),
  LieModule.weightSpaceOfIsLieTower R V χ = { toSubmodule := ↑(LieModule.weightSpace V χ), lie_mem := ⋯ }
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.topology_eq : ∀ (α : Type u_1) (D : Set (Set α)) [inst : Preorder α] [t : TopologicalSpace α] [Topology.IsScottHausdorff α D],
  t = Topology.scottHausdorff α D
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
/-- The triangle inequality is an equality if the middle vector is a nonnegative linear combination
of the other two vectors. See `angle_add_angle_eq_pi_of_angle_eq_pi` for the other equality case.  -/
InnerProductGeometry.angle_eq_angle_add_add_angle_add_of_mem_span : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y z : V},
  y ≠ 0 →
    y ∈ Submodule.span NNReal {x, z} →
      InnerProductGeometry.angle x z = InnerProductGeometry.angle x y + InnerProductGeometry.angle y z
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toContinuousAddMonoidHom_zero : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂], ↑0 = 0
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedOrderHom β γ)
  (g : BoundedOrderHom α β) (a : α), (f.comp g) a = f (g a)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractLeft_algebraMap : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (d : Module.Dual R M) (r : R),
  (CliffordAlgebra.contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r) = 0
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ)
  (X_1 : (SimplexCategory.Truncated n)ᵒᵖ),
  (CategoryTheory.SimplicialObject.Truncated.rightExtensionInclusion X n).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op (Opposite.unop X_1).obj))
-- Mathlib.Algebra.Ring.Parity
Odd.eq_1 : ∀ {α : Type u_2} [inst : Semiring α] (a : α), Odd a = ∃ k, a = 2 * k + 1
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) {X Y Z : A} (f : X ⟶ Y) (g : Y ⟶ Z) [inst_2 : ι.Full]
  [inst_3 : ι.Faithful] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  Λ.chainComplexMap (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (Λ.chainComplexMap f) (Λ.chainComplexMap g)
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_symm_sub : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [F.Additive] (X : C) (Y : D) (f f' : X ⟶ G.obj Y),
  (adj.homEquiv X Y).symm (f - f') = (adj.homEquiv X Y).symm f - (adj.homEquiv X Y).symm f'
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_star : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], (star a).imI = -a.imI
-- Mathlib.Topology.Instances.CantorSet
/-- If `x = 0.d₀d₁...` in base-3 (ternary), and none of the digits `dᵢ` is `1`,
then `x` belongs to the Cantor set.  -/
ofDigits_zero_two_sequence_mem_cantorSet : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → Real.ofDigits a ∈ cantorSet
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mul_sum : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {S : Type u_3} [inst_1 : NonUnitalNonAssocSemiring S] (b : S)
  (s : SkewMonoidAlgebra k G) {f : G → k → S}, b * s.sum f = s.sum fun a c => b * f a c
-- Mathlib.Order.Filter.Extr
isMinOn_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMinOn (⇑OrderDual.toDual ∘ f) s a ↔ IsMaxOn f s a
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoUniformly.neg : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {g : β → α}, TendstoUniformly f g l → TendstoUniformly (-f) (-g) l
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.zag_symm : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], Std.Symm CategoryTheory.Zag
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.familyOfBFamily'_enum : ∀ {α : Type u_1} {ι : Type u} (r : ι → ι → Prop) [inst : IsWellOrder ι r] {o : Ordinal.{u}} (ho : Ordinal.type r = o)
  (f : (a : Ordinal.{u}) → a < o → α) (i : Ordinal.{u}) (hi : i < o),
  Ordinal.familyOfBFamily' r ho f ((Ordinal.enum r) ⟨i, ⋯⟩) = f i hi
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.mem_nhds_bot_iff : ∀ {s : Set EReal}, s ∈ nhds ⊥ ↔ ∃ y, Set.Iio ↑y ⊆ s
-- Mathlib.Analysis.Normed.Field.UnitBall
Submonoid.unitClosedBall.eq_1 : ∀ (𝕜 : Type u_2) [inst : SeminormedRing 𝕜] [inst_1 : NormOneClass 𝕜],
  Submonoid.unitClosedBall 𝕜 = { carrier := Metric.closedBall 0 1, mul_mem' := ⋯, one_mem' := ⋯ }
-- Init.Data.String.OrderInstances
String.Pos.instToIntCoOfNatIntHAddCastUtf8ByteSize : {s : String} → Lean.Grind.ToInt s.Pos (Lean.Grind.IntInterval.co 0 (↑s.utf8ByteSize + 1))
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.prod_mono : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  ⦃s₁ s₂ : NonUnitalSubring R⦄, s₁ ≤ s₂ → ∀ ⦃t₁ t₂ : NonUnitalSubring S⦄, t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Batteries.Data.String.Legacy
/-- Auxuliary definition for `String.Legacy.revPosOf`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
String.Legacy.revPosOfAux : String → Char → String.Pos.Raw → Option String.Pos.Raw
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_le_infEDist_add_hausdorffEDist`.

---

The distance from `x` to `s` or `t` is controlled in terms of the Hausdorff distance
between `s` and `t`.  -/
EMetric.infEdist_le_infEdist_add_hausdorffEdist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
  Metric.infEDist x t ≤ Metric.infEDist x s + Metric.hausdorffEDist s t
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.whisker_right.sizeOf_spec : ∀ {B : Type u} [inst : Quiver B] [inst_1 : SizeOf B] {a b c : CategoryTheory.FreeBicategory B} {f g : a ⟶ b} (h : b ⟶ c)
  (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  sizeOf (CategoryTheory.FreeBicategory.Hom₂.whisker_right h η) =
    1 + sizeOf a + sizeOf b + sizeOf c + sizeOf f + sizeOf g + sizeOf h + sizeOf η
-- Mathlib.Algebra.Opposites
MulOpposite.instUnique : {α : Type u_1} → [Unique α] → Unique αᵐᵒᵖ
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.tensorQuotEquivQuotSMul_tmul_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (x : M) (r : R),
  (TensorProduct.tensorQuotEquivQuotSMul M I) (x ⊗ₜ[R] (Ideal.Quotient.mk I) r) = Submodule.Quotient.mk (r • x)
-- Mathlib.Analysis.PSeries
ENNReal.le_tsum_condensed : ∀ {f : ℕ → ENNReal}, (∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m) → ∑' (k : ℕ), f k ≤ f 0 + ∑' (k : ℕ), 2 ^ k * f (2 ^ k)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiff.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → ContDiff ℝ n fun x => Real.cos (f x)
-- Mathlib.Algebra.DirectSum.Algebra
/-- A family of `LinearMap`s preserving `DirectSum.GOne.one` and `DirectSum.GMul.mul`
describes an `AlgHom` on `⨁ i, A i`. This is a stronger version of `DirectSum.toSemiring`.

Of particular interest is the case when `A i` are bundled subobjects, `f` is the family of
coercions such as `Submodule.subtype (A i)`, and the `[GMonoid A]` structure originates from
`DirectSum.GMonoid.ofAddSubmodules`, in which case the proofs about `GOne` and `GMul`
can be discharged by `rfl`.  -/
DirectSum.toAlgebra : {ι : Type uι} →
  (R : Type uR) →
    (A : ι → Type uA) →
      {B : Type uB} →
        [inst : CommSemiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (A i)] →
            [inst_2 : (i : ι) → Module R (A i)] →
              [inst_3 : AddMonoid ι] →
                [inst_4 : DirectSum.GSemiring A] →
                  [inst_5 : Semiring B] →
                    [inst_6 : DirectSum.GAlgebra R A] →
                      [inst_7 : Algebra R B] →
                        [inst_8 : DecidableEq ι] →
                          (f : (i : ι) → A i →ₗ[R] B) →
                            (f 0) GradedMonoid.GOne.one = 1 →
                              (∀ {i j : ι} (ai : A i) (aj : A j),
                                  (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) →
                                (DirectSum ι fun i => A i) →ₐ[R] B
-- Mathlib.Data.Num.Lemmas
Num.cast_succ : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (n : Num), ↑n.succ = ↑n + 1
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval_eq_sum : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : SMulWithZero R S]
  [inst_3 : Monoid S] (f : LaurentPolynomial R) (x : Sˣ), f.smeval x = f.coeff.sum fun n r => r • ↑(x ^ n)
-- Mathlib.Data.Seq.Computation
Computation.Equiv.trans : ∀ {α : Type u} {s t u : Computation α}, s.Equiv t → t.Equiv u → s.Equiv u
-- Mathlib.Algebra.Group.Int.Even
Int.even_sub_one : ∀ {n : ℤ}, Even (n - 1) ↔ ¬Even n
-- Mathlib.Data.Finset.Union
Finset.map_disjiUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α ↪ β} {s : Finset α} {t : β → Finset γ}
  {h : (↑(Finset.map f s)).PairwiseDisjoint t}, (Finset.map f s).disjiUnion t h = s.disjiUnion (fun a => t (f a)) ⋯
-- Mathlib.Data.Set.NAry
/-- If `a` is a left identity for `f : α → β → β`, then `{a}` is a left identity for
`Set.image2 f`.  -/
Set.image2_left_identity : ∀ {α : Type u_1} {β : Type u_3} {f : α → β → β} {a : α}, (∀ (b : β), f a b = b) → ∀ (t : Set β), Set.image2 f {a} t = t
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instIsDomain : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R], IsDomain Rᵐᵒᵖ
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  {f : (a : α) → β a → Bool}, m.WF → (Std.DHashMap.Raw.filter f m).WF
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.forIn_eq_forIn_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap α fun x => β} [inst : Monad m'] [LawfulMonad m'] {f : α → β → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.forIn f init m = forIn (Std.DHashMap.Const.toArray m) init fun a b => f a.1 a.2 b
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.instCanLiftSetCoeForallForallForallMemForallHMul : ∀ {M : Type u_1} [inst : Mul M],
  CanLift (Set M) (Subsemigroup M) SetLike.coe fun s => ∀ {x y : M}, x ∈ s → y ∈ s → x * y ∈ s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ordered_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a b = Ordering.lt) t.keys
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.eq_symm_comp : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M₁ : Type u_8} {M₂ : Type u_9} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂}
  {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂} {α : Type u_14} (f : α → M₁) (g : α → M₂), f = ⇑e₁₂.symm ∘ g ↔ ⇑e₁₂ ∘ f = g
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If G preserves equalizers and products, it preserves all limits.  -/
CategoryTheory.Limits.preservesLimits_of_preservesEqualizers_and_products : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasEqualizers C] [CategoryTheory.Limits.HasProducts C] (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair G]
  [∀ (J : Type w), CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) G],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, w, v, v₂, u, u₂} G
-- Std.Http.Data.URI.Basic
Std.Http.URI.Authority.mk.injEq : ∀ (userInfo : Option Std.Http.URI.UserInfo) (host : Std.Http.URI.Host) (port : Std.Http.URI.Port)
  (userInfo_1 : Option Std.Http.URI.UserInfo) (host_1 : Std.Http.URI.Host) (port_1 : Std.Http.URI.Port),
  ({ userInfo := userInfo, host := host, port := port } = { userInfo := userInfo_1, host := host_1, port := port_1 }) =
    (userInfo = userInfo_1 ∧ host = host_1 ∧ port = port_1)
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.devosMulRel_iff : ∀ {α : Type u_2} [inst : Group α] [inst_1 : DecidableEq α] {x y : Finset α × Finset α},
  DevosMulRel✝ x y ↔
    (x.1 * x.2).card < (y.1 * y.2).card ∨
      (x.1 * x.2).card = (y.1 * y.2).card ∧ y.1.card + y.2.card < x.1.card + x.2.card ∨
        (x.1 * x.2).card = (y.1 * y.2).card ∧ x.1.card + x.2.card = y.1.card + y.2.card ∧ x.1.card < y.1.card
-- Lean.ScopedEnvExtension
Lean.ScopedEnvExtension.instInhabitedStateStack.default : {α β σ : Type} → Lean.ScopedEnvExtension.StateStack α β σ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_int_module : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx p = 0 → Lean.Grind.CommRing.Poly.denoteAsIntModule ctx p = 0
-- Mathlib.Order.Defs.LinearOrder
cmp_eq_compare : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), cmp a b = compare a b
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.pOpcycles_comp_opcyclesIso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : (Fin 0 → G) →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.opcyclesIso₀ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.pOpcycles (groupHomology.inhomogeneousChains A) 0)) x) =
    (Representation.Coinvariants.mk A.ρ) ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₀ A).hom) x)
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Mon.append_denote : ∀ (ctx : Nat.Internal.Linear.Context) (m₁ m₂ : Nat.Internal.SOM.Mon),
  Nat.Internal.SOM.Mon.denote ctx (m₁ ++ m₂) = Nat.Internal.SOM.Mon.denote ctx m₁ * Nat.Internal.SOM.Mon.denote ctx m₂