mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integralAgainstBilinLM_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂} {f : ContDiffMapSupportedIn E F₁ n K},
  (ContDiffMapSupportedIn.integralAgainstBilinLM B μ φ) f =
    if MeasureTheory.IntegrableOn φ (↑K) μ then ∫ (x : E), (B (f x)) (φ x) ∂μ else 0
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `add_tsub_assoc_of_le` for the equality.  -/
add_tsub_le_assoc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], a + b - c ≤ a + (b - c)
-- Init.Data.String.Lemmas.Slice
String.Slice.back?_eq_get? : ∀ {s : String.Slice}, s.back? = s.endPos.prev?.bind String.Slice.Pos.get?
-- Lean.Language.Basic
/-- Snapshot task of corresponding elaboration in previous document version if any, paired with its
old syntax to be considered for reuse. Should be set to `none` as soon as reuse can be ruled out.
 -/
Lean.Language.SnapshotBundle.old? : {α : Type} → Lean.Language.SnapshotBundle α → Option (Lean.Language.SyntaxGuarded (Lean.Language.SnapshotTask α))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
deriv_cosh : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → deriv (fun x => Real.cosh (f x)) x = Real.sinh (f x) * deriv f x
-- Init.SizeOf
Char.mk.sizeOf_spec : ∀ (val : UInt32) (valid : val.isValidChar), sizeOf { val := val, valid := valid } = 1 + sizeOf val + sizeOf valid
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_sSup : ∀ {α : Type u_2} [inst : TopologicalSpace α] {S : Set (TopologicalSpace.Opens α)}, ↑(sSup S) = ⋃ i ∈ S, ↑i
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.IsEquivalent.tendsto_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u v : α → β} {l : Filter α} {c : β},
  Asymptotics.IsEquivalent l u v → Filter.Tendsto u l (nhds c) → Filter.Tendsto v l (nhds c)
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.fg_of_noetherian : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [IsNoetherian R A]
  (S : Subalgebra R A), S.FG
-- Lean.Meta.Tactic.Intro
_private.Lean.Meta.Tactic.Intro.0.Lean.Meta.introNImp.loop : {σ : Type} →
  Lean.MVarId →
    (Lean.LocalContext → Lean.Name → Bool → σ → Lean.MetaM (Lean.Name × σ)) →
      ℕ → Lean.LocalContext → Array Lean.Expr → ℕ → σ → Lean.Expr → Lean.MetaM (Array Lean.Expr × Lean.MVarId)
-- Mathlib.Order.KrullDimension
Order.instKrullDimLEOfNatNatOfSubsingleton : ∀ {α : Type u_1} [inst : Preorder α] [Subsingleton α], Order.KrullDimLE 0 α
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false →
    (Std.DHashMap.Const.insertMany m l).getKeyD k fallback = m.getKeyD k fallback
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rio_eq_none_iff : ∀ {n i : ℕ}, (*...n).toList[i]? = none ↔ n ≤ i
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.eq_top_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {S : NonUnitalSubalgebra R A}, S = ⊤ ↔ ∀ (x : A), x ∈ S
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instIsAlwaysFiniteInt_1 : Std.Rxo.IsAlwaysFinite ℤ
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.sum : ∀ {Ω : Type u_1} {ι : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : Fintype ι] {E : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : MeasurableSpace E] [BorelSpace E]
  [SecondCountableTopology E] {X : ι → Ω → E},
  ProbabilityTheory.HasGaussianLaw (fun ω x => X x ω) P → ProbabilityTheory.HasGaussianLaw (∑ i, X i) P
-- Mathlib.Topology.Order.MonotoneConvergence
iSup_eq_of_tendsto : ∀ {α : Type u_3} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : CompleteLinearOrder α] [OrderTopology α]
  [Nonempty β] [inst_4 : SemilatticeSup β] {f : β → α} {a : α},
  Monotone f → Filter.Tendsto f Filter.atTop (nhds a) → iSup f = a
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.instForall : ∀ {ι : Type u_2} (G : ι → Type u_1) [inst : (i : ι) → Add (G i)] [∀ (i : ι), UniqueSums (G i)],
  UniqueSums ((i : ι) → G i)
-- Lean.Meta.WrapInstance
_private.Lean.Meta.WrapInstance.0.Lean.Meta.etaStructExpand? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.OfComp.map_iso_inv_app_assoc : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} (e : F.comp G ≅ H)
  [inst_3 : G.Full] [inst_4 : G.Faithful] {A : Type u_5} [inst_5 : AddMonoid A] [inst_6 : CategoryTheory.HasShift C A]
  [inst_7 : CategoryTheory.HasShift D A] [inst_8 : CategoryTheory.HasShift E A] [inst_9 : G.CommShift A]
  [inst_10 : H.CommShift A] (a : A) (X : C) {Z : E} (h : G.obj (F.obj ((CategoryTheory.shiftFunctor C a).obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.CommShift.OfComp.iso e a).inv.app X)) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G a).hom.app (F.obj X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor E a).map (e.hom.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso H a).inv.app X)
          (CategoryTheory.CategoryStruct.comp (e.inv.app ((CategoryTheory.shiftFunctor C a).obj X)) h)))
