mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblZ_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R}, P 2 = 0 → W'.dblZ P = 0
-- Mathlib.Analysis.SpecialFunctions.Log.Base
/-- The real logarithm in a given base. As with the natural logarithm, we define `logb b x` to
be `logb b |x|` for `x < 0`, and `0` for `x = 0`.  -/
Real.logb : ℝ → ℝ → ℝ
-- Mathlib.CategoryTheory.Sites.EffectiveEpimorphic
CategoryTheory.EffectiveEpiStruct.desc.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} {f : Y ⟶ X}
  (self self_1 : CategoryTheory.EffectiveEpiStruct f),
  self = self_1 →
    ∀ {W : C} (e e_1 : Y ⟶ W) (e_e : e = e_1)
      (a :
        ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
          CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
            CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e),
      self.desc e a = self_1.desc e_1 ⋯
-- Mathlib.Data.List.Indexes
List.mapIdxM'_eq_mapIdxM : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m] {α : Type u_1} (f : ℕ → α → m PUnit.{u + 1}) (as : List α),
  List.mapIdxM' f as = List.mapIdxM f as *> pure PUnit.unit
-- Mathlib.Analysis.RCLike.Sqrt
RCLike.sqrt_zero : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], RCLike.sqrt 0 = 0
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_self_lt_prod_self : ∀ {α : Type u_1} [inst : Preorder α] {s₁ s₂ : UpperSet α}, s₁ ×ˢ s₁ < s₂ ×ˢ s₂ ↔ s₁ < s₂
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.zero : ℝ
-- Mathlib.Topology.Separation.Basic
Set.Finite.isDiscrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {s : Set X}, s.Finite → IsDiscrete s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.mkIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G H : CategoryTheory.AddGrp C} (e : G.X ≅ H.X)
  (one_f : CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero)
  (mul_f :
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
        CategoryTheory.AddMonObj.add),
  CategoryTheory.AddGrp.mkIso e one_f mul_f = CategoryTheory.AddGrp.mkIso' e
-- Mathlib.Data.Set.Image
Subtype.map.eq_1 : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ (a : α), p a → q (f a))
  (x : Subtype p), Subtype.map f h x = ⟨f ↑x, ⋯⟩
-- Mathlib.Topology.FiberBundle.Constructions
/-- Fiber bundle instance on the trivial bundle.  -/
Bundle.Trivial.fiberBundle : (B : Type u_1) →
  (F : Type u_2) → [inst : TopologicalSpace B] → [inst_1 : TopologicalSpace F] → FiberBundle F (Bundle.Trivial B F)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  {𝒢 : CategoryTheory.Functor Dᵒᵖ A} (f : 𝒢 ⟶ ℱ) (g : ℱ ⟶ ℱ'.obj),
  CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.symm (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (G.op.whiskerLeft f)
      (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.symm g)
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- Two `AddSubmonoid`s are equal if they have the same elements.  -/
AddSubmonoid.ext : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- Notation for the forward direction morphism of the canonical right distributivity isomorphism  -/
CategoryTheory.Distributive.«term∂R» : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_mem_sphere : ∀ (c : ℂ) {R : ℝ}, 0 ≤ R → ∀ (θ : ℝ), circleMap c R θ ∈ Metric.sphere c R
-- Mathlib.CategoryTheory.Limits.Presheaf
/-- `F ⋙ uliftYoneda` is naturally isomorphic to `uliftYoneda ⋙ F.op.lan`.  -/
CategoryTheory.Presheaf.compULiftYonedaIsoULiftYonedaCompLan : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁ v₂))), F.op.HasLeftKanExtension P] →
            F.comp CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂} ≅
              CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.comp F.op.lan
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonRenameParams.toJson : Lean.Lsp.RenameParams → Lean.Json
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.instPreservesLimitSchemeOppositeCommRingCatRightOpΓOfIsAffineHomMapOfCompactSpaceOfQuasiSeparatedSpaceCarrierCarrierObj : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)]
  [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)],
  CategoryTheory.Limits.PreservesLimit D AlgebraicGeometry.Scheme.Γ.rightOp
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupEquiv : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (a : ↥(MonoidWithZeroHom.ofClass (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v)).valueGroup),
  ↑((IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv K v) a) = ↑a
