mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.mk.inj : ∀ {R : Type u} {M : Type v} {inst : VAdd R M} {carrier : Set M}
  {vadd_mem' : ∀ (c : R) {x : M}, x ∈ carrier → c +ᵥ x ∈ carrier} {carrier_1 : Set M}
  {vadd_mem'_1 : ∀ (c : R) {x : M}, x ∈ carrier_1 → c +ᵥ x ∈ carrier_1},
  { carrier := carrier, vadd_mem' := vadd_mem' } = { carrier := carrier_1, vadd_mem' := vadd_mem'_1 } →
    carrier = carrier_1
-- Mathlib.Algebra.Order.Ring.Synonym
toLex_ofNat : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ) [inst_1 : n.AtLeastTwo], toLex (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Analysis.Convex.StdSimplex
single_mem_stdSimplex : ∀ (𝕜 : Type u_2) {ι : Type u_1} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι]
  [inst_3 : DecidableEq ι] [ZeroLEOneClass 𝕜] (i : ι), Pi.single i 1 ∈ stdSimplex 𝕜 ι
-- Mathlib.Analysis.Complex.Basic
Complex.conjLIE_apply : ∀ (z : ℂ), Complex.conjLIE z = (starRingEnd ℂ) z
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zpowersHom_bijective : ∀ {G : Type u_2} [Infinite G] [inst : Group G] {g : G}, Subgroup.zpowers g = ⊤ → Function.Bijective ⇑((zpowersHom G) g)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.addAux.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.lt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_1 ()
-- Init.Data.UInt.Bitwise
UInt64.shiftRight_xor : ∀ {a b c : UInt64}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.tendsto_rpow_atTop_of_base_lt_one : ∀ {b : ENNReal}, b < 1 → Filter.Tendsto (fun x => b ^ x) Filter.atTop (nhds 0)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
quasispectrum.instCompactSpace : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {B : Type u_3} [inst_1 : NonUnitalNormedRing B] [inst_2 : NormedSpace 𝕜 B]
  [CompleteSpace B] [IsScalarTower 𝕜 B B] [SMulCommClass 𝕜 B B] [ProperSpace 𝕜] (a : B),
  CompactSpace ↑(quasispectrum 𝕜 a)
-- Mathlib.Analysis.Analytic.ChangeOrigin
/-- If a function admits a power series expansion `p` on an open ball `B (x, r)`, then
it is analytic at every point of this ball.  -/
HasFPowerSeriesWithinOnBall.analyticWithinAt_of_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x y : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r → y ∈ insert x s ∩ Metric.eball x r → AnalyticWithinAt 𝕜 f s y
-- Mathlib.RingTheory.Teichmuller
Perfection.teichmuller_spec' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] {x : Perfection (R ⧸ I) p} {y : R},
  (∃ N, ∀ n ≥ N, ∃ z, (Ideal.Quotient.mk I) z = (Perfection.coeff (R ⧸ I) p n) x ∧ z ^ p ^ n ≡ y [SMOD I ^ (n + 1)]) →
    (Perfection.teichmuller p I) x = y
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.mul_mul_conjTranspose_same : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : Fintype n] [Finite m] {A : Matrix n n R},
  A.PosSemidef → ∀ (B : Matrix m n R), (B * A * B.conjTranspose).PosSemidef
