mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insertIfNew!_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {kmi : α},
  (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey?.get ⋯ = kmi → (compare kmi k).isLE = true
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.not_isPreconnected_compl_pair : ∀ {x y : Circle}, x ≠ y → ¬IsPreconnected {x, y}ᶜ
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- The Radon-Nikodym derivative between a complex measure and a positive measure.  -/
MeasureTheory.ComplexMeasure.rnDeriv : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.ComplexMeasure α → MeasureTheory.Measure α → α → ℂ
-- Mathlib.Analysis.SpecialFunctions.NonIntegrable
/-- If `f` is differentiable in a punctured neighborhood of `c`, `‖f x‖ → ∞` as `x → c` (more
formally, along the filter `𝓝[≠] c`), and `f' = O(g)` along `𝓝[≠] c`, where `f'` is the derivative
of `f`, then `g` is not interval integrable on any nontrivial interval `a..b` such that
`c ∈ [a, b]`.  -/
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  {f : ℝ → E} {g : ℝ → F} {a b c : ℝ},
  (∀ᶠ (x : ℝ) in nhdsWithin c {c}ᶜ, DifferentiableAt ℝ f x) →
    Filter.Tendsto (fun x => ‖f x‖) (nhdsWithin c {c}ᶜ) Filter.atTop →
      deriv f =O[nhdsWithin c {c}ᶜ] g → a ≠ b → c ∈ Set.uIcc a b → ¬IntervalIntegrable g MeasureTheory.volume a b
-- Mathlib.Analysis.Complex.IsIntegral
Complex.isIntegral_rat_I : IsIntegral ℚ Complex.I
-- Init.Data.Nat.Lemmas
Nat.one_lt_pow_iff : ∀ {n : ℕ}, n ≠ 0 → ∀ {a : ℕ}, 1 < a ^ n ↔ 1 < a
-- Aesop.Tree.ExtractProof
_private.Aesop.Tree.ExtractProof.0.Aesop.extractSafePrefixRapp : Lean.Environment → Lean.MVarId → Aesop.Rapp → Aesop.SafePrefixM✝ Unit
-- Lean.Environment
_private.Lean.Environment.0.Lean.AsyncContext.mkRaw : Lean.Name → List Lean.Name → Lean.AsyncContext✝
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.PublishDiagnosticsParams.diagnostics : Lean.Lsp.PublishDiagnosticsParams → Array Lean.Lsp.Diagnostic
-- Mathlib.RingTheory.Congruence.Basic
/-- The complete lattice of congruence relations on a given type with multiplication and
addition.  -/
RingCon.instCompleteLattice : {R : Type u_3} → [inst : Add R] → [inst_1 : Mul R] → CompleteLattice (RingCon R)
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- **Alias** of the forward direction of `MeasureTheory.withDensity_eq_zero_iff`. -/
MeasureTheory.withDensity_eq_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ → μ.withDensity f = 0 → f =ᵐ[μ] 0
-- Mathlib.Algebra.Category.Grp.Basic
MulEquiv.toGrpIso_inv : ∀ {X Y : GrpCat} (e : ↑X ≃* ↑Y), e.toGrpIso.inv = GrpCat.ofHom e.symm.toMonoidHom
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.mem_op : ∀ {M : Type u_2} [inst : Add M] {x : Mᵃᵒᵖ} {S : AddSubsemigroup M}, x ∈ S.op ↔ AddOpposite.unop x ∈ S
-- Mathlib.Algebra.Group.Prod
Prod.instIsCancelMul : ∀ {G : Type u_1} {H : Type u_2} [inst : Mul G] [inst_1 : Mul H] [IsCancelMul G] [IsCancelMul H], IsCancelMul (G × H)
-- Init.Data.UInt.Bitwise
USize.not_and_self : ∀ {a : USize}, ~~~a &&& a = 0
-- Mathlib.Analysis.SpecialFunctions.Log.Summable
/-- In a complete normed ring, `∏' i, (1 + f i)` is convergent if the sum of real numbers
`∑' i, ‖f i‖` is convergent.  -/
multipliable_one_add_of_summable : ∀ {ι : Type u_1} {R : Type u_2} [inst : NormedCommRing R] [NormOneClass R] {f : ι → R} [CompleteSpace R],
  (Summable fun i => ‖f i‖) → Multipliable fun i => 1 + f i
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- Given `f` a multilinear map, then the derivative of `x ↦ f (g₁ x, ..., gₙ x)` at `x` applied
to a vector `v` is given by `∑ i, f (g₁ x, ..., g'ᵢ v, ..., gₙ x)`. Version inside a set.  -/
HasFDerivWithinAt.multilinear_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {ι : Type u_2} {E : ι → Type u_3} [inst_3 : (i : ι) → NormedAddCommGroup (E i)]
  [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_5 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E F)
  [inst_6 : DecidableEq ι] {G : Type u_4} [inst_7 : NormedAddCommGroup G] [inst_8 : NormedSpace 𝕜 G]
  {g : (i : ι) → G → E i} {g' : (i : ι) → G →L[𝕜] E i} {s : Set G} {x : G},
  (∀ (i : ι), HasFDerivWithinAt (g i) (g' i) s x) →
    HasFDerivWithinAt (fun x => f fun i => g i x) (∑ i, f.toContinuousLinearMap (fun j => g j x) i ∘SL g' i) s x
-- Mathlib.Data.Sym.Sym2
Sym2.isDiag_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (z : Sym2 α), z.IsDiag
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.GeneralLinearGroup.upperRightHom_apply : ∀ {R : Type u_1} [inst : Ring R] (x : R),
  Matrix.GeneralLinearGroup.upperRightHom x =
    { val := !![1, x; 0, 1], inv := !![1, -x; 0, 1], val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Set.Finite.nullMeasurableSet_sUnion : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)},
  s.Finite → (∀ t ∈ s, MeasureTheory.NullMeasurableSet t μ) → MeasureTheory.NullMeasurableSet (⋃₀ s) μ
-- Mathlib.GroupTheory.Coxeter.Basic
_private.Mathlib.GroupTheory.Coxeter.Basic.0.CoxeterSystem.restrictUnit.eq_1 : ∀ {B : Type u_1} {M : CoxeterMatrix B} {G : Type u_5} [inst : Monoid G] {f : B → G} (hf : M.IsLiftable f) (i : B),
  CoxeterSystem.restrictUnit✝ hf i = { val := f i, inv := f i, val_inv := ⋯, inv_val := ⋯ }
-- Mathlib.CategoryTheory.Yoneda
/-- We have a type-level equivalence between natural transformations from the coyoneda embedding
and elements of `F.obj X.unop`, without any universe switching.
 -/
CategoryTheory.coyonedaEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → {F : CategoryTheory.Functor C (Type v₁)} → (CategoryTheory.coyoneda.obj (Opposite.op X) ⟶ F) ≃ F.obj X
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubringClass.coe_subtype : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : SetLike S R] [hSR : NonUnitalSubringClass S R]
  (s : S), ⇑(NonUnitalSubringClass.subtype s) = Subtype.val
-- Mathlib.Analysis.Normed.Group.Uniform
dist_sub_sub_le_of_le : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] {a₁ a₂ b₁ b₂ : E} {r₁ r₂ : ℝ},
  dist a₁ b₁ ≤ r₁ → dist a₂ b₂ ≤ r₂ → dist (a₁ - a₂) (b₁ - b₂) ≤ r₁ + r₂
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasRightResolutions_of_iso_of_essSurj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.EssSurj] [W₂'.RespectsIso]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [T.HasRightResolutions], B.HasRightResolutions
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.subtype_apply : ∀ {K : Type u} [inst : Field K] {R : ValuationSubring K} (x : ↥R), R.subtype x = ↑x
-- Lean.Data.KVMap
/-- Update a `Name` entry based on its current value.  -/
Lean.KVMap.updateName : Lean.KVMap → Lean.Name → (Lean.Name → Lean.Name) → Lean.KVMap
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.hom_ext_iff : ∀ {X Y : Semigrp} {f g : X ⟶ Y}, f = g ↔ Semigrp.Hom.hom f = Semigrp.Hom.hom g
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.hasForgetToAddMonCat : CategoryTheory.HasForget₂ AddCommMonCat AddMonCat
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.baseChange_negAddY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Projective R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P Q : Fin 3 → A), (W'.baseChange B).negAddY (⇑f ∘ P) (⇑f ∘ Q) = f ((W'.baseChange A).negAddY P Q)
-- Mathlib.Topology.Compactness.Compact
/-- If a filter is disjoint from the cocompact filter, so is its image under any continuous
function.  -/
disjoint_map_cocompact : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {g : X → Y} {f : Filter X},
  Continuous g → Disjoint f (Filter.cocompact X) → Disjoint (Filter.map g f) (Filter.cocompact Y)
