mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.Code.eval.match_1.eq_2 : ∀ (motive : Turing.ToPartrec.Code → Sort u_1) (h_1 : Unit → motive Turing.ToPartrec.Code.zero')
  (h_2 : Unit → motive Turing.ToPartrec.Code.succ) (h_3 : Unit → motive Turing.ToPartrec.Code.tail)
  (h_4 : (f fs : Turing.ToPartrec.Code) → motive (f.cons fs)) (h_5 : (f g : Turing.ToPartrec.Code) → motive (f.comp g))
  (h_6 : (f g : Turing.ToPartrec.Code) → motive (f.case g)) (h_7 : (f : Turing.ToPartrec.Code) → motive f.fix),
  (match Turing.ToPartrec.Code.succ with
    | Turing.ToPartrec.Code.zero' => h_1 ()
    | Turing.ToPartrec.Code.succ => h_2 ()
    | Turing.ToPartrec.Code.tail => h_3 ()
    | f.cons fs => h_4 f fs
    | f.comp g => h_5 f g
    | f.case g => h_6 f g
    | f.fix => h_7 f) =
    h_2 ()
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_neg : ∀ {𝕜 : 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] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {V : (x : M') → TangentSpace I' x},
  VectorField.mpullbackWithin I I' f (-V) s = -VectorField.mpullbackWithin I I' f V s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.mixedEmbedding.fundamentalCone K =
    NumberField.mixedEmbedding.logMap ⁻¹'
        ZSpan.fundamentalDomain
          (Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K) (NumberField.Units.basisUnitLattice K)) \
      {x | NumberField.mixedEmbedding.norm x = 0}
-- Init.Data.String.Lemmas.Splits
/-- You might want to invoke `Slice.Pos.Splits.exists_eq_singleton_append` to be able to apply this.  -/
String.Slice.Pos.Splits.next : ∀ {t₁ : String} {c : Char} {t₂ : String} {s : String.Slice} {p : s.Pos} (h : p.Splits t₁ (String.singleton c ++ t₂)),
  (p.next ⋯).Splits (t₁ ++ String.singleton c) t₂
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- Show that `FirstObj` is isomorphic to `FamilyOfElements`.  -/
CategoryTheory.Equalizer.firstObjEqFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} →
        (R : CategoryTheory.Presieve X) →
          CategoryTheory.Equalizer.FirstObj P R ≅ CategoryTheory.Presieve.FamilyOfElements P R
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.precomp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ι → Type u_8} {mβ : (i : ι) → MeasurableSpace (β i)}
  {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α}
  {f : (x : ι) → Ω → β x} {ι' : Type u_9} {g : ι' → ι},
  Function.Injective g →
    ProbabilityTheory.Kernel.iIndepFun f κ μ → ProbabilityTheory.Kernel.iIndepFun (fun i => f (g i)) κ μ
-- Mathlib.LinearAlgebra.RootSystem.Base
/-- Given a base `α₁, α₂, …`, the height of a root `∑ zᵢαᵢ` relative to this base is `∑ zᵢ`.  -/
RootPairing.Base.height : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] → {P : RootPairing ι R M N} → P.Base → [CharZero R] → ι → ℤ
-- Mathlib.CategoryTheory.EpiMono
/-- Every split mono whose retraction is mono is an iso.  -/
CategoryTheory.IsIso.of_mono_retraction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) [hf : CategoryTheory.IsSplitMono f]
  [hf' : CategoryTheory.Mono (CategoryTheory.retraction f)], CategoryTheory.IsIso f
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_finsetSum_of_support_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Finset α},
  Function.support f ⊆ ↑s → ∑ᶠ (i : α), f i = ∑ i ∈ s, f i
-- Mathlib.SetTheory.ZFC.PSet
PSet.func_mem : ∀ (x : PSet.{u_1}) (i : x.Type), x.Func i ∈ x
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPolyC.go.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Var)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (match Lean.Grind.CommRing.Expr.var x with
    | Lean.Grind.CommRing.Expr.num n => h_1 n
    | Lean.Grind.CommRing.Expr.var x => h_2 x
    | x => h_3 x) =
    h_2 x
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.openCell_zero_eq_singleton : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {j : Topology.RelCWComplex.cell C 0}, Topology.RelCWComplex.openCell 0 j = {↑(Topology.RelCWComplex.map 0 j) ![]}
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.zero_form_isBoundedAtImInfty : ∀ {α : Type u_1} [inst : NormedField α], UpperHalfPlane.IsBoundedAtImInfty 0
-- Std.Data.DHashMap.Basic
/-- Dependent hash maps.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pairs. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.

The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.

These hash maps contain a bundled well-formedness invariant, which means that they cannot
be used in nested inductive types. For these use cases, `Std.DHashMap.Raw` and
`Std.DHashMap.Raw.WF` unbundle the invariant from the hash map. When in doubt, prefer
`DHashMap` over `DHashMap.Raw`.

