mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.WithBot
Equiv.withBotSubtypeNe_apply : ∀ {α : Type u_1} (x : { y // y ≠ ⊥ }),
  Equiv.withBotSubtypeNe x =
    match x with
    | ⟨x, h⟩ => x.unbot h
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.mk : Std.Time.TimeZone.Offset → String → String → Bool → Std.Time.TimeZone
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_neg_one_eq_inv : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : Aˣ), autoParam (0 ≤ ↑a) CFC.rpow_neg_one_eq_inv._auto_1 → ↑a ^ (-1) = ↑a⁻¹
-- Mathlib.Computability.DFA
Language.IsRegular.compl : ∀ {T : Type u} {L : Language T}, L.IsRegular → Lᶜ.IsRegular
-- Mathlib.Topology.MetricSpace.HolderNorm
/-- Version of `memHolder_const` with the spelling `fun _ ↦ c` for the constant function.  -/
memHolder_const' : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {c : Y},
  MemHolder r fun x => c
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.comp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) (X : C),
  (CategoryTheory.CategoryStruct.comp α β).app X = CategoryTheory.CategoryStruct.comp (α.app X) (β.app X)
-- Init.Data.BitVec.Bitblast
/-- A recurrence that describes multiplication as repeated addition.

This function is useful for bit blasting multiplication.
 -/
BitVec.mulRec : {w : ℕ} → BitVec w → BitVec w → ℕ → BitVec w
-- Mathlib.Algebra.Group.Center
Set.addCentralizer_addCentralizer_addCentralizer : ∀ {M : Type u_1} [inst : Add M] (S : Set M), S.addCentralizer.addCentralizer.addCentralizer = S.addCentralizer
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_mul : ∀ {x : ℝ}, 0 ≤ x → ∀ (y : ℝ), √(x * y) = √x * √y
-- Mathlib.Analysis.Calculus.AddTorsor.AffineMap
/-- `AffineMap.lineMap` is smooth in all three arguments.  -/
AffineMap.contDiff_lineMap_uncurry : ∀ {𝕜 : Type u_1} {V : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] {n : WithTop ℕ∞}, ContDiff 𝕜 n fun pqc => (AffineMap.lineMap pqc.1 pqc.2.1) pqc.2.2
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.pp.analyze.trustSubtypeMk : Lean.Option Bool
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_sup_sdiff : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], z \ (x \ y ⊔ y \ x) = z ⊓ (z \ x ⊔ y) ⊓ (z \ y ⊔ x)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_germ_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑Y.toTopCat) (x : ↑X.toTopCat)
  (hx : (CategoryTheory.ConcreteCategory.hom f.base) x ∈ U) {Z : CommRingCat} (h : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.germ U ((CategoryTheory.ConcreteCategory.hom f.base) x) hx)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap f x) h) =
    CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp (X.presheaf.germ ((TopologicalSpace.Opens.map f.base).obj U) x hx) h)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
aestronglyMeasurable_derivWithin_Ioi : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F]
  (μ : MeasureTheory.Measure ℝ), MeasureTheory.AEStronglyMeasurable (fun x => derivWithin f (Set.Ioi x) x) μ
-- Init.Data.Iterators.Basic
/-- Asserts that a certain iterator `it'` could plausibly be the directly succeeding iterator of another
given iterator `it`.
 -/
