mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.SemaphoreState.mk : ℕ → Std.Queue (IO.Promise Unit) → Std.SemaphoreState✝
-- Mathlib.Data.Finset.Pairwise
Finset.pairwiseDisjoint_range_singleton : ∀ {α : Type u_1}, (Set.range singleton).PairwiseDisjoint id
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_subset_Iic_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ioo a b ⊆ Finset.Iic b
-- Mathlib.Topology.Constructions
continuous_subtype_val : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, Continuous Subtype.val
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α}, k ∉ t₂ → Std.ExtDTreeMap.Const.get? (t₁ ∩ t₂) k = none
-- Init.Data.Slice.Operations
/-- Folds a monadic operation from left to right over the elements in a slice.
An accumulator of type `β` is constructed by starting with `init` and monadically combining each
element of the slice with the current accumulator value in turn. The monad in question may permit
early termination or repetition.

Examples for the special case of subarrays:
```lean example
#eval #["red", "green", "blue"].toSubarray.foldlM (init := "") fun acc x => do
  let l ← Option.guard (· ≠ 0) x.length
  return s!"{acc}({l}){x} "
```
```output
some "(3)red (5)green (4)blue "
```
```lean example
#eval #["red", "green", "blue"].toSubarray.foldlM (init := 0) fun acc x => do
  let l ← Option.guard (· ≠ 5) x.length
  return s!"{acc}({l}){x} "
```
```output
none
```
 -/
