mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.List.Defs
/-- List of all permutations of `l`. This version of `permutations` is less efficient but has
simpler definitional equations. The permutations are in a different order,
but are equal up to permutation, as shown by `List.permutations_perm_permutations'`.

```
     permutations [1, 2, 3] =
       [[1, 2, 3], [2, 1, 3], [2, 3, 1],
        [1, 3, 2], [3, 1, 2], [3, 2, 1]]
```
 -/
List.permutations' : {α : Type u_1} → List α → List (List α)
-- Mathlib.Data.PNat.Prime
PNat.prime_five : PNat.Prime 5
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- If `x ≠ y` belong to the same closed ball, then the open segment with endpoints `x` and `y` is
included in the corresponding open ball.  -/
openSegment_subset_ball_of_ne : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y z : E} {r : ℝ},
  x ∈ Metric.closedBall z r → y ∈ Metric.closedBall z r → x ≠ y → openSegment ℝ x y ⊆ Metric.ball z r
-- Mathlib.Logic.Encodable.Basic
instCountablePNat : Countable ℕ+
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
/-- If `C` is an additive category, the forgetful functor `(C ⥤ₗ AddCommGroup) ⥤ (C ⥤ₗ Type v)` is
an equivalence.  -/
AddCommGrpCat.leftExactFunctorForgetEquivalence : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteBiproducts C] → C ⥤ₗ AddCommGrpCat ≌ C ⥤ₗ Type v
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.mul_nonneg : ∀ {d : ℕ} (a b : ℤ√↑d), 0 ≤ a → 0 ≤ b → 0 ≤ a * b
-- Lean.Elab.DefView
Lean.Elab.DefsParsedSnapshot.toSnapshot : Lean.Elab.DefsParsedSnapshot → Lean.Language.Snapshot
-- Mathlib.Topology.Order.IsLUB
Dense.isGLB_inter_iff : ∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {s t : Set α},
  Dense s → IsOpen t → ∀ {x : α}, IsGLB (t ∩ s) x ↔ IsGLB t x
-- Mathlib.Data.ENNReal.Basic
ENNReal.zero_ne_top : 0 ≠ ⊤
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictMonoOn.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [AddLeftStrictMono α], StrictMonoOn f s → ∀ (c : α), StrictMonoOn (fun x => c + f x) s
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_a_ne_zero' : ∀ {R : Type u_1} {a b c d : R} [inst : Semiring R], a ≠ 0 → { a := a, b := b, c := c, d := d }.toPoly.natDegree = 3
-- Mathlib.CategoryTheory.Sites.Whiskering
_private.Mathlib.CategoryTheory.Sites.Whiskering.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.eq_2 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (i : J.R) (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (match CategoryTheory.Limits.WalkingMulticospan.right i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right i => h_2 i) =
    h_2 i
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : β k → β k},
  (t.modify k f).getD k' fallback =
    if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).getD fallback
    else t.getD k' fallback
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofRealCLM_coe : ∀ {K : Type u_1} [inst : RCLike K], ↑RCLike.ofRealCLM = RCLike.ofRealAm.toLinearMap
-- Std.Time.Format.DateFormat
/-- Abbreviated month names (12 elements, index 0 = Jan).
 -/