-- Mathlib.Data.List.Sigma
List.dlookup_kunion_right : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)},
  a ∉ l₁.keys → List.dlookup a (l₁.kunion l₂) = List.dlookup a l₂
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.max_sum_le : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] {f g : ι → M}
  {s : Finset ι}, max (s.sum f) (s.sum g) ≤ ∑ i ∈ s, max (f i) (g i)
-- Lean.Data.Json.Basic
Lean.Json.null : Lean.Json
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt16.size ≤ n → (UInt16.ofNatClamp n).toUSize = USize.ofNatLT (UInt16.size - 1) ⋯
-- Lean.Server.AsyncList
Lean.AsyncList.brecOn_2.go : {ε : Type u} →
  {α : Type v} →
    {motive_1 : Lean.AsyncList ε α → Sort u_1} →
      {motive_2 : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α)) → Sort u_1} →
        {motive_3 : Task (Except ε (Lean.AsyncList ε α)) → Sort u_1} →
          {motive_4 : Except ε (Lean.AsyncList ε α) → Sort u_1} →
            (t : Task (Except ε (Lean.AsyncList ε α))) →
              ((t : Lean.AsyncList ε α) → t.below → motive_1 t) →
                ((t : Lean.Server.ServerTask (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_1 t → motive_2 t) →
                  ((t : Task (Except ε (Lean.AsyncList ε α))) → Lean.AsyncList.below_2 t → motive_3 t) →
                    ((t : Except ε (Lean.AsyncList ε α)) → Lean.AsyncList.below_3 t → motive_4 t) →
                      motive_3 t ×' Lean.AsyncList.below_2 t
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.countKnown : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {len : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec len → ℕ
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.IsFiniteKernel.integrable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ] (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ] {s : Set β},
  MeasurableSet s → MeasureTheory.Integrable (fun x => (κ x).real s) μ
-- Batteries.Lean.Except
_private.Batteries.Lean.Except.0.Except.map.match_1.splitter : {ε : Type u_1} →
  {α : Type u_2} →
    (motive : Except ε α → Sort u_3) →
      (x : Except ε α) → ((err : ε) → motive (Except.error err)) → ((v : α) → motive (Except.ok v)) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- The associator isomorphism for categorical cospan transformations.  -/
CategoryTheory.Limits.CatCospanTransform.termα_ : Lean.ParserDescr
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.Order.Category.BoolAlg
BoolAlg.Hom.ext : ∀ {X Y : BoolAlg} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toList_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α}, ∅.toList = []
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.not_nil_of_adj_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {w u v x : V} {p : G.Walk u v}, p.toSubgraph.Adj w x → ¬p.Nil
-- Mathlib.Algebra.Ring.Defs
NonUnitalCommSemiring.toNonUnitalSemiring : {α : Type u} → [self : NonUnitalCommSemiring α] → NonUnitalSemiring α
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.JordanDecomposition.coe_smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal), ↑r • j = r • j
-- Mathlib.Data.Bundle
Bundle.instCoeTCTotalSpace : {B : Type u_1} → {F : Type u_2} → {E : B → Type u_3} → {x : B} → CoeTC (E x) (Bundle.TotalSpace F E)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toArray_ne_nil : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toArray ≠ #[]
-- Init.Data.String.Iterator
String.Legacy.Iterator.mk.injEq : ∀ (s : String) (i : String.Pos.Raw) (s_1 : String) (i_1 : String.Pos.Raw),
  ({ s := s, i := i } = { s := s_1, i := i_1 }) = (s = s_1 ∧ i = i_1)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCoseparator.hasSeparator_of_hasCoseparator_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.HasCoseparator Cᵒᵖ],
  CategoryTheory.HasSeparator C
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.TranslationInfo.mk : Lean.Name →
  Mathlib.Tactic.Translate.Reorder → Mathlib.Tactic.Translate.RelevantArg → Mathlib.Tactic.Translate.TranslationInfo