Std.IterM.IsPlausibleSuccessorOf : {α : Type w} → {m : Type w → Type w'} → {β : Type w} → [Std.Iterator α m β] → Std.IterM m β → Std.IterM m β → Prop
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addRightCancelSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : AddRightCancelSemigroup M₂] (f : M₁ → M₂)
  (hf : Function.Injective f) (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Injective.addRightCancelSemigroup f hf mul =
    { toAddSemigroup := Function.Injective.addSemigroup f hf mul, toIsRightCancelAdd := ⋯ }
-- Mathlib.Data.Num.Bitwise
SNum.nz.sizeOf_spec : ∀ (a : NzsNum), sizeOf (SNum.nz a) = 1 + sizeOf a
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.prodEquivOfIsTopCompl_symm_apply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q) (x : M),
  (p.prodEquivOfIsTopCompl q h).symm x = ((p.projectionOntoL q h) x, (q.projectionOntoL p ⋯) x)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.Pos.revSkip?_char_eq_some_iff : ∀ {c : Char} {s : String.Slice} {pos res : s.Pos},
  pos.revSkip? c = some res ↔ ∃ (h : pos ≠ s.startPos), res = pos.prev h ∧ (pos.prev h).get ⋯ = c
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- Given a family of elements of a sieve `S` on `X`, and a map `Y ⟶ X`, we can obtain a
family of elements of `S.pullback f` by taking the same elements.
 -/
CategoryTheory.Presieve.FamilyOfElements.pullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {X Y : C} →
        {S : CategoryTheory.Sieve X} →
          (f : Y ⟶ X) →
            CategoryTheory.Presieve.FamilyOfElements P S.arrows →
              CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Sieve.pullback f S).arrows
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whisker_exchange : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {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}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (η : ψ ⟶ ψ')
  {φ φ' : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''} (θ : φ ⟶ φ'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ θ)
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight η φ)
      (CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ' θ)
-- Init.Data.Ord.Basic
Ordering.lt_beq_gt : (Ordering.lt == Ordering.gt) = false
-- Mathlib.Algebra.GCDMonoid.Basic
associated_normalize_iff : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {x y : α},
  Associated x (normalize y) ↔ Associated x y
-- Mathlib.Topology.MetricSpace.Isometry
/-- The identity isometry of a space.  -/
IsometryEquiv.refl : (α : Type u_3) → [inst : PseudoEMetricSpace α] → α ≃ᵢ α
-- Mathlib.Algebra.Group.Prod
MonoidHom.inl_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (x : M), (MonoidHom.inl M N) x = (x, 1)
-- Mathlib.GroupTheory.Coset.Basic
QuotientGroup.orbit_mk_eq_smul : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} (x : α), MulAction.orbitRel.Quotient.orbit ↑x = x • ↑s
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj.eq_1 : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X), S.proj = Quotient.mk''
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.integral_comp_mul_right_Ioi' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) (a : ℝ) {b : ℝ},
  0 < b → b • ∫ (x : ℝ) in Set.Ioi a, g (x * b) = ∫ (x : ℝ) in Set.Ioi (a * b), g x
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.instMkEvalCompMonoidalM : Mathlib.Tactic.BicategoryLike.MkEvalComp Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- Notation for the initial object in `C`  -/
CategoryTheory.Limits.«term⊥__» : Lean.ParserDescr
-- Lean.Parser.Types
/-- Run `p` and record result in parser cache for any further invocation with this `parserName`, parser context, and parser state.
`p` cannot access syntax stack elements pushed before the invocation in order to make caching independent of parser history.
As this excludes trailing parsers from being cached, we also reset `lhsPrec`, which is not read but set by leading parsers, to 0
in order to increase cache hits. Finally, `errorMsg` is also reset to `none` as a leading parser should not be called in the first
place if there was an error.
 -/
