mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.LiminfLimsup
/-- Given an indexed family of sets `s j` and a function `f`, then `limsupReparam j` is equal
to `j` if `f` is bounded above on `s j`, and otherwise to some index `k` such that `f` is bounded
above on `s k` (if there exists one). To ensure good measurability behavior, this index `k` is
chosen as the minimal suitable index. This function is used to write down a limsup in a measurable
way, in `Filter.HasBasis.limsup_eq_ciInf_ciSup` and `Filter.HasBasis.limsup_eq_ite`.  -/
Filter.limsupReparam : {α : Type u_1} →
  {ι : Type u_4} →
    {ι' : Type u_5} →
      [ConditionallyCompleteLinearOrder α] →
        (ι → α) →
          (ι' → Set ι) → (p : ι' → Prop) → [Countable (Subtype p)] → [Nonempty (Subtype p)] → Subtype p → Subtype p
-- Mathlib.Order.Closure
ClosureOperator.IsClosed.closure_le_iff : ∀ {α : Type u_1} [inst : Preorder α] {c : ClosureOperator α} {x y : α}, c.IsClosed y → (c x ≤ y ↔ x ≤ y)
-- Mathlib.Topology.Coherent
Topology.IsCoherentWith.of_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)},
  (∀ (t : Set X), (∀ s ∈ S, IsClosed (Subtype.val ⁻¹' t)) → IsClosed t) → Topology.IsCoherentWith S
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.thmInstanceKey : Lean.Name
-- Mathlib.Algebra.Homology.Localization
HomotopyCategory.mem_quasiIso_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C] {X Y : HomotopyCategory C c}
  (f : X ⟶ Y),
  HomotopyCategory.quasiIso C c f ↔ ∀ (n : ι), CategoryTheory.IsIso ((HomotopyCategory.homologyFunctor C c n).map f)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.diam_image : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F) (s : Set α), Metric.diam (⇑f '' s) = Metric.diam s
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toList.eq_1 : ∀ {α : Type u} {β : Type v} (m : Std.HashMap.Raw α β), m.toList = Std.DHashMap.Raw.Const.toList m.inner
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
/-- A simple graph is *`ε`-far from triangle-free* if one must remove at least
`ε * (card α) ^ 2` edges to make it triangle-free.  -/
SimpleGraph.FarFromTriangleFree : {α : Type u_1} →
  {𝕜 : Type u_3} → [Field 𝕜] → [LinearOrder 𝕜] → (G : SimpleGraph α) → 𝕜 → [Fintype α] → [DecidableRel G.Adj] → Prop
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_of_adjoin_splits_of_aeval : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] {S : Set E},
  (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
    ∀ {x : E} {y : K}, IntermediateField.adjoin F S = ⊤ → (Polynomial.aeval y) (minpoly F x) = 0 → ∃ φ, φ x = y
-- Mathlib.Probability.Distributions.Uniform
PMF.mem_support_uniformOfFintype : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] (a : α), a ∈ (PMF.uniformOfFintype α).support
-- Init.Core
/-- Notation type class for the union operation `∪`.  -/
Union : Type u → Type u
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_smul₀ : ∀ {G₀ : Type u_2} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [inst_3 : MeasurableConstSMul G₀ α] {c : G₀} (hc : c ≠ 0),
  (MeasurableEquiv.smul₀ c hc).symm = MeasurableEquiv.smul₀ c⁻¹ ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Refine a pre-`0`-hypercover by `0`-hypercovers of the pairwise pullbacks.  -/
CategoryTheory.PreZeroHypercover.refineOneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      (E : CategoryTheory.PreZeroHypercover X) →
        [inst_1 : E.HasPullbacks] →
          ((i j : E.I₀) → CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback (E.f i) (E.f j))) →
            CategoryTheory.PreOneHypercover X
-- Lean.Meta.SameCtorUtils
/-- Returns true if `e` occurs either in `t`, or in the type of a sub-expression of `t`.