Std.Time.DateFormatSymbols.monthShort : Std.Time.DateFormatSymbols → Vector String 12
-- Mathlib.Algebra.Group.Defs
AddMonoid.toNSMul : {M : Type u} → [self : AddMonoid M] → NSMul M
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.coe_one : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E], ⇑1 = id
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.modify_bind_get : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  (f : σ → σ),
  (do
      modify f
      get) =
    do
    let s ← get
    modify f
    pure (f s)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.text.sizeOf_spec : sizeOf Lean.Lsp.CompletionItemKind.text = 1
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.mk.inj : ∀ {α : Type u} {inst : BEq α} {inst_1 : Hashable α} {inner inner_1 : Std.ExtHashMap α Unit},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Identity map as an `AffineEquiv`.  -/
AffineEquiv.refl : (k : Type u_1) →
  (P₁ : Type u_2) →
    {V₁ : Type u_6} →
      [inst : Ring k] → [inst_1 : AddCommGroup V₁] → [inst_2 : Module k V₁] → [inst_3 : AddTorsor V₁ P₁] → P₁ ≃ᵃ[k] P₁
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.powerlt_aleph0_le : ∀ (c : Cardinal.{u_1}), c ^< Cardinal.aleph0 ≤ max c Cardinal.aleph0
-- Mathlib.RingTheory.Localization.Away.Lemmas
IsLocalization.Away.quotient_of_isIdempotentElem : ∀ {R : Type u_1} [inst : CommRing R] {e : R}, IsIdempotentElem e → IsLocalization.Away e (R ⧸ Ideal.span {1 - e})
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.Algebra.instLinearRestrictScalars : ∀ {R₀ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R₀] [inst_1 : Ring R] [inst_2 : Ring S]
  [inst_3 : Algebra R₀ R] [inst_4 : Algebra R₀ S] (f : R →ₐ[R₀] S),
  CategoryTheory.Functor.Linear R₀ (ModuleCat.restrictScalars f.toRingHom)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
linearIndepOn_id_pair : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x y : V},
  x ≠ 0 → (∀ (a : K), a • x ≠ y) → LinearIndepOn K id {x, y}
-- Batteries.Data.PairingHeap
/-- `O(n)`. Convert the heap to a list in arbitrary order.  -/
Batteries.PairingHeapImp.Heap.toListUnordered : {α : Type u_1} → Batteries.PairingHeapImp.Heap α → List α
-- Mathlib.Algebra.Order.Interval.Multiset
Multiset.map_add_right_Ioc : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Multiset.map (fun x => x + c) (Multiset.Ioc a b) = Multiset.Ioc (a + c) (b + c)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.hasLeftHomology_of_preserves' : ∀ {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.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [S.HasLeftHomology]
  [F.PreservesLeftHomologyOf S], (F.mapShortComplex.obj S).HasLeftHomology
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.ext : ∀ {ι : 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₁ b₂ : AffineBasis ι k P}, ⇑b₁ = ⇑b₂ → b₁ = b₂
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.cofan_inj_naturality_symm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  (Φ : S₁ ⟶ S₂) {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {Z : C}
  (h : S₂.X.obj Δ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((S₁.s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (Φ.F.app Δ) h) =
    CategoryTheory.CategoryStruct.comp (Φ.f (Opposite.unop A.fst).len)
      (CategoryTheory.CategoryStruct.comp ((S₂.s.cofan Δ).inj A) h)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
/-- `log` is operator concave.  -/
CFC.concaveOn_log : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  ConcaveOn ℝ {a | IsStrictlyPositive a} CFC.log
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- This property `HasRightKanExtension L F` holds when the functor `F` has a right
Kan extension along `L`.  -/
CategoryTheory.Functor.HasRightKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            CategoryTheory.Functor C D → CategoryTheory.Functor C H → Prop
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.inv_hom_whiskerRight_whiskerRight : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) (k : c ⟶ d),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.inv h) k)
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.hom h) k) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g h) k)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- **Alias** of `setOfPred_riemannianEDist_lt_subset_nhds`.

---

Any neighborhood of `x` contains all the points which are close enough to `x` for the
Riemannian distance, `ℝ≥0` version.  -/
setOf_riemannianEDist_lt_subset_nhds : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] [RegularSpace M] {x : M} {s : Set M},
  s ∈ nhds x → ∃ c > 0, {y | Manifold.riemannianEDist I x y < ↑c} ⊆ s
-- Lean.Meta.Tactic.Split
_private.Lean.Meta.Tactic.Split.0.Lean.Meta.Split.substDiscrEqs : Lean.MVarId → Lean.Meta.FVarSubst → Array Lean.FVarId → Lean.MetaM Lean.MVarId
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsIntegralHom
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryLE.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive :
            (x : Std.DTreeMap.Internal.Impl α fun x => β) →
              x.Ordered → (∃ a ∈ x, (compare a k).isLE = true) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, (compare a k).isLE = true) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β) →
                          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2