Lean.Parser.withCacheFn : Lean.Name → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Init.Prelude
/-- `stx.isIdent` is `true` iff `stx` is an identifier.  -/
Lean.Syntax.isIdent : Lean.Syntax → Bool
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.uliftYonedaIsoYoneda_hom_app_hom_app_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{max w v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] (X : C) (X_1 : Cᵒᵖ) (x : ULift.{w, max v w} (Opposite.unop X_1 ⟶ X)),
  (CategoryTheory.ConcreteCategory.hom ((J.uliftYonedaIsoYoneda.hom.app X).hom.app X_1)) x = x.down
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- If a set `s` spans the space, this is a basis contained in `s`.  -/
Module.Basis.ofSpan : {K : Type u_3} →
  {V : Type u_4} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] → {s : Set V} → ⊤ ≤ Submodule.span K s → Module.Basis (↑(⋯.extend ⋯)) K V
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt8.size ≤ n →
    (UInt8.ofNatClamp n).toUInt64 = UInt64.ofNatLT (UInt8.size - 1) UInt8.toUInt64_ofNatClamp_of_le._proof_1
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.BorelCantelli.integrable_process : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} {ℱ : MeasureTheory.Filtration ℕ m0} {s : ℕ → Set Ω}
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ℕ), MeasurableSet (s n)) → ∀ (n : ℕ), MeasureTheory.Integrable (MeasureTheory.BorelCantelli.process s n) μ
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- If `C` has all limits of diagrams `parallelFamily f`, then it has all wide equalizers  -/
CategoryTheory.Limits.hasWideEqualizers_of_hasLimit_parallelFamily : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [∀ {J : Type w} {X Y : C} {f : J → (X ⟶ Y)}, CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelFamily f)],
  CategoryTheory.Limits.HasWideEqualizers C
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- The following diagram is a pullback
```
X --id--> X
|         |
f         f
v         v
Z --id--> Z
```
 -/
CategoryTheory.IsPushout.id_horiz : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (f : X ⟶ Z),
  CategoryTheory.IsPushout (CategoryTheory.CategoryStruct.id X) f f (CategoryTheory.CategoryStruct.id Z)
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.boxProdComm_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (G : SimpleGraph α) (H : SimpleGraph β) (a : β × α),
  (RelIso.symm (G.boxProdComm H)) a = a.swap
-- Mathlib.Order.Lattice.Nat
/-- This combines `Nat.iInf_of_empty` with `ciInf_const`.  -/
Nat.iInf_const_zero : ∀ {ι : Sort u_1}, ⨅ x, 0 = 0
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- To check that `η = traj κ a` it is enough to show that the restriction of `η` to variables `≤ b`
is `partialTraj κ a b` for any `b ≥ n`.  -/
ProbabilityTheory.Kernel.eq_traj' : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1)))
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} (n : ℕ)
  (η : ProbabilityTheory.Kernel ((i : ↥(Finset.Iic a)) → X ↑i) ((n : ℕ) → X n)),
  (∀ b ≥ n, η.map (Preorder.frestrictLe b) = ProbabilityTheory.Kernel.partialTraj κ a b) →
    η = ProbabilityTheory.Kernel.traj κ a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.mul_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Mul β]
  [ContinuousMul β], MeasureTheory.StronglyMeasurable f → ∀ (c : β), MeasureTheory.StronglyMeasurable fun x => f x * c
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.congr : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {w : ι → M}, LinearIndepOn R v s → Set.EqOn v w s → LinearIndepOn R w s
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSliceData : (α : Type u) → Type v → [Ord α] → Type (max u v)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- If the scalar product forms a `Module`, and the `SubMulAction` is not `⊥`, then the
subset inherits the zero.  -/
SubMulAction.instZeroSubtypeMemOfNonempty : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (p : SubMulAction R M) → [n_empty : Nonempty ↥p] → Zero ↥p
-- Mathlib.Topology.UniformSpace.Basic
instIsCountablyGeneratedProdSumUniformity : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : UniformSpace β] [(uniformity α).IsCountablyGenerated]
  [(uniformity β).IsCountablyGenerated], (uniformity (α ⊕ β)).IsCountablyGenerated
