mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
/-- If a function is `C^m` within a set at a point, for some finite `m`, then it is `C^m` within
this set on a neighborhood of the basepoint.  -/
ContMDiffWithinAt.contMDiffOn : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {m n : WithTop ℕ∞} [IsManifold I n M] [IsManifold I' n M'],
  m ≤ n →
    (m = ↑⊤ → n = ⊤) →
      ContMDiffWithinAt I I' n f s x → ∃ u ∈ nhdsWithin x (insert x s), u ⊆ insert x s ∧ ContMDiffOn I I' m f u
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.le_mk_iff_exists_set : ∀ {c : Cardinal.{u}} {α : Type u}, c ≤ Cardinal.mk α ↔ ∃ p, Cardinal.mk ↑p = c
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).max ⋯ = t.max?.elim k fun k' => if cmp k' k = Ordering.lt then k else k'
-- Mathlib.Topology.ContinuousOn
continuousOn_pi' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_5} {X : ι → Type u_6}
  [inst_1 : (i : ι) → TopologicalSpace (X i)] {f : α → (i : ι) → X i} {s : Set α},
  (∀ (i : ι), ContinuousOn (fun y => f y i) s) → ContinuousOn f s
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instReprLambdaTheoremArgs.repr : Mathlib.Meta.FunProp.LambdaTheoremArgs → ℕ → Std.Format
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.image : ∀ {G : Type u_1} [inst : AddGroup G] {A : Set G} {K : ℝ} {F : Type u_2} {H : Type u_3} [inst_1 : AddGroup H]
  [inst_2 : FunLike F G H] [AddMonoidHomClass F G H] (f : F),
  IsApproximateAddSubgroup K A → IsApproximateAddSubgroup K (⇑f '' A)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {he : Std.DTreeMap.Internal.Impl.contains t.maxKey! t = true}, t.getKey t.maxKey! he = t.maxKey!
-- Init.Data.UInt.Lemmas
USize.toBitVec_add : ∀ {a b : USize}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.mk.inj : ∀ {S : Type u_2} {M : Type u_3} {inst : Add M} {inst_1 : SMul S M} {toAddCon : AddCon M}
  {smul : ∀ (s : S) {x y : M}, toAddCon.toSetoid x y → toAddCon.toSetoid (s • x) (s • y)} {toAddCon_1 : AddCon M}
  {smul_1 : ∀ (s : S) {x y : M}, toAddCon_1.toSetoid x y → toAddCon_1.toSetoid (s • x) (s • y)},
  { toAddCon := toAddCon, smul := smul } = { toAddCon := toAddCon_1, smul := smul_1 } → toAddCon = toAddCon_1
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
/-- polynomial functor representation of a dependent product  -/
MvQPF.Pi.P : {n : ℕ} → {A : Type u} → (F : A → TypeVec.{u} n → Type u) → [(α : A) → MvQPF (F α)] → MvPFunctor.{u} n
-- Std.Time.Date.Unit.Week
/-- Convert `Week.Offset` into `Second.Offset`.
 -/
Std.Time.Week.Offset.toSeconds : Std.Time.Week.Offset → Std.Time.Second.Offset
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Example: the **full shift** on alphabet `A` over the multiplicative monoid `G`.
It is the subshift whose underlying set is the set of all configurations
`G → A`.  -/
SymbolicDynamics.FullShift.mulFullShift : (A : Type u_1) →
  (G : Type u_2) → [inst : TopologicalSpace A] → [inst_1 : Monoid G] → SymbolicDynamics.FullShift.MulSubshift A G
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Int.addLeft_one_isCycle : (Equiv.addLeft 1).IsCycle
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.nil_ne_cons : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) (e : b ⟶ a), Quiver.Path.nil ≠ p.cons e
-- Mathlib.Data.Multiset.Filter
Multiset.mem_filter : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α}, a ∈ Multiset.filter p s ↔ a ∈ s ∧ p a
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM.run : {α : Type} → Aesop.ExtractScriptM α → Aesop.TreeM (Aesop.Script.UScript × Bool)
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `*` is a semigroup, if it admits an injective map that preserves `*` to
a semigroup. See note [reducible non-instances].  -/
Function.Injective.semigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : Semigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → Semigroup M₁
-- Mathlib.Order.CompleteLattice.Defs
/-- `aᶜ` is defined as `a ⇨ ⊥`  -/
CompleteLinearOrder.himp_bot : ∀ {α : Type u_8} [self : CompleteLinearOrder α] (a : α), a ⇨ ⊥ = aᶜ
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_mk : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : ContinuousMultilinearMap R (fun x => M) N)
  (h : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → f.toFun v = 0),
  ⇑{ toContinuousMultilinearMap := f, map_eq_zero_of_eq' := h } = ⇑f
-- Mathlib.Data.Set.Countable
Set.Countable.sUnion_iff : ∀ {α : Type u} {s : Set (Set α)}, s.Countable → ((⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable)
-- Mathlib.Algebra.Order.Field.Basic
Monotone.div_const : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {β : Type u_4} [inst_3 : Preorder β]
  {f : β → α}, Monotone f → ∀ {c : α}, 0 ≤ c → Monotone fun x => f x / c