mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k)
-- Mathlib.Order.Interval.Basic
NonemptyInterval.map_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : NonemptyInterval α),
  (NonemptyInterval.map f a).toProd.1 = f a.1.1
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_lt_zero : ∀ {K : Type u_1} [inst : RCLike K] {x : ℝ}, ↑x < 0 ↔ x < 0
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- The exponents of the Cantor normal form are decreasing.  -/
Ordinal.CNF.sortedGT : ∀ (b o : Ordinal.{u_1}), (List.map Prod.fst (Ordinal.CNF b o)).SortedGT
-- Mathlib.Tactic.FieldSimp
/-- Given a field-simp-normal-form expression `L` (a product of powers of atoms), a proof (according
to the value of `DenomCondition`) of that expression's nonzeroness, strict positivity, etc.  -/
Mathlib.Tactic.FieldSimp.DenomCondition.proof : {v : Lean.Level} →
  {M : Q(Type v)} →
    {iM : Q(GroupWithZero «$M»)} → Mathlib.Tactic.FieldSimp.qNF M → Mathlib.Tactic.FieldSimp.DenomCondition iM → Type
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instModule : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      {R : Type u_5} →
        [inst_1 : Semiring R] → [inst_2 : AddCommMonoid Y] → [Module R Y] → Module R (LocallyConstant X Y)
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csInf_add : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M]
  {s t : Set M}, s.Nonempty → BddBelow s → t.Nonempty → BddBelow t → sInf (s + t) = sInf s + sInf t
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instCommRing : {R : Type u_1} → {a b : R} → [CommRing R] → CommRing (QuadraticAlgebra R a b)
-- Mathlib.Algebra.Algebra.Hom
Algebra.ofId_self : ∀ {R : Type u} [inst : CommSemiring R], Algebra.ofId R R = AlgHom.id R R
-- Std.Data.DTreeMap.Raw.Lemmas
/-- A variant of `contains_of_contains_insertMany_list` used in `get_insertMany_list`.  -/
Std.DTreeMap.Raw.Const.contains_of_contains_insertMany_list' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α},
      (Std.DTreeMap.Raw.Const.insertMany t l).contains k = true →
        List.findSomeRev?
              (fun x =>
                match x with
                | (a, b) => if cmp a k = Ordering.eq then some b else none)
              l =
            none →
          t.contains k = true
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.symmetrifyCostar : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) (u : U),
  φ.symmetrify.costar u =
    ⇑(Quiver.symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ ⇑(Quiver.symmetrifyCostar u)
-- Mathlib.LinearAlgebra.Span.Basic
/-- A version of `Submodule.map_span_le` that does not require the `RingHomSurjective`
assumption.  -/
Submodule.image_span_subset : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  (f : M →ₛₗ[σ₁₂] M₂) (s : Set M) (N : Submodule R₂ M₂), ⇑f '' ↑(Submodule.span R s) ⊆ ↑N ↔ ∀ m ∈ s, f m ∈ N
-- Mathlib.RingTheory.Ideal.Quotient.Noetherian
Ideal.Quotient.isNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (I : Ideal R), IsNoetherianRing (R ⧸ I)
-- Mathlib.Logic.Equiv.Set
Equiv.Set.image_symm_preimage : ∀ {α : Type u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) (u s : Set α),
  (fun x => ↑((Equiv.Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' f '' u
-- Std.Data.HashSet.Lemmas
Std.HashSet.forall_mem_toArray_iff_forall_mem_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {p : α → Prop},
  (∀ k ∈ m.toArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.get k h)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.isCharNeTwoNF_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.IsCharNeTwoNF
-- Lean.Elab.Tactic.Rewrite
_private.Lean.Elab.Tactic.Rewrite.0.Lean.Elab.Tactic.elabRewriteConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Meta.Rewrite.Config
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Basic.0.SimplexCategory.mkOfLe.match_1.eq_2 : ∀ (motive : Fin (1 + 1) → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_2 ()
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_C_mul_X : ∀ {R : Type u} {a : R} [inst : Semiring R], a ≠ 0 → (Polynomial.C a * Polynomial.X).degree = 1
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
aestronglyMeasurable_const_smul_iff₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} {G₀ : Type u_7} [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ β] [ContinuousConstSMul G₀ β] {c : G₀},
  c ≠ 0 → (MeasureTheory.AEStronglyMeasurable (fun x => c • f x) μ ↔ MeasureTheory.AEStronglyMeasurable f μ)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.MonadShareCommon.share1 : {m : Type → Type} → [self : Lean.Meta.Sym.Internal.MonadShareCommon m] → Lean.Expr → m Lean.Expr
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_succ_apply_left : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : ℕ} (m : Fin (n + 1) → E),
  (iteratedFDerivWithin 𝕜 (n + 1) f s x) m = ((fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s x) (m 0)) (Fin.tail m)
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Ico_add_one_add_one_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Add α]
  [SuccAddOrder α] [NoMaxOrder α] (a b : α), Finset.Ico (a + 1) (b + 1) = Finset.Ioc a b
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.coe_ofContinuousOpenRestrict_symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap (e.source.domRestrict ↑e)),
  ↑(PartialHomeomorph.ofContinuousOpenRestrict e hc ho).symm = ↑e.symm
-- Mathlib.Order.Filter.Ultrafilter.Defs
Ultrafilter.comap_inf_principal_neBot_of_image_mem : ∀ {α : Type u} {β : Type v} {m : α → β} {s : Set α} {g : Ultrafilter β},
  m '' s ∈ g → (Filter.comap m ↑g ⊓ Filter.principal s).NeBot
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxi.Iterator.instLawfulDeterministicIterator : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α], Std.LawfulDeterministicIterator (Std.Rxi.Iterator α) Id
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prodComparison_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{w, u₂} D]
  (F : CategoryTheory.Functor C D) (A B : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct A B]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct (F.obj A) (F.obj B)] {Z : D} (h : F.obj B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.prod.snd) h
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.isClopen' : ∀ {α : Type u_4} [inst : TopologicalSpace α] (self : TopologicalSpace.Clopens α), IsClopen self.carrier
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.algebraMap_smul : ∀ {R : Type u} (A : Type w) {M : Type v₁} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : MulAction A M] [inst_4 : SMul R M] [IsScalarTower R A M] (r : R) (x : M), (algebraMap R A) r • x = r • x
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_uIcc : ∀ {n : ℕ} (i j : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.uIcc i j) = Finset.uIcc i.rev j.rev
-- Mathlib.RingTheory.Spectrum.Maximal.Localization
PrimeSpectrum.mapPiLocalization_bijective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  Function.Bijective ⇑f → Function.Bijective ⇑(PrimeSpectrum.mapPiLocalization f)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
measurable_natCast : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : NatCast α] (n : ℕ),
  Measurable ↑n
