mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkDoneProgressReport.mk : String → Option String → Bool → Option ℕ → Lean.Lsp.WorkDoneProgressReport
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.flip₂₃_obj_obj_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (G : C₁) (k : C₃) (j : C₂),
  ((F.flip₂₃.obj G).obj k).obj j = ((F.obj G).obj j).obj k
-- Mathlib.Data.Seq.Computation
Computation.liftRel_pure_left : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (cb : Computation β),
  Computation.LiftRel R (Computation.pure a) cb ↔ ∃ b ∈ cb, R a b
-- Lean.Data.Json.Basic
/-- Assuming both inputs `o₁, o₂` are json objects, will compute `{...o₁, ...o₂}`.
If `o₁` is not a json object, `o₂` will be returned.
 -/
Lean.Json.mergeObj : Lean.Json → Lean.Json → Lean.Json
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_ofInt : ∀ (n : ℤ), Int64.ofBitVec (BitVec.ofInt 64 n) = Int64.ofInt n
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
CommMonCat.FilteredColimits.colimitCoconeIsColimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommMonCat),
  CommMonCat.FilteredColimits.colimitCoconeIsColimit F =
    CategoryTheory.Limits.isColimitOfReflects (CategoryTheory.forget₂ CommMonCat MonCat)
      (MonCat.FilteredColimits.colimitCoconeIsColimit (F.comp (CategoryTheory.forget₂ CommMonCat MonCat)))
-- Mathlib.FieldTheory.FinTrdeg
FinTrdeg.mk : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  (∃ E, E.FG ∧ Algebra.IsAlgebraic (↥E) L) → FinTrdeg K L
-- Mathlib.Algebra.CharP.Defs
/-- The exponential characteristic is a prime number or one.
See also `CharP.char_is_prime_or_zero`.  -/
expChar_is_prime_or_one : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (q : ℕ) [hq : ExpChar R q], Nat.Prime q ∨ q = 1
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.prependNode.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (z : Lean.PersistentHashMap.Zipper α β) (keys : Array α) (vals : Array β)
  (hsz : keys.size = vals.size),
  Lean.PersistentHashMap.Zipper.prependNode (Lean.PersistentHashMap.Node.collision keys vals hsz) z =
    Lean.PersistentHashMap.Zipper.consCollision (Std.Rii.Sliceable.mkSlice keys *...*)
      (Std.Rii.Sliceable.mkSlice vals *...*) ⋯ z
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Coreflective.toFull : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {L : CategoryTheory.Functor C D} [self : CategoryTheory.Coreflective L], L.Full
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.recvReady' : {m : Type → Type} →
  {α : Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Std.AtomicT (Std.CloseableChannel.Zero.State✝ α) m Bool
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forM.eq_1 : ∀ {α : Type u} {β : α → Type v} {m : Type w → Type w'} [inst : Monad m] (f : (a : α) → β a → m PUnit.{w + 1})
  (as : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.forM f as = Std.DHashMap.Internal.AssocList.foldlM (fun x => f) PUnit.unit as
-- Init.Data.List.ToArray
List.prod_toArray : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] (l : List α), l.toArray.prod = l.prod
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.Comon_EquivMon_OpOp_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.Comon.Comon_EquivMon_OpOp C).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x => CategoryTheory.Iso.refl ((CategoryTheory.Functor.id (CategoryTheory.Comon C)).obj x)) ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool} {k : α},
  (↑m).WF → (Std.DHashMap.Internal.Raw₀.filter f m).contains k = Option.any (f k) (m.get? k)