For a variant that is more convenient for use in proofs because of extensionalities, see
`Std.ExtDHashMap` which is defined in the module `Std.Data.ExtDHashMap`.
 -/
Std.DHashMap : (α : Type u) → (α → Type v) → [BEq α] → [Hashable α] → Type (max u v)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasStrictFDerivAt.const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸] {a : E → 𝔸}
  {a' : E →L[𝕜] 𝔸}, HasStrictFDerivAt a a' x → ∀ (b : 𝔸), HasStrictFDerivAt (fun y => b * a y) (b • a') x
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  {X Y : CategoryTheory.SimplicialObject A} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.AlternatingFaceMapComplex.map f)
      (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex Y) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X)
      (AlgebraicTopology.NormalizedMooreComplex.map f)
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonOpenNamespace : Lean.FromJson Lean.Lsp.OpenNamespace
-- Mathlib.Algebra.Order.Floor.Div
ceilDiv_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] (b : β), b ⌈/⌉ 0 = 0
-- Mathlib.Analysis.Analytic.Uniqueness
/-- If a function `f : 𝕜 → E` has power series representation `p` on a ball of some radius and for
each positive radius it has some power series representation, then `p` converges to `f` on the whole
`𝕜`.  -/
HasFPowerSeriesOnBall.r_eq_top_of_exists : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {r : ENNReal} {x : 𝕜} {p : FormalMultilinearSeries 𝕜 𝕜 E},
  HasFPowerSeriesOnBall f p x r →
    (∀ (r' : NNReal), 0 < r' → ∃ p', HasFPowerSeriesOnBall f p' x ↑r') → HasFPowerSeriesOnBall f p x ⊤
-- Lean.Elab.DefView
Lean.Elab.DefView.mk.sizeOf_spec : ∀ (kind : Lean.Elab.DefKind) (ref headerRef : Lean.Syntax) (modifiers : Lean.Elab.Modifiers)
  (declId binders : Lean.Syntax) (type? : Option Lean.Syntax) (value : Lean.Syntax)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment))
  (headerSnap? : Option (Lean.Language.SnapshotBundle (Option Lean.Elab.HeaderProcessedSnapshot)))
  (deriving? : Option (Array Lean.Syntax)),
  sizeOf
      { kind := kind, ref := ref, headerRef := headerRef, modifiers := modifiers, declId := declId, binders := binders,
        type? := type?, value := value, docString? := docString?, headerSnap? := headerSnap?, deriving? := deriving? } =
    1 + sizeOf kind + sizeOf ref + sizeOf headerRef + sizeOf modifiers + sizeOf declId + sizeOf binders + sizeOf type? +
            sizeOf value +
          sizeOf docString? +
        sizeOf headerSnap? +
      sizeOf deriving?
-- Batteries.Data.String.Legacy
/-- Returns the position of the last occurrence of a character, `c`, in a string `s`. If `s` does not
contain `c`, returns `none`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.

Examples:
* `"abcabc".revPosOf 'a' = some ⟨3⟩`
* `"abcabc".revPosOf 'z' = none`
* `"L∃∀N".revPosOf '∀' = some ⟨4⟩`
 -/
String.Legacy.revPosOf : String → Char → Option String.Pos.Raw
-- Mathlib.Logic.Equiv.Set
Equiv.image_compl : ∀ {α : Type u_3} {β : Type u_4} (f : α ≃ β) (s : Set α), ⇑f '' sᶜ = (⇑f '' s)ᶜ
-- Std.Http.Protocol.H1
/-- Validates an outgoing response head and selects body framing mode.

For status codes that must not carry a response body, framing headers are still
syntactically validated but the machine always uses `.fixed 0` framing.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.checkSendingMessageHead : Std.Http.Protocol.H1.Message.Head Std.Http.Protocol.H1.Direction.sending →
  Except Std.Http.Protocol.H1.Error Std.Http.Protocol.H1.Machine.BodyMode✝
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Legacy.revPosOfAux.eq_def : ∀ (s : String) (c : Char) (pos : String.Pos.Raw),
  String.Legacy.revPosOfAux s c pos =
    if h : pos = 0 then none
    else
      have this := ⋯;
      have pos := String.Pos.Raw.prev s pos;
      if (String.Pos.Raw.get s pos == c) = true then some pos else String.Legacy.revPosOfAux s c pos
