ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>a b : α<VAR>h0 : f 0 = 0<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>ha0 : ¬a = 0<VAR>hb0 : ¬b = 0<VAR>hf1 : ¬f 1 = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, Prime p
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>a b : α<VAR>h0 : f 0 = 0<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>ha0 : ¬a = 0<VAR>hb0 : ¬b = 0<VAR>hf1 : ¬f 1 = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>∀ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, ∀ q ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset, p ∣ q → p = q
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>a b : α<VAR>h0 : f 0 = 0<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>ha0 : ¬a = 0<VAR>hb0 : ¬b = 0<VAR>hf1 : ¬f 1 = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>∀ (p : α), p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b → Prime p
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁴ : CancelCommMonoidWithZero R<VAR>inst✝³ : UniqueFactorizationMonoid R<VAR>inst✝² : CancelCommMonoidWithZero α<VAR>inst✝¹ : UniqueFactorizationMonoid α<VAR>β : Type u_3<VAR>inst✝ : CancelCommMonoidWithZero β<VAR>f : α → β<VAR>a b : α<VAR>h0 : f 0 = 0<VAR>h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y<VAR>hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i<VAR>hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y<VAR>this✝¹ : DecidableEq α := Classical.decEq α<VAR>ha0 : ¬a = 0<VAR>hb0 : ¬b = 0<VAR>hf1 : ¬f 1 = 0<VAR>this✝ : Nontrivial α<VAR>this : NormalizationMonoid α := UniqueFactorizationMonoid.normalizationMonoid<GOAL>∀ (p : α), p ∈ normalizedFactors a ∨ p ∈ normalizedFactors b → ∀ (q : α), q ∈ normalizedFactors a ∨ q ∈ normalizedFactors b → p ∣ q → p = q
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{u_2, u_1} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝¹ : G.IsEquivalence<VAR>inst✝ : (F ⋙ G).IsEquivalence<GOAL>F.IsEquivalence
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>E : Type u_1<VAR>inst✝² : Category.{u_2, u_1} E<VAR>F : C ⥤ D<VAR>G : D ⥤ E<VAR>inst✝¹ : G.IsEquivalence<VAR>inst✝ : (F ⋙ G).IsEquivalence<GOAL>(F ⋙ G.asEquivalence.functor ⋙ G.asEquivalence.inverse).IsEquivalence
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>f : α → β<VAR>s : Set β<VAR>h : (f ⁻¹' s).Finite<VAR>hs : s ⊆ range f<GOAL>s.Finite
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>f : α → β<VAR>s : Set β<VAR>h : (f ⁻¹' s).Finite<VAR>hs : s ⊆ range f<GOAL>(f '' (f ⁻¹' s)).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>X Y Z : Pointed<VAR>f : X.Hom Y<VAR>g : Y.Hom Z<GOAL>(g.toFun ∘ f.toFun) X.point = Z.point
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r r' : ℝ≥0<VAR>hr : ↑r + ↑r' < p.radius<GOAL>Summable fun s => ‖p (s.fst + s.snd.fst)‖₊ * r ^ s.snd.fst * r' ^ s.fst
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r r' : ℝ≥0<VAR>hr : ↑r + ↑r' < p.radius<GOAL>Summable ((fun s => ‖p (s.fst + s.snd.fst)‖₊ * r ^ s.snd.fst * r' ^ s.fst) ∘ ⇑changeOriginIndexEquiv.symm)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r r' : ℝ≥0<VAR>hr : ↑r + ↑r' < p.radius<GOAL>Summable fun x => ‖p (x.fst - x.snd.card + x.snd.card)‖₊ * r ^ x.snd.card * r' ^ (x.fst - x.snd.card)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r r' : ℝ≥0<VAR>hr : ↑r + ↑r' < p.radius<VAR>this : ∀ (n : ℕ), HasSum (fun s => ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card)) (‖p n‖₊ * (r + r') ^ n)<GOAL>Summable fun x => ‖p (x.fst - x.snd.card + x.snd.card)‖₊ * r ^ x.snd.card * r' ^ (x.fst - x.snd.card)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r r' : ℝ≥0<VAR>hr : ↑r + ↑r' < p.radius<VAR>this : ∀ (n : ℕ), HasSum (fun s => ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card)) (‖p n‖₊ * (r + r') ^ n)<GOAL>Summable fun x => ∑' (y : Finset (Fin x)), ‖p (⟨x, y⟩.fst - ⟨x, y⟩.snd.card + ⟨x, y⟩.snd.card)‖₊ * r ^ ⟨x, y⟩.snd.card * r' ^ (⟨x, y⟩.fst - ⟨x, y⟩.snd.card)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r✝ R r r' : ℝ≥0<VAR>hr : ↑r + ↑r' < p.radius<VAR>this : ∀ (n : ℕ), HasSum (fun s => ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card)) (‖p n‖₊ * (r + r') ^ n)<GOAL>Summable fun x => ‖p x‖₊ * (r + r') ^ x
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>M₁ M₂ : Matroid α<GOAL>M₁ = M₂✶ ↔ M₂ = M₁✶
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>f : M ≃ₗ[R] M<VAR>g : N ≃ₗ[R] N<VAR>n : ℤ<GOAL>congr f g ^ n = congr (f ^ n) (g ^ n)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 1 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<GOAL>Mono (app' φ 2 ⋯)
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁ : Mono (app' φ 1 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<GOAL>∀ {P : C} (g : P ⟶ R₁.obj' 2 ⋯), g ≫ app' φ 2 ⋯ = 0 → g = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁✝ : Mono (app' φ 1 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>f₂ : A ⟶ R₁.obj' 2 ⋯<VAR>h₁ : f₂ ≫ app' φ 2 ⋯ = 0<GOAL>f₂ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁✝ : Mono (app' φ 1 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>f₂ : A ⟶ R₁.obj' 2 ⋯<VAR>h₁ : f₂ ≫ app' φ 2 ⋯ = 0<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<GOAL>f₂ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁✝ : Mono (app' φ 1 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>f₂ : A ⟶ R₁.obj' 2 ⋯<VAR>h₁ : f₂ ≫ app' φ 2 ⋯ = 0<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝ : Epi π₁<VAR>f₁ : A₁ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hf₁ : π₁ ≫ f₂ = f₁ ≫ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).f<GOAL>f₂ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁✝ : Mono (app' φ 1 ⋯)<VAR>h₃ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>f₂ : A ⟶ R₁.obj' 2 ⋯<VAR>h₁ : f₂ ≫ app' φ 2 ⋯ = 0<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝ : Epi π₁<VAR>f₁ : A₁ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<GOAL>f₂ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁✝ : Mono (app' φ 1 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>f₂ : A ⟶ R₁.obj' 2 ⋯<VAR>h₁ : f₂ ≫ app' φ 2 ⋯ = 0<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝ : Epi π₁<VAR>f₁ : A₁ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₃ : (f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<GOAL>f₂ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁✝ : Mono (app' φ 1 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>f₂ : A ⟶ R₁.obj' 2 ⋯<VAR>h₁ : f₂ ≫ app' φ 2 ⋯ = 0<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝¹ : Epi π₁<VAR>f₁ : A₁ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₃ : (f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝ : Epi π₂<VAR>g₀ : A₂ ⟶ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hg₀ : π₂ ≫ f₁ ≫ app' φ 1 ⋯ = g₀ ≫ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).f<GOAL>f₂ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁✝ : Mono (app' φ 1 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>f₂ : A ⟶ R₁.obj' 2 ⋯<VAR>h₁ : f₂ ≫ app' φ 2 ⋯ = 0<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝² : Epi π₁<VAR>f₁ : A₁ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₃ : (f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝¹ : Epi π₂<VAR>g₀ : A₂ ⟶ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hg₀ : π₂ ≫ f₁ ≫ app' φ 1 ⋯ = g₀ ≫ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).f<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝ : Epi π₃<VAR>f₀ : A₃ ⟶ R₁.obj' 0 ⋯<VAR>hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 ⋯<GOAL>f₂ = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>R₁ R₂ : ComposableArrows C 3<VAR>φ : R₁ ⟶ R₂<VAR>hR₁ : R₁.map' 0 2 ⋯ ⋯ = 0<VAR>hR₁' : (mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).Exact<VAR>hR₂ : (mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).Exact<VAR>h₀ : Epi (app' φ 0 ⋯)<VAR>h₁✝ : Mono (app' φ 1 ⋯)<VAR>h₃✝ : Mono (app' φ 3 ⋯)<VAR>A : C<VAR>f₂ : A ⟶ R₁.obj' 2 ⋯<VAR>h₁ : f₂ ≫ app' φ 2 ⋯ = 0<VAR>h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0<VAR>A₁ : C<VAR>π₁ : A₁ ⟶ A<VAR>w✝² : Epi π₁<VAR>f₁ : A₁ ⟶ ((mk₂ (R₁.map' 1 2 ⋯ ⋯) (R₁.map' 2 3 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)<VAR>h₃ : (f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0<VAR>A₂ : C<VAR>π₂ : A₂ ⟶ A₁<VAR>w✝¹ : Epi π₂<VAR>g₀ : A₂ ⟶ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).X₁<VAR>hg₀ : π₂ ≫ f₁ ≫ app' φ 1 ⋯ = g₀ ≫ ((mk₂ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).sc ⋯ 0 ⋯).f<VAR>A₃ : C<VAR>π₃ : A₃ ⟶ A₂<VAR>w✝ : Epi π₃<VAR>f₀ : A₃ ⟶ R₁.obj' 0 ⋯<VAR>hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 ⋯<VAR>h₄ : f₀ ≫ R₁.map' 0 1 ⋯ ⋯ = π₃ ≫ π₂ ≫ f₁<GOAL>f₂ = 0
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Semiring k<VAR>α : Type u_3<VAR>β : Type u_4<VAR>α₂ : Type u_5<VAR>inst✝⁴ : Semiring β<VAR>inst✝³ : One α<VAR>inst✝² : One α₂<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F α α₂<VAR>inst✝ : OneHomClass F α α₂<VAR>f : F<GOAL>mapDomain (⇑f) 1 = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : MeasurableSpace α<VAR>a : α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (a : α), f a ∂dirac a = f a
<VAR>f g : CircleDeg1Lift<GOAL>Tendsto (fun x => x - 1) atTop atTop
<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>S : Type v<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : Nontrivial S<VAR>f : R →+* S<VAR>p : R[X]<VAR>x : S<VAR>hx : eval₂ f x p = 0<VAR>hx' : eval₂ f x (derivative p) = 0<VAR>a b : R[X]<VAR>e : eval₂ f x (a * p + b * derivative p) = eval₂ f x 1<GOAL>False
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.4626, u_2} D<VAR>inst✝ : FinitaryPreExtensive C<VAR>W : C<GOAL>IsSheaf (extensiveTopology C) (yoneda.obj W)
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.4626, u_2} D<VAR>inst✝ : FinitaryPreExtensive C<VAR>W : C<GOAL>∀ {X : C}, ∀ R ∈ (extensiveCoverage C).covering X, IsSheafFor (yoneda.obj W) R
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_3, u_1} C<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.4626, u_2} D<VAR>inst✝ : FinitaryPreExtensive C<VAR>W X : C<VAR>R : Presieve X<VAR>Y : Type<VAR>α : Finite Y<VAR>Z : Y → C<VAR>π : (a : Y) → Z a ⟶ X<VAR>hR : R = ofArrows Z π<VAR>hi : IsIso (Sigma.desc π)<VAR>this✝ : IsIso (Sigma.desc (Cofan.mk X π).inj)<VAR>this : R.Extensive<GOAL>IsSheafFor (yoneda.obj W) R
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>P : ι → α → Prop<VAR>x✝ : α<GOAL>x✝ ∈ ⋃ i, {x | P i x} ↔ x✝ ∈ {x | ∃ i, P i x}
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : K<GOAL>liftAux (RingHom.id K) j p x = j x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : K<VAR>this : (Classical.choose ⋯).2 = x ^ p ^ (Classical.choose ⋯).1<GOAL>liftAux (RingHom.id K) j p x = j x
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<GOAL>∫⁻ (x : X), ↑(f x) ∂μ < ⊤
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<GOAL>∃ c, ∀ (x : X), ↑(f x) ≤ ↑c
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<VAR>x : X<GOAL>↑(f x) ≤ ↑(nndist f 0)
<VAR>X : Type u_1<VAR>inst✝³ : MeasurableSpace X<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : OpensMeasurableSpace X<VAR>μ : Measure X<VAR>inst✝ : IsFiniteMeasure μ<VAR>f : X →ᵇ ℝ≥0<VAR>x : X<VAR>key : f x ≤ nndist f 0<GOAL>↑(f x) ≤ ↑(nndist f 0)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>S : Finset M<GOAL>CompleteLattice.IsCompactElement (span R ↑S)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>S : Finset M<GOAL>CompleteLattice.IsCompactElement (⨆ x ∈ ↑S, span R {x})
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>S : Finset M<GOAL>CompleteLattice.IsCompactElement (⨆ x ∈ S, span R {x})
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>S : Finset M<GOAL>CompleteLattice.IsCompactElement (S.sup fun x => span R {x})
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a : ℤ<GOAL>(shiftAddHom K L n a) 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k✝ N : ℕ<VAR>x : Fin n → ℕ<VAR>k n✝¹ n✝ : ℕ<GOAL>(sphere (n✝¹ + 1) (n✝ + 1) k).card ≤ rothNumberNat ((2 * (n✝ + 1) - 1) ^ (n✝¹ + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k✝ N : ℕ<VAR>x : Fin n → ℕ<VAR>k n✝¹ n✝ : ℕ<GOAL>Fin (n✝¹ + 1) → ℕ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k✝ N : ℕ<VAR>x : Fin n → ℕ<VAR>k n✝¹ n✝ : ℕ<GOAL>∀ x ∈ image (⇑(map (2 * (n✝ + 1) - 1))) (sphere (n✝¹ + 1) (n✝ + 1) k), x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k✝ N : ℕ<VAR>x : Fin n → ℕ<VAR>k n✝¹ n✝ : ℕ<GOAL>Set.InjOn ⇑(map (2 * (n✝ + 1) - 1)) ↑(sphere (n✝¹ + 1) (n✝ + 1) k)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k✝ N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>k n✝¹ n✝ : ℕ<VAR>x : Fin (n✝¹ + 1) → ℕ<GOAL>x ∈ ↑(sphere (n✝¹ + 1) (n✝ + 1) k) → x ∈ {x | ∀ (i : Fin (n✝¹ + 1)), x i < 2 * (n✝ + 1) - 1}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k✝ N : ℕ<VAR>x✝ : Fin n → ℕ<VAR>k n✝¹ n✝ : ℕ<VAR>x : Fin (n✝¹ + 1) → ℕ<GOAL>(∀ (i : Fin (n✝¹ + 1)), x i < n✝ + 1) → ∑ i : Fin (n✝¹ + 1), x i ^ 2 = k → x ∈ {x | ∀ (i : Fin (n✝¹ + 1)), x i < n✝ + 1 + (n✝ + 1) - 1}
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>(map W' f).toJacobian.polynomialX = (MvPolynomial.map f) W'.polynomialX
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>hI : I.IsRadical<VAR>hJ : J.IsRadical<GOAL>(I ⊓ J).IsRadical
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>hI : I.IsRadical<VAR>hJ : J.IsRadical<GOAL>I.radical ⊓ J.radical ≤ I ⊓ J
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u : Multiset α<VAR>a b : α<VAR>s t : Multiset α<VAR>h : t ≤ s<GOAL>card (s - t) + card t = card s
<VAR>R : Type u_1<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing A✝<VAR>inst✝⁷ : Ring B✝<VAR>inst✝⁶ : CommRing S<VAR>inst✝⁵ : Algebra R A✝<VAR>inst✝⁴ : Algebra R B✝<VAR>f✝ : R →+* S<VAR>A : Type u_5<VAR>B : Type u_6<VAR>inst✝³ : Ring A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Algebra R B<VAR>f : A ≃ₐ[R] B<VAR>x : A<VAR>h : IsIntegral R (f x)<GOAL>IsIntegral R x
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.116671, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>opcyclesMap' e.hom h₁ h₂ ≫ opcyclesMap' e.inv h₂ h₁ = 𝟙 h₁.Q
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{?u.116671, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<GOAL>opcyclesMap' e.inv h₂ h₁ ≫ opcyclesMap' e.hom h₁ h₂ = 𝟙 h₂.Q
<VAR>b✝ x y a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>(logb (a * b) c)⁻¹ = (logb a c)⁻¹ + (logb b c)⁻¹
<VAR>b✝ x y a b : ℝ<VAR>h₁ : a ≠ 0<VAR>h₂ : b ≠ 0<VAR>c : ℝ<GOAL>logb c (a * b) = logb c a + logb c b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>s : Set α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>∫⁻ (x : α) in s, c ∂μ < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>s : Set α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ ⊤<GOAL>c * (μ.restrict s) univ < ⊤