-- Mathlib.Geometry.Manifold.Immersion
/-- A `C^n` immersion is `C^n`.  -/
Manifold.IsImmersion.contMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsImmersion I J n f → ContMDiff I J n f
-- Mathlib.Algebra.Group.Defs
SubNegZeroMonoid.mk : {G : Type u_2} → [toSubNegMonoid : SubNegMonoid G] → -0 = 0 → SubNegZeroMonoid G
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_sub : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f g : NormedAddGroupHom V₁ V₂), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.radical_le_iff : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, J.IsPrime → (I.radical ≤ J ↔ I ≤ J)
-- Mathlib.Control.Bitraversable.Instances
_private.Mathlib.Control.Bitraversable.Instances.0.Prod.bitraverse.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α × β → Sort u_3) (x : α) (y : β) (h_1 : (x : α) → (y : β) → motive (x, y)),
  (match (x, y) with
    | (x, y) => h_1 x y) =
    h_1 x y
-- Mathlib.LinearAlgebra.CrossProduct
cross_self : ∀ {R : Type u_1} [inst : CommRing R] (v : Fin 3 → R), (crossProduct v) v = 0
-- Mathlib.Tactic.NormNum.NatFib
Mathlib.Meta.NormNum.isFibAux_one : Mathlib.Meta.NormNum.IsFibAux 1 1 1
-- Init.Data.Rat.Lemmas
Rat.add_le_add_right : ∀ {a b c : ℚ}, a + c ≤ b + c ↔ a ≤ b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulRightStrictMono_of_mulRightReflectLE : ∀ (N : Type u_2) [inst : Mul N] [inst_1 : LinearOrder N] [MulRightReflectLE N], MulRightStrictMono N
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.getDeclFor? : Lean.ParserCompiler.CombinatorAttribute → Lean.Environment → Lean.Name → Option Lean.Name
-- Init.NotationExtra
/-- Unexpander for the `{ x, y, ... }` notation.  -/
Lean.insertUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.Control.Fold
Traversable.foldl_map : ∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] (g : β → γ) (f : α → γ → α)
  (a : α) (l : t β), Traversable.foldl f a (g <$> l) = Traversable.foldl (fun x y => f x (g y)) a l