-- Mathlib.Algebra.Group.Basic
add_left_comm : ∀ {G : Type u_3} [inst : AddCommSemigroup G] (a b c : G), a + (b + c) = b + (a + c)
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addCommGroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : Neg M₁]
  [inst_4 : Sub M₁] [inst_5 : SMul ℤ M₁] [inst_6 : AddCommGroup M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Injective.addCommGroup f hf one mul inv div npow zpow =
    { toAddGroup := Function.Injective.addGroup f hf one mul inv div npow zpow, add_comm := ⋯ }
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.Inv.eq_1 : ∀ (aig : Std.Sat.AIG ℕ) (cnf : Std.Sat.CNF ℕ),
  Std.Sat.AIG.toCNF.State.Inv✝ aig cnf =
    ∀ (assign1 : ℕ → Bool), Std.Sat.CNF.Sat (Std.Sat.AIG.toCNF.cnfSatAssignment✝ aig assign1) cnf
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'_cons : ∀ {α : Type u} (x : α) (s : Stream'.Seq α), (Stream'.Seq.cons x s).length' = s.length' + 1
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.leftAdjointUniq_hom_counit : ∀ {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] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G),
  CategoryTheory.CategoryStruct.comp (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom) adj2.counit = adj1.counit
-- Mathlib.Tactic.TermCongr
/-- The right-hand side of the congruence result.  -/
Mathlib.Tactic.TermCongr.CongrResult.rhs : Mathlib.Tactic.TermCongr.CongrResult → Lean.Expr
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
CategoryTheory.GlueData.diagram.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C),
  D.diagram =
    { left := D.V, right := D.U,
      fst := fun x =>
        match x with
        | (i, j) => D.f i j,
      snd := fun x =>
        match x with
        | (i, j) => CategoryTheory.CategoryStruct.comp (D.t i j) (D.f j i) }
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- (implementation) tensor product of morphisms R-modules  -/
SemimoduleCat.MonoidalCategory.tensorHom : {R : Type u} →
  [inst : CommSemiring R] →
    {M N : SemimoduleCat R} →
      {M' N' : SemimoduleCat R} →
        (M ⟶ N) →
          (M' ⟶ N') → (SemimoduleCat.MonoidalCategory.tensorObj M M' ⟶ SemimoduleCat.MonoidalCategory.tensorObj N N')
-- Mathlib.MeasureTheory.Order.Lattice
AEMeasurable.inf_const : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → M} [inst_1 : Min M] [MeasurableInf M], AEMeasurable f μ → ∀ (c : M), AEMeasurable (fun x => f x ⊓ c) μ
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.aleph0_le_cof_iff : ∀ {α : Type u} [inst : LinearOrder α], Cardinal.aleph0 ≤ Order.cof α ↔ 1 < Order.cof α
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instFunLikeHomRing : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} → {P' : Algebra.Extension R S} → FunLike (P.Hom P') P.Ring P'.Ring
-- Mathlib.Analysis.Complex.Angle
Complex.angle_exp_one : ∀ (x : ℝ), InnerProductGeometry.angle (Complex.exp (↑x * Complex.I)) 1 = |toIocMod Real.two_pi_pos (-Real.pi) x|
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxo.Iterator.instLawfulIteratorLoop : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α] {n : Type u → Type w}
  [inst_5 : Monad n] [LawfulMonad n], Std.LawfulIteratorLoop (Std.Rxo.Iterator α) Id n
