mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- The forgetful monoidal functor from a full monoidal subcategory into the original category
("forgetting" the condition).
 -/
CategoryTheory.ObjectProperty.monoidalι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (P : CategoryTheory.ObjectProperty C) → [inst_2 : P.IsMonoidal] → P.ι.Monoidal
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
ContDiff.sigmoid : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  ContDiff ℝ ⊤ f → ContDiff ℝ ⊤ (Real.sigmoid ∘ f)
-- Std.Internal.UV.System
/-- Represents resource usage statistics for a process or thread.
All time values are in milliseconds.
 -/
Std.Internal.UV.System.RUsage : Type
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_le_one_iff_val_nonneg : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]), ‖x‖ ≤ 1 ↔ 0 ≤ x.valuation
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_eq_mapDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_12} [inst : AddCommMonoid M] (f : α ≃ β) (l : α →₀ M),
  Finsupp.equivMapDomain f l = Finsupp.mapDomain (⇑f) l
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : β → γ} (κ : ProbabilityTheory.Kernel α β),
  Measurable f → ∀ (a : α), (κ.map f) a = MeasureTheory.Measure.map f (κ a)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxc.Iterator.toList_eq_match.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((a : α) → motive (some a)) → motive x
-- Lean.Meta.Eqns
_private.Lean.Meta.Eqns.0.Lean.Meta.alreadyGenerated?.loop : Lean.Name → Lean.Environment → ℕ → Array Lean.Name → Lean.MetaM (Array Lean.Name)
-- Mathlib.Algebra.CharP.MixedCharZero
/-- Reduction to `I` prime ideal: When proving statements about mixed characteristic rings,
after we reduced to `p` prime, we can assume that the ideal `I` in the definition is maximal.
 -/
