mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Atoms
isLUB_atoms_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α] [IsAtomistic α] [inst_3 : OrderTop α],
  IsLUB {a | IsAtom a} ⊤
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear maps on the left preserves `C^n` functions.  -/
ContDiff.continuousLinearMap_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F} (g : F →L[𝕜] G),
  ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => g (f x)
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : SizeOf R] (toSubring : Subring R) [isLocalRing : IsLocalRing ↥toSubring],
  sizeOf { toSubring := toSubring, isLocalRing := isLocalRing } = 1 + sizeOf toSubring + sizeOf isLocalRing
-- Mathlib.Data.Nat.Dist
Nat.dist_zero_left : ∀ (n : ℕ), Nat.dist 0 n = n
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- A homology data for a short complex `S` induces a homology data for `S.op`.  -/
CategoryTheory.ShortComplex.HomologyData.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → S.HomologyData → S.op.HomologyData
-- Init.Data.UInt.Bitwise
USize.shiftRight_eq_shiftRight_mod : ∀ (a b : USize), a >>> b = a >>> (b % USize.ofNat System.Platform.numBits)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.ext_iff : ∀ {R : Type u} {inst : Semiring R} {M N : SemimoduleCat R} {x y : M.Hom N}, x = y ↔ x.hom' = y.hom'
-- Lean.Parser.Do
Lean.Parser.Term.doLetMetaExpr : Lean.Parser.Parser
-- Mathlib.Data.Finset.Image
/-- Point-free form of `Finset.image_image`: `image` distributes over `Function.comp`.  -/
Finset.image_comp_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : DecidableEq β] {f : α → β} [inst_1 : DecidableEq γ] {g : β → γ},
  Finset.image g ∘ Finset.image f = Finset.image (g ∘ f)
-- Init.Prelude
/-- Applies a function to the current state that both computes a new state and a value. The new state
replaces the current state, and the value is returned.

It is equivalent to `do let (a, s) := f (← get); set s; pure a`. However, using `modifyGet` may
lead to higher performance because it doesn't add a new reference to the state value. Additional
references can inhibit in-place updates of data.
 -/
