mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `‖r‖ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, version in a general ring with
summable geometric series. For a version in a field, using division instead of `Ring.inverse`,
see `tsum_coe_mul_geometric_of_norm_lt_one`.  -/
tsum_coe_mul_geometric_of_norm_lt_one' : ∀ {𝕜 : Type u_5} [inst : NormedDivisionRing 𝕜] {r : 𝕜}, ‖r‖ < 1 → ∑' (n : ℕ), ↑n * r ^ n = r * Ring.inverse (1 - r) ^ 2
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.id_τr : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} (α : a ⟶ b),
  (CategoryTheory.CategoryStruct.id α).τr = CategoryTheory.CategoryStruct.id α.r
-- Mathlib.Algebra.Group.Commute.Defs
/-- If `a` commutes with `b`, then `b` commutes with `a`.  -/
AddCommute.symm : ∀ {S : Type u_3} [inst : Add S] {a b : S}, AddCommute a b → AddCommute b a
-- Init.Data.Slice.Array.Iterator
SubarrayIterator : Type u → Type u
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.instMembership : {G : Type u_1} →
  {X : Type u_2} → [inst : Group G] → [inst_1 : MulAction G X] → Membership X (DiscreteTiling.Prototile G X)
-- Mathlib.Topology.Connected.Basic
isPreconnected_closed_iff : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Set α},
  IsPreconnected s ↔
    ∀ (t t' : Set α),
      IsClosed t → IsClosed t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
/-- Conditional Jensen's inequality for finite measures.  -/
_private.Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen.0.ConvexOn.map_condExp_le_of_isFiniteMeasure : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set E} [MeasureTheory.IsFiniteMeasure μ],
  m ≤ mα →
    ConvexOn ℝ s φ →
      LowerSemicontinuousOn φ s →
        (∀ᵐ (a : α) ∂μ, f a ∈ s) →
          IsClosed s →
            MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Function.locallyFinsuppWithin.logCounting.eq_1 : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E],
  Function.locallyFinsuppWithin.logCounting =
    {
      toFun := fun D r =>
        ∑ᶠ (z : E), ↑(((Function.locallyFinsuppWithin.toClosedBall r) D) z) * Real.log (r * ‖z‖⁻¹) +
          ↑(D 0) * Real.log r,
      map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.prod_target : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ),
  (e.prod e').target = e.target ×ˢ e'.target
-- Mathlib.Topology.PartialHomeomorph.Defs
PartialHomeomorph.symm_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialHomeomorph X Y),
  e.symm.toPartialEquiv = e.symm
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instIsRightCancelMul : ∀ {α : Type u_1} [inst : Mul α] [IsLeftCancelMul α], IsRightCancelMul αᵐᵒᵖ
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.d.eq_1 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c) (x : Option ι), HomologicalComplex.extend.d K none x = 0
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.IsMaximal.of_isMaximal_liesOver : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Algebra.IsIntegral A B] (P : Ideal B) (p : Ideal A) [P.LiesOver p] [P.IsMaximal], p.IsMaximal
-- Mathlib.Algebra.Star.Basic
StarRing.toStarAddMonoid : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → [StarRing R] → StarAddMonoid R
-- Init.Data.Int.Order
Int.sub_left_le_of_le_add : ∀ {a b c : ℤ}, a ≤ b + c → a - b ≤ c
-- Lean.Meta.Tactic.Grind.Types
/-- User names for theorem origins that are `.fvar`s. We need to store this information
because subgoals are created while we are solving subgoals.
 -/
Lean.Meta.Grind.Counters.fvarUserNames : Lean.Meta.Grind.Counters → Lean.PHashMap Lean.FVarId Lean.Name
-- Mathlib.FieldTheory.Fixed
FixedPoints.finrank_le_card : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G],
  Module.finrank (↥(FixedPoints.subfield G F)) F ≤ Fintype.card G
-- Mathlib.Topology.Order.LowerUpperTopology
/-- The upper topology is the topology generated by the complements of the right-closed left-infinite
intervals.
 -/
Topology.upper : (α : Type u_1) → [Preorder α] → TopologicalSpace α
-- Mathlib.Analysis.Complex.AbsMax
IsMaxOn.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder β] (f : α → β) (s : Set α) (a : α),
  IsMaxOn f s a = IsMaxFilter f (Filter.principal s) a
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.grade.gradedMonoid : ∀ {M : Type u_1} {R : Type u_3} [inst : AddMonoid M] [inst_1 : CommSemiring R],
  SetLike.GradedMonoid (AddMonoidAlgebra.grade R)
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.toThinSkeleton_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (c : C),
  (CategoryTheory.toThinSkeleton C).obj c = CategoryTheory.ThinSkeleton.mk c
-- Mathlib.RingTheory.Polynomial.HilbertPoly
Polynomial.hilbertPoly.eq_1 : ∀ {F : Type u_1} [inst : Field F] (p : Polynomial F), p.hilbertPoly 0 = 0
-- Init.Data.Range.Polymorphic.SInt
Int8.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Int8