MixedCharZero.reduce_to_maximal_ideal : ∀ (R : Type u_1) [inst : CommRing R] {p : ℕ},
  Nat.Prime p → ((∃ I, I ≠ ⊤ ∧ CharP (R ⧸ I) p) ↔ ∃ I, I.IsMaximal ∧ CharP (R ⧸ I) p)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left_assoc : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
        (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm'))
      h
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval : ∀ {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} [inst : AddCommMonoid M] [inst_1 : Semiring R]
  [inst_2 : Module R M] [inst_3 : Semiring R₁] [inst_4 : Module R₁ M] [inst_5 : Semiring R₂] [inst_6 : Module R₂ M]
  {l₁ l₂ : Mathlib.Tactic.Module.NF R M} {l₁' : Mathlib.Tactic.Module.NF R₁ M} {l₂' : Mathlib.Tactic.Module.NF R₂ M}
  {x₁ x₂ : M}, x₁ = l₁'.eval → x₂ = l₂'.eval → l₁.eval = l₁'.eval → l₂.eval = l₂'.eval → l₁.eval = l₂.eval → x₁ = x₂
-- Init.Prelude
/-- Low-level quotient types. Quotient types coarsen the propositional equality for a type `α`, so that
terms related by some relation `r` are considered equal in `Quot r`.

Set-theoretically, `Quot r` can be seen as the set of equivalence classes of `α` modulo `r`.
Functions from `Quot r` must prove that they respect `r`: to define a function `f : Quot r → β`,
it is necessary to provide `f' : α → β` and prove that for all `x : α` and `y : α`,
`r x y → f' x = f' y`.

`Quot` is a built-in primitive:
 * `Quot.mk` places elements of the underlying type `α` into the quotient.
 * `Quot.lift` allows the definition of functions from the quotient to some other type.
 * `Quot.sound` asserts the equality of elements related by `r`.
 * `Quot.ind` is used to write proofs about quotients by assuming that all elements are constructed
   with `Quot.mk`.

The relation `r` is not required to be an equivalence relation; the resulting quotient type's
equality extends `r` to an equivalence as a consequence of the rules for equality and quotients.
When `r` is an equivalence relation, it can be more convenient to use the higher-level type
`Quotient`.
 -/
Quot : {α : Sort u} → (α → α → Prop) → Sort u
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.symm : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.symm.IsImage t s
-- Mathlib.Algebra.GroupWithZero.Indicator
Set.indicator_const_mul : ∀ {ι : Type u_1} {M₀ : Type u_4} [inst : MulZeroClass M₀] (s : Set ι) (f : ι → M₀) (a : M₀) (i : ι),
  s.indicator (fun x => a * f x) i = a * s.indicator f i
-- Mathlib.Tactic.DeriveTraversable
/-- For a sum type `inductive Foo (α : Type) | foo1 : List α → ℕ → Foo α | ...`
``traverseConstructor `foo1 `Foo applInst f `α `β [`(x : List α), `(y : ℕ)]``
synthesizes `foo1 <$> traverse f x <*> pure y`.  -/
Mathlib.Deriving.Traversable.traverseConstructor : Lean.Name →
  Lean.Name →
    Lean.Expr →
      Lean.Expr →
        Lean.Expr → Lean.Expr → List Lean.Expr → List (Bool × Lean.Expr) → Lean.MVarId → Lean.Elab.TermElabM Unit
-- Std.Do.WP.SimpLemmas
Std.Do.WP.get_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} {Q : Std.Do.PostCond σ (Std.Do.PostShape.arg σ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps], (Std.Do.wp MonadStateOf.get).apply Q = fun s => Q.1 s s
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.min_le_mk_div : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (a b : M),
  min (MulArchimedeanClass.mk a) (MulArchimedeanClass.mk b) ≤ MulArchimedeanClass.mk (a / b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.distinct_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) t.keys
-- Init.Data.List.Lemmas
List.foldl_flatten : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {b : β} {L : List (List α)},
  List.foldl f b L.flatten = List.foldl (fun b l => List.foldl f b l) b L
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.mk : {α : Type u_8} →
  {β : Type u_9} →
    [inst : SupSet α] →
      [inst_1 : SupSet β] → (toFun : α → β) → (∀ (s : Set α), toFun (sSup s) = sSup (toFun '' s)) → sSupHom α β
-- Mathlib.Algebra.Lie.Abelian
/-- A Lie algebra is Abelian iff it is trivial as a Lie module over itself.  -/
IsLieAbelian : (L : Type v) → [Bracket L L] → [Zero L] → Prop
-- Mathlib.Order.Interval.Basic
NonemptyInterval.mk.inj : ∀ {α : Type u_6} {inst : LE α} {toProd : α × α} {fst_le_snd : toProd.1 ≤ toProd.2} {toProd_1 : α × α}
  {fst_le_snd_1 : toProd_1.1 ≤ toProd_1.2},
  { toProd := toProd, fst_le_snd := fst_le_snd } = { toProd := toProd_1, fst_le_snd := fst_le_snd_1 } →
    toProd = toProd_1
-- Mathlib.SetTheory.ZFC.Class
instSDiffClass : SDiff Class.{u_1}
-- Init.Core
/-- A commutative operation satisfies `a ∘ b = b ∘ a`.  -/
Std.Commutative.comm : ∀ {α : Sort u} {op : α → α → α} [self : Std.Commutative op] (a b : α), op a b = op b a
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- If `f` and `g` are homotopic relative to a precylinder `P`, then `g` and `f`
are homotopic relative to `P.symm`  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy.symm : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {P : HomotopicalAlgebra.Precylinder X} → {Y : C} → {f g : X ⟶ Y} → P.LeftHomotopy f g → P.symm.LeftHomotopy g f
-- Mathlib.Algebra.Order.Hom.Basic
AddGroupSeminormClass.toSubadditiveHomClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : AddGroup α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : AddGroupSeminormClass F α β], SubadditiveHomClass F α β
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_eLpNorm_one_densityProcess_limitProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s →
        Filter.Tendsto
          (fun n =>
            MeasureTheory.eLpNorm
              ((fun x => κ.densityProcess ν n a x s) -
                MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s)
                  (ProbabilityTheory.countableFiltration γ) (ν a))
              1 (ν a))
          Filter.atTop (nhds 0)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, (m.getKey? a).isSome = m.contains a
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isColoop_iff_forall_notMem_isCircuit : ∀ {α : Type u_1} {M : Matroid α} {e : α},
  autoParam (e ∈ M.E) Matroid.isColoop_iff_forall_notMem_isCircuit._auto_1 →
    (M.IsColoop e ↔ ∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C)
