mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.fun_finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι]
  {𝔸' : Type u_3} [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'}
  {f' : ι → 𝔸'},
  (∀ i ∈ u, HasDerivWithinAt (f i) (f' i) s x) →
    HasDerivWithinAt (fun x => ∏ i ∈ u, f i x) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) s x
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_inv : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (f : α →ₘ[μ] γ), ↑f⁻¹ =ᵐ[μ] (↑f)⁻¹
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.instInhabited : (V : Type u_1) → [inst : Quiver V] → Inhabited (V ⥤q V)
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.sub : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (f - g) a b
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_top_of_surjective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N),
  Function.Surjective ⇑f → AddSubgroup.map f ⊤ = ⊤
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.neg : ∀ {G : Type u_2} {α : Type u_3} [inst : Neg G] [inst_1 : MeasurableSpace G] [MeasurableNeg G] {m : MeasurableSpace α}
  {f : α → G} {μ : MeasureTheory.Measure α}, AEMeasurable f μ → AEMeasurable (-f) μ
-- Lean.ResolveName
_private.Lean.ResolveName.0.Lean.ResolveName.containsDeclOrReserved : Lean.Environment → Lean.Name → Bool
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomWhiskerRight_comp_assoc : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X X' X'' : C}
  (f : X ⟶ X') (f' : X' ⟶ X'') (Y : C) {Z : V} (h : (X ⟶[V] Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V (CategoryTheory.CategoryStruct.comp f f') Y) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V f' Y)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V f Y) h)
-- Mathlib.Probability.Martingale.Upcrossing
_private.Mathlib.Probability.Martingale.Upcrossing.0.MeasureTheory.upperCrossingTime.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.List.Lemmas
List.cons_head_tail : ∀ {α : Type u_1} {l : List α} (h : l ≠ []), l.head h :: l.tail = l
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The trifunctor `F - ⊗ (F - ⊗ F -)`.  -/
CategoryTheory.MonoidalCategory.curriedTensorPrePre' : {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] →
        [CategoryTheory.MonoidalCategory D] →
          CategoryTheory.Functor C D → CategoryTheory.Functor C (CategoryTheory.Functor C (CategoryTheory.Functor C D))
-- Mathlib.Algebra.Order.Group.Action.Synonym
Lex.instAddAction.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α],
  Lex.instAddAction = { toVAdd := Lex.instVAdd', add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Order.InitialSeg
/-- If `r` is a relation on `α` and `s` in a relation on `β`, then `f : r ≼i s` is an order
embedding whose `Set.range` is a lower set. That is, whenever `b < f a` in `β` then `b` is in the
range of `f`.  -/
InitialSeg : {α : Type u_4} → {β : Type u_5} → (α → α → Prop) → (β → β → Prop) → Type (max u_4 u_5)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote'_go_eq_denote : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly) (r : ℤ),
  Int.Internal.Linear.Poly.denote'.go ctx p r = Int.Internal.Linear.Poly.denote ctx p + r
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_eq_add_sum_sdiff_singleton_of_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] {s : Finset ι} {i : ι},
  i ∈ s → ∀ (f : ι → M), ∑ x ∈ s, f x = f i + ∑ x ∈ s \ {i}, f x
-- Std.Data.ExtTreeMap.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.ExtTreeMap.ofList : {α : Type u} →
  {β : Type v} →
    List (α × β) → (cmp : autoParam (α → α → Ordering) Std.ExtTreeMap.ofList._auto_1) → Std.ExtTreeMap α β cmp
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instInfSet.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M],
  SubAddAction.instInfSet = { sInf := fun S => { carrier := ⋂ s ∈ S, ↑s, vadd_mem' := ⋯ } }
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_subset_uIcc_iff_le : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a₁ a₂ b₁ b₂ : α},
  Finset.uIcc a₁ b₁ ⊆ Finset.uIcc a₂ b₂ ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mk'_toAddSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R}
  (ha : ↑sa = s), (Subsemiring.mk' s sm hm sa ha).toAddSubmonoid = sa
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.prodUnique_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Unique M₂] (a : M × M₂), LinearEquiv.prodUnique a = a.1
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
ModelWithCorners.contMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {n : WithTop ℕ∞},
  ContMDiff I (modelWithCornersSelf 𝕜 E) n ↑I
-- Mathlib.Topology.Homotopy.Contractible
id_nullhomotopic : ∀ (X : Type u_1) [inst : TopologicalSpace X] [ContractibleSpace X], (ContinuousMap.id X).Nullhomotopic
-- Lean.Elab.Tactic.Conv.Pattern
/-- Assuming `isReady` returned true, this adds the generated subgoal to the list
and advances to the next match.
 -/
Lean.Elab.Tactic.Conv.PatternMatchState.accept : Lean.MVarId → Lean.Elab.Tactic.Conv.PatternMatchState → Lean.Elab.Tactic.Conv.PatternMatchState
-- Mathlib.Order.Minimal
image_monotone_setOfPred_minimal_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ x ≤ y)) →
    f '' {x | Minimal (fun x => x ∈ s) x} = {x | Minimal (fun x => x ∈ f '' s) x}
