mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.ConstMulAction
HasCompactSupport.comp_smul : ∀ {α : Type u_2} {G₀ : Type u_4} [inst : TopologicalSpace α] [inst_1 : GroupWithZero G₀] [inst_2 : MulAction G₀ α]
  [ContinuousConstSMul G₀ α] {β : Type u_5} [inst_4 : Zero β] {f : α → β},
  HasCompactSupport f → ∀ {c : G₀}, c ≠ 0 → HasCompactSupport fun x => f (c • x)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Contravariant.MulLECancellable : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [MulLeftReflectLE α] {a : α}, MulLECancellable a
-- Mathlib.CategoryTheory.Sites.Continuous
/-- If `F` is continuous, any sheaf (in an arbitrary universe) remains a sheaf when
precomposing with `F.op` (SGA 4 III 1.5).  -/
CategoryTheory.Functor.op_comp_isSheaf_of_types : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [F.IsContinuous J K] (G : CategoryTheory.Sheaf K (Type t)),
  CategoryTheory.Presieve.IsSheaf J (F.op.comp G.obj)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The `1`-components as a function from the sigma type over `E.I₁ i₁ i₂`.  -/
CategoryTheory.PreOneHypercover.Y' : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S : C} → (E : CategoryTheory.PreOneHypercover S) → E.I₁' → C
-- Init.Data.String.Basic
String.Slice.Pos.cast.congr_simp : ∀ {s t : String.Slice} (pos pos_1 : s.Pos), pos = pos_1 → ∀ (h : s.copy = t.copy), pos.cast h = pos_1.cast h
-- Mathlib.Data.EReal.Basic
EReal.coe_add : ∀ (x y : ℝ), ↑(x + y) = ↑x + ↑y
-- Mathlib.Order.Basic
/-- Construct the trivial linear order on any type with at most one element.  -/
LinearOrder.ofSubsingleton : {α : Type u_5} → [Subsingleton α] → LinearOrder α
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.TransportEnrichment.eId_eq : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {W : Type v'} [inst_3 : CategoryTheory.Category.{w', v'} W]
  [inst_4 : CategoryTheory.MonoidalCategory W] (F : CategoryTheory.Functor V W) [inst_5 : F.LaxMonoidal]
  (X : CategoryTheory.TransportEnrichment F C),
  CategoryTheory.eId W X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map (CategoryTheory.eId V X))
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.toRingHom_mapDomainRingEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (e : M ≃* N),
  (MonoidAlgebra.mapDomainRingEquiv R e).toRingHom = MonoidAlgebra.mapDomainRingHom R ↑e
-- Mathlib.RingTheory.Radical.NatInt
Nat.primeFactors_radical : ∀ (n : ℕ), (UniqueFactorizationMonoid.radical n).primeFactors = n.primeFactors
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExBase.atom.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)} (id id_1 : ℕ),
  (Mathlib.Tactic.Ring.Common.ExBase.atom id = Mathlib.Tactic.Ring.Common.ExBase.atom id_1) = (id = id_1)
-- Mathlib.SetTheory.ZFC.Class
/-- A choice function on the class of nonempty ZFC sets.  -/
ZFSet.choice : ZFSet.{u} → ZFSet.{u}
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.symm_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), f.symm.symm = f
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `μ` is an s-finite measure, and `s ⊆ α × β` is measurable, then `y ↦ μ { x | (x, y) ∈ s }` is
a measurable function.  -/
measurable_measure_prodMk_right : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [MeasureTheory.SFinite μ] {s : Set (α × β)}, MeasurableSet s → Measurable fun y => μ ((fun x => (x, y)) ⁻¹' s)
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_lt_iff_of_compact : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [CompactSpace α]
  {f : BoundedContinuousFunction α β} {M : ℝ}, 0 < M → (‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.indicator_apply_eq_if : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : Zero R] {U : Set X} (f : LocallyConstant X R)
  (a : X) (hU : IsClopen U), (f.indicator hU) a = if a ∈ U then f a else 0
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equivFun_ofEquivFun : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] (e : M ≃ₗ[R] ι → R), (Module.Basis.ofEquivFun e).equivFun = e
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.ofList_eq_insertMany : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {l : List ((a : α) × β a)},
  Std.DTreeMap.Internal.Impl.ofList l = ↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)
