mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Given an equivalence `e : R ≃+* S` of rings and a subring `s` of `R`,
`subringMap e s` is the induced equivalence between `s` and `s.map e`  -/
RingEquiv.subringMap : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocRing R] →
      [inst_1 : NonAssocRing S] → {s : Subring R} → (e : R ≃+* S) → ↥s ≃+* ↥(Subring.map e.toRingHom s)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_15 : HAdd Std.Time.Second.Offset Std.Time.Hour.Offset Std.Time.Second.Offset
-- Lean.Parser.Command
Lean.Parser.Command.namedPrio.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.mono_measure : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f ν → μ ≤ ν → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume_eq_det_inv : ∀ {ι : Type u_2} [inst : Fintype ι] (L : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L] [inst_2 : IsZLattice ℝ L]
  (b : Module.Basis ι ℤ ↥L),
  ZLattice.covolume L MeasureTheory.volume = |↑(LinearEquiv.det (Module.Basis.ofZLatticeBasis ℝ L b).equivFun)|⁻¹
-- Lean.Setup
Lean.ModuleArtifacts.ilean? : Lean.ModuleArtifacts → Option System.FilePath
-- Mathlib.Data.Fin.Tuple.Basic
Fin.comp_snoc : ∀ {n : ℕ} {α : Sort u_2} {β : Sort u_3} (g : α → β) (q : Fin n → α) (y : α), g ∘ Fin.snoc q y = Fin.snoc (g ∘ q) (g y)
-- Init.System.IO
/-- Reads the entire remaining contents of the stream as a UTF-8-encoded string. An exception is
thrown if the contents are not valid UTF-8.

The underlying stream is not automatically closed, and subsequent reads from the stream may block
and/or return data.
 -/
IO.FS.Stream.readToEnd : IO.FS.Stream → IO String
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
AlgebraicTopology.DoldKan.hσ'.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q n m : ℕ) (hnm : AlgebraicTopology.DoldKan.c.Rel m n),
  AlgebraicTopology.DoldKan.hσ' q n m hnm =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.hσ q n) (CategoryTheory.eqToHom ⋯)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- The structure map of the initial algebra is an isomorphism,
hence endofunctors preserve their initial algebras
 -/
CategoryTheory.Endofunctor.Algebra.Initial.str_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Algebra F} (h : CategoryTheory.Limits.IsInitial A), CategoryTheory.IsIso A.str
-- Mathlib.Data.Nat.Digits.Lemmas
/-- The `Finset` of lists whose head is a fixed integer `d` and tail is a list
in `List.fixedLengthDigits b l`.
 -/
List.consFixedLengthDigits : {b : ℕ} → 1 < b → ℕ → ℕ → Finset (List ℕ)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.add_smul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  {X : Cᵒᵖ} (r r' : ↑(R.obj.obj X)) (m : ↑(A.obj.obj X)),
  PresheafOfModules.Sheafify.smul α φ (r + r') m =
    PresheafOfModules.Sheafify.smul α φ r m + PresheafOfModules.Sheafify.smul α φ r' m
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.le_natTrailingDegree : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R},
  p ≠ 0 → (∀ m < n, p.coeff m = 0) → n ≤ p.natTrailingDegree
-- Mathlib.Probability.Distributions.Uniform
PMF.ofMultiset_apply : ∀ {α : Type u_1} {s : Multiset α} (hs : s ≠ 0) (a : α), (PMF.ofMultiset s hs) a = ↑(Multiset.count a s) / ↑s.card
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.preimage_eq_top_iff : ∀ {X Y : SSet} (B : X.Subcomplex) (f : Y ⟶ X), B.preimage f = ⊤ ↔ SSet.Subcomplex.range f ≤ B
-- Std.Data.TreeMap.Basic
/-- Inserts multiple elements into the tree map by iterating over the given collection and calling
`insertIfNew`. If the same key appears multiple times, the first occurrence takes precedence.
 -/
Std.TreeMap.insertManyIfNewUnit : {α : Type u} →
  {cmp : α → α → Ordering} → {ρ : Type u_1} → [ForIn Id ρ α] → Std.TreeMap α Unit cmp → ρ → Std.TreeMap α Unit cmp
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α},
  ∅.getKey? a = none
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)) {Z : ↑(F.obj d)}
  (h_1 : (F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).inv.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv.toNatTrans.app X)
        h_1) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp g h).inv.toNatTrans.app ((F.map f).toFunctor.obj X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X)
        (CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X)
          h_1))