Std.Slice.foldlM : {α : Type v} →
  {γ : Type u} →
    {β : Type v} →
      {δ : Type w} →
        {m : Type w → Type w'} →
          [Monad m] →
            (δ → β → m δ) →
              δ →
                [Std.ToIterator (Std.Slice γ) Id α β] →
                  [inst : Std.Iterator α Id β] → [Std.IteratorLoop α Id m] → Std.Slice γ → m δ
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremLike.setSymbols : {α : Type} → [self : Lean.Meta.Grind.TheoremLike α] → α → List Lean.HeadIndex → α
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- `Prod.map` of two affine maps.  -/
AffineMap.prodMap : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      {V2 : Type u_4} →
        {P2 : Type u_5} →
          {V3 : Type u_6} →
            {P3 : Type u_7} →
              {V4 : Type u_8} →
                {P4 : Type u_9} →
                  [inst : Ring k] →
                    [inst_1 : AddCommGroup V1] →
                      [inst_2 : Module k V1] →
                        [inst_3 : AddTorsor V1 P1] →
                          [inst_4 : AddCommGroup V2] →
                            [inst_5 : Module k V2] →
                              [inst_6 : AddTorsor V2 P2] →
                                [inst_7 : AddCommGroup V3] →
                                  [inst_8 : Module k V3] →
                                    [inst_9 : AddTorsor V3 P3] →
                                      [inst_10 : AddCommGroup V4] →
                                        [inst_11 : Module k V4] →
                                          [inst_12 : AddTorsor V4 P4] →
                                            (P1 →ᵃ[k] P2) → (P3 →ᵃ[k] P4) → P1 × P3 →ᵃ[k] P2 × P4
-- Mathlib.Data.ZMod.Basic
ZMod.instUniqueUnitsOfNatNat : Unique (ZMod 2)ˣ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating the second vector passed to `oangle` does not change twice the angle.  -/
Orientation.two_zsmul_oangle_neg_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), 2 • o.oangle x (-y) = 2 • o.oangle x y
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_one_eq_one_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] {A : Matrix n n α},
  A.hadamard 1 = 1 ↔ A.diag = 1
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tdiv_assoc' : ∀ (b : ℤ) {a c : ℤ}, c ∣ a → (a * b).tdiv c = a.tdiv c * b
-- Mathlib.ModelTheory.Algebra.Field.CharP
FirstOrder.Field.model_fieldOfChar_of_charP : ∀ {p : ℕ} {K : Type u_1} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K] [CharP K p],
  K ⊨ FirstOrder.Language.Theory.fieldOfChar p
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.subtypeVal.eq_1 : ∀ {β : Type u_3} [inst : SemilatticeSup β] [inst_1 : OrderBot β] {P : β → Prop} (Pbot : P ⊥)
  (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)),
  SupBotHom.subtypeVal Pbot Psup = { toSupHom := SupHom.subtypeVal Psup, map_bot' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.trace_kronecker : ∀ {α : Type u_3} {m : Type u_10} {n : Type u_11} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : Semiring α]
  (A : Matrix m m α) (B : Matrix n n α), (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B).trace = A.trace * B.trace
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_Ici_addNat : ∀ {n : ℕ} (m : ℕ) (i : Fin n), (fun x => x.addNat m) ⁻¹' Set.Ici (i.addNat m) = Set.Ici i
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.endsWith_char_eq_false_iff_get : ∀ {c : Char} {s : String}, s.endsWith c = false ↔ ∀ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ ≠ c
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.mapLe.congr_simp : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} (p p_1 : G.Walk u v),
  p = p_1 → SimpleGraph.Walk.mapLe h p = SimpleGraph.Walk.mapLe h p_1
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.mk.injEq : ∀ {V : Type u_1} {W : Type u_2} [inst : SeminormedAddCommGroup V] [inst_1 : SeminormedAddCommGroup W] (toFun : V → W)
  (map_add' : ∀ (v₁ v₂ : V), toFun (v₁ + v₂) = toFun v₁ + toFun v₂) (bound' : ∃ C, ∀ (v : V), ‖toFun v‖ ≤ C * ‖v‖)
  (toFun_1 : V → W) (map_add'_1 : ∀ (v₁ v₂ : V), toFun_1 (v₁ + v₂) = toFun_1 v₁ + toFun_1 v₂)
  (bound'_1 : ∃ C, ∀ (v : V), ‖toFun_1 v‖ ≤ C * ‖v‖),
  ({ toFun := toFun, map_add' := map_add', bound' := bound' } =
      { toFun := toFun_1, map_add' := map_add'_1, bound' := bound'_1 }) =
    (toFun = toFun_1)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.involute_mem_evenOdd_iff : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {x : CliffordAlgebra Q} {n : ZMod 2},
  CliffordAlgebra.involute x ∈ CliffordAlgebra.evenOdd Q n ↔ x ∈ CliffordAlgebra.evenOdd Q n
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_alter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {k k' fallback : α} {f : Option (β k) → Option (β k)},
  (m.alter k f).getKeyD k' fallback =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else fallback else m.getKeyD k' fallback
-- Mathlib.Analysis.Calculus.LHopital
HasDerivAt.lhopital_zero_atBot_on_Iio : ∀ {a : ℝ} {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ x ∈ Set.Iio a, HasDerivAt f (f' x) x) →
    (∀ x ∈ Set.Iio a, HasDerivAt g (g' x) x) →
      (∀ x ∈ Set.Iio a, g' x ≠ 0) →
        Filter.Tendsto f Filter.atBot (nhds 0) →
          Filter.Tendsto g Filter.atBot (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) Filter.atBot l → Filter.Tendsto (fun x => f x / g x) Filter.atBot l
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_add_int_mul_pi : ∀ (x : ℝ) (n : ℤ), Real.cos (x + ↑n * Real.pi) = (-1) ^ n * Real.cos x
-- Mathlib.GroupTheory.Archimedean
/-- If an additive subgroup of a linear ordered
additive commutative group is disjoint with the interval `Set.Ioo 0 a` for some positive `a`, then
this is a cyclic subgroup.  -/
AddSubgroup.cyclic_of_isolated_zero : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G]
  {H : AddSubgroup G} {a : G}, 0 < a → Disjoint (↑H) (Set.Ioo 0 a) → ∃ b, H = AddSubgroup.closure {b}
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_3.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it : Std.IterM m β}
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.pow_lt_top_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  {x : WithTop α} {n : ℕ} [inst_4 : Preorder α], x ^ n < ⊤ ↔ x < ⊤ ∨ n = 0
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.monic_prod_X_sub_C : ∀ {R : Type u} [inst : CommRing R] {α : Type u_1} (b : α → R) (s : Finset α),
  (∏ a ∈ s, (Polynomial.X - Polynomial.C (b a))).Monic
-- Mathlib.SetTheory.Lists
Lists.instInhabited : {α : Type u_1} → Inhabited (Lists α)
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_sup : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C),
  (P ⊔ Q).op = P.op ⊔ Q.op
-- Mathlib.Algebra.Quandle
ShelfHom.map_act : ∀ {S₁ : Type u_1} {S₂ : Type u_2} [inst : Shelf S₁] [inst_1 : Shelf S₂] (f : ShelfHom S₁ S₂) {x y : S₁},
  f (Shelf.act x y) = Shelf.act (f x) (f y)
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgHomClass.ext_topologicalClosure : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A]
  [inst_6 : StarModule R A] [inst_7 : IsSemitopologicalSemiring A] [inst_8 : ContinuousStar A]
  [inst_9 : TopologicalSpace B] [inst_10 : Semiring B] [inst_11 : Algebra R B] [inst_12 : StarRing B] [T2Space B]
  {F : Type u_4} {S : StarSubalgebra R A} [inst_14 : FunLike F (↥S.topologicalClosure) B]
  [AlgHomClass F R (↥S.topologicalClosure) B] [StarHomClass F (↥S.topologicalClosure) B] {φ ψ : F},
  Continuous ⇑φ →
    Continuous ⇑ψ → (∀ (x : ↥S), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x)) → φ = ψ
-- Mathlib.Topology.UniformSpace.Separation
SeparationQuotient.comap_mk_uniformity : ∀ {α : Type u} [inst : UniformSpace α],
  Filter.comap (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (uniformity (SeparationQuotient α)) = uniformity α
-- Mathlib.CategoryTheory.Localization.Construction
/-- The equivalence of categories `(W.Localization ⥤ D) ≌ (W.FunctorsInverting D)`
induced by the composition with `W.Q : C ⥤ W.Localization`.  -/
CategoryTheory.Localization.Construction.whiskeringLeftEquivalence : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (D : Type uD) →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] → CategoryTheory.Functor W.Localization D ≌ W.FunctorsInverting D
-- Mathlib.Algebra.Notation.Prod
Prod.vadd_snd : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : VAdd E α] [inst_1 : VAdd E β] (c : E) (p : α × β),
  (c +ᵥ p).2 = c +ᵥ p.2
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instSMulOfContinuousConstSMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] →
          {R : Type u_5} →
            [inst_3 : SMulZeroClass R β] → [ContinuousConstSMul R β] → SMul R (CompactlySupportedContinuousMap α β)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.toArray_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.InfinitelyUpwardEnumerable α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {lo hi : α},
  ((Std.PRange.succ lo)...=Std.PRange.succ hi).toArray = Array.map Std.PRange.succ (lo...=hi).toArray
-- Mathlib.Topology.Algebra.Valued.ValuedField
Valued.extension_extends : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
  (x : K), Valued.extension ↑x = Valued.v.restrict x
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.IsStableUnderSup.sup_mem_coverings : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.IsStableUnderSup]
  {X : C} {R S : CategoryTheory.Presieve X}, R ∈ J.coverings X → S ∈ J.coverings X → R ⊔ S ∈ J.coverings X