-- Std.Http.Data.Status
Std.Http.Status.forbidden.sizeOf_spec : sizeOf Std.Http.Status.forbidden = 1
-- Mathlib.Algebra.Group.Defs
one_nsmul : ∀ {M : Type u_2} [inst : AddMonoid M] (a : M), 1 • a = a
-- Init.Data.Nat.Lemmas
Nat.not_succ_lt_self : ∀ {n : ℕ}, ¬n.succ < n
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh_hom_app_quotient_obj : ∀ (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]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_4 : c.QFactorsThroughHomotopy C]
  (K : HomologicalComplex C c) (i : ι),
  (HomologicalComplexUpToQuasiIso.homologyFunctorFactorsh C c i).hom.app ((HomotopyCategory.quotient C c).obj K) =
    CategoryTheory.CategoryStruct.comp
      ((HomologicalComplexUpToQuasiIso.homologyFunctor C c i).map
        ((HomologicalComplexUpToQuasiIso.quotientCompQhIso C c).hom.app K))
      (CategoryTheory.CategoryStruct.comp ((HomologicalComplexUpToQuasiIso.homologyFunctorFactors C c i).hom.app K)
        ((HomotopyCategory.homologyFunctorFactors C c i).inv.app K))
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.IterM.step_drop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : k.succ = 0 → motive 0) (h_2 : (k_1 : ℕ) → k.succ = k_1.succ → motive k_1.succ),
  (match h' : k.succ with
    | 0 => h_1 h'
    | k_1.succ => h_2 k_1 h') =
    h_2 k ⋯
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientQuotientEquivQuotient_mk_mk : ∀ {M : Type u_1} [inst : NonAssocSemiring M] (c d : RingCon M) (h : c ≤ d) (x : M),
  (c.quotientQuotientEquivQuotient d h) ⟦⟦x⟧⟧ = ⟦x⟧
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Functor.map_distinguished_op_exact : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {A : Type u_2} [inst_6 : CategoryTheory.Category.{v_2, u_2} A] [inst_7 : CategoryTheory.Abelian A]
  (F : CategoryTheory.Functor Cᵒᵖ A) [inst_8 : F.IsHomological] (T : CategoryTheory.Pretriangulated.Triangle C)
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  ((CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).op.map F).Exact
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
/-- **Alias** of the forward direction of `Subgroup.normal_unop`. -/
Subgroup.Normal.of_unop : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup Gᵐᵒᵖ}, H.unop.Normal → H.Normal
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- The canonical isomorphism `S.homology ≅ S.opcycles` when `S.g = 0`.  -/
CategoryTheory.ShortComplex.asIsoHomologyι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) → S.g = 0 → [inst_2 : S.HasHomology] → S.homology ≅ S.opcycles
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.nonsingular_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y : R),
  W'.Nonsingular x (W'.negY x y) ↔ W'.Nonsingular x y
