mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Function.Basic
Function.update_eq_self : ∀ {α : Sort u} {β : α → Sort v} [inst : DecidableEq α] (a : α) (f : (a : α) → β a), Function.update f a (f a) = f
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Icc_succ_pred_eq_Ioo : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] [inst_3 : PredOrder α]
  [Nontrivial α] (a b : α), Finset.Icc (Order.succ a) (Order.pred b) = Finset.Ioo a b
-- Mathlib.Tactic.Positivity.Core
_private.Mathlib.Tactic.Positivity.Core.0.Mathlib.Meta.Positivity.OrderRel.lt : Mathlib.Meta.Positivity.OrderRel✝
-- Mathlib.Data.Complex.Basic
Complex.im_sq_le_normSq : ∀ (z : ℂ), z.im * z.im ≤ Complex.normSq z
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.nat_mul_iff : ∀ {p x : ℝ} {n : ℕ}, n ≠ 0 → (LiouvilleWith p (↑n * x) ↔ LiouvilleWith p x)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsInducedSubgraph.trans : ∀ {α : Type u_1} {β : Type u_2} {G G₁ G₂ : Graph α β},
  G.IsInducedSubgraph G₁ → G₁.IsInducedSubgraph G₂ → G.IsInducedSubgraph G₂
-- Mathlib.CategoryTheory.Limits.Types.Limits
/-- (internal implementation) the limit cone of a functor,
implemented as flat sections of a pi type
 -/
CategoryTheory.Limits.Types.Small.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) → [Small.{u, max u v} ↑F.sections] → CategoryTheory.Limits.Cone F
-- Batteries.CodeAction.Attr
/-- The list of tactic code actions to apply when a particular tactic kind is highlighted.  -/
Batteries.CodeAction.TacticCodeActions.onTactic : Batteries.CodeAction.TacticCodeActions → Lean.NameMap (Array Batteries.CodeAction.TacticCodeAction)
-- Mathlib.Order.Bounds.Basic
isLUB_empty : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], IsLUB ∅ ⊥
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.coe_aeval : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {a : σ → S} [inst_4 : IsTopologicalSemiring R] [inst_5 : IsUniformAddGroup R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : CompleteSpace S] [inst_8 : T2Space S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S]
  (ha : MvPowerSeries.HasEval a), ⇑(MvPowerSeries.aeval ha) = MvPowerSeries.eval₂ (algebraMap R S) a
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- Type-alias for modifications between strong transformations of pseudofunctors. This is the type
used for the 2-homomorphisms in the bicategory of pseudofunctors.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Hom : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.Order.SuccPred.Basic
PredOrder.ofCore_pred : ∀ {α : Type u_1} [inst : LinearOrder α] (pred : α → α) (hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b < a ↔ b ≤ pred a)
  (hm : ∀ (a : α), IsMin a → pred a = a) (a : α), PredOrder.pred a = pred a
-- Mathlib.Data.Int.Range
/-- List enumerating `[m, n)`. This is the ℤ variant of `List.Ico`.  -/
Int.range : ℤ → ℤ → List ℤ
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.normed_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {μ : MeasureTheory.Measure E} (f : ContDiffBump 0) (x : E),
  f.normed μ (-x) = f.normed μ x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsAddApply : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], IsAddApply (SchwartzMap E F) E F
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.conjAct_pointwise_smul_iff : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup G} {g : G}, ConjAct.toConjAct g • H = H ↔ g ∈ Subgroup.normalizer ↑H
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instHashableBVBit : Hashable Std.Tactic.BVDecide.BVBit
-- Batteries.Data.Array.Lemmas
Array.extract_append_of_size_left_le_start : ∀ {α : Type u_1} {i j : ℕ} {a b : Array α}, a.size ≤ i → (a ++ b).extract i j = b.extract (i - a.size) (j - a.size)
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.instIsIsoHomology₀εOfIsConnected : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C]
  [X.IsConnected], CategoryTheory.IsIso (X.homology₀ε R)
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.mem_unop : ∀ {M : Type u_2} [inst : Add M] {x : M} {S : AddSubsemigroup Mᵃᵒᵖ}, x ∈ S.unop ↔ AddOpposite.op x ∈ S
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic_dvd_geom_sum_of_dvd : ∀ (R : Type u_1) [inst : Ring R] {d n : ℕ},
  d ∣ n → d ≠ 1 → Polynomial.cyclotomic d R ∣ ∑ i ∈ Finset.range n, Polynomial.X ^ i
