mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Strict
Set.OrdConnected.strictConvex : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace β]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [OrderTopology β]
  [inst_7 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] {s : Set β}, s.OrdConnected → StrictConvex 𝕜 s
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.mrange_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.mrange (AddMonoid.Coprod.swap M N) = ⊤
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.toSubmonoid_le : ∀ {G : Type u_1} [inst : Group G] {p q : Subgroup G}, p.toSubmonoid ≤ q.toSubmonoid ↔ p ≤ q
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.exists_accPt_of_nullSingletonClass : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X}
  [MeasureTheory.NullSingletonClass μ] {E : Set X} [TopologicalSpace.SeparableSpace ↑E],
  0 < μ E → ∃ x, AccPt x (Filter.principal E)
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.mul_def : ∀ {α : Type u_2} [inst : NonUnitalNonAssocSemiring α] (f g : α →ₙ+* α), f * g = f.comp g
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterM.match_1.splitter : {β : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → n (ULift.{u_1, 0} Bool)} →
      [inst : MonadAttach n] →
        (out : β) →
          (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) →
            (__do_lift : Subtype (MonadAttach.CanReturn (f out))) →
              ((hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩) →
                ((hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩) →
                  motive __do_lift
-- Mathlib.Tactic.Recall
/-- The `recall` command redeclares a previous definition for illustrative purposes.
This can be useful for files that give an expository account of some theory in Lean.

The syntax of the command mirrors `def`, so all the usual bells and whistles work.
```
recall List.cons_append (a : α) (as bs : List α) : (a :: as) ++ bs = a :: (as ++ bs) := rfl
```
Also, one can leave out the body.
```
recall Nat.add_comm (n m : Nat) : n + m = m + n
```

The command verifies that the new definition type-checks and that the type and value
provided are definitionally equal to the original declaration. However, this does not
capture some details (like binders), so the following works without error.
```
recall Nat.add_comm {n m : Nat} : n + m = m + n
```

Docstrings are permitted but are ignored:
```
/-- The additive commutativity of natural numbers. -/
recall Nat.add_comm (n m : Nat) : n + m = m + n
```
 -/
Mathlib.Tactic.Recall.recall : Lean.ParserDescr
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- The derivative within a set of a monotone function is nonnegative.  -/
MonotoneOn.derivWithin_nonneg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {g : 𝕜 → 𝕜}, MonotoneOn g s → 0 ≤ derivWithin g s x
-- Mathlib.Algebra.GradedMulAction
/-- One is the neutral element for `•`  -/
GradedMonoid.GMulAction.one_smul : ∀ {ιA : Type u_1} {ιM : Type u_3} {A : ιA → Type u_4} {M : ιM → Type u_5} {inst : AddMonoid ιA} {inst_1 : VAdd ιA ιM}
  {inst_2 : GradedMonoid.GMonoid A} [self : GradedMonoid.GMulAction A M] (b : GradedMonoid M), 1 • b = b
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso_inv : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor D (CategoryTheory.Functor C D)) (Y : C)
  (e : F.flip.obj Y ≅ CategoryTheory.Functor.id D) (X : CategoryTheory.GradedObject J D) (a : J × I) (ha : a.2 = 0),
  (CategoryTheory.GradedObject.mapBifunctorObjObjSingle₀Iso F Y e X a ha).inv =
    CategoryTheory.CategoryStruct.comp (e.inv.app (X a.1))
      ((F.obj (X a.1)).map (CategoryTheory.GradedObject.singleObjApplyIsoOfEq 0 Y a.2 ha).inv)
-- Mathlib.Algebra.Polynomial.Eval.Subring
Polynomial.mem_map_rangeS : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) {p : Polynomial S},
  p ∈ (Polynomial.mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS
-- Mathlib.Algebra.Lie.Submodule
/-- Given two nested Lie submodules `N ⊆ N'`,
the inclusion `N ↪ N'` is a morphism of Lie modules.  -/
LieSubmodule.inclusion : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → {N N' : LieSubmodule R L M} → N ≤ N' → ↥N →ₗ⁅R,L⁆ ↥N'
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The `a`-torsion submodule for `a` in `R`, containing all elements `x` of `M` such that
`a • x = 0`.  -/
Submodule.torsionBy : (R : Type u_1) →
  (M : Type u_2) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → R → Submodule R M
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k a : α} {v : β},
  Std.ExtDHashMap.Const.get! (m.insert k v) a = if (k == a) = true then v else Std.ExtDHashMap.Const.get! m a
-- Mathlib.Analysis.Complex.RealDeriv
HasStrictDerivAt.complexToReal_fderiv : ∀ {f : ℂ → ℂ} {f' x : ℂ}, HasStrictDerivAt f f' x → HasStrictFDerivAt f (f' • 1) x
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.isLongestMatchAt_iff_splits : ∀ {pat s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat pos₁ pos₂ ↔
    ∃ t₁ t₂, pos₁.Splits t₁ (pat.copy ++ t₂) ∧ pos₂.Splits (t₁ ++ pat.copy) t₂
-- Lean.Util.Diff
Lean.Diff.Histogram.Entry.mk.sizeOf_spec : ∀ {α : Type u} {lsize rsize : ℕ} [inst : SizeOf α] (leftCount : ℕ) (leftIndex : Option (Fin lsize))
  (leftWF : leftCount = 0 ↔ leftIndex = none) (rightCount : ℕ) (rightIndex : Option (Fin rsize))
  (rightWF : rightCount = 0 ↔ rightIndex = none),
  sizeOf
      { leftCount := leftCount, leftIndex := leftIndex, leftWF := leftWF, rightCount := rightCount,
        rightIndex := rightIndex, rightWF := rightWF } =
    1 + sizeOf leftCount + sizeOf leftIndex + sizeOf leftWF + sizeOf rightCount + sizeOf rightIndex + sizeOf rightWF
-- Mathlib.Data.Prod.Lex
Prod.Lex.instDenselyOrderedLexOfNoMinOrder : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [NoMinOrder β] [DenselyOrdered β],
  DenselyOrdered (Lex (α × β))
-- Mathlib.Topology.ClusterPt
isClosed_iff_clusterPt : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s ↔ ∀ (a : X), ClusterPt a (Filter.principal s) → a ∈ s
-- Aesop.Script.SpecificTactics
Aesop.introsS : Lean.MVarId → Aesop.ScriptM (Lean.MVarId × Array Lean.FVarId)
-- Mathlib.Order.CompleteBooleanAlgebra
PUnit.instCompleteAtomicBooleanAlgebra : CompleteAtomicBooleanAlgebra PUnit.{u_1 + 1}
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.comp_compProd_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ : MeasureTheory.Measure α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel (α × β) γ} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel η],
  (μ.compProd κ).bind ⇑η = (μ.bind ⇑(κ.compProd η)).snd
-- Mathlib.Data.Set.Basic
Set.ofPred_inter_eq_sep : ∀ {α : Type u} (p : α → Prop) (s : Set α), {a | p a} ∩ s = {a | a ∈ s ∧ p a}
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.Overlaps.insert : Lean.Meta.Match.Overlaps → ℕ → ℕ → Lean.Meta.Match.Overlaps
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.insert.match_3.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.map_mk : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S)
  (x : Polynomial (Polynomial R)),
  (WeierstrassCurve.Affine.CoordinateRing.map W' f) ((WeierstrassCurve.Affine.CoordinateRing.mk W') x) =
    (WeierstrassCurve.Affine.CoordinateRing.mk (W'.map f)) (Polynomial.map (Polynomial.mapRingHom f) x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trNormal.eq_def : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ) (x : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.trNormal dec x =
    match x with
    | Turing.TM1.Stmt.move d q => Turing.TM1to1.move n d (Turing.TM1to1.trNormal dec q)
    | Turing.TM1.Stmt.write f q =>
      Turing.TM1to1.read dec fun a => Turing.TM1.Stmt.goto fun x s => Turing.TM1to1.Λ'.write (f a s) q
    | Turing.TM1.Stmt.load f q =>
      Turing.TM1to1.read dec fun a => Turing.TM1.Stmt.load (fun x s => f a s) (Turing.TM1to1.trNormal dec q)
    | Turing.TM1.Stmt.branch p q₁ q₂ =>
      Turing.TM1to1.read dec fun a =>
        Turing.TM1.Stmt.branch (fun x s => p a s) (Turing.TM1to1.trNormal dec q₁) (Turing.TM1to1.trNormal dec q₂)
    | Turing.TM1.Stmt.goto l =>
      Turing.TM1to1.read dec fun a => Turing.TM1.Stmt.goto fun x s => Turing.TM1to1.Λ'.normal (l a s)
    | Turing.TM1.Stmt.halt => Turing.TM1.Stmt.halt
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- Auxiliary construction for `Orientation.rightAngleRotation`, rotation by 90 degrees in an
oriented real inner product space of dimension 2.  -/
Orientation.rightAngleRotationAux₁ : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → [Fact (Module.finrank ℝ E = 2)] → Orientation ℝ E (Fin 2) → E →ₗ[ℝ] E
-- Init.Guard
/-- Tactic to check equality of two expressions.
* `guard_expr e = e'` checks that `e` and `e'` are defeq at reducible transparency.
* `guard_expr e =~ e'` checks that `e` and `e'` are defeq at default transparency.
* `guard_expr e =ₛ e'` checks that `e` and `e'` are syntactically equal.
* `guard_expr e =ₐ e'` checks that `e` and `e'` are alpha-equivalent.

Both `e` and `e'` are elaborated then have their metavariables instantiated before the equality
check. Their types are unified (using `isDefEqGuarded`) before synthetic metavariables are
processed, which helps with default instance handling.
 -/
Lean.Parser.Tactic.guardExprConv : Lean.ParserDescr
-- Lean.DocString.Add
/-- Adds a Verso docstring to the environment.

`binders` should be the syntax of the parameters to the constant that is being documented, as a null
node that contains a sequence of bracketed binders. It is used to allow interactive features such as
document highlights and “find references” to work for documented parameters. If no parameter binders
are available, pass `Syntax.missing` or an empty null node.
 -/
Lean.addVersoDocString : Lean.Name → Lean.Syntax → Lean.TSyntax `Lean.Parser.Command.docComment → Lean.Elab.TermElabM Unit
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.instInhabitedKey : Inhabited Lean.Meta.RefinedDiscrTree.Key
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- Composition of affine isometries.  -/
AffineIsometry.comp : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {V₃ : Type u_6} →
        {P : Type u_10} →
          {P₂ : Type u_11} →
            {P₃ : Type u_12} →
              [inst : NormedField 𝕜] →
                [inst_1 : SeminormedAddCommGroup V] →
                  [inst_2 : NormedSpace 𝕜 V] →
                    [inst_3 : PseudoMetricSpace P] →
                      [inst_4 : NormedAddTorsor V P] →
                        [inst_5 : SeminormedAddCommGroup V₂] →
                          [inst_6 : NormedSpace 𝕜 V₂] →
                            [inst_7 : PseudoMetricSpace P₂] →
                              [inst_8 : NormedAddTorsor V₂ P₂] →
                                [inst_9 : SeminormedAddCommGroup V₃] →
                                  [inst_10 : NormedSpace 𝕜 V₃] →
                                    [inst_11 : PseudoMetricSpace P₃] →
                                      [inst_12 : NormedAddTorsor V₃ P₃] → (P₂ →ᵃⁱ[𝕜] P₃) → (P →ᵃⁱ[𝕜] P₂) → P →ᵃⁱ[𝕜] P₃
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.specOverSpec : {R A : CommRingCat} → [Algebra ↑R ↑A] → (AlgebraicGeometry.Spec A).Over (AlgebraicGeometry.Spec R)
-- Mathlib.Topology.Bases
TopologicalSpace.instSecondCountableTopologyProd : ∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [inst : TopologicalSpace β] [SecondCountableTopology α]
  [SecondCountableTopology β], SecondCountableTopology (α × β)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.isProbabilityMeasure_map_up : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map ULift.up μ)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Given `IsRegularEpi f`, a choice of data for `RegularEpi f`.  -/
CategoryTheory.IsRegularEpi.getStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (f : X ⟶ Y) → [h : CategoryTheory.IsRegularEpi f] → CategoryTheory.RegularEpi f
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.Quot.desc_toCocone_desc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  (c : CategoryTheory.Limits.Cocone F) [inst_1 : DecidableEq J] {A : Type w} [inst_2 : AddCommGroup A]
  (f : AddCommGrpCat.Colimits.Quot F →+ A) (hc : CategoryTheory.Limits.IsColimit c),
  (AddCommGrpCat.Hom.hom (hc.desc (AddCommGrpCat.Colimits.toCocone F f))).comp (AddCommGrpCat.Colimits.Quot.desc F c) =
    f
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_eq_bot : ∀ {R : Type u_2} [inst : NonAssocRing R] {S : Subring R}, S.op = ⊥ ↔ S = ⊥
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.inv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, MeromorphicAt f x → MeromorphicAt f⁻¹ x
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
/-- The (exact) sequence `S.X₁.homology i ⟶ S.X₂.homology i ⟶ S.X₃.homology i`  -/
HomologicalComplex.HomologySequence.composableArrows₂ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          CategoryTheory.ShortComplex (HomologicalComplex C c) → ι → CategoryTheory.ComposableArrows C 2
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getGE!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.Equiv t₂ → t₁.getGE! k = t₂.getGE! k
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- Cancellation of a telescoping product.  -/
List.prod_range_div' : ∀ {G : Type u_7} [inst : Group G] (n : ℕ) (f : ℕ → G),
  (List.map (fun k => f k / f (k + 1)) (List.range n)).prod = f 0 / f n
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.equivalence_join_red : ∀ {α : Type u}, Equivalence (Relation.Join FreeGroup.Red)
-- Init.Data.UInt.Lemmas
USize.toBitVec_toUInt32 : ∀ (n : USize), n.toUInt32.toBitVec = BitVec.setWidth 32 n.toBitVec
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.of_constant_on_connected_clopens : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [LocallyConnectedSpace X] {f : X → Y},
  (∀ (U : Set X), IsConnected U → IsClopen U → ∀ x ∈ U, ∀ y ∈ U, f y = f x) → IsLocallyConstant f
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_inv_Ici : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : PartialOrder G] [inst_3 : CommGroup G] [IsOrderedMonoid G] [MeasurableInv G] [μ.IsInvInvariant] {c : G}
  {f : G → F}, MeasureTheory.IntegrableOn f (Set.Iic c⁻¹) μ → MeasureTheory.IntegrableOn (fun x => f x⁻¹) (Set.Ici c) μ
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- The embedding of a magma into its magma algebra.  -/
MonoidAlgebra.ofMagma : (R : Type u_8) → (M : Type u_9) → [inst : Semiring R] → [inst_1 : Mul M] → M →ₙ* MonoidAlgebra R M
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.eq_zero_of_mem_range_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] {y : β},
  y ∈ MeasureTheory.SimpleFunc.range 0 → y = 0
-- Lean.Meta.Sym.Arith.Types
/-- Classification state for a type with a `Semiring` instance.  -/
Lean.Meta.Sym.Arith.Semiring : Type
-- Lean.Server.Utils
/-- Extracts an `InputContext` from `doc`.  -/
Lean.Server.DocumentMeta.mkInputContext : Lean.Server.DocumentMeta → Lean.Parser.InputContext
-- Mathlib.Analysis.Distribution.TemperedDistribution
SchwartzMap.toTemperedDistributionCLM.eq_1 : ∀ (E : Type u_3) (F : Type u_4) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : SecondCountableTopology E]
  (μ : MeasureTheory.Measure E) [hμ : μ.HasTemperateGrowth],
  SchwartzMap.toTemperedDistributionCLM E F μ =
    {
      toFun := fun f =>
        (ContinuousLinearMap.toPointwiseConvergenceCLM ℂ (RingHom.id ℂ) (SchwartzMap E ℂ) F)
          (SchwartzMap.integralCLM ℂ μ ∘SL (SchwartzMap.pairing (ContinuousLinearMap.lsmul ℂ ℂ).flip) f),
      map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }
-- Mathlib.Order.SetNotation
infSet_to_nonempty : ∀ (α : Type u_1) [InfSet α], Nonempty α
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- Synonym of `Matrix.IsElliptic`, for dot-notation.  -/
Matrix.GeneralLinearGroup.IsElliptic : {R : Type u_1} → [inst : CommRing R] → [Preorder R] → GL (Fin 2) R → Prop
-- Lean.Server.FileWorker.SignatureHelp
Lean.Server.FileWorker.SignatureHelp.Candidate.mk.inj : ∀ {kind : Lean.Server.FileWorker.SignatureHelp.CandidateKind} {appStx : Lean.Syntax}
  {kind_1 : Lean.Server.FileWorker.SignatureHelp.CandidateKind} {appStx_1 : Lean.Syntax},
  { kind := kind, appStx := appStx } = { kind := kind_1, appStx := appStx_1 } → kind = kind_1 ∧ appStx = appStx_1
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_closure_iff : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {x : R},
  x ∈ Subring.closure s ↔ x ∈ AddSubgroup.closure ↑(Submonoid.closure s)
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedGroup.ofMulDist.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : Group E] [inst_2 : PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)),
  SeminormedGroup.ofMulDist h₁ h₂ = { toNorm := inst, toGroup := inst_1, toPseudoMetricSpace := inst_2, dist_eq := ⋯ }
-- Init.Data.Vector.Algebra
Vector.hmul_zero : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} [inst : Zero β] [inst_1 : Zero γ] [inst_2 : HMul α β γ],
  (∀ (c : α), c * 0 = 0) → ∀ (c : α), c * 0 = 0
-- Mathlib.Logic.Encodable.Basic
Encodable.choose_spec : ∀ {α : Type u_1} {p : α → Prop} [inst : Encodable α] [inst_1 : DecidablePred p] (h : ∃ x, p x), p (Encodable.choose h)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
Finset.invMulSubgroup_eq_mul_inv : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A : Finset G) (h : ↑(A * A).card < 3 / 2 * ↑A.card),
  ↑(A.invMulSubgroup h) = ↑A * ↑A⁻¹
-- Mathlib.Order.RelSeries
RelSeries.mem_def : ∀ {α : Type u_1} {r : SetRel α α} {s : RelSeries r} {x : α}, x ∈ s ↔ x ∈ Set.range s.toFun
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Colorable.of_hom : ∀ {V : Type u} {G : SimpleGraph V} {V' : Type u_4} {G' : SimpleGraph V'} {n : ℕ} (f : G →g G'),
  G'.Colorable n → G.Colorable n
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  [inst_1 : SizeOf C] (toPreOneHypercover : CategoryTheory.PreOneHypercover S) (mem₀ : toPreOneHypercover.sieve₀ ∈ J S)
  (mem₁ :
    ∀ (i₁ i₂ : toPreOneHypercover.I₀) ⦃W : C⦄ (p₁ : W ⟶ toPreOneHypercover.X i₁) (p₂ : W ⟶ toPreOneHypercover.X i₂),
      CategoryTheory.CategoryStruct.comp p₁ (toPreOneHypercover.f i₁) =
          CategoryTheory.CategoryStruct.comp p₂ (toPreOneHypercover.f i₂) →
        toPreOneHypercover.sieve₁ p₁ p₂ ∈ J W),
  sizeOf { toPreOneHypercover := toPreOneHypercover, mem₀ := mem₀, mem₁ := mem₁ } =
    1 + sizeOf toPreOneHypercover + sizeOf mem₀
-- Mathlib.Data.Finset.NAry
Finset.image₂_insert_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {a : α} [inst_1 : DecidableEq α],
  Finset.image₂ f (insert a s) t = Finset.image (fun b => f a b) t ∪ Finset.image₂ f s t
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
/-- A morphism of Lie-Rinehart algebras as a semilinear map.  -/
LieRinehartAlgebra.Hom.toLinearMap' : {R : Type u_1} →
  {A₁ : Type u_2} →
    {L₁ : Type u_3} →
      {A₂ : Type u_4} →
        {L₂ : Type u_5} →
          [inst : CommRing R] →
            [inst_1 : CommRing A₁] →
              [inst_2 : LieRing L₁] →
                [inst_3 : Module A₁ L₁] →
                  [inst_4 : LieRingModule L₁ A₁] →
                    [inst_5 : CommRing A₂] →
                      [inst_6 : LieRing L₂] →
                        [inst_7 : Module A₂ L₂] →
                          [inst_8 : LieRingModule L₂ A₂] →
                            [inst_9 : Algebra R A₁] →
                              [inst_10 : LieAlgebra R L₁] →
                                [inst_11 : Algebra R A₂] →
                                  [inst_12 : LieAlgebra R L₂] →
                                    {σ₁₂ : A₁ →ₐ[R] A₂} → LieRinehartAlgebra.Hom σ₁₂ L₁ L₂ → L₁ →ₛₗ[σ₁₂.toRingHom] L₂
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_zero : ∀ (a : ℤ), a.fdiv 0 = 0
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.forgetComp_inv_app : ∀ {W : Type v'} [inst : CategoryTheory.Category.{w', v'} W] [inst_1 : CategoryTheory.MonoidalCategory W] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory W C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory W D]
  {E : Type u₃} [inst_4 : CategoryTheory.EnrichedCategory W E] (F : CategoryTheory.EnrichedFunctor W C D)
  (G : CategoryTheory.EnrichedFunctor W D E) (X : CategoryTheory.ForgetEnrichment W C),
  (F.forgetComp G).inv.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.ForgetEnrichment.of W (G.obj (F.obj (CategoryTheory.ForgetEnrichment.to W X))))
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.le_nnnorm_of_mem : ∀ {A : Type u_3} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] [NormOneClass A] {a : A}
  {r : NNReal}, r ∈ spectrum NNReal a → r ≤ ‖a‖₊
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
groupCohomology.Hilbert90.aux.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] (f f_1 : Gal(L/K) → Lˣ),
  f = f_1 → ∀ (a a_1 : L), a = a_1 → groupCohomology.Hilbert90.aux f a = groupCohomology.Hilbert90.aux f_1 a_1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.isPrime_carrier : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] {f : A} (x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat),
  (AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x).IsPrime
-- Std.Sat.CNF.Basic
Std.Sat.CNF.eval_add : ∀ {α : Type u_1} {f : Std.Sat.CNF α} {c : Std.Sat.CNF.Clause α} (a : α → Bool),
  Std.Sat.CNF.eval a (Std.Sat.CNF.add c f) = (Std.Sat.CNF.Clause.eval a c && Std.Sat.CNF.eval a f)