-- Mathlib.Algebra.Star.LinearMap
/-- Given a matrix `A`, `A.toLin'` is self-adjoint (with respect to the intrinsic star)
iff all its elements are self-adjoint.  -/
Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff : ∀ {R : Type u_4} {m : Type u_5} {n : Type u_6} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] (A : Matrix n m R),
  IsSelfAdjoint (WithConv.toConv (Matrix.toLin' A)) ↔ ∀ (i : n) (j : m), IsSelfAdjoint (A i j)
-- Init.Data.SInt.Lemmas
Int16.toInt32_ofNat' : ∀ {n : ℕ}, ↑n ≤ Int16.maxValue.toInt → (Int16.ofNat n).toInt32 = Int32.ofNat n
-- Init.Data.Float.Model.Float32
/-- Converts an `Int16` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofInt16 : Int16 → Float32.Model
-- Mathlib.Tactic.Translate.Core
/-- The implementation of this function is based on `Meta.transform`.
We can't use `Meta.transform`, because that would cause the types of free variables to be
translated, which would create type-incorrect terms. Instead, we give the free variables
their original type and the translated type is only used when constructing the final term.  -/
_private.Mathlib.Tactic.Translate.Core.0.Mathlib.Tactic.Translate.applyReplacementFun.visit : Mathlib.Tactic.Translate.TranslateData → Lean.Expr → Mathlib.Tactic.Translate.ReplacementM Lean.Expr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.w_prod_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : D) (S' : D') (T : CategoryTheory.Functor C D)
  (T' : CategoryTheory.Functor C' D') {X Y : CategoryTheory.StructuredArrow (S, S') (T.prod T')} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp X.hom.1 (T.map (CategoryTheory.StructuredArrow.Hom.right f).1) = Y.hom.1
-- Mathlib.Tactic.ClickSuggestions.FindPremises
Mathlib.Tactic.ClickSuggestions.Choice.mk.inj : ∀ {rw grw app appAt rw_1 grw_1 app_1 appAt_1 : Bool},
  { rw := rw, grw := grw, app := app, appAt := appAt } = { rw := rw_1, grw := grw_1, app := app_1, appAt := appAt_1 } →
    rw = rw_1 ∧ grw = grw_1 ∧ app = app_1 ∧ appAt = appAt_1
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.toEquiv_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), ↑f.symm = (↑f).symm
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.State.mk.sizeOf_spec : ∀ (result? : Option Lean.Meta.AbstractMVarsResult) (generatorStack : Array Lean.Meta.SynthInstance.GeneratorNode)
  (resumeStack : Array (Lean.Meta.SynthInstance.ConsumerNode × Lean.Meta.SynthInstance.Answer))
  (tableEntries : Std.HashMap Lean.Expr Lean.Meta.SynthInstance.TableEntry),
  sizeOf
      { result? := result?, generatorStack := generatorStack, resumeStack := resumeStack,
        tableEntries := tableEntries } =
    1 + sizeOf result? + sizeOf generatorStack + sizeOf resumeStack + sizeOf tableEntries
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.instTransZagZigzag_1 : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    Trans (fun x1 x2 => CategoryTheory.Zag x1 x2) (fun x1 x2 => CategoryTheory.Zag x1 x2) fun x1 x2 =>
      CategoryTheory.Zigzag x1 x2
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.insert! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β},
  l.WF → (Std.DTreeMap.Internal.Impl.insert! k v l).WF
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_pos : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K)
  (w : NumberField.InfinitePlace K), 0 < ↑NumberField.mixedEmbedding.fundamentalCone.expMap x w
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.lift.eq_1 : ∀ {M : Type u_1} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass P] (c : AddCon M) (f : M →+ P)
  (H : c ≤ AddCon.ker f), c.lift f H = { toFun := fun x => AddCon.liftOn x ⇑f ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  (G : CategoryTheory.Functor C D) [G.IsCoverDense K] (ℱ : CategoryTheory.Sheaf K (Type u_5)) (X : D)
  {s t : ℱ.obj.obj (Opposite.op X)},
  (∀ ⦃Y : C⦄ (f : G.obj Y ⟶ X),
      (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map f.op)) s =
        (CategoryTheory.ConcreteCategory.hom (ℱ.obj.map f.op)) t) →
    s = t
-- Mathlib.Probability.Process.LocalProperty
ProbabilityTheory.IsLocalizingSequence.mk : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : TopologicalSpace ι]
  [inst_2 : OrderTopology ι] {𝓕 : MeasureTheory.Filtration ι mΩ} {τ : ℕ → Ω → WithTop ι}
  {P : autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.IsLocalizingSequence._auto_1},
  ProbabilityTheory.IsPreLocalizingSequence 𝓕 τ P →
    (∀ᵐ (ω : Ω) ∂P, Monotone fun x => τ x ω) → ProbabilityTheory.IsLocalizingSequence 𝓕 τ P
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (a : α) (b : β), (MeasureTheory.SimpleFunc.const α b) a = b
-- Mathlib.RingTheory.Ideal.Prime
Ideal.IsPrime.mk : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I ≠ ⊤ → (∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I) → I.IsPrime
-- Mathlib.Algebra.Lie.Abelian
LieModule.toLinearMap_maxTrivLinearMapEquivLieModuleHom : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (f : ↥(LieModule.maxTrivSubmodule R L (M →ₗ[R] N))),
  ↑(LieModule.maxTrivLinearMapEquivLieModuleHom f) = ↑f
