mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Interval.Multiset
Multiset.map_add_left_Ico : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] (a b c : α),
  Multiset.map (fun x => c + x) (Multiset.Ico a b) = Multiset.Ico (c + a) (c + b)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- Formal Taylor series associated to a function.  -/
ftaylorSeries : (𝕜 : 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] → (E → F) → E → FormalMultilinearSeries 𝕜 E F
-- Mathlib.Topology.Order.DenselyOrdered
nhdsWithin_Iio_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] {a b : α}, a ≤ b → (nhdsWithin a (Set.Iio b)).NeBot
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.parentIsApp : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context → Bool
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy integral formula**: if `f : ℂ → E` is complex differentiable on an open disc and is
continuous on its closure, then for any `w` in this open ball we have
$\oint_{|z-c|=R}(z-w)^{-1}f(z)\,dz=2πif(w)$.  -/
DiffContOnCl.circleIntegral_sub_inv_smul : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {R : ℝ} {c w : ℂ} {f : ℂ → E},
  DiffContOnCl ℂ f (Metric.ball c R) →
    w ∈ Metric.ball c R → ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ • f z = (2 * ↑Real.pi * Complex.I) • f w
-- Mathlib.Data.FunLike.Group
FunLike.coe_coeAddMonoidHom : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : AddZero F] [inst_2 : AddZeroClass β]
  [inst_3 : IsZeroApply F α β] [inst_4 : IsAddApply F α β], ⇑(FunLike.coeAddMonoidHom F α β) = DFunLike.coe
-- Mathlib.Algebra.Order.Module.Defs
smul_nonpos_iff_nonpos_of_pos_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [PosSMulMono α β] [PosSMulReflectLE α β], 0 < a → (a • b ≤ 0 ↔ b ≤ 0)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.symm : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β}, e.IsImage s t → e.symm.IsImage t s
-- Mathlib.Topology.Connected.Basic
/-- The iUnion of connected sets indexed by a subset of a type with an archimedean successor
(like `ℕ` or `ℤ`) such that any two neighboring sets meet is preconnected.  -/
IsConnected.biUnion_of_chain : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
  [IsSuccArchimedean β] {s : β → Set α} {t : Set β},
  t.Nonempty →
    t.OrdConnected →
      (∀ n ∈ t, IsConnected (s n)) →
        (∀ n ∈ t, Order.succ n ∈ t → (s n ∩ s (Order.succ n)).Nonempty) → IsConnected (⋃ n ∈ t, s n)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.mem_append_left : ∀ {α : Type u} {s₁ s₂ : Stream'.WSeq α} {a : α}, a ∈ s₁ → a ∈ s₁.append s₂
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_smul_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T T' : Set α → E →L[ℝ] F} {C C' : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C') (c : ℝ),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s) →
    ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 hT') f = c • (MeasureTheory.L1.setToL1 hT) f
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_apply_eq_zero' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {s : Set α},
  AEMeasurable f μ → ((μ.withDensity f) s = 0 ↔ μ ({x | f x ≠ 0} ∩ s) = 0)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.zero_mem_compactSet : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], 0 ∈ NumberField.mixedEmbedding.fundamentalCone.compactSet K
-- Mathlib.Algebra.Group.Equiv.Basic
/-- A family indexed by a type with a unique element
is `MulEquiv` to the element at the single index.  -/
MulEquiv.piUnique : {ι : Type u_16} →
  (M : ι → Type u_17) → [inst : (j : ι) → Mul (M j)] → [inst_1 : Unique ι] → ((j : ι) → M j) ≃* M default
-- Init.Data.List.Impl
/-- Removes the first occurrence of `a` from `l`. If `a` does not occur in `l`, the list is returned
unmodified.

`O(|l|)`.

This is a tail-recursive version of `List.erase`, used in runtime code.

Examples:
* `[1, 5, 3, 2, 5].eraseTR 5 = [1, 3, 2, 5]`
* `[1, 5, 3, 2, 5].eraseTR 6 = [1, 5, 3, 2, 5]`
 -/