-- Mathlib.Analysis.MeanInequalities
/-- **Minkowski inequality**: the `L_p` seminorm of the infinite sum of two vectors is less than or
equal to the infinite sum of the `L_p`-seminorms of the summands, if these infinite sums both
exist. A version for `ℝ`-valued functions. For an alternative version, convenient if the infinite
sums are not already expressed as `p`-th powers, see `Lp_add_le_tsum_of_nonneg`.  -/
Real.Lp_add_le_hasSum_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p : ℝ},
  1 ≤ p →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        ∀ {A B : ℝ},
          0 ≤ A →
            0 ≤ B →
              HasSum (fun i => f i ^ p) (A ^ p) →
                HasSum (fun i => g i ^ p) (B ^ p) → ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
-- Init.MetaTypes
/-- Unfolds reducible constants and constants tagged with `@[instance_reducible]` (e.g. type
class instances). Does *not* unfold `[implicit_reducible]`.  -/
Lean.Meta.TransparencyMode.instances : Lean.Meta.TransparencyMode
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteComposition.instIsMultiplicative : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C)
  [W.IsStableUnderTransfiniteComposition], W.IsMultiplicative
-- Mathlib.Topology.Bornology.Absorbs
/-- **Alias** of the forward direction of `absorbs_iff_eventually_cobounded_mapsTo`. -/
eventually_cobounded_mapsTo : ∀ {G₀ : Type u_1} {α : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Bornology G₀] [inst_2 : MulAction G₀ α]
  {s t : Set α}, Absorbs G₀ s t → ∀ᶠ (c : G₀) in Bornology.cobounded G₀, Set.MapsTo (fun x => c⁻¹ • x) t s
-- Mathlib.Geometry.Manifold.Immersion
/-- Given `C^n` manifolds `M` and `N` over the same model `I`,
`Sum.inr : N → M ⊕ N` is a `C^n` immersion with complement `Unit`  -/
Manifold.IsImmersionOfComplement.sumInr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_15}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'] [IsManifold I n M] [IsManifold I n M'],
  Manifold.IsImmersionOfComplement Unit I I n Sum.inr
-- Mathlib.Data.Finset.Insert
Finset.not_nontrivial_empty : ∀ {α : Type u_1}, ¬∅.Nontrivial
-- Mathlib.Order.Bounds.Basic
isGLB_pair : ∀ {γ : Type u_3} [inst : SemilatticeInf γ] {a b : γ}, IsGLB {a, b} (a ⊓ b)
-- Init.Grind.AC
Lean.Grind.AC.simp_ac_cert : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Algebra.Group.Equiv.Opposite
AddOpposite.opAddEquiv_symm_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : Mᵃᵒᵖ), AddOpposite.opAddEquiv.symm a = AddOpposite.unop a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSlice.instToIterator : {α : Type u_1} →
  [inst : Ord α] →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RocSliceData α)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxcIterator α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure b.fst)
      α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.contains_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k k' : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).contains k' = t.contains k'
