mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sync.Channel
Std.CloseableChannel.instAsyncWriteOfInhabited : {α : Type} → [Inhabited α] → Std.Async.IO.AsyncWrite (Std.CloseableChannel α) α
-- Mathlib.Topology.MetricSpace.IsometricSMul
edist_div_left : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G]
  (a b c : G), edist (a / b) (a / c) = edist b c
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.relabelNat_size_eq_size : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {aig : Std.Sat.AIG α},
  aig.relabelNat.decls.size = aig.decls.size
-- Mathlib.Data.Set.Function
Set.InjOn.rightInvOn_of_leftInvOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {f' : β → α},
  Set.InjOn f s → Set.LeftInvOn f f' t → Set.MapsTo f s t → Set.MapsTo f' t s → Set.RightInvOn f f' s
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_empty`.

---

The Hausdorff edistance to the empty set is infinite.  -/
EMetric.hausdorffEdist_empty : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set α}, s.Nonempty → Metric.hausdorffEDist s ∅ = ⊤
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.limitCommMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommMonCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommMonCat)).sections],
  CommMonCat.limitCommMonoid F =
    {
      mul :=
        CommMonCat.limitCommMonoid._aux_1 F
          (MonCat.sectionsSubmonoid (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))).toCommMonoid,
      mul_assoc := ⋯,
      one :=
        CommMonCat.limitCommMonoid._aux_4 F
          (MonCat.sectionsSubmonoid (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))).toCommMonoid,
      one_mul := ⋯, mul_one := ⋯,
      npow :=
        CommMonCat.limitCommMonoid._aux_8 F
          (MonCat.sectionsSubmonoid (F.comp (CategoryTheory.forget₂ CommMonCat MonCat))).toCommMonoid,
      npow_zero := ⋯, npow_succ := ⋯, mul_comm := ⋯ }
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.isDenseInducing : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], p ≠ ⊤ → IsDenseInducing Subtype.val
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.lam.sizeOf_spec : ∀ (f : Lean.Expr), sizeOf (Mathlib.Meta.FunProp.MaybeFunctionData.lam f) = 1 + sizeOf f
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- The Radon-Nikodym derivative of the restriction of a measure to a measurable set is the
indicator function of this set.  -/
MeasureTheory.Measure.rnDeriv_restrict_self : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite ν] {s : Set α},
  MeasurableSet s → (ν.restrict s).rnDeriv ν =ᵐ[ν] s.indicator 1
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagations.mk.injEq : ∀ (data data_1 : Lean.Meta.Grind.PendingSolverPropagationsData✝),
  ({ data := data } = { data := data_1 }) = (data = data_1)
-- Mathlib.Data.Set.Prod
Function.pullback_comm_sq : ∀ {X : Type u_2} {Y : Sort u_3} {Z : Type u_1} (f : X → Y) (g : Z → Y),
  f ∘ Function.Pullback.fst = g ∘ Function.Pullback.snd
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.is_ascending_rev_series_of_is_descending : ∀ (G : Type u_1) [inst : AddGroup G] {H : ℕ → AddSubgroup G} {n : ℕ},
  H n = ⊥ → AddSubgroup.IsDescendingCentralSeries H → AddSubgroup.IsAscendingCentralSeries fun m => H (n - m)
-- Mathlib.RingTheory.PowerSeries.Restricted
PowerSeries.isRestricted_C : ∀ {R : Type u_1} [inst : NormedRing R] (c : ℝ) (a : R), PowerSeries.IsRestricted c (PowerSeries.C a)
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.eq_top_of_card_eq : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Finite ↥H], Nat.card ↥H = Nat.card G → H = ⊤
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_one : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R] [inst_1 : One R], ↑1 = 1
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.isUnit_iff_isUnit_apply_one : ∀ {R : Type u_1} [inst : CommRing R] {f : ArithmeticFunction R}, IsUnit f ↔ IsUnit (f 1)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.instCancelMonoid.eq_1 : ∀ {α : Type u_1},
  FreeMonoid.instCancelMonoid =
    { mul := fun x y => FreeMonoid.ofList (FreeMonoid.toList x ++ FreeMonoid.toList y), mul_assoc := ⋯,
      one := FreeMonoid.ofList [], one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯, toIsLeftCancelMul := ⋯,
      toIsRightCancelMul := ⋯ }
-- Mathlib.Order.Interval.Finset.Floor
Int.cast_mem_Icc_iff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a b : α} {n : ℤ},
  ↑n ∈ Set.Icc a b ↔ n ∈ Finset.Icc ⌈a⌉ ⌊b⌋
-- Mathlib.Order.SuccPred.Basic
WithTop.instSuccOrder : {α : Type u_1} →
  [inst : PartialOrder α] → [inst_1 : SuccOrder α] → [(a : α) → Decidable (Order.succ a = a)] → SuccOrder (WithTop α)
-- Mathlib.Topology.Compactification.StoneCech
/-- The map `pure : α → Ultrafilter α` induces on `α` the discrete topology.  -/
induced_topology_pure : ∀ {α : Type u}, TopologicalSpace.induced pure Ultrafilter.topologicalSpace = ⊥
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasLimitsOfShapeDiscreteInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type v}
  [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) C],
  CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete J) (CategoryTheory.Ind C)
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.unit_leftAdjointUniq_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G),
  CategoryTheory.CategoryStruct.comp adj1.unit (CategoryTheory.Functor.whiskerRight (adj1.leftAdjointUniq adj2).hom G) =
    adj2.unit
-- Lean.Util.CollectLevelMVars
Lean.CollectLevelMVars.State.mk.injEq : ∀ (visitedLevel : Lean.LevelSet) (visitedExpr : Lean.ExprSet) (result : Array Lean.LMVarId)
  (visitedLevel_1 : Lean.LevelSet) (visitedExpr_1 : Lean.ExprSet) (result_1 : Array Lean.LMVarId),
  ({ visitedLevel := visitedLevel, visitedExpr := visitedExpr, result := result } =
      { visitedLevel := visitedLevel_1, visitedExpr := visitedExpr_1, result := result_1 }) =
    (visitedLevel = visitedLevel_1 ∧ visitedExpr = visitedExpr_1 ∧ result = result_1)
-- Mathlib.Order.Filter.Bases.Basic
/-- `s` is directed downwards on `i` such that `p i`.  -/
Filter.IsBasis.inter : ∀ {α : Type u_1} {ι : Sort u_4} {p : ι → Prop} {s : ι → Set α},
  Filter.IsBasis p s → ∀ {i j : ι}, p i → p j → ∃ k, p k ∧ s k ⊆ s i ∩ s j
-- Init.Data.Int.Gcd
Int.gcd_add_right_right_of_dvd : ∀ {n k : ℤ} (m : ℤ), n ∣ k → n.gcd (m + k) = n.gcd m
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.abs : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → ℝ},
  IntervalIntegrable f μ a b → IntervalIntegrable (fun x => |f x|) μ a b
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instLT : {M : Type u_1} → [Group M] → [Lattice M] → LT (MulArchimedeanOrder M)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Under.pushoutIsLeftAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushoutsAlong f], (CategoryTheory.Under.pushout f).IsLeftAdjoint
-- Mathlib.Topology.Algebra.Constructions
AddOpposite.comap_op_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : Mᵃᵒᵖ),
  Filter.comap AddOpposite.op (nhds x) = nhds (AddOpposite.unop x)
-- Mathlib.Algebra.Homology.Localization
HomotopyCategory.instIsMultiplicativeQuasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C],
  (HomotopyCategory.quasiIso C c).IsMultiplicative
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k (m₁.diff! m₂) =
          (Std.DTreeMap.Internal.Impl.contains k m₁ && !Std.DTreeMap.Internal.Impl.contains k m₂)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
innerSL_apply_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v w : E), ((innerSL 𝕜) v) w = inner 𝕜 v w
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.exists_d_comp_eq_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C},
  CategoryTheory.IsSeparator G →
    ∀ {A : C} (B : C) [CategoryTheory.Injective B] {M : ModuleCat (CategoryTheory.End G)ᵐᵒᵖ}
      (g : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ A)),
      CategoryTheory.Mono g →
        ∀ (f : M ⟶ ModuleCat.of (CategoryTheory.End G)ᵐᵒᵖ (G ⟶ B)),
          ∃ l,
            CategoryTheory.CategoryStruct.comp (CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d g) l =
              CategoryTheory.IsGrothendieckAbelian.GabrielPopescuAux.d f
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.any.eq_def : ∀ (x : ℕ) (x_1 : (i : ℕ) → i < x → Bool),
  x.any x_1 =
    match x, x_1 with
    | 0, f => false
    | n.succ, f => (n.any fun i h => f i ⋯) || f n ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DHashMap.Raw.Const.getD (m₁.diff m₂) k fallback =
          if k ∈ m₂ then fallback else Std.DHashMap.Raw.Const.getD m₁ k fallback
-- Mathlib.CategoryTheory.GradedObject.Monoidal
/-- Constructor for morphisms from a tensor product of two graded objects.  -/
CategoryTheory.GradedObject.Monoidal.tensorObjDesc : {I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          {X₁ X₂ : CategoryTheory.GradedObject I C} →
            [inst_3 : X₁.HasTensor X₂] →
              {A : C} →
                {k : I} →
                  ((i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)) →
                    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ k ⟶ A)
-- Mathlib.Geometry.Euclidean.Incenter
/-- All excenters exist for a triangle.  -/
Affine.Triangle.excenterExists : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (signs : Finset (Fin 3)),
  Affine.Simplex.ExcenterExists t signs
-- Mathlib.CategoryTheory.Galois.Decomposition
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.mkSelfProdFib.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] (X : C),
  CategoryTheory.PreGaloisCategory.mkSelfProdFib✝ F X =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.PreservesProduct.iso F fun x => X).inv)
      ((CategoryTheory.Limits.Concrete.productEquiv fun x => F.obj X).symm id)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_mono_nnnorm_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) → MeasureTheory.eLpNorm f p μ ≤ MeasureTheory.eLpNorm g p μ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_le_inv_mul_iff : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a b c d : α} [MulRightMono α],
  a * b⁻¹ ≤ d⁻¹ * c ↔ d * a ≤ c * b
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_subset_singleton : ∀ {α : Type u_1} (n : ℕ) (a : α), Multiset.replicate n a ⊆ {a}
-- Init.Data.Option.Attach
Option.all_unattach : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }} {q : α → Bool},
  Option.all q o.unattach = Option.all (q ∘ Subtype.val) o
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (Std.ExtTreeMap.ofList l cmp)[k']? = some v
-- Mathlib.Topology.Order
/-- A topological space is indiscrete if the only open sets are the empty set and the whole space,
that is that its topology equals the indiscrete topology `⊤`.

This can also go by the name "trivial topology" or "codiscrete topology".  -/
IndiscreteTopology : (α : Type u_2) → [TopologicalSpace α] → Prop
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- `a / b` is the unique ordinal `q` satisfying `a = b * q + r` with `r < b`.  -/
Ordinal.div : Div Ordinal.{u_4}
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrowCone_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C}
  (c : CategoryTheory.Limits.Cone K) (F : CategoryTheory.Functor C D) {X : D} (f : X ⟶ F.obj c.pt),
  (c.toStructuredArrowCone F f).pt = CategoryTheory.StructuredArrow.mk f
-- Init.Core
Iff.symm : ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
-- Mathlib.RingTheory.PowerSeries.Expand
PowerSeries.order_expand : ∀ {R : Type u_2} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : PowerSeries R),
  ((PowerSeries.expand p hp) φ).order = p • φ.order
-- Mathlib.CategoryTheory.Abelian.Injective.Dimension
CategoryTheory.HasInjectiveDimensionLT.subsingleton' : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C} {X : C} {n : ℕ}
  [self : CategoryTheory.HasInjectiveDimensionLT X n] (i : ℕ),
  n ≤ i → ∀ ⦃Y : C⦄, Subsingleton (CategoryTheory.Abelian.Ext Y X i)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_pow_coe_angle : ∀ (x : ℂ) (n : ℕ), ↑(x ^ n).arg = n • ↑x.arg
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.top_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] {x : CompleteLattice β} (a : α), ⊤ a = ⊤
-- Lean.LocalContext
/-- Low level API for auxiliary declarations. Do not use directly.  -/
Lean.LocalContext.mkAuxDecl : Lean.LocalContext → Lean.FVarId → Lean.Name → Lean.Expr → Lean.Name → Lean.LocalContext
-- Mathlib.CategoryTheory.Iso
/-- Reinterpret a morphism `f : X ⟶ Y` with an `IsIso f` instance as `Y ≅ X`.  -/
CategoryTheory.asIso' : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (f : Y ⟶ X) → [CategoryTheory.IsIso f] → X ≅ Y
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.Arrow.Hom.zero_left : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T]
  {u v : CategoryTheory.Arrow T}, CategoryTheory.Arrow.Hom.left 0 = 0
-- Mathlib.Algebra.Regular.Basic
/-- If a product is regular, so is its left factor.  -/
IsRegular.of_mul_left : ∀ {R : Type u_1} [inst : CommSemigroup R] {a b : R}, IsRegular (a * b) → IsRegular a
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.imp_sup_left : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} (φ ψ : L.BoundedFormula α n), T.Imp φ (φ ⊔ ψ)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.sieve₁_eq_pullback_sieve₁' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreOneHypercover S) {i₁ i₂ : E.I₀}
  [inst_1 : CategoryTheory.Limits.HasPullback (E.f i₁) (E.f i₂)] {W : C} (p₁ : W ⟶ E.X i₁) (p₂ : W ⟶ E.X i₂)
  (w : CategoryTheory.CategoryStruct.comp p₁ (E.f i₁) = CategoryTheory.CategoryStruct.comp p₂ (E.f i₂)),
  E.sieve₁ p₁ p₂ = CategoryTheory.Sieve.pullback (CategoryTheory.Limits.pullback.lift p₁ p₂ w) (E.sieve₁' i₁ i₂)
-- Mathlib.Analysis.Seminorm
Seminorm.instDistribMulAction : {R : Type u_1} →
  {𝕜 : Type u_3} →
    {E : Type u_7} →
      [inst : SeminormedRing 𝕜] →
        [inst_1 : AddGroup E] →
          [inst_2 : SMul 𝕜 E] →
            [inst_3 : Monoid R] →
              [inst_4 : DistribMulAction R ℝ] →
                [inst_5 : SMul R NNReal] → [IsScalarTower R NNReal ℝ] → DistribMulAction R (Seminorm 𝕜 E)
-- Mathlib.CategoryTheory.Category.Preorder
OrderHom.equivalenceFunctor_functor_obj_obj : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (f : X →o Y) (a : X),
  (OrderHom.equivalenceFunctor.functor.obj f).obj a = f a
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (N : ℕ → C) →
        (ι : (n : ℕ) → N n ⟶ X.obj (Opposite.op { len := n })) →
          ((Δ : SimplexCategoryᵒᵖ) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.SimplicialObject.Splitting.cofan' N X ι Δ)) →
            X.Splitting
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.val_list_sum : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (l : List ↥H), ↑l.sum = (List.map Subtype.val l).sum
-- Init.Data.Range.Polymorphic.Iterators
Std.Rio.Internal.iter.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.Least? α] (r : Std.Rio α),
  Std.Rio.Internal.iter r = { internalState := { next := Std.PRange.least?, upperBound := r.upper } }
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The morphism `opZ^{n₀}(f₂, f₃) ⟶ H^{n₁}(f₁)` induced by `δ`
when `f₁`, `f₂`, `f₃` are composable morphisms and `n₀ + 1 = n₁`.  -/
CategoryTheory.Abelian.SpectralObject.δFromOpcycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ : ℤ) →
                      autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δFromOpcycles._auto_1 →
                        (X.opcycles f₂ f₃ n₀ ⟶ (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁))
-- Mathlib.Data.TypeVec
TypeVec.appendFun_aux : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : (α ::: β).Arrow (α' ::: β')),
  (TypeVec.dropFun f ::: TypeVec.lastFun f) = f
-- Mathlib.Logic.Basic
Ne.dite_eq_left_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a : α} {B : ¬P → α},
  (∀ (h : ¬P), a ≠ B h) → (dite P (fun x => a) B = a ↔ P)
-- Mathlib.Geometry.Convex.Cone.Dual
/-- The dual cone of `s` equals the intersection of dual cones of the points in `s`.  -/
PointedCone.dual_eq_iInter_dual_singleton : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (s : Set M), ↑(PointedCone.dual p s) = ⋂ i, ↑(PointedCone.dual p {↑i})
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.setOfPred_apply : ∀ {α : Type u_8} (p : α → Prop), MeasurableEquiv.setOfPred p = {a | p a}
-- Mathlib.Topology.Order.Compact
/-- A continuous function with compact support is bounded below.  -/
Continuous.bddBelow_range_of_hasCompactMulSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] [inst_4 : One α] {f : β → α}, Continuous f → HasCompactMulSupport f → BddBelow (Set.range f)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.mem_comap : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] {s : Subfield L} {f : K →+* L} {x : K},
  x ∈ Subfield.comap f s ↔ f x ∈ s
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.toPoly'.go.match_1.eq_4 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (a b : Int.Internal.Linear.Expr)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_2 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_3 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b))
  (h_5 : (k : ℤ) → (a : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k a))
  (h_6 : (a : Int.Internal.Linear.Expr) → (k : ℤ) → motive (a.mulR k))
  (h_7 : (a : Int.Internal.Linear.Expr) → motive a.neg),
  (match a.sub b with
    | Int.Internal.Linear.Expr.num k => h_1 k
    | Int.Internal.Linear.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Int.Internal.Linear.Expr.mulL k a => h_5 k a
    | a.mulR k => h_6 a k
    | a.neg => h_7 a) =
    h_4 a b
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.ConstPromiseVal.mk.inj : ∀ {privateConstInfo exportedConstInfo : Lean.ConstantInfo} {exts : Array Lean.EnvExtensionState}
  {nestedConsts : Lean.VisibilityMap✝ Lean.AsyncConsts✝} {privateConstInfo_1 exportedConstInfo_1 : Lean.ConstantInfo}
  {exts_1 : Array Lean.EnvExtensionState} {nestedConsts_1 : Lean.VisibilityMap✝ Lean.AsyncConsts✝},
  { privateConstInfo := privateConstInfo, exportedConstInfo := exportedConstInfo, exts := exts,
        nestedConsts := nestedConsts } =
      { privateConstInfo := privateConstInfo_1, exportedConstInfo := exportedConstInfo_1, exts := exts_1,
        nestedConsts := nestedConsts_1 } →
    privateConstInfo = privateConstInfo_1 ∧
      exportedConstInfo = exportedConstInfo_1 ∧ exts = exts_1 ∧ nestedConsts = nestedConsts_1
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.map_smulₛₗ : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ.[σ] F) (c : R)
  (x : ↥f.domain), ↑f (c • x) = σ c • ↑f x
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.Iter.step_drop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match 0 with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_1 ()