-- Lean.Meta.Tactic.Grind.Types
/-- An entry `{thm_1, ..., thm_n} => {thm}`. Each `thm_i` and `thm` is the proof of a theorem instance.
It means terms created while instantiating `thm_i` were used to create theorem `thm`.
 -/
Lean.Meta.Grind.EMatchDiagInfo : Type
-- Mathlib.Order.Interval.Set.Basic
Set.notMem_Ioc_of_gt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a < c → c ∉ Set.Ioc b a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.skipSuffix?_bool_eq_some_iff : ∀ {p : Char → Bool} {s : String} {pos : s.Pos},
  s.skipSuffix? p = some pos ↔ ∃ (h : s.endPos ≠ s.startPos), pos = s.endPos.prev h ∧ p ((s.endPos.prev h).get ⋯) = true
-- ProofWidgets.Component.PenroseDiagram
/-- Add an object of Penrose type `tp`,
corresponding to (and labelled by) the expression `e`,
to the substance program.
Return its Penrose name.  -/
ProofWidgets.Penrose.DiagramBuilderM.addExpr : String → Lean.Expr → ProofWidgets.Penrose.DiagramBuilderM String
-- Mathlib.Data.Int.Order.Basic
/-- **Alias** of the forward direction of `Int.ofNat_lt`. -/
Int.lt_of_ofNat_lt_ofNat : ∀ {n m : ℕ}, ↑n < ↑m → n < m
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'App_hom_apply : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) (M : ModuleCat R) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.restrictScalarsId'App f hf M).hom) x = x
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.denote_mkImpCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input : aig.BinaryInput},
  ⟦assign, aig.mkImpCached input⟧ =
    (!⟦assign, { aig := aig, ref := input.lhs }⟧ || ⟦assign, { aig := aig, ref := input.rhs }⟧)