-- Init.Prelude
/-- Revert all `addMacroScope` calls. `v = extractMacroScopes n → n = v.review`.
This operation is useful for analyzing/transforming the original identifiers, then adding back
the scopes (via `MacroScopesView.review`).  -/
Lean.extractMacroScopes : Lean.Name → Lean.MacroScopesView
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (X : CategoryTheory.Mon (CategoryTheory.Functor C D)) (x : C),
  (CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.unitIso.hom.app X).hom.app x =
    CategoryTheory.CategoryStruct.id (X.X.obj x)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prod.snd_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} (x : C),
  CategoryTheory.FunctorToTypes.prod.snd.app x = TypeCat.ofHom fun a => a.2
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace
SSet.S.IsUniquelyCodimOneFace.unique : ∀ {X : SSet} {x y : X.S} (hxy : x.IsUniquelyCodimOneFace y) {d : ℕ} (hd : x.dim = d)
  (f : { len := d } ⟶ { len := d + 1 }) [CategoryTheory.Mono f],
  (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex →
    f = SimplexCategory.δ (hxy.index hd)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.any_eq_false' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulBEq α] {p : α → β → Bool},
  (↑m).WF →
    ((↑m).any p = false ↔ ∀ (a : α) (h : m.contains a = true), p a (Std.DHashMap.Internal.Raw₀.Const.get m a h) = false)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_iSup : ∀ {α : Type u_1} {β : Type u_3} {ι : Sort u_4} (f : α → β) (m : ι → MeasureTheory.OuterMeasure α),
  (MeasureTheory.OuterMeasure.map f) (⨆ i, m i) = ⨆ i, (MeasureTheory.OuterMeasure.map f) (m i)
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquivClass.toMulEquiv_injective : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : Mul α] [inst_2 : Mul β]
  [inst_3 : MulEquivClass F α β], Function.Injective MulEquivClass.toMulEquiv
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.mk : {R : Type u_5} →
  {S : Type u_6} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : PartialOrder S] →
          (toMulHom : R →ₙ* S) →
            (∀ (x : R), 0 ≤ toMulHom.toFun x) →
              (∀ (x : R), toMulHom.toFun x = 0 ↔ x = 0) →
                (∀ (x y : R), toMulHom.toFun (x + y) ≤ toMulHom.toFun x + toMulHom.toFun y) → AbsoluteValue R S
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_mono : ∀ {M : Type u_1} [inst : AddMonoid M], Monotone AddSubmonoid.addUnits
-- Mathlib.CategoryTheory.Galois.GaloisObjects
CategoryTheory.PreGaloisCategory.IsGalois.quotientByAutTerminal : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.GaloisCategory C} {X : C}
  [self : CategoryTheory.PreGaloisCategory.IsGalois X],
  Nonempty
    (CategoryTheory.Limits.IsTerminal
      (CategoryTheory.Limits.colimit (CategoryTheory.SingleObj.functor (CategoryTheory.Aut.toEnd X))))
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevInTwo'.eq_1 : ∀ {α : Type u_1} {n : ℕ} (l : { l // l.length = n }),
  List.MergeSort.Internal.splitRevInTwo' l =
    (⟨(List.MergeSort.Internal.splitRevAt (n / 2) ↑l).1, ⋯⟩, ⟨(List.MergeSort.Internal.splitRevAt (n / 2) ↑l).2, ⋯⟩)
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.subtype_apply : ∀ {K : Type u} [inst : DivisionRing K] {s : Subfield K} (x : ↥s), s.subtype x = ↑x
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.linInd : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (self : LieAlgebra.Basis ι H), LinearIndependent R self.h
-- Lean.Util.Trace
Lean.TraceElem.mk.inj : ∀ {ref : Lean.Syntax} {msg : Lean.MessageData} {ref_1 : Lean.Syntax} {msg_1 : Lean.MessageData},
  { ref := ref, msg := msg } = { ref := ref_1, msg := msg_1 } → ref = ref_1 ∧ msg = msg_1
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- Bound for norms of ascending Pochhammer symbols.  -/
PadicInt.norm_ascPochhammer_le : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (k : ℕ) (x : ℤ_[p]), ‖Polynomial.eval x (ascPochhammer ℤ_[p] k)‖ ≤ ‖↑k.factorial‖
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv
Complex.contDiffAt_tan : ∀ {x : ℂ} {n : WithTop ℕ∞}, ContDiffAt ℂ n Complex.tan x ↔ Complex.cos x ≠ 0
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.all_bool_eq : ∀ {p : Char → Bool} {s : String}, s.all p = s.toList.all p
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_lt_mul_iff_of_neg_left : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] {a b c : R}, c < 0 → (c * a < c * b ↔ b < a)
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- An isomorphism in `C` gives an isomorphism in `Cᴹᵒᵖ`.  -/
CategoryTheory.Iso.mop : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ≅ Y) → ({ unmop := X } ≅ { unmop := Y })
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.instFunLike : {ι : Type u_1} →
  {k : Type u_5} →
    {V : Type u_6} →
      {P : Type u_7} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] → [inst_2 : Ring k] → [inst_3 : Module k V] → FunLike (AffineBasis ι k P) ι P
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.singularPart_def : ∀ {α : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [inst : ProbabilityTheory.IsSFiniteKernel κ] [inst_1 : ProbabilityTheory.IsSFiniteKernel η],
  κ.singularPart η =
    (κ + η).withDensity fun a x =>
      ↑(κ.rnDerivAux (κ + η) a x).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal * κ.rnDeriv η a x
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to infinity along a nontrivial filter `l`, then
`fun x ↦ r * f x` tends to infinity if and only if `0 < r`.  -/
Filter.tendsto_const_mul_atTop_iff_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => r * f x) l Filter.atTop ↔ 0 < r)
-- Init.Data.Nat.Bitwise.Lemmas
_private.Init.Data.Nat.Bitwise.Lemmas.0.Nat.two_pow_succ_sub_one_div_two : ∀ {n : ℕ}, (2 ^ (n + 1) - 1) / 2 = 2 ^ n - 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.eq_iff_sign_eq_and_abs_toReal_eq : ∀ {θ ψ : Real.Angle}, θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.toReal| = |ψ.toReal|
-- Std.Data.DHashMap.RawLemmas
/-- Simpler variant of `get?_filter` when `LawfulBEq` is available.  -/
Std.DHashMap.Raw.Const.get?_filter' : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [LawfulBEq α]
  {f : α → β → Bool} {k : α},
  m.WF →
    Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.filter f m) k = Option.filter (f k) (Std.DHashMap.Raw.Const.get? m k)