-- Mathlib.Data.Finset.Defs
/-- **Alias** of `Finset.setOfPred_mem`. -/
Finset.setOf_mem : ∀ {α : Type u_4} {s : Finset α}, {a | a ∈ s} = ↑s
-- Mathlib.Order.UpperLower.Closure
lowerClosure_min : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, s ⊆ t → IsLowerSet t → ↑(lowerClosure s) ⊆ t
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.div_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : One M] [inst_1 : One N] [inst_2 : DivisionMonoid P]
  (g₁ g₂ : OneHom N P) (f : OneHom M N), (g₁ / g₂).comp f = g₁.comp f / g₂.comp f
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.Products.evalFacProps : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] {l : Profinite.NobelingProof.Products I} (J K : I → Prop),
  (∀ a ∈ ↑l, J a) →
    ∀ [inst_1 : (j : I) → Decidable (J j)] [inst_2 : (j : I) → Decidable (K j)] (hJK : ∀ (i : I), J i → K i),
      ⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C J) l) ∘
          Profinite.NobelingProof.ProjRestricts C hJK =
        ⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C K) l)
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- Given two thresholds `p < q`, the sets `{x | v.limRatio ρ x < p}`
and `{x | q < v.limRatio ρ x}` are obviously disjoint. The key to proving that `v.limRatio ρ` is
almost everywhere measurable is to show that these sets have measurable supersets which are also
disjoint, up to zero measure. This is the content of this lemma.  -/
VitaliFamily.exists_measurable_supersets_limRatio : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {ρ : MeasureTheory.Measure α} [MeasureTheory.IsLocallyFiniteMeasure ρ],
  ρ.AbsolutelyContinuous μ →
    ∀ {p q : NNReal},
      p < q →
        ∃ a b,
          MeasurableSet a ∧
            MeasurableSet b ∧ {x | v.limRatio ρ x < ↑p} ⊆ a ∧ {x | ↑q < v.limRatio ρ x} ⊆ b ∧ μ (a ∩ b) = 0
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.newAtom : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  {map : Std.HashMap α ℕ} {a : α} {val : ℕ},
  Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map →
    ∀ (hlt : idx < decls.size),
      decls[idx] = Std.Sat.AIG.Decl.atom a →
        map[a]? = none → Std.Sat.AIG.RelabelNat.State.Inv2 decls (idx + 1) (map.insert a val)
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.compHahnSeries_coeff : ∀ {Γ : Type u_5} {Γ' : Type u_6} [inst : PartialOrder Γ] [inst_1 : PartialOrder Γ'] {R : Type u_7} [inst_2 : CommRing R]
  {U : Type u_8} {V : Type u_9} {W : Type u_10} [inst_3 : AddCommGroup U] [inst_4 : Module R U]
  [inst_5 : AddCommGroup V] [inst_6 : Module R V] [inst_7 : AddCommGroup W] [inst_8 : Module R W]
  (A : HVertexOperator Γ R V W) (B : HVertexOperator Γ' R U V) (u : U) (g' : Γ'),
  (A.compHahnSeries B u).coeff g' = A ((HVertexOperator.coeff B g') u)