-- Mathlib.Order.Minimal
image_antitone_setOfPred_minimal : ∀ {α : Type u_2} {β : Type u_3} {P : α → Prop} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  (∀ ⦃x y : α⦄, P x → P y → (f x ≤ f y ↔ y ≤ x)) →
    f '' {x | Minimal P x} = {x | Maximal (fun x => ∃ x₀, P x₀ ∧ f x₀ = x) x}
-- Mathlib.MeasureTheory.Integral.Bochner.L1
_private.Mathlib.MeasureTheory.Integral.Bochner.L1.0.MeasureTheory.L1.SimpleFunc.termIntegral : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Coinvariants
/-- The functor sending `A, B` to `(A ⊗[k] B)_G`. This is naturally isomorphic to the functor
sending `A, B` to `A ⊗[k[G]] B`, where we give `A` the `k[G]ᵐᵒᵖ`-module structure defined by
`g • a := A.ρ g⁻¹ a`.  -/
Rep.coinvariantsTensor : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        CategoryTheory.Functor (Rep.{u, u, v} k G) (CategoryTheory.Functor (Rep.{u, u, v} k G) (ModuleCat k))
-- Mathlib.RingTheory.Congruence.Defs
RingCon.refl : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) (x : R), c x x
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorLeftMopIso_hom_app_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  (X_1 : Cᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.tensorLeftMopIso X).hom.app X_1).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X_1.unmop X)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.enum_succ_eq_top : ∀ {o : Ordinal.{u_4}}, (Ordinal.enum fun x1 x2 => x1 < x2) ⟨o, ⋯⟩ = ⊤
-- Mathlib.Computability.PartrecCode
/-- **Roger's fixed-point theorem**: any total, computable `f` has a fixed point.
That is, under the interpretation given by `Nat.Partrec.Code.eval`, there is a code `c`
such that `c` and `f c` have the same evaluation.
 -/
Nat.Partrec.Code.fixed_point : ∀ {f : Nat.Partrec.Code → Nat.Partrec.Code}, Computable f → ∃ c, (f c).eval = c.eval
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.p_opcyclesMap : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (β : CategoryTheory.ComposableArrows.mk₁ f ⟶ CategoryTheory.ComposableArrows.mk₁ f') (n : ℤ),
  autoParam (β = CategoryTheory.ComposableArrows.homMk₁ (α.app 0) (α.app 1) ⋯)
      CategoryTheory.Abelian.SpectralObject.p_opcyclesMap._auto_1 →
    CategoryTheory.CategoryStruct.comp (X.pOpcycles f g n) (X.opcyclesMap f g f' g' α n) =
      CategoryTheory.CategoryStruct.comp ((X.H n).map β) (X.pOpcycles f' g' n)
-- Mathlib.Order.Disjoint
Disjoint.sup_right : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α},
  Disjoint a b → Disjoint a c → Disjoint a (b ⊔ c)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.mem_toList_iff_mem : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α] {a : α}, a ∈ r.toList ↔ a ∈ r