-- Mathlib.CategoryTheory.Preadditive.Schur
/-- In any preadditive category with kernels,
the endomorphisms of a simple object form a division ring.  -/
CategoryTheory.instDivisionRingEndOfHasKernelsOfSimple : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasKernels C] → {X : C} → [CategoryTheory.Simple X] → DivisionRing (CategoryTheory.End X)
-- Std.Net.Addr
Std.Net.instInhabitedIPv6Addr.default : Std.Net.IPv6Addr
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.centerToMulOpposite_symm_apply_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (r : ↥(Subsemigroup.center Rᵐᵒᵖ)),
  ↑(NonUnitalSubring.centerToMulOpposite.symm r) = MulOpposite.unop ↑r
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The isomorphism between `S` and the pullback of `S` w.r.t. the identity.  -/
CategoryTheory.GrothendieckTopology.Cover.pullbackId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        (S : J.Cover X) → S.pullback (CategoryTheory.CategoryStruct.id X) ≅ S
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- A subalgebra of `𝔸` that is closed topologically and under `ℚ`-scaling is closed under `exp`.  -/
NormedSpace.exp_mem : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸] {R : Type u_3}
  {S : Type u_4} [inst_3 : Monoid R] [inst_4 : SMul ℚ R] [inst_5 : MulAction R 𝔸] [inst_6 : Algebra ℚ 𝔸]
  [IsScalarTower ℚ R 𝔸] [inst_8 : SetLike S 𝔸] [SubsemiringClass S 𝔸] [SMulMemClass S R 𝔸] {s : S},
  IsClosed ↑s → ∀ {x : 𝔸}, x ∈ s → NormedSpace.exp x ∈ s
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.instProjectiveOppositeGenerator : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C],
  CategoryTheory.Projective (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.generator✝ F)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassPExcept_sub : ∀ (L : PeriodPair) (l₀ : ↥L.lattice) (z : ℂ),
  L.derivWeierstrassPExcept (↑l₀) z - 2 / (z - ↑l₀) ^ 3 = L.derivWeierstrassP z
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.coe_mk' : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal],
  ⇑(QuotientAddGroup.mk' N) = QuotientAddGroup.mk
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.mulVec_cons : ∀ {n : ℕ} {m' : Type uₘ} {α : Type u_1} [inst : NonUnitalCommSemiring α] (A : m' → Fin n.succ → α) (x : α)
  (v : Fin n → α),
  (Matrix.of A).mulVec (Matrix.vecCons x v) = x • Matrix.vecHead ∘ A + (Matrix.of (Matrix.vecTail ∘ A)).mulVec v
-- Init.Data.Range.Polymorphic.Nat
Std.instLawfulRcoIntersectionNat_6 : Std.Rio.LawfulRcoIntersection ℕ
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.psumPart_indiscrete : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] {n : ℕ},
  n ≠ 0 → MvPolynomial.psumPart σ R (Nat.Partition.indiscrete n) = MvPolynomial.psum σ R n