-- Mathlib.Algebra.Group.Prod
/-- Given additive monoids `A`, `B`, the natural inclusion homomorphism
from `B` to `A × B`.  -/
AddMonoidHom.inr : (M : Type u_3) → (N : Type u_4) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → N →+ M × N
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
/-- A bi-Cartesian square in a lattice consists of elements `x₁`, `x₂`, `x₃` and `x₄`
such that `x₂ ⊔ x₃ = x₄` and `x₂ ⊓ x₃ = x₁`.  -/
Lattice.BicartSq : {T : Type u} → T → T → T → T → [Lattice T] → Prop
-- Mathlib.Data.Fin.Tuple.Reflection
/-- Evaluate `FinVec.seq f v = ![(f 0) (v 0), (f 1) (v 1), ...]`  -/
FinVec.seq : {α : Type u_1} → {β : Type u_2} → {m : ℕ} → (Fin m → α → β) → (Fin m → α) → Fin m → β
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- `σ : M.GeneratingSections` is finite type if the index type `σ.I` is finite.  -/
SheafOfModules.GeneratingSections.IsFiniteType : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
          [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] → {M : SheafOfModules R} → M.GeneratingSections → Prop
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The points in a cube with at least one projection equal to 0 or 1.  -/
Cube.boundary : (N : Type u_1) → Set (N → ↑unitInterval)
-- Mathlib.RingTheory.Algebraic.Basic
AlgEquiv.isAlgebraic_iff : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u_2}
  [inst_3 : Ring B] [inst_4 : Algebra R B] (e : A ≃ₐ[R] B), Algebra.IsAlgebraic R A ↔ Algebra.IsAlgebraic R B
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.isStrongLimit_preBeth : ∀ {o : Ordinal.{u_1}}, (Cardinal.preBeth o).IsStrongLimit ↔ Order.IsSuccLimit o
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with shifting the function by a constant on the right.  -/
iteratedFDerivWithin_comp_add_right : ∀ {𝕜 : 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} (n : ℕ) (a x : E),
  iteratedFDerivWithin 𝕜 n (fun z => f (z + a)) s x = iteratedFDerivWithin 𝕜 n f (a +ᵥ s) (x + a)
-- Mathlib.Data.Fintype.Sets
Fintype.finsetOrderIsoSet_toEquiv : ∀ {α : Type u_1} [inst : Fintype α], Fintype.finsetOrderIsoSet.toEquiv = Fintype.finsetEquivSet
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddCommGroup.toCompl_apply : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] (a : G), NormedAddCommGroup.toCompl a = ↑a
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.ext_iff : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} {f g : ↑(GenLoop N X x)},
  f = g ↔ ∀ (y : N → ↑unitInterval), f y = g y
-- Mathlib.CategoryTheory.Limits.Final
/-- If the universal morphism `colimit (F ⋙ coyoneda.obj (op d)) ⟶ colimit (coyoneda.obj (op d))`
is an isomorphism (as it always is when `F` is final),
then `colimit (F ⋙ coyoneda.obj (op d)) ≅ PUnit`
(simply because `colimit (coyoneda.obj (op d)) ≅ PUnit`).
 -/
CategoryTheory.Functor.Final.colimitCompCoyonedaIso : {C : Type v} →
  [inst : CategoryTheory.Category.{v, v} C] →
    {D : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v, u₁} D] →
        (F : CategoryTheory.Functor C D) →
          (d : D) →
            [CategoryTheory.IsIso (CategoryTheory.Limits.colimit.pre (CategoryTheory.coyoneda.obj (Opposite.op d)) F)] →
              CategoryTheory.Limits.colimit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op d))) ≅ PUnit.{v + 1}
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.mono_τ₂_of_exact_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Balanced C] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  S₁.Exact →
    ∀ [CategoryTheory.Mono S₁.f] [CategoryTheory.Mono S₂.f] [CategoryTheory.Mono φ.τ₁] [CategoryTheory.Mono φ.τ₃],
      CategoryTheory.Mono φ.τ₂
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
/-- The general linear group on `R` and `M` is multiplicatively equivalent to the type of linear
equivalences between `M` and itself.  -/
LinearMap.GeneralLinearGroup.generalLinearEquiv : (R : Type u_1) →
  (M : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → LinearMap.GeneralLinearGroup R M ≃* M ≃ₗ[R] M
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (a b : Lean.Grind.CommRing.Expr),
  x = a.add b →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_5 a b
-- Mathlib.Data.Finset.Basic
Finset.pairwiseDisjoint_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {ι : Type u_4} {s : Set ι} {f : ι → Finset α},
  s.PairwiseDisjoint f ↔ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j
-- Mathlib.Condensed.Explicit
/-- A condensed object regarded as a sheaf on `Stonean` preserves finite products.  -/
Condensed.instPreservesFiniteProductsOppositeStoneanObjFunctorIsSheafCoherentTopology : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology Stonean) A),
  CategoryTheory.Limits.PreservesFiniteProducts X.obj
