mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k a : α}, (m.erase k).getKey! a = if (k == a) = true then default else m.getKey! a
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.Context.mk.inj : ∀ {u : Lean.Level} {type fieldInst isChar0Inst ringInst semiringInst : Lean.Expr} {u_1 : Lean.Level}
  {type_1 fieldInst_1 isChar0Inst_1 ringInst_1 semiringInst_1 : Lean.Expr},
  { u := u, type := type, fieldInst := fieldInst, isChar0Inst := isChar0Inst, ringInst := ringInst,
        semiringInst := semiringInst } =
      { u := u_1, type := type_1, fieldInst := fieldInst_1, isChar0Inst := isChar0Inst_1, ringInst := ringInst_1,
        semiringInst := semiringInst_1 } →
    u = u_1 ∧
      type = type_1 ∧
        fieldInst = fieldInst_1 ∧ isChar0Inst = isChar0Inst_1 ∧ ringInst = ringInst_1 ∧ semiringInst = semiringInst_1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos.not_nil : ¬Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsPos []
-- Mathlib.CategoryTheory.Category.Cat
/-- The Functor underlying a 1-morphism in Cat  -/
CategoryTheory.Cat.Hom.toFunctor : {C D : CategoryTheory.Cat} → C.Hom D → CategoryTheory.Functor ↑C ↑D
-- Init.Data.Rat.Lemmas
Rat.natCast_lt_natCast : ∀ {a b : ℕ}, ↑a < ↑b ↔ a < b
-- Mathlib.Topology.ContinuousMap.Compact
BoundedContinuousFunction.dist_mkOfCompact : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  (f g : C(α, β)), dist (BoundedContinuousFunction.mkOfCompact f) (BoundedContinuousFunction.mkOfCompact g) = dist f g
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Mul β],
  MeasureTheory.SimpleFunc.instMul = { mul := fun f g => (MeasureTheory.SimpleFunc.map (fun x1 x2 => x1 * x2) f).seq g }
-- Mathlib.Data.Seq.Computation
Computation.think_equiv : ∀ {α : Type u} (s : Computation α), s.think.Equiv s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, k ∈ Std.ExtDHashMap.map f m → k ∈ m
-- Mathlib.Order.Interval.Set.Disjoint
Set.iUnion_Ioc_eq_Ioi_self_iff : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {f : ι → α} {a : α},
  ⋃ i, Set.Ioc a (f i) = Set.Ioi a ↔ ∀ (x : α), a < x → ∃ i, x ≤ f i
-- Mathlib.Computability.TuringDegree
/-- `f` is Turing equivalent to `g` if `f` is reducible to `g` and `g` is reducible to `f`.
 -/
TuringEquivalent : (ℕ →. ℕ) → (ℕ →. ℕ) → Prop
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_one_eq_univ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : One α] [IsBotOneClass α], Set.Ici 1 = Set.univ
-- Mathlib.RingTheory.Polynomial.Wronskian
/-- `Polynomial.wronskian` as a bilinear map.  -/
Polynomial.wronskianBilin : (R : Type u_1) → [inst : CommRing R] → Polynomial R →ₗ[R] Polynomial R →ₗ[R] Polynomial R
-- Std.Sync.Channel
Std.CloseableChannel.instHashableError : Hashable Std.CloseableChannel.Error
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfoRef.toContInfoImpl : Lean.Elab.Do.ContInfoRef → Lean.Elab.Do.ContInfo
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaEquiv_symm_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : Cᵒᵖ}
  (f : X ⟶ Y) {P : CategoryTheory.Functor Cᵒᵖ (Type w)} (t : P.obj X),
  CategoryTheory.shrinkYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (P.map f)) t) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYoneda.{w, v, u}.map f.unop)
      (CategoryTheory.shrinkYonedaEquiv.symm t)
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.algebraMap_eq : ∀ {A : Type u_1} {B' : Type u_3} [inst : CommRing A] [inst_1 : Ring B'] [inst_2 : Algebra A B'] {B : Type u_4}
  [inst_3 : CommRing B] [inst_4 : Algebra A B] [inst_5 : Algebra B B'] [IsScalarTower A B B'],
  Function.Injective ⇑(algebraMap B B') → ∀ (x : B), minpoly A ((algebraMap B B') x) = minpoly A x
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.op_ofNat : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], AddOpposite.op (OfNat.ofNat n) = OfNat.ofNat n
-- Lean.Parser.Extra
Lean.Parser.termParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Contravariant.toRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : Semigroup α] [inst_1 : PartialOrder α] [inst_2 : MulRightReflectLE α],
  Contravariant.toRightCancelSemigroup = { toSemigroup := inst, toIsRightCancelMul := ⋯ }