-- Std.Data.HashMap.Lemmas
Std.HashMap.nodup_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keys.Nodup
-- Mathlib.Topology.Homeomorph.Lemmas
/-- Homeomorphism between dependent functions `Π i : Fin 2, X i` and `X 0 × X 1`.  -/
Homeomorph.piFinTwo : (X : Fin 2 → Type u) → [inst : (i : Fin 2) → TopologicalSpace (X i)] → ((i : Fin 2) → X i) ≃ₜ X 0 × X 1
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Presieve.presieve₀_preZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (R : CategoryTheory.Presieve S),
  R.preZeroHypercover.presieve₀ = R
-- Mathlib.Data.Set.Inclusion
Set.inclusion_comp_inclusion : ∀ {α : Type u_2} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u), Set.inclusion htu ∘ Set.inclusion hst = Set.inclusion ⋯
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.instUniformSpace : {R : Type u_3} → {M : Type u_4} → [UniformSpace R] → [UniformSpace M] → UniformSpace (TrivSqZeroExt R M)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
ContinuousLinearMap.coe_toContinuousLinearEquivOfDetNeZero : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E]
  [inst_5 : CompleteSpace 𝕜] [inst_6 : T2Space E] [inst_7 : FiniteDimensional 𝕜 E] (f : E →L[𝕜] E) (hf : f.det ≠ 0),
  ↑(f.toContinuousLinearEquivOfDetNeZero hf) = f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.nonsingular_neg : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  W.Nonsingular P → W.Nonsingular (W.neg P)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_insert_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] {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}
  {n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f (insert x s) x ↔ ContMDiffWithinAt I I' n f s x
-- Mathlib.AlgebraicTopology.DoldKan.FunctorN
/-- The canonical isomorphism `toKaroubi (SimplicialObject C) ⋙ N₂ ≅ N₁`.  -/
AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (CategoryTheory.Idempotents.toKaroubi (CategoryTheory.SimplicialObject C)).comp AlgebraicTopology.DoldKan.N₂ ≅
        AlgebraicTopology.DoldKan.N₁
-- Init.Data.UInt.Lemmas
UInt8.eq_of_toFin_eq : ∀ {a b : UInt8}, a.toFin = b.toFin → a = b
-- Mathlib.RingTheory.FreeRing
FreeRing.map_of : ∀ {α : Type u} {β : Type v} (f : α → β) (x : α), (FreeRing.map f) (FreeRing.of x) = FreeRing.of (f x)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- If `edist (f n) (f (n+1))` is bounded above by a function `d : ℕ → ℝ≥0∞`,
then the distance from `f n` to the limit is bounded by `∑'_{k=n}^∞ d k`.  -/
edist_le_tsum_of_edist_le_of_tendsto : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal),
  (∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) →
    ∀ {a : α}, Filter.Tendsto f Filter.atTop (nhds a) → ∀ (n : ℕ), edist (f n) a ≤ ∑' (m : ℕ), d (n + m)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.coind_comp_friend_right.match_1_1.eq_2 : ∀ {α : Type u_1} (motive : Option (α × Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) → Sort u_2) (hd : α)
  (opf' : Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) (h_1 : Unit → motive none)
  (h_2 : (hd : α) → (opf' : Subtype Tactic.ComputeAsymptotics.Seq.FriendlyOperation) → motive (some (hd, opf'))),
  (match some (hd, opf') with
    | none => h_1 ()
    | some (hd, opf') => h_2 hd opf') =
    h_2 hd opf'
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise
SubMulAction.mem_one : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : MulAction R M] [inst_2 : One M] {x : M},
  x ∈ 1 ↔ ∃ r, r • 1 = x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp},
  Array.map Prod.fst t.toArray = t.keysArray
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.span_eq_top : ∀ {ι : 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.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] [P.IsIrreducible],
  Submodule.span R {RootPairing.EmbeddedG2.longRoot P, RootPairing.EmbeddedG2.shortRoot P} = ⊤
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Complex.hasStrictDerivAt_tan : ∀ {x : ℂ}, Complex.cos x ≠ 0 → HasStrictDerivAt Complex.tan (1 / Complex.cos x ^ 2) x
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The residue of `ζ(s)` at `s = 1` is equal to 1.  -/
riemannZeta_residue_one : Filter.Tendsto (fun s => (s - 1) * riemannZeta s) (nhdsWithin 1 {1}ᶜ) (nhds 1)
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
/-- (Implementation detail): Realisation of a `FGAlgCatSkeleton`.  -/
FGAlgCatSkeleton.eval : (R : Type u) → [inst : CommRing R] → FGAlgCatSkeleton R → FGAlgCat R
-- Mathlib.Data.Multiset.Fintype
/-- Another way to coerce a `Multiset` to a type is to go through `m.toEnumFinset` and coerce
that `Finset` to a type.  -/
Multiset.coeEquiv : {α : Type u_1} → [inst : DecidableEq α] → (m : Multiset α) → m.ToType ≃ ↥m.toEnumFinset
-- Mathlib.Algebra.Category.Ring.Limits
/-- An auxiliary declaration to speed up typechecking.
 -/