-- Lean.Meta.Tactic.Grind.Theorems
_private.Lean.Meta.Tactic.Grind.Theorems.0.Lean.Meta.Grind.Theorems.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (smap : Lean.PHashMap Lean.Name (List α))
  (origins erased : Lean.PHashSet Lean.Meta.Grind.Origin) (omap : Lean.PHashMap Lean.Meta.Grind.Origin (List α)),
  sizeOf { smap := smap, origins := origins, erased := erased, omap := omap } =
    1 + sizeOf smap + sizeOf origins + sizeOf erased + sizeOf omap
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.eq_1 : ∀ (x y z : ℤ), PythagoreanTriple x y z = (x * x + y * y = z * z)
-- Mathlib.Geometry.Manifold.HasGroupoid
TopologicalSpace.Opens.chartAt_eq : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {s : TopologicalSpace.Opens M} {x : ↥s}, chartAt H x = (chartAt H ↑x).subtypeRestr ⋯
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
SubStarSemigroup.mk.injEq : ∀ {M : Type v} [inst : Mul M] [inst_1 : Star M] (toSubsemigroup : Subsemigroup M)
  (star_mem' : ∀ {a : M}, a ∈ toSubsemigroup.carrier → star a ∈ toSubsemigroup.carrier)
  (toSubsemigroup_1 : Subsemigroup M)
  (star_mem'_1 : ∀ {a : M}, a ∈ toSubsemigroup_1.carrier → star a ∈ toSubsemigroup_1.carrier),
  ({ toSubsemigroup := toSubsemigroup, star_mem' := star_mem' } =
      { toSubsemigroup := toSubsemigroup_1, star_mem' := star_mem'_1 }) =
    (toSubsemigroup = toSubsemigroup_1)
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.Total.mk.sizeOf_spec : ∀ {V : Type u} [inst : Quiver V] [inst_1 : SizeOf V] (left right : V) (hom : left ⟶ right),
  sizeOf { left := left, right := right, hom := hom } = 1 + sizeOf left + sizeOf right + sizeOf hom
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.attach_affineCombination_coe : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] (s : Finset P) (w : P → k),
  (Finset.affineCombination k s.attach Subtype.val) (w ∘ Subtype.val) = (Finset.affineCombination k s id) w
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- The integral of the derivative of a product of two maps.
Special case of `integral_deriv_mul_eq_sub_of_hasDeriv_right` where the functions have a
  one-sided derivative at the endpoints.  -/
intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivWithinAt : ∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  (∀ x ∈ Set.uIcc a b, HasDerivWithinAt u (u' x) (Set.uIcc a b) x) →
    (∀ x ∈ Set.uIcc a b, HasDerivWithinAt v (v' x) (Set.uIcc a b) x) →
      IntervalIntegrable u' MeasureTheory.volume a b →
        IntervalIntegrable v' MeasureTheory.volume a b →
          ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAt_iff_extract : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  pat ≠ "" →
    (String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ ↔
      s.copy.toByteArray.extract pos₁.offset.byteIdx pos₂.offset.byteIdx = pat.toByteArray)
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- An affine map on the result of adding a vector to a point produces
the same result as the linear map applied to that vector, added to the
affine map applied to that point.  -/
AffineMap.map_vadd : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [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] (f : P1 →ᵃ[k] P2) (p : P1) (v : V1), f (v +ᵥ p) = f.linear v +ᵥ f p
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
CompactlySupportedContinuousMap.monotone_of_nnreal : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal),
  Monotone ⇑Λ
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- A proof that `f` is meromorphic on `closedBall 0 R`.  -/
Complex.CanonicalDecomp.meromorphicOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : ℂ → E} {R : ℝ},
  Complex.CanonicalDecomp f g R → MeromorphicOn f (Metric.closedBall 0 R)
-- Init.Data.UInt.Basic
/-- Bitwise right shift for 8-bit unsigned integers. Usually accessed via the `>>>` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.shiftRight : UInt8 → UInt8 → UInt8
-- Mathlib.Data.Matrix.Reflection
Matrix.dotProductᵣ.eq_1 : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Add α] [inst_2 : Zero α] {m : ℕ} (a b : Fin m → α),
  Matrix.dotProductᵣ a b = FinVec.sum (FinVec.seq (FinVec.map (fun x1 x2 => x1 * x2) a) b)
-- Mathlib.Order.Lex
instInhabitedColex : (α : Type u_2) → [Inhabited α] → Inhabited (Colex α)
-- Lean.Server.References
/-- Parent declaration of the reference.  -/
Lean.Server.References.DocumentRefInfo.parentInfo? : Lean.Server.References.DocumentRefInfo → Option Lean.Server.References.ParentDecl
-- Mathlib.Order.Circular
sbtw_of_btw_not_btw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → ¬btw c b a → sbtw a b c
-- Mathlib.Data.Set.Card
Set.ncard_range_of_injective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → (Set.range f).ncard = Nat.card α
-- Mathlib.Analysis.Normed.Group.Quotient
Ideal.Quotient.normedAlgebra : {R : Type u_3} →
  [inst : SeminormedCommRing R] →
    (I : Ideal R) → (𝕜 : Type u_4) → [inst_1 : NormedField 𝕜] → [NormedAlgebra 𝕜 R] → NormedAlgebra 𝕜 (R ⧸ I)
-- Mathlib.Analysis.Fourier.ZMod
_private.Mathlib.Analysis.Fourier.ZMod.0.ZMod.auxDFT_neg : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E),
  (ZMod.auxDFT✝ fun j => Φ (-j)) = fun k => ZMod.auxDFT✝ Φ (-k)
-- Mathlib.Data.Option.Basic
Option.seq_some : ∀ {α β : Type u_5} {a : α} {f : α → β}, some f <*> some a = some (f a)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.liftingLift : {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] →
        {W : CategoryTheory.MorphismProperty C} →
          {E : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
              (F : CategoryTheory.Functor C E) →
                (hF : W.IsInvertedBy F) →
                  (L : CategoryTheory.Functor C D) →
                    [inst_3 : L.IsLocalization W] →
                      CategoryTheory.Localization.Lifting L W F (CategoryTheory.Localization.lift F hF L)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ιFunctorObj_extension : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  {πX : X ⟶ S}
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  {i : I} (t : A i ⟶ X) (b : B i ⟶ S),
  CategoryTheory.CommSq t (f i) πX b →
    ∃ l,
      CategoryTheory.CategoryStruct.comp (f i) l =
          CategoryTheory.CategoryStruct.comp t (CategoryTheory.SmallObject.ιFunctorObj f πX) ∧
        CategoryTheory.CategoryStruct.comp l (CategoryTheory.SmallObject.πFunctorObj f πX) = b
-- Init.Omega.IntList
Lean.Omega.IntList.get_of_length_le : ∀ {i : ℕ} {xs : Lean.Omega.IntList}, List.length xs ≤ i → xs.get i = 0
-- Mathlib.Topology.Order.Basic
pi_Ioc_mem_nhds : ∀ {ι : Type u_1} {X : ι → Type u_2} [Finite ι] [inst : (i : ι) → LinearOrder (X i)]
  [inst_1 : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), OrderTopology (X i)] {a b x : (i : ι) → X i} [Nonempty ι],
  (∀ (i : ι), a i < x i) → (∀ (i : ι), x i < b i) → Set.Ioc a b ∈ nhds x
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.norm_Integral_le_one : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E], ‖MeasureTheory.L1.SimpleFunc.integralCLM α E μ‖ ≤ 1
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.add_pf : ∀ {α : Type u_1} {a₁ a₂ b₁ b₂ : α} [inst : Add α], a₁ = b₁ → a₂ = b₂ → a₁ + a₂ = b₁ + b₂
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make an isomorphism in `P.Arrow Q X` from isomorphisms in `T` with compatibilities.  -/
CategoryTheory.MorphismProperty.Arrow.isoMk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q W : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        [inst_2 : W.IsMultiplicative] →
          [Q.RespectsIso] →
            [W.RespectsIso] →
              {A B : P.Arrow Q W} →
                (f : A.left ≅ B.left) →
                  (g : A.right ≅ B.right) →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp f.hom B.hom =
                          CategoryTheory.CategoryStruct.comp A.hom g.hom)
                        CategoryTheory.MorphismProperty.Arrow.isoMk._auto_1 →
                      (A ≅ B)