-- Mathlib.Algebra.GroupWithZero.Nat
Nat.instIsCancelMulZero : IsCancelMulZero ℕ
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- If `Indep` has the 'compactness' property that each set `I` satisfies `Indep I` if and only if
`Indep J` for every finite subset `J` of `I`,
then an `IndepMatroid` can be constructed without proving the maximality axiom.
This needs choice, since it can be used to prove that every vector space has a basis.  -/
IndepMatroid.ofFinitary : {α : Type u_1} →
  (E : Set α) →
    (Indep : Set α → Prop) →
      Indep ∅ →
        (∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I) →
          (∀ ⦃I B : Set α⦄, Indep I → ¬Maximal Indep I → Maximal Indep B → ∃ x ∈ B \ I, Indep (insert x I)) →
            (∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I) → (∀ (I : Set α), Indep I → I ⊆ E) → IndepMatroid α
-- Mathlib.Order.Filter.Extr
Filter.EventuallyEq.isMinFilter_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  f =ᶠ[l] g → f a = g a → (IsMinFilter f l a ↔ IsMinFilter g l a)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- There is a homomorphism to a graph from a comapped graph.
When the function is injective, this is an embedding (see `SimpleGraph.Embedding.comap`).  -/
SimpleGraph.Hom.comap : {V : Type u_1} → {W : Type u_2} → (f : V → W) → (G : SimpleGraph W) → SimpleGraph.comap f G →g G
-- Init.Data.Stream
Std.instStreamList : {α : Type u_1} → Std.Stream (List α) α
-- Mathlib.Data.List.Permutation
/-- The `f` argument to `permutationsAux2` when `r = []` can be eliminated.  -/
List.map_permutationsAux2 : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts ys : List α) (f : List α → β),
  List.map f (List.permutationsAux2 t ts [] ys id).2 = (List.permutationsAux2 t ts [] ys f).2
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring.inj : ∀ {id id_1 : ℕ},
  Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring id = Lean.Meta.Sym.Arith.ClassifyResult.nonCommSemiring id_1 →
    id = id_1
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.eq_empty : ∀ (x : ZFSet.{u}), x = ∅ ↔ ∀ (y : ZFSet.{u}), y ∉ x
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- If there is a primitive `n`-th root of unity in `K`, then
`∏ i ∈ Nat.divisors n, cyclotomic' i K = X ^ n - 1`.  -/
Polynomial.prod_cyclotomic'_eq_X_pow_sub_one : ∀ {K : Type u_2} [inst : CommRing K] [inst_1 : IsDomain K] {ζ : K} {n : ℕ},
  0 < n → IsPrimitiveRoot ζ n → ∏ i ∈ n.divisors, Polynomial.cyclotomic' i K = Polynomial.X ^ n - 1
-- Lean.Log
/-- Return the position (as `String.Pos.Raw`) associated with the current reference syntax (i.e., the syntax object returned by `getRef`.)
 -/