-- Mathlib.Algebra.FreeAlgebra
/-- Given a function `f : X → A` where `A` is an `R`-algebra, `lift R f` is the unique lift
of `f` to a morphism of `R`-algebras `FreeAlgebra R X → A`.  -/
FreeAlgebra.lift : (R : Type u_1) →
  {X : Type u_2} →
    [inst : CommSemiring R] →
      {A : Type u_3} → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (X → A) ≃ (FreeAlgebra R X →ₐ[R] A)
-- Mathlib.Algebra.Group.End
MulAut.conj_inv_apply : ∀ {G : Type u_3} [inst : Group G] (g h : G), (MulAut.conj g)⁻¹ h = g⁻¹ * h * g
-- Mathlib.Order.Ideal
Order.Ideal.coe_sup : ∀ {P : Type u_1} [inst : SemilatticeSup P] [inst_1 : IsCodirectedOrder P] {s t : Order.Ideal P},
  ↑(s ⊔ t) = {x | ∃ a ∈ s, ∃ b ∈ t, x ≤ a ⊔ b}
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq_spec_3 : ∀ (x x_1 : Lean.Grind.CommRing.Poly),
  (∀ (a b : ℤ), x = Lean.Grind.CommRing.Poly.num a → x_1 = Lean.Grind.CommRing.Poly.num b → False) →
    (∀ (a : ℤ) (a_1 : Lean.Grind.CommRing.Mon) (a_2 : Lean.Grind.CommRing.Poly) (b : ℤ) (b_1 : Lean.Grind.CommRing.Mon)
        (b_2 : Lean.Grind.CommRing.Poly),
        x = Lean.Grind.CommRing.Poly.add a a_1 a_2 → x_1 = Lean.Grind.CommRing.Poly.add b b_1 b_2 → False) →
      (x == x_1) = false
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_pow : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) {p : MvPolynomial σ R} {n : ℕ}, MvPolynomial.eval₂ f g (p ^ n) = MvPolynomial.eval₂ f g p ^ n
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.all_char_eq_all_beq : ∀ {c : Char} {s : String.Slice}, s.all c = s.all fun x => x == c
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
/-- The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram
of the Stacks entry.
 -/
CategoryTheory.Equalizer.forkMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) →
      {X : C} → (R : CategoryTheory.Presieve X) → P.obj (Opposite.op X) ⟶ CategoryTheory.Equalizer.FirstObj P R
-- Mathlib.RingTheory.Spectrum.Prime.Basic
_private.Mathlib.RingTheory.Spectrum.Prime.Basic.0.PrimeSpectrum.primeSpectrumProdOfSum.match_1.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (motive : PrimeSpectrum R ⊕ PrimeSpectrum S → Sort u_3) (I : Ideal R) (isPrime : I.IsPrime)
  (h_1 : (I : Ideal R) → (isPrime : I.IsPrime) → motive (Sum.inl { asIdeal := I, isPrime := isPrime }))
  (h_2 : (J : Ideal S) → (isPrime : J.IsPrime) → motive (Sum.inr { asIdeal := J, isPrime := isPrime })),
  (match Sum.inl { asIdeal := I, isPrime := isPrime } with
    | Sum.inl { asIdeal := I, isPrime := isPrime } => h_1 I isPrime
    | Sum.inr { asIdeal := J, isPrime := isPrime } => h_2 J isPrime) =
    h_1 I isPrime