-- Mathlib.CategoryTheory.Core
CategoryTheory.Equivalence.core_unitIso_hom_app_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : C ≌ D) (X : CategoryTheory.Core C), (E.core.unitIso.hom.app X).iso.hom = E.unitIso.hom.app X.of
-- Mathlib.Topology.Constructions
instDiscreteTopologyAdditive : ∀ {X : Type u} [inst : TopologicalSpace X] [DiscreteTopology X], DiscreteTopology (Additive X)
-- Mathlib.Tactic.GrindAttrs
/-- A hash set of the grind attributes in Mathlib.

When adding a new grind attribute, manually add it to this hash set as well.  -/
_private.Mathlib.Tactic.GrindAttrs.0.Mathlib.grindAttrs : Std.HashSet Lean.Name
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.frontier_closedBall_eq_empty : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] (x : X) {r : ℝ},
  r ≠ 0 → frontier (Metric.closedBall x r) = ∅
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Exception.revertFailure.injEq : ∀ (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (toRevert : Array Lean.Expr) (varName : String)
  (mctx_1 : Lean.MetavarContext) (lctx_1 : Lean.LocalContext) (toRevert_1 : Array Lean.Expr) (varName_1 : String),
  (Lean.MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert varName =
      Lean.MetavarContext.MkBinding.Exception.revertFailure mctx_1 lctx_1 toRevert_1 varName_1) =
    (mctx = mctx_1 ∧ lctx = lctx_1 ∧ toRevert = toRevert_1 ∧ varName = varName_1)
-- Mathlib.Algebra.Homology.Homotopy
HomologicalComplex.instIsMultiplicativeHomotopyEquivalences : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι}, (HomologicalComplex.homotopyEquivalences V c).IsMultiplicative
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toArray_mapM_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → o δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.mapM f it)).toArray =
    (Std.IterM.mapM
        (fun b => do
          let __do_lift ← liftM (f b)
          g __do_lift)
        it).toArray
-- Mathlib.Topology.Algebra.Module.TransferInstance
Equiv.toLinearEquiv_continuousLinearEquiv : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] [inst_1 : AddCommMonoid β]
  [inst_2 : Semiring R] [inst_3 : Module R β] (e : α ≃ β), ↑(Equiv.continuousLinearEquiv R e) = Equiv.linearEquiv R e
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.hasRightKanExtension_of_preserves : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [L.HasRightKanExtension F] [G.PreservesRightKanExtension F L],
  L.HasRightKanExtension (F.comp G)
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- See `Real.log_le_sub_one_of_pos` for the stronger version when `x ≠ 0`.  -/
Real.log_le_self : ∀ {x : ℝ}, 0 ≤ x → Real.log x ≤ x
-- Mathlib.Analysis.Normed.Ring.Basic
SeminormedRing.mk : {α : Type u_5} →
  [toNorm : Norm α] →
    [toRing : Ring α] →
      [toPseudoMetricSpace : PseudoMetricSpace α] →
        (∀ (x y : α), dist x y = ‖-x + y‖) → (∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖) → SeminormedRing α
-- Std.Internal.Parsec.Basic
/-- Parsing failed, returning the position `pos` where the error occurred and the error `err`.
 -/
Std.Internal.Parsec.ParseResult.error : {α ι : Type} → ι → Std.Internal.Parsec.Error → Std.Internal.Parsec.ParseResult α ι
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.coe_mk' : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (f : (i : ι) → β i)
  (s : Trunc { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }), ⇑{ toFun := f, support' := s } = f
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {km : α}
  {hc : t.contains km = true}, t.max?.get ⋯ = km → t.get km hc = km
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.pushouts_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T.pushouts ≤ T.rlp.llp
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
Summable.mul_left : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : TopologicalSpace α] [IsTopologicalSemiring α] {f : ι → α} (a : α),
  Summable f L → Summable (fun i => a * f i) L
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.isScalarTower_mid : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {α : Type u_1} {β : Type u_2} [inst_3 : SMul α R] [inst_4 : SMul α A] [inst_5 : IsScalarTower α R A]
  [inst_6 : SMul A β] [inst_7 : SMul α β] [IsScalarTower α A β], IsScalarTower α (↥S) β