-- Mathlib.Probability.Process.Predictable
MeasureTheory.measurableSet_prodMk_add_one_of_predictable : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ℕ m} {s : Set (ℕ × Ω)},
  MeasurableSet s → ∀ (n : ℕ), MeasurableSet {ω | (n + 1, ω) ∈ s}
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint : ∀ {J : Type u_1} {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  (F : CategoryTheory.Functor C D) [F.IsRightAdjoint], CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.Algebra.Field.Defs
Rat.cast_def : ∀ {K : Type u_1} [inst : DivisionRing K] (q : ℚ), ↑q = ↑q.num / ↑q.den
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize_zero_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V], NormedSpace.normalize 0 = 0
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange : ∀ {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [W.IsStableUnderBaseChange]
  [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving W] [W.IsStableUnderComposition] [P.IsStableUnderBaseChange]
  [P.IsStableUnderComposition], (AlgebraicGeometry.sourceLocalClosure W P).IsStableUnderComposition
-- Init.Data.String.Lemmas.Basic
String.slice_endPos : ∀ {s : String} {p : s.Pos}, s.slice p s.endPos ⋯ = s.sliceFrom p
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
ContinuousMap.HomotopyEquiv.simplyConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [hY : SimplyConnectedSpace Y]
  (e : ContinuousMap.HomotopyEquiv X Y), SimplyConnectedSpace X
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.le_sum_nonempty_of_subadditive : ∀ {α : Type u_5} {β : Type u_6} [inst : AddMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β),
  (∀ (a b : α), f (a + b) ≤ f a + f b) → ∀ (l : List α), l ≠ ∅ → f l.sum ≤ (List.map f l).sum
-- Init.Data.SInt.Lemmas
Int32.toInt8_neg : ∀ (x : Int32), (-x).toInt8 = -x.toInt8
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.map_adjoin : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B] [inst_7 : StarRing B]
  [inst_8 : StarModule R A] [inst_9 : StarModule R B] (f : A →⋆ₐ[R] B) (s : Set A),
  StarSubalgebra.map f (StarAlgebra.adjoin R s) = StarAlgebra.adjoin R (⇑f '' s)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.measure_mono_null_ae : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s ≤ᵐ[μ] t → μ t = 0 → μ s = 0