List.eraseTR : {α : Type u_1} → [BEq α] → List α → α → List α
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.toLieSubalgebra_inj : ∀ {A : Type u_1} {L : Type u_2} [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L]
  [inst_3 : LieRingModule L A] [inst_4 : LieRinehartRing A L] (R : Type u_3) [inst_5 : CommRing R]
  [inst_6 : Algebra R A] [inst_7 : LieAlgebra R L] [inst_8 : LieRinehartAlgebra R A L]
  (L₁' L₂' : LieRinehartSubalgebra A L), L₁'.toLieSubalgebra R = L₂'.toLieSubalgebra R ↔ L₁' = L₂'
-- Lean.Elab.App
Lean.Elab.Term.elabDotIdent : Lean.Elab.Term.TermElab
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the year to the given `year` value. The month and day are rolled
over to the next valid month and day if necessary.
 -/
Std.Time.PlainDateTime.withYearRollOver : Std.Time.PlainDateTime → Std.Time.Year.Offset → Std.Time.PlainDateTime
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality
/-- **Triangle inequality** for angles in Euclidean geometry.  -/
EuclideanGeometry.angle_le_angle_add_angle : ∀ {V : Type u_2} {P : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p p₁ p₂ p₃ : P),
  EuclideanGeometry.angle p₁ p p₃ ≤ EuclideanGeometry.angle p₁ p p₂ + EuclideanGeometry.angle p₂ p p₃
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- The fiber of the terminal object contains a unique element.  -/
CategoryTheory.GrothendieckTopology.Point.uniqueFiberObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        [CategoryTheory.LocallySmall.{w, v, u} C] →
          (T : C) → CategoryTheory.Limits.IsTerminal T → Unique (Φ.fiber.obj T)
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Composition of two `Equiv`s.  -/
ContRepresentation.Equiv.trans : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        {U : Type u_5} →
          [inst : Monoid G] →
            [inst_1 : Ring R] →
              [inst_2 : AddCommGroup V] →
                [inst_3 : TopologicalSpace V] →
                  [inst_4 : IsTopologicalAddGroup V] →
                    [inst_5 : Module R V] →
                      [inst_6 : AddCommGroup W] →
                        [inst_7 : TopologicalSpace W] →
                          [inst_8 : IsTopologicalAddGroup W] →
                            [inst_9 : Module R W] →
                              [inst_10 : AddCommGroup U] →
                                [inst_11 : Module R U] →
                                  [inst_12 : TopologicalSpace U] →
                                    [inst_13 : IsTopologicalAddGroup U] →
                                      {ρ : ContRepresentation R G V} →
                                        {σ : ContRepresentation R G W} →
                                          {τ : ContRepresentation R G U} → ρ.Equiv σ → σ.Equiv τ → ρ.Equiv τ
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_le_self_of_le_one : ∀ {x : ENNReal} {z : ℝ}, x ≤ 1 → 1 ≤ z → x ^ z ≤ x
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.toIsScalarTower : ∀ {A : Type u_1} [self : NonUnitalCStarAlgebra A], IsScalarTower ℂ A A
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.TM2.step.match_1.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Cfg Γ Λ σ → Sort u_5) (l : Λ)
  (v : σ) (S : (k : K) → List (Γ k))
  (h_1 : (var : σ) → (stk : (k : K) → List (Γ k)) → motive { l := none, var := var, stk := stk })
  (h_2 : (l : Λ) → (v : σ) → (S : (k : K) → List (Γ k)) → motive { l := some l, var := v, stk := S }),
  (match { l := some l, var := v, stk := S } with
    | { l := none, var := var, stk := stk } => h_1 var stk
    | { l := some l, var := v, stk := S } => h_2 l v S) =
    h_2 l v S