-- Mathlib.Algebra.RingQuot
RingQuot.mkRingHom_rel : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} {x y : R},
  r x y → (RingQuot.mkRingHom r) x = (RingQuot.mkRingHom r) y
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommProd_empty : ∀ {α : Type u_3} [inst : Monoid α] (h : {x | x ∈ 0}.Pairwise Commute), Multiset.noncommProd 0 h = 1
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.TensorLE.prop_tensor : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {P₁ P₂ Q : CategoryTheory.ObjectProperty C} [self : P₁.TensorLE P₂ Q] (X₁ X₂ : C),
  P₁ X₁ → P₂ X₂ → Q (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
-- Mathlib.Topology.Order.Hom.Esakia
PseudoEpimorphism.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] (h : PseudoEpimorphism γ δ) (g : PseudoEpimorphism β γ)
  (f : PseudoEpimorphism α β), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.testAgainstNN_lipschitz : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [OpensMeasurableSpace Ω]
  (μ : MeasureTheory.FiniteMeasure Ω), LipschitzWith μ.mass fun f => μ.testAgainstNN f
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Given `u : α → γ` a uniform inducing map, a family `𝓕 : ι → β → α` is uniformly equicontinuous
on a subset `S : Set β` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`,
is uniformly equicontinuous on `S`.  -/
IsUniformInducing.uniformEquicontinuousOn_iff : ∀ {ι : Type u_1} {α : Type u_6} {β : Type u_8} {γ : Type u_10} [uα : UniformSpace α] [uβ : UniformSpace β]
  [uγ : UniformSpace γ] {F : ι → β → α} {S : Set β} {u : α → γ},
  IsUniformInducing u → (UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((fun x => u ∘ x) ∘ F) S)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.edist_iterate_succ_le_geometric : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {K : NNReal} {f : α → α},
  LipschitzWith K f → ∀ (x : α) (n : ℕ), edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * ↑K ^ n
-- Mathlib.Order.KrullDimension
/-- The height of the last element in a series is larger or equal to the length of the series.
 -/
Order.length_le_height_last : ∀ {α : Type u_1} [inst : Preorder α] {p : LTSeries α}, ↑p.length ≤ Order.height (RelSeries.last p)
-- Mathlib.Data.Sym.Basic
Sym.sound : ∀ {α : Type u_1} {n : ℕ} {a b : List.Vector α n}, (↑a).Perm ↑b → Sym.ofVector a = Sym.ofVector b
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.continuous : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), Continuous ⇑e
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- A version of the **Gelfand-Mazur Theorem**.

If `F` is a nontrivial normed `ℂ`-algebra with multiplicative norm, then we obtain a
`ℂ`-algebra equivalence with `ℂ`.  -/
NormedAlgebra.Complex.algEquivOfNormMul : (F : Type u_1) →
  [inst : NormedRing F] →
    [NormOneClass F] → [NormMulClass F] → [inst_3 : NormedAlgebra ℂ F] → [Nontrivial F] → ℂ ≃ₐ[ℂ] F
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y) Z ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y
              Z).inv
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).inv
          Z)
        h)
-- Mathlib.Algebra.Lie.UniversalEnveloping
UniversalEnvelopingAlgebra.lift_ι_apply' : ∀ (R : Type u₁) {L : Type u₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {A : Type u₃}
  [inst_3 : Ring A] [inst_4 : Algebra R A] (f : L →ₗ⁅R⁆ A) (x : L),
  ((UniversalEnvelopingAlgebra.lift R) f) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = f x
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.mapQ.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ Submodule.comap f q), p.mapQ q f h = p.liftQ (q.mkQ ∘ₛₗ f) ⋯
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.ext_iff : ∀ {x y : BoxIntegral.IntegrationParams},
  x = y ↔ x.bRiemann = y.bRiemann ∧ x.bHenstock = y.bHenstock ∧ x.bDistortion = y.bDistortion
-- Mathlib.Data.Multiset.Bind
Multiset.join.eq_1 : ∀ {α : Type u_1}, Multiset.join = Multiset.sum
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.LocallyRingedSpace.GlueData.f_open : ∀ (self : AlgebraicGeometry.LocallyRingedSpace.GlueData) (i j : self.J),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion (self.f i j)
-- Mathlib.Analysis.Distribution.Distribution
Distribution.mapCLM_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_2}
  [inst_2 : AddCommGroup F] [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace F] {F' : Type u_3}
  [inst_5 : AddCommGroup F'] [inst_6 : Module ℝ F'] [inst_7 : TopologicalSpace F'] {n : ℕ∞}
  [inst_8 : IsTopologicalAddGroup F] [inst_9 : ContinuousSMul ℝ F] [inst_10 : IsTopologicalAddGroup F']
  [inst_11 : ContinuousSMul ℝ F'] {A : F →L[ℝ] F'} {T : Distribution Ω F n} {f : TestFunction Ω ℝ n},
  ((Distribution.mapCLM A) T) f = A (T f)
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.le_def : ∀ {X : Type u_1} {d₁ d₂ : DiffeologicalSpace X}, d₁ ≤ d₂ ↔ d₁.toPlots ⊆ d₂.toPlots
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.PreservesLimit₂.of_preservesLimit₂_flip : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G], CategoryTheory.Limits.PreservesLimit₂ K₂ K₁ G.flip
-- Mathlib.Data.Rat.Lemmas
Rat.add_ofNat_den : ∀ (q : ℚ) (n : ℕ), (q + OfNat.ofNat n).den = q.den
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_mul`. -/
ContinuousLinearMap.coe_mul : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] (f g : M₁ →L[R₁] M₁), ↑(f * g) = ↑f * ↑g
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.hasStrictDerivAt_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R 𝕜]
  (q : Polynomial R) (x : 𝕜),
  HasStrictDerivAt (fun x => (Polynomial.aeval x) q) ((Polynomial.aeval x) (Polynomial.derivative q)) x
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.coe_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] {x : CompleteLattice β}, ⇑⊥ = ⊥
-- Init.NotationExtra
Lean.calcStep : Lean.ParserDescr
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
_private.Mathlib.Combinatorics.SetFamily.AhlswedeZhang.0.Finset.lower_aux : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s t : Finset α} {a : α} [inst_1 : DecidableEq α],
  a ∈ lowerClosure ↑(s ∪ t) ↔ a ∈ lowerClosure ↑s ∨ a ∈ lowerClosure ↑t
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.restrictScalarsLinear_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [inst_8 : ∀ (i : ι), ContinuousSMul 𝕜 (E i)] (𝕜' : Type u_5)
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : (i : ι) → Module 𝕜' (E i)]
  [inst_12 : ∀ (i : ι), IsScalarTower 𝕜' 𝕜 (E i)] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F]
  [inst_15 : ContinuousConstSMul 𝕜' F],
  ⇑(ContinuousMultilinearMap.restrictScalarsLinear 𝕜') = ContinuousMultilinearMap.restrictScalars 𝕜'
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.norm_fourier_toL2_eq : ∀ {V : Type u_3} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : FiniteDimensional ℝ V]
  [inst_3 : MeasurableSpace V] [inst_4 : BorelSpace V] {H : Type u_4} [inst_5 : NormedAddCommGroup H]
  [inst_6 : InnerProductSpace ℂ H] [CompleteSpace H] (f : SchwartzMap V H),
  ‖(FourierTransform.fourier f).toLp 2 MeasureTheory.volume‖ = ‖f.toLp 2 MeasureTheory.volume‖
-- Mathlib.Algebra.GradedMonoid
/-- A dependent product for graded monoids represented by the indexed family of types `A i`.
This is a dependent version of `(l.map fA).prod`.

For a list `l : List α`, this computes the product of `fA a` over `a`, where each `fA` is of type
`A (fι a)`.  -/
List.dProd : {ι : Type u_1} →
  {α : Type u_2} →
    {A : ι → Type u_3} →
      [inst : AddMonoid ι] →
        [GradedMonoid.GMonoid A] → (l : List α) → (fι : α → ι) → ((a : α) → A (fι a)) → A (l.dProdIndex fι)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α}
  {h' : k ∈ Std.DHashMap.filterMap f m}, (Std.DHashMap.filterMap f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Topology.Homotopy.Contractible
ContinuousMap.HomotopyEquiv.contractibleSpace_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : ContinuousMap.HomotopyEquiv X Y), ContractibleSpace X ↔ ContractibleSpace Y
-- Mathlib.Analysis.LocallyConvex.PointwiseConvergence
/-- The family of seminorms that induce the topology of pointwise convergence, namely `‖A x‖` for
all `x : E`.  -/
PointwiseConvergenceCLM.seminorm : {𝕜₁ : Type u_3} →
  {𝕜₂ : Type u_4} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_7} →
            {F : Type u_8} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : NormedAddCommGroup F] → [inst_6 : NormedSpace 𝕜₂ F] → E → Seminorm 𝕜₂ (E →SLₚₜ[σ] F)
-- Mathlib.Topology.JacobsonSpace
closedPoints_eq_univ : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X], closedPoints X = Set.univ
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtTarget.coprodMap : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtTarget P]
  {X Y X' Y' : AlgebraicGeometry.Scheme} (f : X ⟶ X') (g : Y ⟶ Y'), P f → P g → P (CategoryTheory.Limits.coprod.map f g)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNat.sizeOf_spec : ∀ (inst lit proof : Lean.Expr),
  sizeOf (Mathlib.Meta.NormNum.Result'.isNat inst lit proof) = 1 + sizeOf inst + sizeOf lit + sizeOf proof
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulMon_nc : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ) (m : Lean.Grind.CommRing.Mon)
  (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulMon_nc k m p) =
    ↑k * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denote ctx p