-- Mathlib.Logic.Equiv.Prod
/-- A subtype of a `Prod` is equivalent to a sigma type whose fibers are subtypes.  -/
Equiv.subtypeProdEquivSigmaSubtype : {α : Type u_9} → {β : Type u_10} → (p : α → β → Prop) → { x // p x.1 x.2 } ≃ (a : α) × { b // p a b }
-- Std.Data.DHashMap.Raw
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.DHashMap.Raw.alter : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [Hashable α] → Std.DHashMap.Raw α β → (a : α) → (Option (β a) → Option (β a)) → Std.DHashMap.Raw α β
-- Mathlib.Topology.Inseparable
Union_closure_singleton_eq_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, ⋃ x ∈ s, closure {x} = s ↔ StableUnderSpecialization s
-- Lean.Declaration
Lean.instBEqRecursorRule.beq : Lean.RecursorRule → Lean.RecursorRule → Bool
-- Mathlib.Order.Compare
Ordering.Compares.ne_gt : ∀ {α : Type u_1} [inst : Preorder α] {o : Ordering} {a b : α}, o.Compares a b → (o ≠ Ordering.gt ↔ a ≤ b)
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.lift : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {X Y : C} →
      {inst_1 : Mathlib.Tactic.Coherence.LiftObj X} →
        {inst_2 : Mathlib.Tactic.Coherence.LiftObj Y} →
          (f : X ⟶ Y) →
            [self : Mathlib.Tactic.Coherence.LiftHom f] →
              Mathlib.Tactic.Coherence.LiftObj.lift X ⟶ Mathlib.Tactic.Coherence.LiftObj.lift Y
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.pos_at_place : ∀ {K : Type u_1} [inst : Field K] (x : (NumberField.RingOfIntegers K)ˣ) (w : NumberField.InfinitePlace K),
  0 < w ((algebraMap (NumberField.RingOfIntegers K) K) ↑x)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.ennrealToMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} {μ : MeasureTheory.VectorMeasure α ENNReal},
  (∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0) ↔ v.AbsolutelyContinuous μ
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.closure_subset_image : ∀ {α : Type ua} [inst : UniformSpace α] {U : SetRel α α}, U ∈ uniformity α → ∀ (s : Set α), closure s ⊆ U.image s
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.preimage_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (self : F.FullyFaithful) {X Y : C} (f : X ⟶ Y), self.preimage (F.map f) = f
-- Mathlib.Data.Finset.Sym
Finset.symInsertEquiv_apply_snd_coe : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α] {n : ℕ} (h : a ∉ s) (m : ↥((insert a s).sym n)),
  ↑((Finset.symInsertEquiv h) m).snd = (Sym.filterNe a ↑m).snd
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
/-- The pretriangulated structure on the opposite category of
a pretriangulated category. It is a scoped instance, so that we need to
`open CategoryTheory.Pretriangulated.Opposite` in order to be able
to use it: the reason is that it relies on the definition of the shift
on the opposite category `Cᵒᵖ`, for which it is unclear whether it should
be a global instance or not.  -/
CategoryTheory.Pretriangulated.Opposite.instOpposite : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.Pretriangulated Cᵒᵖ
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The map `I₁ × I₂ × I₃ → j` that is obtained using `TotalComplexShape c₁ c₂ c₁₂`
and `TotalComplexShape c₁₂ c₃ c` when `c₁ : ComplexShape I₁`, `c₂ : ComplexShape I₂`,
`c₃ : ComplexShape I₃`, `c₁₂ : ComplexShape I₁₂` and `c : ComplexShape J`.  -/
ComplexShape.r : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₃ : Type u_3} →
      {I₁₂ : Type u_4} →
        {J : Type u_6} →
          (c₁ : ComplexShape I₁) →
            (c₂ : ComplexShape I₂) →
              (c₃ : ComplexShape I₃) →
                (c₁₂ : ComplexShape I₁₂) →
                  (c : ComplexShape J) → [TotalComplexShape c₁ c₂ c₁₂] → [TotalComplexShape c₁₂ c₃ c] → I₁ × I₂ × I₃ → J
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.mono : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l l' : Filter α}, f =O[l'] g → l ≤ l' → f =O[l] g
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- Identity map as an affine map.  -/
AffineMap.id : (k : Type u_1) →
  {V1 : Type u_2} →
    (P1 : Type u_3) →
      [inst : Ring k] → [inst_1 : AddCommGroup V1] → [inst_2 : Module k V1] → [inst_3 : AddTorsor V1 P1] → P1 →ᵃ[k] P1
-- Mathlib.Algebra.Polynomial.BigOperators
/-- The degree of a product of polynomials is equal to
the sum of the degrees, where the degree of the zero polynomial is ⊥.
 -/
Polynomial.degree_multiset_prod : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] (t : Multiset (Polynomial R)) [Nontrivial R],
  t.prod.degree = (Multiset.map (fun f => f.degree) t).sum