-- Mathlib.Topology.DiscreteSubset
isDiscrete_iff_nhdsNE : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] {S : Set Y},
  IsDiscrete S ↔ ∀ x ∈ S, nhdsWithin x {x}ᶜ ⊓ Filter.principal S = ⊥
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_norm_sub_self : ∀ {E : Type u_4} [inst : SeminormedAddCommGroup E] (x : E), Filter.Tendsto (fun a => ‖a - x‖) (nhds x) (nhds 0)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_insert_self : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α} {b : β a}, (m.insert a b).getKeyD a fallback = a
-- Init.Data.List.Lemmas
List.forall_mem_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {l : List α} {P : β → Prop},
  (∀ i ∈ List.filterMap f l, P i) ↔ ∀ j ∈ l, ∀ (b : β), f j = some b → P b
-- Mathlib.Algebra.Order.Group.Synonym
toColex_sub : ∀ {α : Type u_1} [inst : Sub α] (a b : α), toColex (a - b) = toColex a - toColex b
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.measurePreserving_piFinTwo : ∀ {α : Fin 2 → Type u} {m : (i : Fin 2) → MeasurableSpace (α i)} (μ : (i : Fin 2) → MeasureTheory.Measure (α i))
  [∀ (i : Fin 2), MeasureTheory.SigmaFinite (μ i)],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinTwo α)) (MeasureTheory.Measure.pi μ) ((μ 0).prod (μ 1))
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instLocallyOfFiniteTypeSndScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.LocallyOfFiniteType (CategoryTheory.Limits.pullback.snd f g)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.all_eq_false_iff_exists_mem_getKey_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {p : α → β → Bool}, m.WF → (m.all p = false ↔ ∃ a, ∃ (h : a ∈ m), p (m.getKey a h) m[a] = false)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roo : ∀ {m n i : ℕ}, (m<...n).toArray[i]? = if i < n - (m + 1) then some (m + 1 + i) else none
-- Mathlib.Analysis.LocallyConvex.HahnBanach
Module.Dual.exists_extension_of_le_seminorm_real : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (S : Subspace ℝ E) (f : Module.Dual ℝ ↥S)
  {p : Seminorm ℝ E}, (∀ (x : ↥S), f x ≤ p ↑x) → ∃ g, (∀ (x : ↥S), g ↑x = f x) ∧ ∀ (x : E), |g x| ≤ p x
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- The injection `x ↦ Pi.single i x` as a linear isometry.  -/
LinearIsometry.single : {ι : Type u_9} →
  [inst : Fintype ι] →
    [DecidableEq ι] →
      (𝕜 : Type u_10) →
        [inst_2 : NontriviallyNormedField 𝕜] →
          (E : ι → Type u_11) →
            [inst_3 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_4 : (i : ι) → NormedSpace 𝕜 (E i)] → (i : ι) → E i →ₗᵢ[𝕜] (j : ι) → E j
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule
/-- Just like exact integration, the trapezoidal approximation retains the same magnitude but
changes sign when the endpoints are swapped.  -/
trapezoidal_integral_symm : ∀ (f : ℝ → ℝ) {N : ℕ}, 0 < N → ∀ (a b : ℝ), trapezoidal_integral f N a b = -trapezoidal_integral f N b a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A function is `StronglyMeasurable` if it is the limit of simple functions.  -/
MeasureTheory.StronglyMeasurable : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace β] → [MeasurableSpace α] → (α → β) → Prop
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] (s : Finset α), s • ∅ = ∅
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.equivCostructuredArrow_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.Cone.equivCostructuredArrow F).counitIso =
    CategoryTheory.NatIso.ofComponents (fun x => x.eta.symm) ⋯
