mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- A presheaf is a sheaf for a topology if it is a sheaf for every sieve in the topology.

If the given topology is given by a pretopology, `isSheaf_pretopology` shows it suffices to
check the sheaf condition at presieves in the pretopology.
 -/
CategoryTheory.Presieve.IsSheaf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.GrothendieckTopology C → CategoryTheory.Functor Cᵒᵖ (Type w) → Prop
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.instSemilatticeSup.eq_1 : ∀ {E : Type u_3} [inst : Group E], GroupNorm.instSemilatticeSup = Function.Injective.semilatticeSup DFunLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.ext_iff : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f g : S.LocalizationMap N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.CategoryTheory.Action.Continuous
CategoryTheory.Functor.mapContAction_obj_obj : ∀ {V : Type u_5} {W : Type u_6} [inst : CategoryTheory.Category.{v_2, u_5} V] {FV : V → V → Type u_7}
  {CV : V → Type u_8} [inst_1 : (X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
  [inst_2 : CategoryTheory.ConcreteCategory V FV] [inst_3 : CategoryTheory.HasForget₂ V TopCat]
  [inst_4 : CategoryTheory.Category.{v_3, u_6} W] {FW : W → W → Type u_9} {CW : W → Type u_10}
  [inst_5 : (X Y : W) → FunLike (FW X Y) (CW X) (CW Y)] [inst_6 : CategoryTheory.ConcreteCategory W FW]
  [inst_7 : CategoryTheory.HasForget₂ W TopCat] (G : Type u_11) [inst_8 : Monoid G] [inst_9 : TopologicalSpace G]
  (F : CategoryTheory.Functor V W) (H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
  (X : ContAction V G), ((CategoryTheory.Functor.mapContAction G F H).obj X).obj = (F.mapAction G).obj X.obj
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.costructuredArrowMapCocone_ι_app : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) (G : CategoryTheory.Functor D H) (α : F ⟶ L.comp G)
  (Y : D) (f : CategoryTheory.CostructuredArrow L Y),
  (L.costructuredArrowMapCocone F G α Y).ι.app f = CategoryTheory.CategoryStruct.comp (α.app f.left) (G.map f.hom)
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.emptyWithCapacity₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {c : ℕ}, Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.Data.Sign.Defs
SignType.enumList_getElem?_ctorIdx_eq : ∀ (x : SignType), SignType.enumList[x.ctorIdx]? = some x
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- `K.restrictionToTruncGE' e).f i` is an isomorphism when `¬ e.BoundaryGE i`.  -/
HomologicalComplex.isIso_restrictionToTruncGE' : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i : ι), ¬e.BoundaryGE i → CategoryTheory.IsIso ((K.restrictionToTruncGE' e).f i)
-- Lean.Data.Json.Parser
Lean.Json.Parser.natMaybeZero : Std.Internal.Parsec.String.Parser ℕ
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.exists_int_le_of_mk_nonneg : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : CommRing R] [inst_2 : IsStrictOrderedRing R] {x : R},
  0 ≤ ArchimedeanClass.mk x → ∃ n, ↑n ≤ x
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.mem_prehaar_empty : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] {K₀ : Set G} {f : TopologicalSpace.Compacts G → ℝ},
  f ∈ MeasureTheory.Measure.haar.haarProduct K₀ ↔
    ∀ (K : TopologicalSpace.Compacts G), f K ∈ Set.Icc 0 ↑(MeasureTheory.Measure.haar.index (↑K) K₀)
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_uIcc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Lattice (α i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a b : α i),
  Pi.single i '' Set.uIcc a b = Set.uIcc (Pi.single i a) (Pi.single i b)
-- Init.Data.SInt.Lemmas
ISize.ofInt_le_iff_le : ∀ {a b : ℤ},
  ISize.minValue.toInt ≤ a →
    a ≤ ISize.maxValue.toInt →
      ISize.minValue.toInt ≤ b → b ≤ ISize.maxValue.toInt → (ISize.ofInt a ≤ ISize.ofInt b ↔ a ≤ b)