-- Init.Data.List.Basic
List.replicateTR.loop.eq_1 : ∀ {α : Type u} (a : α) (a_1 : List α), List.replicateTR.loop a 0 a_1 = a_1
-- Init.Data.UInt.Lemmas
USize.toUInt16_lt : ∀ {a b : USize}, a.toUInt16 < b.toUInt16 ↔ a % 65536 < b % 65536
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Dyadic.pow.match_1.eq_2 : ∀ (motive : Dyadic → Sort u_1) (n k : ℤ) (hn : n % 2 = 1) (h_1 : Unit → motive Dyadic.zero)
  (h_2 : (n k : ℤ) → (hn : n % 2 = 1) → motive (Dyadic.ofOdd n k hn)),
  (match Dyadic.ofOdd n k hn with
    | Dyadic.zero => h_1 ()
    | Dyadic.ofOdd n k hn => h_2 n k hn) =
    h_2 n k hn
-- Mathlib.Algebra.Order.Sub.Basic
tsub_pos_iff_not_le : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, 0 < a - b ↔ ¬a ≤ b
-- Mathlib.Algebra.Notation.Prod
Prod.instPow : {E : Type u_8} → {α : Type u_9} → {β : Type u_10} → [Pow α E] → [Pow β E] → Pow (α × β) E
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isRevMatch_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat pos ↔
    String.Slice.Pattern.Model.PatternModel.Matches pat (s.sliceFrom pos).copy
-- Mathlib.SetTheory.ZFC.Basic
/-- Turns a unary definable function into a unary `PSet` function.  -/
ZFSet.Definable₁.out : (f : ZFSet.{u} → ZFSet.{u}) → [ZFSet.Definable₁ f] → PSet.{u} → PSet.{u}
-- Init.Data.List.Control
/-- Applies the applicative action `f` on every element in the list, left-to-right, and returns the list
of results.

If `m` is also a `Monad`, then using `mapM` can be more efficient.

See `List.forA` for the variant that discards the results. See `List.mapM` for the variant that
works with `Monad`.

This function is not tail-recursive, so it may fail with a stack overflow on long lists.
 -/
List.mapA : {m : Type u → Type v} → [Applicative m] → {α : Type w} → {β : Type u} → (α → m β) → List α → m (List β)
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
/-- The `carrier` of a `NonUnitalStarSubsemiring` is closed under the `star` operation.  -/
NonUnitalStarSubsemiring.star_mem' : ∀ {R : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : Star R] (self : NonUnitalStarSubsemiring R) {a : R},
  a ∈ self.carrier → star a ∈ self.carrier
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.equiv_apply_snd_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.WalkingIso C),
  (CategoryTheory.WalkingIso.equiv F).snd.fst = F.obj CategoryTheory.WalkingIso.one
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.uniformSpace_eq_inf_precomp_of_cover : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] {δ₁ : Type u_6} {δ₂ : Type u_7} (φ₁ : δ₁ → α) (φ₂ : δ₂ → α),
  Set.range φ₁ ∪ Set.range φ₂ = Set.univ →
    UniformFun.uniformSpace α β =
      UniformSpace.comap (⇑UniformFun.ofFun ∘ (fun x => x ∘ φ₁) ∘ ⇑UniformFun.toFun) (UniformFun.uniformSpace δ₁ β) ⊓
        UniformSpace.comap (⇑UniformFun.ofFun ∘ (fun x => x ∘ φ₂) ∘ ⇑UniformFun.toFun) (UniformFun.uniformSpace δ₂ β)
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.instStarSubtypeMemSubsemiringCenter : {α : Type u_1} → [inst : NonUnitalNonAssocSemiring α] → [StarRing α] → Star ↥(Subsemiring.center (CentroidHom α))
-- Mathlib.Topology.Semicontinuity.Basic
ContinuousAt.comp_lowerSemicontinuousAt : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : LinearOrder γ]
  [inst_2 : TopologicalSpace γ] [OrderTopology γ] {δ : Type u_5} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ]
  [OrderTopology δ] {g : γ → δ} {f : α → γ},
  ContinuousAt g (f x) → LowerSemicontinuousAt f x → Monotone g → LowerSemicontinuousAt (g ∘ f) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.getKey! t.minKey! = t.minKey!
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.mem_ker : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] {f : M →ₗ⁅R,L⁆ N} {m : M}, m ∈ f.ker ↔ f m = 0
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.DischargeResult.maxDepth.sizeOf_spec : sizeOf Lean.Meta.Simp.DischargeResult.maxDepth = 1
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_id_left_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (F.obj a)) (F.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.id a) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (F.map f)) h) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv h)
-- Mathlib.Topology.Sheaves.Presheaf
/-- **Alias** of `TopCat.Presheaf.pullbackPushforwardAdjunction`.