Consider the following example:
```lean
inductive Tyₛ : Type (u+1)
| SPi : (T : Type u) -> (T -> Tyₛ) -> Tyₛ

inductive Tmₛ.{u} :  Tyₛ.{u} -> Type (u+1)
| app : Tmₛ (.SPi T A) -> (arg : T) -> Tmₛ (A arg)```
```
When looking for fixed arguments in `Tmₛ.app`, if we only consider occurrences in the term `Tmₛ (A arg)`,
`T` is considered non-fixed despite the fact that `A : T -> Tyₛ`.
This leads to an ill-typed injectivity theorem signature:
```lean
theorem Tmₛ.app.inj {T : Type u} {A : T → Tyₛ} {a : Tmₛ (Tyₛ.SPi T A)} {arg : T} {T_1 : Type u} {a_1 : Tmₛ (Tyₛ.SPi T_1 A)} :
Tmₛ.app a arg = Tmₛ.app a_1 arg →
  T = T_1 ∧ a ≍ a_1 := fun x => Tmₛ.noConfusion x fun T_eq A_eq a_eq arg_eq => eq_of_heq a_eq
```
Instead of checking the type of every subterm, we only need to check the type of free variables, since free variables introduced in
the constructor may only appear in the type of other free variables introduced after them.
 -/
Lean.Meta.occursOrInType : Lean.LocalContext → Lean.Expr → Lean.Expr → Bool
-- Mathlib.Topology.Path
Path.mk : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {x y : X} →
      (toContinuousMap : C(↑unitInterval, X)) → toContinuousMap.toFun 0 = x → toContinuousMap.toFun 1 = y → Path x y
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
/-- Left-whiskering the pushout-product of `X₁` and `X₂` with `W : C` is isomorphic to the
pushout-product of `W ◁ X₁` and `X₂`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPushouts C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        (X₁ X₂ : CategoryTheory.Arrow C) →
          {W : C} →
            [CategoryTheory.Limits.PreservesColimit
                  (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
                    (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
                  (CategoryTheory.MonoidalCategory.tensorLeft W)] →
              CategoryTheory.Arrow.mk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (X₁ □ X₂).hom) ≅
                CategoryTheory.Arrow.mk (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W X₁.hom) □ X₂
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- The morphism `Δ[c.dim + 1] ⟶ X` corresponding to a cell of
a rank function for a proper pairing of a subcomplex of `X : SSet`.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.map : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          {f : P.RankFunction ι} →
            {i : ι} → (c : f.Cell i) → [P.IsProper] → SSet.stdSimplex.obj { len := c.dim + 1 } ⟶ X
-- Mathlib.Topology.Sets.Closeds
/-- The type of closed subsets of a topological space.  -/
TopologicalSpace.Closeds : (α : Type u_4) → [TopologicalSpace α] → Type u_4
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm'_eq_zero_of_ae_eq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] {f : α → ε} {p : ℝ},
  0 < p → (∀ᵐ (x : α) ∂μ, ‖f x‖ₑ = 0) → MeasureTheory.eLpNorm' f p μ = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α},
        Std.DHashMap.Internal.Raw₀.Const.get? (m₁.diff m₂) k =
          if m₂.contains k = true then none else Std.DHashMap.Internal.Raw₀.Const.get? m₁ k
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} {inst_1 : DecidableEq n} [inst_2 : DecidableEq n]
  [inst_3 : Fintype n] (M M_1 : Matrix n n R), M = M_1 → M.charpoly = M_1.charpoly
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.inter : {α : Type u} →
  {β : α → Type v} →
    [BEq α] →
      [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.sSup_normal : ∀ {G : Type u_2} [inst : Group G] (Hs : Set (Subgroup G)), (∀ H ∈ Hs, H.Normal) → (sSup Hs).Normal
-- Init.Data.SInt.Bitwise
Int32.not_or_self : ∀ {a : Int32}, ~~~a ||| a = -1
-- Mathlib.Data.ENat.Basic
ENat.WithBot.coe_eq_natCast : ∀ (n : ℕ), ↑↑n = ↑n
-- Mathlib.Condensed.TopCatAdjunction
/-- The counit of the adjunction `condensedSetToCompactlyGenerated ⊣ compactlyGeneratedToCondensedSet`
is a homeomorphism.
 -/
CondensedSet.compactlyGeneratedAdjunctionCounitHomeo : (X : TopCat) → [UCompactlyGeneratedSpace ↑X] → ↑X.toCondensedSet.toTopCat ≃ₜ ↑X
-- Lean.Util.PPExt
Lean.instCoeFormatFormatWithInfos : Coe Std.Format Lean.FormatWithInfos
-- Lean.Parser.Command
Lean.Parser.Command.declValEqns.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.SizeOf
Subtype.mk.congr_simp : ∀ {α : Sort u} {p : α → Prop} (val val_1 : α) (e_val : val = val_1) (property : p val), ⟨val, property⟩ = ⟨val_1, ⋯⟩
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.main.unpack.go : {α : Type} →
  (Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.Elab.TermElabM α) →
    Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM α
-- Mathlib.NumberTheory.Pell
/-- A solution with `x > 1` must have `y ≠ 0`.  -/
Pell.Solution₁.y_ne_zero_of_one_lt_x : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 1 < a.x → a.y ≠ 0
-- Mathlib.MeasureTheory.Function.LpSpace.Complete
MeasureTheory.Lp.ae_tendsto_of_cauchy_eLpNorm' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} [inst : NormedAddCommGroup E]
  [CompleteSpace E] {f : ℕ → α → E} {p : ℝ},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    1 ≤ p →
      ∀ {B : ℕ → ENNReal},
        ∑' (i : ℕ), B i ≠ ⊤ →
          (∀ (N n m_1 : ℕ), N ≤ n → N ≤ m_1 → MeasureTheory.eLpNorm' (f n - f m_1) p μ < B N) →
            ∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds l)
-- Batteries.Data.DList.Lemmas
Batteries.DList.toList_cons : ∀ {α : Type u_1} (x : α) (l : Batteries.DList α), (Batteries.DList.cons x l).toList = x :: l.toList
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (self : F.DescentData' sq sq₃) (i₁ i₂ i₃ : ι),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂
        ⋯ ⋯)
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂ (sq₃ i₁ i₂ i₃).p₃
        ⋯ ⋯) =
    CategoryTheory.Pseudofunctor.DescentData'.pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
CategoryTheory.Iso.toHopfAlgEquiv_trans : ∀ {R : Type u} [inst : CommRing R] {X Y Z : HopfAlgCat R} (e : X ≅ Y) (f : Y ≅ Z),
  (e ≪≫ f).toHopfAlgEquiv = e.toHopfAlgEquiv.trans f.toHopfAlgEquiv
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.Path.hom₀ : ∀ {X : TopCat} {x y : ↑X} (self : X.Path x y), (CategoryTheory.ConcreteCategory.hom self.hom) 0 = x
-- Mathlib.Order.Interval.Set.Defs
/-- `Iic b` is the left-infinite right-closed interval $(-∞, b]$.  -/
Set.Iic : {α : Type u_1} → [Preorder α] → α → Set α
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.instIsMulCommutative_closure : ∀ {S : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : SetLike S R] [inst_2 : MulMemClass S R] (s : S)
  [IsMulCommutative ↥s], IsMulCommutative ↥(Subring.closure ↑s)
-- Mathlib.RepresentationTheory.Equiv
Representation.leftRegularMapEquiv_apply : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) (f : (Representation.leftRegular k G).IntertwiningMap σ),
  σ.leftRegularMapEquiv f = f (MonoidAlgebra.single 1 1)
-- Mathlib.Data.ZMod.Basic
ZMod.cast_sub' : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [CharP R n] (a b : ZMod n), (a - b).cast = a.cast - b.cast
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeleton.eq_1 : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (n : ℕ∞),
  Topology.RelCWComplex.skeleton C n = Topology.RelCWComplex.skeletonLT C (n + 1)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substInvFun.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)],
  P.substInvFun 0 = 0
-- Mathlib.CategoryTheory.Triangulated.Adjunction
CategoryTheory.Adjunction.IsTriangulated.rightAdjoint_isTriangulated : ∀ {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.Limits.HasZeroObject C}
  {inst_3 : CategoryTheory.Limits.HasZeroObject D} {inst_4 : CategoryTheory.Preadditive C}
  {inst_5 : CategoryTheory.Preadditive D} {inst_6 : CategoryTheory.HasShift C ℤ} {inst_7 : CategoryTheory.HasShift D ℤ}
  {inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive}
  {inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive} {inst_10 : CategoryTheory.Pretriangulated C}
  {inst_11 : CategoryTheory.Pretriangulated D} {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {inst_12 : F.CommShift ℤ} {inst_13 : G.CommShift ℤ} [self : adj.IsTriangulated], G.IsTriangulated
-- Mathlib.Logic.Encodable.Basic
/-- Encodability is preserved by equivalence.  -/
Encodable.ofEquiv : {β : Type u_2} → (α : Type u_3) → [Encodable α] → β ≃ α → Encodable β
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
/-- `Ideal.homogeneousHull 𝒜` and `toIdeal : HomogeneousIdeal 𝒜 → Ideal A` form a Galois
insertion.  -/
Ideal.homogeneousHull.gi : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : Semiring A] →
        [inst_1 : DecidableEq ι] →
          [inst_2 : AddMonoid ι] →
            [inst_3 : SetLike σ A] →
              [inst_4 : AddSubmonoidClass σ A] →
                (𝒜 : ι → σ) →
                  [inst_5 : GradedRing 𝒜] → GaloisInsertion (Ideal.homogeneousHull 𝒜) HomogeneousIdeal.toIdeal
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.getD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → β → β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_pi_add : ∀ (θ : Real.Angle), (↑Real.pi + θ).sign = -θ.sign
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k a : α} {fallback : β a} {v : β k},
      (m.insertIfNew k v).getD a fallback =
        if h : (k == a) = true ∧ m.contains k = false then cast ⋯ v else m.getD a fallback
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey!_eq_getElem!_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] {l : Std.DTreeMap.Internal.Impl α β}, l.minKey! = l.minKey?.get!
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.LFunction_def_even : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Even Φ →
    ∀ (s : ℂ), ZMod.LFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.hurwitzZetaEven (ZMod.toAddCircle j) s
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_add_left_left : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime (y * z + x) y
-- Batteries.Control.Nondet.Basic
Nondet.instMonadLift : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → MonadLift m (Nondet m)
-- Mathlib.Data.Rel
SetRel.IsSymm.sInter : ∀ {α : Type u_1} {ℛ : Set (SetRel α α)}, (∀ R ∈ ℛ, R.IsSymm) → SetRel.IsSymm (⋂₀ ℛ)
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.saveConst : Lean.Name → Lean.Meta.Try.Collector.M Unit
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.coe_dfinsuppSum : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M]
  [inst_2 : (i : ι) → Zero (β i)] [inst_3 : (i : ι) → (y : β i) → Decidable (y ≠ 0)] (c : AddCon M)
  (h : (i : ι) → β i → M) (f : Π₀ (i : ι), β i), ↑(f.sum h) = f.sum fun i b => ↑(h i b)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.decidableNF : DecidablePred ONote.NF
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.touchpointWeights.congr_simp : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 →
    ∀ (signs signs_1 : Finset (Fin (n + 1))),
      signs = signs_1 →
        ∀ (i i_1 : Fin (n + 1)),
          i = i_1 →
            ∀ (a a_1 : Fin (n + 1)), a = a_1 → s.touchpointWeights signs i a = s_1.touchpointWeights signs_1 i_1 a_1
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element of the tree set, panicking if the set is empty.
 -/
Std.TreeSet.min! : {α : Type u} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeSet α cmp → α
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- Characterizing when a subspace `C` of a topological space `X` is a CW complex. Note that this
requires `C` to be closed. If `C` is not closed choose `X` to be `C`.  -/
Topology.CWComplex : {X : Type u} → [TopologicalSpace X] → Set X → Type (u + 1)
-- Mathlib.Order.ModularLattice
instIsUpperModularLatticeOrderDual : ∀ {α : Type u_1} [inst : Lattice α] [IsLowerModularLattice α], IsUpperModularLattice αᵒᵈ
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div.injEq : ∀ (k : ℤ) (e : Lean.Meta.Grind.Arith.CommRing.EqCnstr) (k_1 : ℤ) (e_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div k e = Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.div k_1 e_1) =
    (k = k_1 ∧ e = e_1)
-- Mathlib.NumberTheory.Harmonic.Defs
harmonic_succ : ∀ (n : ℕ), harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- A functor that interprets elements of `D` as functors `C ⥤ V`.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι : (C : Type u₁) →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    (V : Type u₂) →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            (D : Type u₃) →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  CategoryTheory.Functor D (CategoryTheory.Functor C V)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- Limit `→ ∞` for `WithSeminorms`.  -/
WithSeminorms.tendsto_nhds_atTop : ∀ {𝕜 : Type u_2} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι} [inst_4 : SemilatticeSup F]
  [Nonempty F],
  WithSeminorms p →
    ∀ (u : F → E) (y₀ : E),
      Filter.Tendsto u Filter.atTop (nhds y₀) ↔
        ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.instCommMonoid.eq_1 : ∀ {α : Type u} [inst : CommSemigroup α], WithOne.instCommMonoid = { toMonoid := WithOne.instMonoid, mul_comm := ⋯ }
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instHashablePreInstance : Hashable Lean.Meta.Grind.PreInstance
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.mem_cardSuppLTSubfield : ∀ {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [inst : LinearOrder Γ] [inst_1 : AddCommGroup Γ]
  [inst_2 : IsOrderedAddMonoid Γ] [inst_3 : Field R] [hκ : Fact (Cardinal.aleph0 < κ)] {x : HahnSeries Γ R},
  x ∈ HahnSeries.cardSuppLTSubfield Γ R κ ↔ x.cardSupp < κ
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that the
multiplicity of `v` in the factorization of `I`, denoted `val_v(I)`, is nonzero.  -/
Associates.finite_factors : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 →
    ∀ᶠ (v : IsDedekindDomain.HeightOneSpectrum R) in Filter.cofinite,
      ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = 0
-- Mathlib.Algebra.Group.Units.Equiv
/-- A version of `Equiv.mulRight a⁻¹ b` that is defeq to `b / a`.  -/
Equiv.divRight : {G : Type u_5} → [Group G] → G → G ≃ G
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.minKey?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : β → β},
  (Std.ExtDTreeMap.Const.modify t k f).minKey? =
    Option.map (fun km => if cmp km k = Ordering.eq then k else km) t.minKey?
-- Init.Data.Vector.Lemmas
Vector.foldr_flatMap : ∀ {α : Type u_1} {β : Type u_2} {m : ℕ} {γ : Type u_3} {n : ℕ} {f : α → Vector β m} {g : β → γ → γ} {xs : Vector α n}
  {init : γ}, Vector.foldr g init (xs.flatMap f) = Vector.foldr (fun x acc => Vector.foldr g acc (f x)) init xs
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.Slow.instDecidableMemP : {α : Type u_1} →
  {cmp : α → α → Ordering} → {cut : α → Ordering} → {t : RBTree.RBSet α cmp} → Decidable (RBTree.RBSet.MemP cut t)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β} {he : (Std.DTreeMap.Const.alter t k f).isEmpty = false},
  (Std.DTreeMap.Const.alter t k f).minKey he = k ↔
    (f (Std.DTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- A frame of key-value pairs from a collision node.  -/
Lean.PersistentHashMap.Zipper.consCollision : {α : Type u} →
  {β : Type v} →
    (keys : Subarray α) →
      (vals : Subarray β) →
        Std.Slice.size keys = Std.Slice.size vals →
          Lean.PersistentHashMap.Zipper α β → Lean.PersistentHashMap.Zipper α β
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_mk : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s : Set α) (h : IsClopen s), ↑{ carrier := s, isClopen' := h } = s
-- Init.Data.List.Lex
List.not_lex_total : ∀ {α : Type u_1} {r : α → α → Prop},
  (∀ (x y : α), ¬r x y ∨ ¬r y x) → ∀ (l₁ l₂ : List α), ¬List.Lex r l₁ l₂ ∨ ¬List.Lex r l₂ l₁
-- Mathlib.Algebra.Order.Group.Synonym
toDual_vadd' : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : α), OrderDual.toDual b +ᵥ a = b +ᵥ a
-- Mathlib.Order.Ideal
/-- In a directed and nonempty order, the top ideal is `univ`.  -/
Order.Ideal.instOrderTop : {P : Type u_1} → [inst : LE P] → [IsDirectedOrder P] → [Nonempty P] → OrderTop (Order.Ideal P)
-- Mathlib.Analysis.Convex.Function
ConcaveOn.convex_gt : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConcaveOn 𝕜 s f → ∀ (r : β), Convex 𝕜 {x | x ∈ s ∧ r < f x}
-- Mathlib.Data.Finset.Insert
Finset.nontrivial_coe : ∀ {α : Type u_1} {s : Finset α}, (↑s).Nontrivial ↔ s.Nontrivial