Lean.getRefPos : {m : Type → Type} → [Monad m] → [Lean.MonadLog m] → m String.Pos.Raw
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.finite_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, (-s).Finite ↔ s.Finite
-- Mathlib.Topology.MetricSpace.Congruence
congruent_comm : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂], Congruent v₁ v₂ ↔ Congruent v₂ v₁
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobjectMap_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.Limits.kernelSubobjectMap (CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core.injEq : ∀ (e : Lean.Expr) (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) (e_1 : Lean.Expr)
  (lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr),
  (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core e lhs rhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core e_1 lhs_1 rhs_1) =
    (e = e_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1)
-- Mathlib.Data.Set.Card
Function.Injective.encard_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set α), (f '' s).encard = s.encard
-- Mathlib.Analysis.Normed.Operator.Basic
/-- If one controls the norm of every `A x`, `‖x‖ ≠ 0`, then one controls the norm of `A`.  -/
ContinuousLinearMap.opNorm_le_bound' : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) {M : ℝ},
  0 ≤ M → (∀ (x : E), ‖x‖ ≠ 0 → ‖f x‖ ≤ M * ‖x‖) → ‖f‖ ≤ M
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.chainTopCoeff_neg : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  LieModule.chainTopCoeff (-α) β = LieModule.chainBotCoeff α β
-- Mathlib.Data.List.Basic
List.idxOf_of_notMem : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α} {a : α}, a ∉ l → List.idxOf a l = l.length
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.coe_prodEqualWeights : ∀ {ι : Type} {s : Finset ι} {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne]
  (F : ι → ModularForm Γ k), ⇑(ModularForm.prodEqualWeights F) = ∏ i ∈ s, ⇑(F i)
-- Init.Data.Vector.Attach
Vector.count_attachWith : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {p : α → Prop} {xs : Vector α n} (H : ∀ a ∈ xs, p a) {a : { x // p x }},
  Vector.count a (xs.attachWith p H) = Vector.count (↑a) xs
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionOptions : Lean.ToJson Lean.Lsp.CompletionOptions
-- Init.Data.List.MinMaxOn
List.minOn?_singleton : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {x : α} {f : α → β}, List.minOn? f [x] = some x
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.instEssSurjDecomposedDecomposedTo : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], (CategoryTheory.decomposedTo J).EssSurj
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.freeAddGroupCongr_refl : ∀ {α : Type u}, FreeAddGroup.freeAddGroupCongr (Equiv.refl α) = AddEquiv.refl (FreeAddGroup α)
-- Mathlib.Data.Nat.Prime.Basic
Nat.ne_one_iff_exists_prime_dvd : ∀ {n : ℕ}, n ≠ 1 ↔ ∃ p, Nat.Prime p ∧ p ∣ n
-- Mathlib.Topology.Algebra.Monoid
continuousAdd_inf : ∀ {M : Type u_3} [inst : Add M] {t₁ t₂ : TopologicalSpace M}, ContinuousAdd M → ContinuousAdd M → ContinuousAdd M
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSub_smul : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {G : Type u_6} [inst_3 : Group G] [inst_4 : DistribMulAction G V] [SMulCommClass G k V] {s : Finset ι} {w : ι → k},
  ∑ i ∈ s, w i = 0 → ∀ (p : ι → V) (a : G), (s.weightedVSub (a • p)) w = a • (s.weightedVSub p) w
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- Inverse of a diffeomorphism.  -/
Diffeomorph.symm : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_4} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_7} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 F G} →
                            {M : Type u_9} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_11} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] →
                                        {n : WithTop ℕ∞} → Diffeomorph I J M N n → Diffeomorph J I N M n
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.ExtraTheorem.const : Lean.Name → Lean.Elab.Tactic.Grind.ExtraTheorem
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.comp_id : ∀ {β : Type u_3} {γ : Type u_4} [inst : OmegaCompletePartialOrder β] [inst_1 : OmegaCompletePartialOrder γ]
  (f : β →𝒄 γ), f.comp OmegaCompletePartialOrder.ContinuousHom.id = f
-- Init.Data.Nat.Lemmas
Nat.two_pow_sub_two_pow_pred : ∀ {w : ℕ}, 0 < w → 2 ^ w - 2 ^ (w - 1) = 2 ^ (w - 1)
-- Lean.Data.PersistentArray
Lean.PersistentArray.findSomeMAux : {α : Type u} →
  {m : Type v → Type w} → [Monad m] → {β : Type v} → (α → m (Option β)) → Lean.PersistentArrayNode α → m (Option β)