-- Batteries.Data.List.Basic
List.tailsTR.go.eq_1 : ∀ {α : Type u_1} (acc : Array (List α)), List.tailsTR.go [] acc = acc.toListAppend [[]]
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instNegQ : {α : Type u} →
  [inst : Lean.Grind.CommSemiring α] →
    [Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)] → Neg (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.isSupported_one : ∀ {α : Type u} {s : Set α}, FreeCommRing.IsSupported 1 s
-- Mathlib.Algebra.Star.Subsemiring
StarSubsemiring.coe_copy : ∀ {R : Type v} [inst : NonAssocSemiring R] [inst_1 : StarRing R] (S : StarSubsemiring R) (s : Set R) (hs : s = ↑S),
  ↑(S.copy s hs) = s
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_ric_eq_mkSlice_rio : ∀ {α : Type u_1} {xs : Subarray α} {hi : ℕ},
  (Std.Ric.Sliceable.mkSlice xs *...=hi) = Std.Rio.Sliceable.mkSlice xs *...hi + 1
-- Mathlib.Probability.Moments.CovarianceBilinDual
/-- Continuous bilinear form with value `∫ x, L₁ x * L₂ x ∂μ` on `(L₁, L₂)`.
This is equal to the covariance only if `μ` is centered.  -/
ProbabilityTheory.uncenteredCovarianceBilinDual : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    {mE : MeasurableSpace E} →
      [inst_1 : NormedSpace ℝ E] →
        [OpensMeasurableSpace E] → MeasureTheory.Measure E → StrongDual ℝ E →L[ℝ] StrongDual ℝ E →L[ℝ] ℝ
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.mk.sizeOf_spec : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} [inst_2 : SizeOf J] [inst_3 : SizeOf C]
  (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt)
  (fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsLimit.fac._autoParam)
  (uniq :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (m : s.pt ⟶ t.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp m (t.π.app j) = s.π.app j) → m = lift s)
      CategoryTheory.Limits.IsLimit.uniq._autoParam),
  sizeOf { lift := lift, fac := fac, uniq := uniq } = 1
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toAlgHom_unop : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : Aᵐᵒᵖ ≃ₐ[R] Bᵐᵒᵖ), ↑(AlgEquiv.unop f) = AlgHom.unop ↑f
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))},
  CategoryTheory.uliftYonedaEquiv =
    {
      toFun := fun τ =>
        (CategoryTheory.ConcreteCategory.hom (τ.app (Opposite.op X)))
          { down := CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op X)) },
      invFun := fun x =>
        { app := fun Y => TypeCat.ofHom fun y => (CategoryTheory.ConcreteCategory.hom (F.map (Quiver.Hom.op y.down))) x,
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.mem_basicOpen : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ProjectiveSpectrum 𝒜),
  x ∈ ProjectiveSpectrum.basicOpen 𝒜 f ↔ f ∉ x.asHomogeneousIdeal
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_singleton_intCast : ∀ {R : Type uR} {A : Type uA} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (n : ℤ), R[↑n] = ⊥
-- Mathlib.CategoryTheory.Sites.Precoverage
CategoryTheory.Precoverage.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (coverings coverings_1 : (X : C) → Set (CategoryTheory.Presieve X)),
  ({ coverings := coverings } = { coverings := coverings_1 }) = (coverings = coverings_1)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} {l : List α} {k : α} {h : k ∈ Std.TreeMap.unitOfList l cmp},
  (Std.TreeMap.unitOfList l cmp)[k] = ()