-- Mathlib.Order.UpperLower.Closure
upperClosure.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α), upperClosure s = { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }
-- Mathlib.CategoryTheory.Galois.Basic
/-- An object of a category `C` is connected if it is not initial
and has no non-trivial subobjects. Lenstra, 3.12.  -/
CategoryTheory.PreGaloisCategory.IsConnected : {C : Type u₁} → [CategoryTheory.Category.{u₂, u₁} C] → C → Prop
-- Mathlib.Data.Matrix.Mul
/-- Right multiplication by a matrix, as an `AddMonoidHom` from matrices to matrices.  -/
Matrix.addMonoidHomMulRight : {l : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} →
      {α : Type v} → [inst : NonUnitalNonAssocSemiring α] → [Fintype m] → Matrix m n α → Matrix l m α →+ Matrix l n α
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_add_nsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIcoDiv hp a (b + m • p) = toIcoDiv hp a b + ↑m
-- Mathlib.LinearAlgebra.Complex.Module
Complex.instAlgebraOfReal : {R : Type u_1} → [inst : CommSemiring R] → [Algebra R ℝ] → Algebra R ℂ
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.snd' : ∀ {e : ONote} {n : ℕ+} {a : ONote}, (e.oadd n a).NF → a.NFBelow e.repr
-- Mathlib.Tactic.Translate.Core
/-- `translations` stores all of the constants that have been tagged with this attribute,
and maps them to their translation.  -/
Mathlib.Tactic.Translate.TranslateData.translations : Mathlib.Tactic.Translate.TranslateData → Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo
-- Std.Http.Protocol.H1.Writer
/-- Writes the message headers to the output buffer.
 -/
_private.Std.Http.Protocol.H1.Writer.0.Std.Http.Protocol.H1.Writer.writeHeaders : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Message.Head dir.swap → Std.Http.Protocol.H1.Writer dir → Std.Http.Protocol.H1.Writer dir
-- Init.Data.Range.Polymorphic.Basic
Std.Rxo.LawfulHasSize.mk : ∀ {α : Type u} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [inst_2 : Std.Rxo.HasSize α],
  (∀ (lo hi : α), ¬lo < hi → Std.Rxo.HasSize.size lo hi = 0) →
    (∀ (lo hi : α), lo < hi → Std.PRange.succ? lo = none → Std.Rxo.HasSize.size lo hi = 1) →
      (∀ (lo hi lo' : α),
          lo < hi → Std.PRange.succ? lo = some lo' → Std.Rxo.HasSize.size lo hi = Std.Rxo.HasSize.size lo' hi + 1) →
        Std.Rxo.LawfulHasSize α
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.ofEven_comp_toEven : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), (CliffordAlgebra.ofEven Q).comp (CliffordAlgebra.toEven Q) = AlgHom.id R (CliffordAlgebra Q)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.size_eq_match_rcc : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.HasSize α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [Std.Rxc.IsAlwaysFinite α] [Std.Rxc.LawfulHasSize α],
  r.size =
    match Std.PRange.succ? r.lower with
    | none => 0
    | some next => (next...=r.upper).size
-- Mathlib.Topology.JacobsonSpace
subsingleton_image_closure_of_finite_of_isPreirreducible : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [JacobsonSpace X]
  {S : Set X},
  IsLocallyClosed S →
    IsPreirreducible S → Continuous f → IsClosedMap f → (f '' S).Finite → (f '' closure S).Subsingleton