-- Mathlib.Tactic.Translate.Core
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.shouldTranslateUnsafe.visit : Lean.Environment →
  Mathlib.Tactic.Translate.TranslateData →
    IO.Ref (Array Lean.FVarId) →
      Array Lean.FVarId → Lean.LocalContext → Lean.Expr → ExceptT Lean.Expr (StateT (Lean.PtrSet Lean.Expr) BaseIO) Unit
-- Mathlib.Data.Multiset.Defs
/-- The cardinality of a multiset is the sum of the multiplicities
of all its elements, or simply the length of the underlying list.  -/
Multiset.card : {α : Type u_1} → Multiset α → ℕ
-- Mathlib.Analysis.Meromorphic.Basic
/-- Meromorphy of a function on a set.  -/
MeromorphicOn : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → Set 𝕜 → Prop
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_zero : ENNReal.ofReal 0 = 0
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
/-- If a non-unital star subalgebra of a non-unital topological star algebra is commutative, then
so is its topological closure.

See note [reducible non-instances].  -/
NonUnitalStarSubalgebra.nonUnitalCommRingTopologicalClosure : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : NonUnitalRing A] →
          [inst_3 : Module R A] →
            [inst_4 : Star A] →
              [inst_5 : ContinuousStar A] →
                [inst_6 : ContinuousConstSMul R A] →
                  [inst_7 : IsSemitopologicalRing A] →
                    [T2Space A] →
                      (s : NonUnitalStarSubalgebra R A) →
                        (∀ (x y : ↥s), x * y = y * x) → NonUnitalCommRing ↥s.topologicalClosure
-- Init.Core
ForIn'.mk : {m : Type u₁ → Type u₂} →
  {ρ : Type u} →
    {α : outParam (Type v)} →
      {d : outParam (Membership α ρ)} →
        ({β : Type u₁} → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β) → ForIn' m ρ α d
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.mem_filter_iff : ∀ {α : Type u_1} (B : FilterBasis α) {U : Set α}, U ∈ B.filter ↔ ∃ s ∈ B, s ⊆ U
-- Mathlib.Algebra.Algebra.NonUnitalHom
MulHomClass.toMulHom.congr_simp : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f f_1 : F), f = f_1 → ↑f = ↑f_1
-- Lean.Meta.Sym.AlphaShareBuilder
_private.Lean.Meta.Sym.AlphaShareBuilder.0.Lean.Meta.Sym.Internal.mkAppRangeS.go : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Array Lean.Expr → ℕ → Lean.Expr → ℕ → m Lean.Expr
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- A `σ₁₂`-semilinear isometric embedding of a normed `R`-module into an `R₂`-module,
denoted as `f : E →ₛₗᵢ[σ₁₂] E₂`.  -/
LinearIsometry : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        (R →+* R₂) →
          (E : Type u_11) →
            (E₂ : Type u_12) →
              [inst_2 : SeminormedAddCommGroup E] →
                [inst_3 : SeminormedAddCommGroup E₂] → [Module R E] → [Module R₂ E₂] → Type (max u_11 u_12)
-- Mathlib.Algebra.FreeMonoid.Basic
/-- reverses the symbols in an additive free monoid element  -/
FreeAddMonoid.reverse : {α : Type u_1} → FreeAddMonoid α → FreeAddMonoid α
-- Mathlib.Analysis.Convex.Strict
StrictConvex.add_right : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [ContinuousAdd E] {s : Set E},
  StrictConvex 𝕜 s → ∀ (z : E), StrictConvex 𝕜 ((fun x => x + z) '' s)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
AddLECancellable.add : ∀ {α : Type u_1} [inst : LE α] [inst_1 : AddSemigroup α] {a b : α},
  AddLECancellable a → AddLECancellable b → AddLECancellable (a + b)