-- Mathlib.NumberTheory.Primorial
primorial_eq_prod_primesLE : ∀ (n : ℕ), primorial n = ∏ p ∈ n.primesLE, p
-- Init.Data.List.ControlImpl
_private.Init.Data.List.ControlImpl.0.List.flatMapMTR.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List (List β) → Sort u_3) (bs : List (List β))
  (h_1 : (bs : List (List β)) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_1 bs
-- Mathlib.Data.Part
Part.mod_mem_mod : ∀ {α : Type u_1} [inst : Mod α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma % mb ∈ a % b
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Preconnected.support_eq_univ : ∀ {V : Type u} [Nontrivial V] {G : SimpleGraph V}, G.Preconnected → G.support = Set.univ
-- Mathlib.Topology.Bases
/-- A nonempty separable space admits a sequence with dense range. Instead of running `cases` on the
conclusion of this lemma, you might want to use `TopologicalSpace.denseSeq` and
`TopologicalSpace.denseRange_denseSeq`.

If `α` might be empty, then `TopologicalSpace.exists_countable_dense` is the main way to use
separability of `α`.  -/
TopologicalSpace.exists_dense_seq : ∀ (α : Type u) [t : TopologicalSpace α] [TopologicalSpace.SeparableSpace α] [Nonempty α], ∃ u, DenseRange u
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.anyM.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- See Note [custom simps projection]  -/
CategoryTheory.CanonicallyOverClass.Simps.over : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (X S : C) → [CategoryTheory.CanonicallyOverClass X S] → X ⟶ S
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.pure.sizeOf_spec : ∀ (h : Lean.TSyntax `term), sizeOf (Lean.Parser.Tactic.MRefinePat.pure h) = 1 + sizeOf h
-- Mathlib.Order.Interval.Finset.Basic
/-- **Alias** of `Finset.Icc_sdiff_Ico_self`. -/
Finset.Icc_diff_Ico_self : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] {a b : α} [inst_2 : DecidableEq α],
  a ≤ b → Finset.Icc a b \ Finset.Ico a b = {b}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_diff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k fallback : α},
        (m₁.diff m₂).getKeyD k fallback = if m₂.contains k = true then fallback else m₁.getKeyD k fallback
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.hom_ext : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (P : StandardEtalePresentation R S) {f₁ f₂ : S →ₐ[R] T},
  f₁ P.x = f₂ P.x → f₁ = f₂
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk_mem_coboundaries_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (h : p + n = q) (p' : ℤ) (hp' : p' + 1 = p) (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0) (p'' : ℤ),
  p + 1 = p'' →
    (CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf ∈
        CochainComplex.HomComplex.coboundaries K ((CochainComplex.singleFunctor C q).obj X) n ↔
      ∃ g, CategoryTheory.CategoryStruct.comp (K.d p p'') g = f)
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.counitIso_inv_app_app : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  (X : CategoryTheory.Functor (CategoryTheory.SingleObj G) V) (X_1 : CategoryTheory.SingleObj G),
  (Action.FunctorCategoryEquivalence.counitIso.inv.app X).app X_1 = CategoryTheory.CategoryStruct.id (X.obj PUnit.unit)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.map_ΓIso_inv_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U : Y.Opens)
  {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.IsOpenImmersion.ΓIso f U).inv h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U) h
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A map is a homeomorphism iff it is continuous and has a continuous inverse.  -/
isHomeomorph_iff_exists_inverse : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f ↔ Continuous f ∧ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f ∧ Continuous g
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer
/-- If `n ≥ 5`, then the alternating group on `n` letters is perfect (subgroup version)  -/
commutator_alternatingGroup_eq_self : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  5 ≤ Nat.card α → ⁅alternatingGroup α, alternatingGroup α⁆ = alternatingGroup α
-- Mathlib.LinearAlgebra.Reflection
Module.eq_of_mapsTo_reflection_of_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} {y : M} {g : Module.Dual R M} [IsAddTorsionFree M] {Φ : Set M},
  Φ.Finite →
    f x = 2 →
      g y = 2 →
        g x = 2 →
          f y = 2 →
            Set.MapsTo (⇑(Module.preReflection x f)) Φ Φ → Set.MapsTo (⇑(Module.preReflection y g)) Φ Φ → y ∈ Φ → x = y
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M : SheafOfModules R} →
              (I : Type w) → (X : I → C) → J.CoversTop X → ((i : I) → (M.over (X i)).Presentation) → M.QuasicoherentData
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.natCast : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : StarRing R] (n : ℕ), IsSelfAdjoint ↑n
-- Mathlib.Data.Finset.Max
Finset.min'_lt_max' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) {i j : α} (H1 : i ∈ s), j ∈ s → i ≠ j → s.min' ⋯ < s.max' ⋯
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_append_append_append_eq_shiftLeft_setWidth_or : ∀ {w w' w'' w''' w'''' : ℕ} {b : BitVec w} {b' : BitVec w'} {b'' : BitVec w''} {b''' : BitVec w'''},
  BitVec.setWidth w'''' (b ++ b' ++ b'' ++ b''') =
    BitVec.setWidth w'''' b <<< (w' + w'' + w''') ||| BitVec.setWidth w'''' b' <<< (w'' + w''') |||
        BitVec.setWidth w'''' b'' <<< w''' |||
      BitVec.setWidth w'''' b'''
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.zero₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.zero₃._auto_1),
  CategoryTheory.CategoryStruct.comp ((X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h))
      (X.δ f g n₀ n₁ hn₁) =
    0
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.ext_iff : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {S T : L.Substructure M},
  S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
/-- A `SubMulAction` is finitely generated if it is the closure of a finite set.  -/
SubMulAction.FG : {R : Type u_1} → {M : Type u_2} → [inst : SMul R M] → SubMulAction R M → Prop
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetDecl.mk.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (binderName : Lean.Name) (type : Lean.Expr)
  (value : Lean.Compiler.LCNF.LetValue pu),
  sizeOf { fvarId := fvarId, binderName := binderName, type := type, value := value } =
    1 + sizeOf fvarId + sizeOf binderName + sizeOf type + sizeOf value
-- Batteries.Data.MLList.Basic
/-- Implementation of `MLList.ofArray`.  -/
_private.Batteries.Data.MLList.Basic.0.MLList.ofArray.go : {m : Type → Type} → {α : Type} → Array α → ℕ → MLList m α
-- Lean.Meta.AppBuilder
/-- Returns `eq_true h`  -/
Lean.Meta.mkEqTrue : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Topology.Category.TopCat.Yoneda
ContinuousMap.piComparison_fac : ∀ (Y : Type w') [inst : TopologicalSpace Y] {α : Type} (X : α → TopCat),
  (CategoryTheory.Limits.piComparison (ContinuousMap.yonedaPresheaf' Y) fun x => Opposite.op (X x)) =
    CategoryTheory.CategoryStruct.comp
      ((ContinuousMap.yonedaPresheaf' Y).map
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct X).inv
          (TopCat.sigmaIsoSigma X).inv.op))
      (CategoryTheory.CategoryStruct.comp (equivEquivIso (ContinuousMap.sigmaEquiv Y fun x => ↑(X x))).inv
        (CategoryTheory.Limits.Types.productIso fun i => C(↑(X i), Y)).inv)
-- Mathlib.Order.Filter.Bases.Basic
Filter.mem_prod_self_iff : ∀ {α : Type u_1} {la : Filter α} {s : Set (α × α)}, s ∈ la ×ˢ la ↔ ∃ t ∈ la, t ×ˢ t ⊆ s
-- Mathlib.SetTheory.Lists
Lists'.Subset.below.cons : ∀ {α : Type u_1} {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop}
  {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop} {a a' : Lists α} {l l' : Lists' α true} (a_1 : a.Equiv a')
  (a_2 : a' ∈ l'.toList) (a_3 : l.Subset l'), a_1.below → motive_1 a a' a_1 → a_3.below → motive_2 l l' a_3 → ⋯.below
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.Hom.isRingHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.RingObjCat C} (self : R₁.Hom R₂),
  CategoryTheory.IsRingHom self.hom
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.leadingCoeff_mul : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] (p q : Polynomial R),
  (p * q).leadingCoeff = p.leadingCoeff * q.leadingCoeff
-- Mathlib.Data.Finsupp.Basic
Finsupp.equivMapDomain_trans : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {M : Type u_5} [inst : Zero M] (f : α ≃ β) (g : β ≃ γ) (l : α →₀ M),
  Finsupp.equivMapDomain (f.trans g) l = Finsupp.equivMapDomain g (Finsupp.equivMapDomain f l)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.inner_nonneg_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsPositive → ∀ (x : E), 0 ≤ inner 𝕜 x (T x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.min?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : Min α]
  [inst_1 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.keys.min? = t.minKey?
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.strictColimitsOfShape_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] {Q : CategoryTheory.ObjectProperty C},
  P ≤ Q → P.strictColimitsOfShape J ≤ Q.strictColimitsOfShape J
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associator.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E],
  CategoryTheory.sum.associator C D E =
    ((CategoryTheory.Sum.inl_ C (D ⊕ E)).sum'
          ((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))).sum'
      ((CategoryTheory.Sum.inr_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))
-- Std.Http.Data.Status
Std.Http.Status.partialContent.sizeOf_spec : sizeOf Std.Http.Status.partialContent = 1
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : b ⟶ a) (g : c ⟶ a)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] {x : B} (h : x ⟶ c)
  [inst_2 : CategoryTheory.Bicategory.LanLift.CommuteWith f g h],
  (CategoryTheory.Bicategory.LanLift.CommuteWith.lanLiftCompIso f g h).hom =
    CategoryTheory.Bicategory.lanLiftDesc ((CategoryTheory.Bicategory.lanLiftLeftLift f g).whisker h)
-- Mathlib.CategoryTheory.Yoneda
/-- See also `yonedaEquiv_naturality'` for a more general version.  -/
CategoryTheory.yonedaEquiv_naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {F : CategoryTheory.Functor Cᵒᵖ (Type v₁)}
  (f : CategoryTheory.yoneda.obj X ⟶ F) (g : Y ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (F.map g.op)) (CategoryTheory.yonedaEquiv f) =
    CategoryTheory.yonedaEquiv (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map g) f)
-- Std.Http.Data.Request
/-- Creates a new HTTP TRACE Request builder with the specified URI.
 -/
Std.Http.Request.trace : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- There is a general version `le_zero_iff`, but this lemma does not require a `PartialOrder`.  -/
WithZero.nonpos_iff_eq_zero : ∀ {α : Type u_1} [inst : LE α] {x : WithZero α}, x ≤ 0 ↔ x = 0
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₂.eq_1 : ∀ (w x : UInt8),
  ByteArray.utf8DecodeChar?.assemble₂ w x =
    if ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = true then none
    else
      let r := ByteArray.utf8DecodeChar?.assemble₂Unchecked w x;
      if r < 128 then none else some { val := r, valid := ⋯ }