-- Mathlib.Analysis.Convex.MetricSpace
/-- The convex combination `(t, p, q) ↦ t • p + (1 - t) • q` is continuous on `[0, 1] × X × X`
for a convex metric space `X`.  -/
Convexity.continuous_convexCombPair : ∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X],
  Continuous fun x => Convexity.convexCombPair (↑x.1) (1 - ↑x.1) ⋯ ⋯ ⋯ x.2.1 x.2.2
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- The underlying topological space of an object of `CompHausLike P`.  -/
CompHausLike.toTop : {P : TopCat → Prop} → CompHausLike P → TopCat
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.presburgerFunc.one : FirstOrder.presburgerFunc 0
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.mkMetric_toOuterMeasure : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (m : ENNReal → ENNReal),
  (MeasureTheory.Measure.mkMetric m).toOuterMeasure = MeasureTheory.OuterMeasure.mkMetric m
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_range_succ : ∀ {M : Type u_4} [inst : AddMonoid M] (f : ℕ → M) (n : ℕ),
  (List.map f (List.range n.succ)).sum = (List.map f (List.range n)).sum + f n
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.ApplyResult.goals.inj : ∀ {mvarIds mvarIds_1 : List Lean.MVarId},
  Lean.Meta.Sym.ApplyResult.goals mvarIds = Lean.Meta.Sym.ApplyResult.goals mvarIds_1 → mvarIds = mvarIds_1
-- Mathlib.Data.Finset.Pi
Finset.restrict₂_comp_restrict : ∀ {ι : Type u_2} {π : ι → Type u_3} {s t : Finset ι} (hst : s ⊆ t), Finset.restrict₂ hst ∘ t.restrict = s.restrict
-- Mathlib.Analysis.Normed.Group.Ultra
/-- Nonarchimedean norm of a sum is less than or equal the norm of any term in the
sum. This version is phrased using `Finset.sup'` and `Finset.Nonempty` due to `Finset.sup`
operating over an `OrderBot`, which `ℝ` is not.  -/
Finset.Nonempty.norm_sum_le_sup'_norm : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedAddCommGroup M] [IsUltrametricDist M] {s : Finset ι} (hs : s.Nonempty)
  (f : ι → M), ‖∑ i ∈ s, f i‖ ≤ s.sup' hs fun x => ‖f x‖
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.isModuleConvexSpace_self : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R],
  Convexity.IsModuleConvexSpace R R
-- Mathlib.Algebra.Ring.Action.Pointwise.Set
Set.add_smul_subset : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : AddCommMonoid β] [inst_2 : Module α β] (a b : α)
  (s : Set β), (a + b) • s ⊆ a • s + b • s
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.join.eq_1 : ∀ (l : List String), String.join l = List.foldl (fun r s => r ++ s) "" l
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_insertEntry_le_minKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k : α} {v : β k} {l : List ((a : α) × β a)} (hl : Std.Internal.List.DistinctKeys l) {km kmi : α},
  Std.Internal.List.minKey? l = some km →
    (Std.Internal.List.minKey? (Std.Internal.List.insertEntry k v l)).get ⋯ = kmi → (compare kmi km).isLE = true
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.lie_apply : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (D₁ D₂ : LieDerivation R L L) (x : L), ⁅D₁, D₂⁆ x = D₁ (D₂ x) - D₂ (D₁ x)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodePi.match_1.splitter : (n : ℕ) →
  (motive : Fin (n + 1) → Sort u_1) →
    (x : Fin (n + 1)) →
      ((isLt : 0 < n + 1) → motive ⟨0, isLt⟩) → ((i : ℕ) → (hi : i + 1 < n + 1) → motive ⟨i.succ, hi⟩) → motive x
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.comp : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g h : L ≃+* L),
  modularCyclotomicCharacter.toFun n (g * h) =
    modularCyclotomicCharacter.toFun n g * modularCyclotomicCharacter.toFun n h
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.zero_qsmul : ∀ {M : Type u_2} [inst : AddCommGroup M] (x : DivisibleHull M), 0 • x = 0
-- Mathlib.Algebra.GroupWithZero.Units.Basic
zpow_eq_zero_iff : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} {n : ℤ}, n ≠ 0 → (a ^ n = 0 ↔ a = 0)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkTermElabAttribute : Lean.Name → IO (Lean.KeyedDeclsAttribute Lean.Elab.Term.TermElab)
-- Init.Data.List.Basic
List.lengthTR.eq_1 : ∀ {α : Type u_1} (as : List α), as.lengthTR = as.lengthTRAux 0
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.casesWithTrace : Lean.MVarId → Lean.Expr → Lean.Meta.Grind.GoalM (List Lean.MVarId)
-- Mathlib.Analysis.Polynomial.Basic
/-- **Alias** of `Polynomial.isBoundedUnder_abs_atTop_iff`. -/
Polynomial.abs_isBoundedUnder_iff : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun x => |Polynomial.eval x P|) ↔ P.degree ≤ 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isLeftKanExtension_iff_of_iso₂ : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L : CategoryTheory.Functor C D} {F₁ F₂ : CategoryTheory.Functor C H} {F₁' F₂' : CategoryTheory.Functor D H}
  (α₁ : F₁ ⟶ L.comp F₁') (α₂ : F₂ ⟶ L.comp F₂') (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂'),
  CategoryTheory.CategoryStruct.comp α₁ (L.whiskerLeft e'.hom) = CategoryTheory.CategoryStruct.comp e.hom α₂ →
    (F₁'.IsLeftKanExtension α₁ ↔ F₂'.IsLeftKanExtension α₂)
-- Mathlib.NumberTheory.LSeries.Convolution
toArithmeticFunction_congr : ∀ {R : Type u_1} [inst : Zero R] {f f' : ℕ → R},
  (∀ {n : ℕ}, n ≠ 0 → f n = f' n) → toArithmeticFunction f = toArithmeticFunction f'
-- Mathlib.Algebra.Lie.Basic
LieHom.coe_id : ∀ {R : Type u} {L₁ : Type v} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁], ⇑LieHom.id = id
-- Mathlib.Analysis.Distribution.TestFunction
/-- For every compact `K ⊆ Ω`, the inclusion map `𝓓^{n}_{K}(E, F) → 𝓓^{n}(Ω, F)` is
continuous. It is in fact a topological embedding, though this fact is not in Mathlib yet.  -/
TestFunction.continuous_ofSupportedIn : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E}
  (K_sub_Ω : ↑K ⊆ ↑Ω), Continuous (TestFunction.ofSupportedIn K_sub_Ω)
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normal_iff_normalClosure_le : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ IntermediateField.normalClosure F (↥K) L ≤ K
-- Mathlib.Data.PFun
PFun.res_univ : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), PFun.res f Set.univ = ↑f
-- Mathlib.Analysis.Normed.Group.Constructions
Pi.normedCommGroup.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → NormedCommGroup (G i)],
  Pi.normedCommGroup =
    { toNorm := Pi.seminormedGroup.toNorm, toGroup := Pi.seminormedGroup.toGroup, mul_comm := ⋯,
      toPseudoMetricSpace := Pi.seminormedGroup.toPseudoMetricSpace, eq_of_dist_eq_zero := ⋯, dist_eq := ⋯ }