-- Init.Data.UInt.Lemmas
UInt64.neg_mul_neg : ∀ (a b : UInt64), -a * -b = a * b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.TheoremGuard.mk : Lean.Expr → Bool → Lean.Meta.Grind.TheoremGuard
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.ConnectedComponent.toSimpleGraph_hom.eq_1 : ∀ {V : Type u} {G : SimpleGraph V} (C : G.ConnectedComponent),
  C.toSimpleGraph_hom = { toFun := fun u => ↑u, map_rel' := ⋯ }
-- Mathlib.RingTheory.PiTensorProduct
/-- The algebra equivalence from the tensor product of the constant family with
value `R` to `R`, given by multiplication of the entries.
 -/
PiTensorProduct.constantBaseRingEquiv : (ι : Type u_1) → (R : Type u_3) → [inst : CommSemiring R] → [Fintype ι] → (PiTensorProduct R fun x => R) ≃ₐ[R] R
-- Mathlib.Algebra.Group.End
Equiv.nsmul_addLeft : ∀ {α : Type u_4} [inst : AddGroup α] (a : α) (n : ℕ), Equiv.addLeft a ^ n = Equiv.addLeft (n • a)
-- Mathlib.Analysis.Convex.Hull
LinearMap.image_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] (f : E →ₗ[𝕜] F) (s : Set E),
  ⇑f '' (convexHull 𝕜) s = (convexHull 𝕜) (⇑f '' s)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
/-- The identity `1` is given by `aⁱ`.
 -/
_private.Mathlib.GroupTheory.SpecificGroups.Quaternion.0.QuaternionGroup.one : {n : ℕ} → QuaternionGroup n
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.faceSingletonComplIso_hom_ι : ∀ {n : ℕ} (i : Fin (n + 2)),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso i).hom (SSet.stdSimplex.face {i}ᶜ).ι =
    SSet.stdSimplex.δ i
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_pos_iff_of_le : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : LinearOrder k] [IsStrictOrderedRing k] [inst_5 : PartialOrder E] [IsOrderedAddMonoid E] [PosSMulMono k E]
  {f : k → E} {x y : k}, x ≤ y → (0 < slope f x y ↔ f x < f y)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.ext : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {x y : CategoryTheory.PreZeroHypercover S},
  x.I₀ = y.I₀ → x.X ≍ y.X → x.f ≍ y.f → x = y
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_prod_list_ofFn : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {n : ℕ} {a : α} {s : Fin n → Finset α},
  a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instModuleFinite : ∀ (p : ENNReal) (K : Type u_1) (V : Type u_4) [inst : Semiring K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V], Module.Finite K (WithLp p V)