-- Mathlib.Data.Finset.Sigma
Finset.notMem_sigmaLift_of_ne_left : ∀ {ι : Type u_1} {α : ι → Type u_2} {β : ι → Type u_3} {γ : ι → Type u_4} [inst : DecidableEq ι]
  (f : ⦃i : ι⦄ → α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) (x : Sigma γ),
  a.fst ≠ x.fst → x ∉ Finset.sigmaLift f a b
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierInv_comm : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : V → E),
  FourierTransform.fourier (FourierTransformInv.fourierInv f) =
    FourierTransformInv.fourierInv (FourierTransform.fourier f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insertMany_empty_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : Inhabited α] {l : List ((a : α) × β a)}
  {k k' : α},
  compare k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).getKey! k' = k
-- Init.Grind.AC
_private.Init.Grind.AC.0.Lean.Grind.AC.Seq.erase0.match_1.splitter : (motive : Lean.Grind.AC.Seq → Sort u_1) →
  (s : Lean.Grind.AC.Seq) →
    ((x : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x)) →
      ((x : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s)) → motive s
-- Mathlib.Logic.Function.Basic
Function.invFun_surjective : ∀ {α : Sort u_1} {β : Sort u_2} [inst : Nonempty α] {f : α → β},
  Function.Injective f → Function.Surjective (Function.invFun f)
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card.eq_1 : ∀ (α : Type u_3), Nat.card α = Cardinal.toNat (Cardinal.mk α)
-- Mathlib.Data.Multiset.AddSub
Multiset.add_le_add_iff_left : ∀ {α : Type u_1} {s t u : Multiset α}, s + t ≤ s + u ↔ t ≤ u
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsupp.locallyFiniteSupport : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : Zero Y] (f : Function.locallyFinsupp X Y),
  LocallyFiniteSupport f.toFun
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuous.upperSemicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  UpperSemicontinuous f → ∀ (s : Set α) (x : α), UpperSemicontinuousWithinAt f s x
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
/-- The underlying morphism of simplicial sets.  -/
SSet.RelativeMorphism.map : {X Y : SSet} →
  {A : X.Subcomplex} → {B : Y.Subcomplex} → {φ : A.toSSet ⟶ B.toSSet} → SSet.RelativeMorphism A B φ → (X ⟶ Y)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.instIsScalarTower : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (T : Type u_1) [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T],
  IsScalarTower R T (LocalizedModule S M)
-- Mathlib.MeasureTheory.Measure.Haar.Extension
TopologicalGroup.IsSES.pushforward_apply_apply : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {E : Type u_4} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C}
  (H : TopologicalGroup.IsSES φ ψ) [inst_6 : IsTopologicalGroup A] [inst_7 : IsTopologicalGroup B]
  [inst_8 : NormedAddCommGroup E] [inst_9 : MeasurableSpace A] [inst_10 : BorelSpace A] (μA : MeasureTheory.Measure A)
  [hμA : μA.IsHaarMeasure] [inst_11 : NormedSpace ℝ E] [inst_12 : IsTopologicalGroup C]
  [inst_13 : LocallyCompactSpace B] (f : CompactlySupportedContinuousMap B E) (b : B),
  ((H.pushforward μA) f) (ψ b) = ∫ (a : A), (H.pullback f b) a ∂μA
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.toFinsupp_toFreeAbelianGroup : ∀ {X : Type u_1} (f : X →₀ ℤ), FreeAbelianGroup.toFinsupp (Finsupp.toFreeAbelianGroup f) = f
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.instFiniteDimensionalSubtypeMemIntermediateField : ∀ (k : Type u_1) (K : Type u_2) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L : FiniteGaloisIntermediateField k K), FiniteDimensional k ↥L.toIntermediateField
-- Mathlib.Data.ENat.Basic
ENat.toNat_eq_zero : ∀ {n : ℕ∞}, n.toNat = 0 ↔ n = 0 ∨ n = ⊤
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Jacobi symbol of `a` and `b`  -/
NumberTheorySymbols.«termJ(_|_)» : Lean.ParserDescr
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_trans : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α] {a b c : α},
  Std.PRange.UpwardEnumerable.LT a b → Std.PRange.UpwardEnumerable.LT b c → Std.PRange.UpwardEnumerable.LT a c
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.ofHom_hom : ∀ {R S : RingCat} (f : R ⟶ S), RingCat.ofHom (RingCat.Hom.hom f) = f
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.one_sub_self_mul_hsum_powers : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] {x : HahnSeries Γ R}, 0 < x.orderTop → (1 - x) * (HahnSeries.SummableFamily.powers x).hsum = 1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_succ : ∀ {n : ℕ}, (*...=n + 1).toList = (*...=n).toList ++ [n + 1]
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- `C` has all colimits over any type `J` whose objects and morphisms lie in the same universe
and which has `Fintype` objects and morphisms  -/
CategoryTheory.Limits.HasFiniteColimits.out : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Limits.HasFiniteColimits C] (J : Type)
  [𝒥 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J], CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.coeff_supDegree_add_supDegree : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      (p * q).coeff (Function.invFun D (AddMonoidAlgebra.supDegree D p + AddMonoidAlgebra.supDegree D q)) =
        AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