-- Batteries.Data.List.Interleave
List.interleave_append_append_of_length_eq_length : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.length = l₂.length → ∀ (l₃ l₄ : List α), (l₁ ++ l₃).interleave (l₂ ++ l₄) = l₁.interleave l₂ ++ l₃.interleave l₄
-- Mathlib.GroupTheory.Coprod.Basic
/-- The natural projection `M ∗ N →* N`.  -/
Monoid.Coprod.snd : {M : Type u_1} → {N : Type u_2} → [inst : Monoid M] → [inst_1 : Monoid N] → Monoid.Coprod M N →* N
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterStep.bundledQuotient.eq_1 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] [inst_1 : Monad m]
  [inst_2 : LawfulMonad m] (step : Std.IterStep (Std.IterM m β) β),
  step.bundledQuotient = Std.IterStep.mapIterator (Quot.mk (Std.BundledIterM.Equiv m β) ∘ Std.BundledIterM.ofIterM) step
-- Mathlib.Topology.Connected.Clopen
isClopen_preimage_val : ∀ {X : Type u_3} [inst : TopologicalSpace X] {u v : Set X},
  IsOpen u → Disjoint (frontier u) v → IsClopen (Subtype.val ⁻¹' u)
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) The limit cone restricted to `Over i'`. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.c' : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            [inst_1 : ∀ (i : I), CompactSpace ↥(D.obj i)] →
              [inst_2 : CategoryTheory.IsCofiltered I] →
                [inst_3 : ∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] →
                  (A : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) →
                    (j : A.𝒰D.I₀) → CategoryTheory.Limits.Cone (A.D' j)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
/-- A function `f : ℍ → α` is bounded at infinity if it is bounded along `atImInfty`.  -/
UpperHalfPlane.IsBoundedAtImInfty : {α : Type u_1} → [Norm α] → (UpperHalfPlane → α) → Prop
-- Batteries.Data.MLList.Basic
/-- Convert a `List` to a `MLList`.  -/
MLList.ofList : {α : Type u_1} → {m : Type u_1 → Type u_1} → List α → MLList m α
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.Sheaf.toImage_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F') {Z : CategoryTheory.Sheaf J (Type w)} (h : F' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sheaf.toImage f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Sheaf.imageι f) h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.iff_of_isPushout : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {Z X Y A : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ A} {inr : Y ⟶ A} [P.IsStableUnderCobaseChange] [P.CodescendsAlong Q],
  CategoryTheory.IsPushout f g inl inr → Q f → (P inl ↔ P g)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.contains_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Mathlib.Algebra.Module.FinitePresentation
/-- Let `M` be a finitely presented `R`-module, `N` an `R`-module, `S : Submonoid R`.
The linear equivalence between the `M →ₗ[R] N` localized at `S` and
`LocalizedModule S M →ₗ[Localization S] LocalizedModule S N`
 -/
Module.FinitePresentation.linearEquivMapExtendScalars : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] →
                (S : Submonoid R) →
                  [Module.FinitePresentation R M] →
                    LocalizedModule S (M →ₗ[R] N) ≃ₗ[R] LocalizedModule S M →ₗ[Localization S] LocalizedModule S N
-- Mathlib.Algebra.Ring.IsFormallyReal
IsSumNonzeroSq.isSumSq : ∀ {R : Type u_1} [inst : AddMonoid R] [inst_1 : Mul R] {s : R}, IsSumNonzeroSq s → IsSumSq s
-- Mathlib.Algebra.Group.Center
Set.centralizer_subset : ∀ {M : Type u_1} {S T : Set M} [inst : Mul M], S ⊆ T → T.centralizer ⊆ S.centralizer
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesRegistrationOptions.mk : Array Lean.Lsp.FileSystemWatcher → Lean.Lsp.DidChangeWatchedFilesRegistrationOptions
-- Mathlib.Order.Antisymmetrization
not_lt_of_antisymmRel : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → ¬a < b
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep2.mk : List Lean.Constructor →
  StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit →
    StateRefT' IO.RealWorld Lean.CollectLevelMVars.State Lean.MetaM Unit →
      (ℕ → Lean.Level → Lean.Elab.TermElabM Unit) →
        Lean.Elab.TermElabM Unit →
          (List Lean.Name →
              Array Lean.Expr →
                (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.Elab.TermElabM Lean.Elab.Command.InductiveElabStep3) →
            Lean.Elab.Command.InductiveElabStep2