-- Lean.Util.CollectAxioms
/-- Collect axioms reachable from constant `c`, using `extFind?` to look up pre-computed axioms
for imported declarations. Results are cached in `State.seen`.

When processing a constant not found in `extFind?` or the cache, the function temporarily
clears the axiom accumulator, recurses into the constant's dependencies, caches the result
in `seen`, and merges the collected axioms back.
 -/
_private.Lean.Util.CollectAxioms.0.Lean.CollectAxioms.collect : (Lean.Environment → Lean.Name → Option (Array Lean.Name)) → Lean.Name → Lean.CollectAxioms.M✝ Unit
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.mulLeft_toEquiv : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G] (c : G),
  (IsometryEquiv.mulLeft c).toEquiv = Equiv.mulLeft c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termI₁_1 : Lean.ParserDescr
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLE.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} (X Y : CategoryTheory.Subobject B) (h : X ≤ Y),
  X.ofLE Y h = X.ofLE Y h
-- Init.Data.SInt.Lemmas
Int16.toInt_lt : ∀ (x : Int16), x.toInt < 2 ^ 15
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.SpaceResult.space : Std.Format.SpaceResult✝ → ℕ
-- Init.Sym.DSimp.DSimprocDSL
/-- `match`-expression reduction.  -/
Lean.Parser.Sym.DSimp.reduceMatch : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.push_eq_append : ∀ {α : Type u_1} {a : α} {as : Array α}, as.push a = as ++ #[a]
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive false) → (Unit → motive true) → motive x
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isClosed_subsets_of_isClosed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {F : Set α}, IsClosed F → IsClosed {K | ↑K ⊆ F}
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instReflectsIsomorphismsAddCommMonCatForget₂LinearMapIdCarrierAddMonoidHomCarrier : ∀ {R : Type u} [inst : Semiring R], (CategoryTheory.forget₂ (SemimoduleCat R) AddCommMonCat).ReflectsIsomorphisms
-- Mathlib.FieldTheory.AbelRuffini
IsSolvableByRad.brecOn : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  {motive : (a : E) → IsSolvableByRad F a → Prop} {a : E} (t : IsSolvableByRad F a),
  (∀ (a : E) (t : IsSolvableByRad F a), IsSolvableByRad.below t → motive a t) → motive a t