-- Init.Data.UInt.Bitwise
USize.toFin_shiftRight : ∀ (a b : USize), b.toNat < System.Platform.numBits → (a >>> b).toFin = a.toFin >>> b.toFin
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
/-- `f` is continuously differentiable if it is continuously
differentiable at each `x ∈ tsupport f`. See also `contMDiff_section_of_tsupport`
for a similar result for sections of vector bundles.  -/
contMDiff_of_tsupport : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  [inst_11 : Zero M'] {f : M → M'}, (∀ x ∈ tsupport f, ContMDiffAt I I' n f x) → ContMDiff I I' n f
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum may be split into such sums over two subsets.  -/
Finset.weightedVSubOfPoint_sdiff : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) [inst_3 : DecidableEq ι] {s₂ : Finset ι},
  s₂ ⊆ s →
    ∀ (w : ι → k) (p : ι → P) (b : P),
      ((s \ s₂).weightedVSubOfPoint p b) w + (s₂.weightedVSubOfPoint p b) w = (s.weightedVSubOfPoint p b) w
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff.eq_1 : ∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.leadingCoeff f = MvPolynomial.coeff (m.degree f) f
-- Mathlib.Order.KrullDimension
Order.krullDim_pos_iff_of_orderTop : ∀ {α : Type u_3} [inst : PartialOrder α] [OrderTop α], 0 < Order.krullDim α ↔ Nontrivial α
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_of_retract : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L K' L' : HomologicalComplex C c}
  {f : K ⟶ L} {f' : K' ⟶ L'} (h : CategoryTheory.RetractArrow f f') (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] [inst_4 : K'.HasHomology i] [inst_5 : L'.HasHomology i] [hf' : QuasiIsoAt f' i],
  QuasiIsoAt f i
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.isLocalHom_expand : ∀ (R : Type u) [inst : CommRing R] [IsDomain R] {p : ℕ}, 0 < p → IsLocalHom (Polynomial.expand R p)
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- The tensor product of a pair of linear maps between modules.  -/
RingTheory.LinearMap.«term_⊗ₘ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.exists_iff_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {p : G₀ → Prop}, (∃ u, p ↑u) ↔ ∃ x, x ≠ 0 ∧ p x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.nodup_tail_support_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.reverse.support.tail.Nodup ↔ p.support.tail.Nodup
-- Batteries.Data.List.Perm
List.Subperm.exists_of_length_lt : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Subperm l₂ → l₁.length < l₂.length → ∃ a, (a :: l₁).Subperm l₂
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Express `f n` as `f 0` multiplied by the telescoping product of consecutive ratios from
`0` to `n - 1`.  -/
Finset.eq_prod_range_div : ∀ {G : Type u_3} [inst : CommGroup G] (f : ℕ → G) (n : ℕ), f n = f 0 * ∏ i ∈ Finset.range n, f (i + 1) / f i
-- Mathlib.Algebra.Squarefree.Basic
Int.squarefree_natCast : ∀ {n : ℕ}, Squarefree ↑n ↔ Squarefree n
-- Init.Data.Array.Lemmas
Array.mem_toList_iff : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs.toList ↔ a ∈ xs
-- Init.Data.Option.Monadic
Option.forIn_some : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] (a : α) (b : β)
  (f : α → β → m (ForInStep β)),
  forIn (some a) b f = do
    let r ← f a b
    pure r.value
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instCentroidHomClass : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α], CentroidHomClass (CentroidHom α) α
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesWithinAt.fderivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {f : E → F} {x : E} {s : Set E},
  HasFPowerSeriesWithinAt f p s x →
    UniqueDiffWithinAt 𝕜 (insert x s) x → fderivWithin 𝕜 f (insert x s) x = (continuousMultilinearCurryFin1 𝕜 E F) (p 1)
-- Mathlib.GroupTheory.OrderOfElement
/-- See also `Nat.card_zmultiples`.  -/
Fintype.card_zmultiples : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : Fintype G] {x : G},
  Fintype.card ↥(AddSubgroup.zmultiples x) = addOrderOf x
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.maximumIndepSet_card_eq_indepNum : ∀ {α : Type u_3} {G : SimpleGraph α} [inst : Finite α] (t : Finset α), G.IsMaximumIndepSet t → t.card = G.indepNum
-- Mathlib.LinearAlgebra.Multilinear.DirectSum
/-- Two multilinear maps from direct sums are equal if they agree on the generators.  -/
MultilinearMap.directSum_ext : ∀ {R : Type u_1} {ι : Type u_2} {M' : Type u_3} {κ : ι → Type u_4} {M : (i : ι) → κ i → Type u_5}
  [inst : CommSemiring R] [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)]
  [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)] [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] [Finite ι]
  [inst_6 : (i : ι) → DecidableEq (κ i)] ⦃f g : MultilinearMap R (fun i => DirectSum (κ i) fun j => M i j) M'⦄,
  (∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => DirectSum.lof R (κ i) (M i) (p i)) =
        g.compLinearMap fun i => DirectSum.lof R (κ i) (M i) (p i)) →
    f = g
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
ContMDiffMap.mdifferentiable : ∀ {𝕜 : 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 : ContMDiffMap I I' M M' ↑⊤),
  MDiff ⇑f