-- Lean.Server.Requests
Lean.Server.RequestHandler.mk : (Lean.Json → Except Lean.Server.RequestError Lean.Lsp.DocumentUri) →
  (Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)) →
    Lean.Server.RequestHandler
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
ChartedSpace.locallyRingedSpaceMap.congr_simp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {EM : Type u_1} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_2} [inst_3 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  {M : Type u} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace HM M] {EN : Type u_3}
  [inst_6 : NormedAddCommGroup EN] [inst_7 : NormedSpace 𝕜 EN] {HN : Type u_4} [inst_8 : TopologicalSpace HN]
  {IN : ModelWithCorners 𝕜 EN HN} {N : Type u} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace HN N]
  (f f_1 : M → N) (e_f : f = f_1) (hf : ContMDiff IM IN (↑⊤) f),
  ChartedSpace.locallyRingedSpaceMap f hf = ChartedSpace.locallyRingedSpaceMap f_1 ⋯
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The image of a `NonUnitalSubring` along a ring homomorphism is a `NonUnitalSubring`.  -/
NonUnitalSubring.map : {F : Type w} →
  {R : Type u} →
    {S : Type v} →
      [inst : NonUnitalNonAssocRing R] →
        [inst_1 : NonUnitalNonAssocRing S] →
          [inst_2 : FunLike F R S] → [NonUnitalRingHomClass F R S] → F → NonUnitalSubring R → NonUnitalSubring S
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.cycles j ≅ K.homology j`
when the differential to `j` is zero.  -/
HomologicalComplex.isoHomologyπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            (i j : ι) → c.prev j = i → K.d i j = 0 → [inst_2 : K.HasHomology j] → K.cycles j ≅ K.homology j
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkspaceEdit.instAppend : Append Lean.Lsp.WorkspaceEdit
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.List.merge.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : α) (xs : List α) (y : α) (ys : List α)
  (h_1 : (ys : List α) → motive [] ys) (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match x :: xs, y :: ys with
    | [], ys => h_1 ys
    | xs, [] => h_2 xs
    | x :: xs, y :: ys => h_3 x xs y ys) =
    h_3 x xs y ys
-- Init.Data.SInt.Bitwise
Int32.zero_shiftRight : ∀ {a : Int32}, 0 >>> a = 0
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mor₂_eq_zero_iff_mono₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₂ = 0 ↔ CategoryTheory.Mono T.mor₃
-- Mathlib.CategoryTheory.ComposableArrows.Three
/-- The morphism `mk₂ f₁ f₂ ⟶ mk₂ f₁ f₂₃` when `f₂ ≫ f₃ = f₂₃`.  -/
CategoryTheory.ComposableArrows.threeδ₃Toδ₂ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {i j k l : C} →
      (f₁ : i ⟶ j) →
        (f₂ : j ⟶ k) →
          (f₃ : k ⟶ l) →
            (f₂₃ : j ⟶ l) →
              autoParam (CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
                  CategoryTheory.ComposableArrows.threeδ₃Toδ₂._auto_1 →
                (CategoryTheory.ComposableArrows.mk₂ f₁ f₂ ⟶ CategoryTheory.ComposableArrows.mk₂ f₁ f₂₃)
-- Mathlib.Analysis.Calculus.DifferentialForm.VectorField
/-- Let `ω` be a differentiable `n`-form and `V i` be `n + 1` differentiable vector fields.
If `V i` pairwise commute at `x`, i.e., $[V_i, V_j](x) = 0$ for all `i ≠ j`, then

$$
  dω(V_0(x), \dots, V_{n + 1}(x)) = \sum_{i=0}^{n + 1} (-1)^i •
    D_x\left(ω\big(x; V_0(x), \dots, \widehat{V_i(x)}, \dots, V_{n + 1}(x)\big)\right)(V_i(x)).
$$
 -/
extDerivWithin_apply_vectorField_of_pairwise_commute : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {s : Set E} {x : E}
  {ω : E → E [⋀^Fin n]→L[𝕜] F} {V : Fin (n + 1) → E → E},
  DifferentiableWithinAt 𝕜 ω s x →
    (∀ (i : Fin (n + 1)), DifferentiableWithinAt 𝕜 (V i) s x) →
      UniqueDiffWithinAt 𝕜 s x →
        (Pairwise fun i j => VectorField.lieBracketWithin 𝕜 (V i) (V j) s x = 0) →
          ((extDerivWithin ω s x) fun x_1 => V x_1 x) =
            ∑ i, (-1) ^ ↑i • (fderivWithin 𝕜 (fun x => (ω x) (i.removeNth fun x_1 => V x_1 x)) s x) (V i x)
-- Mathlib.Order.Defs.LinearOrder
max_left_comm : ∀ {α : Type u_1} [inst : LinearOrder α] (a b c : α), max a (max b c) = max b (max a c)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.precomp_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left) (a : Fin (n + 1 + 1)), (F.precomp f).obj a = CategoryTheory.ComposableArrows.Precomp.obj F X a
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.instReprCheckResult : Repr Lean.Meta.Grind.CheckResult
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Finset.prod_eq_zero : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : CommMonoidWithZero M₀] {f : ι → M₀} {s : Finset ι} {i : ι},
  i ∈ s → f i = 0 → ∏ j ∈ s, f j = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The multiplication morphism of a monoid object.  -/
CategoryTheory.MonObj.mul : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.MonoidalCategory C} →
      {X : C} → [self : CategoryTheory.MonObj X] → CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X
-- Std.Async.Basic
Std.Async.EAsync.instMonadLiftEIO_1 : {ε : Type} → MonadLift (EIO ε) (Std.Async.EAsync ε)
-- Init.Data.Slice.List.Basic
/-- The maximum length of the slice, starting at the beginning of `list`.  -/
Std.Slice.Internal.ListSliceData.stop : {α : Type u} → Std.Slice.Internal.ListSliceData α → Option ℕ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.not_revMatchesAt_or_isLongestRevMatchAt_skipSuffixWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  (s : String.Slice),
  ¬String.Slice.Pattern.Model.RevMatchesAt pat (s.skipSuffixWhile pat) ∨
    String.Slice.Pattern.Model.IsLongestRevMatchAt pat (s.skipSuffixWhile pat) (s.skipSuffixWhile pat)
-- Mathlib.Topology.Defs.Induced
/-- An open embedding is an embedding with open range.  -/
Topology.IsOpenEmbedding : {X : Type u_1} → {Y : Type u_2} → [tX : TopologicalSpace X] → [tY : TopologicalSpace Y] → (X → Y) → Prop