-- Lean.Data.PersistentArray
Lean.PersistentArray.mk.inj : ∀ {α : Type u} {root : Lean.PersistentArrayNode α} {tail : Array α} {size : ℕ} {shift : USize} {tailOff : ℕ}
  {root_1 : Lean.PersistentArrayNode α} {tail_1 : Array α} {size_1 : ℕ} {shift_1 : USize} {tailOff_1 : ℕ},
  { root := root, tail := tail, size := size, shift := shift, tailOff := tailOff } =
      { root := root_1, tail := tail_1, size := size_1, shift := shift_1, tailOff := tailOff_1 } →
    root = root_1 ∧ tail = tail_1 ∧ size = size_1 ∧ shift = shift_1 ∧ tailOff = tailOff_1
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
/-- The equivalence between sections of `J : SingleObj M ⥤ Type u` and fixed points of the
induced action on `J.obj (SingleObj.star M)`.  -/
CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints : {M : Type v} →
  [inst : Monoid M] →
    (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u)) →
      ↑J.sections ≃ ↑(MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M)))
-- Mathlib.Algebra.Order.Field.Basic
lt_one_div_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (a < 1 / b ↔ b < 1 / a)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The natural transformation induced by `limit.π`.  -/
CategoryTheory.Limits.lim.π : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] →
          (j : J) → CategoryTheory.Limits.lim ⟶ (CategoryTheory.evaluation J C).obj j
-- Mathlib.Algebra.Group.PNatPowAssoc
ppow_mul' : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : Pow M ℕ+] [PNatPowAssoc M] (x : M) (m n : ℕ+), x ^ (m * n) = (x ^ n) ^ m
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRight_map_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (r : R₂ ⟶ R₁) {Y X : CategoryTheory.Comma L R₂} (f : Y ⟶ X),
  ((CategoryTheory.Comma.mapRight L r).map f).right = f.right
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset
Multiset.prod_pos : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [inst_1 : PartialOrder R] [ZeroLEOneClass R] [PosMulStrictMono R]
  [NeZero 1] {s : Multiset R}, (∀ a ∈ s, 0 < a) → 0 < s.prod
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMonoidWithZeroOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : MonoidWithZero β] → [ContinuousMul β] → MonoidWithZero C(α, β)
-- Init.Omega.Int
Lean.Omega.Int.ofNat_max : ∀ (a b : ℕ), ↑(max a b) = max ↑a ↑b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKeyD_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k k' fallback : α},
  (↑m).WF →
    ∀ {f : Option β → Option β},
      (Std.DHashMap.Internal.Raw₀.Const.alter m k f).getKeyD k' fallback =
        if (k == k') = true then if (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).isSome = true then k else fallback
        else m.getKeyD k' fallback
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_take : ∀ {α : Type u_1} {n : ℕ} {xs : Subarray α}, Std.Slice.toList (xs.take n) = List.take n (Std.Slice.toList xs)
-- Mathlib.Algebra.CharP.Lemmas
Commute.add_pow_prime_pow_eq : ∀ {R : Type u_1} [inst : Semiring R] {p : ℕ},
  Nat.Prime p →
    ∀ {x y : R},
      Commute x y →
        ∀ (n : ℕ),
          (x + y) ^ p ^ n =
            x ^ p ^ n + y ^ p ^ n +
              ↑p * x * y * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)