---

The pullback and pushforward along a continuous map are adjoint to each other.  -/
TopCat.Presheaf.pushforwardPullbackAdjunction : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {X Y : TopCat} → (f : X ⟶ Y) → TopCat.Presheaf.pullback C f ⊣ TopCat.Presheaf.pushforward C f
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_of_tendsto_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [IsUniformAddGroup β] [inst_6 : FunLike hom α β]
  [AddMonoidHomClass hom α β] {f : hom}, Filter.Tendsto (⇑f) (nhds 0) (nhds 0) → UniformContinuous ⇑f
-- Lean.Compiler.IR.Basic
Lean.IR.DeclInfo.mk : Option Lean.Name → Lean.IR.DeclInfo
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.WF.merge_node : ∀ {α : Type u_1} {le : α → α → Bool} {a₁ : α} {c₁ : Batteries.PairingHeapImp.Heap α} {a₂ : α}
  {c₂ s₁ s₂ : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.NodeWF le a₁ c₁ →
    Batteries.PairingHeapImp.Heap.NodeWF le a₂ c₂ →
      Batteries.PairingHeapImp.Heap.WF le
        (Batteries.PairingHeapImp.Heap.merge le (Batteries.PairingHeapImp.Heap.node a₁ c₁ s₁)
          (Batteries.PairingHeapImp.Heap.node a₂ c₂ s₂))
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.eq : Lean.Expr → Lean.Expr → Lean.Expr → Nat.EqResult✝
-- Mathlib.Analysis.SpecificLimits.Normed
/-- If `‖f n‖ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` are within
distance `C * r ^ n / (1 - r)` of the sum of the series. This lemma does not assume `0 ≤ r` or
`0 ≤ C`.  -/
norm_sub_le_of_geometric_bound_of_hasSum : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {r C : ℝ} {f : ℕ → α},
  r < 1 →
    (∀ (n : ℕ), ‖f n‖ ≤ C * r ^ n) →
      ∀ {a : α}, HasSum f a → ∀ (n : ℕ), ‖∑ x ∈ Finset.range n, f x - a‖ ≤ C * r ^ n / (1 - r)
-- Lean.Data.Options
Lean.Option.defValue : {α : Type} → Lean.Option α → α
-- Mathlib.Order.RelSeries
Fin.subNat.eq_1 : ∀ {n : ℕ} (m : ℕ) (i : Fin (n + m)) (h : m ≤ ↑i), Fin.subNat m i h = ⟨↑i - m, ⋯⟩
-- Mathlib.NumberTheory.ModularForms.Petersson
/-- If `f, f'` are modular forms and `f` is zero at infinity, then `petersson k f f'` has
exponentially rapid decay at infinity.  -/
UpperHalfPlane.IsZeroAtImInfty.petersson_exp_decay_left : ∀ {F : Type u_1} {F' : Type u_2} [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] (k : ℤ)
  (Γ : Subgroup (GL (Fin 2) ℝ)) [Fact (IsCusp OnePoint.infty Γ)] [Γ.HasDetPlusMinusOne] [DiscreteTopology ↥Γ]
  [ModularFormClass F Γ k] [ModularFormClass F' Γ k] {f : F},
  UpperHalfPlane.IsZeroAtImInfty ⇑f →
    ∀ (f' : F'), ∃ a > 0, UpperHalfPlane.petersson k ⇑f ⇑f' =O[UpperHalfPlane.atImInfty] fun τ => Real.exp (-a * τ.im)
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDF.tendsto_atTop_one : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDF f κ ν →
    ∀ (a : α), ∀ᵐ (b : β) ∂ν a, Filter.Tendsto (f (a, b)) Filter.atTop (nhds 1)
-- Std.Http.Data.Status
/-- 207 Multi-Status
 -/
Std.Http.Status.multiStatus : Std.Http.Status
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Given `e` of the form `k ∣ p` s.t. `e = True` in the core.   -/
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.Algebra.Homology.CochainComplexPlus
/-- The full subcategory of `CochainComplex C ℤ` consisting of bounded below complexes.  -/
CochainComplex.Plus : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Type (max u_1 v_1)
-- Init.Data.List.Erase
List.eraseIdx_zero : ∀ {α : Type u_1} {l : List α}, l.eraseIdx 0 = l.tail
-- Mathlib.Algebra.Ring.Defs
Semiring.toMonoidWithZero : {α : Type u} → [self : Semiring α] → MonoidWithZero α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_of_nonpos_of_le : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddRightMono α] {a b c : α}, a ≤ 0 → b ≤ c → a + b ≤ c
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.j_of_isCharTwoJEqZeroNF : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : W.IsElliptic] [W.IsCharTwoJEqZeroNF],
  W.j = 110592 * W.a₄ ^ 3 / (64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The homotopy "group" indexed by an empty type is in bijection with
the path components of `X`, aka the `ZerothHomotopy`.  -/
homotopyGroupEquivZerothHomotopyOfIsEmpty : {X : Type u_2} →
  [inst : TopologicalSpace X] → (N : Type u_3) → (x : X) → [IsEmpty N] → HomotopyGroup N X x ≃ ZerothHomotopy X
-- Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory
QuadraticModuleCat.cliffordAlgebra_obj_carrier : ∀ {R : Type u} [inst : CommRing R] (M : QuadraticModuleCat R),
  ↑(QuadraticModuleCat.cliffordAlgebra.obj M) = CliffordAlgebra M.form
-- Mathlib.Analysis.Calculus.FDeriv.Basic
Differentiable.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, Differentiable 𝕜 f → DifferentiableAt 𝕜 f x
-- Mathlib.CategoryTheory.Functor.Flat
/-- If `C` is finitely complete, then `F : C ⥤ D` preserves finite limits iff
`Lan F.op : (Cᵒᵖ ⥤ Type*) ⥤ (Dᵒᵖ ⥤ Type*)` preserves finite limits.
 -/
CategoryTheory.preservesFiniteLimits_iff_lan_preservesFiniteLimits : ∀ {C D : Type u₁} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D),
  CategoryTheory.Limits.PreservesFiniteLimits F ↔ CategoryTheory.Limits.PreservesFiniteLimits F.op.lan
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.hasBasis_nhds_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F],
  (nhds 0).HasBasis (fun SV => Bornology.IsVonNBounded 𝕜 SV.1 ∧ SV.2 ∈ nhds 0) fun SV => {f | Set.MapsTo (⇑f) SV.1 SV.2}
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.instHasZeroMorphisms : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → CategoryTheory.Limits.HasZeroMorphisms (HomologicalComplex V c)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.coe_refl : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : Mul α], ⇑(OrderMonoidIso.refl α) = id
-- Mathlib.Data.Set.Subsingleton
Set.antitoneOn_singleton : ∀ {α : Type u} {β : Type v} {a : α} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β), AntitoneOn f {a}
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.mul_polyOfInterest_aux5 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  ↑p ^ (n + 1) * WittVector.polyOfInterest p n = WittVector.remainder p n - WittVector.wittPolyProdRemainder p (n + 1)
-- Init.Data.List.Lemmas
List.getLast_mem : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.getLast h ∈ l
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_mul_omega0`. -/
Ordinal.principal_mul_omega0 : Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) Ordinal.omega0
-- Lean.Data.JsonRpc
Lean.JsonRpc.Response.id : {α : Type u} → Lean.JsonRpc.Response α → Lean.JsonRpc.RequestID
-- Lean.Elab.Command
_private.Lean.Elab.Command.0.Lean.Elab.Command.liftAttrM : {α : Type} → Lean.AttrM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decomposeLinearEquiv_symm_comp_lof : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (ℳ : ι → Submodule R M) [inst_4 : DirectSum.Decomposition ℳ] (i : ι),
  ↑(DirectSum.decomposeLinearEquiv ℳ).symm ∘ₗ DirectSum.lof R ι (fun x => ↥(ℳ x)) i = (ℳ i).subtype
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.definitionProvider : Lean.Lsp.ServerCapabilities → Bool
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.lineMap_toAffineMap : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (p₀ p₁ : P) [inst_5 : TopologicalSpace R]
  [inst_6 : TopologicalSpace V] [inst_7 : ContinuousSMul R V] [inst_8 : ContinuousVAdd V P],
  ↑(ContinuousAffineMap.lineMap p₀ p₁) = AffineMap.lineMap p₀ p₁
-- Mathlib.Data.Setoid.Basic
Setoid.piQuotientEquiv_symm_apply : ∀ {ι : Sort u_4} {α : ι → Sort u_5} (r : (i : ι) → Setoid (α i)) (q : Quotient piSetoid) (i : ι),
  (Setoid.piQuotientEquiv r).symm q i = q.liftOn' (fun x i => Quotient.mk'' (x i)) ⋯ i
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- Via `S.leftHomologyπ : S.cycles ⟶ S.leftHomology`, the object `S.leftHomology` identifies
to the cokernel of `S.toCycles : S.X₁ ⟶ S.cycles`.  -/
CategoryTheory.ShortComplex.leftHomologyIsCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasLeftHomology] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.leftHomologyπ ⋯)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k a fallback : α}
  {v : β}, (t.insertIfNew k v).getKeyD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKeyD a fallback
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_top : ∀ {α : Type u_1} [inst : CompleteLattice α] {L : CompleteSublattice α}, ↑⊤ = ⊤
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.X_ne_zero : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [inst_2 : IsCyclotomicExtension {3} ℚ K], FermatLastTheoremForThreeGen.Solution.X✝ S ≠ 0
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_neg' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : HasDistribNeg α] [inst_2 : GCDMonoid α] {a b : α},
  Associated (gcd a (-b)) (gcd a b)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.coboundaries₁_ext : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{max u u_1, u, u} k G}
  {f₁ f₂ : ↥(groupCohomology.coboundaries₁ A)}, (∀ (g : G), f₁ g = f₂ g) → f₁ = f₂
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.iff_def : ∀ {M : Type u_1} [inst : CommMonoid M] (ζ : M) (k : ℕ), IsPrimitiveRoot ζ k ↔ ζ ^ k = 1 ∧ ∀ (l : ℕ), ζ ^ l = 1 → k ∣ l
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Map `NumDenSameDeg` along a graded ring hom.  -/
HomogeneousLocalization.NumDenSameDeg.map : {ι : Type u_1} →
  {A : Type u_2} →
    {σ : Type u_3} →
      [inst : CommRing A] →
        [inst_1 : SetLike σ A] →
          [AddSubgroupClass σ A] →
            {𝒜 : ι → σ} →
              {B : Type u_4} →
                {τ : Type u_5} →
                  [inst_3 : CommRing B] →
                    [inst_4 : SetLike τ B] →
                      [AddSubgroupClass τ B] →
                        {ℬ : ι → τ} →
                          (f : 𝒜 →+*ᵍ ℬ) →
                            {W₁ : Submonoid A} →
                              {W₂ : Submonoid B} →
                                W₁ ≤ Submonoid.comap f W₂ →
                                  HomogeneousLocalization.NumDenSameDeg 𝒜 W₁ →
                                    HomogeneousLocalization.NumDenSameDeg ℬ W₂
-- Mathlib.Data.Num.Lemmas
/-- Cast a `SNum` to the corresponding integer.  -/
Int.ofSnum : SNum → ℤ
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.IsBase.eq_exchange_of_sdiff_eq_singleton`.

---

If the difference of two IsBases is a singleton, then they differ by an insertion/removal  -/
Matroid.IsBase.eq_exchange_of_diff_eq_singleton : ∀ {α : Type u_1} {M : Matroid α} {B B' : Set α} {e : α},
  M.IsBase B → M.IsBase B' → B \ B' = {e} → ∃ f ∈ B' \ B, B' = insert f B \ {e}
-- Mathlib.Order.OrderIsoNat
le_monotonicSequenceLimit : ∀ {α : Type u_1} [inst : PartialOrder α] [WellFoundedGT α] (a : ℕ →o α) (m : ℕ), a m ≤ monotonicSequenceLimit a