EStateM.modifyGet : {ε σ α : Type u} → (σ → α × σ) → EStateM ε σ α
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.congr_mul : {R : Type u} →
  [inst : Rack R] →
    {a b a' b' : Rack.PreEnvelGroup R} →
      Rack.PreEnvelGroupRel' R a a' → Rack.PreEnvelGroupRel' R b b' → Rack.PreEnvelGroupRel' R (a.mul b) (a'.mul b')
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- The isomorphism between cohomology groups induced by a group isomorphism `e : G ≃* H` and a
isomorphism between representations (restricted by `e`).  -/
groupCohomology.mapIso : {k G H : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      [inst_2 : Group H] →
        {A : Rep.{u, u, u} k H} →
          {B : Rep.{u, u, u} k G} →
            (e : G ≃* H) →
              (e' : ↑B ≃ₗ[k] ↑A) →
                (∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e') → (n : ℕ) → groupCohomology B n ≅ groupCohomology A n
-- Mathlib.Algebra.Homology.LocalCohomology
localCohomology.instCategorySelfLERadical : {R : Type u_1} →
  [inst : CommRing R] → (J : Ideal R) → CategoryTheory.Category.{u_1, u_1} (localCohomology.SelfLERadical J)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.isEmptyRingEquiv_symm_toRingHom : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] [inst_1 : IsEmpty σ],
  (MvPolynomial.isEmptyRingEquiv R σ).symm.toRingHom = MvPolynomial.C
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Partial numerator  -/
GenContFract.Pair.a : {α : Type u_1} → GenContFract.Pair α → α
-- Mathlib.NumberTheory.Padics.RingHoms
/-- `appr n x` gives a value `v : ℕ` such that `x` and `↑v : ℤ_p` are congruent mod `p^n`.
See `appr_spec`.  -/
PadicInt.appr : {p : ℕ} → [hp_prime : Fact (Nat.Prime p)] → ℤ_[p] → ℕ → ℕ
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.biInter_mem : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α} {f : Set α → Set β},
  l.HasBasis p s → Monotone f → ⋂ t ∈ l, f t = ⋂ i, ⋂ (_ : p i), f (s i)
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_add_le : ∀ {p q : ℚ}, (q + p).toNNRat ≤ q.toNNRat + p.toNNRat
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.nsmul` -/
Function.HasFiniteSupport.fun_nsmul : ∀ {α : Type u_1} {M : Type u_3} [inst : AddMonoid M] {f : α → M},
  Function.HasFiniteSupport f → ∀ (n : ℕ), Function.HasFiniteSupport fun i => n • f i
-- Mathlib.RingTheory.DedekindDomain.Instances
instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1 : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [IsDomain S]
  [inst_4 : Algebra R S] {P : Ideal R} [inst_5 : P.IsPrime] [FaithfulSMul R S],
  Module.IsTorsionFree R (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))
-- Lean.Compiler.InitAttr
Lean.isIOUnitRegularInitFn : Lean.Environment → Lean.Name → Bool
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instInhabitedCont' : Inhabited Turing.PartrecToTM2.Cont'
-- Init.Tactics
/-- If the main goal's target type is an inductive type, `constructor` solves it with
the first matching constructor, or else fails.
 -/
Lean.Parser.Tactic.constructor : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyGT_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, compare a k = Ordering.gt},
  Std.DTreeMap.Internal.Impl.getKeyGT k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.getKeyGT k t₂ ⋯ ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
neg_abs_le_neg : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LinearOrder α] [AddLeftMono α] (a : α), -|a| ≤ -a
-- Mathlib.CategoryTheory.Comma.Basic
/-- A natural isomorphism `R₁ ≅ R₂` induces an equivalence of categories
`Comma L R₁ ≌ Comma L R₂`.  -/
CategoryTheory.Comma.mapRightIso : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              {R₁ R₂ : CategoryTheory.Functor B T} → (R₁ ≅ R₂) → (CategoryTheory.Comma L R₁ ≌ CategoryTheory.Comma L R₂)
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parent_root : ∀ (self : Batteries.UnionFind) (x : Fin self.size), self.arr[↑(self.root x)].parent = ↑(self.root x)
-- Mathlib.Data.TwoPointing
TwoPointing.sum_snd : ∀ {α : Type u_1} {β : Type u_2} (p : TwoPointing α) (q : TwoPointing β), (p.sum q).toProd.2 = Sum.inr q.toProd.2
-- Mathlib.Data.Num.ZNum
ZNum.isOrderedAddMonoid : IsOrderedAddMonoid ZNum
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiffOn.smul`

---

The scalar multiplication of two `C^n` functions on a domain is `C^n`.  -/
ContDiffOn.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {𝕜' : Type u_3} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {s : Set E} {f : E → 𝕜'} {g : E → F},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (fun i => f i • g i) s
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]` (also called Jacobi identity).  -/
VectorField.leibniz_identity_mlieBracket : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (minSmoothness 𝕜 3) M]
  [CompleteSpace E] {U V W : (x : M) → TangentSpace I x},
  (ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x => ⟨x, U x⟩) →
    (ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x => ⟨x, V x⟩) →
      (ContMDiff I I.tangent (minSmoothness 𝕜 2) fun x => ⟨x, W x⟩) →
        VectorField.mlieBracket I U (VectorField.mlieBracket I V W) =
          VectorField.mlieBracket I (VectorField.mlieBracket I U V) W +
            VectorField.mlieBracket I V (VectorField.mlieBracket I U W)
-- Mathlib.Control.Functor.Multivariate
TypeVec.PredLast.eq_2 : ∀ {n : ℕ} (α : TypeVec.{u_1} n) {β : Type u_1} (p : β → Prop),
  α.PredLast p =
    match (motive := (x : Fin2 (n + 1)) → (α ::: β) x → Prop) Fin2.fz with
    | a.fs => fun x => True
    | Fin2.fz => p
-- Mathlib.FieldTheory.Galois.Basic
/-- The fixing subgroup of `K : IntermediateField F E` is isomorphic to `Gal(E/K)`.  -/
IntermediateField.fixingSubgroupEquiv : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → (K : IntermediateField F E) → ↥K.fixingSubgroup ≃* Gal(E/↥K)
-- Mathlib.Topology.Separation.Hausdorff
SeparatedNhds.of_finset_finset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] (s t : Finset X), Disjoint s t → SeparatedNhds ↑s ↑t
-- Init.System.IO
IO.FS.instReprSystemTime : Repr IO.FS.SystemTime
-- Init.Data.Vector.Lemmas
Vector.forIn'_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] {xs : Array α} (h : xs.size = n)
  {b : β} {f : (a : α) → a ∈ Vector.mk xs h → β → m (ForInStep β)},
  forIn' (Vector.mk xs h) b f = forIn' xs b fun a m b => f a ⋯ b
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.restoreM_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε α : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m (Except ε α)),
  ⦃(Std.Do.wp x).apply (fun e => Except.casesOn e Q.2.1 Q.1, Q.2.2)⦄ MonadControl.restoreM x ⦃Q⦄
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule.surj : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f], Function.Surjective ⇑(IsLocalizedModule.fromLocalizedModule S f)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.forget_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  (X : CategoryTheory.Grothendieck F), (CategoryTheory.Grothendieck.forget F).obj X = X.base
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- `AddActionHom` maps `fixedBy` to `fixedBy`.  -/
AddActionHom.map_mem_fixedBy : ∀ {G : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddMonoid G] [inst_1 : AddAction G A] [inst_2 : AddAction G B]
  (f : A →ₑ[id] B) {g : G} {a : A}, a ∈ AddAction.fixedBy A g → f a ∈ AddAction.fixedBy B g
-- Mathlib.Data.Nat.ModEq
AddCommGroup.natCast_modEq_natCast : ∀ {M : Type u_1} [inst : AddCommMonoidWithOne M] [CharZero M] {a b n : ℕ}, ↑a ≡ ↑b [PMOD ↑n] ↔ a ≡ b [MOD n]
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.findMin'.match_1.eq_2 : ∀ {α : Type u_1} (motive : Ordnode α → α → Sort u_2) (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) (x_1 : α)
  (h_1 : (x : α) → motive Ordnode.nil x)
  (h_2 : (size : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → (x_2 : α) → motive (Ordnode.node size l x r) x_2),
  (match Ordnode.node size l x r, x_1 with
    | Ordnode.nil, x => h_1 x
    | Ordnode.node size l x r, x_2 => h_2 size l x r x_2) =
    h_2 size l x r x_1
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.moduleCategory : (R : Type u) → [inst : Ring R] → CategoryTheory.Category.{v, max (v + 1) u} (ModuleCat R)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.inclusion.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M α] (s : SubAddAction M α),
  s.inclusion = { toFun := Subtype.val, map_vadd' := ⋯ }
-- Mathlib.Data.Set.Card
Set.ncard_le_one_iff : ∀ {α : Type u_1} {s : Set α},
  autoParam s.Finite Set.ncard_le_one_iff._auto_1 → (s.ncard ≤ 1 ↔ ∀ {a b : α}, a ∈ s → b ∈ s → a = b)
-- Aesop.Search.Expansion.Norm
Aesop.optNormRuleResultEmoji : Option Aesop.NormRuleResult → String
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.right_unitor_inv_hom : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b : B} (f : CategoryTheory.FreeBicategory.Hom a b), CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.SetTheory.ZFC.PSet
/-- The type of pre-sets in universe `u`. A pre-set
is a family of pre-sets indexed by a type in `Type u`.
The ZFC universe is defined as a quotient of this
to ensure extensionality.  -/
PSet : Type (u + 1)
-- Mathlib.Algebra.Lie.TraceForm
LieSubmodule.trace_eq_trace_restrict_of_le_idealizer : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [Module.Free R M] [Module.Finite R M] [IsDomain R] [IsPrincipalIdealRing R] (N : LieSubmodule R L M)
  (I : LieIdeal R L) (h : I ≤ N.idealizer) (x : L) {y : L} (hy : y ∈ I)
  (hy' : optParam (∀ m ∈ N, ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) m ∈ N) ⋯),
  (LinearMap.trace R M) ((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y) =
    (LinearMap.trace R ↥N) (((LieModule.toEnd R L M) x ∘ₗ (LieModule.toEnd R L M) y).restrict hy')
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceₘ.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3)
  (r : Std.DTreeMap.Internal.Impl α β) (h : r.size > Std.DTreeMap.Internal.delta * l.size)
  (h_1 :
    (h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
      motive Std.DTreeMap.Internal.Impl.leaf h)
  (h_2 :
    (size : ℕ) →
      (rk : α) →
        (rv : β rk) →
          (rl rr : Std.DTreeMap.Internal.Impl α β) →
            (h : (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size > Std.DTreeMap.Internal.delta * l.size) →
              motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h)
  (h_3 : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size),
  r = Std.DTreeMap.Internal.Impl.leaf →
    h ≍ h_3 →
      (match r, h with
        | Std.DTreeMap.Internal.Impl.leaf, h => h_1 h
        | Std.DTreeMap.Internal.Impl.inner size rk rv rl rr, h => h_2 size rk rv rl rr h) ≍
        h_1 h_3
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.nnnorm_deriv_mulExpNegMulSq_le_one : ∀ {ε : ℝ}, 0 < ε → ∀ (x : ℝ), ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1
-- Init.Prelude
/-- A functor in the sense used in functional programming, which means a function `f : Type u → Type v`
has a way of mapping a function over its contents. This `map` operator is written `<$>`, and
overloaded via `Functor` instances.

This `map` function should respect identity and function composition. In other words, for all terms
`v : f α`, it should be the case that:

 * `id <$> v = v`

 * For all functions `h : β → γ` and `g : α → β`, `(h ∘ g) <$> v = h <$> g <$> v`

While all `Functor` instances should live up to these requirements, they are not required to _prove_
that they do. Proofs may be required or provided via the `LawfulFunctor` class.

Assuming that instances are lawful, this definition corresponds to the category-theoretic notion of
[functor](https://en.wikipedia.org/wiki/Functor) in the special case where the category is the
category of types and functions between them.
 -/
Functor : (Type u → Type v) → Type (max (u + 1) v)
-- Init.Data.UInt.Basic
/-- Bitwise or for 16-bit unsigned integers. Usually accessed via the `|||` operator.

Each bit of the resulting integer is set if at least one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.lor : UInt16 → UInt16 → UInt16
-- Mathlib.Combinatorics.Quiver.Basic
/-- `Vᵒᵖ` reverses the direction of all arrows of `V`.  -/
Quiver.opposite : {V : Type u_1} → [Quiver V] → Quiver Vᵒᵖ
-- Init.Data.Array.Lemmas
Array.back?_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α}, (Array.map f xs).back? = Option.map f xs.back?
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.add : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddZeroClass β] {f f' : α → β},
  HasCompactSupport f → HasCompactSupport f' → HasCompactSupport (f + f')
-- Mathlib.Order.Interval.Finset.Gaps
Finset.intervalGapsWithin_injOn : ∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α),
  Set.InjOn (fun j => ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (Set.Iio k)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instAddCommGroup : (p : ENNReal) → (V : Type u_4) → [AddCommGroup V] → AddCommGroup (WithLp p V)
-- Mathlib.Analysis.Distribution.TestFunction
/-- If `n₁ ≥ n₂` and `Ω₁ ⊆ Ω₂`, `monoCLM 𝕜` is the continuous `𝕜`-linear inclusion of
`𝓓^{n₁}(Ω₁, F)` inside `𝓓^{n₂}(Ω₂, F)`. Otherwise, this is the zero map.

This is in fact a topological embedding when `n₁ = n₂` and `Ω₁ ⊆ Ω₂` (not in Mathlib as of
March 2026).

The parameters `n₁, n₂, Ω₁, Ω₂` are implicit as they can often be inferred from context, or
specified by a type ascription.  -/
TestFunction.monoCLM : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω₁ Ω₂ : TopologicalSpace.Opens E} →
            {F : Type u_4} →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    {n₁ n₂ : ℕ∞} →
                      [inst_6 : Algebra ℝ 𝕜] →
                        [inst_7 : IsScalarTower ℝ 𝕜 F] → TestFunction Ω₁ F n₁ →L[𝕜] TestFunction Ω₂ F n₂
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Composition of Eilenberg–Moore coalgebra homomorphisms.  -/
CategoryTheory.Comonad.Coalgebra.Hom.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} → {P Q R : G.Coalgebra} → P.Hom Q → Q.Hom R → P.Hom R
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.t_id : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J] (i : J),
  AlgebraicGeometry.Scheme.IsLocallyDirected.t F i i =
    CategoryTheory.CategoryStruct.id ↑(AlgebraicGeometry.Scheme.IsLocallyDirected.V F i i)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
/-- The unit for the tensor `X ⊗ Y` in `Dial C`.  -/
CategoryTheory.Dial.tensorUnitImpl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasFiniteProducts C] → CategoryTheory.Dial C
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- `R / p` has a canonical map to `S / (P ^ e)`, where `e` is the ramification index
of `P` over `p`.  -/
Ideal.Quotient.algebraQuotientPowRamificationIdx : {R : Type u} →
  [inst : CommRing R] →
    {S : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] → (p : Ideal R) → (P : Ideal S) → Algebra (R ⧸ p) (S ⧸ P ^ p.ramificationIdx' P)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Product of a list of elements in a `Subsemiring` is in the `Subsemiring`.  -/
Subsemiring.list_prod_mem : ∀ {R : Type u_1} [inst : Semiring R] (s : Subsemiring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.prod ∈ s
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanImport.toJson : Lean.Lsp.LeanImport → Lean.Json
-- Mathlib.Order.Hom.Bounded
BotHom.coe_copy : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : Bot β] (f : BotHom α β) (f' : α → β) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Init.Data.Int.Linear
Int.Internal.Linear.le_neg_cert : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_union_null_iff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, μ (s ∪ t) = 0 ↔ μ s = 0 ∧ μ t = 0
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `r` is a positive constant, `x ↦ f x / r` tends to infinity along a filter
if and only if `f` tends to infinity along the same filter.  -/
Filter.tendsto_div_const_atTop_of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α}, 0 < r → (Filter.Tendsto (fun x => f x / r) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop)
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Taking a strict initial segment of a path removes the end vertex from the support.  -/
SimpleGraph.Walk.endpoint_notMem_support_takeUntil : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} [inst : DecidableEq V] {p : G.Walk u v},
  p.IsPath → ∀ (hw : w ∈ p.support), v ≠ w → v ∉ (p.takeUntil w hw).support
-- Mathlib.RingTheory.Ideal.Height
Ideal.FiniteHeight.mk : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R}, I = ⊤ ∨ I.height ≠ ⊤ → I.FiniteHeight
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_j : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] {A : Type v} [inst_2 : CommRing A]
  (f : R →+* A), (W.map f).j = f W.j
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
/-- Version of `HasSum.update` for `AddCommMonoid` rather than `AddCommGroup`.
Rather than showing that `f.update` has a specific sum in terms of `HasSum`,
it gives a relationship between the sums of `f` and `f.update` given that both exist.  -/
HasSum.update' : ∀ {β : Type u_2} {L : SummationFilter β} [L.LeAtTop] [L.NeBot] {α : Type u_4} [inst : TopologicalSpace α]
  [inst_1 : AddCommMonoid α] [T2Space α] [ContinuousAdd α] [inst_4 : DecidableEq β] {f : β → α} {a a' : α},
  HasSum f a L → ∀ (b : β) (x : α), HasSum (Function.update f b x) a' L → a + x = a' + f b
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk_eq_self : ∀ {R : Type u} [inst : CommSemiring R] {M : CommRing.Pic R}, CommRing.Pic.mk R M.AsModule = M
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The composition of left adjoint mates is the adjoint mate of the composition.  -/
CategoryTheory.comp_leftAdjointMate_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.HasLeftDual X] [inst_3 : CategoryTheory.HasLeftDual Y]
  [inst_4 : CategoryTheory.HasLeftDual Z] {f : X ⟶ Y} {g : Y ⟶ Z} {Z_1 : C} (h : ᘁX ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (ᘁCategoryTheory.CategoryStruct.comp f g) h =
    CategoryTheory.CategoryStruct.comp (ᘁg) (CategoryTheory.CategoryStruct.comp (ᘁf) h)
-- Mathlib.Order.Bounds.Image
StrictAnti.map_isLeast : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {a : α} {s : Set α},
  StrictAnti f → (IsLeast (f '' s) (f a) ↔ IsGreatest s a)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
_private.Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card.0.termQ : Lean.ParserDescr