mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m.erase k).get? k = none
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.link.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (szl : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' l'' : Std.DTreeMap.Internal.Impl α β) →
            (motive :
                Std.DTreeMap.Internal.Impl.Tree α β
                    ((Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
                  Sort u_3) →
              (x :
                  Std.DTreeMap.Internal.Impl.Tree α β
                    ((Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size)) →
                ((ℓ : Std.DTreeMap.Internal.Impl α β) →
                    (hℓ₁ : ℓ.Balanced) →
                      (hℓ₂ : ℓ.size = (Std.DTreeMap.Internal.Impl.inner szl k' v' l' r').size + 1 + l''.size) →
                        motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
                  motive x
-- Mathlib.Algebra.Order.Rearrangement
/-- **Strict inequality case of the Rearrangement Inequality**: Pointwise multiplication of
`f` and `g`, which antivary together, is strictly decreased by a permutation if and only if
`f` and `g ∘ σ` do not antivary together. Stated by permuting the entries of `g`.  -/
Antivary.sum_mul_lt_sum_mul_comp_perm_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  {σ : Equiv.Perm ι} {f g : ι → α} [inst_4 : Fintype ι],
  Antivary f g → (∑ i, f i • g i < ∑ i, f i • g (σ i) ↔ ¬Antivary f (g ∘ ⇑σ))
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  (i₁ i₂ i₃ : ι) {Z : ↑(F.obj { as := Opposite.op (sq₃ i₁ i₂ i₃).chosenPullback.pullback })}
  (h : (F.map (sq₃ i₁ i₂ i₃).p₂.op.toLoc).toFunctor.obj (obj' i₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) (sq₃ i₁ i₂ i₃).p₁₂ (sq₃ i₁ i₂ i₃).p₁
        (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯)
      h
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.msgToInteractive : Lean.MessageData → Bool → optParam ℕ 0 → IO Lean.Widget.InteractiveMessage
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.instDistribSMul : {M : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} → [inst : AddZeroClass A] → [inst_1 : AddCommMonoid B] → [DistribSMul M B] → DistribSMul M (A →+ B)
-- Lean.Meta.RecursorInfo
Lean.Meta.instToStringRecursorUnivLevelPos : ToString Lean.Meta.RecursorUnivLevelPos
-- Mathlib.Topology.Compactness.SigmaCompact
/-- If `X` is a `σ`-compact space, then a locally finite family of nonempty sets of `X` can have
only countably many elements, `Set.Countable` version.  -/
LocallyFinite.countable_univ : ∀ {X : Type u_1} {ι : Type u_3} [inst : TopologicalSpace X] [SigmaCompactSpace X] {f : ι → Set X},
  LocallyFinite f → (∀ (i : ι), (f i).Nonempty) → Set.univ.Countable
-- Lean.Data.Json.FromToJson.Basic
Lean.Prod.toJson : {α : Type u_1} → {β : Type u_2} → [Lean.ToJson α] → [Lean.ToJson β] → α × β → Lean.Json
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.Measure.QuasiMeasurePreserving.absolutelyContinuous : ∀ {α : Type u_1} {β : Type u_2} {mβ : MeasurableSpace β} {m0 : MeasurableSpace α} {f : α → β}
  {μa : autoParam (MeasureTheory.Measure α) MeasureTheory.Measure.QuasiMeasurePreserving._auto_1}
  {μb : autoParam (MeasureTheory.Measure β) MeasureTheory.Measure.QuasiMeasurePreserving._auto_3},
  MeasureTheory.Measure.QuasiMeasurePreserving f μa μb → (MeasureTheory.Measure.map f μa).AbsolutelyContinuous μb
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.node3L : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α}
  {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) m ↑y →
      Ordnode.Valid' (↑y) r o₂ →
        Ordnode.BalancedSz l.size m.size →
          Ordnode.BalancedSz (l.size + m.size + 1) r.size → Ordnode.Valid' o₁ (l.node3L x m y r) o₂
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabLit : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
Bundle.ContMDiffRiemannianMetric.isVonNBounded : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (b : B) → TopologicalSpace (E b)] [inst_9 : (b : B) → AddCommGroup (E b)]
  [inst_10 : (b : B) → Module ℝ (E b)] [inst_11 : FiberBundle F E] [inst_12 : VectorBundle ℝ F E]
  (self : Bundle.ContMDiffRiemannianMetric IB n F E) (b : B), Bornology.IsVonNBounded ℝ {v | ((self.inner b) v) v < 1}
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toNonUnitalSubalgebra_toSubalgebra : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), S.toNonUnitalSubalgebra.toSubalgebra ⋯ = S
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_def_minFac : ∀ {p : ℕ}, Nat.Prime p ↔ 2 ≤ p ∧ p.minFac = p
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycleOn_singleton : ∀ {α : Type u_2} {f : Equiv.Perm α} {a : α}, f.IsCycleOn {a} ↔ f a = a
-- Mathlib.Algebra.Homology.Single
CochainComplex.toSingle₀Equiv_symm_apply_f_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {C : CochainComplex V ℕ} {X : V} (f : C.X 0 ⟶ X) (n : ℕ),
  ((C.toSingle₀Equiv X).symm f).f (n + 1) = 0
-- Mathlib.Order.KrullDimension
Order.height_top_eq_krullDim : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α], ↑(Order.height ⊤) = Order.krullDim α
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.carrierEquiv_symm_fst : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (T : AlgebraicGeometry.Scheme.Pullback.Triplet f g)
  (p : ↥(AlgebraicGeometry.Spec T.tensor)),
  (CategoryTheory.Limits.pullback.fst f g) (AlgebraicGeometry.Scheme.Pullback.carrierEquiv.symm ⟨T, p⟩) = T.x
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.toValuation_apply : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  (r : R), (AddValuation.toValuation v) r = Multiplicative.ofAdd (OrderDual.toDual (v r))
-- Std.Data.TreeMap.Slice
Std.TreeMap.instSliceableRiiSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.instSliceableRiiSlice._auto_1) →
      Std.Rii.Sliceable (Std.TreeMap α β cmp) α (Std.DTreeMap.Internal.Const.RiiSlice α β)
-- Init.Data.SInt.Basic
/-- Converts a 16-bit signed integer to an arbitrary-precision integer that denotes the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.toInt : Int16 → ℤ
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits_obj : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  (j : J),
  (CategoryTheory.Limits.DiagramOfCocones.mkOfHasColimits F).obj j = CategoryTheory.Limits.colimit.cocone (F.obj j)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_prod_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (a b : α × β),
  Set.Icc a b = Set.Icc a.1 b.1 ×ˢ Set.Icc a.2 b.2
-- Mathlib.Data.Ordmap.Invariants
/-- Concatenate two nodes, performing a left rotation `x (y z) -> ((x y) z)`
if balance is upset.  -/
Ordnode.rotateL : {α : Type u_1} → Ordnode α → α → Ordnode α → Ordnode α
-- Mathlib.Data.Sign.Basic
signHom_apply : ∀ {α : Type u} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α], ⇑signHom = ⇑SignType.sign
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanQueryModuleResponse.fromJson : Lean.Json → Except String Lean.Lsp.LeanQueryModuleResponse
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.eq_4 : ∀ (coeff : ℤ) (a b : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.toPoly'.go coeff (a.sub b) =
    Int.Internal.Linear.Expr.toPoly'.go coeff a ∘ Int.Internal.Linear.Expr.toPoly'.go (-coeff) b
-- Mathlib.Data.ENNReal.Operations
ENNReal.pow_eq_top_iff : ∀ {a : ENNReal} {n : ℕ}, a ^ n = ⊤ ↔ a = ⊤ ∧ n ≠ 0
-- Mathlib.Topology.Constructions.SumProd
Topology.IsClosedEmbedding.inr : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsClosedEmbedding Sum.inr
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.symm : ∀ {α : Type u_1} {s : Finset α} {G : SimpleGraph α} {r k : ℕ} [inst : DecidableEq α] {v w₁ w₂ : α} {t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → G.IsFiveWheelLike r k v w₂ w₁ t s
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.instAddSemigroupQuotient : {S : Type u_2} →
  (M : Type u_3) →
    [inst : SMul S M] → [inst_1 : AddSemigroup M] → (c : ModuleCon S M) → AddSemigroup (ModuleCon.Quotient M c)
-- Mathlib.Data.Fin.Tuple.Basic
Fin.exists_iff_succAbove : ∀ {n : ℕ} {P : Fin (n + 1) → Prop} (p : Fin (n + 1)), (∃ i, P i) ↔ P p ∨ ∃ i, P (p.succAbove i)
-- Mathlib.Topology.Algebra.MulAction
Inseparable.vadd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : VAdd M X]
  [ContinuousVAdd M X] {a b : M} {x y : X}, Inseparable a b → Inseparable x y → Inseparable (a +ᵥ x) (b +ᵥ y)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (↑(m.insertMany l)).getKey? k = m.getKey? k
-- Mathlib.Order.Filter.Ker
Filter.subset_ker : ∀ {α : Type u_2} {f : Filter α} {s : Set α}, s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Whether a given finset is 3AP-free is decidable.  -/
ThreeAPFree.instDecidable : {α : Type u_2} → [inst : AddMonoid α] → [DecidableEq α] → {s : Finset α} → Decidable (ThreeAPFree ↑s)
-- Mathlib.CategoryTheory.Category.Basic
/-- Precompose an equation between morphisms by another morphism  -/
CategoryTheory.whisker_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f g : Y ⟶ X} (h : Z ⟶ Y),
  f = g → CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g
-- Lean.Declaration
Lean.instInhabitedConstructorVal.default : Lean.ConstructorVal
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instSMulNat : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → SMul ℕ (ProbabilityTheory.Kernel α β)
-- Init.Data.UInt.Lemmas
UInt16.mul_assoc : ∀ (a b c : UInt16), a * b * c = a * (b * c)
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isTheta_ofReal_left : ∀ {α : Type u_1} {E : Type u_2} [inst : Norm E] {l : Filter α} {f : α → ℝ} {g : α → E},
  (fun x => ↑(f x)) =Θ[l] g ↔ f =Θ[l] g
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (c₁ : CategoryTheory.Limits.KernelFork S₁.g)
  (hc₁ : CategoryTheory.Limits.IsLimit c₁) (hf₂ : S₂.f = 0) (c₂ : CategoryTheory.Limits.KernelFork S₂.g)
  (hc₂ : CategoryTheory.Limits.IsLimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
      CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂)),
  (CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork φ hf₁ c₁ hc₁ hf₂ c₂ hc₂ f comm).φH = f