-- Mathlib.Order.Lattice
/-- **Alias** of the reverse direction of `pairwise_iff_lt`. -/
Pairwise.of_lt : ∀ {α : Type u} [inst : LinearOrder α] {p : α → α → Prop} [Std.Symm p], (∀ ⦃a b : α⦄, a < b → p a b) → Pairwise p
-- Mathlib.Algebra.PEmptyInstances
SemigroupPEmpty.eq_1 : SemigroupPEmpty = { mul := fun x x_1 => PEmpty.casesOn (fun t => x = t → PEmpty.{u + 1}) x ⋯, mul_assoc := ⋯ }
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.Disjoint.isConj_mul : ∀ {α : Type u} [Finite α] {σ τ π ρ : Equiv.Perm α},
  IsConj σ π → IsConj τ ρ → σ.Disjoint τ → π.Disjoint ρ → IsConj (σ * τ) (π * ρ)
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- **Alias** of `CategoryTheory.Functor.OplaxMonoidal.oplax_left_unitality`. -/
CategoryTheory.Functor.OplaxMonoidal.left_unitality : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.OplaxMonoidal] (X : C),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OplaxMonoidal.δ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X)
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) (F.obj X)))
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.rat_sup_continuous_lemma : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {ε a₁ a₂ b₁ b₂ : α},
  |a₁ - b₁| < ε → |a₂ - b₂| < ε → |max a₁ a₂ - max b₁ b₂| < ε
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity`.

---

The bijection `normalized_factors_equiv_span_normalized_factors.symm` between the set of prime
factors of the ideal `⟨r⟩` and the set of prime factors of `r` preserves multiplicities.  -/
emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] {r : R} (hr : r ≠ 0)
  (I : ↑{I | I ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})}),
  emultiplicity (↑((Ideal.normalizedFactorsEquivSpanNormalizedFactors hr).symm I)) r =
    emultiplicity (↑I) (Ideal.span {r})
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
contMDiffWithinAt_extChartAt_symm_target_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} (x : M),
  ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I n (↑(extChartAt I x).symm) (extChartAt I x).target
    (↑(extChartAt I x) x)
-- Init.Data.BitVec.Bitblast
/-- If `y &&& z = 0`, `x >>> (y ||| z) = x >>> y >>> z`.
This follows as `y &&& z = 0` implies `y ||| z = y + z`,
and thus `x >>> (y ||| z) = x >>> (y + z) = x >>> y >>> z`.
 -/
BitVec.ushiftRight'_or_of_and_eq_zero : ∀ {w₁ w₂ : ℕ} {x : BitVec w₁} {y z : BitVec w₂}, y &&& z = 0#w₂ → x >>> (y ||| z) = x >>> y >>> z
-- Mathlib.Data.TypeVec
TypeVec.appendFun_comp : ∀ {n : ℕ} {α₀ : TypeVec.{u_1} n} {α₁ : TypeVec.{u_2} n} {α₂ : TypeVec.{u_3} n} {β₀ : Type u_1} {β₁ : Type u_2}
  {β₂ : Type u_3} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂),
  (TypeVec.comp f₁ f₀ ::: g₁ ∘ g₀) = TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Specialize.pure_start : ∀ {σs : List (Type u)} {φ : Prop} {H P T : Std.Do.SPred σs} [Std.Do.SPred.Tactic.PropAsSPredTautology φ H],
  φ → (P ∧ H ⊢ₛ T) → P ⊢ₛ T
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.CoproductDisjoint.nonempty_isInitial_of_ne : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {ι : Type u_1} {X : ι → C}
  [self : CategoryTheory.Limits.CoproductDisjoint X] {c : CategoryTheory.Limits.Cofan X}
  (hc : CategoryTheory.Limits.IsColimit c) {i j : ι},
  i ≠ j →
    ∀ (s : CategoryTheory.Limits.PullbackCone (c.inj i) (c.inj j)) (a : CategoryTheory.Limits.IsLimit s),
      Nonempty (CategoryTheory.Limits.IsInitial s.pt)
-- Init.Core
/-- Similar to `decide`, but uses an explicit instance  -/
toBoolUsing : {p : Prop} → Decidable p → Bool
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientWithinAt_congr_set' : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F} {s t : Set F} (y : F),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → (HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.ext_iff : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] {v₁ v₂ : Valuation R Γ₀},
  v₁ = v₂ ↔ ∀ (r : R), v₁ r = v₂ r
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.dist_tmul_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (x x' : E)
  (y y' : F), dist (x ⊗ₜ[𝕜] y) (x' ⊗ₜ[𝕜] y') ≤ ‖x‖ * ‖y‖ + ‖x'‖ * ‖y'‖
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aeval_def : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  (f : σ → S₁) (p : MvPolynomial σ R), (MvPolynomial.aeval f) p = MvPolynomial.eval₂ (algebraMap R S₁) f p
-- Init.Prelude
/-- Slower `Array.append` used in quotations.  -/
Array.appendCore : {α : Type u} → Array α → Array α → Array α
-- Mathlib.Data.Int.GCD
Nat.gcdB.eq_1 : ∀ (x y : ℕ), x.gcdB y = (x.xgcd y).2
-- Lean.Meta.Tactic.Grind.Internalize
Lean.Meta.Grind.updateIndicesFound : Lean.HeadIndex → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.condition_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (c : CategoryTheory.Limits.Cowedge F) {i j : J}
  (f : i ⟶ j) {Z : C} (h : c.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f.op).app i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π c i) h) =
    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π c j) h)
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S' : Solution'`, we may assume that `λ ^ 2` divides `S'.a + S'.b ∨ λ ^ 2` (see also the
result below).  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S' : FermatLastTheoremForThreeGen.Solution'✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  ∃ a' b',
    a' ^ 3 + b' ^ 3 =
        ↑(FermatLastTheoremForThreeGen.Solution'.u✝ S') * FermatLastTheoremForThreeGen.Solution'.c✝ S' ^ 3 ∧
      IsCoprime a' b' ∧ ¬hζ.toInteger - 1 ∣ a' ∧ ¬hζ.toInteger - 1 ∣ b' ∧ (hζ.toInteger - 1) ^ 2 ∣ a' + b'
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `s` is a monotone family of sets and `f` tends to `atTop` along a nontrivial filter,
then the indexed union of `s ∘ f` is equal to the indexed union of `s`.  -/
Monotone.iUnion_comp_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] {l : Filter α} [l.NeBot] {s : β → Set γ},
  Monotone s → ∀ {f : α → β}, Filter.Tendsto f l Filter.atTop → ⋃ a, s (f a) = ⋃ b, s b