-- Init.Data.Sum.Lemmas
Sum.map_id_id : ∀ {α : Type u_1} {β : Type u_2}, Sum.map id id = id
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)
-- Lean.Meta.Tactic.Refl
/-- Try to apply `eq_of_heq`. If successful, then return new goal, otherwise return `mvarId`.
 -/
Lean.MVarId.eqOfHEq : Lean.MVarId → Lean.MetaM Lean.MVarId
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow : ∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsFractionRing 𝒪 K] [inst_5 : IsDedekindDomain 𝒪] [CharZero 𝒪] [Module.Finite ℤ 𝒪] (L : Type u_3) (𝒪' : Type u_4)
  [inst_8 : Field L] [inst_9 : NumberField L] [inst_10 : CommRing 𝒪'] [inst_11 : Algebra 𝒪' L] [IsFractionRing 𝒪' L]
  [inst_13 : IsDedekindDomain 𝒪'] [CharZero 𝒪'] [inst_15 : Algebra K L] [inst_16 : Algebra 𝒪 𝒪'] [inst_17 : Algebra 𝒪 L]
  [IsScalarTower 𝒪 K L] [IsScalarTower 𝒪 𝒪' L] [inst_20 : Module.IsTorsionFree 𝒪 𝒪'] [inst_21 : Module.Free ℤ 𝒪']
  [Module.Finite ℤ 𝒪'] [Module.Finite 𝒪 𝒪'],
  (NumberField.discr L).natAbs = Ideal.absNorm (differentIdeal 𝒪 𝒪') * (NumberField.discr K).natAbs ^ Module.finrank K L
-- Mathlib.Topology.Constructions
/-- A map out of a sum type is continuous iff its restriction to each summand is.  -/
continuous_sigma_iff : ∀ {X : Type u} {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] [inst_1 : TopologicalSpace X]
  {f : Sigma σ → X}, Continuous f ↔ ∀ (i : ι), Continuous fun a => f ⟨i, a⟩
-- Mathlib.Testing.Plausible.Functions
Plausible.TotalFunction.zeroDefaultSupp.eq_1 : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : Zero β] [inst_2 : DecidableEq β] (A : List ((_ : α) × β))
  (a : β),
  (Plausible.TotalFunction.withDefault A a).zeroDefaultSupp =
    (List.map Sigma.fst (List.filter (fun ab => decide (ab.snd ≠ 0)) A.dedupKeys)).toFinset
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.prod_add : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] (a b : Associates.FactorSet α), (a + b).prod = a.prod * b.prod
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.mono : ∀ {α : Type u_2} {β : Type u_4} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : One β] [inst_2 : One γ] {f : α → β}
  {f' : α → γ}, HasCompactMulSupport f → Function.mulSupport f' ⊆ Function.mulSupport f → HasCompactMulSupport f'
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.forIn_filterWithPostcondition : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {o : Type u_1 → Type u_4} {α β γ : Type u_1} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Monad o] [LawfulMonad o] [inst_6 : MonadLiftT m n]
  [LawfulMonadLiftT m n] [inst_8 : MonadLiftT n o] [LawfulMonadLiftT n o] [inst_10 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_12 : Std.IteratorLoop α m o] [Std.LawfulIteratorLoop α m o] {it : Std.IterM m β}
  {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} {init : γ} {g : β → γ → o (ForInStep γ)},
  forIn (Std.IterM.filterWithPostcondition f it) init g =
    forIn it init fun out acc => do
      let __do_lift ← liftM (f out).run
      if __do_lift.down = true then g out acc else pure (ForInStep.yield acc)
-- Mathlib.Analysis.Calculus.FDeriv.Prod
hasStrictFDerivAt_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F},
  HasStrictFDerivAt Prod.fst (ContinuousLinearMap.fst 𝕜 E F) p
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.iff_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {x : TopologicalSpace Y} [DiscreteTopology Y] (f : X → Y),
  IsLocallyConstant f ↔ Continuous f
-- Mathlib.Order.Filter.Basic
Filter.Eventually.frequently : ∀ {α : Type u} {f : Filter α} [f.NeBot] {p : α → Prop}, (∀ᶠ (x : α) in f, p x) → ∃ᶠ (x : α) in f, p x
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.interedges_empty_left : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (t : Finset α), G.interedges ∅ t = ∅
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.IsOrdering.mk : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} [toHasMemOrNegMem : HasMemOrNegMem P]
  [toIsPrime : P.support.IsPrime], P.IsOrdering
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instInvOneClass.eq_1 : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : InvOneClass G] [inst_2 : ContinuousInv G],
  SeparationQuotient.instInvOneClass =
    { toOne := SeparationQuotient.instOne, toInv := SeparationQuotient.instInv, inv_one := ⋯ }
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.boundary_disjointUnion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_5} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'],
  ModelWithCorners.boundary (M ⊕ M') = Sum.inl '' ModelWithCorners.boundary M ∪ Sum.inr '' ModelWithCorners.boundary M'
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- If `G` acts on `X` with trivial stabilizers, `X` is equivalent
to the product of the quotient of `X` by `G` and `G`.
See `MulAction.selfEquivOrbitsQuotientProd` with `φ = Quotient.out`.  -/
MulAction.selfEquivOrbitsQuotientProd' : {G : Type u} →
  {X : Type v} →
    [inst : Group G] →
      [inst_1 : MulAction G X] →
        {φ : Quotient (MulAction.orbitRel G X) → X} →
          Function.LeftInverse Quotient.mk'' φ →
            (∀ (b : X), MulAction.stabilizer G b = ⊥) → X ≃ Quotient (MulAction.orbitRel G X) × G
-- Mathlib.NumberTheory.Primorial
primorial_add_le : ∀ {m n : ℕ}, n ≤ m → primorial (m + n) ≤ primorial m * (m + n).choose m
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.tendsto_harmonic_sub_log_add_one : Filter.Tendsto (fun n => ↑(harmonic n) - Real.log (↑n + 1)) Filter.atTop (nhds Real.eulerMascheroniConstant)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α}, (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.sSup_def : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R A)), sSup S = Algebra.adjoin R (⋃₀ (SetLike.coe '' S))
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHomLeft_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d d' : D} (f : d ⟶ d') (c : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f.op (Opposite.op c) =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c)
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.InftyValuation.map_mul'`. -/
FunctionField.InftyValuation.map_mul' : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] (x y : RatFunc F),
  RatFunc.inftyValuationDef F (x * y) = RatFunc.inftyValuationDef F x * RatFunc.inftyValuationDef F y
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_apply : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (I : Ideal S),
  (Ideal.relNorm R) I = Ideal.span (⇑(Algebra.intNorm R S) '' ↑I)