-- Mathlib.Order.Category.NonemptyFinLinOrd
nonemptyFinLinOrd_dual_comp_forget_to_linOrd : NonemptyFinLinOrd.dual.comp (CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd) =
  (CategoryTheory.forget₂ NonemptyFinLinOrd LinOrd).comp LinOrd.dual
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructor.eq_def : ∀ (ref : Lean.Syntax) (info : Array Lean.Meta.ParamInfo) (explicit : Bool) (idx : ℕ)
  (ps : List Lean.Elab.Tactic.RCases.RCasesPatt),
  Lean.Elab.Tactic.RCases.processConstructor✝ ref info explicit idx ps =
    if x : idx < info.size then
      if (!explicit && info[idx].binderInfo != Lean.BinderInfo.default) = true then
        match Lean.Elab.Tactic.RCases.processConstructor✝ ref info explicit (idx + 1) ps with
        | (ns, tl) => (`_ :: ns, default :: tl)
      else
        if idx + 1 < info.size then
          have p := ps.headD default;
          match Lean.Elab.Tactic.RCases.processConstructor✝ ref info explicit (idx + 1) (ps.tailD []) with
          | (ns, tl) => ((Lean.Elab.Tactic.RCases.RCasesPatt.name?✝ p).getD `_ :: ns, p :: tl)
        else
          match ps with
          | [] => ([`_], [default])
          | [p] => ([(Lean.Elab.Tactic.RCases.RCasesPatt.name?✝ p).getD `_], [p])
          | ps =>
            ([`_],
              [(bif explicit then Lean.Elab.Tactic.RCases.RCasesPatt.explicit ref else id)
                  (Lean.Elab.Tactic.RCases.RCasesPatt.tuple ref ps)])
    else ([], [])
-- Mathlib.Data.Fintype.Lattice
/-- A special case of `Finset.sup_eq_iSup` that omits the useless `x ∈ univ` binder.  -/
Finset.sup_univ_eq_iSup : ∀ {α : Type u_2} {β : Type u_3} [inst : Fintype α] [inst_1 : CompleteLattice β] (f : α → β), Finset.univ.sup f = iSup f
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instNatCast : {R : Type u_1} → [NatCast R] → NatCast (Lex R)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.strictMap_multiplicativeClosure_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D),
  W.multiplicativeClosure.strictMap F ≤ (W.strictMap F).multiplicativeClosure
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
/-- A path whose support contains every vertex is Hamiltonian.  -/
SimpleGraph.Walk.IsPath.isHamiltonian_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a b : α} {p : G.Walk a b},
  p.IsPath → (∀ (w : α), w ∈ p.support) → p.IsHamiltonian
-- Mathlib.Logic.Equiv.Defs
Equiv.existsUnique_congr' : ∀ {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
  (∀ (b : β), p (e.symm b) ↔ q b) → ((∃! a, p a) ↔ ∃! b, q b)
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.isVertexCover_univ : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsVertexCover Set.univ
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.instIsBotOneClass : ∀ {α : Type u} [inst : One α] [inst_1 : LE α] [IsBotOneClass α], IsBotOneClass (WithTop α)
-- Lean.Parser.Extra
Lean.Parser.sepBy1Indent : Lean.Parser.Parser →
  (sep : String) → optParam Lean.Parser.Parser (Lean.Parser.symbol sep) → optParam Bool false → Lean.Parser.Parser
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.inhabited : (α : Type u_1) → [inst : UniformSpace α] → [Inhabited α] → Inhabited (UniformSpace.Completion α)
-- Mathlib.Topology.DiscreteSubset
compl_mem_codiscrete_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set X}, Sᶜ ∈ Filter.codiscrete X ↔ IsClosed S ∧ IsDiscrete S
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.eq_bot_or_exists_simple_le : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  [IsSemisimpleModule R ↥N], N = ⊥ ∨ ∃ m ≤ N, IsSimpleModule R ↥m
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- **Alias** of `TensorProduct.finsuppLeft`.

---

The tensor product of `ι →₀ M` and `N` is linearly equivalent to `ι →₀ M ⊗[R] N`  -/
TensorProduct.finsuppLeft' : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    (N : Type u_4) →
                      [inst_7 : AddCommMonoid N] →
                        [inst_8 : Module R N] →
                          (ι : Type u_5) → [DecidableEq ι] → TensorProduct R (ι →₀ M) N ≃ₗ[S] ι →₀ TensorProduct R M N
-- Mathlib.MeasureTheory.Group.Arithmetic
Multiset.measurable_prod : ∀ {M : Type u_2} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} (l : Multiset (α → M)), (∀ f ∈ l, Measurable f) → Measurable l.prod
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
/-- Characterize the inverse direction of the isomorphism
`PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂` w.r.t. the canonical maps to the limit.  -/
CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂_inv_comp_π_assoc : ∀ {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))
  [inst_5 : CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G] [inst_6 : CategoryTheory.Limits.HasLimit K₁]
  [inst_7 : CategoryTheory.Limits.HasLimit K₂] (j : J₁ × J₂) {Z : C}
  (h :
    (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)).obj j ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesLimit₂.isoLimitUncurryWhiskeringLeft₂ K₁ K₂ G).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limit.π
          (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G)) j)
        h) =
    CategoryTheory.CategoryStruct.comp
      ((G.map (CategoryTheory.Limits.limit.π K₁ j.1)).app (CategoryTheory.Limits.limit K₂))
      (CategoryTheory.CategoryStruct.comp ((G.obj (K₁.obj j.1)).map (CategoryTheory.Limits.limit.π K₂ j.2)) h)