-- Mathlib.Tactic.Translate.Reorder
/-- The recursive reorders for reordering arguments of arguments.
For the purpose of checking equality between reorders, this should be sorted.  -/
Mathlib.Tactic.Translate.ArgReorder.argReorders : Mathlib.Tactic.Translate.ArgReorder → Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.comm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.Equiv t₂ ↔ t₂.Equiv t₁
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_def : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.IsComplement' K ↔ Subgroup.IsComplement ↑H ↑K
-- Mathlib.GroupTheory.Coxeter.Basic
PresentedGroup.of.eq_1 : ∀ {α : Type u_1} {rels : Set (FreeGroup α)} (x : α), PresentedGroup.of x = (PresentedGroup.mk rels) (FreeGroup.of x)
-- Mathlib.Combinatorics.Additive.Corner.Defs
/-- A **corner-free set** in an abelian group is a set containing no non-trivial corner.  -/
IsCornerFree : {G : Type u_1} → [AddCommMonoid G] → Set (G × G) → Prop
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_whiskerLeft_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X X' : C}
  (f : X ⟶ X'),
  f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor X').hom)
-- Init.Data.SInt.Lemmas
UInt8.toInt8_ofNatLT : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatLT n hn).toInt8 = Int8.ofNat n
-- Mathlib.Data.Finset.Empty
Finset.instIsEmpty : ∀ {α : Type u_1}, IsEmpty ↥∅
-- Lean.Elab.Binders
/-- Throw an error if `type` is not a valid local instance.  -/
_private.Lean.Elab.Binders.0.Lean.Elab.Term.checkLocalInstanceParameters : Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.sub_add_cancel_left : ∀ {α : Type u} [inst : SubtractionCommMonoid α] {a : α}, IsAddUnit a → ∀ (b : α), a - (a + b) = -b
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The dependent evaluation natural transformation as the counit of the adjunction.  -/
CategoryTheory.ExponentiableMorphism.ev : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I J : C} →
      (f : I ⟶ J) →
        [inst_1 : CategoryTheory.ChosenPullbacksAlong f] →
          [inst_2 : CategoryTheory.ExponentiableMorphism f] →
            (CategoryTheory.ExponentiableMorphism.pushforward f).comp (CategoryTheory.ChosenPullbacksAlong.pullback f) ⟶
              CategoryTheory.Functor.id (CategoryTheory.Over I)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : MeasureTheory.SignedMeasure α} (μ : MeasureTheory.Measure α)
  {f : α → ℝ},
  Measurable f →
    MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure →
      s = t + μ.withDensityᵥ f → s.HaveLebesgueDecomposition μ
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
LaurentPolynomial.antipode_C_mul_T : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (a : A)
  (n : ℤ),
  (HopfAlgebraStruct.antipode R) (LaurentPolynomial.C a * LaurentPolynomial.T n) =
    LaurentPolynomial.C ((HopfAlgebraStruct.antipode R) a) * LaurentPolynomial.T (-n)