-- Lean.Language.Basic
Lean.Language.SnapshotTask.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (stx? : Option Lean.Syntax) (reportingRange : Lean.Language.SnapshotTask.ReportingRange)
  (cancelTk? : Option IO.CancelToken) (task : Task α),
  sizeOf { stx? := stx?, reportingRange := reportingRange, cancelTk? := cancelTk?, task := task } =
    1 + sizeOf stx? + sizeOf reportingRange + sizeOf cancelTk? + sizeOf task
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} {a b c : M} (f f_1 : CategoryTheory.ShiftedHom X Y a),
  f = f_1 → ∀ (g g_1 : CategoryTheory.ShiftedHom Y Z b), g = g_1 → ∀ (h : b + a = c), f.comp g h = f_1.comp g_1 h
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply_eq_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} [MeasurableSingletonClass α],
  MeasureTheory.Measure.count s = ⊤ ↔ s.Infinite
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.of_same : ∀ {G : Type u_1} [inst : AddSemigroup G] [IsCancelAdd G],
  (∀ {A : Finset G}, A.Nonempty → ∃ a1 ∈ A, ∃ a2 ∈ A, UniqueAdd A A a1 a2) → UniqueSums G
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, WithTop.some ⁻¹' Set.Iio ↑a = Set.Iio a
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.ne_zero_iff : ∀ {M : Type u_1} [inst : MonoidWithZero M] {a b : M}, Associated a b → (a ≠ 0 ↔ b ≠ 0)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribMulAction.ext_iff : ∀ {M : Type u_12} {A : Type u_13} {inst : Monoid M} {inst_1 : AddMonoid A} {x y : DistribMulAction M A},
  x = y ↔ SMul.smul = SMul.smul
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.factors_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {x y : α},
  x ≠ 0 →
    y ≠ 0 →
      Multiset.Rel Associated (UniqueFactorizationMonoid.factors (x * y))
        (UniqueFactorizationMonoid.factors x + UniqueFactorizationMonoid.factors y)
-- Mathlib.Topology.Category.TopCat.OpenNhds
Topology.IsInducing.functorNhds_map : ∀ {X Y : TopCat} {f : X ⟶ Y} (h : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑X)
  {X_1 Y_1 : TopologicalSpace.OpenNhds x} (a : ↑X_1 ⟶ ↑Y_1), (h.functorNhds x).map a = h.functor.map a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- A multiple of the difference of two points added to the first point lies in their affine
span.  -/
smul_vsub_vadd_mem_affineSpan_pair : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (r : k) (p₁ p₂ : P), r • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ line[k, p₁, p₂]
-- Mathlib.Data.List.Sort
/-- The list `List.insertionSort r l` is `List.Pairwise` with respect to `r`.  -/
List.pairwise_insertionSort : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [Std.Total r] [IsTrans α r] (l : List α),
  List.Pairwise r (List.insertionSort r l)
-- Std.Data.DTreeMap.Raw.AdditionalOperations
/-- Updates the values of the map by applying the given function to all mappings.  -/
Std.DTreeMap.Raw.map : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      {cmp : α → α → Ordering} → ((a : α) → β a → γ a) → Std.DTreeMap.Raw α β cmp → Std.DTreeMap.Raw α γ cmp