-- Mathlib.Order.Category.BddDistLat
_private.Mathlib.Order.Category.BddDistLat.0.BddDistLat.Hom.mk.sizeOf_spec : ∀ {X Y : BddDistLat} (hom' : BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Aesop.Util.Basic
Aesop.withAllTransparencySyntax : Lean.Meta.TransparencyMode → Lean.TSyntax `tactic → Lean.TSyntax `tactic
-- Mathlib.Control.Bitraversable.Instances
/-- The bitraverse function for `flip`.  -/
flip.bitraverse : {t : Type u → Type u → Type u} →
  [Bitraversable t] →
    {F : Type u → Type u} →
      [Applicative F] → {α α' β β' : Type u} → (α → F α') → (β → F β') → flip t α β → F (flip t α' β')
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.id.match_1.eq_2 : ∀ {C : Type u_1} (motive : CategoryTheory.WithTerminal C → Sort u_2)
  (h_1 : (a : C) → motive (CategoryTheory.WithTerminal.of a)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of a => h_1 a
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_2 ()
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.ite.injEq : ∀ {α : Type} (a a_1 a_2 a_3 a_4 a_5 : Std.Tactic.BVDecide.BoolExpr α),
  (a.ite a_1 a_2 = a_3.ite a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Data.Option.Basic
Option.eq_of_mem_of_mem : ∀ {α : Type u_1} {a : α} {o1 o2 : Option α}, a ∈ o1 → a ∈ o2 → o1 = o2
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.affineCombination_coord_eq_self : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) [inst_4 : Fintype ι] (q : P),
  ((Finset.affineCombination k Finset.univ ⇑b) fun i => (b.coord i) q) = q
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.apply_lt_veblenWith_apply_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o a : Ordinal.{u}},
  Order.IsNormal f → (f a < Ordinal.veblenWith f o (f a) ↔ a < Ordinal.veblenWith f o a)
-- Mathlib.Algebra.CharP.Defs
CharP.cast_eq_zero_iff : ∀ (R : Type u_2) {inst : AddMonoidWithOne R} (p : outParam ℕ) [self : CharP R p] (x : ℕ), ↑x = 0 ↔ p ∣ x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- If a short complex `S` has both a left and right homology,
this is the canonical morphism `S.leftHomology ⟶ S.rightHomology`.  -/
CategoryTheory.ShortComplex.leftRightHomologyComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasLeftHomology] → [inst_3 : S.HasRightHomology] → S.leftHomology ⟶ S.rightHomology
-- Mathlib.Topology.Order.LiminfLimsup
/-- The `limsSup` of a filter `f` is the greatest cluster point of `f`.  -/
isGreatest_clusterPt_limsSup : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} [f.NeBot],
  autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) f) isGreatest_clusterPt_limsSup._auto_1 →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≤ x2) f) isGreatest_clusterPt_limsSup._auto_3 →
      IsGreatest {x | ClusterPt x f} f.limsSup
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_eq_of_mem_finset : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E}
  [inst_1 : AddCommMonoid E] {s : Finset ι},
  (∀ (ω : Ω), τ ω ∈ WithTop.some '' ↑s) → MeasureTheory.stoppedValue u τ = ∑ i ∈ s, {ω | τ ω = ↑i}.indicator (u i)
-- Mathlib.Tactic.Translate.Reorder
/-- `(reorder := ...)` reorders the arguments/hypotheses in the generated declaration.
This is used in `to_dual` to swap the arguments in `≤`, `<` and `⟶`,
and it is used in `to_additive` to translate from `a ^ n` to `n • a`.
It uses disjoint cycle notation for the permutation. For reordering arguments of an argument `a`,
it uses the notation `a (...)` where `...` can be any reorder.

For example:
- `(reorder := α β, 5 6)` swaps the arguments `α` and `β` with each other and the fifth and
  the sixth argument.
- `(reorder := 3 4 5)` will move the fifth argument before the third argument.
- `(reorder := H (x y))` will swap the arguments `x` and `y` that appear in the hypothesis `H`.