-- Lean.Compiler.LCNF.Basic
/-- Universe level parameter names.
 -/
Lean.Compiler.LCNF.Signature.levelParams : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Signature pu → List Lean.Name
-- Init.Data.Iterators.Basic
/-- The wrapped iterator.

In the wrapper, its productivity is used as a termination measure.
 -/
Std.IterM.TerminationMeasures.Productive.it : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} → [inst : Std.Iterator α m β] → Std.IterM.TerminationMeasures.Productive α m → Std.IterM m β
-- Mathlib.RingTheory.Radical.Basic
EuclideanDomain.eq_divRadical : ∀ {E : Type u_1} [inst : EuclideanDomain E] [inst_1 : NormalizationMonoid E] [inst_2 : UniqueFactorizationMonoid E]
  {a x : E}, UniqueFactorizationMonoid.radical a * x = a → x = EuclideanDomain.divRadical a
-- Std.Data.Internal.List.Associative
Std.Internal.List.self_le_maxKey!_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {v : β k}, (compare k (Std.Internal.List.maxKey! (Std.Internal.List.insertEntryIfNew k v l))).isLE = true
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- A functor preserving larger filtered colimits also preserves smaller filtered colimits.  -/
CategoryTheory.Limits.preservesFilteredColimitsOfSize_of_univLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
  [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.LinearExpr.toArith : Array Lean.Expr → Lean.Meta.Simp.Arith.Nat.LinearExpr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Symmetrized
/-- The element of `SymAlg α` that represents `a : α`.  -/
SymAlg.sym : {α : Type u_1} → α ≃ αˢʸᵐ
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The projection `H^n(f) ⟶ opZ^n(f, g)` to the cokernel of `δ`.  -/
CategoryTheory.Abelian.SpectralObject.pOpcycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) → (n : ℤ) → (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f) ⟶ X.opcycles f g n
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.nndist_eq : ∀ {α : Type u_5} {β : Type u_6} {F : Type u_7} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x y : α),
  nndist (f x) (f y) = Dilation.ratio f * nndist x y
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.pow : ∀ {f : ℝ → ℝ} (p : ℕ),
  AkraBazziRecurrence.GrowsPolynomially f →
    (∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) → AkraBazziRecurrence.GrowsPolynomially fun x => f x ^ p
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.enorm_eq_iSup_enorm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β), ‖f‖ₑ = ⨆ x, ‖f x‖ₑ
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Build a `ModularForm Γ k` from any element of a type carrying a `ModularFormClass Γ k`
instance.  -/
ModularFormClass.modularForm : {F : Type u_1} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {k : ℤ} → [inst : FunLike F UpperHalfPlane ℂ] → [ModularFormClass F Γ k] → F → ModularForm Γ k
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : Group G] [inst_1 : SizeOf G] (toSubgroup : Subgroup G)
  (isNormal' : autoParam toSubgroup.Normal FiniteIndexNormalSubgroup.isNormal'._autoParam)
  (isFiniteIndex' : autoParam toSubgroup.FiniteIndex FiniteIndexNormalSubgroup.isFiniteIndex'._autoParam),
  sizeOf { toSubgroup := toSubgroup, isNormal' := isNormal', isFiniteIndex' := isFiniteIndex' } =
    1 + sizeOf toSubgroup + sizeOf isNormal' + sizeOf isFiniteIndex'
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
/-- If `P : MorphismProperty C` and `F : C ⥤ D`, then
`P.IsInvertedBy F` means that all morphisms in `P` are mapped by `F`
to isomorphisms in `D`.  -/
CategoryTheory.MorphismProperty.IsInvertedBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.MorphismProperty C → CategoryTheory.Functor C D → Prop
-- Lean.Meta.Basic
Lean.Meta.SavedState.mk : Lean.Core.SavedState → Lean.Meta.State → Lean.Meta.SavedState
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift_range : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (H' :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  Set.range
      ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.lift f g H').base) =
    ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base)
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_div_right : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] (a : G), IsOpenMap fun x => x / a
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.meromorphic_weierstrassP : ∀ (L : PeriodPair), Meromorphic L.weierstrassP
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.adjoin_rootSet_eq_range : ∀ {F : Type u} {K : Type v} (L : Type w) [inst : Field K] [inst_1 : Field L] [inst_2 : Field F] [inst_3 : Algebra K L]
  [inst_4 : Algebra K F] (f : Polynomial K) [Polynomial.IsSplittingField K L f] (i : L →ₐ[K] F),
  Algebra.adjoin K (f.rootSet F) = i.range
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pullback₁.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S T : C} (f f_1 : S ⟶ T) (e_f : f = f_1)
  (E E_1 : CategoryTheory.PreZeroHypercover T) (e_E : E = E_1)
  [inst_1 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (E.f i)],
  CategoryTheory.PreZeroHypercover.pullback₁ f E = CategoryTheory.PreZeroHypercover.pullback₁ f_1 E_1
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.map_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10} {S : Type u_11}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : AddCommMonoid S] [inst_6 : Module R M] [inst_7 : Module R N] [inst_8 : Module R S] [inst_9 : Module R P]
  [inst_10 : Module R Q] (f : M →ₗ[R] P) (g : N →ₗ[R] Q) (f' : S →ₗ[R] M) (x : TensorProduct R S N),
  (TensorProduct.map f g) ((LinearMap.rTensor N f') x) = (TensorProduct.map (f ∘ₗ f') g) x
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Status.intro.sizeOf_spec : sizeOf Mathlib.Explode.Status.intro = 1
-- Batteries.Data.List.Basic
/-- Auxliary definition used to define `toChunks`.
`toChunksAux n xs i` returns `(xs.take i, (xs.drop i).toChunks (n+1))`,
that is, the first `i` elements of `xs`, and the remaining elements chunked into
sublists of length `n+1`.  -/
List.toChunksAux : {α : Type u_1} → ℕ → List α → ℕ → List α × List (List α)