-- Mathlib.GroupTheory.Congruence.Hom
Con.ker.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_4} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N] (f : F), Con.ker f = { toSetoid := Setoid.ker ⇑f, mul' := ⋯ }
-- Mathlib.Order.Antisymmetrization
OrderIso.dualAntisymmetrization_symm_apply : ∀ (α : Type u_1) [inst : Preorder α] (a : α),
  (OrderIso.dualAntisymmetrization α).symm (toAntisymmetrization (fun x1 x2 => x1 ≤ x2) (OrderDual.toDual a)) =
    OrderDual.toDual (toAntisymmetrization (fun x1 x2 => x1 ≤ x2) a)
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_le_pow_iff_mem_span_pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ), ‖x‖ ≤ ↑p ^ (-↑n) ↔ x ∈ Ideal.span {↑p ^ n}
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- For `inv ≫ inv = 𝟙` see `inv_comp_inv`.  -/
CategoryTheory.GrpObj.inv_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.GrpObj A], CategoryTheory.inv CategoryTheory.GrpObj.inv = CategoryTheory.GrpObj.inv
-- Lean.LibrarySuggestions.Basic
_private.Lean.LibrarySuggestions.Basic.0.Lean.Expr.FoldRelevantConstantsImpl.State.mk : Lean.PtrSet Lean.Expr → Lean.NameHashSet → Lean.Expr.FoldRelevantConstantsImpl.State✝
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.Integrable.integrableOn : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.VectorMeasure X F} {f : X → E} {s : Set X},
  μ.Integrable f → μ.IntegrableOn f s
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.continuous_of_dominated : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} {Y : Type u_8}
  [inst_6 : TopologicalSpace Y] [FirstCountableTopology Y] {F_1 : Y → X → E} {bound : X → ℝ},
  (∀ (x : Y), MeasureTheory.AEStronglyMeasurable (F_1 x) μ.variation) →
    (∀ (x : Y), ∀ᵐ (a : X) ∂μ.variation, ‖F_1 x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ.variation →
        (∀ᵐ (a : X) ∂μ.variation, Continuous fun x => F_1 x a) → Continuous fun x => ∫ᵛ (a : X), F_1 x a ∂[B; μ]
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a `DivInvMonoid` if `β` is a `DivInvMonoid`.  -/
FunLike.divInvMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : Inv F] →
                [inst_5 : Div F] →
                  [inst_6 : Pow F ℤ] →
                    [inst_7 : DivInvMonoid β] →
                      [IsOneApply F α β] →
                        [IsMulApply F α β] →
                          [IsInvApply F α β] →
                            [IsDivApply F α β] → [IsPowApply ℕ F α β] → [IsPowApply ℤ F α β] → DivInvMonoid F
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.FunctionData.mk : Lean.LocalContext →
  Lean.LocalInstances →
    Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → Lean.Expr → Array ℕ → Mathlib.Meta.FunProp.FunctionData