-- Init.Data.Option.Lemmas
Option.isSome_eq_isSome : ∀ {α : Type u_1} {x : Option α} {α_1 : Type u_2} {y : Option α_1}, x.isSome = y.isSome ↔ (x = none ↔ y = none)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RooSliceData.treeMap : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RooSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.degree_prod_of_monic : ∀ {R : Type u} {ι : Type w} (s : Finset ι) [inst : CommSemiring R] (f : ι → Polynomial R) [Nontrivial R],
  (∀ i ∈ s, (f i).Monic) → (∏ i ∈ s, f i).degree = ∑ i ∈ s, (f i).degree
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_sSup : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R A)), (sSup S).op = sSup (Subalgebra.unop ⁻¹' S)
-- Std.Sync.Channel
/-- Whether the channel is closed already.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Bounded.State.closed : {α : Type} → Std.CloseableChannel.Bounded.State✝ α → Bool
-- Init.Data.Array.Monadic
Array.mapM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β}
  {xs ys : Array α},
  Array.mapM f (xs ++ ys) = do
    let __do_lift ← Array.mapM f xs
    let __do_lift_1 ← Array.mapM f ys
    pure (__do_lift ++ __do_lift_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.whiskerRight_right : ∀ {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.Limits.CatCospanTransformMorphism.whiskerRight α φ).right =
    CategoryTheory.Functor.whiskerRight α.right φ.right
-- Mathlib.LinearAlgebra.Finsupp.Pi
LinearMap.splittingOfFunOnFintypeSurjective_splits : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_5}
  [inst_3 : Finite α] (f : M →ₗ[R] α → R) (s : Function.Surjective ⇑f),
  f ∘ₗ f.splittingOfFunOnFintypeSurjective s = LinearMap.id
-- Init.Core
Lean.Syntax.ident.injEq : ∀ (info : Lean.SourceInfo) (rawVal : Substring.Raw) (val : Lean.Name) (preresolved : List Lean.Syntax.Preresolved)
  (info_1 : Lean.SourceInfo) (rawVal_1 : Substring.Raw) (val_1 : Lean.Name)
  (preresolved_1 : List Lean.Syntax.Preresolved),
  (Lean.Syntax.ident info rawVal val preresolved = Lean.Syntax.ident info_1 rawVal_1 val_1 preresolved_1) =
    (info = info_1 ∧ rawVal = rawVal_1 ∧ val = val_1 ∧ preresolved = preresolved_1)
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
isSymmSndFDerivWithinAt_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  IsSymmSndFDerivWithinAt 𝕜 f Set.univ x ↔ IsSymmSndFDerivAt 𝕜 f x
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.inter_vsub_union_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s₁ s₂ t₁ t₂ : Set β}, s₁ ∩ s₂ -ᵥ (t₁ ∪ t₂) ⊆ s₁ -ᵥ t₁ ∪ (s₂ -ᵥ t₂)
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set_union : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t s' t' : Set α}, s =ᵐ[μ] t → s' =ᵐ[μ] t' → s ∪ s' =ᵐ[μ] t ∪ t'
-- Batteries.Lean.Except
_private.Batteries.Lean.Except.0.Except.map.match_1.eq_1 : ∀ {ε : Type u_1} {α : Type u_2} (motive : Except ε α → Sort u_3) (err : ε) (h_1 : (err : ε) → motive (Except.error err))
  (h_2 : (v : α) → motive (Except.ok v)),
  (match Except.error err with
    | Except.error err => h_1 err
    | Except.ok v => h_2 v) =
    h_1 err
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given a type `ι`, this is the shape of multiequalizer diagrams corresponding
to situations where we want to equalize two families of maps `U i ⟶ V ⟨i, j⟩`
and `U j ⟶ V ⟨i, j⟩` with `i : ι` and `j : ι`.  -/
CategoryTheory.Limits.MulticospanShape.prod : Type w → CategoryTheory.Limits.MulticospanShape