-- Mathlib.Topology.Separation.SeparatedNhds
/-- **Alias** of the forward direction of `separatedNhds_iff_disjoint`. -/
SeparatedNhds.disjoint_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → Disjoint (nhdsSet s) (nhdsSet t)
-- Mathlib.Algebra.Group.Invertible.Basic
/-- Invertibility on either side of a monoid hom with a left-inverse is equivalent.  -/
invertibleEquivOfLeftInverse : {R : Type u_1} →
  {S : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        [inst : Monoid R] →
          [inst_1 : Monoid S] →
            [inst_2 : FunLike F R S] →
              [MonoidHomClass F R S] →
                [inst_4 : FunLike G S R] →
                  [MonoidHomClass G S R] →
                    (f : F) → (g : G) → (r : R) → Function.LeftInverse ⇑g ⇑f → Invertible (f r) ≃ Invertible r
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h : t.WF) {k₁ k₂ : α}
  (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.get k₁ h₁ = t.get k₂ ⋯
-- Mathlib.Data.Finmap
Finmap.union_cancel : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ s₃ : Finmap β},
  s₁.Disjoint s₃ → s₂.Disjoint s₃ → (s₁ ∪ s₃ = s₂ ∪ s₃ ↔ s₁ = s₂)
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_17 : HAdd Std.Time.Second.Offset Std.Time.Week.Offset Std.Time.Second.Offset
-- Std.Http.Internal.Char
/-- quoted-pair = "\\" ( HTAB / SP / VCHAR )
; ASCII-only variant (no obs-text).
 -/
Std.Http.Internal.Char.quotedPairChar : Char → Bool
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_ofPNatList : ∀ (l : List ℕ+) (h : ∀ p ∈ l, p.Prime), (PrimeMultiset.ofPNatList l h).prod = l.prod
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.revSkip?_cast : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.BackwardPattern pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos},
  (pos.cast hst).revSkip? pat = Option.map (fun x => x.cast hst) (pos.revSkip? pat)
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.prod_withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_2} {mβ : MeasurableSpace β}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : α → ENNReal} {g : β → ENNReal},
  Measurable f → Measurable g → (μ.withDensity f).prod (ν.withDensity g) = (μ.prod ν).withDensity fun z => f z.1 * g z.2
-- Init.Data.Vector.Range
Vector.find?_range'_eq_none : ∀ {s n : ℕ} {p : ℕ → Bool}, Vector.find? p (Vector.range' s n) = none ↔ ∀ (i : ℕ), s ≤ i → i < s + n → (!p i) = true
-- Init.Data.List.Basic
/-- Returns the index of the first element equal to `a`, or the length of the list if no element is
equal to `a`. The index is returned as a `Fin`, which guarantees that it is in bounds.

Examples:
 * `["carrot", "potato", "broccoli"].finIdxOf? "carrot" = some 0`
 * `["carrot", "potato", "broccoli"].finIdxOf? "broccoli" = some 2`
 * `["carrot", "potato", "broccoli"].finIdxOf? "tomato" = none`
 * `["carrot", "potato", "broccoli"].finIdxOf? "anything else" = none`
 -/
List.finIdxOf? : {α : Type u} → [BEq α] → α → (l : List α) → Option (Fin l.length)
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.cond.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.coe_of : ∀ (X : Type u) [inst : PartialOrder X], ↑{ carrier := X, str := inst } = X
-- Mathlib.Order.Filter.Basic
Filter.EventuallyLE.ge_iff_eq' : ∀ {α : Type u} {β : Type v} [inst : PartialOrder β] {l : Filter α} {f g : α → β}, g ≤ᶠ[l] f → (f ≤ᶠ[l] g ↔ f =ᶠ[l] g)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.category_comp_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Square C} (f : X.Hom Y) (g : Y.Hom Z),
  (CategoryTheory.CategoryStruct.comp f g).τ₄ = CategoryTheory.CategoryStruct.comp f.τ₄ g.τ₄
-- Std.Time.Date.Unit.Month
/-- Creates an `Offset` from a natural number.
 -/
Std.Time.Month.Offset.ofNat : ℕ → Std.Time.Month.Offset
-- Mathlib.Data.Finsupp.Single
Finsupp.single_eq_of_ne : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M}, a' ≠ a → (fun₀ | a => b) a' = 0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- Shorthand for the 0th group cohomology of a `k`-linear `G`-representation `A`, `H⁰(G, A)`,
defined as the 0th cohomology of the complex of inhomogeneous cochains of `A`.  -/
groupCohomology.H0 : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → Rep.{u, u, u} k G → ModuleCat k
-- Mathlib.SetTheory.Ordinal.Basic
/-- There exists a well-order on `α` whose order type is exactly `ord #α`.  -/
Cardinal.exists_ord_eq_type_lt : ∀ (α : Type u_1), ∃ x, ∃ (x_1 : WellFoundedLT α), (Cardinal.mk α).ord = Ordinal.type fun x1 x2 => x1 < x2