If the translated declaration already exists (i.e. when using `existing` or `self`), the reorder
argument is automatically inferred using the function `guessReorder`.  -/
Mathlib.Tactic.Translate.reorder : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- `H`-free extremal graphs are `H`-free simple graphs having `extremalNumber (card V) H` many
edges.  -/
SimpleGraph.isExtremal_free_iff : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V]
  [inst_1 : DecidableRel G.Adj],
  G.IsExtremal H.Free ↔ H.Free G ∧ G.edgeFinset.card = SimpleGraph.extremalNumber (Fintype.card V) H
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.map_modByMonicHom : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (x : S), h.map (h.modByMonicHom x) = x
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.instMkMor₂MonoidalM_1 : Mathlib.Tactic.BicategoryLike.MkMor₂ Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- **Alias** of the reverse direction of `NumberField.InfinitePlace.isRamified_mk_iff_isMixed`. -/
NumberField.ComplexEmbedding.IsMixed.mk_isRamified : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsMixed k φ → NumberField.InfinitePlace.IsRamified k (NumberField.InfinitePlace.mk φ)
-- Mathlib.Geometry.Manifold.StructureGroupoid
ClosedUnderRestriction.closedUnderRestriction : ∀ {H : Type u_1} {inst : TopologicalSpace H} {G : StructureGroupoid H} [self : ClosedUnderRestriction G]
  {e : OpenPartialHomeomorph H H}, e ∈ G → ∀ (s : Set H), IsOpen s → e.restr s ∈ G
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.denom_div : ∀ {K : Type u} [inst : Field K] (p : Polynomial K) {q : Polynomial K},
  q ≠ 0 →
    ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).denom =
      Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, (Std.DHashMap.map f m).getKey? k = m.getKey? k
-- Init.Data.String.Slice
String.Slice.instInhabitedRevSplitIterator.default : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} → {inst : String.Slice.Pattern.ToBackwardSearcher pat σ} → String.Slice.RevSplitIterator pat s
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_inf : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Min β] (a b : β), ↑(a ⊓ b) = ↑a ⊓ ↑b
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
MulEquiv.uniqueFactorizationMonoid_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : CommMonoidWithZero β] (e : α ≃* β),
  UniqueFactorizationMonoid α ↔ UniqueFactorizationMonoid β
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `MulAction.isBlock_iff_disjoint_smul_of_ne`. -/
MulAction.IsBlock.disjoint_smul_of_ne : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B → ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
-- Aesop.Rule
Aesop.NormSimpRule.entries : Aesop.NormSimpRule → Array Lean.Meta.SimpEntry
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: a countable intersection of dense Gδ sets is dense. Formulated here with
an index set which is a countable type.  -/
dense_iInter_of_Gδ : ∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X},
  (∀ (s : ι), IsGδ (f s)) → (∀ (s : ι), Dense (f s)) → Dense (⋂ s, f s)
-- Mathlib.Data.Semiquot
Semiquot.instMembership : {α : Type u_1} → Membership α (Semiquot α)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toOpens.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] (U : OpenAddSubgroup G),
  ↑U = { carrier := ↑U, is_open' := ⋯ }
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.done.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β], sizeOf Lean.PersistentHashMap.Zipper.done = 1
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- If a sequence of peak functions `φᵢ` converges uniformly to zero away from a point `x₀` and its
integral on some finite-measure neighborhood of `x₀` converges to `1`, and `g` is integrable and
has a limit `a` at `x₀`, then `∫ φᵢ • g` converges to `a`. Version localized to a subset.  -/
tendsto_setIntegral_peak_smul_of_integrableOn_of_tendsto : ∀ {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E}
  {l : Filter ι} {x₀ : α} {s : Set α} {φ : ι → α → ℝ} {a : E} [CompleteSpace E],
  MeasurableSet s →
    ∀ {t : Set α},
      MeasurableSet t →
        t ⊆ s →
          t ∈ nhdsWithin x₀ s →
            μ t ≠ ⊤ →
              (∀ᶠ (i : ι) in l, ∀ x ∈ s, 0 ≤ φ i x) →
                (∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)) →
                  Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (nhds 1) →
                    (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) →
                      MeasureTheory.IntegrableOn g s μ →
                        Filter.Tendsto g (nhdsWithin x₀ s) (nhds a) →
                          Filter.Tendsto (fun i => ∫ (x : α) in s, φ i x • g x ∂μ) l (nhds a)
-- Mathlib.Order.OrdContinuous
LeftOrdContinuous.map_sSup : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] {f : α → β},
  LeftOrdContinuous f → ∀ {s : Set α}, s.Nonempty → f (sSup s) = ⨆ x ∈ s, f x