-- Init.Tactics
/-- If true (default: false), then uses the native code compiler to evaluate the `Decidable` instance,
admitting the result via an axiom. This can be significantly more efficient,
but it is at the cost of increasing the trusted code base, namely the Lean compiler
and all definitions with an `@[implemented_by]` attribute.
The instance is only evaluated once. The `native_decide` tactic is a synonym for `decide +native`.  -/
Lean.Parser.Tactic.DecideConfig.native : Lean.Parser.Tactic.DecideConfig → Bool
-- Mathlib.Data.Set.Insert
Set.insert_ne_self : ∀ {α : Type u_1} {s : Set α} {a : α}, insert a s ≠ s ↔ a ∉ s
-- Init.Data.String.Lemmas.Splits
String.Slice.splits_startPos_iff : ∀ {t₁ t₂ : String} {s : String.Slice}, s.startPos.Splits t₁ t₂ ↔ t₁ = "" ∧ t₂ = s.copy
-- Lean.Elab.Binders
Lean.Elab.Term.expandWhereDecls : Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.getVert_injOn_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), Set.InjOn p.getVert {i | i ≤ p.length} ↔ p.IsPath
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeMapAux.eq_11 : ∀ {C : Type u} (T X₂ : CategoryTheory.FreeMonoidalCategory C) (f : T.Hom X₂)
  (W : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeMapAux (f.whiskerRight W) =
    CategoryTheory.Discrete.natTrans fun X =>
      W.normalizeObj'.map ((CategoryTheory.FreeMonoidalCategory.normalizeMapAux f).app X)
-- Mathlib.Topology.UniformSpace.Closeds
/-- **Alias** of `TopologicalSpace.Closeds.isClosed_setOfPred_totallyBounded`. -/
TopologicalSpace.Closeds.isClosed_setOf_totallyBounded : ∀ {α : Type u_1} [inst : UniformSpace α], IsClosed {s | TotallyBounded ↑s}
-- Mathlib.Data.Nat.Digits.Defs
Nat.ofDigits_append_zero : ∀ {b : ℕ} (l : List ℕ), Nat.ofDigits b (l ++ [0]) = Nat.ofDigits b l
-- Mathlib.Data.Nat.Factorial.Basic
Nat.lt_factorial_self : ∀ {n : ℕ}, 3 ≤ n → n < n.factorial
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivCongrLeft_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (l : α →₀ M),
  (Finsupp.equivCongrLeft f) l = Finsupp.equivMapDomain f l
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffWithinAt.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {ι : Type u_3} {f : ι → E → F} {s : Finset ι} {t : Set E} {x : E},
  (∀ i ∈ s, ContDiffWithinAt 𝕜 n (fun x => f i x) t x) → ContDiffWithinAt 𝕜 n (fun x => ∑ i ∈ s, f i x) t x
-- Mathlib.Order.SupIndep
sSupIndep_iff_pairwiseDisjoint : ∀ {α : Type u_1} [inst : Order.Frame α] {s : Set α}, sSupIndep s ↔ s.PairwiseDisjoint id
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_zero : Nat.primesBelow 0 = ∅
-- Mathlib.Algebra.Module.CharacterModule
/-- Given an abelian group homomorphism `f : A → B`, `f⋆(L) := L ∘ f` defines a linear map
from `B⋆` to `A⋆`.
 -/
CharacterModule.dual : {R : Type uR} →
  [inst : CommRing R] →
    {A : Type uA} →
      [inst_1 : AddCommGroup A] →
        {B : Type uB} →
          [inst_2 : AddCommGroup B] →
            [inst_3 : Module R A] → [inst_4 : Module R B] → (A →ₗ[R] B) → CharacterModule B →ₗ[R] CharacterModule A
-- Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
instCStarAlgebraContinuousLinearMapComplexIdOfCompleteSpace : {E : Type u_1} →
  [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℂ E] → [CompleteSpace E] → CStarAlgebra (E →L[ℂ] E)
-- Mathlib.Data.Multiset.Bind
Multiset.filter_bind : ∀ {α : Type u_1} {β : Type v} (m : Multiset α) (f : α → Multiset β) (p : β → Prop) [inst : DecidablePred p],
  Multiset.filter p (m.bind f) = m.bind fun a => Multiset.filter p (f a)
-- Mathlib.Algebra.Quandle
/-- A *unital shelf* is a shelf equipped with an element `1` such that, for all elements `x`,
we have both `x ◃ 1` and `1 ◃ x` equal `x`.
 -/
UnitalShelf : Type u → Type u
-- Mathlib.Algebra.Lie.Abelian
LieModule.ideal_oper_maxTrivSubmodule_eq_bot : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (I : LieIdeal R L), ⁅I, LieModule.maxTrivSubmodule R L M⁆ = ⊥
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι],
  RootPairing.GeckConstruction.cartanSubalgebra b ≤ RootPairing.GeckConstruction.lieAlgebra b
