ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type u_1<VAR>inst✝² : NonUnitalNonAssocRing R<VAR>inst✝¹ : NonUnitalNonAssocRing S<VAR>inst✝ : NonUnitalNonAssocRing T<VAR>g : S →ₙ+* T<VAR>f : R →ₙ+* S<GOAL>NonUnitalSubring.map g f.range = (g.comp f).range
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>hh₂ : DifferentiableWithinAt 𝕜' h₂ s' (h x)<VAR>hh : DifferentiableWithinAt 𝕜 h s x<VAR>hs : MapsTo h s s'<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hy : y = h x<GOAL>derivWithin (h₂ ∘ h) s x = derivWithin h₂ s' (h x) * derivWithin h s x
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<GOAL>A ^ (-1) = A⁻¹
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A : M<GOAL>A = DivInvMonoid.zpow (↑(Nat.succ 0)) A
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>s : Set ι<VAR>x : ι<VAR>h : x ∉ s<GOAL>v x ∉ span R (v '' s)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>s : Set ι<VAR>x : ι<VAR>h : x ∉ s<VAR>h' : v x ∈ span R (v '' {x})<GOAL>v x ∉ span R (v '' s)
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>s : Set ι<VAR>x : ι<VAR>h : x ∉ s<VAR>h' : v x ∈ span R (v '' {x})<VAR>w : v x ∈ span R (v '' s)<GOAL>False
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>s : Set ι<VAR>x : ι<VAR>h : x ∉ s<VAR>h' : v x ∈ span R (v '' {x})<VAR>w : v x ∈ span R (v '' s)<GOAL>v x = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x✝ y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>s : Set ι<VAR>x : ι<VAR>h : x ∉ s<VAR>h' : v x ∈ span R (v '' {x})<VAR>w : v x ∈ span R (v '' s)<GOAL>Disjoint {x} s
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>u : ℕ → ℝ<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>u : ℕ → ℝ<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → ℝ → ℝ := fun n x => ↑((thickenedIndicator ⋯ {1}) x)<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>u : ℕ → ℝ<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → ℝ → ℝ := fun n x => ↑((thickenedIndicator ⋯ {1}) x)<VAR>vf_cont : ∀ (n : ℕ), Continuous (v n ∘ f)<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>u : ℕ → ℝ<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → ℝ → ℝ := fun n x => ↑((thickenedIndicator ⋯ {1}) x)<VAR>vf_cont : ∀ (n : ℕ), Continuous (v n ∘ f)<VAR>I : ∀ (ν : Measure G), IsFiniteMeasureOnCompacts ν → Tendsto (fun n => ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂ν))<VAR>M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ<VAR>I1 : Tendsto (fun n => ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'))<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>u : ℕ → ℝ<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → ℝ → ℝ := fun n x => ↑((thickenedIndicator ⋯ {1}) x)<VAR>vf_cont : ∀ (n : ℕ), Continuous (v n ∘ f)<VAR>I : ∀ (ν : Measure G), IsFiniteMeasureOnCompacts ν → Tendsto (fun n => ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂ν))<VAR>M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ<VAR>I1 : Tendsto (fun n => ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'))<VAR>J1 : ∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ' = ∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'.haarScalarFactor μ • μ<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>u : ℕ → ℝ<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → ℝ → ℝ := fun n x => ↑((thickenedIndicator ⋯ {1}) x)<VAR>vf_cont : ∀ (n : ℕ), Continuous (v n ∘ f)<VAR>I : ∀ (ν : Measure G), IsFiniteMeasureOnCompacts ν → Tendsto (fun n => ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂ν))<VAR>M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ<VAR>I1 : Tendsto (fun n => ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'))<VAR>J1 : ∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ' = ∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'.haarScalarFactor μ • μ<VAR>J2 : (μ' (f ⁻¹' {1})).toReal = ((μ'.haarScalarFactor μ • μ) (f ⁻¹' {1})).toReal<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>u : ℕ → ℝ<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → ℝ → ℝ := fun n x => ↑((thickenedIndicator ⋯ {1}) x)<VAR>vf_cont : ∀ (n : ℕ), Continuous (v n ∘ f)<VAR>I : ∀ (ν : Measure G), IsFiniteMeasureOnCompacts ν → Tendsto (fun n => ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂ν))<VAR>M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ<VAR>I1 : Tendsto (fun n => ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'))<VAR>J1 : ∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ' = ∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'.haarScalarFactor μ • μ<VAR>J2 : (μ' (f ⁻¹' {1})).toReal = ((μ'.haarScalarFactor μ • μ) (f ⁻¹' {1})).toReal<VAR>C : IsCompact (f ⁻¹' {1})<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>G : Type u_1<VAR>inst✝⁷ : TopologicalSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : TopologicalGroup G<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : BorelSpace G<VAR>μ' μ : Measure G<VAR>inst✝² : μ.IsHaarMeasure<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ'<VAR>inst✝ : μ'.IsMulLeftInvariant<VAR>f : G → ℝ<VAR>hf : Continuous f<VAR>h'f : HasCompactSupport f<VAR>u : ℕ → ℝ<VAR>u_mem : ∀ (n : ℕ), u n ∈ Ioo 0 1<VAR>u_lim : Tendsto u atTop (𝓝 0)<VAR>v : ℕ → ℝ → ℝ := fun n x => ↑((thickenedIndicator ⋯ {1}) x)<VAR>vf_cont : ∀ (n : ℕ), Continuous (v n ∘ f)<VAR>I : ∀ (ν : Measure G), IsFiniteMeasureOnCompacts ν → Tendsto (fun n => ∫ (x : G), v n (f x) ∂ν) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂ν))<VAR>M : ∀ (n : ℕ), ∫ (x : G), v n (f x) ∂μ' = ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ<VAR>I1 : Tendsto (fun n => ∫ (x : G), v n (f x) ∂μ'.haarScalarFactor μ • μ) atTop (𝓝 (∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'))<VAR>J1 : ∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ' = ∫ (x : G), {1}.indicator (fun x => 1) (f x) ∂μ'.haarScalarFactor μ • μ<VAR>J2 : μ' (f ⁻¹' {1}) = (μ'.haarScalarFactor μ • μ) (f ⁻¹' {1})<VAR>C : IsCompact (f ⁻¹' {1})<GOAL>μ' (f ⁻¹' {1}) = μ'.haarScalarFactor μ • μ (f ⁻¹' {1})
<VAR>α✝ α : Type u<VAR>inst✝² : Monoid α<VAR>a b : α<VAR>inst✝¹ : Invertible a<VAR>inst✝ : Invertible b<VAR>h : a = b<GOAL>⅟a = ⅟b
<VAR>α✝ α : Type u<VAR>inst✝² : Monoid α<VAR>a b : α<VAR>inst✝¹ : Invertible a<VAR>inst✝ : Invertible b<VAR>h : a = b<GOAL>a * ⅟b = 1
<VAR>f : ℕ → ℚ<VAR>H : IsCauSeq abs f<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>δ : ℚ<VAR>δ0 : 0 < δ<VAR>δε : ↑δ < ε<VAR>i : ℕ<VAR>hi : ∀ j ≥ i, |f j - f i| < δ<VAR>j : ℕ<VAR>ij : j ≥ i<GOAL>|↑(f j) - ↑(f i)| < ε
<VAR>Q : Type u_1<VAR>inst✝ : Quandle Q<VAR>x : Q<GOAL>x ◃⁻¹ x = x
<VAR>Q : Type u_1<VAR>inst✝ : Quandle Q<VAR>x : Q<GOAL>x ◃ x ◃⁻¹ x = x ◃ x
<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✝ f : R →+* S✝<VAR>S T : Subalgebra R A<GOAL>Algebra.IsIntegral R ↥(S ⊔ T) ↔ Algebra.IsIntegral R ↥S ∧ Algebra.IsIntegral R ↥T
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>a : Multiset α<VAR>i : Multiset (Multiset α)<VAR>l : List (Multiset α)<GOAL>(sum ⟦l⟧).Disjoint a ↔ ∀ b ∈ ⟦l⟧, b.Disjoint a
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a✝ : α<VAR>f g : α → β<VAR>a : Multiset α<VAR>i : Multiset (Multiset α)<VAR>l : List (Multiset α)<GOAL>l.sum.Disjoint a ↔ ∀ b ∈ ↑l, b.Disjoint a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>W : Submodule R (Dual R M)<GOAL>W.quotDualCoannihilatorToDual.Nondegenerate
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>W : Submodule R (Dual R M)<GOAL>ker W.quotDualCoannihilatorToDual = ⊥ ∧ ker W.quotDualCoannihilatorToDual.flip = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>W : Submodule R (Dual R M)<VAR>this : AddCommGroup ↥W := inferInstance<GOAL>ker W.quotDualCoannihilatorToDual = ⊥ ∧ ker W.quotDualCoannihilatorToDual.flip = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup M'<VAR>inst✝ : Module R M'<VAR>W : Submodule R (Dual R M)<VAR>this : AddCommGroup ↥W := inferInstance<GOAL>Function.Injective ⇑W.quotDualCoannihilatorToDual ∧ Function.Injective ⇑W.quotDualCoannihilatorToDual.flip
<VAR>K : Type u_1<VAR>hK : NormedField K<VAR>h : IsNonarchimedean (sorryAx (K → ℝ) true)<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>Γ₀ : Type u_3<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>val : Valued L Γ₀<VAR>hv : v.RankOne<VAR>x y : L<GOAL>norm (x + y) ≤ max (norm x) (norm y)
<VAR>K : Type u_1<VAR>hK : NormedField K<VAR>h : IsNonarchimedean (sorryAx (K → ℝ) true)<VAR>L : Type u_2<VAR>inst✝¹ : Field L<VAR>Γ₀ : Type u_3<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>val : Valued L Γ₀<VAR>hv : v.RankOne<VAR>x y : L<GOAL>v (x + y) ≤ v x ∨ v (x + y) ≤ v y
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<GOAL>l ~ replicate n a ↔ l = replicate n a
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>l : List α<VAR>p : l ~ replicate n a<GOAL>l.length = n ∧ ∀ (b : α), b ∈ l → b = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → ℚ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>(∑ a ∈ s, f a).toNNRat = ∑ a ∈ s, (f a).toNNRat
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>s : Finset α<VAR>f : α → ℚ<VAR>hf : ∀ a ∈ s, 0 ≤ f a<GOAL>∑ i ∈ s, f i = ∑ a ∈ s, ↑(f a).toNNRat
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>n : ℤ<VAR>m : ℕ<GOAL>↑(n ^ m) = ↑n ^ m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a b : α<GOAL>(cmp a b).Compares a b
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁶ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommSemiring N<VAR>inst✝² : Algebra R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>p : MvPolynomial σ R<GOAL>(algebraTensorAlgEquiv R A) (a ⊗ₜ[R] p) = a • (map (algebraMap R A)) p
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>σ : Type u_1<VAR>inst✝⁶ : DecidableEq σ<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : CommSemiring N<VAR>inst✝² : Algebra R N<VAR>A : Type u_3<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>p : MvPolynomial σ R<GOAL>(Algebra.ofId A (MvPolynomial σ A)) a * eval₂ (C.comp ↑(Algebra.ofId R A)) X p = C a * (map (algebraMap R A)) p
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>frontier (ball x r) = sphere x r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : EDist α<VAR>x y : α<VAR>s : Set α<GOAL>0 < s.infsep ↔ 0 < s.einfsep ∧ s.einfsep < ⊤
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>k : Type u_5<VAR>S : Type u_6<VAR>S₃ : Type u_7<VAR>T : Type u_8<VAR>M : Type u_9<VAR>M₁ : Type u_10<VAR>M₂ : Type u_11<VAR>M₃ : Type u_12<VAR>N₁ : Type u_13<VAR>N₂ : Type u_14<VAR>N₃ : Type u_15<VAR>ι : Type u_16<VAR>F : Type u_17<VAR>inst✝¹¹ : Semiring R<VAR>inst✝¹⁰ : Semiring S<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid M₁<VAR>inst✝⁷ : AddCommMonoid M₂<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M₂<VAR>inst✝³ : Module S M₃<VAR>σ : R →+* S<VAR>f : F<VAR>inst✝² : FunLike F M M₃<VAR>inst✝¹ : SemilinearMapClass F σ M M₃<VAR>σ' : S →+* R<VAR>inst✝ : RingHomInvPair σ σ'<VAR>c : S<VAR>x : M<GOAL>c • f x = f (σ' c • x)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J✝ J' : Ideal S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>x : R<GOAL>x ∈ map (RingHom.fst R S) (I.prod J) ↔ x ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J✝ J' : Ideal S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>x : R<GOAL>(∃ x_1 ∈ I.prod J, (RingHom.fst R S) x_1 = x) ↔ x ∈ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁷ : LinearOrderedField 𝕜<VAR>t : Finset (α × β × γ)<VAR>a a' : α<VAR>b b' : β<VAR>c c' : γ<VAR>x : α × β × γ<VAR>ε : 𝕜<VAR>inst✝⁶ : DecidableEq α<VAR>inst✝⁵ : DecidableEq β<VAR>inst✝⁴ : DecidableEq γ<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : Fintype γ<VAR>inst✝ : NoAccidental t<GOAL>((graph t).cliqueFinset 3).card = t.card
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>Measurable fun x => ν (Prod.mk x ⁻¹' s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>(fun s => Measurable fun x => ν (Prod.mk x ⁻¹' s)) ∅
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>∀ t ∈ image2 (fun x x_1 => x ×ˢ x_1) {s | MeasurableSet s} {t | MeasurableSet t}, (fun s => Measurable fun x => ν (Prod.mk x ⁻¹' s)) t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>∀ (t : Set (α × β)), MeasurableSet t → (fun s => Measurable fun x => ν (Prod.mk x ⁻¹' s)) t → (fun s => Measurable fun x => ν (Prod.mk x ⁻¹' s)) tᶜ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁶ : MeasurableSpace α<VAR>inst✝⁵ : MeasurableSpace α'<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace β'<VAR>inst✝² : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : IsFiniteMeasure ν<VAR>s : Set (α × β)<VAR>hs : MeasurableSet s<GOAL>∀ (f : ℕ → Set (α × β)), Pairwise (Disjoint on f) → (∀ (i : ℕ), MeasurableSet (f i)) → (∀ (i : ℕ), (fun s => Measurable fun x => ν (Prod.mk x ⁻¹' s)) (f i)) → (fun s => Measurable fun x => ν (Prod.mk x ⁻¹' s)) (⋃ i, f i)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i<GOAL>blimsup (fun i => cthickening (r i) (s i)) atTop p =ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i<GOAL>blimsup (fun i => cthickening (r i) (s i)) atTop p ≤ᶠ[ae μ] blimsup (fun i => thickening (r i) (s i)) atTop p
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>μ : Measure α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>inst✝ : IsUnifLocDoublingMeasure μ<VAR>p : ℕ → Prop<VAR>s : ℕ → Set α<VAR>r : ℕ → ℝ<VAR>hr : Tendsto r atTop (𝓝 0)<VAR>hr' : ∀ᶠ (i : ℕ) in atTop, p i → 0 < r i<GOAL>blimsup (fun i => thickening (r i) (s i)) atTop p ≤ blimsup (fun i => cthickening (r i) (s i)) atTop p
<VAR>p : ℝ<GOAL>(Summable fun n => ↑n ^ p) ↔ p < -1
<VAR>p : ℝ<GOAL>(Summable fun n => ↑n ^ (-p)) ↔ -p < -1
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>i j : ι<VAR>hij : v i = v j<VAR>l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1<GOAL>i = j
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : AddCommGroup M'<VAR>inst✝⁴ : AddCommGroup M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Nontrivial R<VAR>hv : LinearIndependent R v<VAR>i j : ι<VAR>hij : v i = v j<VAR>l : ι →₀ R := Finsupp.single i 1 - Finsupp.single j 1<VAR>h_total : (Finsupp.total ι M R v) l = 0<GOAL>i = j