-- Init.Data.Vector.Range
Vector.find?_range_eq_none : ∀ {n : ℕ} {p : ℕ → Bool}, Vector.find? p (Vector.range n) = none ↔ ∀ i < n, (!p i) = true
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.coeff_mul_X_sub_C : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R} {r : R} {a : ℕ},
  (p * (Polynomial.X - Polynomial.C r)).coeff (a + 1) = p.coeff a - p.coeff (a + 1) * r
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
Bundle.Trivialization.mdifferentiable : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_12} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_13} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {F : Type u_14}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] {M : Type u_15} [inst_6 : TopologicalSpace M]
  [inst_7 : ChartedSpace H M] (Z : M → Type u_16) [inst_8 : TopologicalSpace (Bundle.TotalSpace F Z)]
  [inst_9 : (b : M) → TopologicalSpace (Z b)] [inst_10 : FiberBundle F Z] [inst_11 : (b : M) → AddCommMonoid (Z b)]
  [inst_12 : (b : M) → Module 𝕜 (Z b)] [inst_13 : VectorBundle 𝕜 F Z] [ContMDiffVectorBundle 1 F Z I]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [MemTrivializationAtlas e],
  OpenPartialHomeomorph.MDifferentiable (I.prod (modelWithCornersSelf 𝕜 F)) (I.prod (modelWithCornersSelf 𝕜 F))
    e.toOpenPartialHomeomorph
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_eq_zero : ∀ {M : Type u_1} [inst : MonoidWithZero M] {a : M}, Associates.mk a = 0 ↔ a = 0
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.piEquivalenceFunctorDiscrete_inverse_map : ∀ (J : Type u₂) (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  {X Y : CategoryTheory.Functor (CategoryTheory.Discrete J) C} (f : X ⟶ Y) (j : J),
  (CategoryTheory.piEquivalenceFunctorDiscrete J C).inverse.map f j = f.app { as := j }
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.State.mk.sizeOf_spec : ∀ (visited : Array Lean.Expr) (checked : Std.HashSet Lean.Expr),
  sizeOf { visited := visited, checked := checked } = 1 + sizeOf visited + sizeOf checked
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulRightCLM_apply_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedAddCommGroup G] [inst_7 : NormedSpace ℝ G] [inst_8 : NormedSpace 𝕜 F]
  (L : E →L[ℝ] G →L[ℝ] ℝ) (f : SchwartzMap E F) (x : E), ((SchwartzMap.smulRightCLM 𝕜 F L) f) x = (L x).smulRight (f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel.map_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y X' Y' : C} (f : X ⟶ Y) (f' : X' ⟶ Y') [inst_2 : CategoryTheory.Limits.HasCokernel f]
  [inst_3 : CategoryTheory.Limits.HasCokernel f'] (q : X ⟶ X')
  (w : CategoryTheory.CategoryStruct.comp f 0 = CategoryTheory.CategoryStruct.comp q f'),
  CategoryTheory.Limits.cokernel.map f f' q 0 w = 0
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (R : CategoryTheory.ProjectiveResolution X), QuasiIso R.π'
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
/-- **Alias** of `le_add_of_le_left`. -/
le_add_right : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α] [CanonicallyOrderedAdd α] {a b c : α}, a ≤ b → a ≤ b + c
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lsum_single : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M]
  [inst_5 : AddCommMonoid N] [inst_6 : Module R₂ N] {σ : R →+* R₂} [inst_7 : Module S N] [inst_8 : SMulCommClass R₂ S N]
  (f : α → M →ₛₗ[σ] N) (i : α) (m : M), (((Finsupp.lsum S) f) fun₀ | i => m) = (f i) m
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.killComplFun_monomial_embDomain : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} (x : σ →₀ ℕ) (r : R),
  MvPowerSeries.killComplFun e ((MvPowerSeries.monomial (Finsupp.embDomain e x)) r) = (MvPowerSeries.monomial x) r