-- Mathlib.Algebra.Group.Center
Set.decidableMemCenter.eq_1 : ∀ {M : Type u_1} [inst : Semigroup M] [inst_1 : (a : M) → Decidable (∀ (b : M), b * a = a * b)] (x : M),
  Set.decidableMemCenter x = decidable_of_iff' (∀ (g : M), g * x = x * g) ⋯
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.innerDone : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m (Std.IterM m β)] [inst_1 : Std.Iterator α₂ m β]
  {it₁ : Std.IterM m (Std.IterM m β)} {it₂ : Std.IterM m β},
  it₂.IsPlausibleStep Std.IterStep.done →
    Std.Iterators.Types.Flatten.IsPlausibleStep { internalState := { it₁ := it₁, it₂ := some it₂ } }
      (Std.IterStep.skip { internalState := { it₁ := it₁, it₂ := none } })
-- Mathlib.Topology.Algebra.Ring.Real
ENNReal.instContinuousInv : ContinuousInv ENNReal
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.instInhabited : Inhabited Lean.Omega.LinearCombo
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H1Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupHomology.cycles A 1)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H1Iso A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.π A 1)) x) =
    (groupHomology.shortComplexH1 A).moduleCatToCycles.range.mkQ
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₁ A).hom) x)
-- Mathlib.Order.CompleteLattice.Basic
sInf_le_sInf_of_isCoinitialFor : ∀ {α : Type u_1} [inst : CompleteSemilatticeInf α] {s t : Set α}, IsCoinitialFor s t → sInf t ≤ sInf s
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
/-- This is the pointwise division of `ArithmeticFunction`s.  -/
ArithmeticFunction.pdiv : {R : Type u_1} → [inst : GroupWithZero R] → ArithmeticFunction R → ArithmeticFunction R → ArithmeticFunction R
-- Mathlib.Data.Sum.Lattice
Sum.Lex.instSemilatticeInf : {α : Type u_1} → {β : Type u_2} → [SemilatticeInf α] → [SemilatticeInf β] → SemilatticeInf (α ⊕ₗ β)
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_congr : ∀ {V : Type u} {G : SimpleGraph V} {W : Type u_4} {H : SimpleGraph W} (f : G ≃g H),
  G.chromaticNumber = H.chromaticNumber
-- Init.Data.Hashable
instHashableUInt32 : Hashable UInt32
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.toCompositionAsSet_boundaries : ∀ {n : ℕ} (c : Composition n), c.toCompositionAsSet.boundaries = c.boundaries
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.map_id : ∀ {R' : Type u} {M : Type v} [inst : CommSemiring R'] [inst_1 : AddCommMonoid M] [inst_2 : Module R' M]
  [inst_3 : Module R'ᵐᵒᵖ M] [inst_4 : IsCentralScalar R' M],
  TrivSqZeroExt.map LinearMap.id = AlgHom.id R' (TrivSqZeroExt R' M)
-- Mathlib.Topology.Category.TopCat.Opens
IsOpenMap.functor_faithful : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)), hf.functor.Faithful
-- Init.Data.Float.Model.Float32
/-- Converts a `Float32.Model` to an `Int16`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float32.Model.toInt16 : Float32.Model → Int16
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
/-- If `L/K` and `φ : L →+* ℂ`, then `IsMixed K φ` if `φ` is not mixed in `K`, i.e., `φ` is real
if and only if it's restriction to `K` is.

This is the complex embedding analogue of `InfinitePlace.IsUnramified K w`, where
`w : InfinitePlace L`. In this case there is an isomorphism between unmixed embeddings and
unramified infinite places.  -/
NumberField.ComplexEmbedding.IsUnmixed : (K : Type u_3) → {L : Type u_4} → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → (L →+* ℂ) → Prop
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.left_inr : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (g : G),
  (SemidirectProduct.inr g).left = 1