-- Mathlib.FieldTheory.KummerExtension
autEquivZmod.congr_simp : ∀ {K : Type u} [inst : Field K] {n : ℕ} {a a_1 : K} (e_a : a = a_1)
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] [inst_4 : NeZero n] {ζ ζ_1 : K}
  (e_ζ : ζ = ζ_1) (hζ : IsPrimitiveRoot ζ n), autEquivZmod H L hζ = autEquivZmod ⋯ L ⋯
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.paddingLeft : Lean.Elab.InlayHintInfo → Bool
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.topologicalSpace : (p : ENNReal) → {ι : Type u_2} → (β : ι → Type u_4) → [(i : ι) → TopologicalSpace (β i)] → TopologicalSpace (PiLp p β)
-- Lean.Data.KVMap
Lean.KVMap.forIn : {δ : Type w} →
  {m : Type w → Type w'} → [Monad m] → Lean.KVMap → δ → (Lean.Name × Lean.DataValue → δ → m (ForInStep δ)) → m δ
-- Mathlib.Topology.Defs.Basic
WithTopology.toTopology.inj : ∀ {X : Type u_1} {t : TopologicalSpace X} {ofTopology ofTopology_1 : X},
  WithTopology.toTopology t ofTopology = WithTopology.toTopology t ofTopology_1 → ofTopology = ofTopology_1
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInfEntourage_le_coverEntropyInf : ∀ {X : Type u_1} {U : SetRel X X} [inst : UniformSpace X] (T : X → X) (F : Set X),
  U ∈ uniformity X → Dynamics.coverEntropyInfEntourage T F U ≤ Dynamics.coverEntropyInf T F
-- Mathlib.Data.Set.Sups
Set.infs_self : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, s ⊼ s = s ↔ InfClosed s
-- Mathlib.RingTheory.HahnSeries.Binomial
HahnSeries.SummableFamily.binomialFamily_mem_support : ∀ {Γ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : LinearOrder Γ] [inst_1 : AddCommMonoid Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : BinomialRing R] [inst_5 : CommRing A]
  [inst_6 : Algebra R A] {x : HahnSeries Γ A},
  0 < (x - 1).orderTop →
    ∀ (r : R) (n : ℕ) {g : Γ}, g ∈ ((HahnSeries.SummableFamily.binomialFamily x r) n).support → 0 ≤ g
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.hom_injective : ∀ {V : Type u} {G : SimpleGraph V} {x : G.Subgraph}, Function.Injective ⇑x.hom
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
/-- A set `S` such that `t = cylinder s S`. `s` is given by `closedCompactCylinders.finset`.  -/
MeasureTheory.closedCompactCylinders.set : {ι : Type u_1} →
  {X : ι → Type u_2} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {t : Set ((i : ι) → X i)} →
        (ht : t ∈ MeasureTheory.closedCompactCylinders X) →
          Set ((i : ↥(MeasureTheory.closedCompactCylinders.finset ht)) → X ↑i)
-- Mathlib.Analysis.Complex.Basic
RCLike.to_complex_nonneg_iff : ∀ {𝕜 : Type u_2} [inst : RCLike 𝕜] {a : 𝕜}, 0 ≤ ↑(RCLike.re a) + ↑(RCLike.im a) * Complex.I ↔ 0 ≤ a
-- Mathlib.Data.Finset.Prod
Finset.product_inter : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t t' : Finset β} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
/-- A continuous linear map from `E` to `F` is still continuous when `E` and `F` are equipped with
their weak topologies.  -/
WeakSpace.map : {𝕜 : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      [inst : CommSemiring 𝕜] →
        [inst_1 : TopologicalSpace 𝕜] →
          [inst_2 : ContinuousAdd 𝕜] →
            [inst_3 : ContinuousConstSMul 𝕜 𝕜] →
              [inst_4 : AddCommMonoid E] →
                [inst_5 : Module 𝕜 E] →
                  [inst_6 : TopologicalSpace E] →
                    [inst_7 : AddCommMonoid F] →
                      [inst_8 : Module 𝕜 F] →
                        [inst_9 : TopologicalSpace F] → (E →L[𝕜] F) → WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F
-- Mathlib.Topology.Category.TopCat.Adjunctions
TopCat.adj₁_counit : TopCat.adj₁.counit =
  { app := fun X => TopCat.ofHom { toFun := id, continuous_toFun := ⋯ }, naturality := TopCat.adj₁._proof_1 }
-- Mathlib.Data.NNReal.Defs
NNReal.instSemilatticeInf : SemilatticeInf NNReal
-- Std.Time.DateTime.WallTime
/-- Adds a `Nanosecond.Offset` to the given `WallTime`.
 -/
Std.Time.WallTime.addNanoseconds : Std.Time.WallTime → Std.Time.Nanosecond.Offset → Std.Time.WallTime
-- Mathlib.Order.Basic
LE.le.ge_or_le : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, a ≤ b → ∀ (c : α), a ≤ c ∨ c ≤ b
-- Mathlib.LinearAlgebra.Pi
LinearMap.proj_comp_single : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i j : ι),
  LinearMap.proj i ∘ₗ LinearMap.single R φ j = LinearMap.diag j i
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSet.preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {t : Set β},
  MeasurableSet t → Measurable f → MeasurableSet (f ⁻¹' t)
-- Mathlib.NumberTheory.MulChar.Lemmas
/-- The non-zero values of a multiplicative character `χ` such that `χ^n = 1`
are `n`th roots of unity.  -/
MulChar.apply_mem_rootsOfUnity_of_pow_eq_one : ∀ {F : Type u_1} [inst : Field F] [Finite F] {R : Type u_2} [inst_2 : CommRing R] {χ : MulChar F R} {n : ℕ},
  χ ^ n = 1 → ∀ {a : F}, a ≠ 0 → ∃ ζ ∈ rootsOfUnity n R, ↑ζ = χ a
-- Init.Core
/-- `PNonScalar` is a type that is not a scalar value in our runtime.
It is used as a stand-in for an arbitrary boxed value to avoid excessive
monomorphization, and it is only created using `unsafeCast`. It is somewhat
analogous to C `void*` in usage, but the type itself is not special.

This is the universe-polymorphic version of `PNonScalar`; it is preferred to use
`NonScalar` instead where applicable.
 -/
PNonScalar : Type u
-- Lean.Meta.Tactic.Grind.Types
/-- Creates an `ENode` for `e` if one does not already exist.
This method assumes `e` has been hash-consed.
 -/
Lean.Meta.Grind.mkENode : Lean.Expr → ℕ → optParam Bool false → Lean.Meta.Grind.GoalM Unit
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.over_forget_compatiblePreserving : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C),
  CategoryTheory.CompatiblePreserving J (CategoryTheory.Over.forget X)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_2 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.or with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_2 ()
-- Init.Data.List.Lemmas
List.mem_flatten_of_mem : ∀ {α : Type u_1} {L : List (List α)} {l : List α} {a : α}, l ∈ L → a ∈ l → a ∈ L.flatten
-- Mathlib.Data.Sigma.Order
Sigma.Lex.noMaxOrder : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Preorder ι] [inst_1 : (i : ι) → Preorder (α i)]
  [∀ (i : ι), NoMaxOrder (α i)], NoMaxOrder (Σₗ (i : ι), α i)