-- Mathlib.CategoryTheory.Limits.VanKampen
_private.Mathlib.CategoryTheory.Limits.VanKampen.0.CategoryTheory.Limits.mapPair.match_1.eq_1 : ∀ (motive : CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair → Sort u_1)
  (h_1 : Unit → motive { as := CategoryTheory.Limits.WalkingPair.left })
  (h_2 : Unit → motive { as := CategoryTheory.Limits.WalkingPair.right }),
  (match { as := CategoryTheory.Limits.WalkingPair.left } with
    | { as := CategoryTheory.Limits.WalkingPair.left } => h_1 ()
    | { as := CategoryTheory.Limits.WalkingPair.right } => h_2 ()) =
    h_1 ()
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.sum_ne_zero_of_injOn_supDegree' : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A} [inst_3 : AddZeroClass A],
  (∃ i ∈ s, f i ≠ 0) → Set.InjOn (AddMonoidAlgebra.supDegree D ∘ f) ↑s → ∑ i ∈ s, f i ≠ 0
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {k a : α}, (m.erase k).get? a = if (k == a) = true then none else m.get? a
-- Std.Data.DTreeMap.Internal.Model
/-- Induction principle on `Impl` with an additional case split on `k ky` for
`Impl.inner _ ky _ _ _` without generalization.
 -/
Std.DTreeMap.Internal.Impl.tree_split_ind_no_gen : ∀ {α : Type u} {β : α → Type v} [Ord α] (k : α → Ordering) {motive : Std.DTreeMap.Internal.Impl α β → Prop},
  motive Std.DTreeMap.Internal.Impl.leaf →
    (∀ (n : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β),
        k ky = Ordering.lt → motive l → motive (Std.DTreeMap.Internal.Impl.inner n ky y l r)) →
      (∀ (n : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β),
          k ky = Ordering.eq → motive l → motive r → motive (Std.DTreeMap.Internal.Impl.inner n ky y l r)) →
        (∀ (n : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β),
            k ky = Ordering.gt → motive r → motive (Std.DTreeMap.Internal.Impl.inner n ky y l r)) →
          ∀ (t : Std.DTreeMap.Internal.Impl α β), motive t
-- Init.Data.List.Erase
List.eraseP_eq_eraseIdx : ∀ {α : Type u_1} {xs : List α} {p : α → Bool},
  List.eraseP p xs =
    match List.findIdx? p xs with
    | none => xs
    | some i => xs.eraseIdx i
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_eq : ∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (i j k : A) (h : i + j = k),
  CategoryTheory.shiftFunctorComm C i j =
    (CategoryTheory.shiftFunctorAdd' C i j k h).symm ≪≫ CategoryTheory.shiftFunctorAdd' C j i k ⋯
-- Mathlib.Data.Set.Card
/-- **Alias** of the reverse direction of `Set.ncard_pos`. -/
Set.Nonempty.ncard_pos : ∀ {α : Type u_1} {s : Set α}, autoParam s.Finite Set.ncard_pos._auto_1 → s.Nonempty → 0 < s.ncard
-- Std.Sat.AIG.Basic
Std.Sat.AIG.ExtendTarget.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} → {newWidth : ℕ} → (w : ℕ) → aig.RefVec w → aig.ExtendTarget newWidth
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.nsmul_nonneg : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.NatModule M] [Lean.Grind.OrderedAdd M]
  {k : ℕ} {a : M}, 0 ≤ a → 0 ≤ k • a
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.SignedMeasure.toMeasureOfLEZero_toSignedMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α)
  (hs : MeasureTheory.VectorMeasure.restrict s Set.univ ≤ MeasureTheory.VectorMeasure.restrict 0 Set.univ),
  (s.toMeasureOfLEZero Set.univ ⋯ hs).toSignedMeasure = -s