RingCat.forget₂AddCommGroupPreservesLimitsAux : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J RingCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget RingCat)).sections] →
        CategoryTheory.Limits.IsLimit ((CategoryTheory.forget₂ RingCat AddCommGrpCat).mapCone (RingCat.limitCone F))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_zpow_iff_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 1 < a → (1 < a ^ n ↔ 0 < n)
-- Mathlib.Order.Filter.Finite
/-- If a filter has finitely many sets, then it is principal.  -/
Filter.eq_principal_of_finite_sets : ∀ {α : Type u} {f : Filter α}, f.sets.Finite → ∃ s, f = Filter.principal s
-- Init.Control.Lawful.Instances
ReaderT.run_seqLeft : ∀ {m : Type u_1 → Type u_2} {ρ α β : Type u_1} [inst : Monad m] (x : ReaderT ρ m α) (y : ReaderT ρ m β) (ctx : ρ),
  (x <* y).run ctx = x.run ctx <* y.run ctx
-- Lean.Data.JsonRpc
/-- Invalid JSON was received by the server. An error occurred on the server while parsing the JSON text.  -/
Lean.JsonRpc.ErrorCode.parseError : Lean.JsonRpc.ErrorCode
-- Init.Core
/-- A reflexive relation satisfies `r a a`.  -/
Std.Refl.refl : ∀ {α : Sort u} {r : α → α → Prop} [self : Std.Refl r] (a : α), r a a
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.syntaxString : String → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α β : LieModule.Weight K (↥H) L),
  α.IsNonZero →
    ∀ {n : ℕ},
      LieAlgebra.IsKilling.chainLength α β < n → LieAlgebra.rootSpace H (-(n • ⇑α) + ⇑(LieModule.chainTop (⇑α) β)) = ⊥
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toArray_rcc' : ∀ {m n k : ℕ}, Array.map (fun x => k + x) (m...=n).toArray = ((k + m)...=k + n).toArray
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.selfEquivSigmaOrbitsQuotientStabilizer.eq_1 : ∀ (G : Type u) (X : Type v) [inst : Group G] [inst_1 : MulAction G X],
  MulAction.selfEquivSigmaOrbitsQuotientStabilizer G X = MulAction.selfEquivSigmaOrbitsQuotientStabilizer' G X ⋯
-- Init.Data.List.Sublist
List.take_subset : ∀ {α : Type u_1} (i : ℕ) (l : List α), List.take i l ⊆ l
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.rangeS_top_iff_surjective : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S},
  f.rangeS = ⊤ ↔ Function.Surjective ⇑f