-- Mathlib.CategoryTheory.Comma.Basic
/-- Composing `unopFunctor L R` with `(snd L R).op` is isomorphic to `fst L.op R.op`.  -/
CategoryTheory.Comma.unopFunctorCompSnd : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (CategoryTheory.Comma.unopFunctor L R).comp (CategoryTheory.Comma.snd R L).op ≅
                  CategoryTheory.Comma.fst L.op R.op
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.msgToInteractiveAux.go : Lean.NamingContext → Option Lean.MessageDataContext → Lean.MessageData → Lean.Widget.MsgFmtM✝ Std.Format
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.coe_toSupHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupBotHom α β),
  ⇑f.toSupHom = ⇑f
-- Init.Data.Iterators.Consumers.Monadic.Loop
Std.IteratorLoop.ext : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} {inst : Std.Iterator α m β} {n : Type x → Type x'}
  {x y : Std.IteratorLoop α m n}, Std.IteratorLoop.forIn = Std.IteratorLoop.forIn → x = y
-- Mathlib.Topology.Bornology.Basic
Bornology.IsBounded.insert : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded s → ∀ (x_1 : α), Bornology.IsBounded (insert x_1 s)
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_natDiv : ∀ {a b a' b' c : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' →
    Mathlib.Meta.NormNum.IsNat b b' → a'.div b' = c → Mathlib.Meta.NormNum.IsNat (a / b) c
-- Init.Data.UInt.Basic
/-- Bitwise exclusive or for 16-bit unsigned integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.xor : UInt16 → UInt16 → UInt16
-- Mathlib.Control.Monad.Cont
ReaderT.callCC : {m : Type u → Type v} →
  {ε : Type u} → [MonadCont m] → {α β : Type u} → (MonadCont.Label α (ReaderT ε m) β → ReaderT ε m α) → ReaderT ε m α
-- Mathlib.Data.FP.Basic
FP.ofRatDn : [C : FP.FloatCfg] → ℚ → FP.Float
-- Std.Http.Data.Body.Stream
Std.Http.Body.instTypeNameStream : TypeName Std.Http.Body.Stream
-- Lean.Compiler.IR.Basic
Lean.IR.instHashableVarId.hash : Lean.IR.VarId → UInt64
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.toSubmonoid_mono : ∀ {G : Type u_1} [inst : Group G], Monotone Subgroup.toSubmonoid
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntryD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : (a : α) × β a) →
          ((fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (x : (a : α) × β a) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l : Std.DTreeMap.Internal.Impl α β) →
                        (size_1 : ℕ) →
                          (k_1 : α) →
                            (v_1 : β k_1) →
                              (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                                (fallback : (a : α) × β a) →
                                  motive
                                    (Std.DTreeMap.Internal.Impl.inner size k v l
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                    fallback) →
                motive x x_1
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.adj_comm : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v w : V), G'.Adj v w ↔ G'.Adj w v
-- Lean.Meta.CongrTheorems
/-- The congr-simp theorems contains only one parameter for this kind of argument, and congr theorems contains two.
They correspond to arguments that are subsingletons/propositions.  -/
Lean.Meta.CongrArgKind.cast : Lean.Meta.CongrArgKind
-- Mathlib.NumberTheory.Height.MvPolynomial
/-- The ultrametric triangle inequality for finite sums.  -/
IsNonarchimedean.apply_sum_le : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : AddCommMonoid β] [inst_1 : FunLike F β ℝ] [NonnegHomClass F β ℝ]
  [ZeroHomClass F β ℝ] {v : F} {l : α → β}, IsNonarchimedean ⇑v → ∀ {s : Finset α}, v (∑ i ∈ s, l i) ≤ ⨆ i, v (l ↑i)
-- Mathlib.Topology.Maps.Basic
IsClosedMap.comap_nhdsSet_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsClosedMap f → Continuous f → ∀ (s : Set Y), Filter.comap f (nhdsSet s) = nhdsSet (f ⁻¹' s)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.kerLift_mk : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (φ : G →* H) (g : G), (QuotientGroup.kerLift φ) ↑g = φ g
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.assoc' : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            (i : a ⟶ d) →
              [CategoryTheory.BicategoricalCoherence i
                    (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))] →
                CategoryTheory.BicategoricalCoherence i
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h)