-- Mathlib.Topology.Neighborhoods
/-- **Alias** of the reverse direction of `TopologicalSpace.ext_iff_nhds`. -/
TopologicalSpace.ext_nhds : ∀ {X : Type u_2} {t t' : TopologicalSpace X}, (∀ (x : X), nhds x = nhds x) → t = t'
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  UpperSemicontinuousOn f s ↔ ∀ x ∈ s, UpperSemicontinuousWithinAt f s x
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_lt_aleph0 : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c < Cardinal.aleph0 ↔ c < Cardinal.aleph0
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNonUnitalNonAssocSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [NonUnitalNonAssocSemiring β] → NonUnitalNonAssocSemiring (MeasureTheory.SimpleFunc α β)
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
/-- When passed an `Equiv.sumCongr`, `MultilinearMap.domDomCongr` distributes over
`MultilinearMap.domCoprod`.  -/
MultilinearMap.domCoprod_domDomCongr_sumCongr : ∀ {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {ι₃ : Type u_4} {ι₄ : Type u_5} [inst : CommSemiring R] {N₁ : Type u_6}
  [inst_1 : AddCommMonoid N₁] [inst_2 : Module R N₁] {N₂ : Type u_7} [inst_3 : AddCommMonoid N₂] [inst_4 : Module R N₂]
  {N : Type u_8} [inst_5 : AddCommMonoid N] [inst_6 : Module R N] (a : MultilinearMap R (fun x => N) N₁)
  (b : MultilinearMap R (fun x => N) N₂) (σa : ι₁ ≃ ι₃) (σb : ι₂ ≃ ι₄),
  MultilinearMap.domDomCongr (σa.sumCongr σb) (a.domCoprod b) =
    (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.inductiveElabAttr.unsafe_impl_2 : IO (Lean.KeyedDeclsAttribute Lean.Elab.Command.InductiveElabDescr)
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.get' : Lean.Meta.Grind.GoalM Lean.Meta.Grind.Arith.Linear.State
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceLE : Lean.Meta.Simp.Simproc
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesWithinOnBall.fderivWithin_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} {s : Set E} [CompleteSpace F],
  HasFPowerSeriesWithinOnBall f p s x r →
    ∀ {y : E},
      ↑‖y‖₊ < r →
        x + y ∈ insert x s →
          UniqueDiffOn 𝕜 (insert x s) →
            fderivWithin 𝕜 f (insert x s) (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsFReduced : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] [inst_4 : ι.Additive] [inst_5 : CategoryTheory.IsIdempotentComplete A]
  [inst_6 : CategoryTheory.IsIdempotentComplete C], Λ.reduced.F.PreservesZeroMorphisms
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} {fallback : β}, t.isEmpty = true → t.getD a fallback = fallback
-- Lean.Server.Requests
Lean.Server.requestHandlers : IO.Ref (Lean.PersistentHashMap String Lean.Server.RequestHandler)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.eraseMany.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type w} [inst_1 : ForIn Id ρ α] (t : Std.DTreeMap.Internal.Impl α β)
  (l : ρ) (h : t.Balanced),
  t.eraseMany l h =
    (have r := ⟨t, ⋯⟩;
      do
      let __s ←
        forIn l r fun a __s =>
            let r := __s;
            have hr := ⋯;
            have r := ⟨(Std.DTreeMap.Internal.Impl.erase a (↑r) hr).impl, ⋯⟩;
            pure (ForInStep.yield r)
      have r : t.IteratedErasureFrom := __s
      pure r).run
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCocycle.IsCohomologous.class_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : CategoryTheory.Functor Cᵒᵖ GrpCat} {I : Type w'}
  {U : I → C} {γ₁ γ₂ : CategoryTheory.PresheafOfGroups.OneCocycle G U}, γ₁.IsCohomologous γ₂ → γ₁.class = γ₂.class
-- Mathlib.Data.Finmap
Multiset.coe_nodupKeys : ∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)}, (↑l).NodupKeys ↔ l.NodupKeys
-- Init.Data.Array.Lemmas
Array.push_ne_empty : ∀ {α : Type u_1} {a : α} {xs : Array α}, xs.push a ≠ #[]
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
SpectrumRestricts.eq_zero_of_neg : ∀ {A : Type u_1} [inst : CStarAlgebra A] {a : A},
  IsSelfAdjoint a →
    SpectrumRestricts a ⇑ContinuousMap.realToNNReal → SpectrumRestricts (-a) ⇑ContinuousMap.realToNNReal → a = 0
-- Mathlib.Data.Multiset.Defs
Multiset.decidableLE : {α : Type u_1} → [DecidableEq α] → DecidableLE (Multiset α)
-- Mathlib.Topology.Closure
frontier.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), frontier s = closure s \ interior s
-- Mathlib.ModelTheory.Basic
/-- Composition of first-order equivalences.  -/
FirstOrder.Language.Equiv.comp : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type w'} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] → {P : Type u_1} → [inst_2 : L.Structure P] → L.Equiv N P → L.Equiv M N → L.Equiv M P
-- Init.Data.Stream
Stream : Type u_1 → outParam (Type u_2) → Type (max u_1 u_2)