-- Init.Sym.Lemmas
Lean.Sym.Char.lt_eq_true : ∀ (a b : Char), decide (a < b) = true → (a < b) = True
-- Mathlib.Algebra.Category.BoolRing
BoolRing.Hom.ext_iff : ∀ {R : BoolRing} {S : BoolRing} {x y : R.Hom S}, x = y ↔ x.hom' = y.hom'
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.π_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (X : F.Elements),
  (CategoryTheory.CategoryOfElements.π F).obj X = X.fst
-- Init.GrindInstances.ToInt
Lean.Grind.instLEInt16SintOfNatNat : Lean.Grind.ToInt.LE Int16 (Lean.Grind.IntInterval.sint 16)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_inter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  (m₁ ∩ m₂).get? k = if k ∈ m₂ then m₁.get? k else none
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.instInhabited : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : PseudoMetricSpace P] → [inst_4 : NormedAddTorsor V P] → Inhabited (P ≃ᵃⁱ[𝕜] P)
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.mapAut_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R] (f : R ≃+* R),
  IsLocalRing.ResidueField.mapAut f = IsLocalRing.ResidueField.mapEquiv f
-- Batteries.Data.PairingHeap
/-- `O(1)`. Get the smallest element in the heap, including the passed in value `a`.  -/
Batteries.PairingHeapImp.Heap.headD : {α : Type u_1} → α → Batteries.PairingHeapImp.Heap α → α
-- Mathlib.GroupTheory.OrderOfElement
addOrderOf_nsmul_of_dvd : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ}, n ≠ 0 → n ∣ addOrderOf x → addOrderOf (n • x) = addOrderOf x / n
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Algebra.TensorProduct.linearEquivIncludeRange_symm_toLinearMap : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring T] [inst_4 : Algebra R T],
  ↑(Algebra.TensorProduct.linearEquivIncludeRange R S T).symm =
    Algebra.TensorProduct.includeLeft.toLinearMap.range.mulMap Algebra.TensorProduct.includeRight.toLinearMap.range
-- Mathlib.Topology.Order.ScottTopology
/-- `toScott` is the identity function to the `WithScott` of a type.  -/
Topology.WithScott.toScott : {α : Type u_1} → α ≃ Topology.WithScott α
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftLift.whisker_lift : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  (t : CategoryTheory.Bicategory.LeftLift f g) {x : B} (h : x ⟶ c),
  (t.whisker h).lift = CategoryTheory.CategoryStruct.comp h t.lift
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.uniformContinuous : ∀ {R : Type u_1} [inst : CommSemiring R] {E₁ : Type u_4} {E₂ : Type u_5} [inst_1 : UniformSpace E₁]
  [inst_2 : UniformSpace E₂] [inst_3 : Ring E₁] [inst_4 : Ring E₂] [inst_5 : Algebra R E₁] [inst_6 : Algebra R E₂]
  [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (f : E₁ →A[R] E₂), UniformContinuous ⇑f
-- Mathlib.Topology.MetricSpace.Basic
NNReal.isUniformEmbedding_coe : IsUniformEmbedding NNReal.toReal
-- Init.Data.Nat.Lemmas
Nat.succ_mul_pos : ∀ {n : ℕ} (m : ℕ), 0 < n → 0 < m.succ * n
-- Mathlib.Data.Multiset.ZeroCons
Multiset.pairwise_zero : ∀ {α : Type u_1} (r : α → α → Prop), Multiset.Pairwise r 0
-- Init.Data.Array.Lemmas
List.flatten_toArray : ∀ {α : Type u_1} {L : List (List α)}, (Array.map List.toArray L.toArray).flatten = L.flatten.toArray
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.natCast_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (n : ℕ), ↑n ∈ S
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f),
  (F.mapComp' f₀₂ f₂₃ f ⋯).hom =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
          (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))))
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The `n+1`-th iterated derivative within a set with unique derivatives can be obtained by
differentiating the `n`-th iterated derivative.  -/
iteratedDerivWithin_succ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜},
  iteratedDerivWithin (n + 1) f s = derivWithin (iteratedDerivWithin n f s) s