-- Mathlib.Data.Set.Prod
Set.prod_inter : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β}, s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Given a diagram `D` of colimit cocones under the `curry.obj G j`, and a cocone under `G`,
we can construct a cocone under the diagram consisting of the cocone points from `D`.
 -/
CategoryTheory.Limits.coconeOfCoconeCurry : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              {D : CategoryTheory.Limits.DiagramOfCocones (CategoryTheory.Functor.curry.obj G)} →
                ((j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) →
                  CategoryTheory.Limits.Cocone G → CategoryTheory.Limits.Cocone D.coconePoints
-- Lean.Meta.Closure
Lean.Meta.Closure.State.mk.sizeOf_spec : ∀ (visitedLevel : Lean.LevelMap Lean.Level) (visitedExpr : Lean.ExprStructMap Lean.Expr) (levelParams : Array Lean.Name)
  (nextLevelIdx : ℕ) (levelArgs : Array Lean.Level)
  (newLocalDecls newLocalDeclsForMVars newLetDecls : Array Lean.LocalDecl) (nextExprIdx : ℕ)
  (exprMVarArgs exprFVarArgs : Array Lean.Expr) (toProcess : Array Lean.Meta.Closure.ToProcessElement),
  sizeOf
      { visitedLevel := visitedLevel, visitedExpr := visitedExpr, levelParams := levelParams,
        nextLevelIdx := nextLevelIdx, levelArgs := levelArgs, newLocalDecls := newLocalDecls,
        newLocalDeclsForMVars := newLocalDeclsForMVars, newLetDecls := newLetDecls, nextExprIdx := nextExprIdx,
        exprMVarArgs := exprMVarArgs, exprFVarArgs := exprFVarArgs, toProcess := toProcess } =
    1 + sizeOf visitedLevel + sizeOf visitedExpr + sizeOf levelParams + sizeOf nextLevelIdx + sizeOf levelArgs +
                  sizeOf newLocalDecls +
                sizeOf newLocalDeclsForMVars +
              sizeOf newLetDecls +
            sizeOf nextExprIdx +
          sizeOf exprMVarArgs +
        sizeOf exprFVarArgs +
      sizeOf toProcess
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.transitionMap.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {m n : ℕ} (hmn : m ≤ n), AdicCompletion.transitionMap I M hmn = AdicCompletion.transitionMap I M hmn
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Restatement of `jacobiTheta₂'_add_left'`: the function `jacobiTheta₂''` is 1-periodic in `z`.  -/
HurwitzZeta.jacobiTheta₂''_add_left : ∀ (z τ : ℂ), HurwitzZeta.jacobiTheta₂'' (z + 1) τ = HurwitzZeta.jacobiTheta₂'' z τ
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.domCongr_symm : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (e : M ≃+ N),
  (AddMonoidAlgebra.domCongr R A e).symm = AddMonoidAlgebra.domCongr R A e.symm
-- Std.Time.Date.Unit.Year
Std.Time.Year.Era.ce.sizeOf_spec : sizeOf Std.Time.Year.Era.ce = 1
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.length.eq_1 : ∀ {α : Type u_1}, Batteries.BinomialHeap.Imp.Heap.nil.length = 0